quark_baseline_matches_anchor_up
plain-language theorem explainer
The theorem shows that the quark baseline rung computed from edges per face in the 3-cube equals the up-quark rung integer 4. A physicist constructing mass ladders from geometric rungs would cite this to confirm the anchor value for up-type quarks. The proof is a one-line simplification that reduces both sides to the numeral 4 via the defining expressions.
Claim. The quark baseline rung given by $2^{D-1}$ at $D=3$ equals the up-quark rung integer 4.
background
This module upgrades boundary assumptions about rung integers to derived status by tracing them to the combinatorics of the 3-cube Q_3. The central definitions are edges_per_face(d) := 2^{d-1}, which evaluates to 4 at D=3, and quark_baseline := edges_per_face D. The rung function r_up assigns the value 4 to the up quark while offsetting higher generations by tau(1) and tau(2).
proof idea
The proof is a one-line wrapper that applies simp to the definitions of quark_baseline, edges_per_face, D, and r_up, reducing both sides directly to 4.
why it matters
This result verifies consistency for the quark baseline (B-12) in the cube-geometry derivation chain that starts from D=3. It anchors the starting rung for up-type quarks in the mass formula yardstick * phi^(rung - 8 + gap(Z)). The declaration supports the overall upgrade of structural quantities from assumption to derivation without touching the phi-ladder or Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.