Mister-Meeseeks · Oct 28, 2026 · Oct 28, 2026 · Oct 28, 2026
diff --git a/research/p104-pr5718-leak-correction/README.md b/research/p104-pr5718-leak-correction/README.md
@@ -0,0 +1,100 @@
+# No inserted carrier correction legalizes a PR5718-shape leak class on the PR6030 P104 word
+
+**Scoped exact result; no new κ.** Base: canonical main `a2b4b0395e293dded1cb17b4e78910b364af2343`; inputs rechecked unchanged at
+`721c03822`. The selected record is unchanged by this package.
+
+Nick Petalas's [PR #6040](https://github.com/CrocSwap/integer-mult-bounds/pull/6040) (`shapesplit.py`, pinned
+here as `inputs/shapesplit.py` from head `1889253f`) finds no PR5718-shape helper split on the PR5907 word. Every
+candidate class either *leaks*, meaning the new helper's direction `d = S e_p` reaches a role whose final chart is
+not `V`, or fails the pairing. It released step (3) of its claim: output corrections at later meetings. This
+package takes that step. It runs on the merged
+[PR #6030](https://github.com/CrocSwap/integer-mult-bounds/pull/6030) word (DreamingOfClouds, κ .003125804), which
+became the selected word at main `721c03822` while this package was being prepared (the input bytes are unchanged),
+and repeats the run on PR5907.
+
+## Result
+
+| Word | Leak classes | Carrier sources | Legalized by an inserted carrier correction |
+|---|---:|---:|---:|
+| PR6030 | 4,033 (390 leak to one role) | **0** | **0** |
+| PR5907 | 4,206 (425 leak to one role) | **0** | **0** |
+
+On both words, no **single** inserted chart-local ADD or SCALE after the cut clears the defect outside `V`, in any
+leak class. Neither does any correction program whose sources all lie along the defect direction. The PR6040
+suggestion `r += q·new` (a correction from a pure multiple of the new helper `z`) cannot clear a leak, with any
+number of corrections. The z-part alone is easy to satisfy. That is why PR6040's z-only criterion is not a useful
+filter once corrections are allowed.
+
+## Why (exact, from linearity)
+
+Fix a class: cut after event `i`, helper `p` at chart `F`, `V = final[p]`, `O` = roles whose final chart is not
+`V`. Let `ℓ = row_p(i)·X` be the value the split retires. In the split word, field `f` holds
+`orig_f(t) + β_f(t)(z − ℓ)` after event `t`. Here `β_f(t)` is the coefficient with which `p`'s cut content reaches
+`f`. So the split outputs are `orig + d ⊗ (z − ℓ)`, and a legal split needs the **O-defect** `d_O ⊗ (z − ℓ)` removed
+(with `z` still reaching a `V`-final output). Insert ADDs `r'_k += q_k f_k` after events `t_k`. The telescoping
+identity for products gives the exact change: `Σ_k q_k S_{t_k} e_{r'_k} ⊗ (corrected value of f_k at t_k)`, where
+`S` is the suffix map of the original word. Hence:
+
+1. **Pure-z sources never suffice.** They add only multiples of `z`, so the `−d_O ⊗ ℓ` part stays. `ℓ ≠ 0` in every
+   leak class (checked). On PR6030's leak-one classes, the z-part screen finds 124 classes it would pass (all
+   4,033 classes, local run: 2,071 pass, 703 by one correction). The direct simulator (`check.py`) confirms for
+   three of them that the z-leak is cleared while the O output keeps a non-z defect.
+2. **A single correction needs a carrier.** For `q v_O ⊗ value_f = −d_O ⊗ (z − ℓ)`, `v_O` must be proportional to
+   `d_O` and `value_f` to `z − ℓ`. That means `orig_f(t) = 0` with `β_f(t) ≠ 0`. A SCALE is the case `f = r'`.
+3. **Carrier programs need a first carrier.** Corrections from carriers add multiples of `z − ℓ` and leave every
+   `orig_f` unchanged. So the first correction in time needs a carrier of the uncorrected word.
+
+The census (`leakfix.py`) tracks `β` for every leak class in one forward pass. It finds **no field, at any event
+after any cut, that is zero in the original word while carrying the cut content**. Items 2 and 3 then exclude all
+4,033 + 4,206 classes. The span machinery (one backward pass of suffix columns) decides the general carrier-source
+equation `d_O + Σ μ_k (v_k)_O = 0` exactly over Q. It rejects solutions that erase `z` from every `V`-final output,
+and it applies PR6040's pairing test to the corrected `d'_p`.
+
+**Positive control.** On the PR5713 word, a carrier and a leak are planted after PR5718's own cut (event 14330,
+chart 602, helper 708): `INIT s; s += p | cut | s −= p; o += p` with `o = 128`. The class leaks to three roles. The
+census finds the single correction `o += s` (μ = −1), and the independent simulator accepts it with no z-leak and no
+non-z defect outside `V`. A doubled coefficient is rejected.
+
+## Reproduce
+
+Python 3.12, standard library, from the repository root (about 90 s):
+
+```sh
+python3.12 -B research/p104-pr5718-leak-correction/verify.py
+python3.12 -B scripts/research_package.py --package research/p104-pr5718-leak-correction
+```
+
+Marker: `PASS_P104_PR5718_LEAK_CORRECTION`. `--write` regenerates `RESULT.json`. Normal replay is read-only and
+compares it byte for byte. The full pure-z screen over all PR6030 classes (`leakfix.run(w, mode='purez')`) takes
+about 7 minutes. It is local-only evidence and is not in the verifier.
+
+A side check (local only, not in the verifier): Matarener's PR5994 `splitcensus.py` and PR6040's census on the
+PR6030 word give 0 witnesses each (8,734 evaluations; group and boundary supports; both input rules).
+
+## Scope and limits
+
+- Scalar O-defect condition only, at the level of PR5994/PR6040: no `V` normalization legality beyond "z still
+  reaches `V`", and no native maps, owned lifetimes, caller, compiler, precision or outer checks.
+- Covered edits: inserted chart-local ADD/SCALE events after the cut; programs of such events whose sources are all
+  carriers in the corrected word; any number of pure-z corrections. **Not covered:** several corrections with
+  non-carrier sources whose rank-one terms combine to `d_O ⊗ (z − ℓ)`; this includes several ADDs into one
+  target from fields whose combination is a carrier. Rewriting existing events, new MOVEs (paid), and injections
+  other than PR5718's unit injection `b = e_p` are also not covered.
+- The census accepts only the PR6040 class list, so it inherits PR6040's input rule ('empty') and class definition.
+
+## Open next questions
+
+- **Combination carriers.** Is some combination of the fields at a chart zero in the original word but nonzero in
+  `β`, at some event after a cut? That would enable multi-ADD corrections. First step: for each event and touched
+  chart, test whether appending the `β` column raises the rank of the field rows. Blocked by speed: a direct
+  Fraction rank test did not finish a 1/50 class subsample in ten minutes. It needs incremental rank maintenance
+  per chart.
+- **Edits that rewrite events.** Changing one existing ADD coefficient after the cut changes the original map and
+  falls outside the identity above. First step: allow one coefficient change and repeat the defect equation.
+
+## Credit
+
+Nick Petalas (PR6040 census and class definition, pinned unmodified), Matarener (PR5994 census and pure-subspace
+decision), flyingviper (PR5718 split shape), Ali Romman (PR5599 split criterion) and DreamingOfClouds (PR5907 and
+PR6030 words) 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-pr5718-leak-correction/RESULT.json b/research/p104-pr5718-leak-correction/RESULT.json
@@ -0,0 +1,296 @@
+{
+ "planted_control": {
+  "class": {
+   "cut_after": 14332,
+   "frame": 602,
+   "kind": "witness",
+   "leak": 3,
+   "pivot": 708
+  },
+  "correction": {
+   "after_event": 14334,
+   "chart": 602,
+   "mu": "-1",
+   "source": 752,
+   "target": 128
+  },
+  "perturbed_rejected": true,
+  "z_leak_before": [
+   128,
+   156,
+   199
+  ]
+ },
+ "pr5907_carrier": {
+  "carrier_sources": 0,
+  "kinds": {
+   "unreachable": 4206
+  },
+  "leak_classes": 4206,
+  "leak_classes_by_leak_count": {
+   "1": 425,
+   "10": 104,
+   "102": 5,
+   "105": 3,
+   "11": 21,
+   "12": 28,
+   "14": 35,
+   "15": 78,
+   "16": 130,
+   "17": 18,
+   "18": 10,
+   "19": 30,
+   "2": 793,
+   "20": 47,
+   "21": 6,
+   "23": 14,
+   "24": 5,
+   "25": 11,
+   "26": 23,
+   "3": 84,
+   "30": 9,
+   "32": 10,
+   "33": 6,
+   "34": 6,
+   "35": 3,
+   "36": 7,
+   "37": 5,
+   "38": 3,
+   "4": 399,
+   "40": 8,
+   "42": 7,
+   "43": 6,
+   "44": 9,
+   "45": 31,
+   "46": 5,
+   "47": 11,
+   "49": 52,
+   "5": 28,
+   "50": 33,
+   "51": 121,
+   "52": 132,
+   "53": 157,
+   "54": 3,
+   "55": 7,
+   "56": 50,
+   "57": 56,
+   "58": 39,
+   "59": 35,
+   "6": 26,
+   "60": 28,
+   "61": 51,
+   "62": 16,
+   "63": 27,
+   "64": 29,
+   "65": 23,
+   "66": 14,
+   "67": 21,
+   "68": 34,
+   "69": 60,
+   "7": 43,
+   "70": 18,
+   "71": 53,
+   "72": 38,
+   "73": 3,
+   "74": 20,
+   "75": 157,
+   "76": 26,
+   "77": 86,
+   "78": 14,
+   "79": 19,
+   "8": 57,
+   "80": 21,
+   "81": 24,
+   "82": 6,
+   "83": 15,
+   "85": 13,
+   "86": 5,
+   "87": 12,
+   "88": 4,
+   "89": 27,
+   "9": 26,
+   "90": 25,
+   "91": 24,
+   "92": 12,
+   "94": 2,
+   "95": 15,
+   "97": 2,
+   "98": 2
+  },
+  "pr6040_counts": {
+   "evaluations": 8913,
+   "kind_leak": 4206,
+   "kind_pairing": 4,
+   "no_helper_prefix": 6374,
+   "pivots": 516,
+   "witnesses": 0
+  }
+ },
+ "pr6030_carrier": {
+  "carrier_sources": 0,
+  "kinds": {
+   "unreachable": 4033
+  },
+  "leak_classes": 4033,
+  "leak_classes_by_leak_count": {
+   "1": 390,
+   "10": 106,
+   "102": 5,
+   "105": 1,
+   "107": 2,
+   "11": 25,
+   "116": 2,
+   "117": 2,
+   "12": 31,
+   "14": 44,
+   "15": 68,
+   "16": 118,
+   "17": 16,
+   "18": 14,
+   "19": 36,
+   "2": 810,
+   "20": 50,
+   "21": 7,
+   "23": 13,
+   "24": 6,
+   "25": 11,
+   "26": 23,
+   "3": 83,
+   "30": 9,
+   "32": 10,
+   "33": 12,
+   "34": 4,
+   "35": 3,
+   "36": 10,
+   "37": 8,
+   "38": 4,
+   "4": 396,
+   "40": 8,
+   "42": 7,
+   "43": 4,
+   "44": 12,
+   "45": 22,
+   "46": 12,
+   "47": 13,
+   "49": 65,
+   "5": 28,
+   "50": 43,
+   "51": 117,
+   "52": 154,
+   "53": 153,
+   "55": 7,
+   "56": 52,
+   "57": 45,
+   "58": 35,
+   "59": 36,
+   "6": 27,
+   "60": 36,
+   "61": 57,
+   "62": 19,
+   "63": 28,
+   "64": 27,
+   "65": 19,
+   "66": 9,
+   "67": 25,
+   "68": 26,
+   "69": 54,
+   "7": 42,
+   "70": 16,
+   "71": 50,
+   "72": 30,
+   "74": 17,
+   "75": 73,
+   "76": 16,
+   "77": 39,
+   "78": 9,
+   "79": 16,
+   "8": 68,
+   "80": 16,
+   "81": 21,
+   "82": 2,
+   "83": 6,
+   "85": 18,
+   "87": 11,
+   "88": 1,
+   "89": 35,
+   "9": 27,
+   "90": 25,
+   "91": 12,
+   "92": 10,
+   "94": 2,
+   "95": 12
+  },
+  "pr6040_counts": {
+   "evaluations": 8734,
+   "kind_leak": 4033,
+   "kind_pairing": 4,
+   "no_helper_prefix": 6275,
+   "pivots": 516,
+   "witnesses": 0
+  }
+ },
+ "pr6030_purez_leak1": {
+  "classes": 390,
+  "demonstrations": [
+   {
+    "O_nonz_defect_after": [
+     218
+    ],
+    "correction": {
+     "after_event": 13741,
+     "chart": 1049,
+     "mu": "1",
+     "source": 681,
+     "target": 683
+    },
+    "cut_after": 13741,
+    "pivot": 681,
+    "z_leak_before": [
+     218
+    ]
+   },
+   {
+    "O_nonz_defect_after": [
+     153
+    ],
+    "correction": {
+     "after_event": 14763,
+     "chart": 1049,
+     "mu": "1",
+     "source": 680,
+     "target": 685
+    },
+    "cut_after": 13747,
+    "pivot": 680,
+    "z_leak_before": [
+     153
+    ]
+   },
+   {
+    "O_nonz_defect_after": [
+     153
+    ],
+    "correction": {
+     "after_event": 14763,
+     "chart": 1049,
+     "mu": "1",
+     "source": 680,
+     "target": 685
+    },
+    "cut_after": 13749,
+    "pivot": 680,
+    "z_leak_before": [
+     153
+    ]
+   }
+  ],
+  "kinds": {
+   "erased": 17,
+   "pairing": 249,
+   "witness": 124
+  },
+  "single_and_pairing_witness": 51,
+  "single_corrections": 298
+ },
+ "schema": "p104-pr5718-leak-correction/v1"
+}