closeout(OPE-2): n-queens formalized, no claim — integrates #3/#5/#6/#7 + erratum + claim packet - #8
Open
agentforce314 wants to merge 10 commits into
Open
agentforce314 wants to merge 10 commits into
agentforce314 wants to merge 10 commits into
Conversation
… pin - Disambiguate five "n-queens" readings on the feasibility rubric; target (a) existence iff n≠2,3 scores 88; expected known-classical, formalize-only - Pin Lean-shaped statement: NonAttacking (Fin n → Fin n, injective + both subtraction-free diagonal families) and n_queens_exists_iff; n=0 convention - Novelty pre-screen: local Mathlib a719ba5c31 (v4.10.0) grep, ZERO named n-queens theorem; literature handles Pauls 1874 / HLM 1969 / Bernhardsson 1991 / Bell–Stevens 2009; PR Paul3435#174 Level A cited as prior art, not solution - Catalog row → shortlisted; ledger block + table row; mathforge score run - Verify: python3 test_mathforge.py (11 OK); python3 bin/mathforge status
…y on branch only) - New ProofLab/NQueensTheorem.lean: NonAttacking (Fin n → Fin n) and n_queens_exists_iff copied verbatim from the Scout pin; optional split queens_exists_of_four_le; both tagged STUB: proof in OPE-6 - decide-level sanity: NonAttacking ![1,3,0,2] (PR Paul3435#174 n=4 witness) - ProofLab.lean imports the new module; ProofLab/NQueens.lean untouched - STATEMENT.md: carries PR #3 text + appended 'Lean pin' section with build tail and #print axioms (now [sorryAx]; done requires none) - Verify: lake build ProofLab.NQueensTheorem exit 0, 2 sorry warnings Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…Lean lemma plan (status: informal) - attacks/n-queens-20260912-180329/: LOG.md (formulas E1/E2/corner, named lemmas, dead ends, Lean-shaped lemma list, wave estimate, hazards), STATUS.json, STRATEGIES.md, verify_construction.py + verify_output.txt (PASS 4<=n<=1000, NonAttacking clauses checked verbatim) - docs/PROBLEM_LEDGER.md: OPE-5 entry No Lean compiled; no novelty claim; handoff to OPE-6. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… E1/E2 + corner extension) Proves n_queens_exists_iff and queens_exists_of_four_le in ProofLab/NQueensTheorem.lean; frozen statements from the OPE-4 pin are byte-identical. Route is the Attack Lead's (OPE-5) 3-formula partition, entirely in ℕ → ℕ with one Fin transfer lemma. n = 2, 3 nonexistence by kernel decide on the function encoding. #print axioms: [propext, Classical.choice, Quot.sound]. Supersedes PR #4. Deviations from the LOG text: f₂ pieces P3/P4 written with the addition first (2*r + 2 - …) to avoid ℕ truncation; e2_no_fix needs 4 ≤ n. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…LOG.md f₂ erratum - ADVERSARIAL_REVIEW.md: fresh rebuild (Built, not Replayed), own #print axioms, keyword grep, cold read of NonAttacking, negative controls per clause, deviations (a)/(b) confirmed, hypothesis diff table, scope/claim posture, machine-trust boundary, 8 residual risks. Verdict: APPROVE WITH RESIDUALS. - review_checks.lean + .out: scratch file run with lake env lean (exit 0). - review_check_f2.py: LOG typed ℕ-form vs signed vs Lean form, 8<=n<=1000. No claim. Artifact reviewed: origin/ope/6-nqueens-proof @ 8ae158a. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…-nqueens-closeout
…nqueens-closeout # Conflicts: # catalog/problems/n-queens/STATEMENT.md
…-nqueens-closeout
… LOG.md erratum, ledger/catalog, claim packet - Integrates ope/3 (Scout), ope/5 (Attack Lead), ope/6 (Formalist proof), ope/7 (Reviewer); one trivial STATEMENT.md conflict resolved by taking the ope/6 version (ope/3 + OPE-4 pin section). - attacks/n-queens-20260912-180329/LOG.md: erratum header + in-place fix of typed f₂ P3/P4 (ℕ-truncation) and e2_no_fix (needs 4 ≤ n), as confirmed by OPE-6 and OPE-7. - STATUS.json → closed-formalized. Ledger + catalog + DOSSIER + feasibility → formalized. - problems/n-queens/CLAIM_PACKET.md via mathforge claim prepare: recommendation NO CLAIM. - Verified on this branch: lake build ProofLab.NQueensTheorem fresh Built, zero sorry, #print axioms = [propext, Classical.choice, Quot.sound]; Reviewer review_checks.lean exit 0. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…c, PDF) - proofs/n-queens/paper/main.tex: internal lab report — statement, 0-indexed construction with Lean lemma tags, formalization + verification, adversarial review (negative controls, hypothesis diff), process/timeline, residual risks, lessons; appendices \VerbatimInput the Lean source and the review/verify transcripts from the repo so they cannot drift. - build.sh: tectonic (XeTeX, bundle fonts by filename). tectonic 0.17.0 installed user-locally at ~/.local/bin (board OK for user-local tooling). - main.pdf committed (18 pp, 120 KB). Ledger row + catalog artifacts point at it. - Claim posture unchanged: internal report, no external claim. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Director close-out — OPE-2 "solve the n-queens problem" (board-named, full process)
Disposition:
formalized, no claim. This PR is the integration of the whole chain plus the close-out artifacts. Merging it (merge commit, not squash) makes #3, #5, #6, #7 redundant — GitHub will mark them merged. #4 is superseded by #6 and should be closed without merging (it carriessorry).What is in here
ope/3-nqueens-scout(OPE-3: n-queens fresh Scout dossier + Level B statement pin (board-named) #3),ope/5-nqueens-attack(attack(OPE-5): n-queens 0-indexed construction, brute check 4..1000, Lean lemma plan (status: informal) #5),ope/6-nqueens-proof(formalist(OPE-6): n-queens namesake theorem, zero sorry (supersedes #4) #6),ope/7-nqueens-review(review(OPE-7): n-queens adversarial review — APPROVE WITH RESIDUALS #7). One trivial conflict incatalog/problems/n-queens/STATEMENT.md(ope/6 = ope/3 + the OPE-4 "Lean pin" section) resolved by taking the ope/6 version.attacks/n-queens-20260912-180329/LOG.mderratum (confirmed by OPE-6 Formalist and OPE-7 Reviewer): typedf₂P3/P4 pieces truncated in ℕ (fixed to2 * r + 2 - n / 2/2 * r + 2 - 3 * (n / 2));e2_no_fixneeded4 ≤ n. Original wording preserved via the header note;STATUS.json→closed-formalized.formalized, no claim, residuals listed.problems/n-queens/CLAIM_PACKET.mdviamathforge claim prepare n-queens, filled in: recommendation NO CLAIM / internal note only.Verification (Director, on this branch)
Residual risks (board-facing, from OPE-7 — no claim regardless)
IsNQueensencoding (OPE-1424: n-queens Level A (n=2 none / n=3 none / n=4 [1,3,0,2]) Paul3435/open-math-lab#174). 2. Only reading (a) existence; (b) counting / (c) asymptotics / (d) completion / (e) toroidal untouched. 3. Definition fidelity is human judgement. 4. Single-machine toolchain, nolean4checker. 5. No novelty; Mathlib screen local-pin only. 6. LOG.md erratum (fixed here). 7.n ≠ 2 ∧ n ≠ 3includes vacuousn = 0. 8. Unusedimport ProofLab.NQueens(harmless).Board merges. Paperclip: OPE-2 (parent), OPE-3..OPE-7 (children, all done).
🤖 Generated with Claude Code