IndisputableMonolith.Gravity.Analysis.SRSConvergesEH4D
IndisputableMonolith/Gravity/Analysis/SRSConvergesEH4D.lean · 349 lines · 39 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Gravity.Analysis.Regge4DContinuumPreflight
3import IndisputableMonolith.Gravity.Analysis.RecognitionMeshExactJBridge4D
4import IndisputableMonolith.Gravity.Analysis.EdgeTTDecomposition4D
5import IndisputableMonolith.Gravity.Analysis.EdgeTTDecompositionCloser4D
6import IndisputableMonolith.Gravity.Analysis.ReggeEdgeStencil4D
7import IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianNormGate4D
8import IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianSymbol4D
9import IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianBlochSymbol4D
10import IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianBlochSymbolZero4D
11import IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianBlochM2Rayleigh4D
12import IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianBlochTorusBridge4D
13import IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4D
14import IndisputableMonolith.Gravity.Analysis.Regge4DExactActionSymbol
15import IndisputableMonolith.Gravity.Analysis.ReggeBlochM2Symbol4D
16
17/-!
18# Named closers: `edge_tt_decomposition` and `S_RS_converges_EH_4d`
19
20QG full-theory campaign, ledger-facing export module for weak-field
21quadratic action recovery. The Props are the preflight names; this
22module is the sole place that may later inhabit them for the ledger flip.
23
24## Honest scope
25
26* Weak-field quadratic action convergence only.
27* Not sourced Einstein equation, continuum Ricci/stress, horizon/coframe,
28 arbitrary-curvature GR, or full nonlinear `wick_action_continuation_4d`.
29* `gap_action_recovery` flips only when both named theorems are inhabited
30 on Elmo with focused axiom audits and adversarial review.
31* Banked: `edge_tt_decomposition_closed`; R2 symbolZero; R3 Rayleigh
32 faces; R4 discrete torus-family bridge → ContinuumSymbolIs at m²
33 Rayleigh; Option-C m² faces; honest `S_RS_converges_EH_4d`.
34* `gap_action_recovery` flips with this inhabitant (MEASURED-native_decide
35 via m² table certificates). Never ContinuumSymbolIs = Tendsto of a
36 j-independent constant face.
37-/
38
39namespace IndisputableMonolith
40namespace Gravity
41namespace Analysis
42namespace SRSConvergesEH4D
43
44open Regge4DContinuumPreflight
45open RecognitionMeshExactJBridge4D
46open EdgeTTDecomposition4D
47open EdgeTTDecompositionCloser4D
48open ReggeEdgeStencil4D
49open ReggeExactFlatHessianNormGate4D
50open ReggeExactFlatHessianSymbol4D
51 (exactHessianM2UnitFrobeniusTTCoeff exactHessianM2GaugeCoeff
52 measuredTTNormCoeffN6)
53open ReggeExactFlatHessianBlochSymbol4D
54open ReggeExactFlatHessianBlochSymbolZero4D
55open ReggeExactFlatHessianBlochTorusBridge4D
56open ReggeExactMidpointM2TTIdentity4D
57 (exactMidpointBlochM2_eq_neg_eighth_frobenius_tt
58 exactMidpointBlochM2_gauge_rayleigh_eq_zero)
59open Regge4DExactActionSymbol (discreteExactReggeSymbol)
60open Filter Topology
61
62noncomputable section
63
64/-- Disambiguate shared aliases after multi-module opens. -/
65abbrev Mat4 := Regge4DContinuumPreflight.Mat4
66abbrev Wave4 := Regge4DContinuumPreflight.Wave4
67abbrev exactFlatCrossTermFold := Regge4DExactActionSymbol.exactFlatCrossTermFold
68
69private theorem frobeniusNormSq_preflight_eq_identity (H : Mat4) :
70 Regge4DContinuumPreflight.frobeniusNormSq H =
71 ReggeExactMidpointM2TTIdentity4D.frobeniusNormSq H :=
72 rfl
73
74private theorem waveNormSq_preflight_eq_identity (k : Wave4) :
75 Regge4DContinuumPreflight.waveNormSq k =
76 ReggeExactMidpointM2TTIdentity4D.waveNormSq k :=
77 rfl
78
79/-! ## §1. Re-export of ledger Prop names -/
80
81abbrev edge_tt_decomposition : Prop :=
82 Regge4DContinuumPreflight.edge_tt_decomposition
83
84abbrev S_RS_converges_EH_4d : Prop :=
85 Regge4DContinuumPreflight.S_RS_converges_EH_4d
86
87/-! ## §2. Edge closer inhabited; SRS still open -/
88
89theorem edge_tt_decomposition_closed :
90 edge_tt_decomposition :=
91 EdgeTTDecompositionCloser4D.edge_tt_decomposition
92
93theorem edge_tt_polarization_witnesses :
94 IsTTPolarization4D axisWave axisTTPlusNormalized ∧
95 IsTTPolarization4D axisWave axisTTCrossNormalized :=
96 continuum_target_hypothesis_nonvacuous
97
98theorem edge_tt_gauge_decoy_not_transverse :
99 ¬ IsTransverse axisWave decoyGauge :=
100 EdgeTTDecompositionCloser4D.decoyGauge_not_transverse
101
102theorem srs_converges_eh_4d_requires_both_gates :
103 S_RS_converges_EH_4d =
104 (Regge4DContinuumEHTarget ∧ Regge4DContinuumGaugeZeroTarget) := rfl
105
106theorem discrete_bookkeeping_times_unitF_eq_EH :
107 discreteBookkeepingFactor * exactHessianM2UnitFrobeniusTTCoeff =
108 Regge4DContinuumPreflight.einsteinHilbertTTCoefficient4D :=
109 discreteBookkeeping_recovers_frozen_EH
110
111theorem adversarial_decoys_still_hold :
112 (finiteTTQuadratic decoyGauge = 32 ∧
113 finiteTTQuadratic (axisTTPlus + decoyGauge) ≠
114 finiteTTQuadratic axisTTPlus) ∧
115 (ReggeBlochM2Symbol4D.m2Symbol axisTTPlus = -3 ∧
116 Regge4DContinuumPreflight.einsteinHilbertTTCoefficient4D =
117 -(1 / 4 : ℝ) ∧
118 (-3 : ℝ) ≠ -(1 / 4 : ℝ)) ∧
119 wrongMeshPowerWeight 3 ≠ correctTorusDensityWeight 3 :=
120 ⟨decoy_provisional_weight_fails_gauge, decoy_one_orbit_m2_is_not_continuum_target,
121 decoy_wrong_mesh_power_side3⟩
122
123/-! ## §3. Status -/
124
125structure SRSConvergesEH4DStatus where
126 edgeTTNamed : Bool
127 srsNamed : Bool
128 edgeTTInhabited : Bool
129 srsInhabited : Bool
130 gapActionRecovery : Bool
131
132def srsConvergesEH4DStatus : SRSConvergesEH4DStatus where
133 edgeTTNamed := true
134 srsNamed := true
135 edgeTTInhabited := true
136 srsInhabited := true
137 gapActionRecovery := true
138
139theorem srsConvergesEH4DStatus_flags :
140 srsConvergesEH4DStatus.edgeTTNamed = true ∧
141 srsConvergesEH4DStatus.srsNamed = true ∧
142 srsConvergesEH4DStatus.edgeTTInhabited = true ∧
143 srsConvergesEH4DStatus.srsInhabited = true ∧
144 srsConvergesEH4DStatus.gapActionRecovery = true := by
145 decide
146
147theorem srs_closer_closed :
148 srsConvergesEH4DStatus.srsInhabited = true ∧
149 srsConvergesEH4DStatus.gapActionRecovery = true := by
150 decide
151
152/-! ## §4. Typed residuals (geometric ContinuumSymbolIs Tendsto) -/
153
154def TypedResidual_fold_eq_midpointBloch : Prop :=
155 ∀ (H : Mat4) (k : Wave4),
156 exactFlatCrossTermFold H k = exactMidpointBlochSymbol H k
157
158def TypedResidual_midpointBloch_symbolZero : Prop :=
159 ∀ H : Mat4, exactMidpointBlochSymbolZero H = 0
160
161def TypedResidual_m2_rayleigh_eq_algebraic_face : Prop :=
162 (∀ (H : Mat4) (k : Wave4),
163 IsTT k H →
164 frobeniusNormSq H = 1 →
165 waveNormSq k ≠ 0 →
166 exactMidpointBlochM2 H k / waveNormSq k =
167 exactHessianM2UnitFrobeniusTTCoeff) ∧
168 (∀ (m : Wave4) (v : Wave4),
169 waveNormSq m ≠ 0 →
170 exactMidpointBlochM2 (pureGaugeFamily m v) m / waveNormSq m =
171 exactHessianM2GaugeCoeff)
172
173def TypedResidual_discrete_torus_family_bridge : Prop :=
174 ∀ (m : IntMode4) (E : Mat4),
175 m ≠ 0 →
176 Tendsto
177 (fun j : ℕ =>
178 exactMidpointBlochSymbol E (realMode (torusSide j) m) /
179 momentumNormSq (torusSide j) m)
180 atTop
181 (nhds (exactMidpointBlochM2 E (fun i => (m i : ℝ)) /
182 waveNormSq (fun i => (m i : ℝ))))
183
184/-- **THEOREM (R2):** midpoint Bloch vanishes at zero momentum. -/
185theorem typedResidual_midpointBloch_symbolZero_closed :
186 TypedResidual_midpointBloch_symbolZero :=
187 ReggeExactFlatHessianBlochSymbolZero4D.typedResidual_midpointBloch_symbolZero
188
189/-- **THEOREM (R3):** cosine two-jet Rayleigh equals algebraic m² faces
190(`-1/8` on unit-F TT; `0` on pure gauge). -/
191theorem typedResidual_m2_rayleigh_eq_algebraic_face_closed :
192 TypedResidual_m2_rayleigh_eq_algebraic_face :=
193 ReggeExactFlatHessianBlochM2Rayleigh4D.typedResidual_m2_rayleigh_eq_algebraic_face
194
195/-- **THEOREM (R4):** discrete torus bridge inhabited (uses R2). -/
196theorem typedResidual_discrete_torus_family_bridge :
197 TypedResidual_discrete_torus_family_bridge :=
198 discrete_torus_family_bridge
199
200theorem typedResidual_discrete_torus_family_bridge_closed :
201 TypedResidual_discrete_torus_family_bridge :=
202 typedResidual_discrete_torus_family_bridge
203
204theorem typedResidual_discrete_torus_family_bridge_of_symbolZero
205 (hZ : TypedResidual_midpointBloch_symbolZero) :
206 TypedResidual_discrete_torus_family_bridge :=
207 discrete_torus_family_bridge_of_symbolZero hZ
208
209/-- Bridge transports ContinuumSymbolIs (mesh midpoint sequence) to the
210m² Rayleigh value for every nonzero mode / every polarization. -/
211theorem continuumSymbolIs_of_discrete_torus_bridge
212 (m : IntMode4) (E : Mat4) (hm : m ≠ 0) :
213 Regge4DContinuumSymbolIs m E
214 (exactMidpointBlochM2 E (fun i => (m i : ℝ)) /
215 waveNormSq (fun i => (m i : ℝ))) :=
216 continuumSymbolIs_midpoint_rayleigh m E hm
217
218/-- Option-C face residual (lane 1): Rayleigh equals scale-explicit EH
219face on TT and vanishes on pure gauge. -/
220def TypedResidual_m2_optionC_faces : Prop :=
221 (∀ (m : IntMode4) (E : Mat4),
222 m ≠ 0 →
223 IsTT (fun i => (m i : ℝ)) E →
224 exactMidpointBlochM2 E (fun i => (m i : ℝ)) /
225 waveNormSq (fun i => (m i : ℝ)) =
226 continuumEHScaleExplicitFace E) ∧
227 (∀ (m : IntMode4) (v : Wave4),
228 m ≠ 0 →
229 exactMidpointBlochM2 (pureGaugeFamily (fun i => (m i : ℝ)) v)
230 (fun i => (m i : ℝ)) /
231 waveNormSq (fun i => (m i : ℝ)) = 0)
232
233theorem typedResidual_m2_optionC_faces :
234 TypedResidual_m2_optionC_faces := by
235 refine ⟨?_, ?_⟩
236 · intro m E hm hTT
237 set k : Wave4 := fun i => (m i : ℝ)
238 have hk : waveNormSq k ≠ 0 := waveNormSq_intMode_ne_zero m hm
239 have hRay := exactMidpointBlochM2_eq_neg_eighth_frobenius_tt E k hTT
240 -- Identity norms are definitionally the preflight norms.
241 have hF :
242 ReggeExactMidpointM2TTIdentity4D.frobeniusNormSq E =
243 frobeniusNormSq E :=
244 (frobeniusNormSq_preflight_eq_identity E).symm
245 have hw :
246 ReggeExactMidpointM2TTIdentity4D.waveNormSq k = waveNormSq k :=
247 (waveNormSq_preflight_eq_identity k).symm
248 calc
249 exactMidpointBlochM2 E k / waveNormSq k
250 = ((-(1 / 8) : ℝ) * ReggeExactMidpointM2TTIdentity4D.frobeniusNormSq E *
251 ReggeExactMidpointM2TTIdentity4D.waveNormSq k) /
252 waveNormSq k := by rw [hRay]
253 _ = ((-(1 / 8) : ℝ) * frobeniusNormSq E * waveNormSq k) / waveNormSq k := by
254 rw [hF, hw]
255 _ = (-(1 / 8) : ℝ) * frobeniusNormSq E := by
256 field_simp [hk]
257 _ = continuumEHScaleExplicitFace E :=
258 (continuumEHScaleExplicitFace_eq E).symm
259 · intro m v hm
260 set k : Wave4 := fun i => (m i : ℝ)
261 have hk : waveNormSq k ≠ 0 := waveNormSq_intMode_ne_zero m hm
262 have hk' : ReggeExactMidpointM2TTIdentity4D.waveNormSq k ≠ 0 := by
263 simpa [waveNormSq_preflight_eq_identity] using hk
264 have hGauge := exactMidpointBlochM2_gauge_rayleigh_eq_zero k v hk'
265 simpa [pureGaugeFamily] using hGauge
266
267/-- Compose bridge + Option-C m² faces into EH Tendsto target. -/
268theorem continuumEHTarget_of_bridge_and_m2_faces
269 (hFaces : TypedResidual_m2_optionC_faces) :
270 Regge4DContinuumEHTarget := by
271 intro m E hm hTT
272 have hRay := continuumSymbolIs_of_discrete_torus_bridge m E hm
273 have hEq := hFaces.1 m E hm hTT
274 simpa [hEq] using hRay
275
276/-- Compose bridge + Option-C m² faces into gauge-zero Tendsto target. -/
277theorem continuumGaugeZeroTarget_of_bridge_and_m2_faces
278 (hFaces : TypedResidual_m2_optionC_faces) :
279 Regge4DContinuumGaugeZeroTarget := by
280 intro m v hm
281 have hRay :=
282 continuumSymbolIs_of_discrete_torus_bridge m
283 (pureGaugeFamily (fun i => (m i : ℝ)) v) hm
284 have hEq := hFaces.2 m v hm
285 simpa [hEq] using hRay
286
287/-- Packaged: bridge closed; S_RS inhabit reduces to Option-C m² faces. -/
288theorem srs_converges_eh_4d_of_m2_optionC_faces
289 (hFaces : TypedResidual_m2_optionC_faces) :
290 S_RS_converges_EH_4d :=
291 ⟨continuumEHTarget_of_bridge_and_m2_faces hFaces,
292 continuumGaugeZeroTarget_of_bridge_and_m2_faces hFaces⟩
293
294theorem TypedResidual_m2_optionC_faces_closed :
295 TypedResidual_m2_optionC_faces :=
296 typedResidual_m2_optionC_faces
297
298theorem S_RS_converges_EH_4d_closed :
299 S_RS_converges_EH_4d :=
300 srs_converges_eh_4d_of_m2_optionC_faces typedResidual_m2_optionC_faces
301
302/-- **R5.** Legacy discreteExact ×2 sequence binder (not Option-C ledger
303`ContinuumSymbolIs`). -/
304def TypedResidual_continuum_discreteExact_rebind : Prop :=
305 ∀ (m : IntMode4) (E : Mat4) (Λ : ℝ),
306 Regge4DDiscreteBookkeepingContinuumSymbolIs m E Λ ↔
307 Tendsto
308 (fun j : ℕ =>
309 discreteExactReggeSymbol j m E /
310 momentumNormSq (torusSide j) m)
311 atTop (nhds Λ)
312
313def GeometricTendstoResidualOpen : Prop :=
314 TypedResidual_fold_eq_midpointBloch ∧
315 TypedResidual_midpointBloch_symbolZero ∧
316 TypedResidual_m2_rayleigh_eq_algebraic_face ∧
317 TypedResidual_discrete_torus_family_bridge ∧
318 TypedResidual_continuum_discreteExact_rebind
319
320/-- Bridge lane and Option-C faces are closed, yielding honest S_RS inhabitance. -/
321theorem discrete_torus_bridge_closed_srs_closed :
322 TypedResidual_discrete_torus_family_bridge ∧
323 TypedResidual_midpointBloch_symbolZero ∧
324 TypedResidual_m2_optionC_faces ∧
325 srsConvergesEH4DStatus.srsInhabited = true ∧
326 srsConvergesEH4DStatus.gapActionRecovery = true :=
327 ⟨typedResidual_discrete_torus_family_bridge,
328 typedResidual_midpointBloch_symbolZero_closed,
329 typedResidual_m2_optionC_faces, rfl, rfl⟩
330
331theorem geometric_tendsto_residuals_named_srs_closed :
332 srsConvergesEH4DStatus.srsInhabited = true ∧
333 srsConvergesEH4DStatus.gapActionRecovery = true :=
334 ⟨rfl, rfl⟩
335
336theorem decoy_finiteN_tt_norm_ne_exact_EH_face :
337 measuredTTNormCoeffN6 ≠
338 Regge4DContinuumPreflight.einsteinHilbertTTCoefficient4D := by
339 unfold measuredTTNormCoeffN6
340 Regge4DContinuumPreflight.einsteinHilbertTTCoefficient4D
341 norm_num
342
343end
344
345end SRSConvergesEH4D
346end Analysis
347end Gravity
348end IndisputableMonolith
349