module module

`IndisputableMonolith.Geometry.SchlaefliTetrahedronProof`

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

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Geometry.ReggeActionFirstVariation module_import
IndisputableMonolith.Geometry.Triangulation3DConsistency module_import
IndisputableMonolith.Gravity.FreudenthalLengthChainEndpointCert module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Geometry.AffineIndepInterior module_import
IndisputableMonolith.Geometry.DihedralDerivatives module_import
IndisputableMonolith.Geometry.SchlaefliTetrahedron module_import

declarations in this module (45)

def volume3ClosedDerivSq L29
theorem hasDerivAt_volume3ClosedDerivSq L34
def dihedralClosedDerivSq L55
def dihedralClosedDerivSqPoly L61
theorem dihedralClosedDerivSq_eq_poly L65
theorem hasDerivAt_sqEdgeCoordinate_from_edgeLength L75
def volume3ClosedDerivLength L83
theorem hasDerivAt_volume3ClosedDerivLength L88
def dihedralClosedDerivLength L108
theorem hasDerivAt_dihedralClosedDerivLength L114
def TetraSchlaefliClosedEquationSq L145
def TetraSchlaefliClosedEquation L152
theorem TetraSchlaefliClosedEquation_of_sq L160
def SchlaefliTetrahedronClosedFormTarget L184
def TetraSchlaefliSixEdgeClosedFormTarget L190
def TetraSchlaefliSixEdgePolynomialTarget L197
def schlaefliPolySummandNorm L207
def schlaefliPolySummandNum L259
def schlaefliPolySummandDen L271
theorem schlaefliPolySummandNorm_eq_num_div_den L278
def schlaefliCommonDenom L287
def schlaefliCommonNumerator L291
theorem schlaefliPolySummandDen_ne_zero L298
theorem schlaefliCommonDenom_ne_zero L309
def SchlaefliCommonNumeratorTarget L319
def SchlaefliPolySummandNormSumTarget L326
theorem sum_fin6_real L331
theorem schlaefliPolySummandNorm_sum_eq_zero L347
def SchlaefliSummandBridgeTarget L387
theorem schlaefli_summand_bridge_edge0 L395
theorem schlaefli_summand_bridge_edge1 L453
theorem schlaefli_summand_bridge_edge2 L510
theorem schlaefli_summand_bridge_edge3 L567
theorem schlaefli_summand_bridge_edge4 L624
theorem schlaefli_summand_bridge_edge5 L681
theorem schlaefliSummandBridge L739
theorem tetraSchlaefliSixEdgePolynomial L751
theorem sixEdgeClosedForm_of_polynomial L770
theorem schlaefliClosedForm_of_sixEdgeSq L784
theorem schlaefliTetrahedronTheorem_of_sixEdgeSq L794
def tetraSchlaefliDerivativeData_closedForm L805
theorem schlaefliTetrahedronTheorem_of_closedForm L815
theorem tetraSchlaefliSixEdgeClosedForm L822
theorem schlaefliTetrahedronClosedForm L827
theorem schlaefliTetrahedronTheorem L833