Research: dense-polar small-T gain screen - no T <= 6 gain in 1,056,861 exhaustive subsets (scoped negative)

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.

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"
+  }
+ ]
+}

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."
+}

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"
+  }
+ ]
+}