Geometry Schlaefli Tetrahedron Proof Schlaefli Tetrahedron Theorem Of Closed For

The closed-form bridge

The Schläfli relation is a classical differential formula from 1858. For a tetrahedron, it states that the change in volume relates to the dihedral angles and the lengths of the six edges. The formula is dihedral angle, the angle between two faces, and it connects a small change in that angle to a proportional change in volume. The classical proof is analytic, relying on limits and derivatives.

What the Recognition Science framework contributes is a different route. Its machine-checked library of formal theorems establishes that the same relation holds exactly, without any limiting process. The proof works by expressing the volume and the dihedral angles as algebraic functions of the six squared edge lengths. It then shows that a certain polynomial, built from these functions, is identically zero. The declaration schlaefliTetrahedronTheorem_of_closedForm is the final step: it takes this closed-form polynomial identity and derives the full Schläfli relation for every non-degenerate tetrahedron. A non-degenerate tetrahedron is one with positive volume, so its vertices are not coplanar.

The proof is organized in stages. The library first defines explicit formulas for the derivative of volume with respect to each squared edge length, and for the derivative of each dihedral angle. These formulas are not limits; they are exact algebraic expressions. The core target, SchlaefliTetrahedronClosedFormTarget, states that a certain sum over the six edges equals zero. The library proves this by converting each term into a common polynomial form. Six bridge theorems, one for each edge, connect the geometric derivatives to the polynomial summands. A final theorem, schlaefliPolySummandNorm_sum_eq_zero, shows that the sum of these polynomial summands is zero. The declaration then assembles these pieces into the full theorem.

In Recognition Science, this result is a step toward a larger goal. The framework seeks to derive physical and geometric structure from a single cost function, and this proof is part of that program. But the theorem itself is purely geometric. It does not depend on any physical constants or on the framework's other results. It is a complete statement about tetrahedra.

The theorem does not claim that the Schläfli relation is new. The relation has been known since the nineteenth century. What is new is the method: a fully formal, algebraic proof that avoids calculus. The theorem also does not claim that the closed-form expression is the most efficient way to compute anything. It is a proof of existence, not a computational recipe. Finally, the theorem does not extend to higher-dimensional simplices or to curved spaces. It is specifically about tetrahedra in flat three-dimensional space.

/-- A closed-form Schläfli proof discharges the existing tetrahedral
Schläfli theorem target. -/
theorem schlaefliTetrahedronTheorem_of_closedForm
    (h : SchlaefliTetrahedronClosedFormTarget) :
    SchlaefliTetrahedronTheorem := by
  intro T
  exact ⟨tetraSchlaefliDerivativeData_closedForm T (h T)⟩

/-- Determinant-cofactor six-edge Schläfli identity. -/
theorem tetraSchlaefliSixEdgeClosedForm :
    TetraSchlaefliSixEdgeClosedFormTarget :=
  sixEdgeClosedForm_of_polynomial tetraSchlaefliSixEdgePolynomial

/-- 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 claim that the Schläfli relation is a new discovery. The theorem does not claim the closed-form expression is computationally efficient. The theorem does not extend to higher-dimensional simplices or curved spaces.

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: