quark_mass_verified
plain-language theorem explainer
The declaration assembles three numerical agreement conditions for the top, bottom, and charm quark masses under the quarter-ladder phi positions into a single certificate. Researchers auditing the Recognition Science mass predictions would reference it to confirm the geometric matches for heavy quarks. The proof proceeds by direct record construction from the supplied hypothesis propositions.
Claim. Suppose the top quark satisfies $|m_{top}^{pred} - m_{top}^{exp}| / m_{top}^{exp} < 0.0005$, the bottom satisfies the bound 0.01, and the charm satisfies 0.02. Then the quarter-ladder certificate holds.
background
The module develops the quarter-ladder hypothesis for quark masses, placing them at quarter-integer rungs on the phi-ladder while sharing the structural base with leptons at sector gauge B=-22. The certificate structure collects the match propositions for the three heavy flavors. An upstream result from the hierarchy module establishes that quark masses follow a phi ratio across six flavors with positive values.
proof idea
The proof is a one-line term-mode construction that populates the QuarkMassCert structure by assigning the top, bottom, and charm match hypotheses to the corresponding fields.
why it matters
This result packages the hypothesis verifications for T12, the quark masses section. It is referenced by the reconciliation theorems that list hypothesis-dependent claims, ensuring separation from the core mass model. The quarter-ladder extends the phi-ladder mass formula to quarks with specific rung positions like 5.75 for top.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.