IndisputableMonolith.Foundation.MetaDoesNotForceObject

   1import IndisputableMonolith.Foundation.SelfBootstrapDistinguishability
   2
   3/-!
   4# Meta-Level Distinction Does Not Force Object-Level Distinction
   5
   6This module records the sharp limit of the T-1 self-bootstrap route.
   7The formal language distinguishes propositions, but that meta-level fact
   8does not force every inhabited object carrier to be non-singleton.
   9
  10The counterexample is the unit carrier.
  11-/
  12
  13namespace IndisputableMonolith
  14namespace Foundation
  15namespace MetaDoesNotForceObject
  16
  17/-- The meta-language has at least one non-trivial propositional distinction. -/
  18theorem meta_language_distinguishes : ∃ P Q : Prop, P ≠ Q :=
  19  SelfBootstrap.meta_language_distinguishes_props
  20
  21/-- Meta-language proposition distinguishability does not force object-level
  22distinguishability on every inhabited carrier. The unit carrier is inhabited
  23and has no two distinct points. -/
  24theorem meta_distinction_does_not_force_object_distinction :
  25    ¬ (∀ K : Type, Nonempty K → ∃ x y : K, x ≠ y) := by
  26  intro h
  27  obtain ⟨x, y, hxy⟩ := h PUnit ⟨PUnit.unit⟩
  28  cases x
  29  cases y
  30  exact hxy rfl
  31
  32/-- Certificate packaging the honest scope of the self-bootstrap route. -/
  33structure MetaDoesNotForceObjectCert : Prop where
  34  /-- The formal meta-language distinguishes propositions. -/
  35  meta_distinguishes : ∃ P Q : Prop, P ≠ Q
  36  /-- That meta-level distinction does not imply object-level non-singletonness
  37      for arbitrary inhabited carriers. -/
  38  no_uniform_object_distinction :
  39    ¬ (∀ K : Type, Nonempty K → ∃ x y : K, x ≠ y)
  40
  41/-- The meta/object separation certificate is theorem-backed. -/
  42theorem metaDoesNotForceObjectCert : MetaDoesNotForceObjectCert where
  43  meta_distinguishes := meta_language_distinguishes
  44  no_uniform_object_distinction :=
  45    meta_distinction_does_not_force_object_distinction
  46
  47end MetaDoesNotForceObject
  48end Foundation
  49end IndisputableMonolith
  50