deltaAxisAdditive
plain-language theorem explainer
The axis-additive formula defines the correction term as half the spatial dimension. Lepton generation derivations cite this closed form to confirm agreement with the cube-geometry structural result at D=3. The definition consists of a single arithmetic operation with no lemmas or reductions.
Claim. The axis-additive correction is defined by $Δ(D) = D/2$ for $D ∈ ℕ$.
background
This module derives the dimension-dependent correction Δ(D) = D/2 from cube geometry without calibration to observed masses. The axis-additive formula originates from the exclusivity proof and supplies the closed expression that matches the facet-mediated structural derivation at physical dimension D=3. The module draws an analogy between the e→μ step, which uses the continuous solid angle 4π, and the μ→τ step, which replaces it with the discrete vertex count 2^{D-1} per facet. This yields the total correction Δ = F/V_facet where F=2D, simplifying to D/2. The vertex count functions as the discrete analog of solid angle.
proof idea
The definition is a direct arithmetic expression that casts the natural number D to a real and divides by two. No upstream lemmas are invoked.
why it matters
This definition provides the axis-additive expression used in delta_D3_derived to equate it with the structural formula at D=3, establishing that Δ(3)=3/2 follows from geometry alone. It also appears in delta_derived_not_calibrated, the complete theorem showing both formulas agree without calibration. Within the Recognition framework this completes the μ→τ generation step using D=3 from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.