Gravity Analysis Regge Exact Flat Hessian Symbol4 D

The exact flat Hessian symbol

In numerical relativity, Regge calculus approximates spacetime with a grid of flat simplices, and the action is a sum over hinges of area times deficit angle. The second variation of this action, the Hessian, controls how small perturbations behave. On a flat background every deficit angle vanishes, and the Hessian reduces to a pure cross term between area and angle variations. The Recognition Science library builds this object exactly, with true per-edge midpoint phases, and proves several of its key coefficients by computation.

The central object is the ledger, a discrete record of events, here the list of edge strains. The library defines the exact flat Hessian symbol with midpoint phases and cross terms only, and proves that for the two physical transverse-traceless polarizations the mass-squared density is isotropic, equal to minus one eighth times the squared Frobenius norm times the squared wave number. For the banked axisTTPlus face, where the norm is the square root of two, the coefficient is exactly minus one quarter, matching the Einstein-Hilbert coefficient. Gauge modes, which are pure coordinate artifacts, have exactly zero coefficient. The library also records a measured finite-grid check at N equals 6 with relative error below one part in ten thousand.

The library is honest about its limits. It does not inhabit the ledger for the convergence of the discrete action to the continuum Einstein-Hilbert action, and it does not flip the gap action recovery flag. The general algebraic coupling table is not present in Lean; only the named mode certificates are proved. The module names these as open targets, not achievements.

theorem exactHessianM2UnitFrobeniusTTCoeff_eq :
    exactHessianM2UnitFrobeniusTTCoeff = -(1 / 8 : ℝ) := rfl

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

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

theorem measuredTTRelErrVsOracleN6_lt_1e4 :
    measuredTTRelErrVsOracleN6 < (1 / 10000 : ℝ) := by
  norm_num [measuredTTRelErrVsOracleN6]

What this page does not claim

This module does not prove the convergence of the discrete action to the continuum Einstein-Hilbert action. This module does not provide a general algebraic table for all mode couplings. This module does not claim the gap action recovery flag is flipped.

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: