modules
plain-language theorem explainer
modules supplies the manifest list of four core modules in the Masses domain. Researchers deriving mass spectra or auditing zero-parameter certificates reference it to confirm the documented scope. The definition is a direct list literal of ModuleSummary records, each tied to Paper1.
Claim. The masses manifest is the list of four ModuleSummary entries: Anchor (canonical constants, Paper1), AnchorPolicy (policy interfaces, Paper1), Assumptions (model assumptions, Paper1), and Basic (mass ladder placeholder, Paper1).
background
ModuleSummary is the structure with fields name, description, and manuscript. In the Masses.Manifest module this definition assembles the documented components that support mass derivations. Upstream, Mass is the real line in RS-native units, Model packages defectMass, orthoMass, energyGap and tests, and AnchorPolicy supplies the pair (lambda, kappa) for coherence anchoring.
proof idea
The definition is a direct list literal of the four ModuleSummary records. No lemmas or tactics are invoked; the body is the explicit enumeration.
why it matters
This definition fixes the scope of the Masses manifest, which is imported by H_RSZeroParameterStatus, ml_derivation_complete, and ml_zero_parameter_certificate. It anchors the mass-ladder construction that feeds the phi-ladder formula and the zero-external-parameter claim for M/L ratios. It touches the open unification of all constant derivations into one master certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.