hypothesis_claims_properly_located
plain-language theorem explainer
The theorem verifies that the four hypothesis-dependent quark mass claims reside exclusively in the Physics module. A physicist separating canonical integer-rung derivations from exploratory quarter-ladder fits would cite it to enforce layer boundaries. The proof is a direct membership check that unfolds the definition of hypothesis_dependent_claims.
Claim. Every claim $c$ belonging to the list of hypothesis-dependent claims satisfies $c$ equals one of H_top_mass_match, H_bottom_mass_match, H_charm_mass_match, or quark_mass_verified.
background
The module separates two quark coordinate conventions. Integer rungs form the canonical core: all particles occupy integer positions on the φ-ladder with mass given by yardstick(Sector) × φ^(r-8 + gap(Z)). Quarter-ladder is the exploratory hypothesis layer that places quarks at quarter-integer residues relative to electron structural mass for tighter phenomenological fits (top at 5.75, bottom at -2.00, charm at -4.50). hypothesis_dependent_claims is the list containing exactly the four claims H_top_mass_match, H_bottom_mass_match, H_charm_mass_match, and quark_mass_verified. Each H_ claim is a Prop asserting that the absolute relative error between predicted and experimental mass lies below a stated tolerance (0.0005 for top, 0.01 for bottom, 0.02 for charm). quark_mass_verified packages the three H_ claims into a single QuarkMassCert certificate.
proof idea
The term proof introduces an arbitrary element c together with the membership hypothesis hc from hypothesis_dependent_claims and returns hc unchanged, confirming that every listed claim belongs to the enumerated set.
why it matters
The declaration closes the layer-separation argument stated in the module header: the two conventions are deliberately non-equivalent, with quarter-ladder confined to the hypothesis lane. It supplies the static check that the mass-match claims (H_top_mass_match etc.) do not leak into the canonical Masses/ files. No downstream theorems depend on it, so it functions as an internal guard rather than a lemma in a larger derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.