conventions_differ_charm
plain-language theorem explainer
The theorem records that the charm quark receives distinct rational coordinates under the integer-rung core model versus the quarter-ladder hypothesis. Model builders separating canonical geometry from phenomenological fits cite it to keep the two layers from being conflated. The proof reduces by direct unfolding of the two record definitions followed by numerical comparison.
Claim. Let $c$ denote the rational coordinate assigned to the charm quark. Then the value of $c$ under the canonical integer-rung assignment differs from its value under the quarter-ladder hypothesis: $c_0 = -4.5$ in the latter while the former places it at an integer rung offset.
background
The module distinguishes two quark coordinate systems inside the Recognition framework. Integer rungs form the canonical core: up-type quarks occupy rungs drawn from {4,15,21} on the φ-ladder, with masses obtained from the yardstick formula $m = y_S · φ^{r-8+gap(Z)}$. Quarter-ladder positions constitute an exploratory hypothesis layer that places quarks at quarter-integer residues relative to the electron structural mass, yielding charm at R = -4.50 for a reported match under 2 percent.
proof idea
One-line wrapper that unfolds the record definitions core_up_rungs and hypothesis_positions then invokes numerical normalization to discharge the inequality on the charm field.
why it matters
The declaration supplies an explicit witness that the integer-rung and quarter-ladder conventions are deliberately non-equivalent for charm, thereby closing the layer-separation claim stated in the module header. It sits downstream of the meta-realization structure for and the two record definitions, reinforcing the canonical status of geometry-derived rungs while isolating the phenomenological adjustments. No parent theorem consumes it directly, yet it prevents conflation when the φ-ladder mass law is applied across sectors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.