admissible_unique
plain-language theorem explainer
Any axis-additive map f from naturals to reals that satisfies the calibration f(3) = 3/2 must equal f(d) = d/2 for every d. Lepton generation calculations in Recognition Science cite the result to fix the tau step coefficient and exclude numerically coincident alternatives. The proof extracts the linear form from additivity, solves the D=3 calibration equation for the slope via field simplification and nlinarith, then substitutes and rings.
Claim. Suppose $f : {N} {to} {R}$ is axis-additive and satisfies the calibration $f(3) = 3/2$. Then $f(d) = d/2$ for every natural number $d$.
background
The Tau Step Exclusivity module shows why the tau generation step coefficient must be W + D/2 rather than alternatives that agree numerically at D=3. An admissible correction is a map f : N to R that is axis-additive (f(a+b) = f(a)+f(b)) and calibrated by f(3) = 3/2. Axis additivity encodes independent per-axis contributions; the calibration anchors the function at physical dimension 3. Upstream results on primitive distinctions and simplicial ledgers supply the structural conditions that motivate this additivity requirement.
proof idea
The tactic proof first applies axisAdditive_linear to the axisAdditive field, obtaining f d = d · f 1. It specializes to d=3, equates to the calibration value 3/2, and solves for f 1 = 1/2 by field_simp followed by nlinarith. For arbitrary d the linearity relation is substituted and ring simplification yields f d = d/2.
why it matters
The theorem is invoked directly by tau_correction_unique_admissible to equate any admissible correction with the explicit D/2 form. It thereby secures uniqueness of the coefficient in the tau step formula inside the lepton generations development. The step aligns with the Recognition Science forcing chain that derives D=3 from the eight-tick octave and self-similar fixed point. It closes one branch of the question on why algebraically distinct alternatives are ruled out once axis additivity is imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.