Gravity Analysis Regge Exact Flat Hessian Norm Gate4 D

A normalization gate for gravity

The Einstein-Hilbert action is the classical starting point for general relativity: it is the integral of spacetime curvature that, when varied, yields Einstein's field equations. In numerical and discrete approaches to gravity, one often works with a transverse-traceless (TT) decomposition of the metric perturbation, and the action's coefficient appears as a constant multiplying the squared Frobenius norm of that perturbation. The question is which constant is correct.

The answer depends on how the norm is normalized. If one fixes the Frobenius norm of the TT perturbation to be 1, exact algebraic manipulation gives the coefficient -1/8. The value -1/4 arises only when the norm squared equals 2, which is the case for a particular historical face of the theory called axisTTPlus. The two values differ by a factor of 2, a discrete bookkeeping factor that appears in the discrete Regge action but not in the continuum Einstein-Hilbert action.

In Recognition Science, this distinction is enforced by a module called ReggeExactFlatHessianNormGate4D. It proves that the exact unit-Frobenius coefficient -1/8 is not equal to the frozen preflight coefficient -1/4, and that the frozen value is exactly 2 times the exact one. The module then certifies a normalization gate as passing, but with a typed blocker string that records the algebraic identity without claiming it as a geometric convergence result. The continuum face is scale-explicit: it is written as (-1/8) times the squared Frobenius norm, and the discrete factor of 2 is banked only as an algebraic identity, not as a ledger statement about convergence.

The module also clarifies a naming subtlety. A definition called continuumEHDiscreteFace returns the value -1/4 times the squared norm, which is the Einstein-Hilbert face. But another definition, continuumEHScaleExplicit, returns -1/8 times the squared norm, which is flagged as actually the Regge action's face, not the Einstein-Hilbert one. The Regge action is a discrete approximation to gravity whose transverse-traceless face is rho times the Einstein-Hilbert one, with rho = 1/2. This matters because the convergence theorem S_RS_converges_EH_4d_closed proves convergence to the Regge face, not to the Einstein-Hilbert face, which is twice it.

theorem exact_unitFrobenius_ne_frozen_preflight_EH :
    exactUnitFrobeniusTTCoefficient ≠ frozenPreflightEHCoefficient := by
  unfold exactUnitFrobeniusTTCoefficient frozenPreflightEHCoefficient
    exactHessianM2UnitFrobeniusTTCoeff einsteinHilbertTTCoefficient4D
  norm_num

/-- Frozen `-1/4` is discrete bookkeeping times the unit-F m² face. -/
theorem frozen_EH_is_discrete_bookkeeping_times_unitF :
    frozenPreflightEHCoefficient =
      discreteBookkeepingFactor * exactUnitFrobeniusTTCoefficient := by
  unfold frozenPreflightEHCoefficient exactUnitFrobeniusTTCoefficient
    discreteBookkeepingFactor exactHessianM2UnitFrobeniusTTCoeff
    einsteinHilbertTTCoefficient4D
  norm_num

theorem normalizationGatePass_true : NormalizationGatePass = true := rfl

theorem continuumEHScaleExplicit_eq (frobeniusSq : ℝ) :
    continuumEHScaleExplicit frobeniusSq =
      (-(1 / 8 : ℝ)) * frobeniusSq := by
  simp [continuumEHScaleExplicit, einsteinHilbertTTCoefficient4D_unitFrobenius]

/-- Value `2 · (-1/8) · ‖E‖_F² = -(1/4) · ‖E‖_F²`, which is the
**Einstein-Hilbert** transverse-traceless face, derived from the Levi-Civita
connection in `ContinuumTTSecondVariation4D` (arc 2 step 7).  The word
`Discrete` in the name is a misnomer: the discrete side is the factor that was
applied, not the value returned.  Kept for stability of consumers, flagged here
rather than renamed. -/
def continuumEHDiscreteFace (frobeniusSq : ℝ) : ℝ :=
  discreteBookkeepingFactor * exactUnitFrobeniusTTCoefficient * frobeniusSq

What this page does not claim

This module does not prove that the discrete Regge action converges to the continuum Einstein-Hilbert action in any geometric sense. The algebraic identity 2*(-1/8) = -1/4 is not claimed to be a statement about the continuum limit or about the ledger S_RS_converges_EH_4d. The value -1/4 is not claimed to be the correct coefficient for the Einstein-Hilbert action on a unit-Frobenius TT perturbation.

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