Prove the unique pair of active feedback operators (no κ)

research/two-edge-feedback-rigidity/PROOF.md

@@ -0,0 +1,150 @@
+# Rigidity of the two existing feedback edges
+
+This scoped proof and its new verifier were produced by Nick Petalas.
+Apache-2.0. The saved-bank interface and its known attaining pair are credited
+to unpaidmoon, PR #6961, building on Cinna Davis's PR #5220 active schedule.
+
+## The inherited interface
+
+Rightmost operators act first. Write Q for the central Gaussian, C for C1,
+D for D1 and b for the unchanged third-input coefficient
+Q^-1 C3 D1 D3. Let F and G be the two feedback operators, respectively.
+The predecessor's saved first-FULL Y row and the pre-query-2 coded X row are
+
+```text
+L = [Q^-1 C D, D, -Q^-1 C D, 0],
+K = [0, -Q D, C D, 0].
+```
+
+Here K is C times the pair-0 X row at that cut. Query 2 returns
+S = Q^-1 (K + F L). The cancellation identity in #6961 gives the row after
+query 4 as
+
+```text
+R(F,G) = B + Q^-1 G Q^-1 (K + F L),
+B      = [0, 0, b, 0].                            (1)
+```
+
+These are inherited schedule premises, not a new native replay. For reference,
+the zero x0 column of K is the cancellation of the first thin against FULL1;
+the bridge adds D x1 to that X bank. The full schedule, phase conventions,
+owned captures and helper contracts remain those of the cited predecessors.
+This contribution begins with (1) and classifies both F and G simultaneously.
+
+## Theorem
+
+Let A be any associative unital ring. Let Q,D be units in A, let C^2=1,
+and assume QD=DQ. Take any b in A and define (1). The operators F,G may
+be arbitrary elements of A; their invertibility is not assumed. Then
+
+```text
+R(F,G) = [D Q^-1, 0, b, 0]
+    if and only if
+F = Q and G = C Q.                                (2)
+```
+
+It already suffices to impose the following two constraints on the row:
+
+```text
+R_1 = 0,
+R_0 + R_2 = D Q^-1 + b.                           (3)
+```
+
+Subscripts 0,1,2,3 correspond to the four original input banks x0,y0,x1,y1.
+This is a statement about independent coefficients, so it retains arbitrary
+values in all four banks.
+
+### Proof
+
+The saved row satisfies L_0+L_2=0, whereas K_0+K_2=C D. Hence (1) gives
+
+```text
+R_0+R_2-b = Q^-1 G Q^-1 C D.                      (4)
+```
+
+The sum has eliminated F without any assumption about F. If (3) holds,
+equation (4), followed by right multiplication by D^-1, gives
+
+```text
+Q^-1 G Q^-1 C = D Q^-1 D^-1 = Q^-1.
+```
+
+Multiply on the left by Q and on the right by C Q. Since C^2=1,
+this forces G=C Q. In particular, G is forced to be a unit even though
+the theorem did not assume it.
+
+Substituting this value into the second-input column of (1) gives
+
+```text
+R_1 = Q^-1 C (F-Q) D.
+```
+
+Both outside factors are units. Therefore R_1=0 forces F=Q.
+This proves necessity using only (3). Conversely, with F=Q and G=C Q,
+
+```text
+K+Q L = [C D, 0, 0, 0],
+R(Q,C Q) = B + Q^-1 C [C D, 0, 0, 0]
+         = [Q^-1 D, 0, b, 0]
+         = [D Q^-1, 0, b, 0].
+```
+
+This also proves sufficiency and the equivalence of (2) and (3). No field
+division, determinant, degree argument, word enumeration, faithful group
+representation, Q^4 relation or C/D commutation was used. In particular,
+the classification survives any quotient in which the interface equations
+and the stated unit relations hold. This is the same rigidity theorem,
+not a physical-cost claim. ∎
+
+## What the classification changes
+
+PR #6961 supplied the pair (Q,C Q), both one-edge obstructions, and explicitly
+excluded classification of every pair from its claim. The new step is the
+elimination (4), which forces that pair even when both operators vary over
+the entire algebra. A larger polynomial or word search on these same two
+edges cannot yield another way to meet this row contract. A further relation
+among physical operators cannot create a second pair of operator values while
+preserving (1) and its unit hypotheses; it can identify different expressions
+for the same pair.
+
+The existing attaining pair is not new. Its ordinary bill and unchanged scalar
+suffix are studied separately in unpaidmoon's open PR #7077. The new proof
+does not replay or recertify that bill or the complete final banks. It does
+not exclude a new saved source, a changed insertion point, a new decoder,
+an altered row target, or a changed source schedule.
+
+## Executable evidence and its boundary
+
+The verifier independently represents (1) by exact 2-by-2 matrices over
+Z/2, Z/3 and Z/4, including noncommuting Q,C and nonunit candidate F,G.
+It enumerates every F,G for each declared fixture and checks the complete
+accepted set, plus the aggregate predicate (3). A separate scalar evaluator
+applies the two feedback operations to every eight-scalar input for its
+three designated fixtures. This finite corroboration is distinct from the
+all-ring proof above. These reduced-interface fixtures are not native
+realizations of the inherited full schedule.
+
+Controls reject a reversed noncommutative product, show why either an x0-only
+check or a zero-y0-only check is insufficient, and reject singular Q/D,
+noninvolutory C, noncommuting Q/D and malformed fixture values. The verifier
+imports no predecessor scientific program and runs no predecessor census.
+
+All loops have fixed domains: modulus at most four, four matrix entries,
+two scalar coordinates, at most 75 fixtures, at most 65,536 operator pairs
+per fixture and at most 65,536 scalar inputs per designated fixture.
+There is no recursion or dynamic code evaluation. Checks use explicit failures
+and remain enabled under optimization. The script owns no subprocesses or
+network resources; its optional new receipt uses an exclusive context-managed
+file and binds all six authored package files by SHA256.
+
+Power-of-Ten rule 3 deviation: CPython's integers, tuples, dictionaries and
+iteration machinery allocate during verification. Fixed allocation is not
+available in this interpreter. The fixed domains above bound live data; a
+census retains at most its 65,536 matrix pairs if every pair were accepted,
+and all 75 small result records. Normal and optimized warning-strict replays
+check the actual path. A fixed-allocation port would need a separate native
+implementation. No low-level fixed-allocation compliance is claimed.
+Functions stay below 60 physical lines. There are no callback dispatch tables,
+hidden imports, mutable shared state or suppressed diagnostics. The repository's
+registered-package checks provide the applicable recurring validation; a new
+whole-repository lint configuration is outside this isolated result.

research/two-edge-feedback-rigidity/README.md

@@ -0,0 +1,81 @@
+# The autonomous row forces a unique two-edge feedback pair
+
+Scoped written proof with exact finite corroboration, produced by Nick Petalas.
+For the unchanged saved-bank interface of
+[unpaidmoon's #6961](https://github.com/CrocSwap/integer-mult-bounds/pull/6961),
+the only two feedback operators attaining its autonomous four-input row are
+`F1=Q` and `F2=C1 Q`. Both operators may vary arbitrarily in the predecessor's
+algebra. The known pair itself is credited to #6961. The new result is its
+uniqueness, which the predecessor explicitly left unproved.
+
+The sum of the first and third output columns eliminates F1 and forces F2.
+The zero second column then forces F1. [PROOF.md](PROOF.md) proves the result
+over every associative unital ring with the declared units and commutation
+relation. It uses no search bound or faithful representation assumption.
+Any quotient preserving those interface equations has the same unique pair
+of operator values. This closes further two-edge tuning within that interface.
+
+No new κ, complete caller, native construction, physical tariff or selected
+frontier change is claimed. The row still contains two input jobs in one bank.
+The existing pair's separate ordinary bill and final-bank question belong to
+[#7077](https://github.com/CrocSwap/integer-mult-bounds/pull/7077); they are cited,
+not reverified. New saved sources, different insertion points and different
+decoder or target contracts remain outside this theorem.
+
+## Reproduction
+
+From the repository root:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/two-edge-feedback-rigidity/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/two-edge-feedback-rigidity/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/two-edge-feedback-rigidity
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/two-edge-feedback-rigidity --check-source-history
+```
+
+CPython 3.12 and its standard library suffice. The direct verifier is also
+Git-free and reads only the six authored files in this directory. It prints
+`PASS_TWO_EDGE_FEEDBACK_RIGIDITY`, exact enumerated coverage and source hashes.
+Add `--receipt /absolute/new/path.json` to save that generated receipt outside
+the package. It refuses to overwrite an existing file. Default replay writes
+no artifacts. The registered normal and optimized checks have 120-second
+timeouts. Provenance validation uses full Git history separately.
+
+The matrix census checks 97,090 operator pairs on 75 fixtures, with exactly
+one solution per fixture. These include all 72 binary unit triples satisfying
+the reduced hypotheses, two specified ternary triples and one Z/4 triple.
+It includes singular candidate feedback operators. The independent scalar
+evaluator checks all 78,658 inputs of the latter three fixtures. Three semantic
+controls and six invalid-fixture controls also pass. The finite fixtures
+corroborate the new abstract theorem; they do not replay the predecessor's
+physical word or certify its native premises.
+
+## Open next questions
+
+- Can a different chronological saved source replace one of these edges with
+  a favorable complete bill? Start by changing one of K or L and deriving its
+  four independent input columns. The unchanged pair is rigid; source
+  availability, full endpoint restoration and physical costs remain blockers.
+- Can a consumer use the unique row without separately decoding its two jobs?
+  Start with an explicit producer/consumer boundary and include the complete
+  ordinary and recursive invoice. No such consumer is supplied here.
+
+Structured first steps and blockers are in [TASK.json](TASK.json).
+
+## Credit and limits
+
+Credit unpaidmoon #6961 for the one-edge obstructions, the saved-bank identities
+and the attaining pair; Cinna Davis #5220 for the active schedule and operator
+algebra; Dugongue / David Ganz #4948 and Dillon #4933 for the retained chronology
+and normalizers; Chris R / Clear1nsight for passive-caller packaging; and their
+retained native, compiler and precision lineage. The new simultaneous
+classification, abstract proof and reduced-interface verifier were produced by
+Nick Petalas. Apache-2.0.
+
+The original `joint-query-controller` card has changed scope to a local
+classification at a fixed interface. It supplies no favorable full caller bill.
+`SOURCES.json` pins predecessor documents as provenance only. No predecessor
+scientific code, selected cold replay, native, Lean or Docker suite is run.
+All five selected assumptions remain. Independent human and formal proof-kernel
+review are unclaimed. CPython's bounded dynamic-allocation deviation is recorded
+in PROOF.md.

research/two-edge-feedback-rigidity/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8",
+      "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/active-feedback-outside-edge/README.md",
+      "usage": "provenance",
+      "git_blob": "f4f14eb7e46d0aad69048eacbae3cc279bfae033",
+      "sha256": "5ec2b59ccdac4bcf413eb43ac894028a1e8146885579d3f229dd2ccf93617895"
+    },
+    {
+      "path": "research/active-feedback-outside-edge/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "920b67909ae7707ec8729772b95384bd3669fa59",
+      "sha256": "7159786b7fa2f16580e363d04364d421deb2f67416d4b5624dc0d4c3538dff3c"
+    },
+    {
+      "path": "research/coded-active-feedback/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "9716baebb4895b07acf9db0cbce010590b03945a",
+      "sha256": "c6233d2759811190c7ea1be455c9351b61c29f6a8afc8584e7bc0dfbc00f3a3d"
+    }
+  ]
+}

research/two-edge-feedback-rigidity/TASK.json

@@ -0,0 +1,90 @@
+{
+  "schema_version": 1,
+  "task_id": "joint-query-controller",
+  "priority_revision": 8,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "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": "changed",
+  "actual_scope": "Classify both existing feedback operators simultaneously at the reduced saved-bank interface: the autonomous row forces F1=Q and F2=C1 Q.",
+  "scope_change_reason": "Take the explicit unproved all-pairs classification in PR6961 rather than seek a new physical QQ16 caller. The result closes two-edge tuning at the fixed row contract, without a favorable complete bill.",
+  "bottleneck_link": "The earlier two-edge witness supplies a coupled component rather than a complete caller. Uniqueness means that merely enlarging both feedback operator grammars cannot change that row solution; a useful construction must change a source, cut, decoder or target contract.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first proved classification with bounded corroboration. Do not extend to new sources, decoders or costs.",
+  "outcome": "completed",
+  "evidence": "PROOF.md and verify.py; generated hash-bound receipts are optional external outputs.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can a different chronological saved source replace one existing edge with a favorable complete bill?",
+      "why_it_matters": "The unchanged two-edge row has a unique solution, so another operator search cannot find a different solution at this interface.",
+      "first_step": "Change one of the K or L rows and derive all four independent input columns at its legal chronological cut.",
+      "blocked_by": "Source availability, full endpoint restoration and physical costs are not supplied."
+    },
+    {
+      "question": "Can an explicit consumer use the unique coupled row directly?",
+      "why_it_matters": "Two jobs in one output bank are not independent target credit.",
+      "first_step": "State a producer/consumer boundary and its complete ordinary and recursive invoice.",
+      "blocked_by": "No such consumer, delivery or cost certificate is supplied."
+    }
+  ]
+}

research/two-edge-feedback-rigidity/VERIFY.json

@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "New all-pairs reduced-interface solution sets, aggregate criterion, literal arbitrary-input endpoints and nine controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Repeat every mathematical and invalid-input check with optimization enabled."
+    }
+  ]
+}