Gravity Analysis Regge Exact Flat Hessian Norm Gate4 D Exact Unit Frobenius Ne F

The normalization gate

The Einstein-Hilbert action is the classical starting point for general relativity: it assigns a number to a spacetime geometry, and its variation yields the Einstein field equations. In numerical work, one often studies the action's second variation on a restricted set of metric perturbations called the transverse-traceless (TT) sector. The result is a quadratic form, and a natural way to compare different discretizations is to normalize it by the squared Frobenius norm of the perturbation, a standard matrix measure of size.

In the framework's machine-checked library, two coefficients for this normalized form have been defined. The first, exactUnitFrobeniusTTCoefficient, is derived from an exact algebraic computation of the Hessian and equals -1/8. The second, frozenPreflightEHCoefficient, is a constant that was used in an earlier automated check and equals -1/4. The theorem exact_unitFrobenius_ne_frozen_preflight_EH proves these two numbers are not equal.

The theorem also records why the discrepancy is not a bug. The frozen value -1/4 is exactly twice the exact value, and the library proves this relation: discrete bookkeeping, a factor of 2 that arises in the discrete Regge action's bookkeeping, multiplies the exact unit-Frobenius coefficient to recover the frozen one. This identity is banked as an algebraic face, not as a geometric statement about the continuum limit. The library explicitly states that this identity does not inhabit the geometric convergence theorems, does not inhabit the ledger statement for the 4D action, and does not flip the action-recovery gap.

The theorem therefore acts as a normalization honesty gate. It certifies that the historical preflight value was a bookkeeping-adjusted face, not the exact unit-Frobenius coefficient, and that the exact value is the one that matches the Regge action's TT face. The gate passes because the mismatch is now a proved, documented fact rather than an unexamined assumption. What the theorem does not claim is that the continuum limit of the discrete action equals the Einstein-Hilbert face; that convergence remains a separate, open geometric question requiring a mesh limit.

def exactUnitFrobeniusTTCoefficient : ℝ := exactHessianM2UnitFrobeniusTTCoeff

def frozenPreflightEHCoefficient : ℝ := einsteinHilbertTTCoefficient4D

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

What this page does not claim

The theorem does not prove that the continuum limit of the discrete Regge action equals the Einstein-Hilbert action; that convergence remains open. The theorem does not claim the -1/4 value is wrong for all purposes; it is the correct value on the axisTTPlus face where the squared Frobenius norm is 2. The theorem does not assert that the discrete bookkeeping factor is geometrically meaningful; it is an algebraic identity only.

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: