step8_audit_package
plain-language theorem explainer
The step-8 audit package asserts that the fold-to-dictionary discriminating gate holds and that convergence reaches the dictionary rather than the hinge moment. Both geometric orbit moments differ from the exact midpoint Bloch M2 on the TT-plus and TT-cross axes, while fold-times-two matches the dictionary at the banked witnesses. Gravity analysts checking the 4D geometric-fold versus dictionary arc would cite it. The proof is a one-line pairing of the two already-proved component theorems.
Claim. The discriminating gate for the fold-dictionary factor is discharged, and the honest convergence reading holds: the geometric all-orbit moments with distinct hinge edge origins differ from the exact midpoint Bloch $M_2$ on both the TT-plus and TT-cross axes, fold-times-two equals the dictionary at the banked witnesses, and the unit and fourfold bookkeeping factors fail as required.
background
This module is the axiom audit for arc 2, step 8 of the 4D geometric-fold versus dictionary comparison. The expected axiom set is the base triple (propext, Classical.choice, Quot.sound). The dictionary side descends from the exact-midpoint Bloch $M_2$ identity whose coefficient-table certificates are kernel-lifted from banked integer decide chunks; the geometric side descends from edge-origin decide certificates over a finite index set. Neither side adds axioms.
The discriminating gate packages six conjuncts (three of them refutations): fold-times-two equals the dictionary at banked witnesses, the geometric all-orbit moment differs from the exact midpoint Bloch $M_2$ on the TT-plus axis, and the unit and fourfold factor equalities fail, with the Einstein-Hilbert face equal to four times the geometric value. The honest convergence reading restates the two geometric-versus-dictionary inequalities (TT-plus and TT-cross) together with the same fold-times-two identity. Upstream scope results fix the Einstein-Hilbert face coefficient as $2\cdot(-1/8)$ times the Frobenius norm squared, show the mesh sequence converges to the Regge face (Regge normalization times that coefficient), and show it does not converge to the Einstein-Hilbert face.
proof idea
One-line term proof: pair the two already-established component theorems. The first supplies the discriminating gate (fold-times-two at banked witnesses, geometric-versus-dictionary inequality on TT-plus, failed unit and fourfold factors, Einstein-Hilbert face equal to four times geometry, and the remaining bookkeeping factor). The second supplies the honest convergence reading (geometric-versus-dictionary inequalities on both TT-plus and TT-cross, plus fold-times-two again). No new algebra is performed here; the package is pure conjunction assembly for the audit printout.
why it matters
This is the terminal audit package for arc 2 step 8: it records that the discriminating gate holds and that the two refutations making it discriminating are present. Downstream use sites are empty; the declaration exists so that a single named theorem, together with the surrounding axiom-print commands, certifies a clean base triple for the whole GeometricFoldVsDictionary4D development and the related SRS scope lemmas (mesh convergence to the Regge face, non-convergence to the Einstein-Hilbert face, and the collision that the moments read their symbols). In the gravity analysis chain it separates the geometric fold from the dictionary midpoint and locks the fold factor of two, preventing a silent collapse of the two sides. It does not itself advance a new physical law; it closes the bookkeeping so later continuum or mass-ladder work can cite a discharged gate rather than an open comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.