F_quarter_admissible
plain-language theorem explainer
F/4 satisfies the admissible correction criteria because it coincides exactly with D/2. Researchers deriving lepton generation steps from hypercube geometry cite this result to equate face-based and axis-based corrections in the tau coefficient. The argument reduces the claim to the already-proved D/2 case via functional equality and transport of the admissibility property.
Claim. The function $f : ℕ → ℝ$ given by $f(D) = F(D)/4$ is axis-additive and satisfies $f(3) = 3/2$.
background
AdmissibleCorrection is the structure requiring a map $f : ℕ → ℝ$ to be axis-additive (i.e., $f(0)=0$ and $f(a+b)=f(a)+f(b)$) together with the calibration $f(3)=3/2$. The module establishes that the tau generation step coefficient must be of the form $W + D/2$ once this admissibility class is imposed. F is the face count of the D-cube (satisfying $F=2D$), so the F/4 form is algebraically identical to D/2. Upstream results supply the edge count E and the axis-additivity predicate used to define the admissible class.
proof idea
One-line wrapper that applies functional extensionality to obtain correction_F_quarter = correction_D_half from F_quarter_eq_D_half, then rewrites the goal and invokes D_half_admissible.
why it matters
The result closes the algebraically equivalent alternatives (Category 1) in the tau-step exclusivity argument, confirming that only the axis-additive D/2 form survives. It feeds the parent claim that (W + D/2) is forced once admissibility is required. The construction aligns with the Recognition framework's T8 (D=3) and the axis-additivity principle stated in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.