attack(OPE-5): n-queens 0-indexed construction, brute check 4..1000, Lean lemma plan (status: informal)

[agentforce314]

Summary

Attack Lead deliverable for OPE-5 (parent OPE-2, board-named n-queens). status: informal — no Lean compiled, no novelty claim (Pauls 1874 / Hoffman–Loessi–Moore 1969 / Bernhardsson 1991). Do not merge until the Director says so.

• attacks/n-queens-20260912-180329/LOG.md — 0-indexed closed forms against the frozen OPE-4 pin (ProofLab.NQueensTheorem.NonAttacking, queens_exists_of_four_le):
  • E1 (n even, n%6 ∈ {0,4}): if r < n/2 then 2r+1 else 2r-n
  • E2 (n even, n%6 = 2): Bernhardsson's second formula with % n resolved into four Nat branches
  • odd n: corner extension of the even n-1 board (side condition: no queen on the main diagonal)
  • per-case named lemmas (e1_lt/inj/anti/main/no_fix, e2_*, corner_*, one Fin transfer lemma nonAttacking_of_nat), each ≤ 10 lines and split_ifs <;> omega-shaped; no ZMod on the critical path
  • Lean-shaped lemma list in dependency order, wave estimate 1 (2 max), per-lemma Nat-subtraction / Fin / % hazards with mitigations
  • dead ends: 1-indexed list surgery, toroidal + corner, single % n for even n
• verify_construction.py + verify_output.txt — the three NonAttacking clauses evaluated verbatim over all ordered pairs for 4 ≤ n ≤ 1000: PASS, zero formula slips. Also checks the no_fix side condition, the optional 2r % n knight formula on n%6 ∈ {1,5}, and E2 on n%6 = 4 (bonus data).
• STATUS.json, STRATEGIES.md, one ledger entry in docs/PROBLEM_LEDGER.md.

How to verify

python3 attacks/n-queens-20260912-180329/verify_construction.py 1000   # ~26 s, exit 0, all PASS

Residual risks

• Mathematical: everything is linear arithmetic cross-checked to n = 1000; still informal until OPE-6's lake build is green with no sorryAx.
• Engineering: omega may stall on e2_main (16 piece-pair cases); the per-pair table in LOG.md is the fallback. Lemma statements are hand-typed, not compiled.

Handoff: OPE-6 (Formalist), then OPE-7 (Adversarial Reviewer).

🤖 Generated with Claude Code