mass_ladder_assumption
plain-language theorem explainer
The mass_ladder_assumption encodes the predicate that every entry in the imported measurement list satisfies the absolute error bound against phi raised to its rung exponent. Model-layer auditors of the Recognition Science mass spectrum would cite this predicate when checking consistency between surrogate data and the phi-ladder formula. The definition is a direct universal quantification that unfolds over the hardcoded list without invoking further lemmas.
Claim. The assumption states that for every measurement $m$ in the imported list, $|m.value - phi^{rung_exponent(m.name)}| ≤ m.error$, where $phi$ is the self-similar fixed point and rung_exponent maps each particle name to its integer ladder position.
background
In the Masses.Assumptions module the mass ladder is treated as a model-layer predicate. The rung_exponent definition assigns the integer 11 to the name mu_e, 6 to tau_mu, and 0 otherwise. The import_measurements list supplies surrogate values such as the inverse fine-structure constant 137.035999084 with its error, together with other electroweak and QCD parameters. This predicate therefore asserts that the listed measurements already lie inside the phi-ladder tolerance.
proof idea
The declaration is a plain definition whose body is the universal quantifier over the measurement list. It applies the rung_exponent function to each name and compares the resulting phi power against the stored value and error; no lemmas are invoked.
why it matters
The predicate is the hypothesis required by mass_ladder_holds and mass_ladder_matches_pdg in the Basic module, which in turn support the proton_relative_error verification. It supplies the model-layer placeholder for the mass formula audit that connects to the phi-ladder scaling yardstick * phi^(rung-8+gap(Z)) and the eight-tick octave structure. The open question it leaves is the first-principles derivation of the rung assignments from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.