nearest_int_positions
plain-language theorem explainer
The theorem computes the nearest integer rungs to the six canonical quarter-ladder quark positions, yielding 6 for top, -2 for bottom, -4 for charm, -10 for strange, -16 for down and -18 for up. Model builders reconciling the exploratory quarter-ladder hypothesis with the canonical integer-rung core in Recognition Science would cite these explicit mappings. The proof is a one-line wrapper that simplifies the floor-function definition against the position constants and dispatches the six equalities by native decision.
Claim. Let $R$ map each quark to its quarter-ladder position and let $N(q) = ⌊q + 1/2⌋$. Then $N(R_t) = 6$, $N(R_b) = -2$, $N(R_c) = -4$, $N(R_s) = -10$, $N(R_d) = -16$ and $N(R_u) = -18$.
background
The module separates two quark coordinate systems. Integer rungs form the canonical core model, with every fermion assigned an integer rung on the φ-ladder via sector-specific yardsticks. Quarter-ladder positions form an exploratory hypothesis layer that places quarks at quarter-integer residues relative to the electron structural mass, achieving sub-2% mass matches for the heavy states. The function quarter_to_nearest_int converts any quarter position $q$ to the nearest integer rung by the rule ⌊q + 1/2⌋. hypothesis_positions supplies the six fixed quarter values: top at 5.75, bottom at -2, charm at -4.5, strange at -10, down at -16 and up at -17.75. Upstream rung definitions in the anchor modules supply the integer targets against which these nearest integers are compared.
proof idea
The proof is a one-line wrapper. It rewrites both quarter_to_nearest_int and hypothesis_positions by simp, then splits the conjunction with constructor and discharges each equality by native_decide on the concrete rational arithmetic.
why it matters
The result supplies the explicit numerical bridge between the quarter-ladder hypothesis and the integer-rung core, directly supporting the module's claim that the two conventions are not equivalent. It therefore closes one concrete gap in the layer-separation strategy for quark masses on the φ-ladder. No downstream theorems yet depend on it; the declaration stands as a self-contained reconciliation check inside the hypothesis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.