localCoeff
plain-language theorem explainer
The local coefficient supplies the cellwise ratio of k-cell count to anchoring vertices per cell in the 3-cube geometry. Researchers deriving first-principles lepton mass corrections would cite it to obtain the facet-mediated term without external fitting. It is realized as the direct quotient of the cellCount and anchorsPerCell functions at the input dimension k.
Claim. For each cell dimension $k$ (vertex, edge, face or cube) in the 3-cube, the local coefficient is the ratio $N_k / A_k$, where $N_k$ is the number of $k$-cells and $A_k$ is the number of vertices anchoring each $k$-cell.
background
This module derives the dimension-dependent correction Δ(D) = D/2 from cube geometry without calibration to observed masses. The goal is to show that Δ(3) = 3/2 is forced by the framework. The deep analogy contrasts the e→μ step (edge-mediated via continuous solid angle 4π) with the μ→τ step (facet-mediated via discrete vertex count as solid-angle analog).
proof idea
This is a direct definition that computes the ratio of cellCount k to anchorsPerCell k after casting both to reals. No auxiliary lemmas are invoked; the body simply performs the division using the already-defined cellCount and anchorsPerCell maps on CellDim.
why it matters
It is invoked by the downstream theorems localCoeff_face (yielding exactly 3/2), localCoeff_eq_three_halves_iff (uniqueness inside the admissible local mechanism class), and the face-ne-edge and face-ne-cube inequalities. This supplies the concrete geometric value for the facet-mediated correction in the μ→τ lepton step, consistent with the Recognition Science forcing chain at T8 (D = 3) and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.