quark_rungs
plain-language theorem explainer
Quark baseline rung is fixed at 4 by the edges-per-face count on the 3-cube. Recognition Science mass derivations cite this to anchor the phi-ladder starting points for the three quark generations. The proof proceeds by unfolding the definitions of quark baseline and edges per face then deciding the three arithmetic statements by native computation.
Claim. The quark baseline rung satisfies $r = 4$, $r + e_p(D) = 15$, and $r + w = 21$, where $r$ denotes the quark baseline rung, $e_p(D)$ the passive field edges at spatial dimension $D=3$, and $w$ the number of wallpaper groups.
background
The module derives baseline rung integers from the combinatorics of the 3-cube Q3. Quark baseline is defined as the number of edges per face, which equals $2^{D-1}$. For $D=3$ this yields 4. Passive field edges are the total cube edges minus active edges per tick, evaluating to 11 at $D=3$. Wallpaper groups are the 17 distinct 2D crystallographic groups identified by Fedorov.
proof idea
The proof unfolds the definitions of quark baseline and edges per face. It then applies the constructor tactic to split the conjunction into three goals and resolves each by native_decide, which computes the equalities directly.
why it matters
This theorem supplies the B-12 item in the baseline derivations table, fixing the quark rung at 4. It supports the mass formula yardstick times phi to the power of rung minus 8 plus gap. The result closes part of the cube-geometry derivation chain that begins from D=3 and feeds the Recognition Composition Law applications in mass spectra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.