quark_fractional_rung_necessity
plain-language theorem explainer
The declaration defines a proposition that the rational rung value for the top quark in the integer core model differs from the top position in the quarter-ladder hypothesis. Mass hierarchy modelers cite it as an empirical marker when separating the parameter-free geometric core from phenomenological adjustments that reach sub-percent accuracy. The definition is a direct comparison of the two rational assignments drawn from the respective layers.
Claim. Let $r_{core,t}$ be the rational rung for the top quark under the integer-rung core convention and $r_{hyp,t}$ the corresponding top position under the quarter-ladder hypothesis. The proposition asserts $r_{core,t} ≠ r_{hyp,t}$.
background
Recognition Science places particle masses on the phi-ladder via the formula $m =$ yardstick(Sector) $× φ^{r-8+gap(Z)}$, with integer rungs for the canonical core model. The module separates this from the quarter-ladder hypothesis, which assigns fractional residues (e.g., top at 23/4) relative to the electron structural mass to improve accuracy for heavy quarks. Upstream structures include SpectralEmergence (forcing SU(3)×SU(2)×U(1) and three generations from Q3 geometry) and J-cost minimization (convexity of $J(x)=(x+1/x)/2-1$ yielding the unique minimum at $x=1$).
proof idea
The definition is a one-line wrapper that sets the proposition equal to the inequality between the core top-rung rational and the hypothesis top position.
why it matters
It formally closes Gap 6 by documenting that the two quark coordinate conventions serve distinct layers: integer rungs remain canonical and parameter-free while the quarter-ladder is exploratory. The marker supports mass-law refinements without contaminating the core derivation from the forcing chain (T5 J-uniqueness through T8 D=3). No downstream theorems depend on it yet, leaving the hypothesis status explicit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.