pith. machine review for the scientific record. sign in
def definition def or abbrev high

modules

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  11@[simp] def modules : List ModuleSummary :=

proof body

Definition body.

  12  [ { name := "Anchor", description := "Canonical constants", manuscript := "Paper1" }
  13  , { name := "AnchorPolicy", description := "Policy interfaces", manuscript := "Paper1" }
  14  , { name := "Assumptions", description := "Model assumptions", manuscript := "Paper1" }
  15  , { name := "Basic", description := "Mass ladder placeholder", manuscript := "Paper1" }
  16  ]
  17
  18end Masses
  19end IndisputableMonolith

used by (28)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.