module module

`IndisputableMonolith.Geometry.PeriodicFreudenthalTorus4D`

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.Gap2FreudenthalPeriodDoubling4D module_import

declarations in this module (69)

def bit L48
def addBit L52
theorem addBit_false L55
theorem addBit_true_eq_mk L60
theorem addBit_false_after_true L65
theorem addBit_true_after_false L69
theorem addBit_true_ne_self L73
theorem addBit_true_injective L89
theorem addBit_injective L120
theorem addBit4_cancel L129
theorem two_bit_steps_ne_id L155
abbrev Vertex4 L187
def addBits4 L190
theorem addBits4_injective L193
theorem addBits4_cancel_offsets L204
def dispBits4 L224
theorem dispBits4_ne_zero L241
theorem dispBits4_injective L246
theorem displacement_classes_are_fifteen L252
def vertexBits4 L263
theorem vertexBits4_injective L281
def addVertexBits4 L285
theorem addVertexBits4_injective L289
structure PeriodicEdge4 L299
theorem card_vertex4 L330
def periodicEdge4EquivProd L336
theorem card_periodicEdge4 L345
def kuhnVerts L361
def edgeSlotPair L486
def kuhnEdgeBase L501
def kuhnEdgeDisp L748
abbrev PeriodicSimplex4 L993
theorem card_periodicSimplex4 L997
theorem kuhn_simplex_count_per_cube L1004
theorem kuhnVerts_zero L1009
theorem kuhnVerts_four L1013
theorem kuhnVerts_label_injective L1017
def localEdgeOf4 L1022
def kuhnCornerAt L1027
theorem localEdgeOf4_endpoints_match_kuhnVerts L1037
theorem kuhn_corners_injective L1050
def pairSlot4 L1071
theorem pairSlot4_spec L1085
def vertexFinEquiv4 L1095
def edgeFinEquiv4 L1100
def simplexFinEquiv4 L1105
def canonicalEdgeVerts4 L1111
def canonicalSimplexVerts4 L1121
def sameUnorderedPair4 L1131
structure Carrier4D L1138
def IsSimplicial4D L1149
def canonicalCarrier4D L1159
theorem canonicalCarrier4D_nV L1167
theorem canonicalCarrier4D_nE L1172
theorem canonicalCarrier4D_nS L1177
theorem canonicalCarrier4D_no_loops L1181
theorem endpoints_injective4 L1192
theorem reverse_impossible4 L1215
theorem canonicalCarrier4D_no_multiedges L1240
theorem canonicalCarrier4D_simplex_injective L1270
theorem canonicalCarrier4D_skeleton L1284
theorem canonicalCarrier4D_isSimplicial L1321
def dispWeight4 L1331
def periodicDispSqEdge4 L1350
theorem dispWeight4_le_four L1353
theorem periodicDispSqEdge4_le_four L1356
def meshVal4D L1364
theorem meshVal4D_pos L1367
theorem meshVal4D_attained L1373