Save one boundary XOR at four calls with both output updates nonzero

research/four-call-productive-observations/README.md

@@ -0,0 +1,186 @@
+# A four-call partial-observation saving with two nonzero output updates
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+**Finite exact certificate with a scoped algebraic proof.** Four fixed children
+need exactly **two** paid adapters under partial observation, versus **three**
+when both outputs are observed at every boundary. Their final endpoint is
+`(x+a, y+a, a, b)` on arbitrary dirty input `(x,y,a,b)`. Both output-update rows
+are nonzero. The complete fixed-child bills are **10 versus 11 XORs**.
+
+This answers Open next question 2 of commdata2338's
+[PR #2020](https://github.com/CrocSwap/integer-mult-bounds/pull/2020), at
+`f4f8d2afdd3fec60c7739dcd826497e9738f80c1`. Its length-at-most-three census
+and model are cited premises, not replayed deliverables. The new result is
+one sharp four-call instance. No new kappa or supplier is claimed.
+
+## Contract
+
+Keep #2020's four coordinates `(d0,d1,w0,w1)`, all initially arbitrary.
+A compulsory child `(o,s,t)` performs these two XORs in order:
+
+```text
+d[o] ^= w[s]
+w[t] ^= w[1-t]
+```
+
+An adapter is one of the two workspace shears or one of the four XORs from
+workspace into an output. Each costs one. Arbitrary finite adapter words may
+occur before the first child and after any child. The children are indivisible
+and their order is fixed. Outputs cannot feed workspace or each other. There
+are no free operations, clean helpers, copies, erasures or extra coordinates.
+
+The eager reference undoes each child's workspace shear immediately. At an
+interior observation, only the specified outputs must match this reference.
+At the end, both outputs and both original workspace coordinates must match.
+The full-observation comparator has the same adapter alphabet and may also
+retain noncanonical workspace between children.
+
+Use the child sequence
+
+```text
+(0,0,0), (1,0,1), (1,0,0), (1,0,0).
+```
+
+Observe both outputs after children 1 and 3, and only `d0` after child 2.
+The final boundary observes the complete state. Thus only one output at one
+interior boundary is hidden. The two workspace shear directions both occur.
+
+## Attaining words
+
+Put `U: w0 ^= w1` and `L: w1 ^= w0`. The partial-observation word uses
+`L` after child 2 and `U` after child 4, with no entry adapter.
+
+| Completed boundary | Candidate state | Required eager outputs |
+| --- | --- | --- |
+| Child 1 | `(x+a, y, a+b, b)` | both: `(x+a,y)` |
+| Child 2, then L | `(x+a, y+a+b, a+b, b)` | only `d0=x+a` |
+| Child 3 | `(x+a, y, a, b)` | both: `(x+a,y)` |
+| Child 4, then U | `(x+a, y+a, a, b)` | complete state |
+
+For full observation, use `U` after child 1, `L` after child 2, and
+`d1 ^= w1` after child 4. After child 3, workspace is `(a+b,b)` and the
+outputs are `(x+a,y)`. Child 4 restores workspace to `(a,b)` but leaves
+`d1=y+a+b`; its final output adapter removes b. This costs three adapters
+and satisfies every full observation. Eager execution costs four adapters.
+
+## Why the minima are exact
+
+Every workspace shear is an odd permutation of the three nonzero vectors
+of `F2^2`. Four child shears have even parity. Since data adapters do not
+change workspace, any program restoring workspace must use an even number
+of workspace adapters. With no workspace adapter, the four child shears
+`U,L,U,U` have a nonidentity product. Thus at least two adapters are required
+even under partial observation. The displayed word attains two.
+
+Suppose a full-observation program had at most two adapters. The same parity
+argument and nonidentity product force exactly two workspace adapters and
+no data adapters. With no data adapters, the full observations force the
+workspace row read by each child to equal the incoming a. Child 1 is the only
+writer of d0. The observations of d1 after children 2 and 3, and at the final
+boundary, force that same reader row a for children 2, 3 and 4.
+
+Each of children 1, 3 and 4 applies U after its read. Immediately afterward,
+the first workspace row differs from a by the nonzero second workspace row.
+Workspace remains invertible, so this difference cannot vanish. Restoring
+the required first row therefore needs an adapter in each of three disjoint
+gaps: between children 1 and 2, between children 3 and 4, and after child 4.
+Two workspace adapters cannot cover them. Hence full observation needs at
+least three total adapters; the full-observation word attains three.
+
+This proof is an identity over every vector space over a characteristic-two
+field. In particular, it holds coordinatewise on dirty binary streams.
+The independent finite checks below establish the same minima directly.
+
+## Evidence and reproduction
+
+`verify.py` enumerates every boundary placement and every ordered adapter
+word of lengths 0, 1 and 2. There are respectively
+`1`, `5*6=30` and `binom(6,2)*6^2=540` schedules, including entry preparation,
+repeated gates and two gates in the same gap. Every shorter program is in
+this list. No full-observation schedule succeeds; exactly two of the
+two-adapter schedules satisfy partial observation, and none shorter does.
+
+A coefficient-row interpreter and a separately written literal Boolean
+interpreter agree on every one of the 571 schedules. The latter executes
+each schedule on all 16 dirty inputs under both observation contracts,
+giving 18,272 complete executions. Three attaining words add 48 executions.
+Six semantic controls include a newly observed hidden output, missing final
+restoration, a moved adapter, a clean-input false positive and its dirty
+counterexample, and forbidden output-to-workspace feedback.
+
+From the repository root, using CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/four-call-productive-observations/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/four-call-productive-observations
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/four-call-productive-observations --check-source-history
+```
+
+Use the reviewer's Python 3.12 path in place of the local interpreter path.
+The registered commands repeat the verifier normally and with `-O`. Both
+print `PASS_FOUR_CALL_PRODUCTIVE_OBSERVATIONS partial=2 full=3 xor=10/11`.
+The verifier emits a generated JSON receipt bound to SHA256 hashes of all
+five package files and the pinned source contract. It writes nothing to the
+checkout. Local replay used CPython 3.12.15 on macOS 27.0.1 arm64.
+
+The predecessor README is the only declared external input. Its byte hash
+authenticates the cited contract, without running predecessor mathematics.
+The catalogue and selected record are historical provenance. Exact base,
+Git blobs and SHA256 pins are in [SOURCES.json](SOURCES.json).
+
+## Limits and expansion decision
+
+This is a fixed-call interface result. The two update rows are equal, so the
+net update has rank one. Both outputs receive the incoming a.
+If the children can be opened or replaced, two direct XORs implement the
+same final endpoint. Ten is therefore not an unrestricted circuit minimum.
+
+The comparison charges eight compulsory child XORs and every adapter. It has
+no source-bound recursive caller, native frame maps, ownership/stock schedule,
+tape movement, precision bound, compiler closure or outer invoice. Those costs
+remain unspecified. No selected cold replay, Lean proof, independent human
+review or full multiplication theorem is claimed.
+
+The search stopped at its first improving four-call instance. Its initial
+test hid d1 at all three interior cuts. Inspecting the attaining word showed
+that it already meets the stronger observations after children 1 and 3, so
+the certificate uses those stronger observations. No four-call census or
+further construction search was run. Stop this contribution at the witness;
+a physical expansion needs a named caller and a complete favorable bill.
+
+Power of Ten rule 3 has a managed-runtime deviation. Python allocates tuples,
+lists and integers during verification. Four coordinates, four-by-four
+coefficient matrices, five gaps, at most four adapters per positive word,
+571 shorter schedules streamed one at a time, and 16 inputs bound live
+mathematical data. Functions stay below
+60 physical lines; all loops have these finite bounds. There is no recursive
+search, dynamic code, network use or subprocess in the scientific verifier.
+
+## Open next questions
+
+- Can a four-call instance save adapters when its two final update rows are
+  linearly independent? This would remove the rank-one limitation. First
+  restrict #2020's model to rank-two net updates and seek one witness. The
+  present result leaves that domain unsearched and unreserved.
+- Does a real mandatory child chain permit this single hidden-output cut?
+  First bind the actual observer, child and dirty-return contracts, then
+  charge their full physical invoice. No qualifying caller is supplied here.
+
+## Credit and scope
+
+commdata2338's #2020 supplies the model, independent earlier census and the
+explicit four-call question. Aaron Wang / navinor's #1155, Adam Gall's
+`observer-safe-restoration`, and Sagar Thakrar's
+`reader-restoration-cuts-seed53` supply the restoration and observation
+lineage credited by #2020. Cinna Davis's #1930 studies a different
+output-to-source prefix-chain contract. None of their files or credit lines
+is changed or copied into this package.
+
+The new contribution is the four-call witness, its two sharp minima and
+their direct exhaustive check. The `coverage-law-change` card is marked
+changed in [TASK.json](TASK.json): this is an abstract boundary-cost side
+result, rather than a new productive target split on the selected word.
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19221578)
+records that scope. Publication and archive intake do not establish supplier
+admission or change the selected frontier.

research/four-call-productive-observations/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "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"
+    },
+    {
+      "path": "research/partial-observation-boundaries/README.md",
+      "usage": "input",
+      "git_blob": "06692e56721422d797f0f8f7d2be5a29428d2ae7",
+      "sha256": "72ddf7a70241b4b02749361149287772dc39def8d86ec6ffd5eddeaf2470609c"
+    }
+  ]
+}

research/four-call-productive-observations/TASK.json

@@ -0,0 +1,111 @@
+{
+  "schema_version": 1,
+  "task_id": "coverage-law-change",
+  "priority_revision": 8,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "original_card": {
+    "id": "coverage-law-change",
+    "question": "Can a completed call earn more independent productive target credit without an offsetting paid bill?",
+    "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"
+    ],
+    "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": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.",
+    "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": "Use #5599 as a completed positive control, then choose one uncovered cut/module beyond an applicable frozen exclusion. Derive independence, saturation and chronological availability rather than counting rational rank alone. Price target credits and all new jobs together, then check compiler and actual caller compatibility. Stop on a nonphysical credit or an unfavorable complete relaxation.",
+    "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": [
+      "target credit",
+      "helper split",
+      "coverage law"
+    ],
+    "existing_checks": [
+      {
+        "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": "changed",
+  "actual_scope": "Answer PR #2020 Open next question 2 with one exact four-call partial-observation saving whose two final output-update rows are nonzero.",
+  "scope_change_reason": "The current card concerns actual productive target splitting. This bounded abstract boundary-cost side result answers an explicit predecessor handoff and does not claim a selected supplier or recursive saving.",
+  "bottleneck_link": "A hidden intermediate output can eliminate paid boundary work even when both final outputs change; actual caller and complete physical cost remain necessary.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first improving four-call instance. Prove its exact minima and package it; do not complete the four-call census or extend the search.",
+  "outcome": "completed",
+  "evidence": "verify.py proves minima 2 and 3 by attaining words and complete shorter-word exclusion. Two interpreters agree on all 571 schedules; 18272 literal shorter-program executions, 48 positive executions and six semantic controls pass.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can a four-call rank-two net-update instance save adapters under partial observation?",
+      "why_it_matters": "Removes the equal-update-row limitation of the present witness.",
+      "first_step": "Restrict the unchanged model to independent final update rows and seek one exact witness.",
+      "blocked_by": "Unsearched; no physical caller is supplied."
+    },
+    {
+      "question": "Does a real mandatory child chain admit this hidden-output boundary?",
+      "why_it_matters": "Needed before turning the scalar interface saving into an admitted recursive gain.",
+      "first_step": "Bind actual observers, children and dirty-return contracts and price the complete physical invoice.",
+      "blocked_by": "No source-bound caller, native maps or complete physical bill are supplied."
+    }
+  ],
+  "source_question": {
+    "pull_request": 2020,
+    "author": "commdata2338",
+    "head": "f4f8d2afdd3fec60c7739dcd826497e9738f80c1",
+    "question": 2
+  },
+  "claim_type": "finite exact certificate with a scoped algebraic proof",
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19221578",
+  "environment": {
+    "python": "CPython 3.12.15",
+    "platform": "macOS 27.0.1 arm64",
+    "dependencies": "standard library only"
+  },
+  "coordination": {
+    "upstream_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+    "priority_revision": 8,
+    "overlap_open_prs": 341,
+    "overlap_open_prs_fetched_at": "2026-10-27T16:10:13.962251+00:00",
+    "overlap_discussion_records": 5525,
+    "overlap_discussions_fetched_at": "2026-10-27T16:11:23.435724+00:00",
+    "remote_pagination_complete": true,
+    "local_notes_complete": false,
+    "merged_search_terms": [
+      "partial observation",
+      "partial-observation-boundaries",
+      "four-call adapter",
+      "both final output rows"
+    ],
+    "limitation": "Metadata and README searches do not cover every diff or unpublished work.",
+    "precommit_refresh_utc": "2026-10-27T16:20:26.099078+00:00",
+    "precommit_upstream_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810"
+  }
+}

research/four-call-productive-observations/VERIFY.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/partial-observation-boundaries/README.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Both exact minima; all 571 shorter schedules; separate coefficient and Boolean interpreters; all dirty inputs; positive words; six semantic controls; generated file-hash receipt."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "The same finite certificate with Python assertions disabled."
+    }
+  ]
+}