Part V — The Theorem · seven builds, seven receipts
These experiments are about making the honest map executable on your own bench — forcing the substrate to declare a regime, reproducing the wrong-direction ratio that taught T5 to disclose, watching distributed Lanczos close the gap that disclosure protected, and stressing the writes-side resolver until it refuses for the right reason. The receipt class is the one the chapter trades in: a PASS row on the validator, a ratio inside a published band, a refusal variant returned at the type level, a \(K\) count that tracks the spectral gap.
Run it live — GQL console
Point at the public read-only instance (no key needed) or your own engine
(start it with GIGI_CORS_ORIGIN=* for browser access — dev only).
—
E14.1Reproduce the wrong-direction ratio
Build
Run the T5 validator script (t5_cauchy_interlacing_lambda1.py under theory/poincare_to_sharding/validation/) unmodified against the three random-regular expander cases \((50,4)\), \((100,4)\), \((100,6)\) and capture the ratio (naive / true) line from each.
Receipt
Three ratios landing in the \(0.144\)–\(0.209\) band the chapter published, with run_natural_clustering_case returning naive_bound_holds == False and matches_expectation == True on every expander row — the failure the validator was configured to expect.
Bonus
Add a \((200, 4)\) row and confirm the ratio stays in-band; the wrong-direction factor is structural, not finite-size noise.
E14.2Wire SpectralRegime onto a fresh bundle
Build
Take any ShardedBundle you can hand-construct and declare its regime three ways: NaturallyCluster, Expander, and CertifiedClusteredAt { conductance: 0.05 }. Call allows_naive_recipe() and requires_distributed_lanczos() on each and tabulate the four answer cells.
Receipt
A four-row table whose entries match the predicates in src/sharded/regime.rs:39-49 exactly — NaturallyCluster and CertifiedClusteredAt allow the naive recipe, Expander alone routes to Lanczos.
Bonus
Construct a CertifiedClusteredAt with conductance: 0.5 and argue from the chapter's natural-clustering vs.\ expander dichotomy why the threshold for trusting that variant is a separate calibration the spec writer owes.
E14.3Time distributed Lanczos against \(K_{4,4}\)
Build
Run the in-tree test lambda_1_blocks_works_on_expander at src/sharded/execution.rs:1001-1029 and instrument the call to record both result.lambda_1 and result.iterations_used.
Receipt
A log line showing \(\lambda_1\) within \(10^{-6}\) of \(4.0\) and an iteration count \(K\) at or below the k_max = 120 default — the canonical T5-failure case recovered exactly by the universal path I shipped in T7.
Bonus
Repeat for \(K_{8,8}\) and \(K_{16,16}\), plot \(K\) against bipartite size, and verify the count stays roughly constant rather than scaling with \(n\) — the wide spectral gap is what makes Lanczos cheap on expanders.
E14.4Benchmark \(K\) across the validator's substrate classes
Build
Run theory/sharding/validation/t7_distributed_lanczos.py and reproduce the live receipt table at the bottom of §14.5 — seven rows across \(P_{50}\), \(P_{100}\), \(C_{50}\), \(C_{100}\), and the three expanders.
Receipt
A SUMMARY block whose \(K\) column matches the chapter's published values within \(\pm 2\) iterations (\(K \approx 49, 99, 25, 50, 39, 65, 44\)) and whose err column lands at \(10^{-11}\) or tighter on every row.
Bonus
Plot \(K\) against \(1/\lambda_2\) on a log-log scale across all seven rows and check the predicted linear-in-inverse-gap relationship Lanczos converges at.
E14.5Refute the precondition with a malformed batch
Build
Construct two WriteConflict batches: one with a lonely conflict (no canceling partner) and one with two same-sign conflicts. Hand each to sharded_write_resolve in src/sharded/resolver.rs:47-58.
Receipt
The first call returns Err(NoCancelingPartner { conflict_id }), the second returns Err(SameSignPartners { a, b, sign }); neither batch is processed. The resolver refuses at the type level, which is the honest writes-side disclosure the chapter named.
Bonus
Add a third batch of \(N = 100\) balanced conflicts and confirm ResolverTrace.steps == 50 with zero residual — the topological-termination receipt from Theorem 5.3 of my paper running on the engine.
E14.6Stress the cross-atlas resolver across the bridge
Build
Reproduce resolver_terminates_in_exactly_n_over_2_steps at src/sharded/cross_atlas.rs:623-633 and extend the loop to include \(n_{\text{pairs}} \in \{500, 1000\}\). Record trace.steps, trace.residual_size, and the diagnostic counts of intra-atlas-A, intra-atlas-B, and bridge pairs.
Receipt
steps == n_total / 2 and residual_size == 0 on every row, with the bridge-pair count non-zero on at least one row — T10's atlas-agnostic claim surviving at scale.
Bonus
Inject a single same-sign pair into the \(n = 1000\) batch and confirm cross_atlas_write_resolve returns a CrossAtlasResolverError variant rather than running to completion.
E14.7Forge the analytic-bridge cocycle gate
Build
Construct a CrossAtlasJoin between two analytic atlases of the same shared geometry and call cross_atlas_cocycle_check at src/sharded/cross_atlas.rs:222 with observed-slack maps populated from the two derived bridges.
Receipt
The forward triples and the round-trip pair both rule observed \(\leq\) budget with \(\delta_{\text{bridge}}\) and \(\delta_{\text{asymm}}\) at machine precision — the analytic-atlas case the chapter promised hits the budget at zero.
Bonus
Perturb one bridge by a small \(\varepsilon\), rerun, and confirm both slacks grow first-order in \(\varepsilon\) as T8 predicts; this is the cocycle survival receipt Part VI's encryption layer is going to lean on.