IndisputableMonolith.Gravity.SevenGaps.Gap2TailFiberShiftBridge
IndisputableMonolith/Gravity/SevenGaps/Gap2TailFiberShiftBridge.lean · 525 lines · 47 declarations
show as:
view math explainer →
1import IndisputableMonolith.Gravity.SevenGaps.Gap2EnrichedCarrierPhase
2
3/-!
4# Wave C1 R4: conditional `TailFiberShift` bridge + candidate no-gos
5
6Codex-adjudicated bankable piece of the enriched-carrier phase route
7(decision / design behind
8`plans/QG_WaveC1_Gap2_Residual_DAG_Draft_20260722.txt` residual R4,
9carrier in `Gap2EnrichedCarrierPhase`).
10
11## What this module banks (CONDITIONAL)
12
13* `TailFiberShift tau`: a tail family of `classMu`-preserving shell
14 automorphisms that rotate the Fin-8 tick by `+1`. This is a
15 **structure hypothesis**, not an inhabited witness. Existence of such
16 a free action is future research.
17* `eventuallyTickFiberMassBalanced_of_tailFiberShift`: the hyp forces
18 eventual tick-fiber mass balance.
19* `oscillatoryTail_of_tailFiberShift` and the labeled-descent form
20 `oscillatoryTail_of_labeled_tailFiberShift`: compose with the banked
21 `eventuallyTickFiberMassBalanced_implies_oscillatoryTail`.
22
23## No-gos (fallback credit)
24
25The obvious candidate operations on labeled exact complexes
26
27* endpoint reversal (`edgeVerts i ↦ Prod.swap`)
28* tetrahedron slot rotation (`tetVerts k ∘ (+1)` on `Fin 4`)
29* their composite
30
31each fix a degenerate labeled complex in every shell (all-loops /
32constant-tet / both). Their induced class maps therefore fix a class in
33every shell, which is incompatible with `tick_shift` (`τ c = τ c + 1`
34is false in `Fin 8`). Signature-level Fin-8 routes remain closed by the
35Burnside stall in `Gap2SignatureBlockerAttack` (mesoscopic cube
36dominance; `SignatureFin8OscillatoryTailBlocker` DEFINED unproved).
37
38## Status
39
40R4 stays OPEN (uninhabited). `gap2_continuum_and_measure` stays false.
41No `sorry`, `admit`, new axiom, or `native_decide`.
42-/
43
44namespace IndisputableMonolith
45namespace Gravity
46namespace SevenGaps
47namespace Gap2TailFiberShiftBridge
48
49open ExactShellGaugeUV
50open ZqContinuumBlocker
51open Gap2TickPhaseSubstrate
52open Gap2TickPhaseTailBlocker
53open Gap2EnrichedCarrierPhase
54
55noncomputable section
56
57/-! ## §1. Conditional structure: TailFiberShift -/
58
59/-- **CONDITIONAL hyp.** From some shell `N` onward, a family of
60exact-path-class automorphisms that rotate the tick by `+1` and preserve
61`classMu`. Not inhabited in this module; free-action search is OPEN. -/
62structure TailFiberShift (tau : ∀ n : ℕ, ExactPathClass n → Fin 8) where
63 N : ℕ
64 shift : ∀ n : ℕ, N ≤ n → ExactPathClass n ≃ ExactPathClass n
65 tick_shift :
66 ∀ n : ℕ, ∀ hn : N ≤ n, ∀ c : ExactPathClass n,
67 tau n (shift n hn c) = tau n c + 1
68 mu_shift :
69 ∀ n : ℕ, ∀ hn : N ≤ n, ∀ c : ExactPathClass n,
70 classMu (shift n hn c) = classMu c
71
72/-! ## §2. Bridge: TailFiberShift ⇒ eventual mass balance -/
73
74private lemma fin8_add_one_ne (p : Fin 8) : p + 1 ≠ p := by
75 intro h
76 have hv := congrArg Fin.val h
77 have hp : p.val < 8 := p.isLt
78 simp only [Fin.val_add] at hv
79 have : (p.val + 1) % 8 ≠ p.val := by omega
80 exact this hv
81
82/-- The shift restricts to a `classMu`-preserving bijection of tick
83fibers `p → p+1`. -/
84theorem tickFiberMass_succ_of_tailFiberShift
85 (tau : ∀ n : ℕ, ExactPathClass n → Fin 8) (h : TailFiberShift tau)
86 {n : ℕ} (hn : h.N ≤ n) (p : Fin 8) :
87 tickFiberMass tau n p = tickFiberMass tau n (p + 1) := by
88 classical
89 let e := h.shift n hn
90 have hmap :
91 (tickFiber tau n p).map e.toEmbedding = tickFiber tau n (p + 1) := by
92 ext d
93 simp only [tickFiber, Finset.mem_map, Finset.mem_filter, Finset.mem_univ,
94 true_and, Equiv.coe_toEmbedding]
95 constructor
96 · rintro ⟨c, hc, rfl⟩
97 rw [h.tick_shift n hn c, hc]
98 · intro hd
99 refine ⟨e.symm d, ?_, e.apply_symm_apply d⟩
100 have htick := h.tick_shift n hn (e.symm d)
101 rw [e.apply_symm_apply] at htick
102 -- htick: tau n d = tau n (e.symm d) + 1
103 -- hd: tau n d = p + 1
104 have : tau n (e.symm d) + 1 = p + 1 := htick.symm.trans hd
105 exact add_right_cancel this
106 unfold tickFiberMass
107 rw [← hmap, Finset.sum_map]
108 refine Finset.sum_congr rfl fun c _ => (h.mu_shift n hn c).symm
109
110/-- Every fiber mass equals the mass of tick `0` (walk by `+1`). -/
111private theorem tickFiberMass_eq_zero_of_tailFiberShift
112 (tau : ∀ n : ℕ, ExactPathClass n → Fin 8) (h : TailFiberShift tau)
113 {n : ℕ} (hn : h.N ≤ n) :
114 ∀ p : Fin 8, tickFiberMass tau n p = tickFiberMass tau n 0 := by
115 intro p
116 have step :
117 ∀ m : ℕ, ∀ hm : m < 8,
118 tickFiberMass tau n ⟨m, hm⟩ = tickFiberMass tau n 0 := by
119 intro m hm
120 induction m with
121 | zero => rfl
122 | succ m ih =>
123 have hm' : m < 8 := Nat.lt_of_succ_lt hm
124 have heq : (⟨m, hm'⟩ : Fin 8) + 1 = ⟨m + 1, hm⟩ := by
125 ext
126 simp only [Fin.val_add]
127 omega
128 have hsucc :=
129 tickFiberMass_succ_of_tailFiberShift tau h hn ⟨m, hm'⟩
130 rw [← heq, ← hsucc, ih hm']
131 exact step p.val p.isLt
132
133/-- **BRIDGE.** A `TailFiberShift` forces eventual equal `classMu` mass
134across all eight tick fibers. -/
135theorem eventuallyTickFiberMassBalanced_of_tailFiberShift
136 (tau : ∀ n : ℕ, ExactPathClass n → Fin 8) (h : TailFiberShift tau) :
137 EventuallyTickFiberMassBalanced tau := by
138 refine ⟨h.N, fun n hn p q => ?_⟩
139 rw [tickFiberMass_eq_zero_of_tailFiberShift tau h hn p,
140 tickFiberMass_eq_zero_of_tailFiberShift tau h hn q]
141
142/-- Abstract composition: conditional shift ⇒ `OscillatoryTail` on the
143tick-derived phase. -/
144theorem oscillatoryTail_of_tailFiberShift
145 (tau : ∀ n : ℕ, ExactPathClass n → Fin 8) (h : TailFiberShift tau) :
146 OscillatoryTail (tickDerivedPhase tau) :=
147 eventuallyTickFiberMassBalanced_implies_oscillatoryTail tau
148 (eventuallyTickFiberMassBalanced_of_tailFiberShift tau h)
149
150/-- Labeled-descent composition for the enriched carrier. -/
151theorem oscillatoryTail_of_labeled_tailFiberShift
152 (lab : LabeledTick) (hInv : GlobalEquivalentInvariant lab)
153 (hshift : TailFiberShift (descendedTick lab hInv)) :
154 OscillatoryTail (enrichedPhase lab hInv) :=
155 oscillatoryTail_of_tailFiberShift (descendedTick lab hInv) hshift
156
157/-! ## §3. Fixed-class blocker (general) -/
158
159/-- A fixed class is incompatible with `+1` tick rotation. -/
160theorem tick_shift_excludes_fixed_point
161 {tau : ∀ n : ℕ, ExactPathClass n → Fin 8} {n : ℕ}
162 {σ : ExactPathClass n ≃ ExactPathClass n}
163 (htick : ∀ c : ExactPathClass n, tau n (σ c) = tau n c + 1)
164 {c : ExactPathClass n} (hfix : σ c = c) : False := by
165 have h := htick c
166 rw [hfix] at h
167 exact (fin8_add_one_ne (tau n c)) h.symm
168
169/-- If a candidate shift family has a fixed class in every tail shell, it
170cannot satisfy the `tick_shift` field of `TailFiberShift`. -/
171theorem fixed_class_blocks_tick_shift
172 (tau : ∀ n : ℕ, ExactPathClass n → Fin 8) (N : ℕ)
173 (shift : ∀ n : ℕ, N ≤ n → ExactPathClass n ≃ ExactPathClass n)
174 (hfix : ∀ n : ℕ, ∀ hn : N ≤ n, ∃ c : ExactPathClass n, shift n hn c = c)
175 (htick :
176 ∀ n : ℕ, ∀ hn : N ≤ n, ∀ c : ExactPathClass n,
177 tau n (shift n hn c) = tau n c + 1) :
178 False := by
179 obtain ⟨c, hc⟩ := hfix N le_rfl
180 exact tick_shift_excludes_fixed_point (htick N le_rfl) hc
181
182/-! ## §4. Candidate operations (labeled) + induced class maps -/
183
184/-- Endpoint reversal: swap the two endpoints of every edge. -/
185def endpointReversal {v e t : ℕ} (K : ExactComplex v e t) :
186 ExactComplex v e t where
187 edgeVerts := fun i => (K.edgeVerts i).swap
188 tetVerts := K.tetVerts
189
190theorem endpointReversal_involutive {v e t : ℕ} (K : ExactComplex v e t) :
191 endpointReversal (endpointReversal K) = K := by
192 cases K
193 simp [endpointReversal]
194
195theorem endpointReversal_ge {v e t : ℕ} {K K' : ExactComplex v e t}
196 (h : GlobalEquivalent K K') :
197 GlobalEquivalent (endpointReversal K) (endpointReversal K') := by
198 obtain ⟨r⟩ := h
199 refine ⟨{
200 vEquiv := r.vEquiv
201 eEquiv := r.eEquiv
202 tEquiv := r.tEquiv
203 edge_comm := fun i => by
204 -- swap both sides of r.edge_comm; Prod.map v v commutes with swap
205 have hcomm :
206 ∀ x : Fin v × Fin v,
207 (Prod.map r.vEquiv r.vEquiv x).swap =
208 Prod.map r.vEquiv r.vEquiv x.swap := fun x => by
209 cases x; rfl
210 simp only [endpointReversal]
211 rw [r.edge_comm i, hcomm]
212 tet_comm := fun i j => by
213 simpa [endpointReversal] using r.tet_comm i j
214 }⟩
215
216/-- Tetrahedron slot rotation: cycle the `Fin 4` argument of `tetVerts`. -/
217def tetSlotRotation {v e t : ℕ} (K : ExactComplex v e t) :
218 ExactComplex v e t where
219 edgeVerts := K.edgeVerts
220 tetVerts := fun k j => K.tetVerts k (j + 1)
221
222theorem tetSlotRotation_ge {v e t : ℕ} {K K' : ExactComplex v e t}
223 (h : GlobalEquivalent K K') :
224 GlobalEquivalent (tetSlotRotation K) (tetSlotRotation K') := by
225 obtain ⟨r⟩ := h
226 refine ⟨{
227 vEquiv := r.vEquiv
228 eEquiv := r.eEquiv
229 tEquiv := r.tEquiv
230 edge_comm := fun i => by
231 simpa [tetSlotRotation] using r.edge_comm i
232 tet_comm := fun i j => by
233 simpa [tetSlotRotation] using r.tet_comm i (j + 1)
234 }⟩
235
236/-- Composite of the two obvious candidates. -/
237def endpointReversalThenTetSlotRotation {v e t : ℕ}
238 (K : ExactComplex v e t) : ExactComplex v e t :=
239 tetSlotRotation (endpointReversal K)
240
241theorem endpointReversalThenTetSlotRotation_ge {v e t : ℕ}
242 {K K' : ExactComplex v e t} (h : GlobalEquivalent K K') :
243 GlobalEquivalent
244 (endpointReversalThenTetSlotRotation K)
245 (endpointReversalThenTetSlotRotation K') :=
246 tetSlotRotation_ge (endpointReversal_ge h)
247
248/-! ### Degenerate labeled fixed points (mission witnesses) -/
249
250/-- All-loop complex of complexity `n` for `n ≥ 1`: signature `(1,n,0)`,
251every edge a self-loop at vertex `0`. -/
252def allLoopsComplex (n : ℕ) (_hn : 1 ≤ n) : ExactComplex 1 n 0 where
253 edgeVerts := fun _ => (0, 0)
254 tetVerts := fun i => i.elim0
255
256theorem endpointReversal_fixes_allLoops (n : ℕ) (hn : 1 ≤ n) :
257 endpointReversal (allLoopsComplex n hn) = allLoopsComplex n hn := by
258 simp [endpointReversal, allLoopsComplex]
259
260/-- Constant tetrahedron of complexity `n` for `n ≥ 1`: signature
261`(1,0,n)`, every tet slot equals vertex `0`. -/
262def constTetComplex (n : ℕ) (_hn : 1 ≤ n) : ExactComplex 1 0 n where
263 edgeVerts := fun i => i.elim0
264 tetVerts := fun _ _ => 0
265
266theorem tetSlotRotation_fixes_constTet (n : ℕ) (hn : 1 ≤ n) :
267 tetSlotRotation (constTetComplex n hn) = constTetComplex n hn := by
268 simp only [tetSlotRotation, constTetComplex]
269
270theorem endpointReversalThenTetSlotRotation_fixes_constTet
271 (n : ℕ) (hn : 1 ≤ n) :
272 endpointReversalThenTetSlotRotation (constTetComplex n hn) =
273 constTetComplex n hn := by
274 -- Const tet: no edges; every slot is 0, so slot rotation is id.
275 -- After unfold, edgeVerts are both `Fin.elim0`-valued on `Fin 0`.
276 simp only [endpointReversalThenTetSlotRotation, endpointReversal,
277 tetSlotRotation, constTetComplex]
278 refine congrArg₂ ExactComplex.mk ?_ rfl
279 funext i; exact i.elim0
280
281theorem endpointReversalThenTetSlotRotation_fixes_allLoops
282 (n : ℕ) (hn : 1 ≤ n) :
283 endpointReversalThenTetSlotRotation (allLoopsComplex n hn) =
284 allLoopsComplex n hn := by
285 simp only [endpointReversalThenTetSlotRotation, endpointReversal,
286 tetSlotRotation, allLoopsComplex]
287 refine congrArg₂ ExactComplex.mk ?_ ?_
288 · funext _i; rfl -- (0,0).swap = (0,0)
289 · funext i; exact i.elim0 -- Fin 0 tetrahedra
290
291/-- Isolated vertices are fixed by both operations (no edges / no tets). -/
292theorem endpointReversal_fixes_isolated (n : ℕ) :
293 endpointReversal (isolatedVertices n) = isolatedVertices n := by
294 simp only [endpointReversal, isolatedVertices]
295 refine congrArg₂ ExactComplex.mk ?_ ?_
296 · funext i; exact i.elim0
297 · funext i; exact i.elim0
298
299theorem tetSlotRotation_fixes_isolated (n : ℕ) :
300 tetSlotRotation (isolatedVertices n) = isolatedVertices n := by
301 simp only [tetSlotRotation, isolatedVertices]
302 refine congrArg₂ ExactComplex.mk rfl ?_
303 funext i; exact i.elim0
304
305theorem endpointReversalThenTetSlotRotation_fixes_isolated (n : ℕ) :
306 endpointReversalThenTetSlotRotation (isolatedVertices n) =
307 isolatedVertices n := by
308 rw [endpointReversalThenTetSlotRotation,
309 endpointReversal_fixes_isolated, tetSlotRotation_fixes_isolated]
310
311/-! ### Induced class-level maps -/
312
313/-- Class map induced by endpoint reversal (signature-preserving). -/
314noncomputable def endpointReversalClass {n : ℕ} :
315 ExactPathClass n → ExactPathClass n :=
316 fun c =>
317 ⟨c.1,
318 Quotient.map endpointReversal
319 (fun _ _ h => endpointReversal_ge h) c.2⟩
320
321theorem endpointReversalClass_mk {n : ℕ} (s : ShellSig n)
322 (K : ExactComplex (sigV s) (sigE s) (sigT s)) :
323 endpointReversalClass ⟨s, Quotient.mk _ K⟩ =
324 ⟨s, Quotient.mk _ (endpointReversal K)⟩ :=
325 rfl
326
327theorem endpointReversalClass_involutive {n : ℕ} (c : ExactPathClass n) :
328 endpointReversalClass (endpointReversalClass c) = c := by
329 cases c with | mk s q =>
330 refine Sigma.ext rfl ?_
331 simp only [heq_eq_eq]
332 refine Quotient.inductionOn q fun K => ?_
333 simp [endpointReversalClass, Quotient.map_mk, endpointReversal_involutive]
334
335noncomputable def endpointReversalClassEquiv (n : ℕ) :
336 ExactPathClass n ≃ ExactPathClass n where
337 toFun := endpointReversalClass
338 invFun := endpointReversalClass
339 left_inv := endpointReversalClass_involutive
340 right_inv := endpointReversalClass_involutive
341
342theorem endpointReversalClass_fixes_isolatedClass (n : ℕ) :
343 endpointReversalClass (isolatedClass n) = isolatedClass n := by
344 simp only [endpointReversalClass, isolatedClass, Quotient.map_mk]
345 exact congrArg (fun K => (⟨isolatedSig n, Quotient.mk _ K⟩ : ExactPathClass n))
346 (endpointReversal_fixes_isolated n)
347
348/-- Class map induced by tet-slot rotation. -/
349noncomputable def tetSlotRotationClass {n : ℕ} :
350 ExactPathClass n → ExactPathClass n :=
351 fun c =>
352 ⟨c.1,
353 Quotient.map tetSlotRotation
354 (fun _ _ h => tetSlotRotation_ge h) c.2⟩
355
356/-- Inverse of one slot rotation: rotate by `−1 = +3` on `Fin 4`. -/
357def tetSlotRotationInv {v e t : ℕ} (K : ExactComplex v e t) :
358 ExactComplex v e t where
359 edgeVerts := K.edgeVerts
360 tetVerts := fun k j => K.tetVerts k (j + 3)
361
362theorem tetSlotRotation_left_inv {v e t : ℕ} (K : ExactComplex v e t) :
363 tetSlotRotationInv (tetSlotRotation K) = K := by
364 cases K with | mk edgeVerts tetVerts =>
365 simp only [tetSlotRotation, tetSlotRotationInv]
366 refine congrArg₂ ExactComplex.mk rfl ?_
367 funext k j
368 apply congrArg (tetVerts k)
369 ext
370 simp only [Fin.val_add]
371 omega
372
373theorem tetSlotRotation_right_inv {v e t : ℕ} (K : ExactComplex v e t) :
374 tetSlotRotation (tetSlotRotationInv K) = K := by
375 cases K with | mk edgeVerts tetVerts =>
376 simp only [tetSlotRotation, tetSlotRotationInv]
377 refine congrArg₂ ExactComplex.mk rfl ?_
378 funext k j
379 apply congrArg (tetVerts k)
380 ext
381 simp only [Fin.val_add]
382 omega
383
384theorem tetSlotRotationInv_ge {v e t : ℕ} {K K' : ExactComplex v e t}
385 (h : GlobalEquivalent K K') :
386 GlobalEquivalent (tetSlotRotationInv K) (tetSlotRotationInv K') := by
387 obtain ⟨r⟩ := h
388 refine ⟨{
389 vEquiv := r.vEquiv
390 eEquiv := r.eEquiv
391 tEquiv := r.tEquiv
392 edge_comm := fun i => by
393 simpa [tetSlotRotationInv] using r.edge_comm i
394 tet_comm := fun i j => by
395 simpa [tetSlotRotationInv] using r.tet_comm i (j + 3)
396 }⟩
397
398noncomputable def tetSlotRotationClassEquiv (n : ℕ) :
399 ExactPathClass n ≃ ExactPathClass n where
400 toFun := tetSlotRotationClass
401 invFun := fun c =>
402 ⟨c.1,
403 Quotient.map tetSlotRotationInv
404 (fun _ _ h => tetSlotRotationInv_ge h) c.2⟩
405 left_inv := by
406 intro c
407 cases c with | mk s q =>
408 refine Sigma.ext rfl ?_
409 simp only [heq_eq_eq]
410 refine Quotient.inductionOn q fun K => ?_
411 simp [tetSlotRotationClass, Quotient.map_mk, tetSlotRotation_left_inv]
412 right_inv := by
413 intro c
414 cases c with | mk s q =>
415 refine Sigma.ext rfl ?_
416 simp only [heq_eq_eq]
417 refine Quotient.inductionOn q fun K => ?_
418 simp [tetSlotRotationClass, Quotient.map_mk, tetSlotRotation_right_inv]
419
420theorem tetSlotRotationClass_fixes_isolatedClass (n : ℕ) :
421 tetSlotRotationClass (isolatedClass n) = isolatedClass n := by
422 simp only [tetSlotRotationClass, isolatedClass, Quotient.map_mk]
423 exact congrArg (fun K => (⟨isolatedSig n, Quotient.mk _ K⟩ : ExactPathClass n))
424 (tetSlotRotation_fixes_isolated n)
425
426/-- Class map induced by the composite operation. -/
427noncomputable def endpointReversalThenTetSlotRotationClass {n : ℕ} :
428 ExactPathClass n → ExactPathClass n :=
429 fun c => tetSlotRotationClass (endpointReversalClass c)
430
431noncomputable def endpointReversalThenTetSlotRotationClassEquiv (n : ℕ) :
432 ExactPathClass n ≃ ExactPathClass n :=
433 (endpointReversalClassEquiv n).trans (tetSlotRotationClassEquiv n)
434
435theorem endpointReversalThenTetSlotRotationClass_eq_equiv {n : ℕ}
436 (c : ExactPathClass n) :
437 endpointReversalThenTetSlotRotationClass c =
438 endpointReversalThenTetSlotRotationClassEquiv n c :=
439 rfl
440
441theorem endpointReversalThenTetSlotRotationClass_fixes_isolatedClass
442 (n : ℕ) :
443 endpointReversalThenTetSlotRotationClass (isolatedClass n) =
444 isolatedClass n := by
445 simp [endpointReversalThenTetSlotRotationClass,
446 endpointReversalClass_fixes_isolatedClass,
447 tetSlotRotationClass_fixes_isolatedClass]
448
449/-! ## §5. No-go theorems for the candidate shift maps -/
450
451/-- **NO-GO.** Endpoint reversal cannot supply a `TailFiberShift`: it
452fixes `isolatedClass n` in every shell, incompatible with `tick_shift`. -/
453theorem endpointReversal_no_tailFiberShift
454 (tau : ∀ n : ℕ, ExactPathClass n → Fin 8) :
455 ¬ ∃ h : TailFiberShift tau,
456 ∀ n : ℕ, ∀ hn : h.N ≤ n, ∀ c : ExactPathClass n,
457 h.shift n hn c = endpointReversalClass c := by
458 rintro ⟨h, hagree⟩
459 refine fixed_class_blocks_tick_shift tau h.N h.shift ?_ h.tick_shift
460 intro n hn
461 refine ⟨isolatedClass n, ?_⟩
462 rw [hagree n hn (isolatedClass n),
463 endpointReversalClass_fixes_isolatedClass]
464
465/-- **NO-GO.** Tetrahedron slot rotation cannot supply a `TailFiberShift`. -/
466theorem tetSlotRotation_no_tailFiberShift
467 (tau : ∀ n : ℕ, ExactPathClass n → Fin 8) :
468 ¬ ∃ h : TailFiberShift tau,
469 ∀ n : ℕ, ∀ hn : h.N ≤ n, ∀ c : ExactPathClass n,
470 h.shift n hn c = tetSlotRotationClass c := by
471 rintro ⟨h, hagree⟩
472 refine fixed_class_blocks_tick_shift tau h.N h.shift ?_ h.tick_shift
473 intro n hn
474 refine ⟨isolatedClass n, ?_⟩
475 rw [hagree n hn (isolatedClass n),
476 tetSlotRotationClass_fixes_isolatedClass]
477
478/-- **NO-GO.** The composite candidate cannot supply a `TailFiberShift`. -/
479theorem endpointReversalThenTetSlotRotation_no_tailFiberShift
480 (tau : ∀ n : ℕ, ExactPathClass n → Fin 8) :
481 ¬ ∃ h : TailFiberShift tau,
482 ∀ n : ℕ, ∀ hn : h.N ≤ n, ∀ c : ExactPathClass n,
483 h.shift n hn c =
484 endpointReversalThenTetSlotRotationClass c := by
485 rintro ⟨h, hagree⟩
486 refine fixed_class_blocks_tick_shift tau h.N h.shift ?_ h.tick_shift
487 intro n hn
488 refine ⟨isolatedClass n, ?_⟩
489 rw [hagree n hn (isolatedClass n),
490 endpointReversalThenTetSlotRotationClass_fixes_isolatedClass]
491
492/-! ## §6. Status (R4 open; gap2 unflipped) -/
493
494structure Gap2TailFiberShiftBridgeStatus where
495 conditionalBridgeLanded : Bool
496 labeledCompositionLanded : Bool
497 candidateNogosLanded : Bool
498 tailFiberShiftInhabited : Bool
499 r4ResidualOpen : Bool
500 gap2ContinuumAndMeasure : Bool
501
502def gap2TailFiberShiftBridgeStatus : Gap2TailFiberShiftBridgeStatus where
503 conditionalBridgeLanded := true
504 labeledCompositionLanded := true
505 candidateNogosLanded := true
506 tailFiberShiftInhabited := false
507 r4ResidualOpen := true
508 gap2ContinuumAndMeasure := false
509
510theorem gap2TailFiberShiftBridgeStatus_flags :
511 gap2TailFiberShiftBridgeStatus.conditionalBridgeLanded = true ∧
512 gap2TailFiberShiftBridgeStatus.labeledCompositionLanded = true ∧
513 gap2TailFiberShiftBridgeStatus.candidateNogosLanded = true ∧
514 gap2TailFiberShiftBridgeStatus.tailFiberShiftInhabited = false ∧
515 gap2TailFiberShiftBridgeStatus.r4ResidualOpen = true ∧
516 gap2TailFiberShiftBridgeStatus.gap2ContinuumAndMeasure = false := by
517 decide
518
519end
520
521end Gap2TailFiberShiftBridge
522end SevenGaps
523end Gravity
524end IndisputableMonolith
525