diff --git a/research/dyadic-center-anchor-bound/CERTIFICATE.json b/research/dyadic-center-anchor-bound/CERTIFICATE.json new file mode 100644 index 0000000000..c263c0b3b7 --- /dev/null +++ b/research/dyadic-center-anchor-bound/CERTIFICATE.json @@ -0,0 +1,30 @@ +{ + "basis": "binomial(h-10,j), j=0,1,2,3", + "difference": "cost(k)-cost(0), k=1,2,3,4", + "positive_newton_coefficients": [ + [ + 20, + 19, + 7, + 1 + ], + [ + 5, + 21, + 11, + 2 + ], + [ + 53, + 48, + 19, + 3 + ], + [ + 122, + 72, + 24, + 4 + ] + ] +} diff --git a/research/dyadic-center-anchor-bound/CLAIM.json b/research/dyadic-center-anchor-bound/CLAIM.json new file mode 100644 index 0000000000..28d66d0253 --- /dev/null +++ b/research/dyadic-center-anchor-bound/CLAIM.json @@ -0,0 +1,41 @@ +{ + "track": "Complex supplier: scoped negative result for a complete center-basis family", + "assignment_seed": 33, + "randomness": "secrets.randbelow(100), backed by OS randomness", + "started_utc": "2026-10-13T13:51:46.586386+00:00", + "base_commit": "47481c89fd30a43f8f882eb4b391e89c29273fd0", + "selected_at_base": { + "pr": 890, + "kappa": "1661957774647029/1000000000000000000" + }, + "candidates": [ + { + "task": "Bounded single-scratch dyadic coefficient synthesis", + "decision": "Not selected: direct overlap with PR882 and PR837." + }, + { + "task": "Raw coordinate-total factory resynthesis", + "decision": "Not selected: active PR922, PR924 and PR931 overlap." + }, + { + "task": "Classify all integral constant-row shears of the historical rank-h center, with complete gather/scatter costs", + "decision": "Selected: algebraic orbit classification and an all-even-h optimum, beyond PR809 one-step and PR937 second-step searches." + } + ], + "object": "A=I+sum(a_i E_i,p), integer a_i, fixing one constant gather row and all nonconstant gather differences; preserve gather alphabet {0,+1,-1} and scatter numerators {0,+1,-1,+2,-2}.", + "method": "Translate to binary anchors; reduce all subsets to cardinality orbits; certify admissibility and exact cost polynomials. Use pivot p=33 mod 26=7 for the h26 finite replay.", + "domain": "All integer shear vectors for every even h>=8 within the stated alphabets; finite diagnostics all 128 anchors at h8, 512 at h10, and 26 cardinality representatives at h26.", + "stopping_rule": "Complete the class theorem, exact polynomial certificate and stated finite diagnostics; do not expand to general nonconstant-row mixing.", + "expected_deliverable": "Scoped optimality/negative-result note, exact offline checker, source pins, meaningful mutation controls, one focused PR.", + "expected_finish_utc": "2026-10-13T14:36:46Z", + "verification_reserved_from_utc": "2026-10-13T14:25:31Z", + "coordination": "No pinned issue in live GraphQL check; local claim per sprint instructions. Open PR list covered 714 entries through PR943; targeted metadata checked PR809, PR937, PR882, PR837 and PR922.", + "status": "completed", + "result": { + "pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/947", + "branch": "research/center-anchor-bound-seed33", + "summary": "Exact constant-row integral-shear classification; PR937 uniquely minimizes the complete cost for fixed pivot and every even h>=10. h8 has a certified size-two exception. No new kappa.", + "verification": "14 main controls, 9 package tests, 4 inherited tests and selected-record integrity pass.", + "completed_utc": "2026-10-13T14:16:18.246472+00:00" + } +} diff --git a/research/dyadic-center-anchor-bound/EXPECTED.json b/research/dyadic-center-anchor-bound/EXPECTED.json new file mode 100644 index 0000000000..d2e6db8d0e --- /dev/null +++ b/research/dyadic-center-anchor-bound/EXPECTED.json @@ -0,0 +1,591 @@ +{ + "assignment_seed": 33, + "base_commit": "47481c89fd30a43f8f882eb4b391e89c29273fd0", + "central_basis_column_direction_obligations": 3700, + "h26_admissible_anchors": 15276, + "h26_affine_rows_checked": 67600, + "h26_binary_anchors": 33554432, + "h26_complete_invoices": [ + { + "G": 10100, + "G_plus_H": 42600, + "H": 32500, + "central_signed_invocation": 85200, + "complete_signed_invocation": 781376, + "complete_three_stage_bound": 15846305280000, + "k": 0 + }, + { + "G": 12100, + "G_plus_H": 44324, + "H": 32224, + "central_signed_invocation": 88648, + "complete_signed_invocation": 784824, + "complete_three_stage_bound": 15916230720000, + "k": 1 + }, + { + "G": 14100, + "G_plus_H": 45381, + "H": 31281, + "central_signed_invocation": 90762, + "complete_signed_invocation": 786938, + "complete_three_stage_bound": 15959102640000, + "k": 2 + }, + { + "G": 16100, + "G_plus_H": 47381, + "H": 31281, + "central_signed_invocation": 94762, + "complete_signed_invocation": 790938, + "complete_three_stage_bound": 16040222640000, + "k": 3 + }, + { + "G": 18100, + "G_plus_H": 48994, + "H": 30894, + "central_signed_invocation": 97988, + "complete_signed_invocation": 794164, + "complete_three_stage_bound": 16105645920000, + "k": 4 + } + ], + "h26_minimum_G_plus_H": 42600, + "h26_orbits": [ + { + "G": 10100, + "G_plus_H": 42600, + "H": 32500, + "admissible": true, + "anchors": 1, + "k": 0, + "original_alphabet": true, + "pivot_numerators": { + "-1": 2300, + "2": 300 + } + }, + { + "G": 12100, + "G_plus_H": 44324, + "H": 32224, + "admissible": true, + "anchors": 25, + "k": 1, + "original_alphabet": true, + "pivot_numerators": { + "-1": 2024, + "0": 276, + "1": 276, + "2": 24 + } + }, + { + "G": 14100, + "G_plus_H": 45381, + "H": 31281, + "admissible": true, + "anchors": 300, + "k": 2, + "original_alphabet": true, + "pivot_numerators": { + "-1": 1771, + "0": 759, + "1": 69, + "2": 1 + } + }, + { + "G": 16100, + "G_plus_H": 47381, + "H": 31281, + "admissible": true, + "anchors": 2300, + "k": 3, + "original_alphabet": true, + "pivot_numerators": { + "-1": 1771, + "0": 759, + "1": 69, + "2": 1 + } + }, + { + "G": 18100, + "G_plus_H": 48994, + "H": 30894, + "admissible": true, + "anchors": 12650, + "k": 4, + "original_alphabet": false, + "pivot_numerators": { + "-1": 1414, + "-2": 210, + "0": 846, + "1": 126, + "2": 4 + } + }, + { + "G": 20100, + "G_plus_H": null, + "H": null, + "admissible": false, + "anchors": 53130, + "k": 5, + "original_alphabet": false, + "pivot_numerators": { + "-1": 1150, + "-2": 100, + "-3": 190, + "0": 950, + "1": 200, + "2": 10 + } + }, + { + "G": 22100, + "G_plus_H": null, + "H": null, + "admissible": false, + "anchors": 177100, + "k": 6, + "original_alphabet": false, + "pivot_numerators": { + "-1": 969, + "-2": 15, + "-3": 114, + "-4": 171, + "0": 1026, + "1": 285, + "2": 20 + } + }, + { + "G": 24100, + "G_plus_H": null, + "H": null, + "admissible": false, + "anchors": 480700, + "k": 7, + "original_alphabet": false, + "pivot_numerators": { + "-1": 816, + "-3": 21, + "-4": 126, + "-5": 153, + "0": 1071, + "1": 378, + "2": 35 + } + }, + { + "G": 26100, + "G_plus_H": null, + "H": null, + "admissible": false, + "anchors": 1081575, + "k": 8, + "original_alphabet": false, + "pivot_numerators": { + "-1": 680, + "-4": 28, + "-5": 136, + "-6": 136, + "0": 1088, + "1": 476, + "2": 56 + } + }, + { + "G": 28100, + "G_plus_H": null, + "H": null, + "admissible": false, + "anchors": 2042975, + "k": 9, + "original_alphabet": false, + "pivot_numerators": { + "-1": 560, + "-5": 36, + "-6": 144, + "-7": 120, + "0": 1080, + "1": 576, + "2": 84 + } + }, + { + "G": 30100, + "G_plus_H": null, + "H": null, + "admissible": false, + "anchors": 3268760, + "k": 10, + "original_alphabet": false, + "pivot_numerators": { + "-1": 455, + "-6": 45, + "-7": 150, + "-8": 105, + "0": 1050, + "1": 675, + "2": 120 + } + }, + { + "G": 32100, + "G_plus_H": null, + "H": null, + "admissible": false, + "anchors": 4457400, + "k": 11, + "original_alphabet": false, + "pivot_numerators": { + "-1": 364, + "-7": 55, + "-8": 154, + "-9": 91, + "0": 1001, + "1": 770, + "2": 165 + } + }, + { + "G": 34100, + "G_plus_H": null, + "H": null, + "admissible": false, + "anchors": 5200300, + "k": 12, + "original_alphabet": false, + "pivot_numerators": { + "-1": 286, + "-10": 78, + "-8": 66, + "-9": 156, + "0": 936, + "1": 858, + "2": 220 + } + }, + { + "G": 36100, + "G_plus_H": null, + "H": null, + "admissible": false, + "anchors": 5200300, + "k": 13, + "original_alphabet": false, + "pivot_numerators": { + "-1": 220, + "-10": 156, + "-11": 66, + "-9": 78, + "0": 858, + "1": 936, + "2": 286 + } + }, + { + "G": 38100, + "G_plus_H": null, + "H": null, + "admissible": false, + "anchors": 4457400, + "k": 14, + "original_alphabet": false, + "pivot_numerators": { + "-1": 165, + "-10": 91, + "-11": 154, + "-12": 55, + "0": 770, + "1": 1001, + "2": 364 + } + }, + { + "G": 40100, + "G_plus_H": null, + "H": null, + "admissible": false, + "anchors": 3268760, + "k": 15, + "original_alphabet": false, + "pivot_numerators": { + "-1": 120, + "-11": 105, + "-12": 150, + "-13": 45, + "0": 675, + "1": 1050, + "2": 455 + } + }, + { + "G": 42100, + "G_plus_H": null, + "H": null, + "admissible": false, + "anchors": 2042975, + "k": 16, + "original_alphabet": false, + "pivot_numerators": { + "-1": 84, + "-12": 120, + "-13": 144, + "-14": 36, + "0": 576, + "1": 1080, + "2": 560 + } + }, + { + "G": 44100, + "G_plus_H": null, + "H": null, + "admissible": false, + "anchors": 1081575, + "k": 17, + "original_alphabet": false, + "pivot_numerators": { + "-1": 56, + "-13": 136, + "-14": 136, + "-15": 28, + "0": 476, + "1": 1088, + "2": 680 + } + }, + { + "G": 46100, + "G_plus_H": null, + "H": null, + "admissible": false, + "anchors": 480700, + "k": 18, + "original_alphabet": false, + "pivot_numerators": { + "-1": 35, + "-14": 153, + "-15": 126, + "-16": 21, + "0": 378, + "1": 1071, + "2": 816 + } + }, + { + "G": 48100, + "G_plus_H": null, + "H": null, + "admissible": false, + "anchors": 177100, + "k": 19, + "original_alphabet": false, + "pivot_numerators": { + "-1": 20, + "-15": 171, + "-16": 114, + "-17": 15, + "0": 285, + "1": 1026, + "2": 969 + } + }, + { + "G": 50100, + "G_plus_H": null, + "H": null, + "admissible": false, + "anchors": 53130, + "k": 20, + "original_alphabet": false, + "pivot_numerators": { + "-1": 10, + "-16": 190, + "-17": 100, + "-18": 10, + "0": 200, + "1": 950, + "2": 1140 + } + }, + { + "G": 52100, + "G_plus_H": null, + "H": null, + "admissible": false, + "anchors": 12650, + "k": 21, + "original_alphabet": false, + "pivot_numerators": { + "-1": 4, + "-17": 210, + "-18": 84, + "-19": 6, + "0": 126, + "1": 840, + "2": 1330 + } + }, + { + "G": 54100, + "G_plus_H": null, + "H": null, + "admissible": false, + "anchors": 2300, + "k": 22, + "original_alphabet": false, + "pivot_numerators": { + "-1": 1, + "-18": 231, + "-19": 66, + "-20": 3, + "0": 66, + "1": 693, + "2": 1540 + } + }, + { + "G": 56100, + "G_plus_H": null, + "H": null, + "admissible": false, + "anchors": 300, + "k": 23, + "original_alphabet": false, + "pivot_numerators": { + "-19": 253, + "-20": 46, + "-21": 1, + "0": 23, + "1": 506, + "2": 1771 + } + }, + { + "G": 58100, + "G_plus_H": null, + "H": null, + "admissible": false, + "anchors": 25, + "k": 24, + "original_alphabet": false, + "pivot_numerators": { + "-20": 276, + "-21": 24, + "1": 276, + "2": 2024 + } + }, + { + "G": 60100, + "G_plus_H": null, + "H": null, + "admissible": false, + "anchors": 1, + "k": 25, + "original_alphabet": false, + "pivot_numerators": { + "-21": 300, + "2": 2300 + } + } + ], + "h26_original_alphabet_anchors": 2626, + "h26_pivot": 7, + "h26_unique_minimizer_k": 0, + "historical_invoice": { + "G": 14100, + "G_plus_H": 45381, + "H": 31281, + "central_signed_invocation": 90762, + "complete_signed_invocation": 786938, + "complete_three_stage_bound": 15959102640000 + }, + "historical_reference_rows": 2776, + "negative_controls": [ + "integral anchor -1", + "integral anchor 2", + "boolean anchor", + "five-anchor numerator -3", + "minus two excluded by original guard", + "missing conjugate scatter", + "missing constant gather", + "missing restore", + "missing compensate", + "missing deliver", + "incorrect polynomial coefficient", + "negative positivity witness", + "h8 refutes extending h>=10 optimum to h8", + "one gather/scatter pair undercharged" + ], + "positive_newton_coefficients": [ + [ + 20, + 19, + 7, + 1 + ], + [ + 5, + 21, + 11, + 2 + ], + [ + 53, + 48, + 19, + 3 + ], + [ + 122, + 72, + 24, + 4 + ] + ], + "small_complete_censuses": [ + { + "admissible_anchors": 99, + "affine_rows_checked": 7168, + "anchors_checked": 128, + "cost_histogram": { + "702": 21, + "713": 7, + "714": 1, + "716": 35, + "748": 35 + }, + "h": 8, + "minimizers": 21, + "minimum_G_plus_H": 702, + "original_alphabet_anchors": 64, + "pivot": 1 + }, + { + "admissible_anchors": 256, + "affine_rows_checked": 61440, + "anchors_checked": 512, + "cost_histogram": { + "1656": 1, + "1661": 36, + "1676": 9, + "1709": 84, + "1778": 126 + }, + "h": 10, + "minimizers": 1, + "minimum_G_plus_H": 1656, + "original_alphabet_anchors": 130, + "pivot": 3 + } + ], + "status": "SCOPED NEGATIVE RESULT; NO NEW KAPPA" +} diff --git a/research/dyadic-center-anchor-bound/OVERLAP.json b/research/dyadic-center-anchor-bound/OVERLAP.json new file mode 100644 index 0000000000..6d16756308 --- /dev/null +++ b/research/dyadic-center-anchor-bound/OVERLAP.json @@ -0,0 +1,102 @@ +{ + "checked_utc": "2026-10-13T14:12:00Z", + "upstream_main": "47481c89fd30a43f8f882eb4b391e89c29273fd0", + "open_pr_count": 717, + "max_open_pr_number": 946, + "pinned_sprint_issue": null, + "relevant_prs": [ + { + "headRefOid": "b6e22dbf548d72f18b722ccb6c2ea8e3d9df6ac1", + "number": 946, + "title": "Tooling: cross-platform byte/codec reproducibility of the make verify surface (no new kappa)", + "updatedAt": "2026-10-13T13:59:08Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/946" + }, + { + "headRefOid": "a3245bf22fa2a2eb778b11128cbc605b130d737f", + "number": 945, + "title": "Finite construction: joint Horner saves 13,072 PR799 backward primitives (no new kappa)", + "updatedAt": "2026-10-13T13:54:59Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/945" + }, + { + "headRefOid": "5dbcfbc63f646de5a1354f6b9760ec03837233f0", + "number": 944, + "title": "Research: classify signed 3x3 connector obstructions and a 14-query repair (no new kappa)", + "updatedAt": "2026-10-13T13:55:19Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/944" + }, + { + "headRefOid": "cf360b4b09b7d0419decdd6ac85421fefed55bdd", + "number": 943, + "title": "Research: sharp four/five-source dirty-connector boundary (no new kappa)", + "updatedAt": "2026-10-13T13:51:34Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/943" + }, + { + "headRefOid": "b303fed6dfe2066dcd78c0d8ed74d2a3b153ba72", + "number": 937, + "title": "Finite complex construction: two center shears save 5,562 primitives per invocation (no new kappa)", + "updatedAt": "2026-10-13T13:41:13Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/937" + }, + { + "headRefOid": "4e2925b076050f8035b054f95416029a63af64fa", + "number": 931, + "title": "Scoped negative result: bounded butterfly search misses the PR681 factory cost", + "updatedAt": "2026-10-13T13:13:07Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/931" + }, + { + "headRefOid": "d02d83332581f6a23616c1366c6b3901d42f4b06", + "number": 924, + "title": "Research: compose PR922 factory fusions with PR924 rescaling", + "updatedAt": "2026-10-13T13:29:56Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/924" + }, + { + "headRefOid": "efd5643c0016b6c6dac26e9ed7dee8a75295ff2a", + "number": 922, + "title": "Research: fuse complex factory to 32 operations (no new kappa)", + "updatedAt": "2026-10-13T12:44:22Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/922" + }, + { + "headRefOid": "e698981e0ffa680b6c5896dace1609025b97ad70", + "number": 882, + "title": "Research construction: seven grid-preserving JP8 circuits save 104 primitives per orientation (no new kappa)", + "updatedAt": "2026-10-13T10:40:17Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/882" + }, + { + "headRefOid": "6c0ed3975fda8f0190b34f1b1bbedb33a925d339", + "number": 863, + "title": "Research construction: a tied contraction saves 1,221 historical complex roles (no new kappa)", + "updatedAt": "2026-10-13T08:16:53Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/863" + }, + { + "headRefOid": "0a2977195efc8fb2a918fbfb694ec8d294387f08", + "number": 837, + "title": "Research: bidirectional Horner saves 312 SW4 primitives per orientation (no new kappa)", + "updatedAt": "2026-10-13T06:57:25Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/837" + }, + { + "headRefOid": "66cabb478385fbaa1a8060123cd57545d703d84e", + "number": 809, + "title": "Research circuit: lower historical dyadic center bill with one basis shear (no new kappa)", + "updatedAt": "2026-10-13T06:03:28Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/809" + } + ], + "distinction": "PR937 supplies the optimum construction; this package proves its exact optimality in the entire integral constant-row shear family. PR809 studies single shears including nonconstant-row mixing. No pending code or additive saving is imported.", + "publication_refresh": { + "checked_utc": "2026-10-13T14:16:18.246472+00:00", + "upstream_main": "007664306fff84fbb1c9a1b4053b69f439764034", + "selected_kappa": "0.001661957774647029", + "all_eight_pinned_inputs_unchanged": true, + "newest_other_open_pr": 946, + "result_pr": 947 + } +} diff --git a/research/dyadic-center-anchor-bound/README.md b/research/dyadic-center-anchor-bound/README.md new file mode 100644 index 0000000000..3c69d4ecf9 --- /dev/null +++ b/research/dyadic-center-anchor-bound/README.md @@ -0,0 +1,215 @@ +# Exact boundary for constant-row shears of the historical complex center + +**Scoped negative result; no new κ.** For every even h≥10, the factor exhibited +in [PR937](https://github.com/CrocSwap/integer-mult-bounds/pull/937) uniquely +minimizes the complete gather/scatter cost in the integer constant-row shear +family defined below, for a fixed pivot. This includes simultaneous shears of +arbitrary support. At h=26 its cost is **42,600**. Further improvement requires +leaving this family or changing its scalar pricing/alphabets. + +This is an algebraic classification and cost proof, accompanied by an exact +checker. It is not an unrestricted circuit optimum, a new construction, a new +κ, a measured runtime improvement, or a formal proof of integer multiplication. +PR937 already supplies the minimizing factor and its savings. The new result +closes the specified family beyond the one-step search in PR809 and the +second-step search in PR937. It does not reopen those searches with more trials. + +The starting base is `47481c89fd30a43f8f882eb4b391e89c29273fd0`. Its accepted +conditional saving is **0.001661957774647029**, PR890/U8-T21 with PR589/555. +The selected certificate, its actual T21 construction and maintainer review +were read; the historical center studied here is not that selected supplier. + +## Reproduce + +Python 3.11+ standard library, offline, from the repository root: + +```sh +python3 -I -B research/dyadic-center-anchor-bound/verify.py +``` + +Expected final line: + +```text +PASS_CENTER_ANCHOR_BOUND h=26 orbits=26 admissible=15276 optimum=42600 all_even_h_ge_10 controls=14 no_new_kappa +``` + +The same command works with `-O` and from another working directory. It does +not write files. `--write` regenerates only this package's `EXPECTED.json`. +`test_package.py` adds relocation, corruption and independent arithmetic tests. + +## Exact family and identity + +Let S,T range over the triples of h coordinates, fix a pivot p, and write s_i, +t_i for their indicators. Keep one constant gather row and all other rows in +the form + +``` +V[p,T] = 1, V[i,T] = t_i - b_i (i != p), +U[S,p] = (3-k)*s_p + |S∩B| - 1, +U[S,i] = s_i - s_p (i != p), +``` + +where B is the set of coordinates with b_i=1 and k=|B|. Before imposing the +gather alphabet, allow every integer b_i. Both t_i=0 and t_i=1 occur among +triples. Therefore the two values −b_i and 1−b_i both belong to {−1,0,1} +**if and only if b_i is 0 or 1**. This proves the reduction from an unbounded +integer domain to all binary anchors; it is not a finite search assumption. + +The repository's original factor is p=0, B={1,2}. Starting from it, every +matrix `A=I+sum(a_i E[i,p])`, with integral a_i and i≠p, gives exactly this +family: `b_i=b_i_original-a_i`, `V'=A V`, `U'=U A^-1`. +The off-diagonal part N has N²=0, so A^-1=I−N. A relabeling gives any pivot. +We change the factor tables; A is **not** an extra operation on dirty centers. +Mixing two nonconstant rows, rescaling rows, changing the constant row, +nonintegral coefficients, helpers, frames and cross-macro sharing are outside +this class. In particular PR809's `I-E[1,2]` move is outside the class itself. + +For the displayed factor, + +``` +(UV)[S,T] = 3*s_p - 1 + sum(i!=p, (s_i-s_p)*t_i) + = |S∩T| - 1, +``` + +because sum(t_i)=3. Thus the center still supplies (|S∩T|−1)/2. Its four +steps `y-=Uc/2; c+=Vx; y+=Uc/2; c-=Vx` add UVx/2 to y and restore every +arbitrary initial center c. Reversing the order and signs supplies the inverse. +The checker compares the affine coefficients modulo sum(t_i)=3, then separately +executes these literal steps on independent input columns at h=8 and h=10. + +## Admissibility is completely classified + +Use the signed scatter numerator alphabet {−2,−1,0,1,2}; numerator ±2 costs +one signed addition, and ±1 costs one halving and one addition. This is the +signed extension explicitly priced in PR809. The original repository validator +allows only {−1,0,1,2}; it is unchanged and is treated separately here. + +All nonpivot scatter entries are in {−1,0,1}. At the pivot, a triple with +s_p=0 and j coordinates in B has numerator j−1. A triple with s_p=1 has +numerator 2−k+j, where it contains two other coordinates. For k≤4 these are +all in the signed alphabet. For k≥5 the smallest achievable numerator is + +``` +2-k + max(0, 2-(h-1-k)) = max(2-k, 5-h) <= -3 (h>=8). +``` + +There are enough coordinates to realize that minimum. Hence exactly k=0,…,4 +are admissible. With the original narrower alphabet exactly k=0,…,3 are +admissible: k=4 realizes −2. Algebraically correct factors outside the alphabet +are rejected as **unpriced**, not called counterexamples to the factor identity. + +Permutations fixing p act transitively on anchors of each size, and preserve +the tables' cost. Thus all 2^(h−1) binary anchors reduce to h size orbits. +At h=26 this covers 33,554,432 anchors, of which 15,276 satisfy the signed +alphabet (2,626 satisfy the original alphabet). The minimum is unique for +each fixed pivot; there are h equivalent choices when the pivot may vary. + +## Exact cost proof for every even h≥10 + +Set n=C(h,3), d=C(h−1,2), e=C(h−2,2), and let c(0)=0, c(±1)=2, c(±2)=1. +Every gather read/addition and scatter operation is charged: + +``` +G_k = n + (h-1)*d + k*(n-2*d) +H_k = 4*(h-1)*e + + sum(s=0,1) sum(j=0,...,3-s) + C(k,j)*C(h-1-k,3-s-j)*c((3-k)*s+j-1). +``` + +A binomial coefficient outside its combinatorial range is zero. G follows +because an unshifted row has d nonzeros and a shifted row has n−d. Each +nonpivot scatter row has e entries of each sign, at cost two each. The final +sum counts every pivot numerator by its two independent subset choices. + +For D_k=(G_k+H_k)−(G_0+H_0), write x=h−10. Exact expansion gives + +| k | C(x,0) | C(x,1) | C(x,2) | C(x,3) | +|---|---:|---:|---:|---:| +| 1 | 20 | 19 | 7 | 1 | +| 2 | 5 | 21 | 11 | 2 | +| 3 | 53 | 48 | 19 | 3 | +| 4 | 122 | 72 | 24 | 4 | + +`CERTIFICATE.json` contains these coefficients. The checker constructs the +cost polynomials by rational polynomial multiplication, independently expands +the binomial basis, and compares **all polynomial coefficients**. It does not +infer an identity or a tail bound from numeric samples. For integer x≥0, +every C(x,j) is nonnegative and the constant coefficients above are positive. +Therefore D_k>0 for all four alternatives, proving the claimed unique optimum. + +At h=8 the five costs are 714, 713, **702**, 716 and 748. Size two is optimal, +with C(7,2)=21 anchors per fixed pivot. This supplies a concrete counterexample +to extending the size-zero claim to h=8; it is included as a positive control +for an adverse result, not described as a failed search. + +## Full accounting and what cannot follow + +For the historical side circuit, M=158,444, C=J=10,400 at h=26. The inherited +invoice is + +``` +signed invocation = 4*M + 2*C + 4*J + 2*G_k + 2*H_k +three-stage scalar bound = 3*n^2 * signed invocation. +``` + +The factors of two pay for both gathers, both scatters, compensation and +restoration. The complete side work is included. At h=26: + +| k | G | H | G+H | Complete signed invocation | +|---|---:|---:|---:|---:| +| 0 | 10,100 | 32,500 | **42,600** | **781,376** | +| 1 | 12,100 | 32,224 | 44,324 | 784,824 | +| 2 (original) | 14,100 | 31,281 | 45,381 | 786,938 | +| 3 | 16,100 | 31,281 | 47,381 | 790,938 | +| 4 (signed extension) | 18,100 | 30,894 | 48,994 | 794,164 | + +The minimum three-stage bound is 15,846,305,280,000, matching PR937. These +are corroborated predecessor savings, not savings newly claimed here. +The checker binds the original h=8/10/26 factors to the actual inherited +generator and the h=26 invoice to `certificates/dyadic-central-factor.json`. +All side constants and phase/recursive obligations are inherited rather than +freshly established by this package. No additional helper, runtime conversion, +source operation, copy or recursive child is introduced by the class proof. + +Retaining all grouped incidences, including zero coefficients, retains the +same h center roles and frame history. The historical W, m, s and paid rank +profile are unchanged. Thus even reaching the class optimum does not improve +the recursive exponent. No composition with PR863's different side-circuit +change, the selected U8 word, or other pending work is asserted. + +## Evidence, limits and attribution + +`EXPECTED.json` records complete all-anchor censuses at h=8 and h=10 (128 and +512 anchors), all 26 literal orbit representatives at h=26, 67,600 h=26 affine +row obligations, and 3,700 central input-column/direction obligations at the +two small sizes. Seed **33**, drawn from OS randomness, chooses pivots 1, 3 +and 7 for these finite diagnostics. The classification and proof cover every +pivot; the seed is not a coverage claim. There is no heuristic search, early +stopping or solver dependency. The experiment stops at the declared class. + +Fourteen controls distinguish wrong maps, unrestored dirty data, forbidden +alphabets, undercharged execution, invalid polynomial certificates and the +h=8 exception. There is no full-size side-circuit replay, new physical/global +admission, selected cold replay, Lean proof or remote CI result here. The +inherited all-size compiler, realization, whole-call hosting, precision/tape +and analytic obligations remain open. A finite replay is not a proof of the +whole multiplication theorem; the all-h family result rests on the written +classification and polynomial proof above. + +`CLAIM.json` records the three candidates, exact base, time budget, seed and +local coordination fallback. No pinned sprint issue was present. Source pins +are in `SOURCES.json`; all executable inputs are already on the starting base. +No pending code is imported. PR809 is pinned at +`66cabb478385fbaa1a8060123cd57545d703d84e`; PR937 at +`b303fed6dfe2066dcd78c0d8ed74d2a3b153ba72`. Their search domains and lack of a +general optimum claim were checked. The final overlap check and actual test +results are in `VALIDATION.md`. + +Credit **Douglas R. Colkitt** for the original factor, signed invocation and +complete invoice, **Curtis Dransfield** for PR809's basis-shear mechanism and +signed alphabet accounting, and **Ross Richardson's PR937** for the minimizing +factor and its complete saving. This contribution adds the exact family +boundary. Prepared by **Ross Richardson (@RossRichardson)** with substantial +**OpenAI Codex assistance** in research, implementation, proof writing and +verification. The checks are not independent human review. Apache-2.0; original +notices and `upstream/` are unchanged. diff --git a/research/dyadic-center-anchor-bound/SOURCES.json b/research/dyadic-center-anchor-bound/SOURCES.json new file mode 100644 index 0000000000..f322ad6f5a --- /dev/null +++ b/research/dyadic-center-anchor-bound/SOURCES.json @@ -0,0 +1,19 @@ +{ + "base_commit": "47481c89fd30a43f8f882eb4b391e89c29273fd0", + "historical_factor_commit": "d55bcd62ceb8f322bcf311a5a66e94c3ac7724f0", + "predecessors": { + "PR809": "66cabb478385fbaa1a8060123cd57545d703d84e", + "PR937": "b303fed6dfe2066dcd78c0d8ed74d2a3b153ba72" + }, + "pending_code_imported": false, + "sha256": { + "scripts/certify.py": "2348d95008276c5d5764f7e028c3918e484582cd589bd4d9b82919161745e53e", + "scripts/exclusion_circuit.py": "b253f9d7318becda1c1f3b24e2287ed44a9c27fcea00cf9d531afb950d0457a0", + "scripts/binary_phase_frames.py": "4148cfa313cf050ed25296e8db36d35871520b8318fd086c7d1facf0c6af67d7", + "scripts/experiments/disjoint_tensor.py": "102dd59bf96033f96ba0dab4c2aba77b3a7a73b67b0f96929ff8b20a98b91cd8", + "scripts/experiments/complex_centers.py": "3744396587d729253d80980f6310b56e7bf0ea21b165bd178d0d6d4c49faf2e2", + "certificates/dyadic-central-factor.json": "ffae0f0a22863718e3134a924592dcf4b05e919223323ba536c587c592bfe6a1", + "notes/dyadic-central-factor.tex": "24c0543fb2fd815f114021f929c3efefa1ae79f29c2f7968585bcd4595a96158", + "docs/research/dyadic-central-factor.md": "e97b1dfe11b5eaebacf3f910131e13bcad586ea5fc1af05db23c00ae0eea5c11" + } +} diff --git a/research/dyadic-center-anchor-bound/VALIDATION.md b/research/dyadic-center-anchor-bound/VALIDATION.md new file mode 100644 index 0000000000..c399e9c192 --- /dev/null +++ b/research/dyadic-center-anchor-bound/VALIDATION.md @@ -0,0 +1,67 @@ +# Executed validation and review boundary + +Base: `47481c89fd30a43f8f882eb4b391e89c29273fd0`. +Environment: macOS, CPython 3.14.6, standard library only. +Prepared by Ross Richardson with substantial OpenAI Codex assistance. + +The following commands passed on 2026-10-13 UTC (2026-10-14 Melbourne): + +```sh +python3 -I -B research/dyadic-center-anchor-bound/verify.py +python3 -I -O -B research/dyadic-center-anchor-bound/test_package.py +python3 -B -m unittest discover -s tests -p test_complex_centers.py +make selected-record-check +git diff --check +``` + +- Main replay: 26 h26 cardinality orbits covering 33,554,432 binary anchors + by the proved permutation symmetry; 15,276 admissible anchors; unique + fixed-pivot minimum 42,600 at k=0. This is not 33 million literal replays. +- Complete literal small censuses: all 128 h8 and 512 h10 anchors. In each + case, admissibility, numerator multiplicities, the affine map and actual + table costs agree with the orbit formulas. +- Four exact rational polynomial identities agree coefficient by coefficient. + Their nonnegative binomial-basis coefficients prove the all-h tail bound. + The h8 exception is retained and checked. +- Twenty literal central commutator replays: five admissible sizes, h8/h10, + both orientations. All 3,700 independent input-column/direction obligations + pass, including arbitrary dirty centers and targets. Executed operations + agree with the complete central invoice. Fourteen main controls pass. +- Nine package tests pass. They include 401,408 direct integer matrix-product + entries (a different finite check from the affine quotient), all 16,384 + integer offsets in {-1,0,1,2}^7 for the gather reduction, all 1,024 + pivot/anchor pairs at h8, polynomial checks, dimension/type corruption, + isolated optimized minimal relocation in a path with spaces, source and + polynomial corruption, and a boolean-versus-integer receipt mutation. + Failure cases preserve the existing receipt. No checker uses `assert` for + its mathematical acceptance decisions. +- Four existing complex-center tests pass. The selected-record integrity + check retains PR890's exact conditional κ and source/proof inventory. +- The original factor file's last change is + `d55bcd62ceb8f322bcf311a5a66e94c3ac7724f0`; its Git blob payload matches the + recorded SHA256. All eight inherited input files are hash-pinned. + +Only `research/dyadic-center-anchor-bound/` is added. No selected supplier, +production generator, `upstream/`, existing certificate or review ledger is +modified. The broad `make verify` regeneration suite and selected cold replay +were not run: this additive note changes none of their inputs. No full side +phase replay, selected global admission, Lean proof or remote CI pass is +claimed. The historical side invoice and recursive/physical obligations are +inherited explicitly, not re-certified by the local result. + +The complete overlap snapshot contained 717 open PRs through #946. Main +then advanced during publication to +`007664306fff84fbb1c9a1b4053b69f439764034`. A fresh fetch confirmed that all +eight mathematical inputs are byte-identical and PR890 remains selected at +0.001661957774647029. The branch retains its exact recorded starting base. +The immediately preceding submission check found no newer overlapping PR. PR809 and PR937 remain +at the pinned heads; the latter already owns the minimum construction and its +savings. This contribution supplies an all-even-h theorem for a defined +simultaneous-shear class, which neither predecessor claims. Other new PRs +concern coefficient schedules, connectors and reproducibility. There was no +pinned coordination issue, so the claim is local; `OVERLAP.json` records the +specific inspected heads. GitHub publication and any later CI are separate +from these local results. + +Published result: [PR947](https://github.com/CrocSwap/integer-mult-bounds/pull/947). +The local sprint claim was updated once with this result and link. diff --git a/research/dyadic-center-anchor-bound/anchor.py b/research/dyadic-center-anchor-bound/anchor.py new file mode 100644 index 0000000000..d396de8480 --- /dev/null +++ b/research/dyadic-center-anchor-bound/anchor.py @@ -0,0 +1,222 @@ +"""Exact constant-row shear family for the historical complex center. + +Apache-2.0. Ross Richardson, with substantial OpenAI Codex assistance. +The original factor and cost convention are Douglas R. Colkitt's work. +""" +from collections import Counter +from fractions import Fraction +from itertools import combinations +from math import comb + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def choose(n, k): + return comb(n, k) if 0 <= k <= n else 0 + + +def factor(h, pivot, anchor): + require(type(h) is int and h >= 8 and h % 2 == 0, "even h >= 8 required") + require(type(pivot) is int and 0 <= pivot < h, "invalid pivot") + require(all(type(i) is int and 0 <= i < h and i != pivot for i in anchor), + "invalid anchor coordinate") + require(len(set(anchor)) == len(anchor), "duplicate anchor coordinate") + b = set(anchor) + triples = list(combinations(range(h), 3)) + gather, scatter = [], [] + for triple in triples: + s = set(triple) + sp = int(pivot in s) + gather.append(tuple(1 if i == pivot else int(i in s) - int(i in b) + for i in range(h))) + scatter.append(tuple((3-len(b))*sp + len(s & b)-1 if i == pivot + else int(i in s)-sp for i in range(h))) + return {"h": h, "pivot": pivot, "anchor": sorted(b), "triples": triples, + "gather": gather, "scatter": scatter} + + +def classify_integral_anchor(h, pivot, offsets): + """V_i=t_i-b_i is in {0,+1,-1} for both t_i values iff b_i in {0,1}.""" + require(type(h) is int and h >= 8 and h % 2 == 0, "even h >= 8 required") + require(type(pivot) is int and 0 <= pivot < h, "invalid pivot") + require(len(offsets) == h and offsets[pivot] == 0, "invalid anchor shape") + require(all(type(b) is int for b in offsets), "integral anchor required") + require(all(b in (0, 1) for b in offsets), "gather alphabet exceeded") + return tuple(i for i, b in enumerate(offsets) if b) + + +def histograms(f): + return (Counter(x for row in f["gather"] for x in row), + Counter(x for row in f["scatter"] for x in row)) + + +def literal_price(f, original_alphabet=False): + v, u = histograms(f) + require(set(v) <= {-1, 0, 1}, "gather alphabet exceeded") + allowed = {-1, 0, 1, 2} if original_alphabet else {-2, -1, 0, 1, 2} + require(set(u) <= allowed, "scatter alphabet exceeded") + return {"G": v[-1]+v[1], "H": 2*(u[-1]+u[1])+u[-2]+u[2]} + + +def orbit(h, k): + """Exact subset-count formula; never price an out-of-alphabet numerator.""" + require(type(h) is int and h >= 8 and h % 2 == 0, "even h >= 8 required") + require(type(k) is int and 0 <= k < h, "invalid anchor cardinality") + u0 = Counter() + for sp in (0, 1): + for j in range(4-sp): + multiplicity = choose(k, j)*choose(h-1-k, 3-sp-j) + if multiplicity: + u0[(3-k)*sp+j-1] += multiplicity + n, d, e = choose(h, 3), choose(h-1, 2), choose(h-2, 2) + require(sum(u0.values()) == n, "orbit multiplicity incomplete") + g = n+(h-1)*d+k*(n-2*d) + admissible = set(u0) <= {-2, -1, 0, 1, 2} + hp = None + if admissible: + hp = 4*(h-1)*e + sum(m*(0 if w == 0 else 1 if abs(w) == 2 else 2) + for w, m in u0.items()) + return {"k": k, "anchors": choose(h-1, k), "G": g, "H": hp, + "G_plus_H": g+hp if hp is not None else None, + "admissible": admissible, "original_alphabet": set(u0) <= {-1, 0, 1, 2}, + "pivot_numerators": {str(w): m for w, m in sorted(u0.items())}} + + +def affine_identity(f): + """Check U V = intersection-1 modulo sum(t_i)=3, as affine forms. + + This checks coefficients, not sampled triple pairs. The written proof + explains why the one relation suffices for every triple input. + """ + h, p, b = f["h"], f["pivot"], set(f["anchor"]) + triples = list(combinations(range(h), 3)) + require(f["triples"] == triples and len(f["gather"]) == len(f["scatter"]) == len(triples), + "incomplete factor dimensions") + require(all(len(row) == h and all(type(a) is int for a in row) + for rows in (f["gather"], f["scatter"]) for row in rows), + "invalid factor row") + for triple, u in zip(f["triples"], f["scatter"]): + s = set(triple) + constant = u[p]-sum(u[i] for i in b) + coefficients = [0 if i == p else u[i] for i in range(h)] + delta = [coefficients[i]-int(i in s) for i in range(h)] + require(len(set(delta)) == 1 and constant+1 == -3*delta[0], + "central affine identity failed") + # Bind the actually supplied V to the affine forms used above. + for triple, v in zip(f["triples"], f["gather"]): + require(v == tuple(1 if i == p else int(i in triple)-int(i in b) + for i in range(h)), "gather form mismatch") + return len(f["triples"]) + + +def central_replay(f, inverse=False, omit=None, billed=None): + """Literal exact replay on independent source, target and dirty-center rows.""" + n, h = len(f["triples"]), f["h"] + x = [{i: Fraction(1)} for i in range(n)] + y = [{n+i: Fraction(1)} for i in range(n)] + c = [{2*n+i: Fraction(1)} for i in range(h)] + paid = 0 + + def add(target, source, scale): + for i, a in source.items(): + target[i] = target.get(i, 0)+scale*a + if not target[i]: + del target[i] + + def gather(sign): + nonlocal paid + for i, row in enumerate(f["gather"]): + for j, a in enumerate(row): + if a: + require(abs(a) == 1, "unpriced gather coefficient") + paid += 1 + add(c[j], x[i], sign*a) + + def scatter(sign): + nonlocal paid + for i, row in enumerate(f["scatter"]): + for j, a in enumerate(row): + if a: + require(abs(a) in (1, 2), "unpriced scatter coefficient") + paid += 2 if abs(a) == 1 else 1 + add(y[i], c[j], Fraction(sign*a, 2)) + + ops = [("compensate", scatter, -1), ("prepare", gather, 1), + ("deliver", scatter, 1), ("restore", gather, -1)] + if inverse: + ops = [(name, op, -sign) for name, op, sign in reversed(ops)] + for name, op, sign in ops: + if name != omit: + op(sign) + require(c == [{2*n+i: Fraction(1)} for i in range(h)], "dirty centers not restored") + sign = -1 if inverse else 1 + sets = [set(t) for t in f["triples"]] + for i, s in enumerate(sets): + expected = {n+i: Fraction(1)} + for j, t in enumerate(sets): + value = Fraction(sign*(len(s & t)-1), 2) + if value: + expected[j] = value + require(y[i] == expected, "dirty target shear failed") + if billed is not None: + require(type(billed) is int and paid == billed, "executed central bill mismatch") + return {"input_columns": 2*n+h, "executed_central_primitives": paid} + + +# Polynomials are coefficient tuples in x=h-10, using exact rationals. +def padd(a, b): + return tuple((a[i] if i < len(a) else 0)+(b[i] if i < len(b) else 0) + for i in range(max(len(a), len(b)))) + + +def pscale(a, scale): + return tuple(scale*x for x in a) + + +def pmul(a, b): + out = [Fraction(0)]*(len(a)+len(b)-1) + for i, x in enumerate(a): + for j, y in enumerate(b): + out[i+j] += x*y + return tuple(out) + + +def pchoose(offset, k): + """Polynomial binom(x+offset,k), for fixed nonnegative k.""" + out = (Fraction(1),) + for j in range(k): + out = pscale(pmul(out, (offset-j, 1)), Fraction(1, j+1)) + return out + + +def difference_polynomial(k): + # Terms common to every anchor cancel. Remaining gather difference: + out = pscale(padd(pchoose(10, 3), pscale(pchoose(9, 2), -2)), k) + for size, sign in ((k, 1), (0, -1)): + for sp in (0, 1): + for j in range(4-sp): + multiplicity = choose(size, j) + if not multiplicity: + continue + weight = (3-size)*sp+j-1 + require(abs(weight) <= 2, "polynomial outside priced alphabet") + price = 0 if weight == 0 else 1 if abs(weight) == 2 else 2 + term = pscale(pchoose(9-size, 3-sp-j), sign*price*multiplicity) + out = padd(out, term) + return out + + +def check_positive_certificate(rows): + require(type(rows) is list and len(rows) == 4, "four polynomial certificates required") + for k, row in enumerate(rows, 1): + require(type(row) is list and len(row) == 4 and all(type(a) is int for a in row), + "invalid polynomial certificate") + require(row[0] > 0 and all(a >= 0 for a in row), "nonpositive certificate") + reconstructed = (Fraction(0),)*4 + for j, a in enumerate(row): + reconstructed = padd(reconstructed, pscale(pchoose(0, j), a)) + require(reconstructed == difference_polynomial(k), "polynomial identity failed") + return True diff --git a/research/dyadic-center-anchor-bound/test_package.py b/research/dyadic-center-anchor-bound/test_package.py new file mode 100644 index 0000000000..5caa7721d0 --- /dev/null +++ b/research/dyadic-center-anchor-bound/test_package.py @@ -0,0 +1,156 @@ +#!/usr/bin/env python3 +"""Independent finite arithmetic and portable-package failure controls. + +Apache-2.0. Ross Richardson, with substantial OpenAI Codex assistance. +Both implementations are AI-assisted, not independent human reviews. +""" +import importlib.util +from copy import deepcopy +from itertools import product +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +spec = importlib.util.spec_from_file_location("anchor_for_tests", HERE / "anchor.py") +anchor = importlib.util.module_from_spec(spec) +spec.loader.exec_module(anchor) + + +class AnchorTests(unittest.TestCase): + def test_independent_literal_matrix_products(self): + # Direct dot products use neither the affine quotient checker nor + # the orbit-count formula. Cover all 128 anchors at h8, including + # mathematically valid factors outside the priced alphabet. + for bits in range(128): + b = [i+1 for i in range(7) if bits & (1 << i)] + f = anchor.factor(8, 0, b) + masks = [sum(1 << i for i in t) for t in f["triples"]] + for sm, u in zip(masks, f["scatter"]): + for tm, v in zip(masks, f["gather"]): + self.assertEqual(sum(a*b for a, b in zip(u, v)), (sm & tm).bit_count()-1) + + def test_integer_domain_reduction(self): + # Independent two-value gather test, including negative/large offsets. + accepted = 0 + for vector in product((-1, 0, 1, 2), repeat=7): + direct = all(-b in (-1, 0, 1) and 1-b in (-1, 0, 1) for b in vector) + try: + selected = anchor.classify_integral_anchor(8, 0, [0, *vector]) + except ValueError: + self.assertFalse(direct) + else: + self.assertTrue(direct) + self.assertEqual(selected, tuple(i+1 for i, b in enumerate(vector) if b)) + accepted += 1 + self.assertEqual(accepted, 128) + + def test_every_pivot_and_anchor_at_h8(self): + for pivot in range(8): + coordinates = [i for i in range(8) if i != pivot] + for bits in range(128): + b = [i for j, i in enumerate(coordinates) if bits & (1 << j)] + f = anchor.factor(8, pivot, b) + maximum = max(abs(x) for row in f["scatter"] for x in row) + self.assertEqual(maximum <= 2, len(b) <= 4) + self.assertEqual(anchor.affine_identity(f), 56) + if len(b) <= 4: + cost = anchor.literal_price(f) + self.assertEqual(cost["G"]+cost["H"], (714, 713, 702, 716, 748)[len(b)]) + + def test_all_h_polynomial_certificate(self): + rows = json.loads((HERE / "CERTIFICATE.json").read_text())["positive_newton_coefficients"] + self.assertTrue(anchor.check_positive_certificate(rows)) + # Supplemental checks of the independently counted subset formula. + # These samples do not replace the polynomial identity or positivity proof. + for h in range(10, 102, 2): + for k, row in enumerate(rows, 1): + expected = sum(a*anchor.choose(h-10, j) for j, a in enumerate(row)) + self.assertEqual(anchor.orbit(h, k)["G_plus_H"]-anchor.orbit(h, 0)["G_plus_H"], + expected) + self.assertGreater(expected, 0) + + def test_corrupt_factor_dimensions_and_types(self): + good = anchor.factor(8, 0, []) + for key in ("gather", "scatter", "triples"): + bad = deepcopy(good) + bad[key].pop() + with self.assertRaisesRegex(ValueError, "incomplete factor dimensions"): + anchor.affine_identity(bad) + bad = deepcopy(good) + bad["scatter"][0] = tuple(True if i == 0 else a for i, a in enumerate(bad["scatter"][0])) + with self.assertRaisesRegex(ValueError, "invalid factor row"): + anchor.affine_identity(bad) + + def relocate(self, directory): + root = Path(directory) / "minimal tree with spaces" + target = root / "research/dyadic-center-anchor-bound" + target.mkdir(parents=True) + for name in ("verify.py", "anchor.py", "SOURCES.json", "CERTIFICATE.json", "EXPECTED.json"): + shutil.copy2(HERE / name, target / name) + pins = json.loads((HERE / "SOURCES.json").read_text()) + for name in pins["sha256"]: + destination = root / name + destination.parent.mkdir(parents=True, exist_ok=True) + shutil.copy2(ROOT / name, destination) + return root, target + + def execute(self, target): + return subprocess.run([sys.executable, "-I", "-O", "-B", str(target / "verify.py")], + cwd=target.parents[1], capture_output=True, text=True, timeout=120) + + def test_optimized_minimal_relocation(self): + with tempfile.TemporaryDirectory(prefix="center-anchor-") as directory: + _, target = self.relocate(directory) + before = (target / "EXPECTED.json").read_bytes() + result = self.execute(target) + self.assertEqual(result.returncode, 0, result.stdout+result.stderr) + self.assertIn("PASS_CENTER_ANCHOR_BOUND", result.stdout) + self.assertEqual((target / "EXPECTED.json").read_bytes(), before) + + def test_source_corruption_rejected_without_overwrite(self): + with tempfile.TemporaryDirectory(prefix="center-anchor-") as directory: + root, target = self.relocate(directory) + source = root / "scripts/experiments/complex_centers.py" + source.write_text(source.read_text()+"\n# altered input\n") + before = (target / "EXPECTED.json").read_bytes() + result = self.execute(target) + self.assertNotEqual(result.returncode, 0) + self.assertIn("source hash mismatch", result.stderr) + self.assertEqual((target / "EXPECTED.json").read_bytes(), before) + + def test_polynomial_corruption_rejected_without_overwrite(self): + with tempfile.TemporaryDirectory(prefix="center-anchor-") as directory: + _, target = self.relocate(directory) + path = target / "CERTIFICATE.json" + certificate = json.loads(path.read_text()) + certificate["positive_newton_coefficients"][0][0] = 21 + path.write_text(json.dumps(certificate)) + before = (target / "EXPECTED.json").read_bytes() + result = self.execute(target) + self.assertNotEqual(result.returncode, 0) + self.assertIn("polynomial identity failed", result.stderr) + self.assertEqual((target / "EXPECTED.json").read_bytes(), before) + + def test_typed_receipt_corruption_rejected_without_overwrite(self): + with tempfile.TemporaryDirectory(prefix="center-anchor-") as directory: + _, target = self.relocate(directory) + path = target / "EXPECTED.json" + receipt = json.loads(path.read_text()) + # False == 0 in Python; canonical JSON comparison must reject it. + receipt["h26_unique_minimizer_k"] = False + path.write_text(json.dumps(receipt)) + before = path.read_bytes() + result = self.execute(target) + self.assertNotEqual(result.returncode, 0) + self.assertIn("expected receipt mismatch", result.stderr) + self.assertEqual(path.read_bytes(), before) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/dyadic-center-anchor-bound/verify.py b/research/dyadic-center-anchor-bound/verify.py new file mode 100644 index 0000000000..3f0de9063f --- /dev/null +++ b/research/dyadic-center-anchor-bound/verify.py @@ -0,0 +1,250 @@ +#!/usr/bin/env python3 +"""Offline exact replay of the constant-row shear classification and cost bound. + +Apache-2.0. Ross Richardson, with substantial OpenAI Codex assistance. +""" +import argparse +from collections import Counter +from copy import deepcopy +from hashlib import sha256 +import importlib.util +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +spec = importlib.util.spec_from_file_location("center_anchor_math", HERE / "anchor.py") +math = importlib.util.module_from_spec(spec) +spec.loader.exec_module(math) +require = math.require +SEED = 33 +SOURCE_PATHS = ( + "scripts/certify.py", "scripts/exclusion_circuit.py", "scripts/binary_phase_frames.py", + "scripts/experiments/disjoint_tensor.py", "scripts/experiments/complex_centers.py", + "certificates/dyadic-central-factor.json", "notes/dyadic-central-factor.tex", + "docs/research/dyadic-central-factor.md", +) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")) + + +def load_json(path): + def unique(pairs): + result = {} + for key, value in pairs: + require(key not in result, "duplicate JSON key") + result[key] = value + return result + return json.loads(path.read_text(), object_pairs_hook=unique) + + +def verify_sources(): + pins = load_json(HERE / "SOURCES.json") + require(pins["base_commit"] == "47481c89fd30a43f8f882eb4b391e89c29273fd0", + "wrong base commit") + require(set(pins["sha256"]) == set(SOURCE_PATHS), "source coverage mismatch") + for path in SOURCE_PATHS: + require(sha256((ROOT / path).read_bytes()).hexdigest() == pins["sha256"][path], + "source hash mismatch: " + path) + return pins + + +def reject(call, reason): + try: + call() + except ValueError as exc: + require(reason in str(exc), "control failed for wrong reason: " + str(exc)) + else: + raise ValueError("negative control accepted: " + reason) + + +def validate_factor(f, row): + require(math.affine_identity(f) == len(f["triples"]), "incomplete affine coverage") + v, u = math.histograms(f) + actual_pivot = Counter(r[f["pivot"]] for r in f["scatter"]) + require({str(w): m for w, m in sorted(actual_pivot.items())} == row["pivot_numerators"], + "pivot numerator histogram mismatch") + require(v[-1]+v[1] == row["G"], "gather price mismatch") + require((set(u) <= {-2, -1, 0, 1, 2}) == row["admissible"], "admissibility mismatch") + if row["admissible"]: + require(math.literal_price(f) == {"G": row["G"], "H": row["H"]}, + "literal cost mismatch") + else: + reject(lambda: math.literal_price(f), "scatter alphabet exceeded") + + +def small_census(h): + pivot = SEED % h + coordinates = [i for i in range(h) if i != pivot] + rows = [math.orbit(h, k) for k in range(h)] + seen = Counter() + costs = Counter() + admissible = original = affine_rows = 0 + for bits in range(1 << (h-1)): + b = [i for j, i in enumerate(coordinates) if bits & (1 << j)] + f = math.factor(h, pivot, b) + row = rows[len(b)] + validate_factor(f, row) + affine_rows += len(f["triples"]) + seen[len(b)] += 1 + admissible += int(row["admissible"]) + original += int(row["original_alphabet"]) + if row["admissible"]: + costs[row["G_plus_H"]] += 1 + require(all(seen[k] == math.choose(h-1, k) for k in range(h)), + "incomplete anchor coverage") + return {"h": h, "pivot": pivot, "anchors_checked": sum(seen.values()), + "admissible_anchors": admissible, "original_alphabet_anchors": original, + "affine_rows_checked": affine_rows, "minimum_G_plus_H": min(costs), + "minimizers": costs[min(costs)], + "cost_histogram": {str(c): n for c, n in sorted(costs.items())}} + + +def invoice(g, h, historical): + s = historical["scalar_charge"] + n = historical["counts"]["v"] + invocation = 4*s["M"]+2*s["C"]+4*s["J"]+2*g+2*h + return {"G": g, "H": h, "G_plus_H": g+h, + "central_signed_invocation": 2*(g+h), + "complete_signed_invocation": invocation, + "complete_three_stage_bound": 3*n*n*invocation} + + +def run(): + pins = verify_sources() + certificate = load_json(HERE / "CERTIFICATE.json") + math.check_positive_certificate(certificate["positive_newton_coefficients"]) + + # Exact binding to the inherited executable factor, not just its prose. + sys.path.insert(0, str(ROOT / "scripts")) + from experiments.complex_centers import factor as reference_factor + reference_rows = 0 + for h in (8, 10, 26): + reference = reference_factor(h) + ours = math.factor(h, 0, (1, 2)) + dense_gather = [tuple(dict(v).get(i, 0) for i in range(h)) + for v in reference["gather"]] + require(reference["triples"] == ours["triples"] and + reference["scatter"] == ours["scatter"] and dense_gather == ours["gather"], + "historical factor mismatch") + reference_rows += len(ours["triples"]) + + small = [small_census(h) for h in (8, 10)] + pivot = SEED % 26 + coordinates = [i for i in range(26) if i != pivot] + orbits = [] + affine_rows = 0 + for k in range(26): + row = math.orbit(26, k) + f = math.factor(26, pivot, coordinates[:k]) + validate_factor(f, row) + affine_rows += len(f["triples"]) + require(row["admissible"] == (k <= 4), "signed alphabet classification failed") + require(row["original_alphabet"] == (k <= 3), "original alphabet classification failed") + orbits.append(row) + require(sum(r["anchors"] for r in orbits) == 2**25, "incomplete h26 orbit coverage") + allowed = [r for r in orbits if r["admissible"]] + minimum = min(r["G_plus_H"] for r in allowed) + require([r["k"] for r in allowed if r["G_plus_H"] == minimum] == [0], + "h26 minimizer mismatch") + + # Literal four-step commutator, all independent inputs, both signs. + replay_columns = 0 + for h in (8, 10): + p = SEED % h + coordinates = [i for i in range(h) if i != p] + for k in range(5): + for inverse in (False, True): + counted = math.orbit(h, k) + replay = math.central_replay(math.factor(h, p, coordinates[:k]), inverse, + billed=2*counted["G_plus_H"]) + replay_columns += replay["input_columns"] + + historical = load_json(ROOT / "certificates/dyadic-central-factor.json") + old = math.literal_price(math.factor(26, 0, (1, 2))) + require(old["G"] == historical["central_factor"]["gather_steps"] and + old["H"] == historical["central_factor"]["scatter_steps"], + "historical invoice mismatch") + old_bill = invoice(old["G"], old["H"], historical) + require(old_bill["complete_three_stage_bound"] == historical["scalar_charge"]["steps"], + "complete historical scalar charge mismatch") + invoices = [dict(k=r["k"], **invoice(r["G"], r["H"], historical)) for r in allowed] + + controls = [] + for bad in (-1, 2): + offsets = [0]*26 + offsets[0] = bad + reject(lambda: math.classify_integral_anchor(26, pivot, offsets), "gather alphabet exceeded") + controls.append("integral anchor " + str(bad)) + offsets = [0]*26 + offsets[0] = True + reject(lambda: math.classify_integral_anchor(26, pivot, offsets), "integral anchor required") + controls.append("boolean anchor") + reject(lambda: math.literal_price(math.factor(26, pivot, [0, 1, 2, 3, 4])), + "scatter alphabet exceeded") + controls.append("five-anchor numerator -3") + reject(lambda: math.literal_price(math.factor(8, 1, [0, 2, 3, 4]), original_alphabet=True), + "scatter alphabet exceeded") + controls.append("minus two excluded by original guard") + f = math.factor(8, 1, []) + bad = deepcopy(f) + bad["scatter"][0] = tuple(0 for _ in range(8)) + reject(lambda: math.affine_identity(bad), "central affine identity failed") + controls.append("missing conjugate scatter") + bad = deepcopy(f) + bad["gather"][0] = tuple(0 for _ in range(8)) + reject(lambda: math.affine_identity(bad), "gather form mismatch") + controls.append("missing constant gather") + for name, message in (("restore", "dirty centers not restored"), + ("compensate", "dirty target shear failed"), + ("deliver", "dirty target shear failed")): + reject(lambda: math.central_replay(f, omit=name), message) + controls.append("missing " + name) + bad = deepcopy(certificate["positive_newton_coefficients"]) + bad[1][0] += 1 + reject(lambda: math.check_positive_certificate(bad), "polynomial identity failed") + controls.append("incorrect polynomial coefficient") + bad[0][0] = -1 + reject(lambda: math.check_positive_certificate(bad), "nonpositive certificate") + controls.append("negative positivity witness") + # The threshold and cleanup controls are comparisons against exact prices. + require(small[0]["minimum_G_plus_H"] == 702 < math.orbit(8, 0)["G_plus_H"], + "h8 counterexample lost") + controls.append("h8 refutes extending h>=10 optimum to h8") + reject(lambda: math.central_replay(f, billed=math.orbit(8, 0)["G_plus_H"]), + "executed central bill mismatch") + controls.append("one gather/scatter pair undercharged") + + return {"status": "SCOPED NEGATIVE RESULT; NO NEW KAPPA", "assignment_seed": SEED, + "base_commit": pins["base_commit"], "h26_pivot": pivot, + "h26_binary_anchors": 2**25, + "h26_admissible_anchors": sum(r["anchors"] for r in allowed), + "h26_original_alphabet_anchors": sum(r["anchors"] for r in orbits if r["original_alphabet"]), + "h26_minimum_G_plus_H": minimum, "h26_unique_minimizer_k": 0, + "h26_orbits": orbits, "h26_affine_rows_checked": affine_rows, + "small_complete_censuses": small, "historical_reference_rows": reference_rows, + "central_basis_column_direction_obligations": replay_columns, + "positive_newton_coefficients": certificate["positive_newton_coefficients"], + "historical_invoice": old_bill, "h26_complete_invoices": invoices, + "negative_controls": controls} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", action="store_true", help="regenerate only this package's EXPECTED.json") + args = parser.parse_args() + result = run() + if args.write: + (HERE / "EXPECTED.json").write_text(json.dumps(result, indent=2, sort_keys=True)+"\n") + else: + require(canonical(result) == canonical(load_json(HERE / "EXPECTED.json")), + "expected receipt mismatch") + print("PASS_CENTER_ANCHOR_BOUND h=26 orbits=26 admissible=15276 optimum=42600 " + "all_even_h_ge_10 controls=14 no_new_kappa") + + +if __name__ == "__main__": + main()