actually
plain-language theorem explainer
In the 4D Regge continuum analysis, the geometric hinge-fold second-variation symbol is not the algebraic midpoint-Bloch dictionary: at both banked transverse-traceless witnesses the dictionary m² is exactly twice the geometric hinge moment. Gravity continuum-limit auditors cite this to split the residual factor 4 into two independent twos (fold-to-action versus Regge 1/ρ). The declaration is still a sorry stub packaging that measurement.
Claim. At the two banked transverse-traceless polarizations on the fixed Bloch direction with $|p|^2=2$ and Frobenius square $2$, the algebraic midpoint-Bloch dictionary mass-squared equals twice the geometric all-orbit hinge moment. Equivalently, the typed residual asserting equality of the exact flat cross-term fold with the midpoint-Bloch symbol is false; the corrected residual is that twice the fold matches the dictionary (already present as the discrete exact Regge symbol).
background
Arc 2, step 8 of the 4D Regge-to-Einstein-Hilbert program. Step 7 fixed Regge's normalization $\rho=1/2$ and showed that the banked dictionary coefficient $-1/8$ is the TT second variation of the Regge action against the continuum EH value $-1/4$. That closed coefficients; it did not identify which discrete symbol the mesh convergence theorem actually sends to the continuum.
The open residual bundle for geometric tendsto carries five typed residuals. Four are inhabited. The fifth (R1) asserts equality of the geometric hinge fold (exact flat cross-term fold) with the algebraic midpoint-Bloch symbol. Continuum preflight binds the dictionary, so only R1 would transport the convergence theorem onto the mesh.
Witness arithmetic is elementary: both banked TT axes have Frobenius square 2, and the banked direction has momentum square 2. Geometric certificates in this tree evaluate the hybrid all-orbit hinge moment (one legacy transported orbit, five edge-origin orbits), not yet a proved identity with the fold itself.
proof idea
Scaffolding: the proof body is an empty sorry stub. The intended route, recorded in the module narrative and sibling names, is direct evaluation at the two TT witnesses on the Bloch direction.
Compute dictionary $m^2$ on axis-TT-plus and axis-TT-cross via the midpoint-Bloch formula (and the TT identity that it equals $-\tfrac18$ times Frobenius for TT modes). Compute the geometric all-orbit hinge moment on the same two axes. Observe the exact ratio $2$ at both witnesses, hence dictionary $=2\times$ geometric moment, refuting bare fold$=$dictionary and justifying the doubled discrete exact Regge symbol as the corrected residual R1′.
§7 explains prior certificate blindness: two of four direction witnesses are gauge zeros (every factor agrees), and the other two were checked against a per-unit-momentum banked coefficient while certificates sit at $|p|^2=2$.
why it matters
Without this split, the torus continuum-limit residual factor 4 (geometric $-1/16$ versus EH $-1/4$) looks like a single unexplained normalization. The module shows it is a product of two twos: the fold-to-action factor measured here, and Regge's $1/\rho$ derived in step 7. Only the second is presently a derived theorem; the first is the content this stub is meant to host.
In the broader Recognition gravity stack this is the honesty checkpoint between discrete Regge symbols and the continuum EH TT Hessian: convergence claims must name the doubled symbol, not the bare fold. Downstream continuum and preflight wiring that bind the dictionary inherit the corrected residual. Linking the hybrid all-orbit moment used by every banked geometric certificate to the exact flat cross-term fold remains a separate uninhabited step (named in the module's §8), so the measurement is sharp at witnesses but not yet fully identified with the fold object in R1's wording.
Framework landmark contact is indirect: $D=3$ spatial (T8) and the eight-tick discrete calculus set the stage for 4D Regge analysis; this lemma is local continuum bookkeeping, not a new forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.