hypothesis_dependent_claims
plain-language theorem explainer
The definition enumerates the four propositions whose validity rests on the quarter-ladder hypothesis for quark placement. A researcher separating the canonical integer-rung core from exploratory adjustments would cite the list to track which mass predictions carry extra assumptions. It is realized by direct enumeration of the relevant identifiers drawn from the QuarkMasses module.
Claim. The list of hypothesis-dependent claims is the set containing the top-quark mass-match proposition, the bottom-quark mass-match proposition, the charm-quark mass-match proposition, and the joint quark-mass verification theorem, where each mass-match proposition asserts that the absolute relative error between the quarter-ladder prediction and the experimental mass lies below the stated tolerance.
background
The Quark Coordinate Reconciliation module maintains two non-equivalent conventions for locating quarks on the phi-ladder. The integer-rung convention is canonical and derives masses parameter-free from cube geometry via the formula m = yardstick(Sector) × phi^(r - 8 + gap(Z)). The quarter-ladder convention is an exploratory hypothesis that places quarks at quarter-integer residues relative to the electron structural mass to achieve sub-percent accuracy for the heavy flavors.
proof idea
The declaration is a direct list definition that enumerates the four string identifiers of the hypothesis claims. No lemmas or tactics are invoked; the body simply records the names H_top_mass_match, H_bottom_mass_match, H_charm_mass_match, and quark_mass_verified taken from the upstream QuarkMasses module.
why it matters
The definition supplies the input list for the downstream theorem hypothesis_claims_properly_located, which verifies that all listed claims reside inside the Physics module. It thereby implements the layer separation stated in the module documentation, keeping the parameter-free integer-rung derivations distinct from the quarter-ladder adjustments that improve heavy-quark predictions. The construction interfaces with the phi-ladder lattice hypothesis structure whose Poisson-summation property remains to be discharged analytically.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.