localCoeff_face_ne_cube
plain-language theorem explainer
The local coefficient assigned to face cells is shown to differ from the coefficient assigned to cube cells inside the tau-step delta derivation. A researcher constructing the lepton mass ladder from simplicial geometry would cite the result to keep the facet correction strictly local rather than conflating it with the global 12/8 ratio. The proof reduces the claim to an explicit real-number inequality by unfolding the two coefficient definitions and applying numerical evaluation.
Claim. The local coefficient associated with the face cell type is not equal to the local coefficient associated with the cube cell type.
background
The module derives the dimension-dependent correction Δ(D) = D/2 directly from cube geometry without external calibration. In the μ→τ step the leading term is the facet count F = 2D while the correction is obtained as Δ = F / V_facet, where V_facet = 2^{D-1} supplies the discrete vertex count per facet. This vertex count functions as the discrete analog of the solid angle 4π that appears in the preceding e→μ edge-mediated step. The local coefficient definitions therefore assign distinct normalization factors to each cell type so that the correction remains cellwise rather than a cross-level ratio.
proof idea
The proof is a term-mode wrapper. It applies simplification to unfold the face and cube coefficient expressions, then invokes numerical normalization to confirm that the resulting real numbers satisfy the strict inequality.
why it matters
The result secures that Δ(3) = 3/2 arises from the forced geometry of the simplicial ledger rather than from any local equality between face and cube coefficients. It thereby supports the first-principles derivation of the tau mass step and prevents the 12/8 ratio from being misread as a cellwise normalization. The theorem sits inside the broader chain that obtains all lepton generation steps from the Recognition Composition Law and the eight-tick octave without calibration to observed masses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.