positiveRatioOrbitInterpret

formal source

  83
  84/-- Fold over `LogicNat` into the positive-ratio carrier for the selected
  85non-trivial generator. -/
  86noncomputable def positiveRatioOrbitInterpret
  87    (C : ComparisonOperator) (h : SatisfiesLawsOfLogic C) :
  88    LogicNat → {x : ℝ // 0 < x}
  89  | LogicNat.identity => ⟨1, one_pos⟩
  90  | LogicNat.step n =>
  91      let γ : ℝ := Classical.choose h.non_trivial
  92      let x := positiveRatioOrbitInterpret C h n
  93      ⟨γ * x.1, mul_pos (Classical.choose_spec h.non_trivial).1 x.2⟩
  94
  95@[simp] theorem positiveRatioOrbitInterpret_val
  96    (C : ComparisonOperator) (h : SatisfiesLawsOfLogic C) (n : LogicNat) :
  97    (positiveRatioOrbitInterpret C h n).1 =
  98      ArithmeticFromLogic.embed (ArithmeticFromLogic.generatorOfLawsOfLogic h) n := by
  99  induction n with
 100  | identity =>
 101      rfl
 102  | step n ih =>
 103      simp [positiveRatioOrbitInterpret, ArithmeticFromLogic.embed, ih,
 104        ArithmeticFromLogic.generatorOfLawsOfLogic]
 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 =>