conventions_differ_top_quark
plain-language theorem explainer
The theorem shows that the integer rung for the top quark in the canonical core model differs from its quarter-ladder position in the exploratory hypothesis. Researchers reconciling quark mass derivations across layers would cite this result to confirm the conventions remain distinct. The proof reduces directly to numerical comparison of the two fixed definitions via simplification and rational arithmetic.
Claim. Let $r_t$ denote the integer rung assigned to the top quark in the core up-quark rungs and $R_t$ the quarter-ladder position in the hypothesis positions. Then $r_t ≠ R_t$.
background
The module separates two quark coordinate systems. Integer rungs form the canonical core: up quarks occupy r ∈ {4, 15, 21} on the φ-ladder, with masses given by yardstick(Sector) × φ^(r - 8 + gap(Z)). Quarter-ladder positions form the hypothesis layer: top quark at R = 5.75 = 23/4, chosen for phenomenological match under 0.05%. The upstream structure records meta-realization properties required by orbit coherence axioms but supplies no numerical values here. The two definitions core_up_rungs and hypothesis_positions are the concrete carriers of these assignments.
proof idea
One-line wrapper that applies simp to unfold the two definitions, then norm_num to compare the resulting rationals and close the inequality.
why it matters
It supplies the explicit non-equivalence statement required by the module's resolution summary, confirming that integer rungs and quarter-ladder positions serve separate purposes. The result anchors the layer separation between parameter-free core and exploratory hypothesis, consistent with the φ-ladder mass formula and the eight-tick octave structure. No downstream theorems depend on it yet; it functions as a boundary marker for the reconciliation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.