`intCost_self`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.UniversalForcing.Strict.Ordered
domain: Foundation
line: 18 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.UniversalForcing.Strict.Ordered 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

  15def intCost (a b : ℤ) : Nat :=
  16  if a = b then 0 else 1
  17
  18@[simp] theorem intCost_self (a : ℤ) : intCost a a = 0 := by
  19  simp [intCost]
  20
  21theorem intCost_symm (a b : ℤ) : intCost a b = intCost b a := by
  22  by_cases h : a = b
  23  · subst h
  24    simp [intCost]
  25  · have h' : b ≠ a := by intro hb; exact h hb.symm
  26    simp [intCost, h, h']
  27
  28/-- Strict ordered integer realization. -/
  29def strictOrderedRealization : StrictLogicRealization where
  30  Carrier := ℤ
  31  Cost := Nat
  32  zeroCost := inferInstance
  33  compare := intCost
  34  compose := fun a b => a + b
  35  one := 0
  36  generator := 1
  37  identity_law := intCost_self
  38  non_contradiction_law := intCost_symm
  39  excluded_middle_law := True
  40  composition_law := True
  41  invariance_law := True
  42  nontrivial_law := by
  43    simp [intCost]
  44
  45def strictOrdered_arith_equiv_logicNat :
  46    (StrictLogicRealization.arith strictOrderedRealization).peano.carrier
  47      ≃ ArithmeticFromLogic.LogicNat :=
  48  (StrictLogicRealization.toLightweight strictOrderedRealization).orbitEquivLogicNat

papers checked against this theorem

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