Certify the R439 K defect as the D-internal cross-term tally

research/r439-k-cross-term-tally/README.md

@@ -0,0 +1,109 @@
+# R439 K defect equals the D-internal cross-term tally
+
+**Finite certificate. No new kappa.** Selected κ stays
+0.001672660197076918. This does not adopt a weakened `K_equals_D` contract
+and does not change a paid profile.
+
+## Question
+
+PR #4092 left this comparison open on the three retained R439 helper-star
+words: does the syntactic `K_equals_D` defect equal the restored-edge cross
+terms introduced inside `D`? The first step named there is to compare the
+sector table with a D-internal propagation tally. Card `bit-helper-contract`,
+scope refined to that comparison.
+
+## Statement
+
+Fix a word with target count `v` and helper count `R`. Helper columns are the
+bits of registers `2v .. 2v+R-1`.
+
+- `K_t` is the helper-column mask on target `t` after the frame-free symbolic
+  replay of `(A, scatter, B)`. Register `r` starts as column `e_r`.
+- `N_t` is the XOR of the register ids named by `D`-gates whose destination
+  is target `t`.
+- `E_t` is the helper-column mask actually xored into target `t` when `D` is
+  executed alone from those same identity columns.
+- The cross-term tally is `C_t = E_t XOR (N_t restricted to helper columns)`.
+
+For an arbitrary `D` section, `C_t` also equals the XOR, over target writes,
+of (helper columns delivered by that write) XOR (helper registers that write
+names). Helper-to-helper gates affect `C` only by changing a later delivery.
+The syntactic defect `K_t XOR (N_t restricted to helper columns)` equals `C_t`
+exactly when `E_t = K_t`.
+
+## Result
+
+On all three pinned words, `E_t = K_t` for every one of the 111 targets, and
+every helper register is back to its own column at the end of `D`. Therefore
+the defect table and the cross-term tally are the same bit set:
+
+| word | `D` gates | targets | defect bits | sectors |
+|---|---:|---:|---:|---:|
+| `r439-helper-stars-seed19` candidate | 1,165 | 111 | 17,636 | 439 |
+| `r439-bsection-stars-seed01` composition | 1,165 | 111 | 17,636 | 439 |
+| `r439-bsection-stars-seed01` candidate | 1,195 | 111 | 17,653 | 439 |
+
+The owner checker agrees on the raw helper part and reports syntactic
+`K_equals_D` false on each word. Deleting the first helper-to-helper gate
+makes `E` differ from `K` on each word, so the match is not a property of
+`K` alone. A three-gate restored edge `h0 ^= h1`, `y ^= h0`, `h0 ^= h1`
+with an empty raw word has nonzero cross term `h1` and defect equal to the
+named column `h0`, so the equality is not true for every `D` section.
+
+The 17,636 and 17,653 figures are the same defect totals PR #4092 counted.
+This package adds the identification of those bits with executed-versus-named
+columns inside `D`, including target-to-target reads that carry helper
+columns written earlier in `D`. It does not re-derive the single-gate or
+single-bit repair census.
+
+## What is not established
+
+`E = K` is a certificate for these three words, not a replacement lemma.
+The synthetic edge is a counterexample to adopting "compare `K` with executed
+delivery" with no extra hypothesis. The 612 target-to-target reads inside
+`D` remain a separate H2 read-kind failure; matching the masks does not erase
+them. No supplier, native schedule, all-size transfer, or selected-frontier
+change is claimed. The bit side does not bind the selected exponent.
+
+## Reproduce
+
+From the repository root, CPython 3.12:
+
+```sh
+python3 -B research/r439-k-cross-term-tally/verify.py
+python3 -I -O -Werror -B research/r439-k-cross-term-tally/verify.py
+python3 scripts/research_package.py --package research/r439-k-cross-term-tally
+```
+
+Expected:
+
+```text
+PASS_R439_K_CROSS_TERM_TALLY words=3 targets=111/111/111 equal_targets=111/111/111 defect_bits=17636/17636/17653 cross_bits=17636/17636/17653 sectors=439/439/439 helpers_restored=3/3 checker_K_equals_D=false/false/false mutation_breaks=3/3 synthetic_unequal=1 no_new_kappa
+```
+
+The verifier exits nonzero on a pin mismatch, a target mismatch, a checker
+disagreement, a mutation that still matches, or a synthetic edge that fails
+to separate the two masks. Runtime is well under a minute.
+
+## Open next questions
+
+1. Which extra hypothesis makes `E = K` true outside this triple? The
+   synthetic edge shows an unconditional reading is false. One further pinned
+   helper-mixing word would separate a construction accident from a legal-word
+   identity. Admitting that hypothesis as the H2/K contract is a policy
+   decision, not a consequence of this tally.
+2. After the mask comparison is read as executed delivery, which H2 clauses
+   still fail on these words? The read-kind clause is the obvious candidate
+   and is not settled by the mask equality.
+
+## Credit
+
+The three words and the syntactic flag are the retained R439 helper-star
+lineage (PR #967 and PR #1062) checked by `research/e8-bit-p111-tuned`.
+PR #3533 isolates one restored helper edge whose literal mask misses the
+delivered column. PR #4092 (Nick Petalas) counts the resulting defect by
+helper sector on these words and leaves the propagation comparison open.
+This package answers that comparison only.
+
+Prepared by unpaidmoon with substantial AI assistance (Cursor Grok).
+Apache-2.0. Predecessor packages keep their own notices.

research/r439-k-cross-term-tally/SOURCES.json

@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5",
+      "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0"
+    },
+    {
+      "path": "research/e8-bit-p111-tuned/code/xcheck_p.py",
+      "usage": "input",
+      "git_blob": "184f5dcf94a486cc7db91ca4db5865916bf26009",
+      "sha256": "af3decc877e27c00001cf56f50c6c09566e8e101297ab34c7860aed96a06d80e"
+    },
+    {
+      "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-helper-stars-seed19/candidate.json.gz",
+      "usage": "input",
+      "git_blob": "8b0210d8b8e9524182e5f54f9bf93c28f4719735",
+      "sha256": "d8b08885e8ce9868200b2645189d15ed18a27fc2742e54990b3257a0ca4df6b8"
+    }
+  ]
+}

research/r439-k-cross-term-tally/TASK.json

@@ -0,0 +1,67 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-helper-contract",
+  "priority_revision": 6,
+  "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f",
+  "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 the three retained R439 helper-star words, test whether the K_equals_D defect equals the D-internal restored-edge cross-term tally, sector by sector. This is the released first step of PR #4092 open question 1, not an adopted weakened K contract.",
+  "scope_change_reason": "The card asks for one replacement H2/K implication or a counterexample. PR #4092 already showed that no sector-local or single-gate repair meets the syntactic flag. The released next comparison is whether that defect equals the executed-versus-syntactic gap inside D. Answering that comparison does not choose the admissible contract or reprice a profile.",
+  "bottleneck_link": "Side result on the non-binding bit supplier. The selected complex side and kappa are unchanged. The comparison says which bits a weakened K flag would have to forgive on these three words; it does not admit a helper-star replacement or a paid-profile improvement.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the three pinned words, the checker agreement, the one-gate deletion control and the synthetic restored-edge counterexample. Do not census another lineage or adopt a contract.",
+  "outcome": "completed",
+  "evidence": "Author-checked finite certificate: E = K on all 111 targets of all three words, so the K_equals_D defect equals the D-internal cross-term tally (17636/17636/17653 bits). Verifier research/r439-k-cross-term-tally/verify.py.",
+  "author": "unpaidmoon",
+  "ai_assistance": "Cursor Grok 4.7 session, including the verifier and the write-up. The certificate is the executed comparison against pinned words and the owner checker, not a model claim.",
+  "open_questions": [
+    {
+      "question": "For which additional hypothesis does K equal executed D delivery, beyond these three words?",
+      "why_it_matters": "The synthetic restored edge shows the equality is not true for an arbitrary D section paired with an arbitrary raw word, so it cannot be adopted as an unconditional replacement for K_equals_D.",
+      "first_step": "State one interface hypothesis that these three legal words satisfy and the synthetic edge violates, then test it on one other pinned helper-mixing word.",
+      "blocked_by": "No blocker for that one-word test. Admitting the hypothesis as the H2/K contract is a separate policy decision and is not made here."
+    },
+    {
+      "question": "Do the 612 target-to-target D reads remain an H2 failure after the mask comparison is weakened to executed delivery?",
+      "why_it_matters": "Matching K to executed delivery repairs only the syntactic helper-mask comparison. H2 also rejects non-helper reads. A replacement that ignores those reads is a different contract.",
+      "first_step": "Split the surviving H2 clauses on these words into frame clauses, destination clauses and read-kind clauses under the executed-delivery reading.",
+      "blocked_by": "None for the clause count. Pricing any repair is outside this certificate."
+    }
+  ]
+}

research/r439-k-cross-term-tally/VERIFY.json

@@ -0,0 +1,23 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/e8-bit-p111-tuned/code/xcheck_p.py",
+    "research/r439-bsection-stars-seed01/candidate.json.gz",
+    "research/r439-bsection-stars-seed01/composition.json.gz",
+    "research/r439-helper-stars-seed19/candidate.json.gz"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "SHA-256 pins; E equals K on every target of the three words; cross tally equals the defect; owner-checker raw K agrees and syntactic K_equals_D is false; deleting one helper edge breaks the match; a synthetic restored edge separates the defect from the cross term"
+    }
+  ]
+}