IndisputableMonolith.Foundation.LogicRealization

   1import Mathlib
   2import IndisputableMonolith.Foundation.LogicAsFunctionalEquation
   3import IndisputableMonolith.Foundation.ArithmeticFromLogic
   4
   5/-!
   6  LogicRealization.lean
   7
   8  Setting-independent interface for the Universal Forcing program.
   9
  10  The point of this file is not to finish Universal Forcing in one stroke.
  11  It creates the common object into which different Law-of-Logic settings
  12  (continuous positive ratios, discrete propositions, categorical settings)
  13  can be mapped.
  14-/
  15
  16namespace IndisputableMonolith
  17namespace Foundation
  18
  19open LogicAsFunctionalEquation
  20open ArithmeticFromLogic
  21
  22universe u v
  23
  24/-- A Law-of-Logic realization: a carrier with comparison cost, identity
  25element, step/generator action, and the structural laws needed by the
  26Universal Forcing program.
  27
  28The fields are intentionally lean: each realization supplies its own topology,
  29order, category, or discrete structure through the propositions carried here.
  30The invariant target is not the ambient carrier; it is the arithmetic object
  31extracted from the identity/step data. -/
  32structure LogicRealization where
  33  Carrier : Type u
  34  Cost : Type v
  35  zeroCost : Zero Cost
  36  compare : Carrier → Carrier → Cost
  37  zero : Carrier
  38  step : Carrier → Carrier
  39  Orbit : Type u
  40  orbitZero : Orbit
  41  orbitStep : Orbit → Orbit
  42  interpret : Orbit → Carrier
  43  interpret_zero : interpret orbitZero = zero
  44  interpret_step : ∀ n : Orbit, interpret (orbitStep n) = step (interpret n)
  45  orbit_no_confusion : ∀ n : Orbit, orbitZero ≠ orbitStep n
  46  orbit_step_injective : Function.Injective orbitStep
  47  orbit_induction :
  48    ∀ P : Orbit → Prop,
  49      P orbitZero →
  50      (∀ n, P n → P (orbitStep n)) →
  51      ∀ n, P n
  52  orbitEquivLogicNat : Orbit ≃ LogicNat
  53  orbitEquiv_zero : orbitEquivLogicNat orbitZero = LogicNat.zero
  54  orbitEquiv_step : ∀ n : Orbit,
  55    orbitEquivLogicNat (orbitStep n) = LogicNat.succ (orbitEquivLogicNat n)
  56  identity : ∀ x : Carrier, compare x x = 0
  57  nonContradiction : ∀ x y : Carrier, compare x y = compare y x
  58  excludedMiddle : Prop
  59  composition : Prop
  60  actionInvariant : Prop
  61  nontrivial : ∃ x : Carrier, compare x zero ≠ 0
  62
  63attribute [instance] LogicRealization.zeroCost
  64
  65namespace LogicRealization
  66
  67/-- The identity-step shadow of a realization. This is the data from which
  68`ArithmeticOf` extracts arithmetic. -/
  69def hasIdentityStep (R : LogicRealization) : Prop :=
  70  ∃ x : R.Carrier, R.compare x R.zero ≠ 0
  71
  72theorem hasIdentityStep_of_nontrivial (R : LogicRealization) :
  73    R.hasIdentityStep :=
  74  R.nontrivial
  75
  76/-- A realization whose internal forced arithmetic embeds faithfully into its
  77ambient carrier. Periodic realizations, such as modular carriers, need not
  78satisfy this; their internal orbit is still free while the carrier
  79interpretation is periodic. -/
  80structure FaithfulArithmeticInterpretation (R : LogicRealization) : Prop where
  81  injective : Function.Injective R.interpret
  82  zero_step_noncollapse : ∀ n : R.Orbit, R.interpret R.orbitZero ≠ R.interpret (R.orbitStep n)
  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 =>
 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. -/
 152theorem positiveRatio_hasIdentityStep
 153    (C : ComparisonOperator) (h : SatisfiesLawsOfLogic C) :
 154    (ofPositiveRatioComparison C h).hasIdentityStep :=
 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
 183