diff --git a/research/cubic-pell-family/PROOF.md b/research/cubic-pell-family/PROOF.md new file mode 100644 index 0000000000..1d57f60cf6 --- /dev/null +++ b/research/cubic-pell-family/PROOF.md @@ -0,0 +1,305 @@ +# A Pell family for the fixed cubic repair + +## Scope and provenance + +This answers Open next question 2 of Nick Petalas's +[PR6653](https://github.com/CrocSwap/integer-mult-bounds/pull/6653): its +certificates at arities 7 and 97 have defect weights `(-r,r/2,r/2)` on +directions `(0,d,e)`; does this pattern extend to an infinite family? +The answer is yes. We also classify **this fixed weight pattern with rational +directions**, not all three-query repairs. + +The fixed cubic reader comes from PR6200. The repair interface and cited +three-query lower bound are apoursh's PR6212; PR6215 treats another direction +family. AAAmirinu's PR6246 and CubeJerry's PR6250 supply the earlier +power-of-two and power-of-two-plus-one branches. PR6653 supplies the explicit +question, the two seed certificates and their predecessor attribution. Its +node lemma is consistent with the calculation below, but the proof here uses +direct coefficient comparison. The source manifests identify the exact bytes +consulted. Classical Pell descent and power-sum identities are not claimed as +new mathematics. + +This is a polynomial identity and a literal restoration program. Query counts +are local operation counts, not a physical cost or a complete recursive +invoice. There is no new supplier admission or κ claim. + +## 1. The defect and fixed weight pattern + +Let the integer arity satisfy $r>2$. All $r$ children are retained: + +```text +repeat r times: + y += a^3 + a += b +``` + +For arbitrary entry values $y=Y,a=A,b=B$, their endpoint is + +$$ + a=A+rB,\qquad b=B,\qquad + y=Y+\sum_{i=0}^{r-1}(A+iB)^3. +$$ + +The target eager endpoint is $a=A,b=B,y=Y+rA^3$. Thus the defect to remove is + +$$ + D_r(A,B)=3S_1A^2B+3S_2AB^2+S_3B^3, +$$ + +where + +$$ + S_1=\frac{r(r-1)}2,\qquad + S_2=\frac{r(r-1)(2r-1)}6,\qquad + S_3=\frac{r^2(r-1)^2}4. +$$ + +For rational directions $d,e$, consider the fixed pattern + +$$ + W_{r,d,e}(A,B) + =-rA^3+\frac r2(A+dB)^3+\frac r2(A+eB)^3. \tag{1} +$$ + +**Theorem 1 (classification of the fixed pattern).** For every integer $r>2$, +the identity $W_{r,d,e}=D_r$ holds with rational $d,e$ if and only if there +is a positive integer $n$ such that + +$$ + r^2-3n^2=1,\qquad + \{d,e\}=\left\{\frac{r-1-n}{2},\frac{r-1+n}{2}\right\}. \tag{2} +$$ + +In every such case the directions are integers, and after ordering them they +satisfy $00$, then + +$$ + 3p^2=(r^2-1)q^2. +$$ + +Since $p^2$ and $q^2$ are coprime, $q^2\mid3$, forcing $q=1$. +Thus $n$ is an integer and (2) follows. It is positive because $r>2$. + +Conversely, suppose (2). Equations (3) and (4) hold. The remaining moment is +also correct: + +$$ + \frac r2(d^3+e^3) + =\frac r2\bigl((d+e)^3-3de(d+e)\bigr) + =\frac{r^2(r-1)^2}{4}=S_3. +$$ + +All four coefficients therefore agree. + +Modulo 4, $r^2-3n^2=1$ implies that $r$ odd makes $n$ even, and $r$ +even makes $n$ odd. Thus $r-1\pm n$ is even and both directions are +integers. Furthermore + +$$ + (r-1)^2-n^2=\frac{2(r-1)(r-2)}3>0, +$$ + +so $n0$. Positivity of $n$ gives $d0$, since $r>\sqrt3n>3n/2$, and $0\le n'2$. ∎ + +## 3. Infinitely many arities outside the earlier classes + +For comparison with the classes listed by PR6653, use the even-index +subsequence + +$$ + R_j=r_{2j},\qquad N_j=n_{2j},\qquad j\ge0. +$$ + +It has the recurrence + +$$ + (R_0,N_0)=(1,0),\qquad + R_{j+1}=7R_j+12N_j,\quad N_{j+1}=4R_j+7N_j. \tag{8} +$$ + +All $R_j$ are odd. They also satisfy + +$$ + R_{j+2}=14R_{j+1}-R_j, +$$ + +so modulo 9 their values repeat $1,7,7$. Indeed the first four residues +are $1,7,7,1$, the next is 7, and the two-coordinate recurrence then repeats +its initial state. Therefore + +$$ + R_j\equiv7\pmod9\quad\hbox{when }j\equiv1,2\pmod3. \tag{9} +$$ + +These arities lie outside the residue classes + +$$ + r\bmod9\in\{0,1,2,5,8\} +$$ + +covered by the cited PR6212/PR6215 constructions. They are at least 7, so +are not the exceptional arities 3 and 4. Being odd and greater than 1, they +are not powers of 2. + +To exclude the power-of-two-plus-one branch, square the fundamental solution: + +$$ + R_j=r_j^2+3n_j^2=1+6n_j^2. +$$ + +For every $j\ge1$, $R_j-1=6n_j^2$ is positive and divisible by 3; it +cannot be a power of 2. Hence $R_j\ne2^s+1$ for every nonnegative integer +$s$. + +The indices $j\ge1$ with $j\not\equiv0\pmod3$ give infinitely many +strictly increasing arities outside **all the earlier infinite classes +listed by PR6653**. This comparison is with those precise classes, not a +claim to have classified every construction in the literature or every later +contribution. Its first values are + +$$ + 7,\ 97,\ 18817,\ 262087,\ 50843527,\ 708158977,\ldots. +$$ + +The first two are Petalas's already established finite certificates. The +uniform family and the complete fixed-pattern classification are the added +result; those seed examples are not claimed anew. + +For example, at $r=18817,n=10864$, the directions are $d=3976,e=14840$ +and the defect weights are $(-18817,18817/2,18817/2)$. + +## 4. Three queries and three shears restore the dirty inputs + +For any $k\ge2$, take the ordered integer directions $02$, including its stated general dyadic-frame model. Combining that +predecessor theorem with this construction makes the dyadic repair query +minimum **exactly three at these arities**, under that same model. The lower +bound is a dependency, not re-proved by the present finite checker. +In particular, query coefficients are fixed independently of input data; +the model has no output feedback into sources, nonlinear source changes, +intermediate observations or access to child interiors. One signed weighted +cube accumulation counts as one query, with source changes additional. + +## 5. What this does not settle + +The classification concerns the weight shape in (1). Failure of the Pell +equation excludes that shape only; it does not exclude other weights, +directions or dyadic frames, nor prove a four-query minimum at any other +arity. A verified finite prefix corroborates the formulas but is not the +proof of the infinite family; Sections 1–3 supply that proof. + +The three-query/three-shear schedule has growing coefficients. Its native +query and shear costs, routing, precision, storage, full caller and recursive +invoice remain unpriced. The formal operation counts do not imply a saving +over eager restoration, a physical realization, or an improvement to the +selected conditional bound. No independent human or formal proof-kernel +acceptance is claimed. + +Prepared by **apoursh** with substantial **OpenAI Codex and subagent +assistance**. Retain Nick Petalas, CubeJerry, AAAmirinu and the cited source +lineage above. Apache-2.0. diff --git a/research/cubic-pell-family/README.md b/research/cubic-pell-family/README.md new file mode 100644 index 0000000000..7732ff31ba --- /dev/null +++ b/research/cubic-pell-family/README.md @@ -0,0 +1,151 @@ +# An infinite equal-weight family for cubic-reader repair + +**Scoped proof and exact checks; no new κ.** Prepared by apoursh with +substantial OpenAI Codex and subagent assistance. Apache-2.0. + +This answers **Open next question 2 of Nick Petalas's +[PR6653](https://github.com/CrocSwap/integer-mult-bounds/pull/6653)**. +Its certificates at arities 7 and 97 have weights `(-r,r/2,r/2)` on +integer directions `(0,d,e)`. We classify that pattern for every integer +`r>2`, even allowing arbitrary rational directions: + +```text +D_r(A,B) = -r*A^3 + (r/2)*(A+d*B)^3 + (r/2)*(A+e*B)^3 +iff +r^2 - 3*n^2 = 1, n a positive integer, +{d,e} = {(r-1-n)/2, (r-1+n)/2}. +``` + +Here `D_r = sum_{i (2r+3n,r+2n)`; the nondegenerate repairs start +at `(7,4)`. The proof includes elementary descent, not just a recurrence +that generates examples. + +The even-index subsequence with half-index not divisible by three gives +infinitely many arities outside every earlier infinite class listed by +PR6653. Its first values are `7,97,18817,262087,50843527,708158977`. +The first two remain Petalas's existing examples. The new result is their +uniform continuation and the complete classification of this weight pattern. + +After retaining all `r` children `y += a^3; a += b`, the repair is: + +```text +a += (e-r)*b +y -= (r/2)*a^3 +a -= n*b +y -= (r/2)*a^3 +a -= d*b +y += r*a^3 +``` + +It uses **three cube queries and three integer shears** and ends at +`(y,a,b)=(Y+r*A^3,A,B)` for arbitrary incoming `Y,A,B`. PR6212's cited +dyadic lower bound makes three queries optimal in its stated model at +these arities. This package does not re-prove that lower bound or claim +three-shear optimality. See [PROOF.md](PROOF.md) for all hypotheses and +exceptions, including the collapsed `r=2` boundary. + +## Evidence and reproduction + +CPython 3.12.14, macOS arm64, standard library only: + +```sh +python3.12 -B scripts/research_package.py --package research/cubic-pell-family +python3.12 -I -W error -B research/cubic-pell-family/verify.py +python3.12 -I -W error -B research/cubic-pell-family/independent_check.py +python3.12 -B scripts/check_research_commit.py --package research/cubic-pell-family --check-modes --check-source-history +python3.12 -B scripts/export_research_package.py export --package research/cubic-pell-family --ref HEAD --output /tmp/cubic-pell.tar +python3.12 -B scripts/export_research_package.py check /tmp/cubic-pell.tar +``` + +The registered hook runs both engines normally and with `-O`, isolated and +warning-strict. No predecessor executable is imported. + +- `verify.py` checks all four cubic coefficients of the exact **symbolic** + off-Pell residual in the two indeterminates `(r,n)`, corroborates 96 + recurrence terms and 32 terms outside the earlier classes, screens arities + 3 through 10,000 by integer square roots, and rejects 12 algebra/domain + controls. It authenticates four predecessor files and rejects altered + bytes for each using in-memory mutations. +- `independent_check.py` uses its own sparse-polynomial interpreter. It + executes every original child and the literal repair for seven arities + through 18,817, retaining a formal arbitrary dirty destination. It checks + 40 rational dirty-input examples and all 1,063,536 direction pairs in the + declared domains: `0<=d=3 and rational directions d,e for the equal-weight cubic defect representation (-r,r/2,r/2) on (0,d,e); derive the Pell recurrence, a three-shear dirty-restoring schedule, and infinitely many arities outside the earlier classes.", + "scope_change_reason": "A source-specific algebraic side question, following the same recorded scope change in PR6653. This establishes a uniform local module, not the catalogue card's complete current-supplier invoice.", + "bottleneck_link": "Side result: replace isolated arity certificates by a complete fixed-weight classification and uniform three-query repair. Query/shear implementation costs, caller integration and precision remain unknown.", + "budget_minutes": 60, + "stop_rule": "Stop after a written all-arity proof, independent exact corroboration and source/export controls; do not widen to arbitrary three-query classification or a physical backend without a new budget decision.", + "outcome": "partial", + "evidence": "PROOF.md; verify.py; independent_check.py; registered replay and committed/export checks.", + "author": "apoursh", + "ai_assistance": "Substantial OpenAI Codex and subagent assistance in derivation, coding, independent checks and packaging; no independent human or formal-kernel review claimed.", + "open_questions": [ + { + "question": "Which arities outside the Pell family and earlier constructions admit other three-query dyadic repairs?", + "why_it_matters": "The equal-weight classification does not classify arbitrary three-query weights or frames.", + "first_step": "For r=15, test the PR6653 node condition and odd-prime weight valuations with unequal weights.", + "blocked_by": "A bounded search failure is not a four-query lower bound." + }, + { + "question": "Does the three-shear Pell schedule improve a complete priced caller?", + "why_it_matters": "A fixed number of weighted queries can still cost more than eager restoration.", + "first_step": "Price r=7 and r=97 under one pinned physical backend using the complete comparison in PR6250.", + "blocked_by": "No backend, coefficient implementation, preparation/routing/precision/storage or full invoice is supplied." + } + ], + "selection_context": { + "seed": "20202020202020202020202020202020", + "track": "recursive-interfaces", + "priority_revision": 8, + "catalog_sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81", + "selected_record_sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1", + "catalog_selection": { + "context": { + "refreshed_on": "2026-10-26", + "kappa": "62009/20000000", + "source_pr": 5599, + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "record": "certificates/selected-result.json", + "review": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "orientation_command": "python3 -B scripts/research_selected_baseline.py", + "scope": "Revision-8 strategic reassessment. PR5599 is selected and independently replayed under five inherited assumptions. Archived successor claims are not admissions. Compare complete signed target/paid moments and the current nine outer rows; no historical balanced-transfer cap is imposed." + }, + "matches_selected": false, + "differences": { + "kappa": { + "catalog": "62009/20000000", + "selected": "363005817/100000000000" + }, + "source_commit": { + "catalog": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected": "93effe2a135bf57b9e484cb630d8dd057159aec9" + }, + "review": { + "catalog": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "selected": "docs/research/pr-intake-evidence/pr7000-application/PROOF-REVIEW.md" + } + }, + "uncompared_fields": [], + "scope": "Compare only kappa, source_commit/audited_source_head and review. Missing fields are unknown. The catalogue context is historical; use selected for the current result and replay. Matching metadata does not establish current task coverage or scientific validation. Input hashes bind this comparison to the picker receipt, not the complete selected source closure." + } + }, + "overlap": { + "predecessor_pr": 6653, + "predecessor_head": "3ea9965e13457fdafc70b784305d026ebfa8faa2", + "live_all_state_searches": { + "6653": 3, + "Pell": 3, + "Pell cubic": 2, + "cubic repair": 21 + }, + "source_overlap_helper": "Attempted author-filtered include-closed intake; gh unavailable, open/closed corpora null. Supplemented by live connector searches and full HEAD filename inventory; no exhaustive body/discussion coverage claimed.", + "discussion_check": "Start-here, active Discussion list and newest-sorted handoffs read via public web retrieval; returned newest handoff dated November 11, so November 12 comment coverage incomplete.", + "advance_claim": "Connector returned403; browser fallback could not safely select the GitHub window. No public claim posted." + }, + "family_expansion_decision": { + "decision": "narrow", + "target": "One all-arity fixed-weight lemma and local restoring schedule.", + "complete_cost_obligations": { + "algebraic_output_and_source_restoration": "proved in PROOF.md", + "query_count_and_shear_count": "constructively bounded by three each", + "physical_backend_and_full_caller_bill": "unknown", + "coefficient_preparation_routing_precision_storage": "unknown" + }, + "stop": "No downstream optimization or supplier claim without a priced source-compatible caller." + } +} diff --git a/research/cubic-pell-family/VERIFY.json b/research/cubic-pell-family/VERIFY.json new file mode 100644 index 0000000000..cdad252e16 --- /dev/null +++ b/research/cubic-pell-family/VERIFY.json @@ -0,0 +1,64 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/cubic-equal-step-classification/PROOF.md", + "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": 120, + "checks": "Exact symbolic residual, recurrence/classification controls, finite all-size corroboration and pinned-source integrity." + }, + { + "argv": [ + "{python}", + "-O", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact symbolic residual, recurrence/classification controls, finite all-size corroboration and pinned-source integrity." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/independent_check.py" + ], + "timeout_seconds": 120, + "checks": "Independent exact polynomial and dirty-program replay, finite census and mutation controls." + }, + { + "argv": [ + "{python}", + "-O", + "-I", + "-W", + "error", + "-B", + "{package}/independent_check.py" + ], + "timeout_seconds": 120, + "checks": "Independent exact polynomial and dirty-program replay, finite census and mutation controls." + } + ] +} diff --git a/research/cubic-pell-family/independent_check.py b/research/cubic-pell-family/independent_check.py new file mode 100644 index 0000000000..34d46e5def --- /dev/null +++ b/research/cubic-pell-family/independent_check.py @@ -0,0 +1,239 @@ +#!/usr/bin/env python3 +"""Independent finite corroboration by literal polynomial execution. + +No imports from the primary verifier or predecessor programs, no closed power +sum or node-weight formula, and no floating point. The universal statement is +the written proof; these finite checks cover implementation and scope failures. +Prepared by apoursh with substantial OpenAI Codex assistance. Apache-2.0. +""" + +from fractions import Fraction +from math import isqrt + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def add(left, right, scale=1): + result = dict(left) + for exponent, value in right.items(): + result[exponent] = result.get(exponent, 0) + scale * value + if result[exponent] == 0: + del result[exponent] + return result + + +def multiply(left, right): + result = {} + for p, x in left.items(): + for q, y in right.items(): + exponent = tuple(a + b for a, b in zip(p, q)) + result[exponent] = result.get(exponent, 0) + x * y + return {p: value for p, value in result.items() if value} + + +def cube(poly): + return multiply(multiply(poly, poly), poly) + + +A = {(1, 0, 0): 1} +B = {(0, 1, 0): 1} +Y = {(0, 0, 1): 1} +CUBIC_EXPONENTS = ((3, 0, 0), (2, 1, 0), (1, 2, 0), (0, 3, 0)) + + +def child_prefix(r): + """Execute every retained child, with formal dirty input Y.""" + a, y = dict(A), dict(Y) + for _ in range(r): + y = add(y, cube(a)) + a = add(a, B) + return a, dict(B), y + + +def repair_program(r, d, e): + # Visit e, d, 0 so the last query is already at the restored source. + return [ + ("shear", e - r), ("query", -Fraction(r, 2)), + ("shear", d - e), ("query", -Fraction(r, 2)), + ("shear", -d), ("query", Fraction(r)), + ] + + +def execute(state, program): + a, b, y = state + for op, value in program: + if op == "shear": + a = add(a, b, value) + elif op == "query": + y = add(y, cube(a), value) + else: + raise ValueError("unknown operation") + return a, b, y + + +def expected(r): + return A, B, add(Y, cube(A), r) + + +def pell_terms(count): + r, n = 1, 0 + result = [] + for _ in range(count): + r, n = 2 * r + 3 * n, r + 2 * n + result.append((r, n)) + return result + + +def directions(r, n): + require(r >= 3 and n > 0 and r * r - 3 * n * n == 1, + "outside nondegenerate positive Pell domain") + d, e = Fraction(r - 1 - n, 2), Fraction(r - 1 + n, 2) + require(d.denominator == e.denominator == 1 and 0 < d < e < r, + "nonintegral or collapsed direction") + return int(d), int(e) + + +def cube_vector(u, denominator=1): + # denominator^3 times (A + (u/denominator)B)^3, from multiplication. + poly = cube(add({p: denominator * v for p, v in A.items()}, B, u)) + return tuple(poly.get(p, 0) for p in CUBIC_EXPONENTS) + + +def direct_defect_vectors(limit): + """Build defects by adding each actual child, never power-sum formulas.""" + running = (0, 0, 0, 0) + constant = cube_vector(0) + result = {} + for r in range(1, limit + 1): + term = cube_vector(r - 1) + running = tuple(x + y for x, y in zip(running, term)) + result[r] = tuple(x - r * c for x, c in zip(running, constant)) + return result + + +def grid_check(limit, denominator): + """All 0 <= d < e <= r on the declared fixed-denominator grid.""" + defects = direct_defect_vectors(limit) + tested, accepted = 0, [] + for r in range(3, limit + 1): + vectors = [cube_vector(u, denominator) + for u in range(denominator * r + 1)] + target = tuple(2 * denominator**3 * x for x in defects[r]) + for u, left in enumerate(vectors): + for v in range(u + 1, len(vectors)): + right = vectors[v] + tested += 1 + actual = tuple(r * (x + y - 2 * c) + for x, y, c in zip(left, right, vectors[0])) + if actual == target: + accepted.append((r, Fraction(u, denominator), + Fraction(v, denominator))) + expected_hits = [] + # This membership calculation neither generates nor filters the search. + for r in range(3, limit + 1): + quotient, remainder = divmod(r * r - 1, 3) + n = isqrt(quotient) + if remainder == 0 and n * n == quotient: + expected_hits.append((r, *directions(r, n))) + require(accepted == expected_hits, "grid disagrees with Pell membership") + return tested, len(accepted) + + +def numeric_execution(r, program, initial): + a, b, y = map(Fraction, initial) + for _ in range(r): + y += a**3 + a += b + for op, value in program: + if op == "shear": + a += value * b + else: + y += value * a**3 + aa, bb, yy = map(Fraction, initial) + require((a, b, y) == (aa, bb, yy + r * aa**3), + "dirty numerical restoration failed") + + +def main(): + terms = pell_terms(32) + require(terms[:4] == [(2, 1), (7, 4), (26, 15), (97, 56)], + "Pell recurrence anchors") + descent_steps = 0 + for k, (r, n) in enumerate(terms, 1): + require(r * r - 3 * n * n == 1, "Pell norm") + rr, nn = r, n + for _ in range(k): + old = rr + rr, nn = 2 * rr - 3 * nn, 2 * nn - rr + require(0 < rr < old and nn >= 0, "positive strict descent") + require(rr * rr - 3 * nn * nn == 1, "descent norm") + descent_steps += 1 + require((rr, nn) == (1, 0), "descent terminal") + + polynomial_programs = 0 + for r, n in terms[1:8]: # 7, 26, 97, 362, 1351, 5042, 18817. + d, e = directions(r, n) + program = repair_program(r, d, e) + require(execute(child_prefix(r), program) == expected(r), + "literal polynomial program failed") + polynomial_programs += 1 + + inputs = [(0, 0, 13), (1, 0, -7), (0, 1, 5), (-2, 3, 11), + (3, -2, -17), (Fraction(1, 2), Fraction(-3, 4), Fraction(5, 7)), + (Fraction(-7, 3), Fraction(2, 5), Fraction(-11, 13)), + (19, 23, -29)] + dirty_cases = 0 + for r, n in terms[1:6]: + for initial in inputs: + numeric_execution(r, repair_program(r, *directions(r, n)), initial) + dirty_cases += 1 + + counts = [grid_check(160, 1), grid_check(32, 8)] + + r, n = 7, 4 + valid = repair_program(r, *directions(r, n)) + mutants = [] + for index, delta in ((1, 1), (0, 1)): + changed = list(valid) + op, value = changed[index] + changed[index] = op, value + delta + mutants.append(changed) + changed = list(valid) + changed[1] = "query", -changed[1][1] + mutants.append(changed) + changed = list(valid) + changed[0], changed[1] = changed[1], changed[0] + mutants.append(changed) + mutants.extend([valid[:4] + valid[5:], valid[:-1]]) + for changed in mutants: + require(execute(child_prefix(r), changed) != expected(r), + "bad weight/direction/sign/order/restore/query accepted") + require(execute(child_prefix(r - 1), valid) != expected(r), + "omitted retained child accepted") + require(execute(child_prefix(7), repair_program(7, Fraction(1, 2), + Fraction(11, 2))) != expected(7), + "nonintegral rational non-Pell directions accepted") + require(execute(child_prefix(6), repair_program(6, 1, 4)) != expected(6), + "non-Pell arity accepted") + domain_rejections = 0 + for pair in ((1, 0), (2, 1), (7, 3), (7, -4), (-7, 4)): + try: + directions(*pair) + except ValueError: + domain_rejections += 1 + else: + raise ValueError("invalid Pell domain accepted") + require(domain_rejections == 5, "scope controls incomplete") + + print("PASS_INDEPENDENT_CUBIC_PELL" + f" polynomial_programs={polynomial_programs} dirty_cases={dirty_cases}" + f" grid_pairs={sum(x for x, _ in counts)} grid_hits={sum(y for _, y in counts)}" + f" pell_terms={len(terms)} descent_steps={descent_steps}" + " mutants=9 domain_rejections=5 no_new_kappa") + + +if __name__ == "__main__": + main() diff --git a/research/cubic-pell-family/verify.py b/research/cubic-pell-family/verify.py new file mode 100644 index 0000000000..c9f227aa5a --- /dev/null +++ b/research/cubic-pell-family/verify.py @@ -0,0 +1,168 @@ +#!/usr/bin/env python3 +"""Exact corroboration; the all-arity proof is PROOF.md. + +Prepared by apoursh with substantial OpenAI Codex assistance. Apache-2.0. +No predecessor executable is imported. Checks remain active under -O. +""" +from fractions import Fraction as Q +from hashlib import sha1, sha256 +import json +from math import isqrt +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +BASE = 'e54523517d0f03e58352e647c403a5af3e525a57' + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def rejected(action): + try: + action() + except ValueError: + return + raise ValueError('negative control accepted') + + +def source_bytes(raw, row): + require(sha256(raw).hexdigest() == row['sha256'], 'source SHA256 mismatch') + obj = b'blob ' + str(len(raw)).encode('ascii') + b'\0' + raw + require(sha1(obj).hexdigest() == row['git_blob'], 'source Git blob mismatch') + + +def check_sources(): + manifest = json.loads((PACKAGE / 'SOURCES.json').read_text()) + require(manifest['base_commit'] == BASE, 'wrong source base') + rows = [row for row in manifest['files'] if row['usage'] == 'input'] + expected = { + 'research/cubic-three-query-arities/README.md', + 'research/dyadic-cubic-repair/PROOF.md', + 'research/cubic-pure-b-boundary/PROOF.md', + 'research/cubic-equal-step-classification/PROOF.md', + } + require({row['path'] for row in rows} == expected and len(rows) == 4, + 'wrong predecessor input set') + for row in rows: + raw = (ROOT / row['path']).read_bytes() + source_bytes(raw, row) + rejected(lambda: source_bytes(raw + b'\nMUTATED', row)) + return len(rows) + + +# Sparse Q-polynomials in indeterminates (r,n), used only for four cubic +# coefficients. This checks the universal residual without sampling r,n. +def add(*polynomials): + out = {} + for poly in polynomials: + for monomial, coefficient in poly.items(): + out[monomial] = out.get(monomial, Q(0)) + coefficient + return {m: c for m, c in out.items() if c} + + +def scale(poly, coefficient): + return {m: c * coefficient for m, c in poly.items() if c * coefficient} + + +def mul(left, right): + out = {} + for (i, j), a in left.items(): + for (k, l), b in right.items(): + m = (i + k, j + l) + out[m] = out.get(m, Q(0)) + a * b + return {m: c for m, c in out.items() if c} + + +def symbolic_residual(): + one, r, n = {(0, 0): Q(1)}, {(1, 0): Q(1)}, {(0, 1): Q(1)} + rm1 = add(r, scale(one, -1)) + d = scale(add(rm1, scale(n, -1)), Q(1, 2)) + e = scale(add(rm1, n), Q(1, 2)) + s1 = scale(mul(r, rm1), Q(1, 2)) + target = [{}, scale(s1, 3), + mul(s1, add(scale(r, 2), scale(one, -1))), mul(s1, s1)] + represented = [add(scale(r, -1), scale(r, Q(1, 2)), scale(r, Q(1, 2))), + scale(mul(r, add(d, e)), Q(3, 2)), + scale(mul(r, add(mul(d, d), mul(e, e))), Q(3, 2)), + scale(mul(r, add(mul(mul(d, d), d), mul(mul(e, e), e))), Q(1, 2))] + pell = add(mul(r, r), scale(mul(n, n), -3), scale(one, -1)) + expected = [{}, {}, scale(mul(r, pell), Q(-1, 4)), + scale(mul(mul(r, rm1), pell), Q(-1, 8))] + residual = [add(a, scale(b, -1)) for a, b in zip(represented, target)] + require(residual == expected, 'universal off-Pell residual identity') + require(any(residual), 'residual incorrectly assumed identically zero') + + +def directions(r, n): + require(type(r) is int and type(n) is int and r >= 3 and n > 0, + 'nondegenerate positive integer domain') + require(r * r - 3 * n * n == 1, 'not a Pell solution') + require((r - 1 - n) % 2 == 0, 'nonintegral direction') + d, e = (r - 1 - n) // 2, (r - 1 + n) // 2 + require(0 < d < e < r, 'source direction order') + return d, e + + +def moments(r, nodes, weights): + require(len(nodes) == len(weights) == 3 and len(set(nodes)) == 3, + 'three distinct nodes required') + require(all(w and w.denominator & (w.denominator - 1) == 0 for w in weights), + 'nonzero dyadic query weights required') + s1 = Q(r * (r - 1), 2) + expected = [Q(0), s1, s1 * Q(2 * r - 1, 3), s1 * s1] + actual = [sum((w * Q(c) ** k for c, w in zip(nodes, weights)), Q(0)) + for k in range(4)] + require(actual == expected, 'cubic coefficient mismatch') + + +def main(): + inputs = check_sources() + symbolic_residual() + r, n = 1, 0 + novel = 0 + for k in range(1, 97): + r, n = 2 * r + 3 * n, r + 2 * n + require(r * r - 3 * n * n == 1, 'recurrence norm') + if k == 1: + require((r, n) == (2, 1), 'degenerate initial term') + rejected(lambda: directions(r, n)) + continue + d, e = directions(r, n) + moments(r, [0, d, e], [Q(-r), Q(r, 2), Q(r, 2)]) + previous = (2 * r - 3 * n, 2 * n - r) + require(1 <= previous[0] < r and 0 <= previous[1] < n, + 'Pell descent did not decrease') + require(previous[0] ** 2 - 3 * previous[1] ** 2 == 1, 'descent norm') + if k % 2 == 0 and (k // 2) % 3: + require(r % 9 == 7 and r % 2 == 1, 'new-class congruences') + require(r & (r - 1) != 0, 'unexpected power of two') + require((r - 1) & (r - 2) != 0, 'unexpected power of two plus one') + novel += 1 + # Membership screening uses integer square roots, not recurrence. + members = [] + for arity in range(3, 10001): + square, rem = divmod(arity * arity - 1, 3) + root = isqrt(square) + if rem == 0 and root * root == square: + d, e = directions(arity, root) + moments(arity, [0, d, e], [Q(-arity), Q(arity, 2), Q(arity, 2)]) + members.append(arity) + require(members == [7, 26, 97, 362, 1351, 5042], 'bounded arity membership') + for r, n in [(1, 0), (2, 1), (7, -4), (7, 5), (15, 8), (Q(7), 4)]: + rejected(lambda r=r, n=n: directions(r, n)) + rejected(lambda: moments(7, [0, 1, 5], [Q(-7), Q(7, 2), Q(9, 2)])) + rejected(lambda: moments(7, [0, 2, 5], [Q(-7), Q(7, 2), Q(7, 2)])) + rejected(lambda: moments(7, [0, 1, 5], [Q(7), Q(-7, 2), Q(-7, 2)])) + rejected(lambda: moments(7, [0, 1, 5], [Q(-7), Q(7, 3), Q(7, 2)])) + rejected(lambda: moments(7, [0, 1, 1], [Q(-7), Q(7, 2), Q(7, 2)])) + print('PASS_CUBIC_PELL sources=' + str(inputs) + + ' symbolic_coefficients=4 pell_terms=96 nondegenerate_terms=95' + + ' novel_class_terms=' + str(novel) + + ' arity_screen=9998 hits=6 source_mutants=4 algebra_domain_controls=12 no_new_kappa') + + +if __name__ == '__main__': + main()