correction_E_eighth
plain-language theorem explainer
The declaration defines the edge-based correction candidate for the tau lepton generation step as the number of hypercube edges divided by eight. Researchers working on first-principles derivations of lepton masses would cite this when comparing alternative correction terms to the axis-additive D/2 form. The definition is a direct one-line wrapper around the hypercube edge count.
Claim. The edge-based correction term for dimension $d$ is defined by $E(d)/8$, where $E(d) = d · 2^{d-1}$ denotes the number of edges in the $d$-dimensional hypercube.
background
The module examines why the coefficient in the tau generation step formula step_μ→τ = F - (W + D/2) · α must be W + D/2 rather than alternatives such as W + E/8. Axis additivity requires that a correction function f satisfies f(0) = 0 and f(a + b) = f(a) + f(b). The upstream cube_edges definition supplies the edge count as d times 2 to the power of d minus one. This candidate is one of several numerically coincident but algebraically distinct options in three dimensions.
proof idea
This is a one-line definition that applies the cube_edges function and divides the result by eight.
why it matters
This definition supports the downstream theorems showing that the E/8 term equals 3/2 in three dimensions yet fails axis additivity. It helps establish the uniqueness of the D/2 correction in the tau step by ruling out the edge-based alternative, consistent with the module's exclusivity principles derived from the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.