ofPositiveRatioComparison

formal source

 105
 106/-- Continuous positive-ratio Law-of-Logic realizations embed into the
 107setting-independent interface. -/
 108noncomputable def ofPositiveRatioComparison
 109    (C : ComparisonOperator) (h : SatisfiesLawsOfLogic C) :
 110    LogicRealization where
 111  Carrier := {x : ℝ // 0 < x}
 112  Cost := ℝ
 113  zeroCost := inferInstance
 114  compare := fun x y => C x.1 y.1
 115  zero := ⟨1, one_pos⟩
 116  step := fun x =>
 117    let γ : ℝ := Classical.choose h.non_trivial
 118    ⟨γ * x.1, mul_pos (Classical.choose_spec h.non_trivial).1 x.2⟩
 119  Orbit := LogicNat
 120  orbitZero := LogicNat.zero
 121  orbitStep := LogicNat.succ
 122  interpret := positiveRatioOrbitInterpret C h
 123  interpret_zero := rfl
 124  interpret_step := by
 125    intro n
 126    rfl
 127  orbit_no_confusion := by
 128    intro n hzero
 129    exact LogicNat.zero_ne_succ n hzero
 130  orbit_step_injective := LogicNat.succ_injective
 131  orbit_induction := by
 132    intro P h0 hs n
 133    exact LogicNat.induction (motive := P) h0 hs n
 134  orbitEquivLogicNat := Equiv.refl LogicNat
 135  orbitEquiv_zero := rfl
 136  orbitEquiv_step := by intro n; rfl
 137  identity := by
 138    intro x