correction_D_half
plain-language theorem explainer
The definition supplies the half-dimension correction term for the tau lepton generation step coefficient in the Recognition Science mass ladder. Physicists deriving unique admissible corrections for lepton steps cite this when closing the algebraically equivalent alternatives to D/2. It is introduced by direct definition as d/2, which downstream results then verify satisfies axis additivity and uniqueness within the admissible class.
Claim. The correction term is defined by $c(d) = d/2$ for each natural number $d$.
background
In the Tau Step Coefficient Exclusivity module the tau generation step takes the form step_μ→τ = F - (W + correction) · α, where the correction must belong to an admissible class obeying axis additivity (f(0)=0 and f(a+b)=f(a)+f(b)) and no constant offset. The definition correction_D_half introduces Candidate 1 as the half-dimension term. Upstream, the Candidate structure from Atomicity encodes an eligible event not already picked in a Finset, while F from AnchorPolicy and TauStepDerivation denotes the face count cube_faces D (equivalently the gap function log(1 + Z/φ)/log(φ)).
proof idea
The definition is a direct arithmetic expression that casts the natural number d to real and divides by 2. No lemmas or tactics are applied; it serves as the base object for the subsequent admissibility and uniqueness theorems.
why it matters
This definition anchors the uniqueness result for the tau correction coefficient, feeding directly into D_half_admissible, F_quarter_eq_D_half, and tau_correction_unique_admissible. It fills the algebraically equivalent slot in the module's exclusivity argument and aligns with the forcing-chain landmark T8 that fixes D = 3 spatial dimensions. The parent theorem tau_correction_unique_admissible then concludes that every admissible correction equals exactly this term.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.