module module

`IndisputableMonolith.Gravity.SevenGaps.PathSumProbes`

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 (1)

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

IndisputableMonolith.Gravity.SevenGaps.FreudenthalTorusClassMass module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Geometry.PeriodicFreudenthalTorus module_import
IndisputableMonolith.Gravity.SevenGaps.PathSumMeasure module_import

declarations in this module (50)

theorem card_vertex L76
def periodicEdgeEquivProd L84
theorem card_periodicEdge L92
theorem card_periodicTet L99
def freudenthalBoundedComplex L118
theorem freudenthalBoundedComplex_nV L135
theorem freudenthalBoundedComplex_nE L139
theorem freudenthalBoundedComplex_nT L143
theorem freudenthalBoundedComplex_nT_pos L147
theorem freudenthalBoundedComplex_edgeVerts L156
theorem freudenthalBoundedComplex_tetVerts L161
theorem freudenthalBoundedComplex_matches_canonical L169
def translateVertex L192
theorem translateVertex_apply L203
def translateEdge L208
theorem translateEdge_apply L214
def translateTet L220
theorem translateTet_apply L224
theorem addBit_add_right L229
theorem addBits_add_right L237
theorem addVertexBits_add_right L249
theorem translateEdge_endpoints L256
theorem translateVertex_zero L268
theorem translateEdge_zero L276
theorem translateTet_zero L284
theorem translateVertex_trans L292
theorem translateEdge_trans L300
theorem translateTet_trans L308
theorem conj_refl L319
theorem conj_trans L327
def translationAut L341
theorem translationAut_vEquiv L402
theorem translationAut_eEquiv L408
theorem translationAut_tEquiv L414
theorem refl_eEquiv L420
theorem refl_tEquiv L424
theorem translationAut_zero L428
theorem translationAut_add L443
theorem translationAut_injective L456
theorem translations_embed_in_aut L479
theorem translationAut_ne_refl L488
theorem autCard_ge_translations L495
theorem mu_freudenthal_le_inv_cube L503
theorem unnormalized_torus_weight_suppressed L520
theorem translationAut_three_injective L531
theorem autCard_ge_27 L535
theorem nontrivial_aut_three L544
structure ProbeStatus L553
def pathSumProbesStatus L566
theorem pathSumProbesStatus_flags L575