IndisputableMonolith.Foundation.NothingToDistinction

   1import IndisputableMonolith.Foundation.AbsoluteFloorClosure
   2
   3/-!
   4# T-2 → T-1 : The Forcing Function From Absolute Nothing To Distinction
   5
   6This module closes the last floor below the Recognition Science forcing chain.
   7The existing absolute floor (`AbsoluteFloorClosure.lean`) took meta-language
   8proposition distinguishability `∃ P Q : Prop, P ≠ Q` and a non-singleton
   9universe as *given* preconditions. Here those preconditions are *derived*, from
  10the strongest possible encoding of absolute nothing, using no axioms.
  11
  12## How absolute nothing is encoded
  13
  14Absolute nothing is the empty type `Empty`: it has no inhabitants and a unique
  15morphism into every type (`Empty.elim`). That is the complete categorical
  16signature of nothing — it is the initial object, the thing with nothing inside
  17and the thing that maps into anything because there is no input to constrain.
  18
  19## The forcing function (the engine)
  20
  21Absolute nothing is not stable, and the instability is forced, not assumed.
  22
  231. To *name* nothing is to write `Empty`. But `Empty` itself has type `Type`.
  24   So the very act of denoting nothing at universe level `n` makes nothing an
  25   *object* at level `n+1`. Nothing reflects upward into something. This is
  26   `naming_nothing_populates_universe : Nonempty Type`.
  27
  282. Once `Type` is inhabited and contains the initial object `Empty`, it also
  29   admits the terminal object `Unit`. These two cannot be the same type:
  30   `Empty` has no inhabitant, `Unit` has one, so any identification transports
  31   the inhabitant of `Unit` into `Empty`, which is impossible. This is
  32   `nothing_ne_something : Nothing ≠ Unit`. That inequality is the first
  33   distinction.
  34
  353. From the first distinction the object-level distinction `∃ x y, x ≠ y`, the
  36   type-level distinction `∃ α β, α ≠ β`, and the propositional distinction
  37   `∃ P Q : Prop, P ≠ Q` all follow as theorems with no premise. The last of
  38   these is exactly the meta-language fact the prior floor assumed; it is now
  39   discharged.
  40
  414. The forced Boolean distinction is the floor consumed by the public T-1
  42   through T8 bridge. This file stays at T-2/T-1 and does not import the
  43   later spine.
  44
  45## Axiom status
  46
  47The core results in this file use **no axioms**. Run
  48`#print axioms nothingToDistinctionCert` to confirm. "From nothing" is meant
  49in the strongest sense available inside a formal system: the distinction is a
  50theorem of bare type formation, resting on no postulate, classical or RS-specific.
  51-/
  52
  53namespace IndisputableMonolith
  54namespace Foundation
  55namespace NothingToDistinction
  56
  57/-! ## T-2: absolute nothing -/
  58
  59/-- Absolute nothing: the type with no inhabitants. The strongest encoding of
  60"there is no object." We keep it as a `def` (not an `abbrev`) so the name does
  61not silently unfold; the unfolding is invoked explicitly where needed. -/
  62def Nothing : Type := Empty
  63
  64/-- Nothing contains nothing. The witness `IsEmpty Nothing` is itself an object:
  65asserting that nothing is empty is already producing a something. -/
  66theorem nothing_has_no_object : IsEmpty Nothing :=
  67  ⟨fun e => Empty.elim e⟩
  68
  69/-- The unique morphism out of nothing into any target. This is the categorical
  70signature of the initial object: nothing maps into everything because there is
  71no inhabitant to constrain the map. -/
  72def nothing_eliminates {C : Sort _} : Nothing → C :=
  73  fun e => Empty.elim e
  74
  75/-! ## The engine: naming nothing populates the universe one level up -/
  76
  77/-- Naming absolute nothing makes nothing an object of `Type`. Nothing at one
  78level is something at the level above. This is the irreversible first step:
  79the universe of types is non-empty the instant nothing is denoted. -/
  80theorem naming_nothing_populates_universe : Nonempty Type :=
  81  ⟨Nothing⟩
  82
  83/-! ## T-1: the first distinction, forced -/
  84
  85/-- The minimal something: the terminal object, with exactly one inhabitant. -/
  86def Something : Type := Unit
  87
  88theorem something_has_object : Nonempty Something :=
  89  ⟨()⟩
  90
  91/-- The first distinction. Nothing and something are necessarily different
  92types: identifying them would carry the inhabitant of `Unit` into `Empty`. No
  93premise is used. -/
  94theorem nothing_ne_something : Nothing ≠ Something := by
  95  intro h
  96  have hn : Nonempty Nothing := by
  97    rw [h]; exact ⟨()⟩
  98  obtain ⟨e⟩ := hn
  99  exact Empty.elim e
 100
 101/-- Type-level distinction, derived from the encoding of absolute nothing. -/
 102theorem type_distinction_forced : ∃ (α β : Type), α ≠ β :=
 103  ⟨Nothing, Something, nothing_ne_something⟩
 104
 105/-- Propositional distinction, derived. This is exactly the meta-language fact
 106`AbsoluteFloorClosure.AbsoluteFloorWitness` previously took as a precondition:
 107`True` (the proposition that holds) and `False` (the proposition that does not)
 108cannot be equal, since equality would carry the proof of `True` into `False`. -/
 109theorem prop_distinction_forced : ∃ P Q : Prop, P ≠ Q :=
 110  ⟨True, False, by intro h; exact h ▸ trivial⟩
 111
 112/-- Object-level distinction on a concrete carrier, derived. The two values of
 113`Bool` are the first realized bit. -/
 114theorem object_distinction_forced : ∃ (α : Type) (x y : α), x ≠ y :=
 115  ⟨Bool, true, false, by decide⟩
 116
 117/-- The Bool instance of the forced distinction, in the exact shape the object
 118floor consumes. -/
 119theorem bool_distinction_from_nothing : ∃ x y : Bool, x ≠ y :=
 120  ⟨false, true, by decide⟩
 121
 122/-- The forcing function itself, stated as an arrow: from the fact that nothing
 123is empty, a distinction is produced. -/
 124theorem nothingForcesDistinction (_ : IsEmpty Nothing) :
 125    ∃ (α β : Type), α ≠ β :=
 126  ⟨Nothing, Something, nothing_ne_something⟩
 127
 128/-! ## Closure into the existing floor -/
 129
 130/-- The absolute-floor witness for `Bool`, with its meta-language precondition
 131now *discharged from nothing* rather than assumed. The `meta_distinguishes`
 132field is supplied by `prop_distinction_forced`. -/
 133theorem absolute_floor_from_nothing :
 134    AbsoluteFloorClosure.AbsoluteFloorWitness Bool where
 135  meta_distinguishes := prop_distinction_forced
 136  nontrivial_specifiable :=
 137    (AbsoluteFloorClosure.bool_absolute_floor).nontrivial_specifiable
 138
 139/-! ## Certificate -/
 140
 141/-- Joint certificate: from the encoding of absolute nothing, the universe is
 142populated, type/propositional/object distinctions all hold, and the prior
 143floor's meta-precondition is discharged. -/
 144structure NothingToDistinctionCert : Prop where
 145  universe_populated : Nonempty Type
 146  type_distinction : ∃ α β : Type, α ≠ β
 147  prop_distinction : ∃ P Q : Prop, P ≠ Q
 148  object_distinction : ∃ (α : Type) (x y : α), x ≠ y
 149  bool_distinction : ∃ x y : Bool, x ≠ y
 150  floor_discharged : AbsoluteFloorClosure.AbsoluteFloorWitness Bool
 151
 152/-- The certificate is theorem-backed. -/
 153theorem nothingToDistinctionCert : NothingToDistinctionCert where
 154  universe_populated := naming_nothing_populates_universe
 155  type_distinction := type_distinction_forced
 156  prop_distinction := prop_distinction_forced
 157  object_distinction := object_distinction_forced
 158  bool_distinction := bool_distinction_from_nothing
 159  floor_discharged := absolute_floor_from_nothing
 160
 161end NothingToDistinction
 162end Foundation
 163end IndisputableMonolith
 164