IndisputableMonolith.Gravity.Analysis.EHSecondVariationExact4DAudit

   1import IndisputableMonolith.Gravity.Analysis.EHSecondVariationExact4D
   2
   3/-!
   4# Axiom audit for `EHSecondVariationExact4D`
   5
   6Every named result, one `#print axioms` each.  Expected footprint for all of them
   7is `[propext, Classical.choice, Quot.sound]`, and the base-triple reading is a
   8claim about postulates only: the ambient theory still supplies the universe
   9hierarchy, inductive types, function types, equality and definitional reduction.
  10
  11Check the output with a parser that joins wrapped lines
  12(`holography/scratch/audit_check.py`), because long axiom lists wrap.
  13-/
  14
  15namespace IndisputableMonolith
  16namespace Gravity
  17namespace Analysis
  18namespace EHSecondVariationExact4DAudit
  19
  20open EHSecondVariationExact4D
  21
  22#print axioms phaseAverage_const
  23#print axioms phaseAverage_sin_sq
  24#print axioms phaseAverage_sin_sq_affine
  25#print axioms exactDensityTT_average
  26#print axioms exactDensityTrace_average
  27#print axioms exactDensityLongitudinal_average
  28#print axioms exact_average_eq_ehFace
  29#print axioms a3_agrees_with_exact
  30#print axioms trace_decoy_misses_the_face
  31#print axioms longitudinal_decoy_misses_the_face
  32#print axioms exact_density_rigid
  33
  34end EHSecondVariationExact4DAudit
  35end Analysis
  36end Gravity
  37end IndisputableMonolith
  38