IndisputableMonolith.Gravity.Analysis.ReggeNormalizationDerived4DAudit

   1import IndisputableMonolith.Gravity.Analysis.ContinuumTTSecondVariation4D
   2import IndisputableMonolith.Gravity.Analysis.ReggeNormalizationDerived4D
   3
   4/-!
   5# Axiom audit: arc 2 step 7
   6
   7Every named theorem of `ContinuumTTSecondVariation4D` (the continuum derivation)
   8and `ReggeNormalizationDerived4D` (the comparison and the pinning of Regge's
   9constant) must report exactly `[propext, Classical.choice, Quot.sound]`.
  10
  11The banked dictionary identity this step compares against is audited here too,
  12so a reader can see the whole chain in one log.
  13
  14Reminder (`institute-identity.mdc`): the base triple is a claim about postulates,
  15not about prior structure.  The ambient theory still supplies the universe
  16hierarchy, inductive types, recursors, function types, definitional equality, and
  17`Decidable` instances.
  18-/
  19
  20namespace IndisputableMonolith.Gravity.Analysis.ReggeNormalizationDerived4DAudit
  21
  22open ContinuumTTSecondVariation4D
  23open ReggeNormalizationDerived4D
  24
  25/-! ## §1. The continuum derivation -/
  26
  27#print axioms ContinuumTTSecondVariation4D.phase_update
  28#print axioms ContinuumTTSecondVariation4D.hasDerivAt_phase_update
  29#print axioms ContinuumTTSecondVariation4D.phase_update_self
  30#print axioms ContinuumTTSecondVariation4D.pd_cos
  31#print axioms ContinuumTTSecondVariation4D.pd_sin
  32#print axioms ContinuumTTSecondVariation4D.linChristoffel_eq
  33#print axioms ContinuumTTSecondVariation4D.linRicci_eq
  34#print axioms ContinuumTTSecondVariation4D.sum_k_mul_row
  35#print axioms ContinuumTTSecondVariation4D.sum_k_chrAmp
  36#print axioms ContinuumTTSecondVariation4D.sum_chrAmp_trace
  37#print axioms ContinuumTTSecondVariation4D.ricciAmp_tt
  38#print axioms ContinuumTTSecondVariation4D.linRicci_tt
  39#print axioms ContinuumTTSecondVariation4D.linRicciScalar_tt
  40#print axioms ContinuumTTSecondVariation4D.linEinstein_tt
  41#print axioms ContinuumTTSecondVariation4D.ehSecondVariationDensity_tt
  42#print axioms ContinuumTTSecondVariation4D.phaseAverage_const_mul
  43#print axioms ContinuumTTSecondVariation4D.phaseAverage_cos_sq
  44#print axioms ContinuumTTSecondVariation4D.density_factors_through_phase
  45#print axioms ContinuumTTSecondVariation4D.ehFace_eq_phaseAverage
  46#print axioms ContinuumTTSecondVariation4D.ehFace_eq_average_of_density
  47#print axioms ContinuumTTSecondVariation4D.ehFace_rigid
  48
  49/-! ## §2. The comparison, the pinning, and the discrimination -/
  50
  51#print axioms ReggeNormalizationDerived4D.frobSq_eq
  52#print axioms ReggeNormalizationDerived4D.momentumSq_eq
  53#print axioms ReggeNormalizationDerived4D.reggeFace_eq
  54#print axioms ReggeNormalizationDerived4D.reggeFace_eq_dictionary
  55#print axioms ReggeNormalizationDerived4D.regge_normalization_pinned
  56#print axioms ReggeNormalizationDerived4D.frobeniusNormSq_axisTTPlus
  57#print axioms ReggeNormalizationDerived4D.waveNormSq_axisWave
  58#print axioms ReggeNormalizationDerived4D.witness_nonzero
  59#print axioms ReggeNormalizationDerived4D.dictionary_witness_value
  60#print axioms ReggeNormalizationDerived4D.rho_one_fails
  61#print axioms ReggeNormalizationDerived4D.rho_pinned_at_witness
  62
  63/-! ## §3. A4 checked in two dimensions -/
  64
  65#print axioms ReggeNormalizationDerived4D.tetrahedron_deficit_sum
  66#print axioms ReggeNormalizationDerived4D.octahedron_deficit_sum
  67#print axioms ReggeNormalizationDerived4D.regge_constant_from_gauss_bonnet
  68#print axioms ReggeNormalizationDerived4D.gauss_bonnet_refutes_rho_one
  69
  70/-! ## §4. The second route -/
  71
  72#print axioms ReggeNormalizationDerived4D.phaseAverage_sin_sq
  73#print axioms ReggeNormalizationDerived4D.lagrangian_route_same_face
  74#print axioms ReggeNormalizationDerived4D.two_routes_differ_pointwise
  75
  76/-! ## §5. What the tree's constants are -/
  77
  78#print axioms ReggeNormalizationDerived4D.discreteBookkeepingFactor_is_inverse_regge
  79#print axioms ReggeNormalizationDerived4D.frozen_preflight_is_the_eh_integral_face
  80#print axioms ReggeNormalizationDerived4D.exact_unit_coefficient_is_the_regge_face
  81
  82/-! ## §6. The composite certificate and the discriminating gate -/
  83
  84#print axioms ReggeNormalizationDerived4D.normalizationGateDischarged
  85#print axioms ReggeNormalizationDerived4D.step7Cert
  86
  87/-! ## §7. The banked identity being compared against -/
  88
  89#print axioms
  90  IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4D.exactMidpointBlochM2_eq_neg_eighth_frobenius_tt
  91
  92end IndisputableMonolith.Gravity.Analysis.ReggeNormalizationDerived4DAudit
  93