IndisputableMonolith.Gravity.SevenGaps.CurvedOperatorUnderdetermination

declarations in this module (22)

• def curvatureCoupledOperator L50
• def singleCurvatureExtension L55
• def doubleCurvatureExtension L60
• def constantPlusField L66
• theorem discLap3_constantPlusField_zero L69
• theorem curvatureCoupledOperator_flat_specialization L80
• theorem extensions_agree_on_entire_flat_specialization L89
• theorem extensions_distinct_at_nonzero_curvature L101
• def curvedDiscreteEigenvalue L120
• def curvedContinuumEigenvalue L126
• theorem curvatureCoupledOperator_planeH L131
• theorem curvedDiscreteEigenvalue_tendsto L148
• theorem curvedContinuumEigenvalues_distinct L156
• theorem flat_spectrum_underdetermines_curvature_coupling L167
• def CurvedSpectrumConverges L195
• def CurvatureCorrectionConsistent L206
• def CurvatureCorrectionRateBound L218
• theorem curvedSpectrumConverges_iff_curvatureCorrectionConsistent L230
• theorem curvatureCorrectionConsistent_of_rateBound L250
• theorem curvedSpectrumConverges_of_correctionRateBound L265
• theorem curvedEigenvalueFamily_rateBound L278
• theorem gap4_curvature_coupling_blocker L299