IndisputableMonolith.Foundation.DistinctionToT4
IndisputableMonolith/Foundation/DistinctionToT4.lean · 460 lines · 22 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Foundation.TMinus1ForcedFromDistinction
3import IndisputableMonolith.Foundation.UnifiedForcingChain
4
5/-!
6# Distinction to T4
7
8This module starts the real closure path from a supplied distinction witness to
9the early forcing spine.
10
11The point is not to return the global `Bool` chain while ignoring the witness.
12Given
13
14```
15h : ∃ x y : K, x ≠ y
16```
17
18`TMinus1ForcedFromDistinction` constructs the forced observable quotient
19
20```
21Quotient (forcedObservableSetoid h)
22```
23
24and proves it equivalent to `Bool`. Here we transport the Boolean
25configuration space and recognition-work cost across that equivalence, yielding
26a T0 recognition-work surface on the quotient generated by the distinction
27itself.
28
29This is Phase 1 of the full T−1→T8 closure. T1-T4 will be routed through this
30transported floor rather than through unthreaded global `Bool` facts.
31-/
32
33namespace IndisputableMonolith
34namespace Foundation
35namespace DistinctionToT4
36
37open CostFromDistinction
38open TMinus1ForcedFromDistinction
39
40universe u
41
42/-! ## The quotient forced by a distinction -/
43
44/-- The observable quotient generated by a distinction witness. -/
45abbrev ForcedQuotient {K : Type*} (h : ∃ x y : K, x ≠ y) :=
46 Quotient (forcedObservableSetoid h)
47
48/-- The forced quotient-to-Bool coordinate equivalence. -/
49noncomputable def forcedQuotientBoolEquiv
50 {K : Type*} (h : ∃ x y : K, x ≠ y) :
51 ForcedQuotient h ≃ Bool :=
52 forcedQuotientEquivBool h
53
54/-! ## Transported configuration space -/
55
56/-- The configuration space on the quotient forced by the distinction. It is
57the Boolean configuration space transported across the forced quotient
58equivalence. -/
59noncomputable instance forcedQuotientConfigSpace
60 {K : Type*} (h : ∃ x y : K, x ≠ y) :
61 ConfigSpace (ForcedQuotient h) where
62 emp := (forcedQuotientBoolEquiv h).symm false
63 join Γ₁ Γ₂ :=
64 (forcedQuotientBoolEquiv h).symm
65 ((forcedQuotientBoolEquiv h Γ₁) || (forcedQuotientBoolEquiv h Γ₂))
66 IsConsistent Γ := forcedQuotientBoolEquiv h Γ = false
67 Independent Γ₁ Γ₂ :=
68 forcedQuotientBoolEquiv h Γ₁ = false ∨ forcedQuotientBoolEquiv h Γ₂ = false
69 emp_consistent := by
70 simp [forcedQuotientBoolEquiv]
71 independent_symm := by
72 intro Γ₁ Γ₂ h_indep
73 exact h_indep.elim (fun h₁ => Or.inr h₁) (fun h₂ => Or.inl h₂)
74 emp_independent := by
75 intro Γ
76 left
77 simp [forcedQuotientBoolEquiv]
78 join_comm := by
79 intro Γ₁ Γ₂
80 apply (forcedQuotientBoolEquiv h).injective
81 cases h₁ : forcedQuotientBoolEquiv h Γ₁ <;>
82 cases h₂ : forcedQuotientBoolEquiv h Γ₂ <;>
83 simp [forcedQuotientBoolEquiv]
84 join_assoc := by
85 intro Γ₁ Γ₂ Γ₃
86 apply (forcedQuotientBoolEquiv h).injective
87 cases h₁ : forcedQuotientBoolEquiv h Γ₁ <;>
88 cases h₂ : forcedQuotientBoolEquiv h Γ₂ <;>
89 cases h₃ : forcedQuotientBoolEquiv h Γ₃ <;>
90 simp [forcedQuotientBoolEquiv]
91 emp_join := by
92 intro Γ
93 apply (forcedQuotientBoolEquiv h).injective
94 cases hΓ : forcedQuotientBoolEquiv h Γ <;>
95 simp [forcedQuotientBoolEquiv]
96 consistent_of_join_indep := by
97 intro Γ₁ Γ₂ _h_indep h₁ h₂
98 change
99 forcedQuotientBoolEquiv h
100 ((forcedQuotientBoolEquiv h).symm
101 (forcedQuotientBoolEquiv h Γ₁ || forcedQuotientBoolEquiv h Γ₂)) = false
102 rw [h₁, h₂]
103 simp [forcedQuotientBoolEquiv]
104 inconsistent_of_join_indep_left := by
105 intro Γ₁ Γ₂ _h_indep h₁ hjoin
106 apply h₁
107 by_cases hΓ₁ : forcedQuotientBoolEquiv h Γ₁ = false
108 · exact hΓ₁
109 · exfalso
110 change
111 forcedQuotientBoolEquiv h
112 ((forcedQuotientBoolEquiv h).symm
113 (forcedQuotientBoolEquiv h Γ₁ || forcedQuotientBoolEquiv h Γ₂)) = false at hjoin
114 have htrue : forcedQuotientBoolEquiv h Γ₁ = true := by
115 cases hp : forcedQuotientBoolEquiv h Γ₁
116 · exact False.elim (hΓ₁ hp)
117 · rfl
118 rw [htrue] at hjoin
119 cases h₂v : forcedQuotientBoolEquiv h Γ₂ <;>
120 simp [h₂v, forcedQuotientBoolEquiv] at hjoin
121
122@[simp] theorem forcedQuotientBoolEquiv_emp
123 {K : Type*} (h : ∃ x y : K, x ≠ y) :
124 forcedQuotientBoolEquiv h (ConfigSpace.emp : ForcedQuotient h) = false :=
125by
126 change forcedQuotientBoolEquiv h ((forcedQuotientBoolEquiv h).symm false) = false
127 simp [forcedQuotientBoolEquiv]
128
129@[simp] theorem forcedQuotientBoolEquiv_join
130 {K : Type*} (h : ∃ x y : K, x ≠ y)
131 (Γ₁ Γ₂ : ForcedQuotient h) :
132 forcedQuotientBoolEquiv h (ConfigSpace.join Γ₁ Γ₂) =
133 (forcedQuotientBoolEquiv h Γ₁ || forcedQuotientBoolEquiv h Γ₂) :=
134by
135 change
136 forcedQuotientBoolEquiv h
137 ((forcedQuotientBoolEquiv h).symm
138 (forcedQuotientBoolEquiv h Γ₁ || forcedQuotientBoolEquiv h Γ₂)) =
139 (forcedQuotientBoolEquiv h Γ₁ || forcedQuotientBoolEquiv h Γ₂)
140 simp [forcedQuotientBoolEquiv]
141
142/-! ## Transported recognition-work cost -/
143
144/-- Recognition-work cost on the quotient generated by the distinction. -/
145noncomputable def forcedQuotientRecognitionCost
146 {K : Type*} (h : ∃ x y : K, x ≠ y) :
147 CostFunction (ForcedQuotient h) where
148 C Γ := UnifiedForcingChain.TMinus1ToT0.boolRecognitionCost.C
149 (forcedQuotientBoolEquiv h Γ)
150 nonneg := by
151 intro Γ
152 exact UnifiedForcingChain.TMinus1ToT0.boolRecognitionCost.nonneg
153 (forcedQuotientBoolEquiv h Γ)
154 dichotomy := by
155 intro Γ
156 change
157 UnifiedForcingChain.TMinus1ToT0.boolRecognitionCost.C
158 (forcedQuotientBoolEquiv h Γ) = 0 ↔
159 forcedQuotientBoolEquiv h Γ = false
160 exact UnifiedForcingChain.TMinus1ToT0.boolRecognitionCost.dichotomy
161 (forcedQuotientBoolEquiv h Γ)
162 additivity := by
163 intro Γ₁ Γ₂ h_indep
164 rw [forcedQuotientBoolEquiv_join]
165 exact UnifiedForcingChain.TMinus1ToT0.boolRecognitionCost.additivity
166 (forcedQuotientBoolEquiv h Γ₁) (forcedQuotientBoolEquiv h Γ₂) h_indep
167
168/-- The transported cost is literally the Boolean recognition cost under the
169forced quotient coordinate. -/
170theorem forcedQuotientRecognitionCost_transport
171 {K : Type*} (h : ∃ x y : K, x ≠ y) (Γ : ForcedQuotient h) :
172 (forcedQuotientRecognitionCost h).C Γ =
173 UnifiedForcingChain.TMinus1ToT0.boolRecognitionCost.C
174 (forcedQuotientBoolEquiv h Γ) :=
175 rfl
176
177/-- The forced quotient carries the recognition-work constraint theorem. -/
178theorem forcedQuotient_recognition_work_constraint
179 {K : Type*} (h : ∃ x y : K, x ≠ y) :
180 Nonempty (CostFunction.RecognitionWorkConstraintCert (ForcedQuotient h)) :=
181 CostFunction.recognition_work_constraint_theorem
182 (forcedQuotientRecognitionCost h)
183
184/-! ## T0 on the distinction-generated quotient -/
185
186/-- T0, but on the quotient generated by the supplied distinction rather than
187the global Boolean floor. -/
188structure T0_FromDistinction
189 {K : Type u} (h : ∃ x y : K, x ≠ y) : Prop where
190 /-- The forced quotient is Boolean. -/
191 quotient_bool : Nonempty (ForcedQuotient h ≃ Bool)
192 /-- The quotient has the transported configuration space. -/
193 recognition_work :
194 Nonempty (CostFunction.RecognitionWorkConstraintCert (ForcedQuotient h))
195 /-- The empty/consistent quotient state has zero cost. -/
196 consistency_cheap :
197 (forcedQuotientRecognitionCost h).C
198 ((forcedQuotientBoolEquiv h).symm false) = 0
199 /-- Every inconsistent quotient state has positive cost. -/
200 contradiction_expensive :
201 ∀ Γ : ForcedQuotient h,
202 ¬ConfigSpace.IsConsistent Γ →
203 0 < (forcedQuotientRecognitionCost h).C Γ
204 /-- Zero cost is exactly consistency on the forced quotient. -/
205 logic_emergent :
206 ∀ Γ : ForcedQuotient h,
207 (forcedQuotientRecognitionCost h).C Γ = 0 ↔
208 ConfigSpace.IsConsistent Γ
209 /-- Recognition work is additive over independent joins on the forced quotient. -/
210 additive_indep :
211 ∀ Γ₁ Γ₂ : ForcedQuotient h,
212 ConfigSpace.Independent Γ₁ Γ₂ →
213 (forcedQuotientRecognitionCost h).C
214 (ConfigSpace.join Γ₁ Γ₂) =
215 (forcedQuotientRecognitionCost h).C Γ₁ +
216 (forcedQuotientRecognitionCost h).C Γ₂
217
218/-- A supplied distinction forces T0 on its own observable quotient. -/
219theorem distinction_forces_T0
220 {K : Type*} (h : ∃ x y : K, x ≠ y) :
221 T0_FromDistinction h where
222 quotient_bool := ⟨forcedQuotientBoolEquiv h⟩
223 recognition_work := forcedQuotient_recognition_work_constraint h
224 consistency_cheap := by
225 rw [forcedQuotientRecognitionCost_transport]
226 simp [forcedQuotientBoolEquiv]
227 rfl
228 contradiction_expensive := by
229 intro Γ hΓ
230 exact (CostFunction.cost_pos_iff_inconsistent
231 (forcedQuotientRecognitionCost h) Γ).mpr hΓ
232 logic_emergent := by
233 intro Γ
234 exact (forcedQuotientRecognitionCost h).dichotomy Γ
235 additive_indep := by
236 intro Γ₁ Γ₂ h_indep
237 exact (forcedQuotientRecognitionCost h).additivity Γ₁ Γ₂ h_indep
238
239/-! ## T1 on the distinction-generated quotient -/
240
241/-- T1, but on the quotient generated by the supplied distinction. -/
242structure T1_FromDistinction
243 {K : Type u} (h : ∃ x y : K, x ≠ y) : Prop where
244 /-- Inconsistent quotient states have positive recognition-work cost. -/
245 inconsistent_positive :
246 ∀ Γ : ForcedQuotient h,
247 ¬ConfigSpace.IsConsistent Γ →
248 0 < (forcedQuotientRecognitionCost h).C Γ
249 /-- Zero-cost quotient states are consistent. -/
250 zero_cost_consistent :
251 ∀ Γ : ForcedQuotient h,
252 (forcedQuotientRecognitionCost h).C Γ = 0 →
253 ConfigSpace.IsConsistent Γ
254 /-- The marked inconsistent quotient state is positive-cost. -/
255 marked_inconsistent_positive :
256 0 < (forcedQuotientRecognitionCost h).C
257 ((forcedQuotientBoolEquiv h).symm true)
258
259/-- T0 on the forced quotient forces T1 on the forced quotient. -/
260theorem distinction_T0_to_T1
261 {K : Type*} {h : ∃ x y : K, x ≠ y}
262 (h0 : T0_FromDistinction h) :
263 T1_FromDistinction h where
264 inconsistent_positive := h0.contradiction_expensive
265 zero_cost_consistent := fun Γ hzero => (h0.logic_emergent Γ).mp hzero
266 marked_inconsistent_positive := by
267 exact h0.contradiction_expensive ((forcedQuotientBoolEquiv h).symm true) (by
268 change forcedQuotientBoolEquiv h ((forcedQuotientBoolEquiv h).symm true) ≠ false
269 simp [forcedQuotientBoolEquiv])
270
271/-- A distinction witness forces T1 on its own observable quotient. -/
272theorem distinction_forces_T1
273 {K : Type*} (h : ∃ x y : K, x ≠ y) :
274 T1_FromDistinction h :=
275 distinction_T0_to_T1 (distinction_forces_T0 h)
276
277/-! ## T2 on the distinction-generated quotient -/
278
279/-- T2, but on the quotient generated by the supplied distinction. -/
280structure T2_FromDistinction
281 {K : Type u} (h : ∃ x y : K, x ≠ y) : Prop where
282 /-- Every quotient state is one of the two forced Boolean-coordinate states. -/
283 state_dichotomy :
284 ∀ Γ : ForcedQuotient h,
285 Γ = (forcedQuotientBoolEquiv h).symm false ∨
286 Γ = (forcedQuotientBoolEquiv h).symm true
287 /-- The two forced quotient states are distinct. -/
288 states_distinct :
289 (forcedQuotientBoolEquiv h).symm false ≠
290 (forcedQuotientBoolEquiv h).symm true
291 /-- Zero cost selects the consistent quotient state. -/
292 zero_cost_selects_consistency :
293 ∀ Γ : ForcedQuotient h,
294 (forcedQuotientRecognitionCost h).C Γ = 0 →
295 Γ = (forcedQuotientBoolEquiv h).symm false
296 /-- Positive cost selects the marked quotient state. -/
297 positive_cost_selects_marked :
298 ∀ Γ : ForcedQuotient h,
299 0 < (forcedQuotientRecognitionCost h).C Γ →
300 Γ = (forcedQuotientBoolEquiv h).symm true
301
302/-- T1 on the forced quotient forces T2 on the forced quotient. -/
303theorem distinction_T1_to_T2
304 {K : Type*} {h : ∃ x y : K, x ≠ y}
305 (h1 : T1_FromDistinction h) :
306 T2_FromDistinction h where
307 state_dichotomy := by
308 intro Γ
309 cases hb : forcedQuotientBoolEquiv h Γ
310 · left
311 apply (forcedQuotientBoolEquiv h).injective
312 simpa [hb, forcedQuotientBoolEquiv]
313 · right
314 apply (forcedQuotientBoolEquiv h).injective
315 simpa [hb, forcedQuotientBoolEquiv]
316 states_distinct := by
317 intro heq
318 have hbool := congrArg (forcedQuotientBoolEquiv h) heq
319 simp [forcedQuotientBoolEquiv] at hbool
320 zero_cost_selects_consistency := by
321 intro Γ hzero
322 have hcons := h1.zero_cost_consistent Γ hzero
323 change forcedQuotientBoolEquiv h Γ = false at hcons
324 apply (forcedQuotientBoolEquiv h).injective
325 simpa [hcons, forcedQuotientBoolEquiv]
326 positive_cost_selects_marked := by
327 intro Γ hpos
328 rcases (show
329 Γ = (forcedQuotientBoolEquiv h).symm false ∨
330 Γ = (forcedQuotientBoolEquiv h).symm true from
331 (by
332 cases hb : forcedQuotientBoolEquiv h Γ
333 · left
334 apply (forcedQuotientBoolEquiv h).injective
335 simpa [hb, forcedQuotientBoolEquiv]
336 · right
337 apply (forcedQuotientBoolEquiv h).injective
338 simpa [hb, forcedQuotientBoolEquiv])) with hfalse | htrue
339 · exfalso
340 rw [hfalse] at hpos
341 have hzero :
342 (forcedQuotientRecognitionCost h).C
343 ((forcedQuotientBoolEquiv h).symm false) = 0 := by
344 rw [forcedQuotientRecognitionCost_transport]
345 simp [forcedQuotientBoolEquiv]
346 rfl
347 rw [hzero] at hpos
348 linarith
349 · exact htrue
350
351/-- A distinction witness forces T2 on its own observable quotient. -/
352theorem distinction_forces_T2
353 {K : Type*} (h : ∃ x y : K, x ≠ y) :
354 T2_FromDistinction h :=
355 distinction_T1_to_T2 (distinction_forces_T1 h)
356
357/-! ## T3 on the distinction-generated quotient -/
358
359/-- T3, but on the quotient generated by the supplied distinction. -/
360structure T3_FromDistinction
361 {K : Type u} (h : ∃ x y : K, x ≠ y) : Prop where
362 /-- The empty consistent quotient entry is zero-cost. -/
363 empty_balanced :
364 (forcedQuotientRecognitionCost h).C
365 (ConfigSpace.emp : ForcedQuotient h) = 0
366 /-- Empty join is neutral on quotient states. -/
367 empty_join_left :
368 ∀ Γ : ForcedQuotient h,
369 ConfigSpace.join (ConfigSpace.emp : ForcedQuotient h) Γ = Γ
370 /-- Empty join is cost-neutral. -/
371 empty_join_cost_neutral :
372 ∀ Γ : ForcedQuotient h,
373 (forcedQuotientRecognitionCost h).C
374 (ConfigSpace.join (ConfigSpace.emp : ForcedQuotient h) Γ) =
375 (forcedQuotientRecognitionCost h).C Γ
376 /-- Independent joins are ledger-additive. -/
377 independent_join_additive :
378 ∀ Γ₁ Γ₂ : ForcedQuotient h,
379 ConfigSpace.Independent Γ₁ Γ₂ →
380 (forcedQuotientRecognitionCost h).C
381 (ConfigSpace.join Γ₁ Γ₂) =
382 (forcedQuotientRecognitionCost h).C Γ₁ +
383 (forcedQuotientRecognitionCost h).C Γ₂
384
385/-- T0 plus T2 on the forced quotient forces T3 on the forced quotient. -/
386theorem distinction_T0_T2_to_T3
387 {K : Type*} {h : ∃ x y : K, x ≠ y}
388 (h0 : T0_FromDistinction h) (_h2 : T2_FromDistinction h) :
389 T3_FromDistinction h where
390 empty_balanced := h0.consistency_cheap
391 empty_join_left := by
392 intro Γ
393 exact ConfigSpace.emp_join Γ
394 empty_join_cost_neutral := by
395 intro Γ
396 rw [ConfigSpace.emp_join]
397 independent_join_additive := h0.additive_indep
398
399/-- A distinction witness forces T3 on its own observable quotient. -/
400theorem distinction_forces_T3
401 {K : Type*} (h : ∃ x y : K, x ≠ y) :
402 T3_FromDistinction h :=
403 distinction_T0_T2_to_T3 (distinction_forces_T0 h) (distinction_forces_T2 h)
404
405/-! ## T4 on the distinction-generated quotient
406
407The `/reality` library continues here with `T4_FromDistinction`, which packages a
408`Recognition.Recognize` witness and a `Recognition.RecognitionStructure` on the
409forced quotient. Those live in the recognition-operator layer that the public
410core slice does not ship, so the public `DistinctionToT4` stops at T3. The
411ledger-floor T0 bridge below depends only on the T0/T1/T2/T3 surface and the
412transported recognition cost. -/
413
414/-! ## Session bundle: T−1 through T3 -/
415
416/-- Completed early slice of the full closure: the supplied distinction forces
417the T−1 floor and T0-T3 on its own observable quotient. (The `/reality` version
418also carries T4 via the recognition-operator layer; see the note above.) -/
419structure DistinctionToT0_Spine
420 (K : Type) (h : ∃ x y : K, x ≠ y) : Prop where
421 /-- The marked pair forced by the distinction. -/
422 marked_pair : Nonempty (BooleanProjectionFromMark.MarkedPair K)
423 /-- The observable floor generated by the distinction. -/
424 observable_floor :
425 ObservableFloor.ObservableFloorWitness K
426 (TMinus1ForcedFromDistinction.forcedObservableSetoid h).r
427 /-- The forced quotient is Boolean. -/
428 quotient_bool :
429 Nonempty (ForcedQuotient h ≃ Bool)
430 /-- T0 holds on the forced quotient. -/
431 t0 : T0_FromDistinction h
432 /-- T1 holds on the forced quotient. -/
433 t1 : T1_FromDistinction h
434 /-- T2 holds on the forced quotient. -/
435 t2 : T2_FromDistinction h
436 /-- T3 holds on the forced quotient. -/
437 t3 : T3_FromDistinction h
438
439/-- A distinction witness forces the T−1-to-T4 spine. -/
440theorem distinction_forces_T0_spine
441 (K : Type) (h : ∃ x y : K, x ≠ y) :
442 DistinctionToT0_Spine K h where
443 marked_pair := ⟨TMinus1ForcedFromDistinction.markedPairOfDistinction h⟩
444 observable_floor := TMinus1ForcedFromDistinction.forcedObservableFloor h
445 quotient_bool := ⟨forcedQuotientBoolEquiv h⟩
446 t0 := distinction_forces_T0 h
447 t1 := distinction_forces_T1 h
448 t2 := distinction_forces_T2 h
449 t3 := distinction_forces_T3 h
450
451/-- Preferred name for the completed early spine theorem (public core: T0-T3). -/
452theorem distinction_forces_T0_to_T3
453 (K : Type) (h : ∃ x y : K, x ≠ y) :
454 DistinctionToT0_Spine K h :=
455 distinction_forces_T0_spine K h
456
457end DistinctionToT4
458end Foundation
459end IndisputableMonolith
460