From e7072eaa9c4a4ba0cca40705428959137828331b Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Tue, 10 Nov 2026 09:59:00 +0000 Subject: [PATCH] Record the ordinary bill of the witness F1=Q, F2=C1 Q On the published owned bank, this pair pays 112 monomial passes more than I and C1 Q^2. The existing scalar suffix is a signed permutation and clears no final bank. No kappa change. Co-authored-by: unpaidmoon --- research/two-edge-witness-bill/PROOF.md | 214 ++++++++++++++ research/two-edge-witness-bill/README.md | 132 +++++++++ research/two-edge-witness-bill/SOURCES.json | 30 ++ research/two-edge-witness-bill/TASK.json | 90 ++++++ research/two-edge-witness-bill/VERIFY.json | 37 +++ research/two-edge-witness-bill/verify.py | 296 ++++++++++++++++++++ 6 files changed, 799 insertions(+) create mode 100644 research/two-edge-witness-bill/PROOF.md create mode 100644 research/two-edge-witness-bill/README.md create mode 100644 research/two-edge-witness-bill/SOURCES.json create mode 100644 research/two-edge-witness-bill/TASK.json create mode 100644 research/two-edge-witness-bill/VERIFY.json create mode 100644 research/two-edge-witness-bill/verify.py diff --git a/research/two-edge-witness-bill/PROOF.md b/research/two-edge-witness-bill/PROOF.md new file mode 100644 index 0000000000..f7cd534df6 --- /dev/null +++ b/research/two-edge-witness-bill/PROOF.md @@ -0,0 +1,214 @@ +# Ordinary bill of the witness `F1 = Q`, `F2 = C1 Q` + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. + +No new κ is claimed. The selected frontier is unchanged. No call is added. + +## The pair and the owned bank + +The published feed in +[research/coded-active-feedback](../coded-active-feedback/PROOF.md) saves the +first FULL output `h`, adds `I · h` into query 2, and adds `C1 Q^2` times +that response into query 4. One extra owned 112-field bank holds `h` and is +later reset and reused for the response. The witness uses that same bank +and the same two insertion points. It replaces the two operators by +`F1 = Q` and `F2 = C1 Q`. Both lie outside the 8,281-policy family. First-edge choices are scalars +times alternating `C1`/`C3` words, and `Q` is not one of those words. +Every nonzero second-edge choice ends in `Q^2`, and `C1 Q` does not. This +note does not re-prove the one-edge obstruction. It prices this pair. + +Rightmost operators act first. `Q^4 = I`, `C1^2 = C3^2 = I`, and each `D` +commutes with `Q` and with the other `D`, while `D_s` conjugates only `C_s` +by `Q^{-1}`. The verifier checks the four conjugations below. + +## While the bank holds `h` + +The pinned replay, and the conjugations just named, give the saved bank + +```text +h = [Q^{-1} C1 D1, D1, -Q^{-1} C1 D1, 0] +``` + +and the pair-0 X bank at query 2 + +```text +X = [0, -C1 Q D1, D1, 0]. +``` + +`I` leaves `h` unchanged. Left multiplication by `Q` cancels the leading +`Q^{-1}` on the two `C1` columns: + +```text +Q h = [C1 D1, Q D1, -C1 D1, 0]. +``` + +The two images differ on `x0`, `y0`, and `x1`. The query-2 arguments are +`C1 X + F1 h`. + +```text +C1 X + h = [Q^{-1} C1 D1, D1 - Q D1, C1 D1 - Q^{-1} C1 D1, 0] +C1 X + Q h = [C1 D1, 0, 0, 0]. +``` + +The two cancelled columns are the identities `C1(-C1 Q D1) + Q D1 = 0` and +`C1 D1 + Q(-Q^{-1} C1 D1) = 0`. The witness argument is one monomial. The +published argument is not. The paid response is `Q^{-1}` times the +argument, so the witness writes + +```text +r2 = [Q^{-1} C1 D1, 0, 0, 0] +``` + +into the reused bank. The published response, on this same bank after +`F1 = I`, is + +```text +[Q^2 C1 D1, -D1 + Q^{-1} D1, Q^{-1} C1 D1 - Q^2 C1 D1, 0]. +``` + +## While the bank holds the response + +On the witness response, + +```text +C1 Q · r2 = [D1, 0, 0, 0] +C1 Q^2 · r2 = [C1 Q C1 D1, 0, 0, 0]. +``` + +Only the witness operator returns `D1`. On the published response the same +two operators differ on `x0`, `y0`, and `x1`. The predecessor identity +`query4:3 = [0, 0, X1, 0] + Q^{-1} F2 r2`, with +`X1 = Q^{-1} C3 D1 D3`, therefore gives the autonomous row + +```text +[D1 Q^{-1}, 0, X1, 0] +``` + +for this pair and not for `C1 Q^2` on the same `r2`. The query adds that +response into bank 1. Bank 1 still holds `h`, whose `x0` column equals +`r2`, so the sum is + +```text +[2 Q^{-1} C1 D1, D1, -Q^{-1} C1 D1, 0]. +``` + +The coefficient `2` is that sum. It is not a second addition and not a +second owned bank. + +## Ordinary bill + +The ledger uses the predecessor's published units: one F-transpose is +896 scalar ADDs, 224 monomial passes and 16 mode CLEARs; one 112-field +addition is 112 ADDs; one capture is 112 COPYs; one reset of the saved +bank is 112 field resets; one uniform power of `Q` or `Q^2` is 112 +monomial passes. `Q` overwrites the saved copy of `h` before that copy is +added. The schedule does not read the unmultiplied copy again, so no third +capture is charged. Zero columns are not discounted. Maps are not fused. + +| Added operation | Published `I`, `C1 Q^2` | Witness `Q`, `C1 Q` | +| --- | ---: | ---: | +| Two feedback additions | 224 ADDs | 224 ADDs | +| One F-transpose, the `C1` in `F2` | 896 ADDs, 224 monomials, 16 CLEARs | same | +| Monomial on saved `h` | none (`I`) | `Q`: 112 monomials | +| Monomial on the saved response | `Q^2`: 112 monomials | `Q`: 112 monomials | +| Captures of `h` and `r2` | 224 COPYs | 224 COPYs | +| Initial, intermediate and final reset | 336 resets | 336 resets | +| Extra owned capacity | 112 fields and 8 modes | same | +| Gaussian children | 0 | 0 under this unit | + +The witness therefore pays 1120 scalar ADDs, 448 monomial passes, 16 mode +CLEARs, 224 COPYs and 336 resets. The published feed pays the same totals +except 336 monomial passes. The difference is one `Q` on `h`. The response +line changes from `Q^2` to `Q` and keeps the count 112. + +This is an upper bound for that circuit under those units. It is not a +minimum, not a tape cost, and not a new κ. The same unit was used for `Q` +and `Q^{-1}` in +[research/owner-indexed-y0-clearance](../owner-indexed-y0-clearance/PROOF.md), +which left the primitive open. If one power of `Q` is a Gaussian child, or +must be expanded before it is a monomial pass, the witness line +"Gaussian children: 0" is false and 448 undercounts. That alternative is +not settled here. + +## The scalar suffix + +After query 4 the schedule executes only the existing scalar suffix: +add bank 0 into bank 2, subtract bank 3 from bank 1, swap banks 0 with 1 +and 2 with 3 while negating the outgoing banks, then add bank 2 into bank 0 +and subtract bank 1 from bank 3. For arbitrary banks `A, B, C, D` the +composition is + +```text +final = (B, -A, D, -C). +``` + +The bridge terms cancel for every content. The suffix is a signed +permutation of the four query-4 banks. It clears a final bank to a target +only when the corresponding preimage is already that signed target. It +does not multiply by `Q`, `C1`, or `C3`, and it does not cancel a nonzero +column against a different column. + +The witness preimages are bank 1 after the response sum, the pure y0 row +`[0, -C1 Q D1, 0, 0]`, the autonomous row, and the FULL3 X bank. None is +the signed uncoded target. The final banks are therefore + +```text +bank 0 = [2 Q^{-1} C1 D1, D1, -Q^{-1} C1 D1, 0] +bank 1 = [0, C1 Q D1, 0, 0] +bank 2 = [D1 Q^{-1}, 0, Q^{-1} C3 D1 D3, 0] +bank 3 = [C3 C1 D1 D3, C3 Q D1 D3, -D1 D3, C3 Q D1 D3]. +``` + +Bank 1 is the same pure y0 monomial as in the published feed. Bank 2 is +the autonomous row, so its y0 and y1 are zero and its x0 and x1 are not. +Bank 0 has three nonzero columns, and its x0 coefficient is 2. Bank 3 has +four nonzero columns, with `y0 = y1 = C3 Q D1 D3`. The uncoded targets are +`D1 Q^{-1}`, `D1 Q`, `D1 D3 Q^{-1}`, and `D1 D3 Q` on the diagonal. No +final bank equals its target. + +The FULL3 shape of bank 3 is the same conjugation family. Before the left +`D3`, bank 2 is `-Q C3` times the post-bridge bank 3, plus the carried +`D1` on x1. Then + +```text +D3 Q C3 D1 = C3 Q D1 D3 +D3 Q C3 Q^{-1} C1 D1 = C3 C1 D1 D3, +``` + +and `D3` commutes with `D1`. Negating that bank is final bank 3. + +Halving bank 0 does not produce target 0. Left multiplication of bank 3 by +`C3` turns y1 into `Q D1 D3` and also turns y0 into that same monomial, so +it is not target 3. Neither operation is part of the suffix. + +## No word-free combination hits a target + +A rational linear combination of the four final banks, with no extra +monomial, is the largest word-free scalar operation on these banks. It +still uses no new call. The target monomials are disjoint from this +support, except for one inseparable pair: + +- Target 0 is the single key `Q^{-1}` on x0 at D-exponent `(1, 0)`. That + key occurs only as bank 2's x0 column. Bank 2's x1 column is + `Q^{-1} C3 D1 D3`, and that key occurs nowhere else. The coefficient + that copies target 0 also copies the x1 monomial. +- Target 1 is `Q` on y0 at D-exponent `(1, 0)`. No final column contains + that key. +- Target 2 is `Q^{-1}` on x1 at D-exponent `(1, 1)`. No final column + contains that key. +- Target 3 is `Q` on y1 at D-exponent `(1, 1)`. No final column contains + that key. Bank 3's y1 key is `C3 Q`, not `Q`. + +The domain of this statement is these four banks and these four targets. +Every one of the sixteen columns was inspected for each key. This is not +a census of feedback pairs, and it does not forbid a monomial multiplier +or a read of an earlier bank. + +## What is not proved + +The witness is one pair. The formal algebra is the predecessor's sufficient +identity model. A quotient that collapses one of these words could make the +same banks look cheaper; no such quotient is proved here. Native tape, +precision, compiler, and outer costs are not repriced. The x1 block of the +published feed and a saved-bank source other than this response are not +taken. The selected conditional κ, `781451/250000000`, is not changed. diff --git a/research/two-edge-witness-bill/README.md b/research/two-edge-witness-bill/README.md new file mode 100644 index 0000000000..0cfafb1c9e --- /dev/null +++ b/research/two-edge-witness-bill/README.md @@ -0,0 +1,132 @@ +# The two-edge witness pays 112 extra monomial passes, and the scalar suffix clears no final bank + +**Scoped bill and suffix identity; no new κ.** On the one reused owned +bank of +[research/coded-active-feedback](../coded-active-feedback/README.md), the +witness `F1 = Q`, `F2 = C1 Q` replaces the published `I` and `C1 Q^2`. +Under the predecessor's uniform field units the witness pays one extra +`Q` on the saved FULL output, 112 monomial passes, and changes the +response monomial from `Q^2` to `Q` at the same 112-pass count. The +existing scalar suffix is a signed permutation of the four query-4 banks. +It clears none of them to an uncoded target. Final banks 0 and 3 stay the +explicit nonzero rows below. + +The selected frontier is unchanged. This does not re-prove the one-edge +coupling of +[research/active-feedback-outside-edge](../active-feedback-outside-edge/README.md). + +## Result + +`Q` and `I` disagree on three columns of the common saved bank + +```text +h = [Q^{-1} C1 D1, D1, -Q^{-1} C1 D1, 0]. +``` + +`Q h` cancels the query-2 argument down to the single monomial `C1 D1`. +`C1 Q` then returns `D1` on that response. `C1 Q^2` on the same response +returns `C1 Q C1 D1`. + +The additional ledger, with each uniform power charged as 112 monomial +passes, is 1120 scalar ADDs, 448 monomial passes, 16 mode CLEARs, 224 +COPYs, 336 resets, 112 owned fields and 8 reused mode fields. The +published feed pays 336 monomial passes and the same other totals. No +Gaussian child is charged while `Q` uses that monomial unit. The unit is +not a tape proof. + +After query 4 the suffix sends banks `(A, B, C, D)` to `(B, -A, D, -C)`. +The witness finals are + +```text +bank 0 = [2 Q^{-1} C1 D1, D1, -Q^{-1} C1 D1, 0] +bank 1 = [0, C1 Q D1, 0, 0] +bank 2 = [D1 Q^{-1}, 0, Q^{-1} C3 D1 D3, 0] +bank 3 = [C3 C1 D1 D3, C3 Q D1 D3, -D1 D3, C3 Q D1 D3]. +``` + +Bank 1 matches the published pure y0 monomial. Banks 0 and 3 do not match +the published feed or their uncoded targets. No rational word-free +combination of these four banks hits any of the four targets: the only +target monomial present is bank 2's restored `D1 Q^{-1}`, and it is tied +to the x1 monomial `Q^{-1} C3 D1 D3`. [PROOF.md](PROOF.md) gives the +cancellations, the ledger, and the support check. + +Evidence class: the operator comparison, the suffix identity, and the four +final rows are proofs in the predecessor's formal algebra. The word-free +miss is a complete support check of these sixteen columns, not a search +and not a census of other pairs. The ledger is an upper bound under +inherited units. + +## Reproduce + +From the repository root, Python 3.12, standard library only: + +```sh +python3 -B scripts/research_package.py --package research/two-edge-witness-bill --check-only +python3 -B scripts/research_package.py --package research/two-edge-witness-bill +``` + +Direct replay: + +```sh +python3 -I -W error -B research/two-edge-witness-bill/verify.py +python3 -I -O -W error -B research/two-edge-witness-bill/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 add a call. It takes the first +open question of +[research/active-feedback-outside-edge](../active-feedback-outside-edge/README.md): +compare `Q` and `C1 Q` with the published `I` and `C1 Q^2` on the same +owned bank, then read final banks 0 and 3. + +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. + +Local overlap at this base found the witness named only as that open +question. The one-edge theorem, the owner-indexed y0 charge, and the +owner-indexed x1 obstruction are different objects and are not redone. + +## Open next questions + +Does one source monomial primitive implement a single power of `Q` at the +same 112-pass unit as `Q^2`? The witness bill charges two such powers, one +on `h` and one on the response, and its zero Gaussian-child line is false +if either power is a Gaussian child. The first step is to bind that +primitive for one `Q` on one 112-field bank and reprice those two lines. +No native word is replayed here. This is the primitive left open by the +owner-indexed y0 charge, now used twice. + +Can one charged monomial, still with no new call, turn final bank 0 or +final bank 3 into its uncoded target while bank 2 stays the autonomous +row? Word-free rational combinations cannot. The first step is one left +monomial on bank 0 or bank 3, charged at 112 passes, checked against that +target and against bank 2. This is not the published-feed x1 owner index +and not a new saved-bank source. + +## Credit + +The schedule, algebra, owned-bank lifetime, and field units 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`. The witness pair and the one-edge +identities are +[research/active-feedback-outside-edge](../active-feedback-outside-edge/README.md). +The monomial unit for one power of `Q` is the convention in +[research/owner-indexed-y0-clearance](../owner-indexed-y0-clearance/README.md), +whose primitive question stays open. New work is the owned-bank comparison, +the witness ledger, the suffix identity, and the support check for banks +0 and 3. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. +Apache-2.0. diff --git a/research/two-edge-witness-bill/SOURCES.json b/research/two-edge-witness-bill/SOURCES.json new file mode 100644 index 0000000000..8bba455056 --- /dev/null +++ b/research/two-edge-witness-bill/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/two-edge-witness-bill/TASK.json b/research/two-edge-witness-bill/TASK.json new file mode 100644 index 0000000000..5cb0b0b5de --- /dev/null +++ b/research/two-edge-witness-bill/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": "Price the two-edge witness F1=Q, F2=C1 Q against the published I and C1 Q^2 on the same owned bank, and read which final banks the existing scalar suffix clears, before adding a call.", + "scope_change_reason": "The card asks whether a changed caller removes real work. This note does not change the query demand. It prices the boundary witness left by research/active-feedback-outside-edge and reads final banks 0 and 3. It does not add a call and does not change kappa.", + "bottleneck_link": "That pair makes one row autonomous only by changing both edges. Its ordinary bill, and whether the existing suffix clears a final bank, decide whether the row is a caller. The published feed remains the coupled component.", + "budget_minutes": 60, + "stop_rule": "Stop after the owned-bank comparison, the field ledger, the suffix identity, and the word-free support check of the four final banks. Do not add a call, bind a native Q primitive, or take the x1-block or alternate saved-bank questions.", + "outcome": "negative-result", + "evidence": "PROOF.md and verify.py", + "author": "unpaidmoon, with substantial Cursor Grok assistance", + "ai_assistance": "Substantial Cursor Grok assistance; no subagents.", + "open_questions": [ + { + "question": "Does one source monomial primitive implement a single power of Q at the same 112-pass unit as Q^2?", + "why_it_matters": "The witness ledger charges two such powers and reports zero Gaussian children only under that unit.", + "first_step": "Bind the primitive for one Q on one 112-field bank and reprice the saved-h line and the response line.", + "blocked_by": "No native word is replayed here." + }, + { + "question": "Can one charged monomial, still with no new call, turn final bank 0 or final bank 3 into its uncoded target while bank 2 stays the autonomous row?", + "why_it_matters": "Word-free rational combinations miss every target, so a repair has to introduce a monomial the suffix does not have.", + "first_step": "Apply one left monomial to bank 0 or bank 3, charge it at 112 passes, and compare that image with the target and with bank 2.", + "blocked_by": "No such monomial is constructed here." + } + ] +} diff --git a/research/two-edge-witness-bill/VERIFY.json b/research/two-edge-witness-bill/VERIFY.json new file mode 100644 index 0000000000..e4b45c4a2b --- /dev/null +++ b/research/two-edge-witness-bill/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, owned-bank images of I versus Q and of C1 Q^2 versus C1 Q, the witness ledger totals, the scalar-suffix permutation, final banks 0 and 3, and the word-free support obstruction." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same bill and suffix checks under optimization. Checks are explicit failures, not assertions." + } + ] +} diff --git a/research/two-edge-witness-bill/verify.py b/research/two-edge-witness-bill/verify.py new file mode 100644 index 0000000000..09034c9172 --- /dev/null +++ b/research/two-edge-witness-bill/verify.py @@ -0,0 +1,296 @@ +#!/usr/bin/env python3 +"""Ordinary bill of the two-edge witness F1=Q, F2=C1 Q. + +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 field ledger uses the predecessor's uniform monomial unit. +""" +from fractions import Fraction +from hashlib import sha256 +import importlib.util +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent +COEFFICIENTS = ("-2", "-1", "-1/2", "1/2", "1", "2") +# Inherited field units from research/coded-active-feedback/PROOF.md. +BANK = 112 +C1_ADDS = 896 +C1_MONOMIALS = 224 +C1_CLEARS = 16 +MODES = 8 + + +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 family_operators(algebra, search, second_edge): + operators = [{}] + for word in search.words(7): + for coefficient in COEFFICIENTS: + body = tuple(word) + ((1, 1) if second_edge else ()) + operators.append(algebra.term(body, (0, 0), coefficient)) + need(len(operators) == len({tuple(sorted(item.items())) for item in operators}) == 91, + "policy edge did not produce 91 operators") + return operators + + +def key_of(monomial): + need(len(monomial) == 1, "expected one monomial") + ((word, degree), value), = monomial.items() + need(value == 1, "expected a unit monomial") + return (word, degree) + + +def occurrences(rows, key): + found = [] + for bank, row in enumerate(rows): + for column, entry in enumerate(row): + if entry.get(key, 0): + found.append((bank, column, entry[key])) + return found + + +def scalar_suffix(algebra, rows): + """The four scalar steps search.replay runs after query 4.""" + out = [list(row) for row in rows] + + def plus(dst, src, sign): + op = algebra.term((), (0, 0), sign) + out[dst] = [algebra.add(x, algebra.mul(op, y)) + for x, y in zip(out[dst], out[src])] + + plus(2, 0, 1) + plus(1, 3, -1) + out[0], out[1] = out[1], [algebra.neg(entry) for entry in out[0]] + out[2], out[3] = out[3], [algebra.neg(entry) for entry in out[2]] + plus(0, 2, 1) + plus(3, 1, -1) + return out + + +def signed_permutation(algebra, rows): + return [ + list(rows[1]), + [algebra.neg(entry) for entry in rows[0]], + list(rows[3]), + [algebra.neg(entry) for entry in rows[2]], + ] + + +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, c3 = algebra.gen(1), algebra.gen(2), algebra.gen(3) + qi, d1, d3 = algebra.inv(q), algebra.D(0), algebra.D(1) + two = algebra.term((), (0, 0), 2) + published_f1, published_f2 = algebra.one, algebra.mul(c1, q, q) + witness_f1, witness_f2 = q, algebra.mul(c1, q) + need(witness_f1 == algebra.term((1,), (0, 0)), "F1 is not Q") + need(witness_f2 == algebra.term((2, 1), (0, 0)), "F2 is not C1 Q") + need(published_f2 == algebra.term((2, 1, 1), (0, 0)), "published F2 is not C1 Q^2") + first_family = family_operators(algebra, search, False) + second_family = family_operators(algebra, search, True) + need(published_f1 in first_family and published_f2 in second_family, + "published edges fell outside the 8,281-policy family") + need(witness_f1 not in first_family and witness_f2 not in second_family, + "the two-edge witness is inside the 8,281-policy family") + + # Conjugations used to move D through the saved banks. + need(algebra.mul(d1, q, c1) == algebra.mul(c1, q, d1), "FULL1 X conjugation changed") + need(algebra.mul(d1, c1, qi) == algebra.mul(qi, c1, d1), "saved h conjugation changed") + need(algebra.mul(d3, q, c3, d1) == algebra.mul(c3, q, d1, d3), + "FULL3 y conjugation changed") + need(algebra.mul(d3, q, c3, qi, c1, d1) == algebra.mul(c3, c1, d1, d3), + "FULL3 x0 conjugation changed") + need(algebra.mul(d1, d3) == algebra.mul(d3, d1), "D1 and D3 no longer commute") + + h = [algebra.mul(qi, c1, d1), d1, algebra.neg(algebra.mul(qi, c1, d1)), {}] + qh = [algebra.mul(c1, d1), algebra.mul(q, d1), algebra.neg(algebra.mul(c1, d1)), {}] + x_at = [{}, algebra.neg(algebra.mul(c1, q, d1)), d1, {}] + need([algebra.mul(q, entry) for entry in h] == qh, "Q h moved") + need(qh != h, "Q and I agree on the saved FULL1 Y bank") + need([qh[j] != h[j] for j in range(4)] == [True, True, True, False], + "Q h should differ on x0, y0 and x1 only") + witness_argument = [algebra.add(algebra.mul(c1, x), algebra.mul(q, y)) + for x, y in zip(x_at, h)] + published_argument = [algebra.add(algebra.mul(c1, x), y) for x, y in zip(x_at, h)] + need(witness_argument == [algebra.mul(c1, d1), {}, {}, {}], + "Q on h did not cancel the query-2 argument down to C1 D1") + need(published_argument != witness_argument, "I on h produced the witness argument") + need(published_argument[1] != {} and published_argument[2] != {}, + "the published argument lost a column") + witness_response = [algebra.mul(qi, entry) for entry in witness_argument] + need(witness_response == [algebra.mul(qi, c1, d1), {}, {}, {}], + "witness response2 is not the single monomial Q^{-1} C1 D1") + need(algebra.mul(witness_f2, witness_response[0]) == d1, "C1 Q did not return D1") + need([algebra.mul(witness_f2, entry) for entry in witness_response] == [d1, {}, {}, {}], + "C1 Q on the witness response is not pure D1") + other = algebra.mul(published_f2, witness_response[0]) + need(other == algebra.mul(c1, q, c1, d1) and other != d1, + "C1 Q^2 on the same witness response should stay off D1") + + published_observed, targets, published_final = search.replay( + algebra, published_f1, published_f2) + witness_observed, witness_targets, witness_final = search.replay( + algebra, witness_f1, witness_f2) + need(witness_targets == targets, "uncoded targets moved between replays") + published_by = dict(published_observed) + witness_by = dict(witness_observed) + need(witness_by["FULL1:1"] == published_by["FULL1:1"] == h, + "saved h is not the common FULL1 Y bank") + need(witness_by["bridge_query2:0"] == x_at, "query-2 X bank moved") + need(witness_by["response2"] == witness_response, "replayed witness response moved") + published_response = [ + algebra.mul(q, q, c1, d1), + algebra.add(algebra.neg(d1), algebra.mul(qi, d1)), + algebra.add(algebra.mul(qi, c1, d1), algebra.neg(algebra.mul(q, q, c1, d1))), + {}, + ] + need(published_by["response2"] == published_response, "published response2 moved") + published_images = ( + [algebra.mul(published_f2, entry) for entry in published_response], + [algebra.mul(witness_f2, entry) for entry in published_response], + ) + need(published_images[0] != published_images[1], + "C1 Q^2 and C1 Q agree on the published response") + need([published_images[0][j] != published_images[1][j] for j in range(3)], + "the two second-edge operators should differ on three published columns") + need(witness_by["response2"] != published_response, + "changing F1 left the owned response unchanged") + + autonomous = [algebra.mul(d1, qi), {}, algebra.mul(qi, c3, d1, d3), {}] + need(witness_by["query4:3"] == autonomous, "witness query-4 row is not autonomous") + need(witness_by["query4:0"] == [{}, algebra.neg(algebra.mul(c1, q, d1)), {}, {}], + "query-4 bank 0 is not the pure negative y0 monomial") + bank0 = [ + algebra.mul(two, qi, c1, d1), + d1, + algebra.neg(algebra.mul(qi, c1, d1)), + {}, + ] + bank3 = [ + algebra.mul(c3, c1, d1, d3), + algebra.mul(c3, q, d1, d3), + algebra.neg(algebra.mul(d1, d3)), + algebra.mul(c3, q, d1, d3), + ] + bank1 = [{}, algebra.mul(c1, q, d1), {}, {}] + need(list(bank0[0].values()) == [Fraction(2)], "bank 0 x0 coefficient is not 2") + need(witness_final[0] == bank0, "final bank 0 moved") + need(witness_final[3] == bank3, "final bank 3 moved") + need(witness_final[1] == published_final[1] == bank1, + "final bank 1 is no longer the published pure y0 monomial") + need(witness_final[2] == autonomous, "final bank 2 is not the autonomous row") + need(bank3[1] == bank3[3], "final bank 3 should keep equal y0 and y1 monomials") + need(all(witness_final[i] != targets[i] for i in range(4)), + "a witness final bank matched its uncoded target") + need(witness_final[0] != published_final[0] and witness_final[3] != published_final[3], + "banks 0 and 3 accidentally matched the published feed") + + # The suffix is a signed permutation for every content. It clears a final + # bank only by relocating a preimage that is already the signed target. + query4 = [witness_by["query4:" + str(i)] for i in range(4)] + need(signed_permutation(algebra, query4) == witness_final, "witness suffix moved") + need(scalar_suffix(algebra, query4) == witness_final, "suffix steps disagree") + for label, feedback1, feedback2 in ( + ("published", published_f1, published_f2), + ("empty", {}, {}), + ("first-only", witness_f1, {}), + ): + observed, _, final = search.replay(algebra, feedback1, feedback2) + by_label = dict(observed) + preimage = [by_label["query4:" + str(i)] for i in range(4)] + need(scalar_suffix(algebra, preimage) == signed_permutation(algebra, preimage) == final, + "suffix identity failed for " + label) + separating = [] + power = 0 + base = algebra.D(0) + degree = algebra.one + for _bank in range(4): + row = [] + for _column in range(4): + power += 1 + degree = algebra.mul(degree, base) + row.append(degree) + separating.append(row) + permuted = signed_permutation(algebra, separating) + need(scalar_suffix(algebra, separating) == permuted, "separating suffix fixture moved") + need(permuted != separating, "separating fixture was already a fixed point") + signed_targets = [ + targets[1], + [algebra.neg(entry) for entry in targets[0]], + targets[3], + [algebra.neg(entry) for entry in targets[2]], + ] + need(all(query4[i] != signed_targets[i] for i in range(4)), + "a query-4 preimage was already the signed target its final bank needs") + + # Word-free rational combinations of these four banks. Each target monomial + # is absent, or it occurs in exactly one column together with a second + # monomial that no other column carries. + pure_q_inverse = key_of(algebra.mul(d1, qi)) + dragged = key_of(algebra.mul(qi, c3, d1, d3)) + pure_q = key_of(algebra.mul(d1, q)) + degree_11_q_inverse = key_of(algebra.mul(d3, d1, qi)) + degree_11_q = key_of(algebra.mul(d3, d1, q)) + need(occurrences(witness_final, pure_q_inverse) == [(2, 0, Fraction(1))], + "target-0 monomial is not isolated on bank 2") + need(occurrences(witness_final, dragged) == [(2, 2, Fraction(1))], + "the autonomous x1 monomial is not isolated on bank 2") + for key, name in ( + (pure_q, "target 1"), + (degree_11_q_inverse, "target 2"), + (degree_11_q, "target 3"), + ): + need(occurrences(witness_final, key) == [], name + " monomial appeared") + half = algebra.term((), (0, 0), Fraction(1, 2)) + need([algebra.mul(half, entry) for entry in bank0] != targets[0], + "halving bank 0 produced target 0") + need([algebra.mul(c3, entry) for entry in bank3] != targets[3], + "one C3 on bank 3 produced target 3") + + # Same owned-bank lifetime as the published component. Q overwrites the + # saved copy of h; that copy is not read again. No zero column is discounted. + witness_monomials = C1_MONOMIALS + BANK + BANK + published_monomials = C1_MONOMIALS + BANK + witness_adds = 2 * BANK + C1_ADDS + need(witness_monomials == 448 and published_monomials == 336, "monomial totals moved") + need(witness_monomials - published_monomials == BANK, "the bill delta is not one Q on h") + need(witness_adds == 1120, "scalar ADD total moved") + need(2 * BANK == 224 and 3 * BANK == 336, "copy and reset totals moved") + need(C1_CLEARS == 16 and MODES == 8 and BANK == 112, "inherited units moved") + print("PASS_TWO_EDGE_WITNESS_BILL") + print("owned_bank_delta", "one extra Q on saved h; response monomial Q^2 replaced by Q") + print("monomial_passes", witness_monomials) + print("published_monomial_passes", published_monomials) + print("scalar_adds", witness_adds) + print("mode_clears", C1_CLEARS) + print("copies", 2 * BANK) + print("resets", 3 * BANK) + print("gaussian_children_under_monomial_unit", 0) + print("final_banks_cleared_by_scalar_suffix", "none") + print("word_free_target_hits", 0) + print("new_kappa", None) + + +if __name__ == "__main__": + main()