module module

`IndisputableMonolith.Gravity.Analysis.ReggeTTContinuumLimit`

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.Analysis.ReggeBlochM2Tendsto4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeTTAlgebraicCloser module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.Analysis.ReggeTTBlochAssembly module_import

declarations in this module (18)

def rawPhaseLinear L33
def rawPhaseQuadratic L38
def rawCosineEvaluatorAtScale L42
def rawCosineFoldAtScale L46
def realModeNormSq L52
def normalizedRealMode L56
def sideScale L60
theorem rawCosineFoldAtScale_zero L66
theorem iteratedDeriv_two_cos_mul L97
theorem of L120
theorem cos_sub_one_div_sq_tendsto L121
theorem rawCosineFold_scale_tendsto L148
theorem rawPhaseQuadratic_normalized L208
theorem reggeTTMoment_normalized L225
theorem realModeNormSq_intCast_pos L244
theorem rawCosineEvaluator_eq_scale L255
theorem momentumNormSq_eq_scale_sq L267
theorem canonicalFiniteH_div_momentumNormSq_tendsto L279