Research: price H2-sem copy-path helper-sharing wraps (no new kappa)

research/h2sem-copyshare-priced/CERTIFICATE.json

@@ -0,0 +1,84 @@
+{
+  "status": "PASS_H2SEM_COPYSHARE_PRICED",
+  "assignment_seed": 42,
+  "task_id": "bit-helper-contract",
+  "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea",
+  "columns": 661,
+  "census": {
+    "operands": 430,
+    "oriented_pairs": 184470,
+    "positive_pairs": 41404,
+    "best_saving": 65,
+    "best_pair": [
+      277,
+      434
+    ],
+    "matching_pairs": 205,
+    "matching_saving": 6231
+  },
+  "bills": {
+    "base": {
+      "native_ADDs": 24305,
+      "D_adds": 18085,
+      "F": 49347,
+      "B": 1113070,
+      "local_bits": 93,
+      "nine_stage_bits": 177
+    },
+    "single": {
+      "native_ADDs": 24240,
+      "D_adds": 18020,
+      "F": 50535,
+      "B": 1113070,
+      "local_bits": 94,
+      "nine_stage_bits": 177
+    },
+    "match": {
+      "native_ADDs": 18074,
+      "D_adds": 11854,
+      "F": 75381,
+      "B": 1196402,
+      "local_bits": 95,
+      "nine_stage_bits": 180
+    }
+  },
+  "paid_profile": {
+    "1": 1323,
+    "2": 1342,
+    "3": 79,
+    "4": 44,
+    "5": 102,
+    "6": 11,
+    "7": 19
+  },
+  "rank_mass": 5129,
+  "h2sem": {
+    "shape": true,
+    "semantic_N_equals_baseline": true,
+    "syntactic_H2_K": {
+      "base": {
+        "H2": true,
+        "K_equals_D": true
+      },
+      "single": {
+        "H2": false,
+        "K_equals_D": false
+      },
+      "match": {
+        "H2": false,
+        "K_equals_D": false
+      }
+    }
+  },
+  "controls": [
+    "unrestored_helper_temp",
+    "wrong_restore_operand",
+    "target_feeds_helper",
+    "source_reads_in_D",
+    "partial_matching_unrestored",
+    "mutated_body_changes_N",
+    "target_temp_plus2_positive"
+  ],
+  "kappa_claim": "none",
+  "new_kappa": false
+}

research/h2sem-copyshare-priced/CLAIM.md

@@ -0,0 +1,19 @@
+# Claim
+
+**Finite bit construction under H2-sem; no new kappa.**
+
+Chooser seed `978940692bb73d58cd4b4e07f8514e57`, task `bit-helper-contract`,
+scope key `3475f46c8358c6a9211b`, base `0b1cccf86e2f5132ed286a26ef0a681a495740ea`.
+
+Under the PR1194 H2-sem replacement for syntactic H2/K, the PR848 helper-temp
+D wraps on the selected R439 word are fully priced:
+
+- single pair 277→434: ADDs 24305→24240 (−65);
+- seed-42 matching (205 pairs): ADDs 24305→18074 (−6231);
+
+with identical complete dirty boundary, semantic N unchanged, paid profile
+`{1:1323,2:1342,3:79,4:44,5:102,6:11,7:19}` (mass 5129) unchanged, and strict
+104/192-bit guards. Syntactic H2/K fail exactly on the wraps.
+
+This is not a selected-supplier proposal and claims no new kappa. It supplies
+the paid invoice that PR1782 left open after interface admission.

research/h2sem-copyshare-priced/NOTICE.md

@@ -0,0 +1,16 @@
+# Notice
+
+This package prices helper-sharing wraps introduced by Aaron Wang in PR848
+(`research/r439-copy-path-sharing-barrier`) under the H2-sem replacement
+contract of woklerx in PR1194
+(`research/r439-semantic-d-contract-seed10/PROOF.md`). The selected R439 word
+and owner checker belong to DreamingOfClouds (PR589) and eumemic (PR555)
+lineage. Open PR1782 (navinor) independently admits the same wraps under
+H2-sem without recomputing F/B or the paid profile; that admission is credited
+and not vendored.
+
+Predecessor notices, licenses and source archives are unchanged. New material
+in this directory is Apache-2.0.
+
+Prepared by Wentao Li with substantial AI assistance.
+Contributor profiles: GitHub VictorLiwentao; X @Is__Victor.

research/h2sem-copyshare-priced/PROOF.md

@@ -0,0 +1,73 @@
+# H2-sem pricing of the PR848 copy-path helper-sharing wraps
+
+## Contract (imported, not re-derived)
+
+Use the replacement scalar contract H2-sem of
+`research/r439-semantic-d-contract-seed10/PROOF.md` (PR1194):
+
+1. Every D gate is at the common zero frame and is source-free.
+2. No target feeds a source or helper (retained H1 inside D).
+3. The complete D operator is exactly `(x,y,h) -> (x, y + N h, h)` for a
+   specified binary matrix N.
+
+The old gate-local H2 requires every D gate to write a target. Helper
+preparation/restoration writes therefore fail syntactic H2. Under H2-sem they
+are legal when the boundary equation holds. Semantic N must equal the raw
+helper-response K of A/scatter/B for the interleaved substitution theorem.
+
+## Objects
+
+Let W be the selected PR589 R439 word
+(`research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz`). Its D section
+has 18,085 helper reads and already satisfies syntactic H2/K.
+
+PR848's wrap for an oriented helper pair `(a,b)` prepends `a ^= b`, rewrites
+every D row that contains `a` by symmetric difference with `b`, and appends the
+reverse restoration `a ^= b`. The arithmetic source-read saving of one pair is
+
+`sum_{rows containing a} (1_{b in row} - 1_{b not in row}) - 2`.
+
+The seed-42 greedy disjoint matching of PR848 selects 205 positive pairs with
+total arithmetic saving 6,231; the best single pair is `(277,434)` with saving
+65. Both figures are recomputed here.
+
+## Boundary lemma (dirty inputs)
+
+Write H for the involution that XORs each selected center by its leaf. The wrap
+is chronologically `H; D0; H` where D0 is the rewritten body. Because H = H^{-1}
+over F2 and the body applies the conjugated coefficient matrix, the composite
+equals the original D map on every F2 input column. Necessity of full helper
+restoration is witnessed by deleting a restore gate: some helper basis column
+fails to return. Equality of the 661 binary D columns therefore certifies the
+H2-sem boundary for every F2-module stream under the common zero-frame reading
+(the same coefficient argument as PR1194).
+
+## Paid invoice
+
+Only D changes. Register frame paths, COPY ranks and the climb histogram are
+unchanged, so the paid recursive profile remains
+
+`{1:1323, 2:1342, 3:79, 4:44, 5:102, 6:11, 7:19}`
+
+with rank mass 5,129. Literal COPY/ERASE stream peaks give:
+
+| word | ADDs | D ADDs | F | B | local bits | nine-stage bits |
+|---|---:|---:|---:|---:|---:|---:|
+| baseline W | 24,305 | 18,085 | 49,347 | 1,113,070 | 93 | 177 |
+| single pair 277→434 | **24,240** | 18,020 | 50,535 | 1,113,070 | 94 | 177 |
+| seed-42 matching (205) | **18,074** | 11,854 | 75,381 | 1,196,402 | 95 | 180 |
+
+Both candidates stay strictly under the inherited 104-bit local and 192-bit
+nine-stage guards. Forward/reverse complete-word F2 boundaries equal the
+baseline. Inherited H1/H3/H4/H5 and U/J/C remain true; syntactic H2 and
+`K_equals_D` are false exactly on the wraps, while semantic N equals the
+baseline N (weight 18,085).
+
+## What this does not claim
+
+No new kappa: the bit supplier does not bind, and the paid profile is
+unchanged. Native C++/Boost replay, hosted supplier emission, all-size
+compiler, rounding/tape and analytic transfer are not executed. Matching
+optimality is not claimed. PR1782's interface-admission package is complementary:
+it established H2-sem legality without recomputing F/B or the paid profile;
+this package supplies that invoice.

research/h2sem-copyshare-priced/README.md

@@ -0,0 +1,75 @@
+# Priced H2-sem admission of the PR848 copy-path helper-sharing wraps
+
+**Priced finite invoice under the H2-sem replacement interface; no new κ.** The
+selected frontier, selected bit supplier and `upstream/` are unchanged. The bit
+side does not bind.
+
+PR848 priced helper-temp sharing on the selected R439 word as an arithmetic
+source-read upper bound and rejected it under gate-local H2. PR1194 supplies the
+replacement contract H2-sem. Open PR1782 checks that the wraps satisfy H2-sem,
+but leaves F/B envelopes and the paid profile uncomputed. This package completes
+that invoice.
+
+## Result
+
+| word | ADDs | D ADDs | F | B | local / nine-stage bits | paid profile |
+|---|---:|---:|---:|---:|---|---|
+| baseline PR589 | 24,305 | 18,085 | 49,347 | 1,113,070 | 93 / 177 | `{1:1323,…,7:19}` mass 5129 |
+| single pair 277→434 | **24,240** (−65) | 18,020 | 50,535 | 1,113,070 | 94 / 177 | unchanged |
+| seed-42 matching (205 pairs) | **18,074** (−6,231) | 11,854 | 75,381 | 1,196,402 | 95 / 180 | unchanged |
+
+Both wraps keep the complete dirty F2 boundary, semantic N equal to the baseline
+N, and the inherited 104/192-bit guards. Syntactic H2 and `K_equals_D` fail
+exactly on the wraps; H1/H3/H4/H5 and U/J/C remain true. Frame paths and nine
+rank-7 COPY ranks are unchanged, so the paid recursive profile is unchanged.
+
+## Reproduce
+
+```sh
+python3 -I -B research/h2sem-copyshare-priced/verify.py
+python3 -I -O -B research/h2sem-copyshare-priced/verify.py
+python3.12 scripts/research_package.py --package research/h2sem-copyshare-priced --check-only
+python3.12 scripts/research_package.py --package research/h2sem-copyshare-priced
+```
+
+Expected:
+
+```text
+PASS_H2SEM_COPYSHARE_PRICED single=277->434 adds=24305->24240 matching_pairs=205 adds=24305->18074 profile_mass=5129 columns=661 controls=7 no_new_kappa
+```
+
+The verifier recomputes the PR848 census, builds both wraps, checks H2-sem shape
+and all 661 D columns, replays the full literal COPY/ERASE stream both ways,
+recomputes F/B and precision guards, extracts the paid profile from frame-path
+climbs plus COPY ranks via the pinned owner checker, and rejects seven controls
+(unrestored helper, wrong restore, target→helper feedback, source read in D,
+partial matching unrestored, mutated body N, and the +2 target-temp positive).
+
+## Scope
+
+- **No new κ.** Paid profile unchanged; bit supplier nonbinding.
+- Native C++/Boost, hosted emission, all-size compiler, tape/rounding and
+  analytic transfer are not run.
+- Matching optimality is not claimed. Intermediate envelopes rise even as ADD
+  counts fall; that trade-off is recorded, not optimized away.
+- Complementary to PR1782 (interface admission without this invoice) and PR848
+  (H2 barrier). Does not vendor their executables.
+
+## Open next questions
+
+1. **Can a different matching lower F while keeping most of the ADD saving?**
+   The seed-42 matching raises F from 49,347 to 75,381. A first step is to
+   re-score pairs by a joint (ADD, F) objective on a frozen shortlist. Blocker:
+   no favorable completed (ADD, F, B) point is known.
+2. **Does the single-pair wrap compose with an already H2-sem-legal star D?**
+   First splice pair 277→434 onto the PR1062/PR1194 candidate and recompute the
+   full invoice. Blocker: maintained acceptance of H2-sem on the composed word.
+
+## Credit
+
+Credit **Aaron Wang / PR848** (pair census, greedy matching, helper-temp wrap),
+**woklerx / PR1194** (H2-sem contract), **navinor / PR1782** (interface admission
+that left pricing open), **DreamingOfClouds / PR589** and **eumemic / PR555**
+(the R439 word and checker lineage). Prepared by Wentao Li with substantial AI
+assistance. Apache-2.0. No independent human review or full multiplication
+theorem is claimed.

research/h2sem-copyshare-priced/SOURCES.json

@@ -0,0 +1,42 @@
+{
+  "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"
+    },
+    {
+      "path": "research/r439-copy-path-sharing-barrier/verify.py",
+      "usage": "input",
+      "git_blob": "5636566096d20039b3092819b0f4d1a283d66436",
+      "sha256": "1863b99b132bc5764508a18167303aaff32c815dc73a8693b84fe89a20301c86"
+    },
+    {
+      "path": "research/r439-semantic-d-contract-seed10/PROOF.md",
+      "usage": "input",
+      "git_blob": "2707fdb0d2f34c1c6c4ea41c2a68e44904a3e4fd",
+      "sha256": "dfbca8c61a92fdf0db8af450dc4466849da37fc296e28b67f357e196e87327db"
+    }
+  ]
+}

research/h2sem-copyshare-priced/TASK.json

@@ -0,0 +1,68 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-helper-contract",
+  "priority_revision": 3,
+  "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea",
+  "chooser_seed": "978940692bb73d58cd4b4e07f8514e57",
+  "scope_key": "3475f46c8358c6a9211b",
+  "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": "Price the PR848 copy-path helper-sharing wraps (single pair 277->434 and seed-42 greedy matching) under the PR1194 H2-sem replacement contract, including full dirty boundary, paid profile, F/B envelopes and precision guards.",
+  "scope_change_reason": "The card's first experiment asks for one replacement H2/K implication and its price. PR1194 already states H2-sem; PR1782 admits these wraps under it without an invoice. This package supplies the missing paid profile and precision accounting on the exact PR848 objects, which is the acceptance gate.",
+  "bottleneck_link": "A priced H2-sem-legal D wrap can reduce scalar ADDs on the nonbinding bit side. The paid recursive profile is checked explicitly; unchanged profile means no selected-moment change.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after one complete invoice for the single-pair and matching wraps with dirty controls, or after a falsifying dirty counterexample to H2-sem on those wraps.",
+  "outcome": "completed",
+  "evidence": "PASS_H2SEM_COPYSHARE_PRICED: single pair saves 65 ADDs (24305->24240); matching saves 6231 ADDs (24305->18074); paid profile mass 5129 unchanged; guards 94/177 and 95/180; 661 columns; 7 controls.",
+  "author": "Wentao Li",
+  "ai_assistance": "Prepared by Wentao Li with substantial AI assistance",
+  "open_questions": [
+    {
+      "question": "Can a different matching lower F while keeping most of the ADD saving?",
+      "why_it_matters": "The seed-42 matching raises F from 49347 to 75381; a joint (ADD,F) optimum could improve precision headroom.",
+      "first_step": "Re-score a frozen shortlist of positive pairs by a joint (ADD, F) objective and recompute one full invoice.",
+      "blocked_by": "No favorable completed (ADD, F, B) point is known."
+    },
+    {
+      "question": "Does the single-pair wrap compose with an already H2-sem-legal star D?",
+      "why_it_matters": "Composition could stack PR848 sharing with PR967/PR1062 star savings under one interface.",
+      "first_step": "Splice pair 277->434 onto the PR1062 candidate and recompute the full H2-sem invoice.",
+      "blocked_by": "Maintainer acceptance of H2-sem on the composed word; full re-invoice cost."
+    }
+  ]
+}