localCoeff_vertex
plain-language theorem explainer
The local coefficient for vertex cells equals 8, defined as the ratio of the number of vertices in the 3-cube to the anchors per vertex cell. Researchers deriving the muon-to-tau lepton step correction in Recognition Science cite this when establishing the facet-mediated contribution Δ(D) = D/2 without empirical fitting. The proof is a one-line wrapper that unfolds the three supporting definitions then applies norm_num.
Claim. Let $C(k)$ denote the number of $k$-cells in the 3-cube and $A(k)$ the number of anchors per $k$-cell. The local coefficient for the vertex cell type satisfies $C(v)/A(v) = 8$, where $v$ is the vertex cell dimension.
background
The module derives the dimension-dependent correction Δ(D) = D/2 from cube geometry without calibration to observed masses, with the goal of showing that Δ(3) = 3/2 is forced by the framework. It contrasts the edge-mediated e→μ step (using 4π as continuous solid angle) with the facet-mediated μ→τ step, where vertex count acts as the discrete analog of solid angle: each facet contributes 1 over the discrete anchoring points 2^{D-1}.
proof idea
The proof is a one-line wrapper that unfolds the definitions of localCoeff, cellCount, and anchorsPerCell, then applies norm_num to evaluate the resulting numerical expression.
why it matters
This result contributes to the derivation of Δ(D) = D/2 in the TauStepDeltaDerivation module, which fills in the facet-mediated correction for the muon-to-tau generation step. It supports the framework's first-principles approach using the eight-tick octave and D = 3 spatial dimensions, with vertex count providing the discrete measure that parallels the 4π term in the electron-to-muon step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.