IndisputableMonolith.Gravity.Analysis.SRSTTFirstVariation4DAudit

   1import IndisputableMonolith.Gravity.Analysis.SRSTTFirstVariation4D
   2
   3/-!
   4# Audit: SRSTTFirstVariation4D
   5
   6Public axiom audit for the Euclidean weak-field TT midpoint first-variation
   7increment. Expected: clean triple
   8`[propext, Classical.choice, Quot.sound]` on the headline, key derivatives,
   9and packaged certificate.
  10-/
  11
  12open IndisputableMonolith.Gravity.Analysis.SRSTTFirstVariation4D
  13
  14#check frobeniusPairing4D
  15#check exactMidpointBlochFirstVariation
  16#check exactMidpointBlochSymbol_line
  17#check hasDerivAt_exactMidpointBlochSymbol_line
  18#check exactMidpointBlochFirstVariation_polarization
  19#check continuumFace_polarization_eq_neg_quarter_frobenius
  20#check hasDerivAt_finiteExactMidpointBlochSymbol_normalized
  21#check continuumTTFirstVariation_closed
  22#check srsTTFirstVariation4D_cert
  23
  24#print axioms hasDerivAt_exactMidpointBlochSymbol_line
  25#print axioms exactMidpointBlochFirstVariation_polarization
  26#print axioms continuumFace_polarization_eq_neg_quarter_frobenius
  27#print axioms hasDerivAt_finiteExactMidpointBlochSymbol_normalized
  28#print axioms continuumTTFirstVariation_closed
  29#print axioms srsTTFirstVariation4D_cert
  30