module module moderate

`IndisputableMonolith.Gravity.Analysis.SRSTTFirstVariation4D`

Infrastructure for the Euclidean weak-field transverse-traceless first variation in four dimensions: 4×4 matrix types, the Frobenius pairing, edge-strain linearity, and the exact midpoint Bloch increment. Gravity analysts recovering the Einstein–Hilbert quadratic action from the Recognition ledger cite it. The module is mostly definitions and elementary algebraic identities feeding a packaged first-variation certificate.

claimOn real $4\times 4$ matrices equip the Frobenius pairing $\langle A,B\rangle_F=\mathrm{tr}(A^\top B)$ and the associated squared norm. Edge strain is linear (additive, homogeneous, odd). Coupling-weight cross terms and the exact midpoint Bloch first-variation increment of the Euclidean weak-field TT sector are recorded as named objects for the Recognition gravity analysis.

background

Recognition Science gravity recovers the Einstein–Hilbert weak-field quadratic action from a ledger-facing discrete action. The upstream module SRSConvergesEH4D is the named-closer export for that campaign: it hosts the preflight Props edge_tt_decomposition and S_RS_converges_EH_4d and is the sole place allowed to inhabit them for the ledger flip.

This module supplies the 4D Euclidean linear-algebra layer those closers need. Matrices are plain $4\times 4$ real arrays (Mat4); wave and coupling index types label TT modes and interaction channels. The Euclidean Frobenius pairing $\langle A,B\rangle_F$ is the inner product that turns edge strain into a quadratic form; its self-pairing recovers the squared Frobenius norm. Edge strain is treated as a linear map on that matrix space (add, scalar multiply, negate, subtract).

Coupling-weight cross terms isolate the mixed contributions that appear when the first variation is expanded about the midpoint Bloch configuration. The headline object is the exact midpoint Bloch first-variation increment of the Euclidean weak-field TT sector.

proof idea

Definition-heavy analysis module, not a single theorem. It introduces matrix and index types, defines the Frobenius pairing and proves the norm-as-self-pairing identity, then records the four linearity lemmas for edge strain by direct expansion. Coupling-weight cross helpers are pure algebraic rearrangements. The exact midpoint Bloch first-variation statement packages those identities into the increment used by the weak-field TT analysis; proofs are elementary matrix algebra over the Euclidean pairing, with no analytic estimates.

why it matters in Recognition Science

Feeds the public axiom audit module SRSTTFirstVariation4DAudit, whose doc-comment demands a clean triple [propext, Classical.choice, Quot.sound] on the headline, key derivatives, and packaged certificate for the Euclidean weak-field TT midpoint first-variation increment.

In the broader QG campaign this sits under the weak-field quadratic-action recovery path opened by SRSConvergesEH4D: once edge-TT decomposition and $S_{\mathrm{RS}}\to S_{\mathrm{EH}}$ in 4D are inhabited, the first-variation calculus here is what turns the discrete ledger action into a continuum Euler–Lagrange identity in the TT sector. It is scaffolding for the gravity side of Recognition Science, not a forcing-chain (T0–T8) step, but it is required before the ledger flip can claim Einstein–Hilbert recovery at quadratic order.

scope and limits

Does not prove full $S_{\mathrm{RS}}\to S_{\mathrm{EH}}$ convergence; that lives upstream as a named closer Prop.
Does not treat Lorentzian signature or Minkowski inner products; Euclidean Frobenius only.
Does not derive nonlinear Einstein equations or strong-field corrections.
Does not fix dimension: the 4 in Mat4 is hard-coded, not forced from T8.
Does not discharge audit obligations; the audit module only checks axiom surface.

used by (1)

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

IndisputableMonolith.Gravity.Analysis.SRSTTFirstVariation4DAudit module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.Analysis.SRSConvergesEH4D module_import

declarations in this module (36)

abbrev Mat4 L46
abbrev Wave4 L47
abbrev CouplingIdx L48
def frobeniusPairing4D L53
theorem frobeniusNormSq_eq_pairing_self L56
theorem edgeStrain_add L59
theorem edgeStrain_smul L79
theorem edgeStrain_neg L94
theorem edgeStrain_sub L98
def couplingWeightCross L105
def couplingWeightCrossIdx L110
def exactMidpointBlochFirstVariation L119
theorem exactMidpointBlochSymbol_eq_irred L123
theorem exactMidpointBlochFirstVariation_eq_irred L129
theorem couplingWeight_line L137
theorem couplingWeightIdx_line L154
theorem weightFn_line L162
theorem exactMidpointBlochSymbol_line L169
theorem hasDerivAt_affine_quad L205
theorem hasDerivAt_exactMidpointBlochSymbol_line L225
theorem exactMidpointBlochFirstVariation_polarization L243
theorem IsSymmetric_add L269
theorem IsSymmetric_sub L274
theorem IsTraceless_add L279
theorem IsTraceless_sub L285
theorem IsTransverse_add L291
theorem IsTransverse_sub L298
theorem IsTT_add L305
theorem IsTT_sub L310
theorem frobeniusPairing4D_polarization L317
theorem continuumFace_polarization_eq_neg_quarter_frobenius L343
theorem momentumNormSq_torus_ne_zero L352
theorem hasDerivAt_finiteExactMidpointBlochSymbol_normalized L363
theorem continuumTTFirstVariation_closed L379
def SRSTTFirstVariation4DCert L451
theorem srsTTFirstVariation4D_cert L471