`MicroMove`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

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

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

  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
  62  unfold pairList
  63  simp only [mem_sort]
  64
  65lemma pairList_nodup (nf : NormalForm) : (pairList nf).Nodup := by
  66  unfold pairList
  67  simp only [sort_nodup]
  68
  69/-- Micro-moves for a single pair. -/

papers checked against this theorem

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