anchorsPerCell
anchorsPerCell counts the vertices per cell type in the 3-cube: one for vertex, two for edge, four for face, eight for cube. Lepton generation work cites it to obtain the discrete facet measure that forces the 3/2 correction in the μ to τ step. The definition is realized by exhaustive case distinction on the four constructors of CellDim.
claimLet $k$ range over the cell dimensions of the 3-cube. The number of vertices per $k$-cell is the function $a(k)$ defined by $a($vertex$)=1$, $a($edge$)=2$, $a($face$)=4$, $a($cube$)=8$.
background
The module derives Δ(D)=D/2 from cube geometry without calibration, showing that Δ(3)=3/2 is forced by the framework. CellDim is the inductive type with constructors vertex, edge, face, cube that enumerates the four cell dimensions in a 3-cube. anchorsPerCell supplies the vertex count per k-cell, which the module identifies as the discrete analog of the solid angle for the facet-mediated correction in the μ→τ step.
proof idea
The definition is given directly by pattern matching on the CellDim constructors, returning the fixed naturals 1, 2, 4, 8. No lemmas are applied and no tactics are used; the body is a pure case expression.
why it matters in Recognition Science
anchorsPerCell supplies the denominator for localCoeff, which proves that only the face case yields the required 3/2 coefficient. This realizes the module insight that vertex count is the discrete solid angle, closing the geometric derivation of the tau step. It supports the uniqueness theorem localCoeff_eq_three_halves_iff and aligns with the eight-tick cube geometry for D=3.
scope and limits
- Does not extend vertex counting beyond the 3-cube.
- Does not incorporate continuous measures such as solid angles.
- Does not derive mass ladders or coupling constants.
- Does not address non-cubic lattices or higher-dimensional cells.
formal statement (Lean)
310def anchorsPerCell : CellDim → ℕ
311 | .vertex => 1
312 | .edge => 2
313 | .face => 4
314 | .cube => 8
315
316/-- Local (cellwise) normalized coefficient: (number of mediators)/(anchors per mediator). -/