Research: present-head I−G/2 forcing census — 18/18 checked entries need +2 (no new kappa)

research/p104-present-head-side-correction-forcing-census/MASTER-HANDOFF.md

@@ -0,0 +1,71 @@
+# Master handoff — `research/p104-present-head-side-correction-forcing-census/`
+
+## Candidate
+
+- Branch: `cursor/present-head-forcing-census-6ab7`
+- Content tip: scientific package at `293b90598af0e7632cdd398da7171c509091f17e`; master path-fix commit is the packaging tip (read with `git rev-parse origin/cursor/present-head-forcing-census-6ab7`).
+- Package: `research/p104-present-head-side-correction-forcing-census/`
+- Base: `20ecf2891d80b5acf18d980b2164fb44ea7faa90` (CrocSwap `main`)
+- Card: `p104-side-correction` (refined), priority revision 6
+- κ: unchanged `0.001672660197076918`
+- Master repair: `test_package.py` used a hardcoded `/workspace` root for pin/corruption fixtures; replaced with `HERE.parents[1]` so gates pass from any worktree.
+
+## Claim
+
+On the published native-channel word, all 18 checked present-head strict
+`I−G/2` side-correction entries among flags `{1,9,43}` (primary + five
+extra off-diagonal nonzero Gram sources per target row) have every
+insertion-class zero-mass placement obstructed and therefore need
+non-private floor `+2`. No counterexample. Primary feeders:
+`X7:387` (flag 1), `X58:333` (flag 9), `X12:131` (flag 43).
+
+## Closest priors (leave alone)
+
+- [#3601](https://github.com/CrocSwap/integer-mult-bounds/pull/3601) flag-43 side-correction bill — cite sample `(59,21)` / feeder 131; do not reprint bill.
+- [#3610](https://github.com/CrocSwap/integer-mult-bounds/pull/3610) flag-1 side-correction bill — cite sample `(7,0)` / feeder 387; do not reprint bill.
+- [#3532](https://github.com/CrocSwap/integer-mult-bounds/pull/3532) / [#3508](https://github.com/CrocSwap/integer-mult-bounds/pull/3508) head-step repairs — leave alone.
+- [#3443](https://github.com/CrocSwap/integer-mult-bounds/pull/3443) flag-9 chronology — published word only; deferred head-step repair not reopened.
+
+## New checkable fact
+
+Cross-entry obstruction census: 18/18 need `+2`, including flag 9's
+published-word feeder `X58` head `333` at leave event 745. Answers OQ2
+of #3601/#3610 without cloning their verify bill builders.
+
+## Evidence commands
+
+```sh
+python3.12 -I -B research/p104-present-head-side-correction-forcing-census/verify.py
+python3.12 -I -O -Werror -B research/p104-present-head-side-correction-forcing-census/verify.py
+python3.12 -I -O -Werror -B research/p104-present-head-side-correction-forcing-census/independent.py
+python3.12 -I -O -Werror -B research/p104-present-head-side-correction-forcing-census/test_package.py
+python3.12 -B scripts/research_package.py --package research/p104-present-head-side-correction-forcing-census
+```
+
+Expected markers:
+
+```text
+PASS_P104_PRESENT_HEAD_SIDE_CORRECTION_FORCING_CENSUS flags={1,9,43} entries=18/18 need_plus_two primary_feeders=X7:387,X58:333,X12:131 no_new_kappa
+PASS_P104_PRESENT_HEAD_SIDE_CORRECTION_FORCING_CENSUS_INDEPENDENT flags={1,9,43} entries=18/18 need_plus_two primary_feeders=X7:387,X58:333,X12:131 no_new_kappa
+PASS_P104_PRESENT_HEAD_SIDE_CORRECTION_FORCING_CENSUS_TESTS groups=6
+PASS_REGISTERED_RESEARCH_PACKAGE research/p104-present-head-side-correction-forcing-census outcome=completed
+```
+
+## Soft-overlap risks
+
+- Scientific novelty is the multi-entry obstruction census + flag-9 feeder,
+  not file clones of #3601/#3610 bill builders (those are not imported).
+- Do not reopen deferred `research/p104-flag9-head-step-repair/`.
+- Do not edit open #3610/#3601/#3532/#3508 packages.
+
+## Open questions
+
+1. Full-row extension beyond the 18-entry sample on Y7/Y23/Y59.
+2. Flag-9 end-cut side-correction bill / private-copy discount on the
+   published word (fallback card; still no co-hosted repair).
+
+## Disposition note for master
+
+Worker produces fork branch + package only. Do **not** open a CrocSwap PR
+from this worker. Master decides publish/defer after independent skeptical
+review.

research/p104-present-head-side-correction-forcing-census/NOTICE.md

@@ -0,0 +1,10 @@
+# Notice
+
+This package is a finite least-frame forcing census of present-head
+`I−G/2` side-correction entries on the published P104 native channel. It
+does not modify frozen upstream sources and does not reprint open
+side-correction bills.
+
+Prepared by Wentao Li <wentaol4@illinois.edu> with substantial AI assistance.
+Apache-2.0; predecessor notices and exact source pins are retained in
+`SOURCES.json`.

research/p104-present-head-side-correction-forcing-census/PROOF.md

@@ -0,0 +1,61 @@
+# Proof sketch — present-head side-correction forcing census
+
+## Setup
+
+Let `W` be the published native-channel program pinned by
+`research/p104-native-channel/inputs/LOWRANK-WITNESS.json` (4058 events).
+Let `G` be the P104 Gram matrix rebuilt from the pinned fixture by the
+standard E8-line enumeration. Present-head flags are those whose basis
+head lies in the matched target final; the published hit set is
+`{0,1,9,43}`. This census takes `{1,9,43}` (flag 0 remains with the
+coefficient cascade) and, for each flag target `t`, checks the primary
+flag source together with five further indices `s ≠ t` with `G[t,s] ≠ 0`.
+
+An `I−G/2` side-correction entry at `(t,s)` asks for a common-chart ADD
+that moves coefficient `−G[t,s]/2` from `Xs` into `Yt`. A **zero-mass
+placement** at cut `u` is a least-frame merge of the live frames of `Xs`
+and `Yt` at time `u`, followed by ordinary common-chart ADD closure for
+the rest of `W`, with no added transports.
+
+## Obstruction (class Z)
+
+For each checked entry and each insertion class `u` (the cut `0` together
+with every time after an `add`/`copy` that touches `Xs` or `Yt`), the
+forward sweep returns a first register whose forced frame is not contained
+in that register's endpoint frame. In all 18×(class count) cases the
+sweep returns a nonempty obstruction. Therefore no checked entry admits a
+zero-mass common-chart placement on the published word.
+
+## Forcing heads
+
+Independently of the insertion sweep, replay ADD closure on `W` and let
+`τ` be the first event at which the live frame of `Xs` is not contained
+in the final frame of `Yt`. At time `τ` at least one initial X-head `h`
+lies in `Xs` and outside the target final. The census records a carrier
+path of ADDs taking `h` from its birth register into `Xs` by time `τ`.
+
+Primary feeders:
+
+- Flag 1 `(7,0)`: `τ = 1074`, feeder `X7` head `387` (Gram `G[7,7] = 2`).
+- Flag 9 `(23,4)`: `τ = 745`, feeder `X58` head `333` (Gram `G[23,58] = 0`).
+- Flag 43 `(59,21)`: `τ = 884`, feeder `X12` head `131` (Gram `G[59,12] = 0`).
+
+These match the leave-alone samples of open #3610 and #3601 for flags 1
+and 43; flag 9 is new on the published chronology.
+
+## Parity floor
+
+Any endpoint-restoring non-private correction that temporarily lifts a
+register into a common parent chart and returns it must pay nested
+transport rank on the way up and on the way down. That contribution is
+even. Combined with the zero-mass obstruction, every checked entry has
+strict non-private side-correction floor `+2`.
+
+Private-copy (`+1`) paths and co-hosted repair discounts are out of
+scope; #3610 already shows an R1 free-ride for flag 1, which does not
+refute the published-word strict floor.
+
+## Theorem
+
+All 18 checked present-head strict entries need `+2`. No counterexample
+entry was found. Selected κ is unchanged.

research/p104-present-head-side-correction-forcing-census/README.md

@@ -0,0 +1,80 @@
+# Present-head side-correction forcing census
+
+**Bounded claim.** On the published native-channel word, every checked
+present-head strict `I−G/2` side-correction entry among flags `{1, 9, 43}`
+needs non-private rank floor `+2`. The census covers each flag's primary
+entry plus five additional off-diagonal nonzero Gram sources on that
+target row (18 entries). No counterexample was found. No new κ.
+
+## Why this package
+
+Open [#3601](https://github.com/CrocSwap/integer-mult-bounds/pull/3601)
+prices flag 43's entry `(59,21)` at the co-hosted cut with strict min `+2`
+and co-host discount 0. Open
+[#3610](https://github.com/CrocSwap/integer-mult-bounds/pull/3610) prices
+flag 1's entry `(7,0)` with R1 free-ride / R0 `+2`. Both leave the same
+OQ: does every present-head target row need `+2` for its strict
+side-correction entry?
+
+This package answers that OQ by a **cross-entry obstruction census** on
+the published word. It is not a reprint of those correction words or
+bills. Flag 9 uses the published chronology
+([#3443](https://github.com/CrocSwap/integer-mult-bounds/pull/3443))
+only; the deferred flag-9 head-step repair is not reopened.
+
+## Method
+
+For each checked entry `(target, source)`:
+
+1. Enumerate insertion classes after every `add`/`copy` that touches the
+   source or target register on the published program.
+2. At each class, inject a least-frame merge of the two registers and
+   sweep forward under common-chart ADD closure (class-Z style). Record
+   the first register whose forced frame exits its endpoint.
+3. Separately, track when the source first exits the target final
+   hyperplane and which initial X-heads are present outside that final.
+4. Conclude zero-mass blocked. Endpoint-restoring non-private nested
+   transports contribute even rank mass, so the strict non-private floor
+   is `+2`.
+
+## Primary feeders (leave-alone citations)
+
+| Flag | Entry | Classes obstructed | Source leaves final | Selected feeder | Gram |
+|---:|---|---:|---:|---|---:|
+| 1 | `(7,0)` coef `+1/2` | 19/19 | 1074 | `X7` head 387 | 2 |
+| 9 | `(23,4)` coef `+1/2` | 25/25 | 745 | `X58` head 333 | 0 |
+| 43 | `(59,21)` coef `−1/2` | 28/28 | 884 | `X12` head 131 | 0 |
+
+Flag 1 and flag 43 feeders match the known samples cited by #3610 and
+#3601 (bills not re-derived). Flag 9's feeder `X58:333` via `G7`/`G16`
+is new relative to those open bills.
+
+## Theorem
+
+All 18 checked present-head strict entries need `+2`. No counterexample
+entry appears in this census. Selected κ
+`0.001672660197076918` is unchanged.
+
+## Exact replay
+
+```sh
+python3.12 -I -O -Werror -B research/p104-present-head-side-correction-forcing-census/verify.py
+python3.12 -I -O -Werror -B research/p104-present-head-side-correction-forcing-census/independent.py
+python3.12 -I -O -Werror -B research/p104-present-head-side-correction-forcing-census/test_package.py
+```
+
+## Limits
+
+- Published word only; co-hosted repair charts are out of scope.
+- Sample of 18 entries, not the full ~48 nonzero off-diagonal sources
+  per present-head target row.
+- Non-private floor only; private-copy `+1` paths are not priced here.
+- Does not admit a corrected supplier or change κ.
+
+## Open next questions
+
+Does the same `+2` floor hold for every off-diagonal nonzero Gram entry on
+the three present-head target rows, beyond this 18-entry sample? Separately,
+can a private-copy or end-cut bill for flag 9 on the published word discount
+the non-private floor the way #3610's R1 free-ride does for flag 1, without
+reopening the deferred flag-9 head-step repair?

research/p104-present-head-side-correction-forcing-census/SOURCES.json

@@ -0,0 +1,57 @@
+{
+  "schema_version": 1,
+  "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+  "upstream": "CrocSwap/integer-mult-bounds",
+  "files": [
+    {
+      "path": "research/p104-joint-unit-flags/CERTIFICATE.json",
+      "usage": "input",
+      "git_blob": "0fa7d2d40566e92f3ea1539723abf438ba65adb8",
+      "sha256": "a98126428a8da6eae91c50afcc42e014a284c82b554ef77e5b3a34fc6d228128",
+      "credit": "Nick Petalas, PR #2981"
+    },
+    {
+      "path": "research/p104-native-channel/inputs/LOWRANK-WITNESS.json",
+      "usage": "input",
+      "git_blob": "86beaf424e9f0f800ae3a62797d94ec9386b7706",
+      "sha256": "0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e",
+      "credit": "Reviewed #1991 native channel witness"
+    },
+    {
+      "path": "research/p104-native-channel/inputs/P104-FIXTURE.json",
+      "usage": "input",
+      "git_blob": "2e16f99b295bb386fd13bd8fbd57b42ef54143a9",
+      "sha256": "516c06f6ec3cb84be588c546108de897650288576dd5fbf5fe44b9c5546ad8a4",
+      "credit": "Reviewed #1991 P104 root fixture"
+    },
+    {
+      "path": "research/p104-present-head-flag1-audit/CERTIFICATE.json",
+      "usage": "provenance",
+      "git_blob": "e9575631b17783beb11ba5eb7fa816d05066a997",
+      "sha256": "2ae8b3ef2e9ecf911debe393cff906dfd7247b9fe4bce01f0f794e42c8f4bb3c",
+      "credit": "Leave-alone #3451 present-head flag 1 chronology"
+    },
+    {
+      "path": "research/p104-present-head-flag9-audit/CERTIFICATE.json",
+      "usage": "provenance",
+      "git_blob": "e41c2ea6a4649dbbd81ba8747ac74ce1728c0f55",
+      "sha256": "a69b05689f724bdb02e31d07f1d1b5864537d9efcd33b4a9fae071facb1e1f01",
+      "credit": "Leave-alone #3443 present-head flag 9 chronology (published word only)"
+    },
+    {
+      "path": "research/p104-present-head-flag43-audit/CERTIFICATE.json",
+      "usage": "provenance",
+      "git_blob": "cc3e0622aabd16798ee0ca2f32212a7e15ee7f1b",
+      "sha256": "65168f4813bdb5e5a64c08ca53d031aab6e734bc8bb025c5321441098fb83ee1",
+      "credit": "Leave-alone #3456 present-head flag 43 chronology"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5",
+      "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0",
+      "pin": "base_commit:docs/research/agent-task-catalog.json",
+      "credit": "Priority revision 6 task catalogue at the pinned base"
+    }
+  ]
+}