module module high

`IndisputableMonolith.Gravity.Analysis.ReggeNormalizationDerived4D`

Sets the free continuum scale factor ρ in the discrete-to-continuum Regge comparison and pins it at 1/2 in 4D. Anyone matching the banked midpoint dictionary face against the Einstein-Hilbert TT second variation cites this module. The argument multiplies the derived continuum face by ρ, equates it to the Regge Hessian face on a TT plane-wave witness, and solves for ρ.

claimIf the discrete Regge action satisfies $\sum_h A_h\delta_h=\rho\int R\sqrt{g}$, then the continuum face against which the Regge Hessian is compared is $\rho$ times the derived Einstein-Hilbert transverse-traceless second variation. In 4D that factor is pinned at $\rho=1/2$, so the dictionary face $-1/8$ (per unit Frobenius and momentum) is exactly the second variation of the Regge action.

background

Arc 2, step 7 of the gravity analysis chain. The continuum module derives, from the Levi-Civita connection alone, the number that the Einstein-Hilbert action assigns to a real transverse-traceless plane wave, in the same convention as the banked Regge midpoint dictionary: $-1/4$ per unit Frobenius norm squared and momentum squared.

The companion identity module closes the exact midpoint Bloch $m^2$ TT identity that supplies the discrete Hessian face on the same wave class. This module introduces the free real scale $\rho$ in the ansatz $\sum_h A_h\delta_h=\rho\int R\sqrt{g}$, defines the scaled continuum face (regge face), and compares it to the dictionary face on an explicit nonzero TT witness.

Notation: Wave4 is the 4D TT plane-wave test object; Frobenius and momentum squares are the two quadratic invariants against which both faces are normalized.

proof idea

Definition layer first: regge face is $\rho$ times the continuum TT second-variation face; regge normalization is the free real $\rho$. Algebraic identities record Frobenius and momentum squares on the axis TT-plus and axis-wave witnesses.

Comparison lemmas equate the scaled continuum face to the banked dictionary face on those witnesses. The pinning theorem solves the resulting scalar equation and obtains $\rho=1/2$. Nonzero-witness and dictionary-value lemmas discharge the denominators so the ratio is well-defined. No continuum derivation is redone here; the module only multiplies, compares, and solves.

why it matters in Recognition Science

Closes the coefficient question in Arc 2 step 7: once $\rho=1/2$ is forced, the banked dictionary value $-1/8$ is identified as the second variation of the Regge action rather than an ad hoc fit. Downstream, GeometricFoldVsDictionary4D uses that pinning to separate the geometric hinge fold from the dictionary and to measure their exact gap of two, moving the discussion from coefficients to the actual continuum limit of the tree. The audit module requires every named theorem here (and in the continuum derivation) to report exactly the axiom set [propext, Classical.choice, Quot.sound], so the pinning sits inside a fully logged classical fragment with no extra gravity axioms.

scope and limits

Does not re-derive the continuum Einstein-Hilbert TT second variation; that is imported.
Does not prove continuum convergence of the Regge tree; only pins the overall scale ρ.
Does not address non-TT modes, massive modes, or dimensions other than 4.
Does not identify the geometric hinge fold with the dictionary; that gap is handled downstream.
Does not fix lattice spacing, curvature expansion order, or higher-derivative corrections.

used by (2)

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

IndisputableMonolith.Gravity.Analysis.GeometricFoldVsDictionary4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeNormalizationDerived4DAudit module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.Analysis.ContinuumTTSecondVariation4D module_import
IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4D module_import

declarations in this module (32)

abbrev Wave4 L58
theorem frobSq_eq L62
theorem momentumSq_eq L64
def reggeFace L71
def reggeNormalization L75
theorem reggeFace_eq L77
theorem reggeFace_eq_dictionary L88
theorem regge_normalization_pinned L99
theorem frobeniusNormSq_axisTTPlus L112
theorem waveNormSq_axisWave L115
theorem witness_nonzero L118
theorem dictionary_witness_value L124
theorem rho_one_fails L133
theorem rho_pinned_at_witness L141
theorem tetrahedron_deficit_sum L156
theorem octahedron_deficit_sum L160
def sphereEHIntegral L164
theorem regge_constant_from_gauss_bonnet L167
theorem gauss_bonnet_refutes_rho_one L174
theorem phaseAverage_sin_sq L190
def lagrangianDensityOfPhase L198
theorem lagrangian_route_same_face L201
theorem two_routes_differ_pointwise L210
theorem discreteBookkeepingFactor_is_inverse_regge L231
theorem frozen_preflight_is_the_eh_integral_face L241
theorem exact_unit_coefficient_is_the_regge_face L252
def NormalizationGateDischarged L270
theorem normalizationGateDischarged L280
def Step7Cert L289
theorem step7Cert L299
def typedResidual_arc2_normalization L310
def typedResidual_naming_defect L321