IndisputableMonolith.Gravity.SevenGaps.HKTKineticFromRecognitionCost · Recognition explainer

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.SevenGaps.Gap5ReparamAttackOnConstraintSector module_import
IndisputableMonolith.Gravity.SevenGaps.HKTKineticFromRecognitionCostAudit module_import

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost.Convexity module_import
IndisputableMonolith.Cost.FunctionalEquation module_import
IndisputableMonolith.Cost.SymplecticAction module_import
IndisputableMonolith.Gravity.SevenGaps.HKTKineticNormalizedRigidity module_import

declarations in this module (68)

structure UniversalKineticCanonicalMom L157
theorem exists_structure_value_ne_zero L171
structure function L184
theorem kinetic_normalization_of_universal_response L191
theorem kinetic_coefficient_unique L228
theorem HKTRigidityUniversalKineticN2_holds L260
def ChannelSeparated L286
theorem universal_of_channelSeparated L290
theorem channelSeparated_of_universal L307
def costKineticProfile L337
structure CostKineticCanonicalMom L341
theorem costKinetic_hp_eq_sinh L352
theorem costKinetic_universal L373
theorem one_lt_cosh_one L382
theorem sinh_one_pos L388
theorem sinh_not_linear L396
theorem no_exact_cost_kinetic_canonicalMom L420
def recogCurvature L445
theorem recogCurvature_eq_one L447
def JlogQuad L451
theorem JlogQuad_eq_half_sq L453
theorem deriv_Jlog_eq_sinh L456
theorem deriv2_Jlog_zero_eq_recogCurvature L461
theorem hasDerivAt_JlogQuad L465
theorem deriv_JlogQuad_eq L474
theorem JlogQuad_matches_Jlog_to_second_order L479
def quadCostKineticProfile L498
structure QuadCostKineticCanonicalMom L502
theorem quadCost_hp_eq_linear L520
theorem quadCost_cKin_ne_zero L540
theorem quadCost_ADM_rigidity L560
theorem vacuumKinetic_not_universalKinetic L584
def hamDynUniversalKinetic L591
theorem hamDyn_satisfies_universalKinetic L594
def jetCost L647
theorem G_jetCost L649
theorem deriv_half_sq L654
theorem deriv_linear_zero L663
theorem isCalibrated_jetCost_iff L673
theorem G_jetCost_recogCurvature L684
def perSiteJetProfile L694
theorem isCalibrated_iff_density_curvature L701
structure CalibratedJetCanonicalMom L721
theorem calibratedJet_hp_eq_linear L735
theorem calibratedJet_cKin_ne_zero L759
theorem calibratedJet_ADM_rigidity L774
def hamDynCalibratedJet L794
theorem hamDyn_satisfies_calibratedJet L809
theorem vacuumKineticLocalProfile_eq_perSiteJet L834
theorem vacuumKinetic_jet_not_calibrated L844
theorem vacuumKinetic_not_calibratedJet L856
theorem compositionLaw_forces_unit_weight L872
theorem rcl_forces_field_independent_weight L888
theorem Jlog_two_arsinh L942
def exactCostKineticProfile L951
theorem exactCostKineticProfile_quadratic L955
structure RCLKineticCanonicalMom L964
theorem rclKinetic_hp_eq_linear L979
theorem rclKinetic_cKin_pos L1006
theorem rclKinetic_cKin_ne_zero L1011
theorem rclKinetic_ADM_rigidity L1023
theorem rclKinetic_positive_kinetic_coefficient L1041
def hamDynRCLKinetic L1059
theorem hamDyn_satisfies_rclKinetic L1076
theorem vacuumKineticLocalProfile_eq_exactCost L1098
theorem vacuumKinetic_weight_not_rcl L1109
theorem no_rcl_presentation_of_vacuumKinetic L1121
theorem jetCost_not_rcl L1157