different_references
plain-language theorem explainer
The two quark mass conventions rest on unequal reference masses: Convention A uses sector-specific yardsticks, Convention B a single electron structural mass. Auditors of the dual-coordinate blocker cite this as a named fact in the quark-sector ledger. The proof is the trivial inhabitant of True, a documentation marker rather than an algebraic derivation.
Claim. The two coexisting quark mass conventions employ distinct reference masses: one uses sector-specific yardsticks (different for up-type and down-type), the other a single electron structural mass base for all quarks.
background
The Quark Sector Audit module records the main obstacle to an end-to-end fermion mass claim: two coordinate conventions for quarks that are not mathematically equivalent and have not been merged into one forward pipeline.
Convention A (canonical core, from the mass-law and anchor modules) writes $m = \mathrm{yardstick}(\mathrm{Sector}) \times \varphi^{r-8+\mathrm{gap}(Z)}$ with integer rungs and distinct up-type versus down-type yardsticks. Convention B (hypothesis module) writes $m = m_{e,\mathrm{struct}} \times \varphi^{R}$ with a shared electron structural mass and quarter-integer residues $R \in \tfrac14\mathbb{Z}$.
This declaration isolates one concrete mismatch: the reference mass each convention multiplies against the $\varphi$-ladder. Sibling markers cover rung-type and generation-spacing differences; together they inventory why reconciliation is still open.
proof idea
Term-mode one-liner: the goal is True, discharged by trivial. No lemmas are applied. Inline comments fix the intended reading (sector yardsticks versus single electron structural mass) so the name is auditable even though the proposition carries no algebraic content.
why it matters
In the Recognition mass framework the lepton chain is parameter-free on one ladder; quarks are not yet on the same footing. The module doc states that until the sector is reconciled into one coordinate system, "correct for all fermions" is not defensible, and that the two conventions are explicitly not meant to be equivalent.
This marker pins the reference-mass half of that dual-coordinate problem (yardstick versus electron structural mass). It sits beside sibling audit facts on rung types, generation spacing, and light-quark accuracy, and feeds the narrative that no reconciliation proof exists yet. It does not itself close the gap; it makes the blocker citable inside the verification layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.