Gravity Analysis Regge Ttderivative Gate Has Deriv At Flat Sqrt Edge Directional

The flat-edge derivative

In the Regge calculus approach to gravity, spacetime is chopped into flat tetrahedral pieces, and the action that governs the geometry is built from the lengths of their edges. A central quantity is the square root of each squared edge length, written √a. The theorem hasDerivAt_flatSqrtEdge_directional states a precise, local fact: at the special flat configuration of a single tetrahedron, if you nudge the six squared edge lengths along any direction, the square root of each edge changes differentiably, and its rate of change is given by the simple formula v_f / (2√a_f), where v_f is the size of the nudge in that edge and a_f is the edge's squared length at the flat point.

This is a statement about a single tetrahedron at one specific point, not about the whole spacetime lattice. The theorem is a derivative, meaning it describes the immediate response to an infinitesimal change, not the behavior over a finite distance. It is also only about the square root factor of the action, not about the full gravitational action or any physical prediction. What it does is establish a clean, exact building block: the derivative of the square root of an edge length at the flat configuration, which is needed for later steps in a larger program of analysis.

The theorem does not claim anything about second derivatives, about the sum over many tetrahedra, or about the continuum limit of the theory. It does not prove that the full action has a derivative, nor does it say anything about the value of any physical observable. Those are explicitly left open. The scope is deliberately narrow: one tetrahedron, one point, one factor of the action, and the first derivative along any direction. This is a lemma in a longer chain, not a standalone physical result.

/-- Directional derivative of one flat sqrt-edge factor (THEOREM): along
the same affine path, `√((a + t·v)_f)` has derivative `v_f/(2√a_f)` at
`t = 0`. -/
theorem hasDerivAt_flatSqrtEdge_directional (v : Fin 6 → ℝ) (f : Fin 6) :
    HasDerivAt (fun t : ℝ => Real.sqrt (freudenthalTetSqEdges f + t * v f))
      (v f / (2 * Real.sqrt (freudenthalTetSqEdges f))) 0 := by
  have hpos : 0 < freudenthalTetSqEdges f := freudenthalTet.sqEdge_pos f
  have hinner : HasDerivAt (fun t : ℝ => freudenthalTetSqEdges f + t * v f) (v f) 0 := by
    simpa using
      ((hasDerivAt_id (0 : ℝ)).mul_const (v f)).const_add (freudenthalTetSqEdges f)
  have hsq : HasDerivAt Real.sqrt (1 / (2 * Real.sqrt (freudenthalTetSqEdges f)))
      (freudenthalTetSqEdges f + (0 : ℝ) * v f) := by
    simpa using Real.hasDerivAt_sqrt (ne_of_gt hpos)
  have hcomp : HasDerivAt (fun t : ℝ => Real.sqrt (freudenthalTetSqEdges f + t * v f))
      (1 / (2 * Real.sqrt (freudenthalTetSqEdges f)) * v f) 0 :=
    hsq.comp (0 : ℝ) hinner
  have hval : v f / (2 * Real.sqrt (freudenthalTetSqEdges f)) =
      1 / (2 * Real.sqrt (freudenthalTetSqEdges f)) * v f := by ring
  rw [hval]
  exact hcomp

/-- Directional derivative of one flat sqrt-edge factor (THEOREM): along
the same affine path, `√((a + t·v)_f)` has derivative `v_f/(2√a_f)` at
`t = 0`. -/
theorem hasDerivAt_flatSqrtEdge_directional (v : Fin 6 → ℝ) (f : Fin 6) :
    HasDerivAt (fun t : ℝ => Real.sqrt (freudenthalTetSqEdges f + t * v f))
      (v f / (2 * Real.sqrt (freudenthalTetSqEdges f))) 0 := by
  have hpos : 0 < freudenthalTetSqEdges f := freudenthalTet.sqEdge_pos f
  have hinner : HasDerivAt (fun t : ℝ => freudenthalTetSqEdges f + t * v f) (v f) 0 := by
    simpa using
      ((hasDerivAt_id (0 : ℝ)).mul_const (v f)).const_add (freudenthalTetSqEdges f)
  have hsq : HasDerivAt Real.sqrt (1 / (2 * Real.sqrt (freudenthalTetSqEdges f)))
      (freudenthalTetSqEdges f + (0 : ℝ) * v f) := by
    simpa using Real.hasDerivAt_sqrt (ne_of_gt hpos)
  have hcomp : HasDerivAt (fun t : ℝ => Real.sqrt (freudenthalTetSqEdges f + t * v f))
      (1 / (2 * Real.sqrt (freudenthalTetSqEdges f)) * v f) 0 :=
    hsq.comp (0 : ℝ) hinner
  have hval : v f / (2 * Real.sqrt (freudenthalTetSqEdges f)) =
      1 / (2 * Real.sqrt (freudenthalTetSqEdges f)) * v f := by ring
  rw [hval]
  exact hcomp

What this page does not claim

The theorem does not prove the existence of any second derivative. The theorem does not establish any result about a sum over many tetrahedra. The theorem does not determine the value of any physical observable or the continuum symbol.

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: