IndisputableMonolith.Gravity.SevenGaps.HKTVacuumSectorKill

declarations in this module (44)

• lemma zmod2_zero_add_one L47
• lemma zmod2_one_add_one L48
• def vacuumShiftHamDensity L53
• def vacuumShiftLocalProfile L57
• def vacuumShiftLocalHa L60
• def vacuumShiftLocalHb L63
• def vacuumShiftLocalHp L65
• def vacuumShiftHamAdvFrom L68
• def vacuumShiftHamAdvTo L73
• theorem vacuumShiftDensity_eq_localProfile L76
• def VacSmear L84
• def VacSmearD L87
• lemma hasFDerivAt_VacSmear L90
• theorem pderivQ_VacSmear L96
• theorem pderivP_VacSmear L110
• def HamVac L117
• theorem HamVac_eq_HamDyn_add_Vac L120
• theorem differentiable_HamVac L134
• def vacuumShiftLocalCellD L143
• lemma vacuumShiftLocalCellD_eq_profilePartials L146
• lemma hasFDerivAt_vacuumShiftLocalCell_raw L163
• lemma hasFDerivAt_vacuumShiftLocalCell L187
• def vacuumShiftLocalSmooth L197
• theorem bracket_MomDyn_VacSmear L205
• theorem bracket_MomDyn_HamVac L223
• theorem bracket_VacSmear_VacSmear L281
• theorem bracket_HamDyn_VacSmear L286
• theorem bracket_VacSmear_HamDyn L299
• theorem bracket_HamVac_HamVac L311
• def vacuumShiftWeakTarget L351
• def vacuumShiftStrongTarget L413
• def vacuumShiftCanonicalMomTarget L465
• def coincidentPhase L479
• theorem not_HKTRigidityStatementPointSplitDynN2Canonical L483
• def HKTRigidityModVacuumStatementN2 L509
• def Note_modVacuumSectorsRemainOpen L529
• theorem note_modVacuumSectorsRemainOpen L531
• def Note_modVacuumKilledInC4 L535
• theorem note_modVacuumKilledInC4 L537
• theorem vacuumShift_satisfies_modVacuum L540
• theorem hamDyn_satisfies_modVacuum L566
• structure HKTVacuumSectorKillStatus L587
• def hktVacuumSectorKillStatus L597
• theorem hktVacuumSectorKillStatus_flags L605