FoldDictionaryFactorDischarged
plain-language theorem explainer
Discriminating gate for Arc 2 step 8: a six-conjunct Prop that pins the geometric hinge fold against the algebraic dictionary at the banked TT witnesses. Gravity continuum-limit auditors cite it when tracking the residual factor four (two from fold-to-dictionary, two from Regge 1/ρ). The body is a pure conjunction of three equalities and three inequalities, not a Boolean success flag.
Claim. The discriminating gate is the conjunction of: (i) at both banked transverse-traceless witnesses, the midpoint Bloch dictionary $m^2$ equals twice the geometric hinge-orbit moment; (ii) at the plus polarization $H_+=\mathrm{diag}(0,0,1,-1)$ and symbol direction $k=(1,1,0,0)$, those two numbers are unequal; (iii) the dictionary is neither $1$ nor $4$ times the geometric moment; (iv) the continuum Einstein-Hilbert face equals four times the geometric moment; (v) the product of the two discrete bookkeeping factors equals $4$.
background
Arc 2 step 8 sits after step 7 closed the coefficient question: the Einstein-Hilbert TT second variation is $-(1/4)$ per unit Frobenius and momentum, Regge normalization is $\rho=1/2$, and the banked dictionary's $-(1/8)$ matches the second variation of the Regge action. That said nothing about what the mesh convergence theorem actually converges to.
Five typed residuals appear in the continuum preflight. Four are inhabited. The fifth (R1) asserts that the geometric hinge fold equals the algebraic midpoint Bloch dictionary; no inhabitant exists. At the banked TT witnesses the dictionary $m^2$ is exactly twice the geometric hinge moment, so the corrected residual is R1$'$ (twice the fold equals the dictionary). The residual factor $4$ in the torus continuum limit is then a product of two twos: fold-to-action, and Regge's $1/\rho$.
The continuum EH face is $-(1/4),|k|^2|H|_F^2$. The geometric side is the mixed orbit hinge moment (legacy transport on one star class, edge origins on the others). The two discrete bookkeeping factors are each the dimension-independent factor $2$ from the $ttSecondDifference=(2/N^3)S''$ convention.
proof idea
Definitional Prop package, not a proved theorem. The body is the literal six-way conjunction of: the named banked-witness statement (twice fold equals dictionary at plus and cross), three numerical refutations at the plus witness and symbol direction (geometric $\neq$ dictionary; dictionary $\neq 1\cdot$ geometric; dictionary $\neq 4\cdot$ geometric), the EH-face identity (face equals four times geometric), and the product of the two bookkeeping constants equaling $4$. Discharge is deferred to the sibling theorem that inhabits this Prop.
why it matters
This gate is the honest reading of the convergence chain after step 8. Module narrative: R1 is false, the gap is exactly two, and earlier certificate suites could not catch it (two of four witnesses on the symbol direction are gauge zeros; the other two compared values at $|k|^2=2$ against a per-unit-momentum banked coefficient). Downstream, foldDictionaryFactorDischarged_holds inhabits the gate, and the step-8 audit package conjoins it with the statement that convergence reaches the dictionary, not the bare hinge moment. Only the Regge $1/\rho$ half of the residual factor four was derived in step 7; this gate records the fold-to-dictionary half as a banked equality plus discriminating refutations, so the gate fails if any of the four numbers moves.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.