Encyclopedia Geometry Geometry Schlaefli Tetrahedron Proof Schlaefli Poly Summand Norm Eq Num Div Den

ARTICLE 3 claims 3 theorems

Geometry Schlaefli Tetrahedron Proof Schlaefli Poly Summand Norm Eq Num Div Den

A single algebraic identity converts six complicated geometry terms into one clean common-denominator form, opening a path to a fully explicit tetrahedron formula.

Verify this page

A bridge to a closed form

The Schläfli formula for a tetrahedron relates how its volume changes when an edge length changes to how its six dihedral angles change. The classical formula is a differential relation: as one edge moves, the sum of certain angle-derivative terms equals a volume-derivative term. The Recognition Science library works toward a fully explicit version of this relation, one written as a single closed-form identity rather than as an implicit external field.

The declaration schlaefliPolySummandNorm_eq_num_div_den establishes one algebraic bridge. It states that a normalized summand, the quantity schlaefliPolySummandNorm, equals a numerator divided by a common denominator. The denominator is a product over all six edges of a per-edge factor, and the numerator is a sum over edges of a per-edge polynomial term. The identity holds for every non-degenerate tetrahedron and for every choice of edge index k.

This bridge matters because it turns a sum of six terms, each involving a square root of a squared-edge length, into a single rational expression with a common denominator. The library proves that this common denominator is never zero for a non-degenerate tetrahedron, so the division is always legitimate. The identity is a definitional equality in the framework's machine-checked library of formal theorems, not a derived result with hidden assumptions.

What the declaration does not claim is broader. It does not by itself prove the full closed-form Schläfli theorem for tetrahedra. It is one component in a chain: the bridge identities for each edge, the sum of normalized summands equaling zero, and the polynomial target all feed into the final theorem schlaefliTetrahedronTheorem. The declaration also does not claim anything about tetrahedra with zero volume or degenerate shapes, since the non-degeneracy condition is built into the statement. It makes no claim about the physical meaning of the formula, only about the algebraic identity between the defined quantities.

The practical payoff is that the framework now has a clean algebraic target to aim at. Instead of checking six separate square-root identities, the proof reduces to verifying one polynomial identity and one sum-to-zero statement. That is the difference between a proof that requires case-by-case computation and one that can be checked by a single algebraic calculation.

THEOREM schlaefliPolySummandNorm · IndisputableMonolith/Geometry/SchlaefliTetrahedronProof.lean
schlaefliPolySummandNorm · IndisputableMonolith/Geometry/SchlaefliTetrahedronProof.lean:203 
/-- Rationalized Schläfli summand after using the cofactor discriminant to
remove the arccos radical.  Up to the common nonzero factor
`1 / sqrt (2 * cm3 a)`, the original polynomial-cofactor summand is this
pure rational expression. -/
def schlaefliPolySummandNorm (a : SqEdges) (e k : Fin 6) : ℝ :=
  match e with
  | 0 =>
      let P := CofactorPolynomial.cmCofactor3Poly 3 3 a
      let Q := CofactorPolynomial.cmCofactor3Poly 4 4 a
      let N := CofactorPolynomial.cmCofactor3Poly 3 4 a
      let Pp := CofactorPolynomial.cmCofactorPartial 3 3 k a
      let Qp := CofactorPolynomial.cmCofactorPartial 4 4 k a
      let Np := CofactorPolynomial.cmCofactorPartial 3 4 k a
      (-(2 * Np * P * Q - N * (Pp * Q + P * Qp))) / (2 * P * Q)
  | 1 =>
      let P := CofactorPolynomial.cmCofactor3Poly 2 2 a
      let Q := CofactorPolynomial.cmCofactor3Poly 4 4 a
      let N := CofactorPolynomial.cmCofactor3Poly 2 4 a
      let Pp := CofactorPolynomial.cmCofactorPartial 2 2 k a
      let Qp := CofactorPolynomial.cmCofactorPartial 4 4 k a
      let Np := CofactorPolynomial.cmCofactorPartial 2 4 k a
      (-(2 * Np * P * Q - N * (Pp * Q + P * Qp))) / (2 * P * Q)
  | 2 =>
      let P := CofactorPolynomial.cmCofactor3Poly 2 2 a
      let Q := CofactorPolynomial.cmCofactor3Poly 3 3 a
      let N := CofactorPolynomial.cmCofactor3Poly 2 3 a
      let Pp := CofactorPolynomial.cmCofactorPartial 2 2 k a
      let Qp := CofactorPolynomial.cmCofactorPartial 3 3 k a
      let Np := CofactorPolynomial.cmCofactorPartial 2 3 k a
      (-(2 * Np * P * Q - N * (Pp * Q + P * Qp))) / (2 * P * Q)
  | 3 =>
      let P := CofactorPolynomial.cmCofactor3Poly 1 1 a
      let Q := CofactorPolynomial.cmCofactor3Poly 4 4 a
      let N := CofactorPolynomial.cmCofactor3Poly 1 4 a
      let Pp := CofactorPolynomial.cmCofactorPartial 1 1 k a
      let Qp := CofactorPolynomial.cmCofactorPartial 4 4 k a
      let Np := CofactorPolynomial.cmCofactorPartial 1 4 k a
      (-(2 * Np * P * Q - N * (Pp * Q + P * Qp))) / (2 * P * Q)
  | 4 =>
      let P := CofactorPolynomial.cmCofactor3Poly 1 1 a
      let Q := CofactorPolynomial.cmCofactor3Poly 3 3 a
      let N := CofactorPolynomial.cmCofactor3Poly 1 3 a
      let Pp := CofactorPolynomial.cmCofactorPartial 1 1 k a
      let Qp := CofactorPolynomial.cmCofactorPartial 3 3 k a
      let Np := CofactorPolynomial.cmCofactorPartial 1 3 k a
      (-(2 * Np * P * Q - N * (Pp * Q + P * Qp))) / (2 * P * Q)
  | 5 =>
      let P := CofactorPolynomial.cmCofactor3Poly 1 1 a
      let Q := CofactorPolynomial.cmCofactor3Poly 2 2 a
      let N := CofactorPolynomial.cmCofactor3Poly 1 2 a
      let Pp := CofactorPolynomial.cmCofactorPartial 1 1 k a
      let Qp := CofactorPolynomial.cmCofactorPartial 2 2 k a
      let Np := CofactorPolynomial.cmCofactorPartial 1 2 k a
      (-(2 * Np * P * Q - N * (Pp * Q + P * Qp))) / (2 * P * Q)
THEOREM schlaefliPolySummandNorm · IndisputableMonolith/Geometry/SchlaefliTetrahedronProof.lean
schlaefliPolySummandNorm · IndisputableMonolith/Geometry/SchlaefliTetrahedronProof.lean:203 
/-- Rationalized Schläfli summand after using the cofactor discriminant to
remove the arccos radical.  Up to the common nonzero factor
`1 / sqrt (2 * cm3 a)`, the original polynomial-cofactor summand is this
pure rational expression. -/
def schlaefliPolySummandNorm (a : SqEdges) (e k : Fin 6) : ℝ :=
  match e with
  | 0 =>
      let P := CofactorPolynomial.cmCofactor3Poly 3 3 a
      let Q := CofactorPolynomial.cmCofactor3Poly 4 4 a
      let N := CofactorPolynomial.cmCofactor3Poly 3 4 a
      let Pp := CofactorPolynomial.cmCofactorPartial 3 3 k a
      let Qp := CofactorPolynomial.cmCofactorPartial 4 4 k a
      let Np := CofactorPolynomial.cmCofactorPartial 3 4 k a
      (-(2 * Np * P * Q - N * (Pp * Q + P * Qp))) / (2 * P * Q)
  | 1 =>
      let P := CofactorPolynomial.cmCofactor3Poly 2 2 a
      let Q := CofactorPolynomial.cmCofactor3Poly 4 4 a
      let N := CofactorPolynomial.cmCofactor3Poly 2 4 a
      let Pp := CofactorPolynomial.cmCofactorPartial 2 2 k a
      let Qp := CofactorPolynomial.cmCofactorPartial 4 4 k a
      let Np := CofactorPolynomial.cmCofactorPartial 2 4 k a
      (-(2 * Np * P * Q - N * (Pp * Q + P * Qp))) / (2 * P * Q)
  | 2 =>
      let P := CofactorPolynomial.cmCofactor3Poly 2 2 a
      let Q := CofactorPolynomial.cmCofactor3Poly 3 3 a
      let N := CofactorPolynomial.cmCofactor3Poly 2 3 a
      let Pp := CofactorPolynomial.cmCofactorPartial 2 2 k a
      let Qp := CofactorPolynomial.cmCofactorPartial 3 3 k a
      let Np := CofactorPolynomial.cmCofactorPartial 2 3 k a
      (-(2 * Np * P * Q - N * (Pp * Q + P * Qp))) / (2 * P * Q)
  | 3 =>
      let P := CofactorPolynomial.cmCofactor3Poly 1 1 a
      let Q := CofactorPolynomial.cmCofactor3Poly 4 4 a
      let N := CofactorPolynomial.cmCofactor3Poly 1 4 a
      let Pp := CofactorPolynomial.cmCofactorPartial 1 1 k a
      let Qp := CofactorPolynomial.cmCofactorPartial 4 4 k a
      let Np := CofactorPolynomial.cmCofactorPartial 1 4 k a
      (-(2 * Np * P * Q - N * (Pp * Q + P * Qp))) / (2 * P * Q)
  | 4 =>
      let P := CofactorPolynomial.cmCofactor3Poly 1 1 a
      let Q := CofactorPolynomial.cmCofactor3Poly 3 3 a
      let N := CofactorPolynomial.cmCofactor3Poly 1 3 a
      let Pp := CofactorPolynomial.cmCofactorPartial 1 1 k a
      let Qp := CofactorPolynomial.cmCofactorPartial 3 3 k a
      let Np := CofactorPolynomial.cmCofactorPartial 1 3 k a
      (-(2 * Np * P * Q - N * (Pp * Q + P * Qp))) / (2 * P * Q)
  | 5 =>
      let P := CofactorPolynomial.cmCofactor3Poly 1 1 a
      let Q := CofactorPolynomial.cmCofactor3Poly 2 2 a
      let N := CofactorPolynomial.cmCofactor3Poly 1 2 a
      let Pp := CofactorPolynomial.cmCofactorPartial 1 1 k a
      let Qp := CofactorPolynomial.cmCofactorPartial 2 2 k a
      let Np := CofactorPolynomial.cmCofactorPartial 1 2 k a
      (-(2 * Np * P * Q - N * (Pp * Q + P * Qp))) / (2 * P * Q)
THEOREM schlaefliCommonDenom_ne_zero · IndisputableMonolith/Geometry/SchlaefliTetrahedronProof.lean
schlaefliCommonDenom_ne_zero · IndisputableMonolith/Geometry/SchlaefliTetrahedronProof.lean:308 
/-- The common denominator is nonzero on a nondegenerate tetrahedron. -/
theorem schlaefliCommonDenom_ne_zero
    (T : NonDegenerateTet) :
    schlaefliCommonDenom T.sqEdge ≠ 0 := by
  unfold schlaefliCommonDenom
  exact Finset.prod_ne_zero_iff.mpr (by
    intro e _
    exact schlaefliPolySummandDen_ne_zero T e)

What this page does not claim

The declaration does not by itself prove the full closed-form Schläfli theorem for tetrahedra. The declaration makes no claim about degenerate or zero-volume tetrahedra. The declaration says nothing about the physical interpretation of the formula.

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