Section 11 — Verification playbook (finite, rerunnable checks)

This section turns the key analytic inequalities used in the breakthrough-periodic approximation step into finite, rerunnable checks over the reduced presentation data.

The philosophy is:

• the proofs are still proofs, but
• every step that claims a concrete constant can be backed by a short script that re-derives that constant and runs a finite battery of sanity checks,
• so symbolic confusion is avoided and later refactors do not silently break hidden assumptions.

The harness lives in paper2_reduction/tools/verify_bundle.py.

11.1 What this harness checks

BCB fixed-length closing (graph-level check)

Given the presentation graph \(G\) and the pipeline-computed closing length \(L_0\), the harness checks

• \(A^{L_0}\) is strictly positive, where \(A\) is the boolean adjacency matrix of \(G\).

This is the machine version of:

• a mixing SFT has a mixing time,
• and in our chosen presentation we can close any start/end vertex pair with a word of exact length \(L_0\).

If this check fails, the bounded-closing property used in Section 8 is not available with the claimed \(L_0\).

Lemma 8.1 quasi-multiplicativity (sample check)

Let \(v\) be the positive bridge word and \(B=P(v)\).
Let \(\beta_{\min},\beta_{\max}>0\) be the entry-wise bounds so that
\[
\beta_{\min}\mathbf 1\mathbf 1^T\le B\le \beta_{\max}\mathbf 1\mathbf 1^T.
\]

The harness samples admissible words \(u\) of a fixed length, constructs connectors of length \(L_0\) to form a closed periodic word of the form
\[
w = u\alpha v\beta
\]
and verifies the Lemma 8.1 inequality in the scalarized norm
\[
\beta_{\min}\,s(U)\,s(W)\le s(UBW)\le \beta_{\max}\,s(U)\,s(W),
\]
with

• \(U=P(\beta)\),
• \(W=P(u\alpha)\),
• \(UBW=P(w)\),
• \(s(M)=\|M\mathbf 1\|_1\) which equals the sum of entries for nonnegative \(M\).

This does not prove the lemma (the proof is already in the paper).
It is a concrete regression check that the computed \(\beta\)-constants and the computed closing length \(L_0\) are numerically consistent with the intended inequality on typical instances.

Doeblin minorization/majorization (sample check, optional)

If doeblin.json exists, the harness samples vectors \(x\ge 0\) and checks that the computed \(\beta_{\min},\beta_{\max}\) for the Doeblin block \(B=P(u_*)\) satisfy the claimed coordinate-wise inequality
\[
\beta_{\min}\langle\mathbf 1,x\rangle\,\mathbf 1\le Bx\le \beta_{\max}\langle\mathbf 1,x\rangle\,\mathbf 1.
\]

11.2 How to run it

From the paper2_reduction directory:

python tools/verify_bundle.py --payload_dir payloads/example1

If you have already run the pipeline into a separate output directory, point --payload_dir to that output directory.

Available knobs:

• --trials controls the number of random samples used in the Lemma/Doeblin checks.
• --u_len controls the sampled word length for \(u\).
• --seed controls the RNG seed for reproducibility.

11.3 Produced artifacts

The harness writes two files into the payload/output directory:

• verification.json — a machine-readable record of which checks ran and which passed
• verification_report.md — a short human-readable summary (PASS or FAIL per check)

These files are also emitted automatically by tools/run_pipeline.py unless --skip_verify is used.

11.4 Reading failures

A failure is actionable:

• BCB failure means the claimed \(L_0\) does not actually close all pairs in the presentation graph.
• Lemma 8.1 sample failures most often indicate one of:
  • the computed bridge is not strictly positive in floating arithmetic,
  • the connector extraction is inconsistent with the exact-length convention,
  • an ordering mistake in the product convention (edge order vs multiplication order),
  • a mismatch between the norm used in the proof and the norm used in the computation.

The remedy is to re-check the product convention and confirm the bridge matrix positivity and connector extraction routine.