Certify that no owned-helper relation subspace pays after #5421 (BIT) or #5383 (complex) (negative result, no new kappa)

docs/ci-verification.md

@@ -1,8 +1,40 @@
 # CI verification
 
-## Current selected-family replay: #4610 with #5241
+## Current selected-family replay: #5413 with #5407 and #5414
 
 The [selected record](../certificates/selected-result.json) binds conditional
+κ = 0.003027288235, the [promotion and scope](research/pr-intake-evidence/pr5413-promotion/PROMOTION.md),
+[explicit source closure](../certificates/frontier5413-source.json),
+[review validation](research/pr-intake-evidence/pr5413-promotion/VALIDATION.json), and
+[integration receipt](research/pr-intake-evidence/pr5413-promotion/INTEGRATION.json).
+
+`make frontier5413-verify` authenticates the selected source manifest, derives
+the certificate from frozen numerical evidence, and exports the complete
+three-package execution closure. It replays #5407's five-stage provider audit,
+#5413's eight-stage admission, and #5414's independent companion screen serially.
+The exported inputs are checked again afterward. Source-bound #4610/#5241 and
+earlier BIT/native/compiler/tape/analytic foundation coverage is explicitly
+reused; its historical suites are not rerun.
+
+Each package runs under an external sampled 1 GiB aggregate descendant-memory
+guard, with timeouts of 660 seconds for the provider and primary packages and
+120 seconds for the companion. On macOS the replay uses the reviewed RLIMIT_AS
+adapter; on Linux it invokes the unmodified package wrappers. The recorded
+successful local macOS replay does not establish a hosted Linux pass.
+
+The [frontier5413 workflow](../.github/workflows/frontier5413.yml) is manual-only,
+uses Python 3.12 on Ubuntu, materializes the declared source closure, and uploads
+receipts and logs. Its status is separate from local validation and recorded in
+the integration receipt. Routine donor PRs do not launch this selected replay.
+
+`make selected-record-check` verifies metadata and source/proof hashes. It does
+not execute the operators or prove the five inherited framework assumptions.
+The finite checks do not establish the full integer multiplication theorem,
+and the uniform word remains unmaterialized.
+
+## Historical selected-family replay: #4610 with #5241
+
+The historical [selected record](../certificates/checkpoints/frontier4610.json) binds conditional
 κ = 0.0030217758, the [review](research/pr-intake-evidence/pr4610/PROOF-REVIEW.md),
 [explicit source closure](../certificates/frontier4610-source.json),
 [review validation](research/pr-intake-evidence/pr4610/VALIDATION.json), and

research/bit-relation-subspaces/README.md

@@ -0,0 +1,109 @@
+# No further owned-helper relation subspace after #5421 (BIT) and #5383 (complex)
+
+**Negative result; no new κ and no new BIT saving.**
+
+[PR #5421](https://github.com/CrocSwap/integer-mult-bounds/pull/5421) (Ali Romman) owns nine helper
+relations on the reverse PR589 BIT word. Each relation zeroes one COPY job (rank 7) and one rank-1 move,
+and costs one rank-8 helper target. Its README says that a further BIT gain needs a new relation space.
+[PR #5428](https://github.com/CrocSwap/integer-mult-bounds/pull/5428) (target 6) proposes systematic
+relation-space selection for the same purpose.
+
+This package answers the question exactly for that word. Any number of additional relations, in any
+combination, removes at most 7.5 units of paid rank mass per relation dimension. A dimension costs one
+rank-8 target. Every relation subspace therefore loses at least `8^t - 7.5 = 0.4424` raw moment per
+local call at `C = 0.00347207`. The bound holds for every `C < 0.031`.
+
+## Model
+
+The model is #5421's. Replay the source records in reverse over GF(2) with 661 entry symbols. A paid job
+is a MOVE of rank `r > 0` or a COPY entrance (rank 7). A relation subspace `V` consists of entry forms
+supported on full-entrance fields, with helper pivots. A job becomes free exactly when the binary row of
+its moved value lies in `V`. The raw moment changes per local call by
+
+```text
+sum over removed jobs of r^t  -  8^t dim V,      t = 1 - C,
+```
+
+and the controller multiplies this by its eighteen full calls. The certificate ignores the frame and pivot
+conditions, so it bounds legal subspaces as well.
+
+## Certificate
+
+Let `E'` be the multiset of job rows, with each row repeated `rank` times, and let `w(V)` be the paid mass
+with rows in `V`. By the matroid union theorem, if `m` copies of `E'` split into `p` linearly independent
+sets, then `m w(V) <= p dim V` for every subspace `V`. Edmonds' augmenting paths make the split exact.
+A row in a tight subspace (`w = 8 dim`) is one for which an extra copy cannot be inserted.
+
+| Check | Result |
+|---|---|
+| Source paid jobs / jobs with a legal row | 2,920 / 2,384 (1,773 distinct rows) |
+| Source word, `E'` into 8 sets | splits, so `max_V (w - 8 dim) = 0` |
+| Source word, tight subspaces | exactly nine, each COPY H7 + MOVE H1: the #5421 relations |
+| Modulo those nine, `E'` into 8 sets | splits; no tight row, so `w(V) < 8 dim V` |
+| Modulo those nine, `2E'` into 15 sets | splits, so `w(V) <= 7.5 dim V` for all `V` |
+| Control: source `2E'` into 15 sets | fails, as required |
+| Control: extra rank-1 job on a COPY row | breaks the 8-split, as required |
+
+Since `r^t <= r` for `r >= 1`, the moment change is at most `(7.5 - 8^t) dim V < 0`.
+[RESULT.json](RESULT.json) holds the rebuilt numbers.
+
+## Part 2: the complex word
+
+The binding complex side uses Cao Yifan's #4610 word with the eight owned relations of
+[PR #5383](https://github.com/CrocSwap/integer-mult-bounds/pull/5383) (Ali Romman), carried through #5392,
+#5398 and the selected #5413 caller. The #5413 caller adds 144 paid and 144 target rank-8 jobs, which
+cancel rank by rank. [complex.py](complex.py) replays the backward word exactly over Q with warp words.
+The model is #5377/#5383's: 326 cold helpers carry rank-9 targets. A climb is freed when its row lies
+in V. A centre job is freed when its row minus an earlier same-frame snapshot lies in V.
+
+| Check | Result |
+|---|---|
+| Backward paid profile | `{1:2201, 2:412, 3:510, 4:127, 5:40, 8:8}` |
+| Candidates | 163 pure-cold climb rows, 56 centre snapshot options |
+| #5383's eight relations | free all eight centres and exactly eight rank-1 zero-site climbs |
+| Remaining climb rows modulo them | 155 rows, linearly independent over Q, rank mass at most 3 |
+
+Because the remaining rows are independent, any further subspace V contains at most `dim V` of them.
+It frees at most `3 dim V` of paid mass, against `9^t dim V = 8.9403 dim V` of lost targets. Every
+extension of #5383's relations therefore loses at least 5.94 raw moment per local call at the
+selected `C = 0.003027288235`. [RESULT-COMPLEX.json](RESULT-COMPLEX.json) holds the rebuild. The result
+does not cover a relation set that omits #5383's eight relations. Snapshot options are alternatives for
+one centre, so they are not single matroid elements. The centre-exchange cap of
+[owned-relation-exhaustion](../owned-relation-exhaustion/README.md) already limits that family, and all
+eight centres are already used.
+
+## Reproduce
+
+```sh
+python3.12 -B scripts/research_package.py --package research/bit-relation-subspaces
+python3.12 -I -B research/bit-relation-subspaces/verify.py
+python3.12 -I -B research/bit-relation-subspaces/complex.py
+python3.12 -I -B research/bit-relation-subspaces/test_verify.py
+```
+
+The verifier uses only the standard library and finishes in about half a minute. It prints
+`PASS_BIT_RELATION_SUBSPACES_NO_FURTHER_GAIN_AFTER_5421`. Part 2 prints
+`PASS_COMPLEX_RELATION_SUBSPACES_NO_FURTHER_GAIN_AFTER_5383` in a few seconds. The controls print
+`PASS_BIT_RELATION_SUBSPACES_CONTROLS`.
+
+## Scope
+
+The result fixes the PR589 operation order, helper inventory and job set. It does not cover a changed
+chronology, a different BIT word or new helpers. Snapshot replacement in the style of PR #5377 applies
+only to owned fields. On this word the only owned paid jobs are the nine COPY jobs, which #5421 already
+removes. The nine relations come from the source word itself, so #5421 is not a live input.
+
+## Open next questions
+
+- Does a changed chronological order or a different BIT word admit a relation subspace of density
+  above `8^t`? First run the same 8- and 15-part splits on its job rows. No frozen changed BIT word with an
+  admitted invoice is available yet.
+- Can a complex relation set that omits #5383's eight relations beat them? First enumerate one
+  snapshot option per centre and run the same independence test on each choice.
+
+## Credit
+
+DreamingOfClouds (PR #589) and eumemic (PR #555) supplied the source word and port construction.
+Cao Yifan supplied the #4610 word. Ali Romman's PR #5421, PR #5377 and PR #5383 supplied the owned-helper relation method that this package
+generalises. zxv's PR #5428 named relation-space selection as a target. Prepared by Mark (Matarener)
+with substantial Claude Code assistance. New work is Apache-2.0.

research/bit-relation-subspaces/RESULT-COMPLEX.json

@@ -0,0 +1,48 @@
+{
+ "V0_frees": {
+  "centres": [
+   11332,
+   11358,
+   11384,
+   11410,
+   11436,
+   11462,
+   11488,
+   11514
+  ],
+  "zero_site_climbs": [
+   15584,
+   15870,
+   15876,
+   17233,
+   17245,
+   17256,
+   17264,
+   17722
+  ]
+ },
+ "backward_paid": {
+  "1": 2201,
+  "2": 412,
+  "3": 510,
+  "4": 127,
+  "5": 40,
+  "8": 8
+ },
+ "bound": "every further relation subspace V frees paid mass <= 3 dim V",
+ "centre_snapshot_options": 56,
+ "cold_helpers": 326,
+ "moment": {
+  "C": "0.003027288235",
+  "loss_per_dimension_at_least": "5.940333969219",
+  "nine_to_t": "8.940333969219"
+ },
+ "pure_cold_climbs": 163,
+ "remaining_profile": {
+  "1": 58,
+  "2": 9,
+  "3": 88
+ },
+ "remaining_rank": 155,
+ "remaining_rows": 155
+}

research/bit-relation-subspaces/RESULT.json

@@ -0,0 +1,147 @@
+{
+ "already_zero": 0,
+ "controls": {
+  "injected_rank1_on_copy_row": "rejected",
+  "source_2E_into_15": "rejected"
+ },
+ "legal_jobs": 2384,
+ "legal_profile": {
+  "1": 1212,
+  "2": 1041,
+  "3": 69,
+  "4": 41,
+  "5": 10,
+  "6": 1,
+  "7": 10
+ },
+ "moment": {
+  "C": "0.0034720700448926",
+  "eight_to_t": "7.942448277269",
+  "loss_per_dimension_at_least": "0.442448277269",
+  "valid_for_C_below": "0.031036468130"
+ },
+ "paid_jobs": 2920,
+ "quotient": {
+  "certificate": "2 w(V) <= 15 dim V for every relation subspace V (mod V0)",
+  "distinct_rows": 1764,
+  "elements": 3719,
+  "max_single_row_mass": 7,
+  "removed_by_V0": 18,
+  "tight": 0
+ },
+ "source": {
+  "distinct_rows": 1773,
+  "elements": 3791,
+  "max_gain_mass": 0,
+  "tight": [
+   [
+    [
+     "COPY",
+     7,
+     4873
+    ],
+    [
+     "MOVE",
+     1,
+     2454
+    ]
+   ],
+   [
+    [
+     "COPY",
+     7,
+     4938
+    ],
+    [
+     "MOVE",
+     1,
+     2447
+    ]
+   ],
+   [
+    [
+     "COPY",
+     7,
+     4995
+    ],
+    [
+     "MOVE",
+     1,
+     2440
+    ]
+   ],
+   [
+    [
+     "COPY",
+     7,
+     5052
+    ],
+    [
+     "MOVE",
+     1,
+     2433
+    ]
+   ],
+   [
+    [
+     "COPY",
+     7,
+     5117
+    ],
+    [
+     "MOVE",
+     1,
+     2426
+    ]
+   ],
+   [
+    [
+     "COPY",
+     7,
+     5182
+    ],
+    [
+     "MOVE",
+     1,
+     2419
+    ]
+   ],
+   [
+    [
+     "COPY",
+     7,
+     5239
+    ],
+    [
+     "MOVE",
+     1,
+     2412
+    ]
+   ],
+   [
+    [
+     "COPY",
+     7,
+     5296
+    ],
+    [
+     "MOVE",
+     1,
+     2405
+    ]
+   ],
+   [
+    [
+     "COPY",
+     7,
+     5353
+    ],
+    [
+     "MOVE",
+     1,
+     2398
+    ]
+   ]
+  ]
+ }
+}

research/bit-relation-subspaces/SOURCES.json

@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "base_commit": "1a3ced60b2f7a46bc70280a04f2eeb8ca027c700",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446",
+      "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/kappa-rebuild/bit/sources/pr589-regenerated/WORD.json.gz",
+      "usage": "input",
+      "git_blob": "85a4499bf9e4911a705d50567a2c2ef6cf23739a",
+      "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f"
+    },
+    {
+      "path": "research/kappa-rebuild/bit/sources/pr589-regenerated/records/249-records.bin",
+      "usage": "input",
+      "git_blob": "bdf9ab4ca0fd74cde6837f95f5f4e88133704e0e",
+      "sha256": "ea44aa047a2a9cf034de8b56b2166c49cf2dbdf9cd9ed6a20299a4f2b05ef09a"
+    },
+    {
+      "path": "research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz",
+      "usage": "input",
+      "git_blob": "46d929df83817b85a5387bcdb9745e0627d6366e",
+      "sha256": "7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05"
+    },
+    {
+      "path": "research/eight-owned-relations/RELATIONS.json",
+      "usage": "input",
+      "git_blob": "f558b9ddd903badb2301944cb978824b32ad42f7",
+      "sha256": "bc9ba05595497f399da5e5a548b2d2c83696e539fa1257ab7e2cb49d438cd9dd"
+    }
+  ]
+}