Foundation Rscoupled Axis Triple Card

Counting independent axes

In mathematics, if you have three sets, each with n elements, the number of ordered triples you can form by picking one element from each is n × n × n, or n³. This is a basic counting principle, taught early in combinatorics. The Recognition Science framework formalizes a version of this idea in its machine-checked library of formal theorems, under the name triple_card.

The framework's version is not about arbitrary sets. It concerns what it calls coupled axes, which are finite lists of items tagged by one of five recognition primitives: the cost function, the golden-ratio ladder, the charge, the three-dimensional lattice, or the gap-45 ceiling. Two axes count as independent in this system only when they are tagged by different primitives. The theorem states that for three axes of the same size n, pairwise independent in this tagged sense, the product of their cardinalities equals n³.

The proof is a direct calculation: each axis has n elements by assumption, so multiplying the three counts gives n × n × n. The machine-checked proof, with zero axioms beyond the standard logical ones, confirms the arithmetic. The declaration also includes a companion result for disjoint sums: three independent axes of size n, taken together as separate piles, have a total of 3n elements, which is just addition.

In Recognition Science, this counting fact is infrastructure for cross-domain combination theorems. The framework models physical dimensions as such tagged axes, and independence between them is what allows their degrees of freedom to multiply rather than add. The triple_card theorem is the formal backbone for later claims about three-dimensional space, but it does not by itself assert anything about physical space. It is a statement about finite sets and their tags.

What the declaration does not claim is equally precise. It does not say that any three axes of the same size are independent; independence requires distinct primitive tags. It does not claim that the theorem applies to infinite axes or to continuous dimensions. It does not assert that the five primitives are the only possible tags, only that these five are defined in the framework. The theorem is a counting statement with a specific condition, and its scope stops exactly there.

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

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

/-- A finite domain axis, tagged by the RS primitive that carries its meaning. -/
structure CoupledAxis (n : ℕ) where
  Ix : Type
  finite : Fintype Ix
  card_eq : @Fintype.card Ix finite = n
  primitive : RSPrimitive

What this page does not claim

The theorem does not apply to axes of different sizes or to infinite sets. The declaration does not establish that physical space is three-dimensional; it only counts finite tagged axes. The five primitives are not proven to be exhaustive; they are defined as the framework's choice.

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: