module module high

`IndisputableMonolith.Gravity.Analysis.ReggeTTHingeAwareZeroMode`

Defines the assembled hinge/edge-diagonal O(1) block of the real-space Regge Hessian at flat geometry: the factor 2πL'' contracted with edge-class polarization coefficients. Supplies a TT witness polarization and wave vector, and proves the hinge contribution cancels the recorded residual on that mode. Cited by the finite Bloch assembly and Gate B spike-convention bridge in the Paper C / Pillar 1 gravity campaign.

claimAt flat squared length $\ell_2^{(d)}$ of displacement class $d$, with $L(\ell_2)=\sqrt{\ell_2}$ so $L''(\ell_2)=-1/(4\ell_2\sqrt{\ell_2})$, the hinge/edge-diagonal block is the scalar $2\pi L''(\ell_2^{(d)})$ contracted against the edge-class coefficients of a polarization matrix. A fixed TT witness polarization and wave vector are exhibited; on that mode the hinge term cancels the recorded residual.

background

This module sits in the Regge TT analysis lane of the QG full-theory campaign (Paper C / Pillar 1). The upstream bucket-fiber aggregation module closes Gate C-A2f: the radical-bearing raw stencil coefficient $J_{fg}/(2\sqrt{a^*_f})$ (flat-angle Jacobian over Freudenthal flat edge data) equals a literal rational table on every bucket and all 36 slot pairs.

Here the focus shifts to the real-space Regge Hessian at flat geometry. Flat hinge deficits vanish, so the deficit constant $2\pi$ remains on the hinge diagonal. The length functional $L(\ell_2)=\sqrt{\ell_2}$ contributes the second derivative $L''$ evaluated at the flat squared length of each displacement class. Contracting that diagonal against edge-class coefficients of a polarization matrix yields the assembled O(1) hinge/edge-diagonal block, term-for-term the hinge object of the sympy diagnostic.

Sibling material includes elementary identities for $\sqrt{2}$ and $1/\sqrt{2}$, a TT witness polarization and wave vector, edge-coefficient extraction, a slot-displacement class map, and the cancellation statement that the hinge kills the recorded residual on the witness mode.

proof idea

Definition-heavy module with short algebraic lemmas. The hinge/edge-diagonal block is assembled by evaluating $2\pi L''$ at the flat squared length of each displacement class and contracting with polarization edge-class coefficients. Square-root identities ($\sqrt{2}\cdot\sqrt{2}=2$, inverse-square relations) discharge coefficient normalizations. The TT witness is checked to be transverse-traceless and its edge coefficients are read off. The main cancellation lemma equates the hinge contribution on that witness against the recorded residual and shows exact cancellation by direct arithmetic on the assembled block.

why it matters in Recognition Science

Feeds two downstream assembly stages. ReggeTTBlochAssembly is the C-DAG1 finite-cell assembly: cosine evaluators from bucket integer phase keys and normalized canonical finite cells for commensurate non-aliased wave vectors. ReggeTTGateBBridge closes Gate B (GateBConventionTarget): the interface moment fold built from the actual raw stencil equals the committed spike LHS under the seven TT hypotheses.

Without a hinge-aware zero mode and residual cancellation, the Bloch and Gate B pipelines cannot certify that the flat Hessian kernel is under control when edge-diagonal O(1) terms are retained. This module therefore supplies the local hinge block and witness that those parents import when they assemble finite cells and bridge spike conventions in Lane C of the finishing charter.

scope and limits

Does not assemble the full finite Bloch cell or cosine phase evaluator.
Does not prove the Gate B spike-convention identity under the seven TT hypotheses.
Does not treat curved backgrounds or non-flat hinge deficits.
Does not derive the bucket-fiber rational table; that is upstream aggregation.
Does not claim uniqueness of the TT witness beyond the exhibited polarization.

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