From 441e09b911157aef60ee249b1c1c03d86d68529d Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Tue, 10 Nov 2026 02:07:07 +0000 Subject: [PATCH] Record the owner-indexed y0 defect and its monomial charge On the published two-edge feed, every D-exponent-0 owner index that keeps D1 Q^{-1} and clears y0 pays the same two monomials. The constant-index fresh image leaves the four final banks stored and leaves the x1 block unpaid. No new kappa. Co-authored-by: unpaidmoon --- research/owner-indexed-y0-clearance/PROOF.md | 183 ++++++++++++++++ research/owner-indexed-y0-clearance/README.md | 118 +++++++++++ .../owner-indexed-y0-clearance/SOURCES.json | 30 +++ research/owner-indexed-y0-clearance/TASK.json | 90 ++++++++ .../owner-indexed-y0-clearance/VERIFY.json | 37 ++++ research/owner-indexed-y0-clearance/verify.py | 195 ++++++++++++++++++ 6 files changed, 653 insertions(+) create mode 100644 research/owner-indexed-y0-clearance/PROOF.md create mode 100644 research/owner-indexed-y0-clearance/README.md create mode 100644 research/owner-indexed-y0-clearance/SOURCES.json create mode 100644 research/owner-indexed-y0-clearance/TASK.json create mode 100644 research/owner-indexed-y0-clearance/VERIFY.json create mode 100644 research/owner-indexed-y0-clearance/verify.py diff --git a/research/owner-indexed-y0-clearance/PROOF.md b/research/owner-indexed-y0-clearance/PROOF.md new file mode 100644 index 0000000000..922234def0 --- /dev/null +++ b/research/owner-indexed-y0-clearance/PROOF.md @@ -0,0 +1,183 @@ +# An owner-indexed reading clears y0 and keeps the restored x0 block + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. + +No new κ is claimed. The selected frontier is unchanged. + +## Object + +Use the published two-edge feed in +[research/coded-active-feedback](../coded-active-feedback/PROOF.md). +After the left endpoint the replay stores four banks. Bank 2 carries the +restored coefficient + +```text +A = D1 Q^{-1} +``` + +together with the y0 coupling `B` and a three-term x1 block. Bank 1 is the +pure y0 monomial `G`. Banks 0 and 3 are the other endpoint banks. All four +are among the 39 saved banks. This note does not rerun the declared +alternating-family lock. + +An owner index assigns to every owner `o` and every final bank `b` a +D-exponent-0 element `m_{o,b}` of the predecessor's `Q, C1, C3` algebra. +The reading on that owner is the left combination of the four banks. It +does not mix owners. The published operators are owner-scalar: the +predecessor's coupling rank is `112` times a frequency factor. An arbitrary +input supported on one owner therefore forces the same operator equation +on that owner. Negative D exponents, owner-mixing maps, and a new feedback +edge are outside this statement. + +## Normal forms + +The pinned replay gives the D-exponent-0 quotients by the unit `A` + +```text +x = X0 A^{-1} = Q^{-1} C1 Q + Q^2 C1 Q +g = G A^{-1} = C1 Q^2 +b = B A^{-1} = Q^{-1} C1 Q^2 - Q^{-1} C1 Q^{-1} +``` + +with `X0` the x0 block of bank 0. Write `s = Q^{-1} C1 Q^2` and +`t = Q^{-1} C1 Q^{-1}`, so `b = s - t`. The four products are + +```text +(Q^{-1} C1 Q) s = Q +(Q^{-1} C1 Q) t = Q^2 +(Q^2 C1 Q) s = 1 +(Q^2 C1 Q) t = Q +``` + +using `Q^4 = 1` and `C1^2 = 1`. Hence + +```text +x b = (Q - Q^2) + (1 - Q) = 1 - Q^2. +``` + +Also `C1 g = Q^2`, so `x b - 1 = -C1 g` and `(x b - 1) g^{-1} = -C1`. +The inverse is `g^{-1} = Q^2 C1`, and + +```text +s g^{-1} = Q^{-1}, +t g^{-1} = Q^{-1} C1 Q C1, +b g^{-1} = Q^{-1} - Q^{-1} C1 Q C1. +``` + +The constant defect is therefore + +```text +const = -b g^{-1} = -Q^{-1} + Q^{-1} C1 Q C1 + = Q^{-1} (C1 Q C1 - I). +``` + +Both words are outside the short declared family of alternating `C1`/`C3` +words, with or without a right `Q^2`. The first word is not an even-Q word. +Let `E` be the span of normal forms whose every Q run has even exponent. +Products stay in `E`: adjacent even exponents add to an even exponent, and +reduction by `Q^4` subtracts a multiple of 4. `C1` lies in `E`, while +`const` does not, so `m0` and `m1` are never both in `E`. + +Bank 3's x0 and y0 columns are single monomials on D-exponent `(1, 1)`. +Left multiplication by a D-exponent-0 element preserves that line. The +target `A` has no D3 component, and a monomial has an inverse in this +algebra, so the bank-3 coefficient in any solution is 0. + +## The identity + +For an arbitrary D-exponent-0 element `m0`, set + +```text +m3 = 0 +m2 = 1 - m0 x +m1 = const - m0 C1. +``` + +Right-multiplying the x0 and y0 equations by `A^{-1}` reduces them to +`m0 x + m2 = 1` and `m0 + m1 g + m2 b = 0`. The second is the calculation +above. Equivalently, every solution satisfies + +```text +m1 + m0 C1 = const. +``` + +The two coefficients in `const` are `±1`. No choice of `m0`, and no choice +of owner, changes either coefficient in this combination. Choosing +`m0 = -Q^{-1} C1` moves the pure `Q^{-1}` term from `m1` into `m0`; the +combination is still `const`. This is an identity in the predecessor's +algebra, not a search over a bounded ansatz. In a quotient that identifies +further words, the image of this identity remains true, but a collapsed +word could make the same element look cheaper. No such quotient is proved +here. + +## The constant-index map + +Use the same multipliers on every owner: + +```text +m0 = 0, m1 = const, m2 = 1, m3 = 0. +``` + +Write them into a fresh image + +```text +S = bank 2 + const · bank 1. +``` + +Bank 1 has zero x0, x1, and y1, so + +```text +S_x0 = A, S_y0 = B + const · G = 0, S_y1 = 0, +``` + +and `S_x1` equals bank 2's x1 block. That block is the published coefficient + +```text +(Q^{-1} C1 Q C1 - Q^{-1}) D1 + Q^{-1} C3 D1 D3, +``` + +three monomials, none of them removed. The four stored endpoint banks are +only read. They stay equal to the replayed left endpoint. + +## Charge + +The algebraic charge is the pair of monomials in `const`, with coefficients +`-1` and `+1`, on every owner. The field ledger below is one circuit for +the constant-index choice. It is an upper bound for that circuit under the +predecessor's published units. It is not a minimum circuit cost, not a +tape proof, and not a new κ. + +The predecessor charges one F-transpose at 896 scalar ADDs, 224 monomial +passes and 16 mode CLEARs; one 112-field addition at 112 ADDs; one capture +at 112 COPYs; and one uniform `Q^2` at 112 monomial passes. This ledger +uses those units. Each of `Q` and `Q^{-1}` is charged as one uniform +monomial pass, the same unit as `Q^2`, because each is one monomial per +field. If `Q^{-1}` must be expanded as three factors, the monomial count +rises by 224 and this table is only a lower figure for that alternative. +That expansion is not established here. + +The factored circuit, overwriting scratch and keeping both sources stored, +is: + +| Step | Inherited unit | Count | +| --- | --- | ---: | +| Copy bank 1 into `U` | 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 ← V - U` | 112 scalar ADDs | 1 | +| `V ← Q^{-1} V` | 112 monomial passes | 1 | +| Copy bank 2 into `S` | 112 COPYs | 1 | +| `S ← S + V` | 112 scalar ADDs | 1 | + +The totals are 2016 scalar ADDs, 672 monomial passes, 32 mode CLEARs, +224 COPYs, 336 extra fields, and the predecessor's 8 mode fields reused. +No Gaussian child is added. Banks 0, 1, 2, and 3 are not written. + +## What is not proved + +The x1 block of `S` is unpaid. Owner-mixing maps, multipliers with a +nonzero D exponent, and a feedback edge outside the published two-edge +feed are not classified. The formal algebra is the predecessor's +sufficient identity model. Native tape, precision, compiler, and outer +costs are not repriced. The selected conditional κ is not changed. diff --git a/research/owner-indexed-y0-clearance/README.md b/research/owner-indexed-y0-clearance/README.md new file mode 100644 index 0000000000..533f786138 --- /dev/null +++ b/research/owner-indexed-y0-clearance/README.md @@ -0,0 +1,118 @@ +# Owner-indexed reading clears y0 and keeps x0 + +**Scoped identity and field ledger; no new κ.** On the published two-edge +feed, every owner-indexed D-exponent-0 left map of the four final banks +that keeps `x0 = D1 Q^{-1}` and clears y0 has the same defect + +```text +m1 + m0 C1 = -Q^{-1} + Q^{-1} C1 Q C1. +``` + +The constant index `m0 = 0`, `m1 = const`, `m2 = 1` writes that defect +into a fresh image. The four stored endpoint banks are not overwritten. +The image's x1 block is the published three-term coefficient and stays +unpaid. [PROOF.md](PROOF.md) gives the products and the circuit. + +The selected frontier is unchanged. This does not rerun the declared +alternating-family lock, and it does not test a new feedback edge. + +## Result + +The predecessor replay stores `A = D1 Q^{-1}` on final bank 2 together +with the y0 coupling, and stores a pure y0 monomial on final bank 1. +Right division by the unit `A` produces three D-exponent-0 elements +`x`, `g`, and `b`. Finite multiplication gives `x b = 1 - Q^2` and +`C1 g = Q^2`, so every D-exponent-0 coefficient `m0` determines + +```text +m3 = 0, m2 = 1 - m0 x, m1 = const - m0 C1, +const = Q^{-1}(C1 Q C1 - I). +``` + +Both coefficients in `const` are forced. Moving `Q^{-1}` into `m0` does +not delete it from the combination. The constant-index fresh image + +```text +S = bank 2 + const · bank 1 +``` + +has x0 block `A`, y0 block 0, and the original x1 block. Banks 0, 1, 2, +and 3 stay equal to the replayed left endpoint. + +One factored circuit, using the predecessor's published field units and +charging each of `Q` and `Q^{-1}` as one 112-field monomial pass, costs +2016 scalar ADDs, 672 monomial passes, 32 mode CLEARs, 224 COPYs, and +336 extra fields, with 8 mode fields reused and no new Gaussian child. +That count is an upper bound for this circuit. It is not a minimum and +not a tape proof. A three-factor reading of `Q^{-1}` is not settled. + +## Reproduce + +From the repository root, Python 3.12, standard library only: + +```sh +python3 -B scripts/research_package.py --package research/owner-indexed-y0-clearance --check-only +python3 -B scripts/research_package.py --package research/owner-indexed-y0-clearance +``` + +Direct replay: + +```sh +python3 -I -W error -B research/owner-indexed-y0-clearance/verify.py +python3 -I -O -W error -B research/owner-indexed-y0-clearance/verify.py +``` + +The optimized command still executes the checks. They are `need` failures, +not assertions. No network, native build, or full multiplier replay is used. + +## Scope + +Original card: `joint-query-controller`. Scope status: **refined**. The +card asks for one source-bound caller identity and its extra charges. +This package does not change the query demand. It takes the owner-indexed +remainder of handoff +[discussion comment 19138525](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19138525) +after [research/coded-active-feedback](../coded-active-feedback/README.md) +restored the missing coefficient. The declared-family obstruction is the +fork package behind draft PR 152; its census is not repeated. + +Base commit: `7c49fe32c55de02c2c873655c804b16e4c3fef0a`. Pins are in +[SOURCES.json](SOURCES.json). The catalogue and selected record are +provenance. `search.py` is a live input. The selected conditional value +used for orientation is the selected record, +`781451/250000000`, not the older decimal printed in the revision-8 +priority note. + +Local overlap at that commit searched the complete note inventory and +found no note containing both "owner-indexed" and "y0 coupling". The +remote overlap cache was absent. A live open-PR search for `y0` on +CrocSwap/integer-mult-bounds returned no pull requests. That search is +not a novelty certificate. + +## Open next questions + +Can a fresh image clear the three-term x1 block while keeping x0 equal +to `D1 Q^{-1}`, keeping y0 zero, and leaving the four final banks stored +unchanged? The y0 term is no longer the obstruction on this image. The +first step is the same four-bank equation on the x1 column, with every +new monomial charged. This package leaves the published x1 coefficient +in place. + +Does one inherited monomial pass implement `Q` and `Q^{-1}`, or must +`Q^{-1}` be expanded before the field ledger is a tape cost? The ledger +uses the predecessor's `Q^2` unit for each uniform power. The first step +is to bind the source monomial primitive for a single power of `Q`. No +native word is replayed here. + +## Credit + +The trace, algebra, and published row 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 one-point odd-Q correction from final bank 1, without +this owner-index identity or this charge, is the fork package +`research/active-feedback-coupling-lock`. The gauge engine remains the +inherited `research/coded-native-caller/gauge.py`. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. +Apache-2.0. diff --git a/research/owner-indexed-y0-clearance/SOURCES.json b/research/owner-indexed-y0-clearance/SOURCES.json new file mode 100644 index 0000000000..40f964f242 --- /dev/null +++ b/research/owner-indexed-y0-clearance/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/coded-active-feedback/search.py", + "usage": "input", + "git_blob": "60de5a87d3f64fc69e2595cdb2df771c91a0fe6e", + "sha256": "1383010827af29a1b0e595e2c1aa2ffad461b266ffc9f936efce1603ff9f5eb6" + }, + { + "path": "research/coded-native-caller/gauge.py", + "usage": "input", + "git_blob": "44ae72b314cccf677b44d75c374be6dcac1c8167", + "sha256": "390391d291353741c89daea999d483660ca185987ed96a15b82576280c487cad" + } + ] +} diff --git a/research/owner-indexed-y0-clearance/TASK.json b/research/owner-indexed-y0-clearance/TASK.json new file mode 100644 index 0000000000..e32c259eac --- /dev/null +++ b/research/owner-indexed-y0-clearance/TASK.json @@ -0,0 +1,90 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "joint-query-controller", + "question": "Can a changed query demand or caller remove real work while satisfying native chronology and restoration?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose an exact caller and a new demand/interface hypothesis. Read the scoped #5617/#5631/#5649/#5747 and #5720/#5745 objections before rebuilding an excluded schedule. Compare the complete matched source/consumer protocols including all retained helper outputs. For an active-mode injection, first check #5745: its canonical delivery claim repays the eight removed centre jobs. Audit that exact claim or change its channel/feedback hypothesis; do not repeat the same free-injection search. Stop if the full favorable budget fails or the required restored output is unobservable.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "query demand", + "active mode", + "5720", + "5745", + "5747", + "caller" + ], + "existing_checks": [ + { + "scope": "PR #4166: author-checked installed producer/service/return/bridge connection; native-component comparison loses.", + "evidence": "research/qq16-caller-install/README.md", + "remaining": "Complete matched physical protocol bill, or changed source-compatible demand/circuit; no affordable supplier yet.", + "status": "author-checked", + "source_commit": "0b082d22a0e9a442d264ab0633e35ef26c790630", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "refined", + "actual_scope": "On the published two-edge feed, an owner-indexed D-exponent-0 left map of the four final banks can keep x0 equal to D1 Q^{-1}, clear y0, and leave those banks stored unchanged. Every such map has the same two-monomial defect, and the constant-index map is charged.", + "scope_change_reason": "The card allows one source-bound caller identity with its extra charges. This package does not change the query demand and does not rerun the declared alternating-family lock. It takes the owner-indexed remainder of handoff discussioncomment-19138525: a port-dependent map on the final banks, with every new monomial charged. The x1 block and any new feedback edge stay outside this result.", + "bottleneck_link": "A productive main job has to be autonomous. The published feed restores D1 Q^{-1} only together with a y0 term. An owner-indexed reading can delete that term, but only by paying a forced two-monomial defect, and the x1 block is still unpaid, so the feed still does not earn a new kappa.", + "budget_minutes": 60, + "stop_rule": "Stop once every D-exponent-0 owner index on the four final banks is reduced to the two-monomial defect and the constant-index fresh image is charged, or once that image fails to keep x0 and clear y0. Do not search a new feedback edge or price a new Gaussian.", + "outcome": "partial", + "evidence": "PROOF.md and verify.py. The defect identity is an algebra calculation on the replayed final banks. The field ledger is one factored circuit under inherited units, not a minimum and not a kappa.", + "author": "unpaidmoon, with substantial Cursor Grok assistance", + "ai_assistance": "Substantial Cursor Grok assistance. No subagents. The predecessor replay and group algebra are imported unchanged.", + "open_questions": [ + { + "question": "Can a fresh image clear the three-term x1 block while keeping x0 equal to D1 Q^{-1}, keeping y0 zero, and leaving the four final banks stored unchanged?", + "why_it_matters": "The y0 term is no longer the obstruction on this image. The image is still not an autonomous job while those three x1 monomials remain.", + "first_step": "Write the same four-bank owner-indexed equation on the x1 column and charge every new monomial if a solution exists.", + "blocked_by": "This package leaves the published x1 coefficient on the fresh image and does not solve that column." + }, + { + "question": "Does one inherited monomial pass implement Q and Q^{-1}, or must Q^{-1} be expanded before this field ledger is a tape cost?", + "why_it_matters": "The ledger charges each of Q and Q^{-1} as one 112-field monomial pass, the unit used for Q^2 in the predecessor table. A three-factor expansion of Q^{-1} would raise the monomial count.", + "first_step": "Bind the source monomial primitive for a single power of Q, then replace only that unit in the factored circuit.", + "blocked_by": "No native word, fixed tape, or precision budget is replayed here." + } + ] +} diff --git a/research/owner-indexed-y0-clearance/VERIFY.json b/research/owner-indexed-y0-clearance/VERIFY.json new file mode 100644 index 0000000000..2a81fc3df1 --- /dev/null +++ b/research/owner-indexed-y0-clearance/VERIFY.json @@ -0,0 +1,37 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "checks": "Pins, final-bank normal forms, defect identity, fresh image, monomial charge, and failure controls.", + "timeout_seconds": 120 + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "checks": "Same owner-indexed charge under optimization. Checks are explicit failures, not assertions.", + "timeout_seconds": 120 + } + ], + "inputs": [ + "research/coded-active-feedback/search.py", + "research/coded-native-caller/gauge.py" + ], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/owner-indexed-y0-clearance/verify.py b/research/owner-indexed-y0-clearance/verify.py new file mode 100644 index 0000000000..e0fed497b7 --- /dev/null +++ b/research/owner-indexed-y0-clearance/verify.py @@ -0,0 +1,195 @@ +#!/usr/bin/env python3 +"""Owner-indexed reading that clears active-feedback y0 and keeps x0. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. +The predecessor replay and group algebra are imported unchanged. +""" +from hashlib import sha256 +import importlib.util +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent +QINV = (-1,) +LONG = (-1, 2, 1, 2) +# Inherited field units from research/coded-active-feedback/PROOF.md. +# One F-transpose recoding, one bank addition, one capture, one Q^2 pass. +C1_ADDS = 896 +C1_MONOMIALS = 224 +C1_CLEARS = 16 +BANK_ADDS = 112 +BANK_COPYS = 112 +MONOMIAL_PASS = 112 + + +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 even_word(word): + """Normal-form words whose every Q run has even exponent.""" + run = 0 + for letter in word: + if abs(letter) == 1: + run += letter + else: + if run % 2: + return False + run = 0 + return run % 2 == 0 + + +def in_even(element): + return all(even_word(word) for (word, _degree), value in element.items() if value) + + +def snapshot(rows): + return tuple(tuple(sorted(entry.items()) for entry in row) for row in rows) + + +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) + qinv, d1, d3 = algebra.inv(q), algebra.D(0), algebra.D(1) + observed, targets, rows = search.replay(algebra, algebra.one, algebra.mul(c1, q, q)) + need(len(observed) == 39, "saved-bank count moved") + left = [row for label, row in observed if label.startswith("left:")] + need(left == rows, "final rows are not the left endpoint banks") + stored = snapshot(rows) + + blank = {} + need(rows[1] == [blank, rows[1][1], blank, blank], "bank 1 is not pure y0") + need(len(rows[1][1]) == 1 and len(rows[2][0]) == 1, "units A and G moved") + a_coef = rows[2][0] + b_coef = rows[2][1] + g_coef = rows[1][1] + x3, y3 = rows[3][0], rows[3][1] + need(len(x3) == 1 and len(y3) == 1, "bank 3 lost its monomial columns") + inv_a = algebra.inv(a_coef) + x = algebra.mul(rows[0][0], inv_a) + g = algebra.mul(g_coef, inv_a) + b = algebra.mul(b_coef, inv_a) + need(g == algebra.term((2, 1, 1), (0, 0)), "g is not C1 Q^2") + need(algebra.mul(c1, g) == algebra.mul(q, q), "C1 g is not Q^2") + one_minus_q2 = algebra.add(algebra.one, algebra.neg(algebra.mul(q, q))) + need(algebra.mul(x, b) == one_minus_q2, "x b is not 1 - Q^2") + need(algebra.mul(algebra.add(algebra.mul(x, b), algebra.neg(algebra.one)), algebra.inv(g)) + == algebra.neg(c1), + "defect slope is not -C1") + const = algebra.mul(algebra.neg(b), algebra.inv(g)) + expected = { + (QINV, (0, 0)): -1, + (LONG, (0, 0)): 1, + } + need({key: int(value) for key, value in const.items()} == expected, + "const support moved") + factored = algebra.mul(qinv, algebra.add(algebra.mul(c1, q, c1), algebra.neg(algebra.one))) + need(factored == const, "factored circuit is not the defect") + need(not in_even(const), "defect collapsed into the even subalgebra") + + # Every D-exponent-0 m0 obeys m1 + m0 C1 = const once the finite products above hold. + # Spot-check the rearrangement, including a relocation of the pure Q^{-1} term into m0. + samples = [ + {}, + algebra.term((2, 3, 1, 1), (0, 0), 1), + algebra.add(algebra.term((3,), (0, 0), 2), algebra.term((1, 2, -1), (0, 0), -3)), + algebra.mul(algebra.neg(qinv), c1), + ] + for m0 in samples: + m2 = algebra.add(algebra.one, algebra.neg(algebra.mul(m0, x))) + m1 = algebra.add(const, algebra.neg(algebra.mul(m0, c1))) + image_x = algebra.add(algebra.mul(m0, rows[0][0]), algebra.mul(m2, a_coef)) + image_y = algebra.add(algebra.mul(m0, rows[0][1]), algebra.mul(m1, g_coef), + algebra.mul(m2, b_coef)) + need(image_x == a_coef and image_y == {}, "sample owner index missed the defect") + need(algebra.add(m1, algebra.mul(m0, c1)) == const, "sample defect was not const") + relocated_m0 = samples[-1] + relocated_m1 = algebra.add(const, algebra.neg(algebra.mul(relocated_m0, c1))) + need(algebra.mul(relocated_m0, c1).get((QINV, (0, 0))) == -1, + "relocation lost Q^{-1}") + need((QINV, (0, 0)) not in relocated_m1, "relocation failed to move Q^{-1} out of m1") + need(any(not even_word(word) for (word, _degree), value in relocated_m0.items() if value), + "relocated m0 became even") + + # Nonzero bank-3 coefficient cannot hide on the D1 line. + stray = algebra.mul(c1, y3) + need(stray and all(degree[1] == 1 for (_word, degree) in stray), + "bank 3 no longer occupies the D3 line") + need(all(degree[1] == 0 for (_word, degree) in b_coef), "coupling left the D1 line") + + # Constant owner index. Fresh image only; the four stored banks are not written. + m1 = const + fresh = [algebra.add(rows[2][j], algebra.mul(m1, rows[1][j])) for j in range(4)] + need(fresh[0] == a_coef and fresh[1] == {} and fresh[3] == {}, + "fresh image did not keep x0 and clear y0") + need(fresh[2] == rows[2][2] and fresh[2] != {}, "x1 block did not stay the published remainder") + published_x1 = algebra.add( + algebra.mul(algebra.add(algebra.mul(qinv, c1, q, c1), algebra.neg(qinv)), d1), + algebra.mul(qinv, c3, d1, d3)) + need(fresh[2] == published_x1, "x1 remainder is not the published three-term coefficient") + need(snapshot(rows) == stored, "stored endpoint banks were overwritten") + for dropped in (QINV, LONG): + partial = {key: value for key, value in m1.items() if key[0] != dropped} + residue = algebra.add(b_coef, algebra.mul(partial, g_coef)) + need(residue, "dropping a defect monomial still cleared y0") + + declared = [] + for word in search.words(4): + declared.append(word) + declared.append(search.reduce_word(tuple(word) + (1, 1))) + declared = set(declared) + for word in (QINV, LONG): + need(word not in declared, "defect monomial fell in the short declared family") + + # Letter count of the factored word Q^{-1}(C1 Q C1 - I), plus the copies and adds + # that keep both source banks stored. + c1_uses = 2 + uniform_monomials = 2 + bank_adds = 2 + bank_copies = 2 + ledger = { + "scalar_adds": c1_uses * C1_ADDS + bank_adds * BANK_ADDS, + "monomial_passes": c1_uses * C1_MONOMIALS + uniform_monomials * MONOMIAL_PASS, + "mode_clears": c1_uses * C1_CLEARS, + "copies": bank_copies * BANK_COPYS, + "extra_fields": 3 * BANK_COPYS, + "mode_fields": 8, + "gaussian_children": 0, + } + need(ledger == { + "scalar_adds": 2016, + "monomial_passes": 672, + "mode_clears": 32, + "copies": 224, + "extra_fields": 336, + "mode_fields": 8, + "gaussian_children": 0, + }, "ledger arithmetic moved") + need(len(const) == 2, "a defect monomial was omitted from the support") + print("PASS_OWNER_INDEXED_Y0_CLEARANCE") + print("defect", "-Q^{-1}+Q^{-1} C1 Q C1") + print("ledger", ledger) + print("x1_terms", len(fresh[2])) + print("new_kappa", None) + + +if __name__ == "__main__": + main()