Prove the declared active-feedback decoder keeps one y0 coupling monomial

research/active-feedback-coupling-lock/PROOF.md

@@ -0,0 +1,110 @@
+# The declared decoder keeps one active-feedback coupling monomial
+
+Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0.
+
+No new κ is claimed. The selected frontier is unchanged.
+
+## Object
+
+Use the published two-edge feed in
+[research/coded-active-feedback](../coded-active-feedback/PROOF.md):
+save the first FULL output `h`, add it to the second query, and add
+`C1 Q^2` times that response to the final query. In the predecessor's
+group algebra the post-query4 bank, and its final image, has x0
+coefficient
+
+```text
+A = D1 Q^{-1}
+```
+
+and y0 coefficient
+
+```text
+B = Q^{-1} C1 Q (I - Q) D1.
+```
+
+The same algebra gives `B = K A` with
+`K = Q^{-1} C1 Q^2 (I - Q)`. Both `K` and `B` are nonzero. This identity
+is the predecessor's left-associate relation; the new statement is about
+the decoder that is allowed to act on every saved bank.
+
+The declared decoder is the infinite family already named by the
+predecessor search: every reduced alternating `C1`/`C3` word, and the
+same words multiplied on the right by `Q^2`. Rational sums of those
+monomials are included. Odd powers of `Q`, port-dependent maps and a
+different feedback edge are not.
+
+## Witness
+
+Write α for the basis key `Q^{-1}` on the `D1` line, word `(-1,)` with
+D-exponent `(1, 0)`. Write β for the basis key word `(-1, 2, 1)` with the
+same D-exponent. The restored coefficient `A` is exactly the α term, and
+the coupling `B` contains the β term with coefficient `+1`.
+
+For a monomial control `W` of D-exponent 0, left multiplication acts on
+these keys by the inverse monomial. Therefore a rational decoder output
+has equal α coefficient in its x0 block and β coefficient in its y0
+block whenever every saved bank does, after pullback by every declared
+`W`.
+
+## Finite support
+
+Replay of the published feed produces 39 saved banks. On input columns
+x0 and y0, the only words that occur on the `D1` line are
+
+```text
+(), (-1,), (-1, 2), (2, 1), (-1, 2, 1), (1, 1, 2), (-1, 2, 1, 1).
+```
+
+The longest has length 4.
+
+For the identity control, the α and β coefficients are equal on every
+bank: both are `1` on `response4`, `query4:3` and final bank `left:2`,
+and both are `0` elsewhere. Those three banks are the published restored
+row and its final image, together with the paid response that creates it.
+
+For a nonempty alternating code word `w` of C-length `n`, the inverse
+does not shorten `w`, and multiplication by α appends `Q^{-1}` at a
+code letter, which does not cancel. The α preimage therefore has length
+`n + 1`. For `n ≥ 4` that length is at least 5, so the preimage misses
+the support. The β preimage is longer. Both pulled-back coefficients
+are 0.
+
+For the right-`Q^2` extension of a nonempty `w`, the same junction count
+gives α-preimage length `n + 3`. For `n ≥ 2` the length is at least 5,
+again outside the support. The empty word's right-`Q^2` extension pulls
+α back to word `(1,)` and β back to `(1, 2, 1)`, neither of which is in
+the support.
+
+The remaining controls are the nonempty alternating words of C-length
+1, 2 and 3, with and without right `Q^2`. There are finitely many. Each
+preimage misses the seven-word support, so both coefficients are 0.
+The verifier enumerates them.
+
+## Conclusion
+
+Every declared decoder output, of any code-word length and any rational
+coefficients, has equal α coefficient on x0 and β coefficient on y0.
+The autonomous target that keeps `A` and deletes the y0 block has those
+coefficients `1` and `0`. It is not attained.
+
+In particular the published coupling cannot be removed by this decoder
+while the restored coefficient is kept: the β term of `B` would have to
+stay equal to 1. This uses every saved bank, including the final four,
+not only the pre-response4 observations in the predecessor's 8,281-policy
+search.
+
+The obstruction is grammatical. Final bank 1 is a pure y0 monomial.
+Left multiplication by the two-term element `B` times that monomial's
+inverse clears y0 on the restored bank and leaves x0 equal to `A`. Both
+words of that correction contain an odd power of `Q`, so the correction
+is not a declared code word and is not priced as a free Pauli. No claim
+is made that an odd-`Q` or port-dependent map has a favorable bill.
+
+## What is not proved
+
+The x1 block of the restored bank is untouched. No new feedback edge is
+tested. The formal algebra is the predecessor's sufficient identity
+model, not a claim that every extra physical relation is absent. Native
+tape, precision, compiler and outer costs are not repriced. The selected
+conditional κ is not changed.

research/active-feedback-coupling-lock/README.md

@@ -0,0 +1,88 @@
+# Declared decoder cannot clear the active-feedback y0 coupling
+
+**Scoped obstruction; no new κ.** In the published two-edge feed of
+[research/coded-active-feedback](../coded-active-feedback/README.md),
+every rational sum of alternating `C1`/`C3` words, with or without a
+right `Q^2`, preserves one monomial of the second-input coupling
+whenever it keeps the restored coefficient `D1 Q^{-1}`.
+
+The predecessor already showed that one bounded search attains only one
+of the four jobs. The new statement is exact for the whole infinite
+decoder family, and it uses all 39 saved banks. The witness is two basis
+coefficients. [PROOF.md](PROOF.md) gives the support bound and the length
+count. The selected frontier is unchanged.
+
+## Result
+
+Let α be the `D1`-line key `Q^{-1}` and β the `D1`-line key
+`Q^{-1} C1 Q`. The restored coefficient is the α term. The coupling
+`Q^{-1} C1 Q (I-Q) D1` contains the β term with coefficient `+1`.
+
+On every saved bank the α and β coefficients agree. Every longer declared
+control pulls both keys outside the seven-word `D1`-line support of the
+trace, so it contributes 0 to both. A decoder output that keeps α
+coefficient 1 therefore keeps β coefficient 1, and the y0 block is not
+zero.
+
+An explicit two-term correction built from final bank 1 does clear that
+y0 block, but both of its words have an odd power of `Q`. It lies outside
+the declared family and is not offered as a free repair.
+
+## Reproduce
+
+From the repository root, Python 3.12, standard library only:
+
+```sh
+python3 -B scripts/research_package.py --package research/active-feedback-coupling-lock --check-only
+python3 -B scripts/research_package.py --package research/active-feedback-coupling-lock
+```
+
+Direct replay:
+
+```sh
+python3 -I -W error -B research/active-feedback-coupling-lock/verify.py
+python3 -I -O -W error -B research/active-feedback-coupling-lock/verify.py
+```
+
+The optimized command still executes the checks. They are `need` failures,
+not assertions. Allow a few seconds. No network, native build or full
+multiplier replay is used.
+
+## Scope
+
+Original card: `joint-query-controller`. Scope status: **refined**. The
+card asks whether one changed caller removes real work. This package
+does not change the query demand. It takes the open coupling question
+left by the active-feedback package, which is the live remainder of the
+passive saved-query handoff
+[discussion comment 19138525](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19138525)
+after that package had already restored the missing coefficient.
+
+Base commit: `7c49fe32c55de02c2c873655c804b16e4c3fef0a`. Pins are in
+[SOURCES.json](SOURCES.json). The catalogue and selected record are
+provenance. `search.py` and `gauge.py` are live inputs.
+
+## Open next questions
+
+Can a port-dependent map, rather than one left multiplier, remove the y0
+term while every required final bank stays intact? The first step is one
+owner-indexed map with the x0 block fixed, the y0 block zero, and the
+other endpoint banks unchanged, then a charge for every new monomial.
+Nothing here supplies that map, and the restored bank's x1 term is a
+separate unpaid obstruction.
+
+Does one feedback edge outside the 8,281-policy family make the whole
+four-input row autonomous? Name the edge and test the row before adding
+calls. This package does not construct one.
+
+## Credit
+
+The trace, algebra and decoder family are Cinna Davis's
+`research/coded-active-feedback`, using Dugongue's PR4948 chronology,
+Dillon's PR4933 code and the passive ceiling packaged by Chris R /
+Clear1nsight. The gauge engine remains the inherited
+`research/coded-native-caller/gauge.py`. New work is the two-point
+support argument and its checker.
+
+Prepared by unpaidmoon with substantial Cursor Grok assistance.
+Apache-2.0.

research/active-feedback-coupling-lock/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/coded-active-feedback/search.py",
+      "usage": "input",
+      "git_blob": "60de5a87d3f64fc69e2595cdb2df771c91a0fe6e",
+      "sha256": "1383010827af29a1b0e595e2c1aa2ffad461b266ffc9f936efce1603ff9f5eb6"
+    },
+    {
+      "path": "research/coded-native-caller/gauge.py",
+      "usage": "input",
+      "git_blob": "44ae72b314cccf677b44d75c374be6dcac1c8167",
+      "sha256": "390391d291353741c89daea999d483660ca185987ed96a15b82576280c487cad"
+    }
+  ]
+}

research/active-feedback-coupling-lock/TASK.json

@@ -0,0 +1,90 @@
+{
+  "schema_version": 1,
+  "task_id": "joint-query-controller",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "original_card": {
+    "id": "joint-query-controller",
+    "question": "Can a changed query demand or caller remove real work while satisfying native chronology and restoration?",
+    "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": "Choose an exact caller and a new demand/interface hypothesis. Read the scoped #5617/#5631/#5649/#5747 and #5720/#5745 objections before rebuilding an excluded schedule. Compare the complete matched source/consumer protocols including all retained helper outputs. For an active-mode injection, first check #5745: its canonical delivery claim repays the eight removed centre jobs. Audit that exact claim or change its channel/feedback hypothesis; do not repeat the same free-injection search. Stop if the full favorable budget fails or the required restored output is unobservable.",
+    "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": [
+      "query demand",
+      "active mode",
+      "5720",
+      "5745",
+      "5747",
+      "caller"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4166: author-checked installed producer/service/return/bridge connection; native-component comparison loses.",
+        "evidence": "research/qq16-caller-install/README.md",
+        "remaining": "Complete matched physical protocol bill, or changed source-compatible demand/circuit; no affordable supplier yet.",
+        "status": "author-checked",
+        "source_commit": "0b082d22a0e9a442d264ab0633e35ef26c790630",
+        "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": "Inside the published two-edge active-feedback trace, the declared alternating code-word decoder, with or without a right Q^2, cannot keep the restored x0 coefficient and erase the y0 coupling.",
+  "scope_change_reason": "The card allows one source-bound obstruction to a changed caller. This package does not propose a new QQ16 demand. It audits the decoder grammar already fixed by research/coded-active-feedback, which is the live remainder of handoff discussioncomment-19138525 after that package restored the missing coefficient.",
+  "bottleneck_link": "A productive main job has to be autonomous. The published active feed restores one coefficient only together with a second-input term. If that term cannot be removed inside the declared decoder, the feed still does not earn the missing productive credit.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop once the declared infinite decoder family is proved to preserve one coupling monomial, or once a legal control inside that family separates the restored coefficient. Do not search a new feedback recipe or price a new Gaussian.",
+  "outcome": "negative-result",
+  "evidence": "PROOF.md and verify.py. The witness is two basis coefficients. No new kappa.",
+  "author": "unpaidmoon, with substantial Cursor Grok assistance",
+  "ai_assistance": "Substantial Cursor Grok assistance. No subagents. The predecessor algebra and replay are imported unchanged.",
+  "open_questions": [
+    {
+      "question": "Can a port-dependent, not globally left, correction remove the y0 term while keeping every required final bank?",
+      "why_it_matters": "The obstruction is for one left multiplier shared by a whole bank. Different owner-wise maps are outside the declared grammar and could still separate the inputs.",
+      "first_step": "Write one owner-indexed map on the final four banks, require the x0 block to stay D1 Q^{-1}, the y0 block to vanish, and the other prescribed endpoint banks to remain intact, then charge every new monomial.",
+      "blocked_by": "No such port-dependent map is supplied here, and the x1 block of the restored bank is a separate unpaid term."
+    },
+    {
+      "question": "Does one changed feedback edge, rather than a larger decoder, make the restored row autonomous?",
+      "why_it_matters": "The 8281-policy search used a bounded word family and was not a proof that every physical feedback fails.",
+      "first_step": "Name one source-bound edge outside that family and test the full four-input row before adding calls.",
+      "blocked_by": "This package does not construct a new edge."
+    }
+  ]
+}

research/active-feedback-coupling-lock/VERIFY.json

@@ -0,0 +1,37 @@
+{
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "checks": "Pins, published row, seven-word support, identity-control equality, short-control preimages outside that support, length formula, decoder images through C-length 12, odd-Q companion outside the family, and the omitted-edge control.",
+      "timeout_seconds": 120
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "checks": "Same coupling lock under optimization. Checks are explicit failures, not assertions.",
+      "timeout_seconds": 120
+    }
+  ],
+  "inputs": [
+    "research/coded-active-feedback/search.py",
+    "research/coded-native-caller/gauge.py"
+  ],
+  "python": "3.12",
+  "requirements": [],
+  "schema_version": 1,
+  "status": "ready"
+}