pith. machine review for the scientific record. sign in
theorem proved term proof high

D1_fails_sync

show as:
view Lean formalization →

The theorem shows that the synchronization condition lcm(2,45) equals 360 fails for spatial dimension D=1, ruling out this case in the Recognition Science forcing chain. A physicist checking dimensional consistency for the Q3 cube and eight-tick octave would cite it to exclude D=1 before invoking the D=3 case. The proof is a direct computational check via native_decide on the concrete natural-number inequality.

claim$lcm(2,45) ≠ 360$

background

The module SpectralEmergence starts from the forced datum D=3 (T8) to obtain the binary cube Q3 with 8 vertices and derives the Standard Model gauge content plus 48 chiral fermion states from |Aut(Q3)|=48. It also records that alternative dimensions fail at least one numerical requirement, including synchronization conditions tied to the eight-tick octave (T7). The constant 45 appearing in the lcm is part of the octave-period consistency check that must hold for the phi-ladder mass hierarchy to close consistently with the 2^D factor.

proof idea

The proof is a one-line term wrapper that applies native_decide to evaluate the concrete inequality on natural numbers.

why it matters in Recognition Science

The declaration supplies one concrete instance of the module claim that no alternative dimension works, thereby supporting the uniqueness of D=3 in the forcing chain T5-T8. It closes a numerical consistency check required before the automorphism order |Aut(Q3)|=48 can be matched to the 24 chiral fermion flavors and the SU(3)×SU(2)×U(1) sector dimensions. No open scaffolding remains for this specific computation.

scope and limits

formal statement (Lean)

 408theorem D1_fails_sync : Nat.lcm (2 ^ 1) 45 ≠ 360 := by native_decide

proof body

Term-mode proof.

 409
 410/-- **THEOREM**: D = 2 fails (lcm(4,45) = 180 ≠ 360). -/