E_eighth_at_3
plain-language theorem explainer
The theorem shows that the edge-based correction candidate at spatial dimension three evaluates to exactly 1.5. A physicist examining alternative hypercube-derived coefficients for the tau generation step would cite it to document numerical agreement with the axis-additive form while preserving algebraic distinction. The proof is a direct computational reduction that unfolds the candidate definition, substitutes the edge-count formula, and normalizes the arithmetic.
Claim. Let $E(d) = d · 2^{d-1}$ be the number of edges in the $d$-dimensional hypercube. Then $E(3)/8 = 3/2$.
background
The TauStepExclusivity module examines why the coefficient in the tau step formula must be $W + D/2$ rather than alternatives such as $W + E/8$. cube_edges(d) counts the edges of the $d$-hypercube as $d · 2^{d-1}$. correction_E_eighth(d) is defined as the candidate correction $(cube_edges d : ℝ)/8$, one of the numerically coincident but algebraically distinct options that all yield 1.5 when $d=3$. The module contrasts these with the axis-additive requirement $f(0)=0$ and $f(a+b)=f(a)+f(b)$ that selects $D/2$.
proof idea
The term proof unfolds correction_E_eighth, simplifies using the cube_edges definition, and applies norm_num to obtain the exact rational 3/2.
why it matters
The result documents that the E/8 candidate matches the value of D/2 at D=3, supporting the module's exclusivity argument that only the axis-additive form survives when algebraic distinction across dimensions is required. It feeds the broader claim that the tau coefficient is forced once admissible corrections are restricted to those obeying additivity and zero offset, consistent with the hypercube geometry used to derive D=3 and the Recognition constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.