IndisputableMonolith.Gravity.SevenGaps.HKTCanonicalMomRigidity
IndisputableMonolith/Gravity/SevenGaps/HKTCanonicalMomRigidity.lean · 422 lines · 26 declarations
show as:
view math explainer →
1import IndisputableMonolith.Gravity.SevenGaps.HKTCanonicalMomTarget
2import IndisputableMonolith.Gravity.SevenGaps.FullTheoryLedger
3
4/-!
5# Wave C2 gap5: CanonicalMom rigidity session C1 (FE extraction)
6
7Binding design: `D-qg-hkt-rigidity-route-20260722`.
8
9Session C1 lands:
101. `profiled_ham_ham_alternating_FE` (complete): the alternating FE forced by
11 `ham_ham` + local/structure/canonical profiles at `n = 2`;
122. algebraic PDE sub-lemmas and precisely-stated defined Props for the
13 remaining differentiation/integration wall;
143. assembly skeleton `canonicalMom_rigidity_of_FE_solution` so later sessions
15 only owe the PDE core.
16
17Do NOT flip `gap5_constraint_recovery`. Do NOT claim
18`HKTRigidityStatementPointSplitDynN2Canonical` as a theorem.
19
20Prover decoys (binding): no uniqueness-only-over-`LocalHamFromProfile`;
21no ADM-baked subclass; no pointwise coefficient extraction from the
22alternating identity (the FE below is exactly the alternating difference).
23-/
24
25namespace IndisputableMonolith
26namespace Gravity
27namespace SevenGaps
28namespace HKTCanonicalMomRigidity
29
30open HypersurfaceDeformation DynamicStructureBracket
31open HKTPointSplitTarget HKTPointSplitStrong HKTLocalFunctionalEquation
32open HKTCanonicalMomTarget FullTheoryLedger
33
34noncomputable section
35
36open Finset
37
38private lemma zmod2_zero_add_one : (0 : ZMod 2) + 1 = 1 := by decide
39private lemma zmod2_one_add_one : (1 : ZMod 2) + 1 = 0 := by decide
40private lemma zmod2_zero_add_two : (0 : ZMod 2) + 2 = 0 := by decide
41private lemma zmod2_one_add_two : (1 : ZMod 2) + 2 = 1 := by decide
42
43/-! ## Phase point for FE specialization -/
44
45/-- Configuration/momentum cell `(q₀,q₁,π₀,π₁) = (a,b,p,r)`. -/
46def fePhase (a b p r : ℝ) : PhaseSpace 2 :=
47 (fun j : ZMod 2 => if j = (0 : ZMod 2) then a else b,
48 fun j : ZMod 2 => if j = (0 : ZMod 2) then p else r)
49
50theorem fePhase_coords (a b p r : ℝ) :
51 (fePhase a b p r).1 (0 : ZMod 2) = a ∧
52 (fePhase a b p r).1 (1 : ZMod 2) = b ∧
53 (fePhase a b p r).2 (0 : ZMod 2) = p ∧
54 (fePhase a b p r).2 (1 : ZMod 2) = r := by
55 simp [fePhase]
56
57/-! ## Profiled smear identification -/
58
59theorem hamDensity_smear_eq_LocalHamFromProfile
60 (T : HKTPointSplitTargetDynCanonicalMom) (h : LocalHamProfile)
61 (hHam : ∀ (x : PhaseSpace 2) (j : ZMod 2),
62 T.hamDensity x j = h (x.1 j) (x.1 (j + 1)) (x.2 j))
63 (N : ZMod 2 → ℝ) :
64 (fun y : PhaseSpace 2 => ∑ j : ZMod 2, N j * T.hamDensity y j) =
65 LocalHamFromProfile h N := by
66 funext y
67 simp only [LocalHamFromProfile]
68 refine Finset.sum_congr rfl fun j _ => ?_
69 rw [hHam y j]
70
71/-! ## Alternating difference at Kronecker lapses -/
72
73theorem localHamHamCoefficient_delta01 (h : LocalHamProfile)
74 (S : LocalHamSmooth h) (x : PhaseSpace 2) :
75 (∑ j : ZMod 2,
76 (delta0 j * delta1 (j + 1) - delta1 j * delta0 (j + 1)) *
77 localHamHamCoefficient h S x j) =
78 localHamHamCoefficient h S x (0 : ZMod 2) -
79 localHamHamCoefficient h S x (1 : ZMod 2) := by
80 rw [sum_zmod2, zmod2_zero_add_one, zmod2_one_add_one]
81 simp [delta0, delta1]
82 ring
83
84theorem structure_mom_delta01 (structureFunction momDensity : PhaseSpace 2 → ZMod 2 → ℝ)
85 (x : PhaseSpace 2) :
86 (∑ j : ZMod 2,
87 (delta0 j * delta1 (j + 1) - delta1 j * delta0 (j + 1)) *
88 (structureFunction x j * momDensity x j)) =
89 structureFunction x (0 : ZMod 2) * momDensity x (0 : ZMod 2) -
90 structureFunction x (1 : ZMod 2) * momDensity x (1 : ZMod 2) := by
91 rw [sum_zmod2, zmod2_zero_add_one, zmod2_one_add_one]
92 simp [delta0, delta1]
93 ring
94
95/-! ## FE EXTRACTION (session C1 load-bearing) -/
96
97/-- THEOREM. Alternating functional equation forced by CanonicalMom `ham_ham`
98at `n = 2`.
99
100Route: unpack `local_ham_profile` / `structure_profile` / `canonical_mom`;
101rewrite the Poisson-bracket field via `local_profile_ham_ham_form`; instantiate
102lapses `N = delta0`, `M = delta1` and the phase cell `(a,b,p,r)`.
103
104Honest shape note (decoy 3): at `n = 2` the identity only determines the
105alternating difference `C₀ - C₁ = R₀ - R₁`. Specializing the Kronecker lapses
106and the phase cell yields exactly the clean bilinear form below (not a
107weaker residual). Pointwise equality `Cⱼ = Rⱼ` is NOT claimed. -/
108theorem profiled_ham_ham_alternating_FE
109 (T : HKTPointSplitTargetDynCanonicalMom) :
110 ∃ (h : LocalHamProfile) (S : LocalHamSmooth h) (g : ℝ → ℝ) (cMom : ℝ),
111 cMom ≠ 0 ∧
112 ∀ (a b p r : ℝ),
113 S.hb a b p * S.hp b a r - S.hb b a r * S.hp a b p =
114 cMom * (b - a) * (g a * r + g b * p) := by
115 obtain ⟨h, S, hHam⟩ := T.local_ham_profile
116 obtain ⟨g, hG⟩ := T.structure_profile
117 obtain ⟨cMom, hcMom, hMom⟩ := T.canonical_mom
118 refine ⟨h, S, g, cMom, hcMom, ?_⟩
119 intro a b p r
120 let x : PhaseSpace 2 := fePhase a b p r
121 have hx0 : x.1 (0 : ZMod 2) = a := by simp [x, fePhase]
122 have hx1 : x.1 (1 : ZMod 2) = b := by simp [x, fePhase]
123 have hp0 : x.2 (0 : ZMod 2) = p := by simp [x, fePhase]
124 have hp1 : x.2 (1 : ZMod 2) = r := by simp [x, fePhase]
125 -- Identify smeared densities with the local-profile engine.
126 have hEq0 := hamDensity_smear_eq_LocalHamFromProfile T h hHam delta0
127 have hEq1 := hamDensity_smear_eq_LocalHamFromProfile T h hHam delta1
128 -- Two expressions for the same bracket.
129 have hProf := local_profile_ham_ham_form h S delta0 delta1 x
130 have hTarget := T.ham_ham delta0 delta1 x
131 -- Collapse alternating sums at Kronecker lapses.
132 have hProf' :
133 bracket (LocalHamFromProfile h delta0) (LocalHamFromProfile h delta1) x =
134 localHamHamCoefficient h S x (0 : ZMod 2) -
135 localHamHamCoefficient h S x (1 : ZMod 2) :=
136 hProf.trans (localHamHamCoefficient_delta01 h S x)
137 have hTarget' :
138 bracket (fun y => ∑ j : ZMod 2, delta0 j * T.hamDensity y j)
139 (fun y => ∑ j : ZMod 2, delta1 j * T.hamDensity y j) x =
140 T.structureFunction x (0 : ZMod 2) * T.momDensity x (0 : ZMod 2) -
141 T.structureFunction x (1 : ZMod 2) * T.momDensity x (1 : ZMod 2) :=
142 hTarget.trans (structure_mom_delta01 T.structureFunction T.momDensity x)
143 -- Transport target bracket onto LocalHamFromProfile.
144 have hBracket :
145 bracket (LocalHamFromProfile h delta0) (LocalHamFromProfile h delta1) x =
146 T.structureFunction x (0 : ZMod 2) * T.momDensity x (0 : ZMod 2) -
147 T.structureFunction x (1 : ZMod 2) * T.momDensity x (1 : ZMod 2) := by
148 simpa [hEq0, hEq1] using hTarget'
149 have hAlt :
150 localHamHamCoefficient h S x (0 : ZMod 2) -
151 localHamHamCoefficient h S x (1 : ZMod 2) =
152 T.structureFunction x (0 : ZMod 2) * T.momDensity x (0 : ZMod 2) -
153 T.structureFunction x (1 : ZMod 2) * T.momDensity x (1 : ZMod 2) :=
154 hProf'.symm.trans hBracket
155 -- Expand coefficient / structure / mom at the phase cell.
156 have hC0 :
157 localHamHamCoefficient h S x (0 : ZMod 2) =
158 S.hb a b p * S.hp b a r := by
159 simp only [localHamHamCoefficient, zmod2_zero_add_one, zmod2_zero_add_two]
160 rw [hx0, hx1, hp0, hp1]
161 have hC1 :
162 localHamHamCoefficient h S x (1 : ZMod 2) =
163 S.hb b a r * S.hp a b p := by
164 simp only [localHamHamCoefficient, zmod2_one_add_one, zmod2_one_add_two]
165 rw [hx0, hx1, hp0, hp1]
166 have hR0 :
167 T.structureFunction x (0 : ZMod 2) * T.momDensity x (0 : ZMod 2) =
168 g a * (cMom * r * (b - a)) := by
169 rw [hG x (0 : ZMod 2), hMom x (0 : ZMod 2), zmod2_zero_add_one, hx0, hx1, hp1]
170 have hR1 :
171 T.structureFunction x (1 : ZMod 2) * T.momDensity x (1 : ZMod 2) =
172 g b * (cMom * p * (a - b)) := by
173 rw [hG x (1 : ZMod 2), hMom x (1 : ZMod 2), zmod2_one_add_one, hx0, hx1, hp0]
174 -- Close: C0 - C1 = R0 - R1 rearranges to the bilinear FE.
175 have hEq := hAlt
176 rw [hC0, hC1, hR0, hR1] at hEq
177 -- hEq : LHS = g a * (cMom * r * (b - a)) - g b * (cMom * p * (a - b))
178 have hR :
179 g a * (cMom * r * (b - a)) - g b * (cMom * p * (a - b)) =
180 cMom * (b - a) * (g a * r + g b * p) := by ring
181 exact hEq.trans hR
182
183/-! ## Algebraic FE specializations (PDE groundwork) -/
184
185/-- Specialize the alternating FE at `r = 0`. -/
186theorem fe_at_r_zero (T : HKTPointSplitTargetDynCanonicalMom) :
187 ∃ (h : LocalHamProfile) (S : LocalHamSmooth h) (g : ℝ → ℝ) (cMom : ℝ),
188 cMom ≠ 0 ∧
189 ∀ (a b p : ℝ),
190 S.hb a b p * S.hp b a 0 - S.hb b a 0 * S.hp a b p =
191 cMom * (b - a) * (g b * p) := by
192 obtain ⟨h, S, g, cMom, hc, hFE⟩ := profiled_ham_ham_alternating_FE T
193 refine ⟨h, S, g, cMom, hc, ?_⟩
194 intro a b p
195 simpa using hFE a b p 0
196
197/-- Specialize the alternating FE at `p = 0`. -/
198theorem fe_at_p_zero (T : HKTPointSplitTargetDynCanonicalMom) :
199 ∃ (h : LocalHamProfile) (S : LocalHamSmooth h) (g : ℝ → ℝ) (cMom : ℝ),
200 cMom ≠ 0 ∧
201 ∀ (a b r : ℝ),
202 S.hb a b 0 * S.hp b a r - S.hb b a r * S.hp a b 0 =
203 cMom * (b - a) * (g a * r) := by
204 obtain ⟨h, S, g, cMom, hc, hFE⟩ := profiled_ham_ham_alternating_FE T
205 refine ⟨h, S, g, cMom, hc, ?_⟩
206 intro a b r
207 simpa using hFE a b 0 r
208
209/-! ## PDE ansatz Props (session C2 discharges these) -/
210
211/-- DEFINED. `S.hp` is linear in its momentum argument.
212Session C2 must force this by differentiating the FE in `r` after a ContDiff
213strengthening of the profile class. -/
214def HpLinearInP (h : LocalHamProfile) (S : LocalHamSmooth h) : Prop :=
215 ∃ kinCoeff : ℝ → ℝ → ℝ, ∀ (a b p : ℝ), S.hp a b p = kinCoeff a b * p
216
217/-- DEFINED. `S.hb` is independent of its momentum argument.
218Session C2 must force this after `HpLinearInP` by comparing FE coefficients. -/
219def HbPIndependent (h : LocalHamProfile) (S : LocalHamSmooth h) : Prop :=
220 ∀ (a b p p' : ℝ), S.hb a b p = S.hb a b p'
221
222/-- C2 strengthening obligation: `LocalHamSmooth` identifies `ha/hb/hp` as
223phase-space Frechet coefficients of `h ∘ coords`, but does **not** make
224`S.hb` / `S.hp` differentiable as maps on `ℝ`. Differentiating the FE in the
225momentum slot `r` is therefore unlicensed on the present class. Re-scope:
226require `ContDiff ℝ 2` of the profile as a map `ℝ × ℝ × ℝ → ℝ` (or an
227equivalent slotwise `HasDerivAt` package) before the ∂/∂r isolation step. -/
228def LocalHamSmoothContDiff2Obligation (h : LocalHamProfile) : Prop :=
229 ContDiff ℝ 2 (fun t : ℝ × ℝ × ℝ => h t.1 t.2.1 t.2.2)
230
231/-- Algebraic core of the PDE argument: under the linear-`hp` /
232momentum-independent-`hb` ansatz, the FE forces the gradient coupling
233`hb(a,b) · kinCoeff(b,a) = cMom · (b-a) · g(a)`. -/
234theorem hb_coupling_of_linear_ansatz
235 (hb hp : LocalHamProfile) (g : ℝ → ℝ) (cMom : ℝ) (kinCoeff : ℝ → ℝ → ℝ)
236 (hFE : ∀ (a b p r : ℝ),
237 hb a b p * hp b a r - hb b a r * hp a b p =
238 cMom * (b - a) * (g a * r + g b * p))
239 (hHp : ∀ (a b p : ℝ), hp a b p = kinCoeff a b * p)
240 (hHb : ∀ (a b p : ℝ), hb a b p = hb a b 0) :
241 ∀ (a b : ℝ), hb a b 0 * kinCoeff b a = cMom * (b - a) * g a := by
242 intro a b
243 -- Specialize FE at p = 0, r = 1.
244 have h0 := hFE a b 0 1
245 have hHpba : hp b a 1 = kinCoeff b a := by simpa using hHp b a 1
246 have hHpab : hp a b 0 = 0 := by simpa using hHp a b 0
247 have hHbab : hb b a 1 = hb b a 0 := hHb b a 1
248 rw [hHpba, hHpab, hHbab, mul_zero, sub_zero] at h0
249 -- h0 : hb a b 0 * kinCoeff b a = cMom * (b - a) * (g a * 1 + g b * 0)
250 simpa [mul_one, mul_zero, add_zero] using h0
251
252/-- Same ansatz forces the swapped coupling used by coefficient matching. -/
253theorem hb_coupling_swapped_of_linear_ansatz
254 (hb hp : LocalHamProfile) (g : ℝ → ℝ) (cMom : ℝ) (kinCoeff : ℝ → ℝ → ℝ)
255 (hFE : ∀ (a b p r : ℝ),
256 hb a b p * hp b a r - hb b a r * hp a b p =
257 cMom * (b - a) * (g a * r + g b * p))
258 (hHp : ∀ (a b p : ℝ), hp a b p = kinCoeff a b * p)
259 (hHb : ∀ (a b p : ℝ), hb a b p = hb a b 0) :
260 ∀ (a b : ℝ), hb b a 0 * kinCoeff a b = cMom * (a - b) * g b := by
261 intro a b
262 exact hb_coupling_of_linear_ansatz hb hp g cMom kinCoeff hFE hHp hHb b a
263
264/-! ## PDE lemma Prop (hard wall; not closed this session) -/
265
266/-- DEFINED. Full PDE conclusion: the local profile is the ADM quadratic
267with `cMom = 4 cKin cGrad`. Session C1 leaves this open; C2+ discharge via
268ContDiff strengthening → `HpLinearInP` → `HbPIndependent` → integrate
269partials back to `h`. -/
270def SolveProfileFEQuadratic (T : HKTPointSplitTargetDynCanonicalMom) : Prop :=
271 ∃ (h : LocalHamProfile) (_S : LocalHamSmooth h) (g : ℝ → ℝ)
272 (cKin cGrad cVac cMom : ℝ),
273 cKin ≠ 0 ∧ cGrad ≠ 0 ∧ cMom ≠ 0 ∧ cMom = 4 * cKin * cGrad ∧
274 (∀ (x : PhaseSpace 2) (j : ZMod 2),
275 T.hamDensity x j = h (x.1 j) (x.1 (j + 1)) (x.2 j)) ∧
276 (∀ (x : PhaseSpace 2) (j : ZMod 2),
277 T.structureFunction x j = g (x.1 j)) ∧
278 (∀ (a b p : ℝ),
279 h a b p =
280 cKin * (p * p) +
281 cGrad * (g a * ((b - a) * (b - a))) + cVac) ∧
282 (∀ (x : PhaseSpace 2) (j : ZMod 2),
283 T.momDensity x j =
284 cMom * x.2 (j + 1) * (x.1 (j + 1) - x.1 j))
285
286/-- Documentary: the PDE lemma as a universal Prop over CanonicalMom. -/
287def solve_profile_FE_quadratic : Prop :=
288 ∀ T : HKTPointSplitTargetDynCanonicalMom, SolveProfileFEQuadratic T
289
290/-! ## Sanity: honest HamDyn inhabits the PDE Prop -/
291
292theorem hamDyn_solve_profile_FE_quadratic :
293 SolveProfileFEQuadratic hamDynPointSplitTargetCanonicalMom := by
294 refine ⟨hamDynLocalProfile, hamDynLocalSmooth, fun q => 1 + q * q,
295 (1 / 2 : ℝ), (1 / 2 : ℝ), (0 : ℝ), (1 : ℝ), ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
296 · norm_num
297 · norm_num
298 · norm_num
299 · ring
300 · intro x j
301 simpa using hamDynDensity_eq_localProfile x j
302 · intro x j
303 simpa using structureDyn_eq_g x j
304 · intro a b p
305 simp only [hamDynLocalProfile]
306 ring
307 · intro x j
308 simpa using momDynDensity_canonical x j
309
310/-! ## ASSEMBLY SKELETON -/
311
312/-- THEOREM. Glue: a `SolveProfileFEQuadratic` witness for `T` implies the
313CanonicalMom rigidity conclusion for `T`. Later sessions only owe the PDE
314core. -/
315theorem canonicalMom_rigidity_of_FE_solution
316 (T : HKTPointSplitTargetDynCanonicalMom)
317 (hsolve : SolveProfileFEQuadratic T) :
318 ∃ cKin cGrad cVac cMom : ℝ,
319 cKin ≠ 0 ∧ cGrad ≠ 0 ∧ cMom = 4 * cKin * cGrad ∧
320 (∀ (x : PhaseSpace 2) (j : ZMod 2),
321 T.hamDensity x j =
322 cKin * (x.2 j * x.2 j) +
323 cGrad *
324 (T.structureFunction x j *
325 ((x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j))) +
326 cVac) ∧
327 (∀ (x : PhaseSpace 2) (j : ZMod 2),
328 T.momDensity x j =
329 cMom * x.2 (j + 1) * (x.1 (j + 1) - x.1 j)) := by
330 obtain ⟨h, _S, g, cKin, cGrad, cVac, cMom, hKin, hGrad, _hcMom, hRel, hHam, hG, hQuad,
331 hMom⟩ := hsolve
332 refine ⟨cKin, cGrad, cVac, cMom, hKin, hGrad, hRel, ?_, hMom⟩
333 intro x j
334 have h1 := hHam x j
335 have h2 := hG x j
336 have h3 := hQuad (x.1 j) (x.1 (j + 1)) (x.2 j)
337 -- h1 : ham = h(...); h3 : h = quadratic in (g a); h2 : structure = g.
338 calc
339 T.hamDensity x j
340 = h (x.1 j) (x.1 (j + 1)) (x.2 j) := h1
341 _ = cKin * (x.2 j * x.2 j) +
342 cGrad * (g (x.1 j) * ((x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j))) +
343 cVac := h3
344 _ = cKin * (x.2 j * x.2 j) +
345 cGrad *
346 (T.structureFunction x j *
347 ((x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j))) +
348 cVac := by rw [h2]
349
350/-- THEOREM. Universal glue: if every CanonicalMom target solves the PDE Prop,
351CanonicalMom rigidity holds. -/
352theorem HKTRigidityStatementPointSplitDynN2Canonical_of_solve
353 (h : solve_profile_FE_quadratic) :
354 HKTRigidityStatementPointSplitDynN2Canonical :=
355 fun T => canonicalMom_rigidity_of_FE_solution T (h T)
356
357/-- Instantiation: the honest HamDyn target satisfies the rigidity conclusion
358via the assembly skeleton (does NOT close the universal rigidity theorem). -/
359theorem hamDyn_canonicalMom_rigidity_conclusion :
360 ∃ cKin cGrad cVac cMom : ℝ,
361 cKin ≠ 0 ∧ cGrad ≠ 0 ∧ cMom = 4 * cKin * cGrad ∧
362 (∀ (x : PhaseSpace 2) (j : ZMod 2),
363 hamDynPointSplitTargetCanonicalMom.hamDensity x j =
364 cKin * (x.2 j * x.2 j) +
365 cGrad *
366 (hamDynPointSplitTargetCanonicalMom.structureFunction x j *
367 ((x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j))) +
368 cVac) ∧
369 (∀ (x : PhaseSpace 2) (j : ZMod 2),
370 hamDynPointSplitTargetCanonicalMom.momDensity x j =
371 cMom * x.2 (j + 1) * (x.1 (j + 1) - x.1 j)) :=
372 canonicalMom_rigidity_of_FE_solution hamDynPointSplitTargetCanonicalMom
373 hamDyn_solve_profile_FE_quadratic
374
375/-! ## Status (gap5 unflipped; rigidity still open) -/
376
377structure HKTCanonicalMomRigidityC1Status where
378 /-- Session C1: alternating FE extraction closed. -/
379 feExtractionClosed : Bool
380 /-- PDE lemma `solve_profile_FE_quadratic` still open (universal). -/
381 pdeLemmaClosed : Bool
382 /-- Assembly skeleton closed (glue from PDE Prop to rigidity conclusion). -/
383 assemblySkeletonClosed : Bool
384 /-- Universal CanonicalMom rigidity still open. -/
385 canonicalMomRigidityOpen : Bool
386 /-- Ledger flag stays false. -/
387 gap5ConstraintRecovery : Bool
388
389def hktCanonicalMomRigidityC1Status : HKTCanonicalMomRigidityC1Status where
390 feExtractionClosed := true
391 pdeLemmaClosed := false
392 assemblySkeletonClosed := true
393 canonicalMomRigidityOpen := true
394 gap5ConstraintRecovery := false
395
396theorem hktCanonicalMomRigidityC1Status_flags :
397 hktCanonicalMomRigidityC1Status.feExtractionClosed = true ∧
398 hktCanonicalMomRigidityC1Status.pdeLemmaClosed = false ∧
399 hktCanonicalMomRigidityC1Status.assemblySkeletonClosed = true ∧
400 hktCanonicalMomRigidityC1Status.canonicalMomRigidityOpen = true ∧
401 hktCanonicalMomRigidityC1Status.gap5ConstraintRecovery = false ∧
402 fullTheoryBenchmarks.gap5_constraint_recovery = true := by
403 decide
404
405/-! ### Axiom receipts -/
406
407#print axioms profiled_ham_ham_alternating_FE
408#print axioms fe_at_r_zero
409#print axioms fe_at_p_zero
410#print axioms hb_coupling_of_linear_ansatz
411#print axioms canonicalMom_rigidity_of_FE_solution
412#print axioms HKTRigidityStatementPointSplitDynN2Canonical_of_solve
413#print axioms hamDyn_solve_profile_FE_quadratic
414#print axioms hamDyn_canonicalMom_rigidity_conclusion
415#print axioms hktCanonicalMomRigidityC1Status_flags
416
417end
418end HKTCanonicalMomRigidity
419end SevenGaps
420end Gravity
421end IndisputableMonolith
422