Gravity Analysis Regge Exact Flat Hessian Symbol4 D Exact Hessian Edge Origins M

The flat-space Hessian

The declaration ExactHessianS_RS_converges_EH_4d_closed is a theorem in the framework's machine-checked library of formal theorems. It establishes that, on a flat four-dimensional background, the second variation of the Regge action, a discrete approximation to Einstein gravity built from flat simplices, matches the continuum Einstein-Hilbert result for the two physical polarizations of a gravitational wave. Concretely, the theorem proves that the coefficient for the transverse-traceless (TT) mode is exactly -1/4, and that the gauge mode, a pure coordinate artifact, has coefficient exactly 0.

The proof is a discrete bookkeeping identity, not a numerical fit. It combines two facts: the unit-Frobenius TT coefficient is -1/8, and twice that equals the Einstein-Hilbert coefficient -1/4. The gauge coefficient is 0 by definition. These are checked by decide, a computational proof procedure that evaluates the expressions exactly over the rational numbers, with all square roots canceling in the final rationals. The theorem is a closed algebraic face of a larger target proposition, ExactHessianS_RS_converges_EH_4d, which also includes a statement about TT isotropy that is not part of this particular proof.

What the theorem does not claim is as important as what it proves. It does not inhabit the ledger S_RS_converges_EH_4d, which would require a full convergence proof of the discrete action to the continuum one. It does not flip gap_action_recovery, a separate flag for a different recovery mechanism. It does not provide a general algebraic coupling table C_abcdij for arbitrary modes; the certificates cover only the named TT and gauge faces. The library explicitly records that the general table is absent, and that the continuum limit for all modes remains an open target.

In plain terms, the declaration is a precise, verified calculation on a restricted but important set of cases: it nails the exact flat-space Hessian for the physical wave modes and the gauge mode, and it is honest that the full continuum story is not yet closed. The framework's own status flags, srsInhabited and gapActionRecovery, are both false, marking the larger convergence question as open.

theorem ExactHessianS_RS_converges_EH_4d_closed :
    ExactHessianS_RS_converges_EH_4d :=
  ⟨ExactHessianTTIsotropyTarget_closed, ExactHessianGaugeZeroTarget_algebraic_face⟩

theorem exactHessianM2AxisTTPlus_eq_EH :
    exactHessianM2AxisTTPlusCoeff = einsteinHilbertTTCoefficient4D := by
  simp [exactHessianM2AxisTTPlusCoeff, einsteinHilbertTTCoefficient4D]

theorem exactHessianM2GaugeCoeff_eq :
    exactHessianM2GaugeCoeff = (0 : ℝ) := rfl

theorem exact_hessian_srs_still_open :
    exactHessianSymbolStatus.srsInhabited = false ∧
      exactHessianSymbolStatus.gapActionRecovery = false := by
  decide

theorem exactHessianAlgebraicM2Table_absent :
    ExactHessianAlgebraicM2TablePresent = false := rfl

What this page does not claim

The theorem does not prove the full continuum limit of the discrete Regge action. The theorem does not provide a general algebraic coupling table for arbitrary modes. The theorem does not claim any numerical agreement beyond the exact rational values -1/4 and 0.

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