From e0fa68e6923d709b5b3b9a80fe847d0d9011046b Mon Sep 17 00:00:00 2001 From: CubeJerry <80299683+CubeJerry@users.noreply.github.com> Date: Fri, 30 Oct 2026 17:32:41 +0800 Subject: [PATCH] Classify dyadic cubic repairs on directions 0,d,2d Add the r = 2^s + 1 chronological repair and the exact scoped denominator obstruction. Preserve predecessor credit, exact source pins and all inherited supplier assumptions. No new kappa. Prepared for @CubeJerry with substantial OpenAI Codex assistance. --- .../CROSSCHECK.json | 165 ++++++++ .../cubic-equal-step-classification/PROOF.md | 301 ++++++++++++++ .../cubic-equal-step-classification/README.md | 122 ++++++ .../RESULT.json | 297 ++++++++++++++ .../SOURCES.json | 44 ++ .../cubic-equal-step-classification/TASK.json | 178 +++++++++ .../VALIDATION.md | 120 ++++++ .../VERIFY.json | 62 +++ .../crosscheck.py | 215 ++++++++++ .../sources/pr6246-PROOF.md | 290 ++++++++++++++ .../cubic-equal-step-classification/verify.py | 376 ++++++++++++++++++ 11 files changed, 2170 insertions(+) create mode 100644 research/cubic-equal-step-classification/CROSSCHECK.json create mode 100644 research/cubic-equal-step-classification/PROOF.md create mode 100644 research/cubic-equal-step-classification/README.md create mode 100644 research/cubic-equal-step-classification/RESULT.json create mode 100644 research/cubic-equal-step-classification/SOURCES.json create mode 100644 research/cubic-equal-step-classification/TASK.json create mode 100644 research/cubic-equal-step-classification/VALIDATION.md create mode 100644 research/cubic-equal-step-classification/VERIFY.json create mode 100644 research/cubic-equal-step-classification/crosscheck.py create mode 100644 research/cubic-equal-step-classification/sources/pr6246-PROOF.md create mode 100644 research/cubic-equal-step-classification/verify.py diff --git a/research/cubic-equal-step-classification/CROSSCHECK.json b/research/cubic-equal-step-classification/CROSSCHECK.json new file mode 100644 index 0000000000..10f8762e37 --- /dev/null +++ b/research/cubic-equal-step-classification/CROSSCHECK.json @@ -0,0 +1,165 @@ +{ + "arity_domain": [ + 3, + 257 + ], + "centered_scope_control": "r50 weights -1,-33,34 on slopes -35,0,35", + "eligible_arity_and_twice_spacing": [ + [ + 3, + 2 + ], + [ + 4, + 4 + ], + [ + 5, + 4 + ], + [ + 8, + 8 + ], + [ + 9, + 8 + ], + [ + 16, + 16 + ], + [ + 17, + 16 + ], + [ + 32, + 32 + ], + [ + 33, + 32 + ], + [ + 64, + 64 + ], + [ + 65, + 64 + ], + [ + 128, + 128 + ], + [ + 129, + 128 + ], + [ + 256, + 256 + ], + [ + 257, + 256 + ] + ], + "eliminated_systems": 510, + "large_new_branch_fixtures": [ + [ + 1, + "3", + [ + "-2", + "1", + "1" + ] + ], + [ + 2, + "5", + [ + "-15/4", + "5/2", + "5/4" + ] + ], + [ + 5, + "33", + [ + "-869/32", + "341/16", + "187/32" + ] + ], + [ + 7, + "129", + [ + "-13717/128", + "5461/64", + "2795/128" + ] + ], + [ + 11, + "2049", + [ + "-3496277/2048", + "1398101/1024", + "700075/2048" + ] + ], + [ + 17, + "131073", + [ + "-14316623189/131072", + "5726623061/65536", + "2863377067/131072" + ] + ], + [ + 31, + "2147483649", + [ + "-3843071683096565077/2147483648", + "1537228672809129301/1073741824", + "768614337478306475/2147483648" + ] + ], + [ + 64, + "18446744073709551617", + [ + "-283568639100782052895368878229994952021/18446744073709551616", + "113427455640312821154458202477256070485/9223372036854775808", + "56713727820156410586452473275482811051/18446744073709551616" + ] + ], + [ + 128, + "340282366920938463463374607431768211457", + [ + "-96493407697763496186309154173906589877895128404827605931279673976976825472341/340282366920938463463374607431768211456", + "38597363079105398474523661669562635951089994888546854679819194669304376546645/170141183460469231731687303715884105728", + "19298681539552699237261830834781317975715138627733896571641284638368072379051/340282366920938463463374607431768211456" + ] + ] + ], + "method": "binary block concatenation; generic rational elimination; normalized nonmonic forms", + "negative_controls": [ + "wrong_spacing:r=33:d=15", + "wrong_spacing:r=33:d=-16", + "wrong_spacing:r=33:d=1/3", + "wrong_spacing:r=129:d=65", + "zero_spacing_singular", + "r14_rational_two_query_weight_not_dyadic" + ], + "nonmonic_systems": 1020, + "status": "PASS_CUBIC_EQUAL_STEP_CROSSCHECK", + "systems_sha256": "ed8354a1e2bcbf5c83bb7de5940b3b6b14c8a8e5582495aef2658a715e1b38db" +} diff --git a/research/cubic-equal-step-classification/PROOF.md b/research/cubic-equal-step-classification/PROOF.md new file mode 100644 index 0000000000..7895356ee8 --- /dev/null +++ b/research/cubic-equal-step-classification/PROOF.md @@ -0,0 +1,301 @@ +# Exact classification of equal-step dyadic cubic repairs + +Prepared for @CubeJerry with substantial OpenAI Codex assistance. Apache-2.0. +The fixed reader interface, chronological defect and unrestricted two-query +obstruction are due to Nick Petalas (#6200) and apoursh (#6212). +AAAmirinu's #6246 supplies the power-of-two branch. The new contribution is +the exhaustive equal-step classification, its `r = 2^s + 1` branch, and the +actual chronological repair for that branch. This is a local exact-arithmetic +result, not an admitted supplier or a runtime improvement. + +## Contract and theorem + +Let `R = Z[1/2]`. Three distinct streams enter with arbitrary values `(Y,A,B)`. +Retain all `r >= 3` children, in their original order and with their interiors +unchanged: + +```text +y += a^3 +a += b +``` + +The eager comparator restores `a -= b` after every child. It finishes at +`(Y + r A^3, A, B)`. Deferred restoration leaves +`(Y + sum_(j=0)^(r-1) (A+jB)^3, A+rB, B)`. +There is no intermediate observation, output feedback into sources, nonlinear +source change, child fusion or output recoding. Source transformations are +invertible linear maps over R and are charged separately. A query adds a +fixed signed R-weighted cube of a source linear form to y. + +Call a three-query repair **equal-step with entry-A at an end** when its three +entry-source directions, in any order, have slopes `0,d,2d` for a nonzero +rational d: each source form is a nonzero multiple of one of +`A, A+dB, A+2dB`. Allow arbitrary nonmonic R-linear forms and arbitrary +`GL_2(R)` source frames. Every query weight is nonzero. This is a restriction +on directions in the entry coordinates, not on names of changing registers. + +**Theorem.** Such a repair exists exactly when either r or r-1 is a power +of two. Necessarily `2d = r` or `2d = r-1`, respectively. After monic +normalization its three weights are unique. The construction is realizable +using only `a += c b` source shears, with b unchanged throughout. + +For `r = 2^s + 1`, `s >= 1`, exactly three appended queries and three +integer source shears suffice. The unrestricted dyadic query minimum is +three by #6212; that lower bound is reused, not new. For `r = 2^s >= 4`, +the construction is exactly the five-event repair already given by #6246. +No statement excludes three unequal-step queries at any other arity. + +## Coefficient elimination forces two possible spacings + +The excess over the eager output, from #6200, is + +```text +f_r = 3 S1 A^2 B + 3 S2 A B^2 + S1^2 B^3, +S1 = r(r-1)/2, S2 = r(r-1)(2r-1)/6. +``` + +A repair subtracts f_r and restores both sources. Negating all query +weights gives a three-cube decomposition of f_r. Normalizing a physical +term `gamma (alpha A + beta B)^3`, with alpha nonzero, gives weight +`gamma alpha^3`, which lies in R. The slope `beta/alpha` may initially be +any rational: no unsupported assumption that a normalized slope is dyadic +is needed. Thus any allowed nonmonic repair implies + +```text +f_r = w0 A^3 + w1 (A+dB)^3 + w2 (A+2dB)^3, wi in R. +``` + +Comparing the four coefficients gives + +```text +w0 + w1 + w2 = 0, +d (w1 + 2w2) = S1, +d^2 (w1 + 4w2) = S2, +d^3 (w1 + 8w2) = S1^2. +``` + +At each node t in `{0,d,2d}`, `t^3 = 3d t^2 - 2d^2 t`. +The last three equations therefore require +`S1^2 = 3d S2 - 2d^2 S1`. Since S1 is nonzero, substitution yields + +```text +0 = 2d^2 - (2r-1)d + r(r-1)/2 + = (2d-r)(2d-r+1)/2. +``` + +Hence the spacing must be `r/2` or `(r-1)/2`, even if nonmonic frames +initially allowed non-dyadic slopes. Conversely, for either spacing the +first three equations determine unique weights and the node identity +implies the fourth. Uniqueness follows from the distinct nodes, or directly +from + +```text +w2 = (S2 - d S1)/(2d^2), +w1 = (2d S1 - S2)/d^2, +w0 = -w1-w2. +``` + +Writing u=2d, the two possibilities are: + +| u | w0, at slope 0 | w1, at slope u/2 | w2, at slope u | +|---|---|---|---| +| r | `-(r-1)(5r+2)/(6r)` | `2(r^2-1)/(3r)` | `(r-1)(r-2)/(6r)` | +| r-1 | `-r(5r-7)/(6(r-1))` | `2r(r-2)/(3(r-1))` | `r(r+1)/(6(r-1))` | + +The first row is #6246's identity, credited in full. The second row is +the additional identity. Both are rational identities for every integer +r>=3; dyadic admissibility is a separate question. + +There is also a direct quadrature interpretation of the second row. +For u=r-1, let `a=r(r+1)/(6(r-1))` and `b=2r(r-2)/(3(r-1))`. +For every polynomial p of degree at most three, + +```text +sum_(j=0)^u p(j) = a [p(0)+p(u)] + b p(u/2). +``` + +To see this independently, center at u/2. Reflection j -> u-j kills the +odd centered moments on both sides. The constant and quadratic moments +give `2a+b=r` and `a u^2/2 = r(r^2-1)/12`, which determine a,b above. +Apply this to p(j)=(A+jB)^3 and subtract r A^3. The result is the second +row because `a-r=w0`, `b=w1`, `a=w2`. This uses classical polynomial +quadrature, not a new general quadrature theorem; the contribution is its +dyadic classification and source-restoring use at this repository interface. + +## Odd primes give the exact dyadic boundary + +In the first row, if an odd prime p divides r, its w2 numerator +`(r-1)(r-2)` is congruent to 2 modulo p. The denominator is divisible by +p, so that factor cannot cancel; w2 is not dyadic. In the second row, +an odd prime p dividing r-1 similarly sees numerator `r(r+1) = 2 mod p`, +again preventing cancellation. This argument includes p=3: the additional +factor 3 in the denominator does not help. + +Therefore the first row requires r to be a power of two, and the second +requires r-1 to be a power of two. Rescaling the physical forms cannot hide +the obstruction: each normalized weight `gamma alpha^3` still belongs to R. +This proves necessity for all allowed nonmonic forms and source frames, +not only the displayed shear implementation. + +Conversely, suppose r is a power of two. Its residue modulo 3 is 1 or 2, +so 3 divides all three displayed numerators in the first row. Cancellation +leaves denominators dividing 2r, a power of two. This is #6246's argument. +If r-1 is a power of two, r is 0 or 2 modulo 3. Thus 3 divides +`r(r+1)`, `r(r-2)` and `r(5r-7)`. The second row's denominators then divide +`2(r-1)`, also a power of two. All three weights are nonzero for r>=3. +This proves sufficiency of coefficient membership. The next section supplies +the missing chronological realization. Since consecutive positive powers +of two occur only at 1 and 2, the eligible spacing is unique for r>=3. + +## Six-event restoration for r = 2^s + 1 + +Put `u=r-1=2^s`, `d=u/2`, and take the second row's weights. Starting from +the actual deferred endpoint `a=A+rB`, append: + +```text +1. a -= b +2. y -= w2 a^3 +3. a -= d b +4. y -= w1 a^3 +5. a -= d b +6. y -= w0 a^3 +``` + +The three queries see `A+uB`, `A+dB`, and A in that order. Their sum is +`-f_r`. The source returns to A, b stays B, and y becomes `Y+rA^3` for +every incoming Y,A,B. No entry snapshot, clean scratch, lost dirty value +or alteration to an original child is used. Every source shear has +determinant one and an integer coefficient. Every query is invertible +because its source does not involve y. Reversing these six events and +negating their coefficients restores the deferred endpoint; reversing each +retained child as `a -= b; y -= a^3` then restores the original entry state. + +For the credited first row, u=r and the initial `a -= b` is absent; +the remaining five events are exactly #6246's schedule. Among schedules +restricted to b-preserving shears and these three query directions, the +source-shear counts are also minimal: a query cannot change a's slope. +The first row starts at one queried slope and must visit the other two, +requiring at least two changes. The second starts at the distinct slope r +and must visit all three, requiring at least three. The displayed orders +attain those bounds. This small visit-count argument is not a minimum for +arbitrary source frames or a physical movement tariff. + +At the new discriminating arity r=33: + +```text +f_33 = (187/32)(A+32B)^3 + (341/16)(A+16B)^3 - (869/32)A^3 + = 1584 A^2 B + 34320 A B^2 + 278784 B^3. +``` + +The actual repair has shears -1,-16,-16 and cube coefficients +`-187/32,-341/16,+869/32`, with the interleaving above. The first shear +is essential: applying the first cube at the deferred slope 33 corrupts +the output even if the sources are later restored. + +## What is new, and what is deliberately not claimed + +The existence of three queries for r=3 belongs to #6212; this formula +reproduces its identity. For `r=2^s+1`, powers of two modulo nine cycle as +`2,4,8,7,5,1`, so r cycles as `3,5,0,8,6,2`. +The #6215 pure-original-B constructions already attain three in the +classes 5,0,8,2. Its four-query floor applies to classes 3 and 6 only +when a nonzero original-B cube is required. Every direction here has a +nonzero A coefficient and so is outside that restricted family. + +Relative to the three pinned predecessors, the new count cases include +`s = 5 mod 6` and `s = 1 mod 6, s>=7`: the first are r=33 and r=129. +They are not covered by #6246's power-of-two arities. The classification +also proves that this exact equal-step idea cannot extend to other r. +These are comparisons with those sources, not a literature-priority claim. + +For example r=14 is excluded by the equal-step theorem but #6212 supplies +three integer queries at slopes 5,4 and the pure-B direction. The verifier +executes that credited schedule as a positive scope control. Consequently, +failure of equal-step membership is explicitly not a four-query lower bound. +The general three-versus-four dyadic classification remains open. + +The location of the zero slope is also essential. At r=50 the identity + +```text +f_50 = -(A-35B)^3 - 33 A^3 + 34(A+35B)^3 +``` + +has equally spaced directions with zero in the middle. From the deferred +slope 50, visit slopes -35,35,0 with shears -85,70,-35 and subtract the +displayed cubes. This is an exact three-query repair although neither 50 +nor 49 is a power of two. It is a positive control outside the stated +`0,d,2d` family, not a counterexample to the theorem or a new query minimum: +#6212 already attains three queries at r=50 because 50=2 modulo 3. + +## Complete logical bill and expansion gate + +Use the predecessor's complete-event prices `Q_c^a(N)` for a query +`y += c a^3` and `L_c(N)` for `a += c b`. A query price must include its +coefficient use, source access, private work/restoration and return. +Different coefficients retain different symbols. Let S_r(N) account for +all additional preparation/controller, routing, precision and storage work +not included in these complete-event prices. It is unknown, not zero. + +The eager program costs + +```text +E_r(N) = r Q_1^a(N) + r L_1(N) + r L_-1(N). +``` + +For the new branch the complete symbolic deferred bill is + +```text +D_r(N) = r Q_1^a(N) + r L_1(N) + + L_-1(N) + Q_-w2^a(N) + 2 L_-d(N) + + Q_-w1^a(N) + Q_-w0^a(N) + S_r(N). +``` + +All original children remain paid. Thus a favorable replacement requires + +```text +Q_-w2^a(N) + Q_-w1^a(N) + Q_-w0^a(N) + 2 L_-d(N) + S_r(N) + < (r-1) L_-1(N). +``` + +If a physical backend recursively implements Q or L, its complete recurrence +must be substituted into these symbols; no recursive child may be dropped. +This package supplies no such backend, numeric inequality or admitted call. +Dyadic membership does not make coefficients free or establish rounded +correctness. Preparing r and weights, division/cancellation by 3, dispatch, +native realization, error propagation, source placement and any scratch +allocation/erasure still require the stated charges or separate proofs. +The expansion decision is to stop after this logical classification. + +No new kappa. All five selected framework assumptions remain: native maps +at arbitrary column multiplicity, owned allocation/erasure, uniform compiler +closure, precision/tape implementation, and analytic recovery. This is neither +a finite-field statement nor a full multiplier proof, supplier admission, +independent human review or formal-kernel verification. + +## Evidence and next questions + +The written elimination and odd-prime argument prove the infinite-domain +classification. `verify.py` checks polynomial identities, exact finite +membership, literal symbolic and dirty-value schedules, their inverses and +semantic rejection controls. `crosscheck.py` derives weights by separate +exact elimination and derives the defect from concatenated reader blocks. +Neither imports predecessor executable code. These computations corroborate +the proof; their finite domains do not establish it alone. Exact executed +coverage is recorded in `RESULT.json` and `VALIDATION.md`. + +Open next questions, with their first steps and blockers, are in README.md +and TASK.json. In particular, changing the direction pattern may escape this +classification; a failed equal-step search cannot close that larger problem. + +## Credit + +Nick Petalas (#6200) supplied the fixed cubic reader, defect, rational query +criterion and restoring-schedule question. Apoursh (#6212) supplied the +dyadic localization obstruction, the unrestricted three-query lower bound +for r>2, earlier three/four-query constructions and the known r=3 identity; +apoursh (#6215) supplied the pure-original-B boundary and its attainments. +AAAmirinu (#6246) supplied the entire power-of-two branch, the two-shear +chronology and its proof. Sricharan Vagvala/theon199 (#1532), Adam Gall +(#1205) and Hanson Sun (#1246) retain the quadratic and linear lineage. +Coefficient comparison, Vandermonde uniqueness and localization arguments +are classical. Source proofs are retained or source-pinned unchanged. diff --git a/research/cubic-equal-step-classification/README.md b/research/cubic-equal-step-classification/README.md new file mode 100644 index 0000000000..d31b3bbb08 --- /dev/null +++ b/research/cubic-equal-step-classification/README.md @@ -0,0 +1,122 @@ +# Classify dyadic cubic repairs on directions 0,d,2d + +For the fixed cubic reader of Nick Petalas's PR6200, a three-query dyadic +repair on entry-source directions `A, A+dB, A+2dB` exists **exactly when r +or r-1 is a power of two** (`r>=3`). The theorem allows arbitrary nonmonic +dyadic forms on these directions and general dyadic source frames. The +entry-A direction must be at an end of the progression. + +The proof forces `d=r/2` or `d=(r-1)/2`; an odd prime dividing the relevant +denominator cannot cancel. The first branch is AAAmirinu's PR6246. The +additional branch `r=2^s+1` has three nonzero weighted-cube queries and +three integer source shears, retaining every original child and restoring +arbitrary incoming sources/output exactly. Apoursh's PR6212 already supplies +the unrestricted three-query lower bound for r>2, so this branch attains it. + +At the first new count case r=33, subtract + +```text +(187/32)(A+32B)^3 + (341/16)(A+16B)^3 - (869/32)A^3 +``` + +using the actual six-event schedule in [PROOF.md](PROOF.md). The new cases +relative to PR6212/6215/6246 include r=33 and r=129 and their infinite +exponent classes. The r=3 identity and the earlier three-query residue +classes retain predecessor credit. Classical three-node quadrature explains +the construction; no historical-priority claim is made. + +**No new κ.** This is a local coefficient/restoration result. Weighted queries +and source changes keep their individual prices in the complete symbolic +event bill. No physical backend, favorable complete cost recurrence, rounded +implementation or supplier admission is supplied. All five selected framework +assumptions remain; the selected result is unchanged. + +## Why the restriction matters + +- The r=14 unequal-direction integer repair from PR6212 succeeds outside + this family. Equal-step exclusion is not a general four-query lower bound. +- At r=50, directions `-35,0,35` also give three integer queries. This is + equally spaced with zero **in the middle**, and is an explicit positive + scope control. The theorem requires directions `0,d,2d`. +- A formal coefficient identity alone is insufficient. Omitting the first + r=33 source shift, or querying before it, fails the actual dirty-state + execution. Both mutations are rejected. + +## Reproduce + +From the repository root, with CPython 3.12 and no third-party dependencies: + +```sh +python3.12 -B scripts/research_package.py --package research/cubic-equal-step-classification +``` + +Expected: `PASS_REGISTERED_RESEARCH_PACKAGE`, after both scripts pass in +normal and optimized Python. Direct checks are `verify.py` and `crosscheck.py` +inside this directory. Neither imports predecessor executable code. Committed +receipts [RESULT.json](RESULT.json) and [CROSSCHECK.json](CROSSCHECK.json) +record the exact domains and results; [VALIDATION.md](VALIDATION.md) records +checks actually executed, environment, transport tests and limitations. + +The written proof establishes the infinite-domain classification. Finite +evidence includes twelve polynomial identities; both rational branches for +r=3..1024; 10,944 spacing tests; fifteen literal symbolic child/repair programs; +189 dirty rational cases with 56,916 events including inverses; and fourteen +primary rejection controls. The separate implementation derives defects by +binary block concatenation and weights by rational Gaussian elimination, +checks 510 systems and 1,020 nonmonic rescalings, and has six controls. +Both paths check very large arities through `2^128+1` without claiming to +execute that many original children. The two scope-positive programs above +are separately checked. These are two implementations by the same +AI-assisted contributor, not independent human or formal-kernel acceptance. + +## Sources, overlap and scope + +Base: `2485805a6d47f36ea83ddde6327d453ac82d44dc`, canonical main, priority +revision 8. The selected certificate is PR6030, κ=0.003125804; historical +priority prose still naming PR5599 is not used as the frontier. + +Exact predecessor heads: + +| Source | Head | What is reused | +|---|---|---| +| PR6212, apoursh | `9c159482e0495b6a97e17e629debe66a0ceb9466` | Interface, dyadic lower bound, known r=3 and integer constructions | +| PR6215, apoursh | `0013c2b40c522ccd19670a8fbd4b1531f13fed2b` | Pure-original-B classification and covered residue classes | +| PR6246, AAAmirinu | `3d21b913efac1e3731bee7f0f4f4a8a84fecec37` | Entire power-of-two branch and its source chronology | + +[SOURCES.json](SOURCES.json) pins source bytes and historical catalogue/selected +provenance. The first two proof inputs are unchanged main files. The pending +PR6246 proof is retained byte-for-byte with its Git blob and SHA256, without +requiring that pending commit as an ancestor. No predecessor code, frozen +archive, selected certificate, shared script or upstream file is modified. + +The broader `joint-query-controller` card is explicitly changed to this local +side result. [TASK.json](TASK.json) records the initial local claim, three +candidates, seed, stop rule, bounded overlap and refresh checks. No sprint +issue was present; Discussion mutation is unavailable in the connected +GitHub tools and no gh CLI is installed, so coordination is recorded locally. +The overlap check covers all 8,722 main note records plus bounded live PR and +newest-handoff searches; it is not a global novelty certificate. Ledger entries +for PR6212/6215 remain partially reviewed: source retention is not theorem +acceptance. Final freshness and publication handoff are recorded in TASK.json. + +## Open next questions + +1. Which remaining arities admit three queries with other direction patterns? + This restriction cannot settle them. Begin with one unclaimed arity and + solve its four coefficient equations, then build the chronological repair. + A finite failed search would not prove a four-query lower bound. +2. Does a real backend make the r=33 repair cheaper than eager restoration? + Bind every query/shear tariff to a concrete caller and test the complete + inequality in PROOF.md, including preparation, routing, precision, storage + and all recursive children. Those missing prices block supplier expansion. + +## Credit and license + +Prepared for **@CubeJerry with substantial OpenAI Codex assistance** in algebra, +proof, both implementations, self-review, verification and packaging. Apache-2.0. +Nick Petalas (#6200), apoursh (#6212/#6215), and AAAmirinu (#6246) retain the +specific contributions above. Sricharan Vagvala/theon199 (#1532), Adam Gall +(#1205) and Hanson Sun (#1246) retain the quadratic/linear deferral lineage. +All predecessor source notices are preserved. No human review, Lean/kernel +proof, hosted scientific CI, full selected replay or complete multiplication +theorem is claimed. diff --git a/research/cubic-equal-step-classification/RESULT.json b/research/cubic-equal-step-classification/RESULT.json new file mode 100644 index 0000000000..91360d8dcd --- /dev/null +++ b/research/cubic-equal-step-classification/RESULT.json @@ -0,0 +1,297 @@ +{ + "arity_domain": [ + 3, + 1024 + ], + "centered_equal_step_scope_control": "r50: slopes -35,0,35 accepted; zero must be at an end in the theorem", + "classification_sha256": "59a24b83f38e6c52c55345f0df51269de94e675cd2bc5347f2ba6ee18248dd33", + "dirty_numeric_cases": 189, + "dirty_numeric_events_including_inverses": 56916, + "eligible_arity_and_twice_spacing": [ + [ + 3, + 2 + ], + [ + 4, + 4 + ], + [ + 5, + 4 + ], + [ + 8, + 8 + ], + [ + 9, + 8 + ], + [ + 16, + 16 + ], + [ + 17, + 16 + ], + [ + 32, + 32 + ], + [ + 33, + 32 + ], + [ + 64, + 64 + ], + [ + 65, + 64 + ], + [ + 128, + 128 + ], + [ + 129, + 128 + ], + [ + 256, + 256 + ], + [ + 257, + 256 + ], + [ + 512, + 512 + ], + [ + 513, + 512 + ], + [ + 1024, + 1024 + ] + ], + "large_new_branch_fixtures": [ + { + "r": "3", + "s": 1, + "weights_w0_w1_w2": [ + "-2", + "1", + "1" + ] + }, + { + "r": "5", + "s": 2, + "weights_w0_w1_w2": [ + "-15/4", + "5/2", + "5/4" + ] + }, + { + "r": "9", + "s": 3, + "weights_w0_w1_w2": [ + "-57/8", + "21/4", + "15/8" + ] + }, + { + "r": "17", + "s": 4, + "weights_w0_w1_w2": [ + "-221/16", + "85/8", + "51/16" + ] + }, + { + "r": "33", + "s": 5, + "weights_w0_w1_w2": [ + "-869/32", + "341/16", + "187/32" + ] + }, + { + "r": "129", + "s": 7, + "weights_w0_w1_w2": [ + "-13717/128", + "5461/64", + "2795/128" + ] + }, + { + "r": "2049", + "s": 11, + "weights_w0_w1_w2": [ + "-3496277/2048", + "1398101/1024", + "700075/2048" + ] + }, + { + "r": "131073", + "s": 17, + "weights_w0_w1_w2": [ + "-14316623189/131072", + "5726623061/65536", + "2863377067/131072" + ] + }, + { + "r": "2147483649", + "s": 31, + "weights_w0_w1_w2": [ + "-3843071683096565077/2147483648", + "1537228672809129301/1073741824", + "768614337478306475/2147483648" + ] + }, + { + "r": "18446744073709551617", + "s": 64, + "weights_w0_w1_w2": [ + "-283568639100782052895368878229994952021/18446744073709551616", + "113427455640312821154458202477256070485/9223372036854775808", + "56713727820156410586452473275482811051/18446744073709551616" + ] + }, + { + "r": "340282366920938463463374607431768211457", + "s": 128, + "weights_w0_w1_w2": [ + "-96493407697763496186309154173906589877895128404827605931279673976976825472341/340282366920938463463374607431768211456", + "38597363079105398474523661669562635951089994888546854679819194669304376546645/170141183460469231731687303715884105728", + "19298681539552699237261830834781317975715138627733896571641284638368072379051/340282366920938463463374607431768211456" + ] + } + ], + "literal_symbolic_events": 8540, + "literal_symbolic_programs": [ + [ + 3, + 2 + ], + [ + 4, + 4 + ], + [ + 5, + 4 + ], + [ + 8, + 8 + ], + [ + 9, + 8 + ], + [ + 16, + 16 + ], + [ + 17, + 16 + ], + [ + 32, + 32 + ], + [ + 33, + 32 + ], + [ + 64, + 64 + ], + [ + 65, + 64 + ], + [ + 128, + 128 + ], + [ + 129, + 128 + ], + [ + 256, + 256 + ], + [ + 257, + 256 + ] + ], + "negative_controls": [ + "r2_outside_classification", + "boolean_arity", + "zero_spacing", + "r33_wrong_branch_has_odd_denominator", + "r14_equal_step_does_not_imply_general_floor", + "wrong_spacing_even_with_fitted_lower_moments", + "changed_weight", + "omitted_initial_shear", + "query_before_initial_shear", + "omitted_final_query", + "fused_or_missing_original_child", + "wrong_return_shear", + "output_feedback_outside_alphabet", + "duplicate_receipt_key" + ], + "polynomial_identities": 12, + "r33": { + "defect_A2B_AB2_B3": [ + "1584", + "34320", + "278784" + ], + "original_children_retained": 33, + "repair_event_prices": { + "cube:-187/32": 1, + "cube:-341/16": 1, + "cube:869/32": 1, + "shear:-1": 1, + "shear:-16": 2 + }, + "weights_w0_w1_w2": [ + "-869/32", + "341/16", + "187/32" + ] + }, + "rational_decompositions": 2044, + "scope": "Written all-r equal-step theorem with exact finite corroboration; no new kappa.", + "spacing_scan": { + "arity": [ + 3, + 40 + ], + "cases": 10944, + "d": "k/8; -32<=k<=256; k!=0" + }, + "status": "PASS_CUBIC_EQUAL_STEP_CLASSIFICATION", + "unequal_step_positive_scope_control": "PR6212 r14: three integer queries accepted" +} diff --git a/research/cubic-equal-step-classification/SOURCES.json b/research/cubic-equal-step-classification/SOURCES.json new file mode 100644 index 0000000000..64d53f46a5 --- /dev/null +++ b/research/cubic-equal-step-classification/SOURCES.json @@ -0,0 +1,44 @@ +{ + "schema_version": 1, + "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "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/cubic-pure-b-boundary/PROOF.md", + "usage": "input", + "git_blob": "9907a6925fadc43b18357af198cb7a816cb5be9f", + "sha256": "f97362ac07cd0ff1fff0d7bb74e5497996eb21f12282825731e779cbed5e0792" + }, + { + "path": "research/dyadic-cubic-repair/PROOF.md", + "usage": "input", + "git_blob": "a1c41a9afc83302f8b664bb45467821b9c088f0f", + "sha256": "1296f12278e198b6a22d8d88355cd58c1ee4fc2ab0e6941721614bb06cb1e7d5" + } + ], + "retained_predecessor": { + "pr": 6246, + "head": "3d21b913efac1e3731bee7f0f4f4a8a84fecec37", + "source_path": "research/cubic-pow2-repair/PROOF.md", + "source_url": "https://github.com/CrocSwap/integer-mult-bounds/blob/3d21b913efac1e3731bee7f0f4f4a8a84fecec37/research/cubic-pow2-repair/PROOF.md", + "local_path": "sources/pr6246-PROOF.md", + "git_blob": "eb613b0b3c723838caa46c9cebeb71c64b1fcf04", + "sha256": "55e59351c466bf30717c57f2d1c65748d7aa985d5fe900853a09474577889793", + "usage": "Retained unchanged proof for scientific credit and scope comparison; no executable code imported. Original head is not asserted as a publication ancestor." + }, + "predecessor_heads": { + "6212": "9c159482e0495b6a97e17e629debe66a0ceb9466", + "6215": "0013c2b40c522ccd19670a8fbd4b1531f13fed2b" + } +} diff --git a/research/cubic-equal-step-classification/TASK.json b/research/cubic-equal-step-classification/TASK.json new file mode 100644 index 0000000000..de4e9144f6 --- /dev/null +++ b/research/cubic-equal-step-classification/TASK.json @@ -0,0 +1,178 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 8, + "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "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": "Classify three dyadic weighted cubic queries whose entry-source directions are 0,d,2d (entry-A at an end), allowing nonmonic forms and general dyadic source frames; attain and chronologically restore the r=2^s+1 branch.", + "scope_change_reason": "Follow the concrete open dyadic cubic-reader handoff of PR6212/6215/6246, narrowing the broader joint-query-controller supplier card to coefficient feasibility and chronological restoration in one exact scalar interface. No complete supplier or favorable physical invoice is claimed.", + "bottleneck_link": "Scoped recursive-interface side result: identifies when repeated eager source restoration can be replaced by a fixed exact repair and excludes other arities only for the specified direction pattern. A favorable physical caller bill remains unknown.", + "budget_minutes": 120, + "stop_rule": "Stop after the exact direction-pattern classification, chronological construction, bounded controls and publication; no wider search or supplier admission.", + "outcome": "completed", + "evidence": "PROOF.md, exact receipts RESULT.json and CROSSCHECK.json, registered replay VERIFY.json, and executed checks in VALIDATION.md.", + "author": "@CubeJerry", + "ai_assistance": "Substantial OpenAI Codex assistance in algebra, proof, two separately implemented checkers, self-review, tests and packaging. No human or proof-kernel acceptance is claimed.", + "open_questions": [ + { + "question": "Which remaining arities admit three dyadic queries outside directions 0,d,2d?", + "why_it_matters": "This theorem excludes only one direction pattern; r14 and centered r50 already escape it.", + "first_step": "Choose an unclaimed arity excluded by the existing three-query families, write the full four coefficient equations for a different pattern, then construct its source-restoring schedule.", + "blocked_by": "No general three-versus-four classification; finite search failure would not prove impossibility." + }, + { + "question": "Does an actual complete backend make the r33 repair cheaper than 33 eager inverse shears?", + "why_it_matters": "Three additional weighted cube queries may cost more than the removed restoration work.", + "first_step": "Bind Q and L to one real caller and evaluate the complete inequality in PROOF.md, including preparation, routing, precision, storage and every recursive child.", + "blocked_by": "No pinned physical backend or favorable full cost recurrence is supplied; supplier expansion stops here." + } + ], + "track_number": 54, + "seed": "747c391a6a8f8e701e7d96c3ad256ecc", + "claim": { + "kind": "CLAIM", + "created_at": "2026-10-30T08:55:59.868065+00:00", + "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "predecessors": { + "6212": "9c159482e0495b6a97e17e629debe66a0ceb9466", + "6215": "0013c2b40c522ccd19670a8fbd4b1531f13fed2b", + "6246": "3d21b913efac1e3731bee7f0f4f4a8a84fecec37" + }, + "expected_finish_utc": "2026-10-30T10:40:00Z", + "method": "Exact coefficient elimination and odd-prime denominator obstruction; literal symbolic dirty-state execution; use seed to select first discriminating exponent s=5 (r=33) over the other new residue s=7.", + "deliverable": "One scoped proof, standalone exact verifier, meaningful controls, complete symbolic event invoice and provenance.", + "posting": "Local claim: no sprint issue exists and the connected GitHub tools expose no Discussion mutations; gh is unavailable." + }, + "time_budget_minutes": 120, + "selection": { + "candidates": [ + "Equal-step dyadic cubic repair classification and r=2^s+1 attainment", + "Minimum source movement for the existing power-of-two repair", + "Sharing one correction across two consecutive cubic batches" + ], + "decision": "First candidate has an explicit open handoff and an exact small test. Second may be a trivial slope-visit count; third lacks a specified physical consumer.", + "seed_use": "int(seed,16) modulo 2 selects exponent class 5 mod 6 before 1 mod 6." + }, + "experiment": { + "domain": "Every integer r>=3, dyadic d!=0, nonzero dyadic weights, exactly the monic forms A,A+dB,A+2dB; arbitrary incoming Y,A,B and source-only shears.", + "stop_rule": "Stop at this classified family and bounded corroboration. No general all-arity three-query census or backend search.", + "optimistic_budget": "Retain r original cube queries and r forward shears. Charge all appended weighted queries and source shears separately; compare their sum plus setup with r eager inverse shears. No price inequality is assumed." + }, + "refinement": "The proof normalizes arbitrary nonmonic dyadic forms on the same directions, strengthening the lower-bound scope without changing the initial direction family. A discovered centered r50 control forced explicit entry-A-at-an-end wording; the classified domain remains 0,d,2d.", + "overlap": { + "initial_local": { + "head": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "records": 8722, + "complete_head_inventory": true, + "remote_cache": "unavailable" + }, + "live_coverage": "GitHub plugin: newest 70 open PR results; all-state cubic-repair and focused cubic/equal and cubic/33 searches; web: active Discussion board and newest visible #1166 handoffs. No exhaustive remote claim coverage.", + "nearest": [ + { + "pr": 6212, + "relation": "Known dyadic lower bound, original open three-query question and r3 identity; no 0,d,2d classification." + }, + { + "pr": 6215, + "relation": "Requires a pure-original-B cube. Our three forms all involve A; r33 and r129 are outside that required-read family." + }, + { + "pr": 6246, + "relation": "Entire r=2^s branch already covered and fully credited. New branch uses r=2^s+1, with one additional initial shear; classification adds the exact odd-prime exclusion for the named directions." + } + ], + "ledger": "PR6212 and PR6215 are partially reviewed; archival merge is not scientific acceptance.", + "novelty_limit": "Bounded overlap evidence is not a global novelty certificate." + }, + "checkpoints": [ + { + "utc": "2026-10-30T08:49:17Z", + "canonical_main": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "method": "Canonical Git fetch and independent GitHub API main-ref lookup; local cloned main is identical.", + "priority_revision": 8, + "selected_pr": 6030, + "selected_record_sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa", + "decision": "Continue concrete cubic handoff, preserve all source pins." + }, + { + "utc": "2026-10-30T09:31:25.894185+00:00", + "canonical_main": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "method": "Successful canonical git fetch --no-tags origin main; independent GitHub main-ref lookup agrees.", + "priority_revision": 8, + "selected_pr": 6030, + "guidance_change": "none: canonical commit identical", + "source_head_change": "none: PR6212, PR6215 and PR6246 exact heads rechecked via GitHub API", + "overlap_refresh": "All-state cubic/repair search (15 returned matches), newest 10 open PRs (latest 6248), prior full 8722-record local notes and visible #1166 handoffs. No overlapping zero-endpoint classification found within this bounded coverage.", + "decision": "Finish the same scoped result and publish; preserve frozen inputs." + } + ], + "completion_handoff": { + "kind": "DONE", + "result": "Exact dyadic classification for entry-source directions 0,d,2d; new r=2^s+1 three-query chronological repair. No new kappa.", + "branch_url": "https://github.com/CubeJerry/integer-mult-bounds/tree/research/cubic-equal-step-20261030-54-747c", + "reproduce": "python3.12 -B scripts/research_package.py --package research/cubic-equal-step-classification", + "expected": "PASS_REGISTERED_RESEARCH_PACKAGE", + "scope_released": true, + "coordination": "Local claim updated once with the result and prepared branch link; no Discussion mutation tool or gh CLI is available. Exact publication commit/tree verification belongs to the prefilled PR description, produced after this package commit." + } +} diff --git a/research/cubic-equal-step-classification/VALIDATION.md b/research/cubic-equal-step-classification/VALIDATION.md new file mode 100644 index 0000000000..96137a7610 --- /dev/null +++ b/research/cubic-equal-step-classification/VALIDATION.md @@ -0,0 +1,120 @@ +# Executed validation and coverage + +Prepared for @CubeJerry with substantial OpenAI Codex assistance. Apache-2.0. + +## Mathematical evidence + +The result is a written scoped proof, corroborated by exact standard-library +arithmetic. It is not a claim that finitely many runs prove an infinite theorem. +Both implementations were written in this contribution by the same AI-assisted +contributor; separate algorithms do not constitute independent human review. + +Environment: Linux x86_64, CPython 3.12.14, no third-party dependencies. +Source base: `2485805a6d47f36ea83ddde6327d453ac82d44dc`. Exact source pins and +the unchanged retained PR6246 proof are in SOURCES.json. + +Executed successfully: + +```sh +python3.12 -B scripts/research_package.py --package research/cubic-equal-step-classification +``` + +All four registered commands use isolated Python, warnings as errors and no +bytecode writes. `verify.py` and `crosscheck.py` each passed in normal and +optimized (`-O`) mode, checking their complete committed JSON receipts. +The wrapper returned `PASS_REGISTERED_RESEARCH_PACKAGE`. There are no +assert-based validation guards in either checker. + +| Coverage | Exact completed domain | +|---|---| +| Polynomial algebra | Three power-sum recurrences and their zero bases; one spacing factorization; eight cleared-denominator coefficient identities | +| Dyadic classification | Both rational branches for every r=3..1024, 2,044 decompositions | +| Spacing corroboration | Every d=k/8, -32<=k<=256, k!=0, for r=3..40: 10,944 cases | +| Literal symbolic programs | All fifteen eligible r<=257, every retained child, repair, inverse repair and full inverse; 8,540 family events | +| Literal dirty values | All 27 triples from {-3/2,0,5/4} at r=3,4,16,33,65,129,257: 189 cases, 56,916 events including inverses | +| Large new-branch cases | s=1,2,3,4,5,7,11,17,31,64,128; exact coefficients and repair/inverse from the symbolic deferred boundary; original exponential-length prefixes are not executed | +| Separate coefficient path | 510 exact systems for both branches at r=3..257; 1,020 nonmonic rescalings; literal power sums checked against binary-block concatenation | +| Separate large cases | s=1,2,5,7,11,17,31,64,128, defect derived by binary-block concatenation and weights by generic Gaussian elimination | +| Positive scope controls | PR6212's unequal-direction r14 repair and centered directions -35,0,35 at r50; both outside the classified direction family | + +The primary's fourteen pinned-reason controls reject domain/zero-spacing +errors, odd denominators, incorrect fitted spacing, a changed weight, +missing or mistimed restoration, an omitted final query, a missing original +child, forbidden output feedback and duplicate JSON keys. In particular, +moving the first query before its initial shear preserves the final source +but fails the output: endpoint source restoration alone is insufficient. + +The separate implementation checks four incorrect spacings against the actual +fourth coefficient, rejects singular zero spacing, and detects the non-dyadic +91/11 coefficient in the credited r14 rational two-query repair. Its nonmonic +tests use both dyadic units and odd nonunits: a nonunit rescaling cannot rescue +an excluded normalized coefficient. These algebraic form tests do not claim +that every nonprimitive row is a physically admissible source frame. + +## Proof review and scope + +Self-review checked the normalization step, division only by nonzero S1 and d, +the p=3 denominator case, modulo-three sufficiency, chronological query locations, +literal inverses, source-shear visit counts and complete symbolic price list. +The centered r50 example prompted explicit wording that zero must be at an end +of the progression. It is retained as a scope-positive control. The new r33 +and r129 count cases are compared against all three pinned predecessors. + +The initial metadata check rejected a list-valued `TASK.evidence`, then rejected +a non-enumerated `outcome`; both fields were corrected to the documented schema. +These were packaging failures, not mathematical counterexamples. No failed +scientific case was removed to obtain a pass. + +## Source history and transport + +The committed-byte preflight passed for all eleven package files and both +declared input files, including owner-execute modes and base-source ancestry: + +```sh +python3.12 -B scripts/check_research_commit.py --package research/cubic-equal-step-classification --check-source-history --check-modes +``` + +The official exporter and its `check --check-inputs` mode passed. The exported +tree contains no Git repository. Both direct checkers passed in normal and +optimized Python using the absolute interpreter path with an empty PATH, +isolated imports and warnings as errors. The fourteen exported files, +including the export manifest, were marked read-only. Every file's bytes and +mode remained unchanged. Normal and optimized stdout matched byte for byte +for each implementation. + +Eighteen actual corrupted-export executions rejected with the specified +diagnostic. Each test used a fresh copy; no committed input was edited: + +| Mutation | Executions | Required diagnostic | +|---|---:|---| +| Append one newline to each PR6212 and PR6215 proof | 2 inputs × 2 scripts × 2 modes = 8 | Primary `SOURCE_BYTES`, cross-check `INPUT_BYTES` | +| Append one newline to the retained PR6246 proof | 2 scripts × 2 modes = 4 | Primary `PREDECESSOR_BYTES`, cross-check `RETAINED_PROOF_BYTES` | +| Replace the retained PR6246 head in SOURCES.json | Primary in 2 modes | `PREDECESSOR_DECLARATION` | +| Replace a RESULT.json integer-one event count with boolean true | Primary in 2 modes | `RECEIPT_MISMATCH` | +| Replace CROSSCHECK.json's first exponent 1 with boolean true | Cross-check in 2 modes | `CROSSCHECK_RECEIPT_MISMATCH` | + +The boolean mutations verify type-sensitive canonical JSON comparison rather +than Python's `True == 1` equality. The initial external export-test harness +failed while cleaning a copied read-only root after the first source mutation; +restoring that temporary root's write permission fixed cleanup. The full +unchanged test set was then rerun and all eighteen rejections completed. No +success receipt from the failed harness attempt is relied on. + +These transport checks authenticate the tested package and explicit inputs; +they do not establish the mathematics or cover undeclared dependencies. +Only base provenance is covered by the source-history check. PR6246's pending +original history is not asserted as an ancestor: its exact proof bytes and +original Git blob are retained and authenticated separately. + +Only this package is added to the canonical base. Publication verification +compares the complete remote Git tree with the tested local tree; the exact +published commit and the fresh verification result are in the PR description. + +## Not executed or not claimed + +No selected-supplier cold replay, native/physical caller replay, rounded program, +full multiplier, external solver, wider arity search, Lean/Docker run or hosted +scientific CI was run. No independent human or proof-kernel acceptance is claimed. +There is no physical cost inequality, supplier admission or new kappa. +The five inherited selected assumptions remain unchanged. Exact events are +priced symbolically; unknown backend costs are not treated as zero. diff --git a/research/cubic-equal-step-classification/VERIFY.json b/research/cubic-equal-step-classification/VERIFY.json new file mode 100644 index 0000000000..45c1e51837 --- /dev/null +++ b/research/cubic-equal-step-classification/VERIFY.json @@ -0,0 +1,62 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/cubic-pure-b-boundary/PROOF.md", + "research/dyadic-cubic-repair/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Universal coefficient identities, finite dyadic classification, literal dirty restoration, two scope-positive examples and 14 rejecting controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Universal coefficient identities, finite dyadic classification, literal dirty restoration, two scope-positive examples and 14 rejecting controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/crosscheck.py" + ], + "timeout_seconds": 60, + "checks": "Independent block-concatenation defect and generic exact elimination, nonmonic normalization, centered scope control and six rejection cases." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/crosscheck.py" + ], + "timeout_seconds": 60, + "checks": "Independent block-concatenation defect and generic exact elimination, nonmonic normalization, centered scope control and six rejection cases." + } + ] +} diff --git a/research/cubic-equal-step-classification/crosscheck.py b/research/cubic-equal-step-classification/crosscheck.py new file mode 100644 index 0000000000..97073e6235 --- /dev/null +++ b/research/cubic-equal-step-classification/crosscheck.py @@ -0,0 +1,215 @@ +#!/usr/bin/env python3 +"""Separate exact coefficient-elimination path; stdlib only, no primary imports. + +By @CubeJerry with substantial OpenAI Codex assistance; Apache-2.0. +This is another implementation by the same AI-assisted contributor, not a +claim of independent human review or a formal proof kernel. +""" +from fractions import Fraction +from hashlib import sha1, sha256 +from math import comb +from pathlib import Path +import argparse +import json + +F = Fraction +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def encode(obj): + return json.dumps(obj, sort_keys=True, separators=(',', ':')) + + +def authenticate(): + for relative, expected in [ + ('research/dyadic-cubic-repair/PROOF.md', + '1296f12278e198b6a22d8d88355cd58c1ee4fc2ab0e6941721614bb06cb1e7d5'), + ('research/cubic-pure-b-boundary/PROOF.md', + 'f97362ac07cd0ff1fff0d7bb74e5497996eb21f12282825731e779cbed5e0792'), + ]: + require(sha256((ROOT/relative).read_bytes()).hexdigest() == expected, + 'INPUT_BYTES:'+relative) + data = (HERE/'sources/pr6246-PROOF.md').read_bytes() + require(sha1(b'blob '+str(len(data)).encode()+b'\0'+data).hexdigest() + == 'eb613b0b3c723838caa46c9cebeb71c64b1fcf04', 'RETAINED_PROOF_BYTES') + + +def append_block(left, right): + """Concatenate [0,n) with n+[0,m); zeroth moment is its length.""" + n = left[0] + return tuple(left[k]+sum(comb(k, j)*n**(k-j)*right[j] + for j in range(k+1)) for k in range(4)) + + +def block_moments(n): + total, block = (0, 0, 0, 0), (1, 0, 0, 0) + while n: + if n % 2: + total = append_block(total, block) + block = append_block(block, block) + n //= 2 + return total + + +def cube_column(alpha, beta): + return tuple(F(comb(3, k))*alpha**(3-k)*beta**k for k in range(4)) + + +def eliminate(columns, target): + """Fit A^3,A^2B,AB^2 by generic exact row reduction, then test B^3.""" + rows = [[F(columns[j][i]) for j in range(3)]+[F(target[i])] for i in range(3)] + for pivot in range(3): + source = next((i for i in range(pivot, 3) if rows[i][pivot]), None) + require(source is not None, 'SINGULAR_DIRECTIONS') + rows[pivot], rows[source] = rows[source], rows[pivot] + divisor = rows[pivot][pivot] + rows[pivot] = [x/divisor for x in rows[pivot]] + for i in range(3): + if i != pivot: + factor = rows[i][pivot] + rows[i] = [x-factor*y for x, y in zip(rows[i], rows[pivot])] + ws = tuple(rows[i][-1] for i in range(3)) + residual = tuple(sum(ws[j]*columns[j][i] for j in range(3))-target[i] + for i in range(4)) + return ws, residual + + +def ring_member(q): + denominator = q.denominator + while denominator % 2 == 0: + denominator //= 2 + return denominator == 1 + + +def is_power_two(n): + if n <= 0: + return False + while n % 2 == 0: + n //= 2 + return n == 1 + + +def target(r): + _, m1, m2, m3 = block_moments(r) + return (F(0), F(3*m1), F(3*m2), F(m3)) + + +def fit(r, d, scales=(F(1), F(1), F(1))): + columns = [cube_column(alpha, alpha*i*d) for i, alpha in enumerate(scales)] + return eliminate(columns, target(r)) + + +def integrate_tail(r, directions, ws): + """Construct and execute a descending source walk from the actual endpoint. + + This derives shears from successive directions, without the primary's + prewritten six-event recipe. Output starts at the uncorrected defect. + """ + slope = F(r) + residual = list(target(r)) + events = [] + for direction, weight in sorted(zip(directions, ws), reverse=True): + if direction != slope: + events.append(('L', direction-slope)) + slope = direction + events.append(('Q', -weight)) + residual = [x-weight*y for x, y in zip(residual, cube_column(F(1), slope))] + require(slope == 0, 'TAIL_SOURCE') + require(residual == [0, 0, 0, 0], 'TAIL_OUTPUT') + return events + + +def run(): + authenticate() + records, eligible, scaled_tests = [], [], 0 + for r in range(3, 258): + sums = block_moments(r) + literal = tuple(sum(j**k for j in range(r)) for k in range(4)) + require(sums == literal, 'BLOCK_VS_LITERAL_READERS') + for u in (r, r-1): + d = F(u, 2) + ws, residual = fit(r, d) + require(residual == (0, 0, 0, 0), 'SOLVED_CUBIC') + valid = all(ring_member(w) for w in ws) + require(valid == is_power_two(u), 'EXACT_CLASSIFICATION') + records.append([r, u, list(map(str, ws)), valid]) + if valid: + eligible.append([r, u]) + events = integrate_tail(r, [F(0), d, 2*d], ws) + require(sum(kind == 'Q' for kind, _ in events) == 3, 'QUERY_COUNT') + require(sum(kind == 'L' for kind, _ in events) == (2 if u == r else 3), + 'SHEAR_COUNT') + # Unit rescalings preserve feasibility; odd nonunit rescalings + # cannot turn any excluded normalized weight into a dyadic one. + for scales in [(F(1, 2), F(-2), F(4)), (F(3), F(-5, 2), F(7, 4))]: + gammas, res = fit(r, d, scales) + require(res == (0, 0, 0, 0), 'NONMONIC_IDENTITY') + require(tuple(g*a**3 for g, a in zip(gammas, scales)) == ws, + 'NORMALIZATION') + actual = all(ring_member(g) for g in gammas) + require(not actual or valid, 'NONMONIC_FALSE_ESCAPE') + if scales[0] == F(1, 2): + require(actual == valid, 'UNIT_RESCALE') + scaled_tests += 1 + large = [] + for s in [1, 2, 5, 7, 11, 17, 31, 64, 128]: + r, d = 2**s+1, F(2**s, 2) + ws, residual = fit(r, d) + require(residual == (0, 0, 0, 0) and all(ring_member(w) for w in ws), + 'LARGE_BINARY_BLOCK') + integrate_tail(r, [F(0), d, 2*d], ws) + large.append([s, str(r), list(map(str, ws))]) + ws33, residual = fit(33, F(16)) + require(ws33 == (F(-869, 32), F(341, 16), F(187, 32)) and not any(residual), + 'R33_FIXED_FIXTURE') + centered_columns = [cube_column(F(1), F(t)) for t in (-35, 0, 35)] + centered_ws, centered_residual = eliminate(centered_columns, target(50)) + require(centered_ws == (-1, -33, 34) and not any(centered_residual), + 'CENTERED_POSITIVE_SCOPE_CONTROL') + # Distinct failure cases, checked against the actual fourth coefficient. + controls = [] + for r, d in [(33, F(15)), (33, F(-16)), (33, F(1, 3)), (129, F(65))]: + _, residual = fit(r, d) + require(residual[:3] == (0, 0, 0) and residual[3] != 0, + 'WRONG_SPACING_CONTROL') + controls.append(f'wrong_spacing:r={r}:d={d}') + try: + fit(33, F(0)) + except ValueError as exc: + require(str(exc) == 'SINGULAR_DIRECTIONS', 'SINGULAR_REASON') + controls.append('zero_spacing_singular') + else: + raise ValueError('ZERO_SPACING_ACCEPTED') + # The r14 Pell repair is rational with coefficient 91/11; it cannot be + # smuggled into R by multiplying its forms by nonzero dyadic scalars. + require(not ring_member(F(91, 11)), 'PELL_DENOMINATOR_CONTROL') + controls.append('r14_rational_two_query_weight_not_dyadic') + return {'status': 'PASS_CUBIC_EQUAL_STEP_CROSSCHECK', + 'method': 'binary block concatenation; generic rational elimination; normalized nonmonic forms', + 'arity_domain': [3, 257], 'eliminated_systems': len(records), + 'systems_sha256': sha256(encode(records).encode()).hexdigest(), + 'eligible_arity_and_twice_spacing': eligible, + 'nonmonic_systems': scaled_tests, 'large_new_branch_fixtures': large, + 'centered_scope_control': 'r50 weights -1,-33,34 on slopes -35,0,35', + 'negative_controls': controls} + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('--emit', action='store_true') + args = parser.parse_args() + result = run() + if not args.emit: + expected = json.loads((HERE/'CROSSCHECK.json').read_text(encoding='utf-8')) + require(encode(result) == encode(expected), 'CROSSCHECK_RECEIPT_MISMATCH') + print(json.dumps(result, sort_keys=True, indent=2)) + + +if __name__ == '__main__': + main() diff --git a/research/cubic-equal-step-classification/sources/pr6246-PROOF.md b/research/cubic-equal-step-classification/sources/pr6246-PROOF.md new file mode 100644 index 0000000000..eb613b0b3c --- /dev/null +++ b/research/cubic-equal-step-classification/sources/pr6246-PROOF.md @@ -0,0 +1,290 @@ +# Three dyadic cubic queries for every power-of-two arity + +Let R=Z[1/2] and r=2^s with integer s>=2. In the fixed cubic-reader +interface of Nick Petalas's PR6200, exactly three appended dyadic cube +queries suffice to repair the retained deferred children. The attaining +schedule uses two integer source shears, restores both arbitrary dirty +sources and gives exactly the eager output. Its query count is minimal by +apoursh's existing PR6212 lower bound, restated below with credit. + +This proof adds a uniform attainment formula, not a new lower bound or a +runtime gain. The source inputs are the unchanged proofs at +[PR6212 head9c159482](https://github.com/CrocSwap/integer-mult-bounds/blob/9c159482e0495b6a97e17e629debe66a0ceb9466/research/dyadic-cubic-repair/PROOF.md) +and +[PR6215 head0013c2b4](https://github.com/CrocSwap/integer-mult-bounds/blob/0013c2b40c522ccd19670a8fbd4b1531f13fed2b/research/cubic-pure-b-boundary/PROOF.md), +with complete byte pins in `SOURCES.json`. + +## Contract and the chronological defect + +The distinct streams y,a,b enter with arbitrary values Y,A,B. Retain +exactly r original children, each with its original order and interior: + +```text +y += a^3 +a += b. +``` + +The eager comparator appends `a -= b` after each such child, so it ends +at (Y+r*A^3,A,B). Deferring those restoring shears retains the original +children and ends at + +```text +(Y + sum_(i=0)^(r-1) (A+iB)^3, A+rB, B). +``` + +There is no observation between children, output feedback into sources, +nonlinear source change, output recoding, or child fusion. Coefficients +are fixed by r independently of the data. Source changes are invertible +R-linear maps; a signed weighted cube accumulation is one query. +Source transformations and coefficient work are paid separately. Exact +arithmetic in this interface is a premise, not a rounded or native backend. + +Using the sums of first, second and third integer powers, the output +excess over the eager comparator is the credited PR6200 defect + +```text +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. +``` + +A restoring repair must subtract this polynomial from y and return the +actual sources (A+rB,B) to (A,B). A formal cube identity alone would not +establish that chronological source restoration. + +## Uniform coefficient identity + +Define + +```text +c1 = (r-1)(r-2)/(6r), +c2 = 2(r^2-1)/(3r), +c0 = -(r-1)(5r+2)/(6r). +``` + +Then the polynomial identity is + +```text +f_r(A,B) = c1*(A+rB)^3 + c2*(A+(r/2)B)^3 + c0*A^3. (1) +``` + +For an independent coefficient derivation, the four relevant combinations +of weights are + +```text +c1+c2+c0 = 0, +c1+c2/2 = (r-1)/2, +c1+c2/4 = (r-1)(2r-1)/(6r), +c1+c2/8 = (r-1)^2/(4r). +``` + +For example, the first equality has numerator +(r-1)(r-2)+4(r^2-1)-(r-1)(5r+2)=0 over denominator6r. +The other three follow by collecting over denominators6r,6r,12r. +Expanding the right side of (1) therefore gives, in the order +A^3,A^2B,AB^2,B^3, + +```text +0, +3r(r-1)/2, +r(r-1)(2r-1)/2, +r^2(r-1)^2/4, +``` + +which are exactly the coefficients of f_r. This is a polynomial identity +over Q for every nonzero r. The power-of-two restriction below establishes +the required coefficient ring and integer shears, not the formal expansion. + +For r=2^s, r is congruent to1 or2 modulo3. Thus3 divides each of + +```text +(r-1)(r-2), r^2-1, (r-1)(5r+2). +``` + +For the last expression, if r=1 mod3 use r-1; if r=2 mod3 use +5r+2=0 mod3. Cancellation removes the only odd prime in the displayed +denominators: after cancelling3, c1 and c0 have denominator dividing2r, +and c2 has denominator dividing r. These are powers of two, so all three +weights belong to R. Also r/2 is an integer. For r>=4, c1,c2 are positive +and c0 is negative, hence every displayed cube query is nonzero. + +This argument does not assert dyadic admissibility of the same formula +for every other integer r. For example, r=3 gives c1=1/9 in this formula, +even though PR6212 supplies a different dyadic three-query formula at r=3. + +## Actual five-event restoring schedule + +Start from the actual deferred endpoint, with a=A+rB and b=B. Append +exactly these five events: + +```text +1. y -= c1*a^3 +2. a -= (r/2)*b +3. y -= c2*a^3 +4. a -= (r/2)*b +5. y -= c0*a^3. +``` + +The first query reads A+rB without a preliminary shift. After event2, +the source is A+(r/2)B, which event3 reads. Event4 returns it to A, +which event5 reads. Register b stays exactly B throughout. By (1), the +three signed query contributions sum to -f_r; the final state is therefore + +```text +(Y+r*A^3,A,B). +``` + +This holds for every incoming Y,A,B. No clean register, entry snapshot, +discarded dirty value or alteration of an original child is used. +The two shears have matrices [[1,-r/2],[0,1]] and determinant1. +A query is invertible because its source is independent of its target y. +The literal inverse repair, starting at the eager endpoint, is + +```text +y += c0*a^3 +a += (r/2)*b +y += c2*a^3 +a += (r/2)*b +y += c1*a^3. +``` + +It restores the deferred endpoint, not yet the original entry state. +Reversing the retained children after this inverse repair applies, for +each child in reverse order, `a -= b` followed by `y -= a^3`; that restores +(Y,A,B) exactly. No query or original child is fused in either direction. + +The schedule thus attains three appended cube queries and two integer +shears. All three queried forms have entry-A coefficient1. In particular +none is a nonzero multiple of the original entry B. + +## Query optimality from PR6212 + +We reuse the unrestricted dyadic lower bound in apoursh's PR6212; the +following is its credited argument, included to specify the exact scope. +It allows arbitrary nonmonic dyadic forms and arbitrary GL_2(R) source +frames, so it applies to the smaller shear-only construction above. + +Every queried source form has R coefficients in A,B. A single weighted +cube cannot have zero A^3 coefficient and nonzero A^2B coefficient, as +f_r does. In a hypothetical two-cube representation, both A coefficients +and both weights must be nonzero. Normalize the A coefficients over Q. +The zero A^3 coefficient forces opposite normalized weights, so + +```text +f_r = lambda*((A+tB)^3-(A+uB)^3), +lambda*(t-u)=S1, +t+u=S2/S1=(2r-1)/3, +t^2+tu+u^2=S1. +``` + +Reorder the directions so k=t-u>0. These equations imply + +```text +(2r-1)^2-6k^2=3, lambda=S1/k, 4S1=3k^2+1. +``` + +Writing rational k in lowest terms shows its denominator squared divides6, +so k is an integer. Reduction of the Pell equation modulo4 makes k odd. +The last identity gives gcd(S1,k)=1, hence the reduced denominator of +lambda is exactly k. Normalization cannot hide an odd prime denominator: +for an admissible nonmonic term gamma*(alpha*A+beta*B)^3, its normalized +weight gamma*alpha^3 still belongs to R. Thus lambda must be dyadic. +Since its denominator k is both odd and a power of two, k=1. The Pell +equation then gives 2r-1=3 and r=2. + +For r>2, therefore, no zero-, one- or two-query dyadic repair is possible. +Together with the five-event schedule, this proves the exact appended +query minimum is three for every r=2^s>=4. It does not prove the two-shear +count optimal, compare physical tariffs, or introduce a new lower-bound +method. + +## Known cases and the original-B boundary + +At r=4, (1) is literally the predecessor's known identity + +```text +f_4 = (1/4)*(A+4B)^3 + (5/2)*(A+2B)^3 - (11/4)*A^3. +``` + +That is a credited reproduction/control, not a new r=4 result. For odd +s>=3, r=2 mod3, and PR6212 already attains the exact three-query minimum +with an integer formula including an original-B cube. For s divisible by6, +r=1 mod9, and PR6215 also supplies three-query attainment. Relative to +these two pinned proofs, the remaining power-of-two residues addressed by +the uniform formula are s=2 or4 mod6, excluding the already known s=2. +This statement concerns the scope of those sources, not literature priority. + +The first previously uncovered power of two in that comparison is r=16: + +```text +c1=35/16, c2=85/8, c0=-205/16, +f_16 = (35/16)*(A+16B)^3 + (85/8)*(A+8B)^3 - (205/16)*A^3 + = 360*A^2*B + 3720*A*B^2 + 14400*B^3. +``` + +Its chronological repair is query -35/16, shear -8, query -85/8, +shear -8, query +205/16, all queries on current a. Since16=7 mod9, +PR6215 proves a four-query minimum in the restricted family that must +contain a nonzero cube of a nonzero scalar multiple of original B. +Our three queried forms all contain original A, so this schedule is outside +that restricted family. It does not contradict or weaken its four-query +theorem. Calling a current register b would not make a form pure-original-B; +the restriction concerns its expression in the entry coordinates. + +## Complete event bill and remaining obligations + +Use the source's complete-event prices Q_c^a(N) for `y += c*a^3` and +L_c(N) for `a += c*b`. A complete query price includes its coefficient use, +source access, private restoration and return. The eager bill is + +```text +r*Q_1^a(N) + r*L_1(N) + r*L_-1(N). +``` + +The deferred schedule retains r*Q_1^a(N)+r*L_1(N) without cancellation +or child fusion, and adds the exact five-event bill + +```text +Q_-c1^a(N) + L_(-r/2)(N) + Q_-c2^a(N) + + L_(-r/2)(N) + Q_-c0^a(N). +``` + +Thus it replaces r restoring shears by two shears and three additional +queries; different coefficients have different tariff symbols. An event +count comparison alone gives no inequality between the two total costs. +In particular r copies of an original child are not silently replaced by +one weighted query. + +For a variable arity, preparing r and the three coefficients, cancelling +the factor3, and preparing the controller/program are additional work. +Dyadic membership is not a zero-cost coefficient generator. Physical +routing, source access, precision, native query realization, private +cleanup, storage and dispatch must be covered by a genuine complete tariff +or separately charged allowance. No such backend or matched favorable +total bill is supplied here. The proof concerns exact arithmetic and does +not imply rounded execution, a finite-field implementation, supplier +admission, a global multiplication-runtime gain or a selected-frontier +change. + +The unrestricted three-versus-four classification for all other integer +arities remains open beyond the cases already resolved by the sources. +Another independent question is the minimum source-transformation cost +under a specified physical tariff. Neither follows from optimality of the +number of appended cube queries. + +## Attribution + +Nick Petalas's [PR6200](https://github.com/CrocSwap/integer-mult-bounds/pull/6200) +supplies the cubic-reader interface, chronological defect, rational two-cube +criterion and restoring-schedule question. Apoursh's +[PR6212](https://github.com/CrocSwap/integer-mult-bounds/pull/6212) supplies +the dyadic localization obstruction, the all-r>2 three-query lower bound, +and the earlier integer/r=3/r=4 constructions. Apoursh's +[PR6215](https://github.com/CrocSwap/integer-mult-bounds/pull/6215) supplies +the pure-original-B boundary and its additional integer attainments. +Sricharan Vagvala / theon199's PR1532 retains the quadratic fixed-reader +paid-repair interface, and Adam Gall's PR1205 and Hanson Sun's PR1246 retain +the linear deferral lineage. Polynomial coefficient comparison and +binary-form decomposition are classical. No historical-priority, +independent human review or proof-kernel acceptance is claimed. +Prepared with substantial OpenAI Codex assistance. Apache-2.0. diff --git a/research/cubic-equal-step-classification/verify.py b/research/cubic-equal-step-classification/verify.py new file mode 100644 index 0000000000..7910eb0524 --- /dev/null +++ b/research/cubic-equal-step-classification/verify.py @@ -0,0 +1,376 @@ +#!/usr/bin/env python3 +"""Exact corroboration of PROOF.md; @CubeJerry / OpenAI Codex; Apache-2.0. + +No predecessor executable code is imported. All guards survive Python -O. +""" +from __future__ import annotations +import argparse +from collections import Counter +from fractions import Fraction as F +from hashlib import sha1, sha256 +from itertools import product +import json +from math import comb +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent +BASE = '2485805a6d47f36ea83ddde6327d453ac82d44dc' +INPUTS = { + 'research/dyadic-cubic-repair/PROOF.md': + '1296f12278e198b6a22d8d88355cd58c1ee4fc2ab0e6941721614bb06cb1e7d5', + 'research/cubic-pure-b-boundary/PROOF.md': + 'f97362ac07cd0ff1fff0d7bb74e5497996eb21f12282825731e779cbed5e0792', +} +PREDECESSOR_HEAD = '3d21b913efac1e3731bee7f0f4f4a8a84fecec37' +PREDECESSOR_BLOB = 'eb613b0b3c723838caa46c9cebeb71c64b1fcf04' + + +class Rejected(ValueError): + pass + + +def need(ok, reason): + if not ok: + raise Rejected(reason) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(',', ':')) + + +def unique_object(pairs): + out = {} + for key, value in pairs: + need(key not in out, 'DUPLICATE_JSON_KEY') + out[key] = value + return out + + +def read_json(path): + return json.loads(path.read_text(encoding='utf-8'), object_pairs_hook=unique_object) + + +def authenticate(): + manifest = read_json(HERE / 'SOURCES.json') + need(manifest['base_commit'] == BASE, 'SOURCE_BASE') + rows = {row['path']: row for row in manifest['files']} + for path, digest in INPUTS.items(): + need(rows[path]['usage'] == 'input' and rows[path]['sha256'] == digest, + 'SOURCE_DECLARATION') + need(sha256((ROOT / path).read_bytes()).hexdigest() == digest, + 'SOURCE_BYTES:' + path) + row = manifest['retained_predecessor'] + need(row['head'] == PREDECESSOR_HEAD and row['git_blob'] == PREDECESSOR_BLOB + and row['local_path'] == 'sources/pr6246-PROOF.md', 'PREDECESSOR_DECLARATION') + data = (HERE / row['local_path']).read_bytes() + blob = sha1(b'blob ' + str(len(data)).encode() + b'\0' + data).hexdigest() + need(blob == PREDECESSOR_BLOB, 'PREDECESSOR_BYTES') + need(sha256(data).hexdigest() == row['sha256'], 'PREDECESSOR_SHA256') + + +def dyadic(x): + return x.denominator & (x.denominator - 1) == 0 + + +def pow2(n): + return n > 0 and n & (n - 1) == 0 + + +def moments(r): + s1 = F(r*(r-1), 2) + return s1, F(r*(r-1)*(2*r-1), 6), s1*s1 + + +def weights(r, d): + need(type(r) is int and r >= 3, 'ARITY_DOMAIN') + need(d != 0, 'ZERO_SPACING') + s1, s2, _ = moments(r) + w2 = (s2-d*s1)/(2*d*d) + w1 = (2*d*s1-s2)/(d*d) + return -w1-w2, w1, w2 + + +def check_decomposition(r, d, ws, require_ring=True): + need(type(r) is int and r >= 3, 'ARITY_DOMAIN') + need(d != 0, 'ZERO_SPACING') + need(len(ws) == 3 and all(w != 0 for w in ws), 'NONZERO_THREE_QUERIES') + if require_ring: + need(dyadic(d) and all(dyadic(w) for w in ws), 'NON_DYADIC') + got = tuple(sum(w*(i*d)**k for i, w in enumerate(ws)) for k in range(4)) + need(got == (F(0),)+moments(r), 'DEFECT_COEFFICIENTS') + + +# Polynomials in r,d: exact coefficient identities, not evaluation samples. +def add(*ps): + out = {} + for p in ps: + for k, value in p.items(): + out[k] = out.get(k, F(0))+value + return {k: v for k, v in out.items() if v} + + +def mul(a, b): + out = {} + for (i, j), x in a.items(): + for (k, l), y in b.items(): + key = i+k, j+l + out[key] = out.get(key, F(0))+x*y + return {k: v for k, v in out.items() if v} + + +def scale(c, p): + return {k: c*v for k, v in p.items() if c*v} + + +def power(p, n): + out = {(0, 0): F(1)} + for _ in range(n): + out = mul(out, p) + return out + + +def shift_r(p): + out = {} + for (i, j), value in p.items(): + for k in range(i+1): + out = add(out, {(k, j): value*comb(i, k)}) + return out + + +def polynomial_checks(): + one, r, d = {(0, 0): F(1)}, {(1, 0): F(1)}, {(0, 1): F(1)} + rm1 = add(r, scale(-1, one)) + s1 = scale(F(1, 2), mul(r, rm1)) + s2 = scale(F(1, 6), mul(mul(r, rm1), add(scale(2, r), scale(-1, one)))) + ms = [{}, s1, s2, mul(s1, s1)] + count = 0 + for k, p in enumerate(ms[1:], 1): + need(add(shift_r(p), scale(-1, p), scale(-1, power(r, k))) == {}, + 'POWER_SUM_RECURRENCE') + need(p.get((0, 0), 0) == 0, 'POWER_SUM_BASE') + count += 1 + factored = mul(add(scale(2, d), scale(-1, r)), + add(scale(2, d), scale(-1, r), one)) + expanded = add(scale(4, power(d, 2)), + scale(-2, mul(add(scale(2, r), scale(-1, one)), d)), mul(r, rm1)) + need(factored == expanded, 'SPACING_FACTORIZATION') + count += 1 + for branch in (0, 1): + u = r if branch == 0 else rm1 + if branch == 0: + ns = [scale(-1, mul(rm1, add(scale(5, r), scale(2, one)))), + scale(4, add(power(r, 2), scale(-1, one))), + mul(rm1, add(r, scale(-2, one)))] + else: + ns = [scale(-1, mul(r, add(scale(5, r), scale(-7, one)))), + scale(4, mul(r, add(r, scale(-2, one)))), mul(r, add(r, one))] + for k in range(4): + lhs = add(*(mul(n, power(scale(F(i, 2), u), k)) for i, n in enumerate(ns))) + need(lhs == scale(6, mul(u, ms[k])), 'UNIFORM_COEFFICIENT_IDENTITY') + count += 1 + return count + + +def children(r): + return [('cube', F(1)), ('shear', F(1))]*r + + +def repair(r, u): + need(u in (r, r-1), 'SPACING_BRANCH') + d = F(u, 2) + w0, w1, w2 = weights(r, d) + check_decomposition(r, d, (w0, w1, w2)) + out = [] if u == r else [('shear', F(-1))] + return out+[('cube', -w2), ('shear', -d), ('cube', -w1), + ('shear', -d), ('cube', -w0)] + + +def inverse(events): + return [(kind, -value) for kind, value in reversed(events)] + + +def symbolic(events, initial=None): + # y coordinates: Y,A^3,A^2B,AB^2,B^3. a=alpha*A+beta*B; b=B. + alpha, beta, y = initial or (F(1), F(0), (F(1), F(0), F(0), F(0), F(0))) + y = list(y) + for kind, value in events: + need(dyadic(value), 'EVENT_RING') + if kind == 'shear': + beta += value + elif kind == 'cube': + for k in range(4): + y[k+1] += value*comb(3, k)*alpha**(3-k)*beta**k + elif kind == 'cube_b': + y[4] += value + else: + raise Rejected('EVENT_ALPHABET') + return alpha, beta, tuple(y) + + +def check_program(r, events): + need(events[:2*r] == children(r), 'RETAINED_CHILDREN') + alpha, beta, y = symbolic(events) + need((alpha, beta) == (1, 0), 'SOURCES_NOT_RESTORED') + need(y == (1, r, 0, 0, 0), 'WRONG_EAGER_OUTPUT') + need(symbolic(inverse(events), (alpha, beta, y)) + == (1, 0, (1, 0, 0, 0, 0)), 'FULL_INVERSE') + + +def numeric(events, state): + y, a, b = state + for kind, value in events: + if kind == 'shear': + a += value*b + elif kind == 'cube': + y += value*a*a*a + elif kind == 'cube_b': + y += value*b*b*b + else: + raise Rejected('EVENT_ALPHABET') + return y, a, b + + +def controls(): + passed = [] + def rejects(name, reason, call): + try: + call() + except Rejected as exc: + need(str(exc) == reason, 'WRONG_REJECTION:'+name) + else: + raise Rejected('CONTROL_ACCEPTED:'+name) + passed.append(name) + ws = weights(33, F(16)) + prefix, tail = children(33), repair(33, 32) + rejects('r2_outside_classification', 'ARITY_DOMAIN', lambda: weights(2, F(1))) + rejects('boolean_arity', 'ARITY_DOMAIN', lambda: weights(True, F(1))) + rejects('zero_spacing', 'ZERO_SPACING', lambda: weights(33, F(0))) + rejects('r33_wrong_branch_has_odd_denominator', 'NON_DYADIC', + lambda: check_decomposition(33, F(33, 2), weights(33, F(33, 2)))) + rejects('r14_equal_step_does_not_imply_general_floor', 'NON_DYADIC', + lambda: check_decomposition(14, F(13, 2), weights(14, F(13, 2)))) + rejects('wrong_spacing_even_with_fitted_lower_moments', 'DEFECT_COEFFICIENTS', + lambda: check_decomposition(33, F(15), weights(33, F(15)), False)) + rejects('changed_weight', 'DEFECT_COEFFICIENTS', + lambda: check_decomposition(33, F(16), (ws[0], ws[1]+F(1, 32), ws[2]))) + rejects('omitted_initial_shear', 'SOURCES_NOT_RESTORED', + lambda: check_program(33, prefix+tail[1:])) + swapped = [tail[1], tail[0]]+tail[2:] + rejects('query_before_initial_shear', 'WRONG_EAGER_OUTPUT', + lambda: check_program(33, prefix+swapped)) + rejects('omitted_final_query', 'WRONG_EAGER_OUTPUT', + lambda: check_program(33, prefix+tail[:-1])) + rejects('fused_or_missing_original_child', 'RETAINED_CHILDREN', + lambda: check_program(33, prefix[2:]+tail)) + altered = tail.copy() + altered[4] = ('shear', F(-15)) + rejects('wrong_return_shear', 'SOURCES_NOT_RESTORED', + lambda: check_program(33, prefix+altered)) + rejects('output_feedback_outside_alphabet', 'EVENT_ALPHABET', + lambda: symbolic([('source_from_y', F(1))])) + rejects('duplicate_receipt_key', 'DUPLICATE_JSON_KEY', + lambda: json.loads('{"r":33,"r":129}', object_pairs_hook=unique_object)) + return passed + + +def evidence(): + authenticate() + polynomial_count = polynomial_checks() + eligible, classification_rows = [], [] + for r in range(3, 1025): + for u in (r, r-1): + ws = weights(r, F(u, 2)) + check_decomposition(r, F(u, 2), ws, False) + valid = all(dyadic(w) for w in ws) + need(valid == pow2(u), 'FINITE_CLASSIFICATION') + classification_rows.append([r, u, list(map(str, ws)), valid]) + if valid: + eligible.append([r, u]) + spacing_count = 0 + for r in range(3, 41): + for numerator in range(-32, 257): + if numerator == 0: + continue + d = F(numerator, 8) + ws = weights(r, d) + actual = sum(w*(i*d)**3 for i, w in enumerate(ws)) == moments(r)[2] + need(actual == (2*d in (r, r-1)), 'FINITE_SPACING_EXHAUSTION') + spacing_count += 1 + large = [] + for s in [1, 2, 3, 4, 5, 7, 11, 17, 31, 64, 128]: + r, u = 2**s+1, 2**s + ws = weights(r, F(u, 2)) + check_decomposition(r, F(u, 2), ws) + s1, s2, s3 = moments(r) + deferred = (F(1), F(r), (F(1), F(r), 3*s1, 3*s2, s3)) + tail = repair(r, u) + eager = symbolic(tail, deferred) + need(eager == (1, 0, (1, r, 0, 0, 0)), 'LARGE_REPAIR') + need(symbolic(inverse(tail), eager) == deferred, 'LARGE_REPAIR_INVERSE') + large.append({'s': s, 'r': str(r), 'weights_w0_w1_w2': list(map(str, ws))}) + programs, symbolic_events = [], 0 + for r, u in eligible: + if r > 257: + continue + tail = repair(r, u) + word = children(r)+tail + check_program(r, word) + deferred = symbolic(children(r)) + need(symbolic(inverse(tail), symbolic(word)) == deferred, 'REPAIR_INVERSE') + programs.append([r, u]) + symbolic_events += 3*len(word)+2*r+len(tail) + # PR6212's unequal-step positive scope control, not a new construction. + scope_tail = [('shear', F(-9)), ('cube', F(-91)), ('shear', F(-1)), + ('cube', F(91)), ('shear', F(-4)), ('cube_b', F(-2730))] + check_program(14, children(14)+scope_tail) + centered_tail = [('shear', F(-85)), ('cube', F(1)), ('shear', F(70)), + ('cube', F(-34)), ('shear', F(-35)), ('cube', F(33))] + check_program(50, children(50)+centered_tail) + numeric_cases = numeric_events = 0 + values = [F(-3, 2), F(0), F(5, 4)] + for r in [3, 4, 16, 33, 65, 129, 257]: + u = r if pow2(r) else r-1 + word = children(r)+repair(r, u) + for state in product(values, repeat=3): + out = numeric(word, state) + y, a, b = state + need(out == (y+r*a**3, a, b), 'DIRTY_ENDPOINT') + need(numeric(inverse(word), out) == state, 'DIRTY_FULL_INVERSE') + numeric_cases += 1 + numeric_events += 2*len(word) + rejected = controls() + invoice = Counter(f'{kind}:{value}' for kind, value in repair(33, 32)) + return { + 'status': 'PASS_CUBIC_EQUAL_STEP_CLASSIFICATION', + 'scope': 'Written all-r equal-step theorem with exact finite corroboration; no new kappa.', + 'polynomial_identities': polynomial_count, + 'arity_domain': [3, 1024], 'rational_decompositions': len(classification_rows), + 'classification_sha256': sha256(canonical(classification_rows).encode()).hexdigest(), + 'eligible_arity_and_twice_spacing': eligible, + 'spacing_scan': {'arity': [3, 40], 'd': 'k/8; -32<=k<=256; k!=0', 'cases': spacing_count}, + 'large_new_branch_fixtures': large, 'literal_symbolic_programs': programs, + 'literal_symbolic_events': symbolic_events, + 'dirty_numeric_cases': numeric_cases, + 'dirty_numeric_events_including_inverses': numeric_events, + 'unequal_step_positive_scope_control': 'PR6212 r14: three integer queries accepted', + 'centered_equal_step_scope_control': 'r50: slopes -35,0,35 accepted; zero must be at an end in the theorem', + 'negative_controls': rejected, + 'r33': {'weights_w0_w1_w2': list(map(str, weights(33, F(16)))), + 'defect_A2B_AB2_B3': list(map(str, (3*moments(33)[0], 3*moments(33)[1], moments(33)[2]))), + 'repair_event_prices': dict(sorted(invoice.items())), 'original_children_retained': 33}, + } + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('--emit', action='store_true', help='emit evidence without receipt comparison') + args = parser.parse_args() + result = evidence() + if not args.emit: + need(canonical(result) == canonical(read_json(HERE/'RESULT.json')), 'RECEIPT_MISMATCH') + print(json.dumps(result, sort_keys=True, indent=2)) + + +if __name__ == '__main__': + main()