`primitive_mem_order`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

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

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

  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
  49  supportPairs : Finset ℕ
  50  coeff : ℕ → Primitive → ℝ
  51  zero_outside : ∀ {pair prim}, pair ∉ supportPairs → coeff pair prim = 0
  52  nontrivial : ∀ {pair}, pair ∈ supportPairs → ∃ prim, coeff pair prim ≠ 0
  53
  54namespace NormalForm
  55
  56/-- Canonical ordered list of supported pairs (ascending). -/
  57noncomputable def pairList (nf : NormalForm) : List ℕ :=
  58  nf.supportPairs.sort (· ≤ ·)
  59
  60lemma pairList_mem {nf : NormalForm} {pair : ℕ} :
  61    pair ∈ pairList nf ↔ pair ∈ nf.supportPairs := by

papers checked against this theorem

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