`logicRealizationOfDistinction`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.UniversalInstantiationFromDistinction
domain: Foundation
line: 94 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.UniversalInstantiationFromDistinction on GitHub at line 94.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  91
  92Any carrier with a named distinction `x ≠ y` is a `LogicRealization` on
  93that very carrier. -/
  94noncomputable def logicRealizationOfDistinction
  95    (K : Type u) [DecidableEq K] (x y : K) (hxy : x ≠ y) :
  96    LogicRealization.{u, 0} where
  97  Carrier := K
  98  Cost := Nat
  99  zeroCost := inferInstance
 100  compare := eqCost
 101  zero := x
 102  step := distinctionStep x y
 103  Orbit := ULift.{u} LogicNat
 104  orbitZero := ULift.up LogicNat.zero
 105  orbitStep := fun n => ULift.up (LogicNat.succ n.down)
 106  interpret := distinctionInterpret x y
 107  interpret_zero := rfl
 108  interpret_step := by
 109    intro n
 110    exact distinctionInterpret_step x y n
 111  orbit_no_confusion := by
 112    intro n h
 113    exact LogicNat.zero_ne_succ n.down (congrArg ULift.down h)
 114  orbit_step_injective := by
 115    intro a b h
 116    apply ULift.ext
 117    exact LogicNat.succ_injective (congrArg ULift.down h)
 118  orbit_induction := by
 119    intro P h0 hs n
 120    cases n with
 121    | up n =>
 122      induction n with
 123      | identity => exact h0
 124      | step n ih => exact hs (ULift.up n) ih

papers checked against this theorem

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