IndisputableMonolith.Gravity.SevenGaps.HKTCanonicalMomRigidityPDEAudit

   1import IndisputableMonolith.Gravity.SevenGaps.HKTCanonicalMomRigidityPDE
   2
   3open IndisputableMonolith.Gravity.SevenGaps.HKTCanonicalMomRigidity
   4open IndisputableMonolith.Gravity.SevenGaps.HKTCanonicalMomTarget
   5open IndisputableMonolith.Gravity.SevenGaps.FullTheoryLedger
   6
   7#check LocalHamSmoothContDiff2Obligation
   8#check sqrtAffineProfile_contDiff2
   9#check not_forced_linear_hp_of_contDiff2_FE
  10#check not_forced_hb_p_independent_of_contDiff2_FE
  11#check ConstantKineticSlope
  12#check hb_shape_of_constant_kinetic_slope
  13#check ADM_quadratic_of_gauges
  14#check HKTRigidityPointSplitDynN2Canonical_smooth
  15#check hamDynLocalProfile_contDiff2
  16#check hamDyn_smooth_scoped_rigidity
  17#check SolveProfileFEQuadratic_of_smoothScopedData
  18#check hktCanonicalMomRigidityC2Status_flags
  19
  20#print axioms sqrtAffineProfile_contDiff2
  21#print axioms not_forced_linear_hp_of_contDiff2_FE
  22#print axioms HKTRigidityPointSplitDynN2Canonical_smooth
  23#print axioms hamDyn_smooth_scoped_rigidity
  24#print axioms SolveProfileFEQuadratic_of_smoothScopedData
  25#print axioms hktCanonicalMomRigidityC2Status_flags
  26
  27example : fullTheoryBenchmarks.gap5_constraint_recovery = true := rfl
  28example : hktCanonicalMomRigidityC2Status.pdeLemmaClosed = false := rfl
  29example : hktCanonicalMomRigidityC2Status.smoothScopedRigidityClosed = true := rfl
  30example : hktCanonicalMomRigidityC2Status.gap5ConstraintRecovery = false := rfl
  31
  32-- Unconditioned rigidity remains a Prop (not claimed as a universal theorem).
  33#check HKTRigidityStatementPointSplitDynN2Canonical
  34#check solve_profile_FE_quadratic
  35