IndisputableMonolith.Gravity.Analysis.SRSConvergesScope4D
Scoped 4D analysis of what the SRS mesh-limit actually hits: the Regge-normalized Einstein–Hilbert face, not the bare EH face. Records the closed-form limit value, proves inequality of the two faces, and packages the Arc-2 Step-8 verdict that the geometric-fold/dictionary collision is real. Gravity auditors cite it when reading the weak-field quadratic recovery chain.
claimIn 4D weak-field TT kinematics, the SRS mesh sequence converges to the Regge face $v_{\mathrm{SRS}}=\rho\,v_{\mathrm{EH}}$ with Regge normalization $\rho=1/2$, hence $v_{\mathrm{SRS}}\neq v_{\mathrm{EH}}$. The mesh does not converge to the bare EH face; the geometric-fold versus dictionary gap of exactly two is therefore a genuine collision, summarized by a scoped Step-8 verdict.
background
Arc 2 of the gravity analysis separates coefficient matching from limit identification. Step 7 fixed the Einstein–Hilbert transverse-traceless second variation at $-1/4$ per unit Frobenius and momentum, and pinned Regge’s normalization $\rho=1/2$, so the banked dictionary value $-1/8$ is exactly the second variation of the Regge action. That closed the coefficient question; it said nothing about which face the discrete convergence theorem lands on.
This module sits between the named closers in SRSConvergesEH4D (edge TT decomposition and the $S_{\mathrm{RS}}\to\mathrm{EH}$ 4D statement) and the geometric-hinge comparison. It introduces 4D matrix and wave carriers, the closed-form SRS limit value, and the EH face value, then compares them under the Regge normalization inherited from Step 7.
Upstream framing: the geometric hinge fold is not the dictionary, and the gap is exactly two. The present file makes that gap operational for the mesh sequence rather than for a single fold identity.
proof idea
Definition layer first: 4D matrix/wave types, then named constants for the SRS limit value and the EH face value. Algebraic identities show the SRS limit equals Regge normalization times the EH face ($\rho=1/2$), hence the two faces are unequal.
Convergence statements are then scoped: the mesh sequence converges to the Regge face and does not converge to the bare EH face. A reading lemma records that a naive symbol-for-symbol identification of moments (R1) fails. Those facts are bundled into the_collision_is_real and a Step8ScopedVerdict proposition discharged by a single holding theorem.
No deep analytic estimates live here; the module is a scope-and-naming layer over the EH4D closers and the geometric-fold comparison.
why it matters in Recognition Science
Feeds the Arc-2 Step-8 axiom audit module, which reprints every declaration of the geometric-fold-versus-dictionary development and expects only the base triple [propext, Classical.choice, Quot.sound]. Without a scoped statement of what the convergence theorem converges to, the coefficient match from Step 7 could be misread as identity of faces.
In the Recognition gravity chain this is the honest-scope gate for weak-field quadratic action recovery: ledger-facing exports may later inhabit the preflight Props only after the limit face is named. The factor-two collision (Regge $\rho=1/2$ versus bare EH) is the concrete obstruction that prevents silently equating the geometric fold with the banked dictionary. Downstream audit and any full-theory ledger flip both depend on that distinction remaining explicit.
scope and limits
- Does not prove the analytic SRS mesh-convergence theorem itself; only scopes its face.
- Does not re-derive the EH TT second variation or the $\rho=1/2$ Regge normalization.
- Does not claim the geometric fold equals the dictionary; it records their gap.
- Does not treat strong-field, non-TT, or dimension other than 4D kinematics.
- Does not discharge ledger-facing Props beyond the scoped Step-8 verdict.
used by (1)
depends on (2)
declarations in this module (12)
-
abbrev
Mat4 -
abbrev
Wave4 -
theorem
srs_limit_value -
theorem
eh_face_value -
theorem
srs_limit_is_regge_normalization_times_eh -
theorem
srs_limit_ne_eh_face -
theorem
mesh_sequence_does_not_converge_to_eh_face -
theorem
mesh_sequence_converges_to_the_regge_face -
theorem
R1_fails_if_the_moments_read_their_symbols -
theorem
the_collision_is_real -
def
Step8ScopedVerdict -
theorem
step8ScopedVerdict_holds