Geometry Schlaefli Tetrahedron Proof Schlaefli Tetrahedron Theorem Of Six Edge S

The six-edge theorem

A tetrahedron is a pyramid with four triangular faces, six edges, and four vertices. Its shape is fully determined by the six edge lengths, and from those lengths one can compute its volume and its six dihedral angles, the angles between pairs of faces. The Schläfli formula is a classical relation describing how the volume changes when the shape is deformed: the change in volume equals a sum over the six edges of a length times the change in the corresponding dihedral angle.

What the machine-checked theorem schlaefliTetrahedronTheorem_of_sixEdgeSq establishes is a closed-form version of this relation. It proves that for any non-degenerate tetrahedron, the sum over all six edges of the square root of the edge length times the derivative of the dihedral angle with respect to a squared-edge coordinate is exactly zero. This is a precise algebraic identity, not an approximation. The proof works by expressing each term in the sum as a rational function of the edge lengths, combining them over a common denominator, and showing the numerator vanishes identically.

The theorem is proved in the framework's machine-checked library of formal theorems, meaning every step is verified by a computer. The chain of reasoning starts with explicit formulas for the volume and dihedral angles in terms of Cayley-Menger determinants, then derives the derivative of the volume with respect to each squared-edge coordinate, and finally shows the six-edge sum collapses to zero. The result holds for all non-degenerate tetrahedra, those with positive volume, with no further restrictions.

What the declaration does not claim is any statement about the fine-structure constant, the Riemann Hypothesis, or any other physical constant. It is purely a geometric identity. It also does not claim that the Schläfli formula itself is new; the classical formula is a known result. What is new is the closed-form, machine-checked proof of the six-edge sum identity, which reduces the hard content to a single algebraic identity that can be verified by computation.

/-- The local tetrahedral Schläfli derivative-data package is now constructed
from the explicit cofactor formulas. -/
theorem schlaefliTetrahedronTheorem :
    SchlaefliTetrahedronTheorem :=
  schlaefliTetrahedronTheorem_of_closedForm schlaefliTetrahedronClosedForm

/-- The rationalized six-edge Schläfli sums vanish. -/
theorem schlaefliPolySummandNorm_sum_eq_zero :
    SchlaefliPolySummandNormSumTarget := by
  intro T k
  rw [sum_fin6_real]
  have h0p := CofactorDerivatives.dihedralCofactorProductPoly_ne_zero_of_nonDegenerate T 0
  have h1p := CofactorDerivatives.dihedralCofactorProductPoly_ne_zero_of_nonDegenerate T 1
  have h5p := CofactorDerivatives.dihedralCofactorProductPoly_ne_zero_of_nonDegenerate T 5
  simp [CofactorDerivatives.dihedralCofactorProductPoly,
    DihedralCayleyMenger.oppositeCMVertices] at h0p h1p h5p
  have h33 : CofactorPolynomial.cmCofactor3Poly 3 3 T.sqEdge ≠ 0 := h0p.1
  have h44 : CofactorPolynomial.cmCofactor3Poly 4 4 T.sqEdge ≠ 0 := h0p.2
  have h22 : CofactorPolynomial.cmCofactor3Poly 2 2 T.sqEdge ≠ 0 := h1p.1
  have h11 : CofactorPolynomial.cmCofactor3Poly 1 1 T.sqEdge ≠ 0 := h5p.1
  let D : ℝ :=
    CofactorPolynomial.cmCofactor3Poly 1 1 T.sqEdge *
      CofactorPolynomial.cmCofactor3Poly 2 2 T.sqEdge *
      CofactorPolynomial.cmCofactor3Poly 3 3 T.sqEdge *
      CofactorPolynomial.cmCofactor3Poly 4 4 T.sqEdge
  have hD : D ≠ 0 := by
    unfold D
    exact mul_ne_zero (mul_ne_zero (mul_ne_zero h11 h22) h33) h44
  have hmul :
      D * (schlaefliPolySummandNorm T.sqEdge 0 k +
          schlaefliPolySummandNorm T.sqEdge 1 k +
          schlaefliPolySummandNorm T.sqEdge 2 k +
          schlaefliPolySummandNorm T.sqEdge 3 k +
          schlaefliPolySummandNorm T.sqEdge 4 k +
          schlaefliPolySummandNorm T.sqEdge 5 k) = 0 := by
    fin_cases k <;>
      unfold D schlaefliPolySummandNorm <;>
      field_simp [h11, h22, h33, h44] <;>
      simp [CofactorPolynomial.cmCofactor3Poly, CofactorPolynomial.cmCofactorPartial] <;>
      ring_nf
  exact (mul_eq_zero.mp hmul).resolve_left hD

What this page does not claim

The theorem does not prove any statement about physical constants such as the fine-structure constant. The theorem does not claim the Schläfli formula is new; it provides a machine-checked proof of a six-edge sum identity. The theorem does not apply to degenerate tetrahedra with zero volume.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Geometry/SchlaefliTetrahedronProof.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: