Validate Q26 proof with Lean 4.32.2

[jkolantree]

Summary

• upgrades the complete Q26 formal project to patched Lean 4.32.2 and mathlib 4.32.2;
• adds public CI for the full theorem build, patched-kernel module replay, and axiom audit;
• publishes the pinned Comparator receipt in which both Lean 4.32.2 and the independently implemented nanoda kernel accept the exact theorem; and
• binds all 26 proof-project Lean files, the dependency pins, trusted challenge, configuration, and retained transcript by hashes and the repository manifest.

Exact claim boundary

• Kernel theorem: no set of exactly thirteen queens dominates the 26 by 26 board.
• gamma(Q26) = 14 is the composite consequence of that theorem, Weakley's cited lower bound, and the independently checked 14-queen witness.
• The unrestricted root-CNF proof receipt remains UNKNOWN_UNCHANGED; this PR does not claim or transfer CNF UNSAT authority.
• Built-in leanchecker is described as a Lean-kernel replay, not an independent verifier. The 900-second local --fresh timeout is retained as NOT_CHECKED, while the separately implemented nanoda run is recorded independently.

Validation

• Lean 4.32.2 lake build: 8,679 / 8,679 jobs
• axiom audit: only propext, Classical.choice, and Quot.sound; exact shadow computation uses none
• patched-kernel module leanchecker: pass
• pinned sandboxed Comparator: nanoda accepted; Lean default kernel accepted; statement and axiom allowlist accepted
• Q26 checker/receipt tests: 11 / 11
• repository unit tests: 276 pass, one Windows symlink-privilege skip
• release inventory: 165 / 165 in source checkout, fresh clone, linked worktree, and Git archive

Reason for the correction

The original public validation used Lean 4.32.1. Lean 4.32.2 fixes a kernel soundness defect, so this follow-up removes 4.32.1 from the current validation path. It does not allege that the Q26 sources exploited that defect.

Advisory: https://lean-lang.org/doc/reference/latest/releases/v4.32.2/

[jkolantree]

CI follow-up: the first q26-lean-proof run did not report a Lean error. It compiled through 8,672 of 8,679 jobs, then received SIGTERM (exit 143) after more than ten minutes without log output during an expensive finite-classifier build. Commit 48cbb78 moves lake build out of the composite setup action and adds a 60-second heartbeat, while retaining a 50-minute step limit inside the 60-minute job limit. The exact build exit is still propagated by wait; no proof/checker gate was weakened. The failed run remains part of the public record.

[jkolantree]

Second CI follow-up: the heartbeat itself worked, but the shell-backgrounded, parallel Lake build was still SIGTERM-killed after Shadow and BoardShadow; no Lean proof error was reported. Commit ff12e1f removes the background main build and serializes the three high-memory modules (Shadow, BichromaticRecipe, MonochromaticRecipe) under a foreground Python supervisor with 60-second heartbeats and exact subprocess-exit propagation, followed by a bare lake build of the full default target. The prior failed run remains public; merge is still blocked pending a terminal green run.

[jkolantree]

Final public verification: PR #19 merged into main at commit 467b623. Post-merge Verify release run 31550096829 completed successfully on that exact commit: q26-lean-proof, verify, and build-pdfs all passed. The Lean job completed the 8,679-job default build, patched-kernel replay, and axiom audit. The exact root-CNF certificate track remains UNKNOWN_UNCHANGED.