E_passive
plain-language theorem explainer
E_passive supplies the integer count of passive field edges in the cubic ledger Q3. Mass anchor and alpha derivations cite this count to fix the geometric seed factor and lepton sector exponents. The definition is a direct specialization of passive_field_edges to dimension 3.
Claim. The number of passive (field-dressing) edges of the cubic ledger $Q_3$ is defined by $E_ {passive} := 11$.
background
The T9 module constructs the refined ledger fraction for the electron mass shift from Q3 geometry. Passive edges are the cube edges that dress the interaction, obtained by subtracting the single active edge per tick from the total cube edges. The upstream passive_field_edges definition computes this difference for any dimension d, while the sibling abbrev in Anchor specializes it to general D.
proof idea
One-line definition that applies passive_field_edges to the concrete argument 3.
why it matters
This supplies the integer 11 that enters the geometric seed factor and the B_pow lepton exponent. It is invoked by geometric_seed_factor_eq_11, passive_edges_at_D3, B_pow, and the lepton rung theorems. The count follows from the D=3 topology fixed by the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.