tildeQ
plain-language theorem explainer
The tildeQ map sends each canonical particle species to an integer charge index q̃. Mass ladder constructions and ablation studies cite this map to supply the discrete input for Z and rung formulas. It forwards the fermion case to the RSBridge definition while returning zero for W, Z, and H. The definition is given by exhaustive pattern matching on the four constructors of Species.
Claim. Define the charge-index function $q̃ : Species → ℤ$ by $q̃(fermion f) = q̃_{RS}(f)$, $q̃(W) = 0$, $q̃(Z) = 0$, $q̃(H) = 0$, where $q̃_{RS}$ assigns 4 to up-type quarks, -2 to down-type quarks, -6 to charged leptons, and 0 to neutrinos.
background
The module introduces Species as the inductive type of canonical particles for the mass framework: fermion wrappers around RSBridge.Fermion together with the bosons W, Z, and H. The tildeQ definition supplies the integer charge index q̃ that serves as input to the rung constructor motifs and the anchor Z map. Upstream, the RSBridge version of tildeQ already encodes the explicit integer assignments for each fermion flavor, while the cost-algebra H reparametrization and the Anchor Z definition provide the surrounding integerization conventions used downstream.
proof idea
The definition proceeds by direct pattern matching on the four constructors of Species. The fermion case delegates to the imported RSBridge.tildeQ; the W, Z, and H cases return the constant 0. No tactics or lemmas are applied beyond the inductive definition itself.
why it matters
This definition supplies the charge index required by ZOf, the ablation_contradictions check, and the Z_drop variants that test necessity of the full anchor formula. It is invoked in the electron_Z_value lemma to obtain the integer 1332. In the Recognition framework it furnishes the discrete q̃ input for the mass formula on the phi-ladder and for the eight-tick octave constructions that follow from T5–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.