Epz_eq
plain-language theorem explainer
Epz equals 11 for D equal to three. Mass derivation work in Recognition Science cites this to fix the passive edge count that enters the phi-ladder yardsticks for lepton and quark sectors. The proof is a one-line simp wrapper that unfolds the definitions of Epz, passive_field_edges, cube_edges, and active_edges_per_tick.
Claim. $E_{pz} = 11$, where $E_{pz}$ is defined as the number of passive field edges in $D=3$ spatial dimensions, given by $D · 2^{D-1} - 1$.
background
The module verifies sector constants from first principles. All sector constants trace back to D=3 from the forcing chain, cube_edges(D) = D · 2^(D-1), active_edges_per_tick = 1 by the atomic tick rule, and passive_field_edges(D) = cube_edges(D) - active_edges_per_tick. The module states that passive_field_edges equals 11 (12 - 1 = 11, the missing 11) and that this number appears in the B_pow formulas for the lepton sector as -(2 × 11) = -22.
proof idea
One-line simp wrapper that unfolds Epz to passive_field_edges D, substitutes the imported D=3, applies cube_edges as 3 · 2^2 = 12, subtracts active_edges_per_tick = 1, and obtains 11.
why it matters
This pins the passive edge count used in the Anchor derivation for sector yardsticks. It closes the verification that all sector constants trace to D=3 and cube combinatorics without free parameters, as stated in the module documentation. The result supports the mass formulas that place lepton and quark masses on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.