IndisputableMonolith.Foundation.SelfBootstrapDistinguishability

   1import Mathlib
   2
   3/-!
   4  SelfBootstrapDistinguishability.lean
   5
   6  Route A for the absolute-floor program.
   7
   8  This module records the precise, Lean-checkable part of the
   9  self-bootstrap argument. It does not pretend to derive an object-level
  10  non-singleton carrier from nothing. It proves the meta-level facts used
  11  by the argument: the formal language already distinguishes propositions,
  12  and the proposition asserting object-level distinguishability is distinct
  13  from its own denial.
  14-/
  15
  16namespace IndisputableMonolith
  17namespace Foundation
  18namespace SelfBootstrap
  19
  20/-- The two-element type carries a definitional distinction. -/
  21theorem bool_distinguishable : (false : Bool) ≠ true := by
  22  decide
  23
  24/-- Any carrier supporting a Boolean predicate with both truth values
  25inherits an object-level distinction. -/
  26theorem distinguishability_lifted_from_bool
  27    {K : Type*} (P : K → Bool)
  28    (hpos : ∃ x : K, P x = true) (hneg : ∃ x : K, P x = false) :
  29    ∃ x y : K, x ≠ y := by
  30  obtain ⟨x, hx⟩ := hpos
  31  obtain ⟨y, hy⟩ := hneg
  32  refine ⟨x, y, ?_⟩
  33  intro hxy
  34  have hfalse : P x = false := by
  35    simpa [hxy] using hy
  36  cases hx.symm.trans hfalse
  37
  38/-- A proposition is never equal to its negation in classical logic. -/
  39theorem prop_ne_not (P : Prop) : P ≠ ¬ P := by
  40  intro h
  41  by_cases hp : P
  42  · have hnp : ¬ P := by
  43      rw [h] at hp
  44      exact hp
  45    exact hnp hp
  46  · have hp' : P := by
  47      rw [h.symm] at hp
  48      exact hp
  49    exact hp hp'
  50
  51/-- The claim that a carrier admits a non-trivial distinction is itself
  52distinguishable from the denial of that claim. -/
  53theorem dist_claim_self_distinguishes (K : Type*) :
  54    (∃ x y : K, x ≠ y) ≠ (¬ ∃ x y : K, x ≠ y) :=
  55  prop_ne_not (∃ x y : K, x ≠ y)
  56
  57/-- The meta-language has at least one non-trivial propositional distinction. -/
  58theorem meta_language_distinguishes_props : ∃ P Q : Prop, P ≠ Q :=
  59  ⟨True, False, by
  60    intro h
  61    have hf : False := by
  62      simpa [h] using True.intro
  63    exact False.elim hf⟩
  64
  65/-- Route A, honest form: object-level distinguishability is never weaker
  66than the meta-level fact that the formal language already distinguishes
  67`Prop` values. The object-level non-singleton condition is still named. -/
  68theorem distinguishability_forced_given_object_witness
  69    (K : Type*) (_h_meta_dist : ∃ P Q : Prop, P ≠ Q)
  70    (h_at_least_two_in_carrier : ∃ x y : K, x ≠ y) :
  71    ∃ x y : K, x ≠ y :=
  72  h_at_least_two_in_carrier
  73
  74/-- Route A certificate: the self-bootstrap route closes at the meta-language
  75floor, not below it. -/
  76structure SelfBootstrapCert : Prop where
  77  meta_distinguishes : ∃ P Q : Prop, P ≠ Q
  78  claim_not_its_negation : ∀ K : Type*, (∃ x y : K, x ≠ y) ≠ (¬ ∃ x y : K, x ≠ y)
  79
  80/-- The self-bootstrap certificate is theorem-backed. -/
  81theorem selfBootstrapCert : SelfBootstrapCert where
  82  meta_distinguishes := meta_language_distinguishes_props
  83  claim_not_its_negation := dist_claim_self_distinguishes
  84
  85end SelfBootstrap
  86end Foundation
  87end IndisputableMonolith
  88