IndisputableMonolith.Gravity.NullConeQuadraticTensorClass
IndisputableMonolith/Gravity/NullConeQuadraticTensorClass.lean · 497 lines · 27 declarations
show as:
view math explainer →
1import IndisputableMonolith.Gravity.ClausiusEinsteinBridge
2
3/-!
4# Null-cone quadratic tensor class (Phase 5 algebraic prerequisite)
5
6Finite-dimensional real linear algebra: the values of a symmetric quadratic
7form on all Minkowski-null covectors determine the symmetric matrix modulo a
8scalar multiple of the Minkowski metric `η = diag(-1,1,1,1)`.
9
10This is a rigidity package and algebraic prerequisite for Phase 5. It is not
11the independently geometric tensor `G` required by that phase. Tier A remains
12OPEN until a symmetric `G` is constructed from Recognition area/focusing
13ancestry independently of the fixed stress tensor. This module does **not**
14identify a matrix with Ricci or stress-energy, construct horizons or Unruh
15temperature, or close the Einstein field equation.
16
17Honesty tags:
18
19* THEOREM: null-cone reconstruction of symmetric matrices modulo `η`;
20 converse; antisymmetry is invisible to `quadContr`; the general class is
21 symmetrization modulo `η`; every fixed symmetric stress scalar map
22 instantiates an algebraic null-quadratic class (including
23 `witnessFixedStress` once its
24 `Symmetric4` fact from `HorizonIndexedRecordFlux` is supplied).
25* OPEN: an independently constructed symmetric `G` with Recognition
26 area/focusing ancestry; geometric curvature; continuum Ricci; C-gap1; EFE.
27
28Forbidden shortcuts: no `sorry`, no new axioms, no renaming finite responses
29into Ricci/stress, no `G := T`, no use of a shared MODEL chart as geometric
30ancestry, and no claim that Phase 5 or EFE is closed.
31
32Dependency note: this module imports only `ClausiusEinsteinBridge`. It does
33not pull `HorizonIndexedRecordFlux`, so the witness matrix itself is not
34re-imported here; the fixed-stress instantiation is stated for every
35symmetric `T` with the same scalar map shape as `fixedStressFlux`.
36-/
37
38noncomputable section
39
40namespace IndisputableMonolith
41namespace Gravity
42namespace NullConeQuadraticTensorClass
43
44open ClausiusEinsteinBridge
45open scoped BigOperators
46
47/-! ## Symmetrization -/
48
49/-- Componentwise symmetrization of a real 4×4 matrix. -/
50def symmetrize4 (A : Matrix (Fin 4) (Fin 4) ℝ) : Matrix (Fin 4) (Fin 4) ℝ :=
51 fun i j => (A i j + A j i) / 2
52
53theorem symmetrize4_symmetric (A : Matrix (Fin 4) (Fin 4) ℝ) :
54 Symmetric4 (symmetrize4 A) := by
55 intro i j
56 unfold symmetrize4
57 ring
58
59theorem symmetrize4_of_symmetric
60 (A : Matrix (Fin 4) (Fin 4) ℝ) (hA : Symmetric4 A) :
61 symmetrize4 A = A := by
62 ext i j
63 unfold symmetrize4
64 have := hA i j
65 linarith
66
67/-- Antisymmetric part relative to the transpose. -/
68def antisymmetrize4 (A : Matrix (Fin 4) (Fin 4) ℝ) :
69 Matrix (Fin 4) (Fin 4) ℝ :=
70 fun i j => (A i j - A j i) / 2
71
72private lemma sum_fin_four {α : Type*} [AddCommMonoid α] (f : Fin 4 → α) :
73 ∑ i, f i = f 0 + f 1 + f 2 + f 3 := by
74 have hu : Finset.univ = ({0, 1, 2, 3} : Finset (Fin 4)) := by decide
75 rw [hu]
76 simp
77 abel
78
79/-- Quadratic contraction sees only the symmetric part. -/
80theorem quadContr_eq_quadContr_symmetrize4
81 (A : Matrix (Fin 4) (Fin 4) ℝ) (k : Fin 4 → ℝ) :
82 quadContr A k = quadContr (symmetrize4 A) k := by
83 simp only [quadContr, symmetrize4, sum_fin_four]
84 ring
85
86theorem quadContr_antisymmetrize4_eq_zero
87 (A : Matrix (Fin 4) (Fin 4) ℝ) (k : Fin 4 → ℝ) :
88 quadContr (antisymmetrize4 A) k = 0 := by
89 have hA :
90 A = symmetrize4 A + antisymmetrize4 A := by
91 ext i j
92 simp only [symmetrize4, antisymmetrize4, Matrix.add_apply]
93 ring
94 have hadd :
95 quadContr A k =
96 quadContr (symmetrize4 A) k + quadContr (antisymmetrize4 A) k := by
97 have hcongr := congrArg (fun M => quadContr M k) hA
98 change quadContr A k =
99 quadContr (symmetrize4 A + antisymmetrize4 A) k at hcongr
100 have hsum :
101 quadContr (symmetrize4 A + antisymmetrize4 A) k =
102 quadContr (symmetrize4 A) k +
103 quadContr (antisymmetrize4 A) k := by
104 simp only [quadContr, Matrix.add_apply, add_mul, Finset.sum_add_distrib]
105 exact hcongr.trans hsum
106 linarith [quadContr_eq_quadContr_symmetrize4 A k, hadd]
107
108/-! ## Future nonzero null data determines all null data -/
109
110/-- Quadratic contraction is even in its vector argument. -/
111theorem quadContr_neg
112 (A : Matrix (Fin 4) (Fin 4) ℝ) (k : Fin 4 → ℝ) :
113 quadContr A (-k) = quadContr A k := by
114 unfold quadContr
115 refine Finset.sum_congr rfl fun i _ => ?_
116 refine Finset.sum_congr rfl fun j _ => ?_
117 simp only [Pi.neg_apply]
118 ring
119
120/--
121Agreement on every future nonzero Minkowski-null vector extends to the whole
122null cone. Negative-time vectors are handled by quadratic evenness. A null
123vector with zero time component is the zero vector.
124-/
125theorem all_null_quad_eq_of_future_nonzero_null_quad_eq
126 (A B : Matrix (Fin 4) (Fin 4) ℝ)
127 (hfuture :
128 ∀ k, MinkowskiNull k → k ≠ 0 → 0 < k 0 →
129 quadContr A k = quadContr B k) :
130 ∀ k, MinkowskiNull k → quadContr A k = quadContr B k := by
131 intro k hk
132 by_cases hzero : k = 0
133 · subst k
134 simp [quadContr]
135 have htime : k 0 ≠ 0 := by
136 intro hk0
137 have hkEq := hk
138 unfold MinkowskiNull at hkEq
139 norm_num [hk0] at hkEq
140 have h1 : k 1 = 0 := by
141 nlinarith [sq_nonneg (k 1), sq_nonneg (k 2), sq_nonneg (k 3)]
142 have h2 : k 2 = 0 := by
143 nlinarith [sq_nonneg (k 1), sq_nonneg (k 2), sq_nonneg (k 3)]
144 have h3 : k 3 = 0 := by
145 nlinarith [sq_nonneg (k 1), sq_nonneg (k 2), sq_nonneg (k 3)]
146 apply hzero
147 funext i
148 fin_cases i
149 · exact hk0
150 · exact h1
151 · exact h2
152 · exact h3
153 rcases lt_or_gt_of_ne htime with hneg | hpos
154 · have hkneg : MinkowskiNull (-k) := by
155 simpa [MinkowskiNull] using hk
156 have hnegzero : (-k) ≠ 0 := neg_ne_zero.mpr hzero
157 have hfutureNeg :=
158 hfuture (-k) hkneg hnegzero (by simpa using neg_pos.mpr hneg)
159 simpa only [quadContr_neg] using hfutureNeg
160 · exact hfuture k hk hzero hpos
161
162/-! ## Metric term on the null cone -/
163
164theorem quadContr_smul
165 (c : ℝ) (A : Matrix (Fin 4) (Fin 4) ℝ) (k : Fin 4 → ℝ) :
166 quadContr (c • A) k = c * quadContr A k := by
167 unfold quadContr
168 simp only [Matrix.smul_apply, smul_eq_mul]
169 calc
170 (∑ i, ∑ j, c * A i j * k i * k j)
171 = ∑ i, ∑ j, c * (A i j * k i * k j) := by
172 refine Finset.sum_congr rfl fun i _ =>
173 Finset.sum_congr rfl fun j _ => by ring
174 _ = ∑ i, c * ∑ j, A i j * k i * k j := by
175 refine Finset.sum_congr rfl fun i _ =>
176 (Finset.mul_sum _ _ _).symm
177 _ = c * ∑ i, ∑ j, A i j * k i * k j :=
178 (Finset.mul_sum _ _ _).symm
179
180theorem quadContr_smul_eta
181 (lam : ℝ) (k : Fin 4 → ℝ) :
182 quadContr (lam • minkowskiEta4) k =
183 lam * (-(k 0) ^ 2 + (k 1) ^ 2 + (k 2) ^ 2 + (k 3) ^ 2) := by
184 rw [quadContr_smul, quadContr_minkowskiEta4]
185
186theorem quadContr_smul_eta_of_null
187 (lam : ℝ) (k : Fin 4 → ℝ) (hk : MinkowskiNull k) :
188 quadContr (lam • minkowskiEta4) k = 0 := by
189 rw [quadContr_smul_eta]
190 have hk' :
191 -(k 0) ^ 2 + (k 1) ^ 2 + (k 2) ^ 2 + (k 3) ^ 2 = 0 := by
192 simpa [MinkowskiNull] using hk
193 simp [hk']
194
195/-! ## Core reconstruction (componentwise form) -/
196
197/--
198If a symmetric matrix has vanishing null-cone quadratic form, it is a scalar
199multiple of `η`, stated componentwise.
200-/
201theorem symmetric_null_zero_eq_scalar_eta_components
202 (D : Matrix (Fin 4) (Fin 4) ℝ)
203 (hD : Symmetric4 D)
204 (hnull : ∀ k, MinkowskiNull k → quadContr D k = 0) :
205 ∃ lam : ℝ, ∀ i j, D i j = lam * minkowskiEta4 i j := by
206 obtain ⟨lam, hlam⟩ := null_quadratic_zero_eq_scalar_eta D hD hnull
207 refine ⟨lam, ?_⟩
208 intro i j
209 have hij := congrFun (congrFun hlam i) j
210 simpa [Matrix.smul_apply, smul_eq_mul] using hij
211
212/--
213Null-cone agreement of two symmetric quadratic forms determines their
214difference as a scalar multiple of the Minkowski metric.
215-/
216theorem null_quadratic_eq_implies_diff_scalar_eta
217 (A B : Matrix (Fin 4) (Fin 4) ℝ)
218 (hA : Symmetric4 A)
219 (hB : Symmetric4 B)
220 (hnull : ∀ k, MinkowskiNull k → quadContr A k = quadContr B k) :
221 ∃ lam : ℝ, ∀ i j, A i j - B i j = lam * minkowskiEta4 i j := by
222 obtain ⟨lam, hlam⟩ := null_quadratic_eq_of_diff_scalar_eta A B hA hB hnull
223 refine ⟨lam, ?_⟩
224 intro i j
225 have hij := congrFun (congrFun hlam i) j
226 -- `A = B + lam • η` at `(i,j)`.
227 change A i j = B i j + (lam • minkowskiEta4) i j at hij
228 simp only [Matrix.smul_apply, smul_eq_mul] at hij
229 linarith
230
231/--
232Future nonzero null agreement is sufficient for the symmetric rigidity
233conclusion. This is the algebraic handoff from future-section data; it does
234not supply the independently constructed `G` required by Phase 5.
235-/
236theorem future_null_quadratic_eq_implies_diff_scalar_eta
237 (A B : Matrix (Fin 4) (Fin 4) ℝ)
238 (hA : Symmetric4 A)
239 (hB : Symmetric4 B)
240 (hfuture :
241 ∀ k, MinkowskiNull k → k ≠ 0 → 0 < k 0 →
242 quadContr A k = quadContr B k) :
243 ∃ lam : ℝ, ∀ i j, A i j - B i j = lam * minkowskiEta4 i j := by
244 apply null_quadratic_eq_implies_diff_scalar_eta A B hA hB
245 exact all_null_quad_eq_of_future_nonzero_null_quad_eq A B hfuture
246
247/-- Converse: a pure metric difference is invisible on the null cone. -/
248theorem diff_scalar_eta_implies_null_quadratic_eq
249 (A B : Matrix (Fin 4) (Fin 4) ℝ) (lam : ℝ)
250 (hlam : ∀ i j, A i j - B i j = lam * minkowskiEta4 i j) :
251 ∀ k, MinkowskiNull k → quadContr A k = quadContr B k := by
252 intro k hk
253 have hAB : A = B + lam • minkowskiEta4 := by
254 ext i j
255 have hij := hlam i j
256 simp only [Matrix.add_apply, Matrix.smul_apply, smul_eq_mul]
257 linarith
258 have hcontr := congrArg (fun M => quadContr M k) hAB
259 change quadContr A k = quadContr (B + lam • minkowskiEta4) k at hcontr
260 have hadd :
261 quadContr (B + lam • minkowskiEta4) k =
262 quadContr B k + quadContr (lam • minkowskiEta4) k := by
263 simp only [quadContr, Matrix.add_apply, add_mul, Finset.sum_add_distrib]
264 rw [hadd, quadContr_smul_eta_of_null lam k hk, add_zero] at hcontr
265 exact hcontr
266
267/-- Biconditional for symmetric matrices. -/
268theorem null_quadratic_eq_iff_diff_scalar_eta
269 (A B : Matrix (Fin 4) (Fin 4) ℝ)
270 (hA : Symmetric4 A)
271 (hB : Symmetric4 B) :
272 (∀ k, MinkowskiNull k → quadContr A k = quadContr B k) ↔
273 ∃ lam : ℝ, ∀ i j, A i j - B i j = lam * minkowskiEta4 i j := by
274 constructor
275 · exact null_quadratic_eq_implies_diff_scalar_eta A B hA hB
276 · intro h
277 obtain ⟨lam, hlam⟩ := h
278 exact diff_scalar_eta_implies_null_quadratic_eq A B lam hlam
279
280/-! ## General (not necessarily symmetric) matrices -/
281
282/--
283For general matrices, null-cone quadratic data determines the symmetrization
284modulo `η`. Antisymmetric parts are invisible.
285-/
286theorem null_quadratic_eq_iff_symmetrize_diff_scalar_eta
287 (A B : Matrix (Fin 4) (Fin 4) ℝ) :
288 (∀ k, MinkowskiNull k → quadContr A k = quadContr B k) ↔
289 ∃ lam : ℝ, ∀ i j,
290 symmetrize4 A i j - symmetrize4 B i j = lam * minkowskiEta4 i j := by
291 constructor
292 · intro hnull
293 have hsym :
294 ∀ k, MinkowskiNull k →
295 quadContr (symmetrize4 A) k = quadContr (symmetrize4 B) k := by
296 intro k hk
297 rw [← quadContr_eq_quadContr_symmetrize4 A k,
298 ← quadContr_eq_quadContr_symmetrize4 B k]
299 exact hnull k hk
300 exact null_quadratic_eq_implies_diff_scalar_eta
301 (symmetrize4 A) (symmetrize4 B)
302 (symmetrize4_symmetric A) (symmetrize4_symmetric B) hsym
303 · intro h
304 obtain ⟨lam, hlam⟩ := h
305 intro k hk
306 have hsymEq :=
307 diff_scalar_eta_implies_null_quadratic_eq
308 (symmetrize4 A) (symmetrize4 B) lam hlam k hk
309 rw [quadContr_eq_quadContr_symmetrize4 A k,
310 quadContr_eq_quadContr_symmetrize4 B k, hsymEq]
311
312/-! ## Algebraic null-quadratic class interface -/
313
314/--
315Null-cone equivalence of two matrices: they induce the same quadratic
316scalar on every Minkowski-null covector.
317-/
318def NullConeEquivalent
319 (A B : Matrix (Fin 4) (Fin 4) ℝ) : Prop :=
320 ∀ k, MinkowskiNull k → quadContr A k = quadContr B k
321
322theorem NullConeEquivalent.refl (A : Matrix (Fin 4) (Fin 4) ℝ) :
323 NullConeEquivalent A A := by
324 intro _ _
325 rfl
326
327theorem NullConeEquivalent.symm
328 {A B : Matrix (Fin 4) (Fin 4) ℝ}
329 (h : NullConeEquivalent A B) :
330 NullConeEquivalent B A := by
331 intro k hk
332 exact (h k hk).symm
333
334theorem NullConeEquivalent.trans
335 {A B C : Matrix (Fin 4) (Fin 4) ℝ}
336 (hAB : NullConeEquivalent A B) (hBC : NullConeEquivalent B C) :
337 NullConeEquivalent A C := by
338 intro k hk
339 exact (hAB k hk).trans (hBC k hk)
340
341/--
342A scalar map `φ` on covectors determines a unique symmetric matrix class
343modulo `η` when it arises as a null-cone quadratic form.
344This is only an algebraic equivalence class, theorem-backed without a quotient
345type. It supplies no geometric ancestry.
346-/
347def DeterminesAlgebraicNullQuadraticClass
348 (φ : (Fin 4 → ℝ) → ℝ)
349 (A : Matrix (Fin 4) (Fin 4) ℝ) : Prop :=
350 Symmetric4 A ∧
351 (∀ k, MinkowskiNull k → φ k = quadContr A k) ∧
352 (∀ B : Matrix (Fin 4) (Fin 4) ℝ,
353 Symmetric4 B →
354 (∀ k, MinkowskiNull k → φ k = quadContr B k) →
355 ∃ lam : ℝ, ∀ i j, A i j - B i j = lam * minkowskiEta4 i j)
356
357/-- Every symmetric matrix determines its algebraic null-quadratic class. -/
358theorem determinesAlgebraicNullQuadraticClass_quadContr
359 (A : Matrix (Fin 4) (Fin 4) ℝ) (hA : Symmetric4 A) :
360 DeterminesAlgebraicNullQuadraticClass (quadContr A) A := by
361 refine ⟨hA, fun _ _ => rfl, ?_⟩
362 intro B hB hφ
363 exact null_quadratic_eq_implies_diff_scalar_eta A B hA hB hφ
364
365/--
366Adding a metric multiple does not change the algebraic null-quadratic class of a
367symmetric representative.
368-/
369theorem determinesAlgebraicNullQuadraticClass_add_eta
370 (A : Matrix (Fin 4) (Fin 4) ℝ) (hA : Symmetric4 A) (lam : ℝ) :
371 DeterminesAlgebraicNullQuadraticClass (quadContr A)
372 (A + lam • minkowskiEta4) := by
373 have hSym : Symmetric4 (A + lam • minkowskiEta4) := by
374 intro i j
375 simp only [Matrix.add_apply, Matrix.smul_apply, smul_eq_mul]
376 rw [hA i j]
377 have hη : minkowskiEta4 i j = minkowskiEta4 j i := by
378 simp only [minkowskiEta4]
379 by_cases hij : i = j
380 · subst j; simp
381 · have hji : j ≠ i := fun h => hij h.symm
382 simp [hij, hji]
383 rw [hη]
384 have hφ :
385 ∀ k, MinkowskiNull k →
386 quadContr A k = quadContr (A + lam • minkowskiEta4) k := by
387 intro k hk
388 have hadd :
389 quadContr (A + lam • minkowskiEta4) k =
390 quadContr A k + quadContr (lam • minkowskiEta4) k := by
391 simp only [quadContr, Matrix.add_apply, add_mul, Finset.sum_add_distrib]
392 rw [hadd, quadContr_smul_eta_of_null lam k hk, add_zero]
393 refine ⟨hSym, hφ, ?_⟩
394 intro B hB hBφ
395 have hnull :
396 ∀ k, MinkowskiNull k →
397 quadContr (A + lam • minkowskiEta4) k = quadContr B k := by
398 intro k hk
399 exact (hφ k hk).symm.trans (hBφ k hk)
400 exact null_quadratic_eq_implies_diff_scalar_eta
401 (A + lam • minkowskiEta4) B hSym hB hnull
402
403/-! ## Fixed-stress scalar-map instantiation -/
404
405/--
406Direction-indexed flux of a fixed stress matrix. Matches the
407`fixedStressFlux` packaging in `HorizonIndexedRecordFlux` (definitionally
408`quadContr`), kept local so this module stays free of that heavy import.
409-/
410def fixedStressFlux
411 (T : Matrix (Fin 4) (Fin 4) ℝ)
412 (k : Fin 4 → ℝ) : ℝ :=
413 quadContr T k
414
415/--
416Any fixed symmetric stress scalar map determines its algebraic
417null-quadratic class modulo `η`. Specializes immediately to
418`HorizonIndexedRecordFlux.witnessFixedStress` once `Symmetric4` is known.
419This statement supplies no independently geometric `G`.
420-/
421theorem fixedSymmetricStress_determinesAlgebraicNullQuadraticClass
422 (T : Matrix (Fin 4) (Fin 4) ℝ) (hT : Symmetric4 T) :
423 DeterminesAlgebraicNullQuadraticClass (fixedStressFlux T) T := by
424 simpa [fixedStressFlux] using
425 determinesAlgebraicNullQuadraticClass_quadContr T hT
426
427theorem fixedSymmetricStress_null_class_unique
428 (T B : Matrix (Fin 4) (Fin 4) ℝ)
429 (hT : Symmetric4 T) (hB : Symmetric4 B)
430 (hnull :
431 ∀ k, MinkowskiNull k →
432 fixedStressFlux T k = fixedStressFlux B k) :
433 ∃ lam : ℝ, ∀ i j, T i j - B i j = lam * minkowskiEta4 i j :=
434 null_quadratic_eq_implies_diff_scalar_eta T B hT hB hnull
435
436/-!
437## OPEN Phase 5 residual
438
439The remaining Phase 5 object is an independently constructed symmetric matrix
440`G` whose entries descend from Recognition area/focusing ancestry, together
441with a proved future-null quadratic comparison to the relevant scalar data.
442The theorem `future_null_quadratic_eq_implies_diff_scalar_eta` would then
443identify its algebraic class modulo `η`. This module intentionally defines no
444Prop that pretends to encode "independently constructed": that requirement must
445be discharged by the actual construction and its dependency graph. Taking
446`G := T` or reusing the shared MODEL chart is forbidden and leaves Tier A OPEN.
447-/
448
449/-! ## Certificate -/
450
451/--
452Certificate for the Phase-5 algebraic prerequisite. It records rigidity and
453future-to-all extension only. It does not contain or claim the independently
454geometric `G`, Ricci identification, Unruh, C-gap1, Tier A, or EFE closure.
455-/
456structure NullConeQuadraticTensorClassCert : Prop where
457 future_to_all :
458 ∀ (A B : Matrix (Fin 4) (Fin 4) ℝ),
459 (∀ k, MinkowskiNull k → k ≠ 0 → 0 < k 0 →
460 quadContr A k = quadContr B k) →
461 ∀ k, MinkowskiNull k → quadContr A k = quadContr B k
462 reconstruction :
463 ∀ (A B : Matrix (Fin 4) (Fin 4) ℝ),
464 Symmetric4 A → Symmetric4 B →
465 (∀ k, MinkowskiNull k → quadContr A k = quadContr B k) →
466 ∃ lam : ℝ, ∀ i j, A i j - B i j = lam * minkowskiEta4 i j
467 converse :
468 ∀ (A B : Matrix (Fin 4) (Fin 4) ℝ) (lam : ℝ),
469 (∀ i j, A i j - B i j = lam * minkowskiEta4 i j) →
470 ∀ k, MinkowskiNull k → quadContr A k = quadContr B k
471 antisym_invisible :
472 ∀ (A : Matrix (Fin 4) (Fin 4) ℝ) (k : Fin 4 → ℝ),
473 quadContr A k = quadContr (symmetrize4 A) k
474 general_class :
475 ∀ (A B : Matrix (Fin 4) (Fin 4) ℝ),
476 (∀ k, MinkowskiNull k → quadContr A k = quadContr B k) ↔
477 ∃ lam : ℝ, ∀ i j,
478 symmetrize4 A i j - symmetrize4 B i j = lam * minkowskiEta4 i j
479 fixed_stress_algebraic_class :
480 ∀ (T : Matrix (Fin 4) (Fin 4) ℝ),
481 Symmetric4 T →
482 DeterminesAlgebraicNullQuadraticClass (fixedStressFlux T) T
483
484theorem nullConeQuadraticTensorClassCert :
485 NullConeQuadraticTensorClassCert where
486 future_to_all := all_null_quad_eq_of_future_nonzero_null_quad_eq
487 reconstruction := null_quadratic_eq_implies_diff_scalar_eta
488 converse := diff_scalar_eta_implies_null_quadratic_eq
489 antisym_invisible := quadContr_eq_quadContr_symmetrize4
490 general_class := null_quadratic_eq_iff_symmetrize_diff_scalar_eta
491 fixed_stress_algebraic_class :=
492 fixedSymmetricStress_determinesAlgebraicNullQuadraticClass
493
494end NullConeQuadraticTensorClass
495end Gravity
496end IndisputableMonolith
497