pith. machine review for the scientific record. sign in
structure definition def or abbrev high

SpectralViability

show as:
view Lean formalization →

SpectralViability D collects the three predicates required for spectral emergence in dimension D: equality to 3, at least three face pairs, and lcm synchronization with 45. A researcher tracing the Recognition Science derivation of particle generations would invoke this structure to certify viability. The declaration is a plain structure definition whose fields are instantiated by reflexivity and native decision procedures in dependent theorems.

claimA natural number D is spectrally viable when D = 3, 3 ≤ (number of opposite face pairs on the D-cube), and lcm(2^D, 45) = 360.

background

The SpectralEmergence module starts from the forced datum D = 3 and examines the binary cube Q_3 with eight vertices. Face pairs, defined as the number of pairs of opposite faces on a D-dimensional cube, equals D and therefore equals three when D = 3; this supplies the three particle generations. The gap_sync field requires that the least common multiple of the 2^D cycle length and the gap-45 constant equals 360, enforcing alignment between the eight-tick octave and the phi-ladder.

proof idea

The declaration is a structure definition with no proof body. Its three fields are simple predicates on D; downstream use sites such as D3_viable populate them via rfl for the linking field and native_decide for the numerical conditions.

why it matters in Recognition Science

SpectralViability serves as the interface for D3_viable, which confirms that D = 3 satisfies the requirements, and for SpectralEmergenceCert, which extracts the gauge content, three generations, and 48 fermionic states from Q_3. It directly implements the module claim that the single forced dimension D = 3 produces the Standard Model structure together with the phi-ladder mass hierarchy. The definition thereby connects T8 to the observable spectrum without additional parameters.

scope and limits

formal statement (Lean)

 396structure SpectralViability (D : ℕ) where
 397  linking : D = 3
 398  sufficient_generations : 3 ≤ face_pairs D
 399  gap_sync : Nat.lcm (2 ^ D) 45 = 360
 400
 401/-- **THEOREM**: D = 3 satisfies all spectral viability requirements. -/

used by (2)

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

depends on (6)

Lean names referenced from this declaration's body.