From a0e0aa3e37116df0f382ad70d9039eb1a95bdb3b Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Tue, 20 Oct 2026 01:39:10 +0000 Subject: [PATCH] Certify the R439 K defect as the D-internal cross-term tally On the three retained helper-star words, executed D delivery matches the raw helper part on every target, so the syntactic K_equals_D defect is exactly that cross-term tally. No new kappa. Co-authored-by: unpaidmoon --- research/r439-k-cross-term-tally/README.md | 109 ++++++++ research/r439-k-cross-term-tally/SOURCES.json | 42 +++ research/r439-k-cross-term-tally/TASK.json | 67 +++++ research/r439-k-cross-term-tally/VERIFY.json | 23 ++ research/r439-k-cross-term-tally/verify.py | 260 ++++++++++++++++++ 5 files changed, 501 insertions(+) create mode 100644 research/r439-k-cross-term-tally/README.md create mode 100644 research/r439-k-cross-term-tally/SOURCES.json create mode 100644 research/r439-k-cross-term-tally/TASK.json create mode 100644 research/r439-k-cross-term-tally/VERIFY.json create mode 100644 research/r439-k-cross-term-tally/verify.py diff --git a/research/r439-k-cross-term-tally/README.md b/research/r439-k-cross-term-tally/README.md new file mode 100644 index 0000000000..8f0ff04f83 --- /dev/null +++ b/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. diff --git a/research/r439-k-cross-term-tally/SOURCES.json b/research/r439-k-cross-term-tally/SOURCES.json new file mode 100644 index 0000000000..66d75a7d77 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/r439-k-cross-term-tally/TASK.json b/research/r439-k-cross-term-tally/TASK.json new file mode 100644 index 0000000000..b31fa07eb5 --- /dev/null +++ b/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." + } + ] +} diff --git a/research/r439-k-cross-term-tally/VERIFY.json b/research/r439-k-cross-term-tally/VERIFY.json new file mode 100644 index 0000000000..35fd45fd6b --- /dev/null +++ b/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" + } + ] +} diff --git a/research/r439-k-cross-term-tally/verify.py b/research/r439-k-cross-term-tally/verify.py new file mode 100644 index 0000000000..7be531810e --- /dev/null +++ b/research/r439-k-cross-term-tally/verify.py @@ -0,0 +1,260 @@ +#!/usr/bin/env python3 +"""D-internal cross-term tally for the retained R439 helper-star K defect. + +On each pinned word, K is the helper-column mask that the frame-free replay of +(A, scatter, B) leaves on each target. N is the syntactic XOR of register ids +named by D-gates that write that target. E is the helper-column mask actually +xored into the target when D is executed alone from identity columns. + +The cross-term tally is C = E XOR (N restricted to helper columns). It also +equals the per-gate XOR of (delivered helper columns XOR named helper columns). +The K_equals_D defect is K XOR (N restricted to helper columns). Those two +masks agree on a target exactly when E = K. + +This script checks that agreement on the three words named by PR #4092, agrees +with the owner checker that the syntactic flag is false, and rejects two +controls: deleting one helper-to-helper gate, and a synthetic restored edge +whose raw word is empty. +""" +import gzip +import hashlib +import importlib.util +import json +import os +import sys + +HERE = os.path.dirname(os.path.abspath(__file__)) +ROOT = os.path.abspath(os.path.join(HERE, "..", "..")) +WORDS = ( + ("helper_star", "research/r439-helper-stars-seed19/candidate.json.gz"), + ("composition", "research/r439-bsection-stars-seed01/composition.json.gz"), + ("candidate", "research/r439-bsection-stars-seed01/candidate.json.gz"), +) +CHECKER = "research/e8-bit-p111-tuned/code/xcheck_p.py" + + +def fail(message): + raise SystemExit("FAIL_R439_K_CROSS_TERM_TALLY " + message) + + +def sha256(path): + digest = hashlib.sha256() + with open(path, "rb") as handle: + for chunk in iter(lambda: handle.read(1 << 20), b""): + digest.update(chunk) + return digest.hexdigest() + + +def load_word(path): + with gzip.open(path, "rt", encoding="utf-8") as handle: + word = json.load(handle) + if not isinstance(word, dict) or "D" not in word or "v" not in word: + fail("word is not a D-section object: " + path) + return word + + +def helper_mask(word): + return ((1 << word["R"]) - 1) << (2 * word["v"]) + + +def syntactic_N(word): + """Register-id mask named by D-gates that write each target.""" + width = word["v"] + named = [0] * width + for _frame, dest, srcs in word["D"]: + if width <= dest < 2 * width: + acc = 0 + for src in srcs: + acc ^= 1 << src + named[dest - width] ^= acc + return named + + +def raw_K(word): + """Helper columns on each target after (A, scatter, B), frames off.""" + width, helpers = word["v"], word["R"] + columns = 2 * width + helpers + mask = helper_mask(word) + val = [1 << reg for reg in range(columns)] + for name in ("A", "scatter", "B"): + if name == "scatter": + copies = [val[reg] for reg in word["ret"]] + for target, row in enumerate(word["scatter"]): + acc = 0 + for index in row: + acc ^= copies[index] + val[width + target] ^= acc + else: + for _frame, dest, srcs in word[name]: + acc = 0 + for src in srcs: + acc ^= val[src] + val[dest] ^= acc + return [val[width + target] & mask for target in range(width)] + + +def executed_D(word): + """Execute D from identity columns. + + Returns E, the per-gate cross tally, and whether every helper register is + back to its own column. E XOR (syntactic helper mask) equals the cross + tally for any D section; that identity is checked by the caller. + """ + width, helpers = word["v"], word["R"] + columns = 2 * width + helpers + mask = helper_mask(word) + val = [1 << reg for reg in range(columns)] + delivered = [0] * width + cross = [0] * width + for _frame, dest, srcs in word["D"]: + acc = 0 + for src in srcs: + acc ^= val[src] + if width <= dest < 2 * width: + named_helper = 0 + for src in srcs: + if src >= 2 * width: + named_helper ^= 1 << src + got = acc & mask + delivered[dest - width] ^= got + cross[dest - width] ^= got ^ named_helper + val[dest] ^= acc + restored = all(val[reg] == (1 << reg) for reg in range(2 * width, columns)) + return delivered, cross, restored + + +def popcount(mask): + return bin(mask).count("1") + + +def sector_counts(masks, width): + seen = set() + for mask in masks: + bit = 0 + while mask: + if mask & 1: + seen.add(bit - 2 * width) + mask >>= 1 + bit += 1 + return len(seen) + + +def first_helper_edge(word): + width = word["v"] + for index, (_frame, dest, srcs) in enumerate(word["D"]): + if dest >= 2 * width and srcs and all(src >= 2 * width for src in srcs): + return index + return None + + +def without_gate(word, index): + clone = dict(word) + clone["D"] = list(word["D"]) + del clone["D"][index] + return clone + + +def synthetic_restored_edge(): + """h0 ^= h1; y ^= h0; h0 ^= h1, with an empty raw word. + + Executed delivery is h0 XOR h1. The syntactic mask names only h0. The raw + helper part is 0, so the defect is not the cross term. + """ + return { + "v": 1, + "R": 2, + "D": [[0, 2, [3]], [0, 1, [2]], [0, 2, [3]]], + "A": [], + "B": [], + "scatter": [[]], + "ret": [2], + } + + +def pin_inputs(): + with open(os.path.join(HERE, "SOURCES.json"), encoding="utf-8") as handle: + rows = json.load(handle)["files"] + for row in rows: + if row["usage"] != "input": + continue + path = os.path.join(ROOT, row["path"]) + digest = sha256(path) + if digest != row["sha256"]: + fail("sha256 mismatch for " + row["path"]) + + +def load_checker(): + path = os.path.join(ROOT, CHECKER) + spec = importlib.util.spec_from_file_location("xcheck_p_pinned", path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def checker_raw_K(module, word): + width = word["v"] + mask = helper_mask(word) + raw, _cur, _stats = module.Word(word).replay( + sections=("A", "scatter", "B"), frames_on=False) + return [raw[width + target] & mask for target in range(width)] + + +def main(): + pin_inputs() + checker = load_checker() + summaries = [] + for name, relative in WORDS: + word = load_word(os.path.join(ROOT, relative)) + width = word["v"] + mask = helper_mask(word) + named = syntactic_N(word) + helper_named = [row & mask for row in named] + observed = raw_K(word) + delivered, cross, restored = executed_D(word) + if not restored: + fail(name + " does not restore helpers at the end of D") + if checker_raw_K(checker, word) != observed: + fail(name + " raw helper part disagrees with the owner checker") + _hypotheses, conclusion, _info = checker.Word(word).interface() + if conclusion["K_equals_D"]: + fail(name + " syntactic K_equals_D is true; the defect premise failed") + for target in range(width): + identity = delivered[target] ^ helper_named[target] + defect = observed[target] ^ helper_named[target] + if identity != cross[target]: + fail(name + " cross tally is not E XOR syntactic helper mask") + if delivered[target] != observed[target] or defect != cross[target]: + fail(name + " target %d defect is not the cross tally" % target) + edge = first_helper_edge(word) + if edge is None: + fail(name + " has no helper-to-helper gate to delete") + mutated, _mut_cross, _mut_restored = executed_D(without_gate(word, edge)) + if mutated == observed: + fail(name + " still matches K after deleting one helper edge") + bits = sum(popcount(row ^ helper_named[target]) for target, row in enumerate(observed)) + summaries.append((name, width, bits, sector_counts( + [observed[t] ^ helper_named[t] for t in range(width)], width))) + + synthetic = synthetic_restored_edge() + syn_named = [row & helper_mask(synthetic) for row in syntactic_N(synthetic)] + syn_K = raw_K(synthetic) + syn_E, syn_cross, syn_restored = executed_D(synthetic) + if not syn_restored or syn_K != [0]: + fail("synthetic restored edge is not an empty-raw restored helper") + if syn_E[0] ^ syn_named[0] != syn_cross[0]: + fail("synthetic cross identity failed") + if syn_cross[0] == 0 or syn_K[0] ^ syn_named[0] == syn_cross[0]: + fail("synthetic edge did not separate the defect from the cross term") + + bits = "/".join(str(item[2]) for item in summaries) + sectors = "/".join(str(item[3]) for item in summaries) + targets = "/".join(str(item[1]) for item in summaries) + print( + "PASS_R439_K_CROSS_TERM_TALLY words=3 targets=%s equal_targets=%s " + "defect_bits=%s cross_bits=%s sectors=%s helpers_restored=3/3 " + "checker_K_equals_D=false/false/false mutation_breaks=3/3 " + "synthetic_unequal=1 no_new_kappa" % (targets, targets, bits, bits, sectors)) + + +if __name__ == "__main__": + main()