E_passive_exact
plain-language theorem explainer
The lemma fixes the passive edge count E_passive to exactly 11 when interpreted as a real. Researchers deriving muon and tau masses from the electron mass via the forced lepton ladder cite this value to anchor the step_e_mu expression. The proof reduces directly to the natural-number definition of E_passive by reflexivity followed by a cast simplification.
Claim. $E_ {rm passive} = 11$
background
In the T10 module the lepton ladder is forced from the electron structural mass (T9) together with cube-derived constants. E_passive is defined upstream as passive_field_edges D for D=3, which equals 11 because the cube has 12 edges with one subtracted for the passive field. The module doc states that the ladder steps combine E_passive=11, faces=6, wallpaper groups W=17, and alpha to determine the muon and tau masses.
proof idea
The term proof first obtains the natural-number equality (E_passive : ℕ) = 11 by reflexivity, then applies simp with Nat.cast_ofNat to lift the equality to reals.
why it matters
This exact value is invoked by the parent theorems lepton_ladder_forced_from_T9 and lepton_ladder_forced_from_T9_v2, which prove the full T10 statement that muon and tau masses are determined by E_passive=11, faces=6, W=17, and alpha. It supplies the concrete number required by the step_e_mu_bounds lemmas and closes the geometric input for the eight-tick structure at D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.