tau_correction_unique_admissible
plain-language theorem explainer
Any function f from natural numbers to reals that is axis-additive and satisfies f(3) equals 3/2 must equal d/2 at every natural d. Lepton generation modelers in Recognition Science cite this to fix the tau step coefficient as W plus D/2. The proof applies the admissible uniqueness lemma then simplifies via the explicit half-dimension form.
Claim. Let $f : ℕ → ℝ$ be axis-additive with $f(3) = 3/2$. Then $f(d) = d/2$ for every natural number $d$.
background
The module proves exclusivity for the coefficient in the tau generation step formula step_μ→τ = F − (W + D/2) · α. AdmissibleCorrection is the structure requiring axis additivity (f(a+b) = f(a) + f(b) with f(0) = 0) together with calibration f(3) = 3/2. This class excludes numerically coincident alternatives such as E/8 or D(D−1)/4 that fail additivity outside D = 3.
proof idea
The proof introduces arbitrary d. It applies the lemma admissible_unique to the function f and hypothesis h, yielding equality with correction_D_half d. The simpa tactic then rewrites the right-hand side using the definition of correction_D_half.
why it matters
This theorem completes the exclusivity argument inside the lepton generations module by showing the dimension term is forced to D/2 within the admissible class. It supports the forced form W + D/2 in the tau step and aligns with the eight-tick octave and spatial dimension D = 3 from the forcing chain. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.