Record the corrected frame ranks of the PR5827 early read.

research/p104-unread-early-read/PROOF.md

@@ -0,0 +1,130 @@
+# Early read on the PR #5827 role-695 interval
+
+This note checks one published replacement. It does not recompute conditional
+kappa, native phases, or the caller bill.
+
+## Pinned words
+
+The source word is the PR #5811 word vendored by PR #5827 at
+`05cd36e5af06d7a3790e30ce3f449fa89b853768`
+(`inputs/pr5811-WORD.json.gz`, canonical SHA256
+`a06445539ad73fe16deae66fef8c52ffc39f5f14c765eab3dc3d98e0e2d8074c`).
+The edited word is that pull request's published program
+(`inputs/pr5827-WORD.json.gz`, canonical SHA256
+`d1e5ee3b9811ce7be0ad80aecf19b41cd9277e838b3a9fe52d25baa610d58782`).
+Those canonical digests are the `source_word_sha256` and `word_sha256`
+fields of that pull request's `WITNESS.json`. The programs differ at
+indices 13815 through 13821 and nowhere else. Boundaries, frames, ports
+and the live set are identical.
+
+## The interval
+
+Write a, b, c, d for roles 695, 733, 773, 709. Write A, C, B for frames
+3, 597, 1031. Replaying every transport before index 13815 on the source
+word, with the same strict nesting rule as a public move into a larger
+frame and a private move into a smaller frame, puts a and b in A, d in C
+and c in B.
+
+The unique source block at that index is
+
+```text
+MOVE c: B -> C   (private)
+ADD  d += c in C
+MOVE b: A -> C
+ADD  b += c in C
+MOVE a: A -> C
+ADD  a += b in C
+MOVE a: C -> B
+```
+
+The replacement is
+
+```text
+ADD  a += b in A
+MOVE a: A -> B
+ADD  a += c in B
+MOVE c: B -> C   (private)
+ADD  d += c in C
+MOVE b: A -> C
+ADD  b += c in C
+```
+
+Both schedules are legal on these entry frames. Both finish with a in B,
+b in C, c in C and d in C, and with images
+
+```text
+a' = a + b + c
+b' = b + c
+c' = c
+d' = d + c
+```
+
+taken over the interval-entry values. The first replacement event reads b
+while b still carries its entry value: b is not the destination of any
+earlier event in the block. Omitting that event stays frame-legal and
+yields `a' = a + c`. Replacing its coefficient 1 by 2 yields a term `2b`.
+Moving that same event to the end of the block is not a legal common-chart
+addition: a then sits in B and b sits in C, while the event still names
+frame A.
+
+Reading the post-update value `b + c` and also adding c, which is the
+arithmetic content of a late read followed by the direct `a += c`, produces
+`a + b + 2c`. That counterfactual is not itself a legal schedule of this
+interval. The legal early read is what keeps the coefficient of c equal to 1.
+
+## Frame ranks
+
+The frame bases have lengths 0, 1 and 5, and their XOR-spans have sizes
+1, 2 and 32, so those lengths are the F_2-dimensions. The spans are strictly
+nested: span(A) proper subset span(C) proper subset span(B). A transport
+rank is the absolute difference of basis lengths, which is the rank used by
+PR #5827's own native boundary check.
+
+The two role-695 transports in the source block therefore have ranks
+
+```text
+A -> C : |1 - 0| = 1
+C -> B : |5 - 1| = 4
+```
+
+and the replacement transport has rank
+
+```text
+A -> B : |5 - 0| = 5.
+```
+
+The other two moves, private c from B to C (rank 4) and public b from A to C
+(rank 1), occur in both schedules. The MOVE-rank multiset therefore changes
+by exactly `-H_1 - H_4 + H_5`.
+
+PR #5827's proof says these frames have dimensions 0, 4 and 5, and that the
+public queries A to C and C to B have ranks 4 and 1. The nesting claim is
+right. The dimensions and the assignment of the two leg ranks are not.
+The histogram change written next to that sentence, `-H_1 - H_4 + H_5`,
+still matches the word.
+
+## Local power sign
+
+For `H_r(t) = r^t` and `0 < t < 1`,
+
+```text
+1^t + 4^t - 5^t > 0.
+```
+
+Indeed `1^t = 1`, and dividing by `5^t` gives the equivalent inequality
+`(1/5)^t + (4/5)^t > 1`. For `v` in `(0, 1)` and `t` in `(0, 1)`,
+`v^(t-1) > 1`, hence `v^t > v`. Both `1/5` and `4/5` lie in `(0, 1)` and
+sum to 1, so the two strict comparisons add. At `t = 1` the difference is 0.
+At `t = 2` it is `1 + 16 - 25 < 0`.
+
+One extra coefficient-+1 ADD is present. Under the scalar rule
+`2 * (3 + bit_length(n) - 1 + bit_count(n) + bit_length(d) - 1)` with
+`n = d = 1`, that ADD costs 8 real scalar primitives. This is a local
+charge, not a caller moment.
+
+## What this does not show
+
+It does not show that the native phase of either actual map matches the
+published receipt, that the full ordinary and outer bill crosses at
+0.00312476680, or that any of the five framework assumptions holds. The
+selected frontier is unchanged.

research/p104-unread-early-read/README.md

@@ -0,0 +1,84 @@
+# Early source observation on the PR #5827 unread path
+
+**Partial audit; no new kappa.** The selected frontier stays the conditional
+result recorded at this base. This package does not admit PR #5827.
+
+## Scope and evidence
+
+Task card: `p104-side-correction`, scope **refined**. The live handoff on
+[Discussion #1166](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166)
+for [PR #5827](https://github.com/CrocSwap/integer-mult-bounds/pull/5827)
+asks for an independent review of the early source observation, the direct
+native phase and the full bill. This package settles the early observation
+and the frame ranks it sits on. The native phase and the caller bill are
+open.
+
+On the pinned PR #5811 word, the seven events at index 13815 are the unique
+copy of the published source block. The published replacement word differs
+only there. Replaying frames up to that cut puts roles 695 and 733 in frame
+3, role 709 in frame 597 and role 773 in frame 1031. Both schedules are
+legal and realize
+
+```text
+a' = a + b + c,  b' = b + c,  c' = c,  d' = d + c
+```
+
+with the same exit frames. The first new event is `ADD 695 += 733` in frame
+3, while role 733 still holds its interval-entry value. Omitting it drops
+`b` from `a`. A coefficient 2 writes `2b`. Placing that event after the
+other six is not a legal common-chart addition.
+
+Frame bases at 3, 597 and 1031 have lengths 0, 1 and 5, and the spans are
+strictly nested. The role-695 legs therefore have ranks 1 (frame 3 to 597)
+and 4 (frame 597 to 1031). The replacement leg has rank 5. PR #5827's proof
+states dimensions 0, 4 and 5 and assigns those two leg ranks in the opposite
+order. The nesting claim is right. The MOVE multiset still changes by
+`-H_1 - H_4 + H_5`, because the other two moves are common to both
+schedules. For every real `t` in `(0, 1)`, `1^t + 4^t - 5^t > 0`. One extra
+coefficient-+1 ADD costs 8 real scalar primitives under the retained local
+rule. That is not a caller moment.
+
+The argument, pins and controls are in [PROOF.md](PROOF.md). Source commits,
+Git blobs and SHA256 pins for the catalogue and selected record are in
+[SOURCES.json](SOURCES.json). The two word files are live inputs; their
+gzip and canonical SHA256 pins are constants in `verify.py`, matched to
+PR #5827 `WITNESS.json`.
+
+## Reproduce
+
+From the repository root, with Python 3.12:
+
+```sh
+python3 scripts/research_package.py --package research/p104-unread-early-read --check-only
+python3.12 -B scripts/research_package.py --package research/p104-unread-early-read
+```
+
+Both registered modes print:
+
+```text
+PASS_P104_UNREAD_EARLY_READ
+```
+
+No network and no third-party package. The verifier walks the vendored
+words directly. It does not import `research/p104-unread-path-resynthesis`.
+
+## Open next questions
+
+- Do the native phases of the actual rank-1 map (frame 3 to 597) and the
+  actual rank-4 map (frame 597 to 1031) match the PR #5827 receipt? The
+  published sentence points a reviewer at a rank-4 map from frame 3 to
+  frame 597, which is not this transport. First lower those two frame
+  pairs. This package does not vendor the Clifford code.
+- Does the complete caller bill still lie in
+  `(0.00312476681507, 0.00312476681508)`? The corrected labels do not
+  change the paid multiset, so the number can survive, but it was not
+  recomputed. The five framework assumptions remain, and this audit is
+  not a reason to move the selected frontier.
+
+## Credit
+
+The words, the seven-event plan and the conditional-kappa claim belong to
+Mason Hale's PR #5811 and Ali Romman's PR #5827, with the retained
+native, helper, controller, compiler and analytic predecessors named there.
+The independent frame walk, the rank correction and this verifier are new.
+Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0.

research/p104-unread-early-read/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    }
+  ]
+}

research/p104-unread-early-read/TASK.json

@@ -0,0 +1,123 @@
+{
+  "schema_version": 1,
+  "task_id": "p104-side-correction",
+  "priority_revision": 8,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "original_card": {
+    "id": "p104-side-correction",
+    "question": "Can joint helper bases and a legal causal split improve the complete P104 productive/paid invoice?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+      "research/p104-helper-subspace-splits/README.md",
+      "research/dyadic-helper-channel-capacity/README.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. 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",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Start with the selected #5599 emitted word and review pending #5718 distinct input/output bases plus #5717/#5719 coverage before claiming work. Pick one uncovered source word, helper group and cut region. Prove the arbitrary-input relation and legal entry/exit corrections, then compare full target and paid profiles. Reject if completion, owned lifetimes or consumer costs repay the gain. A static pairing rank alone is not a physical split.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "P104",
+      "helper basis",
+      "helper split",
+      "5718",
+      "dyadic capacity"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4133: literal-slot defect",
+        "evidence": "research/p104-literal-slot-defect/README.md",
+        "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.",
+        "status": "author-checked",
+        "source_commit": "88666f1dee93fbd85b31fd5d6f91a219e111b5f4",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4136: uniform commutation gap",
+        "evidence": "research/p104-uniform-commutation-gap/README.md",
+        "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.",
+        "status": "author-checked",
+        "source_commit": "281ce601a8be9db470de630759179c23e1dfaa88",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4140: uniform encoding gap",
+        "evidence": "research/p104-uniform-encoding-gap/README.md",
+        "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.",
+        "status": "author-checked",
+        "source_commit": "de25c6525aa866962309df5d107b32d55e6e5628",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4153: source-chart shortcut exhausts its optimistic allowance",
+        "evidence": "research/p104-source-chart-shortcut/README.md",
+        "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.",
+        "status": "author-checked",
+        "source_commit": "9123241fea53df77e51ffe30d9aca1625d4bf3a8",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4154: fiber-tag seam mismatch",
+        "evidence": "research/p104-fiber-tag-seam/README.md",
+        "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.",
+        "status": "author-checked",
+        "source_commit": "4ffcdaee5d6255a9cea1fe53a5424435068089d0",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Independently check the early source observation of open PR #5827 on the pinned PR #5811 word: the seven-event role-695 interval at index 13815, the legal frames at that cut, and the paid ranks of frames 3, 597 and 1031.",
+  "scope_change_reason": "The card asks for one uncovered helper group and a complete invoice. This package does not search for a new split and does not replay the caller. It checks the first clause of the live #1166 handoff on PR #5827, whose smallest next task is an independent review of the early source observation, the direct native phase and the full bill. Only the early observation and its frame ranks are settled here.",
+  "bottleneck_link": "Complex currently binds. PR #5827 claims a small conditional gain by replacing two role-695 transports with one direct transport. The early read is the identity that makes those transports equivalent on arbitrary entry values. Correcting which leg has rank 4 tells a later native-phase audit which maps to inspect. This package does not raise selected kappa.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the unique seven-event identity, the frame-rank correction and the early-read controls. Do not rerun the sealed caller, Clifford lowering or outer moment.",
+  "outcome": "partial",
+  "evidence": "research/p104-unread-early-read/verify.py prints PASS_P104_UNREAD_EARLY_READ. It replays the vendored PR5811 and PR5827 words, checks the four-role images and rejects the proof sentence that frames 3, 597 and 1031 have dimensions 0, 4 and 5.",
+  "author": "unpaidmoon",
+  "ai_assistance": "Substantial Cursor Grok assistance.",
+  "open_questions": [
+    {
+      "question": "Do the actual native phases of the rank-1 frame-3-to-597 map and the rank-4 frame-597-to-1031 map match PR #5827's native receipt?",
+      "why_it_matters": "The published proof assigns those leg ranks in the opposite order. A phase audit that follows the prose would inspect a rank-4 map from frame 3 to frame 597, and that map is not the word's transport.",
+      "first_step": "Lower the two actual frame pairs (3, 597) and (597, 1031) with the PR #5827 native checker and compare recipe ranks to 1 and 4.",
+      "blocked_by": "This package does not vendor the Clifford lowering code and does not rerun PR #5827's native replay."
+    },
+    {
+      "question": "Does the complete caller bill still cross inside (0.00312476681507, 0.00312476681508)?",
+      "why_it_matters": "The corrected labels do not change the paid multiset, which is still one rank 1 and one rank 4 removed and one rank 5 added. The numerical claim can therefore survive, but it was not recomputed here, and the selected frontier must not move on this audit alone.",
+      "first_step": "Run python3.12 -B scripts/research_package.py --package research/p104-unread-path-resynthesis on PR #5827 head 05cd36e5af06d7a3790e30ce3f449fa89b853768.",
+      "blocked_by": "That package is not on this branch. Its registered replay is a separate serial job, and all five framework assumptions remain."
+    }
+  ]
+}

research/p104-unread-early-read/VERIFY.json

@@ -0,0 +1,22 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/p104-unread-early-read/inputs/pr5811-WORD.json.gz",
+    "research/p104-unread-early-read/inputs/pr5827-WORD.json.gz"
+  ],
+  "commands": [
+    {
+      "argv": ["{python}", "-B", "{package}/verify.py"],
+      "timeout_seconds": 60,
+      "checks": "Unique seven-event cut, four-field images, corrected frame ranks 0/1/5, early-read omission and doubled-coefficient controls"
+    },
+    {
+      "argv": ["{python}", "-O", "-B", "{package}/verify.py"],
+      "timeout_seconds": 60,
+      "checks": "Same certificate with assertions removed; require() still rejects a bad schedule"
+    }
+  ]
+}