localCoeff_edge
plain-language theorem explainer
The local coefficient for edge mediators in the 3-cube geometry equals 6. Researchers deriving lepton generation corrections from cube cell counts would cite this to separate edge from face contributions in the Δ derivation. The proof unfolds the ratio of cell counts to anchors per cell then evaluates the numbers directly.
Claim. In the 3-cube, the normalized coefficient for edges, given by the ratio of the number of edges to the number of vertices per edge, equals 6.
background
This module derives the dimension-dependent correction Δ(D) = D/2 from cube geometry without calibration to observed masses. The local coefficient is the ratio of the number of k-cells in the 3-cube to the number of anchoring vertices per cell. For edges this ratio uses 12 edges and 2 vertices per edge; the construction distinguishes edge-mediated steps from facet-mediated steps in the lepton generation sequence.
proof idea
The proof is a one-line wrapper that unfolds the local coefficient definition as the ratio of cell counts to anchors per cell, then applies numerical normalization to reach the value 6.
why it matters
This result feeds the downstream uniqueness theorem showing that only the face-mediated coefficient equals 3/2 while the edge value is 6. It completes one step in the cube-geometry forcing of Δ(3) = 3/2, confirming that edge mediation cannot reproduce the required τ-step correction. The module uses the vertex count as the discrete analog of solid angle to separate the two lepton steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.