module module

`IndisputableMonolith.Gravity.SevenGaps.Gap2FreudenthalPeriodDoubling4D`

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

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Geometry.PeriodicFreudenthalTorus4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeEdgeStencil4D module_import

declarations in this module (28)

instance instNeZero_two_mul L50
def reduceMod L54
theorem reduceMod_val L57
theorem reduceMod_addBit L62
theorem reduceMod_of_lt L74
def periodDoublingVertexMap4D L81
theorem periodDoublingVertexMap4D_addBits4 L88
theorem periodDoublingVertexMap4D_addVertexBits4 L96
theorem freudenthal4D_period_doubling_vertex_map L105
def periodDoublingEdgeMap4D L118
theorem periodDoublingEdgeMap4D_endpoints L123
theorem periodDoublingEdgeMap4D_dispSq_eq L137
theorem freudenthal4D_period_doubling_edge_control L149
def kuhnVertexSet L162
theorem kuhnVertexSet_card L166
theorem freudenthal4D_period_doubling_simplicial_map L180
theorem freudenthal4D_period_doubling_simplicial_witness L203
def embedDouble L215
def liftEdgeDoubled4D L223
theorem liftEdgeDoubled4D_disp L230
theorem liftEdge4D_is_section L237
theorem liftEdgeDoubled4D_injective L270
theorem periodDoubling4D_class_copy L281
theorem dispBits4_eq_classBit L295
theorem dispWeight4_eq_classWeightNat L301
theorem periodicDispSqEdge4_eq_classDispSq L309
def freudenthal4D_period_doubling_package L321
theorem freudenthal4D_period_doubling_package_holds L339