94noncomputable def logicRealizationOfDistinction 95 (K : Type u) [DecidableEq K] (x y : K) (hxy : x ≠ y) : 96 LogicRealization.{u, 0} where 97 Carrier := K
proof body
Definition body.
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 125 orbitEquivLogicNat := 126 { toFun := fun n => n.down 127 invFun := fun n => ULift.up n 128 left_inv := by intro n; cases n; rfl 129 right_inv := by intro n; rfl } 130 orbitEquiv_zero := rfl 131 orbitEquiv_step := by intro n; rfl 132 identity := by 133 intro a 134 exact eqCost_self a 135 nonContradiction := by 136 intro a b 137 exact eqCost_symm a b 138 excludedMiddle := True 139 composition := True 140 actionInvariant := True 141 nontrivial := by 142 refine ⟨y, ?_⟩ 143 have hyx : y ≠ x := fun hy => hxy hy.symm 144 simp [eqCost, hyx] 145 146/-! ## Carrier-level theorem from the bare proposition -/ 147 148/-- Every inhabited carrier with some distinction admits a native 149`LogicRealization`. The `DecidableEq K` instance is obtained classically. -/
used by (4)
From the project-wide theorem graph. These declarations reference this one in their body.