module module

`IndisputableMonolith.Gravity.SevenGaps.HKTCanonicalMomRigidityPDE`

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

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

IndisputableMonolith.Gravity.SevenGaps.HKTCanonicalMomRigidityPDEAudit module_import
IndisputableMonolith.Gravity.SevenGaps.HKTKineticNormalizedRigidity module_import
IndisputableMonolith.Gravity.SevenGaps.HKTVacuumSectorKill module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.HKTCanonicalMomRigidity module_import

declarations in this module (30)

def profileMap L46
theorem LocalHamSmoothContDiff2Obligation_iff L49
def sqrtAffineProfile L56
def sqrtAffineHb L60
def sqrtAffineHp L65
theorem sqrtAffine_one_add_sq_pos L68
theorem sqrtAffine_one_add_sq_ne_zero L72
theorem sqrtAffineProfile_contDiff2 L76
theorem sqrtAffine_satisfies_FE L97
theorem sqrtAffineHp_not_linear_in_p L116
theorem sqrtAffineHb_not_p_independent L127
theorem not_forced_linear_hp_of_contDiff2_FE L139
theorem not_forced_hb_p_independent_of_contDiff2_FE L154
def ConstantKineticSlope L170
def ConstantVacuumGauge L175
theorem hb_shape_of_constant_kinetic_slope L180
theorem ADM_quadratic_of_gauges L206
theorem hamDynLocalProfile_contDiff2 L238
theorem hamDyn_HpLinearInP L269
theorem hamDyn_HbPIndependent L274
theorem hamDyn_constantKineticSlope L278
theorem hamDyn_constantVacuumGauge L286
structure SmoothScopedCanonicalMomData L292
theorem HKTRigidityPointSplitDynN2Canonical_smooth L332
def hamDynSmoothScopedData L370
theorem hamDyn_smooth_scoped_rigidity L402
theorem SolveProfileFEQuadratic_of_smoothScopedData L419
structure HKTCanonicalMomRigidityC2Status L431
def hktCanonicalMomRigidityC2Status L443
theorem hktCanonicalMomRigidityC2Status_flags L451