DEFER: F4 cond2 framed necessity largely already in #1782

research/h2sem-cond2-framed-necessity/EXPECTED.json

@@ -0,0 +1,97 @@
+{
+  "baseline_bill": {
+    "ADDS": 24305,
+    "B": 1113070,
+    "D_ADDS": 18085,
+    "D_gates": 111,
+    "F": 49347,
+    "local_bits": 93,
+    "local_integer": 9528119495320518471870892800,
+    "nine_stage_bits": 177,
+    "nine_stage_integer": 117742596540718658156527847560864213734191286190080000,
+    "profile": {
+      "1": 1323,
+      "2": 1342,
+      "3": 79,
+      "4": 44,
+      "5": 102,
+      "6": 11,
+      "7": 19
+    },
+    "rank_mass": 5129
+  },
+  "census": {
+    "best_pair": [
+      277,
+      434
+    ],
+    "best_saving": 65,
+    "matching_pairs": 205,
+    "matching_saving": 6231,
+    "operands": 430,
+    "oriented_pairs": 184470,
+    "positive_pairs": 41404
+  },
+  "claim": "On this F4 instance, H2-sem condition 2 fails while the framed dirty endpoint (x,y,h)->(x,y+x,h) holds; condition 2 is not necessary for that endpoint conclusion. No general drop of condition 2 is claimed.",
+  "conditions": {
+    "cond1_zero_frame_distinct_operands": true,
+    "cond2_no_target_feeds_helper_or_source": false,
+    "cond3_boundary_operator_exact": true,
+    "frames_at_cut_equal": true,
+    "semantic_N_equals_raw_K": true
+  },
+  "controls": [
+    "baseline word: all inherited flags, D operator, literal endpoint, profile mass 5129",
+    "C1 helper-temp wrap on 277->434 admits H2-sem 1-3 (contrast)",
+    "F4: cond1/3 and frames hold; cond2 fails; inherited H1 fails",
+    "F4 framed+literal forward/reverse dirty endpoint exact on 661 columns",
+    "proof-only original-D splice passes every inherited flag",
+    "exact costs: +69 ADDs, profile mass 5129 unchanged, guards strict",
+    "F4 unrestored feed breaks condition 3",
+    "F4 late restore (after target write) breaks condition 3"
+  ],
+  "endpoint": {
+    "columns": 661,
+    "framed_sectional_exact": true,
+    "literal_forward_exact": true,
+    "literal_reverse_exact": true
+  },
+  "f4_bill": {
+    "ADDS": 24374,
+    "B": 2995586,
+    "D_ADDS": 18154,
+    "D_gates": 113,
+    "F": 50535,
+    "local_bits": 96,
+    "local_integer": 74117432844898582480048224000,
+    "nine_stage_bits": 183,
+    "nine_stage_integer": 6957103126489666085304959651569977533363295446630400000,
+    "profile": {
+      "1": 1323,
+      "2": 1342,
+      "3": 79,
+      "4": 44,
+      "5": 102,
+      "6": 11,
+      "7": 19
+    },
+    "rank_mass": 5129
+  },
+  "f4_meta": {
+    "close_before_index": 110,
+    "fed_target": 221,
+    "helper": 277
+  },
+  "inherited_flag_failures": [
+    "H1_no_target_feeds_z",
+    "H2_D_frame0_targets_from_helpers",
+    "K_equals_D"
+  ],
+  "new_kappa": false,
+  "pair": [
+    277,
+    434
+  ],
+  "status": "PASS_H2SEM_COND2_FRAMED_NECESSITY pair=277->434 cond2=false endpoint=exact profile_mass=5129 adds=24305->24374 no_new_kappa",
+  "virtual_original_D_splice_passes": true
+}

research/h2sem-cond2-framed-necessity/NOTICE.md

@@ -0,0 +1,15 @@
+This package consumes pinned sources from the CrocSwap/integer-mult-bounds
+repository under Apache-2.0. Retained predecessor credit:
+
+- DreamingOfClouds / PR589 and eumemic / PR555: selected R439 word and checker
+  lineage (`research/e8-bit-p111-tuned/`).
+- woklerx / PR1194: H2-sem contract and chronological substitution bridge
+  (`research/r439-semantic-d-contract-seed10/`).
+- PR848 authors: oriented-pair census and C1 helper-temp wrap shape
+  (`research/r439-copy-path-sharing-barrier/`).
+- Aaron Wang / navinor / PR1782: F4 target-feeding-helper probe shape and the
+  open framed condition-2 necessity question (not vendored; reconstructed from
+  the published description against the pinned word/checker).
+- PR1805: priced admitted wraps under H2-sem (companion; not a code dependency).
+
+New text and verifier: Wentao Li with substantial AI assistance. Apache-2.0.

research/h2sem-cond2-framed-necessity/PROOF.md

@@ -0,0 +1,91 @@
+# Framed necessity of H2-sem condition 2 (scoped falsification)
+
+## Proposition
+
+Let W be the pinned selected R439 word
+(`research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz`). Write H2-sem
+for the exact contract of PR1194
+(`research/r439-semantic-d-contract-seed10/PROOF.md`):
+
+1. zero-frame D gates with distinct Y/H operands and no source reads;
+2. no target feeds a helper or source inside D (retained H1 inside D);
+3. complete D operator (x, y, h) → (x, y + N h, h) for a fixed binary matrix N.
+
+Let F4 be the *target-feeding-helper wrap* recorded as a boundary probe in
+PR1782: with the seed-42 best oriented pair (a, b) = (277, 434) and the unique
+last D target t written exactly once at index k = |D| − 1,
+
+- prepend and insert the restored conjugation a += t; …; a += t with the closing
+  restore placed immediately before gate k;
+- on every earlier gate that reads a, replace a by a ⊕ t in the source list.
+
+**Claim (scoped).** On this F4 word:
+
+- H2-sem conditions 1 and 3 hold, and the semantic matrix N equals the raw
+  helper response K of (A, scatter, B) and the baseline N;
+- frames at the D/A cut equal the baseline;
+- condition 2 fails;
+- the complete framed sectional replay on all 661 basis columns equals the
+  desired dirty boundary (x, y, h) → (x, y + x, h), and the independent
+  literal forward/reverse XOR programs agree;
+- the proof-only virtual splice that restores the original target-only D still
+  passes every inherited H1–H5 / U / J / K / C flag.
+
+Consequently, on this exact instance, condition 2 is **not necessary** for the
+framed endpoint substitution conclusion that the chronological bridge is meant
+to transfer. It remains a hypothesis of the written PR1194 block argument; this
+note does not supply a general replacement lemma that drops condition 2 for
+every wrap.
+
+## Exact costs (F4 versus baseline)
+
+| Quantity | Baseline | F4 | Delta |
+| --- | ---: | ---: | ---: |
+| D gates | 111 | 113 | +2 |
+| D source reads / D ADDs | 18085 | 18154 | +69 |
+| Whole-word ADDs | 24305 | 24374 | +69 |
+| Paid profile | {1:1323,2:1342,3:79,4:44,5:102,6:11,7:19} | same | 0 |
+| Rank mass | 5129 | 5129 | 0 |
+| Positive F | 49347 | 50535 | +1188 |
+| Positive B | 1113070 | 2995586 | +1882516 |
+| Local guard `64 F³ B²` | 93 bits | 96 bits | still < 2^104 |
+| Nine-stage guard | 177 bits | 183 bits | still < 2^192 |
+
+F4 is a necessity probe, not a saving construction: it raises ADD count and
+envelopes while leaving the paid profile fixed.
+
+## Why the endpoint can hold without condition 2
+
+Condition 3 already forces every helper and source row of the D operator to be
+the identity and every target row to be the identity plus a helper-only shear.
+The temporary target→helper conjugation in F4 is closed before t's own write, so
+the net D matrix still meets condition 3. Non-D sections are byte-identical to
+the baseline, so the raw K, the virtual original-D splice, and the continuation
+after the D/A cut are unchanged. Equality of the D operator on F₂ coefficients
+gives equality on every F₂-module stream (PR1194's module argument), and the
+framed sectional replay confirms the cut frames match.
+
+Condition 2 is therefore independent of the endpoint identity on this instance:
+it fails while the framed dirty boundary holds. The inherited checker still
+reports `H1_no_target_feeds_z` (and the documented syntactic H2 / K failures),
+so F4 is *not* admitted by the published H2-sem contract; the claim is only that
+condition 2 is not required for the endpoint conclusion itself.
+
+## Controls
+
+- **Unrestored feed.** Dropping the closing a += t breaks condition 3 (a helper
+  row moves).
+- **Late restore.** Closing the conjugation after t's own write breaks condition 3.
+- **C1 contrast.** The PR848 helper-temp wrap on the same pair satisfies all
+  three H2-sem conditions and saves 65 D reads; it is the admitted comparison
+  point, not the necessity witness.
+- **Baseline.** The unwrapped word passes every inherited flag and matches the
+  same endpoint and paid profile.
+
+## Limits
+
+No new κ, no supplier adoption, no claim that every target-feedback wrap is
+safe, and no rewrite of PR1194's published hypotheses. All-size compiler,
+hosting, tape/rounding and analytic obligations remain inherited. Finite
+replay supports the scoped falsification; it is not a formal proof of the
+multiplication theorem.

research/h2sem-cond2-framed-necessity/README.md

@@ -0,0 +1,105 @@
+# H2-sem condition 2 is not necessary for the F4 framed endpoint
+
+**Adversarial interface audit; no new κ.** Complements open
+[PR1782](https://github.com/CrocSwap/integer-mult-bounds/pull/1782) (H2-sem
+admission of the PR848 copy-path wraps; F4 recorded as a boundary probe) and
+[PR1805](https://github.com/CrocSwap/integer-mult-bounds/pull/1805) (priced
+those admitted wraps). This package answers PR1782's open question: on the
+exact F4 target-feeding-helper wrap, is H2-sem condition 2 required for the
+framed dirty endpoint?
+
+## Result
+
+For the seed-42 best pair `277 → 434` on the pinned selected R439 word:
+
+| Check | F4 outcome |
+| --- | --- |
+| H2-sem condition 1 (zero-frame Y/H operands) | pass |
+| H2-sem condition 2 (no target→helper/source) | **fail** |
+| H2-sem condition 3 / semantic N = raw K | pass (661 columns) |
+| Frames at D/A cut | equal to baseline |
+| Framed sectional endpoint `(x,y,h)→(x,y+x,h)` | exact |
+| Literal forward/reverse endpoint | exact |
+| Virtual original-D splice (PR1194 bridge premise) | all H1–H5/U/J/K/C pass |
+| Paid profile / rank mass | unchanged / **5129** |
+
+**Claim:** on this instance, condition 2 is not necessary for the framed endpoint
+substitution conclusion. F4 still fails the published H2-sem contract and the
+inherited H1 flag; this is a necessity falsification, not an admission. No
+general lemma dropping condition 2 for every wrap is claimed. Written argument:
+[PROOF.md](PROOF.md).
+
+### Exact costs (baseline → F4)
+
+| Quantity | Baseline | F4 |
+| --- | ---: | ---: |
+| Whole-word ADDs | 24305 | 24374 (+69) |
+| D ADDs / source reads | 18085 | 18154 (+69) |
+| D gates | 111 | 113 |
+| Rank mass | 5129 | 5129 |
+| F / B | 49347 / 1113070 | 50535 / 2995586 |
+| Local / nine-stage bits | 93 / 177 | 96 / 183 (guards still strict) |
+
+## Reproduce
+
+Python **3.12**, standard library only, from the repository root:
+
+```sh
+python3.12 -I -B research/h2sem-cond2-framed-necessity/verify.py
+python3.12 -I -O -B research/h2sem-cond2-framed-necessity/verify.py
+python3.12 scripts/research_package.py --package research/h2sem-cond2-framed-necessity
+```
+
+Expected:
+
+```text
+PASS_H2SEM_COND2_FRAMED_NECESSITY pair=277->434 cond2=false endpoint=exact profile_mass=5129 adds=24305->24374 no_new_kappa
+PASS_REGISTERED_RESEARCH_PACKAGE research/h2sem-cond2-framed-necessity outcome=completed
+```
+
+`test_package.py` relocates the package and rejects a mutated source pin and a
+mutated expected receipt. Full selected cold replay, Lean, and the multiplication
+theorem were not rerun.
+
+## Scope limits
+
+No new kappa, frontier, native/hosted admission, or compiler/tape claim. Does
+not re-price the PR848/PR1805 admitted wraps. Does not weaken PR1194's published
+hypotheses; it only shows condition 2 is independent of the endpoint identity on
+this F4 witness. Controls: unrestored feed and late restore each break condition 3;
+the C1 helper-temp wrap on the same pair remains the admitted contrast.
+
+## Open next questions
+
+1. **Is there a general replacement for condition 2 that still implies the
+   block-triangular step of PR1194?** Why it matters: a justified weakening would
+   enlarge the admissible wrap class beyond helper-temp conjugations. First step:
+   isolate the exact matrix identity H1 supplies in the W0 factorization and
+   state a D-local substitute. Blocked by: need a proof that covers every
+   zero-frame D, not one F4 witness.
+2. **Do other target-feedback shapes preserve the endpoint while changing the
+   paid profile?** Why it matters: only then could dropping condition 2 interact
+   with κ. First step: enumerate short target-temp conjugations closed before
+   each singleton target write. Blocked by: no favorable completed bill is known;
+   F4 itself raises ADD count.
+
+## Credit
+
+Credit **Aaron Wang / navinor (PR1782)** for the F4 probe shape and the open
+necessity question; **woklerx (PR1194)** for H2-sem and the chronological
+bridge; **PR848** for the pair census and C1 contrast; **DreamingOfClouds
+(PR589)** and **eumemic (PR555)** for the R439 word; **PR1805** for the priced
+admitted-wrap companion (not consumed as code). 
+
+## Disposition (2026-10-14)
+
+**Defer / closed as freestanding upstream claim.** Open
+[CrocSwap/integer-mult-bounds#1782](https://github.com/CrocSwap/integer-mult-bounds/pull/1782)
+already records the F4 `cond2=false` probe with boundary/frames/semantic fields.
+This package’s fuller framed bill is hygiene, not a new independence fact.
+
+
+Prepared by **Wentao Li**
+([VictorLiwentao](https://github.com/VictorLiwentao),
+[@Is__Victor](https://x.com/Is__Victor)) with substantial AI assistance.
+Apache-2.0. No independent human review claimed.

research/h2sem-cond2-framed-necessity/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/CERTIFICATE.json",
+      "usage": "input",
+      "git_blob": "55aec15de43e21e06074dd2bbe0f4b02ad799d09",
+      "sha256": "6235d880c2a671fe11cb54326665eb531c9d6fd80442cd1dcfa39abd867ed441"
+    },
+    {
+      "path": "research/r439-semantic-d-contract-seed10/PROOF.md",
+      "usage": "input",
+      "git_blob": "2707fdb0d2f34c1c6c4ea41c2a68e44904a3e4fd",
+      "sha256": "dfbca8c61a92fdf0db8af450dc4466849da37fc296e28b67f357e196e87327db"
+    }
+  ]
+}