Gravity Analysis Regge4 Dflat Second Variation

The four-dimensional gap

Regge calculus is a way of doing general relativity on a discrete grid: spacetime is chopped into flat pieces, like a four-dimensional crystal, and gravity is described by the angles where these pieces meet. The ledger, a discrete record of these geometric events, tracks how the angles change. The second variation is the mathematical object that tells you how the action, the quantity whose minimization gives the equations of motion, curves when you perturb the geometry. In three dimensions, this calculation closes completely: the framework proves that the true nonlinear action's second variation equals a simplified form known as the Schläfli-reduced edge Hessian.

In four dimensions, the situation is different. The framework's machine-checked library of formal theorems has proved the flat part: when the four-simplex, the simplest four-dimensional building block, is exactly flat, the Schläfli identity holds. This identity says that a certain weighted sum of angle derivatives vanishes, a key cancellation that makes the calculation tractable. The library proves this for the flat seed and for every direction of perturbation, and it proves that the dihedral angles, the angles between the faces, are differentiable along these paths. These are genuine theorems, checked by the kernel.

The gap appears when the geometry is not flat. The full off-flat pathwise Schläfli identity, which would let the framework elevate the nonlinear action to the simplified candidate form, is absent. The candidate itself is identified, and its continuum face on a normalized axis equals -1/16, which differs from the Einstein-Hilbert coefficient of -1/4. This difference is proved, not assumed. The framework's status structure records the situation honestly: the candidate is identified, the flat theorems are present, the pathwise Schläfli is absent, and the elevation is open.

What this means in plain language is that the framework has pushed the four-dimensional calculation as far as the flat geometry allows, and the remaining obstacle is a specific, named mathematical identity. The residual is not a missing rescale or a fitted factor; it is the Schläfli elevation of the nonlinear action. This is a target for future work, not a claim that the framework has failed. The three-dimensional case is closed; the four-dimensional case is one precise step away.

theorem flat_freudenthal_schlaefli_identity (e : Fin 10) :
    (∑ h : Fin 10, flatSchlaefliSummand h e) = 0 :=
  freudenthal4SimplexFlatSchlaefli e

/-- Gate A2-style flat directional kill, re-exported for elevation wiring. -/
theorem flat_freudenthal_directional_schlaefli (v : Fin 10 → ℝ) :
    (∑ h : Fin 10, hingeAreaFlat h * flatDirectionalAngleDeriv v h) = 0 :=
  freudenthal4SimplexFlatDirectionalSchlaefli v

theorem flat_freudenthal_seed_angle_hasDerivAt (k : Fin 10) :
    HasDerivAt (fun t : ℝ => seedDihedralAngle (coordPath k t))
      (angleKernel k) (seedFlatSqEdges k) :=
  hasDerivAt_seedDihedralAngle_coord k

/-- Continuum-facing coefficient after Frobenius pin and `/|symbolDir|²`:
`-1/16`. -/
theorem candidate_continuumFace_normalizedTT_symbolDir :
    distinctHingeMomentForm ((Real.sqrt 2)⁻¹ • axisTTPlus) symbolDir /
        (∑ i : Fin 4, symbolDir i * symbolDir i) =
      (-1 / 16 : ℝ) :=
  continuumFace_normalizedPlus_symbolDir

theorem schlaefli_elevation_to_candidate_misses_eh_face :
    (-1 / 16 : ℝ) ≠ einsteinHilbertTTCoefficient4D :=
  candidate_face_ne_eh.1

What this page does not claim

This module does not prove that the four-dimensional Regge action converges to Einstein-Hilbert gravity. This module does not recover the gap action that would flip the status. This module does not claim the off-flat Schläfli identity is impossible, only that it is not yet proved.

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