Etz_eq
plain-language theorem explainer
The edge count of the three-dimensional hypercube equals 12. This fixes the base combinatoric input for sector yardsticks in the mass derivation. Researchers deriving particle masses from Recognition Science primitives cite the result to confirm the chain contains no free parameters. The proof is a one-line simplification that unfolds the definition and substitutes the hypercube formula.
Claim. $cube_edges(3) = 12$, where $cube_edges(d) = d · 2^{d-1}$.
background
The AnchorDerivation module verifies sector constants from first principles. It starts from D = 3 and the hypercube edge count. cube_edges is defined as the number of edges in a D-hypercube via the formula D multiplied by 2 to the power of (D-1). Etz is the integer cast of this count for the active dimension. The upstream definition states: Number of edges in the D-hypercube: D · 2^(D-1). The module documentation lists the resulting B_pow and r0 values for lepton, up-quark, down-quark, and electroweak sectors, all derived without fitting.
proof idea
One-line wrapper that applies simp to the definitions of Etz, D, and cube_edges. The tactic unfolds Etz to cube_edges D, substitutes D = 3, and evaluates the hypercube formula to obtain the integer 12.
why it matters
This equality supplies the fixed edge count of 12 that enters every sector yardstick in the module table. It closes the verification step that all constants trace to D = 3 and cube combinatorics, supporting the claim of a parameter-free derivation. The result aligns with the T8 landmark that fixes three spatial dimensions and feeds the Recognition Composition Law applications in mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.