Foundation Rscoupled Axis Gap45 Eq

The gap-45 constant

The number 45 appears throughout mathematics and physics as a convenient bound: 45 degrees is half a right angle, and 45 is the sum of the digits from 1 through 9. In Recognition Science, the constant gap45 names a specific complexity ceiling: it is the largest size that a finite domain axis can have before the framework's accounting changes. The declaration gap45_eq states, in the machine-checked library of formal theorems, that this constant is exactly 45. That is its entire content: a definitional identity, verified by direct computation.

The surrounding infrastructure explains why 45 matters. Recognition Science models physical structure as a ledger, a discrete record of events where each event carries a cost. Domain axes, the finite sets that index these events, are tagged by one of five recognition primitives: the cost function, the phi ladder, the charge, the lattice, or the gap-45 ceiling itself. Two axes count as independent only when they carry different primitives; same-size axes tagged alike are not automatically independent. The framework proves that three pairwise independent axes of size n combine in two ways: their tensor product has n³ elements, and their disjoint sum has 3n elements. The constant 45 sits at the top of this scheme as the named ceiling for a single axis.

What gap45_eq does not claim is just as precise. It does not derive 45 from any deeper principle, such as the forcing chain that produces the golden ratio or the number of spatial dimensions. The theorem only says that the constant, once defined, equals 45; it says nothing about why 45, rather than 44 or 46, was chosen. The choice itself is a modeling decision, not a consequence of the framework's axioms. A reader should not take the declaration as evidence that the number 45 is forced by recognition theory; it is a label pinned to a bound that the framework's authors selected.

The practical upshot is modest but real. Within the framework, gap45_eq lets later theorems refer to the ceiling by name without re-deriving its value, and it guarantees that any axis of size 45 is a well-formed object of the theory. The declaration is a bookkeeping step, not a discovery. It keeps the ledger consistent by fixing a reference point, much as a ruler's markings do not explain why an inch is an inch, they only make measurement repeatable.

theorem gap45_eq : gap45 = 45 := rfl

/-- 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 number 45 is derived from the forcing chain or any deeper principle. The constant gap45 has any physical meaning outside the framework's modeling choice. The declaration proves that axes of size 45 are the largest possible in any absolute sense.

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: