From 122d90cdc0fb24244c0afb56d1f3d76c98636cd8 Mon Sep 17 00:00:00 2001 From: josie Date: Wed, 28 Oct 2026 04:01:08 -0400 Subject: [PATCH 1/2] =?UTF-8?q?Third-engine=20check=20of=20the=20PR6030=20?= =?UTF-8?q?leak-correction=20exclusion=20and=20a=20PR5907=20witness=20(no?= =?UTF-8?q?=20new=20=CE=BA)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Left-kernel tracker reproduces PR6067/PR6069 on the selected PR6030 word (4,009 information-lost, 22 no chart-local combination, 2 erased); on PR5907 one class is legalized at the scalar level by a 7-field chart-local combination program, checked by direct simulation. Co-Authored-By: Claude Opus 5.5 --- .../p104-post-cut-information-loss/README.md | 137 ++++ .../RESULT.json | 605 ++++++++++++++++++ .../SOURCES.json | 14 + .../p104-post-cut-information-loss/TASK.json | 137 ++++ .../VERIFY.json | 21 + .../p104-post-cut-information-loss/check.py | 132 ++++ .../inputs/leakfix.py | 377 +++++++++++ .../inputs/shapesplit.py | 176 +++++ .../p104-post-cut-information-loss/kernel.py | 188 ++++++ .../p104-post-cut-information-loss/verify.py | 185 ++++++ 10 files changed, 1972 insertions(+) create mode 100644 research/p104-post-cut-information-loss/README.md create mode 100644 research/p104-post-cut-information-loss/RESULT.json create mode 100644 research/p104-post-cut-information-loss/SOURCES.json create mode 100644 research/p104-post-cut-information-loss/TASK.json create mode 100644 research/p104-post-cut-information-loss/VERIFY.json create mode 100644 research/p104-post-cut-information-loss/check.py create mode 100644 research/p104-post-cut-information-loss/inputs/leakfix.py create mode 100644 research/p104-post-cut-information-loss/inputs/shapesplit.py create mode 100644 research/p104-post-cut-information-loss/kernel.py create mode 100644 research/p104-post-cut-information-loss/verify.py diff --git a/research/p104-post-cut-information-loss/README.md b/research/p104-post-cut-information-loss/README.md new file mode 100644 index 0000000000..935c22915e --- /dev/null +++ b/research/p104-post-cut-information-loss/README.md @@ -0,0 +1,137 @@ +# PR5718-shape leak corrections: third-engine check of the PR6030 exclusion, and a PR5907 witness + +**Scoped exact result; no new κ.** Base: canonical main `721c03822c421b7f7fcbb2598993b947c4d88419`, where +[PR #6030](https://github.com/CrocSwap/integer-mult-bounds/pull/6030) (DreamingOfClouds) is the selected word. The +selected record is unchanged by this package. + +**Priority.** [PR #6045](https://github.com/CrocSwap/integer-mult-bounds/pull/6045) (JosieElliston) left open +*combination carriers* and *rewritten events* for the PR5718-shape leak classes of Nick Petalas's +[PR #6040](https://github.com/CrocSwap/integer-mult-bounds/pull/6040) census. On the selected PR6030 word, both +questions were answered first by apoursh's [PR #6067](https://github.com/CrocSwap/integer-mult-bounds/pull/6067) +(head `4d629cf0`) and independently by jon314159's +[PR #6069](https://github.com/CrocSwap/integer-mult-bounds/pull/6069) (head `b3f5aabd`). Both report 4,009 +information-lost classes, 22 with no chart-local combination carrier, and 2 (cuts 13637/13639, helper 572) where +clearing the leak erases `z`. This package was built without knowledge of them; their overlap surfaced only at +submission. Lemma 1 below is the same information-collision argument as theirs, and the credit for it is theirs. + +What this package adds: + +1. **A third, independent engine for the PR6030 numbers.** It uses an exact left-kernel tracker (29 vectors, about + 20 ms per word), rather than PR6067's `R M⁻¹ S e_p` collision test or PR6069's global dependency filter. It + reproduces 4,009 / 22 / 2. Its 24 residual classes equal PR6069's `global_screen.survivors` class for class + (local comparison against PR6069's committed `EXPECTED.json`; not part of the verifier). +2. **The PR5907 word, where the exclusion fails.** Class (cut after 13776, chart 1031, helper 699, leak to role 149) + is legalized at the scalar level by an orig-zero chart-local combination program. So the PR6030 exclusion + depends on the word: it is not a property of the PR5718 split shape or of the correction model, and the + combination-carrier test is not vacuous on real data. + +## Result + +| Word | Leak classes | Information lost at the cut | Residual | Residual, by chart-local combination closure | +|---|---:|---:|---:|---| +| PR6030 (selected) | 4,033 | 4,009 | 24 | 22 no usable combination, 2 clearable only by erasing `z` (as PR6067/PR6069) | +| PR5907 | 4,206 | **4,180** | 26 | 23 no usable combination, 2 erased, **1 witness** | + +**The PR5907 witness.** Directly after the cut, the seven fields `696 − 698 + 699 − 700 − 702 − 767 + 792` at chart +1031 sum to zero in the original word, and to `z − ℓ` in the split word. Reading this combination into targets 697 +(`μ = 1`), 698 (`μ = 2`) and 700 (`μ = −1`) adds `μ (z − ℓ)` to each. The program lowers to 18 ADDs, 1 SCALE and 1 +COPY, all chart-local. The COPY cannot be avoided with this combination: each read into a field of its own support +lowers its pairing with `z`, which reaches 0 at the last read (an overwrite). The words contain 23 COPY events of +their own, but native legality is not checked here. A plain simulator (`check.py`) shows that every O output equals +the original output exactly. `z` then reaches V-final roles 698, 700 and 702 (not 699), and PR6040's pairing test +passes. Three perturbed programs are rejected. This is **not** a split proposal: native maps, cost, owned lifetimes +and the caller are unchecked, and PR5907 is not the selected word. + +## Lemma 1 (information loss) + +Setting as in PR6040/PR6045. The word acts linearly on `N = n + m` fields (`n = 770` public, `m = 29` owned). After +event `t`, field `f` holds the linear form `row_f(t)` in the inputs; `W(t)` is the `N × n` matrix of these rows. +For a class with cut after event `i` and helper `p`, the split word replaces `p`'s content by a fresh input `z`, so +its state at the cut is `W(i) + e_p ⊗ (z − ℓ)`. Let `P` be the original post-cut map, so `d = P e_p`, and let +`O` be the public roles whose final chart is not `V = final[p]`. The class leaks when `d_o ≠ 0` for some `o ∈ O`. + +> If a leak class can be legalized by some post-cut linear map `G` (that is, `G` gives every O output its original +> value identically in `x` and `z`), then `row_p(i)` lies in the span of `{row_f(i) : f ≠ p}`. + +*Proof.* Take `o ∈ O` with `d_o ≠ 0` and compare `G_o (W(i) + e_p (z − ℓ)) = P_o W(i)`. The coefficient of `z` +gives `(G_o)_p = 0`. What remains is `(G_o − P_o) W(i) = 0`. So `c = G_o − P_o` is in the left kernel of `W(i)`, +with `c_p = −(P_o)_p = −d_o ≠ 0`. ∎ + +Fresh scratch fields only add zero rows, so they do not change the conclusion. The lemma uses neither charts nor +costs, so it holds for every edit made after the cut. Edits *before* the cut are not covered; for example, saving a +copy of `ℓ` before the cut makes `p` redundant. + +## Lemma 2 (tracking the left kernel) + +`K(t) = {c : c W(t) = 0}`. Field `p` is *redundant* at `t` when some `c ∈ K(t)` has `c_p ≠ 0`. `kernel.py` updates +a basis of `K` exactly at each event: ADD `r += q f` maps `c ↦ c A⁻¹` (`c_f −= q c_r`), SCALE `r *= s` maps +`c_r ↦ c_r / s`, INIT/CLEAR `r` gives `(K ∩ {c_r = 0}) + span{e_r}`, COPY `r := q f` gives +`{k + c (e_r − q e_f) : k ∈ K, k_r = 0}`, and MOVE changes nothing. Each rule follows from `W(t+1) = A W(t)`. + +`verify.py` does not rely on these rules. On both words the final field matrix has exact rank 770. Rank never +increases along a word, so every intermediate state has rank 770 and `dim K = 29`. At every leak-class cut it checks that +the tracker holds 29 linearly independent vectors that annihilate the exact `W(i)`; together these show that the +vectors span `K(i)`. A seeded brute-force comparison then runs 300 random small words, comparing the tracker's +redundant set with exact rank deletions after every event. + +## Residual classes: chart-local combination closure + +For a redundant class, `kernel.closure_intervals` decides which insertion points are usable by programs of +*batches*. A batch at time `t` reads `c · state` for some `c ∈ K(t)` supported on the fields of one chart `X`; in the +split word this equals `κ (z − ℓ)`. It then adds multiples of that value to targets at `X`. Such programs never +change an original row. A batch is usable only if `c` pairs nonzero with the z-column, either the original column +`β(t)` or `D(t)`, the forward image of every earlier usable target. That gives a sound upper bound on the reachable +z-columns. PR6045's `correction_spans` and `decide` (pinned, unmodified) then test whether `d_O` can be cleared +without erasing `z`, and apply PR6040's pairing test. The PR5907 witness is then rebuilt as an explicit program and +checked by the plain simulator in `check.py`. That check is independent of the kernel and suffix algebra. The +verifier also confirms that three perturbed programs are rejected. + +## Reproduce + +Python 3.12, standard library, from the repository root (about 20 s): + +```sh +python3.12 -B research/p104-post-cut-information-loss/verify.py +python3.12 -B scripts/research_package.py --package research/p104-post-cut-information-loss +``` + +Marker: `PASS_P104_POST_CUT_INFORMATION_LOSS`. `--write` regenerates `RESULT.json`. Normal replay is read-only and +compares the receipt byte for byte. + +## Scope and limits + +- This is the scalar O-defect condition of PR6040/PR6045 only: the O outputs must equal the original outputs, and + `z` must reach a V-final output. Native maps, owned lifetimes, restoration, caller, compiler, precision, cost and + outer checks are not modelled. +- Lemma 1 covers every linear edit after the cut, for the PR5718 unit injection `b = e_p` at a PR6040 class. It does + not cover edits before the cut, other injections, or a changed class definition. The census inherits PR6040's + input rule ('empty'). +- The residual-class closure covers batch programs whose every read is an orig-zero chart-local combination. It + does not cover programs whose individual reads have nonzero original value and cancel only across several + times. That gap concerns only the 24 PR6030 residual classes, because Lemma 1 already covers the other 4,009. +- The PR5907 witness is a scalar-level existence check, not a priced or native split. + +## Open next questions + +- **Pre-cut edits.** Lemma 1 says that any PR5718-shape split on the PR6030 word must keep `ℓ` somewhere else at + the cut, for example in a copy saved into an owned field before the cut, and that copy must be uncomputed later. + Is there a class where such a save, with its extra owned lifetime, plus a post-cut correction is legal? First + step: for each leak class, add one pre-cut `INIT s; s += p` at the latest chart that `p` shares with a free owned + field, then rerun the closure. +- **Why PR5907 and not PR6030?** On PR6030, the residual helper-700 classes (cuts 13399 to 13441) have their + redundancy relation spread over charts 1031 and 1043, so no chart-local combination exists (observed in a local + run; not a causal claim). First step: compare the chart-1031 field relations of the two words around the + corresponding cuts. +- **Price the PR5907 witness.** Its 20 inserted events and the change of the z-column (it now reaches roles 698, + 700 and 702 instead of 699) need the PR5599 complete signed bill. This matters only if a similar redundant class + appears on the selected word. +- **Cross-time cancellation** on the 24 residual PR6030 classes (see Scope). + +## Credit + +Nick Petalas (PR6040 census and class definition), Matarener (PR5994 census and pure-subspace decision), +flyingviper (PR5718 split shape), Ali Romman (PR5599 split criterion), DreamingOfClouds (PR5907 and PR6030 words) +PR6045 (JosieElliston, session 33: `leakfix.py`, pinned unmodified), and apoursh (PR6067) and jon314159 +(PR6069), who published the PR6030 exclusion and Lemma 1's argument first, retain credit; nothing of theirs is +modified. Prepared for JosieElliston by Claude Opus 5.5 (Anthropic) via Claude Code, as one session of an unattended +overnight run; no human review. Apache-2.0. diff --git a/research/p104-post-cut-information-loss/RESULT.json b/research/p104-post-cut-information-loss/RESULT.json new file mode 100644 index 0000000000..00ece74435 --- /dev/null +++ b/research/p104-post-cut-information-loss/RESULT.json @@ -0,0 +1,605 @@ +{ + "brute_force_trials": 300, + "pr5907": { + "information_lost": 4180, + "leak_classes": 4206, + "residual": 26, + "residual_classes": [ + { + "charts": [], + "cut_after": 13342, + "frame": 539, + "kind": "no_usable_combination", + "leak": 51, + "pivot": 628, + "rho": null, + "usable_points": 0 + }, + { + "charts": [], + "cut_after": 13347, + "frame": 537, + "kind": "no_usable_combination", + "leak": 52, + "pivot": 768, + "rho": null, + "usable_points": 0 + }, + { + "charts": [], + "cut_after": 13349, + "frame": 537, + "kind": "no_usable_combination", + "leak": 52, + "pivot": 768, + "rho": null, + "usable_points": 0 + }, + { + "charts": [], + "cut_after": 13352, + "frame": 539, + "kind": "no_usable_combination", + "leak": 51, + "pivot": 628, + "rho": null, + "usable_points": 0 + }, + { + "charts": [], + "cut_after": 13354, + "frame": 537, + "kind": "no_usable_combination", + "leak": 52, + "pivot": 768, + "rho": null, + "usable_points": 0 + }, + { + "charts": [], + "cut_after": 13358, + "frame": 537, + "kind": "no_usable_combination", + "leak": 52, + "pivot": 768, + "rho": null, + "usable_points": 0 + }, + { + "charts": [], + "cut_after": 13359, + "frame": 537, + "kind": "no_usable_combination", + "leak": 52, + "pivot": 768, + "rho": null, + "usable_points": 0 + }, + { + "charts": [], + "cut_after": 13361, + "frame": 539, + "kind": "no_usable_combination", + "leak": 51, + "pivot": 628, + "rho": null, + "usable_points": 0 + }, + { + "charts": [], + "cut_after": 13364, + "frame": 539, + "kind": "no_usable_combination", + "leak": 51, + "pivot": 628, + "rho": null, + "usable_points": 0 + }, + { + "charts": [ + 1031 + ], + "cut_after": 13776, + "frame": 1031, + "kind": "witness", + "leak": 1, + "pivot": 699, + "rho": "0", + "usable_points": 8 + }, + { + "charts": [], + "cut_after": 13784, + "frame": 1031, + "kind": "no_usable_combination", + "leak": 1, + "pivot": 699, + "rho": null, + "usable_points": 0 + }, + { + "charts": [], + "cut_after": 13784, + "frame": 1043, + "kind": "no_usable_combination", + "leak": 52, + "pivot": 700, + "rho": null, + "usable_points": 0 + }, + { + "charts": [], + "cut_after": 13791, + "frame": 1043, + "kind": "no_usable_combination", + "leak": 52, + "pivot": 700, + "rho": null, + "usable_points": 0 + }, + { + "charts": [], + "cut_after": 13805, + "frame": 1043, + "kind": "no_usable_combination", + "leak": 52, + "pivot": 700, + "rho": null, + "usable_points": 0 + }, + { + "charts": [], + "cut_after": 13806, + "frame": 1043, + "kind": "no_usable_combination", + "leak": 52, + "pivot": 700, + "rho": null, + "usable_points": 0 + }, + { + "charts": [], + "cut_after": 13808, + "frame": 1041, + "kind": "no_usable_combination", + "leak": 51, + "pivot": 767, + "rho": null, + "usable_points": 0 + }, + { + "charts": [], + "cut_after": 13813, + "frame": 1041, + "kind": "no_usable_combination", + "leak": 51, + "pivot": 767, + "rho": null, + "usable_points": 0 + }, + { + "charts": [], + "cut_after": 13818, + "frame": 1043, + "kind": "no_usable_combination", + "leak": 52, + "pivot": 700, + "rho": null, + "usable_points": 0 + }, + { + "charts": [], + "cut_after": 13994, + "frame": 595, + "kind": "no_usable_combination", + "leak": 7, + "pivot": 572, + "rho": null, + "usable_points": 0 + }, + { + "charts": [], + "cut_after": 14022, + "frame": 595, + "kind": "no_usable_combination", + "leak": 7, + "pivot": 572, + "rho": null, + "usable_points": 0 + }, + { + "charts": [], + "cut_after": 14022, + "frame": 595, + "kind": "no_usable_combination", + "leak": 40, + "pivot": 731, + "rho": null, + "usable_points": 0 + }, + { + "charts": [ + 595 + ], + "cut_after": 14026, + "frame": 595, + "kind": "erased", + "leak": 7, + "pivot": 572, + "rho": null, + "usable_points": 19 + }, + { + "charts": [ + 595 + ], + "cut_after": 14028, + "frame": 595, + "kind": "erased", + "leak": 7, + "pivot": 572, + "rho": null, + "usable_points": 17 + }, + { + "charts": [], + "cut_after": 15580, + "frame": 117, + "kind": "no_usable_combination", + "leak": 25, + "pivot": 706, + "rho": null, + "usable_points": 0 + }, + { + "charts": [], + "cut_after": 15596, + "frame": 835, + "kind": "no_usable_combination", + "leak": 2, + "pivot": 626, + "rho": null, + "usable_points": 0 + }, + { + "charts": [], + "cut_after": 15875, + "frame": 835, + "kind": "no_usable_combination", + "leak": 2, + "pivot": 626, + "rho": null, + "usable_points": 0 + } + ], + "residual_kinds": { + "erased": 2, + "no_usable_combination": 23, + "witness": 1 + } + }, + "pr5907_witness": { + "batches": [ + { + "after_event": 13776, + "chart": 1031, + "comb": { + "696": "1", + "698": "-1", + "699": "1", + "700": "-1", + "702": "-1", + "767": "-1", + "792": "1" + }, + "mu": "1", + "target": 697 + }, + { + "after_event": 13776, + "chart": 1031, + "comb": { + "696": "1", + "698": "-1", + "699": "1", + "700": "-1", + "702": "-1", + "767": "-1", + "792": "1" + }, + "mu": "2", + "target": 698 + }, + { + "after_event": 13776, + "chart": 1031, + "comb": { + "696": "1", + "698": "-1", + "699": "1", + "700": "-1", + "702": "-1", + "767": "-1", + "792": "1" + }, + "mu": "-1", + "target": 700 + } + ], + "class": { + "V": 127, + "cut_after": 13776, + "frame": 1031, + "leak": 1, + "pivot": 699 + }, + "inserted_events": 20, + "inserted_ops": { + "ADD": 18, + "COPY": 1, + "SCALE": 1 + }, + "perturbed_rejected": 3, + "z_column": { + "698": "2", + "700": "-1", + "702": "-1" + } + }, + "pr6030": { + "information_lost": 4009, + "leak_classes": 4033, + "residual": 24, + "residual_classes": [ + { + "charts": [], + "cut_after": 13053, + "frame": 539, + "kind": "no_usable_combination", + "leak": 51, + "pivot": 628, + "rho": null, + "usable_points": 0 + }, + { + "charts": [], + "cut_after": 13058, + "frame": 537, + "kind": "no_usable_combination", + "leak": 52, + "pivot": 768, + "rho": null, + "usable_points": 0 + }, + { + "charts": [], + "cut_after": 13060, + "frame": 537, + "kind": "no_usable_combination", + "leak": 52, + "pivot": 768, + "rho": null, + "usable_points": 0 + }, + { + "charts": [], + "cut_after": 13063, + "frame": 539, + "kind": "no_usable_combination", + "leak": 51, + "pivot": 628, + "rho": null, + "usable_points": 0 + }, + { + "charts": [], + "cut_after": 13065, + "frame": 537, + "kind": "no_usable_combination", + "leak": 52, + "pivot": 768, + "rho": null, + "usable_points": 0 + }, + { + "charts": [], + "cut_after": 13070, + "frame": 537, + "kind": "no_usable_combination", + "leak": 52, + "pivot": 768, + "rho": null, + "usable_points": 0 + }, + { + "charts": [], + "cut_after": 13071, + "frame": 537, + "kind": "no_usable_combination", + "leak": 52, + "pivot": 768, + "rho": null, + "usable_points": 0 + }, + { + "charts": [], + "cut_after": 13073, + "frame": 539, + "kind": "no_usable_combination", + "leak": 51, + "pivot": 628, + "rho": null, + "usable_points": 0 + }, + { + "charts": [], + "cut_after": 13075, + "frame": 539, + "kind": "no_usable_combination", + "leak": 51, + "pivot": 628, + "rho": null, + "usable_points": 0 + }, + { + "charts": [], + "cut_after": 13399, + "frame": 1043, + "kind": "no_usable_combination", + "leak": 52, + "pivot": 700, + "rho": null, + "usable_points": 0 + }, + { + "charts": [], + "cut_after": 13413, + "frame": 1043, + "kind": "no_usable_combination", + "leak": 52, + "pivot": 700, + "rho": null, + "usable_points": 0 + }, + { + "charts": [], + "cut_after": 13421, + "frame": 1043, + "kind": "no_usable_combination", + "leak": 52, + "pivot": 700, + "rho": null, + "usable_points": 0 + }, + { + "charts": [], + "cut_after": 13423, + "frame": 1041, + "kind": "no_usable_combination", + "leak": 51, + "pivot": 767, + "rho": null, + "usable_points": 0 + }, + { + "charts": [], + "cut_after": 13426, + "frame": 1041, + "kind": "no_usable_combination", + "leak": 51, + "pivot": 767, + "rho": null, + "usable_points": 0 + }, + { + "charts": [], + "cut_after": 13431, + "frame": 1043, + "kind": "no_usable_combination", + "leak": 52, + "pivot": 700, + "rho": null, + "usable_points": 0 + }, + { + "charts": [], + "cut_after": 13441, + "frame": 1043, + "kind": "no_usable_combination", + "leak": 52, + "pivot": 700, + "rho": null, + "usable_points": 0 + }, + { + "charts": [], + "cut_after": 13610, + "frame": 595, + "kind": "no_usable_combination", + "leak": 7, + "pivot": 572, + "rho": null, + "usable_points": 0 + }, + { + "charts": [], + "cut_after": 13633, + "frame": 595, + "kind": "no_usable_combination", + "leak": 7, + "pivot": 572, + "rho": null, + "usable_points": 0 + }, + { + "charts": [], + "cut_after": 13633, + "frame": 595, + "kind": "no_usable_combination", + "leak": 40, + "pivot": 731, + "rho": null, + "usable_points": 0 + }, + { + "charts": [ + 595 + ], + "cut_after": 13637, + "frame": 595, + "kind": "erased", + "leak": 7, + "pivot": 572, + "rho": null, + "usable_points": 15 + }, + { + "charts": [ + 595 + ], + "cut_after": 13639, + "frame": 595, + "kind": "erased", + "leak": 7, + "pivot": 572, + "rho": null, + "usable_points": 13 + }, + { + "charts": [], + "cut_after": 15148, + "frame": 117, + "kind": "no_usable_combination", + "leak": 25, + "pivot": 706, + "rho": null, + "usable_points": 0 + }, + { + "charts": [], + "cut_after": 15161, + "frame": 835, + "kind": "no_usable_combination", + "leak": 2, + "pivot": 626, + "rho": null, + "usable_points": 0 + }, + { + "charts": [], + "cut_after": 15448, + "frame": 835, + "kind": "no_usable_combination", + "leak": 2, + "pivot": 626, + "rho": null, + "usable_points": 0 + } + ], + "residual_kinds": { + "erased": 2, + "no_usable_combination": 22 + } + }, + "schema": "p104-post-cut-information-loss/v1" +} diff --git a/research/p104-post-cut-information-loss/SOURCES.json b/research/p104-post-cut-information-loss/SOURCES.json new file mode 100644 index 0000000000..9d0fb73902 --- /dev/null +++ b/research/p104-post-cut-information-loss/SOURCES.json @@ -0,0 +1,14 @@ +{ + "schema_version": 1, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "files": [ + {"path": "certificates/selected-result.json", "usage": "provenance", "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"}, + {"path": "docs/research/agent-task-catalog.json", "usage": "provenance", "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"}, + {"path": "research/p104-helper470-twin-rung-removal/WORD.json.gz", "usage": "input", "git_blob": "22f9ab02d1b73ea0aa4b07ce445a14cc2602c760", "sha256": "7834725d9e34ee846a9ccc615221ea81e0201613938afa185d2eda0c9a6c232f"}, + {"path": "research/p104-helper468-rung-removal/WORD.json.gz", "usage": "input", "git_blob": "7ffe7b500b02b9d0de49a85ec53e36004f1a411f", "sha256": "b69a9cb3a26d4f40aa7ad14f814b188fe16a782999f6f56292538e447d67b284"} + ], + "pinned_copies": [ + {"path": "research/p104-post-cut-information-loss/inputs/shapesplit.py", "origin": "PR #6040 (Nick Petalas) head 1889253f, research/.../shapesplit.py, git blob 6eedc849", "sha256": "11e8ef691b28fb4f401a8c2e97b6d462e7a004f0e215a28579d6a654b4ca3304"}, + {"path": "research/p104-post-cut-information-loss/inputs/leakfix.py", "origin": "PR #6045 (JosieElliston) head 23abc00773a72d8e2b4e733b46c453b0f71f6368, research/p104-pr5718-leak-correction/leakfix.py, git blob c54c16899a22f83b9b982159ee941c3eb9e18bdc", "sha256": "dbbdc9ff9ebb55f1b9e832dcbe1aa5e407e7932a8d958a006bdaca6055e7f4ee"} + ] +} diff --git a/research/p104-post-cut-information-loss/TASK.json b/research/p104-post-cut-information-loss/TASK.json new file mode 100644 index 0000000000..41ad2da637 --- /dev/null +++ b/research/p104-post-cut-information-loss/TASK.json @@ -0,0 +1,137 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "chooser_seed": "3e0e7ada685d1dfd0691221bede5f540", + "original_card": { + "id": "p104-side-correction", + "question": "Can joint helper bases and a legal causal split improve the complete P104 productive/paid invoice?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "research/p104-helper-subspace-splits/README.md", + "research/dyadic-helper-channel-capacity/README.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. 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", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Start with the selected #5599 emitted word and review pending #5718 distinct input/output bases plus #5717/#5719 coverage before claiming work. Pick one uncovered source word, helper group and cut region. Prove the arbitrary-input relation and legal entry/exit corrections, then compare full target and paid profiles. Reject if completion, owned lifetimes or consumer costs repay the gain. A static pairing rank alone is not a physical split.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "P104", + "helper basis", + "helper split", + "5718", + "dyadic capacity" + ], + "existing_checks": [ + { + "scope": "PR #4133: literal-slot defect", + "evidence": "research/p104-literal-slot-defect/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "88666f1dee93fbd85b31fd5d6f91a219e111b5f4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4136: uniform commutation gap", + "evidence": "research/p104-uniform-commutation-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "281ce601a8be9db470de630759179c23e1dfaa88", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4140: uniform encoding gap", + "evidence": "research/p104-uniform-encoding-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "de25c6525aa866962309df5d107b32d55e6e5628", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4153: source-chart shortcut exhausts its optimistic allowance", + "evidence": "research/p104-source-chart-shortcut/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "9123241fea53df77e51ffe30d9aca1625d4bf3a8", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4154: fiber-tag seam mismatch", + "evidence": "research/p104-fiber-tag-seam/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "4ffcdaee5d6255a9cea1fe53a5424435068089d0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact scalar test of post-cut corrections for the PR5718-shape leak classes of the PR6040 census on the selected PR6030 word and on the PR5907 word: information-loss exclusion of every linear post-cut program, decided by an exact left-kernel tracker, and for the residual classes the closure of batch programs reading orig-zero chart-local combinations. On PR6030 this is an independent third engine for the result first published in PR6067 (apoursh) and PR6069 (jon314159); new: the PR5907 census and its one scalar-level witness.", + "scope_change_reason": "Answers PR6045's open next questions (combination carriers; rewritten events). PR6067 and PR6069 answered them first on PR6030; their overlap was found only at submission, so the package is reframed as independent corroboration plus the new PR5907 comparison, which shows the exclusion is word-specific.", + "bottleneck_link": "Complex currently binds the selected assembly; a legal zero-paid helper split adds productive credit. This census says that on the selected word a PR5718-shape split needs a pre-cut change (a saved copy of the retired value).", + "budget_minutes": 60, + "stop_rule": "Stop at the exact census with an independent direct-simulation check of any witness; do not build or price a split.", + "outcome": "completed", + "evidence": "verify.py: pinned inputs; class census equals PR6040 counts on both words; final field matrix rank 770; tracker at every cut has 29 independent annihilating vectors; 300-word brute-force tracker comparison; PR6030: 4,009/4,033 leak classes information-lost, residual 24 = 22 no usable chart-local combination + 2 erased; PR5907: 4,180/4,206 lost, residual 23 + 2 erased + 1 witness; witness rebuilt as a 20-event chart-local program, directly simulated (O outputs identical, z reaches V, PR6040 pairing passes), three perturbations rejected; RESULT.json compared.", + "author": "JosieElliston (session 41 of an overnight run)", + "ai_assistance": "Constructed and checked by Claude Opus 5.5 (Anthropic) via Claude Code; independent human and proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a pre-cut save of the retired value (INIT s; s += p before the cut, with its extra owned lifetime) plus a post-cut correction legalize a PR6030 leak class?", + "why_it_matters": "Lemma 1 shows every PR5718-shape split on the selected word needs the retired value held elsewhere at the cut; this is the remaining edit family.", + "first_step": "For each leak class add one pre-cut save into a free owned field at the latest chart shared with p, then rerun closure_intervals and the span decision.", + "blocked_by": "None; owned-field availability and lifetime cost must be modelled." + }, + { + "question": "Does the PR5907 scalar witness (cut 13776, helper 699) survive the complete signed bill?", + "why_it_matters": "It is the only legal-at-scalar-level PR5718-shape split found; it matters only if a similar redundant class appears on the selected word.", + "first_step": "Price its 20 inserted events and the changed z-column under the PR5599 contract.", + "blocked_by": "PR5907 is not the selected word." + }, + { + "question": "Can programs whose individual reads have nonzero original value cancel across times on the 24 residual PR6030 classes?", + "why_it_matters": "The only post-cut edit family not decided for those 24 classes (also PR6067/PR6069 open).", + "first_step": "Write the bilinear cancellation condition sum_k u_k (x) orig_k = 0 for the residual classes and bound it by the kernel of the stacked state.", + "blocked_by": "None." + } + ], + "overlap": { + "found_at_submission": [ + "https://github.com/CrocSwap/integer-mult-bounds/pull/6067", + "https://github.com/CrocSwap/integer-mult-bounds/pull/6069" + ], + "relation": "Same PR6030 counts (4,009/22/2) from a different engine; 24 residual classes equal PR6069 global_screen.survivors class for class (local comparison). PR5907 census and witness are not in either." + } +} diff --git a/research/p104-post-cut-information-loss/VERIFY.json b/research/p104-post-cut-information-loss/VERIFY.json new file mode 100644 index 0000000000..5af8cdbabd --- /dev/null +++ b/research/p104-post-cut-information-loss/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-helper470-twin-rung-removal/WORD.json.gz", + "research/p104-helper468-rung-removal/WORD.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Authenticate inputs and the pinned PR6040/PR6045 modules; class census equals PR6040 counts; exact rank and left-kernel tracker audit at every cut; brute-force tracker comparison; information-loss census and residual combination closure on PR6030 and PR5907; explicit PR5907 witness simulated directly with perturbations rejected; RESULT.json compared byte for byte." + } + ] +} diff --git a/research/p104-post-cut-information-loss/check.py b/research/p104-post-cut-information-loss/check.py new file mode 100644 index 0000000000..f2bacfe456 --- /dev/null +++ b/research/p104-post-cut-information-loss/check.py @@ -0,0 +1,132 @@ +"""Direct check of an explicit post-cut correction program, independent of the kernel and suffix algebra. Apache-2.0. + +Python 3.12, standard library only. A *batch* (after_event t, chart X, comb c, target r', mu) adds mu (z - l) to +field r', where l = row_p(cut) is the retired value: it reads the chart-local combination c . state, whose value in +the split word is kappa (z - l), and adds (mu / kappa) times it. `emit` lowers every batch into primitive +chart-local events (SCALE r' / COPY r' when r' is in the support of c, then ADDs), and returns the corrected word. +`check` re-simulates that corrected word with a plain event simulator and compares it with the original word. +""" +from fractions import Fraction as Q + + +def add(dst, src, q): + for k, v in src.items(): + x = dst.get(k, 0) + q * v + if x: + dst[k] = x + else: + dst.pop(k, None) + + +def need(ok, why): + if not ok: + raise ValueError(why) + + +def step(rows, cur, e): + op, r = e[0], e[1] + if op == 'MOVE': + need(cur[r] == e[2], 'MOVE from the current chart'); cur[r] = e[3] + elif op == 'INIT': + rows[r] = {}; cur[r] = e[2] + elif op == 'CLEAR': + rows[r] = {}; cur[r] = None + elif op == 'SCALE': + need(Q(e[-2]) != 0, 'nonzero SCALE'); rows[r] = {k: v * Q(e[-2]) for k, v in rows[r].items()} + elif op == 'COPY': + need(cur[r] is not None and cur[r] == cur[e[2]], 'COPY is chart-local') + rows[r] = {k: v * Q(e[-2]) for k, v in rows[e[2]].items() if v * Q(e[-2])} + elif op == 'ADD': + need(cur[r] is not None and cur[r] == cur[e[2]] and r != e[2], 'ADD is chart-local') + add(rows[r], rows[e[2]], Q(e[-2])) + else: + need(False, 'unknown op') + + +def start(w): + n = w['public']; m = w['owned_fields'] + return [{r: Q(1)} if r < n else {} for r in range(n + m)], list(w['initial']) + [None] * m + + +def emit(w, cut, p, batches): + """Lower the batches into primitive events; returns (corrected program, inserted events).""" + rows, cur = start(w) + rows = None # only the z-coefficients are needed to choose the coefficients + zc = {} + by_t = {} + for b in batches: + need(cut <= b['after_event'] < len(w['program']), 'batch after the cut') + by_t.setdefault(b['after_event'], []).append(b) + prog, ins = [], [] + for t, e in enumerate(w['program']): + prog.append(e) + op, r = e[0], e[1] + if op == 'MOVE': cur[r] = e[3] + elif op == 'INIT': cur[r] = e[2] + elif op == 'CLEAR': cur[r] = None + _act(zc, e) + if t == cut: + zc = {p: Q(1)} + for b in by_t.get(t, ()): + X, c, tgt = b['chart'], {int(k): Q(v) for k, v in b['comb'].items()}, b['target'] + need(all(cur[f] == X for f in c) and cur[tgt] == X, 'batch is chart-local') + kappa = sum(x * zc.get(f, 0) for f, x in c.items()) + need(kappa != 0, 'combination carries z') + q = Q(b['mu']) / kappa + evs = [] + others = [(f, x) for f, x in sorted(c.items()) if f != tgt] + s = 1 + q * c.get(tgt, 0) + if s == 0: + f0, x0 = others[0]; others = others[1:] + evs.append(['COPY', tgt, f0, str(q * x0), X]) + elif s != 1: + evs.append(['SCALE', tgt, str(s), X]) + evs += [['ADD', tgt, f, str(q * x), X] for f, x in others] + for ev in evs: + _act(zc, ev) + prog += evs; ins += evs + return prog, ins + + +def _act(v, e): + op, r = e[0], e[1] + if op in ('INIT', 'CLEAR'): + v.pop(r, None) + elif op == 'SCALE': + if r in v: v[r] *= Q(e[-2]) + elif op == 'COPY': + y = Q(e[-2]) * v.get(e[2], 0) + if y: v[r] = y + else: v.pop(r, None) + elif op == 'ADD': + y = v.get(r, 0) + Q(e[-2]) * v.get(e[2], 0) + if y: v[r] = y + else: v.pop(r, None) + + +def run(w, prog, cut_index=None, p=None): + """Plain simulation; after program position cut_index, field p holds the fresh input 'z'.""" + rows, cur = start(w) + for j, e in enumerate(prog): + step(rows, cur, e) + if j == cut_index: + rows[p] = {'z': Q(1)} + return rows, cur + + +def check(w, cut, p, batches): + """Exact claims for the corrected split (V = final[p], O = public roles whose final chart is not V): the corrected + word ends in the original final charts; every O output equals the ORIGINAL output exactly (no z, no non-z + defect); z reaches a V-final output. Returns the final z-column over public roles.""" + n = w['public']; V = w['final'][p] + O = [r for r in range(n) if w['final'][r] != V] + orig, cur0 = run(w, w['program']) + prog, ins = emit(w, cut, p, batches) + need(prog[:cut + 1] == w['program'][:cut + 1], 'prefix up to the cut unchanged') + new, cur1 = run(w, prog, cut, p) + need(cur1 == cur0, 'final charts unchanged') + zcol = {r: new[r]['z'] for r in range(n) if new[r].get('z')} + need(all(r not in zcol for r in O), 'no z-leak to a role whose final chart is not V') + need(all(new[r] == orig[r] for r in O), 'every O output equals the original output') + need(any(w['final'][r] == V for r in zcol), 'z still reaches a V-final output') + return zcol, ins diff --git a/research/p104-post-cut-information-loss/inputs/leakfix.py b/research/p104-post-cut-information-loss/inputs/leakfix.py new file mode 100644 index 0000000000..c54c16899a --- /dev/null +++ b/research/p104-post-cut-information-loss/inputs/leakfix.py @@ -0,0 +1,377 @@ +"""Exact test of mid-word corrections for PR5718-shape helper-split leak classes. Apache-2.0. + +Python 3.12, standard library only. Extends Nick Petalas's PR6040 census (`inputs/shapesplit.py`, pinned), which +builds on Matarener's PR5994 census and flyingviper's PR5718 split shape. + +Setting (PR6040). A class is (cut after event i, chart F, helper p of a boundary group (U, V)). A new independent +helper z replaces p after the cut; its output column is d = S_i e_p (S = suffix columns of the original word). The +class "leaks" when d is nonzero on O = {public roles whose final chart is not V}. + +Corrections. Insert chart-local events ADD r' += q f after an event t >= i, where f is a field whose value in +the split word is a pure multiple of z (zero non-z part), and r' is any field at the same chart at time t. By the +product telescoping identity prod(I+D_k)A - prod A = sum_k (orig suffix after t_k) D_k (corrected state at t_k), +and because such an ADD only adds multiples of z (so every non-z part is unchanged), the corrected z-column is + + d' = d + sum_k mu_k v_k, v_k = S_{t_k} e_{r'_k} (suffix column of the ORIGINAL word), + +with mu_k = q_k * (z-coefficient of f_k at t_k in the corrected word). The non-z columns of the word are unchanged. +The non-z part of f in the split word is row_f(t) - zc_f(t) * row_p(i), where zc_f(t) is the coefficient with +which the content of field p at the cut reaches f at t (by linearity, the original word is the split word with +z := row_p(i)). Hence: + + * first-order sources: fields with zero non-z part and zc != 0 in the uncorrected split word; each correction + from such a source can take any mu (corrections in time order, each q chosen after the earlier ones); + * necessary superset: also fields whose whole split-word value is zero (zc = 0, row = 0), which can only carry z + after an earlier correction wrote into them. Any correction program whose sources are pure-z fields has its + v_k inside this superset span. + +Decision per class: is d_O in -span{(v_k)_O}? If so, the pairing of PR6040 (functional_witness) is tested with +rho = d'_p, which is either fixed by the solution or free (when a combination with zero O-part moves the p +coordinate). 'single' = one correction suffices (some v_O proportional to d_O). + +Scope: the z-part necessary condition of PR6040 only. Corrections whose source carries non-z content, the non-z +part of the split normalization, native maps, caller, compiler and outer checks are not modelled. +""" +from collections import defaultdict +from fractions import Fraction as Q +import importlib.util, sys +from pathlib import Path + +HERE = Path(__file__).resolve().parent + + +def _load_shapesplit(): + name = 'pr6040_shapesplit' + if name in sys.modules: + return sys.modules[name] + spec = importlib.util.spec_from_file_location(name, HERE/'inputs'/'shapesplit.py') + mod = importlib.util.module_from_spec(spec); sys.modules[name] = mod; spec.loader.exec_module(mod) + return mod + + +SS = _load_shapesplit() +add, need = SS.add, SS.need + + +def leak_classes(w, in_kind='empty'): + """Re-run the PR6040 forward/backward census, keeping for each class its A, d (full column) and row_p(i). + Returns (classes, counts); counts must equal SS.census(w, in_kind)[0].""" + n = w['public']; m = w.get('owned_fields', max(e[1] for e in w['program']) + 1 - n); N = n + m + prog = w['program']; S = SS.spans(w); dims = [len(f) for f in w['frames']] + groups = SS.groups_of(w) + valid = {g: {f for f in range(len(S)) if S[g[0]] < S[f] < S[g[1]]} for g in groups} + insup = {} + for g, rs in groups.items(): + s = set(rs) | {r for r in range(n) if w['initial'][r] == g[0]} + if in_kind == 'empty': + s |= {r for r in range(n) if dims[w['initial'][r]] == 0} + insup[g] = s + rows = [{r: Q(1)} if r < n else {} for r in range(N)] + cur = list(w['initial']) + [None] * m + at = defaultdict(set) + for r in range(n): + at[cur[r]].add(r) + snaps = defaultdict(list); counts = defaultdict(int) + for i, e in enumerate(prog): + op, r = e[0], e[1] + if op == 'MOVE': + at[e[2]].discard(r); at[e[3]].add(r); cur[r] = e[3]; touched = (e[2], e[3]) + elif op == 'INIT': + rows[r] = {}; cur[r] = e[2]; at[e[2]].add(r); touched = (e[2],) + elif op == 'CLEAR': + rows[r] = {}; at[e[2]].discard(r); cur[r] = None; touched = (e[2],) + elif op == 'SCALE': + rows[r] = {k: v * Q(e[-2]) for k, v in rows[r].items()}; touched = (cur[r],) + elif op == 'COPY': + rows[r] = {k: v * Q(e[-2]) for k, v in rows[e[2]].items()}; touched = (cur[r],) + else: + add(rows[r], rows[e[2]], Q(e[-2])); touched = (cur[r],) + for F in set(touched): + if F is None or not at[F]: + continue + roles = sorted(at[F]) + for g in groups: + if F not in valid[g] or not (groups[g] & at[F]): + continue + counts['evaluations'] += 1 + A = SS.pure_subspace(rows, roles, insup[g]) + hp = [p for p in sorted(groups[g] & at[F]) if any(coef.get(p) for coef, img in A)] + if not any(img for coef, img in A) or not hp: + counts['no_helper_prefix'] += 1 + continue + snaps[i].append((F, g, hp, A, {p: dict(rows[p]) for p in hp})) + pivots = {p for v in snaps.values() for (F, g, hp, A, rp) in v for p in hp} + fin = {p: w['final'][p] for p in pivots} + outside = {p: {r for r in range(n) if w['final'][r] != fin[p]} for p in pivots} + keep = {p: outside[p] | {p} for p in pivots} + cols = [{r: Q(1)} if r < n else {} for r in range(N)] + classes = [] + for i in range(len(prog) - 1, -1, -1): + for (F, g, hp, A, rp) in snaps.get(i, []): + for p in hp: + d = {k: x for k, x in cols[p].items() if k in keep[p]} + leak = sum(1 for k in d if k in outside[p]) + free = {r for r in range(n) if r not in keep[p]} + if leak: + counts['kind_leak'] += 1; kind = 'leak' + else: + kind = 'witness' if SS.functional_witness(A, p, free, d.get(p, Q(0))) else 'pairing' + counts['kind_' + kind] += 1 + classes.append({'cut_after': i, 'frame': F, 'group': g, 'pivot': p, 'kind': kind, 'leak': leak, + 'ranks': [dims[F] - dims[g[0]], dims[g[1]] - dims[F]], + 'A': A, 'd': d, 'dall': dict(cols[p]), 'row_p': rp[p], 'outside': outside[p], 'free': free}) + e = prog[i]; op, r = e[0], e[1] + if op in ('INIT', 'CLEAR'): + cols[r] = {} + elif op == 'COPY': + add(cols[e[2]], cols[r], Q(e[-2])); cols[r] = {} + elif op == 'SCALE': + cols[r] = {k: v * Q(e[-2]) for k, v in cols[r].items()} + elif op == 'ADD': + add(cols[e[2]], cols[r], Q(e[-2])) + counts['witnesses'] = sum(1 for c in classes if c['kind'] == 'witness') + counts['pivots'] = len(pivots) + classes.sort(key=lambda c: (c['cut_after'], c['frame'], c['pivot'])) + return classes, dict(counts) + + +def source_intervals(w, cuts, superset=False, mode='carrier'): + """For each (cut i, pivot p) in `cuts` -> list of (field f, chart X, t0, t1): f has zero non-z part in the split + word at chart X after every event t in [t0, t1], and (unless superset) a nonzero z-coefficient. + One shared forward pass over the original word; z-coefficients zc are tracked per (i, p).""" + n = w['public']; m = w.get('owned_fields', max(e[1] for e in w['program']) + 1 - n); N = n + m + prog = w['program'] + rows = [{r: Q(1)} if r < n else {} for r in range(N)] + cur = list(w['initial']) + [None] * m + starts = defaultdict(list) + for key in cuts: + starts[key[0]].append(key) + zc = {} # key -> {field: coefficient} + rowp = {} # key -> row_p(i) + holders = defaultdict(set) # field -> keys with zc[key][field] != 0 + opened = {} # key -> {field: (chart, t0)} + out = defaultdict(list) + + def pure(key, f): + c = zc[key].get(f, 0) + if c == 0: + return superset and not rows[f] and cur[f] is not None + if mode == 'carrier': # original value zero: split value = c * (z - row_p(i)) + return not rows[f] + rp = rowp[key] + if len(rows[f]) != len(rp): + return False + return all(rows[f].get(k) == c * v for k, v in rp.items()) + + def refresh(key, f, t): + """Update the open interval of f for key after event t.""" + o = opened[key] + if f in o: + X, t0 = o[f] + if not pure(key, f) or cur[f] != X: + out[key].append((f, X, t0, t - 1)); del o[f] + if f not in o and cur[f] is not None and pure(key, f): + o[f] = (cur[f], t) + + for t, e in enumerate(prog): + op, r = e[0], e[1] + changed = {r} + if op == 'MOVE': + cur[r] = e[3] + elif op == 'INIT': + rows[r] = {}; cur[r] = e[2] + elif op == 'CLEAR': + rows[r] = {}; cur[r] = None + elif op == 'SCALE': + rows[r] = {k: v * Q(e[-2]) for k, v in rows[r].items()} + elif op == 'COPY': + rows[r] = {k: v * Q(e[-2]) for k, v in rows[e[2]].items()} + else: + add(rows[r], rows[e[2]], Q(e[-2])) + # z-coefficient propagation, same linear action on the scalar zc[key][*] + aff = set(holders.get(r, ())) + if op in ('ADD', 'COPY'): + aff |= holders.get(e[2], set()) + for key in aff: + z = zc[key]; old = z.get(r, 0) + if op in ('INIT', 'CLEAR'): + new = 0 + elif op == 'SCALE': + new = old * Q(e[-2]) + elif op == 'COPY': + new = Q(e[-2]) * z.get(e[2], 0) + elif op == 'ADD': + new = old + Q(e[-2]) * z.get(e[2], 0) + else: + new = old + if new: + z[r] = new; holders[r].add(key) + else: + z.pop(r, None); holders[r].discard(key) + # interval bookkeeping for keys whose purity of r may have changed + check = aff if not superset else set(opened) + for key in check: + refresh(key, r, t) + # new cuts start after event t + for key in starts.get(t, ()): + i, p = key + zc[key] = {p: Q(1)}; holders[p].add(key); rowp[key] = dict(rows[p]); opened[key] = {} + if superset: + for f in range(N): + if cur[f] is not None and not rows[f] and f != p: + opened[key][f] = (cur[f], t) + refresh(key, p, t) + T = len(prog) - 1 + for key, o in opened.items(): + for f, (X, t0) in o.items(): + out[key].append((f, X, t0, T)) + return out + + +class Span: + """Incremental exact row-echelon basis over Q for sparse dict vectors; coordinate order given by `order`.""" + def __init__(self, order): + self.rank = {k: j for j, k in enumerate(order)} + self.piv = {} # pivot coordinate -> normalized vector + + def reduce(self, v): + v = dict(v) + while v: + k = min(v, key=self.rank.__getitem__) + if k not in self.piv: + return v, k + add(v, self.piv[k], -v[k]) + return v, None + + def insert(self, v): + v, k = self.reduce(v) + if k is None: + return False + s = 1 / v[k] + self.piv[k] = {x: y * s for x, y in v.items()} + return True + + +def correction_spans(w, classes, intervals): + """One backward pass. For every class, the span of v = S_t e_{r'} restricted to O + {p}, over insertion times t + in a source interval and r' at the source's chart. Also flags a single-correction (v_O proportional to d_O).""" + n = w['public']; m = w.get('owned_fields', max(e[1] for e in w['program']) + 1 - n); N = n + m + prog = w['program'] + # chart membership after each event, reconstructed forward then walked backward + cur = list(w['initial']) + [None] * m + for e in prog: + if e[0] == 'MOVE': cur[e[1]] = e[3] + elif e[0] == 'INIT': cur[e[1]] = e[2] + elif e[0] == 'CLEAR': cur[e[1]] = None + at = defaultdict(set) + for f in range(N): + if cur[f] is not None: + at[cur[f]].add(f) + byclass = {} + active_at = defaultdict(list) # t1 -> list of (class index, f, X, t0) + for ci, c in enumerate(classes): + key = (c['cut_after'], c['pivot']) + O = c['outside']; p = c['pivot'] + order = sorted(O) + sorted(r for r in range(n) if r not in O) + byclass[ci] = {'span': Span(order), 'seen': set(), 'single': None, 'n_vectors': 0, 'O': O, + 'dO': {k: x for k, x in c['d'].items() if k in O}, 'd': c['dall']} + for (f, X, t0, t1) in intervals.get(key, ()): + active_at[t1].append((ci, f, X, t0)) + live = [] # currently open (ci, f, X, t0) + version = [0] * N + cols = [{r: Q(1)} if r < n else {} for r in range(N)] + for t in range(len(prog) - 1, -1, -1): + # state: cols = suffix after event t, membership = after event t + live.extend(active_at.get(t, ())) + still = [] + for item in live: + ci, f, X, t0 = item + if t < t0: + continue + still.append(item) + B = byclass[ci] + for r2 in at[X]: + tag = (r2, version[r2]) + if tag in B['seen']: + continue + B['seen'].add(tag) + v = cols[r2] + if not v: + continue + B['n_vectors'] += 1 + O = B['O']; vO = {k: x for k, x in v.items() if k in O} + dO = B['dO'] + if B['single'] is None and vO and set(vO) == set(dO): + k0 = next(iter(dO)); s = -dO[k0] / vO[k0] + if all(dO[k] + s * vO[k] == 0 for k in dO): + rest = dict(B['d']); add(rest, v, s) + if rest: # z must still reach a V-final role (no erasure of the new helper) + B['single'] = {'after_event': t, 'target': r2, 'source': f, 'chart': X, 'mu': str(s)} + B['span'].insert(v) + live = still + e = prog[t]; op, r = e[0], e[1] + # reverse membership of event t + if op == 'MOVE': + at[e[3]].discard(r); at[e[2]].add(r) + elif op == 'INIT': + at[e[2]].discard(r) + elif op == 'CLEAR': + at[e[2]].add(r) + # suffix columns before event t + if op in ('INIT', 'CLEAR'): + cols[r] = {}; version[r] += 1 + elif op == 'COPY': + add(cols[e[2]], cols[r], Q(e[-2])); cols[r] = {}; version[r] += 1; version[e[2]] += 1 + elif op == 'SCALE': + cols[r] = {k: v * Q(e[-2]) for k, v in cols[r].items()}; version[r] += 1 + elif op == 'ADD': + add(cols[e[2]], cols[r], Q(e[-2])); version[e[2]] += 1 + return byclass + + +def decide(c, B): + """Return (kind, rho) for one leak class. 'unreachable': no correction combination clears d on O; + 'erased': only by removing z from every V-final output (the new helper would have no target); otherwise the + PR6040 pairing outcome ('witness' / 'pairing') with rho = d'_p fixed or 'free'.""" + p = c['pivot']; O = c['outside']; sp = B['span'] + r, k = sp.reduce(c['dall']) # O coordinates come first in the elimination order + if k is not None and k in O: + return 'unreachable', None + W = [v for piv, v in sp.piv.items() if piv not in O] # zero O-part: free moves of d' on V-final roles + if not r and not W: + return 'erased', None + rho_free = any(v.get(p) for v in W) + A = c['A']; free = c['free'] + if rho_free: + L1 = [coef.get(p, Q(0)) for coef, img in A] + L2 = [img.get(p, Q(0)) for coef, img in A] + L3 = [{k2: v for k2, v in img.items() if k2 in free} for coef, img in A] + ok = any(L1) and (any(L3) or any(L2)) + return ('witness' if ok else 'pairing'), 'free' + rho = r.get(p, Q(0)) + if not any(v for v in W) and not {x for x in r if x != p} and rho == 0: + return 'erased', None + return ('witness' if SS.functional_witness(A, p, free, rho) else 'pairing'), str(rho) + + +def run(w, in_kind='empty', superset=False, only_leak=True, mode='carrier', select=None): + """mode 'carrier': sources whose ORIGINAL value is zero while carrying p's cut content (their split value is a + multiple of z - row_p(i), the full defect direction); mode 'purez': sources whose split value is a multiple of z + (PR6040's suggested r += q*new; fixes only the z-part).""" + classes, counts = leak_classes(w, in_kind) + todo = [c for c in classes if c['kind'] == 'leak'] if only_leak else classes + if select: + todo = [c for c in todo if select(c)] + cuts = sorted({(c['cut_after'], c['pivot']) for c in todo}) + iv = source_intervals(w, cuts, superset, mode) + spans = correction_spans(w, todo, iv) + res = [] + for ci, c in enumerate(todo): + B = spans[ci] + kind, rho = decide(c, B) + res.append({'cut_after': c['cut_after'], 'frame': c['frame'], 'pivot': c['pivot'], 'group': list(c['group']), + 'ranks': c['ranks'], 'leak': c['leak'], 'sources': len(iv.get((c['cut_after'], c['pivot']), ())), + 'vectors': B['n_vectors'], 'span_rank': len(B['span'].piv), 'kind': kind, 'rho': rho, + 'single': B['single']}) + return counts, res, iv + diff --git a/research/p104-post-cut-information-loss/inputs/shapesplit.py b/research/p104-post-cut-information-loss/inputs/shapesplit.py new file mode 100644 index 0000000000..6eedc849e7 --- /dev/null +++ b/research/p104-post-cut-information-loss/inputs/shapesplit.py @@ -0,0 +1,176 @@ +"""Exact census of PR5718-shape helper splits on a P104 word. Apache-2.0. Python 3.12, standard library only. + +Prepared by Nick Petalas. Extends the criterion and pure-subspace decision of Matarener's PR5994 census +(`research/p104-helper-split-exhaustion`, PR5599 PROOF.md section 1) to the shape of flyingviper's PR5718 split. + +Model (one helper p of a boundary group g = (U, V), cut after event i, strictly intermediate chart F holding p): + * input side: a combination a of the prefix rows of the fields at F with a_p != 0 and c = aP supported on the + group, on roles whose initial chart is U, or (in_kind='empty', PR5718's rule) on every role whose initial chart + is zero-dimensional; + * a new independent helper z replaces p after the cut (unit injection b = e_p, as in PR5718); its z-direction + reaches the outputs as d = S e_p (S = suffix columns of the original word); + * output normalisation only at V: every role whose final chart is V (other than p) may be corrected freely, so d + must vanish on O = {roles whose final chart is not V}; the pair needs a.b = c.d' != 0. +Classes whose d leaks into O are reported as `leak`: such a split needs a mid-word correction of that leak. +""" +from collections import defaultdict +from fractions import Fraction as Q +import gzip, json + + +def need(ok, why): + if not ok: + raise ValueError(why) + + +def read(path): + raw = open(path, 'rb').read() + return json.loads(gzip.decompress(raw) if str(path).endswith('.gz') else raw) + + +def spans(w): + out = [] + for basis in w['frames']: + s = {0} + for v in basis: + need(type(v) is int and 0 < v < 512 and v not in s, 'independent binary basis') + s |= {x ^ v for x in s} + out.append(frozenset(s)) + return out + + +def add(dst, src, q): + for k, v in src.items(): + x = dst.get(k, 0) + q * v + if x: + dst[k] = x + else: + dst.pop(k, None) + + +def groups_of(w): + n = w['public']; main = set(w['live']) | {r + 112 for r in w['live']} + g = defaultdict(set) + for r in range(n): + if r not in main: + g[(w['initial'][r], w['final'][r])].add(r) + return g + + +def pure_subspace(vecs, roles, support): + """Basis of {x : sum x_r vecs[r] supported in `support`} as (coefficients, image) pairs; kernel vectors included.""" + pivots, out = [], [] + for r in roles: + outside = {k: v for k, v in vecs[r].items() if k not in support} + coef = {r: Q(1)} + for key, prow, pcoef in pivots: + if key in outside: + s = -outside[key]; add(outside, prow, s); add(coef, pcoef, s) + if outside: + key = min(outside); s = 1 / outside[key] + pivots.append((key, {k: v * s for k, v in outside.items()}, {k: v * s for k, v in coef.items()})) + else: + img = {} + for x, q in coef.items(): + add(img, vecs[x], q) + out.append((coef, img)) + return out + + +def functional_witness(A, p, free, rho): + """Exact decision over the span of A. With L1 = a_p, L2 = c_p, L3 = c on the free coordinates and rho = d_p, a + split exists iff some a has L1 != 0 and (L3 != 0 or L1 = rho * L2): free coordinates of d' adjust c.d' at will, + otherwise c.d' = rho * c_p must equal a.b = a_p.""" + L1 = [coef.get(p, Q(0)) for coef, img in A] + L2 = [img.get(p, Q(0)) for coef, img in A] + L3 = [{k: v for k, v in img.items() if k in free} for coef, img in A] + if not any(L1): + return False + if any(L3): + return True + M = [L1[k] - rho * L2[k] for k in range(len(A))] # is L1 nonzero on ker M ? + if not any(M): + return True + j = next(k for k in range(len(A)) if M[k]) + return any(L1[k] * M[j] - L1[j] * M[k] for k in range(len(A))) + + +def census(w, in_kind='empty'): + """Returns (counts, classes). in_kind: 'boundary' (group + roles initial at U) or 'empty' (also every role + initial at a zero-dimensional chart).""" + n = w['public']; m = w.get('owned_fields', max(e[1] for e in w['program']) + 1 - n); N = n + m + prog = w['program']; S = spans(w); dims = [len(f) for f in w['frames']] + groups = groups_of(w) + valid = {g: {f for f in range(len(S)) if S[g[0]] < S[f] < S[g[1]]} for g in groups} + insup = {} + for g, rs in groups.items(): + s = set(rs) | {r for r in range(n) if w['initial'][r] == g[0]} + if in_kind == 'empty': + s |= {r for r in range(n) if dims[w['initial'][r]] == 0} + insup[g] = s + rows = [{r: Q(1)} if r < n else {} for r in range(N)] + cur = list(w['initial']) + [None] * m + at = defaultdict(set) + for r in range(n): + at[cur[r]].add(r) + snaps = defaultdict(list); counts = defaultdict(int) + for i, e in enumerate(prog): + op, r = e[0], e[1] + if op == 'MOVE': + at[e[2]].discard(r); at[e[3]].add(r); cur[r] = e[3]; touched = (e[2], e[3]) + elif op == 'INIT': + rows[r] = {}; cur[r] = e[2]; at[e[2]].add(r); touched = (e[2],) + elif op == 'CLEAR': + rows[r] = {}; at[e[2]].discard(r); cur[r] = None; touched = (e[2],) + elif op == 'SCALE': + rows[r] = {k: v * Q(e[-2]) for k, v in rows[r].items()}; touched = (cur[r],) + elif op == 'COPY': + rows[r] = {k: v * Q(e[-2]) for k, v in rows[e[2]].items()}; touched = (cur[r],) + else: + add(rows[r], rows[e[2]], Q(e[-2])); touched = (cur[r],) + for F in set(touched): + if F is None or not at[F]: + continue + roles = sorted(at[F]) + for g in groups: + if F not in valid[g] or not (groups[g] & at[F]): + continue + counts['evaluations'] += 1 + A = pure_subspace(rows, roles, insup[g]) + hp = [p for p in sorted(groups[g] & at[F]) if any(coef.get(p) for coef, img in A)] + if not any(img for coef, img in A) or not hp: + counts['no_helper_prefix'] += 1 + continue + snaps[i].append((F, g, hp, A)) + pivots = {p for v in snaps.values() for (F, g, hp, A) in v for p in hp} + fin = {p: w['final'][p] for p in pivots} + outside = {p: {r for r in range(n) if w['final'][r] != fin[p]} for p in pivots} + keep = {p: outside[p] | {p} for p in pivots} + cols = [{r: Q(1)} if r < n else {} for r in range(N)] + classes = [] + for i in range(len(prog) - 1, -1, -1): + for (F, g, hp, A) in snaps.get(i, []): + for p in hp: + d = {k: x for k, x in cols[p].items() if k in keep[p]} + leak = sum(1 for k in d if k in outside[p]) + if leak: + counts['kind_leak'] += 1 + kind = 'leak' + else: + free = {r for r in range(n) if r not in keep[p]} + kind = 'witness' if functional_witness(A, p, free, d.get(p, Q(0))) else 'pairing' + counts['kind_' + kind] += 1 + classes.append({'cut_after': i, 'frame': F, 'group': list(g), 'pivot': p, + 'ranks': [dims[F] - dims[g[0]], dims[g[1]] - dims[F]], 'kind': kind, 'leak': leak}) + e = prog[i]; op, r = e[0], e[1] + if op in ('INIT', 'CLEAR'): + cols[r] = {} + elif op == 'COPY': + add(cols[e[2]], cols[r], Q(e[-2])); cols[r] = {} + elif op == 'SCALE': + cols[r] = {k: v * Q(e[-2]) for k, v in cols[r].items()} + elif op == 'ADD': + add(cols[e[2]], cols[r], Q(e[-2])) + counts['witnesses'] = sum(1 for c in classes if c['kind'] == 'witness') + counts['pivots'] = len(pivots) + return dict(counts), sorted(classes, key=lambda c: (c['cut_after'], c['frame'], c['pivot'])) diff --git a/research/p104-post-cut-information-loss/kernel.py b/research/p104-post-cut-information-loss/kernel.py new file mode 100644 index 0000000000..4d4fcdc3d4 --- /dev/null +++ b/research/p104-post-cut-information-loss/kernel.py @@ -0,0 +1,188 @@ +"""Left-kernel tracker for the P104 linear words: which fields' contents are linearly redundant at each event. +Apache-2.0. Python 3.12, standard library only. + +A word acts on N = n + m fields; public field r < n starts as the input coordinate x_r, owned fields start empty. +Write W(t) for the N x n matrix of field values (rows = linear forms in the inputs) after event t, and +K(t) = {c in Q^N : c W(t) = 0} for its left kernel. Field p is *redundant* at t when some c in K(t) has c_p != 0, +i.e. row_p(t) lies in the span of the other fields' rows. K evolves by exact rules (README, Lemma 2): + + ADD r += q f (W' = (I + q e_r e_f^T) W): c_f <- c_f - q c_r (c' = c A^{-1}) + SCALE r *= s, s != 0: c_r <- c_r / s + INIT/CLEAR r (row r := 0): K' = (K cap {c_r = 0}) + span{e_r} + COPY r := q f (row r := q row_f): K' = {c : c - c_r e_r + q c_r e_f in K, and that vector has r-coordinate 0} + = {k + c_r (e_r - q e_f) : k in K, k_r = 0} (needs f != r) + MOVE: values unchanged. + +The basis is kept in reduced echelon form (pivot coordinate -> sparse vector); its support is the redundant set. +""" +from fractions import Fraction as Q + + +def need(ok, why): + if not ok: + raise SystemExit('FAIL: ' + why) + + +class Kernel: + def __init__(self, N, empty): + self.vecs = [{f: Q(1)} for f in sorted(empty)] # list of sparse vectors (not necessarily echelon) + self.N = N + + # -- helpers ------------------------------------------------------------------------------------------------ + def _cap_zero(self, r): + """Replace the basis by a basis of K cap {c_r = 0}.""" + hit = [v for v in self.vecs if v.get(r)] + keep = [v for v in self.vecs if not v.get(r)] + if hit: + b = hit[0]; br = b[r] + for v in hit[1:]: + s = v[r] / br + u = dict(v) + for k, x in b.items(): + y = u.get(k, 0) - s * x + if y: u[k] = y + else: u.pop(k, None) + keep.append(u) + self.vecs = keep + + def apply(self, e): + op, r = e[0], e[1] + if op == 'ADD': + f, q = e[2], Q(e[-2]) + need(f != r, 'ADD with distinct source') + for v in self.vecs: + cr = v.get(r) + if cr: + y = v.get(f, 0) - q * cr + if y: v[f] = y + else: v.pop(f, None) + elif op == 'SCALE': + s = Q(e[-2]); need(s != 0, 'nonzero SCALE') + for v in self.vecs: + if r in v: v[r] = v[r] / s + elif op in ('INIT', 'CLEAR'): + self._cap_zero(r) + self.vecs.append({r: Q(1)}) + elif op == 'COPY': + f, q = e[2], Q(e[-2]) + need(f != r, 'COPY with distinct source') + self._cap_zero(r) + u = {r: Q(1)} + if q: u[f] = -q + self.vecs.append(u) + elif op == 'MOVE': + pass + else: + need(False, 'unknown op ' + op) + + def support(self): + s = set() + for v in self.vecs: + s.update(v) + return s + + +def run(w, cuts): + """cuts: set of event indices i. Returns {i: (dim K(i), frozenset support K(i))} for the state after event i.""" + n = w['public']; prog = w['program'] + m = w.get('owned_fields', max(e[1] for e in prog) + 1 - n); N = n + m + K = Kernel(N, range(n, N)) + out = {} + for i, e in enumerate(prog): + K.apply(e) + if i in cuts: + out[i] = (len(K.vecs), frozenset(K.support())) + return out, K + + +def chart_local(vecs, inside): + """Basis of {sum a_j vecs[j]} with every coordinate outside `inside` zero (exact elimination).""" + rows = [dict(v) for v in vecs] + out = [] + while rows: + v = rows.pop() + bad = [k for k in v if k not in inside] + if not bad: + if v: out.append(v) + continue + k = min(bad); x = v[k] + nxt = [] + for u in rows: + y = u.get(k) + if y: + s = y / x; u = dict(u) + for kk, xx in v.items(): + z = u.get(kk, 0) - s * xx + if z: u[kk] = z + else: u.pop(kk, None) + nxt.append(u) + rows = nxt + return out + + +def _act(v, e): + """Apply one event to a column vector v over fields (the forward action on z-coefficients).""" + op, r = e[0], e[1] + if op in ('INIT', 'CLEAR'): + v.pop(r, None) + elif op == 'SCALE': + if r in v: v[r] *= Q(e[-2]) + elif op == 'COPY': + y = Q(e[-2]) * v.get(e[2], 0) + if y: v[r] = y + else: v.pop(r, None) + elif op == 'ADD': + y = v.get(r, 0) + Q(e[-2]) * v.get(e[2], 0) + if y: v[r] = y + else: v.pop(r, None) + + +def closure_intervals(w, i, p): + """Upper bound on the insertion points usable by a correction program whose every inserted batch reads an + orig-zero chart-local combination c (c in K(t), supported on one chart X) into targets at X. Such a batch adds + (c . beta'(t)) (z - row_p(i)) to targets at X, where beta' is the z-coefficient column of the corrected word, + and leaves every orig row unchanged. beta'(t) lies in beta(t) + D(t), where D(t) is the forward image of the + unit columns of all earlier usable targets. A point (t, X) is usable only if some c in K_X(t) pairs nonzero + with beta(t) or with D(t); then all fields at X join D. Returns [(label, X, t, t)] usable points (as + single-event intervals) and the final dim D.""" + n = w['public']; prog = w['program'] + m = w.get('owned_fields', max(e[1] for e in prog) + 1 - n); N = n + m + K = Kernel(N, range(n, N)) + cur = list(w['initial']) + [None] * m + beta = None; D = []; out = []; cache = None + for t, e in enumerate(prog): + op, r = e[0], e[1] + K.apply(e) + if op == 'MOVE': cur[r] = e[3] + elif op == 'INIT': cur[r] = e[2] + elif op == 'CLEAR': cur[r] = None + if beta is not None: + _act(beta, e) + for d in D: + _act(d, e) + D = [d for d in D if d] + if t == i: + beta = {p: Q(1)} + if t < i: + continue + supp = K.support() + key = (tuple(sorted(supp)), tuple(cur[f] for f in sorted(supp)), tuple(tuple(sorted(v.items())) for v in K.vecs)) + if cache is None or cache[0] != key: + charts = {} + for f in supp: + if cur[f] is not None: + charts.setdefault(cur[f], set()).add(f) + loc = {X: chart_local(K.vecs, fs) for X, fs in charts.items()} + cache = (key, {X: B for X, B in loc.items() if B}) + for X, B in cache[1].items(): + usable = any(sum(x * beta.get(f, 0) for f, x in c.items()) for c in B) or \ + any(sum(x * d.get(f, 0) for f, x in c.items()) for c in B for d in D) + if usable: + out.append(('comb', X, t, t)) + have = set() + for d in D: + if len(d) == 1: have.update(d) + for f in range(N): + if cur[f] == X and f not in have: + D.append({f: Q(1)}) + return out, len(D) diff --git a/research/p104-post-cut-information-loss/verify.py b/research/p104-post-cut-information-loss/verify.py new file mode 100644 index 0000000000..6509f4c689 --- /dev/null +++ b/research/p104-post-cut-information-loss/verify.py @@ -0,0 +1,185 @@ +#!/usr/bin/env python3 +"""Verify the post-cut information-loss census for PR5718-shape leak classes on the PR6030 and PR5907 P104 words. +Apache-2.0. Python 3.12, standard library only. Checks: + (0) pinned input bytes: the PR6040 census module, the PR6045 correction module and the two words; + (1) the re-run class census equals PR6040's own census counts on both words; + (2) rank: the final field matrix has exact rank n = 770 on both words, so (rank never increases along a word) + every intermediate state has rank 770 and its left kernel has dimension N - n = 29; + (3) the left-kernel tracker holds 29 vectors at every cut; at every cut they are linearly independent and + annihilate the exact field matrix, hence they span the left kernel (by (2)); + (4) a randomized brute-force comparison of the tracker's redundant set with exact ranks on small words; + (5) the census: a leak class (cut i, pivot p) is 'information-lost' when p is outside the kernel support at i + (no post-cut linear program legalizes it, README Lemma 1); the residual classes go through the chart-local + combination closure and PR6045's span decision; + (6) the one residual PR5907 witness: an explicit 20-event chart-local correction program, lowered and simulated + directly, leaves every O output exactly equal to the original and passes PR6040's pairing test; three + perturbed programs are rejected; + (7) RESULT.json equals the recomputed receipt. +""" +from collections import Counter +from fractions import Fraction as Q +from hashlib import sha256 +from pathlib import Path +import importlib.util, json, random, sys, time + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PINS = {'inputs/shapesplit.py': '11e8ef691b28fb4f401a8c2e97b6d462e7a004f0e215a28579d6a654b4ca3304', # PR6040 1889253f + 'inputs/leakfix.py': 'dbbdc9ff9ebb55f1b9e832dcbe1aa5e407e7932a8d958a006bdaca6055e7f4ee'} # PR6045 23abc007 +for rel, h in PINS.items(): + if sha256((HERE/rel).read_bytes()).hexdigest() != h: + raise SystemExit('pinned input does not match: ' + rel) # checked before any imported code runs + + +def _load(name, path): + spec = importlib.util.spec_from_file_location(name, path) + mod = importlib.util.module_from_spec(spec); sys.modules[name] = mod; spec.loader.exec_module(mod) + return mod + + +SS = _load('pr6040_shapesplit', HERE/'inputs'/'shapesplit.py') # leakfix reuses this module object +L = _load('pr6045_leakfix', HERE/'inputs'/'leakfix.py') +sys.path.insert(0, str(HERE)) +import kernel as KM # noqa: E402 +import check as C # noqa: E402 + +WORDS = {'pr6030': 'research/p104-helper470-twin-rung-removal/WORD.json.gz', + 'pr5907': 'research/p104-helper468-rung-removal/WORD.json.gz'} +need = KM.need +WITNESS = {'word': 'pr5907', 'cut_after': 13776, 'pivot': 699, 'chart': 1031, + 'comb': {'696': '1', '698': '-1', '699': '1', '700': '-1', '702': '-1', '767': '-1', '792': '1'}, + 'targets': [[697, '1'], [698, '2'], [700, '-1']]} + + +def pins(): + src = json.loads((HERE/'SOURCES.json').read_text()) + for row in src['files']: + need(sha256((ROOT/row['path']).read_bytes()).hexdigest() == row['sha256'], 'pin ' + row['path']) + return {k: SS.read(ROOT/v) for k, v in WORDS.items()} + + +def exact_rank(rows): + piv = {} + for r in rows: + v = {k: x for k, x in r.items() if x} + while v: + k = min(v) + if k not in piv: + s = 1 / v[k]; piv[k] = {a: b * s for a, b in v.items()}; break + C.add(v, piv[k], -v[k]) + return len(piv) + + +def tracker_audit(w, cuts): + """Run the tracker alongside the exact field matrix; at every cut check |K| = N - n, independence, annihilation.""" + n = w['public']; m = w['owned_fields']; N = n + m + rows, cur = C.start(w) + K = KM.Kernel(N, range(n, N)) + out = {} + for t, e in enumerate(w['program']): + C.step(rows, cur, e); K.apply(e) + if t in cuts: + need(len(K.vecs) == N - n, 'tracker dimension N - n') + need(exact_rank(K.vecs) == N - n, 'tracker vectors independent') + for c in K.vecs: + acc = {} + for f, x in c.items(): + C.add(acc, rows[f], x) + need(not acc, 'tracker vector annihilates the field matrix') + out[t] = frozenset(K.support()) + need(exact_rank(rows) == n, 'final field matrix has rank n') + return out + + +def brute(seed=20261028, trials=300): + """Small random words: the tracker's redundant set equals {f : rank(W without f) = rank(W)} at every event.""" + rnd = random.Random(seed) + for _ in range(trials): + n, m = rnd.randint(1, 4), rnd.randint(0, 3); N = n + m + rows = [{r: Q(1)} if r < n else {} for r in range(N)] + K = KM.Kernel(N, range(n, N)) + for _ in range(rnd.randint(1, 12)): + r = rnd.randrange(N); f = rnd.choice([x for x in range(N) if x != r] or [r]) + op = rnd.choice(['ADD', 'ADD', 'SCALE', 'INIT', 'CLEAR', 'COPY'] if f != r else ['SCALE', 'INIT', 'CLEAR']) + q = Q(rnd.choice([-2, -1, 1, 2, 3]), rnd.choice([1, 2])) + e = {'ADD': ['ADD', r, f, str(q), 0], 'SCALE': ['SCALE', r, str(q), 0], 'INIT': ['INIT', r, 0], + 'CLEAR': ['CLEAR', r, 0], 'COPY': ['COPY', r, f, str(rnd.choice([0, 1, -2])), 0]}[op] + K.apply(e) + if op in ('INIT', 'CLEAR'): rows[r] = {} + elif op == 'SCALE': rows[r] = {k: v * q for k, v in rows[r].items()} + elif op == 'COPY': rows[r] = {k: v * Q(e[-2]) for k, v in rows[f].items() if v * Q(e[-2])} + else: C.add(rows[r], rows[f], q) + rk = exact_rank(rows) + red = {g for g in range(N) if exact_rank(rows[:g] + rows[g + 1:]) == rk} + need(K.support() == red, 'tracker redundant set equals brute-force rank test') + need(len(K.vecs) == N - rk and exact_rank(K.vecs) == N - rk, 'tracker dimension equals N - rank') + return trials + + +def census(w): + classes, counts = L.leak_classes(w) + need(counts == SS.census(w, 'empty')[0], 'class census equals PR6040 census') + leak = [c for c in classes if c['kind'] == 'leak'] + need(all(c['row_p'] for c in leak), 'retired value nonzero in every leak class') + supp = tracker_audit(w, {c['cut_after'] for c in leak}) + resid = [c for c in leak if c['pivot'] in supp[c['cut_after']]] + iv = {} + for c in resid: + iv[(c['cut_after'], c['pivot'])], _ = KM.closure_intervals(w, c['cut_after'], c['pivot']) + spans = L.correction_spans(w, resid, iv) + rows = [] + for ci, c in enumerate(resid): + kind, rho = L.decide(c, spans[ci]) + pts = iv[(c['cut_after'], c['pivot'])] + rows.append({'cut_after': c['cut_after'], 'pivot': c['pivot'], 'frame': c['frame'], 'leak': c['leak'], + 'usable_points': len(pts), 'charts': sorted({x[1] for x in pts}), + 'kind': kind if pts else 'no_usable_combination', 'rho': rho}) + return {'leak_classes': len(leak), 'information_lost': len(leak) - len(resid), 'residual': len(resid), + 'residual_kinds': dict(sorted(Counter(r['kind'] for r in rows).items())), 'residual_classes': rows}, classes + + +def witness(w, classes): + W = WITNESS; cut, p = W['cut_after'], W['pivot'] + batches = [{'after_event': cut, 'chart': W['chart'], 'comb': W['comb'], 'target': t, 'mu': mu} for t, mu in W['targets']] + zcol, ins = C.check(w, cut, p, batches) + cls = [c for c in classes if (c['cut_after'], c['pivot']) == (cut, p)] + need(len(cls) == 1 and cls[0]['kind'] == 'leak', 'witness class is a PR6040 leak class') + c = cls[0] + need(SS.functional_witness(c['A'], p, c['free'], zcol.get(p, Q(0))), 'PR6040 pairing test passes with rho = z-coefficient at p') + rejected = 0 + for bad in ([batches[0], batches[1], dict(batches[2], mu='-2')], batches[:2], + [dict(batches[0], mu='2'), batches[1], batches[2]]): + try: + C.check(w, cut, p, bad) + except ValueError: + rejected += 1 + need(rejected == 3, 'three perturbed programs rejected') + return {'class': {'cut_after': cut, 'pivot': p, 'frame': c['frame'], 'leak': c['leak'], 'V': w['final'][p]}, + 'batches': batches, 'inserted_events': len(ins), + 'inserted_ops': dict(sorted(Counter(e[0] for e in ins).items())), + 'z_column': {str(k): str(v) for k, v in sorted(zcol.items())}, 'perturbed_rejected': rejected} + + +def main(): + t0 = time.time() + ws = pins() + need(len(ws['pr6030']['program']) == 22803 and len(ws['pr5907']['program']) == 25998, 'word sizes') + print('pins ok', flush=True) + out = {'schema': 'p104-post-cut-information-loss/v1', 'brute_force_trials': brute()} + print('brute force ok', flush=True) + for k in ('pr6030', 'pr5907'): + out[k], classes = census(ws[k]) + print(k, out[k]['information_lost'], out[k]['residual'], out[k]['residual_kinds'], flush=True) + if k == WITNESS['word']: + out['pr5907_witness'] = witness(ws[k], classes) + print('witness', out['pr5907_witness']['z_column'], flush=True) + need(out['pr6030']['residual_kinds'].get('witness', 0) == 0, 'no residual witness on the selected PR6030 word') + text = json.dumps(out, indent=1, sort_keys=True) + '\n' + if '--write' in sys.argv: + (HERE/'RESULT.json').write_text(text) + need((HERE/'RESULT.json').read_text() == text, 'RESULT.json equals the recomputed receipt') + print('PASS_P104_POST_CUT_INFORMATION_LOSS (%.0f s)' % (time.time() - t0)) + + +if __name__ == '__main__': + main() From cab3e569a421166cdd20439e422004528e6b2620 Mon Sep 17 00:00:00 2001 From: josie Date: Wed, 28 Oct 2026 04:01:54 -0400 Subject: [PATCH 2/2] README: cite PR6088 for the cross-time residual Co-Authored-By: Claude Opus 5.5 --- research/p104-post-cut-information-loss/README.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/research/p104-post-cut-information-loss/README.md b/research/p104-post-cut-information-loss/README.md index 935c22915e..8cebdaff0f 100644 --- a/research/p104-post-cut-information-loss/README.md +++ b/research/p104-post-cut-information-loss/README.md @@ -125,7 +125,9 @@ compares the receipt byte for byte. - **Price the PR5907 witness.** Its 20 inserted events and the change of the z-column (it now reaches roles 698, 700 and 702 instead of 699) need the PR5599 complete signed bill. This matters only if a similar redundant class appears on the selected word. -- **Cross-time cancellation** on the 24 residual PR6030 classes (see Scope). +- **Cross-time cancellation** on the 24 residual PR6030 classes (see Scope). JoyboyBrian's + [PR #6088](https://github.com/CrocSwap/integer-mult-bounds/pull/6088) excludes one concrete two-ADD seam family for + helper 572. ## Credit