Prove exact rational cube-query costs for cubic reader repair (no κ)

research/cubic-reader-rational-repair/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<=i<r. The final drifting source is `a+r*b`. S1>0.
+
+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.

research/cubic-reader-rational-repair/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).

research/cubic-reader-rational-repair/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "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"
+    },
+    {
+      "path": "research/quadratic-reader-restoration/README.md",
+      "usage": "provenance",
+      "git_blob": "71c6d22f174f1984cd5aa52b984efa1e08aba289",
+      "sha256": "eaf5278c40eeab8235014926fda17f3fe163c808ab642704802ee26dddc8ce68"
+    }
+  ]
+}