anchorsPerCell
plain-language theorem explainer
anchorsPerCell maps each cell dimension in a 3-cube to its vertex count: 1 for vertices, 2 for edges, 4 for faces, 8 for the cube. Researchers deriving the μ→τ lepton mass step from cube geometry cite it to normalize mediator counts by discrete anchors. The definition is exhaustive case analysis on the CellDim inductive type with no lemmas.
Claim. Let $k$ range over the cell dimensions vertex, edge, face, cube in a 3-cube. The map $a(k)$ returns the number of vertices per $k$-cell: $a($vertex$)=1$, $a($edge$)=2$, $a($face$)=4$, $a($cube$)=8$.
background
CellDim is the inductive type whose constructors are vertex, edge, face, cube, enumerating the four cell dimensions inside a 3-cube. The module derives the correction term Δ(D)=D/2 directly from cube geometry, showing that Δ(3)=3/2 is forced rather than fitted; the vertex count supplies the discrete measure that plays the role of solid angle in the facet-mediated μ→τ step. Upstream structures establish that J-cost minimization is convex and that spectral emergence forces exactly three generations from face-pair counting.
proof idea
Direct definition by pattern matching on the four CellDim constructors, returning the constants 1, 2, 4, 8. No tactics or lemmas are invoked; the body is the exhaustive case split itself.
why it matters
anchorsPerCell supplies the denominator for every localCoeff(k) = cellCount(k) / anchorsPerCell(k). The downstream theorems then prove that only the face case yields exactly 3/2, confirming the facet-mediated correction required for the τ step. It realizes the module's claim that vertex count is the discrete analog of solid angle and closes one link in the chain from D=3 to the observed lepton mass ratios.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.