IndisputableMonolith.Foundation.TMinus1ToT1Bridge

   1import IndisputableMonolith.Foundation.AbsoluteFloorClosure
   2import IndisputableMonolith.Foundation.CostFromDistinction
   3
   4/-!
   5# T-1 to T1 Bridge
   6
   7This public module isolates the first three levels of the forcing chain:
   8
   9* T-1: the absolute floor of distinguishability.
  10* T0: the minimal recognition-work cost interface.
  11* T1: the cost-form Meta-Principle, inconsistent floor states cannot be
  12  selected at zero cost.
  13
  14The point is deliberately modest. This file does not import the analytic
  15`J`-cost surface. It proves the pre-analytic bridge from the absolute floor
  16to the Boolean recognition-work split.
  17-/
  18
  19namespace IndisputableMonolith
  20namespace Foundation
  21namespace TMinus1ToT1Bridge
  22
  23open CostFromDistinction
  24
  25/-! ## T-1: Absolute floor -/
  26
  27/-- T-1: the chain starts from the already-closed absolute-floor certificate. -/
  28structure TMinus1_AbsoluteFloor : Prop where
  29  closure : AbsoluteFloorClosure.AbsoluteFloorClosureCert
  30
  31/-- T-1 holds. -/
  32theorem tminus1_holds : TMinus1_AbsoluteFloor where
  33  closure := AbsoluteFloorClosure.absoluteFloorClosureCert
  34
  35/-! ## Boolean recognition-work floor -/
  36
  37/- The minimal object-level configuration space supplied by the absolute
  38floor is Boolean: `false` is empty/consistent, `true` is marked
  39inconsistent. Independent joins are the joins in which two independent
  40inconsistencies are not double-counted in the same Boolean cell. -/
  41instance boolConfigSpace : ConfigSpace Bool where
  42  emp := false
  43  join := fun a b => a || b
  44  IsConsistent := fun a => a = false
  45  Independent := fun a b => a = false ∨ b = false
  46  emp_consistent := rfl
  47  independent_symm := by
  48    intro a b h
  49    exact h.elim (fun ha => Or.inr ha) (fun hb => Or.inl hb)
  50  emp_independent := by
  51    intro a
  52    exact Or.inl rfl
  53  join_comm := by
  54    intro a b
  55    cases a <;> cases b <;> rfl
  56  join_assoc := by
  57    intro a b c
  58    cases a <;> cases b <;> cases c <;> rfl
  59  emp_join := by
  60    intro a
  61    cases a <;> rfl
  62  consistent_of_join_indep := by
  63    intro a b _hab ha hb
  64    cases a <;> cases b <;> simp at *
  65  inconsistent_of_join_indep_left := by
  66    intro a b _hab ha hjoin
  67    cases a <;> cases b <;> simp at *
  68
  69/-- The concrete recognition-work cost on the Boolean floor. -/
  70def boolRecognitionCost : CostFunction Bool where
  71  C := fun a => if a = false then 0 else 1
  72  nonneg := by
  73    intro a
  74    cases a <;> norm_num
  75  dichotomy := by
  76    intro a
  77    change (if a = false then 0 else 1) = 0 <-> a = false
  78    cases a <;> norm_num
  79  additivity := by
  80    intro a b hab
  81    cases a <;> cases b
  82    · have hjoin : CostFromDistinction.ConfigSpace.join false false = false := rfl
  83      rw [hjoin]
  84      norm_num
  85    · have hjoin : CostFromDistinction.ConfigSpace.join false true = true := rfl
  86      rw [hjoin]
  87      norm_num
  88    · have hjoin : CostFromDistinction.ConfigSpace.join true false = true := rfl
  89      rw [hjoin]
  90      norm_num
  91    · exfalso
  92      change true = false ∨ true = false at hab
  93      exact hab.elim (fun h => Bool.noConfusion h) (fun h => Bool.noConfusion h)
  94
  95/-- The Boolean floor carries the recognition-work constraint theorem. -/
  96theorem bool_recognition_work_constraint :
  97    Nonempty (CostFunction.RecognitionWorkConstraintCert Bool) :=
  98  CostFunction.recognition_work_constraint_theorem boolRecognitionCost
  99
 100/-! ## T0: Logic from recognition work -/
 101
 102/-- T0: logic is the zero/positive split of recognition work. -/
 103structure T0_Logic_Forced : Prop where
 104  recognition_work : Nonempty (CostFunction.RecognitionWorkConstraintCert Bool)
 105  consistency_zero : boolRecognitionCost.C false = 0
 106  inconsistency_positive :
 107    forall a : Bool, Not (ConfigSpace.IsConsistent a) -> 0 < boolRecognitionCost.C a
 108  zero_cost_consistent :
 109    forall a : Bool, boolRecognitionCost.C a = 0 -> ConfigSpace.IsConsistent a
 110  additive_indep :
 111    forall a b : Bool, ConfigSpace.Independent a b ->
 112      boolRecognitionCost.C (ConfigSpace.join a b) =
 113        boolRecognitionCost.C a + boolRecognitionCost.C b
 114
 115/-- T0 holds on the pre-analytic Boolean recognition-work floor. -/
 116theorem t0_holds : T0_Logic_Forced where
 117  recognition_work := bool_recognition_work_constraint
 118  consistency_zero := rfl
 119  inconsistency_positive := by
 120    intro a ha
 121    exact (CostFunction.cost_pos_iff_inconsistent boolRecognitionCost a).mpr ha
 122  zero_cost_consistent := by
 123    intro a hzero
 124    exact (boolRecognitionCost.dichotomy a).mp hzero
 125  additive_indep := boolRecognitionCost.additivity
 126
 127/-! ## Boolean floor interface extracted from T-1 -/
 128
 129/-- The absolute Boolean floor canonically supports the concrete Boolean
 130configuration interface used by the public T0 bridge. -/
 131structure BoolFloorConfigFromWitness
 132    (floor : AbsoluteFloorClosure.AbsoluteFloorWitness Bool) : Prop where
 133  floor_nontrivial : ∃ a b : Bool, a ≠ b
 134  floor_dichotomy : ∀ a : Bool, a = false ∨ a = true
 135  false_true_distinct : (false : Bool) ≠ true
 136  emp_is_false : (ConfigSpace.emp : Bool) = false
 137  join_is_or : ∀ a b : Bool, ConfigSpace.join a b = (a || b)
 138  consistency_iff_false : ∀ a : Bool, ConfigSpace.IsConsistent a ↔ a = false
 139  empty_join_left : ∀ a : Bool, ConfigSpace.join false a = a
 140
 141/-- The Boolean absolute-floor witness supplies the concrete Boolean
 142configuration interface. -/
 143theorem bool_floor_config_from_witness
 144    (floor : AbsoluteFloorClosure.AbsoluteFloorWitness Bool) :
 145    BoolFloorConfigFromWitness floor where
 146  floor_nontrivial :=
 147    AbsoluteFloorClosure.bare_distinguishability_of_absolute_floor floor
 148  floor_dichotomy := by
 149    intro a
 150    cases a
 151    · exact Or.inl rfl
 152    · exact Or.inr rfl
 153  false_true_distinct := by
 154    decide
 155  emp_is_false := rfl
 156  join_is_or := by
 157    intro a b
 158    rfl
 159  consistency_iff_false := by
 160    intro a
 161    rfl
 162  empty_join_left := by
 163    intro a
 164    cases a <;> rfl
 165
 166/-- The Boolean recognition-work cost is unit-normalized on the marked
 167inconsistent state. -/
 168structure BoolRecognitionCostFromFloor
 169    (floor : AbsoluteFloorClosure.AbsoluteFloorWitness Bool) : Prop where
 170  zero_empty : boolRecognitionCost.C false = 0
 171  unit_marked : boolRecognitionCost.C true = 1
 172  inconsistent_unit :
 173    ∀ a : Bool, Not (ConfigSpace.IsConsistent a) -> boolRecognitionCost.C a = 1
 174  positive_iff_inconsistent :
 175    ∀ a : Bool, 0 < boolRecognitionCost.C a ↔ Not (ConfigSpace.IsConsistent a)
 176
 177/-- The Boolean floor supplies the unit-normalized recognition-work cost. -/
 178theorem bool_recognition_cost_from_floor
 179    (floor : AbsoluteFloorClosure.AbsoluteFloorWitness Bool) :
 180    BoolRecognitionCostFromFloor floor where
 181  zero_empty := rfl
 182  unit_marked := rfl
 183  inconsistent_unit := by
 184    intro a ha
 185    cases a
 186    · exfalso
 187      exact ha rfl
 188    · rfl
 189  positive_iff_inconsistent := CostFunction.cost_pos_iff_inconsistent boolRecognitionCost
 190
 191/-! ## T-1 to T0 bridge -/
 192
 193/-- T-1 supplies the Boolean absolute floor and therefore the minimal T0
 194recognition-work interface. -/
 195structure TMinus1_To_T0_Bridge : Prop where
 196  bool_floor : AbsoluteFloorClosure.AbsoluteFloorWitness Bool
 197  floor_config : BoolFloorConfigFromWitness bool_floor
 198  floor_cost : BoolRecognitionCostFromFloor bool_floor
 199  recognition_work : Nonempty (CostFunction.RecognitionWorkConstraintCert Bool)
 200  consistency_zero : boolRecognitionCost.C false = 0
 201  positive_iff_inconsistent :
 202    forall a : Bool, 0 < boolRecognitionCost.C a ↔ Not (ConfigSpace.IsConsistent a)
 203  t0 : T0_Logic_Forced
 204
 205/-- The absolute floor supplies the minimal T0 cost interface. -/
 206theorem tminus1_to_t0_bridge
 207    (floor : TMinus1_AbsoluteFloor) :
 208    TMinus1_To_T0_Bridge where
 209  bool_floor := floor.closure.bool_witness
 210  floor_config := bool_floor_config_from_witness floor.closure.bool_witness
 211  floor_cost := bool_recognition_cost_from_floor floor.closure.bool_witness
 212  recognition_work := bool_recognition_work_constraint
 213  consistency_zero := rfl
 214  positive_iff_inconsistent := CostFunction.cost_pos_iff_inconsistent boolRecognitionCost
 215  t0 := t0_holds
 216
 217/-- The canonical T-1 to T0 bridge. -/
 218theorem tminus1_to_t0_bridge_holds : TMinus1_To_T0_Bridge where
 219  bool_floor := AbsoluteFloorClosure.bool_absolute_floor
 220  floor_config := bool_floor_config_from_witness AbsoluteFloorClosure.bool_absolute_floor
 221  floor_cost := bool_recognition_cost_from_floor AbsoluteFloorClosure.bool_absolute_floor
 222  recognition_work := bool_recognition_work_constraint
 223  consistency_zero := rfl
 224  positive_iff_inconsistent := CostFunction.cost_pos_iff_inconsistent boolRecognitionCost
 225  t0 := t0_holds
 226
 227/-! ## T1: Cost-form Meta-Principle -/
 228
 229/-- T1: an inconsistent recognition-work state cannot be selected at zero cost. -/
 230structure T1_MetaPrinciple_Forced : Prop where
 231  inconsistent_positive :
 232    forall a : Bool, Not (ConfigSpace.IsConsistent a) -> 0 < boolRecognitionCost.C a
 233  zero_cost_consistent :
 234    forall a : Bool, boolRecognitionCost.C a = 0 -> ConfigSpace.IsConsistent a
 235  marked_inconsistent_positive : 0 < boolRecognitionCost.C true
 236
 237/-- T1 follows from T0. This proof uses the T0 hypothesis. -/
 238theorem t1_corollary_of_t0 : T0_Logic_Forced -> T1_MetaPrinciple_Forced :=
 239  fun h0 => {
 240    inconsistent_positive := h0.inconsistency_positive
 241    zero_cost_consistent := h0.zero_cost_consistent
 242    marked_inconsistent_positive := h0.inconsistency_positive true (by
 243      intro htrue
 244      change true = false at htrue
 245      exact Bool.noConfusion htrue)
 246  }
 247
 248/-- T0 supplies the T1 bridge. -/
 249structure T0_To_T1_Bridge (h0 : T0_Logic_Forced) : Prop where
 250  t1 : T1_MetaPrinciple_Forced
 251  t1_eq_corollary : t1 = t1_corollary_of_t0 h0
 252
 253/-- The T0-to-T1 bridge is theorem-backed. -/
 254theorem t0_to_t1_bridge_holds (h0 : T0_Logic_Forced) :
 255    T0_To_T1_Bridge h0 where
 256  t1 := t1_corollary_of_t0 h0
 257  t1_eq_corollary := rfl
 258
 259/-- T1 holds. -/
 260theorem t1_holds : T1_MetaPrinciple_Forced :=
 261  (t0_to_t1_bridge_holds t0_holds).t1
 262
 263/-- Compact public certificate for the first forcing bridge. -/
 264structure TMinus1ToT1Cert : Prop where
 265  tminus1 : TMinus1_AbsoluteFloor
 266  bridge : TMinus1_To_T0_Bridge
 267  t0 : T0_Logic_Forced
 268  t0_to_t1 : T0_To_T1_Bridge t0
 269  t1 : T1_MetaPrinciple_Forced
 270
 271/-- The public T-1 to T1 certificate is theorem-backed. -/
 272theorem tminus1_to_t1_cert : TMinus1ToT1Cert :=
 273  let hm1 := tminus1_holds
 274  let b01 := tminus1_to_t0_bridge hm1
 275  let h0 := b01.t0
 276  let b12 := t0_to_t1_bridge_holds h0
 277  {
 278    tminus1 := hm1
 279    bridge := b01
 280    t0 := h0
 281    t0_to_t1 := b12
 282    t1 := b12.t1
 283  }
 284
 285end TMinus1ToT1Bridge
 286end Foundation
 287end IndisputableMonolith
 288