`Primitive`

definition

show as: view math explainer →

module: IndisputableMonolith.Ethics.Virtues.NormalForm
domain: Ethics
line: 18 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Ethics.Virtues.NormalForm on GitHub at line 18.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  15open Finset
  16
  17/-- Primitive generators in fixed canonical order. -/
  18inductive Primitive
  19  | Love | Justice | Forgiveness | Wisdom | Courage | Temperance | Prudence
  20  | Compassion | Gratitude | Patience | Humility | Hope | Creativity | Sacrifice
  21  deriving DecidableEq, Repr
  22
  23/-- Canonical primitive order as a list. -/
  24def primitiveOrderList : List Primitive :=
  25  [ Primitive.Love, Primitive.Justice, Primitive.Forgiveness,
  26    Primitive.Wisdom, Primitive.Courage, Primitive.Temperance,
  27    Primitive.Prudence, Primitive.Compassion, Primitive.Gratitude,
  28    Primitive.Patience, Primitive.Humility, Primitive.Hope,
  29    Primitive.Creativity, Primitive.Sacrifice ]
  30
  31lemma primitive_mem_order (p : Primitive) : p ∈ primitiveOrderList := by
  32  cases p <;> simp [primitiveOrderList]
  33
  34lemma primitiveOrderList_nodup : primitiveOrderList.Nodup := by
  35  unfold primitiveOrderList
  36  decide
  37
  38/-- Micro moves: (pair scope, primitive, coefficient). -/
  39structure MicroMove where
  40  pair : ℕ
  41  primitive : Primitive
  42  coeff : ℝ
  43
  44namespace MicroMove
  45
  46/-- Canonical micro-move normal form: coefficient table with finite support. -/
  47@[ext]
  48structure NormalForm where

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.