IndisputableMonolith.Foundation.DistinguishabilityFromSpecifiability

   1import Mathlib
   2
   3/-!
   4  DistinguishabilityFromSpecifiability.lean
   5
   6  Route B for the absolute-floor program.
   7
   8  The central point is small but sharp: a non-trivial specification is
   9  equivalent to a non-singleton carrier. If a framework can specify an
  10  ontology with something inside and something outside, it already has the
  11  distinction needed by the Law-of-Logic chain.
  12-/
  13
  14namespace IndisputableMonolith
  15namespace Foundation
  16namespace SpecifiabilityClosure
  17
  18/-- A non-trivial specification of a sub-ontology inside a universe of
  19discourse `K`: a predicate that holds for at least one element and fails
  20for at least one element. -/
  21structure NontrivialSpecification (K : Type*) where
  22  inOntology : K → Prop
  23  someInside : ∃ x : K, inOntology x
  24  someOutside : ∃ x : K, ¬ inOntology x
  25
  26/-- Specifiability forces distinguishability. -/
  27theorem distinguishability_from_specification
  28    {K : Type*} (S : NontrivialSpecification K) :
  29    ∃ x y : K, x ≠ y := by
  30  obtain ⟨P, ⟨x, hx⟩, ⟨y, hy⟩⟩ := S
  31  refine ⟨x, y, ?_⟩
  32  intro hxy
  33  have hyx : P y := by
  34    simpa [hxy] using hx
  35  exact hy hyx
  36
  37/-- Any non-empty proper subtype is a non-trivial specification. -/
  38def nontrivial_specification_of_proper_subtype
  39    {K : Type*} (S : Set K)
  40    (hin : ∃ x : K, x ∈ S) (hout : ∃ x : K, x ∉ S) :
  41    NontrivialSpecification K where
  42  inOntology := fun x => x ∈ S
  43  someInside := hin
  44  someOutside := hout
  45
  46/-- If an ontology is a proper, non-empty subset of its universe of discourse,
  47then it defines a non-trivial specification. -/
  48def nontrivial_spec_from_proper_ontology
  49    {K : Type*} (Ω : Set K)
  50    (h_inhabited : ∃ x : K, x ∈ Ω)
  51    (h_proper : ∃ x : K, x ∉ Ω) :
  52    NontrivialSpecification K :=
  53  nontrivial_specification_of_proper_subtype Ω h_inhabited h_proper
  54
  55/-- If no non-trivial specification exists on an inhabited carrier, then the
  56carrier has at most one element. -/
  57theorem at_most_one_of_no_nontrivial_specification
  58    {K : Type*} [Nonempty K]
  59    (h_no_nts : ¬ Nonempty (NontrivialSpecification K)) :
  60    ∀ x y : K, x = y := by
  61  intro x y
  62  by_contra hxy
  63  apply h_no_nts
  64  have hy_ne_x : y ≠ x := by
  65    intro hyx
  66    exact hxy hyx.symm
  67  exact ⟨
  68    { inOntology := fun z => z = x
  69      someInside := ⟨x, rfl⟩
  70      someOutside := ⟨y, hy_ne_x⟩ }⟩
  71
  72/-- Non-trivial specifiability is equivalent to object-level
  73distinguishability on an inhabited carrier. -/
  74theorem distinguishability_iff_nontrivial_specifiability
  75    {K : Type*} [Nonempty K] :
  76    (∃ x y : K, x ≠ y) ↔ Nonempty (NontrivialSpecification K) := by
  77  constructor
  78  · rintro ⟨x, y, hxy⟩
  79    have hy_ne_x : y ≠ x := by
  80      intro hyx
  81      exact hxy hyx.symm
  82    exact ⟨
  83      { inOntology := fun z => z = x
  84        someInside := ⟨x, rfl⟩
  85        someOutside := ⟨y, hy_ne_x⟩ }⟩
  86  · rintro ⟨S⟩
  87    exact distinguishability_from_specification S
  88
  89/-- Route B certificate: specifiability is exactly the same floor as a
  90non-singleton universe of discourse. -/
  91structure SpecifiabilityClosureCert (K : Type*) [Nonempty K] : Prop where
  92  equivalence :
  93    (∃ x y : K, x ≠ y) ↔ Nonempty (NontrivialSpecification K)
  94
  95/-- The specifiability closure certificate is theorem-backed. -/
  96theorem specifiabilityClosureCert (K : Type*) [Nonempty K] :
  97    SpecifiabilityClosureCert K where
  98  equivalence := distinguishability_iff_nontrivial_specifiability
  99
 100end SpecifiabilityClosure
 101end Foundation
 102end IndisputableMonolith
 103