From 99a352c2f428de0e4c07688e0aedf4ed76ad467a Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Mon, 9 Nov 2026 13:40:58 +0000 Subject: [PATCH] Prove the declared active-feedback decoder keeps one y0 coupling monomial. The published two-edge feed restores D1 Q^{-1} only together with a second-input term. Every alternating code word, with or without a right Q^2, preserves one monomial of that term on all 39 saved banks. Co-authored-by: unpaidmoon --- .../active-feedback-coupling-lock/PROOF.md | 110 ++++++++++++ .../active-feedback-coupling-lock/README.md | 88 +++++++++ .../SOURCES.json | 30 ++++ .../active-feedback-coupling-lock/TASK.json | 90 ++++++++++ .../active-feedback-coupling-lock/VERIFY.json | 37 ++++ .../active-feedback-coupling-lock/verify.py | 169 ++++++++++++++++++ 6 files changed, 524 insertions(+) create mode 100644 research/active-feedback-coupling-lock/PROOF.md create mode 100644 research/active-feedback-coupling-lock/README.md create mode 100644 research/active-feedback-coupling-lock/SOURCES.json create mode 100644 research/active-feedback-coupling-lock/TASK.json create mode 100644 research/active-feedback-coupling-lock/VERIFY.json create mode 100644 research/active-feedback-coupling-lock/verify.py diff --git a/research/active-feedback-coupling-lock/PROOF.md b/research/active-feedback-coupling-lock/PROOF.md new file mode 100644 index 0000000000..27039b6f41 --- /dev/null +++ b/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. diff --git a/research/active-feedback-coupling-lock/README.md b/research/active-feedback-coupling-lock/README.md new file mode 100644 index 0000000000..92a6eec35a --- /dev/null +++ b/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. diff --git a/research/active-feedback-coupling-lock/SOURCES.json b/research/active-feedback-coupling-lock/SOURCES.json new file mode 100644 index 0000000000..40f964f242 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/active-feedback-coupling-lock/TASK.json b/research/active-feedback-coupling-lock/TASK.json new file mode 100644 index 0000000000..72230a8e53 --- /dev/null +++ b/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." + } + ] +} diff --git a/research/active-feedback-coupling-lock/VERIFY.json b/research/active-feedback-coupling-lock/VERIFY.json new file mode 100644 index 0000000000..cba776a50b --- /dev/null +++ b/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" +} diff --git a/research/active-feedback-coupling-lock/verify.py b/research/active-feedback-coupling-lock/verify.py new file mode 100644 index 0000000000..99e17a9de2 --- /dev/null +++ b/research/active-feedback-coupling-lock/verify.py @@ -0,0 +1,169 @@ +#!/usr/bin/env python3 +"""The declared active-feedback decoder preserves one y0 coupling monomial. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. +The predecessor replay and group algebra are imported unchanged. +""" +from hashlib import sha256 +import importlib.util +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent +ALPHA = ((-1,), (1, 0)) +BETA = ((-1, 2, 1), (1, 0)) +SUPPORT = { + (), + (-1,), + (-1, 2), + (2, 1), + (-1, 2, 1), + (1, 1, 2), + (-1, 2, 1, 1), +} + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def load_search(): + path = ROOT / "research/coded-active-feedback/search.py" + spec = importlib.util.spec_from_file_location("active_feedback_search_pinned", path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def declared_controls(search, limit): + """Alternating code words of C-length at most `limit`, with and without right Q^2.""" + family = [] + for word in search.words(limit): + family.append(word) + family.append(search.reduce_word(tuple(word) + (1, 1))) + return list(dict.fromkeys(family)) + + +def c_length(word): + return sum(abs(letter) in (2, 3) for letter in word) + + +def preimage_key(algebra, control, key): + image = algebra.mul(algebra.inv(algebra.term(control, (0, 0))), algebra.term(*key)) + need(len(image) == 1, "control preimage is not a monomial") + ((word, degree), coefficient), = image.items() + need(coefficient == 1 and degree == (1, 0), "preimage left the D1 line") + return word + + +def main(): + pinned = { + "research/coded-active-feedback/search.py": + "1383010827af29a1b0e595e2c1aa2ffad461b266ffc9f936efce1603ff9f5eb6", + "research/coded-native-caller/gauge.py": + "390391d291353741c89daea999d483660ca185987ed96a15b82576280c487cad", + } + for name, digest in pinned.items(): + need(sha256((ROOT / name).read_bytes()).hexdigest() == digest, "changed pin " + name) + search = load_search() + algebra = search.algebra() + q, c1 = algebra.gen(1), algebra.gen(2) + q_inverse, d1 = algebra.inv(q), algebra.D(0) + restored = algebra.mul(d1, q_inverse) + coupling = algebra.mul(q_inverse, c1, q, algebra.add(algebra.one, algebra.neg(q)), d1) + lock = algebra.mul(q_inverse, c1, q, q, algebra.add(algebra.one, algebra.neg(q))) + need(algebra.mul(lock, restored) == coupling, "published y0 coefficient is not the left multiple K A") + need(len(restored) == 1 and len(coupling) == 2 and len(lock) == 2, "unexpected term counts") + need(coupling.get(BETA) == 1, "beta is not a coupling term") + + observed, targets, rows = search.replay(algebra, algebra.one, algebra.mul(c1, q, q)) + by_label = dict(observed) + published = by_label["query4:3"] + need(published[0] == restored and published[1] == coupling, "published row moved") + need(rows[2][0] == restored and rows[2][1] == coupling, "final image of the restored bank moved") + need(published[1].get(BETA) == 1 and published[0].get(ALPHA) == 1, "witness coefficients are not 1") + + support = set() + for _label, row in observed: + for column in (0, 1): + for (word, degree), value in row[column].items(): + if value and degree == (1, 0): + support.add(word) + need(support == SUPPORT, "D1-line word support changed") + + equal_banks = [] + for label, row in observed: + alpha = row[0].get(ALPHA, 0) + beta = row[1].get(BETA, 0) + need(alpha == beta, "identity control already separates " + label) + if alpha: + equal_banks.append(label) + need(equal_banks == ["response4", "query4:3", "left:2"], "unexpected banks carry the witness") + + # Nonempty short words are enumerated. A pure code word of C-length n has + # alpha-preimage length n+1. Its right-Q^2 extension has length n+3. Both + # exceed the support once n >= 4 and n >= 2 respectively. + short = declared_controls(search, 4) + identity_hits = 0 + for control in short: + alpha_word = preimage_key(algebra, control, ALPHA) + beta_word = preimage_key(algebra, control, BETA) + if control == (): + need(alpha_word == ALPHA[0] and beta_word == BETA[0], "identity preimage moved") + identity_hits += 1 + continue + need(alpha_word not in SUPPORT and beta_word not in SUPPORT, + "short control hits the witness support: " + str(control)) + if c_length(control) == 0: + need(alpha_word == (1,) and beta_word == (1, 2, 1), "bare Q^2 preimage changed") + need(identity_hits == 1, "the family lost its identity") + for phase_start in (2, 3): + for n, pure_length, shifted_length in ((4, 5, 7), (5, 6, 8)): + word = tuple(2 + ((j + phase_start) % 2) for j in range(n)) + pure = preimage_key(algebra, word, ALPHA) + shifted = preimage_key(algebra, search.reduce_word(word + (1, 1)), ALPHA) + need(len(pure) == pure_length and len(shifted) == shifted_length, + "length formula failed") + need(pure not in SUPPORT and shifted not in SUPPORT, "long preimage fell into the support") + + # Every declared control, of any C-length, therefore has equal pulled-back + # coefficients: the identity by the bank table, and every other control because + # both preimages miss the finite support. Check the published bound and one + # longer slice directly. + for limit in (7, 12): + for control in declared_controls(search, limit): + alpha_word = preimage_key(algebra, control, ALPHA) + beta_word = preimage_key(algebra, control, BETA) + for _label, row in observed: + need(row[0].get((alpha_word, (1, 0)), 0) == row[1].get((beta_word, (1, 0)), 0), + "decoder image separated the witness") + need(restored.get(ALPHA) == 1, "target lost alpha") + # The autonomous x0 target has no y0 block, so its beta coefficient is 0. + need(restored.get(ALPHA, 0) - 0 == 1, "target witness difference is not 1") + + # Outside the grammar, one left image of final bank 1 clears y0 and keeps A. + # This control is not a declared code word, so it does not contradict the theorem. + companion = rows[1][1] + need(len(companion) == 1 and rows[1][0] == {} and rows[1][2] == {} and rows[1][3] == {}, + "companion bank is not a pure y0 monomial") + correction = algebra.mul(coupling, algebra.inv(companion)) + cleaned = [algebra.add(rows[2][j], algebra.neg(algebra.mul(correction, rows[1][j]))) for j in range(4)] + need(cleaned[0] == restored and cleaned[1] == {}, "odd-Q companion correction failed") + family = set(declared_controls(search, 7)) + for (word, degree), value in correction.items(): + need(value and degree == (0, 0) and word not in family, + "companion correction fell inside the declared family") + + # Wrong second edge must not be described as the same restored coefficient. + _unused, _targets, wrong_rows = search.replay(algebra, algebra.one, {}) + need(wrong_rows[2][0] != restored, "omitted second edge still restored A") + need(targets[0][0] == restored and targets[0][1] == {}, "autonomous target changed") + print("PASS_ACTIVE_FEEDBACK_COUPLING_LOCK") + print("witness_banks", ",".join(equal_banks)) + print("declared_family", "alternating C1/C3 words, optionally times right Q^2") + print("new_kappa", None) + + +if __name__ == "__main__": + main()