IndisputableMonolith.Masses.Manifest

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace Masses
   5
   6structure ModuleSummary where
   7  name : String
   8  description : String
   9  manuscript : String
  10
  11@[simp] def modules : List ModuleSummary :=
  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
  20