Split the R439 literal K defect into target reads and helper wraps across nine words (no new κ)

research/r439-target-closed-k-residual/README.md

@@ -0,0 +1,157 @@
+# R439 literal K defect: target reads versus helper wraps
+
+**Finite certificate on nine named words. No new κ.** The selected κ stays
+0.001672660197076918. This adopts no replacement `K_equals_D` contract, admits
+no supplier and changes no paid profile.
+
+## Question
+
+PR #4092 counted the literal `K_equals_D` defect on the three helper-star words
+(17,636 / 17,636 / 17,653 bits, all 439 helper sectors defective). It asked
+whether that pattern persists on other helper-mixing lineages. The merged
+`r439-k-cross-term-tally` package identified the defect with
+executed-versus-named columns inside `D`, but did not split it. This package
+asks which part comes from the 612 target-to-target reads and which part comes
+from helper-to-helper gates (helper wraps). Card `bit-helper-contract`, scope
+refined to that split.
+
+## Definitions
+
+Over GF(2), register `r` starts as column `e_r`. Helper columns are registers
+`2v .. 2v+R-1` (`v = 111`, `R = 439`).
+
+- `K_t`: helper part of target `t` after the frame-free replay of `(A, scatter, B)`.
+- `N_t`: helper columns named by `D` gates that write target `t` (the literal mask).
+- `N*_t`: helper columns reaching target `t` when `D` is replayed with every
+  helper-to-helper gate skipped (the *target-read-closed* named mask).
+- `E_t`: helper columns reaching target `t` when `D` is replayed in full.
+- `T_t = N*_t + N_t`: the part carried by target-to-target reads.
+- `H_t = K_t + N*_t`: the residual left by helper wraps.
+
+The literal defect is `K_t + N_t = T_t + H_t`. On every word below `E = K`, so
+`H_t = E_t + N*_t`: exactly the extra columns that wrapped helpers deliver.
+
+## Result
+
+| word | D gates | helper gates | literal \|K+N\| | target-read \|T\| | residual \|H\| | \|T∧H\| | residual sectors = donors | sectors passing after closure |
+|---|---:|---:|---:|---:|---:|---:|---:|---:|
+| PR915 target basis | 723 | 0 | 17,095 | 17,095 | **0** | 0 | 0 | 439 / 439 |
+| PR926 disjoint pairs | 1,107 | 384 | 17,485 | 13,148 | 7,447 | 1,555 | 192 | 247 / 439 |
+| PR941 matching candidate | 1,121 | 398 | 17,514 | 13,008 | 7,786 | 1,640 | 199 | 240 / 439 |
+| PR941 floor word | 1,121 | 398 | 17,505 | 12,885 | 7,776 | 1,578 | 199 | 240 / 439 |
+| helper triples | 1,191 | 468 | 17,541 | 12,444 | 8,685 | 1,794 | 232 | 207 / 439 |
+| PR1062 pair control | 1,099 | 376 | 17,504 | 13,110 | 7,424 | 1,515 | 188 | 251 / 439 |
+| PR967 helper stars | 1,165 | 442 | 17,636 | 12,275 | 8,767 | 1,703 | 221 | 218 / 439 |
+| PR1062 composition | 1,165 | 442 | 17,636 | 12,275 | 8,767 | 1,703 | 221 | 218 / 439 |
+| PR1062 candidate | 1,195 | 472 | 17,653 | 12,092 | 9,163 | 1,801 | 236 | 203 / 439 |
+
+Bit counts satisfy `|K+N| = |T| + |H| − 2|T∧H|` on every word. Each word has
+612 `D` gates that write a target and read another target. The literal defect
+touches all 439 helper sectors on every word.
+
+What this establishes on these nine words:
+
+1. **Target reads, not helper mixing, account for the whole literal defect of
+   the helper-free base.** PR915's `D` has no helper-to-helper gate, yet its
+   literal defect is 17,095 bits across all 439 sectors. Closing the named mask
+   under target reads removes all of it: `K = N*` exactly.
+2. **On every helper-mixing word, the residual support is exactly the donor
+   set.** Call a helper a donor when some helper-to-helper gate reads it. The
+   helper sectors carrying residual bits are exactly the donors: 192, 199, 199,
+   232, 188, 221, 221 and 236. On the star words the donors are the 221 / 236
+   star leaves and the 157 / 162 written helpers are the centres. Donors and
+   written helpers are disjoint except for 28 helpers in the triple word.
+3. **The "every sector is defective" reading of PR #4092 comes from target
+   reads.** After target-read closure, 203–251 helper sectors per mixing word
+   satisfy the sector-local condition (no residual bit in that column). The
+   defect left to forgive is concentrated on donor columns: 7,424–9,163 bits,
+   versus 17,485–17,653 literal bits.
+4. `E = K` and all 439 helpers end `D` restored on all nine words. No
+   non-helper column survives in any `N_t`. This extends the cross-term tally's
+   `E = K` certificate from three words to nine.
+
+## Controls
+
+The verifier runs six controls:
+
+- Two-target synthetic `y0 ^= h0; y1 ^= y0` with `K = (h0, h0)`. The literal
+  defect is one bit; `T` is that bit and the residual is zero.
+- Restored wrap `h0 ^= h1; y ^= h0; h0 ^= h1` with semantic `K = h0 + h1`.
+  `E = K` and the residual is the single donor column `h1`.
+- The same wrap against `K = h0` (the cross-term tally's synthetic edge).
+  `E ≠ K`, yet the closed mask reports **zero** residual. Thus `K = N*` alone is
+  **not** a sound replacement check once helper gates are present. A contract
+  built on `N*` must still charge or check the wraps (for example `E = K` with
+  restored helpers).
+- Deleting the first helper-to-helper gate of the PR967 star word breaks both
+  `E = K` and helper restoration.
+- Deleting the first helper-carrying target-to-target read of PR915 leaves a
+  nonzero residual, so PR915's zero residual is not a property of `K` alone.
+- PR #3904's pair on the PR967 star word: target register 112, helper register
+  260 (helper index 38), donor of `D` gate 0 `280 ^= 260`. The bit is in `K` and
+  absent from `N` and `N*`, so it lies in both the literal defect and `H`.
+
+## Correction to PR #4092
+
+PR #4092 (`r439-star-kdefect-sectors`, same author) states that the #3904 pair
+is **not** in the official W0 defect set, because the "sector of column 260"
+has 57 defective targets that exclude 112. That statement is wrong. It mixed
+register numbers with indices. Register 260 is helper index 38. Sector 38 has
+57 defective targets, and they include target index 1, which is register 112.
+#4092 searched for target index 112, which does not exist (`v = 111`). Running
+#4092's own `verify.py --json` confirms this: sector `"38"` lists 57 targets
+including `1`. So the #3904 pair is in the official W0 defect set, and #3904
+agrees with #4092 on it. The two do not use different raw-word definitions for
+this bit. #4092's census totals, sector counts and controls are unaffected. This
+package does not edit #4092's files. The sixth control above pins the corrected
+fact.
+
+## What is not established
+
+This is a finite certificate on nine named words. It does not adopt `K = N*`,
+`E = K` or any other replacement for `K_equals_D` or H2; the third control
+shows `K = N*` alone is unsound with helper gates. The 612 target-to-target
+reads remain a literal H2 read-kind failure. No frame, native schedule, hosted
+invoice, all-size transfer, supplier admission or selected-frontier change is
+claimed. The bit side does not bind the selected exponent.
+
+## Reproduce
+
+From the repository root, CPython 3.12, standard library only (about 0.1 s):
+
+```sh
+python3.12 -B research/r439-target-closed-k-residual/verify.py
+python3.12 scripts/research_package.py --package research/r439-target-closed-k-residual
+```
+
+Expected:
+
+```text
+PASS_R439_TARGET_CLOSED_K_RESIDUAL words=9 pr915_residual=0 star_residual=8767/8767/9163 sectors_equal_donors=9/9 controls=6 no_new_kappa
+```
+
+`verify.py --json OUT` writes the per-word record, including target-read counts,
+donor and written-helper counts and sector-pass counts. All nine inputs are
+bound by SHA-256 in [SOURCES.json](SOURCES.json).
+
+## Open next questions
+
+1. **Can a donor-sector contract replace `K_equals_D` on these words?** A
+   candidate is "`K = N*` plus, for each restored wrap, the donor columns
+   delivered while the wrap is open". It would be checkable from `D` alone and
+   would reject the third control. First step: state it for well-nested
+   restored wraps and test it on the nine words and the controls. Blocker:
+   adopting it as the H2/K interface is a maintainer policy decision.
+2. **Do target reads still fail H2 after closure?** Closing the mask removes
+   the K mismatch from target reads but not H2's read-kind clause. First step:
+   check whether the PR915 semantic substitution proof already covers
+   target-read closure, so the 612 reads need no separate repair.
+
+## Credit
+
+Produced by Nick Petalas. Words and predecessor results are retained unchanged
+with their own attribution: Gareth Davidson (PR915 target basis, PR926 helper
+pairs, `r439-helper-matching` / PR941), Ross Richardson (`r439-helper-triples`),
+Sricharan Vagvala (`r439-helper-stars-seed19`, PR967 lineage), Sagar Thakrar
+(PR1062 `r439-bsection-stars-seed01`), the PR4092 sector census and the
+`r439-k-cross-term-tally` package. Apache-2.0.

research/r439-target-closed-k-residual/SOURCES.json

@@ -0,0 +1,72 @@
+{
+  "schema_version": 1,
+  "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65",
+      "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96"
+    },
+    {
+      "path": "research/r439-bsection-stars-seed01/candidate.json.gz",
+      "usage": "input",
+      "git_blob": "9a17b4920334878d6c949191f6931bd97126fe3c",
+      "sha256": "b452d2c2b0b2a546d1105b1da9769aa78e5c54d6f00e97b30c77e3f54ce445ee"
+    },
+    {
+      "path": "research/r439-bsection-stars-seed01/composition.json.gz",
+      "usage": "input",
+      "git_blob": "d95fc2bf795fd9ef8d8bae9d70693c5e64948cec",
+      "sha256": "0203fea9fa442ca206fe683aa5b6860adac680d63b9fb8be6bd42b39aa7b5cce"
+    },
+    {
+      "path": "research/r439-bsection-stars-seed01/pair_control.json.gz",
+      "usage": "input",
+      "git_blob": "16972bc96de0c81321eb2feef70766c403017016",
+      "sha256": "628ebfebe215e153338e88e2e324040d139a111eebfb090929697c7a0b6f3f59"
+    },
+    {
+      "path": "research/r439-helper-matching/candidate.json.gz",
+      "usage": "input",
+      "git_blob": "b3befb831854157e14512ac40fa48dbea289d105",
+      "sha256": "60531408445a1d7c793dff6821e767739012db1d2646f49aec7fdf7fe0b979f3"
+    },
+    {
+      "path": "research/r439-helper-matching/floor-word.json.gz",
+      "usage": "input",
+      "git_blob": "906e935541d6a5d2ca40d2885e21e46b4675b0ee",
+      "sha256": "4be50c06f91bc605660d4f9fba865c330f82dc4c364041870b725c220d16244e"
+    },
+    {
+      "path": "research/r439-helper-matching/vendor/pr915/candidate.json.gz",
+      "usage": "input",
+      "git_blob": "7f1f188f516ca4661f419dc72114751abf3cc920",
+      "sha256": "ac30266144f8772ec8cd629153993aa9eb692fe745a9f95015a1b7fa88977a2e"
+    },
+    {
+      "path": "research/r439-helper-matching/vendor/pr926/candidate.json.gz",
+      "usage": "input",
+      "git_blob": "0a192829589d6cbcec0f32695a928d24e6c33549",
+      "sha256": "6ac771545e823c054e005429c405dbb2c01ff80fce181b714e1af5e28b6b7cb2"
+    },
+    {
+      "path": "research/r439-helper-stars-seed19/candidate.json.gz",
+      "usage": "input",
+      "git_blob": "8b0210d8b8e9524182e5f54f9bf93c28f4719735",
+      "sha256": "d8b08885e8ce9868200b2645189d15ed18a27fc2742e54990b3257a0ca4df6b8"
+    },
+    {
+      "path": "research/r439-helper-triples/candidate.json.gz",
+      "usage": "input",
+      "git_blob": "e74d3a8edecac5ca9262b774a965702c19207bea",
+      "sha256": "11f5c75711090892827d536b6bf82b4001e02ebd13d10e87a1aa915a4e78704b"
+    }
+  ]
+}

research/r439-target-closed-k-residual/TASK.json

@@ -0,0 +1,67 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-helper-contract",
+  "priority_revision": 7,
+  "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+  "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": "refined",
+  "actual_scope": "On nine pinned R439 D words from four lineages (PR915 helper-free basis, PR926/PR941 pairs, helper triples, PR1062 pair control, three helper-star words), split the literal K_equals_D defect into the part carried by target-to-target reads and the residual left by helper-to-helper gates. Answers PR #4092 open question 2; no replacement contract is adopted.",
+  "scope_change_reason": "The card asks for a replacement H2/K implication or a counterexample. Before stating one, the defect it must forgive needs to be located. PR #4092 counted it and r439-k-cross-term-tally identified it with executed-versus-named columns, but neither separated target reads from helper wraps. This split shows what a helper-mixing replacement actually has to cover.",
+  "bottleneck_link": "Side result on the non-binding bit supplier. The selected complex side and kappa are unchanged. It narrows the defect a helper-wrap replacement for K_equals_D must forgive to the donor sectors, and shows target-read closure alone is unsound once helper gates exist.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the nine pinned words, the exact split table, the donor-support identity and six controls. Do not adopt a contract, reprice a profile or search for new words.",
+  "outcome": "completed",
+  "evidence": "Author-checked finite certificate: PR915 residual is 0 of 17,095 literal bits; on the eight helper-mixing words the residual support equals the donor set (192-236 sectors) and 203-251 sectors pass after target-read closure. E = K and helpers restore on all nine. Verifier research/r439-target-closed-k-residual/verify.py. Also corrects PR #4092's statement that the PR3904 pair lies outside the defect set (register/index mix-up).",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can a donor-sector contract (K = N* plus donor columns delivered while each restored wrap is open) replace K_equals_D on these words?",
+      "why_it_matters": "It would be checkable from D alone, would reject the mismatched-K control that K = N* accepts, and would cover exactly the residual this package locates.",
+      "first_step": "State it for well-nested restored wraps and test it on the nine words and the six controls.",
+      "blocked_by": "Adopting it as the H2/K interface is a maintainer policy decision; the finite test has no blocker."
+    },
+    {
+      "question": "Does the PR915 semantic substitution proof already cover target-read closure, so the 612 target-to-target reads need no separate H2 repair?",
+      "why_it_matters": "Closure removes the K mismatch from target reads but not H2's literal read-kind clause.",
+      "first_step": "Read PR915's PROOF.md substitution argument against the N* definition used here.",
+      "blocked_by": "None."
+    }
+  ]
+}

research/r439-target-closed-k-residual/VERIFY.json

@@ -0,0 +1,28 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/r439-bsection-stars-seed01/candidate.json.gz",
+    "research/r439-bsection-stars-seed01/composition.json.gz",
+    "research/r439-bsection-stars-seed01/pair_control.json.gz",
+    "research/r439-helper-matching/candidate.json.gz",
+    "research/r439-helper-matching/floor-word.json.gz",
+    "research/r439-helper-matching/vendor/pr915/candidate.json.gz",
+    "research/r439-helper-matching/vendor/pr926/candidate.json.gz",
+    "research/r439-helper-stars-seed19/candidate.json.gz",
+    "research/r439-helper-triples/candidate.json.gz"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "SHA-256 pins; exact split table on nine words; residual support equals the donor set; E equals K and helpers restore; published 17636/17653 literal totals; six controls including the unsound K = N* case; PR3904 pair located in K, N, N* (corrects PR4092's comparison)"
+    }
+  ]
+}