F_quarter_eq_D_half
plain-language theorem explainer
The identity establishes that the hypercube face correction divided by four equals half the dimension for every natural number d. Physicists deriving the tau lepton generation coefficient in Recognition Science cite it to collapse notationally distinct but equivalent terms in the step formula. The proof unfolds the correction definitions, applies the cube faces count, and reduces the equality by ring arithmetic.
Claim. For all natural numbers $d$, the quarter-face correction equals the half-dimension correction: $F(d)/4 = d/2$, where $F(d) = 2d$ is the number of faces of the $d$-dimensional hypercube.
background
The Tau Step Exclusivity module examines why the coefficient in the tau generation step formula must be W + D/2 rather than alternative expressions that evaluate to the same number at D=3. It separates algebraically identical rewritings from numerically coincident but structurally different corrections that violate axis additivity.
proof idea
The proof introduces arbitrary d, unfolds the two correction definitions, simplifies using the cube_faces fact that the hypercube has 2d faces, and applies ring to confirm the arithmetic reduction (2d)/4 = d/2.
why it matters
This result shows F/4 is algebraically identical to D/2 and therefore not a distinct alternative, directly enabling the downstream theorems F_quarter_admissible and F_quarter_not_alternative that transport admissibility. It fills the algebraic-equivalence slot in the module's exclusivity argument and reinforces the dimension-dependent correction required by the Recognition Science forcing chain for lepton masses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.