module module

`IndisputableMonolith.Verification.CubeGeometryCert`

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

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants.AlphaDerivation module_import

declarations in this module (4)

structure CubeGeometryCert L48
theorem magic_numbers_from_D3 L123
theorem eight_tick_is_cube_vertices L133
theorem eleven_enters_geometric_seed L137