def
definition
def or abbrev
ofPositiveRatioComparison
show as:
view Lean formalization →
formal statement (Lean)
108noncomputable def ofPositiveRatioComparison
109 (C : ComparisonOperator) (h : SatisfiesLawsOfLogic C) :
110 LogicRealization where
111 Carrier := {x : ℝ // 0 < x}
proof body
Definition body.
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
139 exact h.identity x.1 x.2
140 nonContradiction := by
141 intro x y
142 exact h.non_contradiction x.1 y.1 x.2 y.2
143 excludedMiddle := ExcludedMiddle C
144 composition := RouteIndependence C
145 actionInvariant := ScaleInvariant C
146 nontrivial := by
147 rcases h.non_trivial with ⟨x, hx, hcost⟩
148 exact ⟨⟨x, hx⟩, hcost⟩
149
150/-- The continuous positive-ratio realization satisfies the abstract
151identity-step predicate. -/