Adversarial audit of the 0.6725106958 candidate (2026-08-12)

An audit run from a fresh clone by a session that did not build any of the instruments below, against the source paper's own text. The brief was: attack the mathematics, and describe plainly whatever survives.

Result in one line. No error was found in the algebra, and one hole the ledger had left implicit was closed. What is not closed is a single named analytic lemma: the retention inequality is established as a genuine one-sided supremum over on-line configurations, but only at four sampled pair depths and over a swept family of pair sets, not uniformly in either. Until it is uniform, D >= theta*R0 is not available and the composition does not deliver the improved constant.

0. What was run

Fresh .venv, rigor.BACKEND = python-flint, both backends present.

1. The chain, restated from the source

Re-deriving the composition from the paper's Proposition 4.4 rather than from this hunt's own documents, to check for double counting.

The paper writes  = P₁ + Q′ (simple on-line block; everything else), and applies its Lemma 3.2 (rank–trace, via von Neumann) to get

‖Â‖²_F ≥ 2 tr P₁ − s₁ + 4 tr Q′ − 4(s₂ + p) (paper)

whence s₁ ≥ 4 tr  − 2N(I′) − ‖Â‖²_F, and with tr Ĝ = N(1+o(1)), ‖Ĝ‖²_F = N(1/c*₁ + o(1)), the constant 2 − 1/c*₁ = 0.6725007….

The hunt's route replaces Lemma 3.2 by the Frobenius expansion and treats the two blocks separately:

‖Â‖²_F = ‖P₁‖²_F + 2 tr(P₁Q′) + ‖Q′‖²_F ≥ (2 tr P₁ − s₁ + R) + 2 tr(P₁Q′) + (4 tr Q′ − 4 n₊(Q′))

using (n_i − 1)² ≥ 0 on the on-line side (which is where the +R comes from, R being the off-diagonal Gram mass the paper's spectral step never sees) and, on the off-line side, λ² ≥ 4λ − 4 for λ > 0 together with λ² ≥ 0 ≥ 4λ for λ ≤ 0, i.e. exactly the paper's own n₊(Q′) ≤ s₂ + p (its Prop 4.1). Subtracting:

The improvement over the paper is exactly R + 2 tr(P₁Q′).

This is not a double count. The 4 tr Q′ − 4 n₊(Q′) term appears identically in both routes; the hunt neither spends it twice nor needs the paper to have left it unused. The ledger's phrase "the 4-per-pair cushion the paper's (L) would have consumed" reads as though the cushion were the source of the gain; it is not. The gain is R + 2 tr(P₁Q′), and nothing else.

Why the per-pair decomposition is nevertheless forced. Taking ‖Q′‖²_F ≥ 4 tr Q′ − 4 n₊(Q′) whole leaves the requirement −2 tr(P₁Q′) ≤ (1−θ)R. Measured on this hunt's own worst adversarial placement that is 0.0796 ≤ 1.3e-5 — false by four orders of magnitude. So the chain must go per-pair,

‖Q′‖²_F = Σ_p ‖Q_p‖²_F + Σ_{p≠p′} tr(Q_p Q_{p′}), ‖Q_p‖²_F = (4 tr Q_p − 4 b_p) + slack(y_p),

and the load-bearing inequality is

−2 tr(P₁Q′) ≤ (1−θ) R + Σ_p slack(y_p) + Σ_{p≠p′} tr(Q_p Q_{p′}). (★)

The pair-pair term sits on the right, it is measured negative, and it is therefore load-bearing rather than decorative.

2. Closed by this audit: the pair-pair term is the dual's T_signed

paper_joint.budget charges Σ_r slack(y_r) + T_signed, with T_signed = 2 Σ_{i<j} T(t_i − t_j, y_i, y_j) and T(dt,y₁,y₂) = W(dt,|y₁−y₂|) + W(dt,y₁+y₂). Nothing in the tree pinned T_signed against the composition's Σ_{p≠p′} tr(Q_p Q_{p′}), so the identification dictionary had a fifth entry missing.

It is an identity. Writing Q_p = 2(x_p x_pᵀ − y_p y_pᵀ) with x_p + i y_p = v_{z_p}/√(2πA),

tr(Q_p Q_q) = 2 [ Re⟨v_p, v_q⟩² + Re⟨v_p, v̄_q⟩² ],

and LAW D turns the two inner products into Φ₂(Δt + i(y_p−y_q))/A and Φ₂(Δt + i(y_p+y_q))/A, which is W(Δt, y_p−y_q) + W(Δt, y_p+y_q).

Measured on explicit truncated-grid matrices (K = 1200):

Defects are the assembly's own ~1/K LAW D truncation. So the joint dual does budget the pair-pair term, and (★) is the statement its verdict makes.

3. Audit finding A: the end-to-end battery omits the term it is testing

identification_seam.end_to_end's SHARP row compares

damage := −2 tr(PQ) against (1−θ)R + Σ_p slack_p

with the pair-pair term absent from the left. By §1 it belongs there.

Re-run with damage − cross against the same budget, all eleven configurations still hold, with room:

So the omission changes no verdict in this battery — but the reason is that the battery's three binding rows are single-pair, where cross = 0 identically, and every multi-pair row uses the benign 9-point lattice whose damage is hugely negative. The battery therefore never tests the combination the adversary would actually choose: on-line points at the joint damage minima of a multi-pair field. The joint dual sweeps that supremum; the end-to-end matrix check does not corroborate it there.

Recommended: add multi-pair rows whose on-line points are placed at the joint field's minima (the _damage_minima device, applied to the summed field), and put cross on the left of the SHARP row.

4. Audit finding B: the shipped band instrument is unusable at shallow depth

PaperBandDual ships with step = 5e-4. Sweeping the depth continuum at θ = 0.995 with that step:

At y = 5e-4 the verdict is negative, and at y ≲ 1e-4 the instrument finds no bands at all and returns cap = 0 while its own no_missed_band control reports clear = False — a silent pass, not a pass.

This is the instrument, not the mathematics. A band has half-width ~y, and bands() adds a local slope margin slope·step whose ratio to the true band maximum scales as 2·step/y. Refining the step at fixed y confirms it (G = 100):

The refined ratio converges to ≈0.49 at every depth tested, the same value the shipped step reports at y = 0.02. So (★) looks comfortable and roughly depth-uniform down to at least y = 5e-4 — but the shipped instrument would report a false negative for any session that probed there, and the four depths the rational certificate covers are all in the region where the coarse step happens to be adequate.

Recommended: tie step to min(y)/40 (or accept a supplied step) and re-run the depth ladder; then extend band_certificate.py to a depth cover rather than four depth points.

5. What is universally quantified and what is sampled

Two mismatches worth naming, both routine to repair, neither yet repaired:

1. The Lean skeleton's hypothesis is ⟨u_i,u_i⟩ = 1. The paper's vectors are truncated to 0 ≤ k < d, so ‖u‖² ≤ 1 with equality only in the limit (its Lemma 2.2 sums over k ∈ ℤ). For sub-unit norms the conclusion is s ≥ 2 tr P − ‖P+Q‖²_F + D, not s ≥ 2N − …; the difference 2(N − tr P) is exactly what seam (i) has to show is o(N). The kernel-checked artifact therefore does not literally apply to the objects it is applied to.
2. Σ_p b_p = p vs n₊(Q′) ≤ s₂ + p. The per-pair route measures b_p = 1; the paper bounds the whole index. They agree when s₂ = 0. The multiple-on-line case (s₂ > 0) is not exercised by the battery.

6. Verdict

The mechanism is written down and correct as far as it goes; the improvement term is identified exactly; the composition is arithmetic and kernel-checked; the census floor has an exact rational dual; the retention has a rational cell-cover at the depths it covers. One analytic statement remains genuinely open, and it is the one the whole reading rests on:

Retention lemma (open). There is a θ ≥ 0.995 such that for every finite on-line configuration and every finite set of off-line pairs with depths in (0, ½], inequality (★) holds.

Established: the supremum over on-line configurations, for fixed pair sets, at four depths exactly and on a depth grid numerically. Not established: uniformity in the depth, and uniformity over pair sets. Without it the corollary's hypothesis D ≥ θ·R₀ is unavailable, and H + 2θc_u does not follow from the source paper's theorems.

The rest of the outstanding work — the units seam, the unit-vector hypothesis, the Lean leaves for the four kernel minima, the multi-pair rows in the battery — is bookkeeping and mechanisation, not discovery.

7. Follow-through (same day)

Both instrument defects are repaired and the untested corner is measured; the ledger entry "Audit follow-through" has the full record.

• Finding A: the cross term is on the left of the sharp row and three joint-minima rows are in the battery; all 14 rows hold.
• Finding B: PaperBandDual.for_depth resolves shallow depths (the y = 5e-4 ratio moves 1.436 → 0.5088) and the empty-band silent pass now reports undecided.
• The co-optimizing adversary (coopt_adversary.py): 57 restarts choosing pair positions, depths, on-line points and multiplicities together find no violation; the engaged worst case reaches 0.5754 of budget — worse than every swept family, 1.7× short of violation. The §6 obligation is unchanged; 0.5754 is now the number a uniformity proof has to beat.

8. Supersession (same day, parallel sessions on main)

Sessions working from this audit closed part of §6 before this branch merged; the ledger's three "Blocker" sections are the record. Current state of the §6 obligation:

• Depth uniformity: CLOSED at the single-pair layer (hardened, not kernel-checked): depth_uniform.py, 18 cells tiling (0, ½] with the shallow end closed by homogeneity rather than by cells — the y² damage scaling and the convexity of the square completion give one finite inequality for an interval with no smallest point.
• Pair-set uniformity: still OPEN, and the per-pair route is refuted. The joint cap is superadditive above the multiplicity threshold, and from four pairs on a unit lattice the per-pair sum exceeds the budget while the joint verdict closes — the joint field's shielding is load-bearing, exactly the corner §3 flagged. The obligation is now one bandlimited nonnegative-kernel inequality in two exponential sums (ledger, "Blocker 2").
• The asymptotic transfer is derived (factor exactly 1) with a headline caveat: the improvement is a liminf statement, not effective below T ≈ 10^(1.7×10⁶).

This section is a pointer, not a re-audit; grades are the ledger's.