IndisputableMonolith.Gravity.SevenGaps.HKTCanonicalMomRigidityAudit

   1import IndisputableMonolith.Gravity.SevenGaps.HKTCanonicalMomRigidity
   2
   3open IndisputableMonolith.Gravity.SevenGaps.HKTCanonicalMomRigidity
   4open IndisputableMonolith.Gravity.SevenGaps.HKTCanonicalMomTarget
   5open IndisputableMonolith.Gravity.SevenGaps.FullTheoryLedger
   6
   7#check profiled_ham_ham_alternating_FE
   8#check fe_at_r_zero
   9#check fe_at_p_zero
  10#check HpLinearInP
  11#check HbPIndependent
  12#check LocalHamSmoothContDiff2Obligation
  13#check hb_coupling_of_linear_ansatz
  14#check SolveProfileFEQuadratic
  15#check solve_profile_FE_quadratic
  16#check hamDyn_solve_profile_FE_quadratic
  17#check canonicalMom_rigidity_of_FE_solution
  18#check HKTRigidityStatementPointSplitDynN2Canonical_of_solve
  19#check hamDyn_canonicalMom_rigidity_conclusion
  20#check hktCanonicalMomRigidityC1Status_flags
  21
  22#print axioms profiled_ham_ham_alternating_FE
  23#print axioms fe_at_r_zero
  24#print axioms hb_coupling_of_linear_ansatz
  25#print axioms canonicalMom_rigidity_of_FE_solution
  26#print axioms HKTRigidityStatementPointSplitDynN2Canonical_of_solve
  27#print axioms hamDyn_solve_profile_FE_quadratic
  28#print axioms hamDyn_canonicalMom_rigidity_conclusion
  29#print axioms hktCanonicalMomRigidityC1Status_flags
  30
  31example : fullTheoryBenchmarks.gap5_constraint_recovery = true := rfl
  32example : hktCanonicalMomRigidityC1Status.feExtractionClosed = true := rfl
  33example : hktCanonicalMomRigidityC1Status.pdeLemmaClosed = false := rfl
  34example : hktCanonicalMomRigidityC1Status.gap5ConstraintRecovery = false := rfl
  35
  36-- Rigidity statement remains a Prop (not claimed as a theorem this session).
  37#check HKTRigidityStatementPointSplitDynN2Canonical
  38