diff --git a/research/saved-bank-query-source/PROOF.md b/research/saved-bank-query-source/PROOF.md new file mode 100644 index 0000000000..df39af5a08 --- /dev/null +++ b/research/saved-bank-query-source/PROOF.md @@ -0,0 +1,214 @@ +# One saved bank autonomizes the query-4 row + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. + +No new κ is claimed. The selected frontier stays `781451/250000000`. + +## What is proved + +Three statements, in the group algebra of +[research/coded-active-feedback](../coded-active-feedback/PROOF.md). + +1. **Identity.** Save the pair-0 X bank at the `bridge_query2` snapshot. + Add the one operator `I - C1 Q C1` times that bank into the existing + final-query argument, and keep the published second operator `C1 Q^2` + on `response2`. The four-input row after query 4 is the autonomous row + `[A, 0, X1, 0]`. +2. **Charge.** That operator is the unique algebra element which does + this for the named bank. It has exactly two monomials. Each monomial + cancels one term of the y0 coupling and one term of the x1 defect. + Dropping either monomial leaves both defects nonzero. +3. **Census.** Among the 29 recorded banks that exist before the + final-query argument and are not `response2`, this is the only bank + for which any algebra element works. The nine observations recorded + at or after `response4` are not sources for that argument. The same + two lemmas reject them as well. + +The census is exhaustive for that finite list of recorded banks. It is +not a search over operators: each bank is settled by a zero column or by +the inverse of a one-term column. It is not a proof that every further +physical quotient has the same negative list. The positive identity +descends to every quotient of this algebra. + +## The row and the correction + +The published feed uses `F1 = I` on the saved first-FULL Y bank and +`F2 = C1 Q^2` on `response2`. After query 4, and before the scalar +suffix, the pair-1 Y bank is + +```text +[A, B, X1 + E, 0] +``` + +with `A = D1 Q^{-1}`, `X1 = Q^{-1} C3 D1 D3`, and + +```text +B = Q^{-1} C1 Q D1 - Q^{-1} C1 Q^2 D1 +E = -Q^{-1} D1 + Q^{-1} C1 Q C1 D1. +``` + +`B` and `E` are nonzero. The autonomous row is `[A, 0, X1, 0]`. The +query multiplies its argument by `Q^{-1}` and adds the response into +this Y bank, so an extra summand `P S` in the argument adds +`Q^{-1} P S` to the row. The required correction is therefore + +```text +P S = Q [0, -B, -E, 0] = [0, ρ1, ρ2, 0] +ρ1 = -C1 Q D1 + C1 Q^2 D1 +ρ2 = D1 - C1 Q C1 D1. +``` + +`Q` commutes with `D1`. Both `ρ1` and `ρ2` have two monomials. Columns +0 and 3 of the correction are zero, so the published `A` and the zero +y1 coefficient stay in place exactly when `P` contributes nothing there. + +## The named bank + +Write `S` for the pair-0 X bank. The schedule writes it as follows. + +The right boundary starts that bank at `[I, 0, -I, 0]`. Query 0 adds +`C1 Q^{-1}` times this bank into the pair-0 Y bank, whose y0 column is +still `I`. FULL1 then adds `-Q C1` times the Y bank and left-multiplies +by `D1`. The y0 column of that sum is `-Q C1`. Conjugation gives + +```text +D1 (Q C1) = C1 Q D1, +``` + +because `D1` commutes with `Q` and `D1 C1 = Q^{-1} C1 Q D1`, so the +inserted `Q^{-1}` cancels the leading `Q`. The other three columns +cancel, and the pair-0 X bank at FULL1 and at IDLE is + +```text +[0, -C1 Q D1, 0, 0]. +``` + +IDLE left-multiplies the pair-1 X bank, which is still the input `x1`, +by `D1`. The following `+1` bridge adds that bank into pair-0 X. Query 2 +writes the pair-0 Y bank only. The `bridge_query2` snapshot is therefore + +```text +S = [0, -C1 Q D1, D1, 0]. +``` + +`bridge_minus` subtracts the same pair-1 X bank and deletes the `D1` +on `x1`. The copy has to be taken at or before the `bridge_query2` +snapshot. The live pair-0 X bank at the final query has a zero x1 +column. + +## The operator + +`S1 = -C1 Q D1` is a one-term element, so it has a two-sided inverse. +Right multiplication by that unit preserves the number of monomials. +The equation `P S1 = ρ1` has the unique solution + +```text +P = ρ1 S1^{-1} = I - C1 Q C1, +``` + +and that element has exactly two monomials. Direct expansion, using +`C1^2 = I` and `D`-exponent 0 on `P`, gives + +```text +P S1 = -C1 Q D1 + C1 Q^2 D1 = ρ1 +P S2 = D1 - C1 Q C1 D1 = ρ2 +P S0 = P S3 = 0. +``` + +Hence `P S = ρ`, and the row becomes `[A, 0, X1, 0]`. The chronological +replay adds `P S` beside the published summand `C1 Q^2 response2`. It +does not replace that summand, and it does not rewrite any bank +recorded before the argument. + +## Charge of the two monomials + +Rightmost factors act first, as in the predecessor. On the row, after +the query's `Q^{-1}`: + +| Monomial | y0 contribution | x1 contribution | +| --- | --- | --- | +| `I` | `-Q^{-1} C1 Q D1` | `Q^{-1} D1` | +| `-C1 Q C1` | `Q^{-1} C1 Q^2 D1` | `-Q^{-1} C1 Q C1 D1` | + +The first column of the table is `-B`. The second is `-E`. Both +monomials contribute `0` on `x0` and on `y1`, because those columns of +`S` are zero. Either monomial alone leaves one term of `B` and one term +of `E`. Both are charged. + +One circuit under the predecessor's published units, keeping the saved +copy and using a second scratch bank: + +| Step | Unit | Count | +| --- | --- | ---: | +| Copy `bridge_query2:0` into `U` before `bridge_minus` | 112 COPYs | 1 | +| `V ← C1 U` | one F-transpose | 1 | +| `V ← Q V` | 112 monomial passes | 1 | +| `V ← C1 V` | one F-transpose | 1 | +| `V ← U - V` | 112 scalar ADDs | 1 | +| Add `V` into the final-query argument | 112 scalar ADDs | 1 | + +A F-transpose is 896 scalar ADDs, 224 monomial passes and 16 mode +CLEARs. One monomial pass on a 112-owner bank is the predecessor's +`Q^2` unit. The totals are 2016 scalar ADDs, 560 monomial passes, +32 mode CLEARs, 112 COPYs, 224 extra fields, and the inherited 8 mode +fields reused. No Gaussian child is added. This is an upper ledger for +this circuit. It is not a minimum, not a tape proof, and not a κ. + +## Census of the other recorded banks + +Let `ρ = [0, ρ1, ρ2, 0]` with both middle columns nonzero. For a +recorded bank `T`: + +- If `T1 = 0` or `T2 = 0`, then `P T` cannot equal `ρ`. +- If `T0` or `T3` is a one-term element, it is a unit, so `P T` has a + zero in that column only for `P = 0`. Then `P T ≠ ρ`. +- If `T1` is a one-term element, `P = ρ1 T1^{-1}` is the only candidate. + It works only when the other three columns match `ρ`. + +`search.replay` records 30 observations before it builds the `response4` +argument. Excluding `response2` leaves 29 legal sources. The verifier +checks the ordered label list against the schedule and partitions those +29 by the first applicable lemma: + +| Class | Count | Labels | +| --- | ---: | --- | +| Zero on y0 or on x1 | 19 | `right:0` through `right:3`, `response0`, `query0:0`, `query0:2`, `query0:3`, `FULL1:0`, `FULL1:2`, `FULL1:3`, `IDLE:0`, `IDLE:2`, `IDLE:3`, `bridge_query2:2`, `bridge_query2:3`, `bridge_minus:0`, `bridge_minus:2`, `FULL3:0` | +| Unit on x0 or on y1 | 6 | `query0:1`, `FULL1:1`, `IDLE:1`, `bridge_minus:3`, `FULL3:2`, `FULL3:3` | +| Unique candidate spoils x0 | 3 | `bridge_query2:1`, `bridge_minus:1`, `FULL3:1` | +| Works | 1 | `bridge_query2:0` | + +The three labels in the third class are the same vector: the pair-0 Y +bank is not rewritten by `bridge_minus` or by FULL3. Its y0 column is +the unit `Q^{-1} D1`, so the only candidate is +`C1 Q^{-1} - C1 Q^2`. That candidate clears y0 and the x1 defect and +writes `-D1 + C1 Q^2 C1 D1` on x0, which is nonzero. The restored +coefficient `A` moves. + +The nine later labels are `response4`, `query4:0` through `query4:3`, +and `left:0` through `left:3`. They are the final response or the +scalar suffix, so they are not inputs of this argument. The same +partition rejects all nine. + +`response2` is outside the claim because an extra operator on it would +change the coefficient of the published second edge. Its x0 column is +nevertheless a unit, so the only algebra element that preserves `A` is +zero, and zero does not clear `B`. + +## What the suffix does not do + +The scalar suffix is the published bridge, the signed swap, and the two +final additions. With this insertion, none of the four final banks +equals the corresponding uncoded target. The autonomous statement is the +pre-suffix row `query4:3` only. It is not a caller. + +## What is not proved + +No statement is made about a sum of two saved banks, a port-dependent +map, a new call, or an operator inserted anywhere except the existing +final-query argument. The negative census uses this formal algebra, +whose relations are `Q^4 = C1^2 = C3^2 = I`, commuting `D` exponents, +and the inherited conjugation rule. A further physical relation can +kill a nonzero residual and is outside the census. The positive +identity is an equality in this algebra, so it remains an equality in +every quotient. Native tape, precision, compiler, and outer costs are +not priced. The selected conditional κ is not changed. diff --git a/research/saved-bank-query-source/README.md b/research/saved-bank-query-source/README.md new file mode 100644 index 0000000000..4a1ce7b6e3 --- /dev/null +++ b/research/saved-bank-query-source/README.md @@ -0,0 +1,148 @@ +# One saved bank other than response2 autonomizes the query-4 row + +**Scoped identity and finite census; no new κ.** On the published +two-edge feed of +[research/coded-active-feedback](../coded-active-feedback/README.md), +save the pair-0 X bank at the `bridge_query2` snapshot and add +`I - C1 Q C1` times that bank into the final-query argument. The +second operator stays `C1 Q^2` on `response2`. No call is added. The +four-input row after query 4 is autonomous. + +In this formal algebra the operator is the unique element that does +this for the named bank. It has two monomials, and each cancels one y0 +term and one x1 term. Among the other 28 banks recorded before that argument, no +algebra element works. [PROOF.md](PROOF.md) gives the schedule +identity, the monomial charge, and the census. The selected frontier +is unchanged. + +## Result + +The autonomous row at this checkpoint is `[A, 0, X1, 0]`, where +`A = D1 Q^{-1}` and `X1 = Q^{-1} C3 D1 D3`. The published row, with +`F2 = C1 Q^2` and no extra source, is `[A, B, X1 + E, 0]`. Here + +```text +B = Q^{-1} C1 Q (I - Q) D1 +E = (Q^{-1} C1 Q C1 - Q^{-1}) D1. +``` + +The named bank is the replay label `bridge_query2:0`: + +```text +S = [0, -C1 Q D1, D1, 0]. +``` + +`bridge_minus` deletes the `D1` on `x1`, so the copy is taken at this +snapshot. The one operator is `P = I - C1 Q C1`. The replay with +`C3 X + C1 Q^2 response2 + P S` as the final-query argument equals +`[A, 0, X1, 0]` on the pre-suffix row. + +The two monomials, after the query's `Q^{-1}`, contribute + +```text +I: y0 = -Q^{-1} C1 Q D1, x1 = Q^{-1} D1 +-C1 Q C1: y0 = Q^{-1} C1 Q^2 D1, x1 = -Q^{-1} C1 Q C1 D1. +``` + +Their sum is `[0, -B, -E, 0]`. Either monomial alone leaves a term of +`B` and a term of `E`. The field ledger for one circuit that emits both, +under the predecessor's published units, is 2016 scalar ADDs, 560 +monomial passes, 32 mode CLEARs, 112 COPYs, and 224 extra fields. It is +an upper bound for that circuit, not a tape proof. + +The 29 legal sources are the recorded observations before `response4`, +excluding `response2`. Nineteen have a zero y0 or x1 column. Six have a +unit x0 or y1 column, which forces the operator to vanish. Three labels +are the same pair-0 Y bank; its unique candidate clears `B` and `E` and +writes a nonzero x0 correction. Only `bridge_query2:0` works. The nine +later observations are not inputs of this argument, and the same lemmas +reject them. + +The scalar suffix does not produce the four uncoded target banks. This +row witness is not a caller. + +## Evidence class + +The row identity is a proof in the predecessor's formal algebra. The +list of 29 legal banks is an exhaustive finite census: the domain is +the replay's observation list, the enumeration is the ordered labels in +[verify.py](verify.py), and every bank is settled by a zero column or by +the inverse of a one-term column. There is no operator search. A further +physical relation can make a rejected residual zero; that quotient is +outside the census. The positive equality descends to every quotient. + +## Reproduce + +From the repository root, Python 3.12, standard library only: + +```sh +python3 -B scripts/research_package.py --package research/saved-bank-query-source --check-only +python3 -B scripts/research_package.py --package research/saved-bank-query-source +``` + +Direct replay: + +```sh +python3 -I -W error -B research/saved-bank-query-source/verify.py +python3 -I -O -W error -B research/saved-bank-query-source/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 and does not price a new caller. It +answers the second open question of +[research/active-feedback-outside-edge](../active-feedback-outside-edge/README.md), +merged PR #6961. The two-edge bill of `F1 = Q`, `F2 = C1 Q` is not this +package. The x1 block of an owner-indexed fresh image is not this +package. + +Base commit: `17469fff78c22941280f04d39dc5a1faee09c840`. Pins are in +[SOURCES.json](SOURCES.json). The catalogue and selected record are +provenance. The selected conditional result remains +`781451/250000000`. `search.py` and `gauge.py` are live inputs. + +Overlap at this base covered the local note inventory and a live search +of open upstream PR titles. The matching note is the predecessor +package above, where this question is still open. No open upstream PR +title states this saved-bank insertion. PR #7033 is the owner-indexed +x1 block. The declared alternating-decoder lock and the owner-indexed +y0 map read banks after the suffix; they do not insert an operator into +the final-query argument. + +## Open next questions + +After this insertion, which coefficients of the four final banks does +the unchanged scalar suffix clear? The autonomous statement stops at +`query4:3`, and none of the four final banks is the uncoded target. The +first step is to compare those four banks in this replay with the +uncoded targets, before adding a call or a second saved source. No +tape or outer bill is priced here. + +Does one named relation outside `Q^4 = C1^2 = C3^2 = I` and the +inherited `D` conjugation make `bridge_minus:0` succeed? That live bank +has a zero x1 column in this algebra, which is why the saved copy is +required. The first step is to impose that one relation and recompute +`P S` for this same operator. The positive identity on +`bridge_query2:0` is not reopened by a quotient. + +## Credit + +The schedule, algebra, and published feed 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 +`research/coded-native-caller/gauge.py`. The question is open question 2 +of `research/active-feedback-outside-edge` (merged PR #6961). The +declared-family lock and the owner-indexed y0 map are neighboring +results and are not redone. New work is the named bank, the operator +`I - C1 Q C1`, the two-monomial charge, and the census of the other +recorded banks. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. +Apache-2.0. diff --git a/research/saved-bank-query-source/SOURCES.json b/research/saved-bank-query-source/SOURCES.json new file mode 100644 index 0000000000..8bba455056 --- /dev/null +++ b/research/saved-bank-query-source/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "17469fff78c22941280f04d39dc5a1faee09c840", + "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/saved-bank-query-source/TASK.json b/research/saved-bank-query-source/TASK.json new file mode 100644 index 0000000000..4e380a22eb --- /dev/null +++ b/research/saved-bank-query-source/TASK.json @@ -0,0 +1,90 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 8, + "base_commit": "17469fff78c22941280f04d39dc5a1faee09c840", + "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": "Name the saved bank bridge_query2:0 and the one operator I - C1 Q C1 added into the existing final-query argument, with the second operator held at C1 Q^2, and decide whether the four-input row becomes autonomous.", + "scope_change_reason": "The card asks whether a changed caller removes real work. This note does not change the query demand. It answers open question 2 of research/active-feedback-outside-edge, the saved-bank source left open by merged PR #6961.", + "bottleneck_link": "The published feed restores one coefficient only together with a coupled row. One saved bank other than response2, inserted by one operator into the existing final query, is the source-bound change that can separate that row without a new call.", + "budget_minutes": 60, + "stop_rule": "Stop after the named bank, the unique operator, the two-monomial charge, and the finite census of the other recorded banks. Do not add a second source, retarget the suffix, or price an outer bill.", + "outcome": "completed", + "evidence": "PROOF.md and verify.py", + "author": "unpaidmoon, with substantial Cursor Grok assistance", + "ai_assistance": "Substantial Cursor Grok assistance; no subagents.", + "open_questions": [ + { + "question": "After this insertion, which coefficients of the four final banks does the unchanged scalar suffix clear?", + "why_it_matters": "The autonomous statement stops at query4:3. The suffix moves that bank, and none of the four final banks is the uncoded target, so the row witness is not yet a caller.", + "first_step": "Compare the four final banks in this replay with the uncoded targets, before adding a call or a second saved source.", + "blocked_by": "No tape, rounding, compiler, or outer bill is priced, and the suffix is not retargeted here." + }, + { + "question": "Does one named relation outside Q^4=C1^2=C3^2=I and the inherited D conjugation make the live bank bridge_minus:0 succeed?", + "why_it_matters": "That bank has a zero x1 column in this algebra, which is why the saved copy is required. A quotient can kill a nonzero residual and is outside the census. The positive identity descends to every quotient.", + "first_step": "Impose that one relation and recompute P S for I - C1 Q C1 on bridge_minus:0.", + "blocked_by": "No additional physical relation is imposed here." + } + ] +} diff --git a/research/saved-bank-query-source/VERIFY.json b/research/saved-bank-query-source/VERIFY.json new file mode 100644 index 0000000000..3764b81eda --- /dev/null +++ b/research/saved-bank-query-source/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/coded-active-feedback/search.py", + "research/coded-native-caller/gauge.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Pins, the published coupled row, the derived bridge_query2:0 bank, the unique operator I-C1 Q C1, both monomial charges, the inserted replay, the 29-bank census, the nine post-query rejections, the response2 unit control, and the field-ledger arithmetic." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same identities under optimization. Checks are explicit failures, not assertions." + } + ] +} diff --git a/research/saved-bank-query-source/verify.py b/research/saved-bank-query-source/verify.py new file mode 100644 index 0000000000..2b701c95d1 --- /dev/null +++ b/research/saved-bank-query-source/verify.py @@ -0,0 +1,374 @@ +#!/usr/bin/env python3 +"""One saved bank other than response2, with the second operator held at C1 Q^2. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. +The predecessor schedule and group algebra are imported unchanged. No call +is added. The positive identity is one algebra element on one named bank. +The census is the finite list of recorded banks, not a search over operators. +""" +from hashlib import sha256 +import importlib.util +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent +# Inherited field units from research/coded-active-feedback/PROOF.md. +C1_ADDS = 896 +C1_MONOMIALS = 224 +C1_CLEARS = 16 +BANK_ADDS = 112 +BANK_COPYS = 112 +MONOMIAL_PASS = 112 + +PRE_QUERY = ( + "right:0", "right:1", "right:2", "right:3", + "response0", + "query0:0", "query0:1", "query0:2", "query0:3", + "FULL1:0", "FULL1:1", "FULL1:2", "FULL1:3", + "IDLE:0", "IDLE:1", "IDLE:2", "IDLE:3", + "response2", + "bridge_query2:0", "bridge_query2:1", "bridge_query2:2", "bridge_query2:3", + "bridge_minus:0", "bridge_minus:1", "bridge_minus:2", "bridge_minus:3", + "FULL3:0", "FULL3:1", "FULL3:2", "FULL3:3", +) +POST_QUERY = ( + "response4", + "query4:0", "query4:1", "query4:2", "query4:3", + "left:0", "left:1", "left:2", "left:3", +) +ZERO_COLUMN = ( + "right:0", "right:1", "right:2", "right:3", + "response0", "query0:0", "query0:2", "query0:3", + "FULL1:0", "FULL1:2", "FULL1:3", + "IDLE:0", "IDLE:2", "IDLE:3", + "bridge_query2:2", "bridge_query2:3", + "bridge_minus:0", "bridge_minus:2", + "FULL3:0", +) +UNIT_KILLS = ( + "query0:1", "FULL1:1", "IDLE:1", + "bridge_minus:3", "FULL3:2", "FULL3:3", +) +UNIQUE_FAILS = ("bridge_query2:1", "bridge_minus:1", "FULL3:1") +POST_ZERO = ("query4:0", "left:1") +POST_UNIT = ("response4", "query4:2", "query4:3", "left:2", "left:3") +POST_UNIQUE_FAILS = ("query4:1", "left:0") + + +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("saved_bank_search_pinned", path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def schedule(algebra, feedback1, feedback2, insert=None): + """search.replay, plus one optional left operator on the saved pair-0 X bank.""" + q, qi = algebra.gen(1), algebra.inv(algebra.gen(1)) + c1, c3 = algebra.gen(2), algebra.gen(3) + d1, d3 = algebra.D(0), algebra.D(1) + rows = [[algebra.one if i == j else {} for j in range(4)] for i in range(4)] + observed = [] + + def snap(label): + observed.extend((label + ":" + str(i), [dict(entry) for entry in row]) + for i, row in enumerate(rows)) + + def plus(dst, src, op): + rows[dst] = [algebra.add(x, algebra.mul(op, y)) + for x, y in zip(rows[dst], rows[src])] + + def left(index, op): + rows[index] = [algebra.mul(op, entry) for entry in rows[index]] + + def query(pair, argument, label, after=None): + response = [algebra.mul(qi, entry) for entry in argument] + observed.append((label, [dict(entry) for entry in response])) + rows[2 * pair + 1] = [algebra.add(x, algebra.mul(after or algebra.one, y)) + for x, y in zip(rows[2 * pair + 1], response)] + return response + + def full(pair, code, stage): + plus(2 * pair, 2 * pair + 1, algebra.neg(algebra.mul(q, code))) + left(2 * pair, stage) + left(2 * pair + 1, stage) + + def bridge(dst, src, sign): + plus(2 * dst, 2 * src, algebra.term((), (0, 0), sign)) + plus(2 * src + 1, 2 * dst + 1, algebra.term((), (0, 0), -sign)) + + rows[0][2], rows[3][1] = algebra.neg(algebra.one), algebra.one + snap("right") + query(0, rows[0], "response0", c1) + snap("query0") + full(0, c1, d1) + snap("FULL1") + late_y = [dict(entry) for entry in rows[1]] + left(2, d1) + left(3, d1) + snap("IDLE") + bridge(0, 1, 1) + before_query2 = [dict(entry) for entry in rows[0]] + argument = [algebra.add(algebra.mul(c1, x), algebra.mul(feedback1, y)) + for x, y in zip(rows[0], late_y)] + response2 = query(0, argument, "response2") + snap("bridge_query2") + saved = [dict(entry) for entry in rows[0]] + bridge(0, 1, -1) + snap("bridge_minus") + full(1, c3, d3) + snap("FULL3") + argument = [algebra.add(algebra.mul(c3, x), algebra.mul(feedback2, y)) + for x, y in zip(rows[2], response2)] + if insert is not None: + argument = [algebra.add(x, algebra.mul(insert, z)) + for x, z in zip(argument, saved)] + query(1, argument, "response4") + snap("query4") + bridge(1, 0, 1) + for x, y in ((0, 1), (2, 3)): + rows[x], rows[y] = rows[y], [algebra.neg(entry) for entry in rows[x]] + plus(0, 2, algebra.one) + plus(3, 1, algebra.neg(algebra.one)) + snap("left") + return observed, [list(row) for row in rows], saved, before_query2 + + +def derived_source(algebra): + """Pair-0 X bank after the +1 bridge, from the schedule steps that write it.""" + q, qi = algebra.gen(1), algebra.inv(algebra.gen(1)) + c1, d1 = algebra.gen(2), algebra.D(0) + row0 = [algebra.one, {}, algebra.neg(algebra.one), {}] + response = [algebra.mul(qi, entry) for entry in row0] + row1 = [algebra.add(x, algebra.mul(c1, y)) + for x, y in zip([{}, algebra.one, {}, {}], response)] + row0 = [algebra.add(x, algebra.mul(algebra.neg(algebra.mul(q, c1)), y)) + for x, y in zip(row0, row1)] + full1 = [algebra.mul(d1, entry) for entry in row0] + idle_x = [{}, {}, d1, {}] + saved = [algebra.add(x, y) for x, y in zip(full1, idle_x)] + return full1, saved + + +def classify(algebra, bank, rho): + if bank[1] == {} or bank[2] == {}: + return "zero-column", None + for index in (0, 3): + if len(bank[index]) == 1: + inverse = algebra.inv(bank[index]) + need(algebra.mul(bank[index], inverse) == algebra.one + and algebra.mul(inverse, bank[index]) == algebra.one, + "one-term column is not a two-sided unit") + return "unit-kills", None + need(len(bank[1]) == 1, "unclassified bank: y0 column is not a unit") + inverse = algebra.inv(bank[1]) + need(algebra.mul(bank[1], inverse) == algebra.one + and algebra.mul(inverse, bank[1]) == algebra.one, + "y0 column is not a two-sided unit") + operator = algebra.mul(rho[1], inverse) + image = [algebra.mul(operator, column) for column in bank] + if image == rho: + return "works", operator + return "unique-fails", (operator, image) + + +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, qi = algebra.gen(1), algebra.inv(algebra.gen(1)) + c1, c3 = algebra.gen(2), algebra.gen(3) + d1, d3 = algebra.D(0), algebra.D(1) + published_f1, published_f2 = algebra.one, algebra.mul(c1, q, q) + need(published_f2 == algebra.term((2, 1, 1), (0, 0)), "second operator is not C1 Q^2") + + published, targets, published_final = search.replay(algebra, published_f1, published_f2) + labels = [label for label, _row in published] + need(tuple(labels) == PRE_QUERY + POST_QUERY, "recorded bank list moved") + need(len(published) == 39, "saved-bank count is not 39") + by_label = dict(published) + local, local_final, saved, before_query2 = schedule(algebra, published_f1, published_f2) + need([(label, row) for label, row in local] == published, "local schedule drifted from search.replay") + need(local_final == published_final, "local suffix drifted from search.replay") + + row = by_label["query4:3"] + restored = algebra.mul(d1, qi) + original_x1 = algebra.mul(qi, c3, d1, d3) + coupling = row[1] + extra = algebra.add(row[2], algebra.neg(original_x1)) + autonomous = [restored, {}, original_x1, {}] + need(row[0] == restored and row[3] == {} and coupling != {} and extra != {}, + "published row is not A plus a y0 coupling plus an x1 defect") + need(row != autonomous, "published feed is already autonomous") + need(coupling == algebra.add(algebra.mul(qi, c1, q, d1), + algebra.neg(algebra.mul(qi, c1, q, q, d1))), + "y0 coupling is not Q^{-1} C1 Q (I-Q) D1") + need(extra == algebra.add(algebra.neg(algebra.mul(qi, d1)), + algebra.mul(qi, c1, q, c1, d1)), + "x1 defect is not (Q^{-1} C1 Q C1 - Q^{-1}) D1") + rho = [algebra.mul(q, column) for column in [{}, algebra.neg(coupling), algebra.neg(extra), {}]] + need(rho[0] == {} and rho[3] == {} and len(rho[1]) == 2 and len(rho[2]) == 2, + "the required correction is not two monomials on y0 and on x1") + + need(algebra.mul(d1, q, c1) == algebra.mul(c1, q, d1), + "D1 conjugation of Q C1 moved") + full1, derived = derived_source(algebra) + need(full1 == [ {}, algebra.neg(algebra.mul(c1, q, d1)), {}, {} ], + "FULL1 pair-0 X is not the single monomial -C1 Q D1") + need(full1 == by_label["FULL1:0"] == by_label["IDLE:0"], + "FULL1/IDLE pair-0 X drifted from the derivation") + need(derived == [ {}, algebra.neg(algebra.mul(c1, q, d1)), d1, {} ], + "derived saved bank is not [0, -C1 Q D1, D1, 0]") + need(saved == before_query2 == derived == by_label["bridge_query2:0"], + "bridge_query2:0 is not the pair-0 X bank saved before bridge-minus") + need(by_label["bridge_minus:0"][2] == {} and by_label["bridge_minus:0"] != saved, + "bridge-minus did not delete the x1 monomial that the saved copy keeps") + + operator = algebra.add(algebra.one, algebra.neg(algebra.mul(c1, q, c1))) + need(operator == algebra.add(algebra.term((), (0, 0)), + algebra.neg(algebra.term((2, 1, 2), (0, 0)))), + "named operator is not I - C1 Q C1") + need(len(operator) == 2, "named operator does not have exactly two monomials") + inverse = algebra.inv(saved[1]) + need(algebra.mul(rho[1], inverse) == operator, "y0 column does not force this operator") + need([algebra.mul(operator, column) for column in saved] == rho, + "named operator misses the required correction") + for term in operator: + partial = {term: operator[term]} + need([algebra.mul(partial, column) for column in saved] != rho, + "one monomial of the operator already corrected the row") + need(len(algebra.mul(partial, saved[1])) == 1, + "a monomial image on the unit column changed support size") + need(len(algebra.mul(operator, saved[1])) == len(operator) == len(rho[1]), + "left multiplication by the unit column did not preserve support size") + + identity = algebra.one + signed = algebra.neg(algebra.mul(c1, q, c1)) + identity_row = [algebra.mul(qi, identity, column) for column in saved] + signed_row = [algebra.mul(qi, signed, column) for column in saved] + need(identity_row[0] == {} and identity_row[3] == {}, "identity monomial touched x0 or y1") + need(signed_row[0] == {} and signed_row[3] == {}, "C1 Q C1 monomial touched x0 or y1") + need(identity_row[1] == algebra.neg(algebra.mul(qi, c1, q, d1)), + "identity monomial is not -Q^{-1} C1 Q D1 on y0") + need(identity_row[2] == algebra.mul(qi, d1), + "identity monomial is not Q^{-1} D1 on x1") + need(signed_row[1] == algebra.mul(qi, c1, q, q, d1), + "C1 Q C1 monomial is not Q^{-1} C1 Q^2 D1 on y0") + need(signed_row[2] == algebra.neg(algebra.mul(qi, c1, q, c1, d1)), + "C1 Q C1 monomial is not -Q^{-1} C1 Q C1 D1 on x1") + need(algebra.add(identity_row[1], signed_row[1]) == algebra.neg(coupling), + "the two y0 monomials do not sum to -B") + need(algebra.add(identity_row[2], signed_row[2]) == algebra.neg(extra), + "the two x1 monomials do not sum to -E") + need(identity_row != [{}, algebra.neg(coupling), algebra.neg(extra), {}], + "dropping C1 Q C1 still cleared both defects") + need(signed_row != [{}, algebra.neg(coupling), algebra.neg(extra), {}], + "dropping I still cleared both defects") + + inserted, inserted_final, _saved, _before = schedule( + algebra, published_f1, published_f2, insert=operator) + inserted_by = dict(inserted) + need(inserted_by["query4:3"] == autonomous, "insertion did not autonomize query4:3") + need(inserted_by["response2"] == by_label["response2"], + "insertion changed response2 or the published second operator") + for label in PRE_QUERY: + need(inserted_by[label] == by_label[label], "insertion rewrote a bank saved before the argument") + need(all(inserted_final[i] != targets[i] for i in range(4)), + "a final bank matched its uncoded target") + need(inserted_final != targets, "the suffix produced the four uncoded targets") + bare = [algebra.add(x, y) for x, y in zip(saved, [{}, {}, {}, {}])] + bare[2] = {} + need([algebra.mul(operator, column) for column in bare] != rho, + "the same operator worked after deleting the saved x1 monomial") + + groups = {"zero-column": [], "unit-kills": [], "unique-fails": [], "works": []} + for label in PRE_QUERY: + if label == "response2": + continue + kind, payload = classify(algebra, by_label[label], rho) + groups[kind].append(label) + if label == "bridge_query2:0": + need(kind == "works" and payload == operator, "witness was not the unique solution") + elif label in UNIQUE_FAILS: + need(kind == "unique-fails", "paired Y bank was not a unique failure") + failed_operator, image = payload + need(image[0] != {} and image[1] == rho[1] and image[2] == rho[2] and image[3] == {}, + "unique failure did not clear y0 and x1 while spoiling x0") + need(tuple(groups["zero-column"]) == ZERO_COLUMN, "zero-column census moved") + need(tuple(groups["unit-kills"]) == UNIT_KILLS, "unit-kill census moved") + need(tuple(groups["unique-fails"]) == UNIQUE_FAILS, "unique-failure census moved") + need(groups["works"] == ["bridge_query2:0"], "more than one legal saved bank worked") + need(len(groups["zero-column"]) + len(groups["unit-kills"]) + + len(groups["unique-fails"]) + len(groups["works"]) == 29, + "legal saved-bank census is not 29") + for label in UNIQUE_FAILS: + need(by_label[label] == by_label["bridge_query2:1"], + "the three pair-0 Y labels are not the same bank") + failed_operator = algebra.add(algebra.mul(c1, qi), algebra.neg(algebra.mul(c1, q, q))) + need(classify(algebra, by_label["bridge_query2:1"], rho)[1][0] == failed_operator, + "unique operator on the pair-0 Y bank moved") + spoiled = [algebra.mul(failed_operator, column) for column in by_label["bridge_query2:1"]] + need(spoiled[0] == algebra.add(algebra.neg(d1), algebra.mul(c1, q, q, c1, d1)), + "x0 image on the pair-0 Y bank is not -D1 + C1 Q^2 C1 D1") + + post_groups = {"zero-column": [], "unit-kills": [], "unique-fails": [], "works": []} + for label in POST_QUERY: + kind, _payload = classify(algebra, by_label[label], rho) + post_groups[kind].append(label) + need(tuple(post_groups["zero-column"]) == POST_ZERO, "post-query zero-column list moved") + need(tuple(post_groups["unit-kills"]) == POST_UNIT, "post-query unit-kill list moved") + need(tuple(post_groups["unique-fails"]) == POST_UNIQUE_FAILS, "post-query unique-failure list moved") + need(post_groups["works"] == [], "a bank recorded at or after response4 corrected the row") + + response = by_label["response2"] + need(len(response[0]) == 1, "response2 x0 column is not a unit") + need(algebra.mul(response[0], algebra.inv(response[0])) == algebra.one, + "response2 x0 column lost its inverse") + kind, _payload = classify(algebra, response, rho) + need(kind == "unit-kills", "an extra operator on response2 could preserve x0") + + ledger = { + "scalar_adds": 2 * C1_ADDS + 2 * BANK_ADDS, + "monomial_passes": 2 * C1_MONOMIALS + 1 * MONOMIAL_PASS, + "mode_clears": 2 * C1_CLEARS, + "copies": 1 * BANK_COPYS, + "extra_fields": 2 * BANK_COPYS, + "mode_fields_reused": 8, + "gaussian_children": 0, + } + need(ledger == { + "scalar_adds": 2016, + "monomial_passes": 560, + "mode_clears": 32, + "copies": 112, + "extra_fields": 224, + "mode_fields_reused": 8, + "gaussian_children": 0, + }, "ledger arithmetic moved") + print("PASS_SAVED_BANK_QUERY_SOURCE") + print("saved_bank", "bridge_query2:0") + print("operator", "I - C1 Q C1") + print("second_operator", "C1 Q^2") + print("row_autonomous", True) + print("legal_banks_tested", 29) + print("legal_banks_that_work", 1) + print("post_query_banks_that_work", 0) + print("ledger", ledger) + print("new_kappa", None) + + +if __name__ == "__main__": + main()