From a052f0da36a3845c2ec785fd44e5b9e50de3b688 Mon Sep 17 00:00:00 2001 From: commdata2338 <199849969+commdata2338@users.noreply.github.com> Date: Tue, 13 Oct 2026 17:12:31 -0500 Subject: [PATCH] Research: certify A8 simplex P112 copy floor 71 The fixed A8 simplex nine-term all-pairs decoder has sharp copied-information cost 71 on the matching-frame P112 puncture and its 945 coordinate-permutation images, over arbitrary complex row shifts. This answers PR #1248's first open question for one frame orbit. Since 71 exceeds the standard P112 cost 64, the family cannot give the contemplated copy saving. No new kappa or physical supplier is claimed. Adds research/a8-p112-decoder-screen/ only. Submitted by @commdata2338 with substantial AI assistance (OpenAI Codex research and implementation; packaged with Claude Code). --- .../a8-p112-decoder-screen/CERTIFICATE.json | 1968 +++++++++++++++++ research/a8-p112-decoder-screen/PROOF.md | 185 ++ research/a8-p112-decoder-screen/README.md | 129 ++ research/a8-p112-decoder-screen/SOURCES.json | 68 + research/a8-p112-decoder-screen/TASK.json | 73 + research/a8-p112-decoder-screen/VALIDATION.md | 70 + research/a8-p112-decoder-screen/VERIFY.json | 42 + .../a8-p112-decoder-screen/independent.py | 220 ++ .../a8-p112-decoder-screen/test_package.py | 88 + research/a8-p112-decoder-screen/verify.py | 364 +++ 10 files changed, 3207 insertions(+) create mode 100644 research/a8-p112-decoder-screen/CERTIFICATE.json create mode 100644 research/a8-p112-decoder-screen/PROOF.md create mode 100644 research/a8-p112-decoder-screen/README.md create mode 100644 research/a8-p112-decoder-screen/SOURCES.json create mode 100644 research/a8-p112-decoder-screen/TASK.json create mode 100644 research/a8-p112-decoder-screen/VALIDATION.md create mode 100644 research/a8-p112-decoder-screen/VERIFY.json create mode 100644 research/a8-p112-decoder-screen/independent.py create mode 100644 research/a8-p112-decoder-screen/test_package.py create mode 100644 research/a8-p112-decoder-screen/verify.py diff --git a/research/a8-p112-decoder-screen/CERTIFICATE.json b/research/a8-p112-decoder-screen/CERTIFICATE.json new file mode 100644 index 0000000000..2e668cca66 --- /dev/null +++ b/research/a8-p112-decoder-screen/CERTIFICATE.json @@ -0,0 +1,1968 @@ +{ + "active_witness_costs": [ + 1, + 8, + 8, + 9, + 9, + 9, + 9, + 9, + 9 + ], + "all_pairs_checked_per_witness": 12544, + "anchors": [ + { + "anchor": 0, + "compatible_leaves": 52832, + "configurations": 2131, + "maximum_histogram": { + "10": 2131 + }, + "partner_dimension_histogram": [ + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1 + ], + "planes": 5808 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2 + ], + "planes": 1 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1 + ], + "planes": 13433 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 2 + ], + "planes": 14 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1 + ], + "planes": 13272 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 2 + ], + "planes": 42 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1 + ], + "planes": 7280 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 2 + ], + "planes": 70 + }, + { + "dimensions": [ + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 2520 + }, + { + "dimensions": [ + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 70 + }, + { + "dimensions": [ + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 693 + }, + { + "dimensions": [ + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 42 + }, + { + "dimensions": [ + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 140 + }, + { + "dimensions": [ + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 7 + }, + { + "dimensions": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 35 + }, + { + "dimensions": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 8 + } + ], + "planes": 43435, + "rejected_branches": 19822 + }, + { + "anchor": 1, + "compatible_leaves": 52832, + "configurations": 2131, + "maximum_histogram": { + "10": 2131 + }, + "partner_dimension_histogram": [ + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1 + ], + "planes": 5808 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2 + ], + "planes": 1 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1 + ], + "planes": 13433 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 2 + ], + "planes": 14 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1 + ], + "planes": 13272 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 2 + ], + "planes": 42 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1 + ], + "planes": 7280 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 2 + ], + "planes": 70 + }, + { + "dimensions": [ + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 2520 + }, + { + "dimensions": [ + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 70 + }, + { + "dimensions": [ + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 693 + }, + { + "dimensions": [ + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 42 + }, + { + "dimensions": [ + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 140 + }, + { + "dimensions": [ + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 7 + }, + { + "dimensions": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 35 + }, + { + "dimensions": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 8 + } + ], + "planes": 43435, + "rejected_branches": 19822 + }, + { + "anchor": 2, + "compatible_leaves": 52832, + "configurations": 2131, + "maximum_histogram": { + "10": 2131 + }, + "partner_dimension_histogram": [ + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1 + ], + "planes": 5808 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2 + ], + "planes": 1 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1 + ], + "planes": 13433 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 2 + ], + "planes": 14 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1 + ], + "planes": 13272 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 2 + ], + "planes": 42 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1 + ], + "planes": 7280 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 2 + ], + "planes": 70 + }, + { + "dimensions": [ + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 2520 + }, + { + "dimensions": [ + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 70 + }, + { + "dimensions": [ + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 693 + }, + { + "dimensions": [ + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 42 + }, + { + "dimensions": [ + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 140 + }, + { + "dimensions": [ + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 7 + }, + { + "dimensions": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 35 + }, + { + "dimensions": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 8 + } + ], + "planes": 43435, + "rejected_branches": 19697 + }, + { + "anchor": 3, + "compatible_leaves": 52832, + "configurations": 2131, + "maximum_histogram": { + "10": 2131 + }, + "partner_dimension_histogram": [ + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1 + ], + "planes": 5808 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2 + ], + "planes": 1 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1 + ], + "planes": 13433 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 2 + ], + "planes": 14 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1 + ], + "planes": 13272 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 2 + ], + "planes": 42 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1 + ], + "planes": 7280 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 2 + ], + "planes": 70 + }, + { + "dimensions": [ + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 2520 + }, + { + "dimensions": [ + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 70 + }, + { + "dimensions": [ + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 693 + }, + { + "dimensions": [ + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 42 + }, + { + "dimensions": [ + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 140 + }, + { + "dimensions": [ + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 7 + }, + { + "dimensions": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 35 + }, + { + "dimensions": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 8 + } + ], + "planes": 43435, + "rejected_branches": 19697 + }, + { + "anchor": 4, + "compatible_leaves": 52832, + "configurations": 2131, + "maximum_histogram": { + "10": 2131 + }, + "partner_dimension_histogram": [ + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1 + ], + "planes": 5808 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2 + ], + "planes": 1 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1 + ], + "planes": 13433 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 2 + ], + "planes": 14 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1 + ], + "planes": 13272 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 2 + ], + "planes": 42 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1 + ], + "planes": 7280 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 2 + ], + "planes": 70 + }, + { + "dimensions": [ + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 2520 + }, + { + "dimensions": [ + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 70 + }, + { + "dimensions": [ + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 693 + }, + { + "dimensions": [ + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 42 + }, + { + "dimensions": [ + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 140 + }, + { + "dimensions": [ + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 7 + }, + { + "dimensions": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 35 + }, + { + "dimensions": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 8 + } + ], + "planes": 43435, + "rejected_branches": 18790 + }, + { + "anchor": 5, + "compatible_leaves": 52832, + "configurations": 2131, + "maximum_histogram": { + "10": 2131 + }, + "partner_dimension_histogram": [ + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1 + ], + "planes": 5808 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2 + ], + "planes": 1 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1 + ], + "planes": 13433 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 2 + ], + "planes": 14 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1 + ], + "planes": 13272 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 2 + ], + "planes": 42 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1 + ], + "planes": 7280 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 2 + ], + "planes": 70 + }, + { + "dimensions": [ + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 2520 + }, + { + "dimensions": [ + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 70 + }, + { + "dimensions": [ + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 693 + }, + { + "dimensions": [ + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 42 + }, + { + "dimensions": [ + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 140 + }, + { + "dimensions": [ + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 7 + }, + { + "dimensions": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 35 + }, + { + "dimensions": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 8 + } + ], + "planes": 43435, + "rejected_branches": 18790 + }, + { + "anchor": 6, + "compatible_leaves": 52832, + "configurations": 2131, + "maximum_histogram": { + "10": 2131 + }, + "partner_dimension_histogram": [ + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1 + ], + "planes": 5808 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2 + ], + "planes": 1 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1 + ], + "planes": 13433 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 2 + ], + "planes": 14 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1 + ], + "planes": 13272 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 2 + ], + "planes": 42 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1 + ], + "planes": 7280 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 2 + ], + "planes": 70 + }, + { + "dimensions": [ + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 2520 + }, + { + "dimensions": [ + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 70 + }, + { + "dimensions": [ + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 693 + }, + { + "dimensions": [ + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 42 + }, + { + "dimensions": [ + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 140 + }, + { + "dimensions": [ + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 7 + }, + { + "dimensions": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 35 + }, + { + "dimensions": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 8 + } + ], + "planes": 43435, + "rejected_branches": 16155 + }, + { + "anchor": 7, + "compatible_leaves": 52832, + "configurations": 2131, + "maximum_histogram": { + "10": 2131 + }, + "partner_dimension_histogram": [ + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1 + ], + "planes": 5808 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2 + ], + "planes": 1 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1 + ], + "planes": 13433 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 2 + ], + "planes": 14 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1 + ], + "planes": 13272 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 2 + ], + "planes": 42 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1 + ], + "planes": 7280 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 2 + ], + "planes": 70 + }, + { + "dimensions": [ + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 2520 + }, + { + "dimensions": [ + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 70 + }, + { + "dimensions": [ + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 693 + }, + { + "dimensions": [ + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 42 + }, + { + "dimensions": [ + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 140 + }, + { + "dimensions": [ + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 7 + }, + { + "dimensions": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 35 + }, + { + "dimensions": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 2 + ], + "planes": 8 + } + ], + "planes": 43435, + "rejected_branches": 16155 + }, + { + "anchor": 8, + "compatible_leaves": 39485, + "configurations": 2251, + "maximum_histogram": { + "9": 2251 + }, + "partner_dimension_histogram": [ + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "planes": 4365 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1 + ], + "planes": 11552 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1 + ], + "planes": 13356 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1 + ], + "planes": 8792 + }, + { + "dimensions": [ + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1 + ], + "planes": 3710 + }, + { + "dimensions": [ + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 1176 + }, + { + "dimensions": [ + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 392 + }, + { + "dimensions": [ + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 56 + }, + { + "dimensions": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "planes": 36 + } + ], + "planes": 43435, + "rejected_branches": 13907 + } + ], + "column_label_ranks": [ + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9 + ], + "coordinate_permutation_punctures": 945, + "deficiency_upper_bound": 10, + "dropped_witness_costs": [ + 0, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9 + ], + "frame_indices": [ + 0, + 15, + 26, + 33, + 42, + 89, + 112, + 119 + ], + "frame_labels": [ + 508, + 499, + 463, + 319, + 259, + 268, + 304, + 448 + ], + "kind": "scoped proof with exhaustive finite lemmas", + "live_root_rank": 8, + "live_roots": 112, + "model": "fixed A8 simplex; one P112 frame puncture; all-pairs; separate term costs", + "schema_version": 1, + "semantic_controls": [ + "coefficient_perturbation", + "active_term_deleted", + "label_pairing_corrupted", + "nonorthogonal_puncture", + "unpunctured_dimension_lemma", + "omitted_mutual_compatibility_changes_bound", + "false_cost_seventy", + "nonreal_kernel_shift_positive" + ], + "sharp_copy_cost": 71, + "total_compatible_leaves": 462141, + "total_configurations": 19299, + "total_planes": 390915 +} diff --git a/research/a8-p112-decoder-screen/PROOF.md b/research/a8-p112-decoder-screen/PROOF.md new file mode 100644 index 0000000000..4f18ea6417 --- /dev/null +++ b/research/a8-p112-decoder-screen/PROOF.md @@ -0,0 +1,185 @@ +# Sharp copy cost 71 for the A8 simplex on a matching-frame P112 puncture + +This is a scoped mathematical proof whose finite lemmas are exhaustively +recomputed by two implementations. It is not a formal multiplication theorem. +The deficiency-space method is due to the P120 predecessor, mightyOil's +[PR1248](https://github.com/CrocSwap/integer-mult-bounds/pull/1248). The one-sided +overcomplete representation comes from joaqcoo's +[PR1224](https://github.com/CrocSwap/integer-mult-bounds/pull/1224). Here the +puncture changes the finite lemmas, and every lemma needed below is recomputed. + +## 1. Fixed family and puncture + +Work in the sum-zero subspace V of Q^9. Use the 120 oriented E8 root lines + +- e_a-e_b for 0 <= a < b <= 8, in lexicographic order (36 lines); +- 1_S-(1/3)1 for three-element subsets S of {0,...,8}, in lexicographic order + (84 lines). + +Puncture the orthogonal frame + + F = { e_(2j)-e_(2j+1), + e_(2j)+e_(2j+1)+e_8-(1/3)1 : j=0,1,2,3 }. + +Its zero-based indices are [0,15,26,33,42,89,112,119]. It is the first +orthogonal eight-frame in the declared root order; the verifier checks this +by complete lexicographic backtracking until the first solution. Let P be +the 112 live lines. They span V (rank eight, checked over Q). + +Fix the nine simplex normals b_k=e_k-(1/9)1, and T_ik=r_ik for live roots r_i. +The variable factor D has 112 rows and nine columns. Require + + D T^t = 2G, G_ij = r_i dot r_j, + +on **all** live pairs, with ordinary transpose. Coefficients can be arbitrary +complex numbers. Terms are charged separately by the F2 rank of the pairing +matrix (G_ij+1) mod 2 restricted to their nonzero row and column supports. +Zero terms are allowed, but the sharp witness below has all nine terms active. + +Since the live roots span V, the identity is equivalent to + + D_ik = 2r_ik + t_i, t_i arbitrary in C. + +Indeed D_i-2r_i is orthogonal to V and hence is a multiple of the all-ones +vector. This argument is valid over C with the bilinear ordinary transpose; +no positivity or conjugation is invoked. + +## 2. Exact reduction to binary deficiency spaces + +Use labels in F2^9: + + u_ab = 1+e_a+e_b, u_S = 1_S. + +For every pair of the 120 roots, u_i dot u_j=(G_ij+1) mod 2. This is checked +on all 14,400 entries. For each k, the live labels on the column support +{i:r_ik != 0} span all of F2^9. Thus the pairing rank of term k equals the +dimension of the label span on its row support {i:D_ik != 0}. + +Define + + K_k = {w : w dot u_i=0 whenever D_ik != 0}, delta_k=dim K_k. + +The total copy cost is exactly 81-sum_k delta_k. It is enough to prove that +the sum of the nine deficiencies is at most ten. + +If w in K_j and z in K_k both evaluate to one on u_i, then D_ij=D_ik=0. +Consequently r_ij=r_ik. Call this necessary relation compatibility of the two +functionals at columns j,k. It uses only zero patterns, so it applies to all +complex shifts, including generic shifts that create no zero entries. + +## 3. Finite covering of every possible deficiency tuple + +If every delta_k <= 1, the sum is at most nine already. Otherwise choose an +anchor j with delta_j >= 2 and a binary plane U contained in K_j. We check +every anchor and every plane; no symmetry assumption enters the primary check. + +Each binary plane has a unique representation by 0 64/112`, the family cannot improve the standard P112 copied-information +bill, even before extra physical costs. This is a copy-cost rejection of one +route, not a completed recurrence calculation or a bound for arbitrary decoders. + +## Exact scope and evidence + +The roots are `e_a-e_b` and `1_S-(1/3)1` in the sum-zero subspace of Q^9. The +fixed column normals are `b_k=e_k-(1/9)1`. On live roots, `T_ik=r_ik` and every +exact decoder is `D_ik=2r_ik+t_i`, with arbitrary `t_i` in C and ordinary +transpose. The puncture is + +```text +F = {e_(2j)-e_(2j+1), e_(2j)+e_(2j+1)+e_8-(1/3)1 : j=0,1,2,3} +``` + +It has indices `[0,15,26,33,42,89,112,119]` in the pair-then-triple lexicographic +root order. Terms are billed separately by binary pairing rank. Masked +identities and shared-copy pricing are excluded. + +All nine column-label spans still have rank nine, so the copy cost is +`81 - sum(delta_k)`. However, puncturing creates two-dimensional partner +deficiency spaces: the P120 dimension-one lemma is false here. Enumerating all +subspaces of these enlarged spaces and imposing their mutual compatibility +proves `sum(delta_k) <= 10`. + +- Primary replay: all nine anchors, 390,915 binary planes, 19,299 distinct + ordered partner-space tuples, and 462,141 compatible subspace choices. +- Separate replay: labels reconstructed from the Gram pairing matrix, + annihilator row reduction, direct Cartesian-product enumeration, and a + checked stabilizer transporting two anchor representatives to all nine. +- Both check all 12,544 entries of the active witness. The primary also checks + the zero-term witness; the separate checker prices actual pairing submatrices. +- Eight semantic controls include a coefficient error, a deleted term, corrupt + labels, a nonorthogonal puncture, the false inherited dimension-one lemma, + missing mutual compatibility, a false cost of 70, and a valid non-real shift. +- Six package tests exercise optimized relocated/read-only replay, the separate + checker without the primary file, and changed, incomplete, missing or + malformed receipts. + +The argument covering every complex shift is in [PROOF.md](PROOF.md). The +deterministic finite evidence is [CERTIFICATE.json](CERTIFICATE.json). The +second implementation is by the same AI assistant, not independent human review. + +## Reproduce + +From the repository root, Python 3.12 and the standard library: + +```sh +python3 -I -B research/a8-p112-decoder-screen/verify.py +python3 -I -B research/a8-p112-decoder-screen/independent.py +python3 scripts/research_package.py --package research/a8-p112-decoder-screen --check-only +python3 scripts/research_package.py --package research/a8-p112-decoder-screen +``` + +The last command runs both checkers and the six package tests. Expected markers: + +```text +PASS_A8_P112_DECODER_FLOOR planes=390915 configurations=19299 compatible_leaves=462141 cost=71 controls=8 +PASS_A8_P112_INDEPENDENT anchors=2 transported=9 planes=86870 compatible_leaves=92317 cost=71 +PASS_REGISTERED_RESEARCH_PACKAGE research/a8-p112-decoder-screen outcome=negative-result +``` + +`verify.py --write` explicitly regenerates the certificate. Normal replay is +read-only. Source pins and exact predecessor heads are in [SOURCES.json](SOURCES.json); +the pending predecessors are attribution/context, not imported code or assumed +finite lemmas. [TASK.json](TASK.json) records the chooser, scope and next questions. +See [VALIDATION.md](VALIDATION.md) for measured checks and limits. + +No supplier word, delivery/frame/restoration/hosting invoice, new moment, +selected cold replay, Lean proof, or complete multiplication theorem is supplied. +The selected frontier and all inherited all-size/compiler, common-label and +mutable-source, hosting, precision/tape, recovery, analytic-transfer and bit +H1-H5 obligations remain unchanged. Hosted CI and human review are unclaimed. + +## Coordination + +Base `dadfea6e8a78ff6ba901705f87532a71c6f5bbb8`; chooser nonce +`a57142e8e77d6c0af036ca35809daf69`, track `complex-mechanisms`, revision 2, +card `complex-masked-decoder`, scope key `2a6f2c726b78f9ae7d26`. This refines +the card's overcomplete-family branch to PR1248's explicit puncture question. + +Nearest predecessors are PR1248 (P120 optimum) and PR1224 (normal form and +bounded searches). PR1212/1213 and discussion #1275 concern eight-term masked +rigidity; PR1236 and discussion #1267 concern masked root-star/co-star supports. +These are distinct hypotheses. Two parallel sessions from the same account +study bit-side zero-frame feedback (discussion #1290) and selected bit hosting +(discussion #1289); this package does neither. The original claim is in +[discussion #1241](https://github.com/CrocSwap/integer-mult-bounds/discussions/1241#discussioncomment-18909913). +The final overlap check used a shared snapshot of 788 open PRs and 40 +discussion records with complete pagination, fetched at 21:54:03 and 21:54:12 +UTC on 2026-10-13. It may miss later changes. + +## Open next questions + +- **Other frame punctures relative to the fixed simplex.** Do they also have + minimum cost at least 64? Enumerate orthogonal frames and their S9 orbits, + then recompute column ranks and partner dimensions for a representative + outside the matching-frame orbit. This tests whether the remaining P112 + part of PR1248's question can improve copy cost. The present enumerator + deliberately rejects partner dimensions above two and may need extension. +- **Another specified nine-normal frame.** Can the A7+A1 or A2+E6 family in + PR1224 admit copy cost below 64 on a named P112 puncture? First establish its + exact ratio classes, column spans and a favorable complete cost budget. + The simplex's common kernel vector and compatibility census do not transfer + automatically; physical realization would remain an additional obligation. + +## Credit and disclosure + +Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance. + +Credit Philipp / **mightyOil**, PR1248, for the deficiency-space method, P120 +floor and explicit P112 follow-up; **joaqcoo**, PR1224, for the nine-term normal +form, A8 frame and ratio-class viewpoint; **DreamingOfClouds**, PR717/595/446, +for the decoder and pairing-rank cost model; **themilkman216**, PR968, and +**woklerx**, PR1077/1180, for surrounding floor results; and the classical +E8/A8 geometry. The selected supplier lineage retains its existing credit. +No predecessor file is changed. New work is Apache-2.0, the repository license. diff --git a/research/a8-p112-decoder-screen/SOURCES.json b/research/a8-p112-decoder-screen/SOURCES.json new file mode 100644 index 0000000000..5de83e4d2c --- /dev/null +++ b/research/a8-p112-decoder-screen/SOURCES.json @@ -0,0 +1,68 @@ +{ + "schema_version": 1, + "base_commit": "dadfea6e8a78ff6ba901705f87532a71c6f5bbb8", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce" + }, + { + "path": "research/complex-decoder-field-extension-seed44/README.md", + "usage": "input", + "git_blob": "a6e6d2e04249191c1bce5c6e2977c11f9969b7a3", + "sha256": "788a99eef3f187c2cbff6d490933fcc8f8e7fd15d1b685c188023605916887d4" + }, + { + "path": "research/complex-frame-pair-decoders/README.md", + "usage": "input", + "git_blob": "be5bbbee8e30a4ee39fa513896e8fc7e0bb3721e", + "sha256": "edd848b0177dc73a6e2646d4fd82f0b2ceae37e642bf19d6af602579a041a57e" + } + ], + "predecessor_references": [ + { + "pr": 1248, + "head": "f226f4329a996b0a1bea8794179a91b5d0ed80bf", + "author": "Philipp / mightyOil", + "role": "Method and question attribution; no imported code or unverified finite-lemma dependency. Not required for runtime replay.", + "files": [ + { + "path": "research/a8-simplex-decoder-floor/README.md", + "git_blob": "cc814ae890f18da884b70ae6e471f31a75bade5f", + "sha256": "4f279ea113cea46593609cdcd580099c24ec8aa02428aae0c5bae54baa0e4557" + }, + { + "path": "research/a8-simplex-decoder-floor/PROOF.md", + "git_blob": "4d1d3bcd8799c833dfbb63ed5319af5fe863fa1a", + "sha256": "7e3a5407fc535fd9cc7f25f06aab787b0216f09121e571938cccedb383aab3c4" + } + ] + }, + { + "pr": 1224, + "head": "00e6ed0810b8ebc7f6133e2c036d0f1c9a3a4162", + "author": "joaqcoo", + "role": "Method and question attribution; no imported code or unverified finite-lemma dependency. Not required for runtime replay.", + "files": [ + { + "path": "research/nine-term-decoder-normal-form-seed42/README.md", + "git_blob": "9cf8ecd3eda302b57ab14302c429b00c255f2dba", + "sha256": "d272081da47d6ea6a2404fddff211418dd6e7c236babf7eb4560737e818c1677" + }, + { + "path": "research/nine-term-decoder-normal-form-seed42/PROOF.md", + "git_blob": "e510fd180a286445fd6fc484057001bfc60f8c9c", + "sha256": "0503e07f1764708e9e72c01be88d3dad1b213e73eb3c23397a603032791fd23a" + } + ] + } + ] +} diff --git a/research/a8-p112-decoder-screen/TASK.json b/research/a8-p112-decoder-screen/TASK.json new file mode 100644 index 0000000000..46e568faa0 --- /dev/null +++ b/research/a8-p112-decoder-screen/TASK.json @@ -0,0 +1,73 @@ +{ + "schema_version": 1, + "task_id": "complex-masked-decoder", + "priority_revision": 2, + "base_commit": "dadfea6e8a78ff6ba901705f87532a71c6f5bbb8", + "original_card": { + "id": "complex-masked-decoder", + "question": "Can one specified masked or overcomplete decoder improve the complete moment budget?", + "starting_points": [ + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md" + ], + "methods": [ + "Synthesize a decoder with exact coefficients and fully priced helper endpoints.", + "Bound the best possible budget for a fixed support alphabet before synthesis." + ], + "acceptance_gate": "Change an assumption of the eight-term all-pairs bound and count all copied information, frames and restoration.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-decoder-field-extension-seed44/verify.py" + ], + "expected": "PASS_COMPLEX_DECODER_FIELD_EXTENSION_S44", + "inspect": "Locate the excluded classes: masked identities, at least nine terms, and deeper punctures.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Choose one finite support alphabet and test exact decoding constraints before building a whole network.", + "bottleneck_link": "A cheaper fully realized decoder could increase deficit or lower recursive cost on the binding complex side.", + "allowed_variations": [ + "Select a specific masked or overcomplete family with exact labels and supports." + ], + "scope_change_triggers": [ + "Repeating the exact eight-term all-pairs search inside its proved scope." + ], + "overlap_terms": [ + "masked decoder", + "overcomplete", + "eight-term" + ] + }, + "scope_status": "refined", + "actual_scope": "Sharp separate-term copy-cost floor for the fixed A8 simplex nine-term all-pairs decoder on the matching-frame P112 puncture and its 945 coordinate-permutation images, over arbitrary complex row shifts.", + "scope_change_reason": "Take the card's overcomplete-family branch and PR1248's explicit P112 follow-up. Change the puncture from P120, recompute every finite lemma, and use only proved coordinate symmetry for the corollary.", + "bottleneck_link": "The complex supplier binds. A copy cost at most 63 would be a necessary first saving against standard P112 cost 64 under this billing model. The sharp floor 71 rejects this family before physical synthesis; no complete moment or supplier claim follows.", + "budget_minutes": 60, + "stop_rule": "Stop construction if an exact floor excludes cost at most 63; otherwise certify a candidate before any physical budget claim. About 60 minutes total, with final quarter for verification and handoff. No expanded optimizer search.", + "outcome": "negative-result", + "evidence": "PROOF.md and CERTIFICATE.json: all 390915 planes across nine anchors; 19299 partner-space tuples; 462141 compatible subspace choices; sum deficiency at most 10; sharp all-nine-active witness cost 71. Separate Gram-derived implementation and eight semantic controls; six package tests.", + "author": "commdata2338", + "ai_assistance": "Substantial OpenAI Codex assistance in research, both implementations, proof, testing and writing. Same-assistant separate implementation is not independent human review.", + "open_questions": [ + { + "question": "What is the fixed-simplex optimum for a P112 frame puncture outside the 945 matching-frame orbit?", + "why_it_matters": "The remaining frame orientations could have different copy costs and are not bounded here.", + "first_step": "Enumerate E8 orthogonal frames modulo explicit S9 coordinate permutations; recompute column ranks and partner dimensions for one unrepresented orbit.", + "blocked_by": "This proof covers one orbit only; larger partner spaces require a complete subspace enumerator beyond dimensions zero through two." + }, + { + "question": "Can another specified nine-normal family from PR1224 beat copy cost 64 on a named P112 puncture?", + "why_it_matters": "A different normal frame changes the zero-pattern constraints and may evade this scoped obstruction.", + "first_step": "Choose A7+A1 or A2+E6, derive its kernel and ratio classes, and screen exact label ranks plus a favorable complete cost budget.", + "blocked_by": "The common all-ones kernel and this compatibility census are specific to the A8 simplex; physical costs would remain additional obligations." + } + ], + "chooser": { + "nonce": "a57142e8e77d6c0af036ca35809daf69", + "track": "complex-mechanisms", + "scope_key": "2a6f2c726b78f9ae7d26", + "priority_revision": 2 + }, + "coordination": "Claim posted in discussion #1241 (comment 18909913) by the submitting account; the agent session itself made no GitHub writes." +} diff --git a/research/a8-p112-decoder-screen/VALIDATION.md b/research/a8-p112-decoder-screen/VALIDATION.md new file mode 100644 index 0000000000..28e50b51f0 --- /dev/null +++ b/research/a8-p112-decoder-screen/VALIDATION.md @@ -0,0 +1,70 @@ +# Local validation + +Executed on 2026-10-13 with CPython 3.12.3, Linux x86_64, standard library only. +The package uses one busy process at a time and no GPU. No packages were +installed. All source and evidence generation ran in one donated agent session. + +## Completed checks + +```sh +python3 -B research/complex-decoder-field-extension-seed44/verify.py +python3 -B scripts/research_baseline.py +python3 -I -B research/a8-p112-decoder-screen/verify.py --write +python3 -I -B research/a8-p112-decoder-screen/independent.py +python3 -I -B research/a8-p112-decoder-screen/test_package.py -k missing_receipt +python3 -B scripts/research_package.py --package research/a8-p112-decoder-screen --check-only +python3 -B scripts/research_package.py --package research/a8-p112-decoder-screen +python3 -B -m unittest discover -s tests -p 'test_research_*.py' +python3 -B scripts/verify_selected_result.py +``` + +Every command passed. The registered replay reran the primary checker, separate +checker and full six-test package file in **58.024 seconds**; its six tests took +39.221 seconds. The 20 repository research-workflow tests passed with no skips +(0.386 seconds reported by unittest). These are host-specific verifier timings, +not multiplication-runtime measurements. No broad historical replay was run. + +The primary check covers 390,915 planes across all nine anchors, 19,299 partner +space tuples and 462,141 compatible subspace choices. It re-derives the sharp +cost 71, both witnesses, the 945-frame orbit, and eight semantic controls. The +separate checker uses different label coordinates, annihilator algebra and +Cartesian products, checks 86,870 planes for two symmetry representatives, +and proves its transport to all nine anchors using explicit permutations. + +The eight semantic controls comprise six deliberate rejection cases, a check +that dropping mutual compatibility admits the false deficiency allowance 11, +and a positive non-real kernel-shift fixture. The six package tests check: + +- isolated optimized replay in a relocated read-only directory with unchanged + file hashes; +- the separate checker with the primary checker file absent; +- rejection of an altered cost claim, a missing anchor, a missing receipt, and + malformed JSON. + +The initial predecessor command is a source-bound positive control, not the +selected supplier's cold replay. The baseline and selected-record integrity +checks confirmed the recorded selected kappa and pins; no selected file was +edited. The new scripts use explicit exceptions, so their checks remain active +under `python -O`. + +## What was not checked + +No other P112 frame orbit, arbitrary nine-normal family, masked identity, +shared-copy implementation or physical supplier is certified. No delivery, +restoration, frame, hosting, precision/tape or complete moment invoice was +constructed. `make frontier1094-verify`, native/Lean builds, hosted CI, an +all-size compiler and the complete multiplication theorem were not run or +proved. The written covering argument has no independent human review. + +PR1248 and PR1224 were fetched anonymously and read at the exact heads in +SOURCES.json. Their code and certificates are not runtime dependencies; the +new package recomputes its own needed finite facts. The predecessor head/hash +references are attribution evidence and are not checked by the generic runner, +which checks the main-tree source inventory in `SOURCES.json.files`. + +The final overlap query used a shared offline snapshot: 788 open PRs +fetched 2026-10-13T21:54:03.402700+00:00 and 40 discussion records fetched +2026-10-13T21:54:12.002645+00:00, both marked complete pagination. It does not +cover later updates or every diff. The claim is in discussion #1241. + +Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance. diff --git a/research/a8-p112-decoder-screen/VERIFY.json b/research/a8-p112-decoder-screen/VERIFY.json new file mode 100644 index 0000000000..808084f7f4 --- /dev/null +++ b/research/a8-p112-decoder-screen/VERIFY.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All nine anchors, exhaustive deficiency bound, 945-frame symmetry orbit, both witnesses and eight semantic controls." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 120, + "checks": "Separate Gram-derived labels, annihilator algebra, Cartesian products, checked anchor stabilizer and direct pairing-rank witness." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 180, + "checks": "Six optimized relocation, read-only, separate-code and receipt-corruption package controls." + } + ] +} diff --git a/research/a8-p112-decoder-screen/independent.py b/research/a8-p112-decoder-screen/independent.py new file mode 100644 index 0000000000..02035af27f --- /dev/null +++ b/research/a8-p112-decoder-screen/independent.py @@ -0,0 +1,220 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Separate check: Gram-derived labels, annihilator algebra, Cartesian products. + +No primary or predecessor imports. The primary checks nine anchors; here an +explicit frame stabilizer reduces the coverage to two orbits, {0,...,7}, {8}. +Separate implementation by the same AI assistant is not independent peer review. +""" + +from collections import Counter +from fractions import Fraction +from functools import lru_cache +from itertools import combinations, product +import json +from pathlib import Path + + +def check(value, message): + if not value: + raise RuntimeError(message) + + +def rref(vectors, width=9): + rows = sorted(set(vectors) - {0}) + n = 0 + for column in range(width): + pivot = next((i for i in range(n, len(rows)) if (rows[i] >> column) & 1), None) + if pivot is None: + continue + rows[n], rows[pivot] = rows[pivot], rows[n] + for i in range(len(rows)): + if i != n and ((rows[i] >> column) & 1): + rows[i] ^= rows[n] + n += 1 + return tuple(rows[:n]) + + +@lru_cache(maxsize=100000) +def combine(a, b): + return rref(a + b) + + +@lru_cache(maxsize=100000) +def annihilator(equations): + pivots = [(x & -x).bit_length() - 1 for x in equations] + answer = [] + for f in range(9): + if f not in pivots: + answer.append((1 << f) | sum(((x >> f) & 1) << p + for x, p in zip(equations, pivots))) + check(all((v & e).bit_count() % 2 == 0 for v in answer for e in equations), + 'annihilator equations') + return tuple(answer) + + +def nonzero_span(basis): + space = {0} + for vector in basis: + space |= {x ^ vector for x in tuple(space)} + return tuple(sorted(space - {0})) + + +def geometry(): + roots = [] + for a in range(9): + for b in range(a + 1, 9): + row = [Fraction(0)] * 9 + row[a], row[b] = Fraction(1), Fraction(-1) + roots.append(tuple(row)) + for subset in combinations(range(9), 3): + roots.append(tuple(Fraction(int(k in subset)) - Fraction(1, 3) for k in range(9))) + gram = [[sum(x * y for x, y in zip(a, b)) for b in roots] for a in roots] + check(all(x.denominator == 1 for row in gram for x in row), 'integral Gram') + pairing = [[(int(x) + 1) % 2 for x in row] for row in gram] + columns, selected = [], [] + for j in range(120): + column = sum(pairing[i][j] << i for i in range(120)) + if len(rref(columns + [column], 120)) > len(columns): + columns.append(column) + selected.append(j) + check(len(columns) == 9, 'full pairing rank nine') + labels = [sum(pairing[i][j] << p for p, j in enumerate(selected)) for i in range(120)] + frame = (0, 15, 26, 33, 42, 89, 112, 119) + check(all(gram[i][j] == 0 for i, j in combinations(frame, 2)), 'frame orthogonality') + # Explicit generators preserve the puncture and are transitive on 0..7. + swaps = [[(0, 1)], [(0, 2), (1, 3)], [(0, 4), (1, 5)], [(0, 6), (1, 7)]] + lookup = {r: i for i, r in enumerate(roots)} + permutations = [] + for exchanges in swaps: + permutation = list(range(9)) + for a, b in exchanges: + permutation[a], permutation[b] = permutation[b], permutation[a] + images = [] + for root in roots: + image = tuple(root[permutation[k]] for k in range(9)) + if image not in lookup: + image = tuple(-x for x in image) + check(image in lookup, 'root-line permutation') + images.append(lookup[image]) + check({images[i] for i in frame} == set(frame), 'puncture stabilizer') + permutations.append(permutation) + orbit = {0} + while True: + new = orbit | {p[i] for p in permutations for i in orbit} + if new == orbit: + break + orbit = new + check(orbit == set(range(8)) and all(p[8] == 8 for p in permutations), 'anchor orbits') + indices = [i for i in range(120) if i not in frame] + live_roots = [roots[i] for i in indices] + live_labels = [labels[i] for i in indices] + for k in range(9): + check(len(rref(u for u, r in zip(live_labels, live_roots) if r[k])) == 9, + 'column rank in Gram-derived label coordinates') + # Direct ranks of the actual pairing submatrices, not the label shortcut. + d = [[2 * (x - r[2 if i == 0 else 0]) for x in r] for i, r in enumerate(live_roots)] + for i, row in enumerate(d): + for j, root in enumerate(live_roots): + check(sum(x * y for x, y in zip(row, root)) == 2 * gram[indices[i]][indices[j]], + 'rational all-pairs identity') + costs = [] + for k in range(9): + ys = [indices[j] for j, r in enumerate(live_roots) if r[k]] + matrix = [sum(pairing[indices[i]][j] << p for p, j in enumerate(ys)) + for i, row in enumerate(d) if row[k]] + costs.append(len(rref(matrix, len(ys)))) + check(costs == [1, 8, 8, 9, 9, 9, 9, 9, 9], 'direct pairing-rank witness price') + return live_roots, live_labels, selected, permutations + + +def audit_anchor(roots, labels, anchor): + others = [k for k in range(9) if k != anchor] + equations = {} + for k in others: + relevant = [(u, r) for u, r in zip(labels, roots) if r[k] != r[anchor]] + equations[k] = [rref(u for u, _ in relevant if (u & w).bit_count() % 2) + for w in range(512)] + configs = {} + dimension_hist = Counter() + # Enumerate planes using RREF bases, not the primary's sorted nonzero pairs. + plane_bases = set() + for a in range(1, 512): + for b in range(a + 1, 512): + plane_bases.add(rref((a, b))) + check(len(plane_bases) == 43435, 'all planes by canonical RREF') + for a, b in sorted(plane_bases): + spaces = tuple(nonzero_span(annihilator(combine(equations[k][a], equations[k][b]))) + for k in others) + dims = tuple(sorted((len(h) + 1).bit_length() - 1 for h in spaces)) + check(max(dims) <= 2, 'partner space dimensions') + dimension_hist[dims] += 1 + configs[spaces] = configs.get(spaces, 0) + 1 + options_cache = {} + for spaces in configs: + for k, h in zip(others, spaces): + key = (k, h) + if key in options_cache: + continue + subspaces = [()] + [(z,) for z in h] + if len(h) == 3: + subspaces.append(rref(h)) + result = [] + for basis in subspaces: + constraints = rref(x for z in basis for x in equations[k][z]) + zero_rows = frozenset(i for i, u in enumerate(labels) + if any((u & z).bit_count() % 2 for z in basis)) + result.append((len(basis), constraints, zero_rows)) + options_cache[key] = result + compatible_count = raw_count = 0 + maximum_hist = Counter() + for spaces in configs: + maximum = 0 + for choices in product(*(options_cache[k, h] for k, h in zip(others, spaces))): + raw_count += 1 + # Test rowwise consistency directly: all forced-zero coordinates at + # a row must have the same coefficient. No bitset compatibility table. + consistent = True + forced_value = {} + for k, (_, _, zero_rows) in zip(others, choices): + for row in zero_rows: + value = roots[row][k] + if row in forced_value and forced_value[row] != value: + consistent = False + break + forced_value[row] = value + if not consistent: + break + if not consistent: + continue + compatible_count += 1 + constraints = rref(x for _, equations_, _ in choices for x in equations_) + score = 9 - len(constraints) + sum(dim for dim, _, _ in choices) + check(score <= 10, 'deficiency upper bound') + maximum = max(maximum, score) + maximum_hist[maximum] += 1 + return {'anchor': anchor, 'planes': len(plane_bases), 'configurations': len(configs), + 'compatible_leaves': compatible_count, 'raw_products': raw_count, + 'maximum_histogram': {str(k): v for k, v in sorted(maximum_hist.items())}, + 'partner_dimension_histogram': [{'dimensions': list(k), 'planes': v} + for k, v in sorted(dimension_hist.items())]} + + +def main(): + roots, labels, selected, permutations = geometry() + receipt = json.loads((Path(__file__).resolve().parent / 'CERTIFICATE.json').read_text()) + results = [audit_anchor(roots, labels, a) for a in (0, 8)] + for result in results: + anchors = range(8) if result['anchor'] == 0 else (8,) + for a in anchors: + for key in ('planes', 'configurations', 'compatible_leaves', 'maximum_histogram', + 'partner_dimension_histogram'): + check(result[key] == receipt['anchors'][a][key], 'primary receipt mismatch: ' + key) + check(receipt['sharp_copy_cost'] == 71 and receipt['active_witness_costs'] == + [1, 8, 8, 9, 9, 9, 9, 9, 9], 'price receipt') + print('PASS_A8_P112_INDEPENDENT anchors=2 transported=9 planes=86870 ' + 'compatible_leaves=92317 cost=71') + + +if __name__ == '__main__': + main() diff --git a/research/a8-p112-decoder-screen/test_package.py b/research/a8-p112-decoder-screen/test_package.py new file mode 100644 index 0000000000..aef2d0d550 --- /dev/null +++ b/research/a8-p112-decoder-screen/test_package.py @@ -0,0 +1,88 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Relocation, optimized execution, and receipt rejection controls.""" + +import hashlib +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent + + +class PackageControls(unittest.TestCase): + def setUp(self): + self.temporary = tempfile.TemporaryDirectory(prefix='a8-p112-') + self.root = Path(self.temporary.name) + self.package = self.root / 'package' + self.package.mkdir() + for name in ('verify.py', 'independent.py', 'CERTIFICATE.json'): + shutil.copyfile(HERE / name, self.package / name) + + def tearDown(self): + self.temporary.cleanup() + + def run_script(self, script='verify.py'): + return subprocess.run([sys.executable, '-I', '-O', '-B', str(self.package / script)], + cwd=self.root, capture_output=True, text=True, timeout=120) + + def change_receipt(self, change): + path = self.package / 'CERTIFICATE.json' + value = json.loads(path.read_text()) + change(value) + path.write_text(json.dumps(value) + '\n') + + def test_primary_optimized_relocated_read_only(self): + paths = list(self.package.iterdir()) + before = {p.name: hashlib.sha256(p.read_bytes()).hexdigest() for p in paths} + for path in paths: + path.chmod(0o444) + self.package.chmod(0o555) + try: + result = self.run_script() + finally: + self.package.chmod(0o755) + for path in paths: + path.chmod(0o644) + self.assertEqual(result.returncode, 0, result.stderr[-1000:]) + self.assertIn('PASS_A8_P112_DECODER_FLOOR', result.stdout) + self.assertEqual(before, {p.name: hashlib.sha256(p.read_bytes()).hexdigest() + for p in self.package.iterdir()}) + + def test_separate_checker_without_primary(self): + (self.package / 'verify.py').unlink() + result = self.run_script('independent.py') + self.assertEqual(result.returncode, 0, result.stderr[-1000:]) + self.assertIn('PASS_A8_P112_INDEPENDENT', result.stdout) + + def test_changed_claim_rejected(self): + self.change_receipt(lambda value: value.update(sharp_copy_cost=70)) + result = self.run_script() + self.assertNotEqual(result.returncode, 0) + self.assertIn('certificate differs from exact replay', result.stderr) + + def test_missing_anchor_rejected(self): + self.change_receipt(lambda value: value['anchors'].pop(4)) + result = self.run_script() + self.assertNotEqual(result.returncode, 0) + self.assertIn('certificate differs from exact replay', result.stderr) + + def test_missing_receipt_rejected(self): + (self.package / 'CERTIFICATE.json').unlink() + result = self.run_script() + self.assertNotEqual(result.returncode, 0) + self.assertIn('FileNotFoundError', result.stderr) + + def test_truncated_receipt_rejected(self): + (self.package / 'CERTIFICATE.json').write_text('{"anchors": [') + result = self.run_script() + self.assertNotEqual(result.returncode, 0) + self.assertIn('JSONDecodeError', result.stderr) + + +if __name__ == '__main__': + unittest.main() diff --git a/research/a8-p112-decoder-screen/verify.py b/research/a8-p112-decoder-screen/verify.py new file mode 100644 index 0000000000..188d3a8fda --- /dev/null +++ b/research/a8-p112-decoder-screen/verify.py @@ -0,0 +1,364 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Exact finite lemmas for one A8 simplex P112 decoder floor. + +The deficiency method follows mightyOil's PR1248. This implementation extends +it to the declared puncture, enumerating every subspace of every partner space. +No predecessor code, numerical solver, or unproved symmetry reduction is used. +""" + +import argparse +from collections import Counter +from fractions import Fraction +from itertools import combinations +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +FRAME = (0, 15, 26, 33, 42, 89, 112, 119) +FULL = (1 << 9) - 1 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def binary_basis(vectors): + pivots = {} + for value in vectors: + while value: + p = value.bit_length() - 1 + if p in pivots: + value ^= pivots[p] + else: + pivots[p] = value + break + return tuple(pivots[p] for p in sorted(pivots, reverse=True)) + + +def rank(vectors): + return len(binary_basis(vectors)) + + +def rational_rank(rows): + pivots = {} + for row in rows: + v = list(map(Fraction, row)) + for p in range(len(v)): + if not v[p]: + continue + if p in pivots: + multiple = v[p] + v = [x - multiple * y for x, y in zip(v, pivots[p])] + else: + multiple = v[p] + pivots[p] = [x / multiple for x in v] + break + return len(pivots) + + +def members(mask): + while mask: + bit = mask & -mask + yield bit.bit_length() - 1 + mask ^= bit + + +def dot(a, b): + return sum(x * y for x, y in zip(a, b)) + + +def model(): + """Rows are (binary label, v=3r), in the declared canonical order.""" + rows = [] + for a, b in combinations(range(9), 2): + rows.append((FULL ^ (1 << a) ^ (1 << b), + tuple(3 * (int(k == a) - int(k == b)) for k in range(9)))) + for triple in combinations(range(9), 3): + label = sum(1 << k for k in triple) + rows.append((label, tuple(2 if k in triple else -1 for k in range(9)))) + return rows + + +def first_frame(rows): + adjacency = [{j for j in range(i + 1, len(rows)) + if dot(rows[i][1], rows[j][1]) == 0} for i in range(len(rows))] + + def visit(prefix, candidates): + if len(prefix) == 8: + return prefix + for i in sorted(candidates): + rest = candidates & adjacency[i] + if len(prefix) + 1 + len(rest) >= 8: + found = visit(prefix + (i,), rest) + if found is not None: + return found + return None + + return visit((), set(range(len(rows)))) + + +def matching_frame_orbit(rows): + """Coordinate-permutation images: choose one singleton and four pairs.""" + lookup = {v: i for i, (_, v) in enumerate(rows)} + + def matchings(items): + if not items: + yield () + return + a = items[0] + for b in items[1:]: + for rest in matchings(tuple(x for x in items[1:] if x != b)): + yield ((a, b),) + rest + + frames = set() + for singleton in range(9): + for pairs in matchings(tuple(k for k in range(9) if k != singleton)): + indices = [] + for a, b in pairs: + pair = tuple(3 * (int(k == a) - int(k == b)) for k in range(9)) + triple = tuple(2 if k in (a, b, singleton) else -1 for k in range(9)) + indices.extend((lookup[pair], lookup[triple])) + frame = tuple(sorted(indices)) + require(all(dot(rows[i][1], rows[j][1]) == 0 for i, j in combinations(frame, 2)), + 'matching-frame orbit orthogonality') + frames.add(frame) + require(len(frames) == 945 and FRAME in frames, 'matching-frame orbit count') + return len(frames) + + +def check_model(rows, frame=FRAME): + require(len(rows) == 120 and len({u for u, _ in rows}) == 120, + '120 distinct root labels required') + require(len(frame) == 8 and len(set(frame)) == 8 and + all(type(i) is int and 0 <= i < 120 for i in frame), 'frame shape') + for i, j in combinations(frame, 2): + require(dot(rows[i][1], rows[j][1]) == 0, 'puncture must be an orthogonal frame') + for u, v in rows: + require(sum(v) == 0 and dot(v, v) == 18, 'sum-zero norm-two root') + for w, z in rows: + gram, remainder = divmod(dot(v, z), 9) + require(remainder == 0, 'integral Gram entries') + require((u & w).bit_count() % 2 == (gram + 1) % 2, + 'binary label/Gram pairing') + live = [row for i, row in enumerate(rows) if i not in frame] + require(len(live) == 112 and rational_rank(v for _, v in live) == 8, + 'live roots span the eight-dimensional sum-zero space') + require(rank(u for u, _ in live) == 9, 'live labels span F2^9') + for k in range(9): + require(rank(u for u, v in live if v[k]) == 9, 'column support label rank nine') + return live + + +def tables(live): + words = [sum(((u & w).bit_count() % 2) << i + for i, (u, _) in enumerate(live)) for w in range(512)] + unequal = {(j, k): sum((v[j] != v[k]) << i for i, (_, v) in enumerate(live)) + for j, k in combinations(range(9), 2)} + return words, unequal + + +def compatibility_spaces(live, words, unequal, anchor): + others = [k for k in range(9) if k != anchor] + allowed, forced = {}, {} + for k in others: + different = unequal[min(k, anchor), max(k, anchor)] + allowed[k] = [sum(1 << z for z in range(1, 512) + if not (words[w] & words[z] & different)) + for w in range(512)] + for z in range(1, 512): + support = words[z] & different + forced[k, z] = binary_basis(u for i, (u, _) in enumerate(live) + if support >> i & 1) + return others, allowed, forced + + +def plane_configurations(others, allowed): + """Every plane has exactly one encoding 0= (a ^ b): + continue + planes += 1 + hs = tuple(allowed[k][a] & allowed[k][b] for k in others) + dimensions = [] + for h in hs: + vectors = list(members(h)) + require(len(vectors) in (0, 1, 3), 'partner space dimension at most two') + if len(vectors) == 3: + require(vectors[0] ^ vectors[1] == vectors[2], 'partner plane closure') + dimensions.append((len(vectors) + 1).bit_length() - 1) + histogram[tuple(sorted(dimensions))] += 1 + if hs not in configs: + configs[hs] = {'first_plane': (a, b), 'multiplicity': 0} + configs[hs]['multiplicity'] += 1 + require(planes == 43435 and sum(c['multiplicity'] for c in configs.values()) == planes, + 'complete plane coverage') + return configs, [{'dimensions': list(ds), 'planes': count} + for ds, count in sorted(histogram.items())] + + +def subspace_options(k, h, forced, words): + """All subspaces of H: zero, every line, and H itself if dim H=2.""" + vectors = list(members(h)) + require(len(vectors) in (0, 1, 3), 'unsupported partner dimension') + options = [((), (), 0)] + for z in vectors: + options.append(((z,), forced[k, z], words[z])) + if len(vectors) == 3: + require(vectors[0] ^ vectors[1] == vectors[2], 'partner plane closure') + options.append((binary_basis(vectors), + binary_basis(x for z in vectors for x in forced[k, z]), + words[vectors[0]] | words[vectors[1]])) + return options + + +def enumerate_configuration(others, hs, forced, words, unequal, mutual=True): + choices = [(k, subspace_options(k, h, forced, words)) for k, h in zip(others, hs)] + choices.sort(key=lambda item: -len(item[1])) + best, leaves, conflicts = 0, 0, 0 + + def visit(position, constraints, dimension_sum, selected): + nonlocal best, leaves, conflicts + if position == len(choices): + leaves += 1 + # K_anchor is contained in the annihilator of these constraints. + best = max(best, 9 - len(constraints) + dimension_sum) + return + k, options = choices[position] + for zs, fs, support in options: + if mutual and any(support & old_support & unequal[min(k, j), max(k, j)] + for j, old_support in selected): + conflicts += 1 + continue + visit(position + 1, binary_basis(constraints + fs), + dimension_sum + len(zs), selected + [(k, support)]) + + visit(0, (), 0, []) + return best, leaves, conflicts + + +def census(live, words, unequal): + result = [] + for anchor in range(9): + others, allowed, forced = compatibility_spaces(live, words, unequal, anchor) + configs, histogram = plane_configurations(others, allowed) + maxima = Counter() + leaves = conflicts = 0 + for hs in configs: + maximum, count, rejected = enumerate_configuration(others, hs, forced, words, unequal) + require(maximum <= 10, 'total deficiency exceeds ten') + maxima[maximum] += 1 + leaves += count + conflicts += rejected + result.append({'anchor': anchor, 'planes': 43435, 'configurations': len(configs), + 'partner_dimension_histogram': histogram, + 'maximum_histogram': dict(sorted(maxima.items())), + 'compatible_leaves': leaves, 'rejected_branches': conflicts}) + return result + + +def check_identity(live, coefficients): + require(len(coefficients) == len(live) and all(len(c) == 9 for c in coefficients), + 'decoder shape') + for (_, v), c in zip(live, coefficients): + for _, z in live: + require(dot(c, z) == 2 * dot(v, z), 'exact all-pairs identity') + + +def witness(live, all_active): + # The first live line is e_0-e_2. Switch its anchor to 2 to activate term 0. + c = [tuple(2 * (x - v[2 if all_active and i == 0 else 0]) for x in v) + for i, (_, v) in enumerate(live)] + check_identity(live, c) + costs = [rank(u for (u, _), row in zip(live, c) if row[k]) for k in range(9)] + require(sum(costs) == 71, 'witness cost must be seventy-one') + require(not all_active or min(costs) > 0, 'all nine terms must be active') + return c, costs + + +def semantic_controls(rows, live, words, unequal, c): + passed = [] + + def rejected(name, function): + try: + function() + except ValueError: + passed.append(name) + return + raise ValueError('control unexpectedly accepted: ' + name) + + bad = list(c) + bad[0] = tuple(x + (k == 0) for k, x in enumerate(bad[0])) + rejected('coefficient_perturbation', lambda: check_identity(live, bad)) + bad = list(c) + bad[0] = (0,) + bad[0][1:] + rejected('active_term_deleted', lambda: check_identity(live, bad)) + corrupt = list(rows) + corrupt[1] = (corrupt[1][0] ^ 1, corrupt[1][1]) + rejected('label_pairing_corrupted', lambda: check_model(corrupt)) + rejected('nonorthogonal_puncture', lambda: check_model(rows, (1,) + FRAME[1:])) + others, allowed, forced = compatibility_spaces(live, words, unequal, 0) + hs = tuple(allowed[k][1] & allowed[k][508] for k in others) + require(hs[0].bit_count() == 3, 'puncturing permits a partner plane') + rejected('unpunctured_dimension_lemma', lambda: require(hs[0].bit_count() <= 1, + 'false dimension-one inference')) + relaxed, _, _ = enumerate_configuration(others, hs, forced, words, unequal, mutual=False) + checked, _, _ = enumerate_configuration(others, hs, forced, words, unequal) + require(relaxed == 11 and checked == 10, 'mutual compatibility is necessary') + passed.append('omitted_mutual_compatibility_changes_bound') + rejected('false_cost_seventy', lambda: require(sum(rank(u for (u, _), row in zip(live, c) + if row[k]) for k in range(9)) == 70, + 'support ranks disagree with claimed cost')) + # A non-real shift C_i = 2v_i + 3i*1, checked using integer real/imaginary parts. + check_identity(live, [tuple(2 * x for x in v) for _, v in live]) + require(all(dot((3,) * 9, v) == 0 for _, v in live), 'imaginary shift is in the kernel') + require(9 * rank(u for u, _ in live) == 81, 'generic complex shift cost') + passed.append('nonreal_kernel_shift_positive') + return passed + + +def compute(): + rows = model() + require(first_frame(rows) == FRAME, 'declared frame is not lexicographically first') + live = check_model(rows) + words, unequal = tables(live) + anchors = census(live, words, unequal) + _, dropped = witness(live, False) + c, active = witness(live, True) + result = {'schema_version': 1, 'kind': 'scoped proof with exhaustive finite lemmas', + 'model': 'fixed A8 simplex; one P112 frame puncture; all-pairs; separate term costs', + 'frame_indices': list(FRAME), 'frame_labels': [rows[i][0] for i in FRAME], + 'coordinate_permutation_punctures': matching_frame_orbit(rows), + 'live_roots': 112, 'live_root_rank': 8, 'column_label_ranks': [9] * 9, + 'anchors': anchors, 'total_planes': sum(a['planes'] for a in anchors), + 'total_configurations': sum(a['configurations'] for a in anchors), + 'total_compatible_leaves': sum(a['compatible_leaves'] for a in anchors), + 'deficiency_upper_bound': 10, 'sharp_copy_cost': 71, + 'dropped_witness_costs': dropped, 'active_witness_costs': active, + 'all_pairs_checked_per_witness': 112 * 112, + 'semantic_controls': semantic_controls(rows, live, words, unequal, c)} + return json.loads(json.dumps(result)) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write', action='store_true', help='regenerate the deterministic certificate') + args = parser.parse_args() + path = HERE / 'CERTIFICATE.json' + expected = None if args.write else json.loads(path.read_text()) + result = compute() + if args.write: + path.write_text(json.dumps(result, indent=2, sort_keys=True) + '\n') + else: + require(expected == result, 'certificate differs from exact replay') + print('PASS_A8_P112_DECODER_FLOOR planes=390915 configurations=19299 ' + 'compatible_leaves=462141 cost=71 controls=8') + + +if __name__ == '__main__': + main()