cellCount
This definition supplies the integer counts of vertices, edges, faces, and the single cube inside a 3-cube: eight, twelve, six, and one respectively. Researchers deriving the facet-mediated lepton step in Recognition Science cite it to obtain the local coefficient 3/2 without external mass input. The definition is a direct pattern match on the four constructors of CellDim.
claimLet $C$ denote the inductive type whose constructors are vertex, edge, face, and cube. The function cellCount : $C$ → ℕ is defined by cellCount(vertex) = 8, cellCount(edge) = 12, cellCount(face) = 6, cellCount(cube) = 1.
background
The module derives the dimension-dependent correction Δ(D) = D/2 from cube geometry without calibration to observed masses, with the explicit goal of showing that Δ(3) = 3/2 is forced. CellDim is the inductive type whose four constructors label the cell dimensions 0 through 3 in a 3-cube; the supplied definition gives the number of k-cells, which serve as the discrete anchoring points per mediator. Upstream structures include SpectralEmergence, which forces exactly three generations from face-pair count, and PhysicsComplexityStructure, which establishes convexity of the J-cost function.
proof idea
One-line wrapper that applies pattern matching on the CellDim inductive type, returning the four hardcoded natural numbers directly.
why it matters in Recognition Science
The definition supplies the integer inputs required by every localCoeff theorem in the same module, in particular localCoeff_face which yields exactly 3/2 and thereby closes the μ→τ step. It therefore realizes the module's central claim that Δ(3) = 3/2 follows from cube geometry alone, consistent with the framework's T8 forcing of three spatial dimensions and the discrete solid-angle analogy stated in the module doc-comment.
scope and limits
- Does not compute cell counts for any dimension other than three.
- Does not derive the counts from an underlying counting argument; they are supplied by definition.
- Does not apply to non-cubic polytopes or higher-dimensional lattices.
- Does not encode any dynamical evolution or time dependence.
formal statement (Lean)
303def cellCount : CellDim → ℕ
304 | .vertex => 8
305 | .edge => 12
306 | .face => 6
307 | .cube => 1
308
309/-- Number of vertices (0-cells) per k-cell (anchors per mediator). -/