Complete and externally validate the exact Q26 result

.github/workflows/verify-release.yml

@@ -72,9 +72,9 @@ jobs:
                   raise SystemExit(return_code)
           PY
 
-      - name: Replay the theorem through the patched Lean kernel
+      - name: Replay the definitive theorem through the patched Lean kernel
         working-directory: formal/q26_grid_annihilator
-        run: lake env leanchecker Q26GridAnnihilator.Unconditional
+        run: lake env leanchecker Q26GridAnnihilator.Definitive
 
       - name: Print the theorem axiom boundary
         working-directory: formal/q26_grid_annihilator

CHANGELOG.md

@@ -1,5 +1,29 @@
 # Changelog
 
+## Post-v1.4.0 definitive Q26 Lean theorem - 2026-08-11
+
+This follow-up adds a direct verdict theorem to the Q26 Lean project:
+
+- formalizes the retained fourteen-queen witness and checks both its exact
+  cardinality and domination of all 676 board squares;
+- upgrades the exact-cardinality-thirteen obstruction to a lower bound for
+  every dominating set by a monotonicity and finite-padding argument;
+- exports `Q26GridAnnihilator.q26_domination_exact`, which directly gives a
+  fourteen-queen dominator and proves that every dominator has at least
+  fourteen queens; and
+- changes public CI's patched-kernel replay target from `Unconditional` to
+  `Definitive`.
+
+Thus the final equality no longer depends on importing Weakley's lower bound
+or an external witness check. A v2 external receipt uses a self-contained
+challenge for both `no_thirteen_queen_dominator` and `q26_domination_exact`;
+the Lean 4.32.2 kernel and independently implemented nanoda kernel accepted
+both statements. Its projection binds 27 Lean files, while the application
+source manifest contains those files plus three project pins, for 30 entries.
+The retained run took 922.842 seconds and peaked at 21.8 GB. The unrestricted
+root-CNF certificate status remains `UNKNOWN`; this theorem is not an
+LRAT/DRAT replay receipt.
+
 ## Post-v1.4.0 Q26 patched-kernel validation - 2026-08-11
 
 This follow-up hardens the published exact-cardinality Q26 theorem after a

MANIFEST.sha256

@@ -4,11 +4,11 @@ f28298c16fdb91b16ca87bead23a9293e3edf25a1c8bfaf8a4269c53eae8ec86  ./.github/ISSU
 5df874a2694a1e3fd39854be78dc737afec989d1b0edca8a648944a553014766  ./.github/ISSUE_TEMPLATE/prior-art-equivalence.yml
 5e8e4a3fc0fcd563eb5ea5ddc1f2546ed101df4cd55e97f07d7b17c21fcf1f32  ./.github/ISSUE_TEMPLATE/scope-correction.yml
 541ab3b54a149a763f66985e8062ad73795e7a4e6587e9a6335ca09e5dbdf014  ./.github/ISSUE_TEMPLATE/type-or-proof-error.yml
-61c8084033967113d668c398ceb311dc324d9ccaaed980b5642d16769f3b119e  ./.github/workflows/verify-release.yml
+694edb141248a79ab0179b813c29a74b08f211889e7d7b2cc9b91fa070eac293  ./.github/workflows/verify-release.yml
 2eb56f5d30d92fdd871d8bb8a83adbccbe6b15175d8a18be925794be78e3ce77  ./.gitignore
 ee4a4ebfc2de9f960f032576bfd57236e37dc9c465fdecce35c2a81da05f9e5c  ./.zenodo.json
 c8fe1c48196b4e8591f5e78bc0b29c7e1ac6a855b4e2df7e0ef47125a69836df  ./AUDIT_REPORT_v1.0.0.md
-2483ec52076d94a9a4e553223860133a106a40da308f52a5985cc7d9c687cdb2  ./CHANGELOG.md
+9fb4243918b0472fcce855b253e5b7f9986b5ad96dd917e92f7b2dc6d789aa9a  ./CHANGELOG.md
 06e6fc8cb5e118923e639f298a74cc62221bebd529010fe19488c26e8d4d72b8  ./CITATION.cff
 ccff4822b8d2bb3ec2dba332283eafd5193db3639e1bd5d35e40fce9f5c65f0f  ./CONTRIBUTING.md
 632c312b84e5f440444e2cd25513eacf41e4876ddcac3e64f5ca9591c7be24eb  ./DISCLOSURE.md
@@ -17,7 +17,7 @@ a4b6a51b30cc788052b4a2f276ba88d0effbd998cf408d89cceb5c8f4a6f645c  ./LICENSE
 c8747e82b4e652035f2390ae648c0baabba2c3ad0f47c6d27d3c8e6d706284a3  ./LICENSES/code.txt
 d633b150311aa162b4b4baec0580a6ad4a0997e0cbf1226963fd86c0112451ac  ./LICENSES/paper-and-documentation.txt
 8609a8f220f0f69fad5476fb5a66c9edf5e681563e86029e34e0327cf1cfd1f3  ./Makefile
-dac2d96ea95024dbc6001479740fe035c7305741a93da5a05b439c56c9fa60d8  ./README.md
+0078e0e34fb293e0bd2b6833d366ad0a05a4fd93a15193b6efa3931e6c7b3ca6  ./README.md
 c3fa014b23879048885b4a04757dd05e2129102e0582d62b82ef346a4564731b  ./REPRODUCING.md
 f5000369c499804337d2ea58b0be4eb9ae8800bc13eb008989eb2bfcb8ce4f5d  ./ROADMAP.md
 d9b1b2120d21a8e4e13c345d982fea9d96a42ee0c1ae6853c4dbe8bd380c7b2b  ./SOURCE_AVAILABILITY.md
@@ -26,11 +26,11 @@ d9b1b2120d21a8e4e13c345d982fea9d96a42ee0c1ae6853c4dbe8bd380c7b2b  ./SOURCE_AVAIL
 5d0163fecc44367b00bf830103145af7ecad0197c263cdced9011f9fb0077d79  ./applications/Collatz_Recursive_Sufficiency_Audit.md
 8947ff6657c15f104230a9d42841a2090b0d8a7c1ad8a42d6ab0f3270c0e7f14  ./applications/Electrostatic_Critical_Point_Transfer.md
 c6ced0ebd2d5a1eba08ebbc32a8f5f1fde89b0f235634ea2ecaf3784ae0bad31  ./applications/Operational_Channel_Crosswalk_2026.md
-b46c34cadebfd6a2ab3666c47e86d47d2fb327127a98ed6682d13a0a2c4d85c2  ./applications/Q26_Color_Split_Grid_Annihilator_Proof.md
-050f5d75fc5d3b183cea1032d29e54cf6dfac3635559c723f6e37e2ec84cf95e  ./applications/Q26_Queen_Domination_Attack.md
-573a7d0897d0e2ee5ebb52cfb6ac4757d7608f3d93d652d514f8d93259bbf4ea  ./applications/Q26_Symmetry_Parity_Profile_Reduction.md
-b0c3f951b6d1d9f5c51a532329611454984ad9c37b747266efc2c016e12a8913  ./applications/Q26_lean_4_32_2_source_sha256.txt
-ed40e491a6e170eb07bd63525dd9c0909577ef755d464437c426c00f4bd1566b  ./applications/Q26_lean_4_32_2_validation.json
+4af0ef8c4921d8c180263488f61871ddfe7734b9bc203c79a4840a7e369aef63  ./applications/Q26_Color_Split_Grid_Annihilator_Proof.md
+eea2330f2fd86fc93b4f95fb70d32efc786d556ee43713d0557cf1389187f073  ./applications/Q26_Queen_Domination_Attack.md
+54b455526aeafd73c39988dd0df3159d7349c066c56d1dcac5266e2a8d5122b5  ./applications/Q26_Symmetry_Parity_Profile_Reduction.md
+19d39323b325e86df7ce2c7396cf76acdaac5408d0b2d3b6ef58eba71d65c599  ./applications/Q26_lean_4_32_2_source_sha256.txt
+f0ea8bae107132bdf81d12eaac1306b14c05bea5f3158efb23a021930e183497  ./applications/Q26_lean_4_32_2_validation.json
 ff646f1a9cc856dc7805bddba18680bfca25f5c004aa6c3ee7c234f4796f4897  ./applications/Q26_queen_domination_known_14.json
 3fc303c3d1091deeb069b4232a54cdd6cdc1a2694caa10053c08f23dcbb46e4c  ./applications/Q26_symmetry_parity_profiles.json
 23664d28fea876abcfce1b1788477f697ae0e69f04ff1cbb3d401e416c069ac1  ./applications/Riemann_DQPT_Transfer.md
@@ -71,10 +71,10 @@ e0fcc72a93306108f601dd1db4c4599ef4fd4dfc316e2d2fa915abf8ce49c991  ./fixtures/F13
 be752fd2fba4ccfefccf895946fa37e1bd687a9ad4de6dc9d322285ff0c441e2  ./fixtures/F13_lorentz_auxiliary_passivity/verify_lorentz_passivity.py
 ddb1f9951b1cad8bdd5a0c68f1b51a913fa5cb24bd5634133f0d33c3418b12ed  ./fixtures/README.md
 5375c2c5e323f40c0031aa8c82f66bb9197214001039e6a8c9ff2a5eb3aa24a9  ./formal/q26_grid_annihilator/.gitignore
-dbf6ed8d1e0503ed920f9bea88716f72d8e0fea02e76f24700d664f03d9c776e  ./formal/q26_grid_annihilator/Q26GridAnnihilator.lean
+7ac4c9f2644e4c9757b687c557de26fe2c4ae18601fa8eae7570de7861128caa  ./formal/q26_grid_annihilator/Q26GridAnnihilator.lean
 f3c4f3fba94e4f6a20198a1bb734a9aa61ce2a3c1352b9bb63fdedd5fb84db5b  ./formal/q26_grid_annihilator/Q26GridAnnihilator/ArbitraryCardinality.lean
 8bf8e1edebdf91107c0a44e5f1912d2103b33ed92907652e7c6e46c1ae2e82a5  ./formal/q26_grid_annihilator/Q26GridAnnihilator/ArbitraryCardinalityAxiomAudit.lean
-77efd9ebf6c7e6d346f2dfbe79234178eff6240fc3f2fcccc4819e57cc848037  ./formal/q26_grid_annihilator/Q26GridAnnihilator/AxiomAudit.lean
+66ea5563308ccaf97f18700f7b224d544ad48dca8850a837addcc4735598230c  ./formal/q26_grid_annihilator/Q26GridAnnihilator/AxiomAudit.lean
 cce6164a0289c3e629d026b5f9ee1a8210c6fecab311e1690cbbf6af16aa9801  ./formal/q26_grid_annihilator/Q26GridAnnihilator/Basic.lean
 9e72879a9ca5c5208e2beec6f7847832331c87f3f68fb9d938fcaa8a29532d79  ./formal/q26_grid_annihilator/Q26GridAnnihilator/BichromaticClosure.lean
 b9ff8ed020df32ad0d3cd89afd0003e616d41f1ce8dd0520be0cf06bd270545b  ./formal/q26_grid_annihilator/Q26GridAnnihilator/BichromaticRecipe.lean
@@ -83,6 +83,7 @@ f25eec715cca89286c40901385ed0c8b246e1ab51479ae4f66c673193eed608f  ./formal/q26_g
 7f5cb08297560331d8541bdfbf2b6ec9525cc6f2a50b9572b0d4220893578ccc  ./formal/q26_grid_annihilator/Q26GridAnnihilator/ColorBridge.lean
 c4e625be03d515a203e7ca16435e569c847a31b735d77dc5ef31a50af5b908f9  ./formal/q26_grid_annihilator/Q26GridAnnihilator/Conditional.lean
 33d7bc227e3e2cd50793985ec44e3463f2dfeb14ea6dedae08761fdeb31cfc43  ./formal/q26_grid_annihilator/Q26GridAnnihilator/CoordinateSets.lean
+d4c685996dd287c23f514dea0e54574303825f19bd287780ef1c309731fa3bf1  ./formal/q26_grid_annihilator/Q26GridAnnihilator/Definitive.lean
 186ae40985027e713d7d8780389f5d2dcdf11af23b61fe268c3d3ca88203d6f7  ./formal/q26_grid_annihilator/Q26GridAnnihilator/GridMoment.lean
 13a8a44f5f61080c0b50ce8c66fc2f560871b72b3e0e02e01d2bd6191139eda3  ./formal/q26_grid_annihilator/Q26GridAnnihilator/MomentAlgebra.lean
 f6ee8110c6d43303153eb807c3ceb3d43a2196b13e512e3b9ed0d3482a11186c  ./formal/q26_grid_annihilator/Q26GridAnnihilator/MonochromaticArithmetic.lean
@@ -97,17 +98,18 @@ c764949aa3c58a95f8a5e2e35b311a9ff67df621890097e41b250c7e3883ca77  ./formal/q26_g
 48da0228750b4bc8095a2b0991994011a091c4ed1f5b9ee77c06abc9f4108d2f  ./formal/q26_grid_annihilator/Q26GridAnnihilator/Profiles.lean
 1f5e8e043560c91e9066522b10dd59a4525a6046f70ef0f911ce5569e4a93823  ./formal/q26_grid_annihilator/Q26GridAnnihilator/Shadow.lean
 e99424bc1d6324745ed99d79411326bdbe679b5db3f2146b7de3fc80b441c4fa  ./formal/q26_grid_annihilator/Q26GridAnnihilator/Unconditional.lean
-bc1a7f6152d33a0af13c0684160ec8aa942780c3afc3ba082b543714fadeaa50  ./formal/q26_grid_annihilator/README.md
+15652817526bc3d11ce9a303d8c3a14a51dbdb3039f09d6dbd8cbf8be78d0da5  ./formal/q26_grid_annihilator/README.md
 9ffcadb0b01034ce2511c62c55ea324d34184150458c8478cd79c739f727836a  ./formal/q26_grid_annihilator/lake-manifest.json
 26c9b9c924728993040e43bebc56740e8e6dd3d9d65471072a47e3df6ccd9fea  ./formal/q26_grid_annihilator/lakefile.toml
 2bdc48adfa58d0017e538a0ad117c5d73d35deec879978f909406a80c8037273  ./formal/q26_grid_annihilator/lean-toolchain
-b79f07d80ba46e31dd6541799d4d0115965478f90fb4d4bfff4d26a4ccdc25ae  ./formal/q26_grid_annihilator/validation/README.md
-58de64fc29e959623892ecd62221874b88ee03c8a0e3f4b891295d49a3f9f55e  ./formal/q26_grid_annihilator/validation/TrustedChallenge.lean
-6d936584b49bfee564ffea01f05feeed4152f9cb8e99af580e6cb583c2927eef  ./formal/q26_grid_annihilator/validation/comparator-config.json
-5c01c67463ad7d608718afef742263d9270c5c280bb172a6bb68c29163123201  ./formal/q26_grid_annihilator/validation/comparator_receipt.json
-711914828799ca70bdf2d867cc0bf4ebe72d9118659dec1943b08fb43120310e  ./formal/q26_grid_annihilator/validation/evidence/comparator-q26.txt
-4c30cd20aa29c88e090fbb65538b096de8e87ce6a5f36bf97b544f345838726a  ./formal/q26_grid_annihilator/validation/evidence/lean-source-projection-sha256.txt
-a20cdbd53f67cbf0748a257daf3af9a8a94f643292d91797833870318ca3ba6b  ./formal/q26_grid_annihilator/validation/reproduce-on-ubuntu.sh
+174043eca05bab4f38ce89a1de79d475d9d62076b3c2c0eb123d0dff1e11a9a7  ./formal/q26_grid_annihilator/validation/README.md
+8e57b02d00ce5d59244edf91cdff5396ff44a692efba535a49caaffd9401514c  ./formal/q26_grid_annihilator/validation/TrustedChallenge.lean
+03aacc69c02f1a6edb56216de96aa2485f1e4adfd3c348cf7c1db6e4624c13b5  ./formal/q26_grid_annihilator/validation/comparator-config.json
+6985061fdb70939aeff2aa6c67a673c55a756972e3df26d0c471f589f343ea47  ./formal/q26_grid_annihilator/validation/comparator_receipt.json
+dcbafc7b1460d6c80bd97a5ba9bcf01e61df485395d70a8cc3e6e42dceb0ea8b  ./formal/q26_grid_annihilator/validation/evidence/comparator-q26.txt
+3f64723316a43b35c70559c95c9b3efb4af101f4631875b77f04893bb37d8125  ./formal/q26_grid_annihilator/validation/evidence/external-run-q26.txt
+358f8fcdcea4ae5255f62cb399d57e9addafc8adc54e24f222ad3732a1c5b764  ./formal/q26_grid_annihilator/validation/evidence/lean-source-projection-sha256.txt
+6bccd21c40170e020179284f6c00f2387e4a3c93186011f52417483773f308b7  ./formal/q26_grid_annihilator/validation/reproduce-on-ubuntu.sh
 22af36273a34d2d9d41b0414272802847d252b433771cd334d2c8ac1c94b51ba  ./framework/Derived_Holonomy_Certificates.md
 080b172f5c0cb8e8e8ff355d749e5877f13711989a256e3e5537bfbef28c9588  ./framework/Electromagnetic_Evidence_Bridge.md
 6cea78a283f2c3d608e08287681167d579b7ce5772d0bb8d8671cfb7e56e9a25  ./framework/Lorentz_Auxiliary_State_Passivity.md
@@ -141,9 +143,9 @@ a9ef88a0239760b88b02f21b9655588022e4e888690fca4c2edf1352061079bf  ./tests/test_e
 3bcb040340495cca4058e589b46f79398503da2776eb552112630eca09b811e0  ./tests/test_f13_fixture.py
 cb749dd5c4be63c287c56515a9c690b557e57e95e3ec26db43d4646a06669f73  ./tests/test_inventory_contexts.py
 dca5895cc85edb5c06eb1ca19d00bbf12d47c4ee7ad0c5e13cf9a4d993f46e54  ./tests/test_manifest_validator.py
-274e46648ea865cb221c7792568001d039c9a56a040916b4385a74a40285cadd  ./tests/test_markdown_math.py
+41fa404dbc91f69dd3b1fe1d847725a925ba4b25f2f97b4560ee54c1d30b9070  ./tests/test_markdown_math.py
 59dc63326504cfe12fc1d48efa19d4a71c313e831e282358c5127c5a92968f83  ./tests/test_operational_channel_core.py
-93c7860500a4374ad356597bec66d126327796a6a402073be0895b38c0349321  ./tests/test_q26_grid_annihilator_checker.py
+b4b55eda7dee1f3687ea968fe0f97dd80114de69102532095f085da7d18554f9  ./tests/test_q26_grid_annihilator_checker.py
 6bf90984a3f85067e3c6468cdbc07e8c1a4b24015afbb57502cdf93a7ae700f4  ./tests/test_q26_queen_domination.py
 8543ad27aa25ff73cfe6ce5ffb3c635a891ea7b27abd797b9230cf12f2b53f06  ./tests/test_q26_symmetry_profiles.py
 02519503cc20a1ebefed32191c74593231ab88247ddd5e56e8bd7fc14aff1a13  ./tests/test_release_identity.py
@@ -154,7 +156,7 @@ dca5895cc85edb5c06eb1ca19d00bbf12d47c4ee7ad0c5e13cf9a4d993f46e54  ./tests/test_m
 d5a0b63e621639f149b1eb315d735a71e7fb51826a78dfde0fc6a11d4ff72fd5  ./tests/test_zdq_case.py
 530a72de36aef2154d265b29de50f84ec1dd01412db45eb4267c51971c4a26bb  ./tools/archive_validation.py
 8eb049ac1b011309d5cd773c8a991f14f40996a0a61801b41a4a77c138fe704b  ./tools/build_archives.py
-67d04e99b0d1307b66c378d368e5db821ce2bbcee7d3581217f3449fb0e32ac4  ./tools/check_markdown_math.py
+6b7a8c46b70501df84670e8ba60182fda1beeede0fcb1206b155ca85b94374dc  ./tools/check_markdown_math.py
 e20b4b17d04607800912fd0307ab784e3ee9dca2504662c315afa43096516f20  ./tools/q26_grid_annihilator_checker.py
 d0ebc0fa2621b6f8b547fc9b7d060c1dfba7f079254905c58d7c2fae968bdf55  ./tools/q26_queen_domination.py
 31447ea77d5151110858704165d69ed3707c876f5eba2cf17685932672c0777e  ./tools/q26_symmetry_profiles.py

README.md

@@ -45,7 +45,7 @@ The unit of evaluation is not the universe. It is one claimed transfer.
 | Framework module | [Exact rational derived-holonomy certificates](framework/Derived_Holonomy_Certificates.md) | Inspect the post-v1.4.0 exact-Q homotopy/left-null certificate and its evidence boundary |
 | Mathematical-physics application | [Electrostatic critical-point transfer](applications/Electrostatic_Critical_Point_Transfer.md) | Inspect quantitative critical-point transfer, positive-source compactness, the four-charge at-least-nine construction, and the bounded five-charge reconstruction |
 | Source-admission crosswalk | [ASTRA dual-rent audit](applications/ASTRA_Dual_Rent_Crosswalk.md) | Inspect corrected physical-change and diagnostic-gain semantics, exact countermodels, static reservoir degeneracy, source identities, and preserved verification failures |
-| Finite combinatorics theorem | [Q26 grid-annihilator proof](applications/Q26_Color_Split_Grid_Annihilator_Proof.md) | Inspect the exact-cardinality Lean obstruction, the cited lower bound and checked 14-queen witness yielding $\gamma(Q_{26})=14$, and the separate root-CNF status that remains UNKNOWN |
+| Finite combinatorics theorem | [Q26 grid-annihilator proof](applications/Q26_Color_Split_Grid_Annihilator_Proof.md) | Inspect the direct Lean theorem giving an explicit 14-queen dominator and proving that every dominator has at least 14 queens, and the separate root-CNF status that remains UNKNOWN |
 | Finite combinatorics campaign | [Q26 queen domination](applications/Q26_Queen_Domination_Attack.md) | Inspect three independent encodings, theorem-derived search reductions, the checked 14-queen witness, and the separate root-CNF certificate track that remains UNKNOWN |
 | Finite combinatorics reduction | [Q26 symmetry-parity shells](applications/Q26_Symmetry_Parity_Profile_Reduction.md) | Reproduce the exhaustive 156-shell structural over-cover and its 142-shell Weakley-Lemma-6 tightening without treating shells as placements or UNSAT cases |
 | Application crosswalk | [Four July 2026 experiments](applications/Operational_Channel_Crosswalk_2026.md) | Compare hybrid photons, a driven plasmonic time crystal, Hiroshima alloy evidence, and a microwave probabilistic-bit processor without conflating their physics |