Johnson graph coloring witness

Independently reconstruct the forum-reported table-seeded constant-weight exclusion map through k=500.

First action: Run `curl --fail --location --create-dirs --output sources/codes-se-cw-2026-07-21.html https://codes.se/bounds/cw.html`, then record its SHA-256 and retrieval timestamp before implementing tools/table_seeded_bound_audit.py.

Stop or redirect when: Stop when two independent exact update orders either reproduce exactly {16,112,256,268} with an origin ledger or expose the first irreducible missing or ambiguous seed. Do not extend beyond k=500 or begin a design/coloring search.

• Reconstruct the reported table-seeded constant-weight-code exclusions through k=500.
  Freeze codes.se/cw.html, build two exact fixed-point propagators with seed provenance, and compare the survivor sets.
• Formalize coloring implies LS(k-1,k,2k) and derived LS(4,5,k+5).
  Run /root/proof-factory/scripts/bootstrap-formal-conjectures.sh and compile the reduction against the pinned Property definition without sorry.
• Test tactical-decomposition constraints for LS(4,5,21).
  Encode only design-level intersection equations and validate the encoding on smaller known large-set controls.

• formal proof with premise retrieval
  Formalize the clique-to-Steiner-large-set reduction in the pinned Formal Conjectures environment and reuse nearby finite-set/coloring lemmas.
• counterexample and witness search
  Derive necessary Steiner large sets, validate their exact encodings on a known positive instance and adversarial corruptions, and distinguish independently reproducible bounds from unsupported reports.

• Infer nonexistence of S(4,5,21) from searches with prescribed automorphism groups.
  They do not cover asymmetric designs, and the authors explicitly describe the negative results as little evidence.
  Reopen only if: An unrestricted proof-checked enumeration or theorem exhausting all automorphism possibilities.
• Treat the forum's k<=500 four-survivor statement as established.
  No frozen seeds, implementation, origin ledger, or certificate was supplied, and the independently run bare recurrence leaves every prime offset.
  Reopen only if: Two independently implemented exact table-seeded propagations with matching origin ledgers.
• Naive direct SAT encoding of J(32,16) on the audited host.
  It requires over 10.2 billion color variables and roughly 1.31 trillion edge-color clauses.
  Reopen only if: A rigorous compression, orbit theorem, or structural reduction changing the scale by orders of magnitude.
• Present one S(4,5,21) model as a solution to Erdős #835.
  The coloring implies LS(15,16,32), and derivation gives LS(4,5,21), not merely one constituent design.
  Reopen only if: Supply a proved lift or a complete independently checked coloring.