theorem
proved
fermion_count_24
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.SpectralEmergence on GitHub at line 228.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
225 Quarks: 3 colors × 3 generations × 2 flavors (up/down) = 18
226 Leptons: 1 × 3 generations × 2 flavors (ν/e) = 6
227 Total: 24 -/
228theorem fermion_count_24 : fermion_flavors = 24 := by
229 native_decide
230
231/-- **THEOREM (D × 2^D identity)**: The fermion flavor count equals
232 the cube dimension times its vertex count. -/
233theorem fermions_eq_D_times_V : fermion_flavors = 3 * V 3 := by
234 native_decide
235
236/-- **THEOREM (Aut(Q₃) / 2 identity)**: The fermion flavor count is
237 half the automorphism group order (particle vs antiparticle). -/
238theorem fermions_eq_half_aut : 2 * fermion_flavors = aut_order 3 := by
239 native_decide
240
241/-- Total fermion states including chirality doubling. -/
242def total_fermion_states : ℕ := 2 * fermion_flavors
243
244/-- **THEOREM**: Total fermion states = |Aut(Q₃)| = 48.
245 The symmetry group of Q₃ IS the fermion state space. -/
246theorem fermion_states_eq_aut : total_fermion_states = aut_order 3 := by
247 native_decide
248
249/-- **THEOREM**: The quark-to-lepton ratio is 3:1 (= color dimension). -/
250theorem quark_lepton_ratio :
251 SpectralSector.dim .color * face_pairs 3 * 2 =
252 3 * (SpectralSector.dim .hypercharge * face_pairs 3 * 2) := by
253 native_decide
254
255/-! ## Part 5: Mass Structure — The φ-Ladder Eigenvalues
256
257Each spectral sector has a characteristic mass scale set by φ.
258The J-cost evaluated at φ^n gives the mass-energy at rung n