AdmissibleCorrection
plain-language theorem explainer
The structure defines the class of dimension-dependent corrections that are additive over independent axes and normalized to 3/2 at D=3. Researchers deriving lepton generation steps would invoke this predicate to exclude alternative correction forms that coincide numerically at D=3 but differ algebraically elsewhere. The definition is a direct conjunction of the axis-additivity predicate and the calibration equation at D=3.
Claim. A map $f : ℕ → ℝ$ is an admissible dimension correction if it is axis-additive, i.e., $f(0)=0$ and $f(a+b)=f(a)+f(b)$ for all $a,b ∈ ℕ$, and satisfies the calibration $f(3)=3/2$.
background
The module establishes exclusivity for the coefficient in the tau generation step formula step_μ→τ = F - (W + D/2) · α. Axis additivity requires that corrections from independent axes add without offset, which forces linearity f(d) = d · f(1) on natural numbers. The calibration at D=3 fixes the slope to 1/2, yielding the D/2 form. This predicate draws on the admissible notion from information thermodynamics, which enforces a local consistency condition on the ledger. Upstream results on simplicial edge lengths and quantum channel corrections supply the dimensional context in which such additivity arises naturally from the phi-ladder structure.
proof idea
The declaration is a structure definition that packages the axis-additivity predicate with the calibration equation at 3. No proof steps are required beyond the conjunction of the two fields.
why it matters
This definition supplies the hypothesis for the uniqueness theorem admissible_unique, which shows that any such f must equal d/2 for all d. It thereby closes the argument that the tau correction coefficient is forced to W + D/2 rather than the algebraically distinct alternatives such as E/8. The construction aligns with the eight-tick octave and D=3 spatial dimensions in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.