Foundation Rscoupled Axis Rsprimitive

The five primitives

In mathematics, a primitive is an object that is not built from other objects of the same kind. In Recognition Science, the framework's library of machine-checked formal theorems defines five such primitives: jCost, phiLadder, sigmaCharge, q3Lattice, and gap45. Each is a label that names a distinct kind of meaning carried by a finite domain axis, which is a finite set of positions or states that a system can occupy. The five labels are not derived from each other; they are the base vocabulary for tagging axes.

The declaration RSPrimitive establishes that there are exactly five such labels. The theorem rsPrimitive_count proves that the number of primitives is 5, and the proof is a direct computation, so the claim is exact and machine-checked. The five names themselves are chosen by the framework as a definitional choice, not forced by any theorem. The count of five, however, is a proved fact about that choice.

The purpose of the labels becomes clear in the framework's account of independence. Two finite axes of the same size are not automatically independent; in Recognition Science they count as independent only when they carry different primitives. The definition independent states this condition: axis A and axis B are independent exactly when their primitive tags differ. This is a definition, a modeling choice, not a derived law. The framework then uses this notion to build structures of three pairwise independent axes of the same size, and proves that the product of their cardinalities is n^3 and the sum of their cardinalities is 3n. These cardinality theorems are proved in the library.

In Recognition Science, the framework models a three-dimensional space as a triple of pairwise independent axes of the same size, each tagged by a different primitive. The framework proves that the product of the cardinalities of such a triple is n^3, which is the tensor-product count, and the sum is 3n, which is the disjoint-sum count. These are structural facts about the framework's definitions. They do not by themselves establish that physical space has three dimensions; the framework's claim about physical space is a separate, larger step that remains open.

What RSPrimitive does not claim is just as important. It does not claim that the five labels correspond to anything in the physical world; that is a modeling choice. It does not claim that the count of five is forced by the framework's axioms; it is a definitional choice. It does not claim that any particular axis, such as the one tagged by phiLadder, has any special properties beyond being a label. The declaration is a foundation for building structures, not a statement about the world.

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 five primitives correspond to anything in the physical world. The count of five is forced by the framework's axioms; it is a definitional choice. Any particular axis, such as the one tagged by phiLadder, has special properties beyond being a label.

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: