Masses Assumptions

Masses assumptions

Masses assumptions is the model layer of Recognition Science that centralises the phenomenological assumptions used by the masses modules. It is intentionally lightweight and sits in the Model portion of the codebase. The module defines two predicates: mass_ladder_assumption and sterile_exclusion_assumption. These are assumptions, not theorems; they are definitional choices about what the masses modules may take as given.

The mass ladder assumption states that every imported measurement m satisfies |m.value - phi ^ rung_exponent m.name| ≤ m.error. In plain language, each measured mass sits within its measurement error of the phi-power value assigned to its rung. This is a placeholder for the ladder audit: the module currently assumes the bound holds for the imported measurements, and the docstring notes that the surrogate is pending. The sterile exclusion assumption is an alias for the physics-side sterile exclusion assumption, imported as a surrogate.

What this module establishes is narrow. It does not prove that masses lie on the ladder; it defines the predicate that would assert they do, and it currently assumes that predicate for the imported data. The distinction matters because the scaling law for particle masses is established elsewhere, but the comparison against measured PDG values is an empirical check, not a theorem. This module marks the boundary where the framework stops proving and starts assuming, for the purposes of the masses modules.

MODEL mass_ladder_assumption · IndisputableMonolith/Masses/Assumptions.lean

MODEL mass_ladder_assumption · IndisputableMonolith/Masses/Assumptions.lean

MODEL sterile_exclusion_assumption · IndisputableMonolith/Masses/Assumptions.lean

What this page does not claim

This module does not prove that measured masses lie on the phi-power ladder. This module does not derive the phi-power scaling law for particle masses. This module does not establish the sterile exclusion assumption from first principles.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Masses/Assumptions.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: