IndisputableMonolith.Gravity.Analysis.ReggeBlochStarEdgeOriginsM2Eval4D · Recognition explainer

used by (2)

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

IndisputableMonolith.Gravity.Analysis.ReggeBlochStarEdgeOriginsM2Eval4DAudit module_import
IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianSymbol4D module_import

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.Analysis.ReggeBlochM2Symbol4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeBlochStarEdgeOrigins4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeBlochTransportedAllOrbitM2Eval4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeFlat4DHessianAssembly module_import

declarations in this module (117)

abbrev Mat4 L44
abbrev Wave4 L45
structure SeedEdgeContribZ L51
def toReal12 L56
def toReal13 L61
def toReal22 L66
def seedEdgeContribsZ_t12 L71
def seedEdgeContribsZ_t13 L99
def seedEdgeContribsZ_t22 L129
def seedEdgeContribsZ_t21 L167
def seedEdgeContribsZ_t31 L168
theorem seedEdgeContribsZ_t12_length L170
theorem seedEdgeContribsZ_t13_length L171
theorem seedEdgeContribsZ_t22_length L172
def hingeBaseZ L176
def transportOriginZ L179
def phase2EdgeSymbolZ L183
def edgePhase2Z L192
def slotKppEdge L197
def m2OrbitCertZ12Edge L202
def m2OrbitCertZ21Edge L207
def m2OrbitCertZ13Edge L212
def m2OrbitCertZ31Edge L217
def m2OrbitCertZ22Edge L222
def gaugeM1100E2CoeffZ L230
def gaugeM1100E2 L235
theorem classCoeff_gaugeM1100E2_int L239
theorem seedEdgeContribs_t12_eq_Z L247
theorem seedEdgeContribs_t21_eq_Z L252
theorem seedEdgeContribs_t13_eq_Z L256
theorem seedEdgeContribs_t31_eq_Z L261
theorem seedEdgeContribs_t22_eq_Z L265
lemma transportOrigin_int L272
lemma hingeBase_int L279
theorem phaseScale_edge_eq_phase2EdgeSymbolZ L284
lemma sqrt2_mul_self L305
lemma sqrt3_mul_self L308
lemma radical2_edge_slot_arith L311
lemma radical3_edge_slot_arith L320
lemma rational_edge_slot_arith L329
lemma sum_div_const_st L334
lemma edgeContribPhase2_toReal12 L341
lemma edgeContribPhase2_toReal13 L350
lemma edgeContribPhase2_toReal22 L359
lemma list_sum_map_sqrt2_div16 L368
lemma list_sum_map_sqrt3_div48 L379
lemma list_sum_map_div16 L390
theorem slotOrbitDeficitPhase2EdgeOrigins_t12_eq_Z L401
theorem slotOrbitDeficitPhase2EdgeOrigins_t21_eq_Z L414
theorem slotOrbitDeficitPhase2EdgeOrigins_t13_eq_Z L427
theorem slotOrbitDeficitPhase2EdgeOrigins_t31_eq_Z L440
theorem slotOrbitDeficitPhase2EdgeOrigins_t22_eq_Z L453
lemma area_push_sqrt2 L467
lemma area_push_sqrt3 L488
theorem m2OrbitSlotCoeffEdgeOrigins_t12_eq_cert L511
theorem m2OrbitSlotCoeffEdgeOrigins_t21_eq_cert L531
theorem m2OrbitSlotCoeffEdgeOrigins_t13_eq_cert L551
theorem m2OrbitSlotCoeffEdgeOrigins_t31_eq_cert L571
theorem m2OrbitSlotCoeffEdgeOrigins_t22_eq_cert L591
theorem sum_m2OrbitCertZ12Edge_axis L624
theorem sum_m2OrbitCertZ21Edge_axis L631
theorem sum_m2OrbitCertZ13Edge_axis L638
theorem sum_m2OrbitCertZ31Edge_axis L645
theorem sum_m2OrbitCertZ22Edge_axis L652
theorem sum_m2OrbitCertZ12Edge_cross L661
theorem sum_m2OrbitCertZ21Edge_cross L668
theorem sum_m2OrbitCertZ13Edge_cross L675
theorem sum_m2OrbitCertZ31Edge_cross L682
theorem sum_m2OrbitCertZ22Edge_cross L689
theorem sum_m2OrbitCertZ12Edge_gauge L698
theorem sum_m2OrbitCertZ21Edge_gauge L705
theorem sum_m2OrbitCertZ13Edge_gauge L712
theorem sum_m2OrbitCertZ31Edge_gauge L719
theorem sum_m2OrbitCertZ22Edge_gauge L726
theorem sum_m2OrbitCertZ12Edge_counterex L733
theorem sum_m2OrbitCertZ21Edge_counterex L740
theorem sum_m2OrbitCertZ13Edge_counterex L747
theorem sum_m2OrbitCertZ31Edge_counterex L754
theorem sum_m2OrbitCertZ22Edge_counterex L761
theorem sum_m2SlotCertZ_counterex L768

… and 37 more