strictPositiveRatioRealization

formal source

  16open LogicAsFunctionalEquation
  17
  18/-- Strict positive-ratio realization from the existing Law-of-Logic package. -/
  19noncomputable def strictPositiveRatioRealization
  20    (C : ComparisonOperator) (h : SatisfiesLawsOfLogic C) :
  21    StrictLogicRealization where
  22  Carrier := {x : ℝ // 0 < x}
  23  Cost := ℝ
  24  zeroCost := inferInstance
  25  compare := fun x y => C x.1 y.1
  26  compose := fun x y => ⟨x.1 * y.1, mul_pos x.2 y.2⟩
  27  one := ⟨1, one_pos⟩
  28  generator :=
  29    let γ : ℝ := Classical.choose h.non_trivial
  30    ⟨γ, (Classical.choose_spec h.non_trivial).1⟩
  31  identity_law := by
  32    intro x
  33    exact h.identity x.1 x.2
  34  non_contradiction_law := by
  35    intro x y
  36    exact h.non_contradiction x.1 y.1 x.2 y.2
  37  excluded_middle_law := ExcludedMiddle C
  38  composition_law := RouteIndependence C
  39  invariance_law := ScaleInvariant C
  40  nontrivial_law := by
  41    exact (Classical.choose_spec h.non_trivial).2
  42
  43/-- Strict positive-ratio forced arithmetic is canonically `LogicNat`. -/
  44noncomputable def positiveRatio_arith_equiv_logicNat
  45    (C : ComparisonOperator) (h : SatisfiesLawsOfLogic C) :
  46    (StrictLogicRealization.arith (strictPositiveRatioRealization C h)).peano.carrier
  47      ≃ ArithmeticFromLogic.LogicNat :=
  48  (StrictLogicRealization.toLightweight (strictPositiveRatioRealization C h)).orbitEquivLogicNat
  49