IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaForced

   1/-
   2  PrimitiveRecognitionCalculus/DeltaForced.lean
   3
   4  The demarcation predicate: what it means for a type to be δ-forced, and the
   5  headline split it induces (ℕ, ℤ, ℚ forced; ℝ not).
   6
   7  Thesis (the ontological reading this module formalizes): an object is PHYSICALLY
   8  REAL if and only if it is δ-forced. "δ-forced" is given an exact mathematical
   9  content here: a type is δ-forced when it carries an explicit countable certificate,
  10  i.e. an injection into ℕ. This is the formal residue of "finitely generated from
  11  the act of distinction": distinction produces an enumerated carrier, and an
  12  enumeration is exactly a certificate `X ↪ ℕ`.
  13
  14  This is deliberately a CERTIFICATE notion, not a cardinality slogan. `Nonempty
  15  (X ↪ ℕ)` says a witnessing injection EXISTS; for the forced tower we exhibit the
  16  injection explicitly and choice-free (`Encodable.encode`), so the positive facts
  17  are constructive, not merely classically true. The negative fact `¬ DeltaForced ℝ`
  18  is a statement ABOUT the display-tier continuum and may use the classical
  19  uncountability of ℝ; that is on the non-forced side of the line and does not
  20  contaminate the forced side.
  21
  22  Relation to the companion results:
  23  - Milan's `Distinction, Initiality, and Recognition Quotients` proves the
  24    cardinality wall (a finite presentation is countable, ℝ is not). This module
  25    turns that size fact into a predicate and DEFENDS the ontological reading Milan's
  26    paper explicitly declines to assert, by pinning "forced" to a checkable
  27    certificate and showing the forced realm is closed under the operations
  28    distinction performs (pairing, restriction, branch).
  29  - `PRCCompletenessIndependence` proves completeness is model-theoretically
  30    independent of the cost/field axioms. `Omniscience.lean` measures HOW MUCH a
  31    completeness posit costs in omniscience. This module says WHICH objects survive
  32    the cut.
  33
  34  No project-local axioms. No sorry. Forced-side facts are `Classical.choice`-free.
  35-/
  36
  37import Mathlib
  38import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Omniscience
  39
  40namespace IndisputableMonolith
  41namespace Foundation
  42namespace PrimitiveRecognitionCalculus
  43namespace Forced
  44
  45universe u v
  46
  47/-- A type is **δ-forced** when it carries an explicit countable certificate: an
  48injection into ℕ. This is the formal content of "finitely generated, hence
  49enumerable, from the act of distinction." -/
  50def DeltaForced (X : Type u) : Prop := Nonempty (X ↪ ℕ)
  51
  52/-- The ontological reading: **physically real** is, by thesis, exactly δ-forced. The
  53mathematical content is carried entirely by `DeltaForced`; this name records the
  54claim that the demarcation line below is the physical one. -/
  55def PhysicallyReal (X : Type u) : Prop := DeltaForced X
  56
  57@[simp] theorem physicallyReal_iff_deltaForced (X : Type u) :
  58    PhysicallyReal X ↔ DeltaForced X := Iff.rfl
  59
  60/-! ### The forced tower (constructive, choice-free)
  61
  62Each carrier of the δ tower exhibits an EXPLICIT certificate, built here by hand so
  63that the positive facts are `Classical.choice`-free. We deliberately do not route
  64through `Encodable`/`Nat.pair`: Mathlib's `Nat.unpair_pair` (and hence every
  65`Encodable` injectivity and `Nat.pair_eq_pair`) is proved via `Nat.sqrt` and depends
  66on `Classical.choice`. The certificates below depend only on `propext` and
  67`Quot.sound`, matching the δ tower's own constructive status (ℕδ → ℤδ → ℚδ in
  68`DistinctionNat`/`SignedOrbit`/`RatioOrbit`). -/
  69
  70/-- Explicit certificate ℤ → ℕ: nonnegatives to evens, negatives to odds. -/
  71def intToNat : ℤ → ℕ
  72  | (Int.ofNat k) => 2 * k
  73  | (Int.negSucc k) => 2 * k + 1
  74
  75theorem intToNat_inj : Function.Injective intToNat := by
  76  intro a b h
  77  cases a with
  78  | ofNat ka => cases b with
  79    | ofNat kb => have hk : ka = kb := by have : 2 * ka = 2 * kb := h; omega
  80                  rw [hk]
  81    | negSucc kb => exfalso; have : 2 * ka = 2 * kb + 1 := h; omega
  82  | negSucc ka => cases b with
  83    | ofNat kb => exfalso; have : 2 * ka + 1 = 2 * kb := h; omega
  84    | negSucc kb => have hk : ka = kb := by have : 2 * ka + 1 = 2 * kb + 1 := h; omega
  85                    rw [hk]
  86
  87/-- The Cantor pairing, defined locally so its reduction is under our control (the
  88Mathlib `Nat.pair` is the same function but its injectivity lemmas pull
  89`Classical.choice` through `Nat.sqrt`). -/
  90def dpair (a b : ℕ) : ℕ := if a < b then b * b + a else a * a + a + b
  91
  92/-- Injectivity of `dpair`, proved choice-free directly from the `if`-definition. The
  93two branches tile each square block `[m², (m+1)²)`; the cross cases are arithmetically
  94impossible and the diagonal cases pin both coordinates. -/
  95theorem dpair_inj2 {a b c d : ℕ} (h : dpair a b = dpair c d) : a = c ∧ b = d := by
  96  rcases Nat.lt_or_ge a b with hab | hab <;> rcases Nat.lt_or_ge c d with hcd | hcd
  97  · -- a < b, c < d : diagonal
  98    rw [dpair, if_pos hab, dpair, if_pos hcd] at h
  99    rcases Nat.lt_trichotomy b d with hbd | hbd | hbd
 100    · exfalso
 101      have e : (b + 1) * (b + 1) = b * b + 2 * b + 1 := by ring
 102      have m : (b + 1) * (b + 1) ≤ d * d := Nat.mul_le_mul (by omega) (by omega)
 103      omega
 104    · subst hbd; exact ⟨by omega, rfl⟩
 105    · exfalso
 106      have e : (d + 1) * (d + 1) = d * d + 2 * d + 1 := by ring
 107      have m : (d + 1) * (d + 1) ≤ b * b := Nat.mul_le_mul (by omega) (by omega)
 108      omega
 109  · -- a < b, c ≥ d : cross, impossible
 110    exfalso
 111    rw [dpair, if_pos hab, dpair, if_neg (Nat.not_lt.mpr hcd)] at h
 112    rcases Nat.lt_trichotomy b c with hbc | hbc | hbc
 113    · have e : (b + 1) * (b + 1) = b * b + 2 * b + 1 := by ring
 114      have m : (b + 1) * (b + 1) ≤ c * c := Nat.mul_le_mul (by omega) (by omega)
 115      omega
 116    · subst hbc; omega
 117    · have e : (c + 1) * (c + 1) = c * c + 2 * c + 1 := by ring
 118      have m : (c + 1) * (c + 1) ≤ b * b := Nat.mul_le_mul (by omega) (by omega)
 119      omega
 120  · -- a ≥ b, c < d : cross, impossible
 121    exfalso
 122    rw [dpair, if_neg (Nat.not_lt.mpr hab), dpair, if_pos hcd] at h
 123    rcases Nat.lt_trichotomy a d with had | had | had
 124    · have e : (a + 1) * (a + 1) = a * a + 2 * a + 1 := by ring
 125      have m : (a + 1) * (a + 1) ≤ d * d := Nat.mul_le_mul (by omega) (by omega)
 126      omega
 127    · subst had; omega
 128    · have e : (d + 1) * (d + 1) = d * d + 2 * d + 1 := by ring
 129      have m : (d + 1) * (d + 1) ≤ a * a := Nat.mul_le_mul (by omega) (by omega)
 130      omega
 131  · -- a ≥ b, c ≥ d : diagonal
 132    rw [dpair, if_neg (Nat.not_lt.mpr hab), dpair, if_neg (Nat.not_lt.mpr hcd)] at h
 133    rcases Nat.lt_trichotomy a c with hac | hac | hac
 134    · exfalso
 135      have e : (a + 1) * (a + 1) = a * a + 2 * a + 1 := by ring
 136      have m : (a + 1) * (a + 1) ≤ c * c := Nat.mul_le_mul (by omega) (by omega)
 137      omega
 138    · subst hac; exact ⟨rfl, by omega⟩
 139    · exfalso
 140      have e : (c + 1) * (c + 1) = c * c + 2 * c + 1 := by ring
 141      have m : (c + 1) * (c + 1) ≤ a * a := Nat.mul_le_mul (by omega) (by omega)
 142      omega
 143
 144/-- Structure-eta equality for ℚ (definitional proof irrelevance on the `den_nz` and
 145`reduced` fields), choice-free. -/
 146theorem rat_eq_of {a b : ℚ} (hn : a.num = b.num) (hd : a.den = b.den) : a = b := by
 147  obtain ⟨na, da, dnza, reda⟩ := a
 148  obtain ⟨nb, db, dnzb, redb⟩ := b
 149  simp only at hn hd
 150  subst hn; subst hd; rfl
 151
 152/-- Explicit certificate ℚ → ℕ: pair the (forced) numerator and denominator. -/
 153def ratToNat (q : ℚ) : ℕ := dpair (intToNat q.num) q.den
 154
 155theorem ratToNat_inj : Function.Injective ratToNat := by
 156  intro a b h
 157  have h2 : dpair (intToNat a.num) a.den = dpair (intToNat b.num) b.den := h
 158  obtain ⟨hn, hd⟩ := dpair_inj2 h2
 159  exact rat_eq_of (intToNat_inj hn) hd
 160
 161/-- ℕ is δ-forced: it is its own certificate. -/
 162theorem deltaForced_nat : DeltaForced ℕ := ⟨Function.Embedding.refl ℕ⟩
 163
 164/-- ℤ is δ-forced via the explicit even/odd certificate. Choice-free. -/
 165theorem deltaForced_int : DeltaForced ℤ := ⟨⟨intToNat, intToNat_inj⟩⟩
 166
 167/-- ℚ is δ-forced via the explicit paired certificate. This is the top of the forced
 168tower constructed in the companion algebra paper (ℕδ → ℤδ → ℚδ). Choice-free. -/
 169theorem deltaForced_rat : DeltaForced ℚ := ⟨⟨ratToNat, ratToNat_inj⟩⟩
 170
 171/-! ### The continuum is not forced
 172
 173`ℝ` carries no certificate: a certificate would make ℝ countable, contradicting its
 174classical uncountability. This is the formal "the continuum is display tier, not
 175forced." The proof legitimately uses the classical cardinality of ℝ. -/
 176
 177/-- A δ-forced type is countable (the certificate is an injection into ℕ).
 178Choice-free. -/
 179theorem countable_of_deltaForced {X : Type u} (h : DeltaForced X) : Countable X := by
 180  obtain ⟨e⟩ := h
 181  exact e.injective.countable
 182
 183/-- The continuum is **not** δ-forced. A certificate would force `Countable ℝ`, but
 184ℝ has cardinality `𝔠 > ℵ₀`. -/
 185theorem not_deltaForced_real : ¬ DeltaForced ℝ := by
 186  intro h
 187  have hc : Countable ℝ := countable_of_deltaForced h
 188  have hle : Cardinal.mk ℝ ≤ Cardinal.aleph0 := Cardinal.mk_le_aleph0_iff.mpr hc
 189  rw [Cardinal.mk_real] at hle
 190  exact absurd hle (not_le.mpr Cardinal.aleph0_lt_continuum)
 191
 192/-! ### The demarcation theorem
 193
 194The headline split that carries the paper: the entire δ tower is physically real,
 195and the continuum is not. -/
 196
 197/-- The forced tower is constructively (choice-free) physically real. Isolated from
 198the ℝ statement so the positive content carries no `Classical.choice`: this is the
 199exact formal residue of "the δ tower ℕδ → ℤδ → ℚδ is built, not posited." -/
 200theorem forcedTower :
 201    PhysicallyReal ℕ ∧ PhysicallyReal ℤ ∧ PhysicallyReal ℚ :=
 202  ⟨deltaForced_nat, deltaForced_int, deltaForced_rat⟩
 203
 204/-- **Demarcation.** The δ tower (ℕ, ℤ, ℚ) is physically real; the continuum ℝ is
 205not. The forced-tower conjuncts are choice-free (`forcedTower`); the ℝ conjunct uses
 206the classical uncountability of ℝ, which is a fact about the display-tier object, not
 207about the forced side. -/
 208theorem demarcation :
 209    PhysicallyReal ℕ ∧ PhysicallyReal ℤ ∧ PhysicallyReal ℚ ∧ ¬ PhysicallyReal ℝ :=
 210  ⟨deltaForced_nat, deltaForced_int, deltaForced_rat, not_deltaForced_real⟩
 211
 212/-! ### Closure of the forced realm
 213
 214The forced types are closed under the operations distinction actually performs:
 215forming a pair (product), restricting to a distinguished sub-collection (subtype),
 216and choosing a branch (sum). These use the `Countable` bridge and are classical;
 217they describe the algebra of the forced realm, not the primary demarcation, so they
 218are kept separate from the choice-free core above. -/
 219
 220/-- δ-forced ↔ countable. The forward direction is choice-free; the backward
 221direction extracts a certificate from countability and uses choice. -/
 222theorem deltaForced_iff_countable (X : Type u) : DeltaForced X ↔ Countable X := by
 223  constructor
 224  · exact countable_of_deltaForced
 225  · intro h
 226    obtain ⟨f, hf⟩ := h.exists_injective_nat'
 227    exact ⟨⟨f, hf⟩⟩
 228
 229/-- Pairing two forced collections is forced. -/
 230theorem deltaForced_prod {X : Type u} {Y : Type v}
 231    (hX : DeltaForced X) (hY : DeltaForced Y) : DeltaForced (X × Y) := by
 232  have : Countable X := countable_of_deltaForced hX
 233  have : Countable Y := countable_of_deltaForced hY
 234  exact (deltaForced_iff_countable _).mpr inferInstance
 235
 236/-- Restricting a forced collection to a distinguished sub-collection is forced. -/
 237theorem deltaForced_subtype {X : Type u} (hX : DeltaForced X) (p : X → Prop) :
 238    DeltaForced {x // p x} := by
 239  have : Countable X := countable_of_deltaForced hX
 240  exact (deltaForced_iff_countable _).mpr inferInstance
 241
 242/-- Choosing between two forced branches is forced. -/
 243theorem deltaForced_sum {X : Type u} {Y : Type v}
 244    (hX : DeltaForced X) (hY : DeltaForced Y) : DeltaForced (X ⊕ Y) := by
 245  have : Countable X := countable_of_deltaForced hX
 246  have : Countable Y := countable_of_deltaForced hY
 247  exact (deltaForced_iff_countable _).mpr inferInstance
 248
 249end Forced
 250end PrimitiveRecognitionCalculus
 251end Foundation
 252end IndisputableMonolith
 253