factor_pinned_axisTTPlus
plain-language theorem explainer
Any real scalar relating the dictionary midpoint-Bloch m² to the geometric hinge-orbit m² on the plus TT polarization at symbolDir must equal 2. Gravity continuum-limit auditors cite this to pin the fold-to-dictionary factor as a measurement, not a free choice. The proof rewrites both sides to the banked values −1/2 and −1/4, then finishes by linear arithmetic.
Claim. Let $H_+$ be the unnormalized plus TT polarization $\mathrm{diag}(0,0,1,-1)$ and let $k=(1,1,0,0)$. If the cosine two-jet coefficient of the centered Bloch symbol at $(H_+,k)$ equals $c$ times the mixed geometric hinge-orbit moment at the same pair, then $c=2$.
background
This module (Arc 2, step 8) compares two m² objects on the 4D Regge lattice. The dictionary side is exactMidpointBlochM2: the cosine two-jet coefficient of the centered Bloch symbol, a weighted sum of −(phase)²/2 over couplings. The geometric side is m2AllOrbitMomentDistinctHingeEdgeOrigins: a mixed fold that keeps the legacy transported moment on the t11 orbit and uses edge-origin moments on the remaining star orbits.
The witness is the banked plus polarization $H_+=\mathrm{diag}(0,0,1,-1)$ (unnormalized) evaluated at symbolDir $k=(1,1,0,0)$. Upstream, the dictionary evaluates to $-1/2$ once TT and unit Frobenius/wave identities are applied; the geometric hinge moment evaluates to $-1/4$ by the exact flat Hessian symbol computation. The module thesis is that residual R1 (fold equals dictionary) is false, and the discrepancy is exactly a factor of two at both banked TT witnesses.
proof idea
Term-mode proof in two steps. Rewrite the hypothesis with the two evaluation lemmas: dictionary m² at $(H_+,k)$ is $-1/2$, geometric hinge m² is $-1/4$. The assumed relation becomes $-1/2 = c\cdot(-1/4)$. linarith forces $c=2$. No further case analysis or TT bookkeeping is needed here; those obligations live inside the two evaluation lemmas.
why it matters
Pins the fold-to-dictionary factor at the plus TT witness as a measured constant rather than a normalization choice. Together with the parallel cross-polarization pin, this supports the module claim that dictionary m² is exactly twice the geometric hinge moment at both banked TT witnesses, so the corrected residual is R1′ (twice the fold equals the dictionary), already present as discreteExactReggeSymbol.
In the continuum bookkeeping of Regge4DTorusContinuumLimit, the residual factor 4 (geometric $-1/16$ against Einstein-Hilbert $-1/4$) factors as two twos: this fold-to-action factor, and Regge's $1/\rho$ from step 7. Only the second was previously derived. No downstream consumers are wired yet; the result stands as the uniqueness half of the Arc 2 step-8 measurement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.