factor_one_fails
plain-language theorem explainer
At the banked transverse-traceless plus axis on the fixed symbol direction, the midpoint-Bloch dictionary mass-squared is not one times the geometric hinge-fold moment. Anyone citing the Arc 2 step-8 refutation of residual R1 (fold equals dictionary) needs this inequality. The proof rewrites both sides to explicit rationals via the banked evaluations and finishes by numerical normalization.
Claim. At the banked transverse-traceless plus axis and the fixed symbol direction, the exact midpoint-Bloch dictionary second moment $m^2$ is unequal to $1$ times the geometric all-orbit distinct-hinge-edge-origin moment $m^2$. Equivalently the candidate scale $c=1$ fails, so residual R1 (geometric hinge fold equals algebraic dictionary) is refuted.
background
Arc 2, step 8 of the 4D Regge analysis asks what the continuum-convergence theorem actually converges to. Step 7 fixed Regge normalization $\rho=1/2$ and matched the Einstein-Hilbert transverse-traceless second variation, but said nothing about the mesh limit. The residual bundle carries five typed residuals; four are inhabited. The fifth, R1, asserts that the geometric hinge fold (exact flat cross-term fold of the Regge 4D action symbol) equals the algebraic midpoint-Bloch dictionary. No inhabitant of R1 exists in the tree.
This module compares the two objects at banked transverse-traceless witnesses on a fixed symbol direction. The dictionary side is the midpoint-Bloch $m^2$; the geometric side is the all-orbit hinge-edge-origin moment $m^2$. Sibling evaluations pin both numerals at the plus axis. The module thesis is that R1 is false and the honest gap is exactly a factor of two, so the residual factor four against the Einstein-Hilbert face factors as two times two.
proof idea
Short term-mode proof. Rewrite the left-hand side by the banked dictionary evaluation at the plus axis and symbol direction, and the right-hand side by the matching geometric evaluation. Both sides become explicit rational numerals. norm_num discharges the resulting numerical inequality. No further lemmas are needed beyond those two sibling evaluations.
why it matters
This is the direct refutation of residual R1 at the plus-axis witness: $c=1$ fails. Downstream, foldDictionaryFactorDischarged_holds packages it with the matching cross-axis inequality, the factor-four failure, the fold-times-two identity at the banked witnesses, and the Einstein-Hilbert face relation, discharging the fold-versus-dictionary bookkeeping bundle.
In the module narrative the residual factor four recorded on the torus continuum limit (geometric $-1/16$ against Einstein-Hilbert $-1/4$) splits into two twos: the fold-to-dictionary factor proved in this module, and Regge's $1/\rho$ from step 7. Only the second was previously derived. Closing R1 and replacing it by the doubled residual R1' (twice the fold equals the dictionary) is what lets the convergence chain point at the already-present doubled object rather than at an equality that never held.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.