Epz
plain-language theorem explainer
Epz supplies the integer count of passive field edges for three spatial dimensions, obtained by subtracting the single active edge per tick from the twelve cube edges. Sector mass derivations cite it to build alternative B_pow expressions, such as minus twice this value for leptons. The definition is a direct cast of the upstream passive_field_edges function evaluated at the dimension constant D.
Claim. Let Epz denote the integer value of passive_field_edges(D), where passive_field_edges(d) equals cube_edges(d) minus active_edges_per_tick and D equals 3, yielding 11.
background
The AnchorDerivation module verifies that sector yardsticks for masses follow from cube combinatorics once D equals 3 is fixed. Upstream, passive_field_edges(d) is defined as cube_edges(d) minus active_edges_per_tick, with the doc-comment noting that for D=3 the result is the key number 11. The module doc states that all sector constants trace back to D=3, cube_edges(D)=12, active_edges_per_tick=1, and passive_field_edges=11, with no free parameters.
proof idea
One-line definition that applies passive_field_edges to the constant D and casts the natural-number result to integers.
why it matters
Epz anchors the alternative formulas in B_pow_alt for the four sectors and is invoked inside the equality proof B_pow_eq_alt that confirms these match the primary definitions. It closes the first-principles chain for lepton, quark, and electroweak B_pow and r0 values, linking directly to the T8 result that D equals 3 and the cube-edge counting that produces the missing-11 passive edges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.