module module high

`IndisputableMonolith.Gravity.Analysis.ReggeTTHingeAwareZeroMode`

Assembles the hinge/edge-diagonal O(1) block of the real-space Regge Hessian at flat geometry: the 2π L'' diagonal contracted with edge-class polarization coefficients. Gravity analysts cite it when matching the sympy hinge residual against a TT witness polarization. Algebraic identities for √2 factors and a cancellation lemma show the hinge term cancels the recorded residual on that witness.

claimAt flat squared edge lengths $\ell_2$, with $L(\ell_2)=\sqrt{\ell_2}$ so $L''(\ell_2)=-1/(4\ell_2\sqrt{\ell_2})$, the assembled hinge/edge-diagonal block is the $2\pi L''$ diagonal of the real-space Regge Hessian contracted with the edge-class coefficients of a polarization matrix. A fixed TT witness polarization and wave vector make this hinge contribution cancel the recorded residual.

background

Regge calculus linearizes curvature about a flat triangulation. Deficits vanish at flat, so the Hessian hinge diagonal retains only the constant $2\pi$ times the second derivative of edge length $L=\sqrt{\ell_2}$. Displacement classes $d$ carry flat squared lengths $\ell_{2,d}$; the edge-class coefficients of a polarization matrix contract that diagonal into a single O(1) block.

The parent campaign is QG full-theory Paper C / Pillar 1, Lane C. Upstream bucket-fiber aggregation already reduced radical-bearing raw stencil coefficients $J_{fg}/(2\sqrt{a^*_f})$ (flat-angle Jacobian over Freudenthal flat tuples) to literal rational tables on every bucket and all 36 slot pairs. This module supplies the matching hinge object that the sympy diagnostic isolates term-for-term.

Sibling material fixes a concrete TT witness polarization and wave vector, proves it is transverse-traceless, extracts its polarization edge coefficients, and records elementary identities $\sqrt{2}\cdot\sqrt{2}=2$ and $(1/\sqrt{2})^2=1/2$ used in the contraction.

proof idea

Definition-heavy module with short algebraic lemmas, not a single deep theorem. It defines the hinge/edge-diagonal block from $2\pi L''$ and edge-class polarization data, introduces the TT witness polarization and wave vector, and proves the witness is TT with explicit edge coefficients. Elementary field lemmas discharge $\sqrt{2}$ normalizations. The main content lemma shows the hinge block cancels the recorded residual when contracted against that witness. Slot-displacement classification supports the edge-class indexing. No long tactic scripts; structure is assemble definitions, then cancel.

why it matters in Recognition Science

Closes the hinge half of the real-space O(1) residual that Gate B and finite Bloch assembly must match. Downstream ReggeTTBlochAssembly is the C-DAG1 finite-cell stage: cosine evaluators from bucket integer phase keys, normalized canonical finite cells for commensurate non-aliased wave vectors. Downstream ReggeTTGateBBridge closes Gate B by equating the interface moment fold reggeTTMoment (support, phase quadratic, amplitude from the actual raw stencil) to the committed spike LHS under the seven TT hypotheses.

Without a hinge-aware zero-mode witness, the sympy residual and the Lean stencil cannot be identified on the edge-diagonal sector. The module therefore sits between bucket aggregation (rational tables) and the Bloch/Gate-B bridges that finish Lane C of the Paper C charter. It does not itself prove the full TT spectrum; it supplies the hinge cancellation identity those parents import.

scope and limits

Does not prove the full Regge TT spectrum or dispersion relation.
Does not assemble finite Bloch cells or cosine phase evaluators.
Does not discharge Gate B spike equality under the seven TT hypotheses.
Does not treat curved backgrounds; Hessian is evaluated at flat only.
Does not re-derive bucket-fiber rational tables; those are upstream.

used by (2)

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

IndisputableMonolith.Gravity.Analysis.ReggeTTBlochAssembly module_import
IndisputableMonolith.Gravity.Analysis.ReggeTTGateBBridge module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.Analysis.ReggeTTBucketAggregation module_import

declarations in this module (59)

theorem below L24
def hingeEdgeDiagonalBlock L117
def ttWitnessPolarization L125
def ttWitnessWaveVector L131
theorem sqrt2_mul_self L136
theorem inv_sqrt2_mul_self L139
theorem inv_sqrt2_sq L143
theorem ttWitness_isTT L149
theorem ttWitness_polEdgeCoeff L167
theorem hinge_cancels_recorded_residual L187
def slotDispClass L204
class the L213
theorem slotDispClass_grounded L216
theorem w00 L228
theorem w01 L230
theorem w02 L232
theorem w03 L234
theorem w04 L236
theorem w05 L238
theorem w10 L240
theorem w11 L242
theorem w12 L244
theorem w13 L246
theorem w14 L248
theorem w15 L250
theorem w20 L252
theorem w21 L254
theorem w22 L256
theorem w23 L258
theorem w24 L260
theorem w25 L262
theorem w30 L264
theorem w31 L266
theorem w32 L268
theorem w33 L270
theorem w34 L272
theorem w35 L274
theorem w40 L276
theorem w41 L278
theorem w42 L280
theorem w43 L282
theorem w44 L284
theorem w45 L286
theorem w50 L288
theorem w51 L290
theorem w52 L292
theorem w53 L294
theorem w54 L296
theorem w55 L298
def assembledConstantBlock L312
theorem zeroMode_free_coefficients L326
theorem polEdgeCoeff_alternatingSum L342
theorem assembledConstantBlock_eq_zero L359
theorem assembled_witness_split L376
theorem commensurateMomentum_zero L386
theorem planeWaveTetVelocity_zeroMomentum L393
theorem rawCellStencil_zeroMomentum L408
theorem canonicalFiniteH_zeroMomentum_eq_zero L472
theorem zeroMomentum_symbol_is_zero L486