IndisputableMonolith.Foundation.UniversalInstantiationFromDistinction

   1import Mathlib
   2import IndisputableMonolith.Foundation.LogicRealization
   3import IndisputableMonolith.Foundation.UniversalForcing
   4
   5/-!
   6# Universal Instantiation from One Distinction
   7
   8This module repairs the core skeptical objection to
   9`RealityFromDistinction`: a bare distinction should not merely be bundled
  10beside an already-existing canonical reality certificate. It should first
  11instantiate the Law-of-Logic realization interface on its own carrier.
  12
  13Given any carrier `K` with two distinguishable points `x ≠ y`, we build a
  14`LogicRealization` whose carrier is exactly `K`. The comparison is the
  15two-valued equality cost, the identity point is `x`, and the step map is
  16the constant map to `y`. The internal orbit is the free `LogicNat` orbit.
  17
  18This construction is intentionally minimal. It does not assert that every
  19carrier has a native smooth real-valued J-cost. It proves the first
  20universal step that is actually true:
  21
  22* every non-singleton carrier instantiates the Law-of-Logic interface;
  23* therefore Universal Forcing applies to that carrier;
  24* therefore the carrier has the same forced arithmetic object as the
  25  canonical recognition realization.
  26
  27The continuous J/spacetime layer is then reached through canonical
  28realization-invariance, not by pretending that an arbitrary `K` is itself
  29the positive real line.
  30-/
  31
  32namespace IndisputableMonolith
  33namespace Foundation
  34namespace UniversalInstantiationFromDistinction
  35
  36open ArithmeticFromLogic
  37open UniversalForcing
  38
  39universe u
  40
  41/-! ## Equality cost on an arbitrary carrier -/
  42
  43/-- Two-valued equality cost: zero on equal inputs, one on distinct inputs. -/
  44def eqCost {K : Type u} [DecidableEq K] (a b : K) : Nat :=
  45  if a = b then 0 else 1
  46
  47theorem eqCost_self {K : Type u} [DecidableEq K] (a : K) :
  48    eqCost a a = 0 := by
  49  simp [eqCost]
  50
  51theorem eqCost_symm {K : Type u} [DecidableEq K] (a b : K) :
  52    eqCost a b = eqCost b a := by
  53  unfold eqCost
  54  by_cases h : a = b
  55  · subst h
  56    simp
  57  · have hba : ¬ b = a := fun hb => h hb.symm
  58    simp [h, hba]
  59
  60theorem eqCost_ne_one {K : Type u} [DecidableEq K] {a b : K} (h : a ≠ b) :
  61    eqCost a b = 1 := by
  62  simp [eqCost, h]
  63
  64/-! ## Instantiating `LogicRealization` on K -/
  65
  66/-- The canonical interpretation of a lifted `LogicNat` into a carrier with a
  67named base point `x` and a named distinct point `y`: zero maps to `x`, every
  68successor maps to `y`. The `ULift` lets the orbit live in the same universe as
  69the arbitrary carrier. -/
  70def distinctionInterpret {K : Type u} (x y : K) : ULift.{u} LogicNat → K
  71  | ⟨LogicNat.identity⟩ => x
  72  | ⟨LogicNat.step _⟩ => y
  73
  74/-- The step map induced by a single distinction: every state advances to the
  75distinguished second point. This gives a total endomap on `K`. -/
  76def distinctionStep {K : Type u} (_x y : K) : K → K :=
  77  fun _ => y
  78
  79@[simp] theorem distinctionInterpret_zero {K : Type u} (x y : K) :
  80    distinctionInterpret x y (ULift.up LogicNat.identity) = x := rfl
  81
  82@[simp] theorem distinctionInterpret_step {K : Type u} (x y : K)
  83    (n : ULift.{u} LogicNat) :
  84    distinctionInterpret x y (ULift.up (LogicNat.step n.down)) =
  85      distinctionStep x y (distinctionInterpret x y n) := by
  86  cases n with
  87  | up n =>
  88    cases n <;> rfl
  89
  90/-- **Universal instantiation theorem.**
  91
  92Any carrier with a named distinction `x ≠ y` is a `LogicRealization` on
  93that very carrier. -/
  94noncomputable def logicRealizationOfDistinction
  95    (K : Type u) [DecidableEq K] (x y : K) (hxy : x ≠ y) :
  96    LogicRealization.{u, 0} where
  97  Carrier := K
  98  Cost := Nat
  99  zeroCost := inferInstance
 100  compare := eqCost
 101  zero := x
 102  step := distinctionStep x y
 103  Orbit := ULift.{u} LogicNat
 104  orbitZero := ULift.up LogicNat.zero
 105  orbitStep := fun n => ULift.up (LogicNat.succ n.down)
 106  interpret := distinctionInterpret x y
 107  interpret_zero := rfl
 108  interpret_step := by
 109    intro n
 110    exact distinctionInterpret_step x y n
 111  orbit_no_confusion := by
 112    intro n h
 113    exact LogicNat.zero_ne_succ n.down (congrArg ULift.down h)
 114  orbit_step_injective := by
 115    intro a b h
 116    apply ULift.ext
 117    exact LogicNat.succ_injective (congrArg ULift.down h)
 118  orbit_induction := by
 119    intro P h0 hs n
 120    cases n with
 121    | up n =>
 122      induction n with
 123      | identity => exact h0
 124      | step n ih => exact hs (ULift.up n) ih
 125  orbitEquivLogicNat :=
 126    { toFun := fun n => n.down
 127      invFun := fun n => ULift.up n
 128      left_inv := by intro n; cases n; rfl
 129      right_inv := by intro n; rfl }
 130  orbitEquiv_zero := rfl
 131  orbitEquiv_step := by intro n; rfl
 132  identity := by
 133    intro a
 134    exact eqCost_self a
 135  nonContradiction := by
 136    intro a b
 137    exact eqCost_symm a b
 138  excludedMiddle := True
 139  composition := True
 140  actionInvariant := True
 141  nontrivial := by
 142    refine ⟨y, ?_⟩
 143    have hyx : y ≠ x := fun hy => hxy hy.symm
 144    simp [eqCost, hyx]
 145
 146/-! ## Carrier-level theorem from the bare proposition -/
 147
 148/-- Every inhabited carrier with some distinction admits a native
 149`LogicRealization`. The `DecidableEq K` instance is obtained classically. -/
 150theorem exists_logicRealization_of_distinction
 151    (K : Type u) [Nonempty K] (h : ∃ x y : K, x ≠ y) :
 152    Nonempty (LogicRealization.{u, 0}) := by
 153  classical
 154  rcases h with ⟨x, y, hxy⟩
 155  exact ⟨logicRealizationOfDistinction K x y hxy⟩
 156
 157/-- A more precise version retaining the chosen points. -/
 158theorem exists_named_logicRealization_of_distinction
 159    (K : Type u) [Nonempty K] (h : ∃ x y : K, x ≠ y) :
 160    ∃ x y : K, ∃ hxy : x ≠ y,
 161      Nonempty (LogicRealization.{u, 0}) := by
 162  classical
 163  rcases h with ⟨x, y, hxy⟩
 164  exact ⟨x, y, hxy, ⟨logicRealizationOfDistinction K x y hxy⟩⟩
 165
 166/-! ## Universal Forcing applies to the K-native realization -/
 167
 168/-- The forced arithmetic of the `K`-native realization is canonically
 169`LogicNat`. -/
 170noncomputable def distinction_arithmetic_equiv_logicNat
 171    {K : Type u} [DecidableEq K] (x y : K) (hxy : x ≠ y) :
 172    (UniversalForcing.arithmeticOf
 173      (logicRealizationOfDistinction K x y hxy)).peano.carrier ≃ LogicNat :=
 174  (logicRealizationOfDistinction K x y hxy).orbitEquivLogicNat
 175
 176/-- Any two non-singleton carriers, with chosen distinctions, have
 177canonically equivalent forced arithmetic. -/
 178noncomputable def distinction_realizations_have_same_arithmetic
 179    {K L : Type u} [DecidableEq K] [DecidableEq L]
 180    {x y : K} {a b : L} (hxy : x ≠ y) (hab : a ≠ b) :
 181    (UniversalForcing.arithmeticOf
 182      (logicRealizationOfDistinction K x y hxy)).peano.carrier ≃
 183    (UniversalForcing.arithmeticOf
 184      (logicRealizationOfDistinction L a b hab)).peano.carrier :=
 185  (logicRealizationOfDistinction K x y hxy).orbitEquivLogicNat.trans
 186    (logicRealizationOfDistinction L a b hab).orbitEquivLogicNat.symm
 187
 188/-! ## Certificate -/
 189
 190structure UniversalInstantiationCert (K : Type u) [Nonempty K] : Prop where
 191  instantiate :
 192    (∃ x y : K, x ≠ y) → Nonempty (LogicRealization.{u, 0})
 193  named :
 194    (∃ x y : K, x ≠ y) →
 195      ∃ x y : K, ∃ hxy : x ≠ y,
 196        Nonempty (LogicRealization.{u, 0})
 197
 198theorem universalInstantiationCert
 199    (K : Type u) [Nonempty K] :
 200    UniversalInstantiationCert K where
 201  instantiate := exists_logicRealization_of_distinction K
 202  named := exists_named_logicRealization_of_distinction K
 203
 204end UniversalInstantiationFromDistinction
 205end Foundation
 206end IndisputableMonolith
 207