Z_lepton
plain-language theorem explainer
Z_lepton supplies a constant-zero placeholder for lepton ribbon integers in the mass model. Downstream code in anomalous moments and scales cites it to treat leptons as uniform demo inputs. The implementation is a direct lambda ignoring its argument and returning zero.
Claim. $Z_ lepton : ℤ → ℤ$ is the constant map $Z_ lepton(q) = 0$ for any integer charge index $q$.
background
The Recognition Science mass model assigns particles to the phi-ladder via integer Z values derived from charge and sector. Tick denotes the fundamental time quantum τ₀ = 1. A counts active edges per tick and equals 1. The module records phi-ladder ribbon machinery as a narrative scaffold whose RS derivations remain unformalised; downstream code treats the definitions as demo inputs.
proof idea
The definition is a direct constant function that maps every integer to zero. No lemmas or tactics are invoked.
why it matters
Z_lepton feeds Z_of_charge to select the lepton branch and supports anomalous_moment and gap_lepton in Physics.AnomalousMoments. It stands in for the full Z computation from the Recognition Composition Law until the ribbon machinery is formalised. It touches the open question of deriving exact lepton Z from the eight-tick octave and D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.