IndisputableMonolith.Gravity.SevenGaps.HKTKineticNormalizedRigidity · Recognition explainer

used by (3)

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

IndisputableMonolith.Gravity.SevenGaps.Gap5ConstraintCloseStatus module_import
IndisputableMonolith.Gravity.SevenGaps.HKTKineticFromRecognitionCost module_import
IndisputableMonolith.Gravity.SevenGaps.HKTKineticNormalizedRigidityAudit module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.HKTCanonicalMomRigidityPDE module_import
IndisputableMonolith.Gravity.SevenGaps.HKTVacuumSectorKill module_import

declarations in this module (85)

lemma zmod2_zero_add_one L36
lemma zmod2_one_add_one L37
lemma zmod2_zero_add_two L38
lemma zmod2_one_add_two L39
def vacuumKineticA L43
def vacuumKineticW L45
def vacuumKineticK L50
theorem vacuumKineticW_eq_design L54
def vacuumKineticLocalProfile L59
def vacuumKineticHamDensity L62
theorem one_add_sq_ne_zero L65
theorem vacuumKineticA_pos L68
theorem vacuumKineticA_ne_zero L71
theorem vacuumKineticW_diag L74
theorem vacuumKinetic_diag L77
def vacuumKineticHbClosed L81
def vacuumKineticHpClosed L84
theorem contDiff_vacuumKineticA L90
theorem contDiff_vacuumKinetic_kinTerm L97
theorem contDiff_vacuumKinetic_wTerm L105
theorem vacuumKinetic_profile_contDiff L111
theorem vacuumKineticLocalProfile_contDiff2 L119
theorem hasDerivAt_vacuumKinetic_p L125
theorem hasDerivAt_vacuumKineticK_b L144
theorem hasDerivAt_vacuumKineticW_b L182
theorem hasDerivAt_vacuumKinetic_b L199
def vacuumKineticLocalHa L214
def vacuumKineticLocalHb L218
def vacuumKineticLocalHp L222
theorem vacuumKineticLocalHp_eq_closed L226
theorem vacuumKineticLocalHb_eq_closed L239
theorem vacuumKinetic_FE L252
theorem vacuumKinetic_localCoeff_eq_structure_mom L265
def vacuumKineticCellCoords L278
def vacuumKineticCellCoordsD L281
lemma hasFDerivAt_vacuumKineticCellCoords L284
lemma hasFDerivAt_vacuumKineticLocalCell L289
def vacuumKineticLocalSmooth L340
def vacuumKineticHamAdvFrom L348
def vacuumKineticHamAdvTo L352
theorem vacuumKineticHam_eq_LocalHamFromProfile L356
theorem differentiable_vacuumKineticHam L361
theorem bracket_bilinear_basis_zmod2 L368
theorem mom_ham_split_vacuumKinetic L427
theorem ham_ham_vacuumKinetic L474
def vacuumKineticNondegPhase L487
theorem vacuumKinetic_nondeg L490
def vacuumKineticWeakTarget L496
theorem vacuumKinetic_kinetic_regular_witness L527
def vacuumKineticStrongTarget L554
theorem vacuumKineticDensity_eq_localProfile L568
def vacuumKineticCanonicalMomTarget L573
def coincidentPhaseKin L585
theorem not_HKTRigidityModVacuumStatementN2 L589
theorem vacuumKinetic_structure_nonconstant L620
theorem fe_diagonal_trivial L625
theorem vacuumKinetic_fails_modVacuum_hamShape L632
structure KineticNormalizedCanonicalMom L668
def HKTRigidityKineticNormalizedN2 L679
lemma localCellD_eval_p0 L694
lemma localCellD_eval_b0 L702
theorem LocalHamSmooth_hp_unique L712
theorem LocalHamSmooth_hb_unique L724
theorem hasDerivAt_profileMap_p L737
theorem hasDerivAt_profileMap_b L749
def cellCoords0 L761
def cellCoords0D L764
lemma hasFDerivAt_cellCoords0 L767
theorem cellCoords0_fePhase L773
theorem LocalHamSmooth_hp_eq_fderiv L777
theorem LocalHamSmooth_hb_eq_fderiv L813
theorem hasDerivAt_hp_of_normalized L850
theorem hasDerivAt_hb_of_normalized L857
theorem kinetic_split_of_intensivity L867
theorem hb0_of_intensivity_FE L897
theorem gradient_recovery_of_intensivity L918
theorem alternating_FE_of_profile L980
theorem ftc_recovery_of_normalized L1049
theorem HKTRigidityKineticNormalizedN2_holds L1079
def hamDynKineticNormalized L1109

… and 5 more