Geometry Regge Rigorous Foundation

The Regge foundation

Regge calculus, introduced by Tullio Regge in 1961, is a way to do general relativity without coordinates. Instead of a smooth manifold, spacetime is built from flat tetrahedral blocks glued together. Curvature lives along the shared edges, the hinges, and the Einstein equations become algebraic relations between edge lengths and dihedral angles. It is a practical scheme for numerical relativity, but its mathematical foundations have often been taken on faith.

The new foundation supplies a rigorous basis for one of Regge calculus's central claims: that the second derivative of the action with respect to edge lengths, the Hessian, has off-diagonal entries equal to minus the area of the shared triangle, M_ij = -area(f_ij). This is the Regge component theorem. The foundation proves the groundwork: the Cayley-Menger polynomial CM_3, which gives the squared volume of a tetrahedron from its six edge lengths, is a genuine polynomial, smooth everywhere, and satisfies the classical identity 288 V² = CM_3(a). It verifies this identity at two test points, the regular and right-angle unit tetrahedra.

The foundation also proves that the gradient of CM_3 is explicit and well-behaved. A polynomial Taylor identity, cm3 (a + h) = cm3 a + ⟨grad, h⟩ + Q(a, h) + C(h), is proved by ring, and the directional derivative along each edge is shown to exist. The conformal edge ansatz, where edge lengths are parameterized by vertex potentials ξ as L_ij = ℓ₀ · exp((ξ_i + ξ_j)/2), is proved to be smooth, and the composition cm3 ∘ conformalSqEdge is also smooth. These are the analytic facts needed before any differentiation can happen.

In Recognition Science, this foundation is the first step toward deriving the Regge component theorem from within the framework. The framework's machine-checked library of formal theorems now contains a certified Cayley-Menger polynomial layer. The full theorem, however, is not yet proved. It requires three external classical hypotheses: Schläfli's identity, the dihedral cosine formula via Cayley-Menger cofactors, and the smoothness of the dihedral angle on the realisability cone. These are named, recorded, and imported from the standard literature, exactly as the framework handles other deep external results like Cheeger-Müller-Schrader.

The honest summary is that this foundation proves the smoothness and differentiability of the volume-squared function, which is the necessary analytic core. The Regge component theorem itself remains a conditional result, pending the three classical hypotheses. This is not a failure; it is the correct formal-math practice of separating what is proved from what is assumed. The foundation is the genuine first step of a multi-month formalization program, and it gives the framework a solid footing in Regge calculus.

theorem reggeRigorousFoundationCert : ReggeRigorousFoundationCert where
  cm3_polynomial_explicit := fun a => by unfold cm3; ring
  cm3_smooth := cm3_contDiff
  cm3_regular := cm3_regular_unit
  cm3_rightAngle := cm3_rightAngle_unit
  cm3_taylor_identity := cm3_taylor
  cm3_update_form := cm3_update_polyform
  conformal_smooth := conformalSqEdge_contDiff
  cm3_conformal_smooth := cm3_conformal_contDiff

/-- The conformal edge map is smooth in ξ (each component is `exp` of a
linear combination, which is smooth, times a positive constant). -/
theorem conformalSqEdge_contDiff (ℓ₀ : ℝ) (n : ℕ∞) :
    ContDiff ℝ n (conformalSqEdge ℓ₀) := by
  -- conformalSqEdge ℓ₀ ξ e = ℓ₀² * exp(ξ v1 + ξ v2)
  -- This is smooth in ξ via composition of smooth functions.
  -- The output is in (Fin 6 → ℝ); use contDiff_pi.
  rw [contDiff_pi]
  intro e
  -- Now we need ContDiff ℝ n (fun ξ => conformalSqEdge ℓ₀ ξ e).
  unfold conformalSqEdge
  -- Goal: ContDiff ℝ n (fun ξ => ℓ₀ ^ 2 * Real.exp (ξ (edgeVertices e).1 + ξ (edgeVertices e).2))
  have h_v1 : ContDiff ℝ n (fun ξ : Fin 4 → ℝ => ξ (edgeVertices e).1) :=
    (ContinuousLinearMap.proj (R := ℝ) (φ := fun _ : Fin 4 => ℝ)
      (edgeVertices e).1).contDiff
  have h_v2 : ContDiff ℝ n (fun ξ : Fin 4 → ℝ => ξ (edgeVertices e).2) :=
    (ContinuousLinearMap.proj (R := ℝ) (φ := fun _ : Fin 4 => ℝ)
      (edgeVertices e).2).contDiff
  have h_sum : ContDiff ℝ n
      (fun ξ : Fin 4 → ℝ => ξ (edgeVertices e).1 + ξ (edgeVertices e).2) :=
    h_v1.add h_v2
  have h_exp_smooth : ContDiff ℝ n (Real.exp : ℝ → ℝ) := Real.contDiff_exp
  have h_exp : ContDiff ℝ n
      (fun ξ : Fin 4 → ℝ => Real.exp (ξ (edgeVertices e).1 + ξ (edgeVertices e).2)) := by
    have := ContDiff.comp (g := Real.exp) (f := fun ξ : Fin 4 → ℝ =>
              ξ (edgeVertices e).1 + ξ (edgeVertices e).2) h_exp_smooth h_sum
    simpa using this
  -- ℓ₀^2 * exp(...) is smooth via product with a constant function.
  have h_const : ContDiff ℝ n (fun _ : Fin 4 → ℝ => ℓ₀ ^ 2) := contDiff_const
  exact ContDiff.mul h_const h_exp

theorem cm3_conformal_contDiff (ℓ₀ : ℝ) (n : ℕ∞) :
    ContDiff ℝ n (fun ξ : Fin 4 → ℝ => cm3 (conformalSqEdge ℓ₀ ξ)) := by
  exact (cm3_contDiff n).comp (conformalSqEdge_contDiff ℓ₀ n)

What this page does not claim

The full Regge component theorem M_ij = -area(f_ij) is not proved; it is conditional on three named external hypotheses. Schläfli's identity is not proved in the foundation; it is recorded as a named external classical hypothesis. The foundation does not derive the Regge component theorem from the Recognition Science framework's own axioms.

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/ReggeRigorousFoundation.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: