Foundation Rscoupled Axis Coupled Axis

Coupled axes

A coupled axis is a finite set of positions, each with a fixed size, carrying a tag that says what kind of meaning the axis holds. In Recognition Science, a framework that derives structure from a ledger of recognition events, the tag is one of five recognition primitives: the cost function, the phi ladder, the sigma charge, the q3 lattice, or the gap-45 ceiling. The declaration CoupledAxis packages these three ingredients, a finite index type, a proof that its cardinality equals a given number n, and a primitive tag, into one object.

The central point is that two finite axes of the same cardinality are not automatically independent. In this framework they count as independent only when they are tagged by different recognition primitives. The definition independent states exactly that: two axes are independent precisely when their primitive tags differ. This matters because combining three independent axes of the same size n yields a product count of n cubed, a theorem proved in the machine-checked library of formal theorems, while three axes that share a tag do not qualify for that combination.

The framework proves two counting facts about such triples. If three axes are pairwise independent and each has size n, then the product of their cardinalities is n cubed, and the cardinality of their disjoint sum is three times n. Both are simple consequences of the size proofs carried inside each axis. The framework also defines a constant gap45, set to 45, as a complexity ceiling, but the declaration does not itself say what that ceiling means physically.

What CoupledAxis does not claim is just as important. It does not claim that any two axes with different tags are physically independent in the world; independence here is a formal condition about tags, not a statement about measurement. It does not claim that the five primitives are the only possible tags, only that these five are the ones used. It does not claim that the number 45 has any derived significance; it is a definitional choice, not a theorem. And it does not claim that a triple of independent axes exists for any n; the structure requires a proof that such axes can be constructed, which the declaration itself does not supply.

/-- 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

/-- The gap-45 complexity ceiling. -/
def gap45 : ℕ := 45

What this page does not claim

The declaration does not claim that different primitive tags imply physical independence in the world. The declaration does not claim that the five primitives are exhaustive or that gap45 has derived significance. The declaration does not claim that independent triples exist for any given n; it only structures them.

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: