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  -- The three slots below are *carried* propositions, not proof obligations:
 139  -- `LogicRealization` stores a `Prop` in each (`excludedMiddle`, `composition`,
 140  -- `actionInvariant`) and never forces it to hold. We therefore store the
 141  -- genuine, setting-appropriate statements that DO hold for the two-valued
 142  -- equality cost, and discharge each below (`logicRealizationOfDistinction_*`).
 143  --
 144  -- We deliberately do NOT store a multiplicative composition law: equality cost
 145  -- provably fails (L4) multiplicative composition consistency
 146  -- (`PrimitiveDistinction.equality_cost_insufficient_for_recognition`). That
 147  -- failure is exactly why this realization is minimal and the continuous J/φ
 148  -- layer is reached by realization-invariance, not by pretending an arbitrary
 149  -- `K` is the positive real line. The `composition` slot therefore carries the
 150  -- additive triangle inequality that the equality cost DOES satisfy.
 151  excludedMiddle := ∀ a b : K, a = b ∨ a ≠ b
 152  composition := ∀ a b c : K, eqCost a c ≤ eqCost a b + eqCost b c
 153  actionInvariant := ∀ a b : K, distinctionStep x y a = distinctionStep x y b
 154  nontrivial := by
 155    refine ⟨y, ?_⟩
 156    have hyx : y ≠ x := fun hy => hxy hy.symm
 157    simp [eqCost, hyx]
 158
 159/-! ## The carried law-slots are genuine, not vacuous
 160
 161The three `Prop`-valued slots of the minimal realization (`excludedMiddle`,
 162`composition`, `actionInvariant`) carry statements that actually hold for the
 163two-valued equality cost. We discharge them here so the realization is not
 164"too permissive": it makes named, true claims appropriate to a single
 165distinction, and explicitly declines the one law (multiplicative composition)
 166that equality cost provably cannot satisfy. -/
 167
 168/-- The minimal distinction realization genuinely satisfies the excluded-middle
 169content it carries: every pair on the carrier is same-or-different. -/
 170theorem logicRealizationOfDistinction_excludedMiddle
 171    {K : Type u} [DecidableEq K] (x y : K) (hxy : x ≠ y) :
 172    (logicRealizationOfDistinction K x y hxy).excludedMiddle := by
 173  show ∀ a b : K, a = b ∨ a ≠ b
 174  exact fun a b => eq_or_ne a b
 175
 176/-- The minimal distinction realization satisfies the *additive* composition law
 177(the triangle inequality) of its two-valued equality cost. This is NOT the
 178multiplicative composition consistency (L4), which equality cost provably fails
 179(`PrimitiveDistinction.equality_cost_insufficient_for_recognition`); the slot
 180deliberately carries only the additive law that does hold. -/
 181theorem logicRealizationOfDistinction_composition
 182    {K : Type u} [DecidableEq K] (x y : K) (hxy : x ≠ y) :
 183    (logicRealizationOfDistinction K x y hxy).composition := by
 184  show ∀ a b c : K, eqCost a c ≤ eqCost a b + eqCost b c
 185  intro a b c
 186  by_cases hac : a = c
 187  · have h0 : eqCost a c = 0 := by simp [eqCost, hac]
 188    rw [h0]; exact Nat.zero_le _
 189  · have hac1 : eqCost a c = 1 := eqCost_ne_one hac
 190    have hsplit : a ≠ b ∨ b ≠ c := by
 191      by_contra hcon
 192      push_neg at hcon
 193      exact hac (hcon.1.trans hcon.2)
 194    rw [hac1]
 195    rcases hsplit with hab | hbc
 196    · have h1 : eqCost a b = 1 := eqCost_ne_one hab
 197      have h2 : 0 ≤ eqCost b c := Nat.zero_le _
 198      omega
 199    · have h1 : eqCost b c = 1 := eqCost_ne_one hbc
 200      have h2 : 0 ≤ eqCost a b := Nat.zero_le _
 201      omega
 202
 203/-- The distinction step action is invariant across inputs: it is the constant
 204map onto the marked second point. -/
 205theorem logicRealizationOfDistinction_actionInvariant
 206    {K : Type u} [DecidableEq K] (x y : K) (hxy : x ≠ y) :
 207    (logicRealizationOfDistinction K x y hxy).actionInvariant := by
 208  show ∀ a b : K, distinctionStep x y a = distinctionStep x y b
 209  intro _ _; rfl
 210
 211/-! ## Carrier-level theorem from the bare proposition -/
 212
 213/-- Every inhabited carrier with some distinction admits a native
 214`LogicRealization`. The `DecidableEq K` instance is obtained classically. -/
 215theorem exists_logicRealization_of_distinction
 216    (K : Type u) [Nonempty K] (h : ∃ x y : K, x ≠ y) :
 217    Nonempty (LogicRealization.{u, 0}) := by
 218  classical
 219  rcases h with ⟨x, y, hxy⟩
 220  exact ⟨logicRealizationOfDistinction K x y hxy⟩
 221
 222/-- A more precise version retaining the chosen points. -/
 223theorem exists_named_logicRealization_of_distinction
 224    (K : Type u) [Nonempty K] (h : ∃ x y : K, x ≠ y) :
 225    ∃ x y : K, ∃ hxy : x ≠ y,
 226      Nonempty (LogicRealization.{u, 0}) := by
 227  classical
 228  rcases h with ⟨x, y, hxy⟩
 229  exact ⟨x, y, hxy, ⟨logicRealizationOfDistinction K x y hxy⟩⟩
 230
 231/-! ## Universal Forcing applies to the K-native realization -/
 232
 233/-- The forced arithmetic of the `K`-native realization is canonically
 234`LogicNat`. -/
 235noncomputable def distinction_arithmetic_equiv_logicNat
 236    {K : Type u} [DecidableEq K] (x y : K) (hxy : x ≠ y) :
 237    (UniversalForcing.arithmeticOf
 238      (logicRealizationOfDistinction K x y hxy)).peano.carrier ≃ LogicNat :=
 239  (logicRealizationOfDistinction K x y hxy).orbitEquivLogicNat
 240
 241/-- Any two non-singleton carriers, with chosen distinctions, have
 242canonically equivalent forced arithmetic. -/
 243noncomputable def distinction_realizations_have_same_arithmetic
 244    {K L : Type u} [DecidableEq K] [DecidableEq L]
 245    {x y : K} {a b : L} (hxy : x ≠ y) (hab : a ≠ b) :
 246    (UniversalForcing.arithmeticOf
 247      (logicRealizationOfDistinction K x y hxy)).peano.carrier ≃
 248    (UniversalForcing.arithmeticOf
 249      (logicRealizationOfDistinction L a b hab)).peano.carrier :=
 250  (logicRealizationOfDistinction K x y hxy).orbitEquivLogicNat.trans
 251    (logicRealizationOfDistinction L a b hab).orbitEquivLogicNat.symm
 252
 253/-! ## Certificate -/
 254
 255structure UniversalInstantiationCert (K : Type u) [Nonempty K] : Prop where
 256  instantiate :
 257    (∃ x y : K, x ≠ y) → Nonempty (LogicRealization.{u, 0})
 258  named :
 259    (∃ x y : K, x ≠ y) →
 260      ∃ x y : K, ∃ hxy : x ≠ y,
 261        Nonempty (LogicRealization.{u, 0})
 262
 263theorem universalInstantiationCert
 264    (K : Type u) [Nonempty K] :
 265    UniversalInstantiationCert K where
 266  instantiate := exists_logicRealization_of_distinction K
 267  named := exists_named_logicRealization_of_distinction K
 268
 269end UniversalInstantiationFromDistinction
 270end Foundation
 271end IndisputableMonolith
 272