Research: H2-sem admission of the PR848 copy-path helper-sharing wrap (no new kappa)

research/r439-copyshare-h2sem-admission/CERTIFICATE.json

@@ -0,0 +1,93 @@
+{
+  "status": "PASS_R439_COPYSHARE_H2SEM_ADMISSION",
+  "assignment_nonce": "df6f572bc7d7dbccbe487fe013268a12",
+  "task_id": "bit-helper-contract",
+  "scope_status": "refined",
+  "columns": 661,
+  "word_canonical_sha256": "5642fd0e35a1acc11acff8d0c08350c1617e95f310d4d35ad63a651f9eeeba0b",
+  "pr848_census": {
+    "operands": 430,
+    "oriented_pairs": 184470,
+    "positive_pairs": 41404,
+    "best_saving": 65,
+    "best_pair": [
+      277,
+      434
+    ],
+    "matching_pairs": 205,
+    "matching_saving": 6231
+  },
+  "baseline_d_source_reads": 18085,
+  "implication_I_single_pair_277_434": {
+    "cond1_zero_frame_distinct_operands": true,
+    "cond2_no_target_feeds_helper_or_source": true,
+    "boundary_operator_exact": true,
+    "frames_at_cut_equal": true,
+    "semantic_K_equals_raw_K": true,
+    "literal_N_equals_semantic_N": false,
+    "inherited_flag_failures": [
+      "H2_D_frame0_targets_from_helpers",
+      "K_equals_D"
+    ],
+    "d_source_reads": 18020
+  },
+  "implication_I_greedy_matching_205_pairs": {
+    "cond1_zero_frame_distinct_operands": true,
+    "cond2_no_target_feeds_helper_or_source": true,
+    "boundary_operator_exact": true,
+    "frames_at_cut_equal": true,
+    "semantic_K_equals_raw_K": true,
+    "literal_N_equals_semantic_N": false,
+    "inherited_flag_failures": [
+      "H2_D_frame0_targets_from_helpers",
+      "K_equals_D"
+    ],
+    "d_source_reads": 11854
+  },
+  "control_c2_target_temp": {
+    "cond1_zero_frame_distinct_operands": true,
+    "cond2_no_target_feeds_helper_or_source": true,
+    "boundary_operator_exact": true,
+    "frames_at_cut_equal": true,
+    "semantic_K_equals_raw_K": true,
+    "literal_N_equals_semantic_N": true,
+    "inherited_flag_failures": [],
+    "d_source_reads": 18087
+  },
+  "f4_target_feed_probe": {
+    "cond1_zero_frame_distinct_operands": true,
+    "cond2_no_target_feeds_helper_or_source": false,
+    "boundary_operator_exact": true,
+    "frames_at_cut_equal": true,
+    "semantic_K_equals_raw_K": true,
+    "literal_N_equals_semantic_N": false,
+    "inherited_flag_failures": [
+      "H1_no_target_feeds_z",
+      "H2_D_frame0_targets_from_helpers",
+      "K_equals_D"
+    ],
+    "d_source_reads": 18154
+  },
+  "f5_source_feed_probe": {
+    "scalar_operator_exact": true,
+    "cond1_zero_frame_distinct_operands": false,
+    "cond2_no_target_feeds_helper_or_source": true,
+    "framed_replay_rejection": "climb not nested: register 0 from frame 2 (dim 1) to frame 0 (dim 0)",
+    "d_source_reads": 18154
+  },
+  "bridge": {
+    "virtual_splice_flags_all_pass": true,
+    "continuation_state_and_frames_equal_at_D_A_cut": true,
+    "pr1194_proof": "research/r439-semantic-d-contract-seed10/PROOF.md"
+  },
+  "negative_and_positive_controls": [
+    "baseline word passes all inherited flags and the virtual-splice premises",
+    "F1 unrestored helper temp rejected at endpoints",
+    "F2 wrong-restore operand breaks the boundary equation on a dirty helper column",
+    "F3 mid-body restore (chronological cut inside the wrap) breaks the boundary equation",
+    "F4 target-feeding-helper wrap operator-preserving but outside H2-sem condition 2",
+    "F5 source-feeding helper wrap: operator exact, framed replay rejects the frame-0 source read",
+    "C2 target-temp wrap admitted with exactly +2 reads (no saving)"
+  ],
+  "kappa_claim": "none"
+}

research/r439-copyshare-h2sem-admission/README.md

@@ -0,0 +1,152 @@
+# H2-sem admission of the PR848 copy-path helper-sharing wrap (no new kappa)
+
+**Scoped interface audit; no circuit pricing, no supplier adoption.** The selected
+result, the selected bit supplier and `upstream/` are unchanged. The exact
+replacement contract is woklerx's H2-sem (PR1194,
+`research/r439-semantic-d-contract-seed10/PROOF.md`); this package decides one
+precise implication of it on one precise family of words and tries to falsify
+that implication on dirty inputs and chronological cuts.
+
+## Object and question
+
+PR848 (`research/r439-copy-path-sharing-barrier`) priced source-read sharing
+inside the frame-zero D section of the selected R439 word
+(`research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz`, v=111, R=439,
+111 D gates, 18,085 helper reads). Its oriented-pair census over the 430
+non-retained helper operands found 41,404 arithmetically positive pairs (best
+277 -> 434, saving 65) and one seed-42 greedy disjoint matching of 205 pairs for
+6,231 source reads. PR848 recorded the figure as an arithmetic upper bound only:
+the inherited gate-local H2 (`H2_D_frame0_targets_from_helpers`) requires every D
+gate to write a target, so every helper-writing preparation/restoration pair is
+rejected (its control C1 preserves the scalar operator and fails H2).
+
+**Question (card `bit-helper-contract`, first experiment).** Write one
+replacement H2/K implication for a helper-mixing word and try to falsify it on
+dirty inputs. The replacement is H2-sem: D gates at the zero frame with distinct
+operands drawn from targets and helpers, the retained no-target-feedback
+prohibition, and the full boundary equation `(x,y,h) -> (x,y+N h,h)`, with the K
+check comparing the *semantic* N against raw A/scatter/B instead of gate-local
+source reads.
+
+**Implication (I), the audited statement.** If a wrapped D section satisfies
+H2-sem conditions 1-3 with semantic N unchanged, and the unchanged predecessor
+checker passes every inherited H1-H5 and U/J/K/C flag on the PR1194 virtual
+splice (literal A/scatter/B/C with the original D), then the PR1194 chronological
+substitution bridge transfers the interleaved-lemma conclusion to the wrapped
+word, on arbitrary dirty inputs.
+
+## Result: implication (I) holds on the tested instances
+
+| wrap | H2-sem 1-3 | boundary op. on 661 cols | frames at cut | semantic K | inherited flags failing | D source reads |
+|---|---|---|---|---|---|---:|
+| C1: pair 277 -> 434 | pass | exact | equal | N = K | exactly H2, K_equals_D | 18,085 - 65 = 18,020 |
+| seed-42 matching (205 pairs) | pass | exact | equal | N = K | exactly H2, K_equals_D | 18,085 - 6,231 = 11,854 |
+| C2: PR848 target-temp (control) | pass | exact | equal | N = K | none | 18,087 (+2) |
+
+All 661 basis columns are replayed exactly; by F2 linearity (PR1194's module
+argument) coefficient equality on those columns is equality on every F2 module,
+so this covers arbitrary finite and infinite dirty streams in the stated
+interpretation. The virtual splice is the pinned baseline word itself, which
+passes all inherited flags; the continuation state and frames at the D/A cut are
+byte-equal between each wrap and the baseline.
+
+So the PR848 obstruction ("any helper-writing preparation/restoration pair is
+rejected") is scoped to the inherited gate-local H2 only: under H2-sem the C1
+wrap and the whole greedy matching are interface-admissible helper-mixing words,
+and the semantic K check passes exactly where the literal extractor fails.
+
+## Falsification attempts (why the contract clauses matter)
+
+| control | outcome |
+|---|---|
+| F1 unrestored helper temp | rejected at endpoints (boundary equation broken on helper columns) |
+| F2 wrong restore operand | boundary equation broken on a dirty helper column |
+| F3 restore at a mid-body chronological cut | boundary equation broken (the wrap must span every dependent read) |
+| F4 target-feeding-helper wrap (span closed before the fed target's own gate) | **scalar operator exact, endpoint passes, frames equal** — rejected only by H2-sem condition 2 (the retained no-target-feedback clause; the checker's H1 also fails). A weaker replacement that drops that clause would admit it. |
+| F5 source-feeding-helper wrap | scalar operator exact, but the framed replay rejects the frame-0 source read outright (`climb not nested: register 0 from frame 2 (dim 1) to frame 0 (dim 0)`): raw operator identity does not justify frame-sensitive execution |
+
+F4 and F5 are the recorded boundary of the replacement: the exact boundary
+equation alone is strictly weaker than H2-sem. F5 additionally confirms at one
+concrete instance the warning in PR1194 and `r439-abc-semantic-bridge` that a
+raw block identity must not be treated as a framed equivalence.
+
+## Reproduce
+
+Standard library only (Python 3.10+), from the repository root:
+
+```sh
+python3 -I -B research/r439-copyshare-h2sem-admission/verify.py
+python3 -I -O -B research/r439-copyshare-h2sem-admission/test_package.py
+python3 scripts/research_package.py --package research/r439-copyshare-h2sem-admission --check-only
+```
+
+Expected (about 40 s for the first command):
+
+```text
+PASS_R439_COPYSHARE_H2SEM_ADMISSION pair=277->434 saving=65 matching_pairs=205 matching_saving=6231 columns=661 controls=7 no_new_kappa
+```
+
+`CERTIFICATE.json` is compared field for field; `test_package.py` replays at a
+fresh location and rejects a mutated source pin, a mutated certificate and a
+missing pin block. The verifier recomputes PR848's complete pair census and
+greedy matching deterministically (seed 42) and checks its recorded constants.
+
+## Scope: what is not claimed
+
+* **No priced construction.** The 6,231 figure remains a source-read arithmetic
+  bound. The wrapped words are not billed: F/B positive envelopes, the 104/192-bit
+  guards, COPY/ERASE accounting and the paid profile were not recomputed, and no
+  word is proposed as a supplier. Intermediate integer envelopes can differ even
+  at an identical binary endpoint (PR1194), so the precision guards are an
+  explicit open obligation.
+* **No kappa, frontier or native/hosted admission.** The all-size compiler,
+  common-label realization, hosting, precision/tape, recovery and analytic
+  obligations are untouched.
+* **The bridge is PR1194's, applied.** The chronological substitution theorem and
+  its module argument are credited to PR1194; this package contributes the exact
+  instance-level admission and the falsification controls, not a new lemma.
+* Greedy matching optimality is not claimed (PR848's matching is one seeded
+  pass). F4 shows condition 2 is not redundant with the boundary equation at this
+  instance; whether some target-feedback wrap is safe under a weaker replacement
+  needs its own lemma and is not decided here.
+
+## Overlap
+
+The submission-time `find_overlap.py` snapshot (446 open PRs including drafts,
+418 discussion records, complete pagination, 2026-10-14 09:50 UTC) for `H2-sem`,
+`semantic zero-frame D`, `copy-path sharing`, `copyshare`, `helper-temp`,
+`277 -> 434`, `pair sharing wrap` matches only this package, its claim
+([discussion 1166](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18920693))
+and PR848's own record; no open PR or discussion claim covers H2-sem admission of
+copy-path sharing wraps. This is not a novelty certificate.
+
+## Open next questions
+
+* **Bill the admitted wrap.** Recompute F/B, the exact local/nine-stage bit
+  expressions and the paid profile for the 205-pair wrapped word and check the
+  precision guards. Why it matters: this is the only path from an
+  interface-admissible 6,231-read reduction to an actual bit-circuit saving.
+  First step: rerun `research/r439-bsection-stars-seed01/verify.py`'s bound
+  machinery on the wrapped D. Blocked by: the envelope code lives in the
+  predecessor packages and must be reused unchanged; the 192-bit nine-stage cap
+  already sat at 99.996% on the helper-star word.
+* **Is H2-sem condition 2 necessary at a framed level?** F4 preserves the full
+  scalar operator yet is excluded by the retained no-target-feedback clause.
+  Why it matters: a justified weakening would enlarge the admissible wrap class.
+  First step: state the exact conclusion the interleaved lemma needs from H1 and
+  test the F4-shaped word against it. Blocked by: the lemma's proof uses H1 in
+  its block-triangular step; an operator-level check alone cannot replace it.
+
+## Credit and disclosure
+
+Prepared by **Aaron Wang** with help from opencode. Apache-2.0; no independent
+human review is claimed. Credit **Aaron Wang, PR848**
+(`research/r439-copy-path-sharing-barrier`: the pair census, the greedy
+matching and the C1-C3 controls whose C1/C2 shapes are reused here), **woklerx,
+PR1194** (`research/r439-semantic-d-contract-seed10/PROOF.md`: the H2-sem
+contract and chronological substitution bridge), **Arham Tahir**
+(`research/r439-abc-semantic-bridge`: the source-bound bridge-application
+pattern), **eumemic PR555** and **DreamingOfClouds PR589** (the R439 word), and
+the retained scalar-interface/xcheck lineage. The word, the unchanged
+`xcheck_p.py` owner checker and PR848's census code are consumed as pinned
+sources; no predecessor package is vendored or modified.

research/r439-copyshare-h2sem-admission/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11",
+      "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1",
+      "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075"
+    },
+    {
+      "path": "research/e8-bit-p111-tuned/code/xcheck_p.py",
+      "usage": "input",
+      "git_blob": "184f5dcf94a486cc7db91ca4db5865916bf26009",
+      "sha256": "af3decc877e27c00001cf56f50c6c09566e8e101297ab34c7860aed96a06d80e"
+    },
+    {
+      "path": "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz",
+      "usage": "input",
+      "git_blob": "85a4499bf9e4911a705d50567a2c2ef6cf23739a",
+      "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f"
+    }
+  ]
+}

research/r439-copyshare-h2sem-admission/TASK.json

@@ -0,0 +1,66 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-helper-contract",
+  "priority_revision": 3,
+  "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea",
+  "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": [
+      "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.",
+    "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": "One replacement H2/K implication (PR1194's H2-sem) audited on the PR848 copy-path helper-temp sharing wrap of the selected R439 word: the single pair 277->434 first, then the seed-42 greedy 205-pair matching, with dirty-input and chronological-cut falsification controls.",
+  "scope_change_reason": "The card's first experiment is kept exactly (one replacement H2/K implication, falsified on dirty inputs); the instance is narrowed from a generic helper-star to the helper-mixing word the inherited H2 provably rejects (PR848 control C1), so the replacement is tested where the old interface fails. The allowed variation 'narrow to one boundary implication' applies; no source count or scalar-count-only change is made.",
+  "bottleneck_link": "A legitimate replacement could admit a cheaper bit circuit: PR848 priced 6,231 D source reads of helper-sharing savings that gate-local H2 rejects; this audit decides only the interface admission, so scalar savings alone still do not alter the selected moment.",
+  "budget_minutes": 60,
+  "stop_rule": "One implication, one matched family (single pair and the fixed seed-42 matching), controls complete; no envelope/pricing work after the interface question is decided.",
+  "outcome": "completed",
+  "evidence": "CERTIFICATE.json and verify.py (7 controls); written implication statement and falsification table in README.md",
+  "author": "Aaron Wang",
+  "ai_assistance": "Substantial AI assistance from opencode; no independent human review.",
+  "open_questions": [
+    {
+      "question": "Do the admitted 205-pair and single-pair wraps satisfy the F/B positive envelopes, the exact local 104-bit and nine-stage 192-bit expressions and the paid-profile accounting?",
+      "why_it_matters": "The 6,231 source-read reduction becomes a real bit-circuit saving only if every billed guard still holds; identical binary endpoints do not bound intermediate integer envelopes.",
+      "first_step": "Rerun the bound machinery of research/r439-bsection-stars-seed01/verify.py on the wrapped D and compare F/B and both bit expressions.",
+      "blocked_by": "The envelope code is pinned in predecessor packages and must be reused unchanged; the helper-star word already sat at 99.996% of the nine-stage cap."
+    },
+    {
+      "question": "Is H2-sem condition 2 (no target feeds a source or helper) necessary at the framed level, or does some weaker replacement admit the F4-shaped target-feeding wrap?",
+      "why_it_matters": "F4 preserves the full scalar operator and endpoint yet is excluded by the retained clause; a justified weakening enlarges the admissible wrap class.",
+      "first_step": "Extract the exact use of H1 in the interleaved lemma's block-triangular step and test the F4 word against that conclusion alone.",
+      "blocked_by": "The lemma's proof invokes H1 directly; an operator-level check cannot replace it without a new chronological argument."
+    }
+  ]
+}

research/r439-copyshare-h2sem-admission/VERIFY.json

@@ -0,0 +1,33 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/e8-bit-p111-tuned/code/xcheck_p.py",
+    "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 240,
+      "checks": "PR848 pair census and seed-42 matching, H2-sem conditions 1-3, exact boundary operator on all 661 columns, frames at the D/A cut, semantic vs literal K, inherited flag pattern, and five failure controls (F1-F5) plus the C2 width control."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-B",
+        "{package}/test_package.py"
+      ],
+      "timeout_seconds": 240,
+      "checks": "Relocated replay at a fresh path plus three real on-disk corruptions: mutated source pin, mutated certificate and missing pin block."
+    }
+  ]
+}