IndisputableMonolith.Foundation.TMinus1ForcedFromDistinction

   1import Mathlib
   2import IndisputableMonolith.Foundation.ObservableFloorWitness
   3import IndisputableMonolith.Foundation.BooleanProjectionFromMark
   4
   5/-!
   6# T−1 Forced from a Distinction
   7
   8This is the non-half-measure version of the T−1 repair.
   9
  10The primitive is not an external admissibility package.  The primitive is a
  11distinction witness:
  12
  13```
  14h : ∃ x y : K, x ≠ y
  15```
  16
  17From that witness we construct, rather than assume:
  18
  19* a marked pair;
  20* the Boolean projection generated by the distinction;
  21* the observable equivalence relation generated by that projection;
  22* the two-class quotient;
  23* uniqueness of Boolean coordinates up to Boolean automorphism;
  24* the legacy raw floor required by the existing `RealityCertificate`.
  25
  26This module therefore preserves the strong thesis at the correct formal level:
  27everything in the T−1 floor interface is forced by the supplied distinction
  28witness.  If there is no object-level distinction, there is no object-level
  29forcing.  But once the distinction is given, the Boolean/observable floor is not
  30an extra measure.
  31-/
  32
  33namespace IndisputableMonolith
  34namespace Foundation
  35namespace TMinus1ForcedFromDistinction
  36
  37open ObservableFloor
  38open BooleanProjectionFromMark
  39
  40/-! ## 1. From raw witness to marked pair -/
  41
  42/-- Extract the marked pair carried by a distinction witness. -/
  43noncomputable def markedPairOfDistinction
  44    {K : Type*} (h : ∃ x y : K, x ≠ y) : MarkedPair K where
  45  base := Classical.choose h
  46  alt := Classical.choose (Classical.choose_spec h)
  47  distinct := Classical.choose_spec (Classical.choose_spec h)
  48
  49/-- The Boolean projection forced by a chosen distinction witness. -/
  50noncomputable def forcedBoolProjection
  51    {K : Type*} (h : ∃ x y : K, x ≠ y) : K → Bool :=
  52  boolProjection (markedPairOfDistinction h)
  53
  54@[simp] theorem forcedBoolProjection_base
  55    {K : Type*} (h : ∃ x y : K, x ≠ y) :
  56    forcedBoolProjection h (markedPairOfDistinction h).base = false :=
  57  (boolProjection_canonical_given_mark (markedPairOfDistinction h)).1
  58
  59@[simp] theorem forcedBoolProjection_alt
  60    {K : Type*} (h : ∃ x y : K, x ≠ y) :
  61    forcedBoolProjection h (markedPairOfDistinction h).alt = true :=
  62  (boolProjection_canonical_given_mark (markedPairOfDistinction h)).2
  63
  64/-! ## 2. The observable relation generated by the distinction -/
  65
  66/-- The observable equivalence relation forced by a distinction: two
  67representatives are equivalent exactly when the forced Boolean projection gives
  68the same value on them. -/
  69noncomputable def forcedObservableSetoid
  70    {K : Type*} (h : ∃ x y : K, x ≠ y) : Setoid K where
  71  r x y := forcedBoolProjection h x = forcedBoolProjection h y
  72  iseqv := by
  73    constructor
  74    · intro x
  75      rfl
  76    · intro x y hxy
  77      exact hxy.symm
  78    · intro x y z hxy hyz
  79      exact hxy.trans hyz
  80
  81/-- The distinction witness gives two representatives not identified by the
  82observable relation it generates. -/
  83theorem forcedObservableFloor
  84    {K : Type*} (h : ∃ x y : K, x ≠ y) :
  85    ObservableFloorWitness K (forcedObservableSetoid h).r := by
  86  refine ⟨(markedPairOfDistinction h).base, (markedPairOfDistinction h).alt, ?_⟩
  87  intro hrel
  88  simp [forcedObservableSetoid] at hrel
  89
  90/-- The forced observable quotient is nontrivial. -/
  91theorem forcedQuotientNontrivial
  92    {K : Type*} (h : ∃ x y : K, x ≠ y) :
  93    ∃ a b : Quotient (forcedObservableSetoid h), a ≠ b :=
  94  (ObservableFloor.quotient_nontrivial_iff_observableFloor
  95    (forcedObservableSetoid h)).mpr (forcedObservableFloor h)
  96
  97/-! ## 3. The forced quotient is Boolean -/
  98
  99/-- The quotient-to-Bool map induced by the forced projection. -/
 100noncomputable def forcedQuotientToBool
 101    {K : Type*} (h : ∃ x y : K, x ≠ y) :
 102    Quotient (forcedObservableSetoid h) → Bool :=
 103  Quotient.lift (forcedBoolProjection h) (by
 104    intro x y hxy
 105    exact hxy)
 106
 107/-- A Boolean representative for a Boolean value in the forced quotient. -/
 108noncomputable def forcedBoolRepresentative
 109    {K : Type*} (h : ∃ x y : K, x ≠ y) :
 110    Bool → Quotient (forcedObservableSetoid h)
 111  | false => Quotient.mk (forcedObservableSetoid h) (markedPairOfDistinction h).base
 112  | true => Quotient.mk (forcedObservableSetoid h) (markedPairOfDistinction h).alt
 113
 114/-- The forced quotient map sends the distinguished representatives to their
 115Boolean names. -/
 116@[simp] theorem forcedQuotientToBool_representative
 117    {K : Type*} (h : ∃ x y : K, x ≠ y) (b : Bool) :
 118    forcedQuotientToBool h (forcedBoolRepresentative h b) = b := by
 119  cases b <;> simp [forcedQuotientToBool, forcedBoolRepresentative]
 120
 121/-- Every quotient class is equal to the representative of its Boolean value. -/
 122theorem forcedBoolRepresentative_left_inv
 123    {K : Type*} (h : ∃ x y : K, x ≠ y)
 124    (q : Quotient (forcedObservableSetoid h)) :
 125    forcedBoolRepresentative h (forcedQuotientToBool h q) = q := by
 126  refine Quotient.inductionOn q ?_
 127  intro z
 128  by_cases hz : forcedBoolProjection h z = false
 129  · simp [forcedQuotientToBool, forcedBoolRepresentative, hz]
 130    exact Quotient.sound (by
 131      change forcedBoolProjection h (markedPairOfDistinction h).base =
 132        forcedBoolProjection h z
 133      simp [hz])
 134  · have hztrue : forcedBoolProjection h z = true := by
 135      cases hp : forcedBoolProjection h z
 136      · exact False.elim (hz hp)
 137      · rfl
 138    simp [forcedQuotientToBool, forcedBoolRepresentative, hztrue]
 139    exact Quotient.sound (by
 140      change forcedBoolProjection h (markedPairOfDistinction h).alt =
 141        forcedBoolProjection h z
 142      simp [hztrue])
 143
 144/-- The observable quotient generated by a distinction is equivalent to Bool. -/
 145noncomputable def forcedQuotientEquivBool
 146    {K : Type*} (h : ∃ x y : K, x ≠ y) :
 147    Quotient (forcedObservableSetoid h) ≃ Bool where
 148  toFun := forcedQuotientToBool h
 149  invFun := forcedBoolRepresentative h
 150  left_inv := forcedBoolRepresentative_left_inv h
 151  right_inv := forcedQuotientToBool_representative h
 152
 153/-! ## 4. Boolean coordinates are forced up to automorphism -/
 154
 155/-- Boolean coordinates on the forced quotient. -/
 156structure ForcedBooleanCoordinates {K : Type*} (h : ∃ x y : K, x ≠ y) where
 157  coord : Quotient (forcedObservableSetoid h) ≃ Bool
 158
 159/-- The canonical coordinates generated by the distinction witness. -/
 160noncomputable def canonicalForcedBooleanCoordinates
 161    {K : Type*} (h : ∃ x y : K, x ≠ y) :
 162    ForcedBooleanCoordinates h where
 163  coord := forcedQuotientEquivBool h
 164
 165/-- Coordinate change between two Boolean coordinate systems on the quotient
 166generated by the same distinction. -/
 167def forcedBooleanCoordinateChange
 168    {K : Type*} {h : ∃ x y : K, x ≠ y}
 169    (c₁ c₂ : ForcedBooleanCoordinates h) : Bool ≃ Bool :=
 170  c₁.coord.symm.trans c₂.coord
 171
 172/-- Boolean coordinates forced by the same distinction are unique up to Boolean
 173automorphism. -/
 174theorem forcedBooleanCoordinates_unique_up_to_bool_aut
 175    {K : Type*} {h : ∃ x y : K, x ≠ y}
 176    (c₁ c₂ : ForcedBooleanCoordinates h) :
 177    c₂.coord = c₁.coord.trans (forcedBooleanCoordinateChange c₁ c₂) := by
 178  ext q
 179  simp [forcedBooleanCoordinateChange]
 180
 181/-! ## 5. The distinction forces a two-class observable Boolean floor
 182
 183The `/reality` library continues here into the legacy `RealityCertificate`
 184interface (`recognition_certificate_forced_from_distinction` and the
 185`bundling_decomposition` audit), which depend on the full forcing-chain stack.
 186The public core slice keeps only the self-contained floor statements that the
 187ledger-floor T0 bridge consumes. -/
 188
 189/-- The supplied distinction forces the raw floor expected by the legacy
 190certificate interface. -/
 191theorem rawFloor_forced_from_distinction
 192    {K : Type*} (h : ∃ x y : K, x ≠ y) :
 193    ∃ x y : K, x ≠ y :=
 194  h
 195
 196/-- The supplied distinction forces a two-class observable Boolean floor. -/
 197theorem booleanObservableFloor_forced_from_distinction
 198    {K : Type*} (h : ∃ x y : K, x ≠ y) :
 199    Nonempty (Quotient (forcedObservableSetoid h) ≃ Bool) :=
 200  ⟨forcedQuotientEquivBool h⟩
 201
 202/-- The canonical Boolean distinction witness. -/
 203theorem bool_distinction : ∃ x y : Bool, x ≠ y :=
 204  ⟨false, true, Bool.noConfusion⟩
 205
 206end TMinus1ForcedFromDistinction
 207end Foundation
 208end IndisputableMonolith
 209