recognition /
Foundation /
Foundation.SpectralEmergence /
explainer
No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
210 theorem generations_eq_dimension : face_pairs 3 = 3 := three_generations
proof body
Term-mode proof.
211
212 /-! ## Part 4: Fermion Census — The 24 and 48 Theorems
213
214 The total number of chiral fermion flavors is D × 2^D = 24.
215 The total fermionic state count is |Aut(Q₃)| = 48. -/
216
217 /-- The chiral fermion flavor count: each sector contributes a number
218 of flavors determined by matter_dim × generations × chiralities_per_sector. -/
depends on (19)
Lean names referenced from this declaration's body.
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
face_pairs
in IndisputableMonolith.Foundation.ParticleGenerations
decl_use
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
face_pairs
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
three_generations
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
Fermion
in IndisputableMonolith.Masses.RSBridge.Anchor
decl_use
Fermion
in IndisputableMonolith.Masses.SMVerification
decl_use
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
total
in IndisputableMonolith.NavierStokes.DiscreteVorticity
decl_use
and
in IndisputableMonolith.NumberTheory.CirclePhaseLift
decl_use
total
in IndisputableMonolith.NumberTheory.RiemannHypothesis.ErrorBudget
decl_use
three_generations
in IndisputableMonolith.Physics.ThreeGenerations
decl_use
Fermion
in IndisputableMonolith.RSBridge.Anchor
decl_use