Z_quark
plain-language theorem explainer
The quark Z function maps an integer charge Q to the value 4 plus (6Q) squared plus (6Q) to the fourth. Mass computations cite this expression when the sector flag selects the quark branch. The definition is a direct closed-form polynomial with no lemmas or reduction steps.
Claim. $Z(Q) = 4 + (6Q)^2 + (6Q)^4$ for integer charge $Q$.
background
The Scales module supplies binary scales and φ-exponential wrappers for mass quantities. This definition gives the concrete quartic polynomial for the quark Z value. It replaces the zero-returning placeholder from the upstream Ribbons module, whose doc-comment describes a noncomputable stub returning zero for all inputs.
proof idea
The declaration is a direct definition that assigns the polynomial expression 4 + (6 * Q)^2 + (6 * Q)^4. No lemmas are applied and no tactics are invoked; it is a one-line algebraic assignment.
why it matters
This supplies the quark-specific formula invoked by the charge-based Z selector to compute canonical pure mass from word, generation class, and charge. It completes the quark branch of the mass formula in the Recognition Science framework, consistent with the phi-ladder scaling landmark. It discharges the placeholder stub in the Ribbons module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.