IndisputableMonolith.Cosmology.LatticeBallEdges

declarations in this module (22)

• def dirs L51
• theorem dirs_card L53
• def E L57
• def Dset L62
• theorem boundary_xpos L67
• theorem boundary_xneg L85
• theorem boundary_ypos L103
• theorem boundary_yneg L121
• theorem step_card L140
• theorem Dset_card L168
• theorem total_edge_card L182
• theorem edges_length L232
• def carried L241
• theorem carried_edge_card L248
• theorem interface_sq_le_total L270
• theorem carried_ge_interface L281
• theorem boundary_zpos L394
• theorem boundary_zneg L414
• theorem three_mul_step_card L435
• theorem three_mul_Dset_card L474
• theorem three_mul_total_edge_card L489
• theorem interface_cube_le_total_sq L581