IndisputableMonolith.Gravity.SevenGaps.HKTPointSplitStrong

declarations in this module (38)

• def siteDelta L41
• lemma siteDelta_self L44
• lemma siteDelta_ne L47
• def computedHamAdvFrom L52
• def computedHamAdvTo L58
• lemma zmod2_succ_ne L63
• lemma zmod2_zero_add_one' L66
• lemma zmod2_one_add_one' L67
• theorem hamAdvFrom_eq_computed L70
• theorem hamAdvTo_eq_computed L97
• structure HKTPointSplitTargetDynStrong L136
• def quarticHamDensity2 L157
• def zeroMomDensity2 L161
• def decorativeStructure2 L165
• def quarticHam2 L168
• def quarticHam2D L171
• lemma hasFDerivAt_quarticHam2 L174
• theorem differentiable_quarticHam2 L180
• lemma pderivQ_quarticHam2 L184
• theorem bracket_quarticHam2_quarticHam2 L191
• lemma zeroMom2_eq_zero L196
• lemma differentiable_zeroMom2 L202
• lemma bracket_zeroMom2_any L208
• lemma decorativeStructure2_not_constant L226
• def quarticNondegPhase L232
• theorem quarticHamDensity2_nondeg L235
• def quarticZeroMomTarget L243
• theorem quarticZeroMomTarget_mom_vanishes L285
• theorem quarticZeroMom_fails_mom_load_bearing L291
• theorem quarticZeroMomTarget_not_strong L302
• def momLoadBearingWitnessPhase L314
• lemma momLoadBearingWitness_vals L318
• theorem hamDyn_mom_load_bearing_witness L325
• theorem hamDyn_kinetic_regular_witness L342
• def hamDynPointSplitTargetStrong L356
• theorem hktPointSplitTargetDynStrong_two_nonvacuous L370
• theorem strong_target_discriminates_decoy L375
• def HKTRigidityStatementPointSplitDynN2Strong L389