Z_quark
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 in Recognition Science
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.
scope and limits
- Does not handle lepton Z values.
- Does not include phi-ladder rung or gap adjustments.
- Does not reference J-uniqueness or the recognition composition law.
- Does not depend on the eight-tick octave or spatial dimension D=3.
Lean usage
Z_of_charge true (6 * Q)formal statement (Lean)
93@[simp] def Z_quark (Q : ℤ) : ℤ := 4 + (6 * Q) ^ (2 : Nat) + (6 * Q) ^ (4 : Nat)