Encyclopedia Gravity Gravity Analysis Regge Ttderivative Gate Has Deriv At Flat Angle Directional

ARTICLE 3 claims 3 theorems

Gravity Analysis Regge Ttderivative Gate Has Deriv At Flat Angle Directional

A machine-checked theorem proves that the angles of a single flat tetrahedron respond smoothly to small changes in its edge lengths, a precise local step in a larger unfinished program.

Verify this page

A local differentiability result

In the geometry of a tetrahedron, a dihedral angle is the angle between two faces meeting along an edge. The declaration hasDerivAt_flatAngle_directional concerns one specific tetrahedron: the regular one, where all six edges have equal length. The theorem states that if you begin with this regular shape and nudge each of its six edge lengths by a small amount, each of its six dihedral angles changes in a way that is differentiable. More precisely, the rate of change of any angle along any such nudge is a weighted sum of the edge-length changes, with weights given by a precomputed table called the flat angle Jacobian. This is a statement about a single tetrahedron at a single point, not about a whole lattice or a continuum.

The proof is not a numerical approximation. It is a kernel-checked theorem in the framework's machine-checked library of formal theorems, built from the standard trio of axioms [propext, Classical.choice, Quot.sound], with no unproven assumptions. A companion theorem, hasDerivAt_flatWeightedAngleSum, shows that a particular weighted sum of the angles, weighted by the square roots of the edge lengths, is also differentiable at the flat point, and its derivative is simply the sum of the edge-length changes times the angle values. The reason the angle-derivative terms cancel exactly is a proved identity called the tetrahedral Schläfli identity, not a numerical coincidence.

This result is one small gate in a larger program that aims to study a certain action built from tetrahedra on a periodic lattice. The program's ultimate goal is to understand the continuum limit of this action, and whether it has a property called isotropy, meaning it looks the same in all directions. This theorem is a necessary local ingredient for that goal, but it is far from the whole story.

The declaration does not claim that the second derivative of the plane-wave action profile exists; that is a later stage of the program and remains open. It does not claim anything about the sum over the periodic lattice, since everything here is per-tetrahedron. It does not prove the value of the continuum symbol, which remains numerical evidence only, nor does it prove the isotropy target, which remains open. The theorem is a precise, local, first-derivative statement, and that is all.

THEOREM hasDerivAt_flatAngle_directional · IndisputableMonolith/Gravity/Analysis/ReggeTTDerivativeGate.lean
hasDerivAt_flatAngle_directional · IndisputableMonolith/Gravity/Analysis/ReggeTTDerivativeGate.lean:493 
/-- Directional derivative of one flat dihedral angle (THEOREM): along the
affine path `t ↦ a + t·v` through the flat tuple, the `f`-th dihedral angle
has derivative `∑_k v_k · flatAngleJacobian f k` at `t = 0`.  The
directional derivative is assembled from the six proved coordinate partial
derivatives through the `C¹` Fréchet derivative at the flat point. -/
theorem hasDerivAt_flatAngle_directional (v : Fin 6 → ℝ) (f : Fin 6) :
    HasDerivAt
      (fun t : ℝ =>
        dihedralAngle3Sq (fun j : Fin 6 => freudenthalTetSqEdges j + t * v j) f)
      (∑ k : Fin 6, v k * flatAngleJacobian f k) 0 := by
  have hC : ContDiffAt ℝ 1 (fun x : SqEdges => dihedralAngle3Sq x f)
      freudenthalTetSqEdges :=
    Geometry.ReggeActionFirstVariation.dihedralAngle3Sq_contDiffAt_nonDegenerate
      freudenthalTet f 1 (flatCos_ne_endpoints f)
  have hDiff : DifferentiableAt ℝ (fun x : SqEdges => dihedralAngle3Sq x f)
      freudenthalTetSqEdges :=
    hC.differentiableAt (by simp)
  have hF : HasFDerivAt (fun x : SqEdges => dihedralAngle3Sq x f)
      (fderiv ℝ (fun x : SqEdges => dihedralAngle3Sq x f) freudenthalTetSqEdges)
      freudenthalTetSqEdges :=
    hDiff.hasFDerivAt
  have hγ : HasDerivAt
      (fun t : ℝ => (fun j : Fin 6 => freudenthalTetSqEdges j + t * v j)) v 0 := by
    rw [hasDerivAt_pi]
    intro j
    simpa using
      ((hasDerivAt_id (0 : ℝ)).mul_const (v j)).const_add (freudenthalTetSqEdges j)
  have hF' : HasFDerivAt (fun x : SqEdges => dihedralAngle3Sq x f)
      (fderiv ℝ (fun x : SqEdges => dihedralAngle3Sq x f) freudenthalTetSqEdges)
      (fun j : Fin 6 => freudenthalTetSqEdges j + (0 : ℝ) * v j) := by
    simpa using hF
  have hcomp := HasFDerivAt.comp_hasDerivAt (x := (0 : ℝ))
    (f := fun t : ℝ => (fun j : Fin 6 => freudenthalTetSqEdges j + t * v j))
    hF' hγ
  have hvalue :
      (fderiv ℝ (fun x : SqEdges => dihedralAngle3Sq x f) freudenthalTetSqEdges) v =
        ∑ k : Fin 6, v k * flatAngleJacobian f k := by
    rw [Geometry.ReggeActionFirstVariation.continuousLinearMap_apply_eq_sum_single]
    refine Finset.sum_congr rfl fun k _ => ?_
    exact congrArg (fun z => v k * z)
      (Geometry.ReggeActionFirstVariation.fderiv_dihedralAngle3Sq_apply_single
        freudenthalTet f k (flatCos_ne_endpoints f))
  rw [hvalue] at hcomp
  simpa [Function.comp_def] using hcomp
THEOREM hasDerivAt_flatAngle_directional · IndisputableMonolith/Gravity/Analysis/ReggeTTDerivativeGate.lean
hasDerivAt_flatAngle_directional · IndisputableMonolith/Gravity/Analysis/ReggeTTDerivativeGate.lean:493 
/-- Directional derivative of one flat dihedral angle (THEOREM): along the
affine path `t ↦ a + t·v` through the flat tuple, the `f`-th dihedral angle
has derivative `∑_k v_k · flatAngleJacobian f k` at `t = 0`.  The
directional derivative is assembled from the six proved coordinate partial
derivatives through the `C¹` Fréchet derivative at the flat point. -/
theorem hasDerivAt_flatAngle_directional (v : Fin 6 → ℝ) (f : Fin 6) :
    HasDerivAt
      (fun t : ℝ =>
        dihedralAngle3Sq (fun j : Fin 6 => freudenthalTetSqEdges j + t * v j) f)
      (∑ k : Fin 6, v k * flatAngleJacobian f k) 0 := by
  have hC : ContDiffAt ℝ 1 (fun x : SqEdges => dihedralAngle3Sq x f)
      freudenthalTetSqEdges :=
    Geometry.ReggeActionFirstVariation.dihedralAngle3Sq_contDiffAt_nonDegenerate
      freudenthalTet f 1 (flatCos_ne_endpoints f)
  have hDiff : DifferentiableAt ℝ (fun x : SqEdges => dihedralAngle3Sq x f)
      freudenthalTetSqEdges :=
    hC.differentiableAt (by simp)
  have hF : HasFDerivAt (fun x : SqEdges => dihedralAngle3Sq x f)
      (fderiv ℝ (fun x : SqEdges => dihedralAngle3Sq x f) freudenthalTetSqEdges)
      freudenthalTetSqEdges :=
    hDiff.hasFDerivAt
  have hγ : HasDerivAt
      (fun t : ℝ => (fun j : Fin 6 => freudenthalTetSqEdges j + t * v j)) v 0 := by
    rw [hasDerivAt_pi]
    intro j
    simpa using
      ((hasDerivAt_id (0 : ℝ)).mul_const (v j)).const_add (freudenthalTetSqEdges j)
  have hF' : HasFDerivAt (fun x : SqEdges => dihedralAngle3Sq x f)
      (fderiv ℝ (fun x : SqEdges => dihedralAngle3Sq x f) freudenthalTetSqEdges)
      (fun j : Fin 6 => freudenthalTetSqEdges j + (0 : ℝ) * v j) := by
    simpa using hF
  have hcomp := HasFDerivAt.comp_hasDerivAt (x := (0 : ℝ))
    (f := fun t : ℝ => (fun j : Fin 6 => freudenthalTetSqEdges j + t * v j))
    hF' hγ
  have hvalue :
      (fderiv ℝ (fun x : SqEdges => dihedralAngle3Sq x f) freudenthalTetSqEdges) v =
        ∑ k : Fin 6, v k * flatAngleJacobian f k := by
    rw [Geometry.ReggeActionFirstVariation.continuousLinearMap_apply_eq_sum_single]
    refine Finset.sum_congr rfl fun k _ => ?_
    exact congrArg (fun z => v k * z)
      (Geometry.ReggeActionFirstVariation.fderiv_dihedralAngle3Sq_apply_single
        freudenthalTet f k (flatCos_ne_endpoints f))
  rw [hvalue] at hcomp
  simpa [Function.comp_def] using hcomp
THEOREM flatAngleJacobian_schlaefli · IndisputableMonolith/Gravity/Analysis/ReggeTTDerivativeGate.lean
flatAngleJacobian_schlaefli · IndisputableMonolith/Gravity/Analysis/ReggeTTDerivativeGate.lean:484 
/-- SCHLÄFLI CANCELLATION AT FLAT (THEOREM): for every squared-edge
coordinate `k`, `∑_f √(a_f) · flatAngleJacobian f k = 0` at the flat tuple.
This is the proved six-edge closed-form tetrahedral Schläfli identity
(`tetraSchlaefliSixEdgeClosedForm`) instantiated at the Freudenthal
tetrahedron and written in stencil vocabulary. -/
theorem flatAngleJacobian_schlaefli (k : Fin 6) :
    (∑ f : Fin 6, Real.sqrt (freudenthalTetSqEdges f) * flatAngleJacobian f k) = 0 :=
  Geometry.SchlaefliTetrahedronProof.tetraSchlaefliSixEdgeClosedForm freudenthalTet k

What this page does not claim

The theorem does not prove the existence of second derivatives of the action profile. The theorem does not make any statement about a sum over a lattice or a continuum limit. The theorem does not establish the value of the continuum symbol or the isotropy target.

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/Gravity/Analysis/ReggeTTDerivativeGate.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