research: record the compensated-shear hypothesis for the R439 K foot…

research/r439-shear-compensation-hypothesis/README.md

@@ -0,0 +1,147 @@
+# Compensated restored shears keep the R439 helper footprint
+
+**Partial 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
+
+The K-defect tally on the three retained helper-star words shows that the
+helper mask `E` actually written by `D`, starting from identity columns,
+equals the forward footprint `K` left by `(A, scatter, B)`. A three-gate
+restored edge `h0 ^= h1`, `y ^= h0`, `h0 ^= h1` restores its helpers and
+still has `E` different from the column it names. The released question is
+which extra hypothesis the three words satisfy and that edge violates, tested
+on one other pinned helper-mixing word. The hypothesis is not allowed to be
+only "this `D` was built to match `K`".
+
+Card `bit-helper-contract`, scope refined to that hypothesis.
+
+## Hypothesis
+
+Let the parent word be `research/r439-target-compensation/candidate.json.gz`.
+Its `D` is three blocks: 306 target-to-target gates, 111 helper reads (one
+per target), and 306 target-to-target gates. Neither transport block writes
+a helper, and neither reads anything but targets.
+
+A **compensated restored shear** of that parent is a word whose `D` is
+
+```text
+S + P + M + Q + reverse(S)
+```
+
+where `P` and `Q` are the parent's transport blocks, `S` is a list of gates
+`h_a ^= h_b`, and `M` is the parent's middle support after the updates
+`columns[b] ^= columns[a]` in that edge order. Bit `i` of `columns[j]` means
+target `i` names helper `j`.
+
+The three tally words and the pinned degree-1 pair control
+`research/r439-bsection-stars-seed01/pair_control.json.gz` all have this
+shape. Their edge counts are 221, 221, 236 and 188. The synthetic edge is
+the shear `h0 ^= h1` with a middle that still names only `h0`.
+
+## One-edge identity
+
+Suppose each helper `j` currently holds a value `V_j` in an abelian 2-group,
+and target `i` is about to receive the sum of `V_j` over `j` in its support
+`S_i`. After the gate `h_a ^= h_b`, the new value of `h_a` is `V_a + V_b` and
+`h_b` is unchanged. Replace the support by toggling membership of `b` on
+exactly the targets that already name `a`.
+
+- If target `i` does not name `a`, its support and its sum are unchanged.
+- If it names `a` and already names `b`, the new sum replaces `V_a + V_b`
+  by `V_a + V_b` from the dirty `h_a` alone. The named `b` is dropped.
+- If it names `a` and does not name `b`, the new sum is
+  `(V_a + V_b) + V_b = V_a`. The extra `V_b` is cancelled by naming `b`.
+
+So one compensated edge preserves every target sum. The leading transport
+block only mixes targets, and targets start with no helper columns, so it
+does not change the helper footprint. The trailing block is the same map for
+the parent and the sheared word, so the final executed mask `E` is the
+parent's `E`. Reversing `S` restores every helper because `P`, `M` and `Q`
+do not write helpers and each shear is an involution.
+
+The parent's own execution has `E = K`. A descendant with the same forward
+helper footprint therefore also has `E = K`. The star word keeps `A`,
+`scatter` and `B` byte for byte. The composition, the later candidate and
+the pair control change `B` and `C`; their forward helper masks were checked
+equal to the parent's, not deduced from the text of those edits.
+
+The identity does not use the gain order or the degree bound of the star
+search. The verifier also runs five compensated edges that are not in those
+searches, and the same five edges without the support update. Compensation
+keeps `E`. Dropping it changes `E`.
+
+## What was checked
+
+| object | edges | shape | `E = K =` parent `K` |
+|---|---:|---|---|
+| parent target-compensation | 0 | bare bracket | yes |
+| helper-stars-seed19 candidate | 221 | compensated | yes |
+| bsection composition | 221 | compensated | yes |
+| bsection candidate | 236 | compensated | yes |
+| bsection pair control | 188 | compensated | yes |
+| five-edge probe, support updated | 5 | compensated | `E` unchanged |
+| same probe, support not updated | 5 | not the hypothesis | `E` changes |
+| synthetic `h0 ^= h1` then read `h0` | 1 | not the hypothesis | delivers `h0+h1`, not `h0` |
+
+The pair control is the other pinned helper-mixing word. It is not one of
+the three tally words. It satisfies the hypothesis, so the agreement is the
+shear identity rather than a property of those three greedy outputs alone.
+
+## What is not established
+
+`E = K` is not claimed for an arbitrary restored helper program. The
+synthetic edge is the counterexample to that reading. Changed `B` and `C`
+sections are checked only for the three words that carry them. The 612
+target-to-target reads inside `D` remain an open H2 read-kind clause. No
+supplier, native schedule, all-size transfer, or selected-frontier change is
+claimed.
+
+## Reproduce
+
+From the repository root, CPython 3.12:
+
+```sh
+python3 -B research/r439-shear-compensation-hypothesis/verify.py
+python3 -I -O -Werror -B research/r439-shear-compensation-hypothesis/verify.py
+python3 scripts/research_package.py --package research/r439-shear-compensation-hypothesis
+```
+
+Expected first line:
+
+```text
+PASS_R439_SHEAR_COMPENSATION words=4 edges=221/221/236/188 parent_E_equals_K=1 descendants_E_equals_K=4 shape=4 one_edge_steps=871 compensated_probe=1 uncompensated_probe=1 synthetic_rejects=1 no_new_kappa
+```
+
+The verifier exits nonzero if a pin drifts, a descendant is not the
+compensated shape, `E` or `K` moves, the one-edge identity fails, the
+compensated probe moves `E`, or the uncompensated probe or synthetic edge
+fails to separate. Runtime is a few seconds.
+
+## Open next questions
+
+1. Does every later phase-B rewrite with this same `D` bracket preserve `K`,
+   or only the three checked variants? The shear lemma fixes `E`. Those
+   variants were executed; their `B` and `C` edits were not identified.
+   First step: compare one other pinned B-section word's forward helper mask
+   with the parent. Blocked by the absence of a structural account of those
+   edits.
+2. Which H2 clause still fails once `E` is read as delivered columns? The
+   read-kind clause on the 612 target-to-target gates is the obvious
+   candidate and is not settled here. First step: name the first failing
+   read of `H2_D_frame0_targets_from_helpers` on the star word. Blocked
+   because this package does not rerun that checker and does not propose a
+   replacement predicate.
+
+## Credit
+
+The parent bracket is the target-compensation word. The shear assembly and
+the star and pair-control words are the helper-star builder (PR #967) and
+the phase-B package `research/r439-bsection-stars-seed01`. PR #3533 isolates
+one restored helper edge whose literal mask misses the delivered column.
+PR #4092 (Nick Petalas) counts the defect by sector. The tally that left
+this question open is PR #4115.
+
+Prepared by unpaidmoon with substantial AI assistance (Cursor Grok).
+Apache-2.0. Predecessor packages keep their own notices.

research/r439-shear-compensation-hypothesis/SOURCES.json

@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f",
+  "files": [
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5",
+      "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0"
+    },
+    {
+      "path": "research/r439-target-compensation/candidate.json.gz",
+      "usage": "input",
+      "git_blob": "7f1f188f516ca4661f419dc72114751abf3cc920",
+      "sha256": "ac30266144f8772ec8cd629153993aa9eb692fe745a9f95015a1b7fa88977a2e"
+    },
+    {
+      "path": "research/r439-helper-stars-seed19/candidate.json.gz",
+      "usage": "input",
+      "git_blob": "8b0210d8b8e9524182e5f54f9bf93c28f4719735",
+      "sha256": "d8b08885e8ce9868200b2645189d15ed18a27fc2742e54990b3257a0ca4df6b8"
+    },
+    {
+      "path": "research/r439-bsection-stars-seed01/composition.json.gz",
+      "usage": "input",
+      "git_blob": "d95fc2bf795fd9ef8d8bae9d70693c5e64948cec",
+      "sha256": "0203fea9fa442ca206fe683aa5b6860adac680d63b9fb8be6bd42b39aa7b5cce"
+    },
+    {
+      "path": "research/r439-bsection-stars-seed01/candidate.json.gz",
+      "usage": "input",
+      "git_blob": "9a17b4920334878d6c949191f6931bd97126fe3c",
+      "sha256": "b452d2c2b0b2a546d1105b1da9769aa78e5c54d6f00e97b30c77e3f54ce445ee"
+    },
+    {
+      "path": "research/r439-bsection-stars-seed01/pair_control.json.gz",
+      "usage": "input",
+      "git_blob": "16972bc96de0c81321eb2feef70766c403017016",
+      "sha256": "628ebfebe215e153338e88e2e324040d139a111eebfb090929697c7a0b6f3f59"
+    }
+  ]
+}

research/r439-shear-compensation-hypothesis/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": "Which extra shape makes the executed helper mask E equal the forward footprint K on the three retained R439 helper-star words, while the synthetic restored edge fails that shape, and does the pinned degree-1 pair control satisfy it?",
+  "scope_change_reason": "The card asks for a replacement H2/K contract and a paid profile. This package does not adopt one. It answers the released next question of the K-defect tally: name a hypothesis the three legal words satisfy and the synthetic edge violates, then test one other pinned helper-mixing word. Stop if the hypothesis is only that D was built to match K.",
+  "bottleneck_link": "A legitimate H2/K replacement could admit a cheaper bit circuit. Scalar agreement of two masks does not. The compensated-shear shape says when that agreement is forced, and the synthetic edge shows it is not free.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop once the compensated-shear shape is checked on the parent, the three tally words and the pair control, the one-edge identity is recorded, and the uncompensated probe and synthetic edge are shown to miss E. Do not adopt K_equals_D, price a new profile, or search another star forest.",
+  "outcome": "partial",
+  "evidence": "verify.py checks the parent bracket, four descendant shapes, equality of E and K with the parent footprint, the one-edge identity on all 866 real edges plus five probe edges, one compensated probe, one uncompensated probe, and the three-gate synthetic edge.",
+  "author": "unpaidmoon",
+  "ai_assistance": "Substantial Cursor Grok assistance in the shape check, the verifier and the write-up. No proof assistant was used.",
+  "open_questions": [
+    {
+      "question": "Does every phase-B rewrite that keeps this D bracket preserve the forward helper footprint K, or only the three checked B/C variants?",
+      "why_it_matters": "The shear lemma fixes E. E equals K on those variants only because their changed B and C sections were checked to leave K unchanged.",
+      "first_step": "Take one other pinned B-section word with the same 306+111+306 transport blocks and compare its forward helper mask with the parent.",
+      "blocked_by": "No structural account of those B and C edits is claimed here, so a new word needs its own execution."
+    },
+    {
+      "question": "After E is read as delivered columns, which H2 clause still fails on these words?",
+      "why_it_matters": "Mask agreement does not repair the 612 target-to-target reads inside D. Adopting a contract still needs that clause.",
+      "first_step": "Evaluate H2_D_frame0_targets_from_helpers on the star word and name the first failing read.",
+      "blocked_by": "This package does not rerun the owner interface checker and does not propose a replacement predicate."
+    }
+  ]
+}

research/r439-shear-compensation-hypothesis/VERIFY.json

@@ -0,0 +1,25 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/r439-target-compensation/candidate.json.gz",
+    "research/r439-helper-stars-seed19/candidate.json.gz",
+    "research/r439-bsection-stars-seed01/composition.json.gz",
+    "research/r439-bsection-stars-seed01/candidate.json.gz",
+    "research/r439-bsection-stars-seed01/pair_control.json.gz"
+  ],
+  "commands": [
+    {
+      "argv": ["{python}", "-B", "{package}/verify.py"],
+      "timeout_seconds": 60,
+      "checks": "Parent E equals K, four compensated-shear descendants keep that footprint, the one-edge identity holds on their edges, and an uncompensated probe and the synthetic edge do not."
+    },
+    {
+      "argv": ["{python}", "-I", "-O", "-Werror", "-B", "{package}/verify.py"],
+      "timeout_seconds": 60,
+      "checks": "The same certificate under isolated imports, optimized bytecode and warnings as errors."
+    }
+  ]
+}