module module

`IndisputableMonolith.Gravity.Analysis.ReggeBlochStarEdgeOrigins4D`

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.Regge4DExactActionSymbol module_import
IndisputableMonolith.Gravity.Analysis.ReggeBlochStarEdgeOriginsM2Eval4D module_import

depends on (6)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.Analysis.ReggeBlochAllOrbitSymbol4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeBlochFold4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeBlochOrbitTransport4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeBlochTransportedAllOrbit4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeEdgeStencil4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeHinge4DOrbitClassification module_import

declarations in this module (25)

abbrev Mat4 L37
abbrev Wave4 L38
structure SeedEdgeContrib L41
def seedEdgeContribs_t12 L47
theorem seedEdgeContribs_t12_length L161
def seedEdgeContribs_t13 L165
theorem seedEdgeContribs_t13_length L289
def seedEdgeContribs_t22 L293
theorem seedEdgeContribs_t22_length L457
def seedEdgeContribs_t21 L461
def seedEdgeContribs_t31 L462
def seedEdgeContribs L464
def transportOrigin L473
def edgeContribPhased L477
def phasedDeficitDotEdgeOrigins L484
lemma list_sum_map_smul_planeWave L489
theorem phasedDeficitDotEdgeOrigins_smul L509
def edgeContribPhase2 L518
def slotOrbitDeficitPhase2EdgeOrigins L524
def m2OrbitSlotCoeffEdgeOrigins L530
def m2OrbitMomentEdgeOrigins L537
def m2AllOrbitMomentDistinctHingeEdgeOrigins L542
structure StarEdgeOriginsStatus L550
def starEdgeOriginsStatus L555
theorem starEdgeOriginsStatus_flags L560