oneOrbitRayNormalizedCoeff_axisTTPlus
plain-language theorem explainer
The one-orbit ray-normalized coefficient of the plus TT polarization equals −3/2. Gravity analysts working the Regge–Bloch continuum limit cite this to separate the single-orbit M₂ symbol from the frozen Einstein–Hilbert target −1/4. The proof unfolds the normalized-coefficient definition and substitutes the known values m₂ = −3 and |symbolDir|² = 2.
Claim. For the plus transverse-traceless polarization $H=\mathrm{diag}(0,0,1,-1)$, the one-orbit ray coefficient $m_2(H)/|\mathrm{symbolDir}|^2$ equals $-3/2$.
background
This module banks algebraic identities for the transported 4D continuum sequence (the multi-orbit Bloch fold on the torus family) without claiming Einstein–Hilbert Tendsto to −1/4 or inhabiting the full continuum EH convergence Prop. The concrete continuum object is the distinct-hinge fold with weight 1/r_τ.
The plus TT axis is the unnormalized matrix diag(0,0,1,−1). The M₂ symbol on that axis evaluates to −3. The direction vector symbolDir has squared Euclidean norm 2 (sum of four coordinate squares). The one-orbit ray-normalized coefficient is the quotient of those two quantities: m₂(H) divided by |symbolDir|². The module doc records that for axis TT this quotient is −3/2, not the frozen EH coefficient −1/4.
proof idea
One-line algebraic evaluation. Unfold the definition of the normalized coefficient (m₂ over the squared norm of symbolDir). Rewrite with the two banked evaluations: m₂ on the plus TT axis equals −3, and the squared norm of symbolDir equals 2. The quotient is then (−3)/2.
why it matters
Feeds the immediate parent inequality oneOrbit_ray_normalized_ne_eh_coefficient, which shows the one-orbit ray coefficient on plus TT is not the frozen 4D Einstein–Hilbert TT coefficient. That decoy strengthening is listed among the banked theorems of the transported algebraic closer: it separates single-orbit M₂ data from the open continuum targets Regge4DContinuumEHTarget (Tendsto of the normalized transported fold to −1/4 on Frobenius TT) and Regge4DContinuumGaugeZeroTarget (Tendsto to 0 on pure gauge). The result does not flip gap_action_recovery and does not inhabit those open Tendsto Props; it only pins the algebraic ray coefficient used in the decoy comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.