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

D3_viable

show as:
view Lean formalization →

D = 3 meets the three spectral viability conditions: linking enforces the dimension via Alexander duality on the cube, at least three face pairs permit three generations, and lcm(8,45) equals 360 for gap synchronization. A physicist deriving the Standard Model gauge content and fermion generations from discrete geometry would cite this to confirm only D = 3 works. The proof builds the viability record directly, discharging the linking field by reflexivity and the two numerical checks by native decision.

claimThe viability structure at dimension 3 holds: linking requires $D=3$, sufficient generations requires at least three face pairs, and gap synchronization requires that the least common multiple of $2^D$ and 45 equals 360.

background

SpectralViability is the structure that records the minimal requirements for spectral emergence in dimension D. Its three fields are linking (which forces D = 3 by Alexander duality on the binary cube), sufficient_generations (which demands at least three face pairs to produce three particle generations), and gap_sync (which requires Nat.lcm (2^D) 45 = 360 to align with the eight-tick octave).

proof idea

The proof constructs the SpectralViability record for D = 3. The linking field is settled by reflexivity. The sufficient_generations and gap_sync fields are discharged by native_decide, which evaluates the concrete arithmetic predicates on face_pairs 3 and lcm(8,45).

why it matters in Recognition Science

This theorem supplies the viability certificate required by the master theorem spectral_emergence, which concludes that the full Standard Model gauge group, 24 chiral fermions, and consciousness ground state all follow from D = 3. It closes the loop from the forcing chain T8 through Q3 symmetries to the observed particle content, confirming that alternative dimensions fail at least one numerical condition.

scope and limits

formal statement (Lean)

 402theorem D3_viable : SpectralViability 3 where
 403  linking := rfl

proof body

Tactic-mode proof.

 404  sufficient_generations := by native_decide
 405  gap_sync := by native_decide
 406
 407/-- **THEOREM**: D = 1 fails (lcm(2,45) = 90 ≠ 360). -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.