IndisputableMonolith.Gravity.SevenGaps.HKTKineticFromRecognitionCostAudit

   1import IndisputableMonolith.Gravity.SevenGaps.HKTKineticFromRecognitionCost
   2
   3/-!
   4# Axiom audit: constraint-sector recognition premise
   5
   6Every declaration cited in the paper
   7`papers/QG_Constraint_Sector_Recognition_Premise_20260725.tex` must print
   8within `[propext, Classical.choice, Quot.sound]`.
   9
  10The retained-failure declarations of §7 are audited too. They are cited in the
  11paper as proved defects, so their axiom cleanliness is load-bearing in exactly
  12the same way as the positive results.
  13-/
  14
  15open IndisputableMonolith.Gravity.SevenGaps
  16open IndisputableMonolith.Gravity.SevenGaps.HKTKineticFromRecognitionCost
  17
  18/-! ## §2 and §3: half the premise was never an assumption -/
  19
  20#check kinetic_normalization_of_universal_response
  21#check kinetic_coefficient_unique
  22#check HKTRigidityUniversalKineticN2_holds
  23#check universal_of_channelSeparated
  24#check channelSeparated_of_universal
  25
  26#print axioms kinetic_normalization_of_universal_response
  27#print axioms kinetic_coefficient_unique
  28#print axioms HKTRigidityUniversalKineticN2_holds
  29#print axioms universal_of_channelSeparated
  30#print axioms channelSeparated_of_universal
  31
  32/-! ## §4: scope of the linear-chart exclusion -/
  33
  34#check costKinetic_hp_eq_sinh
  35#check sinh_not_linear
  36#check no_exact_cost_kinetic_canonicalMom
  37
  38#print axioms costKinetic_hp_eq_sinh
  39#print axioms sinh_not_linear
  40#print axioms no_exact_cost_kinetic_canonicalMom
  41
  42/-! ## §6: the enlarged class is not empty -/
  43
  44#check vacuumKinetic_not_universalKinetic
  45#check hamDyn_satisfies_universalKinetic
  46
  47#print axioms vacuumKinetic_not_universalKinetic
  48#print axioms hamDyn_satisfies_universalKinetic
  49
  50/-! ## §7: the retained failure, with its defects -/
  51
  52#check isCalibrated_jetCost_iff
  53#check jetCost_not_rcl
  54
  55#print axioms isCalibrated_jetCost_iff
  56#print axioms jetCost_not_rcl
  57
  58/-! ## §8: the composition law carries the premise -/
  59
  60#check compositionLaw_forces_unit_weight
  61#check rcl_forces_field_independent_weight
  62#check Jlog_two_arsinh
  63#check exactCostKineticProfile_quadratic
  64#check rclKinetic_hp_eq_linear
  65#check rclKinetic_cKin_pos
  66#check rclKinetic_cKin_ne_zero
  67#check rclKinetic_ADM_rigidity
  68#check rclKinetic_positive_kinetic_coefficient
  69#check hamDyn_satisfies_rclKinetic
  70#check vacuumKineticLocalProfile_eq_exactCost
  71#check vacuumKinetic_weight_not_rcl
  72#check no_rcl_presentation_of_vacuumKinetic
  73
  74#print axioms compositionLaw_forces_unit_weight
  75#print axioms rcl_forces_field_independent_weight
  76#print axioms Jlog_two_arsinh
  77#print axioms exactCostKineticProfile_quadratic
  78#print axioms rclKinetic_hp_eq_linear
  79#print axioms rclKinetic_cKin_pos
  80#print axioms rclKinetic_cKin_ne_zero
  81#print axioms rclKinetic_ADM_rigidity
  82#print axioms rclKinetic_positive_kinetic_coefficient
  83#print axioms hamDyn_satisfies_rclKinetic
  84#print axioms vacuumKineticLocalProfile_eq_exactCost
  85#print axioms vacuumKinetic_weight_not_rcl
  86#print axioms no_rcl_presentation_of_vacuumKinetic
  87