IndisputableMonolith.Geometry.PeriodicFreudenthalTorus · Recognition explainer

used by (4)

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

IndisputableMonolith.Gravity.Analysis.FreudenthalStencilPreflight module_import
IndisputableMonolith.Gravity.PhysicalSixTetCubicDirichletInstance module_import
IndisputableMonolith.Gravity.SevenGaps.PathSumProbes module_import
IndisputableMonolith.Gravity.TensorShearSector module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Geometry.FreudenthalCubeTriangulation module_import

declarations in this module (59)

abbrev Vertex L28
def bit L30
def addBit L34
theorem addBit_false L37
theorem addBit_true_eq_mk L42
theorem addBit_false_after_true L47
theorem addBit_true_after_false L51
theorem addBit_true_ne_self L55
def addBits L71
def dispBits L76
def vertexBits L86
def addVertexBits L96
theorem addBit_true_injective L101
theorem addBit_injective L132
theorem addBits_injective L139
theorem addVertexBits_injective L150
theorem addVertexBits_surjective L158
theorem existsUnique_addVertexBits_eq L164
theorem sum_ite_eq_of_addVertexBits L175
structure PeriodicEdge L195
def cubeEdgeBase L241
def cubeEdgeDisp L264
def localEdgeOf L287
abbrev PeriodicTet L295
def vertexFinEquiv L300
def edgeFinEquiv L306
def tetFinEquiv L312
def canonicalEdgeSlot L318
theorem canonicalEdgeSlot_eq_some_implies L330
theorem canonicalEdgeSlot_eq_some_of_noDup L354
def canonicalEdgeVerts L387
def canonicalTetVerts L399
def canonicalEdgeInTet L408
theorem canonicalEdgeInTet_eq_some_implies L415
def CanonicalPeriodicLocalEdgeNoDup L427
theorem canonicalPeriodicLocalEdgeNoDup L432
theorem canonicalEdgeInTet_iff_of_noDup L440
def periodicDispSqEdge L459
def canonicalGlobalSqEdge L468
theorem freudenthalTet_sqEdge_eq_periodicDispSqEdge_localEdgeOf L473
theorem canonicalLocalSqEdge_eq_global L484
theorem canonicalLocalEdge_complete L497
def canonicalPeriodicTriangulation L515
def canonicalPeriodicEdgeEquiv L526
def canonicalPeriodicTetEquiv L532
def CanonicalPeriodicEndpointIncidence L542
theorem localEdgeOf_endpoints_match_tetVerts L552
theorem canonicalPeriodicEndpointIncidence L569
def canonicalPeriodicIncidenceConsistent_of_endpoint L590
def canonicalPeriodicIncidenceConsistent L610
structure EncodedPeriodicFreudenthalTorus L620
def canonicalEncodedPeriodicFreudenthalTorus_of_incidence L635
def canonicalEncodedPeriodicFreudenthalTorus_of_endpoint L652
def canonicalEncodedPeriodicFreudenthalTorus L661
theorem canonicalEncodedPeriodic_K_tetVerts_eq L668
theorem canonicalEncodedPeriodic_tetEquiv_eq L677
theorem canonicalEncodedPeriodic_tetVerts_addVertexBits L685
def edgeSlotPartition_of_encodedPeriodicFreudenthalTorus L700
def edgeSlotBookkeeping_of_encodedPeriodicFreudenthalTorus L717