Foundation Rscoupled Axis

Independence and counting

The classical picture of a coordinate axis is a line of positions, one for each number. Recognition Science keeps that picture but adds a label. A recognition axis, a finite set of positions that a recognition process can occupy, carries a tag saying which primitive kind of recognition gives it meaning. The framework defines exactly five such primitive tags: the cost function, the phi ladder, the sigma charge, the q3 lattice, and the gap-45 ceiling. A result in the machine-checked library proves that there are five primitives and no more.

The central definition is independence. Two axes of the same size are independent only when their tags differ. Two axes tagged by the same primitive are not automatically independent; they might be coupled, meaning their positions are not free to vary separately. This is a deliberate departure from raw set theory, where any two sets of the same cardinality are interchangeable. In the framework, the tag is part of the axis, so equal size alone does not buy independence.

The counting results are theorems. Take three axes, each with n positions, and require that every pair is independent. If you combine them by a tensor product, the theorem proves the total count is n × n × n. If instead you combine them by a disjoint sum, the theorem proves the total count is 3n. Both proofs are checked by the machine, with no axioms beyond the standard three.

In Recognition Science, this infrastructure supports the claim that three spatial dimensions are forced. The framework models space as three independent axes of the same size, and the counting theorems give the natural arithmetic for that model: n³ for a volume, 3n for a line of three segments. The physical bridge from recognition to actual space remains open, but the combinatorial skeleton is fixed.

theorem rsPrimitive_count : Fintype.card RSPrimitive = 5 := by
  decide

/-- RS-independence means the axes are carried by different primitives. -/
def independent {n m : ℕ} (A : CoupledAxis n) (B : CoupledAxis m) : Prop :=
  A.primitive ≠ B.primitive

/-- The tensor-product count of three same-size RS-independent axes is n^3. -/
theorem triple_card {n : ℕ} (T : RSIndependentTriple n) :
    tripleProductCard T = n * n * n := by
  unfold tripleProductCard
  rw [T.axis1.card_eq, T.axis2.card_eq, T.axis3.card_eq]

/-- Cardinality of the disjoint sum of three same-size RS-independent axes. -/
theorem disjoint_sum_card {n : ℕ} (S : RSDisjointSum3 n) :
    @Fintype.card S.axis1.Ix S.axis1.finite +
      @Fintype.card S.axis2.Ix S.axis2.finite +
      @Fintype.card S.axis3.Ix S.axis3.finite = 3 * n := by
  rw [S.axis1.card_eq, S.axis2.card_eq, S.axis3.card_eq]
  ring

What this page does not claim

The framework does not claim that three spatial dimensions are physically derived here; only the combinatorial counting theorems are proved. The module does not define what the five primitives mean physically beyond their names. Independence by different tags is a definitional choice, not a theorem about the physical world.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/RSCoupledAxis.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: