quark_baseline_matches_anchor_down
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.