module module

`IndisputableMonolith.Gravity.SevenGaps.HKTCanonicalMomRigidity`

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.HKTCanonicalMomRigidityAudit module_import
IndisputableMonolith.Gravity.SevenGaps.HKTCanonicalMomRigidityPDE module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.FullTheoryLedger module_import
IndisputableMonolith.Gravity.SevenGaps.HKTCanonicalMomTarget module_import

declarations in this module (26)

lemma zmod2_zero_add_one L38
lemma zmod2_one_add_one L39
lemma zmod2_zero_add_two L40
lemma zmod2_one_add_two L41
def fePhase L46
theorem fePhase_coords L50
theorem hamDensity_smear_eq_LocalHamFromProfile L59
theorem localHamHamCoefficient_delta01 L73
theorem structure_mom_delta01 L84
theorem profiled_ham_ham_alternating_FE L108
theorem fe_at_r_zero L186
theorem fe_at_p_zero L198
def HpLinearInP L214
def HbPIndependent L219
def LocalHamSmoothContDiff2Obligation L228
theorem hb_coupling_of_linear_ansatz L234
theorem hb_coupling_swapped_of_linear_ansatz L253
def SolveProfileFEQuadratic L270
def solve_profile_FE_quadratic L287
theorem hamDyn_solve_profile_FE_quadratic L292
theorem canonicalMom_rigidity_of_FE_solution L315
theorem HKTRigidityStatementPointSplitDynN2Canonical_of_solve L352
theorem hamDyn_canonicalMom_rigidity_conclusion L359
structure HKTCanonicalMomRigidityC1Status L377
def hktCanonicalMomRigidityC1Status L389
theorem hktCanonicalMomRigidityC1Status_flags L396