E_passive
plain-language theorem explainer
E_passive supplies the integer count of passive field edges in three-dimensional cube geometry, obtained by subtracting the single active edge per tick from the total of twelve edges. Mass and alpha derivations in the Recognition framework cite this value when building sector exponents and rung ladders. The declaration is realized as a direct abbreviation of the passive_field_edges function applied at D.
Claim. $E_ {passive} := cube_edges(D) - active_edges_per_tick$, which evaluates to 11 for spatial dimension $D=3$.
background
The Masses.Anchor module centralizes parameter-free constants derived from cube geometry in three dimensions. Total edges equal twelve while one edge remains active per tick, so the passive count is eleven; these passive edges dress the interactions in the mass formulas. The upstream passive_field_edges definition performs exactly this subtraction: cube_edges d minus active_edges_per_tick, and the module doc states that E_passive equals E_total minus one.
proof idea
One-line abbreviation that applies passive_field_edges directly to the dimension D.
why it matters
This supplies the integer 11 that enters the geometric seed factor for the fine-structure constant and the lepton-sector B_pow = -22. It is used by geometric_seed_factor_eq_11, passive_edges_at_D3, B_pow, r_lepton_values, and tau. The definition realizes the D=3 requirement of the forcing chain through explicit cube-edge counting and closes part of the mass-ladder construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.