IndisputableMonolith.Gravity.Analysis.ReggeBlochTransportedAllOrbitM2Eval4D · Recognition explainer

used by (4)

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

IndisputableMonolith.Gravity.Analysis.Regge4DTensorAlgebraicCloser module_import
IndisputableMonolith.Gravity.Analysis.ReggeBlochLocalIncidenceM2Eval4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeBlochStarEdgeOriginsM2Eval4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeBlochTransportedAllOrbitM2Eval4DAudit module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.Analysis.ReggeBlochM2Symbol4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeBlochTransportedAllOrbit4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeFlat4DHessianAssembly module_import

declarations in this module (165)

abbrev Mat4 L62
theorem sum_mul_pushforward L69
theorem sum_mul_pushforward_weighted L84
lemma sum_div_const_st L99
lemma sum_six_orbits L104
def area12Z L120
def area21Z L123
def area13Z L126
def area31Z L129
def area22Z L132
theorem areaCov12_eq_z L135
theorem areaCov21_eq_z L139
theorem areaCov13_eq_z L143
theorem areaCov31_eq_z L147
theorem areaCov22_eq_z L151
def slotAZ12 L157
def slotAZ21 L160
def slotAZ13 L163
def slotAZ31 L166
def slotAZ22 L169
def slotKppOrbit L172
def m2OrbitCertZ12 L178
def m2OrbitCertZ21 L182
def m2OrbitCertZ13 L186
def m2OrbitCertZ31 L190
def m2OrbitCertZ22 L194
lemma sqrt2_mul_self L200
lemma sqrt3_mul_self L203
lemma radical2_slot_arith L206
lemma radical3_slot_arith L215
lemma area_push_sqrt2 L224
lemma area_push_sqrt3 L245
lemma ker_push_sqrt2_half L266
lemma ker_push_sqrt3 L296
theorem m2TransportedOrbitSlotCoeff_t12_eq_cert L326
theorem m2TransportedOrbitSlotCoeff_t21_eq_cert L355
theorem m2TransportedOrbitSlotCoeff_t13_eq_cert L385
theorem m2TransportedOrbitSlotCoeff_t31_eq_cert L414
theorem m2TransportedOrbitSlotCoeff_t22_eq_cert L444
theorem sum_m2OrbitCertZ12_axis L500
theorem sum_m2OrbitCertZ21_axis L507
theorem sum_m2OrbitCertZ13_axis L514
theorem sum_m2OrbitCertZ31_axis L521
theorem sum_m2OrbitCertZ22_axis L528
theorem sum_m2OrbitCertZ12_gauge L535
theorem sum_m2OrbitCertZ21_gauge L542
theorem sum_m2OrbitCertZ13_gauge L549
theorem sum_m2OrbitCertZ31_gauge L556
theorem sum_m2OrbitCertZ22_gauge L563
theorem m2TransportedOrbitMoment_t12_axis L570
theorem m2TransportedOrbitMoment_t21_axis L582
theorem m2TransportedOrbitMoment_t13_axis L594
theorem m2TransportedOrbitMoment_t31_axis L606
theorem m2TransportedOrbitMoment_t22_axis L618
theorem m2TransportedOrbitMoment_t11_axis L630
theorem m2TransportedAllOrbitMoment_axisTTPlus_symbolDir L636
theorem M2TransportedAllOrbitAxisSymbolDirEvalOpen_holds L645
theorem m2TransportedOrbitMoment_t12_gauge L651
theorem m2TransportedOrbitMoment_t21_gauge L663
theorem m2TransportedOrbitMoment_t13_gauge L675
theorem m2TransportedOrbitMoment_t31_gauge L687
theorem m2TransportedOrbitMoment_t22_gauge L699
theorem m2TransportedOrbitMoment_t11_gauge L711
theorem m2TransportedAllOrbitMoment_decoyGauge_symbolDir L715
theorem m2TransportedAllOrbitMomentDistinctHinge_axisTTPlus_symbolDir L726
theorem M2DistinctHingeAxisSymbolDirEvalOpen_holds L738
theorem m2TransportedAllOrbitMomentDistinctHinge_decoyGauge_symbolDir L742
theorem m2TransportedAllOrbitMomentDistinctHinge_axisTTPlusNormalized_symbolDir L757
theorem sum_m2SlotCertZ_cross L770
theorem sum_m2OrbitCertZ12_cross L777
theorem sum_m2OrbitCertZ21_cross L784
theorem sum_m2OrbitCertZ13_cross L791
theorem sum_m2OrbitCertZ31_cross L798
theorem sum_m2OrbitCertZ22_cross L805
theorem m2Symbol_axisTTCross L810
theorem m2TransportedOrbitMoment_t11_cross L821
theorem m2TransportedOrbitMoment_t12_cross L825
theorem m2TransportedOrbitMoment_t21_cross L837
theorem m2TransportedOrbitMoment_t13_cross L849
theorem m2TransportedOrbitMoment_t31_cross L861

… and 85 more