Pith. sign in
module module moderate

IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianBlochM2Rayleigh4DAudit

show as:
view Lean formalization →

Audit module for the exact midpoint Bloch mass-squared Rayleigh identities on the flat 4D Regge Hessian. It packages the unit-Frobenius transverse-traceless face (Rayleigh quotient equal to -1/8) and the pure-gauge vanishing face into a typed residual certificate. Gravity analysts cite it when checking that the algebraic face equalities match the analytic Bloch symbols. Structure is residual inhabitation over the parent analysis module, not a new derivation.

claimAudit certificate that the exact midpoint Bloch $m^2$ Rayleigh quotient on the flat 4D Regge Hessian equals the algebraic faces: for unit-Frobenius transverse-traceless modes, $\mathrm{Rayleigh}(H,k)/|k|^2=-1/8$; for pure-gauge families, the same quotient vanishes.

background

Recognition Science gravity analysis works with discrete Regge calculus on a flat background and studies the Hessian of the action in Bloch (plane-wave) coordinates. The midpoint Bloch symbol yields a mass-squared Rayleigh quotient whose low-momentum faces must match pure algebraic predictions.

The parent module states two faces: unit-Frobenius TT modes give exactMidpointBlochM2 $H,k/|k|^2=-1/8$, while pure-gauge families give quotient zero. Those identities live as a typed residual TypedResidual_m2_rayleigh_eq_algebraic_face, with the rational certificate in ReggeExactMidpointM2TTIdentity4D.

This audit module imports that analysis layer and exposes the residual inhabitation for downstream gravity checks, without introducing new geometric hypotheses.

proof idea

No independent proof body. The module is an audit shell: it imports ReggeExactFlatHessianBlochM2Rayleigh4D and inhabits the typed residual that the midpoint Bloch $m^2$ Rayleigh quotient equals the algebraic faces (TT face $-1/8$, pure-gauge face $0$). Argument structure is residual packaging and certificate reference, not a fresh tactic script.

why it matters in Recognition Science

Places a checkable residual stamp on the R3 face equalities for the flat 4D Regge Hessian Bloch symbol. Downstream gravity stacks that need the TT mass-squared face or gauge-null face can cite the audit rather than re-open the rational certificate in ReggeExactMidpointM2TTIdentity4D. In the broader RS gravity program this locks the discrete Hessian spectrum against continuum algebraic expectations before curvature or matter couplings are restored. No used-by edges are recorded yet; the module is a leaf audit over the analysis import.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.