oneOrbitRayNormalizedCoeff
plain-language theorem explainer
Defines the one-orbit ray coefficient of a 4×4 hinge matrix as the m2 Bloch symbol divided by the squared Euclidean norm of the fixed symbol direction. Gravity analysts cite it when comparing the transported (1,1)-orbit continuum ray against the frozen Einstein–Hilbert TT coefficient. The body is a one-line quotient of two already-defined real quantities.
Claim. For a $4\times 4$ real matrix $H$, the one-orbit ray-normalized coefficient is $m_2(H)\,/\,|k|^2$, where $m_2(H)$ is the double sum of slot coefficients over the 24 hinges and 10 time-types, and $|k|^2=\sum_{i=0}^{3} k_i^2$ with fixed direction $k=(1,1,0,0)$.
background
The module banks algebraic identities for the transported 4D Regge continuum sequence without claiming Einstein–Hilbert Tendsto to $-1/4$ on Frobenius TT or flipping the gap-action ledger. The concrete continuum object is the multi-orbit Bloch fold blochFoldAllDistinctHinge (weight $1/r_\tau$) on the torus family.
Mat4 is the preflight $4\times 4$ matrix type. The numerator m2Symbol H sums slot coefficients over all 24 hinges and 10 time slots. The denominator uses symbolDir, the fixed ray $k=(1,1,0,0)$ in $\mathbb{R}^4$, so $|k|^2=2$. The doc states that on axis TT this normalized coefficient equals $-3/2$, not the EH value $-1/4$.
Upstream cost algebra defines the shifted cost $H(x)=J(x)+1=\frac12(x+x^{-1})$ turning the Recognition Composition Law into d'Alembert form; that $H$ is unrelated to the matrix argument here beyond shared naming in the monolith.
proof idea
Pure definition: the body is the quotient of m2Symbol H by the sum of squares of the four components of symbolDir. No tactics, no lemmas applied at the definition site. Downstream evaluation on axis TT unfolds this definition, rewrites the numerator via m2Symbol_axisTTPlus and the denominator via symbolDir_normSq, then obtains $-3/2$ by arithmetic.
why it matters
This coefficient is the decoy-strengthening witness that the one-orbit ray after $|k|^2$ normalization is not the frozen Einstein–Hilbert TT coefficient. It feeds three local results: the explicit evaluation on axis TT equals $-3/2$; the inequality against einsteinHilbertTTCoefficient4D (which is $-1/4$); and the honesty theorem banked_does_not_inhabit_eh_or_flip_gap, which records that banked $(1,1)$ identities leave continuum EH Tendsto and gap-action recovery both false.
In the module's open list, Regge4DContinuumEHTarget (Tendsto of the normalized transported fold to $-1/4$ on Frobenius TT) and the pure-gauge zero target remain uninhabited. The definition therefore supports the disclosure that the algebraic closer does not flip gap_action_recovery and does not claim EH continuum recovery. It sits in the gravity analysis stack that prepares continuum symbol limits for Recognition Science's geometric sector, without yet closing the EH matching step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.