Foundation Rscoupled Axis Rsindependent Triple

The meaning of an independent triple

In mathematics, two sets of the same size are not automatically independent. Independence is a property that must be defined. The Recognition Science framework defines it through the concept of a recognition primitive, a basic kind of tagging that gives an axis its meaning. The framework's machine-checked library of formal theorems contains a structure called RSIndependentTriple, which captures the precise conditions under which three axes of equal size are independent.

The definition works as follows. An axis is a finite set of a given cardinality, tagged with one of five recognition primitives. These primitives are named jCost, phiLadder, sigmaCharge, q3Lattice, and gap45. Two axes are independent when they carry different primitives. An RSIndependentTriple is then a collection of three axes of the same size, where each pair is independent. This means all three axes must carry three different primitives; no two may share a tag.

The framework proves two consequences of this definition. For a triple of axes each of size n, the product of the three cardinalities is n³. For the disjoint sum of the three axes, the total cardinality is 3n. These are simple arithmetic facts that follow directly from the definition of independence. The theorems are checked by the machine, with no unproved assumptions.

In Recognition Science, this structure is infrastructure for combining results across different domains. The point is that two finite axes of the same size are not automatically independent; they count as independent only when tagged by different recognition primitives. This gives a formal way to combine three domains without accidental overlap. The definition itself does not say which primitives correspond to which physical or mathematical concepts, nor does it assert that such a triple exists for any particular size n. It only states what independence means and what its cardinality consequences are.

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

/-- Pairwise independent triple of same-size axes. -/
structure RSIndependentTriple (n : ℕ) where
  axis1 : CoupledAxis n
  axis2 : CoupledAxis n
  axis3 : CoupledAxis n
  indep12 : independent axis1 axis2
  indep13 : independent axis1 axis3
  indep23 : independent axis2 axis3

/-- 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 declaration does not assert that any particular triple of axes exists for any given size. The declaration does not say which recognition primitives correspond to which physical quantities. The declaration does not itself derive three spatial dimensions.

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: