factor_four_fails
plain-language theorem explainer
At the plus TT polarization and banked symbol direction, the algebraic midpoint-Bloch m² is not four times the geometric hinge-orbit moment. Anyone tracking the fold-to-Einstein-Hilbert residual factor of 4 cites this to rule out a single bookkeeping factor of 4. The proof rewrites both sides to explicit rationals and finishes by norm_num.
Claim. For the plus transverse-traceless polarization $\mathrm{diag}(0,0,1,-1)$ and the banked symbol direction, the exact midpoint Bloch second-moment $m^2$ is not equal to four times the geometric all-orbit distinct-hinge-edge-origin moment at the same data: $m^2_{\mathrm{dict}} \neq 4\, m^2_{\mathrm{geom}}$.
background
This module (Arc 2, step 8) separates what the Regge tree actually converges from the Einstein-Hilbert face. Step 7 fixed Regge normalization $\rho=1/2$ and the EH transverse-traceless second variation $-1/4$ per unit Frobenius and momentum, so the banked dictionary coefficient $-1/8$ matches the Regge action. Convergence still needs the geometric hinge fold to match that dictionary; the residual package treats that identification as R1, and R1 has no inhabitant.
The five typed residuals of the continuum preflight include R1 (fold equals midpoint Bloch dictionary). Here one shows R1 is false at banked TT witnesses: dictionary $m^2$ is twice the geometric hinge moment, not equal to it. The residual factor 4 between geometric $-1/16$ and EH $-1/4$ therefore factors as two twos: fold-to-dictionary and Regge $1/\rho$.
The plus polarization is the unnormalized matrix with $1$ and $-1$ on the last two diagonal entries. Upstream, the dictionary evaluation at this polarization and symbol direction is the explicit value $-1/2$, via the TT identity reducing midpoint Bloch $m^2$ to $-\frac18$ times Frobenius times wave weight.
proof idea
Term-mode, two rewrites then arithmetic. Replace the left-hand side by the banked dictionary evaluation dict_m2_axisTTPlus_symbolDir, which gives $-1/2$. Replace the right-hand side coefficient via geom_m2_axisTTPlus_symbolDir, the geometric hinge-orbit moment at the same TT witness and symbol direction. norm_num checks the resulting rational inequality (equivalently $-1/2 \neq 4\cdot m^2_{\mathrm{geom}}$). No case splits or external analytic lemmas beyond those two closed evaluations.
why it matters
Closes one conjunct of the fold-versus-dictionary discharge package. Downstream, foldDictionaryFactorDischarged_holds assembles: twice the fold equals the dictionary at banked witnesses, geometric side differs from dictionary, factor one fails, factor four fails, the EH face is four times the geometric side, and the two bookkeeping factors are distinct. The module doc states the honest reading: the recorded residual 4 is a product of two twos, and only Regge's $1/\rho$ (step 7) is derived; the fold-to-action two is measured here, not forced from first principles.
In the continuum chain this blocks treating the whole EH gap as a single normalization constant $c=4$ on the fold. It supports replacing R1 by R1' (twice the geometric fold equals the dictionary) and pointing at the already-present doubled object discreteExactReggeSymbol. No direct link to T0-T8 or the RCL; this is pure 4D Regge symbol bookkeeping inside the gravity analysis arc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.