IndisputableMonolith.Foundation.BooleanProjectionFromMark

   1import Mathlib
   2
   3/-!
   4# Boolean Projection from a Marked Pair
   5
   6The T-1 Boolean floor is canonical only after a distinguishing mark has been
   7chosen. A non-singleton carrier supplies at least one two-point shadow, but a
   8larger carrier does not choose that shadow uniquely.
   9-/
  10
  11namespace IndisputableMonolith
  12namespace Foundation
  13namespace BooleanProjectionFromMark
  14
  15/-- A named two-point mark inside a carrier. -/
  16structure MarkedPair (K : Type*) where
  17  base : K
  18  alt : K
  19  distinct : base ≠ alt
  20
  21/-- The Boolean projection determined by a marked pair: the base point maps to
  22`false`, and every non-base point maps to `true`. -/
  23noncomputable def boolProjection {K : Type*} (m : MarkedPair K) : K → Bool := by
  24  classical
  25  exact fun z => if z = m.base then false else true
  26
  27/-- Given a marked pair, the induced Boolean projection sends the marked base
  28to `false` and the marked alternative to `true`. -/
  29theorem boolProjection_canonical_given_mark {K : Type*} (m : MarkedPair K) :
  30    boolProjection m m.base = false ∧ boolProjection m m.alt = true := by
  31  classical
  32  constructor
  33  · simp [boolProjection]
  34  · have halt_ne_base : m.alt ≠ m.base := fun h => m.distinct h.symm
  35    simp [boolProjection, halt_ne_base]
  36
  37/-- Without a mark, a three-point carrier has multiple inequivalent Boolean
  38shadows. This witnesses that non-singletonness alone does not canonically
  39select a Boolean floor projection. -/
  40theorem bool_projection_not_canonical_without_mark :
  41    ∃ (K : Type) (m1 m2 : MarkedPair K),
  42      boolProjection m1 ≠ boolProjection m2 := by
  43  classical
  44  let m1 : MarkedPair (Fin 3) :=
  45    { base := 0
  46      alt := 1
  47      distinct := by decide }
  48  let m2 : MarkedPair (Fin 3) :=
  49    { base := 1
  50      alt := 0
  51      distinct := by decide }
  52  refine ⟨Fin 3, m1, m2, ?_⟩
  53  intro h
  54  have h0 := congrArg (fun f : Fin 3 → Bool => f 0) h
  55  simp [boolProjection, m1, m2] at h0
  56
  57/-- Certificate packaging the marked-pair Boolean projection facts. -/
  58structure BooleanProjectionFromMarkCert : Prop where
  59  /-- Every marked pair canonically determines a two-valued shadow. -/
  60  marked_pair_projection :
  61    ∀ {K : Type*} (m : MarkedPair K),
  62      boolProjection m m.base = false ∧ boolProjection m m.alt = true
  63  /-- Non-singletonness alone does not choose a unique two-valued shadow. -/
  64  no_canonical_projection_without_mark :
  65    ∃ (K : Type) (m1 m2 : MarkedPair K),
  66      boolProjection m1 ≠ boolProjection m2
  67
  68/-- The Boolean-projection certificate is theorem-backed. -/
  69theorem booleanProjectionFromMarkCert : BooleanProjectionFromMarkCert where
  70  marked_pair_projection := boolProjection_canonical_given_mark
  71  no_canonical_projection_without_mark :=
  72    bool_projection_not_canonical_without_mark
  73
  74end BooleanProjectionFromMark
  75end Foundation
  76end IndisputableMonolith
  77