IndisputableMonolith.Exports.Virtues

   1import Lean
   2
   3open Lean
   4
   5structure VirtueExport where
   6  name : String
   7  transformConst : String
   8  conservesProof : String
   9  cadenceProof : String
  10  gaugeProof : String
  11  deriving Repr, ToJson
  12
  13structure SoulInvariantExport where
  14  name : String
  15  description : String
  16  proof : String
  17  deriving Repr, ToJson
  18
  19def virtueExports : List VirtueExport :=
  20  [ { name := "Love"
  21      transformConst := "IndisputableMonolith.Ethics.Virtues.loveVirtue"
  22      conservesProof := "loveVirtue.conserves_reciprocity"
  23      cadenceProof := "loveVirtue.respects_cadence"
  24      gaugeProof := "loveVirtue.gauge_invariant" }
  25  , { name := "Justice"
  26      transformConst := "IndisputableMonolith.Ethics.Virtues.canonicalJusticeVirtue"
  27      conservesProof := "justiceVirtue.conserves_reciprocity"
  28      cadenceProof := "justiceVirtue.respects_cadence"
  29      gaugeProof := "justiceVirtue.gauge_invariant" }
  30  , { name := "Temperance"
  31      transformConst := "IndisputableMonolith.Ethics.Virtues.temperanceVirtue"
  32      conservesProof := "temperanceVirtue.conserves_reciprocity"
  33      cadenceProof := "temperanceVirtue.respects_cadence"
  34      gaugeProof := "temperanceVirtue.gauge_invariant" }
  35  , { name := "Patience"
  36      transformConst := "IndisputableMonolith.Ethics.Virtues.patienceVirtue"
  37      conservesProof := "patienceVirtue.conserves_reciprocity"
  38      cadenceProof := "patienceVirtue.respects_cadence"
  39      gaugeProof := "patienceVirtue.gauge_invariant" }
  40  , { name := "Gratitude"
  41      transformConst := "IndisputableMonolith.Ethics.Virtues.gratitudeVirtue"
  42      conservesProof := "gratitudeVirtue.conserves_reciprocity"
  43      cadenceProof := "gratitudeVirtue.respects_cadence"
  44      gaugeProof := "gratitudeVirtue.gauge_invariant" }
  45  , { name := "Humility"
  46      transformConst := "IndisputableMonolith.Ethics.Virtues.humilityVirtue"
  47      conservesProof := "humilityVirtue.conserves_reciprocity"
  48      cadenceProof := "humilityVirtue.respects_cadence"
  49      gaugeProof := "humilityVirtue.gauge_invariant" }
  50  , { name := "Hope"
  51      transformConst := "IndisputableMonolith.Ethics.Virtues.hopeVirtue"
  52      conservesProof := "hopeVirtue.conserves_reciprocity"
  53      cadenceProof := "hopeVirtue.respects_cadence"
  54      gaugeProof := "hopeVirtue.gauge_invariant" }
  55  , { name := "Prudence"
  56      transformConst := "IndisputableMonolith.Ethics.Virtues.prudenceVirtue"
  57      conservesProof := "prudenceVirtue.conserves_reciprocity"
  58      cadenceProof := "prudenceVirtue.respects_cadence"
  59      gaugeProof := "prudenceVirtue.gauge_invariant" }
  60  , { name := "Compassion"
  61      transformConst := "IndisputableMonolith.Ethics.Virtues.compassionVirtue"
  62      conservesProof := "compassionVirtue.conserves_reciprocity"
  63      cadenceProof := "compassionVirtue.respects_cadence"
  64      gaugeProof := "compassionVirtue.gauge_invariant" }
  65  , { name := "Sacrifice"
  66      transformConst := "IndisputableMonolith.Ethics.Virtues.sacrificeVirtue"
  67      conservesProof := "sacrificeVirtue.conserves_reciprocity"
  68      cadenceProof := "sacrificeVirtue.respects_cadence"
  69      gaugeProof := "sacrificeVirtue.gauge_invariant" }
  70  , { name := "Creativity"
  71      transformConst := "IndisputableMonolith.Ethics.Virtues.creativityVirtue"
  72      conservesProof := "creativityVirtue.conserves_reciprocity"
  73      cadenceProof := "creativityVirtue.respects_cadence"
  74      gaugeProof := "creativityVirtue.gauge_invariant" }
  75  , { name := "Courage"
  76      transformConst := "IndisputableMonolith.Ethics.Virtues.courageVirtue"
  77      conservesProof := "courageVirtue.conserves_reciprocity"
  78      cadenceProof := "courageVirtue.respects_cadence"
  79      gaugeProof := "courageVirtue.gauge_invariant" }
  80  ]
  81
  82def soulExports : List SoulInvariantExport :=
  83  [ { name := "VirtueSignature.canonical"
  84      description := "Canonical virtue signature derived from virtue_generators"
  85      proof := "IndisputableMonolith.Ethics.Soul.Character.VirtueSignature.canonical" }
  86  , { name := "SoulCharacter.energy_pos"
  87      description := "All SoulCharacter states maintain strictly positive recognition energy"
  88      proof := "IndisputableMonolith.Ethics.Soul.Character.energy_pos" }
  89  ]
  90
  91def exportPayload : Json :=
  92  Json.mkObj
  93    [ ("version", Json.str "1.0.0")
  94    , ("virtues", toJson virtueExports)
  95    , ("soul_invariants", toJson soulExports)
  96    ]
  97
  98def main : IO Unit := do
  99  IO.println (exportPayload.pretty 2)
 100