IndisputableMonolith.Gravity.Analysis.ReggeBlochAllOrbitSymbol4D

declarations in this module (43)

• def isOrbit L53
• theorem isOrbit_iff_pop L60
• theorem isOrbit_t11_iff_isT11 L73
• theorem orbit_slot_count_nat L78
• theorem orbit_slot_count_real L91
• theorem complement_orbit_deficit_kernels L101
• theorem orbitAreaCov_uses_heron_grads L109
• def factorizedOrbitSlotTerm L125
• def factorizedBlochFoldOrbit L133
• def factorizedBlochFoldAll L138
• theorem factorizedBlochFoldOrbit_t11_eq L141
• theorem factorizedBlochFoldOrbit_zeroMomentum L154
• theorem factorizedBlochFoldAll_zeroMomentum L181
• theorem factorizedBlochFoldAll_axis_zeroMomentum L188
• theorem factorizedBlochFoldAll_gauge_zeroMomentum L192
• def foldOrbitAlong L199
• def foldAllAlong L203
• def phaseScaleDir L207
• theorem classMidpointPhase_scaleDir L211
• theorem phasedClassDot_scaleDir L226
• theorem foldOrbitAlong_neg L234
• theorem foldOrbitAlong_even L250
• theorem foldAllAlong_neg L254
• theorem foldAllAlong_even L259
• lemma zero_smul_dir L263
• theorem foldAllAlong_zero L267
• theorem foldAllAlong_axis_zero L273
• theorem foldAllAlong_gauge_zero L277
• def m2OrbitMomentPoly L285
• def m2AllOrbitMomentPoly L297
• theorem m2OrbitMomentPoly_of_area_zero L301
• theorem foldOrbitAlong_zero L309
• theorem foldOrbitAlong_axis_zero L316
• theorem foldOrbitAlong_gauge_zero L322
• def OrbitFoldAlongM2Tendsto L330
• def AllOrbitFoldAlongM2Tendsto L336
• def ArbitraryDirectionCosineTwoJet L341
• def AllOrbitArbitraryDirectionCosineTwoJet L345
• structure BlochAllOrbitSymbol4DStatus L350
• def blochAllOrbitSymbol4DStatus L368
• theorem blochAllOrbitSymbol4DStatus_flags L381
• theorem decoy_one_orbit_m2_is_not_continuum_target L398
• theorem open_props_are_status_false L406