D_half_admissible
plain-language theorem explainer
D/2 satisfies the two conditions for an admissible dimension correction: it is axis-additive and equals 1.5 when D equals 3. Researchers deriving the tau lepton generation coefficient in the Recognition Science framework cite this result to exclude alternative corrections such as E/8 or quadratic forms. The proof proceeds by direct term-mode application of the structure constructors and simplification on the explicit definition of correction_D_half.
Claim. The function $f : ℕ → ℝ$ given by $f(n) = n/2$ is admissible: it is axis-additive and satisfies $f(3) = 3/2$.
background
In the Tau Step Exclusivity module, admissible corrections are defined via the structure AdmissibleCorrection f, which requires axisAdditive f (f(0)=0 and f(a+b)=f(a)+f(b)) together with the calibration f(3)=3/2. This local setting addresses why the coefficient in the tau step formula step_μ→τ = F - (W + D/2) · α must use D/2 rather than alternatives that coincide numerically at D=3 but differ algebraically. The module doc states that alternatives fall into algebraically equivalent cases (F/4 = D/2) and numerically coincident but algebraically distinct cases (E/8, D(D-1)/4, D²/6). Upstream results supply the axis-additivity predicate and the D=3 calibration from sibling definitions in the same module.
proof idea
The term proof refines the AdmissibleCorrection structure by providing the axisAdditive field via simp on correction_D_half together with Nat.cast_add and add_div, then supplies the calib_D3 field by simpa on the same explicit definition.
why it matters
This theorem establishes the base case for admissible corrections and is used directly by F_quarter_admissible to transport admissibility via the definitional equality correction_F_quarter = correction_D_half. It supports the exclusivity argument for the coefficient W + D/2 in the tau generation step by confirming that D/2 meets the axis-additivity and D=3 calibration requirements. In the broader framework it aligns with the forcing of D=3 spatial dimensions (T8) and the requirement that corrections remain additive across independent axes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.