quark_baseline_matches_anchor_down
The theorem establishes equality between the baseline rung integer for the down quark and the downward integer anchor r_down for label d in the Recognition Science mass ladder. Researchers deriving particle masses from cube geometry and the phi-ladder would cite this result to fix the zero point for quark rungs. The proof is a one-line simplification that unfolds the definitions of quark_baseline, edges_per_face, spatial dimension D, and the anchor function to reach numerical equality.
claimThe baseline rung integer for the down quark equals the downward integer anchor $r_↓(d)$.
background
This module derives baseline rung integers, octave offsets, and color offsets from the combinatorics of the 3-cube Q₃, upgrading prior boundary assumptions to derived status. The quark baseline is defined as 2^{D-1} with D=3 the spatial dimension; the same expression supplies the color offset for quarks via face-coupling in the Z-map. Upstream results include the structure of J-cost from PhiForcingDerived.of and the derivation of integers from logic primitives.
proof idea
The term proof applies simp to the definitions of quark_baseline, edges_per_face, D, and Integers.r_down. Both sides reduce directly to the common integer value 4.
why it matters in Recognition Science
The result completes derivation of the quark baseline rung (B-12) from D=3 cube geometry, placing it inside the mass formula yardstick × φ^(rung − 8 + gap(Z)). It draws on the eight-tick octave and D=3 from the unified forcing chain (T7–T8). No downstream uses are recorded yet, but the theorem supports the broader program of converting boundary assumptions into derived quantities.
scope and limits
- Does not compute numerical quark masses.
- Does not incorporate generation mixing.
- Does not derive lepton or neutrino baselines.
- Does not address higher-order Z-map corrections.
formal statement (Lean)
176theorem quark_baseline_matches_anchor_down :
177 (quark_baseline : ℤ) = Integers.r_down "d" := by
proof body
Term-mode proof.
178 simp [quark_baseline, edges_per_face, D, Integers.r_down]
179
180/-! ## B-25: Color offset in Z-map = 2^(D−1)
181
182The color offset c in the charge index Z = aQ̃² + bQ̃⁴ + c (for quarks)
183equals the number of edges per face of Q_D. Quarks carry color charge
184(face-coupling), so their Z-index receives an additive offset equal to
185the edge count of one face: c = 2^(D−1) = 4. -/
186
187/-- **B-25 DERIVED**: Color offset from face edge count. -/