From 0013c2b40c522ccd19670a8fbd4b1531f13fed2b Mon Sep 17 00:00:00 2001 From: apoursh <8867770+apoursh@users.noreply.github.com> Date: Thu, 29 Oct 2026 15:21:02 -0400 Subject: [PATCH] Prove sharp pure-b cubic-query boundary modulo nine --- research/cubic-pure-b-boundary/PROOF.md | 269 +++++++++++++ research/cubic-pure-b-boundary/README.md | 158 ++++++++ .../cubic-pure-b-boundary/SOURCE-PINS.json | 17 + research/cubic-pure-b-boundary/SOURCES.json | 18 + research/cubic-pure-b-boundary/TASK.json | 111 ++++++ research/cubic-pure-b-boundary/VERIFY.json | 59 +++ .../independent_check.py | 299 +++++++++++++++ .../sources/pr6212-PROOF.md | 255 ++++++++++++ research/cubic-pure-b-boundary/verify.py | 362 ++++++++++++++++++ 9 files changed, 1548 insertions(+) create mode 100644 research/cubic-pure-b-boundary/PROOF.md create mode 100644 research/cubic-pure-b-boundary/README.md create mode 100644 research/cubic-pure-b-boundary/SOURCE-PINS.json create mode 100644 research/cubic-pure-b-boundary/SOURCES.json create mode 100644 research/cubic-pure-b-boundary/TASK.json create mode 100644 research/cubic-pure-b-boundary/VERIFY.json create mode 100644 research/cubic-pure-b-boundary/independent_check.py create mode 100644 research/cubic-pure-b-boundary/sources/pr6212-PROOF.md create mode 100644 research/cubic-pure-b-boundary/verify.py diff --git a/research/cubic-pure-b-boundary/PROOF.md b/research/cubic-pure-b-boundary/PROOF.md new file mode 100644 index 0000000000..9907a6925f --- /dev/null +++ b/research/cubic-pure-b-boundary/PROOF.md @@ -0,0 +1,269 @@ +# Sharp query count when cubic repair includes an original-b cube + +Prepared by apoursh with substantial OpenAI Codex assistance. Apache-2.0. +Nick Petalas's PR6200 supplies the fixed cubic-reader interface; apoursh's +PR6212 supplies the dyadic two-query obstruction and earlier constructions. +The new result is the exact boundary for repairs containing a pure-b query, +including arbitrary nonmonic forms, and the integer construction across it. + +## Fixed contract and theorem + +Use exact arithmetic with dyadic coefficients R=Z[1/2]. The distinct streams +y,a,b start arbitrary. Retain every one of r original children, each in 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. The deferred program retains all original +children, then repairs the output and both sources. Source changes are in +GL_2(R); query updates add signed R-weighted cubes of source linear forms. +Coefficients do not depend on input values. There is no output feedback, +intermediate observation, child fusion, nonlinear source map or output recoding. +Source transformations, their inverses and coefficient work are paid separately. + +Here **pure-b means a nonzero cube of a nonzero scalar multiple of the +original entry b**, not simply a read from whichever register is currently +named b. General frames may temporarily mix both sources. The theorem counts +appended nonzero cube queries and requires at least one pure-b query. Zero +queries cannot be inserted to meet this requirement. + +**Theorem.** For every integer r>=3, the exact minimum in this restricted +family is + +``` +3, if r mod 9 belongs to {0,1,2,5,8}; +4, if r mod 9 belongs to {3,4,6,7}. +``` + +Every upper bound uses integer source transformations and integer query +weights. The lower bound allows arbitrary nonmonic dyadic forms and arbitrary +GL_2(R) source changes. In particular, widening from source shears to general +dyadic frames cannot remove the four-query floor while retaining a pure-b read. + +This is not an unrestricted four-query lower bound. For example r=3 admits +three dyadic queries when all three forms involve entry a. The separate r=2 +unrestricted two-query result belongs to PR6212 and is outside this theorem's +domain. No runtime or multiplication-bound improvement is asserted. + +## Chronological defect and elementary lower bound + +Let A,B denote entry a,b. The retained deferred program ends at + +``` +(y + sum_{i=0}^{r-1}(A+i*B)^3, A+r*B, B). +``` + +Its excess output over the eager comparator is, as in PR6200, + +``` +f_r(A,B) = 3S1*A^2*B + 3S2*A*B^2 + S1^2*B^3, +S1=r(r-1)/2, S2=r(r-1)(2r-1)/6. +``` + +Every appended source is an R-linear form in A,B: multiply the source-frame +matrices in chronological order. Thus any repair gives a signed weighted-cube +decomposition of -f_r. Negating weights gives one for f_r, without changing +the number of queries or the pure-B property. + +At most two cubes including a pure-B term are impossible. There is then at +most one term involving A. Its A^3 coefficient must vanish, forcing that +term's weight or A coefficient to be zero and therefore also its A^2*B +coefficient to be zero. But 3S1 is nonzero. This proves a three-query lower +bound for the entire restricted family, without invoking the predecessor's +stronger unrestricted dyadic lower bound. + +## A modulo-nine obstruction for two remaining forms + +Reduction R -> Z/9Z is well defined because 2 is invertible modulo 9. +Ignore the B^3 coefficient and project a physical weighted cube to + +``` +gamma*(alpha*A+beta*B)^3 + -> (gamma*alpha^3, 3*gamma*alpha^2*beta, 3*gamma*alpha*beta^2) mod 9. +``` + +If alpha is divisible by 3, this triple is zero. Otherwise alpha is a unit +modulo 9 and the triple is `(lambda,3*lambda*t,3*lambda*t^2)`, where +lambda=gamma*alpha^3 and t=beta/alpha in Z/9Z. A zero triple can be represented +by lambda=0. These reductions do not assume a dyadic normalized slope over Q. + +Suppose two projected cubes sum to a vector with its first two coordinates +zero. The first coordinate gives lambda_2=-lambda_1. The second gives +`3*lambda_1*(t_1-t_2)=0`. Consequently the third is + +``` +3*lambda_1*(t_1^2-t_2^2) + = [3*lambda_1*(t_1-t_2)]*(t_1+t_2) = 0 mod 9. +``` + +This identity holds in Z/9Z despite its zero divisors. We never divide by +lambda or by a slope difference. It covers zero weights, nonprimitive forms +and arbitrary nonmonic forms, which only strengthens the obstruction. + +For r congruent to 3,4 modulo 9, the target projection of f_r is `(0,0,6)`; +for r congruent to 6,7 it is `(0,0,3)`. Indeed 3S1=3r(r-1)/2 and +3S2=r(r-1)(2r-1)/2 modulo 9 depend only on r modulo 9. A pure-B term projects +to zero. Any three-query repair containing it has at most two remaining +projected cubes, so the preceding identity rules it out in all four classes. + +The independent finite certificate enumerates all 9^3=729 triples +(gamma,alpha,beta) modulo 9, obtaining 33 full weighted-cube tensors and 21 +distinct projections. Their 441 ordered pair sums have 57 distinct values. +Neither forbidden target is present. This exhaustive finite calculation +corroborates the universal reduction argument; no unbounded search is inferred. + +## Integer attainment when r=2 mod 3 + +This is the construction from PR6212. Put + +``` +t=(r+1)/3, s=(r-2)/3, +mu=S1*(r-2)*(r+1)/6=2*binom(r+1,4). +``` + +For r>=3 in this class, r>=5 and t,s,mu are positive integers. Expansion gives + +``` +f_r = S1*((A+t*B)^3-(A+s*B)^3) + mu*B^3. +``` + +Starting at the actual source `(A+r*B,B)`, append + +``` +a += (t-r)*b +y -= S1*a^3 +a -= b +y += S1*a^3 +a -= s*b +y -= mu*b^3 +``` + +There are three nonzero queries, including the original-B cube, and three +source shears. The final source is exactly `(A,B)`, and the output subtracts f_r. + +## New integer attainment when r=0 or 1 mod 9 + +Now S1 is divisible by 9. Let N=S1/9 and mu=S1*(3S1-1)/9, both positive +integers. Direct expansion gives + +``` +f_r = N*((3A+r*B)^3-(3A+(r-1)*B)^3) + mu*B^3. +``` + +One of r,r-1 is divisible by 3. Its form factors as three times a monic +integer form, moving a factor 27 into its weight. The other form has primitive +integer coefficients and can be a row of an invertible integer source frame. +The following explicit program realizes both cases and charges the frame. + +Set epsilon=-1 and q=r/3 for r=0 mod 9; set epsilon=1 and q=(r-1)/3 for +r=1 mod 9. Define simultaneous source transformations + +``` +M_epsilon(a,b) = (3a+epsilon*b, a), +M_epsilon^-1(a,b) = (b, epsilon*a-3*epsilon*b). +``` + +Their matrices have integer entries and determinant -epsilon, a unit. From +the actual deferred endpoint append, in this order, + +``` +a += (q-r)*b +y += epsilon*3*S1*a^3 +(a,b) = M_epsilon(a,b) +y -= epsilon*N*a^3 +(a,b) = M_epsilon^-1(a,b) +a -= q*b +y -= mu*b^3 +``` + +The first query reads A+qB. The second reads 3A+(3q+epsilon)B. In the +r=0 case their contributions are `-3S1*(A+qB)^3+N*(3A+(r-1)B)^3`; +in the r=1 case they are `+3S1*(A+qB)^3-N*(3A+rB)^3`. Together with the +last query, these are -f_r in both cases. The inverse frame returns both +sources before the last shear restores A. The last query therefore reads +the actual original B. All three coefficients are nonzero. + +For r=10, S1=45, N=5, q=3 and mu=670. The decomposition is + +``` +f_10 = 5*(3A+10B)^3 - 135*(A+3B)^3 + 670*B^3. +``` + +The repair applies shear -7, query +135, M_1, query -5, M_1^-1, +shear -3, and original-B query -670. B changes temporarily under the frame; +an implementation that silently treats it as immutable would be wrong. + +## Four-query attainment and the scope control + +For all r>=3, PR6212's integer construction uses + +``` +p=binom(r+1,3), m=binom(r,3), d=S1^2-S1, +f_r=p*(A+B)^3+m*(A-B)^3-S2*A^3+d*B^3. +``` + +From `(A+rB,B)` apply shear 1-r, query -p on a, shear -2, query -m on a, +shear +1, query +S2 on a, and query -d on b. All four queries are nonzero; +the source is restored and the last query is pure-B. This attains the +four-query lower bound in residues 3,4,6,7. The other five residues have +three-query attainment and the elementary lower bound, proving the theorem. + +For comparison, + +``` +f_3=(A+B)^3+(A+2B)^3-2*A^3. +``` + +This gives three unrestricted queries, all with nonzero entry-A coefficient: +from A+3B visit slopes 2,1,0 with three -1 shears and weights -1,-1,+2. +It restores every source and output but has no pure-B query. Thus the new +four-query floor at r=3 cannot be relabeled an unrestricted floor. + +## Complete logical tariffs and remaining obligations + +Let Q_c^a,Q_c^b price complete weighted cube queries on the current named +source, including source access, coefficient use, private restoration and +return. Let L_c price `a += c*b`; let F_M price the complete simultaneous +source-frame operation M. These are distinct paid operations. 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. In the new r=0,1 mod 9 construction, +its additional bill is exactly + +``` +L_(q-r) + Q_(epsilon*3S1)^a + F_Mepsilon + Q_(-epsilon*N)^a + + F_(Mepsilon^-1) + L_-q + Q_-mu^b. +``` + +The older three- and four-query programs likewise charge every displayed +shear and query. No frame or its inverse is free, and two source frames +cannot be compared numerically with two shears without an actual tariff. +Coefficient generation, routing, precision, storage and dispatch remain +additional caller obligations. The simultaneous matrix description certifies +an algebraic source map, not an uncharged in-place or scratch-free backend. +Every map is invertible, so reverse order and literal event inverses restore +the arbitrary incoming state. The primary checker executes the reversed repair +and full programs on symbolic inputs; the independent checker separately +checks the forward restoring schedules, including their inverse-frame events. + +The result excludes approximate queries, finite-field substitution as the +execution model and altered child interiors. Modulo nine is used only as a +necessary image of exact dyadic arithmetic. No native implementation, complete +favorable physical bill, supplier admission, selected assumption discharge, +independent human/formal-kernel acceptance or new kappa follows. + +## Attribution + +PR6212 retains credit for the earlier dyadic results, three/four-query formulas +and this open question. Nick Petalas retains PR6200's chronological defect, +rational two-query theorem and source-restoring interface. Sricharan Vagvala / +theon199 retains PR1532's quadratic fixed-reader/paid-repair interface, with +Adam Gall / PR1205 and Hanson Sun / PR1246 retaining the linear lineage. +Elementary modular reduction and binary-form decomposition are classical; +no historical-priority claim is made. diff --git a/research/cubic-pure-b-boundary/README.md b/research/cubic-pure-b-boundary/README.md new file mode 100644 index 0000000000..a3bb812a06 --- /dev/null +++ b/research/cubic-pure-b-boundary/README.md @@ -0,0 +1,158 @@ +# Sharp cubic-query boundary with an original-b correction + +Prepared by **apoursh** with substantial OpenAI Codex assistance. Apache-2.0. +**Scoped proof with exact finite corroboration; no new kappa.** + +For the fixed cubic-reader program of Nick Petalas's +[PR6200](https://github.com/CrocSwap/integer-mult-bounds/pull/6200), retain all +r children `y += a^3; a += b`, then restore the arbitrary incoming sources +and reproduce the eager output. [PR6212](https://github.com/CrocSwap/integer-mult-bounds/pull/6212) +left the general three-versus-four dyadic query question open. + +This contribution completely classifies the family that **contains a nonzero +cube of the original entry b**. This is a source-line requirement, not merely +the name of the register read while frames are changing. For every r>=3: + +| r modulo 9 | Exact minimum appended cube queries in this family | +|---|---:| +| 0, 1, 2, 5, 8 | 3 | +| 3, 4, 6, 7 | 4 | + +The lower bound allows arbitrary nonmonic dyadic forms and all invertible +dyadic source frames. All attaining programs have integer coefficients. +[PROOF.md](PROOF.md) gives the modular obstruction and explicit restoration. + +The key obstruction is small. Modulo nine, two weighted cubes whose summed +a³ and a²b coefficients vanish must also have zero ab² coefficient. +A pure original-b cube cannot affect any of those three coefficients. +The forbidden residue classes have projected defect (0,0,3) or (0,0,6). + +The new construction covers residues 0,1, where nonmonic source forms are +useful. For example, +`f_10=5(3a+10b)^3-135(a+3b)^3+670b^3`. +Starting at the actual deferred sources (a_entry+10b,b), its repair is + +``` +a -= 7*b +y += 135*a^3 +(a,b) = (3*a+b, a) # simultaneous source frame +y -= 5*a^3 +(a,b) = (b, a-3*b) # simultaneous inverse frame +a -= 3*b +y -= 670*b^3 +``` + +Both sources temporarily mix and then return exactly to their entry values. +The two source frames and their implementation costs are explicit paid work. +The program retains all ten original child calls; it is not a runtime-saving +claim. The older three-query class and universal four-query construction are +credited to PR6212. + +The unrestricted question remains open. In particular r=3 has a three-query +repair without a pure-b read, so the four-query entry in the table cannot be +reinterpreted as an unrestricted lower bound. That example is a checked scope +control. The theorem starts at r=3; PR6212's unrestricted r=2 result is separate. + +## Reproduce + +CPython 3.12 and the standard library, from the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/cubic-pure-b-boundary +python3.12 -I -W error -B research/cubic-pure-b-boundary/verify.py +python3.12 -I -O -W error -B research/cubic-pure-b-boundary/verify.py +python3.12 -I -W error -B research/cubic-pure-b-boundary/independent_check.py +python3.12 -I -O -W error -B research/cubic-pure-b-boundary/independent_check.py +python3.12 -B scripts/check_research_commit.py --package research/cubic-pure-b-boundary --check-source-history --check-modes +``` + +The runner registers both checkers in normal and optimized isolated, +warning-strict execution. All checks are bounded and read-only. The primary +checker follows exact cubic coefficients and source matrices, retaining every +child, restoring both sources and checking literal inverse programs. Its +obstruction certificate uses divided moments modulo three. +It replays 254 complete programs for r=3..256 (56 new three-query, 84 older +three-query and 114 four-query programs), plus nine explicitly separate +closed-defect fixtures near one million. All 729 physical two-form assignments +modulo three are checked; 249 satisfy the first two zero-moment premises. +Seventeen semantic and scope controls include singular/nonunit frames, +incorrect inverses, missing readers/restoration and entry-source classification. + +The independent checker derives the child ladder by binary concatenation of +sparse polynomials and fits query weights by exact elimination. It enumerates +all 729 physical coefficient triples modulo nine: 33 weighted tensors, +21 projected tensors, and 57 distinct sums from 441 ordered projection pairs. +It checks 135 arities (3..128 and all nine residues near 9*2^80), including +30 nonmonic three-query schedules, 45 older three-query schedules and 60 +four-query schedules. Mutation controls and the r=3 scope control exercise +the distinction between current-register b and the original-b line. + +The finite quotient calculation is exhaustive for its modulus. The written +reduction explains why that finite obstruction applies at every arity in the +listed residue classes; the arity tests alone do not prove a universal theorem. +Separate AI derivations are not independent human or formal-kernel acceptance. +All four registered commands passed on CPython 3.12.14, macOS arm64. Actual +copies with a corrupted retained proof or a changed predecessor-head label are +rejected. Committed bytes/modes/source history, official export integrity and +read-only Git-free normal/optimized replays are the publication checks; their +results are reported in the PR separately from hosted CI. + +## Scope, coordination and provenance + +This is an explicitly changed algebraic side scope of `joint-query-controller`. +The initial unrestricted investigation was refined publicly to the exact +original-b family after the modular obstruction and attainment were found. +The [canonical claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19276156) +records that refinement. No selected-supplier acceptance gate is claimed. + +Canonical base is `a5bff3bf133e482541c09eba4e773884bdb2b1b7`, priority revision 8. +Entry overlap covered the newest twenty PRs through #6212, the all-state +`cubic dyadic` search and newest fifteen visible handoffs. The sparse local +helper searched 30 of 8,623 HEAD note paths with no usable remote cache. +Coverage is bounded, not a novelty certificate. + +[SOURCE-PINS.json](SOURCE-PINS.json) identifies PR6212 at +`9c159482e0495b6a97e17e629debe66a0ceb9466`. The +[retained proof](sources/pr6212-PROOF.md) preserves its exact interface, +constructions and attribution offline; its bytes match both the published +Git object and immutable GitHub raw URL, and are hash-checked during replay. +No predecessor executable is imported. The pending head is not asserted to +be an ancestor of this branch or authenticated by the source-history preflight; +that preflight covers the base provenance in [SOURCES.json](SOURCES.json). +All scientific runtime inputs are package-local and trigger package replay. + +A prior binding-only baseline pass is reused after finding all 1,227 covered +Git paths unchanged. This is not a scientific cold replay. The selected +PR6030 record, kappa=781451/250000000 and its five framework assumptions remain +unchanged. Only this isolated research package is added. + +The model excludes intermediate observations, output feedback, nonlinear +source changes, child fusion and approximate queries. Modulo nine is a +necessary image of exact dyadic arithmetic, not a substituted execution model. +An actual caller, native realization, source-frame implementation, precision, +routing, storage, dispatch and complete favorable paid bill are not supplied. +No Lean, Docker, selected cold replay or full multiplication proof is claimed. + +## Credit + +Nick Petalas retains PR6200's fixed-reader chronology, defect, rational theorem +and repair interface. PR6212 retains its dyadic results, earlier upper formulas +and open question. Sricharan Vagvala / theon199's PR1532, Adam Gall / PR1205 +and Hanson Sun / PR1246 retain the quadratic and linear interface lineage. +Modular reduction and binary-form decomposition are classical; no historical +priority is claimed. Prepared for apoursh with substantial OpenAI Codex +assistance in derivation, bounded exploration, proof, separately authored +verification, mathematical audit, documentation and publication. + +## Open next questions + +1. **Unrestricted three-query repair:** classify the remaining arities when + every query may involve entry a. Start with arbitrary nonmonic mixed forms + in residues 3,4,6,7 and construct legal restoring frames, or prove a new + obstruction. The present pure-b floor does not settle this. +2. **An actual caller and tariff:** determine whether a real fixed-reader + interface requires the pure-b correction and whether the framed program + beats eager restoration after every cost is charged. The missing backend + and favorable complete bill block supplier expansion. + +[TASK.json](TASK.json) records relevance, first steps and blockers. diff --git a/research/cubic-pure-b-boundary/SOURCE-PINS.json b/research/cubic-pure-b-boundary/SOURCE-PINS.json new file mode 100644 index 0000000000..25350ff17d --- /dev/null +++ b/research/cubic-pure-b-boundary/SOURCE-PINS.json @@ -0,0 +1,17 @@ +{ + "schema_version": 1, + "predecessor": { + "pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/6212", + "head": "9c159482e0495b6a97e17e629debe66a0ceb9466", + "author": "apoursh", + "license": "Apache-2.0" + }, + "documents": [ + { + "path": "sources/pr6212-PROOF.md", + "source_path": "research/dyadic-cubic-repair/PROOF.md", + "source_url": "https://raw.githubusercontent.com/apoursh/integer-mult-bounds/9c159482e0495b6a97e17e629debe66a0ceb9466/research/dyadic-cubic-repair/PROOF.md", + "sha256": "1296f12278e198b6a22d8d88355cd58c1ee4fc2ab0e6941721614bb06cb1e7d5" + } + ] +} diff --git a/research/cubic-pure-b-boundary/SOURCES.json b/research/cubic-pure-b-boundary/SOURCES.json new file mode 100644 index 0000000000..75db18102e --- /dev/null +++ b/research/cubic-pure-b-boundary/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/cubic-pure-b-boundary/TASK.json b/research/cubic-pure-b-boundary/TASK.json new file mode 100644 index 0000000000..2750be57f9 --- /dev/null +++ b/research/cubic-pure-b-boundary/TASK.json @@ -0,0 +1,111 @@ +{ + "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": "For r>=3 classify the minimum appended dyadic cube-query count among exact repairs containing a nonzero cube of the original entry-b line. Allow arbitrary nonmonic forms and GL_2(Z[1/2]) source changes; retain every original reader and restore both arbitrary sources.", + "scope_change_reason": "An algebraic side result following PR6212 open question 1, instead of a complete current-supplier bill. The initial unrestricted three-versus-four investigation was narrowed publicly to the exact pure-b family after finding its modular obstruction and integer attainment; the unrestricted question remains open.", + "bottleneck_link": "This identifies exactly when retaining a particular repair output forces an extra nonlinear query, even with general source frames. No actual supplier imposes the pure-b requirement in this package; the result is a scoped interface theorem, not card-level supplier admission.", + "budget_minutes": 60, + "stop_rule": "Stop after the sharp restricted-family theorem, constructive source restoration, independent finite quotient certificate, controls and publication. Do not expand a finite search failure into an unrestricted lower bound or pursue native construction without an actual caller and favorable complete bill.", + "outcome": "completed", + "evidence": "PROOF.md supplies the universal modulo-nine reduction and source-restoring constructions. verify.py uses exact coefficient maps and divided moments modulo three; independent_check.py uses sparse polynomial execution, exact weight fitting and exhaustive weighted tensors modulo nine. Finite evidence and written proof have distinct scopes.", + "author": "apoursh", + "ai_assistance": "Substantial OpenAI Codex assistance in derivation, bounded exploratory searches, proof, independently authored checkers, mathematical audit, documentation and publication; prepared by apoursh. Independent human and formal-kernel acceptance are unclaimed.", + "open_questions": [ + { + "question": "Does every r>=3 admit three dyadic queries when a pure original-b read is not required?", + "why_it_matters": "The new four-query floor depends on retaining that read; the r=3 control demonstrates that dropping it can change the optimum.", + "first_step": "Analyze three arbitrary mixed nonmonic forms in residues 3,4,6,7 modulo nine and require an explicit admissible restoring source schedule. Use exact equations and arithmetic obstructions rather than treating bounded slope searches as exclusion proofs.", + "blocked_by": "No unrestricted classification is established; finding three queries for more examples does not by itself settle all arities." + }, + { + "question": "Does an actual fixed-reader caller benefit from the framed three-query repair?", + "why_it_matters": "Fewer queries can be offset by source frames, inverse frames, nonunit weights and coefficient preparation.", + "first_step": "Pin one actual caller and any requirement for an original-b correction; compare all retained children and the complete eager/deferred tariffs, including both M_epsilon and its inverse, routing, coefficient generation, precision, storage and dispatch.", + "blocked_by": "No admitted backend or favorable complete physical bill is supplied. Stop supplier construction expansion until these are known." + } + ], + "selection": { + "kind": "continuation-of-explicit-open-handoff", + "source_pr": 6212, + "source_head": "9c159482e0495b6a97e17e629debe66a0ceb9466", + "task_card_seed": "f5ef40c6b5b9ed6f7f4aa8765f945b54" + }, + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19276156", + "scope_update": "The same claim was updated with the exact pure-b theorem and the unresolved unrestricted question before packaging.", + "coverage": "Newest twenty PRs through 6212, all-state cubic dyadic search and newest fifteen visible handoffs. Sparse local helper searched 30 of 8623 HEAD note paths, with 8593 omitted and no usable remote cache. No global novelty certificate.", + "nearest": "PR6212 provides the two-query obstruction and prior upper constructions; Nick Petalas PR6200 provides the rational criterion and fixed-reader chronology. New work is the modular pure-b obstruction and integer source-frame construction for residues0,1 modulo9.", + "completion_refresh": "Canonical main and PR6212 head unchanged. Latest twenty PRs now reach6213; its full body concerns fixed-budget hidden-window optima, not this source-query family. The newest fifteen visible handoffs include a new PR6141 characteristic-five certificate claim, also distinct. No competing pure-b classification was visible; coverage remains bounded." + }, + "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 covered Git paths remain unchanged; this is not a scientific cold replay.", + "selected": "PR6030, kappa=781451/250000000; five framework assumptions unchanged." + } +} diff --git a/research/cubic-pure-b-boundary/VERIFY.json b/research/cubic-pure-b-boundary/VERIFY.json new file mode 100644 index 0000000000..51d84d5fa7 --- /dev/null +++ b/research/cubic-pure-b-boundary/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 arbitrary-input source-frame chronology, original child retention, full inverses, pure-entry-b membership, divided-moment obstruction and source hashes with controls. Normal execution." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact arbitrary-input source-frame chronology, original child retention, full inverses, pure-entry-b membership, divided-moment obstruction and source hashes with controls. Optimized execution." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/independent_check.py" + ], + "timeout_seconds": 120, + "checks": "Independent sparse polynomial execution and coefficient fitting; exhaustive modulo-nine tensor certificate and scope controls. Normal execution." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/independent_check.py" + ], + "timeout_seconds": 120, + "checks": "Independent sparse polynomial execution and coefficient fitting; exhaustive modulo-nine tensor certificate and scope controls. Optimized execution." + } + ] +} diff --git a/research/cubic-pure-b-boundary/independent_check.py b/research/cubic-pure-b-boundary/independent_check.py new file mode 100644 index 0000000000..8ecc1bf4d8 --- /dev/null +++ b/research/cubic-pure-b-boundary/independent_check.py @@ -0,0 +1,299 @@ +#!/usr/bin/env python3 +"""Independent quotient-ring and symbolic-state audit of the pure-b boundary. + +Prepared by apoursh with substantial OpenAI Codex assistance. Apache-2.0. +Retains Nick Petalas's chronological interface and the predecessor credits +recorded in README.md. No imports from the primary checker; no file writes. +""" + +import itertools +import json +from fractions import Fraction + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +# Free entry variables (a,b,y), represented by sparse exact polynomials. +ONE = {(0, 0, 0): Fraction(1)} +A = {(1, 0, 0): Fraction(1)} +B = {(0, 1, 0): Fraction(1)} +Y = {(0, 0, 1): Fraction(1)} +CUBICS = [(3, 0, 0), (2, 1, 0), (1, 2, 0), (0, 3, 0)] +LOW_RESIDUES = {3, 4, 6, 7} + + +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 scaled(coefficient, polynomial): + return {exponent: coefficient * value for exponent, value in polynomial.items() + if coefficient * value} + + +def times(left, right): + answer = {} + for left_power, left_value in left.items(): + for right_power, right_value in right.items(): + exponent = tuple(x + y for x, y in zip(left_power, right_power, strict=True)) + answer[exponent] = answer.get(exponent, Fraction(0)) + left_value * right_value + 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 line(slope): + return plus(A, scaled(slope, B)) + + +def translate_a(polynomial, offset): + answer = {} + for exponent, coefficient in polynomial.items(): + term = times(times(power(line(offset), exponent[0]), power(B, exponent[1])), + power(Y, exponent[2])) + answer = plus(answer, scaled(coefficient, term)) + return answer + + +def entry_after_ladder(arity): + # Concatenate literal reader-before-shift blocks by binary doubling. + # No closed-form sums or primary fixed-coefficient routines are used. + 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 + need(offset == arity, "literal ladder consumes its exact arity") + return {"a": line(arity), "b": B, "y": plus(Y, accumulated)} + + +def desired_state(arity): + return {"a": A, "b": B, "y": plus(Y, scaled(arity, power(A, 3)))} + + +def defect_for(arity): + initial = entry_after_ladder(arity) + desired = desired_state(arity) + return plus(initial["y"], scaled(-1, desired["y"])) + + +def dyadic(value): + denominator = Fraction(value).denominator + return denominator & (denominator - 1) == 0 + + +def dyadic_unit(value): + value = Fraction(value) + numerator = abs(value.numerator) + return dyadic(value) and numerator > 0 and numerator & (numerator - 1) == 0 + + +def inverse_frame(matrix): + a, b, c, d = matrix + determinant = a * d - b * c + need(dyadic_unit(determinant), "source frame determinant must be a dyadic unit") + return tuple(Fraction(value, determinant) for value in (d, -b, -c, a)) + + +def entry_b_line(polynomial): + return set(polynomial) == {(0, 1, 0)} and polynomial[(0, 1, 0)] != 0 + + +def execute(initial, program): + state = dict(initial) + reads = pure_b_reads = shifts = frames = 0 + for operation, argument in program: + if operation == "frame": + a, b, c, d = map(Fraction, argument) + need(all(dyadic(value) for value in (a, b, c, d)), "dyadic frame entries") + need(dyadic_unit(a * d - b * c), "source frame determinant must be a dyadic unit") + old_a, old_b = state["a"], state["b"] + state["a"] = plus(scaled(a, old_a), scaled(b, old_b)) + state["b"] = plus(scaled(c, old_a), scaled(d, old_b)) + frames += 1 + continue + coefficient = Fraction(argument) + need(dyadic(coefficient), "dyadic shear or query coefficient") + if operation == "shift": + state["a"] = plus(state["a"], scaled(coefficient, state["b"])) + shifts += 1 + elif operation in {"read_a", "read_b"}: + source = state["a"] if operation == "read_a" else state["b"] + state["y"] = plus(state["y"], scaled(coefficient, power(source, 3))) + if coefficient: + reads += 1 + pure_b_reads += int(entry_b_line(source)) + else: + raise ValueError("unknown instruction") + return state, {"queries": reads, "entry_b_queries": pure_b_reads, + "shears": shifts, "frames": frames} + + +def fit_weights(defect, forms): + cubes = [power(form, 3) for form in forms] + rows = [[cube.get(monomial, Fraction(0)) for cube in cubes] + + [defect.get(monomial, Fraction(0))] for monomial in CUBICS] + pivots = [] + for column in range(len(cubes)): + pivot = next((i for i in range(len(pivots), len(rows)) if rows[i][column]), None) + need(pivot is not None, "independent query forms") + index = len(pivots) + 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)] + pivots.append(index) + need(not any(all(value == 0 for value in row[:-1]) and row[-1] for row in rows), + "all four cubic equations are consistent") + weights = [rows[index][-1] for index in pivots] + reconstructed = {} + for weight, cube in zip(weights, cubes, strict=True): + reconstructed = plus(reconstructed, scaled(weight, cube)) + need(reconstructed == defect, "independently fitted full cubic identity") + need(all(weight.denominator == 1 and weight != 0 for weight in weights), + "all displayed query weights are nonzero integers") + return weights + + +def restoration_program(arity, defect): + if arity % 3 == 2: + high, low = (arity + 1) // 3, (arity - 2) // 3 + weights = fit_weights(defect, [line(high), line(low), B]) + return [("shift", high - arity), ("read_a", -weights[0]), + ("shift", low - high), ("read_a", -weights[1]), + ("shift", -low), ("read_b", -weights[2])], "old_three" + if arity % 9 in {0, 1}: + epsilon = -1 if arity % 9 == 0 else 1 + q = arity // 3 + primitive = plus(scaled(3, A), scaled(3 * q + epsilon, B)) + weights = fit_weights(defect, [line(q), primitive, B]) + matrix = (3, epsilon, 1, 0) + return [("shift", q - arity), ("read_a", -weights[0]), + ("frame", matrix), ("read_a", -weights[1]), + ("frame", inverse_frame(matrix)), ("shift", -q), + ("read_b", -weights[2])], "nonmonic_three" + weights = fit_weights(defect, [line(1), line(-1), A, B]) + return [("shift", 1 - arity), ("read_a", -weights[0]), + ("shift", -2), ("read_a", -weights[1]), + ("shift", 1), ("read_a", -weights[2]), ("read_b", -weights[3])], "four" + + +def quotient_ring_certificate(): + modulus = 9 + tensors = set() + parameter_count = 0 + for gamma, alpha, beta in itertools.product(range(modulus), repeat=3): + tensors.add((gamma * alpha ** 3 % modulus, 3 * gamma * alpha ** 2 * beta % modulus, + 3 * gamma * alpha * beta ** 2 % modulus, gamma * beta ** 3 % modulus)) + parameter_count += 1 + projections = {tensor[:3] for tensor in tensors} + pair_sums = {tuple((x + y) % modulus for x, y in zip(left, right, strict=True)) + for left in projections for right in projections} + need(parameter_count == 729 and len(tensors) == 33 and len(projections) == 21, + "complete physical-coefficient residue enumeration") + need(len(pair_sums) == 57, "all projected two-cube sums") + need(not any(first == second == 0 and third != 0 for first, second, third in pair_sums), + "two cubes cannot have only a nonzero ab-squared projected coefficient") + excluded, targets = [], {} + for residue in range(modulus): + defect = defect_for(residue + modulus) + target = tuple(defect.get(monomial, Fraction(0)) for monomial in CUBICS[:3]) + need(all(coefficient.denominator == 1 for coefficient in target), "integral quotient-ring target") + projected = tuple(coefficient.numerator % modulus for coefficient in target) + targets[str(residue)] = projected + if projected not in pair_sums: + excluded.append(residue) + need(set(excluded) == LOW_RESIDUES, "exact pure-b obstruction residue classes") + return {"modulus": modulus, "physical_parameter_triples": parameter_count, + "weighted_cube_tensors": len(tensors), "projected_tensors": len(projections), + "ordered_projected_pairs": len(projections) ** 2, "distinct_pair_sums": len(pair_sums), + "excluded_residues": excluded, "target_projections": targets} + + +def verify_arity(arity): + defect = defect_for(arity) + need(defect.get((3, 0, 0), 0) == 0 and defect[(2, 1, 0)] != 0, + "one mixed cube plus pure-b reads cannot supply the coefficient pattern") + program, family = restoration_program(arity, defect) + final, counts = execute(entry_after_ladder(arity), program) + need(final == desired_state(arity), "full arbitrary-input source and accumulator restoration") + expected = 4 if arity % 9 in LOW_RESIDUES else 3 + need(counts["queries"] == expected and counts["entry_b_queries"] >= 1, + "nonzero entry-b read and stated query count") + if family == "nonmonic_three": + need(counts["frames"] == 2 and counts["shears"] == 2, "declared nonmonic source-frame schedule") + return family + + +def controls(): + arity = 10 + initial, desired = entry_after_ladder(arity), desired_state(arity) + program, family = restoration_program(arity, defect_for(arity)) + need(family == "nonmonic_three", "nonmonic mutation fixture") + no_restore, _ = execute(initial, program[:5] + program[6:]) + need(no_restore["y"] == desired["y"] and no_restore["a"] != A, + "a correct accumulator cannot mask an unrestored source") + early_b = program[:4] + [program[-1]] + program[4:-1] + wrong_source, counts = execute(initial, early_b) + need(wrong_source["a"] == A and wrong_source["b"] == B + and wrong_source["y"] != desired["y"] and counts["entry_b_queries"] == 0, + "temporary second slot is not the entry-b line") + wrong_sign = list(program) + wrong_sign[1] = ("read_a", -wrong_sign[1][1]) + need(execute(initial, wrong_sign)[0]["y"] != desired["y"], "wrong query sign is observable") + try: + execute(initial, [("frame", (3, 0, 0, 1))]) + except ValueError as error: + need(str(error) == "source frame determinant must be a dyadic unit", "specific nonunit-frame rejection") + else: + raise ValueError("a frame requiring division by three was accepted") + unrestricted = [("shift", -1), ("read_a", -1), ("shift", -1), + ("read_a", -1), ("shift", -1), ("read_a", 2)] + final, counts = execute(entry_after_ladder(3), unrestricted) + need(final == desired_state(3) and counts["queries"] == 3 and counts["entry_b_queries"] == 0, + "r3 has an unrestricted three-query repair outside the pure-b contract") + return {"negative": ["missing_source_restore", "reading_temporary_b_slot", + "wrong_query_sign", "nonunit_source_frame"], + "positive_scope": ["r3_three_queries_without_entry_b_read"]} + + +def main(): + quotient = quotient_ring_certificate() + large_arities = [9 * 2 ** 80 + residue for residue in range(9)] + arities = sorted(set(range(3, 129)) | set(large_arities)) + families = {"old_three": 0, "nonmonic_three": 0, "four": 0} + for arity in arities: + families[verify_arity(arity)] += 1 + control_results = controls() + result = {"claim_type": "exact finite quotient-ring certificate and symbolic schedule checks", + "quotient_ring": quotient, "consecutive_arities": "3..128", + "large_arities": large_arities, "whole_state_schedule_checks": len(arities), + "schedule_families": families, "negative_controls": len(control_results["negative"]), + "positive_scope_controls": len(control_results["positive_scope"]), + "controls": control_results, "formal_kernel_or_full_supplier_proof": False} + print(json.dumps(result, sort_keys=True)) + print("PASS_INDEPENDENT_CUBIC_PURE_B_BOUNDARY") + + +if __name__ == "__main__": + main() diff --git a/research/cubic-pure-b-boundary/sources/pr6212-PROOF.md b/research/cubic-pure-b-boundary/sources/pr6212-PROOF.md new file mode 100644 index 0000000000..a1c41a9afc --- /dev/null +++ b/research/cubic-pure-b-boundary/sources/pr6212-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/cubic-pure-b-boundary/verify.py b/research/cubic-pure-b-boundary/verify.py new file mode 100644 index 0000000000..1afcd513a6 --- /dev/null +++ b/research/cubic-pure-b-boundary/verify.py @@ -0,0 +1,362 @@ +#!/usr/bin/env python3 +"""Finite exact certificates for cubic repairs containing an entry-b cube. + +Prepared by apoursh with substantial OpenAI Codex assistance. Apache-2.0. +PR6212 supplies the preceding dyadic repair results, retaining Nick Petalas's +PR6200 contract and the Sricharan Vagvala/Adam Gall/Hanson Sun lineage. +No predecessor executable is imported. Universal claims rest on PROOF.md; +this program distinguishes full original-child replays from closed-defect +fixtures and classifies each query in entry-source coordinates. +""" + +import hashlib +import itertools +import json +from fractions import Fraction +from pathlib import Path + + +SOURCE_HEAD = "9c159482e0495b6a97e17e629debe66a0ceb9466" +THREE_RESIDUES = {0, 1, 2, 5, 8} +ENTRY = ((1, 0, 0, 0, 0), (1, 0), (0, 1)) +IDENTITY = ((1, 0), (0, 1)) +# Output basis: y_entry,a_entry^3,a_entry^2*b_entry,a_entry*b_entry^2,b_entry^3. +# Source vectors use the ordered basis 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") + need(manifest["predecessor"] == { + "pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/6212", + "head": SOURCE_HEAD, "author": "apoursh", "license": "Apache-2.0", + }, "exact predecessor identity") + documents = manifest["documents"] + need(len(documents) == 1 and documents[0]["path"] == "sources/pr6212-PROOF.md", + "one exact predecessor proof") + item = documents[0] + source_path = "research/dyadic-cubic-repair/PROOF.md" + need(item["source_path"] == source_path, "predecessor source path") + need(item["source_url"] == "https://raw.githubusercontent.com/" + f"apoursh/integer-mult-bounds/{SOURCE_HEAD}/{source_path}", "exact-head source 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"]) + return {item["path"]: digest} + + +def add(left, right): + return tuple(a+b for a, b in zip(left, right, strict=True)) + + +def dyadic(value): + need(isinstance(value, (int, Fraction)), "exact rational scalar") + denominator = Fraction(value).denominator + return denominator & (denominator-1) == 0 + + +def determinant(matrix): + return matrix[0][0]*matrix[1][1] - matrix[0][1]*matrix[1][0] + + +def frame_inverse(matrix): + need(len(matrix) == 2 and all(len(row) == 2 for row in matrix), "two-source frame shape") + need(all(dyadic(value) for row in matrix for value in row), "dyadic frame entries") + det = determinant(matrix) + need(det != 0 and dyadic(Fraction(1)/det), "source frame invertible over dyadics") + a, b = matrix[0] + c, d = matrix[1] + return ((Fraction(d)/det, -Fraction(b)/det), (-Fraction(c)/det, Fraction(a)/det)) + + +def frame_apply(matrix, a, b): + return tuple(add(tuple(row[0]*x for x in a), tuple(row[1]*x for x in b)) + for row in matrix) + + +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 run(events, state=ENTRY): + output, a, b = state + queries = [] + for opcode, payload, label in events: + if opcode == "shear": + need(dyadic(payload) and payload != 0, "nonzero dyadic shear") + a = add(a, tuple(payload*x for x in b)) + elif opcode == "frame": + frame_inverse(payload) + a, b = frame_apply(payload, a, b) + elif opcode == "cube": + source, weight = payload + need(source in ("a", "b"), "cube reads a source register") + need(dyadic(weight) and weight != 0, "nonzero dyadic query weight") + form = a if source == "a" else b + output = add(output, weighted_cube(weight, form)) + queries.append((weight, form, source, label)) + else: + raise ValueError("event outside declared source/query alphabet") + return (output, a, b), queries + + +def inverse(events): + result = [] + for opcode, payload, label in reversed(events): + if opcode == "frame": + result.append((opcode, frame_inverse(payload), label)) + elif opcode == "shear": + result.append((opcode, -payload, label)) + elif opcode == "cube": + result.append((opcode, (payload[0], -payload[1]), label)) + else: + raise ValueError("event outside declared source/query alphabet") + return result + + +def pure_entry_b(queries): + return [query for query in queries if query[0] != 0 and query[1][0] == 0 + and query[1][1] != 0] + + +def moments(r): + need(isinstance(r, int) and r >= 3, "arity at least three") + return r*(r-1)//2, r*(r-1)*(2*r-1)//6 + + +def endpoint(r): + return ((1, r, 0, 0, 0), ENTRY[1], ENTRY[2]) + + +def drifting_endpoint(r): + first, second = moments(r) + return ((1, r, 3*first, 3*second, first*first), (1, r), (0, 1)) + + +def original_children(r): + return [event for i in range(r) for event in ( + ("cube", ("a", 1), f"child-{i}-read"), + ("shear", 1, f"child-{i}-shift"))] + + +def eager_program(r): + return [event for i in range(r) for event in ( + ("cube", ("a", 1), f"child-{i}-read"), + ("shear", 1, f"child-{i}-shift"), + ("shear", -1, f"eager-{i}-restore"))] + + +def high_class_repair(r): + need(r % 9 in (0, 1), "high-class residue") + first, _ = moments(r) + epsilon = -1 if r % 9 == 0 else 1 + q = (r if epsilon == -1 else r-1)//3 + need(first % 9 == 0, "integer nonmonic query weight") + weight, pure_weight = first//9, first*(3*first-1)//9 + matrix = ((3, epsilon), (1, 0)) + undo = ((0, 1), (epsilon, -3*epsilon)) + need(frame_inverse(matrix) == undo, "literal unimodular inverse") + return [ + ("shear", q-r, "repair-first-source"), + ("cube", ("a", epsilon*3*first), "repair-monic-query"), + ("frame", matrix, "repair-nonmonic-frame"), + ("cube", ("a", -epsilon*weight), "repair-nonmonic-query"), + ("frame", undo, "repair-undo-frame"), + ("shear", -q, "repair-final-source"), + ("cube", ("b", -pure_weight), "repair-entry-b-query"), + ] + + +def old_three_repair(r): + need(r % 3 == 2, "old three-query residue") + first, _ = moments(r) + t, s = (r+1)//3, (r-2)//3 + numerator = first*(r-2)*(r+1) + need(numerator % 6 == 0, "integer old pure-b weight") + return [ + ("shear", t-r, "repair-first-source"), + ("cube", ("a", -first), "repair-first-query"), + ("shear", s-t, "repair-second-source"), + ("cube", ("a", first), "repair-second-query"), + ("shear", -s, "repair-final-source"), + ("cube", ("b", -numerator//6), "repair-entry-b-query"), + ] + + +def four_repair(r): + first, second = moments(r) + need((first-second) % 2 == 0, "integer universal weights") + return [ + ("shear", 1-r, "repair-first-source"), + ("cube", ("a", -(first+second)//2), "repair-first-query"), + ("shear", -2, "repair-second-source"), + ("cube", ("a", -(second-first)//2), "repair-second-query"), + ("shear", 1, "repair-final-source"), + ("cube", ("a", second), "repair-third-query"), + ("cube", ("b", -(first*first-first)), "repair-entry-b-query"), + ] + + +def selected_repair(r): + moments(r) + if r % 9 in (0, 1): + return high_class_repair(r), "new-three" + if r % 3 == 2: + return old_three_repair(r), "old-three" + return four_repair(r), "four" + + +def check_program(r, expand_children): + repair, kind = selected_repair(r) + drift = drifting_endpoint(r) + final, queries = run(repair, drift) + need(final == endpoint(r), "arbitrary-input repaired endpoint") + need(run(inverse(repair), final)[0] == drift, "exact repair inverse") + need(len(pure_entry_b(queries)) == 1, "one nonzero cube of entry b") + expected = 3 if r % 9 in THREE_RESIDUES else 4 + need(len(queries) == expected, "predicted nonzero query count") + shears = sum(event[0] == "shear" for event in repair) + frames = sum(event[0] == "frame" for event in repair) + need((shears, frames) == ((2, 2) if kind == "new-three" else (3, 0)), + "complete logical source-event count") + need(all(Fraction(query[0]).denominator == 1 for query in queries), "integer query attainment") + if kind == "new-three": + after_frame = run(repair[:3], drift)[0] + need(after_frame[2] != ENTRY[2], "nonmonic frame really changes b temporarily") + need(run(repair[:5], drift)[0][2] == ENTRY[2], "inverse frame restores entry b") + if expand_children: + children = original_children(r) + need(run(children)[0] == drift, "literal retained-child chronology") + program = children+repair + need(program[:2*r] == children, "all original children retained unchanged") + need(run(program)[0] == final, "full retained-child program") + need(run(eager_program(r))[0] == final, "exact eager comparison") + need(run(inverse(program), final)[0] == ENTRY, "literal full-program inverse") + return {"kind": kind, "queries": len(queries), "shears": shears, "frames": frames} + + +def divided_moments(values): + gamma, alpha, beta, delta, eta, theta = values + return ((gamma*alpha**3 + delta*eta**3) % 3, + (gamma*alpha*alpha*beta + delta*eta*eta*theta) % 3, + (gamma*alpha*beta*beta + delta*eta*theta*theta) % 3) + + +def modular_certificate(): + tested, antecedents = 0, 0 + for values in itertools.product(range(3), repeat=6): + zeroth, first, second = divided_moments(values) + tested += 1 + if zeroth == first == 0: + antecedents += 1 + need(second == 0, "two forms: M0=M1=0 implies M2=0 modulo three") + need(tested == 729, "complete six-variable residue census") + targets = [] + for r in range(3, 257): + first, second = moments(r) + blocked = first % 3 == 0 and second % 3 != 0 + need(blocked == (r % 9 not in THREE_RESIDUES), "exact obstruction residue pattern") + if blocked: + targets.append(r) + return {"residue_assignments": tested, "antecedent_assignments": antecedents, + "excluded_arities_in_scan": len(targets), "excluded_residues": [3, 4, 6, 7]} + + +def expect_rejected(function, diagnostic): + try: + function() + except ValueError as error: + need(str(error) == diagnostic, "specific mutation diagnostic") + else: + raise ValueError("mutation unexpectedly accepted: " + diagnostic) + + +def mutation_controls(): + r, drift = 10, drifting_endpoint(10) + repair = high_class_repair(r) + expect_rejected(lambda: run([("frame", ((3, 1), (6, 2)), "singular")], drift), + "source frame invertible over dyadics") + expect_rejected(lambda: run([("frame", ((3, 0), (0, 1)), "nonunit")], drift), + "source frame invertible over dyadics") + wrong_inverse = repair[:] + wrong_inverse[4] = ("frame", ((0, 1), (1, -2)), "wrong-inverse") + need(run(wrong_inverse, drift)[0] != endpoint(r), "wrong inverse rejected") + need(run(repair[:2]+repair[3:], drift)[0] != endpoint(r), "dropped forward frame rejected") + no_inverse, queries = run(repair[:4]+repair[5:], drift) + need(no_inverse[2] != ENTRY[2] and not pure_entry_b(queries), "temporary b must be restored") + no_shear = run(repair[:5]+repair[6:], drift)[0] + need(no_shear[0] == endpoint(r)[0] and no_shear[1] != ENTRY[1], "final source shear necessary") + no_b, queries = run(repair[:-1], drift) + need(no_b[1:] == ENTRY[1:] and no_b[0] != endpoint(r)[0] and not pure_entry_b(queries), + "nonzero entry-b correction necessary") + moved_b = repair[:3]+[repair[-1]]+repair[3:-1] + wrong_output, queries = run(moved_b, drift) + need(wrong_output[1:] == ENTRY[1:] and wrong_output[0] != endpoint(r)[0], + "current-b query is not necessarily an entry-b query") + need(any(query[2] == "b" for query in queries) and not pure_entry_b(queries), + "entry-coordinate pure-b classification") + _, swapped = run([("frame", ((0, 1), (1, 0)), "swap"), + ("cube", ("a", 1), "entry-b-via-a")]) + need(len(pure_entry_b(swapped)) == 1, "entry-b can be held in current a") + changed_weight = repair[:] + changed_weight[3] = ("cube", ("a", repair[3][1][1]+1), "wrong-weight") + need(run(changed_weight, drift)[0] != endpoint(r), "nonmonic weight mutation") + children = original_children(r) + need(run(children[1:]+repair)[0] != endpoint(r), "all original cube calls necessary") + need(run([children[1], children[0], *children[2:], *repair])[0] != endpoint(r), + "read-then-shear chronology necessary") + need(divided_moments((1, 1, 0, 2, 1, 1)) == (0, 2, 2), "first moment cannot be omitted") + need(divided_moments((1, 1, 1, 1, 1, 2)) == (2, 0, 2), "zeroth moment cannot be omitted") + first, second = moments(3) + need((3*first) % 3 == (3*second) % 3 == (first*first) % 3 == 0 and second % 3 != 0, + "raw coefficient reduction loses the divided-moment obstruction") + unrestricted = [("shear", -2, "outside-class"), ("cube", ("a", -1), "outside-class"), + ("shear", 1, "outside-class"), ("cube", ("a", -1), "outside-class"), + ("shear", -2, "outside-class"), ("cube", ("a", 2), "outside-class")] + result, queries = run(unrestricted, drifting_endpoint(3)) + need(result == endpoint(3) and len(queries) == 3 and not pure_entry_b(queries), + "unrestricted r3 three-query repair is outside the pure-b class") + expect_rejected(lambda: moments(2), "arity at least three") + return ["singular-frame", "nonunit-determinant", "wrong-frame-inverse", + "dropped-forward-frame", "unrestored-temporary-b", "omitted-final-source-shear", + "omitted-entry-b-correction", "current-b-versus-entry-b", "entry-b-in-current-a", + "nonmonic-query-weight", "omitted-original-reader", "reversed-child-chronology", + "missing-first-moment", "missing-zeroth-moment", "raw-versus-divided-moments", + "unrestricted-r3-outside-class", "arity-two-outside-domain"] + + +def main(): + package = Path(__file__).resolve().parent + hashes = authenticate_sources(package) + counts = {"new-three": 0, "old-three": 0, "four": 0} + original_count = 0 + for r in range(3, 257): + receipt = check_program(r, expand_children=True) + counts[receipt["kind"]] += 1 + original_count += r + large = [] + for r in range(1_000_000, 1_000_009): + large.append({"r": r, **check_program(r, expand_children=False)}) + modular = modular_certificate() + controls = mutation_controls() + print("PASS_CUBIC_PURE_B_BOUNDARY " + json.dumps({ + "source_head": SOURCE_HEAD, "source_sha256": hashes, + "full_program_scan": {"first": 3, "last": 256, "count": 254}, + "programs_by_construction": counts, "retained_original_children": original_count, + "large_closed_defect_only": large, "modular_divided_moment_certificate": modular, + "controls": controls, "nonzero_entry_b_queries_per_repair": 1, + "new_three_event_bill": {"cube_queries": 3, "shears": 2, "frames": 2}, + "scope": "finite certificates; universal restricted-class proof is in PROOF.md", + "no_unrestricted_rank_or_backend_saving_claim": True, + }, sort_keys=True)) + + +if __name__ == "__main__": + main()