module module

`IndisputableMonolith.Gravity.Analysis.ReggeTTAlgebraicCloser`

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

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

IndisputableMonolith.Gravity.Analysis.ReggeTTContinuumCloser module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.Analysis.ReggeTTContinuumLimit module_import
IndisputableMonolith.Gravity.Analysis.ReggeTTGateBBridge module_import

declarations in this module (26)

theorem slotMidTwice_eq_core L99
theorem bucketKeyOf_eq L105
theorem rawCosineSupport_eq_rawMomentSupport L114
theorem rawTripleWeight_eq L123
theorem rawBucketAmplitude_eq L128
theorem rawPhaseQuadratic_eq L137
theorem continuumMoment_eq_bridgeMoment L142
def adjugateQuadraticForm L157
theorem adjugate00 L161
theorem adjugate01 L165
theorem adjugate02 L169
theorem adjugate10 L173
theorem adjugate11 L177
theorem adjugate12 L181
theorem adjugate20 L185
theorem adjugate21 L189
theorem adjugate22 L193
theorem adjugateQuadraticForm_explicit L198
theorem committedSpikeLHS_spikeInput_expand L219
theorem committedSpikeLHS_eq_half_adjugate L250
theorem bridgeMoment_eq_half_adjugate L274
theorem continuumMoment_eq_half_adjugate L288
theorem adjugateQuadraticForm_tt L307
theorem reggeTTMoment_tt_real L346
theorem reggeTTMoment_tt_value L372
theorem canonicalFiniteH_div_momentumNormSq_tendsto_isotropy L416