localCoeff_face_ne_edge
plain-language theorem explainer
This theorem shows that the face-mediated local coefficient 3/2 differs from the edge-mediated value 6 within the admissible local mechanism class. Derivations of dimension-dependent mass corrections in lepton generations cite it to establish uniqueness of the facet contribution before assembling the full delta. The proof is a one-line wrapper that unfolds the two prior evaluations of the coefficient and reduces the inequality to a numerical check.
Claim. In the local coefficient defined by the ratio of cell count to anchors per cell, the face-mediated value differs from the edge-mediated value: $3/2 ≠ 6$.
background
The module derives the correction Δ(D) = D/2 for the μ→τ lepton step from cube geometry. It treats the vertex count 2^{D-1} as the discrete analog of solid angle, so each facet contributes a differential term 1/V. The local coefficient is the ratio (number of mediators) / (anchors per mediator). Upstream results establish the concrete values: the edge case evaluates to 6 and the face case to 3/2.
proof idea
The proof unfolds the definitions of the face and edge coefficients supplied by the two preceding theorems, then applies simplification and numeric normalization to obtain the concrete inequality 3/2 ≠ 6.
why it matters
It confirms that the facet-mediated coefficient 3/2 is admissible and distinct from the edge value 6, supporting the uniqueness claim in the doc-comment for the μ→τ step. The result sits inside the first-principles derivation of Δ(D) = D/2 and aligns with the eight-tick octave and D = 3 forced earlier in the chain. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.