Z_of_charge
plain-language theorem explainer
Z_of_charge selects the integer charge factor by sector flag for input Q6 = 6Q. Mass ribbon calculations cite it when assembling canonical masses from words and generation class. The definition is a direct conditional dispatch to the sector-specific Z functions.
Claim. Define the charge factor function by cases: if the sector flag is true then apply the quark map to Q6, otherwise apply the lepton map to Q6, where Q6 stands for the integerized charge 6Q.
background
The module supplies placeholder ribbon machinery for mass construction and is marked as a Model file whose RS derivations remain informal. Word is defined as List Ribbon, with each Ribbon following a deterministic ring pattern spread across the eight-tick clock. In this module both Z_quark and Z_lepton are the constant-zero functions on ℤ. Upstream, the theorem from in PrimitiveDistinction extracts four structural conditions plus three definitional facts from seven independent axioms.
proof idea
One-line definition by conditional on the Boolean flag that delegates directly to Z_quark or Z_lepton.
why it matters
The definition supplies the Z argument to massCanonFromWord, which then calls rungFrom and Derivation.massCanonPure to obtain the canonical pure mass. It therefore participates in the φ-ladder mass formula inside the Masses domain, even though the module itself is still a narrative scaffold. The construction touches the open question of replacing the zero stubs with the non-trivial maps that appear in RecogSpec.Scales and Physics.AnomalousMoments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.