IndisputableMonolith.Gravity.Analysis.Regge4DTorusContinuumLimit

declarations in this module (43)

• abbrev Mat4 L52
• def torusSiteCount L57
• theorem torusSiteCount_eq L59
• def torusDensityWeight L64
• theorem torusDensityWeight_eq_correct L66
• theorem torusDensityWeight_ne_wrong L69
• def familySide L75
• def intModeDir L79
• def secondDifferenceBookkeepingFactor4D L87
• def ttSecondDifferenceDensityWeight L90
• theorem ttSecondDifferenceDensityWeight_eq L93
• def cellSumCosMulCosFactor L103
• theorem density_cellSum_cancellation L109
• def survivingDictionaryFactor4D L121
• theorem survivingDictionaryFactor4D_eq_one L123
• theorem survivingDictionaryFactor4D_eq_cancellation L126
• def canonicalFiniteH4D L135
• theorem canonicalFiniteH4D_eq L138
• theorem canonicalFiniteH4D_eq_finiteTransportedSymbol L143
• theorem canonicalFiniteH4D_smul L150
• def finiteTorusHessian L158
• theorem finiteTorusHessian_eq_canonical L161
• theorem finiteTorusHessian_eq_finiteTransportedSymbol L165
• def BlochCellSum4DCosMulCosOpen L179
• theorem BlochCellSum4DCosMulCosOpen_scalar_holds L187
• def NonlinearSecondVariation4D L195
• def SchlafliElevationToDistinctHingeOpen L206
• def CanonicalFiniteH4DEqDistinctHingeFoldOpen L214
• theorem dictionary_identifies_fold_of_cellSum_scaled L220
• def FiniteTorusHessianEqAllOrbitFold L237
• theorem FiniteTorusHessianEqAllOrbitFold_holds L243
• def TorusNormalizedTendsto L253
• theorem torusNormalized_eq_continuumSymbol L260
• def TorusNormalizedTendstoExactAction L265
• def TorusNormalizedTendstoDiscreteBookkeeping L275
• def TorusNormalizedTendstoLegacyFold L280
• def DistinctHingePinnedMomentVsEH L294
• theorem distinctHinge_pinned_ne_eh L297
• def TorusC2DensityExtensionOpen L305
• structure Regge4DTorusContinuumLimitStatus L311
• def regge4DTorusContinuumLimitStatus L321
• theorem regge4DTorusContinuumLimitStatus_flags L331
• theorem dictionary_does_not_inhabit_eh_or_flip_gap L347