E_passive_exact
plain-language theorem explainer
The lemma proves that the passive edge count equals exactly eleven. Researchers deriving muon and tau masses from the electron mass via the lepton ladder cite this value to anchor the electron-to-muon step size. The proof is a one-line wrapper that reduces the real claim to the natural-number definition by reflexivity followed by casting.
Claim. The passive edge count in three-dimensional cube geometry satisfies $E = 11$.
background
The module proves T10 necessity results for the lepton ladder, replacing earlier axioms with derived bounds on muon and tau masses. The passive edge count is introduced as the output of passive_field_edges in three dimensions, which the anchor definition evaluates as twelve minus one. This integer enters the step function for the electron-to-muon transition together with the inverse of four pi and the square of the fine-structure constant.
proof idea
The proof is a one-line wrapper. It first asserts the natural-number equality by reflexivity on the anchor definition, then applies simplification to cast the value into the reals.
why it matters
This lemma supplies the exact integer required by the main theorem lepton_ladder_forced_from_T9, which derives the full lepton mass ladder from the electron mass (T9), cube geometry, wallpaper groups, and alpha. It closes the geometric input for the T10 forcing step that begins from the eight-tick octave and three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.