From da6308454686c77372e82a60e196ccb828285360 Mon Sep 17 00:00:00 2001 From: Hanson Sun <182361798+bbMisk@users.noreply.github.com> Date: Tue, 13 Oct 2026 23:56:46 -0400 Subject: [PATCH] Prove COPY71 for the complementary A8 simplex frame orbit --- .../a8-one-pair-frame-floor/CERTIFICATE.json | 1489 +++++++++++++++++ research/a8-one-pair-frame-floor/PROOF.md | 174 ++ research/a8-one-pair-frame-floor/README.md | 121 ++ research/a8-one-pair-frame-floor/SOURCES.json | 50 + research/a8-one-pair-frame-floor/TASK.json | 110 ++ .../a8-one-pair-frame-floor/VALIDATION.json | 67 + research/a8-one-pair-frame-floor/VERIFY.json | 39 + .../a8-one-pair-frame-floor/independent.py | 279 +++ .../a8-one-pair-frame-floor/test_package.py | 100 ++ research/a8-one-pair-frame-floor/verify.py | 424 +++++ 10 files changed, 2853 insertions(+) create mode 100644 research/a8-one-pair-frame-floor/CERTIFICATE.json create mode 100644 research/a8-one-pair-frame-floor/PROOF.md create mode 100644 research/a8-one-pair-frame-floor/README.md create mode 100644 research/a8-one-pair-frame-floor/SOURCES.json create mode 100644 research/a8-one-pair-frame-floor/TASK.json create mode 100644 research/a8-one-pair-frame-floor/VALIDATION.json create mode 100644 research/a8-one-pair-frame-floor/VERIFY.json create mode 100644 research/a8-one-pair-frame-floor/independent.py create mode 100644 research/a8-one-pair-frame-floor/test_package.py create mode 100644 research/a8-one-pair-frame-floor/verify.py diff --git a/research/a8-one-pair-frame-floor/CERTIFICATE.json b/research/a8-one-pair-frame-floor/CERTIFICATE.json new file mode 100644 index 0000000000..d651e6d815 --- /dev/null +++ b/research/a8-one-pair-frame-floor/CERTIFICATE.json @@ -0,0 +1,1489 @@ +{ + "active_witness_costs": [ + 1, + 8, + 8, + 9, + 9, + 9, + 9, + 9, + 9 + ], + "all_pairs_checked_per_witness": 12544, + "anchors": [ + { + "anchor": 0, + "compatible_leaves": 52829, + "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": 19816 + }, + { + "anchor": 1, + "compatible_leaves": 52829, + "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": 19816 + }, + { + "anchor": 2, + "compatible_leaves": 39482, + "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": 13904 + }, + { + "anchor": 3, + "compatible_leaves": 39482, + "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": 13904 + }, + { + "anchor": 4, + "compatible_leaves": 39482, + "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": 13904 + }, + { + "anchor": 5, + "compatible_leaves": 39482, + "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": 13904 + }, + { + "anchor": 6, + "compatible_leaves": 39482, + "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": 13904 + }, + { + "anchor": 7, + "compatible_leaves": 39482, + "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": 13904 + }, + { + "anchor": 8, + "compatible_leaves": 39482, + "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": 13904 + } + ], + "column_label_ranks": [ + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9 + ], + "coordinate_permutation_punctures": 1080, + "deficiency_upper_bound": 10, + "dropped_witness_costs": [ + 0, + 8, + 9, + 9, + 9, + 9, + 9, + 9, + 9 + ], + "frame_indices": [ + 0, + 85, + 94, + 99, + 105, + 108, + 112, + 113 + ], + "frame_labels": [ + 508, + 28, + 100, + 388, + 168, + 328, + 304, + 208 + ], + "frame_partition": { + "all_frames_sha256": "58f0515dd5e6a1b1dc15b30625935d70904a65b88b406d57aa9e3f2aa540f596", + "matching_frames": 945, + "matching_representative": [ + 0, + 15, + 26, + 33, + 42, + 89, + 112, + 119 + ], + "one_pair_counts_by_pair": [ + 30, + 30, + 30, + 30, + 30, + 30, + 30, + 30, + 30, + 30, + 30, + 30, + 30, + 30, + 30, + 30, + 30, + 30, + 30, + 30, + 30, + 30, + 30, + 30, + 30, + 30, + 30, + 30, + 30, + 30, + 30, + 30, + 30, + 30, + 30, + 30 + ], + "one_pair_frames": 1080, + "one_pair_orbit_sha256": "30c09e9f3b985bfe63ab991a1e77df9cca8c01a8e3d74ac0c9516238207a1947", + "one_pair_representative": [ + 0, + 85, + 94, + 99, + 105, + 108, + 112, + 113 + ], + "total_frames": 2025 + }, + "kind": "scoped proof with exhaustive finite lemmas", + "live_root_rank": 8, + "live_roots": 112, + "model": "fixed A8 simplex; one-pair P112 frame orbit; 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", + "omitted_frame_orbit_member", + "matching_orbit_is_not_complementary" + ], + "sharp_copy_cost": 71, + "total_compatible_leaves": 382032, + "total_configurations": 20019, + "total_planes": 390915 +} diff --git a/research/a8-one-pair-frame-floor/PROOF.md b/research/a8-one-pair-frame-floor/PROOF.md new file mode 100644 index 0000000000..7055dc5001 --- /dev/null +++ b/research/a8-one-pair-frame-floor/PROOF.md @@ -0,0 +1,174 @@ +# The complementary A8 simplex frame orbit + +This proof follows PR1248's deficiency method and PR1304's punctured-frame +extension. The changed frame, orbit coverage and finite lemmas below are +recomputed; no pending theorem supplies an assumed lower bound. + +## Statement + +Let V be the sum-zero subspace of R^9. Take the 120 root lines represented by +`e_a-e_b` for `0<=a= 7*9^(1-a)+8^(1-a) > 8*8^(1-a), 0<=a<1. +``` + +This is strictly worse than the eight rank-eight coordinate COPY terms under +those same accounting parameters. It does not compare complete suppliers +with changed widths, role counts or shared-copy mechanisms. + +## Scope + +The result does not cover changed nine-normal families, unrestricted factors, +masked identities, other live-set sizes or shared-copy billing. No physical +word, frame/restoration/hosting proof, selected cold replay, new κ or all-size +multiplication theorem is supplied. The selected construction's inherited +algorithmic, analytic, precision and bit-interface obligations remain open. + +Credit commdata2338/PR1304, Philipp/mightyOil/PR1248, joaqcoo/PR1224 and the +decoder/label lineage listed in README.md. Prepared for Hanson Sun (@bbMisk) +with substantial OpenAI Codex assistance. Apache-2.0. diff --git a/research/a8-one-pair-frame-floor/README.md b/research/a8-one-pair-frame-floor/README.md new file mode 100644 index 0000000000..8f3748696a --- /dev/null +++ b/research/a8-one-pair-frame-floor/README.md @@ -0,0 +1,121 @@ +# Sharp COPY cost 71 on the remaining A8 simplex P112 frame orbit + +The fixed nine-normal A8 simplex decoder has minimum separate COPY cost **71** +on each of the **1,080 one-pair frame punctures**, for arbitrary complex row +shifts. An exact witness with all nine terms active attains the bound. Thus +this family cannot beat the standard P112 COPY cost 64. + +This resolves the other-frame question in +[commdata2338's PR1304](https://github.com/CrocSwap/integer-mult-bounds/pull/1304). +That predecessor covers 945 matching frames. A complete census here partitions +all 2,025 orthogonal E8 eight-frames into precisely those 945 frames and the +1,080 frames treated here. The latter consist of one pair root and a Fano +plane on the other seven coordinates. No theorem from a pending PR is assumed +to establish the new orbit's bound. + +This is a scoped proof with exhaustive finite lemmas, **not a new supplier or +κ result**. It leaves the selected record and frozen sources unchanged. + +## Exact scope and evidence + +In the sum-zero subspace of Q^9, use roots `e_a-e_b` and +`1_S-(1/3)1`, for three-element sets S, in lexicographic order within those +two groups. Fix `T_ik=r_ik`; require `D T^t=2G` on all live pairs, with ordinary +transpose. Every permitted D has `D_ik=2r_ik+t_i`, with arbitrary `t_i` in C. +Term costs are binary label-pairing ranks on the actual nonzero supports. + +The representative puncture is `[0,85,94,99,105,108,112,113]`. The proof in +[PROOF.md](PROOF.md) reduces all complex shifts to finite binary deficiency +compatibility. The two coordinate-anchor classes give: + +| Anchors | Planes per anchor | Partner-space tuples per anchor | Compatible choices per anchor | Maximum deficiency sum | +|---|---:|---:|---:|---:| +| 0, 1 | 43,435 | 2,131 | 52,829 | 10 | +| 2 through 8 | 43,435 | 2,251 | 39,482 | 9 | + +The primary replay checks all nine anchors: 390,915 planes, 20,019 distinct +ordered partner-space tuples across anchors, and 382,032 compatible choices. +The resulting cost is at least `81-10=71`. Witness costs are +`(0,8,9,9,9,9,9,9,9)` and, with all terms active, +`(1,8,8,9,9,9,9,9,9)`. Both all-pairs identities are checked exactly. + +The second implementation derives labels from the rational Gram matrix, +uses nullspaces and Cartesian products instead of the primary bitmask search, +and checks two anchors with explicit puncture-preserving permutations covering +all nine. It also re-enumerates all frames and constructs the new orbit from +36 pairs and 30 Fano planes, separately from the primary coordinate-orbit BFS. + +Both implementations are adapted from PR1304, with exact original file pins +in [SOURCES.json](SOURCES.json) and attribution in their headers. Every finite +premise for the changed puncture is recomputed. This is reuse of credited +methods; no independent peer review is claimed. + +## Reproduce + +From the repository root, standard library only: + +```sh +python3.12 -B scripts/research_package.py --package research/a8-one-pair-frame-floor +``` + +The registered replay runs the primary checker, second checker and package +failure tests. Individual checks also work with Python 3.12 or later: + +```sh +python3 -I -B research/a8-one-pair-frame-floor/verify.py +python3 -I -B research/a8-one-pair-frame-floor/independent.py +python3 -I -B research/a8-one-pair-frame-floor/test_package.py +``` + +Expected mathematical markers: + +```text +PASS_A8_ONE_PAIR_FRAME_FLOOR frames=1080 anchors=9 planes=390915 configurations=20019 compatible_leaves=382032 cost=71 controls=10 +PASS_A8_ONE_PAIR_SECOND_CHECK anchors=2 transported=9 planes=86870 compatible_leaves=92311 cost=71 +``` + +Default replay is read-only and compares the entire deterministic certificate. +`verify.py --write` explicitly regenerates it. Ten semantic controls cover +identity, support costs, labels, puncture legality, compatibility, complex +shifts and omitted/misidentified frame coverage. Package tests exercise altered, +missing and malformed receipts and optimized relocated replay. + +## Limits and credit + +Only this fixed nine-normal, all-pairs, separately charged family is covered. +Other normals, arbitrary two-factor or masked decoders, other live-set sizes +and shared-copy pricing are outside the result. The COPY power comparison in +the proof fixes the width, normalization and multiplicity; it is not a complete +supplier invoice. Physical gathering, frame legality, restoration, hosting, +precision/tape, all-size/compiler, common-label/mutable-source, analytic and +bit H1–H5 obligations are not checked. No selected cold replay, Lean proof, +hosted-CI success, human review or maintainer acceptance is claimed. + +Predecessor credit: + +- commdata2338, PR1304: matching-frame floor, both adapted implementations, + and the explicit other-frame question. +- Philipp / mightyOil, PR1248: the deficiency-space method on P120. +- joaqcoo, PR1224: the one-sided nine-term normal form and A8 family. +- DreamingOfClouds, PR717/595/446: decoder and separate-copy label model; + Joel Pulikkan / GamingPuzzled, PR620: the coordinate COPY64 construction; + themilkman216, PR968, and woklerx, PR1077: surrounding all-pairs bounds. + +Base main: `ebedc0895eb4c06725af020bc1af165722b0a3ce`. The task, selector nonce, +exact predecessor heads and overlap boundaries are in [TASK.json](TASK.json). +The claim is in [discussion 1241](https://github.com/CrocSwap/integer-mult-bounds/discussions/1241#discussioncomment-18914233). + +Prepared for Hanson Sun (@bbMisk), with substantial OpenAI Codex assistance in +the mathematics, both adaptations, verification and writing. Apache-2.0. + +## Open next questions + +- **A different specified nine-normal family.** Can an A7+A1 or A2+E6 family + from PR1224 achieve COPY cost below 64 on a named P112 puncture? First derive + its exact kernel-shift classes and column-label ranks, then a favorable + finite compatibility bound. The fixed simplex normals are essential here; + neither the deficiency table nor the frame symmetry automatically transfers. +- **Shared-copy accounting.** Can a concrete physical implementation share + copied information across these nine terms at a net saving? First write its + entry/exit contract and full recursive bill. This theorem assumes separate + term charges; a support overlap alone is not a paid implementation. diff --git a/research/a8-one-pair-frame-floor/SOURCES.json b/research/a8-one-pair-frame-floor/SOURCES.json new file mode 100644 index 0000000000..5a6a241868 --- /dev/null +++ b/research/a8-one-pair-frame-floor/SOURCES.json @@ -0,0 +1,50 @@ +{ + "schema_version": 1, + "base_commit": "ebedc0895eb4c06725af020bc1af165722b0a3ce", + "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-frame-pair-decoders/verify.py", + "usage": "provenance", + "git_blob": "57dd8993e8ac016e8a92a9a885392b58014137bb", + "sha256": "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395" + } + ], + "external_predecessors": [ + { + "pr": 1304, + "author": "commdata2338, with substantial OpenAI Codex assistance", + "head": "a052f0da36a3845c2ec785fd44e5b9e50de3b688", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1304", + "usage": "Method and adapted implementations; no pending theorem is assumed. Exact original file pins below.", + "files": [ + { + "path": "research/a8-p112-decoder-screen/verify.py", + "git_blob": "188d3a8fda62067dd6f7c37e79a65a3e0cbe2fa7", + "sha256": "c8dff5ebf75511bf7c5e962a42189977ef5b20ce02e6f9734e4648e695ca3148" + }, + { + "path": "research/a8-p112-decoder-screen/independent.py", + "git_blob": "02035af27f93aee0f0205b69a3be99fe4362fd13", + "sha256": "e646772a4b25a26808bdded1362481a63c92fbaa3d61ad33aa6bfea38a40ff03" + }, + { + "path": "research/a8-p112-decoder-screen/PROOF.md", + "git_blob": "4f18ea6417759e73f9e03b5878f75c3fe3b0efd7", + "sha256": "2e7640f6bf1a683fe7e830414065c41e8fa38155023a97a27aadaa9a5f8a068b" + } + ] + } + ] +} diff --git a/research/a8-one-pair-frame-floor/TASK.json b/research/a8-one-pair-frame-floor/TASK.json new file mode 100644 index 0000000000..be8ae9e8d9 --- /dev/null +++ b/research/a8-one-pair-frame-floor/TASK.json @@ -0,0 +1,110 @@ +{ + "schema_version": 1, + "task_id": "complex-masked-decoder", + "priority_revision": 2, + "base_commit": "ebedc0895eb4c06725af020bc1af165722b0a3ce", + "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": "Fixed A8 simplex nine-term all-pairs decoders on the 1080 one-pair orthogonal-frame punctures; arbitrary complex per-row kernel shifts; separate COPY costs.", + "scope_change_reason": "Take the overcomplete branch and resolve PR1304's explicit question about frame orbits outside its 945 matching frames.", + "bottleneck_link": "A separate COPY cost below the existing 64 is a necessary first saving for this fixed nine-normal family; reject before paying physical realization if the exact floor exceeds 64.", + "budget_minutes": 60, + "stop_rule": "Stop construction if an exact copy-only relaxation proves cost at least 64. Spend at most 40 minutes on the census/proof and reserve the remainder for validation and handoff.", + "outcome": "negative-result", + "evidence": "Exact sharp COPY floor 71 on all 1080 one-pair frames. All 2025 frames partition into S9 orbits 945+1080; 390915 planes, 20019 partner-space tuples and 382032 compatible choices; exact all-active witness; second arithmetic implementation and semantic/package rejection controls.", + "author": "Hanson Sun (bbMisk), with OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in mathematics, implementation, verification and writing. No independent human review.", + "open_questions": [ + { + "question": "Can another specified nine-normal family from PR1224 attain COPY cost below 64 on a named P112 puncture?", + "why_it_matters": "The fixed A8 simplex family cannot supply a separate-copy saving on this remaining frame orbit.", + "first_step": "Choose A7+A1 or A2+E6 normals, derive their exact kernel-shift classes and column ranks, and formulate a finite compatibility bound.", + "blocked_by": "The simplex normals and compatibility census do not transfer automatically; physical realization remains separate." + }, + { + "question": "Can a physical implementation share copied information across the nine terms at a net saving?", + "why_it_matters": "The theorem prices each term separately; sharing changes an explicit hypothesis.", + "first_step": "Specify a concrete entry/exit contract and complete recursive bill for a shared-copy implementation.", + "blocked_by": "Support overlap alone does not establish legal gathering, frames, restoration or hosting." + } + ], + "selector_nonce": "c5f00b62a291989a1ddeed9c8a5aa1a1", + "scope_key": "complex-masked-decoder/a8-simplex/p112-one-pair-frames/complex-row-shifts", + "nearest_overlap": [ + { + "pr": 1304, + "head": "a052f0da36a3845c2ec785fd44e5b9e50de3b688", + "difference": "Predecessor proves sharp floor 71 for 945 matching frames only; this package addresses the complementary 1080 frames." + }, + { + "pr": 1248, + "head": "f226f4329a996b0a1bea8794179a91b5d0ed80bf", + "difference": "P120 deficiency-space method; no P112 puncture bound." + }, + { + "pr": 1224, + "head": "00e6ed0810b8ebc7f6133e2c036d0f1c9a3a4162", + "difference": "Nine-term normal form and candidate family; no exact one-pair P112 optimum." + } + ], + "optimistic_budget": "At most 63 separate copied coordinates would be needed to beat COPY64; set every extra frame, gathering, restoration and hosting charge to zero for this screen.", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1241#discussioncomment-18914233", + "submission_base_commit": "81e81af67714bdc8d1693b0bf5c29468b92f62ff", + "submission_priority_review": { + "revision": 3, + "disposition": "Retain the assigned revision-2 result. This is a completed COPY-family obstruction, not a new complex kappa or packing claim. PROOF.md additionally compares separate COPY powers for fixed billing; no incumbent ceiling calculation is invoked." + }, + "overlap_check": { + "searched_at": "2026-10-14T03:52:55.567152+00:00", + "coverage": { + "open_prs": { + "fetched_at": "2026-10-14T03:52:26.272461+00:00", + "complete_pagination": true, + "records": 733 + }, + "discussions": { + "fetched_at": "2026-10-14T03:52:55.514421+00:00", + "complete_pagination": true, + "records": 244 + } + }, + "warnings": [], + "limits": "Remote PR scope is open PRs including drafts. Closed work is searched through local READMEs, TASK metadata and ledger only. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission.", + "finding": "No additional claim for the complementary 1080 A8 one-pair punctures found in the stated coverage. The session claim is excluded from that observation. PR1590 concerns other root-unit decoder lemmas; PR1304 remains the matching-frame predecessor. No novelty guarantee." + } +} diff --git a/research/a8-one-pair-frame-floor/VALIDATION.json b/research/a8-one-pair-frame-floor/VALIDATION.json new file mode 100644 index 0000000000..633463cdc6 --- /dev/null +++ b/research/a8-one-pair-frame-floor/VALIDATION.json @@ -0,0 +1,67 @@ +{ + "schema_version": 1, + "environment": { + "platform": "macOS-27.0.1-arm64-arm-64bit-Mach-O", + "machine": "arm64", + "registered_python": "Python 3.12.13", + "optimized_crosscheck_python": "3.14.6" + }, + "commands": [ + { + "argv": [ + "python3.12", + "-B", + "scripts/research_package.py", + "--package", + "research/a8-one-pair-frame-floor" + ], + "exit_status": 0, + "result": "Both mathematical checkers and five package tests passed; ten primary semantic controls." + }, + { + "argv": [ + "python3", + "-I", + "-O", + "-B", + "research/a8-one-pair-frame-floor/verify.py" + ], + "exit_status": 0 + }, + { + "argv": [ + "python3", + "-I", + "-O", + "-B", + "research/a8-one-pair-frame-floor/independent.py" + ], + "exit_status": 0 + }, + { + "argv": [ + "python3", + "-B", + "scripts/verify_selected_result.py" + ], + "exit_status": 0 + }, + { + "argv": [ + "python3", + "-B", + "research/complex-decoder-field-extension-seed44/verify.py" + ], + "exit_status": 0, + "scope": "Original task positive control only." + } + ], + "certificate_sha256": "0b3dce20649b6785ddf4fa5724521a803f987bc3389158006b1d569bb9479f98", + "not_run": [ + "Full selected supplier cold replay", + "Native physical admission", + "Lean proof", + "Hosted CI", + "Independent human review" + ] +} diff --git a/research/a8-one-pair-frame-floor/VERIFY.json b/research/a8-one-pair-frame-floor/VERIFY.json new file mode 100644 index 0000000000..e1e6134744 --- /dev/null +++ b/research/a8-one-pair-frame-floor/VERIFY.json @@ -0,0 +1,39 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete frame/orbit coverage; all nine deficiency anchors; sharp witnesses; ten semantic controls; exact full receipt comparison." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 120, + "checks": "Gram-derived labels and nullspaces; Cartesian compatibility; two stabilizer anchor orbits; direct witness ranks; separate Fano frame coverage." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 240, + "checks": "Missing, malformed, false-cost, incomplete-anchor and changed-orbit receipts; optimized read-only relocated replay." + } + ] +} diff --git a/research/a8-one-pair-frame-floor/independent.py b/research/a8-one-pair-frame-floor/independent.py new file mode 100644 index 0000000000..c50b3627f9 --- /dev/null +++ b/research/a8-one-pair-frame-floor/independent.py @@ -0,0 +1,279 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Second arithmetic implementation: Gram labels, nullspaces, Cartesian products. + +Adapted from commdata2338's PR1304 independent.py at a052f0da36a3845c2ec785fd44e5b9e50de3b688 +(original blob 02035af27f93aee0f0205b69a3be99fe4362fd13, Apache-2.0). +Changes: the one-pair puncture and its explicitly checked stabilizer, +anchor representatives 0 and 2, and the complementary orbit's exact receipts. +No primary or predecessor imports. Both adaptations are by the same assistant; +this is not independent peer review. Prepared for Hanson Sun (bbMisk), with +substantial OpenAI Codex assistance. +""" + +from collections import Counter +from fractions import Fraction +from functools import lru_cache +from itertools import combinations, permutations, product +import hashlib +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 check_frame_coverage(roots, gram, frame): + """Set-clique census plus the pair/Fano construction; no orbit-BFS reuse.""" + neighbors = [{j for j in range(i + 1, 120) if gram[i][j] == 0} + for i in range(120)] + frames = set() + + def extend(prefix, candidates): + if len(prefix) == 8: + frames.add(prefix) + return + for i in sorted(candidates): + remaining = candidates & neighbors[i] + if len(prefix) + 1 + len(remaining) >= 8: + extend(prefix + (i,), remaining) + + extend((), set(range(120))) + check(len(frames) == 2025, 'complete rational Gram frame census') + one_pair = {f for f in frames if sum(i < 36 for i in f) == 1} + matching = {f for f in frames if sum(i < 36 for i in f) == 4} + check(len(one_pair) == 1080 and len(matching) == 945 and + one_pair | matching == frames, 'independent frame partition') + # The representative's seven triple roots give a labeled Fano plane. + lines = [tuple(k - 2 for k, x in enumerate(roots[i]) if x > 0) + for i in frame if i >= 36] + check(len(lines) == 7 and all(len(t) == 3 for t in lines), 'Fano seed') + planes = {tuple(sorted(tuple(sorted(p[k] for k in t)) for t in lines)) + for p in permutations(range(7))} + check(len(planes) == 30, 'all coordinate images of the Fano plane') + lookup = {r: i for i, r in enumerate(roots)} + constructed = set() + for a, b in combinations(range(9), 2): + others = [k for k in range(9) if k not in (a, b)] + pair = tuple(Fraction(int(k == a) - int(k == b)) for k in range(9)) + for plane in planes: + indices = [lookup[pair]] + for t in plane: + triple = {others[k] for k in t} + root = tuple(Fraction(int(k in triple)) - Fraction(1, 3) for k in range(9)) + indices.append(lookup[root]) + constructed.add(tuple(sorted(indices))) + check(constructed == one_pair, 'Fano construction exactly covers the complementary orbit') + def digest(fs): + return hashlib.sha256(json.dumps(sorted(fs), separators=(',', ':')).encode()).hexdigest() + return {'all_frames_sha256': digest(frames), 'one_pair_orbit_sha256': digest(one_pair)} + + +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, 85, 94, 99, 105, 108, 112, 113) + check(all(gram[i][j] == 0 for i, j in combinations(frame, 2)), 'frame orthogonality') + frame_coverage = check_frame_coverage(roots, gram, frame) + # Explicit puncture stabilizer; the two anchor orbits are {0,1}, {2,...,8}. + permutations = [ + [1, 0, 2, 3, 4, 5, 6, 7, 8], + [0, 1, 3, 2, 4, 5, 7, 6, 8], + [0, 1, 4, 2, 3, 5, 8, 6, 7], + [0, 1, 5, 2, 6, 3, 7, 4, 8], + [0, 1, 6, 2, 5, 3, 8, 4, 7], + [0, 1, 7, 2, 8, 3, 5, 4, 6], + [0, 1, 8, 2, 7, 3, 6, 4, 5], + ] + lookup = {r: i for i, r in enumerate(roots)} + for permutation in permutations: + check(sorted(permutation) == list(range(9)), 'coordinate permutation') + 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') + for representative, expected in [(0, {0, 1}), (2, set(range(2, 9)))]: + orbit = {representative} + while True: + new = orbit | {p[i] for p in permutations for i in orbit} + if new == orbit: + break + orbit = new + check(orbit == expected, 'anchor orbit') + 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, frame_coverage + + +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, frame_coverage = geometry() + receipt = json.loads((Path(__file__).resolve().parent / 'CERTIFICATE.json').read_text()) + for key, value in frame_coverage.items(): + check(value == receipt['frame_partition'][key], 'frame census receipt: ' + key) + results = [audit_anchor(roots, labels, a) for a in (0, 2)] + for result in results: + anchors = (0, 1) if result['anchor'] == 0 else range(2, 9) + 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_ONE_PAIR_SECOND_CHECK anchors=2 transported=9 planes=86870 ' + f"compatible_leaves={sum(r['compatible_leaves'] for r in results)} cost=71") + + +if __name__ == '__main__': + main() diff --git a/research/a8-one-pair-frame-floor/test_package.py b/research/a8-one-pair-frame-floor/test_package.py new file mode 100644 index 0000000000..faacde2395 --- /dev/null +++ b/research/a8-one-pair-frame-floor/test_package.py @@ -0,0 +1,100 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Fail-closed receipt and portable replay controls, in disposable copies only.""" + +from contextlib import contextmanager +import hashlib +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent + + +@contextmanager +def isolated(): + with tempfile.TemporaryDirectory(prefix='a8-one-pair-') as temporary: + package = Path(temporary) / 'relocated' + package.mkdir() + for name in ('verify.py', 'independent.py', 'CERTIFICATE.json'): + shutil.copyfile(HERE / name, package / name) + try: + yield package + finally: + package.chmod(0o755) + for path in package.iterdir(): + path.chmod(0o644) + + +def replay(package, script, optimized=False): + flags = ['-I', '-B'] + (['-O'] if optimized else []) + return subprocess.run([sys.executable, *flags, str(package / script)], + cwd=package.parent, text=True, capture_output=True, timeout=120) + + +def mutate_receipt(package, change): + path = package / 'CERTIFICATE.json' + receipt = json.loads(path.read_text()) + change(receipt) + path.write_text(json.dumps(receipt)) + + +def tree_hashes(package): + return {p.name: hashlib.sha256(p.read_bytes()).hexdigest() for p in package.iterdir()} + + +class PackageTests(unittest.TestCase): + def assert_rejected(self, result, reason): + self.assertNotEqual(result.returncode, 0, result.stdout + result.stderr) + self.assertNotIn('PASS_A8_', result.stdout) + self.assertIn(reason, result.stderr) + + def test_missing_and_malformed_receipts(self): + for contents, reason in [(None, 'FileNotFoundError'), ('{', 'JSONDecodeError')]: + with self.subTest(reason=reason), isolated() as package: + path = package / 'CERTIFICATE.json' + if contents is None: + path.unlink() + else: + path.write_text(contents) + self.assert_rejected(replay(package, 'verify.py'), reason) + + def test_false_copy_cost(self): + with isolated() as package: + mutate_receipt(package, lambda c: c.update(sharp_copy_cost=70)) + self.assert_rejected(replay(package, 'verify.py', optimized=True), + 'certificate differs from exact replay') + + def test_missing_anchor(self): + with isolated() as package: + mutate_receipt(package, lambda c: c['anchors'].pop()) + self.assert_rejected(replay(package, 'verify.py'), + 'certificate differs from exact replay') + + def test_changed_frame_coverage(self): + with isolated() as package: + mutate_receipt(package, lambda c: c['frame_partition'].update( + one_pair_orbit_sha256='0' * 64)) + self.assert_rejected(replay(package, 'independent.py', optimized=True), + 'frame census receipt: one_pair_orbit_sha256') + + def test_optimized_read_only_relocated_replay(self): + with isolated() as package: + before = tree_hashes(package) + for path in package.iterdir(): + path.chmod(0o444) + package.chmod(0o555) + for script, marker in [('verify.py', 'PASS_A8_ONE_PAIR_FRAME_FLOOR'), + ('independent.py', 'PASS_A8_ONE_PAIR_SECOND_CHECK')]: + result = replay(package, script, optimized=True) + self.assertEqual(result.returncode, 0, result.stdout + result.stderr) + self.assertIn(marker, result.stdout) + self.assertEqual(before, tree_hashes(package), 'default replay wrote to its input tree') + + +if __name__ == '__main__': + unittest.main(verbosity=2) diff --git a/research/a8-one-pair-frame-floor/verify.py b/research/a8-one-pair-frame-floor/verify.py new file mode 100644 index 0000000000..ec67025ad9 --- /dev/null +++ b/research/a8-one-pair-frame-floor/verify.py @@ -0,0 +1,424 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Exact A8 simplex copy floor on the complementary one-pair frame orbit. + +Adapted from commdata2338's PR1304 verify.py at a052f0da36a3845c2ec785fd44e5b9e50de3b688 +(original blob 188d3a8fda62067dd6f7c37e79a65a3e0cbe2fa7, Apache-2.0). +The deficiency method is due to mightyOil's PR1248, following joaqcoo's PR1224. +Changes: one-pair puncture, complete frame/orbit census, new nine-anchor results, +and orbit-boundary controls. All finite premises are recomputed. +Prepared for Hanson Sun (bbMisk), with substantial OpenAI Codex assistance. +""" + +import argparse +from collections import Counter +from fractions import Fraction +import hashlib +from itertools import combinations +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +FRAME = (0, 85, 94, 99, 105, 108, 112, 113) +MATCHING_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 all_frames(rows): + """Every size-eight clique, visited once in increasing index order.""" + adjacent = [sum(1 << j for j in range(i + 1, len(rows)) + if dot(rows[i][1], rows[j][1]) == 0) + for i in range(len(rows))] + answer = [] + + def extend(prefix, candidates): + if len(prefix) == 8: + answer.append(prefix) + return + while candidates and len(prefix) + candidates.bit_count() >= 8: + bit = candidates & -candidates + i = bit.bit_length() - 1 + candidates ^= bit + extend(prefix + (i,), candidates & adjacent[i]) + + extend((), (1 << len(rows)) - 1) + return set(answer) + + +def permutation_maps(rows): + """Adjacent coordinate transpositions generate the full S9 action.""" + lookup = {v: i for i, (_, v) in enumerate(rows)} + maps = [] + for k in range(8): + images = [] + for _, root in rows: + v = list(root) + v[k], v[k + 1] = v[k + 1], v[k] + image = tuple(v) + if image not in lookup: + image = tuple(-x for x in image) + require(image in lookup, 'coordinate swap preserves root lines') + images.append(lookup[image]) + require(sorted(images) == list(range(120)), 'root-line permutation is bijective') + maps.append(images) + return maps + + +def orbit_of(frame, maps): + seen = {tuple(sorted(frame))} + todo = list(seen) + while todo: + current = todo.pop() + for permutation in maps: + image = tuple(sorted(permutation[i] for i in current)) + if image not in seen: + seen.add(image) + todo.append(image) + return seen + + +def require_partition(frames, matching, one_pair): + require(len(frames) == 2025, 'complete E8 frame count') + require(len(matching) == 945 and len(one_pair) == 1080, 'S9 orbit sizes') + require(not matching & one_pair and matching | one_pair == frames, + 'two disjoint coordinate orbits exhaust all frames') + require(all(sum(i < 36 for i in f) == 4 for f in matching), + 'matching orbit has four pair roots') + require(all(sum(i < 36 for i in f) == 1 for f in one_pair), + 'complementary orbit has one pair root') + + +def frame_partition(rows): + frames = all_frames(rows) + maps = permutation_maps(rows) + matching = orbit_of(MATCHING_FRAME, maps) + one_pair = orbit_of(FRAME, maps) + require_partition(frames, matching, one_pair) + # A pair and a Fano plane on the remaining seven coordinates. This is + # checked for every frame, rather than assumed to establish coverage. + per_pair = Counter() + for frame in one_pair: + pair = next(i for i in frame if i < 36) + excluded = {k for k, x in enumerate(rows[pair][1]) if x} + triples = [set(members(rows[i][0])) for i in frame if i >= 36] + require(len(triples) == 7 and all(len(t) == 3 and not t & excluded + for t in triples), 'Fano points') + counts = Counter(tuple(sorted(p)) for t in triples for p in combinations(t, 2)) + require(len(counts) == 21 and set(counts.values()) == {1}, 'Fano line pairs') + per_pair[pair] += 1 + require(per_pair == Counter({i: 30 for i in range(36)}), '30 Fano planes per pair') + def digest(fs): + return hashlib.sha256(json.dumps(sorted(fs), separators=(',', ':')).encode()).hexdigest() + return {'total_frames': 2025, 'matching_frames': 945, 'one_pair_frames': 1080, + 'one_pair_representative': list(FRAME), 'matching_representative': list(MATCHING_FRAME), + 'one_pair_counts_by_pair': [per_pair[i] for i in range(36)], + 'all_frames_sha256': digest(frames), 'one_pair_orbit_sha256': digest(one_pair)} + + +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') + maps = permutation_maps(rows) + frames = all_frames(rows) + matching, one_pair = orbit_of(MATCHING_FRAME, maps), orbit_of(FRAME, maps) + rejected('omitted_frame_orbit_member', + lambda: require_partition(frames, matching, one_pair - {FRAME})) + rejected('matching_orbit_is_not_complementary', + lambda: require_partition(frames, matching, matching)) + return passed + + +def compute(): + rows = model() + orbits = frame_partition(rows) + 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-pair P112 frame orbit; all-pairs; separate term costs', + 'frame_indices': list(FRAME), 'frame_labels': [rows[i][0] for i in FRAME], + 'frame_partition': orbits, + 'coordinate_permutation_punctures': 1080, + '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_ONE_PAIR_FRAME_FLOOR frames=1080 anchors=9 planes=390915 ' + f"configurations={result['total_configurations']} " + f"compatible_leaves={result['total_compatible_leaves']} cost=71 " + f"controls={len(result['semantic_controls'])}") + + +if __name__ == '__main__': + main()