Pith. sign in
module module moderate

IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianBlochM2Rayleigh4D

show as:
view Lean formalization →

Equates Rayleigh quotients of the exact midpoint Bloch m² (from the flat 4D Regge Hessian) to unit-Frobenius TT and pure-gauge coefficients on the preflight carrier. Gravity analysts cite it when matching discrete second-variation symbols to continuum EH quadratic form. The module mainly disambiguates multi-open aliases, then reduces each quotient by the midpoint m²–TT identity and preflight norm normalizations.

claimOn the frozen 4D continuum preflight data, the Rayleigh quotient of the exact midpoint Bloch $m^2$ symbol equals the unit-Frobenius transverse-traceless coefficient, equals the pure-gauge coefficient, and matches the algebraic face residual; Frobenius and wave norms on the preflight carrier reduce to the identity normalizations used by the TT edge decomposition.

background

This sits in the QG full-theory 4D continuum closure lane. At a flat background every deficit vanishes, so the second variation of the Regge action $S=\sum_h A_h\delta_h$ collapses to the cross term $S''=\sum_h(dA_h)(d\delta_h)$ in squared-length coordinates. That Hessian is packaged as a finite trig polynomial (Bloch symbol) over a fixed coupling table.

Upstream, the continuum preflight freezes the weak-field EH target, mesh carrier, normalized TT data, and pure-gauge family before any recovery claim. The edge TT decomposition supplies the linear-algebra transverse-traceless split of symmetric $4\times 4$ matrices against a nonzero Euclidean wave covector. The midpoint $m^2$ TT identity closes the algebraic link between that Bloch $m^2$ and the TT projector.

Sibling objects here are thin: matrix and wave carriers (Mat4, Wave4), preflight norm identities, and four Rayleigh equalities tying midpoint Bloch $m^2$ to unit-Frobenius TT, gauge, and algebraic-face residuals.

proof idea

Definition-and-identity module, not a deep analytic argument. After multi-module opens it rebinds shared aliases so matrix, wave, and residual names do not collide. Preflight Frobenius and wave squared-norms are shown equal to the identity normalizations on the frozen carrier. Each Rayleigh statement is then a short algebraic reduction: apply the exact midpoint $m^2$–TT identity, insert the TT or gauge face from the edge decomposition, and cancel the preflight norm factors. Typed residual faces follow the same pattern. No continuum limit or Tendsto step lives here.

why it matters in Recognition Science

Supplies the Rayleigh-side equalities that the audit module checks and that the ledger export SRSConvergesEH4D needs when inhabiting the named closer $S_{RS}\to\mathrm{EH}$ in 4D weak field. Downstream that export is the sole place allowed to flip the preflight Props for quadratic-action recovery; without matching discrete $m^2$ Rayleigh data to TT and gauge coefficients, the continuum EH target stays unlinked from the exact flat Hessian symbol.

In the campaign ledger this is a binding increment on the path from Stage-1 Bloch symbol through midpoint $m^2$ identity to named closers edge_tt_decomposition and S_RS_converges_EH_4d. It does not itself prove continuum recovery; it freezes the algebraic Rayleigh faces those closers quote.

scope and limits

used by (2)

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

depends on (5)

Lean names referenced from this declaration's body.

declarations in this module (8)