From 37996b4cba8ecb946d5f438e664c3f67ad0619d2 Mon Sep 17 00:00:00 2001 From: Matarener <52912325+Matarener@users.noreply.github.com> Date: Sat, 24 Oct 2026 15:15:19 +0300 Subject: [PATCH 1/3] Certify that no owned-helper relation subspace pays on the BIT word after #5421 (negative result, no new kappa) On the reverse PR589 BIT word, a matroid-union certificate shows that every relation subspace V removes paid rank mass w(V) <= 7.5 dim V modulo #5421's nine relations, so each extra relation dimension loses at least 0.44 raw moment per local call. Calibration recovers exactly #5421's nine relations as the only tight subspaces of the source word. Co-Authored-By: Claude Opus 5.5 (1M context) --- research/bit-relation-subspaces/README.md | 83 +++++ research/bit-relation-subspaces/RESULT.json | 147 ++++++++ research/bit-relation-subspaces/SOURCES.json | 30 ++ research/bit-relation-subspaces/TASK.json | 67 ++++ research/bit-relation-subspaces/VERIFY.json | 32 ++ .../bit-relation-subspaces/test_verify.py | 57 ++++ research/bit-relation-subspaces/verify.py | 316 ++++++++++++++++++ 7 files changed, 732 insertions(+) create mode 100644 research/bit-relation-subspaces/README.md create mode 100644 research/bit-relation-subspaces/RESULT.json create mode 100644 research/bit-relation-subspaces/SOURCES.json create mode 100644 research/bit-relation-subspaces/TASK.json create mode 100644 research/bit-relation-subspaces/VERIFY.json create mode 100644 research/bit-relation-subspaces/test_verify.py create mode 100644 research/bit-relation-subspaces/verify.py diff --git a/research/bit-relation-subspaces/README.md b/research/bit-relation-subspaces/README.md new file mode 100644 index 0000000000..b92547c097 --- /dev/null +++ b/research/bit-relation-subspaces/README.md @@ -0,0 +1,83 @@ +# No further BIT helper relation subspace after #5421 + +**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. + +## 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/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`. 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. +- Does the same certificate close relation subspaces on the selected complex word, which is the binding + side? Complex relation searches so far tested single relations. A subspace of density above `9^t` there + would raise κ directly. The partition must run over Q with rank-9 targets. + +## Credit + +DreamingOfClouds (PR #589) and eumemic (PR #555) supplied the source word and port construction. +Ali Romman's PR #5421 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. diff --git a/research/bit-relation-subspaces/RESULT.json b/research/bit-relation-subspaces/RESULT.json new file mode 100644 index 0000000000..56584f3124 --- /dev/null +++ b/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 + ] + ] + ] + } +} diff --git a/research/bit-relation-subspaces/SOURCES.json b/research/bit-relation-subspaces/SOURCES.json new file mode 100644 index 0000000000..d3c5c7d6c4 --- /dev/null +++ b/research/bit-relation-subspaces/SOURCES.json @@ -0,0 +1,30 @@ +{ + "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" + } + ] +} diff --git a/research/bit-relation-subspaces/TASK.json b/research/bit-relation-subspaces/TASK.json new file mode 100644 index 0000000000..465fe0518c --- /dev/null +++ b/research/bit-relation-subspaces/TASK.json @@ -0,0 +1,67 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 7, + "base_commit": "1a3ced60b2f7a46bc70280a04f2eeb8ca027c700", + "original_card": { + "id": "bit-helper-contract", + "question": "Can one precisely specified helper-mixing word satisfy a replacement for the inherited H2/K interface?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/r439-bsection-stars-seed01/README.md", + "research/r439-copy-path-sharing-barrier/README.md" + ], + "methods": [ + "Derive a replacement interface lemma and price its implementation.", + "Seek an exact dirty-input or chronological-cut counterexample to the proposed replacement." + ], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/r439-bsection-stars-seed01/verify.py" + ], + "expected": "PASS_R439_BSECTION_STARS", + "inspect": "Compare the two false H2/K flags with the unchanged paid profile in its README.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write one replacement H2/K implication for a single helper-star operation, then try to falsify it on dirty inputs.", + "bottleneck_link": "A legitimate replacement could admit a cheaper bit circuit; scalar savings alone do not alter the selected moment.", + "allowed_variations": [ + "Choose one helper-star or quartet instance; narrow to one boundary implication." + ], + "scope_change_triggers": [ + "Changing only source count or scalar addition count without an interface argument." + ], + "overlap_terms": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D", + "helper-star" + ] + }, + "scope_status": "changed", + "actual_scope": "On the PR589 reverse BIT word used by PR #5421, can any subspace of owned helper relations (any dimension, any combination, not only single relations) make more paid jobs free than it costs in lost rank-8 helper targets, after #5421's nine COPY relations?", + "scope_change_reason": "PR #5421 removes nine COPY jobs with nine owned helper relations and states that a further BIT gain needs a new relation space; PR #5428 (target 6) proposes systematic relation-space selection. This package answers that question exactly for the fixed source word by a matroid-union certificate instead of a search, rather than constructing a new helper interface.", + "bottleneck_link": "Side result; no new kappa and no new BIT saving. It closes the relation-space extension of #5421 on its own word: every additional relation dimension loses at least 0.44 raw moment per local call.", + "budget_minutes": 120, + "stop_rule": "Stop at the exact certificate for the fixed word; do not change the chronology, the word or the helper inventory.", + "outcome": "negative-result", + "evidence": "verify.py replays the reversed PR589 records over GF(2) (2,920 paid jobs, 2,384 with a legal relation row), recovers exactly #5421's nine relations as the only tight subspaces of the source word, and certifies modulo them that 2E' splits into 15 linearly independent sets, i.e. w(V) <= 7.5 dim V < 8^t dim V for every relation subspace V; two live controls fail as required and test_verify.py rejects four mutations.", + "author": "Mark (Matarener)", + "ai_assistance": "Prepared with substantial Claude Code (Claude) assistance.", + "open_questions": [ + { + "question": "Does a changed chronological order or a different BIT word admit a relation subspace of density above 8^t?", + "why_it_matters": "This certificate fixes the PR589 operation order; the density bound is a property of the job rows of this word.", + "first_step": "Run the same 8- and 15-part splits on the job rows of any changed BIT word before searching relations on it.", + "blocked_by": "No changed BIT word with an admitted invoice is available as a frozen input." + }, + { + "question": "Does the same certificate close relation subspaces on the selected complex word (the binding side)?", + "why_it_matters": "Complex relation searches so far tested single relations; a relation subspace of density above 9^t there would raise kappa directly.", + "first_step": "Build the rational job-row multiset of the selected complex caller and run the matroid partition over Q.", + "blocked_by": "Rows are rational and the helper targets have rank 9; the partition must run over Q with the matching target rank." + } + ] +} diff --git a/research/bit-relation-subspaces/VERIFY.json b/research/bit-relation-subspaces/VERIFY.json new file mode 100644 index 0000000000..f1459a0caa --- /dev/null +++ b/research/bit-relation-subspaces/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/kappa-rebuild/bit/sources/pr589-regenerated/WORD.json.gz", + "research/kappa-rebuild/bit/sources/pr589-regenerated/records/249-records.bin" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Pinned inputs; source reverse identity and #5421 source paid profile; calibration: source E' splits into 8 independent sets and the tight subspaces are exactly #5421's nine COPY+MOVE relations; modulo them E' splits into 8 sets with no tight row and 2E' splits into 15 independent sets (w(V) <= 7.5 dim V); moment loss >= 0.4424 per dimension at C = 0.00347207; live controls (source 2E' into 15 fails, an injected rank-1 job on a COPY row breaks the 8-split); stored RESULT.json equals the rebuild." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 300, + "checks": "Rejecting controls: drifted input hash, corrupted MOVE rank in the source records, a dependent part in the partition certificate, tampered RESULT.json." + } + ] +} diff --git a/research/bit-relation-subspaces/test_verify.py b/research/bit-relation-subspaces/test_verify.py new file mode 100644 index 0000000000..42fd4253b9 --- /dev/null +++ b/research/bit-relation-subspaces/test_verify.py @@ -0,0 +1,57 @@ +"""Rejecting controls for verify.py. Each mutation must raise SystemExit('FAIL...').""" +import json +import sys +from pathlib import Path + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import verify as V # noqa: E402 + + +def rejects(name, fn): + try: + fn() + except SystemExit as exc: + if not str(exc).startswith('FAIL'): + raise + print('rejected:', name) + return + raise AssertionError('control accepted: ' + name) + + +def drift(): + rows = json.loads((HERE / 'SOURCES.json').read_text(encoding='utf-8')) + row = next(r for r in rows['files'] if r['usage'] == 'input') + data = (V.ROOT / row['path']).read_bytes() + V.require(V.hashlib.sha256(data).hexdigest() == '0' * 64, 'input drift: ' + row['path']) + + +def corrupted_record(): + word, records = V.load() + i = next(k for k, r in enumerate(records) if r[0] == 0 and r[4] == 1) + r = list(records[i]); r[4] = 2; records = records[:i] + [tuple(r)] + records[i + 1:] + V.paid_jobs(word, records) + + +def dependent_part(): + word, records = V.load() + _, legal = V.paid_jobs(word, records) + rows, mass, per, elems = V.multiset(legal, {}) + ok, P = V.split(elems, 8) + e, twin = next((a, b) for a in range(len(P.elems)) for b in range(a + 1, a + 8) + if b < len(P.elems) and P.elems[a] == P.elems[b]) + k, other = P.where[e], P.where[twin] + P.members[other].remove(twin); P.members[k].append(twin) + V.require(P.check(), 'every part independent and exact cover') + + +def tampered_result(): + stored = json.loads((HERE / 'RESULT.json').read_text(encoding='utf-8')) + stored['quotient']['tight'] = 1 + V.require(stored['quotient']['tight'] == 0, 'stored RESULT.json equals the rebuild') + + +for name, fn in [('drifted input hash', drift), ('corrupted MOVE rank in the source records', corrupted_record), + ('dependent part in the partition certificate', dependent_part), ('tampered RESULT.json', tampered_result)]: + rejects(name, fn) +print('PASS_BIT_RELATION_SUBSPACES_CONTROLS') diff --git a/research/bit-relation-subspaces/verify.py b/research/bit-relation-subspaces/verify.py new file mode 100644 index 0000000000..f2b9721d6b --- /dev/null +++ b/research/bit-relation-subspaces/verify.py @@ -0,0 +1,316 @@ +#!/usr/bin/env python3 +"""No further owned-helper relation subspace pays on the PR589 reverse BIT word after #5421's nine relations. + +Standard library only; well under a minute. Reads the PR589 regenerated BIT source (WORD.json.gz and the +249-records.bin event list), pinned by SHA256 in SOURCES.json. + +Model (exactly the one of PR #5421, Ali Romman, generalised from single relations to relation subspaces): + * replay the source records in reverse order over GF(2) with 661 independent entry symbols + (111 X, 111 Y, 439 helpers); every paid job is a MOVE of rank r > 0 or a COPY entrance (rank 7); + * a set of owned helper relations is a subspace V of entry forms whose support lies in fields with the full + entrance frame and which has helper pivots; owning the pivots and setting V to zero makes a job free iff + the binary row of its moved value lies in V; each dimension of V loses one rank-8 helper target; + * per local call the raw moment changes by sum_{removed jobs} r^t - 8^t dim V, t = 1 - C; the p16/a7 + controller multiplies this by its eighteen full calls (thin queries and idle transforms are unchanged). +Legality (frames, helper pivots) is only relaxed below, so every bound is also a bound for legal V. + +Certificate (matroid union theorem, Edmonds / Nash-Williams): let E' be the multiset of job rows, each row +repeated rank times. If m copies of E' split into p linearly independent sets then m w(V) <= p dim V for every +subspace V, where w(V) is the paid rank mass with rows in V. Tight subspaces (w = 8 dim) are exactly the rows to +which an extra element cannot be added by an Edmonds augmenting path. + +Checks: + 1. pinned inputs; the source paid profile {1:1323,2:1342,3:79,4:44,5:102,6:11,7:19} of #5421; + 2. calibration on the source word: E' splits into 8 independent sets (max_V w - 8 dim = 0), and the tight + subspaces are exactly nine one-dimensional ones, each = one COPY (H7) + one MOVE (H1): #5421's relations; + 3. modulo those nine relations V0: E' still splits into 8 sets and no row is tight (w(V) < 8 dim V), and + 2E' splits into 15 independent sets, so w(V) <= 7.5 dim V for every V of every dimension; + 4. since r^t <= r for r >= 1, the moment change is <= (7.5 - 8^t) dim V < 0 for every C < log(8/7.5)/log 8; + 5. live controls: on the source word 2E' does not split into 15 sets, and an injected rank-1 job on a #5421 + COPY row makes E' not 8-splittable; + 6. the stored RESULT.json equals the rebuild. +Usage: python3 -I -B verify.py [--write] +""" +import argparse, collections, gzip, hashlib, json, struct, sys +from decimal import Decimal as D, getcontext +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent +SRC = ROOT / 'research' / 'kappa-rebuild' / 'bit' / 'sources' / 'pr589-regenerated' +SIZE, PORTS = 661, 111 +SOURCE_PAID = {1: 1323, 2: 1342, 3: 79, 4: 44, 5: 102, 6: 11, 7: 19} +C_5421 = D('0.0034720700448926') # raw moment root of #5421's new controller +getcontext().prec = 50 + + +def require(ok, message): + if not ok: + raise SystemExit('FAIL: ' + message) + + +def pinned_inputs(): + rows = json.loads((HERE / 'SOURCES.json').read_text(encoding='utf-8'))['files'] + for row in rows: + if row['usage'] == 'input': + data = (ROOT / row['path']).read_bytes() + require(hashlib.sha256(data).hexdigest() == row['sha256'], 'input drift: ' + row['path']) + + +def load(): + word = json.loads(gzip.decompress((SRC / 'WORD.json.gz').read_bytes())) + records = list(struct.iter_unpack('<6i', (SRC / 'records' / '249-records.bin').read_bytes())) + return word, records + + +def paid_jobs(word, records): + """Reverse replay over GF(2); every paid job with the binary row of its moved value.""" + rows = [1 << i for i in range(SIZE)] + [0] + jobs = [] + for idx, (op, x, y, a, b, _) in enumerate(reversed(records)): + if op == 0: + if b: + jobs.append((idx, 'MOVE', b, rows[x])) + elif op == 1: + if a & 1: + rows[x] ^= rows[y] + elif op == 3: + require(y == SIZE and rows[SIZE] == 0, 'source COPY entrance into the empty centre') + jobs.append((idx, 'COPY', 7, rows[x])) + rows[SIZE] = rows[x] + elif op == 2: + require(y == SIZE and rows[x] == rows[SIZE], 'source COPY exit') + rows[SIZE] = 0 + else: + require(False, 'unknown source record') + want = [(1 << i) ^ ((1 << (i - PORTS)) if PORTS <= i < 2 * PORTS else 0) for i in range(SIZE)] + [0] + require(rows == want, 'source reverse identity (X,Y) -> (X,Y+X), helpers fixed') + require(dict(collections.Counter(j[2] for j in jobs)) == SOURCE_PAID, 'source paid profile of #5421') + full = sum(1 << i for i in range(SIZE) if word['final'][i] == 1) + helpers = sum(1 << i for i in range(2 * PORTS, SIZE)) + legal = [j for j in jobs if j[3] and j[3] & ~full == 0 and j[3] & helpers] + return jobs, legal + + +def echelon(rows): + b = {} + for r in rows: + while r: + h = r.bit_length() - 1 + if h in b: + r ^= b[h] + else: + b[h] = r + break + return b + + +def reduce(b, r): + while r: + h = r.bit_length() - 1 + v = b.get(h) + if v is None: + return r + r ^= v + return 0 + + +class Partition: + """Matroid partition of a multiset of GF(2) rows into k linearly independent parts (Edmonds).""" + + def __init__(self, elems, k): + self.elems, self.k = elems, k + self.members = [[] for _ in range(k)] + self.basis = [None] * k + self.where = {} + + def _build(self, k): + b = {} + for idx, e in enumerate(self.members[k]): + r, c = self.elems[e], 1 << idx + while r: + h = r.bit_length() - 1 + if h in b: + v, cv = b[h]; r ^= v; c ^= cv + else: + b[h] = (r, c); break + self.basis[k] = b + + def circuit(self, k, e): + if self.basis[k] is None: + self._build(k) + b, r, c = self.basis[k], self.elems[e], 0 + while r: + h = r.bit_length() - 1 + t = b.get(h) + if t is None: + return None + r ^= t[0]; c ^= t[1] + out, i = [], 0 + while c: + if c & 1: + out.append(self.members[k][i]) + c >>= 1; i += 1 + return out + + def augment(self, x): + """Insert element x by a shortest augmenting path; return (True, None) or (False, reachable set).""" + prev, queue, qi = {x: None}, [x], 0 + order = sorted(range(self.k), key=lambda k: len(self.members[k])) + while qi < len(queue): + y = queue[qi]; qi += 1 + for k in order: + if self.where.get(y) == k: + continue + circ = self.circuit(k, y) + if circ is None: + moves, z = [(y, k)], y + while prev[z] is not None: + py, pk = prev[z]; moves.append((py, pk)); z = py + touched = set() + for z, kk in moves: + old = self.where.get(z) + if old is not None: + self.members[old].remove(z); touched.add(old) + for z, kk in moves: + self.members[kk].append(z); self.where[z] = kk; touched.add(kk) + for t in touched: + self.basis[t] = None + return True, None + for z in circ: + if z not in prev: + prev[z] = (y, k); queue.append(z) + return False, set(queue) + + def check(self): + """Independent re-check: every part independent and the parts cover the multiset exactly once.""" + independent = all(len(echelon([self.elems[e] for e in m])) == len(m) for m in self.members) + cover = sorted(e for m in self.members for e in m) == list(range(len(self.elems))) + return independent and cover + + +def multiset(legal, V0): + """Rows modulo V0 with their paid rank mass; returns (distinct rows, mass, jobs per row, element list).""" + per = collections.defaultdict(list) + for j in legal: + q = reduce(V0, j[3]) + if q: + per[q].append(j) + rows = sorted(per) + mass = {q: sum(j[2] for j in per[q]) for q in rows} + elems = [q for q in rows for _ in range(mass[q])] + return rows, mass, per, elems + + +def split(elems, k, copies=1, base_k=8): + """Try to split `copies` copies of elems into k independent sets; returns (ok, Partition).""" + allel = elems * copies + if copies == 1: + P = Partition(allel, k) + fails = 0 + for e in sorted(range(len(allel)), key=lambda e: allel[e]): + ok, _ = P.augment(e) + fails += not ok + return fails == 0 and P.check(), P + ok8, P8 = split(elems, base_k) + if not ok8: + return False, P8 + groups, n = P8.members, len(elems) + parts = [[c * n + e for e in g] for c in range(copies) for g in groups] + parts.sort(key=len) + loose = [e for g in parts[:base_k * copies - k] for e in g] + P = Partition(allel, k) + for kk, g in enumerate(parts[base_k * copies - k:]): + P.members[kk] = list(g) + for e in g: + P.where[e] = kk + fails = 0 + for e in loose: + ok, _ = P.augment(e) + fails += not ok + return fails == 0 and P.check(), P + + +def tight_flats(rows, per, P): + """Rows lying in a subspace with w = 8 dim: an extra copy cannot be inserted. Returns the minimal flats.""" + flats = {} + base_members = [list(m) for m in P.members] + base_where = dict(P.where) + for q in rows: + P.elems.append(q); x = len(P.elems) - 1 + ok, reach = P.augment(x) + if not ok: + span = echelon([P.elems[e] for e in reach]) + inside = [r for r in rows if reduce(span, r) == 0] + key = tuple(sorted(span)) + flats[key] = dict(dim=len(span), mass=sum(j[2] for r in inside for j in per[r]), + jobs=sorted([j[1], j[2], j[0]] for r in inside for j in per[r])) + P.elems.pop() + P.members = [list(m) for m in base_members]; P.basis = [None] * P.k + P.where = dict(base_where) + return sorted(flats.values(), key=lambda f: f['jobs']) + + +def build(): + pinned_inputs() + word, records = load() + jobs, legal = paid_jobs(word, records) + out = dict(paid_jobs=len(jobs), legal_jobs=len(legal), legal_profile=dict(sorted(collections.Counter(j[2] for j in legal).items())), + already_zero=sum(1 for j in jobs if not j[3])) + # 2. calibration on the source word + rows, mass, per, elems = multiset(legal, {}) + ok, P = split(elems, 8) + require(ok, 'source E\' splits into 8 independent sets') + flats = tight_flats(rows, per, P) + require(len(flats) == 9 and all(f['dim'] == 1 and f['mass'] == 8 and [j[:2] for j in f['jobs']] == [['COPY', 7], ['MOVE', 1]] + for f in flats), 'tight subspaces on the source word are exactly the nine #5421 relations') + out['source'] = dict(distinct_rows=len(rows), elements=len(elems), max_gain_mass=0, + tight=[f['jobs'] for f in flats]) + # 3. modulo the nine relations + V0 = echelon([j[3] for j in legal if j[1] == 'COPY']) + require(len(V0) == 9, 'nine independent #5421 relation forms') + rows, mass, per, elems = multiset(legal, V0) + ok, P = split(elems, 8) + require(ok, 'E\' modulo V0 splits into 8 independent sets') + flats = tight_flats(rows, per, P) + require(flats == [], 'no tight subspace modulo V0') + ok15, _ = split(elems, 15, copies=2) + require(ok15, '2E\' modulo V0 splits into 15 independent sets') + out['quotient'] = dict(distinct_rows=len(rows), elements=len(elems), removed_by_V0=sum(1 for j in legal if reduce(V0, j[3]) == 0), + max_single_row_mass=max(mass.values()), tight=0, + certificate='2 w(V) <= 15 dim V for every relation subspace V (mod V0)') + # 4. moment + t = 1 - C_5421 + eight_t = (t * D(8).ln()).exp() + threshold = (D(8) / D('7.5')).ln() / D(8).ln() + require(D('7.5') < eight_t and C_5421 < threshold, 'density 7.5 is below 8^t') + out['moment'] = dict(C=str(C_5421), eight_to_t=str(eight_t.quantize(D('1e-12'))), + loss_per_dimension_at_least=str((eight_t - D('7.5')).quantize(D('1e-12'))), + valid_for_C_below=str(threshold.quantize(D('1e-12')))) + # 5. live controls + rows_s, mass_s, per_s, elems_s = multiset(legal, {}) + ok_s, _ = split(elems_s, 15, copies=2) + require(not ok_s, 'control: source word 2E\' must not split into 15 sets (tight #5421 relations)') + copy_row = next(j[3] for j in legal if j[1] == 'COPY') + bad = list(elems_s) + [copy_row] + ok_b, _ = split(bad, 8) + require(not ok_b, 'control: an extra rank-1 job on a #5421 COPY row must break the 8-split') + out['controls'] = dict(source_2E_into_15='rejected', injected_rank1_on_copy_row='rejected') + return out + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument('--write', action='store_true') + args = ap.parse_args() + result = build() + path = HERE / 'RESULT.json' + text = json.dumps(result, indent=1, sort_keys=True) + '\n' + if args.write: + path.write_bytes(text.encode('utf-8')) + require(path.exists() and json.loads(path.read_text(encoding='utf-8')) == json.loads(text), 'stored RESULT.json equals the rebuild') + print('PASS_BIT_RELATION_SUBSPACES_NO_FURTHER_GAIN_AFTER_5421') + + +if __name__ == '__main__': + main() From 80e3ef2781fc0e1ee3212a5efd63a2a90802aba8 Mon Sep 17 00:00:00 2001 From: Matarener <52912325+Matarener@users.noreply.github.com> Date: Sat, 24 Oct 2026 13:35:00 +0300 Subject: [PATCH 2/3] Point the current CI section at frontier5413 (exact repair from #5420) Canonical main still names make frontier4610-verify while the selected record requires frontier5413-verify, so the shared onboarding test fails before any package replay. This reuses byte-for-byte the docs/ci-verification.md repair of #5420 (head baa8fbb8345c2fab0bc213479539c338d4c80443, Clear1nsight); no scientific file changes. Co-Authored-By: Claude Opus 5.5 (1M context) --- docs/ci-verification.md | 34 +++++++++++++++++++++++++++++++++- 1 file changed, 33 insertions(+), 1 deletion(-) diff --git a/docs/ci-verification.md b/docs/ci-verification.md index 494b7ca1d4..3bf623230e 100644 --- a/docs/ci-verification.md +++ b/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 From 285013bb011c41899bd346632aed03a9c5310917 Mon Sep 17 00:00:00 2001 From: Matarener <52912325+Matarener@users.noreply.github.com> Date: Sat, 24 Oct 2026 15:26:32 +0300 Subject: [PATCH 3/3] Add part 2: no further owned relation pays on the complex #4610 word after #5383 On the complex #4610 backward word (local word of the selected #5383 -> #5398 -> #5413 chain), #5383's eight relations free all eight centres and eight zero-site climbs; modulo them the 155 remaining pure-cold climb rows are linearly independent over Q with rank mass <= 3, so every further relation subspace loses at least 5.94 raw moment per dimension. Co-Authored-By: Claude Opus 5.5 (1M context) --- research/bit-relation-subspaces/README.md | 38 +++- .../RESULT-COMPLEX.json | 48 +++++ research/bit-relation-subspaces/SOURCES.json | 12 ++ research/bit-relation-subspaces/TASK.json | 14 +- research/bit-relation-subspaces/VERIFY.json | 16 +- research/bit-relation-subspaces/complex.py | 189 ++++++++++++++++++ .../bit-relation-subspaces/test_verify.py | 34 +++- 7 files changed, 335 insertions(+), 16 deletions(-) create mode 100644 research/bit-relation-subspaces/RESULT-COMPLEX.json create mode 100644 research/bit-relation-subspaces/complex.py diff --git a/research/bit-relation-subspaces/README.md b/research/bit-relation-subspaces/README.md index b92547c097..e1111d39f1 100644 --- a/research/bit-relation-subspaces/README.md +++ b/research/bit-relation-subspaces/README.md @@ -1,4 +1,4 @@ -# No further BIT helper relation subspace after #5421 +# No further owned-helper relation subspace after #5421 (BIT) and #5383 (complex) **Negative result; no new κ and no new BIT saving.** @@ -47,16 +47,43 @@ A row in a tight subspace (`w = 8 dim`) is one for which an extra copy cannot be 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`. The controls print +`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 @@ -71,13 +98,12 @@ removes. The nine relations come from the source word itself, so #5421 is not a - 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. -- Does the same certificate close relation subspaces on the selected complex word, which is the binding - side? Complex relation searches so far tested single relations. A subspace of density above `9^t` there - would raise κ directly. The partition must run over Q with rank-9 targets. +- 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. -Ali Romman's PR #5421 and PR #5383 supplied the owned-helper relation method that this package +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. diff --git a/research/bit-relation-subspaces/RESULT-COMPLEX.json b/research/bit-relation-subspaces/RESULT-COMPLEX.json new file mode 100644 index 0000000000..e4d7c9dfd9 --- /dev/null +++ b/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 +} diff --git a/research/bit-relation-subspaces/SOURCES.json b/research/bit-relation-subspaces/SOURCES.json index d3c5c7d6c4..b1ee7df338 100644 --- a/research/bit-relation-subspaces/SOURCES.json +++ b/research/bit-relation-subspaces/SOURCES.json @@ -25,6 +25,18 @@ "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" } ] } diff --git a/research/bit-relation-subspaces/TASK.json b/research/bit-relation-subspaces/TASK.json index 465fe0518c..34fd629524 100644 --- a/research/bit-relation-subspaces/TASK.json +++ b/research/bit-relation-subspaces/TASK.json @@ -41,13 +41,13 @@ ] }, "scope_status": "changed", - "actual_scope": "On the PR589 reverse BIT word used by PR #5421, can any subspace of owned helper relations (any dimension, any combination, not only single relations) make more paid jobs free than it costs in lost rank-8 helper targets, after #5421's nine COPY relations?", + "actual_scope": "On the PR589 reverse BIT word used by PR #5421, can any subspace of owned helper relations (any dimension, any combination, not only single relations) make more paid jobs free than it costs in lost rank-8 helper targets, after #5421's nine COPY relations? Part 2: the same question on the complex #4610 backward word (the local word of the selected #5383 -> #5398 -> #5413 chain) after #5383's eight relations.", "scope_change_reason": "PR #5421 removes nine COPY jobs with nine owned helper relations and states that a further BIT gain needs a new relation space; PR #5428 (target 6) proposes systematic relation-space selection. This package answers that question exactly for the fixed source word by a matroid-union certificate instead of a search, rather than constructing a new helper interface.", - "bottleneck_link": "Side result; no new kappa and no new BIT saving. It closes the relation-space extension of #5421 on its own word: every additional relation dimension loses at least 0.44 raw moment per local call.", + "bottleneck_link": "Side result; no new kappa and no new BIT saving. It closes the relation-space extension of #5421 on its BIT word (each extra relation dimension loses >= 0.44 raw moment per local call) and of #5383 on the binding complex word (>= 5.94).", "budget_minutes": 120, "stop_rule": "Stop at the exact certificate for the fixed word; do not change the chronology, the word or the helper inventory.", "outcome": "negative-result", - "evidence": "verify.py replays the reversed PR589 records over GF(2) (2,920 paid jobs, 2,384 with a legal relation row), recovers exactly #5421's nine relations as the only tight subspaces of the source word, and certifies modulo them that 2E' splits into 15 linearly independent sets, i.e. w(V) <= 7.5 dim V < 8^t dim V for every relation subspace V; two live controls fail as required and test_verify.py rejects four mutations.", + "evidence": "verify.py replays the reversed PR589 records over GF(2) (2,920 paid jobs, 2,384 with a legal relation row), recovers exactly #5421's nine relations as the only tight subspaces of the source word, and certifies modulo them that 2E' splits into 15 linearly independent sets, i.e. w(V) <= 7.5 dim V < 8^t dim V for every relation subspace V; two live controls fail as required and test_verify.py rejects four mutations. Part 2: complex.py frees all eight centres and eight zero-site climbs with #5383's relations and proves exactly over Q that the 155 remaining pure-cold climb rows are linearly independent with rank mass <= 3, so any further relation loses >= 5.94 per dimension; test_verify.py adds three complex mutations.", "author": "Mark (Matarener)", "ai_assistance": "Prepared with substantial Claude Code (Claude) assistance.", "open_questions": [ @@ -58,10 +58,10 @@ "blocked_by": "No changed BIT word with an admitted invoice is available as a frozen input." }, { - "question": "Does the same certificate close relation subspaces on the selected complex word (the binding side)?", - "why_it_matters": "Complex relation searches so far tested single relations; a relation subspace of density above 9^t there would raise kappa directly.", - "first_step": "Build the rational job-row multiset of the selected complex caller and run the matroid partition over Q.", - "blocked_by": "Rows are rational and the helper targets have rank 9; the partition must run over Q with the matching target rank." + "question": "Can a complex relation set that does not contain #5383's eight relations beat them?", + "why_it_matters": "Part 2 certifies only extensions of the selected relations; a different basis could free other snapshot options.", + "first_step": "Enumerate one snapshot option per centre (at most 8 centres) and run the same independence test on each choice.", + "blocked_by": "Snapshot options are alternatives for one centre, so they are not single matroid elements; the research/owned-relation-exhaustion centre-exchange cap already limits this family." } ] } diff --git a/research/bit-relation-subspaces/VERIFY.json b/research/bit-relation-subspaces/VERIFY.json index f1459a0caa..a8399c6468 100644 --- a/research/bit-relation-subspaces/VERIFY.json +++ b/research/bit-relation-subspaces/VERIFY.json @@ -5,7 +5,9 @@ "requirements": [], "inputs": [ "research/kappa-rebuild/bit/sources/pr589-regenerated/WORD.json.gz", - "research/kappa-rebuild/bit/sources/pr589-regenerated/records/249-records.bin" + "research/kappa-rebuild/bit/sources/pr589-regenerated/records/249-records.bin", + "research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz", + "research/eight-owned-relations/RELATIONS.json" ], "commands": [ { @@ -18,6 +20,16 @@ "timeout_seconds": 300, "checks": "Pinned inputs; source reverse identity and #5421 source paid profile; calibration: source E' splits into 8 independent sets and the tight subspaces are exactly #5421's nine COPY+MOVE relations; modulo them E' splits into 8 sets with no tight row and 2E' splits into 15 independent sets (w(V) <= 7.5 dim V); moment loss >= 0.4424 per dimension at C = 0.00347207; live controls (source 2E' into 15 fails, an injected rank-1 job on a COPY row breaks the 8-split); stored RESULT.json equals the rebuild." }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/complex.py" + ], + "timeout_seconds": 300, + "checks": "Part 2 (complex #4610 backward word): pinned inputs; backward paid profile; #5383's eight relations free all eight centres and exactly eight rank-1 zero-site climbs; modulo them the 155 remaining pure-cold climb rows are linearly independent over Q with rank mass <= 3, so any further relation subspace frees <= 3 dim V (moment loss >= 5.94 per dimension at C = 0.003027288235); stored RESULT-COMPLEX.json equals the rebuild." + }, { "argv": [ "{python}", @@ -26,7 +38,7 @@ "{package}/test_verify.py" ], "timeout_seconds": 300, - "checks": "Rejecting controls: drifted input hash, corrupted MOVE rank in the source records, a dependent part in the partition certificate, tampered RESULT.json." + "checks": "Rejecting controls: drifted input hash, corrupted MOVE rank in the source records, a dependent part in the partition certificate, tampered RESULT.json. Complex: one #5383 relation dropped, an injected dependent row, a corrupted climb rank." } ] } diff --git a/research/bit-relation-subspaces/complex.py b/research/bit-relation-subspaces/complex.py new file mode 100644 index 0000000000..de19c42e93 --- /dev/null +++ b/research/bit-relation-subspaces/complex.py @@ -0,0 +1,189 @@ +#!/usr/bin/env python3 +"""Part 2: no further owned cold-helper relation pays on the complex #4610 backward word after #5383's eight. + +Standard library only; a few seconds. Reads Cao Yifan's #4610 word +(research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz) and the eight owned relations of PR #5383 / #5387 +(research/eight-owned-relations/RELATIONS.json), both pinned by SHA256 in SOURCES.json. This is the local word of +the #5383 -> #5392 -> #5398 chain; the selected #5413 caller adds 144 paid and 144 target rank-8 jobs that cancel +rank by rank, so its relation question is this one. + +Model (the #5377/#5383 owned-relation model, extended from single relations to subspaces): + * replay the backward program exactly over Q with warp words (free group ring); cold helpers (start frame 0, + final frame 1, 326 of them, rank-9 targets) are free inputs and a relation subspace V lies in their span; + * a paid climb is free iff its row is a pure cold-helper combination lying in V; a centre job (rank 8) is free + iff row(centre) - row(Z) lies in V for some earlier snapshot Z of a field standing in its destination frame; + * each dimension of V costs one rank-9 target; per local call the raw moment changes by + sum_{removed} r^t - 9^t dim V. +Checks: + 1. pinned inputs; the backward paid profile {1:2201,2:412,3:510,4:127,5:40,8:8}; + 2. the eight #5383 relations V0 make all eight centres and exactly eight rank-1 zero-site climbs free; + 3. modulo V0 every remaining pure-cold climb row (155 rows, rank mass <= 3 each) is linearly independent over Q, + and no centre remains; hence any further subspace V removes at most 3 dim V of paid mass and the moment + change is <= (3 - 9^t) dim V < 0; + 4. the stored RESULT-COMPLEX.json equals the rebuild. +Usage: python3 -I -B complex.py [--write] +""" +import argparse, collections, gzip, hashlib, json +from decimal import Decimal as D, getcontext +from fractions import Fraction as Q +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent +WORD = ROOT / 'research' / 'kappa-round3-warp-20261022' / 'ACTUAL-WORD.json.gz' +RELATIONS = ROOT / 'research' / 'eight-owned-relations' / 'RELATIONS.json' +BACKWARD_PAID = {1: 2201, 2: 412, 3: 510, 4: 127, 5: 40, 8: 8} +C_SELECTED = D('0.003027288235') +NL = 632 +getcontext().prec = 50 + + +def require(ok, message): + if not ok: + raise SystemExit('FAIL: ' + message) + + +def pinned_inputs(): + rows = json.loads((HERE / 'SOURCES.json').read_text(encoding='utf-8'))['files'] + for row in rows: + if row['usage'] == 'input': + data = (ROOT / row['path']).read_bytes() + require(hashlib.sha256(data).hexdigest() == row['sha256'], 'input drift: ' + row['path']) + + +def add_into(dst, src, q): + for k, v in src.items(): + nv = dst.get(k, 0) + q * v + if nv: + dst[k] = nv + else: + dst.pop(k, None) + + +def candidates(word): + """Pure cold-helper climb rows (A) and centre-minus-snapshot rows (B), as {cold index: Fraction}.""" + c = word['canonical']; fr = c['frames']; prog = word['programs']['backward'] + cold = {i for i in range(224, NL) if c['start'][i] == 0 and c['final'][i] == 1} + require(len(cold) == 326 and all(len(fr[c['final'][i]]) - len(fr[c['start'][i]]) == 9 for i in cold), + '326 cold helpers with rank-9 targets') + rows = {('L', i): {(('L', i), ()): Q(1)} for i in range(NL)}; rows[('C', 0)] = {(('C', 0), ()): Q(1)} + frames = {('L', i): c['start'][i] for i in range(NL)}; frames[('C', 0)] = None + centre_frames = {e[3] for e in prog if e[0] == 'center'} + snapshots = collections.defaultdict(list) + paid = collections.Counter(); A, B = [], [] + + def pure(row): + return bool(row) and all(wd == () and r[0] == 'L' and r[1] in cold for (r, wd) in row) + + def vec(row): + return {r[1]: q for (r, wd), q in row.items()} + + def snap(role): + if frames[role] in centre_frames and rows[role]: + snapshots[frames[role]].append(dict(rows[role])) + for t, e in enumerate(prog): + k = e[0] + if k == 'climb': + X = ('L', e[2]); paid[e[5]] += 1 + if pure(rows[X]): + A.append((t, e[5], vec(rows[X]))) + frames[X] = e[4]; snap(X) + elif k == 'center': + X = ('C', e[1]); paid[e[4]] += 1 + for rz in snapshots[e[3]]: + d = dict(rows[X]); add_into(d, rz, Q(-1)) + require(bool(d), 'no centre equals an earlier snapshot exactly') + if pure(d): + B.append((t, e[4], vec(d))) + frames[X] = e[3] + elif k == 'warp': + X = tuple(e[1]); op = e[2] + sym = (1 if op > 0 else -1) * (abs(op) + 10 ** 6) + rows[X] = {(r_, wd[1:] if wd and wd[0] == -sym else (sym,) + wd): q for (r_, wd), q in rows[X].items()} + frames[X] = e[4]; snap(X) + elif k == 'scalar': + g, frame = e[1], e[2]; d_ = tuple(g[1]) + if g[0] == 'clear': + rows[d_] = {}; frames[d_] = frame + elif g[0] == 'copy': + rows[d_] = dict(rows[tuple(g[2])]) + elif g[0] == 'add': + add_into(rows[d_], rows[tuple(g[2])], Q(g[3], g[4])) + elif g[0] == 'scale': + rows[d_] = {kk: Q(g[2], g[3]) * v for kk, v in rows[d_].items()} + snap(d_) + require(dict(paid) == BACKWARD_PAID, 'backward paid profile of the #4610 word') + return A, B + + +class Echelon: + """Exact rational row echelon on sparse rows {column: Fraction}.""" + + def __init__(self): + self.rows = {} + + def reduce(self, v): + v = dict(v) + while v: + col = min(v) + if col not in self.rows: + return v + f = v[col] + add_into(v, self.rows[col], -f) + return v + + def add(self, v): + v = self.reduce(v) + if not v: + return False + col = min(v); f = v[col] + self.rows[col] = {k: x / f for k, x in v.items()} + return True + + +def build(): + pinned_inputs() + word = json.loads(gzip.decompress(WORD.read_bytes())) + A, B = candidates(word) + rel = json.loads(RELATIONS.read_text(encoding='utf-8')) + V0 = Echelon() + for row in rel['rows']: + require(V0.add({int(k): Q(s) for k, s in row.items()}), 'eight independent #5383 relations') + require(len(V0.rows) == 8, 'V0 has dimension eight') + centres = sorted({t for t, _, v in B if not V0.reduce(v)}) + require(len(centres) == 8 and len({t for t, _, _ in B}) == 8, 'V0 frees all eight centre jobs') + zero_sites = sorted((t, r) for t, r, v in A if not V0.reduce(v)) + require(len(zero_sites) == 8 and all(r == 1 for _, r in zero_sites), 'V0 frees exactly eight rank-1 zero-site climbs') + rest = [(t, r, V0.reduce(v)) for t, r, v in A if V0.reduce(v)] + E = Echelon() + independent = all(E.add(v) for _, _, v in rest) + require(independent, 'remaining pure-cold climb rows are linearly independent modulo V0') + max_rank = max(r for _, r, _ in rest) + require(max_rank == 3, 'remaining rows have rank mass at most 3') + t_ = 1 - C_SELECTED + nine_t = (t_ * D(9).ln()).exp() + require(D(max_rank) < nine_t, 'density 3 is below 9^t') + return dict(cold_helpers=326, backward_paid=dict(sorted(BACKWARD_PAID.items())), + pure_cold_climbs=len(A), centre_snapshot_options=len(B), + V0_frees=dict(centres=centres, zero_site_climbs=[t for t, _ in zero_sites]), + remaining_rows=len(rest), remaining_rank=len(E.rows), remaining_profile=dict(sorted(collections.Counter(r for _, r, _ in rest).items())), + bound='every further relation subspace V frees paid mass <= 3 dim V', + moment=dict(C=str(C_SELECTED), nine_to_t=str(nine_t.quantize(D('1e-12'))), + loss_per_dimension_at_least=str((nine_t - 3).quantize(D('1e-12'))))) + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument('--write', action='store_true') + args = ap.parse_args() + result = build() + path = HERE / 'RESULT-COMPLEX.json' + text = json.dumps(result, indent=1, sort_keys=True) + '\n' + if args.write: + path.write_bytes(text.encode('utf-8')) + require(path.exists() and json.loads(path.read_text(encoding='utf-8')) == json.loads(text), 'stored RESULT-COMPLEX.json equals the rebuild') + print('PASS_COMPLEX_RELATION_SUBSPACES_NO_FURTHER_GAIN_AFTER_5383') + + +if __name__ == '__main__': + main() diff --git a/research/bit-relation-subspaces/test_verify.py b/research/bit-relation-subspaces/test_verify.py index 42fd4253b9..bddadbfe2c 100644 --- a/research/bit-relation-subspaces/test_verify.py +++ b/research/bit-relation-subspaces/test_verify.py @@ -51,7 +51,39 @@ def tampered_result(): V.require(stored['quotient']['tight'] == 0, 'stored RESULT.json equals the rebuild') +import complex as CX # noqa: E402 + + +def complex_missing_relation(): + rel = json.loads(CX.RELATIONS.read_text(encoding='utf-8')) + word = json.loads(CX.gzip.decompress(CX.WORD.read_bytes())) + A, B = CX.candidates(word) + V0 = CX.Echelon() + for row in rel['rows'][:-1]: + V0.add({int(k): CX.Q(s) for k, s in row.items()}) + CX.require(len({t for t, _, v in B if not V0.reduce(v)}) == 8, 'V0 frees all eight centre jobs') + + +def complex_dependent_row(): + word = json.loads(CX.gzip.decompress(CX.WORD.read_bytes())) + A, B = CX.candidates(word) + rows = [v for _, _, v in A] + rows.append({k: 2 * x for k, x in rows[0].items()}) + E = CX.Echelon() + CX.require(all(E.add(v) for v in rows), 'remaining pure-cold climb rows are linearly independent modulo V0') + + +def complex_corrupted_rank(): + word = json.loads(CX.gzip.decompress(CX.WORD.read_bytes())) + e = next(ev for ev in word['programs']['backward'] if ev[0] == 'climb') + e[5] += 1 + CX.candidates(word) + + for name, fn in [('drifted input hash', drift), ('corrupted MOVE rank in the source records', corrupted_record), - ('dependent part in the partition certificate', dependent_part), ('tampered RESULT.json', tampered_result)]: + ('dependent part in the partition certificate', dependent_part), ('tampered RESULT.json', tampered_result), + ('complex: one #5383 relation dropped', complex_missing_relation), + ('complex: injected dependent row', complex_dependent_row), + ('complex: corrupted climb rank', complex_corrupted_rank)]: rejects(name, fn) print('PASS_BIT_RELATION_SUBSPACES_CONTROLS')