diff --git a/research/polar-law-small-t-screen/CERTIFICATE.json b/research/polar-law-small-t-screen/CERTIFICATE.json new file mode 100644 index 0000000000..0b5a0b9e35 --- /dev/null +++ b/research/polar-law-small-t-screen/CERTIFICATE.json @@ -0,0 +1,539 @@ +{ + "any_gain_found": false, + "basis_pivots": { + "B6_pivot": { + "bases_tried": 120, + "basis": [ + 12, + 28, + 32, + 20, + 3, + 25 + ], + "cost": 36, + "min_cost_minus_v": 0 + }, + "D6_pivot": { + "bases_tried": 120, + "basis": [ + 11, + 14, + 5, + 18, + 9, + 13 + ], + "cost": 30, + "min_cost_minus_v": 0 + }, + "E6_pivot": { + "bases_tried": 121, + "basis": [ + 16, + 7, + 19, + 20, + 29, + 25 + ], + "cost": 36, + "min_cost_minus_v": 0 + }, + "pm1T4_pivot": { + "bases_tried": 120, + "basis": [ + 31, + 13, + 26, + 28 + ], + "cost": 81, + "min_cost_minus_v": 41 + }, + "pm1T5_pivot": { + "bases_tried": 120, + "basis": [ + 118, + 109, + 15, + 14, + 41 + ], + "cost": 319, + "min_cost_minus_v": 198 + } + }, + "bounded": { + "A6_greedy": { + "greedy": { + "cost": 4, + "mask": 1048640, + "min_cost_minus_v": 2, + "v": 2 + }, + "random": { + "cost": 4, + "mask": 16640, + "min_cost_minus_v": 2, + "v": 2 + } + }, + "B6_greedy": { + "greedy": { + "cost": 12, + "mask": 64424572800, + "min_cost_minus_v": 0, + "v": 12 + }, + "random": { + "cost": 36, + "mask": 68719476735, + "min_cost_minus_v": 0, + "v": 36 + } + }, + "D6_greedy": { + "greedy": { + "cost": 20, + "mask": 255851535, + "min_cost_minus_v": 0, + "v": 20 + }, + "random": { + "cost": 30, + "mask": 1073741823, + "min_cost_minus_v": 0, + "v": 30 + } + }, + "E6_greedy": { + "greedy": { + "cost": 36, + "mask": 68719476735, + "min_cost_minus_v": 0, + "v": 36 + }, + "random": { + "cost": 36, + "mask": 68719476735, + "min_cost_minus_v": 0, + "v": 36 + } + }, + "pm1T4_greedy": { + "greedy": { + "cost": 14, + "mask": 174039793991, + "min_cost_minus_v": 0, + "v": 14 + }, + "random": { + "cost": 3, + "mask": 2415919104, + "min_cost_minus_v": 1, + "v": 2 + } + }, + "pm1T5_greedy": { + "greedy": { + "cost": 27, + "mask": 5192378872062439509191647649890305, + "min_cost_minus_v": 14, + "v": 13 + }, + "random": { + "cost": 12, + "mask": 19807040628566154767130167298, + "min_cost_minus_v": 8, + "v": 4 + } + }, + "pm1T6_greedy": { + "greedy": { + "cost": 23, + "mask": 14091273712067035392852765436994749862153990435480400354413793698201747017637192375589951440301712677971951616, + "min_cost_minus_v": 11, + "v": 12 + }, + "random": { + "cost": 12, + "mask": 14474011181624471095097012920753003568678378756842214965251702345049980272640, + "min_cost_minus_v": 8, + "v": 4 + } + } + }, + "control_failures": [], + "controls": { + "A4": { + "block_ranks": [ + 4, + 4, + 4, + 4 + ], + "cost": 16, + "v": 10 + }, + "A5": { + "block_ranks": [ + 5, + 5, + 5, + 5, + 5 + ], + "cost": 25, + "v": 15 + }, + "A6": { + "block_ranks": [ + 6, + 6, + 6, + 6, + 6, + 6 + ], + "cost": 36, + "v": 21 + }, + "D4": { + "block_ranks": [ + 3, + 3, + 3, + 3 + ], + "cost": 12, + "v": 12 + }, + "D5": { + "block_ranks": [ + 4, + 4, + 4, + 4, + 4 + ], + "cost": 20, + "v": 20 + }, + "D6": { + "block_ranks": [ + 5, + 5, + 5, + 5, + 5, + 5 + ], + "cost": 30, + "v": 30 + }, + "E6": { + "block_ranks": [ + 6, + 6, + 6, + 6, + 6, + 6 + ], + "cost": 36, + "v": 36 + }, + "E6_firstB0": { + "block_ranks": [ + 6, + 7, + 6, + 6, + 6, + 6 + ], + "cost": 37, + "v": 36 + }, + "E6_storedB0": { + "block_ranks": [ + 6, + 6, + 6, + 6, + 6, + 6 + ], + "cost": 36, + "v": 36 + }, + "E7": { + "block_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "cost": 49, + "v": 63 + }, + "E8": { + "block_ranks": [ + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9 + ], + "cost": 72, + "v": 120 + }, + "F4": { + "block_ranks": [ + 9, + 9, + 9, + 9 + ], + "cost": 36, + "v": 24 + } + }, + "exhaustive": [ + { + "best_cost": 1, + "best_mask": 16, + "best_v": 1, + "gain_count": 0, + "gains": [], + "label": "T3_pm1_all_subsets", + "lines": 13, + "min_cost_minus_v": 0, + "subsets_checked": 8191, + "tie_count": 63 + }, + { + "best_cost": 2, + "best_mask": 3, + "best_v": 2, + "gain_count": 0, + "gains": [], + "label": "D4_all_subsets", + "lines": 12, + "min_cost_minus_v": 0, + "subsets_checked": 4095, + "tie_count": 63 + }, + { + "best_cost": 2, + "best_mask": 3, + "best_v": 2, + "gain_count": 0, + "gains": [], + "label": "D5_all_subsets", + "lines": 20, + "min_cost_minus_v": 0, + "subsets_checked": 1048575, + "tie_count": 1023 + } + ], + "full_configs": { + "A4": { + "T": 5, + "block_ranks": [ + 4, + 4, + 4, + 4, + 4 + ], + "cost": 20, + "cost_minus_v": 10, + "v": 10 + }, + "A5": { + "T": 6, + "block_ranks": [ + 5, + 5, + 5, + 5, + 5, + 5 + ], + "cost": 30, + "cost_minus_v": 15, + "v": 15 + }, + "A6": { + "T": 7, + "block_ranks": [ + 6, + 6, + 6, + 6, + 6, + 6, + 6 + ], + "cost": 42, + "cost_minus_v": 21, + "v": 21 + }, + "B5": { + "T": 5, + "block_ranks": [ + 5, + 5, + 5, + 5, + 5 + ], + "cost": 25, + "cost_minus_v": 0, + "v": 25 + }, + "B6": { + "T": 6, + "block_ranks": [ + 6, + 6, + 6, + 6, + 6, + 6 + ], + "cost": 36, + "cost_minus_v": 0, + "v": 36 + }, + "C6": { + "T": 6, + "block_ranks": [ + 6, + 6, + 6, + 6, + 6, + 6 + ], + "cost": 36, + "cost_minus_v": 0, + "v": 36 + }, + "D4": { + "T": 4, + "block_ranks": [ + 3, + 3, + 3, + 3 + ], + "cost": 12, + "cost_minus_v": 0, + "v": 12 + }, + "D5": { + "T": 5, + "block_ranks": [ + 4, + 4, + 4, + 4, + 4 + ], + "cost": 20, + "cost_minus_v": 0, + "v": 20 + }, + "D6": { + "T": 6, + "block_ranks": [ + 5, + 5, + 5, + 5, + 5, + 5 + ], + "cost": 30, + "cost_minus_v": 0, + "v": 30 + }, + "E6_stored_basis": { + "T": 6, + "block_ranks": [ + 6, + 6, + 6, + 6, + 6, + 6 + ], + "cost": 36, + "cost_minus_v": 0, + "v": 36 + }, + "F4": { + "T": 4, + "block_ranks": [ + 9, + 9, + 9, + 9 + ], + "cost": 36, + "cost_minus_v": 12, + "v": 24 + }, + "pm1_T4": { + "T": 4, + "block_ranks": [ + 21, + 21, + 21, + 21 + ], + "cost": 84, + "cost_minus_v": 44, + "v": 40 + }, + "pm1_T5": { + "T": 5, + "block_ranks": [ + 61, + 61, + 61, + 61, + 61 + ], + "cost": 305, + "cost_minus_v": 184, + "v": 121 + }, + "pm1_T6": { + "T": 6, + "block_ranks": [ + 198, + 198, + 198, + 198, + 198, + 198 + ], + "cost": 1188, + "cost_minus_v": 824, + "v": 364 + } + }, + "model": "full-orthogonal-pattern pairing B0, exact coordinate Gram decoder, cost = sum_j rank_F2 B[R_j, A_j]", + "python": "3.12.14", + "screen": "dense-polar small-T gain screen (discussion 1166 comment 18934590 item 3)" +} \ No newline at end of file diff --git a/research/polar-law-small-t-screen/README.md b/research/polar-law-small-t-screen/README.md new file mode 100644 index 0000000000..836a35b2a7 --- /dev/null +++ b/research/polar-law-small-t-screen/README.md @@ -0,0 +1,125 @@ +# Dense-polar small-T gain screen (scoped negative; no κ claim) + +**What this is.** A bounded, exact screen of the open question posed as item 3 of +[this request](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18934590) +(DreamingOfClouds, 2026-10-14): the `T^2` threshold law of +[PR 2125](https://github.com/CrocSwap/integer-mult-bounds/pull/2125) is only +argued, and *"a proof, or a `T <= 6` configuration with cost < v, would settle +it"*. **No `T <= 6` configuration with cost < v was found** in the declared +domains below. This is a scoped negative over those domains, not an +impossibility proof. + +Contributor: **Aaron Wang**, with help from opencode (substantial AI +assistance). Base main `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`, +priority revision 4, chooser nonce `f29c10b2afbbb16fee6c3f9fda099134`. +The drawn `recursive-interfaces` cards were covered or live-claimed at entry; +this takes the named open request instead (scope change recorded in +`TASK.json`). + +## Model (unchanged, from #1590 / #446 Theorem C / PR 2125) + +A configuration is a list of root lines `t = 1..v` with vectors +`p(t) = q(t)` in `Q^T`. The full-orthogonal-pattern pairing `B` has unit +diagonal and `B_ts = 1` exactly where `p(t)·p(s) = 0` (admissible). The exact +coordinate Gram decoder `M = sum_j p_j q_j^T = Gram` is priced + +```text +cost = sum_{j=1..T} rank_F2 B[R_j, A_j], R_j = supp p_j, A_j = supp q_j, +``` + +Theorem C without the floor `w` (so any lower bound on this cost is the +stronger statement). A **gain** is `cost < v`, as in the PR 2125 table where +E7 (49 < 63) is the first gain found. + +## Established + +**1. Positive control: the PR 2125 table reproduces exactly** under an +independently written implementation (`search.py` re-derives roots, the exact +coordinate decoder over `Q`, and the F2 block ranks; PR 2125's code is pinned +but not imported): + +| unit | v | T | cost (B0 or stored B) | expected (PR 2125) | +|---|---:|---:|---:|---| +| D4 / D5 / D6 (standard coords, B0) | 12 / 20 / 30 | 4 / 5 / 6 | 12 / 20 / 30 | 12 / 20 / 30 (CHECKED) | +| A4 / A5 / A6 (first-independent basis, B0) | 10 / 15 / 21 | 5 / 6 / 7 | 16 / 25 / 36 | 16 / 25 / 36 (B0 upper bounds) | +| E6 (stored basis + stored B) | 36 | 6 | 36 | 36 (CHECKED) | +| E6 (first-independent basis, B0) | 36 | 6 | 37 | 37 (recorded) | +| E7 (first-independent basis, B0) | 63 | 7 | 49 | 49 (CHECKED, first gain) | +| E8 (first-independent basis, B0) | 120 | 8 | 72 | 72 (CHECKED) | + +F4 is record-only: standard coordinates with B0 give 36; PR 2125's recorded 24 +is a value from a searched pairing/basis. Both are upper bounds on the F2 +minimum (PR 2125 states its table costs are costs of specific `B`). + +Mutation controls pass: replacing `B` by the identity changes the cost on D5 +and E7, so the pricing is sensitive to the pairing as required. + +**2. Exhaustive puncture censuses (no gain, exact coverage).** For every +nonempty subset of lines, with the decoder and `B` restricted to the subset: + +| family | lines | subsets checked | gains (`cost < v`) | min(`cost - v`) | ties | +|---|---:|---:|---:|---:|---:| +| all {−1,0,1}^3 lines (T = 3) | 13 | 8,191 | 0 | 0 | 63 | +| D4 punctures (T = 4) | 12 | 4,095 | 0 | 0 | 63 | +| D5 punctures (T = 5) | 20 | 1,048,575 | 0 | 0 | 1,023 | + +So `cost >= v` holds exactly (with frequent ties) on **all 1,056,861 tested +subsets**, including every `T = 3` configuration over the {−1,0,1}^3 alphabet. +The T = 3 slice is consistent with the open core statement (A) of PR 2111 +(`cost >= v` at T = 3) on this alphabet. + +**3. Full configurations at T <= 6 and bounded searches.** B5, B6, C6, D4, +D5, D6 and E6 tie at `cost = v`; A4-A6 and F4 (standard, B0) and the +{−1,0,1}^T line sets (v = 40 / 121 / 364 at T = 4 / 5 / 6) are strictly above +v. Notably the {−1,0,1}^T sets have `v > T^2` at T = 5, 6 (121 > 25, +364 > 36) and show **no** gain (cost − v = 184 / 824): `v > T^2` is not +sufficient for a gain, consistent with the law being a necessary-condition +claim. Seeded greedy and random puncture searches on E6, D6, B6, A6 and the +{−1,0,1}^T sets, and seeded basis pivots on E6, D6, B6, {−1,0,1}^4, {−1,0,1}^5 +(cost depends on the basis; 120 random bases each plus the stored E6 basis), +find `min(cost - v) = 0` at best. No gain anywhere. + +## Scope and limitations + +- Cost is that of **one decoder per configuration** (the coordinate Gram + factorization in the declared basis) with **`B = B0`** (or the stored E6 + pairing). The configuration's minimum over all admissible `B` and all + exact factorizations can only be lower; a gain found here would have been a + true gain, but a negative here excludes only the tested decoder/pairing + pairs. PR 2125's annealed values (e.g. A5 at 21 < 25) confirm that other + pairings can price lower. +- Covered exhaustively: subsets of the {−1,0,1}^3 line set, D4 and D5, in the + declared bases. Everything else is bounded (seeded, recorded in + `CERTIFICATE.json`): no exhaustive claim over E6/D6/B6/{−1,0,1}^T punctures, + no non-root configurations, no `p != q` pairs, no overcomplete (`m > T`) + decoders, no fields other than `Q`/`F2`. +- No claim about `T >= 7`, no supplier, no kappa change, no selected-record + change. The T^2 law itself is not proved here. + +## Open next questions + +1. **Overcomplete punctures.** Does any `T <= 6` configuration admit an + `m = T + 1` exact factorization (as in the E6 one-extra-frame families of + PR 2240 / PR 2247) with cost < v? It matters because the coupling-lemma + square floors fix `m = T`; a first step is the D5 puncture space with one + redundant frame; blocker: the factorization space is infinite over `Q` + and needs a finite support-cell reduction like the lambda-cell method. +2. **Pairing minimisation on the ties.** D5 punctures show 1,023 ties with + `B = B0`; is `min_B cost = v` for these, or does a sparser `B` price below + v? First step: exact search over `B` on the largest tie punctures; blocker: + `rank_F2 B[R, A]` is not monotone in `B`, so branch-and-bound must be + rank-aware. +3. **Basis sensitivity at T = 6.** The E6 stored basis prices 36 with `B = B0` + and 37 in the first-independent basis. A GL_6(Q) optimisation of the basis + (or a proof that the minimum over bases is >= v) would sharpen the screen. + +## Reproduce + +```sh +python3 -B research/polar-law-small-t-screen/verify.py +``` + +Expected final line: `PASS_POLAR_SMALLT_SCREEN`. Runs in a few minutes with +Python 3.10+ and the standard library only (no third-party packages, no SAT, +no solver). `search.py` writes `CERTIFICATE.json`; `verify.py` reruns the +screen and checks the certificate against the pinned expectations. diff --git a/research/polar-law-small-t-screen/SOURCES.json b/research/polar-law-small-t-screen/SOURCES.json new file mode 100644 index 0000000000..d98750df6f --- /dev/null +++ b/research/polar-law-small-t-screen/SOURCES.json @@ -0,0 +1,40 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + } + ], + "package_data": [ + { + "path": "research/polar-law-small-t-screen/sources/e6_best.json", + "sha256": "80bb03e235b297ebf961cdc921268e7b1d40701128b1cb0c0c30449263270bcf", + "origin": "PR 2125 research/char2-threshold/data/e6_best.json at head d9eb80ac183bb4df185ca044fd65432b817333bb (DreamingOfClouds); read-only input to search.py" + }, + { + "path": "research/polar-law-small-t-screen/sources/pr2125_roots.py", + "sha256": "65d791524ddcdd923aefc536fae772176c4432dbd7c9ffcf2670051a22e411d7", + "origin": "PR 2125 research/char2-threshold/lib/roots.py at head d9eb80ac; pinned reference copy, not imported by search.py" + }, + { + "path": "research/polar-law-small-t-screen/sources/pr2125_units.py", + "sha256": "0a4261c8fc1a74f77e278863dfed223cf063003940e7e1a50d1a8fadffb73d39", + "origin": "PR 2125 research/char2-threshold/lib/units.py at head d9eb80ac; pinned reference copy, not imported by search.py" + }, + { + "path": "research/polar-law-small-t-screen/sources/pr2125_checks_units.py", + "sha256": "1d6c0a326c9740370cdd132df08955406874b7414321c3c8b171b30f623acc1b", + "origin": "PR 2125 research/char2-threshold/checks/units.py at head d9eb80ac; pinned reference copy, not imported by search.py" + } + ] +} \ No newline at end of file diff --git a/research/polar-law-small-t-screen/TASK.json b/research/polar-law-small-t-screen/TASK.json new file mode 100644 index 0000000000..da93361630 --- /dev/null +++ b/research/polar-law-small-t-screen/TASK.json @@ -0,0 +1,74 @@ +{ + "schema_version": 1, + "task_id": "coverage-law-change", + "original_card": { + "id": "coverage-law-change", + "question": "Can a template or call contract leave two or more unpaid coordinates per live family?", + "starting_points": [ + "research/complex-local-word-ceiling/README.md", + "research/idle-axis-hosting/PROOF.md", + "certificates/selected-result.json" + ], + "methods": [ + "State a replacement for the coverage identity (mass = 72W + 64N) and the contract change that realizes it, with its implementation cost.", + "Find an obstruction: show which data-endpoint obligation forces exactly one unpaid coordinate in the current template." + ], + "acceptance_gate": "An explicit replacement identity, verified on a small complete instance with dirty inputs, priced with ceiling.ceiling(unpaid=...).", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Explain where the single unpaid coordinate per family comes from in the hosted template; propose one change and price it. Ideal budget: two unpaid coordinates per family is 3.77x (levers.py).", + "bottleneck_link": "The deficit is one coordinate per family minus the centre charge; doubling unpaid coordinates per family scales it directly.", + "allowed_variations": [ + "One template change or one endpoint-contract change.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Counting a coordinate as unpaid while leaving it unadvanced in the data endpoint." + ], + "overlap_terms": [ + "coverage identity", + "unpaid coordinate", + "deficit law", + "W - 64N" + ] + }, + "scope_status": "changed", + "scope_change_reason": "All three drawn recursive-interfaces cards were covered or live-claimed at entry (2026-10-15 02:25-02:40 UTC). coverage-law-change's obstruction question was answered by ctoth's FINDING in discussion 1587 (the one unpaid coordinate is forced by the line-port contract) and its plane-port successor is worked live (philippeVV claims through 02:01 UTC); centre-path-sharing has 7 local packages plus discussion 1516's proven 64-per-call floor; connector-alphabet-change is claimed live (1337isnot1337 Cycle 43/44 claims at 01:53 and 02:23 UTC). The donation prompt makes an explicit open request from the handoffs thread a legitimate scope change, so this session takes discussion 1166 comment 18934590 item 3 (DreamingOfClouds): the PR 2125 T^2 threshold law is only argued, and 'a proof, or a T <= 6 configuration with cost < v, would settle it'.", + "actual_scope": "Exact screen for a T <= 6 configuration with dense-polar cost < v (full-orthogonal-pattern pairing B0, exact coordinate Gram decoder, cost = sum_j rank_F2 B[R_j, A_j]): positive control reproducing the PR 2125 table; exhaustive puncture censuses of the {0,+/-1}^3 line set (T = 3) and of D4 (T = 4) and D5 (T = 5); full systems A4-A6, B5, B6, C6, D4-D6, F4 and the {0,+/-1}^T line sets at T = 4, 5, 6; seeded greedy/random puncture searches and seeded basis pivots on E6, D6, B6 and the {0,+/-1}^T sets. Scoped negative: no gain found; min(cost - v) = 0 exactly on the exhaustive domains.", + "bottleneck_link": "The dense-polar law is one of the three remaining gaps of the rank-3/decoder theory that prices the local decoder words feeding the complex and bit suppliers; a T <= 6 gain would change what small-T decoder interfaces can cost, while a scoped negative keeps the v <= T^2 tie regime closed to this class of screens.", + "stop_rule": "Stop after the declared domains: the three exhaustive censuses and the seeded bounded searches as recorded in CERTIFICATE.json; no claim outside them and no repeated search with a different seed alone.", + "evidence": "CERTIFICATE.json (all counts, block ranks, seeds); controls reproduce PR 2125's checked table values 12/20/30 (D4/D5/D6), 36 and 37 (E6), 49 (E7), 72 (E8) and its A4-A6 B0 upper bounds 16/25/36 under an independently written implementation; mutation controls (B = I) change the cost. 1,056,861 subsets checked exhaustively with zero gains.", + "outcome": "negative-result", + "author": "Aaron Wang", + "ai_assistance": "with help from opencode (substantial AI assistance; no independent human review claimed)", + "open_questions": [ + { + "question": "Does any T <= 6 configuration admit an overcomplete (m = T + 1) exact factorization with cost < v?", + "why_it_matters": "The coupling-lemma square floors fix m = T; every known gain mechanism (E7/E8) lives in the square regime, so overcomplete terms are the untested route at small T.", + "first_step": "Run the one-extra rank-one frame family (as in PR 2240) on the D5 puncture space and price every lambda support cell.", + "blocked_by": "The factorization space over Q is infinite; it needs the finite support-cell reduction used for E6 before an exhaustive claim is possible." + }, + { + "question": "On the 1,023 tied D5 punctures (cost = v with B = B0), is the minimum over admissible pairings B exactly v, or can a sparser B price below v?", + "why_it_matters": "rank_F2 B[R, A] is not monotone in B, so the tie census does not settle the pairing minimum; a below-v pairing would be a genuine T = 5 gain.", + "first_step": "Exact branch-and-bound over B on the largest tied punctures (v >= 8), with rank-aware pruning.", + "blocked_by": "No monotone relaxation is known; the search must enumerate pairings or find a rank-aware bound." + }, + { + "question": "Is the E6 basis minimum of the B0 cost >= v over all GL_6(Q) bases?", + "why_it_matters": "Cost depends on the basis (36 stored vs 37 first-independent); a basis below 36 would be a T = 6 gain and settle item 3 positively.", + "first_step": "Deterministic descent over basis changes on the E6 line set with exact recomputation of P, Q supports.", + "blocked_by": "The support pattern is not continuous in the basis; local moves can escape any greedy descent." + } + ], + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "predecessor_credit": "Model, cost formula and the T^2 threshold question: DreamingOfClouds (https://github.com/CrocSwap/integer-mult-bounds/pull/2125, https://github.com/CrocSwap/integer-mult-bounds/pull/2228, https://github.com/CrocSwap/integer-mult-bounds/pull/2111, discussion request https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18934590). Prior lattice #446/#595/#1590. The E6 stored basis and pairing are their data/e6_best.json, pinned by SHA-256 in SOURCES.json package_data." +} \ No newline at end of file diff --git a/research/polar-law-small-t-screen/VERIFY.json b/research/polar-law-small-t-screen/VERIFY.json new file mode 100644 index 0000000000..747a199a2b --- /dev/null +++ b/research/polar-law-small-t-screen/VERIFY.json @@ -0,0 +1,22 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/polar-law-small-t-screen/search.py", + "research/polar-law-small-t-screen/verify.py", + "research/polar-law-small-t-screen/sources/e6_best.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Reruns the full screen: PR 2125 table controls (D4/D5/D6, A4-A6, E6 36/37, E7 49, E8 72), F4 record, B=I mutation controls, exhaustive puncture censuses (8191/4095/1048575 subsets, zero gains), full-system table, seeded greedy/random/basis-pivot searches; asserts CERTIFICATE.json matches and prints PASS_POLAR_SMALLT_SCREEN" + } + ] +} \ No newline at end of file diff --git a/research/polar-law-small-t-screen/search.py b/research/polar-law-small-t-screen/search.py new file mode 100644 index 0000000000..55cd08ab77 --- /dev/null +++ b/research/polar-law-small-t-screen/search.py @@ -0,0 +1,567 @@ +"""Dense-polar-law small-T gain screen. + +Model (DreamingOfClouds, PR 2125 / PR 2228 / #1590): a configuration is a list of +root lines t = 1..v with vectors p(t) = q(t) in Q^T. The full-orthogonal-pattern +pairing B has unit diagonal and B_ts = 1 exactly where dot(p(t), p(s)) = 0. The +exact coordinate Gram decoder M = sum_j p_j q_j^T = Gram is priced +cost = sum_j rank_F2 B[R_j, A_j] (Theorem C without the floor w), where +R_j = supp p_j and A_j = supp q_j. A gain is cost < v. + +Question screened (discussion 1166 comment 18934590 item 3): does any T <= 6 +configuration have cost < v? + +Everything here is exact integer / rational / F2 arithmetic, standard library +only. Independent reimplementation; PR 2125's files are pinned only as the +source of the table values and of the stored E6 basis/pairing. +""" +import itertools +import json +import hashlib +import os +import random +import sys +from fractions import Fraction as F + +HERE = os.path.dirname(os.path.abspath(__file__)) +E6_BEST_PATH = os.path.join(HERE, "sources", "e6_best.json") + + +# ---------------------------------------------------------------- root lines + +def canon(r): + f = next(x for x in r if x) + return tuple(r) if f > 0 else tuple(-x for x in r) + + +def lines(R): + seen, out = set(), [] + for r in R: + c = canon(r) + if c not in seen: + seen.add(c) + out.append(c) + return out + + +def A(n): + R = [] + for i in range(n + 1): + for j in range(i + 1, n + 1): + v = [0] * (n + 1) + v[i], v[j] = 2, -2 + R.append(v) + return lines(R) + + +def D(n): + R = [] + for i in range(n): + for j in range(i + 1, n): + for s in (2, -2): + v = [0] * n + v[i], v[j] = 2, s + R.append(v) + return lines(R) + + +def Bn(n): + R = [] + for i in range(n): + v = [0] * n + v[i] = 2 + R.append(v) + for j in range(i + 1, n): + for s in (2, -2): + w = [0] * n + w[i], w[j] = 2, s + R.append(w) + return lines(R) + + +def Cn(n): + R = [] + for i in range(n): + v = [0] * n + v[i] = 4 + R.append(v) + for j in range(i + 1, n): + for s in (2, -2): + w = [0] * n + w[i], w[j] = 2, s + R.append(w) + return lines(R) + + +def F4(): + R = [] + for i in range(4): + v = [0] * 4 + v[i] = 2 + R.append(v) + for j in range(i + 1, 4): + for s in (2, -2): + w = [0] * 4 + w[i], w[j] = 2, s + R.append(w) + for sg in itertools.product((1, -1), repeat=4): + R.append(list(sg)) + return lines(R) + + +def E8(): + R = [list(r) for r in D(8)] + for sg in itertools.product((1, -1), repeat=8): + if sg.count(-1) % 2 == 0: + R.append(list(sg)) + return lines(R) + + +def dot(a, b): + return sum(x * y for x, y in zip(a, b)) + + +def E7(): + return [r for r in E8() if sum(r) == 0] + + +def E6(): + r1 = [2, -2, 0, 0, 0, 0, 0, 0] + r2 = [0, 2, -2, 0, 0, 0, 0, 0] + return [r for r in E8() if dot(r, r1) == 0 and dot(r, r2) == 0] + + +def pm1_lines(T): + """All lines with coordinates in {0, +1, -1}, canonical sign.""" + R = [] + for r in itertools.product((1, 0, -1), repeat=T): + if any(r): + R.append(list(r)) + return lines(R) + + +# ------------------------------------------------------------ F2 machinery + +def rank2(rows): + piv = [] + for x in rows: + for p in piv: + x = min(x, x ^ p) + if x: + piv.append(x) + piv.sort(reverse=True) + return len(piv) + + +def b0_rows(L): + """Full orthogonal pattern as bitset rows: unit diagonal + orth pairs.""" + v = len(L) + out = [] + for t in range(v): + bits = 1 << t + for s in range(v): + if s != t and dot(L[t], L[s]) == 0: + bits |= 1 << s + out.append(bits) + return out + + +def supports(P): + """Column supports of the coefficient matrix P (nonzero test over Q).""" + v = len(P) + T = len(P[0]) if P else 0 + return [frozenset(t for t in range(v) if P[t][j] != 0) for j in range(T)] + + +def cost_from_supports(Brows, RS, AS): + out = [] + for R, A in zip(RS, AS): + if not R or not A: + out.append(0) + continue + amask = 0 + for s in A: + amask |= 1 << s + rows = [Brows[t] & amask for t in R] + out.append(rank2(rows)) + return out + + +# ------------------------------------------------- exact coordinate decoder + +def solve_coords(basis, r): + n = len(basis) + m = len(r) + M = [[F(basis[i][k]) for i in range(n)] + [F(r[k])] for k in range(m)] + piv, row = [], 0 + for c in range(n): + p = next((i for i in range(row, m) if M[i][c] != 0), None) + if p is None: + raise ValueError("dependent basis") + M[row], M[p] = M[p], M[row] + inv = M[row][c] + M[row] = [x / inv for x in M[row]] + for i in range(m): + if i != row and M[i][c] != 0: + f = M[i][c] + M[i] = [a - f * b for a, b in zip(M[i], M[row])] + row += 1 + return [M[i][n] for i in range(n)] + + +def frac_rank(rows): + M = [[F(x) for x in r] for r in rows] + rk = 0 + if not M: + return 0 + for c in range(len(M[0])): + p = next((i for i in range(rk, len(M)) if M[i][c] != 0), None) + if p is None: + continue + M[rk], M[p] = M[p], M[rk] + for i in range(rk + 1, len(M)): + if M[i][c] != 0: + f = M[i][c] / M[rk][c] + M[i] = [a - f * b for a, b in zip(M[i], M[rk])] + rk += 1 + return rk + + +def first_basis(L): + idx, cur = [], [] + for i, r in enumerate(L): + if frac_rank(cur + [r]) > len(cur): + idx.append(i) + cur.append(r) + return idx + + +def decoder_std(L): + return [[F(x) for x in r] for r in L], [[F(x) for x in r] for r in L] + + +def decoder_basis(L, bidx): + basis = [L[i] for i in bidx] + n = len(basis) + C = [[dot(basis[i], basis[k]) for k in range(n)] for i in range(n)] + P = [solve_coords(basis, r) for r in L] + Q = [[sum(P[t][i] * C[i][k] for i in range(n)) for k in range(n)] for t in range(len(L))] + return P, Q + + +def config_cost(L, P, Q, Brows=None): + if Brows is None: + Brows = b0_rows(L) + RS, AS = supports(P), supports(Q) + br = cost_from_supports(Brows, RS, AS) + return sum(br), br + + +# ------------------------------------------------------------------ controls + +def expect(name, got, want, fails): + ok = got == want + print("CTRL %-38s got=%s want=%s %s" % (name, got, want, "OK" if ok else "MISMATCH")) + if not ok: + fails.append((name, got, want)) + return ok + + +def controls(fails): + tab = {} + for nm in ("D4", "D5", "D6"): + L = {"D4": D(4), "D5": D(5), "D6": D(6)}[nm] + P, Q = decoder_std(L) + c, br = config_cost(L, P, Q) + tab[nm] = (len(L), c, br) + expect("%s standard B0 cost" % nm, c, {"D4": 12, "D5": 20, "D6": 30}[nm], fails) + for nm, want in (("A4", 16), ("A5", 25), ("A6", 36)): + L = {"A4": A(4), "A5": A(5), "A6": A(6)}[nm] + P, Q = decoder_basis(L, first_basis(L)) + c, br = config_cost(L, P, Q) + tab[nm] = (len(L), c, br) + expect("%s first-basis B0 cost" % nm, c, want, fails) + L7, L8 = E7(), E8() + P7, Q7 = decoder_basis(L7, first_basis(L7)) + c7, br7 = config_cost(L7, P7, Q7) + tab["E7"] = (len(L7), c7, br7) + expect("E7 first-basis B0 cost", c7, 49, fails) + P8, Q8 = decoder_basis(L8, first_basis(L8)) + c8, br8 = config_cost(L8, P8, Q8) + tab["E8"] = (len(L8), c8, br8) + expect("E8 first-basis B0 cost", c8, 72, fails) + # E6: stored basis + stored pairing (PR 2125 data/e6_best.json), then B0 + L6 = E6() + with open(E6_BEST_PATH, encoding="utf-8") as f: + e6 = json.load(f) + P6, Q6 = decoder_basis(L6, e6["basis"]) + Bstored = [e6["rows"][t] for t in range(len(L6))] + cs, brs = config_cost(L6, P6, Q6, Bstored) + expect("E6 stored basis + stored B cost", cs, e6["cost"], fails) + cb, brb = config_cost(L6, P6, Q6) + tab["E6"] = (len(L6), cs, brs) + P6f, Q6f = decoder_basis(L6, first_basis(L6)) + cf, brf = config_cost(L6, P6f, Q6f) + expect("E6 first-basis B0 cost", cf, 37, fails) + tab["E6_firstB0"] = (len(L6), cf, brf) + tab["E6_storedB0"] = (len(L6), cb, brb) + # F4: record-only. PR 2125 reports 24 as a recorded (searched) value, not a + # checked B0 value; standard coordinates with B0 give another upper bound. + Lf = F4() + Pf, Qf = decoder_std(Lf) + cff, brff = config_cost(Lf, Pf, Qf) + tab["F4"] = (len(Lf), cff, brff) + print("CTRL %-38s got=%s (record-only; PR 2125 recorded 24 from a searched pairing)" % ("F4 standard B0 cost", cff)) + # mutation control: B = identity must differ from B0 on D5 and E7 + L5 = D(5) + P5, Q5 = decoder_std(L5) + v = len(L5) + Bi = [1 << t for t in range(v)] + ci, _ = config_cost(L5, P5, Q5, Bi) + expect("D5 mutated B=I cost differs from 20", ci != 20, True, fails) + ci7, _ = config_cost(L7, P7, Q7, [1 << t for t in range(len(L7))]) + expect("E7 mutated B=I cost differs from 49", ci7 != 49, True, fails) + return tab + + +# ------------------------------------------------------- exhaustive punctures + +def exhaustive_punctures(L, P, Q, label, min_v=1): + """All subsets of L (decoder and B0 restricted to the subset).""" + n = len(L) + Bfull = b0_rows(L) + Pnz = [[j for j in range(len(P[0])) if P[t][j] != 0] for t in range(n)] + Qnz = [[j for j in range(len(Q[0])) if Q[s][j] != 0] for s in range(n)] + T = len(P[0]) + best = None # (cost - v, mask) + gains, ties = [], 0 + checked = 0 + for mask in range(1, 1 << n): + vs = mask.bit_count() + if vs < min_v: + continue + checked += 1 + br = [] + for j in range(T): + rows = [Bfull[t] & mask for t in range(n) if (mask >> t) & 1 and j in Pnz[t]] + if not rows: + br.append(0) + continue + cols = 0 + for s in range(n): + if (mask >> s) & 1 and j in Qnz[s]: + cols |= 1 << s + br.append(rank2([rw & cols for rw in rows])) + c = sum(br) + d = c - vs + if best is None or d < best[0]: + best = (d, mask, vs, c) + if c < vs: + gains.append((mask, vs, c)) + elif c == vs: + ties += 1 + return { + "label": label, + "lines": n, + "subsets_checked": checked, + "min_cost_minus_v": best[0], + "best_mask": best[1], + "best_v": best[2], + "best_cost": best[3], + "gains": gains[:10], + "gain_count": len(gains), + "tie_count": ties, + } + + +# -------------------------------------------------------- bounded searchers + +def greedy_search(L, P, Q, rng, restarts=12, steps=250, vmin=2): + """Hill-climb on subsets: add/remove one line, minimize cost - v.""" + n = len(L) + Bfull = b0_rows(L) + T = len(P[0]) + + def cost_of(mask): + br = 0 + for j in range(T): + rows = [Bfull[t] & mask for t in range(n) if (mask >> t) & 1 and P[t][j] != 0] + cols = 0 + for s in range(n): + if (mask >> s) & 1 and Q[s][j] != 0: + cols |= 1 << s + br += rank2([rw & cols for rw in rows]) if rows else 0 + return br + + best = None + for _ in range(restarts): + vs = rng.randint(vmin, n) + mask = 0 + for t in rng.sample(range(n), vs): + mask |= 1 << t + cur = cost_of(mask) - mask.bit_count() + if best is None or cur < best[0]: + best = (cur, mask) + for _ in range(steps): + t = rng.randrange(n) + cand = mask ^ (1 << t) + if cand.bit_count() < vmin: + continue + d = cost_of(cand) - cand.bit_count() + if d <= cur: + mask, cur = cand, d + if d < best[0]: + best = (d, mask) + return {"min_cost_minus_v": best[0], "mask": best[1], + "v": best[1].bit_count(), "cost": best[0] + best[1].bit_count()} + + +def basis_pivot_search(L, rng, trials=150, bidx0=None): + """Bounded search over bases of the line span: pick T independent lines as + the basis, build the exact coordinate decoder, price B0. Reports the min.""" + n = len(L) + T = frac_rank(L) + best = None + idxs = list(range(n)) + cands = [] + if bidx0 is not None: + cands.append(list(bidx0)) + for _ in range(trials): + rng.shuffle(idxs) + pick, cur = [], [] + for i in idxs: + if len(pick) >= T: + break + if frac_rank(cur + [L[i]]) > len(cur): + pick.append(i) + cur.append(L[i]) + if len(pick) == T: + cands.append(pick) + for bidx in cands: + try: + P, Q = decoder_basis(L, bidx) + except ValueError: + continue + c, _ = config_cost(L, P, Q) + d = c - n + if best is None or d < best[0]: + best = (d, c, list(bidx)) + return {"min_cost_minus_v": best[0], "cost": best[1], "basis": best[2], "bases_tried": len(cands)} + + +def random_subsets(L, P, Q, rng, trials=300, vmin=2): + n = len(L) + Bfull = b0_rows(L) + T = len(P[0]) + best = None + for _ in range(trials): + vs = rng.randint(vmin, n) + mask = 0 + for t in rng.sample(range(n), vs): + mask |= 1 << t + br = 0 + for j in range(T): + rows = [Bfull[t] & mask for t in range(n) if (mask >> t) & 1 and P[t][j] != 0] + cols = 0 + for s in range(n): + if (mask >> s) & 1 and Q[s][j] != 0: + cols |= 1 << s + br += rank2([rw & cols for rw in rows]) if rows else 0 + d = br - vs + if best is None or d < best[0]: + best = (d, mask, vs, br) + return {"min_cost_minus_v": best[0], "mask": best[1], "v": best[2], "cost": best[3]} + + +def main(): + sys.stdout.reconfigure(encoding="utf-8") + fails = [] + cert = { + "screen": "dense-polar small-T gain screen (discussion 1166 comment 18934590 item 3)", + "model": "full-orthogonal-pattern pairing B0, exact coordinate Gram decoder, cost = sum_j rank_F2 B[R_j, A_j]", + "python": sys.version.split()[0], + } + print("== controls (PR 2125 table) ==") + tab = controls(fails) + cert["controls"] = {k: {"v": v, "cost": c, "block_ranks": br} for k, (v, c, br) in tab.items()} + + print("== exhaustive punctures ==") + ex = [] + for lab, L, P, Q in ( + ("T3_pm1_all_subsets", pm1_lines(3), *decoder_std(pm1_lines(3))), + ("D4_all_subsets", D(4), *decoder_std(D(4))), + ("D5_all_subsets", D(5), *decoder_std(D(5))), + ): + r = exhaustive_punctures(L, P, Q, lab) + ex.append(r) + print("EX %-24s subsets=%d min(cost-v)=%d best v=%d cost=%d gains=%d ties=%d" + % (lab, r["subsets_checked"], r["min_cost_minus_v"], r["best_v"], r["best_cost"], + r["gain_count"], r["tie_count"])) + cert["exhaustive"] = ex + + print("== full configurations at T <= 6 ==") + full = {} + for nm, L in (("A4", A(4)), ("A5", A(5)), ("A6", A(6)), + ("B5", Bn(5)), ("B6", Bn(6)), ("C6", Cn(6)), + ("D4", D(4)), ("D5", D(5)), ("D6", D(6)), ("F4", F4()), + ("pm1_T4", pm1_lines(4)), ("pm1_T5", pm1_lines(5)), ("pm1_T6", pm1_lines(6))): + P, Q = decoder_std(L) + c, br = config_cost(L, P, Q) + full[nm] = {"v": len(L), "T": len(L[0]), "cost": c, "cost_minus_v": c - len(L), "block_ranks": br} + print("FULL %-8s v=%3d T=%d cost=%4d cost-v=%d" % (nm, len(L), len(L[0]), c, c - len(L))) + for nm, L in (("E6_stored_basis", None),): + L = E6() + with open(E6_BEST_PATH, encoding="utf-8") as f: + e6 = json.load(f) + P, Q = decoder_basis(L, e6["basis"]) + c, br = config_cost(L, P, Q) + full[nm] = {"v": len(L), "T": 6, "cost": c, "cost_minus_v": c - len(L), "block_ranks": br} + print("FULL %-8s v=%3d T=6 cost=%4d cost-v=%d (B0; stored B costs 36)" % (nm, len(L), c, c - len(L))) + cert["full_configs"] = full + + print("== bounded searches (seeded) ==") + rng = random.Random(20261015) + bounded = {} + for nm, L, basis in (("E6_greedy", E6(), "stored"), ("D6_greedy", D(6), "std"), + ("B6_greedy", Bn(6), "std"), ("A6_greedy", A(6), "std"), + ("pm1T4_greedy", pm1_lines(4), "std"), ("pm1T5_greedy", pm1_lines(5), "std"), + ("pm1T6_greedy", pm1_lines(6), "std")): + if basis == "stored": + with open(E6_BEST_PATH, encoding="utf-8") as f: + e6 = json.load(f) + P, Q = decoder_basis(L, e6["basis"]) + else: + P, Q = decoder_std(L) + g = greedy_search(L, P, Q, rng) + s = random_subsets(L, P, Q, rng, trials=200) + bounded[nm] = {"greedy": g, "random": s} + print("BND %-12s greedy min(cost-v)=%d (v=%d) random min=%d (v=%d)" + % (nm, g["min_cost_minus_v"], g["v"], s["min_cost_minus_v"], s["v"])) + cert["bounded"] = bounded + + print("== bounded basis pivots (seeded; cost depends on basis) ==") + pivots = {} + with open(E6_BEST_PATH, encoding="utf-8") as f: + e6 = json.load(f) + for nm, L, b0 in (("E6_pivot", E6(), e6["basis"]), ("D6_pivot", D(6), None), + ("B6_pivot", Bn(6), None), ("pm1T4_pivot", pm1_lines(4), None), + ("pm1T5_pivot", pm1_lines(5), None)): + r = basis_pivot_search(L, rng, trials=120, bidx0=b0) + pivots[nm] = r + print("PIV %-12s bases=%d min(cost-v)=%d cost=%d" % (nm, r["bases_tried"], r["min_cost_minus_v"], r["cost"])) + cert["basis_pivots"] = pivots + + cert["control_failures"] = fails + cert["any_gain_found"] = any(r["gain_count"] for r in ex) or any( + g["greedy"]["min_cost_minus_v"] < 0 or g["random"]["min_cost_minus_v"] < 0 + for g in bounded.values()) or any( + r["min_cost_minus_v"] < 0 for r in pivots.values()) + out = os.path.join(HERE, "CERTIFICATE.json") + with open(out, "w", encoding="utf-8") as f: + json.dump(cert, f, indent=1, sort_keys=True) + print("ANY_GAIN_FOUND:", cert["any_gain_found"]) + print("CERTIFICATE:", out) + return 1 if fails else 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/research/polar-law-small-t-screen/sources/e6_best.json b/research/polar-law-small-t-screen/sources/e6_best.json new file mode 100644 index 0000000000..ee5760953b --- /dev/null +++ b/research/polar-law-small-t-screen/sources/e6_best.json @@ -0,0 +1 @@ +{"basis": [16, 7, 19, 20, 29, 25], "rows": [4279222275, 64441270275, 13904919564, 54815112204, 22995481392, 45723366192, 40422657984, 28295876544, 16169829360, 52550173680, 24253762764, 44465065164, 41177641020, 27540910140, 27487432899, 41231118531, 44386421811, 24332405811, 52408615695, 16311386895, 62412991146, 56978134618, 47819676006, 30358742422, 38143370601, 20707695001, 11612542629, 6309980757, 34871810709, 17939457637, 9850939737, 6561633705, 6592042326, 9745033638, 17762248346, 34652658282], "cost": 36} \ No newline at end of file diff --git a/research/polar-law-small-t-screen/sources/pr2125_checks_units.py b/research/polar-law-small-t-screen/sources/pr2125_checks_units.py new file mode 100644 index 0000000000..14e22af149 --- /dev/null +++ b/research/polar-law-small-t-screen/sources/pr2125_checks_units.py @@ -0,0 +1,21 @@ +"""Group G1: exact F2 costs of root-unit decoders (the T^2 threshold table). For each unit the exact T-block decoder M = P Q^T = Gram (pure Fractions), +its zero pattern, and the exact F2 cost sum_j rank_F2 B[R_j, A_j] of an admissible pairing B. B0 = full orthogonal pattern.""" +import sys, os, json +sys.path.insert(0, os.path.join(os.path.dirname(os.path.abspath(__file__)), '..', 'lib')) +from roots import *; from units import * +DATA = os.path.join(os.path.dirname(os.path.abspath(__file__)), '..', 'data') +def row(name, L, P, Q, B, label): + v = len(L); T = len(P[0]); ex = exact(L, P, Q); adm = admissible(L, B); br = block_ranks(P, Q, B) + print("UN %s v=%d T=%d rank(L)=%d decoder exact (M = Gram): %s; B admissible: %s; %s; block ranks %s; cost %d; T^2 = %d; cost - v = %d" % ( + name, v, T, rank(L), ex, adm, label, br, sum(br), T * T, sum(br) - v)) +for nm in ('D4', 'D5', 'D6'): + L = unit(nm); P, Q = decoder_std(L); row(nm, L, P, Q, b0(L), 'standard coordinates, B = B0') +L = unit('E6'); e6 = json.load(open(os.path.join(DATA, 'e6_best.json'))) +P, Q = decoder(L, e6['basis']); B = [[(e6['rows'][t] >> s) & 1 for s in range(len(L))] for t in range(len(L))] +row('E6', L, P, Q, B, 'stored basis and stored B (found by local search from B0)') +print("UN E6 B0 in the stored basis costs %d; in the first-independent basis %d" % (sum(block_ranks(P, Q, b0(L))), sum(block_ranks(*decoder(L, first_basis(L)), b0(L))))) +for nm in ('E7', 'E8'): + L = unit(nm); P, Q = decoder(L, first_basis(L)); row(nm, L, P, Q, b0(L), 'first independent lines as basis, B = B0') +for nm in ('A4', 'A5', 'A6'): + L = unit(nm); P, Q = decoder(L, first_basis(L)); row(nm, L, P, Q, b0(L), 'first independent lines as basis, B = B0 (upper bound only)') +print("UN T^2 vs v for roots: D4 16 vs 12, D5 25 vs 20, D6 36 vs 30, E6 36 vs 36, E7 49 vs 63, E8 64 vs 120") diff --git a/research/polar-law-small-t-screen/sources/pr2125_roots.py b/research/polar-law-small-t-screen/sources/pr2125_roots.py new file mode 100644 index 0000000000..54d37bdd30 --- /dev/null +++ b/research/polar-law-small-t-screen/sources/pr2125_roots.py @@ -0,0 +1,39 @@ +"""Root lines of the units A_n, D_n, E6, E7, E8 in pure Python (integer coordinates scaled by 2, so the half-integer E8 roots are integral). +A 'line' is a root up to sign; lines are returned with first nonzero coordinate positive, in a fixed generation order.""" +import itertools +def canon(r): + f = next(x for x in r if x) + return tuple(r) if f > 0 else tuple(-x for x in r) +def lines(R): + seen = set(); out = [] + for r in R: + c = canon(r) + if c not in seen: seen.add(c); out.append(c) + return out +def A(n): + R = [] + for i in range(n + 1): + for j in range(i + 1, n + 1): + v = [0] * (n + 1); v[i] = 2; v[j] = -2; R.append(v) + return lines(R) +def D(n): + R = [] + for i in range(n): + for j in range(i + 1, n): + for s in (2, -2): + v = [0] * n; v[i] = 2; v[j] = s; R.append(v) + return lines(R) +def E8(): + R = [list(r) for r in D(8)] + for sg in itertools.product((1, -1), repeat=8): + if sg.count(-1) % 2 == 0: R.append(list(sg)) + return lines(R) +def dot(a, b): return sum(x * y for x, y in zip(a, b)) +def E7(): + return [r for r in E8() if sum(r) == 0] # orthogonal to s = (1,...,1)/2 +def E6(): + r1 = [2, -2, 0, 0, 0, 0, 0, 0]; r2 = [0, 2, -2, 0, 0, 0, 0, 0] # = -1 in the root normalisation: an A2 + return [r for r in E8() if dot(r, r1) == 0 and dot(r, r2) == 0] +def unit(name): + return {'D4': lambda: D(4), 'D5': lambda: D(5), 'D6': lambda: D(6), 'A4': lambda: A(4), 'A5': lambda: A(5), 'A6': lambda: A(6), + 'E6': E6, 'E7': E7, 'E8': E8}[name]() diff --git a/research/polar-law-small-t-screen/sources/pr2125_units.py b/research/polar-law-small-t-screen/sources/pr2125_units.py new file mode 100644 index 0000000000..080677f9b6 --- /dev/null +++ b/research/polar-law-small-t-screen/sources/pr2125_units.py @@ -0,0 +1,69 @@ +"""Exact T-block decoders of root units and F2 costs. decoder(L, basis): P = coordinates of each root line in the chosen basis of the unit, +Q = P . Gram(basis) (exact Fractions), so that M = P Q^T = Gram(L) (coordinates scaled by 2, entries are 4 ). The F2 cost of an admissible B +is sum_j rank_F2 B[R_j, A_j] with R_j = supp p_j, A_j = supp q_j (Theorem C without the floor).""" +from fractions import Fraction as F +from roots import dot +def solve_coords(basis, r): + """exact coordinates x with sum_i x_i basis_i = r (basis independent rows): Gaussian elimination over Q.""" + n = len(basis); m = len(r) + M = [[F(basis[i][k]) for i in range(n)] + [F(r[k])] for k in range(m)] + piv = []; row = 0 + for c in range(n): + p = next((i for i in range(row, m) if M[i][c] != 0), None) + if p is None: raise ValueError('dependent basis') + M[row], M[p] = M[p], M[row]; M[row] = [x / M[row][c] for x in M[row]] + for i in range(m): + if i != row and M[i][c] != 0: + f = M[i][c]; M[i] = [a - f * b for a, b in zip(M[i], M[row])] + row += 1 + for i in range(n, m): assert M[i][n] == 0, 'vector not in span' + return [M[i][n] for i in range(n)] +def first_basis(L): + idx = []; cur = [] + for i, r in enumerate(L): + try: + solve_coords(cur + [r], r) if False else None + except Exception: pass + if rank(cur + [r]) > len(cur): idx.append(i); cur.append(r) + return idx +def rank(rows): + M = [[F(x) for x in r] for r in rows]; rk = 0 + if not M: return 0 + for c in range(len(M[0])): + p = next((i for i in range(rk, len(M)) if M[i][c] != 0), None) + if p is None: continue + M[rk], M[p] = M[p], M[rk] + for i in range(rk + 1, len(M)): + if M[i][c] != 0: + f = M[i][c] / M[rk][c]; M[i] = [a - f * b for a, b in zip(M[i], M[rk])] + rk += 1 + return rk +def decoder(L, bidx): + basis = [L[i] for i in bidx]; n = len(basis) + C = [[dot(basis[i], basis[k]) for k in range(n)] for i in range(n)] + P = [solve_coords(basis, r) for r in L] + Q = [[sum(P[t][i] * C[i][k] for i in range(n)) for k in range(n)] for t in range(len(L))] + return P, Q +def exact(L, P, Q): + v = len(L) + return all(sum(P[t][j] * Q[s][j] for j in range(len(P[0]))) == dot(L[t], L[s]) for t in range(v) for s in range(v)) +def rank2(rows): + piv = [] + for x in rows: + for p in piv: x = min(x, x ^ p) + if x: piv.append(x); piv.sort(reverse=True) + return len(piv) +def block_ranks(P, Q, B): + v = len(P); T = len(P[0]); out = [] + for j in range(T): + R = [t for t in range(v) if P[t][j] != 0]; A = [s for s in range(v) if Q[s][j] != 0] + out.append(rank2([sum(B[t][s] << i for i, s in enumerate(A)) for t in R])) + return out +def b0(L): + """full orthogonal pattern: B_ts = 1 iff t = s or r_t orthogonal to r_s.""" + v = len(L); return [[1 if (t == s or dot(L[t], L[s]) == 0) else 0 for s in range(v)] for t in range(v)] +def admissible(L, B): + v = len(L); return all(B[t][t] == 1 and all(B[t][s] == 0 or dot(L[t], L[s]) == 0 for s in range(v) if s != t) for t in range(v)) +def decoder_std(L): + """standard coordinates (basis e_1..e_n, Gram 4I in the x2 scaling): P = Q = the root coordinates; M = P Q^T = .""" + return [[F(x) for x in r] for r in L], [[F(x) for x in r] for r in L] diff --git a/research/polar-law-small-t-screen/verify.py b/research/polar-law-small-t-screen/verify.py new file mode 100644 index 0000000000..76f10cb79b --- /dev/null +++ b/research/polar-law-small-t-screen/verify.py @@ -0,0 +1,85 @@ +"""Verify the dense-polar small-T gain screen. + +Reruns search.py (deterministic, seeded) and checks CERTIFICATE.json against +the pinned PR 2125 table values and the exhaustive-census counts. +""" +import json +import os +import subprocess +import sys + +HERE = os.path.dirname(os.path.abspath(__file__)) + +PINNED_CONTROLS = { + "D4": {"v": 12, "cost": 12}, + "D5": {"v": 20, "cost": 20}, + "D6": {"v": 30, "cost": 30}, + "A4": {"v": 10, "cost": 16}, + "A5": {"v": 15, "cost": 25}, + "A6": {"v": 21, "cost": 36}, + "E7": {"v": 63, "cost": 49}, + "E8": {"v": 120, "cost": 72}, + "E6": {"v": 36, "cost": 36}, + "E6_firstB0": {"v": 36, "cost": 37}, +} + +PINNED_EXHAUSTIVE = { + "T3_pm1_all_subsets": {"subsets_checked": 8191, "gain_count": 0, "min_cost_minus_v": 0}, + "D4_all_subsets": {"subsets_checked": 4095, "gain_count": 0, "min_cost_minus_v": 0}, + "D5_all_subsets": {"subsets_checked": 1048575, "gain_count": 0, "min_cost_minus_v": 0}, +} + + +def main(): + sys.stdout.reconfigure(encoding="utf-8") + py = sys.executable + run = subprocess.run([py, os.path.join(HERE, "search.py")], + capture_output=True, text=True, encoding="utf-8") + print(run.stdout[-2000:]) + if run.returncode != 0: + print("FAIL search.py exited", run.returncode) + print(run.stderr[-1000:]) + return 1 + with open(os.path.join(HERE, "CERTIFICATE.json"), encoding="utf-8") as f: + cert = json.load(f) + bad = [] + for name, want in PINNED_CONTROLS.items(): + got = cert["controls"].get(name) + if got is None: + bad.append("missing control " + name) + continue + for k, w in want.items(): + if got.get(k) != w: + bad.append("control %s %s: got %s want %s" % (name, k, got.get(k), w)) + ex = {r["label"]: r for r in cert["exhaustive"]} + for name, want in PINNED_EXHAUSTIVE.items(): + got = ex.get(name) + if got is None: + bad.append("missing exhaustive " + name) + continue + for k, w in want.items(): + if got.get(k) != w: + bad.append("exhaustive %s %s: got %s want %s" % (name, k, got.get(k), w)) + if cert.get("any_gain_found") is not False: + bad.append("any_gain_found is not False") + if cert.get("control_failures"): + bad.append("control failures recorded: %s" % cert["control_failures"]) + # every bounded search must report a nonnegative min + for group in ("bounded", "basis_pivots"): + for nm, entry in cert.get(group, {}).items(): + vals = entry.values() if group == "basis_pivots" else ( + [entry["greedy"], entry["random"]]) + for sub in vals: + if isinstance(sub, dict) and sub.get("min_cost_minus_v", 0) < 0: + bad.append("%s/%s reports a gain" % (group, nm)) + if bad: + for b in bad: + print("FAIL", b) + print("FAIL_POLAR_SMALLT_SCREEN") + return 1 + print("PASS_POLAR_SMALLT_SCREEN") + return 0 + + +if __name__ == "__main__": + sys.exit(main())