delta_D3_derived
plain-language theorem explainer
The theorem establishes that the structural and axis-additive expressions for the lepton-generation correction agree exactly at D=3, both yielding 3/2. Physicists deriving tau masses from cube geometry would cite it to confirm the value follows without empirical fitting. The proof is a direct rewrite using the D=3 specializations of the two formulas.
Claim. At the physical dimension $D=3$, the structural correction from cube geometry equals the axis-additive correction, so both equal $3/2$.
background
This module derives the dimension-dependent correction from cube geometry without calibration to observed masses. The central analogy treats the muon-to-tau step as facet-mediated: the leading term is the facet count $F=2D$ while the correction per facet is the reciprocal of the discrete vertex count $2^{D-1}$, giving the total correction $F/V$. The vertex count functions as the discrete analog of the solid angle that appears in the earlier electron-to-muon step. Upstream results supply the structural formula specialized at D=3 and the axis-additive property.
proof idea
The proof is a one-line rewrite that applies the D=3 instances of the structural formula and the axis-additive formula.
why it matters
This result is used by the complete derivation theorem that assembles the structural value 3/2, the axis-additive value 3/2, and their agreement to show the correction is derived rather than calibrated. It fills the step confirming that the physical dimension D=3 (T8) forces the mass formula on the phi-ladder without adjustment. The module comment notes that only D=3 is physical and that the axis-additive form is the unique one satisfying the required additive structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.