module module

`IndisputableMonolith.Gravity.SevenGaps.HKTOneSiteCounterexample`

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 (4)

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

IndisputableMonolith.Gravity.SevenGaps.Gap5ConstraintCloseStatus module_import
IndisputableMonolith.Gravity.SevenGaps.Gap5ConstraintResidualDAG module_import
IndisputableMonolith.Gravity.SevenGaps.HKTGroundworkAudit module_import
IndisputableMonolith.Gravity.SevenGaps.HKTOneSiteCounterexampleAudit module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.HypersurfaceDeformation module_import

declarations in this module (23)

def quarticHamDensity L35
def zeroMomDensity L39
def quarticHam L43
def quarticHamD L47
lemma hasFDerivAt_quarticHam L50
theorem differentiable_quarticHam L56
lemma pderivQ_quarticHam L60
theorem bracket_quarticHam_quarticHam L69
lemma zeroMom_eq_zero L74
lemma differentiable_zeroMom L80
lemma pderivQ_zeroMom L85
lemma pderivP_zeroMom L91
lemma bracket_zeroMom_any L97
lemma zmod1_one_eq_zero L102
lemma zmod1_add_self L104
lemma zmod1_wronskian_zero L107
lemma zmod1_lapse_diff_zero L112
theorem one_site_wronskians_vacuous L120
def quarticOneSiteHKT L131
def momPoint L162
lemma momPoint_q L165
lemma momPoint_p L166
theorem not_HKTRigidityStatement_one L171