CellDim
plain-language theorem explainer
CellDim enumerates the four cell types in a 3-cube as vertex (0-cell), edge (1-cell), face (2-cell), and cube (3-cell). Researchers deriving the μ→τ lepton step cite it to index mediator counts and anchoring points in the facet-mediated correction. The declaration is a plain inductive enumeration that directly supplies the domain for cellCount and localCoeff without additional proof steps.
Claim. Let $C$ be the inductive type whose constructors label the cells of the 3-cube: one for 0-cells (vertices), one for 1-cells (edges), one for 2-cells (faces), and one for 3-cells (cubes).
background
The module derives Δ(D) = D/2 from cube geometry by contrasting the edge-mediated e→μ step (using continuous solid angle 4π) with the facet-mediated μ→τ step (using discrete vertex count 2^{D-1} as the analog of solid angle). CellDim supplies the discrete labels needed to count mediators per cell and anchors per mediator. Upstream structures on J-cost convexity and spectral emergence already force D = 3 together with exactly three generations; the present definition simply indexes the geometric objects required for the local coefficient calculation.
proof idea
The declaration is an inductive definition with four constructors and a derived DecidableEq instance. No lemmas are applied; the type is introduced directly to serve as the domain for the sibling functions cellCount, anchorsPerCell, and localCoeff.
why it matters
CellDim indexes the localCoeff computation whose only solution in the 3-cube is the face case, thereby forcing Δ(3) = 3/2 without calibration. This supplies the missing geometric step that closes the μ→τ mass formula inside the Recognition framework (T8: D = 3, eight-tick octave, RCL). It feeds the downstream theorems that equate the local coefficient to 3/2 precisely when mediation occurs on faces.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.