conventions_differ_bottom
The bottom quark receives distinct rational coordinates under the integer-rung core model versus the quarter-ladder hypothesis. Modelers separating geometric derivations from phenomenological fits cite the result to keep the two layers independent. The proof reduces the stated inequality to a direct numerical check by unfolding the two definitions and normalizing.
claimLet $b_0$ be the rational rung coordinate assigned to the bottom quark in the integer-rung core convention and let $b_h$ be the bottom position in the quarter-ladder hypothesis. Then $b_0 ≠ b_h$.
background
Recognition Science places fermions on a phi-ladder whose rungs are fixed by the self-similar point phi and the eight-tick octave. The core convention restricts every particle to integer rungs, with down-type quarks occupying the set {4,15,21}; masses follow the yardstick formula m = yardstick(S) × phi^(r-8+gap(Z)). A separate exploratory layer relaxes this to quarter-integer residues relative to the electron structural mass, placing the bottom quark at -2.00. The module records that these two assignments serve different purposes and are not required to agree. Upstream rung definitions in the constants module supply the integer values used by the core layer.
proof idea
The term proof first simplifies the two record projections core_down_rungs.b and hypothesis_positions.bottom, then applies norm_num to compare the resulting rationals and discharge the inequality.
why it matters in Recognition Science
The theorem implements the layer separation stated in the module doc-comment, keeping the canonical integer-rung derivation distinct from the quarter-ladder hypothesis that improves heavy-quark accuracy. It thereby protects the parameter-free core from contamination by empirical adjustments. No downstream theorems are recorded, yet the result closes one concrete instance of the general claim that the two conventions differ.
scope and limits
- Does not claim the integer-rung and quarter-ladder assignments coincide for any quark.
- Does not derive the quarter-ladder residues from the forcing chain or RCL.
- Does not extend the inequality to up quarks or leptons.
- Does not quantify mass-prediction errors under either convention.
formal statement (Lean)
187theorem conventions_differ_bottom :
188 (core_down_rungs.b : ℚ) ≠ hypothesis_positions.bottom := by
proof body
Term-mode proof.
189 simp only [core_down_rungs, hypothesis_positions]
190 norm_num
191
192/-! ## Hypothesis marker (no axiom) -/
193
194/-- **HYPOTHESIS**: Quarks require fractional rungs for sub-percent accuracy.
195
196This is an EMPIRICAL observation, not a derived theorem:
197- The core integer-rung model predicts quark masses with larger errors
198- The quarter-ladder hypothesis achieves <2% accuracy for heavy quarks
199- This definition is a *marker* for hypothesis-dependent claims; it is **not** an `axiom`. -/