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)
137theorem lepton_total_span :
138 lepton_step_12 + lepton_step_23 = wallpaper_groups := by native_decide
proof body
Term-mode proof.
139
140/-!
141### Down-Quark Sector (coupling dimension d=2, faces)
142
143Down quarks traverse DOWN from faces to vertices.
144Gen 1→2 step: F = 6 (face count = coupling dimension count)
145Gen 2→3 step: V = 8 (vertex count = complementary dimension)
146Total span: V + F = 14 = W - D
147-/
148
149/-- Down-quark generation steps from cube geometry. -/
depends on (20)
Lean names referenced from this declaration's body.
-
step
in IndisputableMonolith.Complexity.CellularAutomata
decl_use
-
wallpaper_groups
in IndisputableMonolith.Constants.AlphaDerivation
decl_use
-
wallpaper_groups
in IndisputableMonolith.Constants.AlphaHigherOrder
decl_use
-
V
in IndisputableMonolith.Cosmology.InflatonPotentialFromJCost
decl_use
-
Quark
in IndisputableMonolith.CrossDomain.CubeFaceUniversality
decl_use
-
from
in IndisputableMonolith.Foundation.PrimitiveDistinction
decl_use
-
V
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
Sector
in IndisputableMonolith.Masses.Anchor
decl_use
-
W
in IndisputableMonolith.Masses.Anchor
decl_use
-
Sector
in IndisputableMonolith.Masses.RSBridge.Anchor
decl_use
-
Sector
in IndisputableMonolith.Masses.RungConstructor.Basic
decl_use
-
lepton_step_12
in IndisputableMonolith.Masses.SectorDependentTorsion
decl_use
-
lepton_step_23
in IndisputableMonolith.Masses.SectorDependentTorsion
decl_use
-
F
in IndisputableMonolith.Physics.AnchorPolicy
decl_use
-
F
in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation
decl_use
-
W
in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation
decl_use
-
W
in IndisputableMonolith.Physics.MassTopology
decl_use
-
F
in IndisputableMonolith.Pipelines
decl_use
-
V
in IndisputableMonolith.RRF.Core.Glossary
decl_use
-
Sector
in IndisputableMonolith.RSBridge.Anchor
decl_use