IndisputableMonolith.Foundation.UniversalForcing.Strict.PositiveRatio

   1import IndisputableMonolith.Foundation.UniversalForcing.StrictRealization
   2
   3/-!
   4  Strict/PositiveRatio.lean
   5
   6  Strict continuous positive-ratio realization, built directly from
   7  `SatisfiesLawsOfLogic` in `LogicAsFunctionalEquation`.
   8-/
   9
  10namespace IndisputableMonolith
  11namespace Foundation
  12namespace UniversalForcing
  13namespace Strict
  14namespace PositiveRatio
  15
  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
  50/-- The strict-derived lightweight realization has the same forced arithmetic
  51as the existing positive-ratio lightweight wrapper. -/
  52noncomputable def positiveRatio_strict_equiv_existing
  53    (C : ComparisonOperator) (h : SatisfiesLawsOfLogic C) :
  54    (StrictLogicRealization.arith (strictPositiveRatioRealization C h)).peano.carrier
  55      ≃ (UniversalForcing.arithmeticOf (LogicRealization.ofPositiveRatioComparison C h)).peano.carrier :=
  56  ArithmeticOf.equivOfInitial
  57    (StrictLogicRealization.arith (strictPositiveRatioRealization C h))
  58    (UniversalForcing.arithmeticOf (LogicRealization.ofPositiveRatioComparison C h))
  59
  60end PositiveRatio
  61end Strict
  62end UniversalForcing
  63end Foundation
  64end IndisputableMonolith
  65