From 00b08c5ae3a0f8a3645773978c5a557684e29e91 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Tue, 10 Nov 2026 10:20:08 +0000 Subject: [PATCH] Prove a D-exponent (0,-1) owner index leaves the x1 residual Every D3^{-1} correction of the sharp index keeps coefficient 1 on Q^{-1} C1 Q^2 C1 C3 D1 D3. The boundary-preserving family is u1=-u0 C1, u2=-u0 x, u3=0. No kappa change. Co-authored-by: unpaidmoon --- .../owner-indexed-d3-inverse-term/PROOF.md | 283 +++++++++++++ .../owner-indexed-d3-inverse-term/README.md | 133 ++++++ .../SOURCES.json | 30 ++ .../owner-indexed-d3-inverse-term/TASK.json | 84 ++++ .../owner-indexed-d3-inverse-term/VERIFY.json | 38 ++ .../owner-indexed-d3-inverse-term/verify.py | 387 ++++++++++++++++++ 6 files changed, 955 insertions(+) create mode 100644 research/owner-indexed-d3-inverse-term/PROOF.md create mode 100644 research/owner-indexed-d3-inverse-term/README.md create mode 100644 research/owner-indexed-d3-inverse-term/SOURCES.json create mode 100644 research/owner-indexed-d3-inverse-term/TASK.json create mode 100644 research/owner-indexed-d3-inverse-term/VERIFY.json create mode 100644 research/owner-indexed-d3-inverse-term/verify.py diff --git a/research/owner-indexed-d3-inverse-term/PROOF.md b/research/owner-indexed-d3-inverse-term/PROOF.md new file mode 100644 index 0000000000..44eff6a30a --- /dev/null +++ b/research/owner-indexed-d3-inverse-term/PROOF.md @@ -0,0 +1,283 @@ +# A D-exponent (0,-1) correction leaves the sharp x1 residual + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. + +No new κ is claimed. The selected frontier is unchanged. + +Evidence class: **proof** in the predecessor's formal algebra, under the +hypotheses below. The coefficient `u0` ranges over an infinite-dimensional +space. This is not an enumeration of words, not a bounded search, and not +a theorem about every quotient or every nonzero D exponent. + +## Object + +Use the published two-edge feed in +[research/coded-active-feedback](../coded-active-feedback/PROOF.md), +replayed by `search.replay(one, C1 Q^2)`. The four final banks and the +sharp index are the ones recorded by open PR #7033 in +`research/owner-indexed-x1-obstruction`: the D-exponent-0 multipliers + +```text +m0 = const C1 = -Q^{-1} C1 + Q^{-1} C1 Q, +m1 = 0, +m2 = Q^{-1} C1 Q^2 C1 Q, +m3 = 0, +``` + +with `const = -Q^{-1} + Q^{-1} C1 Q C1` and + +```text +x = Q^2 (I + Q) C1 Q. +``` + +Their fresh image has `x0 = A = Q^{-1} D1`, `y0 = 0`, `y1 = 0`, and + +```text +x1 = R = Q^{-1} C1 Q^2 C1 C3 D1 D3. +``` + +`verify.py` recomputes this image from the replay. It does not import the +unmerged package. The D-exponent-0 nonvanishing argument of #7033 is not +repeated. + +An owner index reads the four stored banks. It does not mix owners and +does not write the banks. A D-exponent `(0,-1)` correction of the sharp +index is a fresh image + +```text +S = sum_b (sharp_b + u_b D3^{-1}) · bank b, +``` + +where each `u_b` is an arbitrary element of D exponent `(0,0)`. One bank +means the other three coefficients are zero. Letters are `1 = Q`, +`-1 = Q^{-1}`, `2 = C1`, and `3 = C3`. The algebra is `search.algebra()`: +the free product `C4(Q) * C2(C1) * C2(C3)`, formal D exponents, and `D_i` +conjugating only `C_i` by `Q^{-1}`. Distinct D exponents are basis labels +in this algebra. No relation `D^4 = I` is imposed. + +## The four transported columns + +Left multiplication by `D3^{-1}` adds `(0,-1)` to every degree and +replaces each `C3` by `Q C3 Q^{-1}`. Letters `Q` and `C1` are fixed. +`verify.py` compares the resulting sixteen columns with the replay. +They are + +```text +bank 0, degree (1,-1): + x0 = Q^{-1} C1 + Q^2 C1 + y0 = Q^{-1} + x1 = -Q^2 C1 + y1 = 0 +bank 1, degree (1,-1): + y0 = C1 Q + x0 = x1 = y1 = 0 +bank 2: + x0 = Q^{-1} degree (1,-1) + y0 = Q^{-1} C1 Q - Q^{-1} C1 Q^2 degree (1,-1) + x1 = -Q^{-1} + Q^{-1} C1 Q C1 degree (1,-1) + + C3 Q^{-1} degree (1,0) + y1 = 0 +bank 3, degree (1,0): + x0 = Q C3 Q^2 C1 + y0 = Q C3 Q^{-1} + x1 = -I + Q C3 Q^{-1} C1 - Q C3 Q^2 C1 + y1 = Q C3 +``` + +Bank 3's `x0` word is the one place a `C3` is rewritten. The raw +conjugate of `C3 Q^{-1} C1` is `Q C3 Q^{-1} Q^{-1} C1`, and the Q-run +`Q^{-2}` normalizes to `Q^2`, giving `Q C3 Q^2 C1`. + +Every x1 transport misses D degree `(1,1)`. A D-exponent-0 left factor +adds degree `(0,0)`, so it preserves those degrees. The sharp x1 column +is exactly `R`, at degree `(1,1)`. Therefore, for every coefficient +tuple `(u0,u1,u2,u3)`, + +```text +S_x1 = R + (terms of D degree other than (1,1)). +``` + +The coefficient of `Q^{-1} C1 Q^2 C1 C3 D1 D3` stays `1`. In particular +`S_x1` is not zero. This is the whole four-bank family, not a sample of +`u_b`. + +## Right multiplication by a monomial is injective + +The reducer is the left-to-right stack in `search.reduce_word`. Its stack +after reading a word is the reduced word. A reduced word is alternating +canonical syllables: a Q syllable is empty, `Q`, `Q^2`, or `Q^{-1}`, and a +C syllable is a single `C1` or `C3` different from the previous letter. +Reading that word again pushes the same syllables, so reduction is +idempotent, and + +```text +reduce(reduce(A) + B) = reduce(A + B) +``` + +for every word pair. The four-syllable normal forms are a control for this +fold, not the proof. + +On normal words, right multiplication by `Q^r` adds `r` to the final +Q exponent modulo 4 and leaves the preceding prefix fixed. Addition +modulo 4 is bijective, so every Q power, including `Q^{-1}` and `Q^2`, +is bijective. Right multiplication by `C_i` is the involution that +deletes a final `C_i` or appends one; a normal word does not end with +two copies of `C_i`, so the second application restores the word. + +Right multiplication by a normal word is the composition of its syllable +maps, hence bijective. For a one-term element `g` of nonzero coefficient, +a D-exponent-0 element `u` satisfies `u g = 0` only when `u = 0`: degree +0 does not conjugate the word of `g`, the product has one output term per +term of `u`, and those words are distinct. + +The same fold gives the association used below. For D-exponent-0 elements +`u,z` and a monomial `g`, + +```text +(u z) g = u (z g), +``` + +because both sides are bilinear and, on monomials, both word maps reduce +the concatenated letters. + +## The boundary family + +Write `T_b` for the column transports above. Direct expansion gives + +```text +x T_{2,x0} = (Q^{-1} + Q^2) C1 Q · Q^{-1} + = (Q^{-1} + Q^2) C1 + = T_{0,x0} +``` + +at degree `(1,-1)`. For the y0 columns, write + +```text +A = Q^{-1} C1 Q, B = Q^2 C1 Q, S = Q^{-1} C1 Q^2, +``` + +so `x = A + B` and `T_{2,y0} = A - S`. Then `A^2 = I`, `B A = Q^{-1}`, +`A S = Q`, and `B S = I`, hence + +```text +x T_{2,y0} = (I + Q^{-1}) - (I + Q) = Q^{-1} - Q. +``` + +Also `C1 T_{1,y0} = C1 (C1 Q) = Q`, so + +```text +C1 T_{1,y0} + x T_{2,y0} = Q^{-1} = T_{0,y0}. +``` + +Both `x` and `C1` use only `Q` and `C1`, so each commutes with +`D3^{-1}`. The sharp image already has `x0 = A` and `y0 = 0`, and the +transports of banks 0, 1, and 2 lie in degree `(1,-1)` on those two +columns. Bank 3's x0 and y0 transports lie in degree `(1,0)` and are the +monomial units `Q C3 Q^2 C1` and `Q C3 Q^{-1}`. The degree-`(1,0)` part +of `S_y0` is therefore `u3` times a unit, and the degree-`(1,0)` part of +`S_x0` is `A` plus `u3` times a unit. Either forces + +```text +u3 = 0. +``` + +The degree-`(1,-1)` equations are then + +```text +(u0 x + u2) T_{2,x0} = 0, +(u0 C1 + u1) T_{1,y0} = 0. +``` + +`T_{2,x0} = Q^{-1}` and `T_{1,y0} = C1 Q` are monomial units, so + +```text +u2 = -u0 x, u1 = -u0 C1. +``` + +Conversely, every `u0` with these coefficients keeps `x0 = A`, `y0 = 0`, +and `y1 = 0`: banks 0, 1, and 2 have zero y1 transport, and `u3 = 0`. +The x1 column of this family is `S_x1 = R + u0 Δ` with +`Δ = T_{0,x1} - x T_{2,x1}`. For the witness `u0 = I`, so `u2 = -x`, +the products are: + +```text +(-x)(-Q^{-1}) = Q^{-1} C1 + Q^2 C1, +(-x)(Q^{-1} C1 Q C1) = -C1 - Q^{-1} C1, +T_{0,x1} = -Q^2 C1. +``` + +The degree-`(1,-1)` sum is `-C1`. The only degree-`(1,0)` source in +`T_{2,x1}` is `C3 Q^{-1}`, and + +```text +(-x)(C3 Q^{-1}) = -Q^{-1} C1 Q C3 Q^{-1} - Q^2 C1 Q C3 Q^{-1}. +``` + +Thus + +```text +Δ = -C1 D1 D3^{-1} + - Q^{-1} C1 Q C3 Q^{-1} D1 + - Q^2 C1 Q C3 Q^{-1} D1. +``` + +`Δ` has no degree-`(1,1)` term, so `R` remains with coefficient 1 for +every `u0`. One bank is the special case in which two of `u0,u1,u2` +vanish. Since `x` and `C1` are nonzero, that forces `u0 = 0`. + +## The witness and its charge + +Take `u0 = I`. Then `u1 = -C1` and + +```text +u2 = -x = -Q^{-1} C1 Q - Q^2 C1 Q. +``` + +The new multiplier monomials, beyond the three sharp monomials, are + +```text +D3^{-1} on bank 0, +-C1 D3^{-1} on bank 1, +-Q^{-1} C1 Q D3^{-1} on bank 2, +-Q^2 C1 Q D3^{-1} on bank 2. +``` + +The fresh x1 column is `R + Δ`: the residual monomial, unchanged, plus +the three monomials of `Δ`. The algebraic charge of this near-miss is +the four new multiplier monomials together with those three image +monomials. None of them removes `R`. No scalar-field minimum and no tape +cost are claimed. The four stored banks are only read. + +For a general `u0`, the same charge is the support of `u0`, of `-u0 C1`, +and of `-u0 x`, together with the support of `u0 Δ` in the image. Every +such support leaves the residual monomial in place. + +## One homogeneous term on one bank + +The single-bank case above is degree `(0,-1)`. The same gate applies to +every other single degree. Each bank has a monomial column among x0 and +y0: bank 0 and bank 1 use y0, and bank 2 and bank 3 use x0. For any D +exponent `d`, `D^d` times that monomial is one monomial, because the +product of two one-term elements is one term. Right multiplication by +that monomial is injective on D-exponent-0 elements by the syllable +argument. Adding only `u D^d` on that bank therefore keeps `x0 = A` and +`y0 = 0` exactly when `u = 0`, and the zero coefficient leaves `R`. + +This does not classify two banks at a degree other than `(0,-1)`. + +## What is not proved + +A D exponent other than `(0,-1)`, spread across two or more banks, can +meet degree `(1,1)`. The same closed form `u1 = -u0 C1`, `u2 = -u0 x`, +`u3 = 0` keeps the boundary when `D3^{-1}` is replaced by `D3`, because +`x` and `C1` commute with every power of `D3`. For `u0 = I` that positive +power changes the degree-`(1,1)` line: `verify.py` checks that the line +properly contains `R` and that x1 is still not zero. No coefficient is +solved there. + +Owner-mixing maps, a feedback edge other than `(I, C1 Q^2)`, and a +physical relation that identifies distinct D exponents are outside this +statement. In a quotient that moves degree `(1,1)` onto a shifted degree, +the formal coefficient 1 need not remain visible. No such quotient is +proved here. The result is not an autonomous decoder, not a new caller +bill, and not a change of the selected conditional κ. diff --git a/research/owner-indexed-d3-inverse-term/README.md b/research/owner-indexed-d3-inverse-term/README.md new file mode 100644 index 0000000000..9eb7fdd744 --- /dev/null +++ b/research/owner-indexed-d3-inverse-term/README.md @@ -0,0 +1,133 @@ +# A D-exponent (0,-1) correction leaves the sharp x1 residual + +**Scoped proof; no new κ.** On the published two-edge feed, start from the +sharp owner index of open PR #7033 and add arbitrary D-exponent-0 +coefficients times `D3^{-1}` on the four final banks. The fresh x1 column +still contains + +```text +Q^{-1} C1 Q^2 C1 C3 D1 D3 +``` + +with coefficient 1. The four stored endpoint banks are not overwritten. +Keeping `x0 = D1 Q^{-1}` and y0 zero forces the coefficients + +```text +u1 = -u0 C1, u2 = -u0 x, u3 = 0, +``` + +with `u0` an arbitrary D-exponent-0 element and `x = Q^2 (I + Q) C1 Q`. +The x1 column is then the residual monomial plus `u0` times a fixed +three-monomial defect. [PROOF.md](PROOF.md) gives the transports and the +products. + +One bank is included: the gate column of that bank is a monomial unit, so +the coefficient must be zero, and the sharp residual remains. The same +gate blocks one homogeneous term of every other D exponent on one bank. +It does not block two banks at an exponent other than `(0,-1)`. + +The selected frontier is unchanged. This does not rerun the D-exponent-0 +obstruction, the y0 defect, or the one-edge `C1 Q` row. + +## Result + +The sharp image has `x0 = A = Q^{-1} D1`, y0 zero, y1 zero, and x1 equal +to the one monomial above. Left multiplication by `D3^{-1}` moves every +bank-x1 degree off `(1,1)`. A D-exponent-0 factor preserves degree, so no +choice of the four coefficients deletes that monomial. + +The witness `u0 = I` uses four new multiplier monomials + +```text +D3^{-1}, -C1 D3^{-1}, -Q^{-1} C1 Q D3^{-1}, -Q^2 C1 Q D3^{-1} +``` + +on banks 0, 1, and 2. Its x1 column is the residual plus + +```text +-C1 D1 D3^{-1} +- Q^{-1} C1 Q C3 Q^{-1} D1 +- Q^2 C1 Q C3 Q^{-1} D1. +``` + +Those monomials are the algebraic charge of this near-miss. They do not +clear the block. No scalar-field minimum and no tape cost are claimed. + +## Reproduce + +From the repository root, Python 3.12, standard library only: + +```sh +python3 -B scripts/research_package.py --package research/owner-indexed-d3-inverse-term --check-only +python3 -B scripts/research_package.py --package research/owner-indexed-d3-inverse-term +``` + +Direct replay: + +```sh +python3 -I -W error -B research/owner-indexed-d3-inverse-term/verify.py +python3 -I -O -W error -B research/owner-indexed-d3-inverse-term/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, or an obstruction to that +change, together with its charges. This package does not change the query +demand. It takes the first open question of +[research/owner-indexed-x1-obstruction](https://github.com/CrocSwap/integer-mult-bounds/pull/7033): +add one term of D exponent `(0,-1)` to the sharp index and recompute the +four columns. The multi-bank family of that same exponent is the same +degree count, not a second exponent. + +Base commit: `17469fff78c22941280f04d39dc5a1faee09c840`. Pins are in +[SOURCES.json](SOURCES.json). The catalogue is provenance. The selected +record, `search.py`, and `gauge.py` are live inputs. The verifier rejects +a moved κ. The selected conditional value is the selected record, +`781451/250000000`. + +Overlap before this package was added, at base +`17469fff78c22941280f04d39dc5a1faee09c840`: `scripts/find_overlap.py +--refresh --all-terms` searched the complete local note inventory (10178 +paths) and a snapshot of 339 open PR records fetched at 2026-11-10T10:15:04Z +plus 7013 discussion records fetched at 2026-11-10T10:16:06Z. Both phrases +`D exponent (0,-1)` and `owner-indexed` match only +[discussion reply 19513867](https://github.com/CrocSwap/integer-mult-bounds/discussions/4930#discussioncomment-19513867), +which asks this question and does not answer it. Open PR #7033 states the +same question with the exponent in backticks, so that literal pair misses +its body; the PR was read directly. That search is not a novelty +certificate. Closed PR bodies were outside the snapshot. + +## Open next questions + +Can a D-exponent `(0,1)` correction of the same sharp index, using two or +more banks, make the fresh x1 column zero while keeping `x0 = D1 Q^{-1}` +and y0 zero? Exponent `(0,-1)` never meets the residual degree. One +homogeneous term on one bank is already blocked for every degree by the +monomial gate. The coefficient shape `u1 = -u0 C1`, `u2 = -u0 x`, +`u3 = 0` still keeps the boundary at `D3`, and for `u0 = I` the +degree-`(1,1)` line properly contains the residual, so that positive +power is not the calculation above. The first step is to decide whether +any D-exponent-0 `u0` makes `R + u0 Δ_+` the zero element, where `Δ_+` +is the defect of that positive power, and to charge every monomial of a +solution. No such `u0` is solved here. The omitted-physical-relation +question of PR #7033 is a separate remainder and is not taken 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 y0 defect is `research/owner-indexed-y0-clearance`. +The sharp index and the residual monomial are open PR #7033, +`research/owner-indexed-x1-obstruction`, head +`bc08ea6b28c345b0164ff1631642974719da087a`. The declared-family obstruction +is `research/active-feedback-coupling-lock`. The one-edge `C1 Q` row is +`research/active-feedback-outside-edge`. 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-d3-inverse-term/SOURCES.json b/research/owner-indexed-d3-inverse-term/SOURCES.json new file mode 100644 index 0000000000..2dd75c18f3 --- /dev/null +++ b/research/owner-indexed-d3-inverse-term/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "17469fff78c22941280f04d39dc5a1faee09c840", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "input", + "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-d3-inverse-term/TASK.json b/research/owner-indexed-d3-inverse-term/TASK.json new file mode 100644 index 0000000000..6ff7f038fe --- /dev/null +++ b/research/owner-indexed-d3-inverse-term/TASK.json @@ -0,0 +1,84 @@ +{ + "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": "On the published two-edge feed, every D-exponent (0,-1) correction of the sharp owner index from PR #7033 leaves coefficient 1 on the x1 monomial Q^{-1} C1 Q^2 C1 C3 D1 D3. The corrections that keep x0 = D1 Q^{-1} and y0 zero are exactly u1 = -u0 C1, u2 = -u0 x, u3 = 0 for an arbitrary D-exponent-0 element u0. Their x1 column is that monomial plus u0 times a fixed three-monomial defect. One bank forces u0 = 0. The four banks stay stored. No new kappa.", + "scope_change_reason": "The card allows one source-bound caller identity or an obstruction to that change. This package does not change the query demand and does not rerun the D-exponent-0 obstruction of PR #7033, the y0 defect, or the one-edge C1 Q result. It answers the D-exponent (0,-1) term named by that PR, including every bank coefficient of that same exponent.", + "bottleneck_link": "An autonomous main row needs x1 = 0 with x0 = D1 Q^{-1} and y0 = 0. Every formal D-exponent (0,-1) correction of the sharp index leaves the residual monomial's coefficient equal to 1, so this term does not earn a new kappa.", + "budget_minutes": 60, + "stop_rule": "Stop once every D-exponent (0,-1) correction of the sharp index is shown to keep coefficient 1 on the residual monomial, including the boundary-preserving family. Do not solve a D-exponent (0,1) correction or a physical quotient.", + "outcome": "negative-result", + "evidence": "PROOF.md and verify.py. The four transported x1 columns miss D degree (1,1), and a D-exponent-0 factor preserves degree. The boundary family is the closed form u1=-u0 C1, u2=-u0 x, u3=0. The syllable-length-4 replay is a control, not a census of u0. No kappa change.", + "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 D-exponent (0,1) correction of the same sharp index, using two or more banks, make the fresh x1 column zero while keeping x0 = D1 Q^{-1} and y0 zero?", + "why_it_matters": "Exponent (0,-1) never meets the residual degree. One homogeneous term on one bank is already blocked for every degree by the monomial gate, but two banks at exponent (0,1) can meet x1 degree (1,0) and therefore degree (1,1).", + "first_step": "Use the coefficient shape u1 = -u0 C1, u2 = -u0 x, u3 = 0, which keeps the boundary at D3 as well as at D3^{-1}. For u0 = I the degree-(1,1) line properly contains the residual. Decide whether any D-exponent-0 u0 makes R + u0 Delta_+ the zero element, and charge every monomial of a solution.", + "blocked_by": "This package classifies only exponent (0,-1), plus the one-bank gate for a single homogeneous degree. The positive-power defect is not solved." + } + ] +} diff --git a/research/owner-indexed-d3-inverse-term/VERIFY.json b/research/owner-indexed-d3-inverse-term/VERIFY.json new file mode 100644 index 0000000000..bf967e58d1 --- /dev/null +++ b/research/owner-indexed-d3-inverse-term/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "research/coded-active-feedback/search.py", + "research/coded-native-caller/gauge.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "checks": "Pins, sharp residual, D3^{-1} column transports, boundary family, witness charge, and failure controls.", + "timeout_seconds": 120 + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "checks": "Same D-exponent (0,-1) identity under optimization. Checks are explicit failures, not assertions.", + "timeout_seconds": 120 + } + ] +} diff --git a/research/owner-indexed-d3-inverse-term/verify.py b/research/owner-indexed-d3-inverse-term/verify.py new file mode 100644 index 0000000000..130d8c2e10 --- /dev/null +++ b/research/owner-indexed-d3-inverse-term/verify.py @@ -0,0 +1,387 @@ +#!/usr/bin/env python3 +"""D-exponent (0,-1) corrections of the sharp owner index leave the x1 residual. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. +The predecessor replay and group algebra are imported unchanged. +The syllable-length-4 replay is a control. The proof is the identity in PROOF.md. +""" +from hashlib import sha256 +import importlib.util +import json +from fractions import Fraction +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent +QINV = (-1,) +LONG = (-1, 2, 1, 2) +SHARP_M2 = (-1, 2, 1, 1, 2, 1) +RESIDUAL = (-1, 2, 1, 1, 2, 3) +DELTA = ( + ((2,), (1, -1), -1), + ((-1, 2, 1, 3, -1), (1, 0), -1), + ((1, 1, 2, 1, 3, -1), (1, 0), -1), +) + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def load_search(): + path = ROOT / "research/coded-active-feedback/search.py" + spec = importlib.util.spec_from_file_location("active_feedback_search_pinned", path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def support(element): + return {(word, degree): int(value) if value.denominator == 1 else value + for (word, degree), value in element.items()} + + +def degree_part(element, degree): + return {key: value for key, value in element.items() if key[1] == degree} + + +def degrees(element): + return {degree for (_word, degree) in element} + + +def literal(algebra, rows): + total = {} + for word, degree, coefficient in rows: + total = algebra.add(total, algebra.term(word, degree, coefficient)) + return total + + +def syllable_count(max_syllables): + factors = ("Q", "C1", "C3") + sizes = {"Q": 3, "C1": 1, "C3": 1} + previous = {factor: sizes[factor] for factor in factors} + total = 1 + sum(previous.values()) + for _length in range(2, max_syllables + 1): + current = {} + for factor in factors: + current[factor] = sizes[factor] * sum( + previous[other] for other in factors if other != factor) + total += current[factor] + previous = current + return total + + +def syllable_length(word): + count = 0 + previous = None + for letter in word: + factor = "Q" if abs(letter) == 1 else letter + if factor != previous: + count += 1 + previous = factor + return count + + +def normal_words(algebra, max_syllables): + syllables = { + "Q": ((1,), (1, 1), (-1,)), + "C1": ((2,),), + "C3": ((3,),), + } + found = {(): None} + frontier = [()] + while frontier: + current = frontier + frontier = [] + for word in current: + if syllable_length(word) >= max_syllables: + continue + previous = found[word] + for factor, choices in syllables.items(): + if factor == previous: + continue + for syllable in choices: + produced = algebra.mul(algebra.term(word, (0, 0)), + algebra.term(syllable, (0, 0))) + need(len(produced) == 1, "syllable product left the group") + (new, degree), value = next(iter(produced.items())) + need(degree == (0, 0) and value == 1, "syllable product was not a unit") + if new not in found: + found[new] = factor + frontier.append(new) + return found + + +def final_q_exponent(word): + index = len(word) + while index and abs(word[index - 1]) == 1: + index -= 1 + tail = word[index:] + if tail == (): + return 0, word + if tail == (1,): + return 1, word[:index] + if tail == (1, 1): + return 2, word[:index] + if tail == (-1,): + return 3, word[:index] + raise ValueError("normal word has a noncanonical Q tail") + + +def main(): + pinned = { + "research/coded-active-feedback/search.py": + "1383010827af29a1b0e595e2c1aa2ffad461b266ffc9f936efce1603ff9f5eb6", + "research/coded-native-caller/gauge.py": + "390391d291353741c89daea999d483660ca185987ed96a15b82576280c487cad", + "certificates/selected-result.json": + "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa", + } + for name, digest in pinned.items(): + need(sha256((ROOT / name).read_bytes()).hexdigest() == digest, "changed pin " + name) + selected = json.loads((ROOT / "certificates/selected-result.json").read_text(encoding="utf-8")) + need(selected["kappa"] == "781451/250000000", "selected frontier value moved") + + 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) + d3inv = algebra.inv(d3) + blank = {} + 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 = tuple(tuple(tuple(sorted(entry.items())) for entry in row) for row in rows) + + const = algebra.add(algebra.term(QINV, (0, 0), -1), algebra.term(LONG, (0, 0))) + one_plus_q = algebra.add(algebra.one, q) + x = algebra.mul(algebra.mul(q, q), one_plus_q, c1, q) + sharp_m0 = algebra.mul(const, c1) + sharp_m2 = algebra.add(algebra.one, algebra.neg(algebra.mul(sharp_m0, x))) + sharp_m1 = algebra.add(const, algebra.neg(algebra.mul(sharp_m0, c1))) + need(sharp_m1 == blank, "sharp index reopened y0") + need(support(sharp_m0) == {((-1, 2), (0, 0)): -1, ((-1, 2, 1), (0, 0)): 1}, + "sharp m0 support moved") + need(sharp_m2 == algebra.term(SHARP_M2, (0, 0)), "sharp m2 is not one monomial") + sharp = [algebra.add(algebra.mul(sharp_m0, rows[0][column]), + algebra.mul(sharp_m2, rows[2][column])) + for column in range(4)] + residual = algebra.term(RESIDUAL, (1, 1)) + anchor = algebra.term(QINV, (1, 0)) + need(sharp[0] == anchor and sharp[1] == blank and sharp[3] == blank, + "sharp image did not keep x0 and clear y0 and y1") + need(sharp[2] == residual, "sharp x1 is not the residual monomial") + + expected = [ + [ + algebra.add(algebra.term((-1, 2), (1, -1)), algebra.term((1, 1, 2), (1, -1))), + algebra.term((-1,), (1, -1)), + algebra.term((1, 1, 2), (1, -1), -1), + blank, + ], + [ + blank, + algebra.term((2, 1), (1, -1)), + blank, + blank, + ], + [ + algebra.term((-1,), (1, -1)), + algebra.add(algebra.term((-1, 2, 1), (1, -1)), + algebra.term((-1, 2, 1, 1), (1, -1), -1)), + algebra.add(algebra.term((-1,), (1, -1), -1), + algebra.term((-1, 2, 1, 2), (1, -1)), + algebra.term((3, -1), (1, 0))), + blank, + ], + [ + algebra.term((1, 3, 1, 1, 2), (1, 0)), + algebra.term((1, 3, -1), (1, 0)), + algebra.add(algebra.term((), (1, 0), -1), + algebra.term((1, 3, -1, 2), (1, 0)), + algebra.term((1, 3, 1, 1, 2), (1, 0), -1)), + algebra.term((1, 3), (1, 0)), + ], + ] + transported = [[algebra.mul(d3inv, rows[bank][column]) for column in range(4)] + for bank in range(4)] + need(transported == expected, "D3^{-1} column transports moved") + for bank in range(4): + need((1, 1) not in degrees(transported[bank][2]), + "a D3^{-1} x1 transport met the residual degree") + need(degrees(transported[0][0]) == {(1, -1)} and degrees(transported[0][1]) == {(1, -1)}, + "bank 0 gate degrees moved") + need(degrees(transported[1][1]) == {(1, -1)} and transported[1][0] == blank, + "bank 1 gate degrees moved") + need(degrees(transported[2][0]) == {(1, -1)} and degrees(transported[2][1]) == {(1, -1)}, + "bank 2 gate degrees moved") + need(degrees(transported[3][0]) == {(1, 0)} and degrees(transported[3][1]) == {(1, 0)}, + "bank 3 gate degrees moved") + + gates = ( + transported[0][1], + transported[1][1], + transported[2][0], + transported[3][0], + transported[3][1], + ) + for gate in gates: + inverse = algebra.inv(gate) + need(algebra.mul(gate, inverse) == algebra.one and algebra.mul(inverse, gate) == algebra.one, + "a gate column is not a monomial unit") + + # The degree-0 identities transport because x and C1 contain no C3. + need(algebra.mul(d3inv, x) == algebra.mul(x, d3inv), "x failed to commute with D3^{-1}") + need(algebra.mul(d3inv, c1) == algebra.mul(c1, d3inv), "C1 failed to commute with D3^{-1}") + need(algebra.add(transported[0][0], algebra.neg(algebra.mul(x, transported[2][0]))) == blank, + "x0 transport identity failed") + y_identity = algebra.add(transported[0][1], + algebra.neg(algebra.mul(c1, transported[1][1])), + algebra.neg(algebra.mul(x, transported[2][1]))) + need(y_identity == blank, "y0 transport identity failed") + delta = algebra.add(transported[0][2], algebra.neg(algebra.mul(x, transported[2][2]))) + need(delta == literal(algebra, DELTA), "homogeneous x1 defect moved") + need((1, 1) not in degrees(delta) and delta != blank, "defect met the residual degree or vanished") + + samples = [ + blank, + algebra.one, + c1, + c3, + q, + algebra.mul(qinv, c1), + algebra.add(c3, algebra.mul(q, q), algebra.term((2, 3), (0, 0), -2)), + algebra.term((2, 3, 1, 1, 2), (0, 0), 5), + ] + for coefficient in samples: + need(degrees(coefficient) <= {(0, 0)}, "sample left the D-exponent-0 line") + u1 = algebra.mul(algebra.neg(coefficient), c1) + u2 = algebra.mul(algebra.neg(coefficient), x) + solved_u2 = algebra.mul(algebra.neg(algebra.mul(coefficient, transported[0][0])), + algebra.inv(transported[2][0])) + y_load = algebra.add(algebra.mul(coefficient, transported[0][1]), + algebra.mul(u2, transported[2][1])) + solved_u1 = algebra.mul(algebra.neg(y_load), algebra.inv(transported[1][1])) + need(solved_u1 == u1 and solved_u2 == u2, "boundary solution left the closed form") + image = [] + for column in range(4): + image.append(algebra.add( + sharp[column], + algebra.mul(coefficient, transported[0][column]), + algebra.mul(u1, transported[1][column]), + algebra.mul(u2, transported[2][column]))) + need(image[0] == anchor and image[1] == blank and image[3] == blank, + "boundary family failed to keep x0 and clear y0 and y1") + need(degree_part(image[2], (1, 1)) == residual, "boundary family changed the residual") + need(image[2] == algebra.add(residual, algebra.mul(coefficient, delta)), + "boundary x1 is not the residual plus u0 times the defect") + # Arbitrary coefficients, not only the boundary family. + stray = algebra.add( + sharp[2], + algebra.mul(coefficient, transported[0][2]), + algebra.mul(c3, transported[1][2]), + algebra.mul(q, transported[2][2]), + algebra.mul(c1, transported[3][2])) + need(degree_part(stray, (1, 1)) == residual, + "a non-boundary (0,-1) correction changed the residual") + + # Witness u0 = I. Four new multiplier monomials, three extra x1 monomials. + witness_u1 = algebra.neg(c1) + witness_u2 = algebra.neg(x) + need(support(witness_u2) == {((-1, 2, 1), (0, 0)): -1, ((1, 1, 2, 1), (0, 0)): -1}, + "witness u2 is not -Q^{-1} C1 Q - Q^2 C1 Q") + witness = [] + for column in range(4): + witness.append(algebra.add( + sharp[column], + transported[0][column], + algebra.mul(witness_u1, transported[1][column]), + algebra.mul(witness_u2, transported[2][column]))) + need(witness[0] == anchor and witness[1] == blank and witness[3] == blank, + "witness did not keep the boundary") + need(witness[2] == algebra.add(residual, delta) and len(witness[2]) == 4, + "witness x1 is not the residual plus the three-term defect") + need(degree_part(witness[2], (1, 1)) == residual, "witness cancelled or duplicated the residual") + + # One bank, any listed degree: the monomial gate forces the coefficient to vanish. + single_degrees = ((0, 0), (0, -1), (0, 1), (1, 0), (-1, 1), (2, -3)) + gate_columns = (1, 1, 0, 0) + for degree in single_degrees: + shift = algebra.term((), degree) + for bank, column in enumerate(gate_columns): + gate = algebra.mul(shift, rows[bank][column]) + need(len(gate) == 1, "a single-bank gate stopped being one monomial") + inverse = algebra.inv(gate) + need(algebra.mul(gate, inverse) == algebra.one, "a single-bank gate is not a unit") + image = [algebra.add(sharp[index], algebra.mul(shift, rows[bank][index])) + for index in range(4)] + need(image[0] != anchor or image[1] != blank, + "a nonzero single-bank term kept x0 and y0") + if degree == (0, -1): + need(degree_part(image[2], (1, 1)) == residual, + "a single-bank (0,-1) term changed the residual") + + # Syllable control for the fold and the Q-exponent bijection. Not a census of u0. + words = normal_words(algebra, 4) + need(len(words) == syllable_count(4) == 192, "four-syllable normal forms are incomplete") + syllables = ((1,), (1, 1), (-1,), (2,), (3,)) + for word in words: + need(search.reduce_word(word) == word, "generated word was not normal") + exponent, prefix = final_q_exponent(word) + for syllable in syllables: + extended = word + syllable + need(search.reduce_word(search.reduce_word(word) + syllable) == search.reduce_word(extended), + "reducer fold failed on a four-syllable word") + if abs(syllable[0]) == 1: + power = { (1,): 1, (1, 1): 2, (-1,): 3 }[syllable] + shifted = algebra.mul(algebra.term(word, (0, 0)), algebra.term(syllable, (0, 0))) + (new, degree), value = next(iter(shifted.items())) + new_exponent, new_prefix = final_q_exponent(new) + need(degree == (0, 0) and value == 1, "Q power left the degree-0 group") + need(new_prefix == prefix and new_exponent == (exponent + power) % 4, + "Q power did not act on the final exponent") + for gate in gates: + ((gate_word, gate_degree), gate_value), = gate.items() + cancelled = algebra.mul(algebra.term(word, (0, 0)), gate, algebra.inv(gate)) + need(cancelled == algebra.term(word, (0, 0)), + "a gate failed to cancel on a four-syllable word") + need(gate_value != 0 and gate_degree != (0, 0), "gate degree collapsed") + need(gate_word == search.reduce_word(gate_word), "gate word was not normal") + + # Failure controls. + for bank in range(4): + only = [algebra.add(sharp[column], transported[bank][column]) for column in range(4)] + need(only[0] != anchor or only[1] != blank, "one bank of D3^{-1} kept the boundary") + need(degree_part(only[2], (1, 1)) == residual, "one bank of D3^{-1} changed the residual") + positive = algebra.D(1) + copied = [] + for column in range(4): + copied.append(algebra.add( + sharp[column], + algebra.mul(positive, rows[0][column]), + algebra.mul(witness_u1, positive, rows[1][column]), + algebra.mul(witness_u2, positive, rows[2][column]))) + need(copied[0] == anchor and copied[1] == blank and copied[3] == blank, + "the commuting coefficient shape stopped preserving the boundary at D3") + need(copied[2] != blank and degree_part(copied[2], (1, 1)) != residual, + "D3^{+1} reproduced the (0,-1) residual line") + need(residual.items() <= degree_part(copied[2], (1, 1)).items(), + "the unchecked D3^{+1} shape already deleted the residual key") + need(tuple(stored) == tuple(tuple(tuple(sorted(entry.items())) for entry in row) for row in rows), + "stored endpoint banks were overwritten") + need(selected["kappa"] == "781451/250000000", "selected frontier value moved during the check") + + print("PASS_OWNER_INDEXED_D3_INVERSE_TERM") + print("evidence_class", "proof") + print("residual_coefficient", 1) + print("boundary_family", "u1=-u0*C1, u2=-u0*x, u3=0") + print("witness_new_multiplier_monomials", 4) + print("witness_x1_terms", len(witness[2])) + print("syllable_control", 4) + print("new_kappa", None) + + +if __name__ == "__main__": + main()