IndisputableMonolith.Gravity.SevenGaps.HKTKineticNormalizedRigidityAudit

   1import IndisputableMonolith.Gravity.SevenGaps.HKTKineticNormalizedRigidity
   2
   3open IndisputableMonolith.Gravity.SevenGaps.HKTKineticNormalizedRigidity
   4open IndisputableMonolith.Gravity.SevenGaps.HKTVacuumSectorKill
   5open IndisputableMonolith.Gravity.SevenGaps.FullTheoryLedger
   6
   7#check vacuumKineticCanonicalMomTarget
   8#check not_HKTRigidityModVacuumStatementN2
   9#check KineticNormalizedCanonicalMom
  10#check ftc_recovery_of_normalized
  11#check HKTRigidityKineticNormalizedN2_holds
  12#check hamDynKineticNormalized
  13#check hamDyn_satisfies_kineticNormalized
  14#check vacuumKinetic_not_kineticNormalized
  15#check hktKineticNormalizedRigidityStatus_flags
  16
  17#print axioms not_HKTRigidityModVacuumStatementN2
  18#print axioms ftc_recovery_of_normalized
  19#print axioms HKTRigidityKineticNormalizedN2_holds
  20#print axioms hamDyn_satisfies_kineticNormalized
  21#print axioms vacuumKinetic_not_kineticNormalized
  22#print axioms kinetic_split_of_intensivity
  23#print axioms gradient_recovery_of_intensivity
  24
  25example : fullTheoryBenchmarks.gap5_constraint_recovery = true := rfl
  26example : hktKineticNormalizedRigidityStatus.modVacuumRigidityKilled = true := rfl
  27example : hktKineticNormalizedRigidityStatus.kineticNormalizedRigidityClosed = true := rfl
  28example : hktKineticNormalizedRigidityStatus.ftcRecoveryDerived = true := rfl
  29example : hktVacuumSectorKillStatus.modVacuumRigidityOpen = false := rfl
  30