localCoeff_eq_three_halves_iff
plain-language theorem explainer
The theorem shows that in the local cell mechanism for a 3-cube the coefficient equals 3/2 precisely when mediation occurs through faces. Researchers deriving the mu-to-tau lepton step from first principles would cite it to confirm the facet correction is forced by geometry alone. The proof proceeds by exhaustive case analysis on the four cell dimensions, computing the explicit coefficient value for each and obtaining numerical contradictions except for the face case.
Claim. In the 3-cube, for a cell dimension $k$, the local coefficient satisfies localCoeff$(k) = 3/2$ if and only if $k$ is a face.
background
The module derives the dimension-dependent correction Δ(D) = D/2 directly from 3-cube geometry without mass calibration. CellDim is the inductive enumeration of the four cell types (vertex, edge, face, cube) in the 3-cube; localCoeff is computed from cellCount and anchorsPerCell for each type. The local theoretical setting compares the edge-mediated e→μ step (using continuous solid angle 4π) with the facet-mediated μ→τ step (using discrete vertex count 2^{D-1} as the analog of solid angle).
proof idea
The proof performs case analysis on the inductive CellDim. For vertex, edge and cube it assumes equality to 3/2, unfolds localCoeff together with cellCount and anchorsPerCell, and obtains the contradictory numerical equalities 8 = 3/2, 6 = 3/2 and 1/8 = 3/2. For the face case it directly unfolds the definitions and normalizes to obtain the identity 3/2 = 3/2.
why it matters
The result establishes uniqueness of the 3/2 coefficient inside the admissible local mechanism class, thereby forcing Δ(3) = 3/2 in the first-principles derivation of the tau step. It supplies the geometric justification for the facet-mediated correction in the lepton generation chain and aligns with the framework's T8 forcing of D = 3 together with the eight-tick octave structure. No downstream theorems yet consume it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.