F_quarter_not_alternative
plain-language theorem explainer
The result shows that the face-based correction F/4 coincides identically with the dimension-based D/2 for every natural-number dimension. Physicists deriving the unique coefficient in the tau lepton generation step would cite it to eliminate the F/4 alternative from the admissible class. The proof is a one-line term wrapper that applies function extensionality to the algebraic identity proved by the sibling lemma.
Claim. The face-quarter correction equals the dimension-half correction: $correction_{F/4} = correction_{D/2}$.
background
The Tau Step Exclusivity module examines the tau generation step formula step_μ→τ = F - (W + D/2) · α and asks why the correction coefficient must be W + D/2 rather than W + F/4 or other forms that evaluate to the same number at D = 3. The sibling theorem F_quarter_eq_D_half supplies the algebraic identity ∀ d : ℕ, correction_F_quarter d = correction_D_half d by unfolding the definitions, invoking cube_faces = 2d, and simplifying with ring tactics. Upstream results supply the required notions: independent axes from RSCoupledAxis (axes carried by distinct primitives) and admissible corrections from CostModel and MaxwellDEC (positivity and alignment conditions that exclude constant offsets).
proof idea
The proof is a one-line term-mode wrapper that applies funext directly to the pointwise equality F_quarter_eq_D_half.
why it matters
This corollary disposes of the algebraically equivalent alternative in the module's exclusivity argument, confirming that only the D/2 form survives once axis additivity and zero-offset conditions are imposed. It feeds the main claim that the coefficient W + D/2 is forced by the Recognition Science principles of independent axes and admissible corrections. The result sits inside the T8 forcing of three spatial dimensions and the requirement that corrections remain additive across axes; it does not yet address the numerically coincident but algebraically distinct alternatives such as E/8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.