FoldTimesTwoEqDictionaryM2
plain-language theorem explainer
R1′ is the corrected residual: for every transverse-traceless pair (H,k), the dictionary m² moment equals twice the geometric hinge-fold m² moment. Auditors of the Regge continuum residual tree cite it in place of the false R1 (fold equals dictionary once). It is only a Prop definition; §4 of the module proves the equality at two banked witnesses, not universally.
Claim. For every real $4\times 4$ matrix $H$ and momentum $k\in\mathbb{R}^4$, if $(H,k)$ is transverse-traceless, then the exact midpoint Bloch $m^2$ moment of $(H,k)$ equals twice the geometric all-orbit distinct-hinge edge-origin $m^2$ moment of $(H,k)$.
background
Arc 2, step 8 of the gravity analysis asks what the Regge continuum convergence theorem actually converges to. Five typed residuals sit in the open residual bundle; four are inhabited. The fifth, R1, asserts that the geometric hinge fold equals the algebraic midpoint-Bloch dictionary. No inhabitant of R1 exists in the tree, and the module shows R1 is false.
At both banked transverse-traceless witnesses the dictionary $m^2$ is exactly twice the geometric hinge moment. The corrected residual is therefore R1′: twice the fold equals the dictionary, stated on $m^2$ moments (where every certificate lives). The tree already carries the doubled object as the discrete exact Regge symbol.
IsTT is the transverse-traceless predicate on the pair $(H,k)$. The left side is the dictionary $m^2$; the right side is the geometric all-orbit moment built from distinct hinge edge origins. The residual factor 4 in the torus continuum limit then factors as two twos: this fold-to-action factor, and Regge's $1/\rho$ from step 7.
proof idea
No proof: this is a bare Prop definition whose body is the universal statement above. The equality is the claim content, not a derived lemma. Downstream certificates that check R1′ at concrete witnesses inhabit instances of this Prop by direct numerical comparison of the two $m^2$ sides under IsTT.
why it matters
This declaration names the residual that should have been stated. Module narrative: R1 is false, the gap is exactly two, and only the corrected R1′ can carry continuum convergence to the mesh once the dictionary is bound. The residual factor 4 recorded in the torus continuum limit is then the product of this fold-to-action two and the step-7 Regge normalization two; only the second is derived from Einstein-Hilbert matching.
No downstream theorems currently depend on the name (used_by is empty). Its role is diagnostic and architectural: it separates the uninhabited universal claim from the weaker two-witness result proved in §4, so the two are never confused. Framework-wise it sits in the gravity analysis chain after T8-style dimensional forcing is already fixed and after the Regge coefficient question is closed; it does not touch the J-cost or phi-ladder landmarks directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.