Etz
plain-language theorem explainer
Etz supplies the integer edge count of the three-dimensional hypercube obtained by casting the hypercube formula to ℤ. Mass anchor derivations cite this constant when building alternative expressions for B_pow and r0 across lepton, quark, and electroweak sectors. The definition is a direct one-line cast from cube_edges applied to D.
Claim. $E_{tz} := D · 2^{D-1}$ cast to an integer, where $D=3$ yields the total edge count of the 3-hypercube.
background
The module verifies sector constants derived from first principles using D=3 (from T8) and the hypercube edge count. cube_edges(d) is defined as d * 2^(d-1), the number of edges in a D-dimensional hypercube. Etz casts this natural-number result to ℤ for integer arithmetic in sector yardstick formulas. Upstream result cube_edges states: Number of edges in the D-hypercube: D · 2^(D-1). The local setting traces all sector constants to D=3, cube_edges(D)=12, active_edges_per_tick=1, and passive_field_edges=11.
proof idea
One-line definition that applies cube_edges to D and casts the result to ℤ.
why it matters
Etz anchors the alternative formulas for B_pow and r0 in the mass derivation chain. It appears in B_pow_alt for the down-quark sector as (2 * Etz) - 1 and supports the equality theorems B_pow_eq_alt and r0_eq_alt. This supports the parameter-free derivation of sector yardsticks from cube combinatorics, consistent with T8 fixing D=3 and the eight-tick octave structure. Downstream doc-comments confirm the formulas match the main Anchor definitions without free parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.