Encyclopedia Geometry Geometry Schlaefli Tetrahedron Proof Schlaefli Poly Summand Norm Sum Eq Zero

ARTICLE 2 claims 2 theorems

Geometry Schlaefli Tetrahedron Proof Schlaefli Poly Summand Norm Sum Eq Zero

A theorem in the framework's machine-checked library shows that six carefully weighted terms, one for each edge of a tetrahedron, always add to zero.

Verify this page

A zero sum in the tetrahedron

A tetrahedron, the simplest three-dimensional solid, has four triangular faces and six edges. In 1852 the geometer Ludwig Schläfli proved a relation for such shapes: if you gently change the lengths of the edges, a certain combination of the changes in the dihedral angles (the angles between faces) and the changes in the volume always balance to zero. This is the Schläfli differential relation, a classical tool in geometry.

The Recognition Science framework's machine-checked library of formal theorems contains a declaration named schlaefliPolySummandNorm_sum_eq_zero. In plain language, this theorem states that for any non-degenerate tetrahedron, and for any one of its six edges, the sum over all six edges of a particular weighted term is exactly zero. Each term is built from the squared edge lengths and the cofactors of the Cayley-Menger matrix, a matrix whose determinant gives the square of the volume. The theorem is a formal, machine-checked proof of this zero-sum identity.

The declaration is part of a larger proof effort. The library also proves a closed-form expression for the derivative of the volume with respect to a squared edge length, and a polynomial version of the Schläfli relation. The schlaefliPolySummandNorm_sum_eq_zero theorem is a key step in showing that the classical Schläfli relation holds for all tetrahedra, expressed in a closed, algebraic form.

In Recognition Science, this result is not about the framework's core ideas like recognition or ledgers. It is a piece of pure geometry, formalized and verified. The theorem does not claim that the Schläfli relation is new, nor does it claim anything about the physical universe. It is a mathematical fact, proved in a formal system, about the geometry of tetrahedra.

THEOREM schlaefliPolySummandNorm_sum_eq_zero · IndisputableMonolith/Geometry/SchlaefliTetrahedronProof.lean
schlaefliPolySummandNorm_sum_eq_zero · IndisputableMonolith/Geometry/SchlaefliTetrahedronProof.lean:346 
/-- 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
THEOREM schlaefliPolySummandNorm_sum_eq_zero · IndisputableMonolith/Geometry/SchlaefliTetrahedronProof.lean
schlaefliPolySummandNorm_sum_eq_zero · IndisputableMonolith/Geometry/SchlaefliTetrahedronProof.lean:346 
/-- 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. It does not claim any physical consequence or connection to the Recognition Science framework's core concepts. It does not claim that the zero-sum identity holds for degenerate tetrahedra.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND