From 9c159482e0495b6a97e17e629debe66a0ceb9466 Mon Sep 17 00:00:00 2001 From: apoursh <8867770+apoursh@users.noreply.github.com> Date: Thu, 29 Oct 2026 14:55:54 -0400 Subject: [PATCH] Classify dyadic cubic-reader repair coefficients --- research/dyadic-cubic-repair/PROOF.md | 255 ++++++++++++ research/dyadic-cubic-repair/README.md | 151 +++++++ research/dyadic-cubic-repair/SOURCE-PINS.json | 23 ++ research/dyadic-cubic-repair/SOURCES.json | 18 + research/dyadic-cubic-repair/TASK.json | 110 +++++ research/dyadic-cubic-repair/VERIFY.json | 59 +++ .../dyadic-cubic-repair/independent_check.py | 305 ++++++++++++++ .../sources/pr6200-PROOF.md | 195 +++++++++ .../sources/pr6200-README.md | 126 ++++++ research/dyadic-cubic-repair/verify.py | 384 ++++++++++++++++++ 10 files changed, 1626 insertions(+) create mode 100644 research/dyadic-cubic-repair/PROOF.md create mode 100644 research/dyadic-cubic-repair/README.md create mode 100644 research/dyadic-cubic-repair/SOURCE-PINS.json create mode 100644 research/dyadic-cubic-repair/SOURCES.json create mode 100644 research/dyadic-cubic-repair/TASK.json create mode 100644 research/dyadic-cubic-repair/VERIFY.json create mode 100644 research/dyadic-cubic-repair/independent_check.py create mode 100644 research/dyadic-cubic-repair/sources/pr6200-PROOF.md create mode 100644 research/dyadic-cubic-repair/sources/pr6200-README.md create mode 100644 research/dyadic-cubic-repair/verify.py diff --git a/research/dyadic-cubic-repair/PROOF.md b/research/dyadic-cubic-repair/PROOF.md new file mode 100644 index 0000000000..a1c41a9afc --- /dev/null +++ b/research/dyadic-cubic-repair/PROOF.md @@ -0,0 +1,255 @@ +# Prime denominators in cubic-reader repair + +Prepared by apoursh with substantial OpenAI Codex assistance. Apache-2.0. +This extends Nick Petalas's PR6200, pinned in SOURCE-PINS.json. Its rational +two-cube criterion is restated and credited below. The new step is the exact +coefficient-ring obstruction, including nonmonic forms, and integer repairs. + +## Contract and claims + +Let P be any set of primes and R=Z[P^-1], a subring of Q. All coefficients +of appended source transformations and weighted cube queries must lie in R. +Source transformations belong to GL_2(R), so their inverses also lie in R. +The original streams y,a,b are arbitrary and distinct. For an integer r>=2, +retain exactly r original children, in the order + +``` +y += a^3 +a += b +``` + +The eager comparator restores `a -= b` after each child, ending at +`(y+r*a^3,a,b)` in entry coordinates. A deferred program keeps every child +and then repairs both source and output. There is no intermediate observation, +output feedback into sources, nonlinear source change, output recoding or +access to child interiors. Coefficients are fixed independently of input data. +One signed weighted cube accumulation is one query. Reading b directly is +allowed and separately priced, as in PR6200; source changes and coefficient +preparation are additional work. All claims concern exact arithmetic, not +rounded execution, finite fields or a native implementation. + +**Theorem.** Two appended cube queries suffice over R if and only if there +exists a positive integer k such that + +``` +(2r-1)^2 - 6k^2 = 3 +``` + +and every prime divisor of k belongs to P. One query is always impossible. +This lower bound allows arbitrary nonmonic source forms and all GL_2(R) +source changes. The attaining program uses only integer source shears. + +**Dyadic consequences.** For R=Z[1/2], the minimum is two exactly at r=2. +It is exactly three for r>=5 with r=2 mod 3. For every remaining r>=3, +the minimum lies between three and four; no exact three-versus-four claim +is made here. In fact the upper constructions below use integer coefficients. + +## The forced two-query parameters + +Write entry sources as a,b. The unchanged deferred children add +sum_{i=0}^{r-1}(a+i*b)^3 and leave the actual source a+r*b. Their output +excess over the eager comparator is + +``` +f = 3S1*a^2*b + 3S2*a*b^2 + S1^2*b^3, +S1 = r(r-1)/2, S2 = r(r-1)(2r-1)/6. +``` + +This follows by the sums of first, second and third powers. Each source form +seen by an appended query has coefficients in R in entry coordinates, since +it is a row of a product of matrices over R. Thus q queries give a sum of q +R-weighted cubes representing -f. Changing all signs represents f instead. + +The following coefficient comparison is PR6200's rational argument. A single +cube cannot have zero a^3 coefficient and nonzero a^2*b coefficient. In any +two-cube representation, both weights and both a coefficients must be +nonzero, since otherwise the same contradiction holds. Normalize the a +coefficients over Q. Cancellation of a^3 gives opposite normalized weights: + +``` +f = lambda*((a+t*b)^3 - (a+s*b)^3), +lambda*(t-s)=S1, t+s=S2/S1, t^2+t*s+s^2=S1. +``` + +The directions are distinct. With n=2r-1, u=(t+s)/2 and h=(t-s)/2, + +``` +u=n/6, h^2=(2r^2-2r-1)/12, lambda=S1/(2h). +``` + +Ordering the directions gives h>0. Set k=2h. Then n^2-6k^2=3. If +k=A/B is reduced with B>0, integrality of 6A^2/B^2 implies B^2 divides 6, +so B=1. Conversely an integer k satisfying this equation yields the above +rational representation. No classification of all Pell solutions is needed. +The nonzero defect also excludes a zero-query repair. + +## Exact localization obstruction + +The Pell equation implies 3 divides n. Reducing modulo 4, since n is odd, +gives k odd. Hence n/3 and k are odd integers and the forced slopes are + +``` +t=(n/3+k)/2, s=(n/3-k)/2, +``` + +both integers. Moreover + +``` +4S1 = 3k^2+1, +``` + +so gcd(S1,k)=1. The reduced denominator of lambda=S1/k is therefore exactly +k. This is the prime-denominator obstruction missing from the rational test. + +It cannot be hidden by scaling a query. For any admissible term +gamma*(alpha*a+beta*b)^3 with nonzero alpha, its normalized weight is +gamma*alpha^3, which lies in R because gamma and alpha do. The ratio +beta/alpha need not lie in R and we do not assume it does. Nevertheless the +rational comparison forces the two normalized weights to be +lambda and +-lambda and their slopes to be the integers above. Necessarily lambda lies +in R. A reduced rational S1/k lies in Z[P^-1] exactly when every prime of k +is inverted. This proves necessity even for nonmonic forms and a larger +class of forms than actual source frames may realize. + +For sufficiency, from the actual final source a+r*b append + +``` +a += (t-r)*b +y -= lambda*a^3 +a += (s-t)*b +y += lambda*a^3 +a -= s*b +``` + +All shears have integer coefficients, each has determinant one, and both +query weights are in R. The source returns to entry a, b stays fixed, and +the output subtracts f. Omit exactly zero shifts. This is an admissible +two-query program for arbitrary incoming y,a,b, completing both directions. + +For dyadics, k must be a power of two and is odd, hence k=1. The equation +then forces n=3 and r=2. At r=2 the two queries have coefficients -1,+1; +the source shifts are -1,-1. For every r>2, at least three dyadic queries +are required even when two rational queries exist. + +## Three integer queries for r=2 mod 3 + +Set t=(r+1)/3 and s=(r-2)/3, so t-s=1 and both are integers in this class. +Expanding gives + +``` +f = S1*((a+t*b)^3 - (a+s*b)^3) + mu*b^3, +mu = S1*(r-2)*(r+1)/6 = 2*binom(r+1,4). +``` + +The last expression proves mu is an integer. It is positive for r>=5 +and zero at r=2. Append + +``` +a += (t-r)*b +y -= S1*a^3 +a -= b +y += S1*a^3 +a -= s*b +y -= mu*b^3 +``` + +At r=2 omit the zero shift and zero query. At r>=5 this is exactly three +queries and three shears, attaining the dyadic lower bound. For r=14: + +``` +a -= 9*b +y -= 91*a^3 +a -= b +y += 91*a^3 +a -= 4*b +y -= 2730*b^3 +``` + +PR6200's optimal rational repair uses two queries with weights +/-91/11. +Here k=11, so a dyadic repair cannot retain that count even with nonmonic +forms. The three-query integer repair is optimal in the dyadic alphabet. + +## Four integer queries for every r + +Let p=(S1+S2)/2=binom(r+1,3), m=(S2-S1)/2=binom(r,3), and +d=S1^2-S1. All are integers. Coefficient comparison proves + +``` +f = p*(a+b)^3 + m*(a-b)^3 - S2*a^3 + d*b^3. +``` + +From the actual drifting source append + +``` +a += (1-r)*b +y -= p*a^3 +a -= 2*b +y -= m*a^3 +a += b +y += S2*a^3 +y -= d*b^3 +``` + +The source returns to entry a before the last two queries; b is unchanged. +For r>=3 every displayed query coefficient is nonzero. Thus the construction +has four queries and three shears. At r=2 use the sharper program above. +The bracket outside r=2 mod 3 does not mean each such arity is unresolved. +For example, expansion gives the dyadic three-query identities + +``` +f_3 = (a+b)^3 + (a+2*b)^3 - 2*a^3, +f_4 = (5/2)*(a+2*b)^3 + (1/4)*(a+4*b)^3 - (11/4)*a^3. +``` + +Visit the displayed nonzero slopes in descending order and finish at slope +zero to restore the actual source. Thus these two arities also attain three. +We do not classify three-query attainability for all remaining arities. +Every event in every program is invertible, since its target is absent from +its source expression; reversal with negated coefficients is a literal inverse. +No entry snapshot, clean scratch, lost dirty value or change to an original +child is used. The identities and chronology prove the result for arbitrary +incoming values, beyond any finite verifier domain. + +## Paid boundary and limits + +Use PR6200's complete-event prices: Q_c^a(N) or Q_c^b(N) for a weighted cube +on its named source, and L_c(N) for `a += c*b`. A query includes its coefficient, +source access, private restoration and return. Zero events are omitted. +The eager bill is + +``` +r*Q_1^a + r*L_1 + r*L_-1. +``` + +The deferred bill retains r*Q_1^a+r*L_1 and adds every displayed repair event +at its own price. In the exact-three class, the increment is + +``` +L_(t-r) + Q_-S1^a + L_-1 + Q_S1^a + L_-s + Q_-mu^b. +``` + +The universal four-query increment is + +``` +L_(1-r) + Q_-p^a + L_-2 + Q_-m^a + L_1 + Q_S2^a + Q_-d^b. +``` + +At r=14 the integer repair replaces fourteen eager restoring shifts by +three shears and three additional cube queries. It saves eleven shift events; +it does not establish a cheaper execution. The distinct weights, coefficient +generation, routing, precision, storage, dispatch and controller preparation +still need a matched physical bill. If a backend can only cube a fixed +register, routing b into that register and restoring it must also be priced. +No such backend is supplied. Changing the permitted operations or allowing +child fusion is a different problem. No selected-frontier change follows. + +## Attribution + +Nick Petalas's PR6200 supplies the defect, rational lower bound, Pell criterion, +restoring-schedule pattern and the explicit dyadic open question. Those steps +are reproduced here to make the strengthened theorem self-contained, not +claimed as new. Sricharan Vagvala / theon199's PR1532 retains the quadratic +fixed-reader/paid-repair interface; Adam Gall / PR1205 and Hanson Sun / PR1246 +retain the linear deferral and repair lineage. Binary-form power decomposition +and elementary localization arguments are classical. No literature-priority +claim or independent human/formal-kernel acceptance is made. diff --git a/research/dyadic-cubic-repair/README.md b/research/dyadic-cubic-repair/README.md new file mode 100644 index 0000000000..de6b0954b4 --- /dev/null +++ b/research/dyadic-cubic-repair/README.md @@ -0,0 +1,151 @@ +# Dyadic coefficients for cubic-reader repair + +Prepared by **apoursh** with substantial OpenAI Codex assistance. Apache-2.0. +**Scoped proof with exact finite corroboration; no new kappa.** + +This answers the first open question of Nick Petalas's +[PR6200](https://github.com/CrocSwap/integer-mult-bounds/pull/6200), pinned at +`8b705d15869ba12d55adcb9075c68a2c7d44602d`. Retain every original child +`y += a^3; a += b`, then repair the source and output to the eager endpoint +on arbitrary incoming y,a,b. The predecessor proves that two rational cube +queries suffice exactly when `(2r-1)^2-6k^2=3` has an integer solution k. + +The new coefficient-ring classification is: + +- Over `Z[P^-1]`, two queries suffice exactly when that equation has a + positive integer solution k and every prime divisor of k is inverted. +- The obstruction applies to arbitrary nonmonic forms: rescaling cannot hide + the forced reduced weight denominator k. +- Over dyadics `Z[1/2]`, two queries suffice **only for r=2**. +- For r>=5 with r=2 mod 3, exactly **three integer-weighted queries** attain + the dyadic minimum. Four integer-weighted queries suffice for every r>=3. + Three dyadic queries also attain r=3 and r=4. A full classification of + three versus four for the other residue classes remains open here. + +[PROOF.md](PROOF.md) proves the all-r statements and gives the complete +source-restoring schedules. At r=14, the optimal rational repair uses weights +`+/-91/11`; dyadic coefficients require at least three queries. This integer +program attains three, starting from the actual drifted source `a_entry+14*b`: + +``` +a -= 9*b +y -= 91*a^3 +a -= b +y += 91*a^3 +a -= 4*b +y -= 2730*b^3 +``` + +Every one of the fourteen original cube children remains. The program replaces +fourteen eager restoration shifts with three shears and three extra cube +queries. This is an event-count comparison, not a runtime improvement. +Weighted query, coefficient preparation, source access, routing, private +restoration, precision, storage and dispatch costs still need a physical bill. +Reading b directly is in the predecessor's alphabet; a backend restricted to +one designated read register must also pay routing and its reversal. + +## Reproduce + +From the repository root with CPython 3.12 and the standard library: + +```sh +python3.12 -B scripts/research_package.py --package research/dyadic-cubic-repair +python3.12 -I -W error -B research/dyadic-cubic-repair/verify.py +python3.12 -I -O -W error -B research/dyadic-cubic-repair/verify.py +python3.12 -I -W error -B research/dyadic-cubic-repair/independent_check.py +python3.12 -I -O -W error -B research/dyadic-cubic-repair/independent_check.py +python3.12 -B scripts/check_research_commit.py --package research/dyadic-cubic-repair --check-source-history +``` + +The registered runner executes both checkers in normal and optimized modes. +Checks are exact, bounded and read-only. The written proof establishes the +universal lower bound and constructions; finite arithmetic scans do not prove +them by extrapolation. The independent checker is separately authored AI work, +not independent human or proof-kernel review. No predecessor executable is +imported, and no selected-supplier cold replay is claimed. + +The primary checker replays 255 universal integer programs (r=2..256) and +85 congruence-family programs, including every retained child, the eager +endpoint, source restoration and both literal inverses. Seven Pell fixtures +test the forced denominators; 584 nonmonic normalizations over 38 ring-case +iterations corroborate the localization argument. Ten semantic controls +detect changed query weights, omitted readers or restoration, reversed +chronology, an assumed entry snapshot, forbidden coefficients and feedback. + +The independent checker obtains the defect by binary concatenation of literal +reader blocks and fits cube weights by exact elimination. It checks 136 +arities, including eight Pell fixtures and three large arities, with 136 +four-form and 51 main-family replays, plus the r=3,4 examples. Four controls +test restoration, signs and hidden odd denominators. The distinct derivation +avoids importing the primary checker or predecessor code. + +Both registered normal/optimized replays passed locally on CPython 3.12.14, +macOS arm64. Separate copies with either retained source document corrupted +or the predecessor head changed are rejected. Committed-byte/mode/source-history +preflight, official export integrity and read-only Git-free replay are the +publication checks; their results are reported in the PR. + +## Sources, coordination and scope + +The retained [source proof](sources/pr6200-PROOF.md) and +[source README](sources/pr6200-README.md) preserve the precise pending contract, +open question, attribution and license for offline review. Their bytes were +compared exactly against the immutable raw URLs in +[SOURCE-PINS.json](SOURCE-PINS.json); the primary verifier checks both hashes. +The pending head is a source label, not an asserted ancestor of this branch. +It is not a Git source pin in SOURCES.json, and the source-history preflight +does not independently authenticate publication of that pending head. + +[SOURCES.json](SOURCES.json) pins the original card and selected record through +base `a5bff3bf133e482541c09eba4e773884bdb2b1b7`. All scientific runtime files +are package-local, so package changes trigger replay; there are no external +live inputs. Full source documents are retained for the cited contract, not +as a copied predecessor computation. The selected record remains PR6030, +`kappa=781451/250000000`, with its five framework assumptions unchanged. + +This is an explicitly changed scope of `joint-query-controller`: a nonlinear +coefficient-feasibility side result answering a concrete handoff. It does not +meet the card's complete supplier acceptance gate. A prior binding-only +orientation pass is reused after comparing all 1,227 covered paths against +the refreshed canonical base and finding no changes. No scientific replay +or assumption discharge is inferred from that reuse. + +The [canonical claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19275718) +records the investigation. Overlap coverage includes the newest twenty PRs +through #6211, all-state searches for `cubic dyadic`, `cubic repair` and `6200`, +and the newest fifteen visible handoffs. The local sparse helper searched +30 of 8,623 HEAD note paths and had no usable remote cache; this is not a +global novelty certificate. PR6200 explicitly leaves this question open. +PR6192/6208's linear cyclotomic operators and PR5084/5132's norm-six feature +factorization concern different objects; their computations are not combined. + +The contract excludes child fusion, intermediate observations, output feedback, +nonlinear source maps, approximate queries and finite fields. No actual native +caller, selected-supplier integration, favorable complete invoice, all-size +compiler, stock bound, Lean or Docker replay is supplied. Shared infrastructure, +predecessor packages, frozen evidence and selected frontier are unchanged. + +## Credit + +Nick Petalas retains PR6200's defect calculation, rational criterion, Pell +test, restoring-schedule method and dyadic handoff. Sricharan Vagvala / +theon199 retains PR1532's quadratic fixed-reader/paid-repair interface; +Adam Gall / PR1205 and Hanson Sun / PR1246 retain the linear lineage. +Classical binary-form decompositions and elementary localization retain their +background credit. No general Waring-rank theorem or historical priority is +claimed. OpenAI Codex assisted derivation, proof, separately authored checkers, +mathematical audit, documentation and publication for apoursh. + +## Open next questions + +1. **Which further arities admit three dyadic queries?** The proof includes + r=3 and r=4 examples outside the main congruence family. Start with the + three-form coefficient equations, allowing nonmonic forms and using prime + valuations to derive further families or an obstruction. A failed monic + or finite search would not settle the remaining three-versus-four gap. +2. **Can an actual r=14 caller benefit?** First pin the indivisible child + interface and price every event in the displayed program and eager + comparator. The missing backend and complete favorable bill block any + claim of paid-work or multiplication-bound improvement. + +Structured relevance, first steps and blockers are in [TASK.json](TASK.json). diff --git a/research/dyadic-cubic-repair/SOURCE-PINS.json b/research/dyadic-cubic-repair/SOURCE-PINS.json new file mode 100644 index 0000000000..92de9b2545 --- /dev/null +++ b/research/dyadic-cubic-repair/SOURCE-PINS.json @@ -0,0 +1,23 @@ +{ + "schema_version": 1, + "predecessor": { + "pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/6200", + "head": "8b705d15869ba12d55adcb9075c68a2c7d44602d", + "author": "Nick Petalas", + "license": "Apache-2.0" + }, + "documents": [ + { + "path": "sources/pr6200-PROOF.md", + "source_path": "research/cubic-reader-rational-repair/PROOF.md", + "source_url": "https://raw.githubusercontent.com/CrocSwap/integer-mult-bounds/8b705d15869ba12d55adcb9075c68a2c7d44602d/research/cubic-reader-rational-repair/PROOF.md", + "sha256": "f0a5a46a034f51b18d30155cc7a8e64975b8d83e1067e5b10380edba10853b2d" + }, + { + "path": "sources/pr6200-README.md", + "source_path": "research/cubic-reader-rational-repair/README.md", + "source_url": "https://raw.githubusercontent.com/CrocSwap/integer-mult-bounds/8b705d15869ba12d55adcb9075c68a2c7d44602d/research/cubic-reader-rational-repair/README.md", + "sha256": "934265233487d863b153898f3384278737c4077f6a7f87e9d7f38b4567ce9de4" + } + ] +} diff --git a/research/dyadic-cubic-repair/SOURCES.json b/research/dyadic-cubic-repair/SOURCES.json new file mode 100644 index 0000000000..75db18102e --- /dev/null +++ b/research/dyadic-cubic-repair/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7", + "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" + } + ] +} diff --git a/research/dyadic-cubic-repair/TASK.json b/research/dyadic-cubic-repair/TASK.json new file mode 100644 index 0000000000..6ee52c3760 --- /dev/null +++ b/research/dyadic-cubic-repair/TASK.json @@ -0,0 +1,110 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 8, + "base_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7", + "original_card": { + "id": "joint-query-controller", + "question": "Can a changed query demand or caller remove real work while satisfying native chronology and restoration?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose an exact caller and a new demand/interface hypothesis. Read the scoped #5617/#5631/#5649/#5747 and #5720/#5745 objections before rebuilding an excluded schedule. Compare the complete matched source/consumer protocols including all retained helper outputs. For an active-mode injection, first check #5745: its canonical delivery claim repays the eight removed centre jobs. Audit that exact claim or change its channel/feedback hypothesis; do not repeat the same free-injection search. Stop if the full favorable budget fails or the required restored output is unobservable.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "query demand", + "active mode", + "5720", + "5745", + "5747", + "caller" + ], + "existing_checks": [ + { + "scope": "PR #4166: author-checked installed producer/service/return/bridge connection; native-component comparison loses.", + "evidence": "research/qq16-caller-install/README.md", + "remaining": "Complete matched physical protocol bill, or changed source-compatible demand/circuit; no affordable supplier yet.", + "status": "author-checked", + "source_commit": "0b082d22a0e9a442d264ab0633e35ef26c790630", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Answer PR6200 open question 1: classify two-query cubic-reader repair over Z[P^-1], including arbitrary nonmonic source forms; derive dyadic exact-two and exact-three cases and integer all-r upper bounds.", + "scope_change_reason": "A bounded algebraic interface side result following the explicit PR6200 handoff, instead of a selected-supplier complete-budget construction. The card-level supplier acceptance gate is not claimed.", + "bottleneck_link": "Coefficient restrictions can invalidate a query-count saving when fixed original readers are retained and their source restored. This identifies that obstruction and an attaining alternative; no actual supplier or favorable complete physical bill is identified.", + "budget_minutes": 60, + "stop_rule": "Stop after the denominator theorem, restoring schedules, independent finite checks and scoped publication. Do not expand into native construction or claim savings without a source-bound caller and complete favorable bill.", + "outcome": "completed", + "evidence": "PROOF.md supplies the all-r theorem. verify.py and independent_check.py provide separately authored exact finite polynomial, chronological and arithmetic checks with rejection controls. Neither finite replay nor separate AI review is human or formal-kernel acceptance.", + "author": "apoursh", + "ai_assistance": "Substantial OpenAI Codex assistance in derivation, proof, implementation, separately authored verification, mathematical audit, packaging and publication; prepared by apoursh.", + "open_questions": [ + { + "question": "Which further arities admit three dyadic queries, beyond r=2 mod 3 and the explicit r=3,4 examples?", + "why_it_matters": "The theorem leaves a one-query gap in these arities while settling the rational two-query transfer question.", + "first_step": "Analyze the three-form coefficient equations with arbitrary nonmonic dyadic forms and prime valuations; derive further families or an obstruction. A failed monic or finite search cannot exclude all physical rescalings.", + "blocked_by": "A complete classification across all remaining arities is not supplied; some individual examples outside the main congruence family already attain three." + }, + { + "question": "Does an actual caller with indivisible cubic readers make the integer r=14 repair cheaper?", + "why_it_matters": "Replacing eleven source-shift events by three weighted cube queries does not itself lower paid work or improve kappa.", + "first_step": "Pin one actual child interface and compare the complete eager and deferred tariffs, including Q^a_-91,Q^a_91,Q^b_-2730,L_-9,L_-1,L_-4 and all coefficient, routing, precision, restoration and dispatch costs.", + "blocked_by": "No admitted backend, native implementation or favorable complete matched bill is known in this package; stop construction expansion until these are specified." + } + ], + "selection": { + "kind": "explicit-open-handoff", + "predecessor_pr": 6200, + "task_card_seed": "8d6e875b922c69692e102c1c465811d6", + "note": "Same selected card and seed rebound to refreshed base after leaving the prior contribution branch; no reroll." + }, + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19275718", + "coverage": "Newest 20 PRs through 6211; all-state queries cubic dyadic, cubic repair and 6200; newest 15 visible handoffs. Sparse local helper searched 30 of 8623 HEAD note paths; 8593 unsearched, no usable remote cache. This is bounded coverage, not a novelty certificate.", + "nearest": "Nick Petalas PR6200 explicitly asks the dyadic denominator question. PR6192/6208 concern linear cyclotomic Clifford operators; PR5084/5132 concern a distinct norm-six feature factorization. No computations or savings are combined.", + "completion_refresh": "Canonical main and PR6200 head unchanged before publication; latest twenty PRs still end at #6211 and the newest fifteen visible #1166 comments include this claim with no later competing claim. Bounded coverage only." + }, + "orientation": { + "kind": "source-bound-reuse-bindings-only", + "prior_base": "3f0152a32eeebac0df11946dbd50cabe5a7f7839", + "current_base": "a5bff3bf133e482541c09eba4e773884bdb2b1b7", + "coverage_paths": 1227, + "invalidation": "Rerun if any covered selected source, baseline helper/dependency, selected record, catalogue or guidance path changes. All 1227 covered paths are unchanged in Git at the current base. This reuse is not a scientific cold replay.", + "selected": "PR6030, kappa=781451/250000000; five framework assumptions remain unchanged." + } +} diff --git a/research/dyadic-cubic-repair/VERIFY.json b/research/dyadic-cubic-repair/VERIFY.json new file mode 100644 index 0000000000..090a566d12 --- /dev/null +++ b/research/dyadic-cubic-repair/VERIFY.json @@ -0,0 +1,59 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact chronological cubic maps, integer/dyadic coefficient checks, source hashes and semantic rejection controls. Normal execution." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact chronological cubic maps, integer/dyadic coefficient checks, source hashes and semantic rejection controls. Optimized execution." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/independent_check.py" + ], + "timeout_seconds": 120, + "checks": "Independent polynomial and coefficient-system derivation; exact source restoration and arithmetic controls. Normal execution." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/independent_check.py" + ], + "timeout_seconds": 120, + "checks": "Independent polynomial and coefficient-system derivation; exact source restoration and arithmetic controls. Optimized execution." + } + ] +} diff --git a/research/dyadic-cubic-repair/independent_check.py b/research/dyadic-cubic-repair/independent_check.py new file mode 100644 index 0000000000..540f122389 --- /dev/null +++ b/research/dyadic-cubic-repair/independent_check.py @@ -0,0 +1,305 @@ +#!/usr/bin/env python3 +"""Independent finite audit of dyadic cubic repair, using exact polynomials. + +Prepared by apoursh with substantial OpenAI Codex assistance. Apache-2.0. +The chronological interface and rational two-query criterion are credited to +Nick Petalas's PR6200 and its retained predecessors. This checker imports no +primary verifier and does not infer an all-arity theorem from a finite scan. +""" + +import json +from fractions import Fraction +from math import gcd, isqrt + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +# Sparse polynomials in three free variables: entry a, unchanged b, entry y. +ONE = {(0, 0, 0): Fraction(1)} +A = {(1, 0, 0): Fraction(1)} +B = {(0, 1, 0): Fraction(1)} +Y = {(0, 0, 1): Fraction(1)} +CUBIC_MONOMIALS = [(3, 0, 0), (2, 1, 0), (1, 2, 0), (0, 3, 0)] + + +def plus(left, right): + answer = dict(left) + for exponent, coefficient in right.items(): + answer[exponent] = answer.get(exponent, Fraction(0)) + coefficient + return {exponent: coefficient for exponent, coefficient in answer.items() if coefficient} + + +def times_scalar(coefficient, polynomial): + return {exponent: coefficient * value for exponent, value in polynomial.items() + if coefficient * value} + + +def times(left, right): + answer = {} + for e, u in left.items(): + for f, v in right.items(): + exponent = tuple(x + y for x, y in zip(e, f, strict=True)) + answer[exponent] = answer.get(exponent, Fraction(0)) + u * v + return {exponent: coefficient for exponent, coefficient in answer.items() if coefficient} + + +def power(polynomial, exponent): + answer = ONE + for _ in range(exponent): + answer = times(answer, polynomial) + return answer + + +def translate_a(polynomial, offset): + source = plus(A, times_scalar(offset, B)) + answer = {} + for exponent, coefficient in polynomial.items(): + term = times(times(power(source, exponent[0]), power(B, exponent[1])), + power(Y, exponent[2])) + answer = plus(answer, times_scalar(coefficient, term)) + return answer + + +def chronological_state(arity): + # Build sum_{j=0}^{r-1}(a+j*b)^3 by concatenating binary-sized blocks. + # This executes the reader-before-shift chronology without Faulhaber formulas. + remaining, width, offset = arity, 1, 0 + block, accumulated = power(A, 3), {} + while remaining: + if remaining & 1: + accumulated = plus(accumulated, translate_a(block, offset)) + offset += width + remaining //= 2 + if remaining: + block = plus(block, translate_a(block, width)) + width *= 2 + require(offset == arity, "binary ladder consumed the exact arity") + return {"a": plus(A, times_scalar(arity, B)), "b": B, + "y": plus(Y, accumulated)} + + +def target_state(arity): + return {"a": A, "b": B, "y": plus(Y, times_scalar(arity, power(A, 3)))} + + +def dyadic(value): + denominator = Fraction(value).denominator + return denominator & (denominator - 1) == 0 + + +def execute(state, program, dyadic_only=True): + state = dict(state) + for instruction, coefficient in program: + coefficient = Fraction(coefficient) + require(not dyadic_only or dyadic(coefficient), "instruction coefficient is not dyadic") + if instruction == "shift": + state["a"] = plus(state["a"], times_scalar(coefficient, state["b"])) + elif instruction == "source_cube": + state["y"] = plus(state["y"], times_scalar(coefficient, power(state["a"], 3))) + elif instruction == "b_cube": + state["y"] = plus(state["y"], times_scalar(coefficient, power(state["b"], 3))) + else: + raise ValueError("unknown instruction") + return state + + +def solve_weights(target, linear_forms): + # Independent coefficient fitting by elimination, with all four equations. + cubes = [power(form, 3) for form in linear_forms] + rows = [[cube.get(monomial, Fraction(0)) for cube in cubes] + + [target.get(monomial, Fraction(0))] for monomial in CUBIC_MONOMIALS] + pivot_rows = [] + for column in range(len(cubes)): + pivot = next((i for i in range(len(pivot_rows), len(rows)) if rows[i][column]), None) + if pivot is None: + return None + index = len(pivot_rows) + rows[index], rows[pivot] = rows[pivot], rows[index] + divisor = rows[index][column] + rows[index] = [value / divisor for value in rows[index]] + for i in range(len(rows)): + if i != index: + coefficient = rows[i][column] + rows[i] = [x - coefficient * y + for x, y in zip(rows[i], rows[index], strict=True)] + pivot_rows.append(index) + if any(all(value == 0 for value in row[:-1]) and row[-1] for row in rows): + return None + answer = [rows[index][-1] for index in pivot_rows] + reconstructed = {} + for coefficient, cube in zip(answer, cubes, strict=True): + reconstructed = plus(reconstructed, times_scalar(coefficient, cube)) + require(reconstructed == target, "fitted cubes reproduce every polynomial coefficient") + return answer + + +def form(slope): + return plus(A, times_scalar(slope, B)) + + +def compact(program): + return [(operation, Fraction(coefficient)) for operation, coefficient in program if coefficient] + + +def four_program(arity, defect): + weights = solve_weights(defect, [form(1), form(-1), A, B]) + require(weights is not None and all(value.denominator == 1 for value in weights), + "universal four-form coefficients are integers") + program = [("shift", 1 - arity), ("source_cube", -weights[0]), + ("shift", -2), ("source_cube", -weights[1]), + ("shift", 1), ("source_cube", -weights[2]), ("b_cube", -weights[3])] + return compact(program), weights + + +def three_program(arity, defect): + require(arity % 3 == 2, "three-form family arity") + high, low = (arity + 1) // 3, (arity - 2) // 3 + weights = solve_weights(defect, [form(high), form(low), B]) + require(weights is not None and all(value.denominator == 1 for value in weights), + "three-form coefficients are integers") + program = [("shift", high - arity), ("source_cube", -weights[0]), + ("shift", low - high), ("source_cube", -weights[1]), + ("shift", -low), ("b_cube", -weights[2])] + return compact(program), weights + + +def rational_root(value): + numerator, denominator = value.numerator, value.denominator + if numerator < 0: + return None + p, q = isqrt(numerator), isqrt(denominator) + return Fraction(p, q) if p * p == numerator and q * q == denominator else None + + +def two_query_candidate(arity, defect): + k = rational_root(Fraction(2 * arity * arity - 2 * arity - 1, 3)) + if k is None: + return None + n = 2 * arity - 1 + require(k.denominator == 1 and k.numerator % 2 == 1, "integral odd Pell parameter") + k = k.numerator + require(n * n - 6 * k * k == 3 and n % 3 == 0, "Pell equation and slope divisibility") + high, low = (Fraction(n, 3) + k) / 2, (Fraction(n, 3) - k) / 2 + require(high.denominator == low.denominator == 1, "two normalized slopes are integers") + weights = solve_weights(defect, [form(high), form(low)]) + require(weights is not None and weights[0] == -weights[1], "forced opposite weights") + s1 = Fraction(defect[(2, 1, 0)], 3) + require(s1.denominator == 1 and gcd(k, s1.numerator) == 1, "Pell weight coprimality") + require(weights[0] == s1 / k and weights[0].denominator == k, "forced reduced denominator") + program = compact([("shift", high - arity), ("source_cube", -weights[0]), + ("shift", low - high), ("source_cube", -weights[1]), ("shift", -low)]) + return {"k": k, "weights": weights, "program": program} + + +def inspect_arity(arity): + chronological, target = chronological_state(arity), target_state(arity) + defect = plus(chronological["y"], times_scalar(-1, target["y"])) + s1, s2 = arity * (arity - 1) // 2, arity * (arity - 1) * (2 * arity - 1) // 6 + expected = {(2, 1, 0): Fraction(3 * s1), (1, 2, 0): Fraction(3 * s2), + (0, 3, 0): Fraction(s1 * s1)} + require(defect == expected, "literal ladder agrees with cited defect") + require((3, 0, 0) not in defect and defect[(2, 1, 0)] != 0, + "one-cube coefficient obstruction at this arity") + program, weights = four_program(arity, defect) + require(execute(chronological, program) == target, "universal four schedule restores a,b,y") + require(weights == [Fraction(s1 + s2, 2), Fraction(s2 - s1, 2), -s2, s1 * s1 - s1], + "independently fitted universal coefficients") + require((s1 - s2) % 2 == 0, "integer parity improvement over merely dyadic coefficients") + candidate = two_query_candidate(arity, defect) + two_dyadic = False + if candidate is not None: + require(execute(chronological, candidate["program"], False) == target, + "rational two-cube schedule restores all outputs") + two_dyadic = all(dyadic(value) for value in candidate["weights"]) + require(two_dyadic == (arity == 2), "dyadic two-query eligibility on checked arities") + three_count = None + if arity % 3 == 2: + program, weights = three_program(arity, defect) + require(execute(chronological, program) == target, "integer three-form schedule restores all outputs") + three_count = sum(operation.endswith("cube") for operation, _ in program) + require(three_count == (2 if arity == 2 else 3), "nonzero query count") + require(arity == 2 or not two_dyadic, "three-query optimality corroboration") + return {"rational_two": candidate is not None, "dyadic_two": two_dyadic, + "three_family": three_count is not None, "three_query": three_count == 3} + + +def exceptional_three_examples(): + programs = { + 3: [("shift", -1), ("source_cube", -1), + ("shift", -1), ("source_cube", -1), + ("shift", -1), ("source_cube", 2)], + 4: [("source_cube", Fraction(-1, 4)), ("shift", -2), + ("source_cube", Fraction(-5, 2)), ("shift", -2), + ("source_cube", Fraction(11, 4))], + } + for arity, program in programs.items(): + require(sum(operation == "source_cube" for operation, _ in program) == 3, + "exceptional example uses exactly three cube queries") + require(execute(chronological_state(arity), program) == target_state(arity), + "exceptional three-query schedule restores the entire arbitrary-input state") + return sorted(programs) + + +def controls(): + arity = 14 + initial, target = chronological_state(arity), target_state(arity) + program = [("shift", -9), ("source_cube", -91), ("shift", -1), + ("source_cube", 91), ("shift", -4), ("b_cube", -2730)] + require(execute(initial, program) == target, "literal r14 integer program") + no_restore = execute(initial, program[:4] + program[5:]) + require(no_restore["y"] == target["y"] and no_restore["a"] != A and no_restore["b"] == B, + "missing source restoration remains observable despite correct accumulator") + wrong_sign = list(program) + wrong_sign[1] = ("source_cube", 91) + require(execute(initial, wrong_sign)["y"] != target["y"], "wrong cube sign is detected") + defect = plus(initial["y"], times_scalar(-1, target["y"])) + rational = two_query_candidate(arity, defect) + require(rational["weights"][0] == Fraction(91, 11), "r14 forbidden prime fixture") + try: + execute(initial, rational["program"]) + except ValueError as error: + require(str(error) == "instruction coefficient is not dyadic", "precise coefficient rejection") + else: + raise ValueError("forbidden 91/11 rational repair accepted as dyadic") + gamma, alpha, beta = Fraction(91, 88), Fraction(2), Fraction(20) + physical = times_scalar(gamma, power(plus(times_scalar(alpha, A), times_scalar(beta, B)), 3)) + normalized = times_scalar(Fraction(91, 11), power(form(10), 3)) + require(physical == normalized, "nonmonic rescaling preserves the forbidden normalized weight") + require(dyadic(alpha) and dyadic(beta) and not dyadic(gamma) + and gamma * alpha ** 3 == Fraction(91, 11), "scaled query does not hide the odd prime") + return ["missing_final_source_restore", "wrong_cube_sign", "forbidden_91_over_11", + "nonmonic_91_over_88_hidden_denominator"] + + +def main(): + pell_arities = [] + n, k = 3, 1 + for _ in range(8): + require(n * n - 6 * k * k == 3, "generated Pell fixture") + pell_arities.append((n + 1) // 2) + n, k = 5 * n + 12 * k, 2 * n + 5 * k + large_arities = [10 ** 6, 10 ** 12 + 1, 2 ** 128 + 1] + arities = sorted(set(range(2, 129)) | set(pell_arities) | set(large_arities)) + results = {arity: inspect_arity(arity) for arity in arities} + exceptional = exceptional_three_examples() + rejected = controls() + summary = {"status": "finite independent exact polynomial evidence", + "arity_count": len(arities), "consecutive_arities": "2..128", + "pell_arities": pell_arities, "large_arities": large_arities, + "whole_state_four_form_replays": len(results), + "whole_state_three_family_replays": sum(item["three_family"] for item in results.values()), + "exact_three_family_cases": sum(item["three_query"] for item in results.values()), + "exceptional_three_examples": exceptional, + "rational_two_candidate_replays": sum(item["rational_two"] for item in results.values()), + "dyadic_two_arities_checked": [arity for arity, item in results.items() if item["dyadic_two"]], + "controls": rejected, "control_count": len(rejected), + "formal_kernel_or_all_arity_scan_proof": False} + print(json.dumps(summary, sort_keys=True)) + print("PASS_INDEPENDENT_DYADIC_CUBIC_REPAIR") + + +if __name__ == "__main__": + main() diff --git a/research/dyadic-cubic-repair/sources/pr6200-PROOF.md b/research/dyadic-cubic-repair/sources/pr6200-PROOF.md new file mode 100644 index 0000000000..7209cd0473 --- /dev/null +++ b/research/dyadic-cubic-repair/sources/pr6200-PROOF.md @@ -0,0 +1,195 @@ +# Exact rational cube-query repair + +This scoped proof is produced by Nick Petalas. Apache-2.0. + +## Contract and theorem + +Work over Q. The distinct streams y,a,b have arbitrary incoming values. For an +integer r>=2 retain exactly r original children, each performing + +``` +y += a^3 +a += b +``` + +The eager program follows every child by `a -= b`. Its endpoint is +`(y+r*a^3,a,b)`, in entry coordinates. The deferred program retains all the +children and appends a repair. It must have the same endpoint for every input. +There is no intermediate observation and no feedback from y into a or b. + +A repair may apply invertible rational linear changes to the source pair and +add signed, rationally weighted cubes of source linear forms to y. Each such +cube accumulation is one query, including its coefficient. Source changes and +coefficient preparation are additional work. The attaining programs use only +`a += c*b`, preserve b throughout, and explicitly restore a. The lower bound +allows the larger class of all rational source linear forms, so it applies to +these programs too. Extra nonlinear operations, access to original child +interiors, output recoding and output-dependent source changes are excluded. + +**Theorem.** The exact minimum number of appended cube queries is + +``` +2, if q_r = (2r^2-2r-1)/12 is a rational square; +3, otherwise. +``` + +Over R the minimum is always two. In particular r=3 needs three rational +queries, while r=14 needs two. This is a query lower bound and an attaining +restoring program in a declared alphabet, not an arithmetic-circuit lower +bound or a complete supplier cost. + +## Derive the chronological defect + +Child i, indexed from zero, observes `a+i*b` in entry coordinates. Thus the +unrepaired deferred output differs from the eager output by + +``` +f(a,b) = 3S1*a^2*b + 3S2*a*b^2 + S3*b^3, +S1 = r(r-1)/2, +S2 = r(r-1)(2r-1)/6, +S3 = S1^2. +``` + +These expressions follow by expanding each of the r cubes and summing i, +i^2 and i^3 for 0<=i0. + +Every appended source transformation is independent of y and linear in entry +a,b. Consequently any q-query repair represents -f as a sum of q signed +weighted cubes of rational linear forms. Multiple queries in the same +direction can be combined for a lower-bound argument. Any additional linear +output terms cannot change these homogeneous cubic coefficients. + +## Necessity of the rational-square criterion + +One cube cannot represent f. Its zero a^3 coefficient would force its a +coefficient to vanish, contradicting the nonzero a^2*b coefficient. + +Suppose two cubes represent f. Neither linear form can have zero a +coefficient, since the remaining cube would then have a nonzero a^3 +coefficient. Normalize both a coefficients to one, absorbing their cubes +into their rational weights. Cancellation of a^3 makes the weights opposite. +The two directions must be distinct. We therefore have + +``` +f = lambda*((a+t*b)^3 - (a+s*b)^3), t != s. +``` + +Coefficient comparison gives + +``` +lambda*(t-s) = S1, +t+s = S2/S1, +t^2+t*s+s^2 = S3/S1. +``` + +Put `u=(t+s)/2` and `h=(t-s)/2`. The equations become + +``` +u = S2/(2S1), +h^2 = S3/S1 - 3u^2 = (2r^2-2r-1)/12 = q_r. +``` + +If t,s are rational, h is rational. Conversely, if q_r is a rational square, +take its positive rational square root h, set t=u+h, s=u-h, and +`lambda=S1/(2h)`. These choices satisfy all four cubic coefficients. Since +q_r>0 for r>=2, h is nonzero. This proves both directions and the two-query +minimum whenever the square criterion holds. Over R, the positive root always +exists, proving the real statement too. + +## An explicit three-query repair and source restoration + +For any nonzero rational h, direct expansion gives + +``` +f = S1/(2h)*((a+(u+h)*b)^3 - (a+(u-h)*b)^3) + + (S3-3S1*u^2-S1*h^2)*b^3. +``` + +If the square criterion fails, choose h=1. The last coefficient is nonzero, +since otherwise q_r=1 would be a square. This gives exactly three queries. +Starting from the actual drifting source `a+r*b`, append + +``` +a += (u+h-r)*b +y -= S1/(2h)*a^3 +a -= 2h*b +y += S1/(2h)*a^3 +a -= (u-h)*b +y -= (S3-3S1*u^2-S1*h^2)*b^3 +``` + +Omit the final cube only when its coefficient is zero, and omit exactly zero +shifts. The first two cube inputs are the required entry-coordinate forms. +The fifth event returns a to its entry value; b never changes. Subtracting f +gives the eager y endpoint for arbitrary incoming y,a,b. Every event is +invertible because its target is absent from its source expression. Reversing +event order and negating coefficients is a literal inverse. No clean state, +copy, hidden source snapshot or discarded dirty value is used. + +For r=3, u=5/6 and q_r=11/12. The six repair events have shift coefficients +`-7/6,-2,1/6` and cube coefficients `-3/2,3/2,1/4`, the last reading b. +For r=14, u=9/2 and h=11/2. The five repair events are + +``` +a -= 4*b +y -= (91/11)*a^3 +a -= 11*b +y += (91/11)*a^3 +a += b +``` + +Both examples restore the actual source, rather than assuming an entry copy. + +## An integer decision criterion + +The square condition is equivalently the existence of an integer k with + +``` +(2r-1)^2 - 6k^2 = 3. +``` + +Indeed `q_r=((2r-1)^2-3)/24`. If its reduced rational square root is A/B, +then B^2 divides 24, so B divides 2. Hence k=2A/B is an integer. The converse +uses the root k/2. This is a decision criterion, not a classification of all +solutions of the Pell-type equation. The bounded checker enumerates arities; +the all-r result is the coefficient proof above. + +## Complete logical event bill and boundaries + +Let `Q_c(N)` price a complete `y += c*a^3` child on N coordinates, including +its coefficient, source access, private restoration and return. Let `L_c(N)` +price a complete `a += c*b`. A b-cube uses the corresponding complete query +price with b as source. Set the prices of omitted zero operations to zero. +Then the eager program costs exactly + +``` +r*Q_1(N) + r*L_1(N) + r*L_-1(N). +``` + +The deferred program costs exactly `r*Q_1(N)+r*L_1(N)` plus every displayed +repair event at its own price. In particular r=14 adds `Q_-91/11 + Q_91/11` +and `L_-4 + L_-11 + L_1`. Its original fourteen cube children all remain. +It saves eleven source-shift events and adds two cube-query events, with +nonunit rational coefficients. Query counts alone do not establish a saving. +Coefficient generation, routing, precision, storage and controller preparation +are additional obligations. No numerical backend price is substituted here. + +The fixed original calls are essential. If they can be opened, the target +`y += r*a^3` can be computed directly and no deferral comparison is needed. +The all-r statement is exact rational arithmetic. Approximate queries, finite +fields, nonlinear source maps and intermediate observations are outside it. +No selected assumption, physical supplier or multiplication theorem is proved. + +## Credit + +Sricharan Vagvala / theon199's [PR #1532](https://github.com/CrocSwap/integer-mult-bounds/pull/1532) +provides the quadratic fixed-reader/paid-repair interface and its sharp +square-query floor. Adam Gall / PR1205 and Hanson Sun / PR1246 retain the +underlying linear deferral and paid repair lineage. Their computations are +cited, not replayed as a deliverable here. + +Binary-form power decomposition is classical. Carlini, Catalisano and Geramita's +[monomial Waring-rank paper](https://arxiv.org/abs/1110.0745) is relevant +background; this proof does not claim a new general Waring-rank theorem. +The contribution is the exact arithmetic-sensitive cubic-reader criterion, +its rational restoring schedules and the stated interface cost consequence. diff --git a/research/dyadic-cubic-repair/sources/pr6200-README.md b/research/dyadic-cubic-repair/sources/pr6200-README.md new file mode 100644 index 0000000000..3522d487b6 --- /dev/null +++ b/research/dyadic-cubic-repair/sources/pr6200-README.md @@ -0,0 +1,126 @@ +# Exact rational query cost for cubic-reader repair + +This contribution is produced by Nick Petalas. Apache-2.0. +Independent human and formal proof-kernel review are unclaimed. + +**Scoped proof with exact finite corroboration. No new kappa.** For every +integer r>=2, retain r children `y += a^3; a += b` and defer their source +restorations. The minimum appended signed cube-query count over rational +source linear forms is exactly two if + +``` +(2r^2-2r-1)/12 is a rational square, +``` + +and exactly three otherwise. Over the reals it is always two. Thus rational +source frames impose a cost invisible in the real relaxation. [PROOF.md](PROOF.md) +derives the defect, proves necessity by coefficient comparison, constructs +attaining schedules and includes every source restoration. + +The first discriminator is r=3, whose criterion value is 11/12. Its rational +repair needs three queries. At r=14 the value is 121/4, and the optimal repair +from the actual final source `a_entry+14*b` is + +``` +a -= 4*b +y -= (91/11)*a^3 +a -= 11*b +y += (91/11)*a^3 +a += b +``` + +Every source and output starts arbitrary; b stays unchanged. Original child +calls remain intact. No entry snapshot or clean scratch is assumed. The +fourteen-child program saves eleven source-shift events and adds two cube +queries. Its complete backend tariff still includes the displayed nonunit +coefficients, private restoration, source access and physical implementation. +This is not a claim that the resulting program is cheaper. + +## Reproduce + +From the repository root, using CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/cubic-reader-rational-repair/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/cubic-reader-rational-repair/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/cubic-reader-rational-repair +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/cubic-reader-rational-repair --check-source-history +``` + +Replace the absolute interpreter path with a local CPython 3.12 executable on +another machine. The direct success marker is +`PASS_CUBIC_READER_RATIONAL_REPAIR`, in a generated JSON receipt bound to the +SHA256 hashes of all six package files. No receipt is hand-written and the +verifier writes nothing. Both registered commands have a 120-second limit. + +[verify.py](verify.py) checks eager, repaired and inverse maps by full cubic +polynomial convolution, rather than relying on coordinate-basis inputs. It +also executes dirty integer and rational triples, scans the square criterion +through r=10,000, and compares both directions of the two-cube coefficient +equations on a fixed rational slope set. The scan lists the exact two-query +arities in its bounded domain. The all-r lower bound rests on the written +proof, not extrapolation from that scan. Mutation controls omit restoration, +omit or reverse the last cube correction, and reverse chronology; separate +controls check the arithmetic boundary and the failure of basis-only tests. + +## Provenance and limits + +This changes the `joint-query-controller` card to a self-contained nonlinear +interface side result. Its connection is the cost of preserving original +recursive calls while repairing their shared source at a later boundary. +No current supplier with these indivisible cubic readers is identified. +The positive-control command `scripts/research_selected_baseline.py` passed +with `PASS_RESEARCH_BASELINE_BINDINGS_ONLY`. That is orientation, not a +scientific replay. At canonical base +`a5bff3bf133e482541c09eba4e773884bdb2b1b7`, priority revision 8, the selected +record resolves to PR6030, kappa .003125804. Older priority prose still names +PR5599; this package follows the selected record and changes neither. + +Credit Sricharan Vagvala / theon199's [PR #1532](https://github.com/CrocSwap/integer-mult-bounds/pull/1532) +for the quadratic fixed-reader/paid-repair interface and its square-query +floor, Adam Gall / PR1205 for linear observation, and Hanson Sun / PR1246 for +paid linear repair. Their computations are cited premises, not rechecked +deliverables. Classical binary-form power decompositions retain their credit, +including Carlini, Catalisano and Geramita's +[Waring-rank work](https://arxiv.org/abs/1110.0745). No general Waring-rank +theorem or literature-priority claim is made. The new result is the exact +arithmetic-sensitive cubic interface criterion and its restoring schedules. + +[SOURCES.json](SOURCES.json) pins the predecessor README, task card and selected +record as historical provenance. There are no external scientific runtime +inputs and no predecessor program is imported. Live PRs, current handoffs, +local reservations, recent account work and merged README/PR searches were +checked. The overlap cache's sparse local-note inventory is incomplete, so +absence of a match is not proof of novelty. The +[advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19272267) +states the same delivered mathematical scope. + +The theorem excludes output feedback, altered child interiors, intermediate +observations, nonlinear source maps, approximate queries and finite fields. +Source-frame and coefficient work is paid separately from query count. No +physical native realization, precision or stock bound, all-size compiler, +complete caller invoice, selected assumption discharge, Lean build, Docker +replay or complete multiplication theorem is supplied. + +The verifier has no recursion, subprocess, dynamic evaluation or input CLI. +Its arities are bounded by 10,000, full polynomial programs by r=64, and +numeric programs by r=32. States contain at most five cubic monomials; all +event lists have finite capacities derived from these bounds. Every function +is below sixty lines and checks use explicit exceptions under optimized Python. +Python managed allocation is a Power of Ten rule 3 deviation, bounded by the +fixed fixture sizes. The two callback targets used only for rejection controls +are a rule 9 deviation. Warning-strict normal and optimized replay provide the +available diagnostics; no external static analyzer or proof kernel is claimed. + +## Open next questions + +1. Which admissible dyadic coefficients permit the same two-query minimum? + Rational square roots alone do not ensure that query weights and source + shifts are dyadic. Start with the two normalized slopes and weight forced + by the proof. The missing step is a prime-denominator classification. +2. Does an actual recursive supplier expose indivisible cubic readers for + which the complete r=14 tariff beats eager restoration? Start by pinning + its child return map and pricing every displayed query and source shift. + No such admitted backend or physical coefficient implementation is supplied. + +Structured relevance, first steps and blockers are in [TASK.json](TASK.json). diff --git a/research/dyadic-cubic-repair/verify.py b/research/dyadic-cubic-repair/verify.py new file mode 100644 index 0000000000..2fd6855f0f --- /dev/null +++ b/research/dyadic-cubic-repair/verify.py @@ -0,0 +1,384 @@ +#!/usr/bin/env python3 +"""Exact finite certificates for the dyadic cubic-reader repair alphabet. + +Prepared by apoursh with substantial OpenAI Codex assistance. Apache-2.0. +Nick Petalas's PR6200 supplies the fixed-reader contract and rational theorem; +Sricharan Vagvala, Adam Gall and Hanson Sun retain the preceding lineage. +No predecessor executable is imported. The all-arity localization and +minimality statements are written proofs, not extrapolations from this scan. +""" + +import hashlib +import json +from fractions import Fraction +from math import gcd, isqrt +from pathlib import Path + + +SOURCE_HEAD = "8b705d15869ba12d55adcb9075c68a2c7d44602d" +SOURCE_BASE = "research/cubic-reader-rational-repair/" +ENTRY = ((1, 0, 0, 0, 0), (1, 0), (0, 1)) +# Output coordinates are y_entry, a_entry^3, a_entry^2*b_entry, +# a_entry*b_entry^2, b_entry^3. Source coordinates are a_entry,b_entry. + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def authenticate_sources(package): + manifest = json.loads((package / "SOURCE-PINS.json").read_text()) + need(manifest["schema_version"] == 1, "source schema") + predecessor = manifest["predecessor"] + need(predecessor == { + "pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/6200", + "head": SOURCE_HEAD, "author": "Nick Petalas", "license": "Apache-2.0", + }, "exact predecessor identity") + documents = manifest["documents"] + expected = {"sources/pr6200-PROOF.md", "sources/pr6200-README.md"} + need(len(documents) == 2 and {item["path"] for item in documents} == expected, + "both exact predecessor documents") + hashes = {} + for item in documents: + filename = item["path"].removeprefix("sources/pr6200-") + source_path = SOURCE_BASE + filename + need(item["source_path"] == source_path, "predecessor source path") + need(item["source_url"] == "https://raw.githubusercontent.com/" + f"CrocSwap/integer-mult-bounds/{SOURCE_HEAD}/{source_path}", + "predecessor exact-head URL") + path = (package / item["path"]).resolve() + need(path.is_relative_to(package), "source path inside package") + digest = hashlib.sha256(path.read_bytes()).hexdigest() + need(digest == item["sha256"], "source digest: " + item["path"]) + hashes[item["path"]] = digest + return hashes + + +def add(left, right): + return tuple(a + b for a, b in zip(left, right, strict=True)) + + +def weighted_cube(weight, form): + a, b = form + return (0, weight * a**3, 3 * weight * a*a*b, + 3 * weight * a*b*b, weight * b**3) + + +def moments(r): + need(isinstance(r, int) and r >= 2, "integer arity at least two") + first = r * (r - 1) // 2 + second = r * (r - 1) * (2*r - 1) // 6 + return first, second + + +def defect(r): + first, second = moments(r) + return (0, 0, 3*first, 3*second, first*first) + + +def endpoint(r): + return ((1, r, 0, 0, 0), ENTRY[1], ENTRY[2]) + + +def original_children(r): + # Event fields are opcode, coefficient, source, provenance label. + return [event for i in range(r) for event in ( + ("cube", 1, "a", f"child-{i}-read"), + ("shift", 1, "b", f"child-{i}-shift"))] + + +def eager_program(r): + return [event for i in range(r) for event in ( + ("cube", 1, "a", f"child-{i}-read"), + ("shift", 1, "b", f"child-{i}-shift"), + ("shift", -1, "b", f"eager-{i}-restore"))] + + +def run(events, state=ENTRY): + output, a, b = state + for opcode, coefficient, source, _ in events: + need(isinstance(coefficient, (int, Fraction)), "exact scalar coefficient") + need(coefficient != 0, "zero events must be omitted") + if opcode == "shift": + need(source == "b", "source shift reads b only") + a = add(a, tuple(coefficient * value for value in b)) + elif opcode == "cube": + need(source in ("a", "b"), "cube reads an actual source stream") + output = add(output, weighted_cube(coefficient, a if source == "a" else b)) + else: + raise ValueError("event outside declared alphabet") + return output, a, b + + +def inverse(events): + return [(op, -coefficient, source, label) + for op, coefficient, source, label in reversed(events)] + + +def dyadic(value): + denominator = Fraction(value).denominator + return denominator & (denominator - 1) == 0 + + +def decomposition_value(terms, b_weight): + result = weighted_cube(b_weight, (0, 1)) + for slope, weight in terms: + result = add(result, weighted_cube(weight, (1, slope))) + return result + + +def four_decomposition(r): + first, second = moments(r) + need((first - second) % 2 == 0, "integer universal cube weights") + terms = [(1, (first + second)//2), (-1, (second - first)//2), (0, -second)] + return terms, first*first - first + + +def three_decomposition(r): + need(r % 3 == 2, "integer three-query subclass") + first, _ = moments(r) + numerator = first * (r - 2) * (r + 1) + need(numerator % 6 == 0, "integer pure-b weight") + return [((r + 1)//3, first), ((r - 2)//3, -first)], numerator//6 + + +def repair_events(r, terms, b_weight): + events, position = [], r + for slope, weight in terms: + if weight == 0: + continue + if slope != position: + events.append(("shift", slope-position, "b", "repair-source")) + events.append(("cube", -weight, "a", "repair-query")) + position = slope + if position != 0: + events.append(("shift", -position, "b", "repair-restore")) + if b_weight != 0: + events.append(("cube", -b_weight, "b", "repair-query")) + return events + + +def check_program(r, terms, b_weight, require_dyadic=True): + need(decomposition_value(terms, b_weight) == defect(r), "exact cubic decomposition") + children = original_children(r) + actual_drift = run(children) + need(actual_drift == (add(endpoint(r)[0], defect(r)), (1, r), (0, 1)), + "retained chronological defect and actual drifting source") + repair = repair_events(r, terms, b_weight) + program = children + repair + need(program[:2*r] == children, "all original children retained unchanged") + if require_dyadic: + need(all(dyadic(event[1]) for event in program), "every physical coefficient dyadic") + final = run(program) + need(final == endpoint(r), "arbitrary-input repaired endpoint") + need(run(inverse(program), final) == ENTRY, "literal full-program inverse") + need(run(inverse(repair), final) == actual_drift, "literal repair inverse") + need(run(eager_program(r)) == final, "same arbitrary-input eager endpoint") + return {"queries": sum(event[0] == "cube" for event in repair), + "shifts": sum(event[0] == "shift" for event in repair), + "original_children": r} + + +def square_root(value): + value = Fraction(value) + numerator, denominator = isqrt(value.numerator), isqrt(value.denominator) + if numerator*numerator == value.numerator and denominator*denominator == value.denominator: + return Fraction(numerator, denominator) + return None + + +def prime_factors(number): + factors, divisor = set(), 2 + while divisor*divisor <= number: + if number % divisor == 0: + factors.add(divisor) + while number % divisor == 0: + number //= divisor + divisor += 1 + if number > 1: + factors.add(number) + return factors + + +def localized(value, allowed_primes): + return prime_factors(Fraction(value).denominator) <= allowed_primes + + +def pell_data(r): + first, _ = moments(r) + n = 2*r - 1 + root = square_root(Fraction(2*r*r - 2*r - 1, 12)) + quotient, remainder = divmod(n*n - 3, 6) + k = isqrt(quotient) + integer_solution = remainder == 0 and k*k == quotient + need((root is not None) == integer_solution, "rational-square and integer-Pell equivalence") + if root is None: + return None + need(root == Fraction(k, 2) and k > 0, "half-integral square root") + need(n*n - 6*k*k == 3 and n % 3 == 0, "Pell identity and divisible numerator") + need(k % 2 == 1 and (n//3) % 2 == 1, "odd k and odd one-third numerator") + need(4*first == 3*k*k + 1 and gcd(first, k) == 1, "coprime forced weight numerator") + t, s = (n//3 + k)//2, (n//3 - k)//2 + weight = Fraction(first, k) + need(t-s == k and t+s == n//3, "integer normalized slopes") + need(weight.denominator == k, "forced weight has exact reduced denominator k") + need(decomposition_value([(t, weight), (s, -weight)], 0) == defect(r), + "forced rational two-cube identity") + need(dyadic(weight) == (r == 2), "only arity two has dyadic Pell weight") + return {"r": r, "n": n, "k": k, "t": t, "s": s, "weight": weight} + + +def localization_checks(data): + k, weight = data["k"], data["weight"] + factors = prime_factors(k) + rings = [set(), {2}, factors, factors | {2}] + rings.extend(factors - {prime} for prime in sorted(factors)) + # This finite corroboration is distinct from the universal nonmonic + # normalization argument in the written proof. + scales = sorted({Fraction(1), Fraction(2), Fraction(1, 2), Fraction(3), + Fraction(1, 3), Fraction(k), Fraction(1, k), Fraction(2, k)}) + normalization_count = 0 + for primes in rings: + permitted = factors <= primes + need(localized(weight, primes) == permitted, "exact localization criterion") + need(localized(-weight, primes) == permitted, "opposite normalized weight") + for slope, normalized_weight in ((data["t"], weight), (data["s"], -weight)): + admissible = [] + for alpha in scales: + beta = alpha*slope + gamma = normalized_weight/(alpha**3) + need(gamma*alpha**3 == normalized_weight and beta/alpha == slope, + "nonmonic normalization") + need(weighted_cube(gamma, (alpha, beta)) == + weighted_cube(normalized_weight, (1, slope)), + "all four nonmonic cubic coefficients") + accepted = all(localized(value, primes) for value in (alpha, beta, gamma)) + need(not accepted or permitted, "no forbidden prime hidden by rescaling") + admissible.append(accepted) + normalization_count += 1 + need(any(admissible) == permitted, "monic attainment and sampled nonmonic obstruction") + return normalization_count, len(rings) + + +def expect_rejected(function, diagnostic): + try: + function() + except ValueError as error: + need(str(error) == diagnostic, "specific rejection diagnostic") + else: + raise ValueError("mutation unexpectedly accepted: " + diagnostic) + + +def mutation_controls(): + r = 14 + terms, b_weight = three_decomposition(r) + children = original_children(r) + repair = repair_events(r, terms, b_weight) + need(repair == [("shift", -9, "b", "repair-source"), + ("cube", -91, "a", "repair-query"), + ("shift", -1, "b", "repair-source"), + ("cube", 91, "a", "repair-query"), + ("shift", -4, "b", "repair-restore"), + ("cube", -2730, "b", "repair-query")], "literal r14 schedule") + changed = repair[:] + op, coefficient, source, label = changed[1] + changed[1] = (op, coefficient+1, source, label) + need(run(children+changed) != endpoint(r), "wrong query coefficient rejected") + missing_restore = [event for event in repair if event[3] != "repair-restore"] + result = run(children+missing_restore) + need(result[0] == endpoint(r)[0] and result[1] != ENTRY[1], "source restoration independently necessary") + need(run(children+repair[:-1]) != endpoint(r), "pure-b correction cannot be omitted") + omitted_child = children[1:] + need(omitted_child != children and run(omitted_child+repair) != endpoint(r), + "original reader cannot be omitted") + reversed_first = [children[1], children[0], *children[2:]] + need(run(reversed_first+repair) != endpoint(r), "read-before-shift chronology necessary") + # Shift as if an entry snapshot existed, then restore the real source. + # The source endpoint is correct but its sampled cube arguments are wrong. + snapshot_schedule = repair[:] + snapshot_schedule[0] = ("shift", repair[0][1]+r, "b", "repair-source") + snapshot_schedule[4] = ("shift", repair[4][1]-r, "b", "repair-restore") + result = run(children+snapshot_schedule) + need(result[1:] == ENTRY[1:] and result[0] != endpoint(r)[0], "actual source semantics necessary") + data = pell_data(r) + need(data is not None, "r14 rational two-query fixture") + rational = [(data["t"], data["weight"]), (data["s"], -data["weight"])] + expect_rejected(lambda: check_program(r, rational, 0), "every physical coefficient dyadic") + alpha = Fraction(1, 11) + gamma = data["weight"] / alpha**3 + need(dyadic(gamma) and not dyadic(alpha) and not dyadic(alpha*data["t"]), + "integral query weight cannot hide non-dyadic source") + need(gamma == 11011 and gamma*alpha**3 == Fraction(91, 11), "hidden denominator exact values") + alpha = Fraction(11) + gamma = data["weight"] / alpha**3 + need(dyadic(alpha) and dyadic(alpha*data["t"]) and not dyadic(gamma), + "integral source cannot hide non-dyadic query weight") + expect_rejected(lambda: run([("shift", 1, "y", "forbidden-feedback")]), + "source shift reads b only") + return ["query-coefficient", "final-source-restoration", "pure-b-correction", + "retained-original-reader", "read-before-shift-chronology", "actual-drifting-source", + "rational-square-is-not-dyadic", "denominator-in-source", "denominator-in-query", + "output-feedback-excluded"] + + +def main(): + package = Path(__file__).resolve().parent + hashes = authenticate_sources(package) + four_count, three_count, retained_total = 0, 0, 0 + pell_scan = [] + for r in range(2, 257): + result = check_program(r, *four_decomposition(r)) + need(result["queries"] == (2 if r == 2 else 4), "universal nonzero query count") + need(result["shifts"] <= 3, "universal source-shift count") + four_count += 1 + retained_total += r + if r % 3 == 2: + result = check_program(r, *three_decomposition(r)) + need(result["queries"] == (2 if r == 2 else 3), "subclass nonzero query count") + need(result["shifts"] <= 3, "subclass source-shift count") + three_count += 1 + data = pell_data(r) + if data is not None: + pell_scan.append(r) + need(pell_scan == [2, 14, 134], "bounded rational two-query arities") + pell_fixtures, normalizations, ring_cases = [], 0, 0 + n, k = 3, 1 + for _ in range(7): + r = (n+1)//2 + data = pell_data(r) + need(data is not None and data["k"] == k, "fixed Pell recurrence fixture") + count, rings = localization_checks(data) + normalizations += count + ring_cases += rings + pell_fixtures.append({**data, "weight": str(data["weight"]), + "denominator_primes": sorted(prime_factors(k))}) + n, k = 5*n+12*k, 2*n+5*k + rational_program_arities = [2, 14, 134, 1322] + for r in rational_program_arities: + data = pell_data(r) + result = check_program(r, [(data["t"], data["weight"]), + (data["s"], -data["weight"])], 0, require_dyadic=False) + need(result["queries"] == 2, "rational comparison uses two queries") + controls = mutation_controls() + print("PASS_DYADIC_CUBIC_REPAIR " + json.dumps({ + "source_head": SOURCE_HEAD, "source_sha256": hashes, + "scope": "exact finite corroboration; universal claims require PROOF.md", + "arity_scan": {"first": 2, "last": 256, "count": 255}, + "universal_integer_programs": four_count, + "subclass_integer_programs": three_count, + "original_children_in_universal_programs": retained_total, + "rational_two_query_arities_in_scan": pell_scan, + "rational_two_query_programs": rational_program_arities, + "pell_fixtures": pell_fixtures, + "localization_ring_cases": ring_cases, + "nonmonic_normalizations": normalizations, + "mutations_rejected": controls, + "r14_dyadic_repair": {"queries": 3, "source_shifts": 3, + "retained_children": 14, "eager_restore_shifts": 14}, + "no_backend_saving_or_kappa_claim": True, + }, sort_keys=True)) + + +if __name__ == "__main__": + main()