Encyclopedia Geometry Geometry Dihedral Derivatives Has Deriv At Dihedral Angle3 Sq From Cofactors

ARTICLE 3 claims 3 theorems

Geometry Dihedral Derivatives Has Deriv At Dihedral Angle3 Sq From Cofactors

A machine-checked theorem states exactly how a tetrahedron's dihedral angle changes when its edge lengths shift, under specific non-degeneracy conditions.

Verify this page

The derivative theorem

A dihedral angle is the angle between two faces of a tetrahedron, the three-dimensional analogue of the corner angle of a triangle. The theorem in question concerns a tetrahedron whose six edge lengths are allowed to vary along a smooth one-parameter path. It states that the dihedral angle at a chosen edge is a differentiable function of the path parameter, and it gives the exact formula for its rate of change: the derivative equals minus one over the square root of one minus the cosine squared, multiplied by the derivative of the cosine of the angle. This is the standard chain rule for the arccosine function, applied to a cosine that is itself defined through Cayley-Menger cofactors.

The theorem's conditions are precise. The cosine of the dihedral angle must not equal plus or minus one at the base point, which excludes the degenerate cases where the angle is 0 or π (a flat or fully folded tetrahedron). The product of two specific diagonal cofactors must be non-zero, and the denominator of the dihedral cosine must also be non-zero. These are the algebraic counterparts of requiring that the tetrahedron is non-degenerate and that the angle is not at an endpoint of its range. Under these conditions, the theorem provides the derivative formula as a function of the squared edge lengths and the derivatives of the cofactor minors.

In Recognition Science, this theorem is a component in a larger analytic machine. The framework models physical structure through a discrete ledger of recognition events, and here it is establishing the calculus needed for dihedral angles in a geometric setting. The theorem itself is proved in the framework's machine-checked library of formal theorems, meaning every step of the derivation is verified by a computer. It is not an empirical measurement or a conjecture; it is a formal result about the mathematics of tetrahedra.

What the theorem does not claim is equally important. It does not assert that any particular physical tetrahedron exists, nor does it assign values to any edge lengths. It does not prove that the cofactor derivatives themselves exist; those are taken as hypotheses. The theorem is conditional: if the cofactor cosine has a derivative along the path, and if the non-degeneracy conditions hold, then the dihedral angle has the stated derivative. It is a piece of the analytical foundation, not a statement about any specific configuration of matter.

The practical upshot is that anyone working with tetrahedral geometry, whether in classical mechanics or within the Recognition Science framework, now has a verified tool for computing how angles respond to changes in edge lengths. This is the kind of result that makes further geometric and physical derivations possible, providing a reliable link between the algebraic structure of Cayley-Menger determinants and the differential behavior of angles.

THEOREM hasDerivAt_dihedralAngle3Sq_from_cofactors · IndisputableMonolith/Geometry/DihedralDerivatives.lean
hasDerivAt_dihedralAngle3Sq_from_cofactors · IndisputableMonolith/Geometry/DihedralDerivatives.lean:97 
/-- Dihedral angle derivative generated directly from Cayley-Menger cofactor
derivatives for the numerator and the two diagonal denominator cofactors. -/
theorem hasDerivAt_dihedralAngle3Sq_from_cofactors
    {γ : ℝ → CayleyMengerPolynomial.SqEdges} {x num' pp' qq' : ℝ} (e : Fin 6)
    (hnum : HasDerivAt
      (fun t : ℝ =>
        let p := (oppositeCMVertices e).1
        let q := (oppositeCMVertices e).2
        CayleyMengerMatrix.cmCofactor3 (γ t) p q) num' x)
    (hpp : HasDerivAt
      (fun t : ℝ =>
        let p := (oppositeCMVertices e).1
        CayleyMengerMatrix.cmCofactor3 (γ t) p p) pp' x)
    (hqq : HasDerivAt
      (fun t : ℝ =>
        let q := (oppositeCMVertices e).2
        CayleyMengerMatrix.cmCofactor3 (γ t) q q) qq' x)
    (hprod_ne :
      (let p := (oppositeCMVertices e).1
       let q := (oppositeCMVertices e).2
       CayleyMengerMatrix.cmCofactor3 (γ x) p p *
         CayleyMengerMatrix.cmCofactor3 (γ x) q q) ≠ 0)
    (hden_ne : dihedralDenom3 (γ x) e ≠ 0)
    (hm : dihedralCos3Sq (γ x) e ≠ -1)
    (hp : dihedralCos3Sq (γ x) e ≠ 1) :
    HasDerivAt (fun t : ℝ => dihedralAngle3Sq (γ t) e)
      (-(1 / Real.sqrt (1 - (dihedralCos3Sq (γ x) e) ^ 2)) *
        dihedralCos3SqDerivValue γ x num'
          (dihedralDenom3DerivValue γ x pp' qq' e) e) x := by
  exact hasDerivAt_dihedralAngle3Sq_along e
    (hasDerivAt_dihedralCos3Sq_from_cofactors e hnum hpp hqq hprod_ne hden_ne)
    hm hp
THEOREM hasDerivAt_dihedralAngle3Sq_from_cofactors · IndisputableMonolith/Geometry/DihedralDerivatives.lean
hasDerivAt_dihedralAngle3Sq_from_cofactors · IndisputableMonolith/Geometry/DihedralDerivatives.lean:97 
/-- Dihedral angle derivative generated directly from Cayley-Menger cofactor
derivatives for the numerator and the two diagonal denominator cofactors. -/
theorem hasDerivAt_dihedralAngle3Sq_from_cofactors
    {γ : ℝ → CayleyMengerPolynomial.SqEdges} {x num' pp' qq' : ℝ} (e : Fin 6)
    (hnum : HasDerivAt
      (fun t : ℝ =>
        let p := (oppositeCMVertices e).1
        let q := (oppositeCMVertices e).2
        CayleyMengerMatrix.cmCofactor3 (γ t) p q) num' x)
    (hpp : HasDerivAt
      (fun t : ℝ =>
        let p := (oppositeCMVertices e).1
        CayleyMengerMatrix.cmCofactor3 (γ t) p p) pp' x)
    (hqq : HasDerivAt
      (fun t : ℝ =>
        let q := (oppositeCMVertices e).2
        CayleyMengerMatrix.cmCofactor3 (γ t) q q) qq' x)
    (hprod_ne :
      (let p := (oppositeCMVertices e).1
       let q := (oppositeCMVertices e).2
       CayleyMengerMatrix.cmCofactor3 (γ x) p p *
         CayleyMengerMatrix.cmCofactor3 (γ x) q q) ≠ 0)
    (hden_ne : dihedralDenom3 (γ x) e ≠ 0)
    (hm : dihedralCos3Sq (γ x) e ≠ -1)
    (hp : dihedralCos3Sq (γ x) e ≠ 1) :
    HasDerivAt (fun t : ℝ => dihedralAngle3Sq (γ t) e)
      (-(1 / Real.sqrt (1 - (dihedralCos3Sq (γ x) e) ^ 2)) *
        dihedralCos3SqDerivValue γ x num'
          (dihedralDenom3DerivValue γ x pp' qq' e) e) x := by
  exact hasDerivAt_dihedralAngle3Sq_along e
    (hasDerivAt_dihedralCos3Sq_from_cofactors e hnum hpp hqq hprod_ne hden_ne)
    hm hp
THEOREM hasDerivAt_dihedralAngle3Sq_from_cofactors · IndisputableMonolith/Geometry/DihedralDerivatives.lean
hasDerivAt_dihedralAngle3Sq_from_cofactors · IndisputableMonolith/Geometry/DihedralDerivatives.lean:97 
/-- Dihedral angle derivative generated directly from Cayley-Menger cofactor
derivatives for the numerator and the two diagonal denominator cofactors. -/
theorem hasDerivAt_dihedralAngle3Sq_from_cofactors
    {γ : ℝ → CayleyMengerPolynomial.SqEdges} {x num' pp' qq' : ℝ} (e : Fin 6)
    (hnum : HasDerivAt
      (fun t : ℝ =>
        let p := (oppositeCMVertices e).1
        let q := (oppositeCMVertices e).2
        CayleyMengerMatrix.cmCofactor3 (γ t) p q) num' x)
    (hpp : HasDerivAt
      (fun t : ℝ =>
        let p := (oppositeCMVertices e).1
        CayleyMengerMatrix.cmCofactor3 (γ t) p p) pp' x)
    (hqq : HasDerivAt
      (fun t : ℝ =>
        let q := (oppositeCMVertices e).2
        CayleyMengerMatrix.cmCofactor3 (γ t) q q) qq' x)
    (hprod_ne :
      (let p := (oppositeCMVertices e).1
       let q := (oppositeCMVertices e).2
       CayleyMengerMatrix.cmCofactor3 (γ x) p p *
         CayleyMengerMatrix.cmCofactor3 (γ x) q q) ≠ 0)
    (hden_ne : dihedralDenom3 (γ x) e ≠ 0)
    (hm : dihedralCos3Sq (γ x) e ≠ -1)
    (hp : dihedralCos3Sq (γ x) e ≠ 1) :
    HasDerivAt (fun t : ℝ => dihedralAngle3Sq (γ t) e)
      (-(1 / Real.sqrt (1 - (dihedralCos3Sq (γ x) e) ^ 2)) *
        dihedralCos3SqDerivValue γ x num'
          (dihedralDenom3DerivValue γ x pp' qq' e) e) x := by
  exact hasDerivAt_dihedralAngle3Sq_along e
    (hasDerivAt_dihedralCos3Sq_from_cofactors e hnum hpp hqq hprod_ne hden_ne)
    hm hp

What this page does not claim

The theorem does not assert the existence of any specific physical tetrahedron. The theorem does not prove that the cofactor derivatives exist; these are hypotheses. The theorem does not assign values to edge lengths or angles.

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