core_uses_integer_rungs
plain-language theorem explainer
The integer-rung quark mass convention is formally assigned to the core (parameter-free) model layer. Anyone citing the canonical φ-ladder mass law for quarks uses this to keep that placement separate from the exploratory quarter-ladder. The proof is pure definitional equality: reflexivity on the layer-assignment map.
Claim. Under the formal layer assignment of quark coordinate conventions, the integer-rung convention sits in the core model layer: $\mathrm{layer}(\mathrm{IntegerRung})=\mathrm{Core}$.
background
This module resolves Gap 6 in the Recognition Science mass sector: two coexisting quark coordinate conventions that are not meant to be mathematically equivalent. They serve different roles and live on different layers.
Convention A (integer rungs) is the canonical core placement. All particles occupy integer rungs on the φ-ladder, with sector yardsticks fixed by cube geometry. Up and down quarks use $r\in{4,15,21}$; leptons use $r\in{2,13,19}$. Masses follow $m=\mathrm{yardstick}(\mathrm{Sector})\times\varphi^{r-8+\mathrm{gap}(Z)}$.
Convention B (quarter-ladder) is a phenomenological hypothesis: quarks sit on quarter-integer residues relative to the electron structural mass (e.g. top at $R=5.75=23/4$). The map convention_layer sends IntegerRung to Core and QuarterLadder to Hypothesis, making that split machine-checkable.
proof idea
One-line term proof by rfl. Unfolding convention_layer on the IntegerRung constructor yields Core by the defining equation of the layer map, so the equality is definitional.
why it matters
Gap 6 is closed by layer separation rather than by forcing the two conventions to agree. This theorem pins the integer-rung side as core: the parameter-free derivation from geometry that feeds the standard RS mass formula on the φ-ladder (yardstick times $\varphi^{r-8+\mathrm{gap}(Z)}$). The quarter-ladder remains explicitly exploratory, with its own companion statement that it is hypothesis-layer only.
No downstream consumers are wired yet; the declaration is a documentation lock so later mass and hierarchy work cannot silently promote quarter-residues into the core. It sits next to the rung-fraction support (quarter : $\mathbb{Z}\to$ Rung) without importing that embedding into the canonical model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.