positiveRatio_interpret_injective

formal source

 155  hasIdentityStep_of_nontrivial _
 156
 157/-- The continuous positive-ratio orbit interpretation is injective. -/
 158theorem positiveRatio_interpret_injective
 159    (C : ComparisonOperator) (h : SatisfiesLawsOfLogic C) :
 160    Function.Injective (positiveRatioOrbitInterpret C h) := by
 161  intro a b hab
 162  have hval := congrArg Subtype.val hab
 163  rw [positiveRatioOrbitInterpret_val, positiveRatioOrbitInterpret_val] at hval
 164  exact ArithmeticFromLogic.embed_injective
 165    (ArithmeticFromLogic.generatorOfLawsOfLogic h) hval
 166
 167/-- The continuous positive-ratio realization interprets its forced arithmetic
 168faithfully into the positive real carrier. -/
 169theorem positiveRatio_faithful
 170    (C : ComparisonOperator) (h : SatisfiesLawsOfLogic C) :
 171    FaithfulArithmeticInterpretation (ofPositiveRatioComparison C h) where
 172  injective := by
 173    intro a b hab
 174    exact positiveRatio_interpret_injective C h hab
 175  zero_step_noncollapse := by
 176    intro n hcollapse
 177    exact LogicNat.zero_ne_succ n (positiveRatio_interpret_injective C h hcollapse)
 178
 179end LogicRealization
 180
 181end Foundation
 182end IndisputableMonolith