deltaAxisAdditive_D3
plain-language theorem explainer
The axis-additive formula for the dimension-dependent lepton correction evaluates to exactly 3/2 at spatial dimension three. Researchers deriving tau masses from cube geometry in the Recognition Science framework cite this to confirm the shift is forced by structure rather than fitted to data. The proof expands the axis-additive definition and reduces the resulting arithmetic expression via numerical normalization.
Claim. The axis-additive correction satisfies $Δ_α(3) = 3/2$.
background
In the Recognition Science treatment of lepton generations the μ→τ step introduces a dimension-dependent correction Δ(D) obtained from facet counting on the D-cube. The axis-additive formula encodes the per-axis contribution to this correction, derived from exclusivity constraints on the simplicial ledger. The module shows that this expression coincides with the structural formula at the physical dimension D = 3, yielding Δ(3) = 3/2 without external calibration.
proof idea
The proof is a one-line wrapper that unfolds the definition of deltaAxisAdditive and applies norm_num to verify the arithmetic identity at D = 3.
why it matters
This theorem is invoked directly by delta_D3_derived, which equates the structural and axis-additive expressions and thereby establishes that Δ(3) = 3/2 follows from cube geometry. It closes the loop on the module's claim that the correction is forced by the framework rather than calibrated, consistent with the derivation of three spatial dimensions and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.