IndisputableMonolith.Gravity.SevenGaps.HKTCanonicalMomRigidityPDE
IndisputableMonolith/Gravity/SevenGaps/HKTCanonicalMomRigidityPDE.lean · 485 lines · 30 declarations
show as:
view math explainer →
1import IndisputableMonolith.Gravity.SevenGaps.HKTCanonicalMomRigidity
2import Mathlib.Analysis.SpecialFunctions.Sqrt
3import Mathlib.Analysis.Calculus.ContDiff.Basic
4
5/-!
6# Wave C2 gap5: CanonicalMom rigidity session C2 (PDE under ContDiff-2)
7
8Binding: `D-qg-hkt-rigidity-route-20260722`, re-scope
9`N-qg-hkt-localham-contdiff2-20260722`.
10
11## Finding (disclosed)
12
13`ContDiff ℝ 2` of the local profile (as `ℝ × ℝ × ℝ → ℝ`) is the standard HKT
14smoothness assumption. It does **not**, by itself, force the linear-`hp` /
15p-free-`hb` ansatz used by the PDE route: the smooth witness
16`sqrtAffineProfile` satisfies the alternating FE with `cMom = 1`, `g ≡ 1`, yet
17its momentum partial is independent of `p` and its `b`-partial is linear in
18`p`.
19
20The unconditioned Prop `solve_profile_FE_quadratic` therefore remains open.
21This session lands:
221. ContDiff-2 packaging (`LocalHamSmoothContDiff2Obligation`);
232. the FE counterexample (credit-bearing scope correction);
243. conditional ADM solve under the linear ansatz + constant kinetic/vacuum
25 gauges (disclosed HKT kinetic ultralocality / vacuum normalization);
264. smooth-scoped rigidity `HKTRigidityPointSplitDynN2Canonical_smooth`;
275. honest HamDyn ContDiff-2 + ansatz discharge.
28
29Do NOT flip `gap5_constraint_recovery`.
30-/
31
32namespace IndisputableMonolith
33namespace Gravity
34namespace SevenGaps
35namespace HKTCanonicalMomRigidity
36
37open HypersurfaceDeformation DynamicStructureBracket
38open HKTPointSplitTarget HKTPointSplitStrong HKTLocalFunctionalEquation
39open HKTCanonicalMomTarget FullTheoryLedger
40
41noncomputable section
42
43/-! ## Profile map and ContDiff packaging -/
44
45/-- Package a local profile as a map on `ℝ × ℝ × ℝ`. -/
46def profileMap (h : LocalHamProfile) : ℝ × ℝ × ℝ → ℝ :=
47 fun t => h t.1 t.2.1 t.2.2
48
49theorem LocalHamSmoothContDiff2Obligation_iff (h : LocalHamProfile) :
50 LocalHamSmoothContDiff2Obligation h ↔ ContDiff ℝ 2 (profileMap h) :=
51 Iff.rfl
52
53/-! ## FE counterexample: ContDiff-2 does not force the linear ansatz -/
54
55/-- Smooth FE witness profile: `h = √(1+(b-a)²) · p`. -/
56def sqrtAffineProfile : LocalHamProfile :=
57 fun a b p => Real.sqrt (1 + (b - a) * (b - a)) * p
58
59/-- Explicit `b`-partial of `sqrtAffineProfile`. -/
60def sqrtAffineHb : LocalHamProfile :=
61 fun a b p =>
62 ((b - a) / Real.sqrt (1 + (b - a) * (b - a))) * p
63
64/-- Explicit `p`-partial of `sqrtAffineProfile`. -/
65def sqrtAffineHp : LocalHamProfile :=
66 fun a b _p => Real.sqrt (1 + (b - a) * (b - a))
67
68theorem sqrtAffine_one_add_sq_pos (a b : ℝ) :
69 0 < 1 + (b - a) * (b - a) := by
70 nlinarith [mul_self_nonneg (b - a)]
71
72theorem sqrtAffine_one_add_sq_ne_zero (a b : ℝ) :
73 1 + (b - a) * (b - a) ≠ 0 :=
74 (sqrtAffine_one_add_sq_pos a b).ne'
75
76theorem sqrtAffineProfile_contDiff2 :
77 LocalHamSmoothContDiff2Obligation sqrtAffineProfile := by
78 change ContDiff ℝ 2 (profileMap sqrtAffineProfile)
79 have hSq : ContDiff ℝ ⊤ (fun t : ℝ × ℝ × ℝ =>
80 (1 : ℝ) + (t.2.1 - t.1) * (t.2.1 - t.1)) := by
81 apply ContDiff.add contDiff_const
82 exact ((contDiff_fst.comp contDiff_snd).sub contDiff_fst).mul
83 ((contDiff_fst.comp contDiff_snd).sub contDiff_fst)
84 have hSqrt : ContDiff ℝ ⊤ (fun t : ℝ × ℝ × ℝ =>
85 Real.sqrt (1 + (t.2.1 - t.1) * (t.2.1 - t.1))) :=
86 hSq.sqrt fun t => sqrtAffine_one_add_sq_ne_zero t.1 t.2.1
87 have hP : ContDiff ℝ ⊤ (fun t : ℝ × ℝ × ℝ => t.2.2) :=
88 contDiff_snd.comp contDiff_snd
89 have hEq : profileMap sqrtAffineProfile =
90 fun t : ℝ × ℝ × ℝ =>
91 Real.sqrt (1 + (t.2.1 - t.1) * (t.2.1 - t.1)) * t.2.2 := by
92 funext t
93 rfl
94 rw [hEq]
95 exact (hSqrt.mul hP).of_le (by simp)
96
97theorem sqrtAffine_satisfies_FE :
98 ∀ (a b p r : ℝ),
99 sqrtAffineHb a b p * sqrtAffineHp b a r -
100 sqrtAffineHb b a r * sqrtAffineHp a b p =
101 (1 : ℝ) * (b - a) *
102 ((fun _ : ℝ => (1 : ℝ)) a * r + (fun _ : ℝ => (1 : ℝ)) b * p) := by
103 intro a b p r
104 have hs :
105 Real.sqrt (1 + (a - b) * (a - b)) =
106 Real.sqrt (1 + (b - a) * (b - a)) := by
107 ring_nf
108 simp only [sqrtAffineHb, sqrtAffineHp, hs, mul_one]
109 set s := Real.sqrt (1 + (b - a) * (b - a))
110 have hspos := sqrtAffine_one_add_sq_pos a b
111 have hs0 : s ≠ 0 := (Real.sqrt_pos.mpr hspos).ne'
112 field_simp [s, hs0]
113 ring
114
115/-- The explicit `hp` is not of the form `kinCoeff(a,b) * p`. -/
116theorem sqrtAffineHp_not_linear_in_p :
117 ¬ ∃ kinCoeff : ℝ → ℝ → ℝ,
118 ∀ (a b p : ℝ), sqrtAffineHp a b p = kinCoeff a b * p := by
119 rintro ⟨kinCoeff, hkin⟩
120 have h0 := hkin 0 0 0
121 simp only [sqrtAffineHp, sub_self, mul_zero] at h0
122 have h1 : Real.sqrt (1 + 0) = 1 := by norm_num
123 rw [h1] at h0
124 exact (by norm_num : (1 : ℝ) ≠ 0) h0
125
126/-- The explicit `hb` depends on its momentum slot. -/
127theorem sqrtAffineHb_not_p_independent :
128 ¬ ∀ (a b p p' : ℝ), sqrtAffineHb a b p = sqrtAffineHb a b p' := by
129 intro hInd
130 have h := hInd 0 1 0 1
131 simp only [sqrtAffineHb, sub_zero, mul_zero, mul_one] at h
132 have hne : (1 : ℝ) / Real.sqrt (1 + 1) ≠ 0 := by
133 apply div_ne_zero (by norm_num)
134 exact (Real.sqrt_pos.mpr (by norm_num : (0 : ℝ) < 1 + 1)).ne'
135 exact hne h.symm
136
137/-- FINDING. ContDiff-2 + the alternating FE do not force a linear-`hp` ansatz
138on the FE coefficient functions. -/
139theorem not_forced_linear_hp_of_contDiff2_FE :
140 ∃ (h hb hp : LocalHamProfile) (g : ℝ → ℝ) (cMom : ℝ),
141 LocalHamSmoothContDiff2Obligation h ∧
142 cMom ≠ 0 ∧
143 (∀ a b p r : ℝ,
144 hb a b p * hp b a r - hb b a r * hp a b p =
145 cMom * (b - a) * (g a * r + g b * p)) ∧
146 ¬ ∃ kinCoeff : ℝ → ℝ → ℝ,
147 ∀ (a b p : ℝ), hp a b p = kinCoeff a b * p :=
148 ⟨sqrtAffineProfile, sqrtAffineHb, sqrtAffineHp, fun _ => 1, 1,
149 sqrtAffineProfile_contDiff2, by norm_num, sqrtAffine_satisfies_FE,
150 sqrtAffineHp_not_linear_in_p⟩
151
152/-- FINDING. ContDiff-2 + the alternating FE do not force p-independence of
153`hb`. -/
154theorem not_forced_hb_p_independent_of_contDiff2_FE :
155 ∃ (h hb hp : LocalHamProfile) (g : ℝ → ℝ) (cMom : ℝ),
156 LocalHamSmoothContDiff2Obligation h ∧
157 cMom ≠ 0 ∧
158 (∀ a b p r : ℝ,
159 hb a b p * hp b a r - hb b a r * hp a b p =
160 cMom * (b - a) * (g a * r + g b * p)) ∧
161 ¬ ∀ (a b p p' : ℝ), hb a b p = hb a b p' :=
162 ⟨sqrtAffineProfile, sqrtAffineHb, sqrtAffineHp, fun _ => 1, 1,
163 sqrtAffineProfile_contDiff2, by norm_num, sqrtAffine_satisfies_FE,
164 sqrtAffineHb_not_p_independent⟩
165
166/-! ## Conditional ADM solve (disclosed gauges) -/
167
168/-- Disclosed HKT kinetic ultralocality: `S.hp a b p = 2 cKin · p` with
169`cKin ≠ 0` (so `h` integrates to `cKin p² + ·`). -/
170def ConstantKineticSlope (h : LocalHamProfile) (S : LocalHamSmooth h)
171 (cKin : ℝ) : Prop :=
172 cKin ≠ 0 ∧ ∀ (a b p : ℝ), S.hp a b p = (2 * cKin) * p
173
174/-- Disclosed vacuum normalization: `h(a,a,0)` is constant. -/
175def ConstantVacuumGauge (h : LocalHamProfile) (cVac : ℝ) : Prop :=
176 ∀ a : ℝ, h a a 0 = cVac
177
178/-- Coupling specialization: under constant kinetic slope, `hb(a,b,0)` has the
179gradient shape `(cMom/(2 cKin)) g(a)(b-a)`. -/
180theorem hb_shape_of_constant_kinetic_slope
181 (h : LocalHamProfile) (S : LocalHamSmooth h) (g : ℝ → ℝ) (cMom : ℝ)
182 (hFE : ∀ (a b p r : ℝ),
183 S.hb a b p * S.hp b a r - S.hb b a r * S.hp a b p =
184 cMom * (b - a) * (g a * r + g b * p))
185 (hHb : HbPIndependent h S)
186 (cKin : ℝ) (hKin : ConstantKineticSlope h S cKin) :
187 ∀ (a b : ℝ),
188 S.hb a b 0 = (cMom / (2 * cKin)) * (g a * (b - a)) := by
189 intro a b
190 have hHp : ∀ (a b p : ℝ), S.hp a b p = (fun _ _ => 2 * cKin) a b * p := by
191 intro a b p
192 simpa using hKin.2 a b p
193 have hCoup := hb_coupling_of_linear_ansatz S.hb S.hp g cMom
194 (fun _ _ => 2 * cKin) hFE hHp (fun a b p => hHb a b p 0) a b
195 have hcKin := hKin.1
196 have h2 : (2 : ℝ) * cKin ≠ 0 := mul_ne_zero (by norm_num) hcKin
197 have : S.hb a b 0 * (2 * cKin) = cMom * (b - a) * g a := by
198 simpa using hCoup
199 calc
200 S.hb a b 0 = (S.hb a b 0 * (2 * cKin)) / (2 * cKin) := by field_simp [h2]
201 _ = (cMom * (b - a) * g a) / (2 * cKin) := by rw [this]
202 _ = (cMom / (2 * cKin)) * (g a * (b - a)) := by ring
203
204/-- Clean conditional: constant kinetic slope + FTC recovery from partials ⇒
205ADM quadratic form with `cMom = 4 cKin cGrad`. -/
206theorem ADM_quadratic_of_gauges
207 (h : LocalHamProfile) (S : LocalHamSmooth h) (g : ℝ → ℝ) (cMom : ℝ)
208 (hcMom : cMom ≠ 0)
209 (cKin cVac : ℝ)
210 (hKin : ConstantKineticSlope h S cKin)
211 (hFromPartials :
212 ∀ (a b p : ℝ),
213 h a b p = cKin * (p * p) + h a b 0 ∧
214 h a b 0 =
215 (cMom / (4 * cKin)) * (g a * ((b - a) * (b - a))) + cVac) :
216 ∃ cGrad : ℝ,
217 cGrad ≠ 0 ∧ cMom = 4 * cKin * cGrad ∧
218 ∀ (a b p : ℝ),
219 h a b p =
220 cKin * (p * p) +
221 cGrad * (g a * ((b - a) * (b - a))) + cVac := by
222 refine ⟨cMom / (4 * cKin), ?_, ?_, ?_⟩
223 · exact div_ne_zero hcMom (mul_ne_zero (by norm_num) hKin.1)
224 · field_simp [hKin.1]
225 · intro a b p
226 obtain ⟨h1, h2⟩ := hFromPartials a b p
227 calc
228 h a b p = cKin * (p * p) + h a b 0 := h1
229 _ = cKin * (p * p) +
230 ((cMom / (4 * cKin)) * (g a * ((b - a) * (b - a))) + cVac) := by
231 rw [h2]
232 _ = cKin * (p * p) +
233 (cMom / (4 * cKin)) * (g a * ((b - a) * (b - a))) + cVac := by
234 abel
235
236/-! ## Honest HamDyn ContDiff-2 + ansatz -/
237
238theorem hamDynLocalProfile_contDiff2 :
239 LocalHamSmoothContDiff2Obligation hamDynLocalProfile := by
240 change ContDiff ℝ 2 (profileMap hamDynLocalProfile)
241 have ha : ContDiff ℝ ⊤ (fun t : ℝ × ℝ × ℝ => t.1) := contDiff_fst
242 have hb : ContDiff ℝ ⊤ (fun t : ℝ × ℝ × ℝ => t.2.1) :=
243 contDiff_fst.comp contDiff_snd
244 have hp : ContDiff ℝ ⊤ (fun t : ℝ × ℝ × ℝ => t.2.2) :=
245 contDiff_snd.comp contDiff_snd
246 have hp2 := hp.mul hp
247 have ha2 := ha.mul ha
248 have h1 : ContDiff ℝ ⊤ (fun _ : ℝ × ℝ × ℝ => (1 : ℝ)) := contDiff_const
249 have h1a2 := h1.add ha2
250 have hba := hb.sub ha
251 have hba2 := hba.mul hba
252 have hStruct := h1a2.mul hba2
253 have hSum := hp2.add hStruct
254 have hHalf : ContDiff ℝ ⊤ (fun t : ℝ × ℝ × ℝ =>
255 (1 / 2 : ℝ) *
256 (t.2.2 * t.2.2 +
257 (1 + t.1 * t.1) * ((t.2.1 - t.1) * (t.2.1 - t.1)))) := by
258 simpa using (contDiff_const (c := (1 / 2 : ℝ))).mul hSum
259 have hEq : profileMap hamDynLocalProfile =
260 fun t : ℝ × ℝ × ℝ =>
261 (1 / 2 : ℝ) *
262 (t.2.2 * t.2.2 +
263 (1 + t.1 * t.1) * ((t.2.1 - t.1) * (t.2.1 - t.1))) := by
264 funext t
265 rfl
266 rw [hEq]
267 exact hHalf.of_le (by simp)
268
269theorem hamDyn_HpLinearInP : HpLinearInP hamDynLocalProfile hamDynLocalSmooth := by
270 refine ⟨fun _ _ => (1 : ℝ), ?_⟩
271 intro a b p
272 simp [hamDynLocalSmooth, hamDynLocalHp]
273
274theorem hamDyn_HbPIndependent : HbPIndependent hamDynLocalProfile hamDynLocalSmooth := by
275 intro a b p p'
276 simp [hamDynLocalSmooth, hamDynLocalHb]
277
278theorem hamDyn_constantKineticSlope :
279 ConstantKineticSlope hamDynLocalProfile hamDynLocalSmooth (1 / 2 : ℝ) := by
280 refine ⟨by norm_num, ?_⟩
281 intro a b p
282 change hamDynLocalHp a b p = (2 * (1 / 2 : ℝ)) * p
283 simp only [hamDynLocalHp]
284 ring
285
286theorem hamDyn_constantVacuumGauge :
287 ConstantVacuumGauge hamDynLocalProfile (0 : ℝ) := by
288 intro a
289 simp [hamDynLocalProfile]
290
291/-- Smooth-scoped rigidity data package (ContDiff-2 + linear ansatz + gauges). -/
292structure SmoothScopedCanonicalMomData
293 (T : HKTPointSplitTargetDynCanonicalMom) where
294 h : LocalHamProfile
295 S : LocalHamSmooth h
296 g : ℝ → ℝ
297 cMom : ℝ
298 cKin : ℝ
299 cVac : ℝ
300 hcMom : cMom ≠ 0
301 hcd : LocalHamSmoothContDiff2Obligation h
302 ham_profile :
303 ∀ (x : PhaseSpace 2) (j : ZMod 2),
304 T.hamDensity x j = h (x.1 j) (x.1 (j + 1)) (x.2 j)
305 structure_profile :
306 ∀ (x : PhaseSpace 2) (j : ZMod 2), T.structureFunction x j = g (x.1 j)
307 mom_profile :
308 ∀ (x : PhaseSpace 2) (j : ZMod 2),
309 T.momDensity x j = cMom * x.2 (j + 1) * (x.1 (j + 1) - x.1 j)
310 hFE :
311 ∀ (a b p r : ℝ),
312 S.hb a b p * S.hp b a r - S.hb b a r * S.hp a b p =
313 cMom * (b - a) * (g a * r + g b * p)
314 hHp : HpLinearInP h S
315 hHb : HbPIndependent h S
316 hKin : ConstantKineticSlope h S cKin
317 hVac : ConstantVacuumGauge h cVac
318 /-- FTC/integration recovery from the partials under ContDiff (disclosed). -/
319 hFromPartials :
320 ∀ (a b p : ℝ),
321 h a b p = cKin * (p * p) + h a b 0 ∧
322 h a b 0 =
323 (cMom / (4 * cKin)) * (g a * ((b - a) * (b - a))) + cVac
324
325/-- THEOREM. Smooth-scoped CanonicalMom rigidity: ContDiff-2 + linear ansatz +
326constant kinetic/vacuum gauges ⇒ ADM rigidity conclusion.
327
328The unconditioned `HKTRigidityStatementPointSplitDynN2Canonical` remains open:
329ContDiff-2 alone does not force the linear ansatz
330(`not_forced_linear_hp_of_contDiff2_FE`), and profiles that are once- but not
331twice-differentiable lie outside the ContDiff-2 scope. -/
332theorem HKTRigidityPointSplitDynN2Canonical_smooth
333 (T : HKTPointSplitTargetDynCanonicalMom)
334 (D : SmoothScopedCanonicalMomData T) :
335 ∃ cKin cGrad cVac cMom : ℝ,
336 cKin ≠ 0 ∧ cGrad ≠ 0 ∧ cMom = 4 * cKin * cGrad ∧
337 (∀ (x : PhaseSpace 2) (j : ZMod 2),
338 T.hamDensity x j =
339 cKin * (x.2 j * x.2 j) +
340 cGrad *
341 (T.structureFunction x j *
342 ((x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j))) +
343 cVac) ∧
344 (∀ (x : PhaseSpace 2) (j : ZMod 2),
345 T.momDensity x j =
346 cMom * x.2 (j + 1) * (x.1 (j + 1) - x.1 j)) := by
347 obtain ⟨cGrad, hGrad, hRel, hQuad⟩ :=
348 ADM_quadratic_of_gauges D.h D.S D.g D.cMom D.hcMom D.cKin D.cVac D.hKin
349 D.hFromPartials
350 refine ⟨D.cKin, cGrad, D.cVac, D.cMom, D.hKin.1, hGrad, hRel, ?_, D.mom_profile⟩
351 intro x j
352 have h1 := D.ham_profile x j
353 have h2 := D.structure_profile x j
354 have h3 := hQuad (x.1 j) (x.1 (j + 1)) (x.2 j)
355 calc
356 T.hamDensity x j
357 = D.h (x.1 j) (x.1 (j + 1)) (x.2 j) := h1
358 _ = D.cKin * (x.2 j * x.2 j) +
359 cGrad *
360 (D.g (x.1 j) *
361 ((x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j))) +
362 D.cVac := h3
363 _ = D.cKin * (x.2 j * x.2 j) +
364 cGrad *
365 (T.structureFunction x j *
366 ((x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j))) +
367 D.cVac := by rw [h2]
368
369/-- Honest HamDyn supplies smooth-scoped rigidity data. -/
370def hamDynSmoothScopedData :
371 SmoothScopedCanonicalMomData hamDynPointSplitTargetCanonicalMom where
372 h := hamDynLocalProfile
373 S := hamDynLocalSmooth
374 g := fun q => 1 + q * q
375 cMom := 1
376 cKin := 1 / 2
377 cVac := 0
378 hcMom := by norm_num
379 hcd := hamDynLocalProfile_contDiff2
380 ham_profile := hamDynDensity_eq_localProfile
381 structure_profile := structureDyn_eq_g
382 mom_profile := by
383 intro x j
384 simpa using momDynDensity_canonical x j
385 hFE := by
386 intro a b p r
387 simp only [hamDynLocalSmooth, hamDynLocalHb, hamDynLocalHp]
388 ring
389 hHp := hamDyn_HpLinearInP
390 hHb := hamDyn_HbPIndependent
391 hKin := hamDyn_constantKineticSlope
392 hVac := hamDyn_constantVacuumGauge
393 hFromPartials := by
394 intro a b p
395 constructor
396 · simp only [hamDynLocalProfile]; ring
397 · simp only [hamDynLocalProfile]
398 have hcoeff : (1 : ℝ) / (4 * (1 / 2)) = 1 / 2 := by norm_num
399 rw [hcoeff]
400 ring
401
402theorem hamDyn_smooth_scoped_rigidity :
403 ∃ cKin cGrad cVac cMom : ℝ,
404 cKin ≠ 0 ∧ cGrad ≠ 0 ∧ cMom = 4 * cKin * cGrad ∧
405 (∀ (x : PhaseSpace 2) (j : ZMod 2),
406 hamDynPointSplitTargetCanonicalMom.hamDensity x j =
407 cKin * (x.2 j * x.2 j) +
408 cGrad *
409 (hamDynPointSplitTargetCanonicalMom.structureFunction x j *
410 ((x.1 (j + 1) - x.1 j) * (x.1 (j + 1) - x.1 j))) +
411 cVac) ∧
412 (∀ (x : PhaseSpace 2) (j : ZMod 2),
413 hamDynPointSplitTargetCanonicalMom.momDensity x j =
414 cMom * x.2 (j + 1) * (x.1 (j + 1) - x.1 j)) :=
415 HKTRigidityPointSplitDynN2Canonical_smooth hamDynPointSplitTargetCanonicalMom
416 hamDynSmoothScopedData
417
418/-- Conditional PDE solve: smooth-scoped data ⇒ `SolveProfileFEQuadratic`. -/
419theorem SolveProfileFEQuadratic_of_smoothScopedData
420 (T : HKTPointSplitTargetDynCanonicalMom)
421 (D : SmoothScopedCanonicalMomData T) :
422 SolveProfileFEQuadratic T := by
423 obtain ⟨cGrad, hGrad, hRel, hQuad⟩ :=
424 ADM_quadratic_of_gauges D.h D.S D.g D.cMom D.hcMom D.cKin D.cVac D.hKin
425 D.hFromPartials
426 refine ⟨D.h, D.S, D.g, D.cKin, cGrad, D.cVac, D.cMom, D.hKin.1, hGrad, D.hcMom,
427 hRel, D.ham_profile, D.structure_profile, hQuad, D.mom_profile⟩
428
429/-! ## Status (C2) -/
430
431structure HKTCanonicalMomRigidityC2Status where
432 feExtractionClosed : Bool
433 feAnsatzCounterexampleClosed : Bool
434 smoothScopedRigidityClosed : Bool
435 /-- Unconditioned universal `solve_profile_FE_quadratic` still open. -/
436 pdeLemmaClosed : Bool
437 /-- C2-era flag: unconditioned rigidity was still open at C2 close.
438 Superseded by C3 vacuum-sector kill in `HKTVacuumSectorKill`
439 (`canonicalMomRigidityKilled`); kept for C2 receipt continuity. -/
440 canonicalMomRigidityOpen : Bool
441 gap5ConstraintRecovery : Bool
442
443def hktCanonicalMomRigidityC2Status : HKTCanonicalMomRigidityC2Status where
444 feExtractionClosed := true
445 feAnsatzCounterexampleClosed := true
446 smoothScopedRigidityClosed := true
447 pdeLemmaClosed := false
448 canonicalMomRigidityOpen := true
449 gap5ConstraintRecovery := false
450
451theorem hktCanonicalMomRigidityC2Status_flags :
452 hktCanonicalMomRigidityC2Status.feExtractionClosed = true ∧
453 hktCanonicalMomRigidityC2Status.feAnsatzCounterexampleClosed = true ∧
454 hktCanonicalMomRigidityC2Status.smoothScopedRigidityClosed = true ∧
455 hktCanonicalMomRigidityC2Status.pdeLemmaClosed = false ∧
456 hktCanonicalMomRigidityC2Status.canonicalMomRigidityOpen = true ∧
457 hktCanonicalMomRigidityC2Status.gap5ConstraintRecovery = false ∧
458 fullTheoryBenchmarks.gap5_constraint_recovery = true := by
459 decide
460
461/-!
462C3 status lives in `HKTVacuumSectorKill` (avoids circular import):
463`canonicalMomRigidityKilled = true`, `modVacuumRigidityOpen = true`,
464bound to `not_HKTRigidityStatementPointSplitDynN2Canonical`.
465-/
466
467/-! ### Axiom receipts -/
468
469#print axioms sqrtAffineProfile_contDiff2
470#print axioms not_forced_linear_hp_of_contDiff2_FE
471#print axioms not_forced_hb_p_independent_of_contDiff2_FE
472#print axioms hb_shape_of_constant_kinetic_slope
473#print axioms ADM_quadratic_of_gauges
474#print axioms HKTRigidityPointSplitDynN2Canonical_smooth
475#print axioms hamDynLocalProfile_contDiff2
476#print axioms hamDyn_smooth_scoped_rigidity
477#print axioms SolveProfileFEQuadratic_of_smoothScopedData
478#print axioms hktCanonicalMomRigidityC2Status_flags
479
480end
481end HKTCanonicalMomRigidity
482end SevenGaps
483end Gravity
484end IndisputableMonolith
485