module module

`IndisputableMonolith.Gravity.SevenGaps.HKTPointSplitTarget`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (2)

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

IndisputableMonolith.Gravity.SevenGaps.HKTPointSplitStrong module_import
IndisputableMonolith.Gravity.SevenGaps.HKTPointSplitTargetAudit module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.DynamicStructureBracket module_import
IndisputableMonolith.Gravity.SevenGaps.HKTDynamicTarget module_import

declarations in this module (62)

lemma zmod2_zero_add_one L44
lemma zmod2_one_add_one L45
lemma zmod2_zero_sub_one L46
lemma zmod2_one_sub_one L47
lemma sum_zmod2 L49
abbrev LocalMomProfile L57
def momFromProfile L59
def MomFromProfile L62
def quadraticHamDensity L66
theorem quadraticHamDensity_smear L69
structure LocalMomSmooth L77
def localMomCellD L91
lemma hasFDerivAt_localMomCell L97
def MomFromProfileD L104
lemma hasFDerivAt_MomFromProfile L108
lemma localMomCellD_pdir L115
lemma localMomCellD_qdir L126
theorem pderivP_MomFromProfile L135
theorem pderivQ_MomFromProfile L157
def UnsplitMomHamForProfile L181
def ForcedUnsplitPartialRelation L188
theorem forced_unsplit_partial_relation_impossible L193
def unsplitNoGoPhase L200
def delta0 L204
def delta1 L205
lemma unsplitNoGo_vals L207
theorem bracket_MomFromProfile_delta0_unsplitNoGo L216
theorem unsplit_RHS_delta0_unsplitNoGo L258
theorem unsplit_mom_ham_no_smooth_nearestNeighbor_witness_frozenHam L285
theorem unsplit_mom_ham_no_smooth_local_witness L307
structure HKTPointSplitTargetDyn L327
def hamAdvectionSplit L374
def hamDynDensity L380
def UnsplitMomHamForProfileDyn L389
theorem until L402
def UnsplitMomHamNoSmoothNearestNeighborWitnessHamDyn L403
def momDynDensity L406
def structureDyn L409
def hamDynAdvFrom L413
def hamDynAdvTo L418
def momDynBracketDensity L426
def MomDyn L429
theorem hamDynDensity_smear L432
theorem structureDyn_eq_concrete L439
theorem MomDyn_closed L443
def MomDynD L450
lemma hasFDerivAt_MomDyn L454
theorem differentiable_MomDyn L469
theorem pderivQ_MomDyn_zero L472
theorem pderivQ_MomDyn_one L478
theorem pderivP_MomDyn_zero L484
theorem pderivP_MomDyn_one L490
theorem bracket_MomDyn_MomDyn L496
theorem bracket_MomDyn_HamDyn L521
theorem structureDyn_not_constant L551
def hamDynNondegPhase L557
theorem hamDynDensity_nondeg L560
def hamDynPointSplitTarget L566
theorem hktPointSplitTargetDyn_two_nonvacuous L606
theorem DgenSym_eq_zero_two L611
theorem zero_density_fails_nondegenerate L625
def HKTRigidityStatementPointSplitDynN2 L638