Symmetric rendezvous on unlabelled complete graphs below the Anderson–Weber constant: certified manuscripts, exact-rational certificates, Lean 4 formalization, and independent audit layer

Abstract

This record contains two companion manuscripts on symmetric rendezvous on unlabelled complete graphs, together with their complete reproducibility supplement Paper I (upper bound) constructs a legal symmetric strategy with lim E[T_n]/(n−1) = 0.82887837309423433534… < c_AW = 0.82888497379541092987…, with certified gap below −660/10^8, refuting asymptotic optimality of optimized ordinary Anderson–Weber play at leading order. Paper II (lower bound) proves the universal bound liminf V_n/n > I_0 + 11254877/10^8 = 0.71533218782648964537…, improving the best previously stated explicit benchmark 0.6389n − o(n) of Dani, Hayes, Moore, and Russell. The supplement archive contains the frozen research notes with SHA-256 manifests, the exact-rational certificate and verification scripts, a Lean 4 formalization of the upper-bound result (toolchain and mathlib pinned; axiom audit included), an independently written audit layer (five audit rounds, a dependency-free Lean audit core, and a constants bridge), the signed claims registers, and the manuscript sources. Verification entry points are listed in release/HOW_TO_VERIFY.md inside the archive; per-file integrity is recorded in SHA256SUMS, and the archived repository commit in SHA256SUMS.commit. No sign decision in the certificate chain uses floating-point arithmetic.