Geometry Schlaefli Tetrahedron Proof

The tetrahedron's closed form

The Schläfli formula relates the change in a polyhedron's volume to the changes in its dihedral angles, the angles between faces. For a tetrahedron, the simplest polyhedron with four triangular faces, this relation is a sum over its six edges. The classical problem is to express the derivative of volume with respect to an edge length in a fully explicit, closed form, free of implicit or external fields.

This result establishes exactly that. It proves, in a machine-checked library of formal theorems, that for any non-degenerate tetrahedron, the derivative of volume with respect to any of its six edge lengths equals a sum of terms involving the derivative of the dihedral angle. The proof is constructive: it derives a polynomial expression for each summand and then shows the total sum vanishes. The final theorem, schlaefliTetrahedronTheorem, states that the closed-form equation holds for all non-degenerate tetrahedra.

The key step is a reduction to a single polynomial identity. A normalized polynomial is defined for each edge, and it is proved that the sum of these six polynomials is zero. This identity, schlaefliPolySummandNorm_sum_eq_zero, is the hard content. Once it is established, the bridge theorems for each edge connect the polynomial summands to the dihedral derivative terms, completing the proof.

In Recognition Science, this result is part of a broader program. The framework models physical structure from a ledger of recognition events, and it derives constants like the golden ratio and the number of spatial dimensions from a forcing chain. This result, however, is a self-contained geometric theorem. It does not depend on the framework's axioms; it is a classical result proved with full rigor. Its role is to provide a clean, closed-form foundation for geometric quantities that the framework may later use.

The practical consequence is that the derivative of a tetrahedron's volume is no longer an implicit quantity. It is a concrete, computable expression in terms of the six edge lengths and the Cayley-Menger determinant. This removes a major obstacle for any further analysis that requires differentiating volume, whether in the framework or in classical geometry.

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

/-- 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

This module does not derive the Schläfli formula itself; it proves a closed-form version for the tetrahedron. The result does not depend on or imply any Recognition Science axioms or constants. No claim is made about the physical interpretation of the derivative within the framework.

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: