module module

`IndisputableMonolith.Gravity.FreudenthalLengthChainEndpointCert`

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

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Geometry.FreudenthalCubeTriangulation module_import
IndisputableMonolith.Geometry.SchlaefliTetrahedronProof module_import

declarations in this module (39)

def freudenthalSchlaefliPolySummandNormTable L24
theorem snorm_zero_0_0 L64
theorem snorm_zero_0_1 L72
theorem snorm_zero_0_2 L80
theorem snorm_zero_0_3 L88
theorem snorm_0_4 L96
theorem snorm_0_5 L104
theorem snorm_zero_1_0 L112
theorem snorm_1_1 L120
theorem snorm_1_2 L128
theorem snorm_1_3 L136
theorem snorm_1_4 L144
theorem snorm_1_5 L152
theorem snorm_zero_2_0 L160
theorem snorm_2_1 L168
theorem snorm_2_2 L176
theorem snorm_2_3 L184
theorem snorm_2_4 L192
theorem snorm_zero_2_5 L200
theorem snorm_zero_3_0 L208
theorem snorm_3_1 L216
theorem snorm_3_2 L224
theorem snorm_3_3 L232
theorem snorm_3_4 L240
theorem snorm_zero_3_5 L248
theorem snorm_4_0 L256
theorem snorm_4_1 L264
theorem snorm_4_2 L272
theorem snorm_4_3 L280
theorem snorm_4_4 L288
theorem snorm_zero_4_5 L296
theorem snorm_5_0 L304
theorem snorm_5_1 L312
theorem snorm_zero_5_2 L320
theorem snorm_zero_5_3 L328
theorem snorm_zero_5_4 L336
theorem snorm_zero_5_5 L344
theorem freudenthalSchlaefliPolySummandNorm_eq_table L353
theorem freudenthalDihedralClosedDerivLength_snorm L395