IndisputableMonolith.Gravity.Analysis.ReggeBlochTransportedAllOrbit4D

declarations in this module (65)

• abbrev Mat4 L55
• def orbitSeedKernel L60
• theorem orbitSeedKernel_eq_assembly L68
• def pushforwardClass L73
• def transportedOrbitDeficit L76
• def transportedOrbitArea L79
• def slotOrbitDeficitKer L82
• def slotOrbitAreaCov L87
• def transportedOrbitSlotTerm L91
• def blochFoldOrbit L98
• def blochFoldAll L102
• def orbitStarSize L110
• theorem orbitStarSize_pos L118
• theorem orbitStarSize_ne_zero L121
• def blochFoldAllDistinctHinge L127
• theorem classDot_pushforward L132
• theorem phasedClassDot_pushforward L147
• theorem orbitSeedKernel_t11 L166
• theorem transportedOrbitDeficit_t11 L169
• theorem slotOrbitDeficitKer_t11 L175
• def pushAreaZ4 L181
• lemma pushforward_areaCov11_div4 L185
• lemma slotAreaCov_div4 L207
• lemma pushAreaZ4_eq_slotAreaCovZ4 L214
• theorem slotOrbitAreaCov_t11 L223
• theorem slotOrbitAreaCov_t11_eq L232
• def AreaPushforwardMatchOpen L238
• theorem AreaPushforwardMatchOpen_holds L242
• theorem transportedOrbitSlotTerm_t11 L246
• theorem blochFoldOrbit_t11 L257
• theorem transportedOrbitSlotTerm_zeroMomentum L265
• def ZeroMomTrueWeightMatchOpen L280
• theorem transportedOrbitSlotTerm_smul L285
• theorem blochFoldOrbit_smul L296
• theorem blochFoldAll_smul L302
• theorem blochFoldAll_zero L307
• theorem blochFoldAllDistinctHinge_smul L311
• theorem blochFoldAllDistinctHinge_zero L322
• def slotOrbitKerDot L330
• def m2TransportedOrbitSlotCoeffTrunc L336
• def m2TransportedOrbitSlotCoeffFull L349
• theorem m2TransportedOrbitSlotCoeffFull_eq_trunc_of_ker0 L364
• abbrev m2TransportedOrbitSlotCoeff L382
• def m2TransportedOrbitMoment L384
• def m2TransportedAllOrbitMoment L388
• def m2TransportedAllOrbitMomentDistinctHinge L392
• def m2TransportedOrbitMomentFull L398
• def m2TransportedAllOrbitMomentDistinctHingeFull L402
• lemma sum_mul_classCoeff_smul L407
• lemma sum_mul_classCoeff_phase_smul L415
• theorem m2TransportedOrbitSlotCoeffTrunc_smul L425
• theorem m2TransportedOrbitSlotCoeff_smul L438
• theorem m2TransportedOrbitSlotCoeffFull_smul L444
• theorem m2TransportedOrbitMoment_smul L460
• theorem m2TransportedAllOrbitMomentDistinctHinge_smul L467
• theorem m2TransportedOrbitMomentFull_smul L479
• theorem m2TransportedAllOrbitMomentDistinctHingeFull_smul L486
• theorem phaseScaleDir_symbolDir L498
• theorem m2TransportedOrbitSlotCoeff_t11 L502
• theorem m2TransportedOrbitMoment_t11 L514
• def M2TransportedAllOrbitAxisSymbolDirEvalOpen L525
• def M2DistinctHingeAxisSymbolDirEvalOpen L530
• structure ReggeBlochTransportedAllOrbit4DStatus L536
• def reggeBlochTransportedAllOrbit4DStatus L546
• theorem reggeBlochTransportedAllOrbit4DStatus_flags L557