IndisputableMonolith.Gravity.SevenGaps.Gap6LookalikeReceipt
IndisputableMonolith/Gravity/SevenGaps/Gap6LookalikeReceipt.lean · 314 lines · 28 declarations
show as:
view math explainer →
1import IndisputableMonolith.Gravity.SevenGaps.WickHingeDataComplete
2import IndisputableMonolith.Gravity.SevenGaps.WickFourOneAllHinges
3import IndisputableMonolith.Gravity.SevenGaps.WickThreeTwoHinges
4import IndisputableMonolith.Gravity.SevenGaps.CausalSimplexWick
5import IndisputableMonolith.Gravity.SevenGaps.GluedPentsHingeWitness
6import IndisputableMonolith.Gravity.SevenGaps.ThreePentCausalConsistency
7import IndisputableMonolith.Gravity.SevenGaps.WickActionCertFamilyAssembly
8import IndisputableMonolith.Gravity.SevenGaps.FullTheoryLedger
9import IndisputableMonolith.Gravity.SevenGaps.CampaignLedger
10import IndisputableMonolith.Gravity.Analysis.SRSConvergesEH4D
11
12/-!
13# Wave C4 R0: gap6 lookalike-falsify receipt (updated F3 2026-07-23;
14# honesty patch 2026-07-23)
15
16Falsify-before-proving residual from
17`plans/QG_WaveC4_Gap6_Residual_DAG_Draft_20260722.txt` §R0
18(`TypedResidual_gap6_lookalike_decoys_fail`).
19
20Each banked lookalike below is a positive theorem that a later session
21might rename into the ledger terminal. This module packages per-lookalike
22**separation certificates**: the lookalike holds, and a post-close witness
23that it does **not** discharge / would not have sufficed for
24`wick_action_continuation_4d_v2` (domain mismatch, V1 action-field kill,
25or distinct closer co-assertion).
26
27F3 succession (2026-07-23): gap6 closed via `wick_action_continuation_4d_v2`.
28Lookalike mathematics is retained; obsolete "gap6 stays false" conjuncts
29are replaced by post-close-compatible separation (E-gap6-postclose-critic-20260723
30patch 1). Binding detail:
31`WickActionV2CloseStatus.gap6_lorentzian_action_bound_to_v2`.
32
33No `sorry`, `admit`, new axiom, or `native_decide`.
34-/
35
36namespace IndisputableMonolith
37namespace Gravity
38namespace SevenGaps
39namespace Gap6LookalikeReceipt
40
41open FullTheoryLedger
42open CampaignLedger
43open CausalSimplex4D (CausalPentType causalSimplex4DStatus cm4)
44open CausalSimplexWick (CausalTetType lorentzianSectorStatus)
45open WickHingeDataComplete
46open WickActionComplexFirst
47open WickActionInteriorHinge
48open WickFourOneAllHinges (fourOneCosPath)
49open WickThreeTwoHinges (threeTwoCosPath tStarMixed)
50open GluedPentsHingeWitness
51open ThreePentCausalConsistency
52open Analysis.SRSConvergesEH4D
53
54noncomputable section
55
56/-! ## §1. Dimension mismatch (3D edge-tuple continuation ≠ 4D carrier) -/
57
58/-- 3D CDT tetrahedra use 4 vertices; the 4D carrier uses 5. -/
59theorem simplex3d_vertex_card_ne_4d :
60 Fintype.card (Fin 4) ≠ Fintype.card (Fin 5) := by
61 decide
62
63/-- 3D edge tuples are `Fin 6 → ℝ`; 4D edge tuples are `Fin 10 → ℝ`. -/
64theorem simplex3d_edge_card_ne_4d :
65 Fintype.card (Fin 6) ≠ Fintype.card (Fin 10) := by
66 decide
67
68/-- Re-export: the 3D lookalike theorem is banked (edge-tuple algebra
69`alpha ↦ -alpha` only). -/
70theorem lorentzian_continuation_3d_banked
71 (ty : CausalTetType) (a alpha : ℝ) :
72 CausalSimplexWick.lorentzianSqEdges ty a (-alpha) =
73 CausalSimplexWick.euclideanSqEdges ty a alpha :=
74 CausalSimplexWick.lorentzian_continuation ty a alpha
75
76/-- **S1 certificate.** 3D edge-tuple algebra; carrier dimension / edge
77arity differ from the 4D ledger shape. The 3D sector's action-level Bool
78stays open (3D never received the action closer). -/
79def LorentzianContinuation3DNotAction4DCertificate : Prop :=
80 (∀ ty : CausalTetType, ∀ a alpha : ℝ,
81 CausalSimplexWick.lorentzianSqEdges ty a (-alpha) =
82 CausalSimplexWick.euclideanSqEdges ty a alpha) ∧
83 Fintype.card (Fin 4) ≠ Fintype.card (Fin 5) ∧
84 Fintype.card (Fin 6) ≠ Fintype.card (Fin 10) ∧
85 lorentzianSectorStatus.lorentzian_action_continuation_open = true
86
87theorem lorentzianContinuation3DNotAction4DCertificate :
88 LorentzianContinuation3DNotAction4DCertificate :=
89 ⟨lorentzian_continuation_3d_banked, simplex3d_vertex_card_ne_4d,
90 simplex3d_edge_card_ne_4d, rfl⟩
91
92/-- Re-export: 4D kinematical edge continuation is also banked, and is
93likewise not the action-level closer. -/
94theorem lorentzian_continuation_4d_kinematical_banked
95 (ty : CausalPentType) (a alpha : ℝ) :
96 CausalSimplex4D.lorentzianSqEdges ty a (-alpha) =
97 CausalSimplex4D.euclideanSqEdges ty a alpha :=
98 CausalSimplex4D.lorentzian_continuation ty a alpha
99
100/-- **S1 twin (4D kinematical).** Edge-tuple `alpha ↦ -alpha` on
101`SqEdges10` is kinematical algebra. Post-close separation: the lookalike
102holds for all `α`, including outside CertV2's causal range `7/12 < α`
103(witness `α = 0`); hence it is strictly weaker than /
104would not have sufficed for `wick_action_continuation_4d_v2`. -/
105def LorentzianContinuation4DKinematicalNotActionCertificate : Prop :=
106 (∀ ty : CausalPentType, ∀ a alpha : ℝ,
107 CausalSimplex4D.lorentzianSqEdges ty a (-alpha) =
108 CausalSimplex4D.euclideanSqEdges ty a alpha) ∧
109 ¬ ((7 / 12 : ℝ) < (0 : ℝ))
110
111theorem lorentzianContinuation4DKinematicalNotActionCertificate :
112 LorentzianContinuation4DKinematicalNotActionCertificate :=
113 ⟨lorentzian_continuation_4d_kinematical_banked, by norm_num⟩
114
115/-! ## §2. Hinge-DATA completeness ≠ action-level closer (S2) -/
116
117/-- **S2 certificate.** `wick_hinge_data_continuation_complete` quantifies
118`BranchRegularOn` / cosine paths over single-simplex opposite pairs. It
119does not inhabit a deficit-weighted three-pent action. Post-close
120separation: hinge-data coexists with V1
121`ContinuousOn (wickActionPath 1) (Icc 0 1)` unsatisfiability; hinge-data
122alone would not have sufficed for the action-level target (V2 closed via
123Ioc + cutLimit family assembly). -/
124def HingeDataNotActionLevelCertificate : Prop :=
125 (∀ p q : Fin 5, p ≠ q →
126 (BranchRegularOn
127 (fun t => continuationEdgesC CausalPentType.fourOne 1 1 t) p q
128 (Set.Ioo 0 1)
129 ∧ ContinuousOn (fourOneCosPath p q) (Set.Icc 0 1)
130 ∧ fourOneCosPath p q 1 = -(1 / 4 : ℂ))
131 ∧ (BranchRegularOn
132 (fun t => continuationEdgesC CausalPentType.threeTwo 1 1 t) p q
133 (Set.Ioo 0 1)
134 ∧ ContinuousOn (threeTwoCosPath p q) (Set.Icc 0 1)
135 ∧ threeTwoCosPath p q 1 = -(1 / 4 : ℂ))) ∧
136 ¬ ContinuousOn (wickActionPath 1) (Set.Icc 0 1)
137
138theorem hingeDataNotActionLevelCertificate :
139 HingeDataNotActionLevelCertificate :=
140 ⟨wick_hinge_data_continuation_complete, contAction_not_satisfiable_at_one⟩
141
142/-! ## §3. cm4 sign ≠ Lorentzian realizability (S3 / L-4) -/
143
144/-- **S3 certificate.** Per-pent `cm4 < 0` is a sign fact, not
145action-level Wick continuation. Post-close separation: the sign fact
146holds for all `0 ≤ α`, including outside CertV2's causal range
147(witness `α = 0`); hence it would not have sufficed for
148`wick_action_continuation_4d_v2`. -/
149def Cm4SignNotActionLevelCertificate : Prop :=
150 (∀ a alpha : ℝ, 0 < a → 0 ≤ alpha →
151 cm4 (inducedSqEdges pentAVert a alpha) < 0 ∧
152 cm4 (inducedSqEdges pentBVert a alpha) < 0 ∧
153 cm4 (inducedSqEdges pentCVert a alpha) < 0) ∧
154 ¬ ((7 / 12 : ℝ) < (0 : ℝ))
155
156theorem cm4SignNotActionLevelCertificate :
157 Cm4SignNotActionLevelCertificate :=
158 ⟨threePent_lorentzian_cm4_neg, by norm_num⟩
159
160/-! ## §4. BranchRegularOn / product-form ≠ deficit-sum certificate (S4/S9) -/
161
162/-- **S4+S9 certificate.** Product-form `csqrt(C_pp*C_qq)` is
163kernel-killed at interior arc parameters. -/
164def BranchRegularOnNotDeficitSumCertificate : Prop :=
165 ((tStarMixed ∈ Set.Ioo (0 : ℝ) 1
166 ∧ cmCofactorC (continuationEdgesC CausalPentType.threeTwo 1 1 tStarMixed) 1 1
167 * cmCofactorC (continuationEdgesC CausalPentType.threeTwo 1 1 tStarMixed) 4 4
168 = -40
169 ∧ (-40 : ℂ) ∉ Complex.slitPlane)
170 ∧ ((2 / 3 : ℝ) ∈ Set.Ioo (0 : ℝ) 1
171 ∧ cmCofactorC (continuationEdgesC CausalPentType.threeTwo 1 1 (2 / 3)) 1 1
172 * cmCofactorC (continuationEdgesC CausalPentType.threeTwo 1 1 (2 / 3)) 2 2
173 = -48
174 ∧ (-48 : ℂ) ∉ Complex.slitPlane)) ∧
175 (tStar ∈ Set.Ioo (0 : ℝ) 1
176 ∧ cmCofactorC (continuationEdgesC CausalPentType.fourOne 1 1 tStar) 3 3
177 * cmCofactorC (continuationEdgesC CausalPentType.fourOne 1 1 tStar) 4 4
178 = -32
179 ∧ (-32 : ℂ) ∉ Complex.slitPlane)
180
181theorem branchRegularOnNotDeficitSumCertificate :
182 BranchRegularOnNotDeficitSumCertificate :=
183 ⟨wick_product_form_kills_memorialized, product_form_crossing⟩
184
185/-! ## §5. Two-pent path-link kill (S6) -/
186
187/-- Re-export: interior hinge counting requires ≥ 3 pents. -/
188theorem interior_hinge_needs_three_pents_banked
189 (pents : Finset (Finset (Fin 6)))
190 (hcycle : IsCycleLink (pents.image (fun P => P \ hinge))) :
191 3 ≤ pents.card :=
192 interior_hinge_needs_three_pents pents hcycle
193
194/-- **S6 kill.** The two-pent complex never presents an interior hinge. -/
195theorem two_pent_interior_impossible :
196 ¬ IsCycleLink (twoPentComplex.image (fun P => P \ hinge)) :=
197 twoPent_hinge_never_interior
198
199/-- Packaged two-pent decoy kill + counting lemma. -/
200def TwoPentNotInteriorActionCertificate : Prop :=
201 (¬ IsCycleLink (twoPentComplex.image (fun P => P \ hinge))) ∧
202 (∀ pents : Finset (Finset (Fin 6)),
203 IsCycleLink (pents.image (fun P => P \ hinge)) → 3 ≤ pents.card)
204
205theorem twoPentNotInteriorActionCertificate :
206 TwoPentNotInteriorActionCertificate :=
207 ⟨two_pent_interior_impossible, interior_hinge_needs_three_pents_banked⟩
208
209/-! ## §6. Euclidean EH recovery ≠ gap6 close (S7) -/
210
211/-- **S7 certificate.** `S_RS_converges_EH_4d` inhabits
212`gap_action_recovery`; it is Euclidean EH recovery, not the Lorentzian
213action-continuation closer. Post-close separation: EH co-asserts with the
214real gap6 closer `wick_action_continuation_4d_v2` (distinct named
215terminals; EH alone would not have sufficed for gap6 / V2). -/
216def EHRecoveryNotGap6Certificate : Prop :=
217 S_RS_converges_EH_4d ∧
218 fullTheoryBenchmarks.gap_action_recovery = true ∧
219 wick_action_continuation_4d_v2 ∧
220 fullTheoryBenchmarks.gap6_lorentzian_action = true
221
222theorem ehRecoveryNotGap6Certificate :
223 EHRecoveryNotGap6Certificate :=
224 ⟨S_RS_converges_EH_4d_closed, rfl, wick_action_continuation_4d_v2_holds, rfl⟩
225
226/-! ## §7. Ledger terminal guard (post-F3 succession) -/
227
228/-- **Guard Prop after F3 close.** Gap6 flipped via V2; campaign /
229CausalSimplex4D action-open bits cleared; kinematical Wick certified;
2303D LorentzianSector action bit remains open. -/
231def Gap6LedgerTerminalGuard : Prop :=
232 fullTheoryBenchmarks.gap6_lorentzian_action = true ∧
233 sevenGapsCampaignStatus.gap6_action_continuation_open = false ∧
234 causalSimplex4DStatus.action_level_continuation_open = false ∧
235 lorentzianSectorStatus.lorentzian_action_continuation_open = true ∧
236 sevenGapsCampaignStatus.gap6_kinematical_wick_certified = true
237
238theorem gap6LedgerTerminalGuard : Gap6LedgerTerminalGuard :=
239 ⟨rfl, rfl, rfl, rfl, rfl⟩
240
241/-! ## §8. DAG R0 residual (all lookalike decoys fail) -/
242
243/-- **DAG R0 residual Prop.** Lookalikes separated by content; post-F3
244guard records the V2 ledger close. -/
245def TypedResidual_gap6_lookalike_decoys_fail : Prop :=
246 LorentzianContinuation3DNotAction4DCertificate ∧
247 LorentzianContinuation4DKinematicalNotActionCertificate ∧
248 HingeDataNotActionLevelCertificate ∧
249 Cm4SignNotActionLevelCertificate ∧
250 BranchRegularOnNotDeficitSumCertificate ∧
251 TwoPentNotInteriorActionCertificate ∧
252 EHRecoveryNotGap6Certificate ∧
253 Gap6LedgerTerminalGuard
254
255/-- R0 residual closed by the lookalike-falsify package. -/
256theorem typedResidual_gap6_lookalike_decoys_fail :
257 TypedResidual_gap6_lookalike_decoys_fail :=
258 ⟨lorentzianContinuation3DNotAction4DCertificate,
259 lorentzianContinuation4DKinematicalNotActionCertificate,
260 hingeDataNotActionLevelCertificate,
261 cm4SignNotActionLevelCertificate,
262 branchRegularOnNotDeficitSumCertificate,
263 twoPentNotInteriorActionCertificate,
264 ehRecoveryNotGap6Certificate,
265 gap6LedgerTerminalGuard⟩
266
267theorem TypedResidual_gap6_lookalike_decoys_fail_closed :
268 TypedResidual_gap6_lookalike_decoys_fail :=
269 typedResidual_gap6_lookalike_decoys_fail
270
271/-! ## §9. Status (R0 lookalike receipt closed; gap6 flipped via V2) -/
272
273structure Gap6LookalikeReceiptStatus where
274 /-- R0 lookalike-falsify receipt closed. -/
275 lookalikeReceiptClosed : Bool
276 /-- Frozen V1 schema: closed (not open). -/
277 wickActionSchemaOpen : Bool
278 /-- Deficit-sum branch regularity: closed via CertV2. -/
279 deficitSumBranchOpen : Bool
280 /-- Ledger terminal: closed via `wick_action_continuation_4d_v2`. -/
281 wickActionTerminalOpen : Bool
282 /-- Ledger flag flipped 2026-07-23. -/
283 gap6LorentzianAction : Bool
284
285def gap6LookalikeReceiptStatus : Gap6LookalikeReceiptStatus where
286 lookalikeReceiptClosed := true
287 wickActionSchemaOpen := false
288 deficitSumBranchOpen := false
289 wickActionTerminalOpen := false
290 gap6LorentzianAction := true
291
292/-- Status theorem: R0 lookalike separation retained; gap6 closed via V2. -/
293theorem gap6LookalikeReceiptStatus_flags :
294 gap6LookalikeReceiptStatus.lookalikeReceiptClosed = true ∧
295 gap6LookalikeReceiptStatus.wickActionSchemaOpen = false ∧
296 gap6LookalikeReceiptStatus.deficitSumBranchOpen = false ∧
297 gap6LookalikeReceiptStatus.wickActionTerminalOpen = false ∧
298 gap6LookalikeReceiptStatus.gap6LorentzianAction = true ∧
299 fullTheoryBenchmarks.gap6_lorentzian_action = true ∧
300 sevenGapsCampaignStatus.gap6_action_continuation_open = false ∧
301 causalSimplex4DStatus.action_level_continuation_open = false ∧
302 lorentzianSectorStatus.lorentzian_action_continuation_open
303 = true ∧
304 sevenGapsCampaignStatus.gap6_kinematical_wick_certified
305 = true := by
306 decide
307
308end
309
310end Gap6LookalikeReceipt
311end SevenGaps
312end Gravity
313end IndisputableMonolith
314