IndisputableMonolith.Gravity.SevenGaps.HKTCanonicalMomTarget

declarations in this module (53)

• lemma zmod2_zero_add_one L33
• lemma zmod2_one_add_one L34
• lemma zmod2_succ_ne L35
• def quarticBalancedStructure2 L41
• def quarticBalancedHamDensity2 L45
• def quarticBalancedMomDensity2 L51
• def quarticBalancedHamAdvFrom2 L56
• def quarticBalancedHamAdvTo2 L61
• def quarticBalancedMomBracketDensity2 L67
• def quarticBalancedHam2 L72
• def MomBalanced L75
• theorem quarticBalanced_balance L78
• theorem MomBalanced_closed L85
• def MomBalancedD L95
• lemma hasFDerivAt_MomBalanced L102
• theorem differentiable_MomBalanced L123
• theorem pderivQ_MomBalanced L127
• theorem pderivP_MomBalanced L135
• theorem bracket_MomBalanced_MomBalanced L143
• theorem bracket_MomBalanced_quarticHam L176
• theorem bracket_quarticBalancedHam_quarticBalancedHam L235
• theorem quarticBalancedStructure2_not_constant L246
• def quarticBalancedNondegPhase L253
• theorem quarticBalancedHamDensity2_nondeg L256
• def quarticBalancedLoadPhase L262
• theorem quarticBalanced_mom_load_bearing_witness L266
• theorem quarticBalanced_kinetic_regular_witness L286
• def quarticBalancedWeakTarget L307
• def quarticBalancedStrongTarget L381
• def constConfigPhase L396
• theorem not_HKTRigidityStatementPointSplitDynN2Strong L401
• structure HKTPointSplitTargetDynCanonicalMom L429
• def hamDynLocalProfile L445
• def hamDynLocalHa L449
• def hamDynLocalHb L452
• def hamDynLocalHp L455
• def hamDynLocalCellD L460
• lemma hamDynLocalCellD_eq_profilePartials L469
• lemma hasFDerivAt_hamDynLocalCell_raw L483
• lemma hasFDerivAt_hamDynLocalCell L511
• def hamDynLocalSmooth L521
• theorem hamDynDensity_eq_localProfile L527
• theorem structureDyn_eq_g L532
• theorem momDynDensity_canonical L537
• def hamDynPointSplitTargetCanonicalMom L543
• theorem hktPointSplitTargetDynCanonicalMom_nonvacuous L554
• def canonicalMomSepPhase L560
• theorem quarticBalanced_fails_canonical_mom L563
• theorem canonicalMom_excludes_balanced_quartic L576
• def HKTRigidityStatementPointSplitDynN2Canonical L611
• structure HKTCanonicalMomStatus L628
• def hktCanonicalMomStatus L638
• theorem hktCanonicalMomStatus_flags L644