quark_baseline_eq
plain-language theorem explainer
The quark baseline rung is fixed at 4 by the edges-per-face count in the 3-cube. Researchers deriving masses on the phi-ladder would cite this to anchor the starting rung for the quark sector. The proof is a one-line term reduction that unfolds the definition and invokes the D=3 geometry theorem.
Claim. At spatial dimension $D=3$, the quark baseline rung equals 4, where the baseline is the number of edges per face of the $D$-cube.
background
This module upgrades boundary assumptions to derived status by tracing them to the single input $D=3$ and the combinatorics of the 3-cube $Q_3$. The quark baseline (item B-12) is obtained as $2^{D-1}$, evaluating to 4. The function edges_per_face counts edges incident to each face in the hypercube geometry, and the upstream theorem edges_per_face_at_D3 asserts the value 4 directly by native decision at $D=3$.
proof idea
The proof is a term-mode reduction: it unfolds the definition quark_baseline := edges_per_face D and then applies the theorem edges_per_face_at_D3, which states that this quantity equals 4 at $D=3$.
why it matters
This result supplies the starting rung for quarks in the mass formula yardstick * phi^(rung-8+gap(Z)). It is referenced downstream by the neutrino rung derivation. Within the Recognition Science framework it realizes the B-12 derivation step, confirming that the quark baseline traces directly to the forced $D=3$ from the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.