Pith. sign in
module module moderate

IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianNormGate4D

show as:
view Lean formalization →

Norm-gate audit for the exact flat 4D Regge Hessian: it freezes the discrete bookkeeping factor 2 that converts the unit-Frobenius TT coefficient into the frozen weak-field Einstein–Hilbert target (EH audit §2.3). Gravity continuum-closure work cites it to separate genuine continuum recovery from mesh bookkeeping. Equalities are algebraic identities on named coefficients, not continuum limits.

claimIn the exact flat 4D Regge Hessian setting, a dimension-independent discrete bookkeeping factor equals $2$. The frozen preflight Einstein–Hilbert TT coefficient equals this factor times the exact unit-Frobenius TT coefficient, and both the unit-Frobenius and proposed unit-Frobenius EH coefficients match the exact-action symbol on the normalized TT face.

background

Regge calculus replaces the continuum Einstein–Hilbert action by a sum over hinges $S=\sum_h A_h\delta_h$. At a flat background every deficit vanishes, so the second variation reduces to the cross term $S''=\sum_h(dA_h)(d\delta_h)$ in squared-length coordinates. Upstream modules supply the exact flat Hessian Bloch symbol and the exact-action continuum symbol: the true Hessian annihilates vertex-gauge modes and sends normalized TT on the axis-plus face to $-1/4$.

This module sits in the Gravity analysis layer that prepares continuum preflight data. It names the frozen preflight EH coefficient, the exact unit-Frobenius TT coefficient, and a discrete bookkeeping factor whose intended value is the constant $2$ from EH audit §2.3. The factor is mesh bookkeeping, not a dynamical coupling: it records how discrete TT normalization and hinge counting relate the exact-action symbol to the frozen weak-field EH target used later in continuum closure.

proof idea

Definition-heavy audit module. It introduces named coefficient constants (frozen preflight EH, exact unit-Frobenius TT, discrete bookkeeping factor) and proves algebraic identities among them: the bookkeeping factor equals $2$, equals the exact-action normalization, and multiplies the unit-Frobenius coefficient to recover the frozen EH target. Separate lemmas record that exact unit-Frobenius differs from the frozen preflight value until the factor is inserted, and that unit-Frobenius (and proposed unit-Frobenius) EH coefficients agree with the exact symbol on the TT face. No continuum limit or spectral argument lives here; the work is coefficient arithmetic pinned to upstream exact-action and Hessian-symbol modules.

why it matters in Recognition Science

Continuum recovery of the Einstein–Hilbert quadratic action from simplicial Regge–Simons data needs a frozen weak-field target that is honest about discrete normalization. This module supplies that bookkeeping gate so later stages do not silently absorb a factor of $2$ into a false continuum claim.

It is imported by the 4D continuum preflight (which freezes EH targets and decoys before further computation), by the exact midpoint Bloch trig-polynomial symbol and its audit, by the norm-gate audit companion, and by the ledger-facing closer module that will eventually inhabit S_RS_converges_EH_4d. Those parents treat the factor-$2$ relation as settled discrete infrastructure while they attack gauge discrimination, Bloch two-jet limits, and weak-field quadratic recovery.

scope and limits

used by (5)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (24)