diff --git a/research/cubic-local-solubility/PROOF.md b/research/cubic-local-solubility/PROOF.md new file mode 100644 index 0000000000..83eba9a2db --- /dev/null +++ b/research/cubic-local-solubility/PROOF.md @@ -0,0 +1,448 @@ +# Three-cube local solubility for every cubic-reader arity + +Prepared by apoursh with substantial OpenAI Codex assistance. Apache-2.0. +Nick Petalas's PR6200 supplies the fixed reader and defect; apoursh's PR6212 +supplies the coefficient-ring and general-frame contract. Nick Petalas's +PR6653 supplies the node lemma and the remaining-arity question. The +pure-original-B identity used below belongs to apoursh's PR6215. + +## Contract and theorem + +Let R=Z[1/2]. Keep all r>=3 children, in their original order and without +changing their interiors: + +``` +y += a^3 +a += b +``` + +The three streams are distinct registers with arbitrary incoming values +(Y,A,B); their values need not differ. The eager comparator restores +`a -= b` after each child and ends at (Y+rA^3,A,B). The deferred endpoint is +(Y+sum_{i=0}^{r-1}(A+iB)^3,A+rB,B). Put + +``` +S = r(r-1)/2, n = 2r-1, +f_r(A,B) = sum_{i=0}^{r-1}(A+iB)^3 - rA^3 + = 3S A^2 B + Sn A B^2 + S^2 B^3. +``` + +The inherited exact repair problem permits fixed, input-independent +R-weighted cube queries and invertible R-linear source transformations. +There is no output feedback, intermediate observation, nonlinear source +change, output recoding, child fusion or access to child interiors. Sources, +source inverses and query coefficients must be charged separately. An exact +repair would subtract f_r as a polynomial over R. This package proves a +necessary-condition result in finite quotients, not such an exact repair. + +**Theorem.** For every integer r>=3 and every odd integer m>1, there exist +integers q_j,u_j,v_j, j=0,1,2, with gcd(u_j,v_j)=1, such that + +``` +f_r(A,B) = sum_{j=0}^2 q_j(u_j A+v_j B)^3 (mod m) +``` + +coefficientwise. Each source row (u_j,v_j) extends to a determinant-one +integer matrix. Consequently an appended program with at most three +nonzero weighted cube queries restores the two sources **exactly** and +reproduces the eager output **modulo m**. The coefficients and frames may +depend on r and m but are independent of Y,A,B. + +There is also a three-term identity with coefficients and invertible source +frames in Z_p, the p-adic integers, for every odd prime p. This statement +asserts attainability by at most three queries; it is not a local query +minimum. + +For operational congruences, incoming values may be arbitrary elements of +R, reduced by R -> R/mR. The polynomial statement avoids any restriction to +finite test inputs. Fractions whose denominators are not invertible modulo +m are not assigned an artificial modular evaluation. + +**Consequence.** No proof that solely establishes nonexistence of an +unrestricted three-query representation in a finite odd quotient of R can +show an exact dyadic four-query lower bound for this family. The same is +true of finitely many such congruence tests imposed simultaneously. This +does not rule out odd-prime valuation arguments that constrain one fixed +global rational representation, or additional restrictions on its forms, +weights or schedule. + +## Identity integral at the prime 3 + +Set + +``` +c = (3r-1)/4, +w0 = -r(r-1)(r+13) / [6(3r-1)], +w1 = r(r^2-1) / [6(3r-5)], +wc = 16r(r-1)(r-2) / [3(3r-1)(3r-5)]. +``` + +Then the following identity holds over Q: + +``` +f_r = w0 A^3 + w1(A+B)^3 + wc(A+cB)^3. (I) +``` + +All three weights are nonzero for r>=3, and c>=2, so its three directions +0,1,c are distinct. Here is a derivation using the credited node lemma. +For nodes 0,1,c, that lemma's condition + +``` +3 e2 = n e1 - 3S +``` + +becomes (3-n)c=n-3S. Since r>=3, cancellation of r-2 gives c=(3r-1)/4. +The first three coefficient equations are + +``` +w0+w1+wc = 0, +w1+c*wc = S, +w1+c^2*wc = Sn/3. +``` + +Subtracting the second from the third and using c(c-1)!=0 gives +`wc=S(n/3-1)/(c(c-1))`, then `w1=S-c*wc` and `w0=-w1-wc`. +Substitution and cancellation give the three displayed weights. For +completeness, each node x satisfies x^3=(1+c)x^2-cx. Thus their weighted +third moment is + +``` +w1+c^3*wc = (1+c)Sn/3-cS + = S[n(1+c)/3-c] = S^2, +``` + +where the last equality is exactly the node condition. This supplies the +B^3 coefficient and proves (I) without a finite-search premise. + +Write Z_(3) for the rationals whose reduced denominator is prime to 3. +All coefficients of (I) lie in Z_(3). The factors 3r-1 and 3r-5 are prime +to 3; the remaining factor 3 in each displayed denominator cancels. Indeed, +modulo 3 the w0 numerator r(r-1)(r+13) becomes r(r-1)(r+1), and the w1 +numerator is r(r-1)(r+1). Each is a product of three consecutive residue +classes. The wc numerator contains r(r-1)(r-2), with the same property. +The node c has denominator 4. No cancellation claim about other odd primes +is made or needed. + +In particular, (I) defines an exact identity over Z_3 and a coefficientwise +identity modulo every power of 3. Its rows have the following +Z_(3)-valued determinant-one completions: + +``` +H0 = [[1,0],[0,1]], +H1 = [[1,1],[0,1]], +Hc = [[1,c],[0,1]]. +``` + +Their inverses are obtained by negating the upper-right entry. A source +frame may therefore expose each cube and then restore both sources in the +local ring. + +## Credited identity integral away from 3 + +The pure-original-B identity from PR6215 is + +``` +f_r = (S/9)(3A+rB)^3 + -(S/9)(3A+(r-1)B)^3 + + [S(3S-1)/9] B^3. (II) +``` + +As a rational identity it is valid for every r, including the arities at +which these coefficients fail to be dyadic. Expansion gives A^3 coefficient +zero, A^2 B coefficient 3S, and A B^2 coefficient Sn. Since +`r^3-(r-1)^3=6S+1`, its B^3 coefficient is + +``` +S(6S+1)/9 + S(3S-1)/9 = S^2. +``` + +Every coefficient in (II) lies in Z[1/3]. The source rows have +Z[1/3]-valued determinant-one completions + +``` +K0 = [[3,r],[0,1/3]], +K1 = [[3,r-1],[0,1/3]], +K2 = [[0,1],[-1,0]]. +``` + +These matrices and their inverses are defined over Z_p for every prime +p!=3 and modulo every integer coprime to 3. Thus (II) gives the required +local identity at all odd primes other than 3; (I) supplies the prime 3. +These are exact local identities with rational coefficients whose relevant +prime denominators are absent, not approximations. + +## A common elementary-shear word for the local frames + +Write + +``` +U(x) = [[1,x],[0,1]], L(x) = [[1,0],[x,1]]. +``` + +Their literal actions are `a += x*b` and `b += x*a`, respectively. Each has +determinant one and inverse obtained by negating x. For five coefficients +x0,...,x4, define W(x0,...,x4) by the following **execution order**: + +``` +U(x0), L(x1), U(x2), L(x3), U(x4). +``` + +On a column source vector its matrix is therefore +`U(x4)L(x3)U(x2)L(x1)U(x0)`. The same word realizes every local frame above: + +``` +H_j = W(c_j,0,0,0,0), (c0,c1,c2)=(0,1,c), +K_j = W(t_j/3,-3,-2/3,1,2), (t0,t1)=(r,r-1), +K2 = W(1,-1,1,0,0). +``` + +For the middle line, direct multiplication gives + +``` +U(2)L(1)U(-2/3)L(-3) = [[3,0],[0,1/3]], +``` + +and multiplication on the right by U(t/3) gives `[[3,t],[0,1/3]]`. +For the last line, `U(1)L(-1)U(1)=[[0,1],[-1,0]]`. This checks the +execution orientation, not just the individual source directions. All +H-word coefficients are defined modulo a power of 3, and all K-word +coefficients are defined modulo an integer coprime to 3. + +## Combining the identities at an arbitrary odd modulus + +Fix odd m>1 and write + +``` +m = m3*m0, m3=3^v_3(m), gcd(m0,3)=1. +``` + +Then gcd(m3,m0)=1. Use the three terms of (I), in their displayed order, +modulo m3; use the three terms of (II), in their displayed order, modulo m0. +When a factor is 1, omit its vacuous component. For each term j, combine +its pair of weights by the Chinese remainder theorem to obtain an integer +representative q_j in `{0,...,m-1}`. Separately combine each of the five +H-word coefficients with the corresponding K-word coefficient, obtaining +integer representatives x_j0,...,x_j4 in the same range. This is a +componentwise CRT operation on rational values whose denominators are +invertible in the component where they are used. + +Define the actual integer source frame + +``` +N_j = W(x_j0,x_j1,x_j2,x_j3,x_j4). +``` + +Since matrix multiplication commutes with reduction, N_j reduces to H_j +modulo m3 and to K_j modulo m0. It is an actual product of five integer +elementary shears, so it belongs to SL_2(Z), and its inverse is the reversed +word with every coefficient negated. If (u_j,v_j) is its first row, then +gcd(u_j,v_j)=1: any common divisor would divide the determinant 1. Thus +primitive integer source rows and their realizations are produced directly; +no division by a row entry or separate matrix-lifting theorem is required. + +The first row of each N_j reduces to the corresponding CRT combination of +the local cube directions. Polynomial operations commute with reduction, so + +``` +f_r = sum_{j=0}^2 q_j(u_j A+v_j B)^3 in (Z/mZ)[A,B]. (III) +``` + +Because both sides before reduction have integer coefficients, there is +an integer-coefficient cubic H_{r,m} such that + +``` +f_r(A,B) - sum_{j=0}^2 q_j(u_j A+v_j B)^3 = m H_{r,m}(A,B). (IV) +``` + +This is a finite explicit construction of the primitive lifts. Computing +m3 requires only stripping factors of 3, and the remaining preparation +uses rational cancellation, modular inverses and CRT. That preparation is +still work to be charged; no efficient physical backend is asserted. + +## Chronology and exact source restoration + +Let J be the set of j for which the chosen q_j is nonzero. From the actual +deferred endpoint first apply + +``` +a -= r*b +``` + +so that the source pair is exactly (A,B). Then, for each j in J, append + +``` +(a,b) = N_j(a,b) +y -= q_j*a^3 +(a,b) = N_j^-1(a,b) +``` + +The j-th query reads exactly u_j A+v_j B. Its inverse frame returns both +sources before the next frame. Therefore the full endpoint is exactly + +``` +(Y+rA^3 + m H_{r,m}(A,B), A, B). (V) +``` + +Sources are restored as exact algebraic expressions, including all dirty +incoming values; only the output comparison is weakened to a congruence. +For arbitrary Y,A,B in R, (V) reduces to the eager endpoint in R/mR. +There is no entry snapshot, initialized source, output feedback or altered +child. Each frame has its displayed algebraic inverse. Each query has a +literal inverse obtained by negating its weight, since its source does not +involve y. Reversing the full event sequence restores the incoming state +exactly, independently of the output congruence. + +There are |J|<=3 nonzero query events. Zero residue weights are represented +by zero and their frame/query/inverse blocks are omitted; they are not +counted as nonzero queries. The schedule has one initial shear and at most +three frame/inverse-frame pairs, each pair realized by ten literal shear +slots. Thus at most 31 elementary source shears suffice, with zero shears +omitted. This is neither an exact-three claim for each modulus nor a +source-operation minimum. The explicit shear words use only the two source +registers at the algebraic interface; a physical implementation must still +account for coefficient use and any private storage or restoration. + +The same chronology with H_j or K_j and the corresponding rational weights +gives exact output as well as exact sources over the appropriate Z_p. +These local programs can use coefficients outside R. Conversely, the +integer-lift program above uses coefficients in R but generally has only +modular output correctness. Neither statement supplies a global exact +three-query dyadic repair. + +## What the modular obstruction consequence does and does not say + +Suppose an exact global dyadic three-query program existed. Reducing its +coefficients and source matrices modulo an odd m would yield a program in +the quotient: determinants of GL_2(R) are units in R and remain units under +reduction. Thus nonexistence in a quotient would be a necessary obstruction +to global existence. The theorem proves that this particular nonexistence +condition never occurs for f_r: (III)-(V) provide a valid quotient witness. +Every nontrivial finite quotient of R is covered by an odd modulus. To see +this, intersect its kernel ideal with Z, obtaining dZ. If a/2^k lies in the +kernel, then a lies in that intersection, so the kernel is dR. Removing +factors of 2 from d does not change this ideal. The trivial quotient +provides no nonexistence obstruction either. + +For finitely many odd moduli m_1,...,m_k, take their least common multiple +M. The single integer-lift program constructed for M reduces to a witness +for all of them simultaneously. Independently requiring compatibility of +the finite congruences therefore does not create a nonexistence test. + +The witnesses depend on the modulus. We do not produce one fixed set of +dyadic coefficients that works for every modulus, a compatible bounded +family of integer lifts, or a global rational point satisfying every +integrality requirement. The exact identities over all Z_p likewise need +not select the same global representation. Therefore valuation arguments +concerning a fixed set of rational forms, an imposed direction pattern, +a height bound, one restricted coefficient family, or another global +arithmetic constraint remain possible. The theorem does not refute the +broader odd-prime-valuation suggestion in PR6653; it closes the narrower +route of unrestricted finite-quotient nonexistence. + +## The initially open arity r=15 + +For r=15, S=105 and + +``` +f_15 = 315A^2B+3045AB^2+11025B^3. +``` + +The two rational identities become + +``` +f_15 = -(245/11)A^3 + 14(A+B)^3 + (91/11)(A+11B)^3, + +f_15 = 315(A+5B)^3 + -(35/3)(3A+14B)^3 + +(10990/3)B^3. +``` + +The second display factors the first cube in (II). Its denominators are +powers of 3, while the first display's denominator 11 is prime to 3. +Neither displayed identity is an exact dyadic certificate. They suffice +for every odd prime and, by the construction above, every odd modulus. +No exact global three-query construction or four-query lower bound at r=15 +is asserted here. + +## Complete event boundary and remaining obligations + +Let Q_k^a price a complete weighted query `y += k*a^3`; let La_k and Lb_k +price `a += k*b` and `b += k*a`, respectively. Every price must include the +specified coefficients, source access, private work, restoration and return +under one matched backend. Zero events are omitted rather than assigned +an unspecified physical charge. For x=(x0,...,x4), the complete price +inventory of its forward frame word is + +``` +F(x) = La_x0 + Lb_x1 + La_x2 + Lb_x3 + La_x4. +``` + +The inverse executes the coefficients in reverse order with their signs +negated, with inventory + +``` +F_inverse(x) = La_-x4 + Lb_-x3 + La_-x2 + Lb_-x1 + La_-x0. +``` + +These are sums of named elementary events, not primitive unpriced frame +operations. The full appended inventory is + +``` +I_{r,m} = La_-r + sum_{j in J}[F(x_j) + Q_-qj^a + F_inverse(x_j)]. +``` + +All retained children remain paid. The eager bill is + +``` +E_r = r Q_1^a + r La_1 + r La_-1 + Omega_eager. +``` + +The constructed program's bill is + +``` +D_{r,m} = r Q_1^a + r La_1 + I_{r,m} + Omega_modular. +``` + +The Omega terms include any remaining coefficient generation, modulus +handling, rational cancellation, modular-inverse/CRT preparation, routing, +precision, storage, dispatch and controller costs not included in the +complete event prices. Those prices and residual terms are unknown, not +zero. If a common modular output contract and matched costs were +established, a cost saving would require + +``` +I_{r,m} + Omega_modular - Omega_eager < r La_-1. +``` + +No such inequality or backend is supplied. More fundamentally, modular +output equality does not satisfy the inherited exact-output specification; +this program cannot replace the eager exact program on the strength of a +price comparison. Recovering exact output, implementing the coefficients +and controlling growth or rounding would require additional proofs and +paid operations. No physical multiplier, supplier admission, +selected-assumption discharge, selected-frontier change or new kappa follows. + +## Attribution and proof status + +Nick Petalas's PR6200 supplies the cubic reader, chronological defect and +repair interface. apoursh's PR6212 supplies the localization and +nonmonic/general-frame contract; its unrestricted dyadic two-query floor is +not changed or used to assert a modular minimum here. apoursh's PR6215 +supplies identity (II) and the distinction between an original-B direction +and a temporarily changed register. Nick Petalas's PR6653 supplies the node +lemma used to derive (I), the integer-direction search boundary, and the +remaining-arity question that motivates this restricted obstruction result. +CubeJerry's PR6250 and AAAmirinu's PR6246 retain the equal-step and power-of-two +predecessor credit in that question's lineage. Sricharan Vagvala/theon199's +PR1532, Adam Gall's PR1205 and Hanson Sun's PR1246 retain the quadratic and +linear fixed-reader/paid-repair lineage. + +The Chinese remainder theorem, elementary matrix operations, localization +and binary-form decomposition are classical. The contribution +is the displayed 3-integral identity and its combination with the credited +identity to close this finite-quotient obstruction route at the repository's +specific cubic-reader interface. No historical-priority claim is made. +The written identities and explicit frame construction address all r and m in the +stated domains. Finite exact replay corroborates them; it does not establish +the infinite quantifiers by enumeration. Independent code is not independent +human review or formal proof-kernel acceptance. diff --git a/research/cubic-local-solubility/README.md b/research/cubic-local-solubility/README.md new file mode 100644 index 0000000000..f10ec0fa91 --- /dev/null +++ b/research/cubic-local-solubility/README.md @@ -0,0 +1,149 @@ +# Three cube queries survive every finite odd-modulus test + +**Scoped obstruction-method result; no new κ.** Prepared by apoursh with +substantial OpenAI Codex assistance. Apache-2.0. + +For every integer arity r>=3 and every odd modulus m>1, the fixed cubic-reader +defect has a representation modulo m by at most three weighted cubes. The +source forms can be reached using **integer determinant-one shears**, with +both arbitrary incoming sources restored **exactly**. Output repair is only +modulo m. One explicit construction uses at most 31 source shears and three +query slots; zero events can be omitted. + +Consequently, failure of unrestricted three-query feasibility in a finite +odd quotient cannot prove a four-query lower bound. The same conclusion holds +for any finite collection of odd moduli by using their least common multiple. +This answers one possible route in Open next question 1 of Nick Petalas's +[PR6653](https://github.com/CrocSwap/integer-mult-bounds/pull/6653), which +suggests testing odd-prime valuations at the unresolved arity 15. + +**It does not settle exact dyadic feasibility at r=15 or classify all arities.** +Arguments coupling prime valuations of a single global rational representation +remain possible. Local solutions are allowed to differ between primes; a +modular certificate need not give an exact output identity over Z[1/2]. + +## The construction + +Let S=r(r-1)/2 and n=2r-1. The defect from the retained original children is + +``` +f_r = 3S A^2 B + Sn A B^2 + S^2 B^3. +``` + +The [proof](PROOF.md) derives a three-cube identity on directions +0,1,(3r-1)/4 whose coefficients are integral at 3. The rational extension of +apoursh's PR6215 pure-B identity is integral away from 3. Split +m=3^v*b, gcd(b,3)=1, and combine the three weights and five shear slots for +each source frame by CRT. This produces integer instructions with literal +inverse instructions; no unproved source-frame lifting assumption is used. +The construction is independent of the input values, retains all children, +and needs no source snapshot, clean scratch, output feedback or child access. + +The discriminating case is r=15: + +``` +f15 = -(245/11) A^3 + 14(A+B)^3 + (91/11)(A+11B)^3 + = 315(A+5B)^3 - (35/3)(3A+14B)^3 + (10990/3)B^3. +``` + +The first identity works modulo powers of 3; the second works modulo every +integer coprime to 3. Neither displayed rational identity is a dyadic repair. +CRT solves every finite odd-modulus test, without supplying one exact global +repair. The independent checker exhibits an actual modulo-33 repair that +restores A,B but misses the exact eager output by -13472019. + +## Evidence and replay + +CPython 3.12, standard library only, from the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/cubic-local-solubility +python3.12 -I -W error -B research/cubic-local-solubility/verify.py +python3.12 -I -W error -B research/cubic-local-solubility/independent_check.py +``` + +The registered replay runs both checkers normally and with `-O`; explicit +checks remain active under optimization. No network, solver or generated +artifact is needed by either direct checker. + +- [verify.py](verify.py) proves both displayed coefficient identities by exact + polynomial arithmetic in Q[r] after clearing the nonzero denominators. + It checks the complete three-case denominator argument modulo 3, constructs + 3,682 integer-shear modular certificates, and symbolically executes every + retained child, query and inverse. Seven algebra/program rejection controls, + eight domain controls and three source-byte mutation controls must fail. +- [independent_check.py](independent_check.py) imports neither the primary + checker nor predecessor code. It directly expands both rational identities + for r=3..128; its distinct construction combines source rows, then uses + primitive integer lifts and Bezout frames. It checks 1,344 certificates, + 5,376 literal dirty-input executions, three rejected faulty variants and + the exact-versus-modular counterexample. +- [PROOF.md](PROOF.md) supplies the all-arity/all-modulus argument. The finite + check domains are corroboration, not an extension by enumeration. The two + implementations are separate Codex-agent work; independent human and + formal proof-kernel review are not claimed. + +The symbolic event inventory includes the initial restoration, every frame, +every inverse and all query slots. Physical pricing, coefficient preparation, +precision, storage, routing and a matched caller invoice remain unknown. +No bound improvement, priced supplier, shear optimality or modular query +minimum is claimed. The selected construction and its five assumptions remain +unchanged. + +## Scope and coordination + +[TASK.json](TASK.json) retains the exact `joint-query-controller` contextual +card and declares changed scope: a limitation on the finite-congruence +obstruction method, rather than a complete physical query-controller supplier. +The family decision is **narrow**: close this particular obstruction route, +then stop. This differs from the exact r=24 certificate in +[PR7475](https://github.com/CrocSwap/integer-mult-bounds/pull/7475) and the +fixed-weight Pell family in +[PR7478](https://github.com/CrocSwap/integer-mult-bounds/pull/7478). +Neither pending contribution is a mathematical or executable dependency here. + +Canonical upstream was pulled at entry to +`e54523517d0f03e58352e647c403a5af3e525a57`; guidance is unchanged from the +preceding round. Selected-baseline source orientation passed, not a scientific +cold replay of the selected supplier. Live all-state PR title/body searches on +2026-11-12 for `cubic local solubility`, `cubic odd moduli`, `three-query CRT`, +`cubic finite quotient` and related phrases found no duplicate. The nearest +modular obstruction, PR6215, explicitly requires a nonzero original-B query; +our 3-primary construction need not retain that restriction. +The dedicated overlap helper lacked remote corpora because `gh` was absent; +accessible Discussion pages were cached and did not certify current claims. +No absence-of-overlap guarantee or public reservation is asserted. + +## Open next questions + +1. **Global arithmetic at r=15.** Can one exact rational three-cube + representation have all actual form coefficients and weights dyadic? + Start with the predecessor node equation and compatibility of valuations + across one fixed triple, or exhibit a primitive-row certificate. This + matters because three versus four remains unresolved. Mere nonexistence + in a finite odd quotient is now excluded as a method. +2. **Restricted direction families.** Which additional constraints on a + three-query program create a valid modular obstruction? Start from + PR6215's original-B restriction and check whether the constraint survives + CRT patching. A precise contract is required: the unrestricted theorem + does not erase existing restricted-family lower bounds. + +Concrete first steps and blockers are also in TASK.json. Physical pricing of +these modular witnesses is not proposed as a supplier-development task. + +## Attribution and exact sources + +Nick Petalas's PR6200 supplies the fixed reader and defect; his PR6653 supplies +the node lemma and open classification question. apoursh's PR6212 supplies +the dyadic general-frame contract and lower-bound context. apoursh's PR6215 +supplies the pure-B identity and its explicitly restricted modulo-nine +obstruction; we use that identity rationally outside its dyadic attainment +classes and retain that distinction. The new result is the complementary +prime-local identity and the universal CRT consequence with legal integer +source frames, not a claim to the Chinese remainder theorem or classical +binary-form decomposition. + +[SOURCES.json](SOURCES.json) pins the exact predecessor bytes at the canonical +base, alongside historical provenance for the task catalogue and selected +record. All three proof-relevant inputs are declared in VERIFY.json. Frozen +sources, predecessor code and shared infrastructure are unchanged. diff --git a/research/cubic-local-solubility/SOURCES.json b/research/cubic-local-solubility/SOURCES.json new file mode 100644 index 0000000000..69a690922b --- /dev/null +++ b/research/cubic-local-solubility/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "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/cubic-three-query-arities/README.md", + "usage": "input", + "git_blob": "80c3a43f12e0ad4d586ed69eb3c8278cb60475e2", + "sha256": "d6f818ad69170fde178582595d3b5aa3e5ea1e6e4fde9d8e866f185aa2de5b55" + }, + { + "path": "research/dyadic-cubic-repair/PROOF.md", + "usage": "input", + "git_blob": "a1c41a9afc83302f8b664bb45467821b9c088f0f", + "sha256": "1296f12278e198b6a22d8d88355cd58c1ee4fc2ab0e6941721614bb06cb1e7d5" + } + ] +} diff --git a/research/cubic-local-solubility/TASK.json b/research/cubic-local-solubility/TASK.json new file mode 100644 index 0000000000..863e0b1ff9 --- /dev/null +++ b/research/cubic-local-solubility/TASK.json @@ -0,0 +1,103 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "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": "Prove that for every r>=3 and every finite odd modulus, the fixed cubic-reader defect has at most three weighted cube queries with integer SL2 source frames and exact source restoration, ruling out an unrestricted finite-congruence nonexistence method.", + "scope_change_reason": "A source-specific obstruction-method audit of PR6653 Open next question 1, not the original card complete physical supplier gate. This is distinct from the preceding exact r24 and fixed-weight Pell contributions.", + "bottleneck_link": "Side result: prevents pursuing an impossible finite-odd-modulus obstruction to unrestricted four-query lower bounds; exact global dyadic existence and complete physical invoices remain open.", + "budget_minutes": 60, + "stop_rule": "Stop after the all-arity local identities, legal CRT source-frame construction, sharp scope statement and independent replay; do not expand into a global classification or physical implementation campaign.", + "outcome": "partial", + "evidence": "PROOF.md universal argument; verify.py symbolic Q[r] identities and explicit integer-shear CRT programs; independent_check.py distinct primitive-row/Bezout construction, literal replays and modular-versus-exact counterexample.", + "author": "apoursh", + "ai_assistance": "Substantial OpenAI Codex assistance with separate theory, overlap/audit and independent implementation agents; no independent human or formal proof-kernel review.", + "open_questions": [ + { + "question": "Does r15 admit an exact global three-query dyadic repair?", + "why_it_matters": "This remains an unresolved case of the three-versus-four classification.", + "first_step": "Analyze compatible valuations across one fixed rational node/weight triple, or construct a primitive integer-row certificate; use PR6653 node condition.", + "blocked_by": "Local solvability does not imply one global dyadic solution; finite odd-modulus nonexistence is unavailable." + }, + { + "question": "Which restricted source-direction contracts still admit modular lower bounds?", + "why_it_matters": "The unrestricted theorem does not erase valid restrictions such as PR6215 original-B requirement.", + "first_step": "Test whether a named direction restriction is preserved by the two local identities and CRT source-frame construction.", + "blocked_by": "A precise restriction and its stability under reduction/patching must be specified." + } + ], + "family_decision": { + "decision": "narrow", + "evidence_status": "author-checked, with distinct independent Codex implementation", + "boundary": "All r>=3 and oddm>1; retain all children; integer source shears with exact inverses; exact source restoration and output coefficient congruence only; dirty input values in Z[1/2].", + "obligations": { + "prime_local_identities": "proved", + "integer_CRT_frame_and_restoration": "constructively upper-bounded", + "unrestricted_finite_modular_obstruction_route": "excluded within stated method", + "global_dyadic_existence": "unknown", + "physical_costs_and_caller_invoice": "unknown" + }, + "stop": "No further finite-modulus search for unrestricted nonexistence; reopen only for a named global or restricted-contract implication." + } +} diff --git a/research/cubic-local-solubility/VERIFY.json b/research/cubic-local-solubility/VERIFY.json new file mode 100644 index 0000000000..4369cb8c8b --- /dev/null +++ b/research/cubic-local-solubility/VERIFY.json @@ -0,0 +1,63 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/cubic-pure-b-boundary/PROOF.md", + "research/cubic-three-query-arities/README.md", + "research/dyadic-cubic-repair/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Universal Q[r] identities, source pins, integer-shear CRT, exact restoration, modular scope and rejection controls" + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Universal Q[r] identities, source pins, integer-shear CRT, exact restoration, modular scope and rejection controls under optimized Python" + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/independent_check.py" + ], + "timeout_seconds": 60, + "checks": "Independent rational expansion, primitive-row CRT and Bezout frames, dirty execution and counterexample controls" + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "-O", + "{package}/independent_check.py" + ], + "timeout_seconds": 60, + "checks": "Independent rational expansion, primitive-row CRT and Bezout frames, dirty execution and counterexample controls under optimized Python" + } + ] +} diff --git a/research/cubic-local-solubility/independent_check.py b/research/cubic-local-solubility/independent_check.py new file mode 100644 index 0000000000..77c9acacb7 --- /dev/null +++ b/research/cubic-local-solubility/independent_check.py @@ -0,0 +1,246 @@ +#!/usr/bin/env python3 +"""Independent bounded checks of the odd-modulus three-cube construction. + +No primary verifier, certificate, or predecessor implementation is imported. +Exact rational expansion, CRT, primitive integer lifts, Bezout frames, and +literal source restoration are checked separately. These finite checks +corroborate the proof; they are not a proof of its universal quantifiers. +""" + +from fractions import Fraction as F +from math import gcd +import json + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def cube(a, b): + return (a**3, 3 * a * a * b, 3 * a * b * b, b**3) + + +def add_scaled(left, right, coefficient): + return tuple(x + coefficient * y for x, y in zip(left, right)) + + +def defect(arity): + result = (-arity, 0, 0, 0) + for i in range(arity): + result = add_scaled(result, cube(1, i), 1) + return result + + +def identities(arity): + r = arity + s = r * (r - 1) // 2 + at_three = ( + (F(-r * (r - 1) * (r + 13), 6 * (3 * r - 1)), F(1), F(0)), + (F(r * (r * r - 1), 6 * (3 * r - 5)), F(1), F(1)), + (F(16 * r * (r - 1) * (r - 2), 3 * (3 * r - 1) * (3 * r - 5)), + F(1), F(3 * r - 1, 4)), + ) + away_from_three = ( + (F(s, 9), F(3), F(r)), + (F(-s, 9), F(3), F(r - 1)), + (F(s * (3 * s - 1), 9), F(0), F(1)), + ) + return at_three, away_from_three + + +def check_rational_identities(arity): + expected = defect(arity) + at_three, away = identities(arity) + for terms in (at_three, away): + result = (F(0),) * 4 + for weight, a, b in terms: + require(weight != 0, "zero rational identity weight") + result = add_scaled(result, cube(a, b), weight) + require(result == expected, "rational cubic identity failed") + for term in at_three: + require(all(value.denominator % 3 for value in term), "nonintegral at 3") + for term in away: + for value in term: + denominator = value.denominator + while denominator % 3 == 0: + denominator //= 3 + require(denominator == 1, "denominator has prime factor other than 3") + + +def residue(value, modulus): + if modulus == 1: + return 0 + require(gcd(value.denominator, modulus) == 1, "denominator not invertible") + return value.numerator * pow(value.denominator, -1, modulus) % modulus + + +def crt(left, left_modulus, right, right_modulus): + if left_modulus == 1: + return right % right_modulus + if right_modulus == 1: + return left % left_modulus + correction = (right - left) * pow(left_modulus, -1, right_modulus) + return (left + left_modulus * (correction % right_modulus)) % (left_modulus * right_modulus) + + +def bezout(a, b): + old_r, new_r = a, b + old_s, new_s = 1, 0 + old_t, new_t = 0, 1 + while new_r: + quotient = old_r // new_r + old_r, new_r = new_r, old_r - quotient * new_r + old_s, new_s = new_s, old_s - quotient * new_s + old_t, new_t = new_t, old_t - quotient * new_t + require(old_r == 1, "row is not primitive") + return old_s, old_t + + +def primitive_frame(a, b, modulus): + require(gcd(gcd(a, b), modulus) == 1, "row is not unimodular modulo m") + if b == 0: + b = modulus + # A complete residue period suffices. The proof supplies existence; + # this independent finite implementation does not factor b. + for k in range(b): + lifted_a = a + k * modulus + if gcd(lifted_a, b) == 1: + s, t = bezout(lifted_a, b) + frame = (lifted_a, b, -t, s) + require(frame[0] * frame[3] - frame[1] * frame[2] == 1, "frame determinant") + return frame + raise ValueError("primitive integer lift not found") + + +def certificate(arity, modulus, reduce_fraction=residue): + require(modulus > 1 and modulus % 2 == 1, "modulus must be odd and greater than one") + a, b = 1, modulus + while b % 3 == 0: + a *= 3 + b //= 3 + first, second = identities(arity) + terms = [] + for first_term, second_term in zip(first, second): + combined = tuple( + crt(reduce_fraction(x, a), a, reduce_fraction(y, b), b) + for x, y in zip(first_term, second_term) + ) + weight, u, v = combined + frame = primitive_frame(u, v, modulus) + require(frame[0] % modulus == u and frame[1] % modulus == v, "lift changed row residues") + terms.append((weight, frame)) + return tuple(terms) + + +def apply_frame(a, b, frame): + u, v, c, d = frame + if isinstance(a, tuple): + return add_scaled(tuple(u * x for x in a), b, v), add_scaled(tuple(c * x for x in a), b, d) + return u * a + v * b, c * a + d * b + + +def inverse(frame): + u, v, c, d = frame + return d, -v, -c, u + + +def symbolic_program(arity, terms, skip_inverse=None): + a, b, output = (1, 0), (0, 1), (0, 0, 0, 0) + for _ in range(arity): + output = add_scaled(output, cube(*a), 1) + a = add_scaled(a, b, 1) + a = add_scaled(a, b, -arity) + for index, (weight, frame) in enumerate(terms): + a, b = apply_frame(a, b, frame) + output = add_scaled(output, cube(*a), -weight) + if index != skip_inverse: + a, b = apply_frame(a, b, inverse(frame)) + return a, b, output + + +def accept(arity, modulus, terms, skip_inverse=None): + actual = (0, 0, 0, 0) + for weight, frame in terms: + u, v, c, d = frame + require(u * d - v * c == 1, "frame is not determinant one") + actual = add_scaled(actual, cube(u, v), weight) + require(all((x - y) % modulus == 0 for x, y in zip(actual, defect(arity))), "modular identity failed") + a, b, output = symbolic_program(arity, terms, skip_inverse) + require(a == (1, 0) and b == (0, 1), "sources not restored exactly") + require(all((x - y) % modulus == 0 for x, y in zip(output, (arity, 0, 0, 0))), "modular eager output failed") + + +def literal_program(arity, terms, a, b, y): + for _ in range(arity): + y += a**3 + a += b + a -= arity * b + for weight, frame in terms: + a, b = apply_frame(a, b, frame) + y -= weight * a**3 + a, b = apply_frame(a, b, inverse(frame)) + return a, b, y + + +def reject(label, callback): + try: + callback() + except ValueError: + return label + raise ValueError(f"negative control accepted: {label}") + + +def wrong_inverse(value, modulus): + if modulus == 1: + return 0 + return value.numerator * value.denominator % modulus + + +def run_checks(): + arities = tuple(range(3, 65)) + (97, 128) + moduli = (3, 9, 27, 81, 5, 7, 11, 23, 25, 49, 121, 529, + 15, 33, 69, 99, 207, 363, 1587, 2783, 29403) + dirty_inputs = ((1, 0, 7), (0, 1, -3), (-2, 3, 19), (5, -4, -11)) + for arity in range(3, 129): + check_rational_identities(arity) + for arity in arities: + for modulus in moduli: + terms = certificate(arity, modulus) + accept(arity, modulus, terms) + for a, b, y in dirty_inputs: + final_a, final_b, final_y = literal_program(arity, terms, a, b, y) + require((final_a, final_b) == (a, b), "literal source restoration failed") + require((final_y - y - arity * a**3) % modulus == 0, "literal modular output failed") + + terms = certificate(15, 33) + controls = [ + reject("denominator used instead of its inverse", lambda: accept(15, 33, certificate(15, 33, wrong_inverse))), + reject("omitted inverse source frame", lambda: accept(15, 33, terms, skip_inverse=2)), + reject("wrong retained arity", lambda: accept(16, 33, terms)), + ] + a, b, y = 1, 1, 7 + final_a, final_b, final_y = literal_program(15, terms, a, b, y) + exact_target = y + 15 * a**3 + require((final_a, final_b) == (a, b), "counterexample source restoration failed") + require(final_y != exact_target, "counterexample unexpectedly gives exact equality") + require((final_y - exact_target) % 33 == 0, "counterexample lacks modular equality") + controls.append("modular equality distinguished from exact global equality") + return { + "status": "pass", + "rational_identity_arities": [3, 128], + "modular_arities": list(arities), + "moduli": list(moduli), + "symbolic_modular_certificates": len(arities) * len(moduli), + "literal_dirty_runs": len(arities) * len(moduli) * len(dirty_inputs), + "rejected_controls": controls, + "not_an_exact_repair": { + "arity": 15, "modulus": 33, "input_a_b_y": [a, b, y], + "exact_target": exact_target, "actual_output": final_y, + "difference": final_y - exact_target, + }, + } + + +if __name__ == "__main__": + print(json.dumps(run_checks(), indent=2)) diff --git a/research/cubic-local-solubility/verify.py b/research/cubic-local-solubility/verify.py new file mode 100644 index 0000000000..1bb3dd22f2 --- /dev/null +++ b/research/cubic-local-solubility/verify.py @@ -0,0 +1,217 @@ +"""Symbolic identities and explicit integer-shear CRT construction. + +apoursh, with substantial OpenAI Codex assistance. Apache-2.0. +No external dependencies, subprocesses, caches, output files or assertions. +""" +from copy import deepcopy +from fractions import Fraction as F +from hashlib import sha256 +import json +from math import gcd +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def trim(p): + p = list(map(F, p)) + while len(p) > 1 and p[-1] == 0: + p.pop() + return tuple(p) + + +def add(a, b): + out = [F(0)] * max(len(a), len(b)) + for i, x in enumerate(a): out[i] += x + for i, x in enumerate(b): out[i] += x + return trim(out) + + +def scale(a, k): + return trim([k*x for x in a]) + + +def sub(a, b): + return add(a, scale(b, -1)) + + +def mul(*polys): + result = (F(1),) + for p in polys: + out = [F(0)] * (len(result)+len(p)-1) + for i, x in enumerate(result): + for j, y in enumerate(p): out[i+j] += x*y + result = trim(out) + return result + + +def cube_poly(a, b): + return (mul(a,a,a), scale(mul(a,a,b),3), scale(mul(a,b,b),3), mul(b,b,b)) + + +def tensor_poly(weights, forms): + total = [(F(0),)] * 4 + for w, (a, b) in zip(weights, forms): + total = [add(x,mul(w,y)) for x,y in zip(total,cube_poly(a,b))] + return total + + +def symbolic_identities(first_factor=32, second_sign=-1): + """Check Q[r] coefficient identities after clearing only nonzero factors.""" + r, one, zero = (0,1), (1,), (0,) + s = scale(mul(r,sub(r,one)),F(1,2)) + n = sub(scale(r,2),one) + target = [zero,scale(s,3),mul(s,n),mul(s,s)] + u,v = sub(scale(r,3),one),sub(scale(r,3),(5,)) + denominator = scale(mul(u,v),6) + # This is D*w_j, with D=6(3r-1)(3r-5); node c=(3r-1)/4. + numerators = [scale(mul(r,sub(r,one),add(r,(13,)),v),-1), + mul(r,sub(mul(r,r),one),u), + scale(mul(r,sub(r,one),sub(r,(2,))),first_factor)] + actual1 = tensor_poly(numerators,[(one,zero),(one,one),(one,scale(u,F(1,4)))]) + expected1 = [mul(denominator,t) for t in target] + weights2 = [scale(s,F(1,9)),scale(s,F(-1,9)), + scale(mul(s,add(scale(s,3),(second_sign,))),F(1,9))] + actual2 = tensor_poly(weights2,[((3,),r),((3,),sub(r,one)),(zero,one)]) + return actual1 == expected1 and actual2 == list(map(trim,target)) + + +def cube(a,b): + return (a**3,3*a*a*b,3*a*b*b,b**3) + + +def domain(r,m): + require(type(r) is int and r>=3, 'arity must be an integer >=3') + require(type(m) is int and m>1 and m%2==1, 'modulus must be an odd integer >1') + + +def local_data(r): + s = r*(r-1)//2 + weights3 = [F(-r*(r-1)*(r+13),6*(3*r-1)), + F(r*(r*r-1),6*(3*r-5)), + F(16*r*(r-1)*(r-2),3*(3*r-1)*(3*r-5))] + weights_away = [F(s,9),F(-s,9),F(s*(3*s-1),9)] + # Five chronological shear slots, acting on a,b,a,b,a respectively. + words3 = [(c,0,0,0,0) for c in (F(0),F(1),F(3*r-1,4))] + words_away = [(F(t,3),-3,F(-2,3),1,2) for t in (r,r-1)] + words_away.append((1,-1,1,0,0)) + return weights3,weights_away,words3,words_away + + +def residue(value,m): + if m==1: return 0 + value = F(value) + require(gcd(value.denominator,m)==1, 'denominator is not a residue unit') + return value.numerator*pow(value.denominator,-1,m)%m + + +def crt(x,y,a,b): + if a==1: return y%b + if b==1: return x%a + return (x+a*((y-x)*pow(a,-1,b)%b))%(a*b) + + +def construct(r,m): + domain(r,m) + a,b = 1,m + while b%3==0: a,b = a*3,b//3 + weights3,weights_away,words3,words_away = local_data(r) + def combine(x,y): return crt(residue(x,a),residue(y,b),a,b) + weights = [combine(x,y) for x,y in zip(weights3,weights_away)] + words = [[combine(x,y) for x,y in zip(xs,ys)] for xs,ys in zip(words3,words_away)] + return weights,words + + +def frame(word): + rows = [[1,0],[0,1]] + for i,k in zip((0,1,0,1,0),word): + rows[i] = [x+k*y for x,y in zip(rows[i],rows[1-i])] + require(rows[0][0]*rows[1][1]-rows[0][1]*rows[1][0]==1,'noninvertible frame') + return rows + + +def replay(r,weights,words,restore=True): + rows, output = [[1,0],[0,1]],[0]*4 + for _ in range(r): + output = [x+y for x,y in zip(output,cube(*rows[0]))] + rows[0] = [x+y for x,y in zip(rows[0],rows[1])] + rows[0] = [x-r*y for x,y in zip(rows[0],rows[1])] + for q,word in zip(weights,words): + for i,k in zip((0,1,0,1,0),word): + rows[i] = [x+k*y for x,y in zip(rows[i],rows[1-i])] + output = [x-q*y for x,y in zip(output,cube(*rows[0]))] + if restore: + for i,k in reversed(list(zip((0,1,0,1,0),word))): + rows[i] = [x-k*y for x,y in zip(rows[i],rows[1-i])] + return output,rows + + +def certificate_ok(r,m,weights,words,restore=True): + output,rows = replay(r,weights,words,restore) + return rows==[[1,0],[0,1]] and all((x-y)%m==0 for x,y in zip(output,(r,0,0,0))) + + +def source_binding(): + pins = json.loads((HERE/'SOURCES.json').read_text())['files'] + checked = 0 + for row in pins: + if row['usage']!='input': continue + data = (ROOT/row['path']).read_bytes() + require(sha256(data).hexdigest()==row['sha256'],'source hash mismatch') + require(sha256(data+b'\n').hexdigest()!=row['sha256'],'source mutation accepted') + checked += 1 + return checked + + +def main(): + inputs = source_binding() + require(symbolic_identities(),'universal rational identity') + require(not symbolic_identities(first_factor=31),'wrong third weight accepted') + require(not symbolic_identities(second_sign=1),'wrong pure-B correction accepted') + # These three residue cases are exhaustive for integer r modulo3. + for r in range(3): + require(r*(r-1)*(r+13)%3==0 and r*(r*r-1)%3==0 + and r*(r-1)*(r-2)%3==0,'missing factor3') + require((3*r-1)%3!=0 and (3*r-5)%3!=0,'nonunit local denominator') + cases = [(r,m) for r in range(3,49) for m in range(3,160,2)] + cases += [(r,m) for r in (3,15,22,24,30,31,97,1000) + for m in (243,729,363,891,315,22275)] + for r,m in cases: + weights,words = construct(r,m) + for word in words: frame(word) + require(certificate_ok(r,m,weights,words),f'CRT certificate r={r},m={m}') + # An integer residue representative is an exact dyadic program, but only + # its output congruence is certified. Its exact cubic residual is nonzero. + weights,words = construct(15,33) + output,rows = replay(15,weights,words) + require(rows==[[1,0],[0,1]],'scope-control source restoration') + require(output!=[15,0,0,0] and all((x-y)%33==0 for x,y in zip(output,(15,0,0,0))), + 'modular success was conflated with exact equality') + badw = weights[:]; badw[0] += 1 + require(not certificate_ok(15,33,badw,words),'wrong query weight accepted') + badwords = deepcopy(words); badwords[1][0] += 1 + require(not certificate_ok(15,33,weights,badwords),'wrong CRT shear accepted') + require(not certificate_ok(15,33,weights,words,restore=False),'missing frame inverse accepted') + require(not certificate_ok(14,33,weights,words),'wrong retained arity accepted') + try: residue(F(1,3),9) + except ValueError: pass + else: raise ValueError('illegal local reduction accepted') + rejected_domains = 0 + for r,m in ((2,9),(True,9),(F(3),9),(3,1),(3,0),(3,8),(3,-3),(3,True)): + try: construct(r,m) + except ValueError: rejected_domains += 1 + else: raise ValueError('invalid domain accepted') + print(json.dumps({'status':'pass','symbolic_all_arity_identities':2, + 'integer_shear_modular_certificates':len(cases), + 'source_inputs_and_mutations':inputs, + 'algebra_program_rejections':7,'domain_rejections':rejected_domains, + 'exact_vs_modular_scope_control':'pass'},indent=2)) + + +if __name__=='__main__': main()