diff --git a/research/hidden-window-optima/PROOF.md b/research/hidden-window-optima/PROOF.md new file mode 100644 index 0000000000..ebe4424175 --- /dev/null +++ b/research/hidden-window-optima/PROOF.md @@ -0,0 +1,200 @@ +# Exact minimum width at every normalized budget + +Research draft, 2026-10-29. Substantial OpenAI Codex assistance. +Apache-2.0. This is a proposed mathematical proof, not a formal certification. + +## Scope and inherited reduction + +Fix integers h,N >= 1. Let A_j,B_j be nonnegative integers for +0 <= j <= 2h+2, with sum A_j <= N and sum B_j <= N. Put +F(p) = sum_j (B_j-A_j) 2^(jp). Require zeros of multiplicity at least h +at p=0,1, two distinct interior zeros alpha0 between them. +The quantity to minimize is w=beta-alpha. N is the budget **per profile**, +including common paid padding, not the combined count of the two profiles. + +Karnaugh33's PR6139 supplies the following reduction, which we also explain +so its applicability is explicit. Set x=2^p. Nonzero Q(x)=F(log_2 x) has +degree at most 2h+2; its required roots already account for that degree. +Division by the monic integer endpoint factors gives + + Q(x)=(-1)^(h+1)(x-1)^h(x-2)^h R(x), + R(x)=a*x^2-z*x+c, a,z,c positive integers, + 10. + +Every root of Q is positive, so its coefficients alternate strictly. Q(1)=0 +makes its positive and negative coefficient sums equal. Each equals + + W=|Q(-1)|/2 = S*(a+z+c), S=6^h/2. + +These are the counts after cancelling common calls; every realization adds +the same nonnegative integer padding vector H to both coefficient parts. +It is allowed precisely when sum H <= N-W. Conversely every quadratic with +the displayed root conditions yields such profiles with the required signs. +Thus, with L=floor(N/S), feasible residuals are exactly + + a,z,c positive integers; D=a+z+c <= L; + 2a0; 4a-2z+c>0; Delta=z^2-4ac>0. (A) + +The strict vertex, endpoint and discriminant conditions in (A) are necessary +and sufficient for two distinct roots in (1,2). Width increases strictly with + + Delta/z^2, w=log_2((z+sqrt(Delta))/(z-sqrt(Delta))). (B) + +In particular, k=R(1)=a+c-z is a positive integer, D=2z+k and +z <= Z=floor((L-1)/2). These facts, the discriminant bound and the family +below are inherited from PR6139. PR6153 classifies equality in its lower bound +log_2((Z+1)/(Z-1)); it leaves the actual optimum at other budgets open. + +## Theorem + +1. If L<31, there is no eligible profile pair. +2. If 31<=L<=34, the unique oriented residual is (a,z,c)=(5,15,11). + Its discriminant is 5 and the minimum width is + log_2((15+sqrt(5))/(15-sqrt(5))). +3. For every L>=35, **every** width-minimizing residual has Delta=1. + Let z_star be the largest odd z for which some positive integers a,c obey + + 4ac=z^2-1, a+z+c<=L, 2a4*k*ell. Necessity follows from +positive endpoint values, and from the positive sum and product of the two +positive y roots. Sufficiency follows from the same sum/product conditions +and the strictly positive discriminant. The inverse integer map is + + a=k+v+ell, z=4k+3v+2ell, c=4k+2v+ell, + D=a+z+c=9k+6v+4ell. + +Since k,ell>=1, the discriminant condition forces v>=3. Hence D>=31, +with equality only at (k,v,ell)=(1,3,1). Any different positive integer +triple satisfying these lower bounds increases D by at least four. Thus +there are no eligible residuals below 31, and (a,z,c)=(5,15,11) is the +only one through 34. It has Delta=5 and both roots strictly in (1,2). +This proves both small-budget statements without a computational assumption. +The polynomial itself already appears as a semantic control in PR6153's +verifier; its existence is predecessor evidence, not a new discovery here. +The new statement is the exact infeasibility/uniqueness threshold. + +The literal coefficient and endpoint-coordinate censuses independently +corroborate this argument. The exception prevents extending the rational-root +optimizer conclusion to every feasible budget. + +## Why discriminant one always wins above the threshold + +For L>=35 choose n=floor(sqrt((L+1)/4)), equivalently the largest integer n +with 4n^2-1<=L. Then n>=3. The PR6139 family + + (a_0,z_0,c_0)=(n(n-1), 2n^2-1, n(n+1)) + +has D_0=4n^2-1<=L, Delta_0=1 and roots (n+1)/n, n/(n-1) in (1,2). +Maximality of n implies L<=4(n+1)^2-2 and hence + + Z <= 2n^2+4n, + 2z_0-Z >= 2n^2-4n-2 > 0 (n>=3). (D) + +An integer quadratic discriminant is 0 or 1 modulo 4. Consequently any +positive discriminant different from one is at least four. Every such +eligible quadratic satisfies + + Delta/z^2 >= 4/Z^2 > 1/z_0^2. + +The last inequality is strict by (D). The available family member therefore +has strictly smaller width by (B). No Delta>1 residual can minimize width, +including scaled rational-root residuals and irrational-root residuals. +This domination is a proof for all budgets, not an extrapolation of a census. + +## Exact search, complete optimizers and certificates + +For Delta=1, z must be odd. The roots are (z-1)/(2a) and (z+1)/(2a), +so the strict root conditions are exactly the last two inequalities in (C). +For a fixed z, write t=(z-1)/2. Then ac=t(t+1), and (C) is equivalent to + + a divides t(t+1), + (t+1)/2 < a < t, + c=t(t+1)/a, a+(2t+1)+c<=L. (E) + +This gives a direct divisor verifier. Search odd z from the largest odd +integer <=Z down to z_0 inclusive. The first nonempty list in (E) supplies +z_star and every minimizer. Existence at z_0 proves termination. Earlier +odd z must all have empty lists; lower z give strictly larger width, and the +dominance lemma already excludes every other discriminant. + +A second exact representation is useful for efficient construction. For +1<=k<=L-2z, set + + U=2zk+k^2+1. + +The identity (c-a)^2=(a+c)^2-4ac shows that a candidate exists precisely when +u=isqrt(U) obeys u^2=U, z+k-u is even, and + + a=(z+k-u)/2, c=(z+k+u)/2 + +satisfy the strict conditions (C). Here c>a follows from rs>1. Conversely +these tests imply Delta=1 and D=2z+k<=L. Iterating k returns all residuals +for the chosen z without any factorization assumption. The constructor uses +this square test; the certificate verifier independently uses (E). + +The number of tested odd z is O(sqrt(L)), because Z-z_0<=4n+1. The maximum +k is at most L-2z_0<=8n+4. Thus the constructor makes O(L) exact square +tests; this is an arithmetic-operation bound, not a bit-complexity claim. +The simple divisor verifier is slower and is deliberately a separate route. + +The finite oracle also minimizes all discriminants: for a fixed z,a in (A), +Delta/z^2 strictly decreases as c increases. Therefore only the largest +allowed c need be tested to recover every minimizing residual at a budget. +This justifies the independently organized quadratic-size oracle in verify.py. +It does not assume the discriminant-one theorem. + +## What changes relative to predecessors + +PR6139 proves the normalization, width bound, comparison statistic, feasible +seed family, and one exact budget census. Nick Petalas's PR6153 proves the +complete equality-budget classification. This draft adds the strict domination +of all Delta>1 residuals for every L>=35, the complete small-budget exception, +and the exact optimization/certificate procedure for every remaining budget. +It does not supersede or claim authorship of their results. + +The base construction belongs to zxv's PR6049, with Nick Petalas's PR5174 and +Ali Romman's rank-budget lineage. Integer discriminants, the quadratic formula, +divisor enumeration and monotonicity are classical. No global novelty claim. + +## Limits and review + +The exact minimal power-of-two alphabet and endpoint multiplicities are essential. +PR6139 already gives a larger-support counterexample to a broader inverse-budget +claim. Nothing here covers arbitrary alphabets, actual supplier realization, +independent targets, native operators, dirty restoration, compiler admission, +stock, precision/tape, or analytic recovery. No new kappa or multiplication +algorithm follows. The selected result and all five assumptions remain unchanged. + +Finite exact checks corroborate the proof; neither human mathematical review +nor proof-assistant verification has occurred. Both predecessor PRs are recorded +as partially reviewed in the current repository ledger. The author checks have been supplemented by separate AI proof/code and +adversarial reviews, including differently organized exact censuses. These +reviews can still share reasoning errors and do not constitute human or formal +acceptance. The next useful task is independent human or proof-kernel review +of (D), the strict root endpoints and certificate soundness. diff --git a/research/hidden-window-optima/README.md b/research/hidden-window-optima/README.md new file mode 100644 index 0000000000..4cf52f81a3 --- /dev/null +++ b/research/hidden-window-optima/README.md @@ -0,0 +1,157 @@ +# Exact optima for fixed-budget hidden windows + +Claim type: proposed scoped mathematical proof with exact finite corroboration. +Prepared for human review; no new kappa. + +This follows Karnaugh33's [PR6139](https://github.com/CrocSwap/integer-mult-bounds/pull/6139) +and Nick Petalas's [PR6153](https://github.com/CrocSwap/integer-mult-bounds/pull/6153). +PR6153 already classifies all budgets attaining the earlier lower bound. Its +remaining question is the actual minimum width at every other budget. + +The proposed proof here reduces that optimization to discriminant one, with +one completely classified small-budget exception, proved algebraically in +endpoint coordinates. The reference implementation +returns all minimizing residuals and a finite certificate checked by a separate +divisor formulation. No new multiplication algorithm or kappa is claimed. + +## Exact claim + +Use the same minimal rank alphabet 2^j, 0<=j<=2h+2, integer call counts, +h-fold endpoint zeros, two distinct interior roots and positive window as in +PR6139. The call budget N is **per profile**, including common paid padding. +Set S=6^h/2 and L=floor(N/S). Then: + +- L<31: no eligible profile pair exists. +- 31<=L<=34: the only oriented residual is 5x^2-15x+11, with discriminant 5. +- L>=35: every minimum-width residual has discriminant 1. Maximize its trace z + over the exact integer search in [PROOF.md](PROOF.md); the minimum width is + log_2((z+1)/(z-1)). All ties and permitted common padding are included. + +The proof supplies a feasible discriminant-one seed whose width is strictly +less than every residual with discriminant at least four. Integer discriminants +cannot equal two or three. This proves the reduction for every budget, rather +than inferring it from a search. The remaining search uses square tests in +(z,k), with k=R(1); certificate verification uses divisors of t(t+1). + +This is an exact finite algorithm and an all-budget theorem under the stated +hypotheses. It is not an elementary closed formula for the maximizing trace. + +## Examples + +The table uses h=1, hence S=3. Counts are per side before common padding. + +| N | L | All optimal residuals (a,z,c), meaning ax^2-zx+c | Calls per side | +|---:|---:|---|---| +| 92 | 30 | none | — | +| 93 | 31 | (5,15,11), discriminant 5 | 93 | +| 111 | 37 | (6,17,12) | 105 | +| 120 | 40 | (6,19,15) | 120 | +| 432 | 144 | (28,71,45), (30,71,42) | 432, 429 | +| 1000 | 333 | (60,161,108), (72,161,90) | 987, 969 | +| 3000 | 1000 | (205,491,294), (210,491,287) | 2970, 2964 | + +The (5,15,11) polynomial already appears in PR6153's verifier; the new claim +is its complete small-budget uniqueness threshold. The N=1000 result exactly +reproduces PR6139's census. The L=144 tie is also +in PR6153. They are regression checks, not new claims. Intermediate and larger +cases illustrate the general procedure; the uniform claim rests on the proof. + +## Reproduce locally + +Python 3.10+ standard library only; tested here with CPython 3.14.7. +From this package directory: + +```sh +python3 -I -W error -B verify.py +python3 -I -W error -O -B verify.py +python3 -I -W error -B independent_check.py --package . +python3 -I -W error -O -B independent_check.py --package . +python3 -I -W error -B endpoint_coordinate_check.py +python3 -I -W error -O -B endpoint_coordinate_check.py +python3 -I -W error -B optimum.py --budget 1000 --h 1 +python3 -I -W error -B optimum.py --normalized-budget 100000 +``` + +Expected suite marker: `PASS_EXACT_HIDDEN_WINDOW_OPTIMA`. The initial full +normal replay took about two seconds on the author host; time is host-dependent. +Commands write JSON to stdout only. They do not use network, subprocesses, +repository executables or optional dependencies. Checks use explicit exceptions +and remain active under optimization. The suite compiles the adjacent `optimum.py` source bytes directly and hashes +those same bytes in its receipt; adjacent bytecode caches cannot replace them. +Isolated Python mode works. + +The repository package runner accepts the metadata and six pinned provenance +files with `--check-only`. VERIFY.json registers all six checker commands for +its required Python 3.12 environment. That managed replay was not run locally: +Python 3.12 was unavailable; direct replays used CPython 3.14.7. The metadata +pass is not a mathematical acceptance check. + +The reference API accepts 0<=L<=100000, or 1<=h<=16 and a positive N with +floor(N/(6^h/2))<=100000. It rejects booleans, wrong types and values outside +those bounds. The mathematical proof has no such caps. The constructor makes +O(L) exact square tests; no bit-complexity or runtime improvement claim is made. + +## Verification coverage + +- Literal positive-coefficient enumeration checks **10,586,800 triples** through + L=400, including every discriminant, and all **401** budget prefixes. It finds + 14,498 eligible residuals and the unique exception below 35. +- A separately organized divisor census checks all **4,062** budgets 35..4096, + finds 1,867 discriminant-one residuals, and verifies every certificate and tie. + It makes 260,610 divisor trials. The dominance proof is still required to + exclude other discriminants outside the full-triple census. +- An all-discriminant largest-c oracle checks 13 specified budgets through + L=8192, totaling **2,815,810** (a,z) pairs. Its completeness argument is written + in PROOF.md and its small cases agree with the literal census. +- 78 signed profiles check exact counts, rank mass, endpoint multiplicities and + signs; 156 common-padding/scaling cases check h=1..6 and budget remainders. +- 21 invalid-input/certificate controls, two excluded-root-boundary fixtures, + a seed-only counterexample, four larger reference cases through L=100000, + and 2,002 seed-interval/large-integer fixtures pass. +- Separate reviewer checks add a signed-quartic/Sturm census of 13,590,150 + trials through h=1,N=150; a Farey-root census through L=4096; 741 malformed + certificates; and an endpoint-coordinate census of 98,182 triples through + L=512. See REVIEW.md for independence and coverage limits. + +Normal and optimized outputs should agree after excluding elapsed time. The +stdout receipt hashes this package's Python, Markdown and JSON files. +SOURCES.json binds predecessor and guidance files to exact Git blob IDs and +SHA256 hashes at the recorded base commit; these are provenance, not runtime imports. + +## Credit, review status and limits + +[SOURCES.json](SOURCES.json) pins current main +`a5bff3bf133e482541c09eba4e773884bdb2b1b7` and the exact predecessor heads. +Both PR6139 and PR6153 are merged but listed as **partially reviewed** in the +current ledger. Their scientific status is not promoted by this draft. + +Karnaugh33 supplies the normalization, width bound, comparison statistic and +seed family. Nick Petalas supplies the complete bound-attainment classification. +zxv's PR6049 supplies the minimal-support framework, retaining Nick Petalas's +PR5174 and Ali Romman's rank-budget lineage. The quadratic and divisor identities +are classical. No global literature-priority claim is made. + +This proof, code and checks were produced with substantial OpenAI Codex +assistance, using GPT-6 Astra Ultra authoring and separate AI reviewers. +Separate AI reviewers challenged the proof, reran normal/optimized checks and +added independent signed-polynomial/Sturm, Farey-root and endpoint-coordinate +censuses. One source-loading weakness was corrected in this package; original +research evidence was preserved. See REVIEW.md for coverage and limits. +Human mathematical review and proof-assistant checking remain outstanding. + +The alphabet and zero-pattern restrictions are essential. No arbitrary-rank or +larger-support result, legal native supplier, independent targets, restoration, +compiler, stock, precision/tape or analytic recovery is established. The five +framework assumptions and selected kappa 781451/250000000 remain unchanged. +Selected scientific replay, predecessor executables, Lean, Docker and hosted +CI were not run. No existing package or selected record was edited. + +## Open next questions + +First independently review the discriminant-domination inequality and exact +search completeness. A useful later formalization would prove the finite +integer certificate checker sound under the polynomial reduction. Its blocker +is a proof-kernel development, not a larger search. No additional construction +or arbitrary-alphabet campaign is reserved or justified by this side result. + +Apache-2.0; retain predecessor attribution. diff --git a/research/hidden-window-optima/REVIEW.md b/research/hidden-window-optima/REVIEW.md new file mode 100644 index 0000000000..cc68f7c810 --- /dev/null +++ b/research/hidden-window-optima/REVIEW.md @@ -0,0 +1,91 @@ +# Independent AI review and reproducibility scope + +Two separate GPT-6 Astra Ultra reviewers examined the proposed theorem and +code on 2026-10-29. They did not write the original proof or solver. A third +reviewer checked upstream overlap and attribution. This is independent AI +review, not independent human review or formal mathematical acceptance. + +## Findings and correction + +Neither mathematical reviewer found a defect in the stated minimal-alphabet +theorem, its strict discriminant domination, all-profile reduction, common +padding, optimizer ties or exact-search completeness. + +The proof/code reviewer found one conditional source-integrity weakness: +Python's `-B` disables bytecode writes but can still load a matching cached +`.pyc`. The original `verify.py` imported `optimum.py` with SourceFileLoader, +then hashed source text. In a scratch copy, an inert cached marker executed +instead of the source marker despite `-B`. The original package had no such +cache, and the recorded scientific replays were not affected. + +The prepared package corrects this by capturing `optimum.py` bytes, compiling +those exact bytes with `dont_inherit=True`, and hashing those same bytes in the +receipt. Both independent checker scripts use that approach too. This binds +the executed subject module to the receipt; it does not make the filesystem +an atomic snapshot or formally certify Python execution. + +The adversarial reviewer supplied the endpoint-coordinate proof now included +in PROOF.md: D=9k+6v+4ell with k,ell>=1 and v>=3. It proves the threshold 31 +and uniqueness through 34 algebraically, removing the finite base-case table +from the theorem's logical dependencies. The polynomial (5,15,11) itself was +already a semantic control in PR6153; its prior existence is credited. + +## Independent domains + +`independent_check.py` starts from all bounded signed quartics with Q(1)=Q(2)=0, +before assuming alternating signs or using the author's quadratic eligibility +predicate. Exact polynomial division and a generic rational Sturm sequence +test the interior-root condition. At h=1 and per-profile N<=150 it checks +13,590,150 coefficient triples, 323,071 bounded endpoint polynomials, ten +eligible polynomials and all 151 budget prefixes. + +Its separate Farey-neighbor root census compares the exact ratio of rational +roots rather than the author's discriminant score, square test or divisor +routine. It covers all 1,867 discriminant-one residuals through L=4096 and +all 4,062 budgets 35..4096, including 1,211 budgets with multiple optima. +Primitive rational linear factors have determinant one when the quadratic +discriminant is one; this supplies the census parametrization. The written +domination lemma is still required to exclude other discriminants beyond +the signed-quartic census. It also rejects 741 malformed certificates, checks +ten valid controls and six endpoint/repeated-root/rational/irrational fixtures. + +`endpoint_coordinate_check.py` independently uses the increasing change of +variable y=(x-1)/(2-x) and positive-root conditions in y. Its weighted-cost +census through L=512 checks 98,182 positive coordinate triples, 31,238 eligible +residuals, all 513 budget prefixes, and all tie lists, with four excluded +boundary/sign controls. It imports neither the author's eligibility predicate +nor its certificate verifier. It calls the solver only to compare answers. + +Both scripts are standard-library-only, bounded, stdout-only and reproducible +from the package. Their default domains are registered in VERIFY.json in +normal and optimized modes. Acceptance checks remain active under `-O`. + +## Overlap and attribution + +PR6153's [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19246930) +expressly excludes the general finite-budget optimum. Its +[completion handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19247488) +releases that scope and leaves the exact optimum outside its attainment set open. +This package supplies the discriminant domination and all-budget optimization +procedure; it does not claim PR6139's bound or PR6153's equality classification. + +The bounded upstream audit inspected current main, topical all-state PR searches, +Discussion6052, the latest 150 handoff comments and latest 30 mechanism comments. +It found no competing same-instance result or later matching active claim in +those inspected records. Uninspected older comments and the broader literature +remain outside that coverage; no absolute novelty claim is made. + +## Remaining obligations + +Finite corroboration and separate AI reviews do not prove the uniform theorem +in a formal kernel. The same model family and shared predecessor mathematics +can produce common errors. Human review should focus on the all-profile +reduction, strict domination inequality and exact-search completeness. + +The reference implementation's finite caps are separate from the uniform +mathematical statement. No arbitrary-rank, larger-support, physical-supplier, +native, compiler, restoration, stock, precision/tape or analytic-recovery +obligation is discharged. No selected cold replay or new kappa is claimed. + +Substantial OpenAI Codex assistance throughout. Apache-2.0. Predecessor and +classical attribution is retained in PROOF.md and SOURCES.json. diff --git a/research/hidden-window-optima/SOURCES.json b/research/hidden-window-optima/SOURCES.json new file mode 100644 index 0000000000..b2c35699d4 --- /dev/null +++ b/research/hidden-window-optima/SOURCES.json @@ -0,0 +1,76 @@ +{ + "schema_version": 1, + "base_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7", + "files": [ + { + "path": "certificates/selected-result.json", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa", + "usage": "provenance" + }, + { + "path": "research/fixed-budget-hidden-windows/PROOF.md", + "git_blob": "f6b886f3cefae035ff2d3c04016f346ee8d4459e", + "sha256": "d95c150f21c38abfb46bd3a8279dd6ebdcb821e2f77268e93325923c80fc3920", + "usage": "provenance" + }, + { + "path": "research/hidden-window-attainment-budgets/README.md", + "git_blob": "169f72b5dc5d1b936c66f5040bcbee6cf98402eb", + "sha256": "039d4c207cf9f7d43b0bc800b0426e20450f7a8ad27edff57fef1735aae6a06d", + "usage": "provenance" + }, + { + "path": "research/hidden-window-attainment-budgets/PROOF.md", + "git_blob": "f4667317d75fcacd6b7dd4993abd5f7136239f3d", + "sha256": "37e34290a8209303c857facffd3c942e81e6718101d387d6a8dc3e7b4244dbca", + "usage": "provenance" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/hidden-window-attainment-budgets/verify.py", + "usage": "provenance", + "git_blob": "05ad035122ffd021c53865b9a78e3ec0c6b12575", + "sha256": "759498fa0dbad8145b929a73385d7019dc6842180cbf76f91ee8e7b23e0fb6e0" + } + ], + "predecessors": [ + { + "pr": 6139, + "author": "Karnaugh33", + "head": "3b9de03623e8bf05af49f9f9c5fc7a426cbde9e5", + "merge_commit": "c62bc64ea5e349d6d527415be15106f9b2f7631c", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/6139", + "ledger_status": "partially reviewed", + "used_for": "Normalization, discriminant comparison, feasible seed family, exact N=1000 reference census" + }, + { + "pr": 6153, + "author": "Nick Petalas (petalas)", + "head": "0ef36537f64f6d11e7574268266ef7aeffc4df1e", + "merge_commit": "4f46cbba931456a3b88be68a7cdf3de7eb842144", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/6153", + "ledger_status": "partially reviewed", + "used_for": "Completed attainment classification; explicit open question on actual optimum at all other budgets" + }, + { + "pr": 6049, + "author": "zxv", + "head": "2646b6d67ceb74b9868e632f3a27312d8be62a0e", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/6049", + "used_for": "Minimal-support hidden-window framework; retained PR5174 and Ali Romman lineage" + } + ], + "selected_result": { + "kappa_rational": "781451/250000000", + "kappa_decimal": "0.003125804", + "assumptions_unchanged": 5, + "replay_not_run": "make frontier6030-verify" + }, + "credit": "Karnaugh33, with substantial OpenAI Codex assistance and separate independent AI review; predecessor and classical identities retain attribution." +} diff --git a/research/hidden-window-optima/TASK.json b/research/hidden-window-optima/TASK.json new file mode 100644 index 0000000000..d7dcbca996 --- /dev/null +++ b/research/hidden-window-optima/TASK.json @@ -0,0 +1,99 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 8, + "base_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7", + "original_card": { + "id": "independent-moment", + "question": "Does a changed construction's serialized target/paid invoice independently support its claimed improvement?", + "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", + "docs/research/recursive-invoice-preflight.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": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "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": "Independently recount one changed emitted word and its complete caller, importing no constructor or pricing engine. Include target losses, owned lifetimes, native orientation and extra charges. Check existing #5633/#5708/#5717/#5719 coverage to avoid duplicate audits and preserve its exact head. Stop after the chosen missing implication; a correct root alone is not supplier admission.", + "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": [ + "invoice", + "signed moment", + "productive target", + "independent recount" + ], + "existing_checks": [ + { + "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.", + "evidence": "research/staged-fourth-mixture-ceiling/README.md", + "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.", + "status": "author-checked", + "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.", + "evidence": "research/r437-two-window-carrier/README.md", + "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.", + "status": "author-checked", + "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e", + "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": "Determine the exact minimum hidden-window width at every normalized budget in the minimal power-of-two alphabet model, with complete optimizers and an exact certificate procedure.", + "scope_change_reason": "Explicit user-directed follow-up to PR6153's open next question, rather than a random assignment or a new physical invoice recount. The original catalogue card is retained as provenance; this is a scoped arithmetic optimization theorem.", + "bottleneck_link": "Exact fixed-budget signed-power comparisons in the PR6049/6139/6153 lineage; no physical realization or selected supplier improvement.", + "budget_minutes": 60, + "stop_rule": "Stop at a reviewed scoped proof and bounded exact verification; no larger alphabet or native supplier search.", + "outcome": "completed", + "evidence": "PROOF.md, exact optimizer, independent finite checks and normal/optimized replay; human and formal validation remain open.", + "author": "Karnaugh33", + "ai_assistance": "Substantial OpenAI Codex assistance, including GPT-6 Astra Ultra authoring and separate independent AI proof/code and adversarial reviews. No human or proof-kernel acceptance claimed.", + "open_questions": [ + { + "question": "Can the discriminant domination and exact certificate checker soundness be formalized under the minimal-alphabet hypotheses?", + "why_it_matters": "The uniform conclusion currently rests on a written proof; finite checks and independent AI review do not replace kernel verification.", + "first_step": "Formalize the strict integer inequality 2*z0>Z and the equivalence between eligible quadratics and the certificate search.", + "blocked_by": "No proof-kernel development or independent human mathematical review is supplied." + } + ] +} diff --git a/research/hidden-window-optima/VERIFY.json b/research/hidden-window-optima/VERIFY.json new file mode 100644 index 0000000000..8a749f9362 --- /dev/null +++ b/research/hidden-window-optima/VERIFY.json @@ -0,0 +1,88 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Author exact optimizer, full coefficient/divisor/largest-c oracles, profiles, padding and controls under normal Python" + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Author exact optimizer, full coefficient/divisor/largest-c oracles, profiles, padding and controls under optimized Python" + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/independent_check.py", + "--package", + "{package}" + ], + "timeout_seconds": 120, + "checks": "Separate reviewer signed-quartic/Sturm, Farey-root and malformed-certificate checks under normal Python" + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/independent_check.py", + "--package", + "{package}" + ], + "timeout_seconds": 120, + "checks": "Separate reviewer signed-quartic/Sturm, Farey-root and malformed-certificate checks under optimized Python" + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/endpoint_coordinate_check.py" + ], + "timeout_seconds": 120, + "checks": "Separate adversarial reviewer endpoint-coordinate census, thresholds, boundaries and complete ties under normal Python" + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/endpoint_coordinate_check.py" + ], + "timeout_seconds": 120, + "checks": "Separate adversarial reviewer endpoint-coordinate census, thresholds, boundaries and complete ties under optimized Python" + } + ] +} diff --git a/research/hidden-window-optima/endpoint_coordinate_check.py b/research/hidden-window-optima/endpoint_coordinate_check.py new file mode 100644 index 0000000000..5f60b79bad --- /dev/null +++ b/research/hidden-window-optima/endpoint_coordinate_check.py @@ -0,0 +1,117 @@ +#!/usr/bin/env python3 +"""Independent adversarial review, stdlib only; reads reviewed author code. + +Apache-2.0. Substantial OpenAI Codex assistance from separate AI review. +Independent exact enumeration in endpoint/Mobius coordinates. No imports of +author predicates, certificate verifier, or existing verification suite. +All checks are explicit and remain enabled under python -O. +The optimizer is compiled from the exact source bytes recorded in the receipt; +no Python bytecode cache is loaded. +""" + +import argparse +import hashlib +import json +import platform +from pathlib import Path + + +CAP = 512 + + +def check(condition, message): + if not condition: + raise RuntimeError(message) + + +def candidates(cap): + """All strict interior-root residuals via positive roots on y>0. + + x=(1+2y)/(1+y), and (1+y)^2 R(x)=ell*y^2-v*y+k. + Its two roots are distinct and positive iff k,ell,v>0 and v^2>4*k*ell. + D=9*k+6*v+4*ell. No a,z vertex or endpoint predicate is imported. + """ + trials = 0 + buckets = [[] for _ in range(cap + 1)] + for k in range(1, cap // 9 + 1): + for ell in range(1, (cap - 9 * k) // 4 + 1): + for v in range(1, (cap - 9 * k - 4 * ell) // 6 + 1): + trials += 1 + delta = v * v - 4 * k * ell + if delta <= 0: + continue + a = k + v + ell + z = 4 * k + 3 * v + 2 * ell + c = 4 * k + 2 * v + ell + D = 9 * k + 6 * v + 4 * ell + check(a + z + c == D, "budget identity") + check(z * z - 4 * a * c == delta, "discriminant identity") + check((a - z + c, -4 * a + 3 * z - 2 * c, + 4 * a - 2 * z + c) == (k, v, ell), "inverse map") + buckets[D].append((delta, z * z, [a, z, c], [k, v, ell])) + return trials, buckets + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--author-package", type=Path, default=Path(__file__).resolve().parent, + help="directory containing the reviewed optimum.py; defaults to this directory") + author = parser.parse_args().author_package + captured = {name: (author / name).read_bytes() for name in + ("PROOF.md", "optimum.py", "verify.py", "README.md", "SOURCES.json")} + namespace = {"__name__": "reviewed_optimum", "__file__": str(author / "optimum.py")} + exec(compile(captured["optimum.py"], str(author / "optimum.py"), "exec", + dont_inherit=True), namespace) + solve_normalized = namespace["solve_normalized"] + trials, buckets = candidates(CAP) + num = den = None + winners = [] + eligible = 0 + budgets_with_ties = 0 + selected = {} + for L, rows in enumerate(buckets): + eligible += len(rows) + for d, zz, row, coordinates in rows: + if num is None or d * den < num * zz: + num, den, winners = d, zz, [row] + elif d * den == num * zz: + winners.append(row) + result = solve_normalized(L) + if not winners: + check(result["status"] == "infeasible" and result["residuals"] == [], + "feasibility mismatch at L=" + str(L)) + else: + score = result["score"] + check(result["status"] == "optimal", "status mismatch at L=" + str(L)) + check(score[0] * den == num * score[1], "score mismatch at L=" + str(L)) + check(result["residuals"] == sorted(winners), "complete winners mismatch at L=" + str(L)) + budgets_with_ties += len(winners) > 1 + if L in (30, 31, 34, 35, 39, 40, 62, 63, 98, 99, 142, 143, 144, 333, 512): + selected[L] = result + small = [row for rows in buckets[:35] for _, _, row, _ in rows] + check(small == [[5, 15, 11]], "small-budget exception mismatch") + # Deliberately excluded endpoints and coincident roots, expressed without + # using the author's a,z predicates. Each vanishing condition removes a + # required positive finite y root or makes the two roots coincide. + excluded = {"x=1": [0, 3, 1], "x=2": [1, 3, 0], + "repeated root": [1, 2, 1], "negative y roots": [1, -3, 1]} + for label, (k, v, ell) in excluded.items(): + check(not (k > 0 and ell > 0 and v > 0 and v * v > 4 * k * ell), label) + report = { + "marker": "PASS_ENDPOINT_COORDINATE_ATTACK", + "python": platform.python_version(), "max_L": CAP, + "budgets_compared": CAP + 1, "positive_coordinate_triples": trials, + "eligible_residuals": eligible, "budgets_with_multiple_optima": budgets_with_ties, + "small_budget_residuals": small, "excluded_boundary_controls": excluded, + "selected_budget_results": selected, + "counterexamples": [], + "scope": "Bounded exact corroboration with alternate coordinates; not formal proof verification.", + "input_sha256": {name: hashlib.sha256(data).hexdigest() for name, data in captured.items()}, + "source_loading": "compile captured optimum.py bytes with dont_inherit=True; no bytecode cache", + "review_script_sha256": hashlib.sha256(Path(__file__).read_bytes()).hexdigest(), + } + print(json.dumps(report, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/hidden-window-optima/independent_check.py b/research/hidden-window-optima/independent_check.py new file mode 100644 index 0000000000..e1afe1e451 --- /dev/null +++ b/research/hidden-window-optima/independent_check.py @@ -0,0 +1,321 @@ +#!/usr/bin/env python3 +"""Independent bounded corroboration; exact arithmetic, standard library only. + +Separate AI reviewer, 2026-10-29; Apache-2.0. No human/formal certification. +Reads the requested package's optimum.py as bytes, executes those exact source +bytes, and prints JSON. Does not write files, use networks, or spawn processes. + +Two independently organized domains: +1. Every integer signed quartic with Q(1)=Q(2)=0, positive leading coefficient, + and positive/negative coefficient mass at most --signed-budget. Feasibility + uses a generic rational Sturm sequence, not the author's root inequalities. +2. All ordered Farey-neighbor roots m/n < p/q in (1,2) with np-mq=1 and + (m+n)(p+q)<=--farey-cap. Width comparisons use the exact root ratio pn/qm, + not the author's discriminant statistic, square tests, or divisor routine. + This second domain covers Delta=1 only; the reviewed dominance proof remains + necessary to exclude other discriminants outside the first finite domain. +""" + +import argparse +import copy +from fractions import Fraction +import hashlib +import json +from math import gcd +from pathlib import Path +import platform +import types + + +def require(ok, message): + if not ok: + raise RuntimeError(message) + + +def trim(poly): + poly = list(poly) + while poly and poly[-1] == 0: + poly.pop() + return poly + + +def divide(num, den): + num, den = trim(num), trim(den) + require(bool(den), "zero polynomial divisor") + quotient = [Fraction(0)] * max(0, len(num) - len(den) + 1) + while len(num) >= len(den): + shift = len(num) - len(den) + factor = Fraction(num[-1], den[-1]) + quotient[shift] = factor + for j, coefficient in enumerate(den): + num[shift + j] -= factor * coefficient + num = trim(num) + return trim(quotient), num + + +def evaluate(poly, x): + value = 0 + for coefficient in reversed(poly): + value = value * x + coefficient + return value + + +def sturm_count(poly, left, right): + require(evaluate(poly, left) != 0 and evaluate(poly, right) != 0, + "Sturm fixture must avoid endpoint roots") + chain = [trim(poly), trim([i * c for i, c in enumerate(poly)][1:])] + while chain[-1]: + _, remainder = divide(chain[-2], chain[-1]) + if not remainder: + break + chain.append([-c for c in remainder]) + + def variations(x): + signs = [(v > 0) - (v < 0) for p in chain if (v := evaluate(p, x))] + return sum(a != b for a, b in zip(signs, signs[1:])) + + return variations(left) - variations(right) + + +def signed_quartic_census(opt, cap): + """Full signed-coefficient domain, before any alternating-sign assumption.""" + buckets = [[] for _ in range(cap + 1)] + trials = bounded = endpoint_rejected = root_count_rejected = eligible = 0 + for q4 in range(1, cap + 1): + for q3 in range(-cap, cap + 1): + for q2 in range(-cap, cap + 1): + trials += 1 + # Solve the two linear equalities Q(1)=Q(2)=0 exactly. + q1 = -3 * q2 - 7 * q3 - 15 * q4 + q0 = 2 * q2 + 6 * q3 + 14 * q4 + if abs(q1) > cap or abs(q0) > cap: + continue + Q = [q0, q1, q2, q3, q4] + mass = sum(max(c, 0) for c in Q) + if mass > cap: + continue + bounded += 1 + require(sum(Q) == 0 and evaluate(Q, 2) == 0, "linear constraints") + require(sum(max(-c, 0) for c in Q) == mass, "signed masses") + # Generic exact polynomial division checks the endpoint factors. + residual, rem1 = divide(Q, [-1, 1]) + residual, rem2 = divide(residual, [-2, 1]) + require(not rem1 and not rem2 and len(residual) == 3, "deflation") + if evaluate(residual, 1) == 0 or evaluate(residual, 2) == 0: + endpoint_rejected += 1 + continue + if sturm_count(residual, 1, 2) != 2: + root_count_rejected += 1 + continue + require(all(c.denominator == 1 for c in residual), "integer quotient") + c, b, a = map(int, residual) + z = -b + require(a > 0 and z > 0 and c > 0, "positive-root coefficient signs") + require(Q[0] > 0 > Q[1] and Q[2] > 0 > Q[3] and Q[4] > 0, + "alternating full polynomial") + require(mass == 3 * (a + z + c), "normalization from full coefficients") + require(evaluate(Q, Fraction(z, 2 * a)) > 0, "oriented positive window") + eligible += 1 + score = Fraction(z * z - 4 * a * c, z * z) + buckets[mass].append((score, [a, z, c])) + require(trials == cap * (2 * cap + 1) ** 2, "signed domain count") + best, winners = None, [] + changes = [] + for N, rows in enumerate(buckets): + for score, row in rows: + if best is None or score < best: + best, winners = score, [row] + elif score == best: + winners.append(row) + cert = opt.solve_normalized(N // 3) + if best is None: + require(cert["status"] == "infeasible", "signed feasibility at N=" + str(N)) + else: + require(cert["status"] == "optimal", "signed status at N=" + str(N)) + require(Fraction(*cert["score"]) == best, "signed score at N=" + str(N)) + require(cert["residuals"] == sorted(winners), "signed all ties at N=" + str(N)) + if rows: + changes.append({"per_profile_N": N, "new_eligible": len(rows), + "optimum_residuals": sorted(winners)}) + return {"per_profile_N_cap": cap, "normalized_L_cap": cap // 3, + "signed_coefficient_trials": trials, "bounded_endpoint_polynomials": bounded, + "endpoint_root_rejections": endpoint_rejected, + "Sturm_root_count_rejections": root_count_rejected, + "eligible_polynomials": eligible, "budget_prefixes": cap + 1, + "eligible_mass_events": changes} + + +def farey_census(opt, cap): + buckets = [[] for _ in range(cap + 1)] + root_pairs, numerator_trials, congruence_trials = set(), 0, 0 + # q>=2 and p>=3 imply p+q>=5, hence 2n+1 <= floor(cap/5). + for n in range(2, (cap // 5 - 1) // 2 + 1): + for m in range(n + 1, 2 * n): + numerator_trials += 1 + if gcd(m, n) != 1: + continue + # np-mq=1, so q == -inverse(m) modulo n. + q0 = (-pow(m, -1, n)) % n + if q0 < 2: + q0 += n + max_q = (cap // (m + n) - 1) // 2 + for q in range(q0, max_q + 1, n): + congruence_trials += 1 + p, rem = divmod(m * q + 1, n) + require(rem == 0, "Farey congruence") + if not q < p < 2 * q: + continue + cost = (m + n) * (p + q) + if cost > cap: + continue + require(n * p - m * q == 1, "strict adjacent roots") + row = [n * q, m * q + n * p, m * p] + require(sum(row) == cost, "root-product budget") + require(tuple(row) not in root_pairs, "duplicate Farey parametrization") + root_pairs.add(tuple(row)) + buckets[cost].append((Fraction(p * n, q * m), row)) + best, winners, multi, checked = None, [], 0, 0 + tie_examples = [] + for L, rows in enumerate(buckets): + for ratio, row in rows: + if best is None or ratio < best: + best, winners = ratio, [row] + elif ratio == best: + winners.append(row) + if L < 35: + require(best is None, "unexpected Delta=1 small case") + continue + cert = opt.solve_normalized(L) + require(cert["residuals"] == sorted(winners), "Farey all optimizers at L=" + str(L)) + require(best == Fraction(cert["z_star"] + 1, cert["z_star"] - 1), + "independent root ratio at L=" + str(L)) + require(opt.verify_certificate(cert), "valid certificate") + checked += 1 + if len(winners) > 1: + multi += 1 + if len(tie_examples) < 5: + tie_examples.append({"L": L, "residuals": sorted(winners)}) + return {"normalized_L_cap": cap, "numerator_trials": numerator_trials, + "congruence_trials": congruence_trials, "unique_Delta1_residuals": len(root_pairs), + "budget_prefixes_checked": checked, "budgets_with_ties": multi, + "first_tie_budgets": tie_examples} + + +def certificate_mutations(opt): + tested = 0 + exception_counts = {} + + def rejects(cert, label): + nonlocal tested + try: + opt.verify_certificate(cert) + except (ValueError, TypeError, OverflowError) as exc: + tested += 1 + name = type(exc).__name__ + exception_counts[name] = exception_counts.get(name, 0) + 1 + else: + raise RuntimeError("malformed certificate accepted: " + label) + + for value in (None, [], True, 1, "{}"): + rejects(value, "top-level type") + + def leaves(value, path=()): + if isinstance(value, dict): + for key, item in value.items(): + yield from leaves(item, path + (key,)) + elif isinstance(value, list): + for i, item in enumerate(value): + yield from leaves(item, path + (i,)) + else: + yield path, value + + for L in (0, 30, 31, 34, 35, 40, 144, 333, 4096, 100000): + valid = opt.solve_normalized(L) + require(opt.verify_certificate(valid), "unmutated control") + for key in valid: + cert = copy.deepcopy(valid) + del cert[key] + rejects(cert, "missing " + key) + cert = copy.deepcopy(valid) + cert["unverified"] = "extra" + rejects(cert, "extra field") + for path, leaf in leaves(valid): + if path == ("normalized_budget",): + choices = [str(L), float(L), True, -1, 100001] + elif type(leaf) is int: + choices = [leaf + 1, float(leaf), True, str(leaf), None] + elif type(leaf) is str: + choices = [leaf + "!", None, 0] + elif leaf is None: + choices = [0, False, "null"] + else: + raise RuntimeError("unexpected valid leaf type") + for replacement in choices: + cert = copy.deepcopy(valid) + target = cert + for component in path[:-1]: + target = target[component] + target[path[-1]] = replacement + rejects(cert, repr(path)) + for key in ("residuals", "excluded_odd_traces"): + items = valid.get(key) + if not items: + continue + for variant in (items[:-1], items + items[:1]): + cert = copy.deepcopy(valid) + cert[key] = variant + rejects(cert, key + " omitted/duplicate") + if len(items) > 1: + cert = copy.deepcopy(valid) + cert[key] = list(reversed(items)) + rejects(cert, key + " reversed canonical order") + return {"malformed_cases_rejected": tested, "exception_counts": exception_counts, + "valid_controls": 10} + + +def boundary_checks(): + fixtures = [([3, -5, 2], "root at 1"), ([6, -7, 2], "root at 2"), + ([2, -3, 1], "both endpoints"), ([9, -12, 4], "double interior root"), + ([11, -15, 5], "irrational interior pair"), + ([12, -17, 6], "rational interior pair")] + results = [] + for poly, name in fixtures: + boundary = evaluate(poly, 1) == 0 or evaluate(poly, 2) == 0 + count = None if boundary else sturm_count(poly, 1, 2) + accepted = not boundary and count == 2 + require(accepted == ("interior pair" in name), "boundary fixture " + name) + results.append({"fixture": name, "accepted": accepted, "interior_root_count": count}) + return results + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--package", required=True, type=Path) + parser.add_argument("--signed-budget", default=150, type=int) + parser.add_argument("--farey-cap", default=4096, type=int) + args = parser.parse_args() + require(1 <= args.signed_budget <= 600, "bounded signed-budget range 1..600") + require(35 <= args.farey_cap <= 10000, "bounded farey-cap range 35..10000") + source_path = args.package / "optimum.py" + source = source_path.read_bytes() + opt = types.ModuleType("independent_review_subject") + opt.__file__ = str(source_path) + exec(compile(source, str(source_path), "exec", dont_inherit=True), opt.__dict__) + report = { + "claim_type": "independent AI review with bounded exact corroboration", + "python": platform.python_version(), + "boundary_fixtures": boundary_checks(), + "signed_quartics": signed_quartic_census(opt, args.signed_budget), + "Farey_root_pair_census": farey_census(opt, args.farey_cap), + "certificate_mutations": certificate_mutations(opt), + "source_sha256": {name: hashlib.sha256((args.package / name).read_bytes()).hexdigest() + for name in ("PROOF.md", "README.md", "SOURCES.json", "optimum.py", "verify.py")}, + "executed_optimum_sha256": hashlib.sha256(source).hexdigest(), + "checker_sha256": hashlib.sha256(Path(__file__).read_bytes()).hexdigest(), + "marker": "PASS_INDEPENDENT_EXACT_REVIEW", + } + print(json.dumps(report, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/hidden-window-optima/optimum.py b/research/hidden-window-optima/optimum.py new file mode 100644 index 0000000000..4b7cbde626 --- /dev/null +++ b/research/hidden-window-optima/optimum.py @@ -0,0 +1,144 @@ +#!/usr/bin/env python3 +"""Exact hidden-window optimum under the hypotheses in PROOF.md. + +Private draft, substantial OpenAI Codex assistance, Apache-2.0. +No external imports, network, subprocesses, or file writes. +The uniform theorem has no size cap; this reference API deliberately does. +""" + +import argparse +import json +from math import isqrt + +MAX_L = 100_000 +MAX_H = 16 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def checked_int(value, low, high, name): + require(type(value) is int, name + " must be an integer, not bool") + require(low <= value <= high, name + " outside reference implementation range") + return value + + +def residuals_from_squares(L, z): + """All discriminant-one residuals at fixed odd trace, via k=R(1).""" + found = [] + for k in range(1, L - 2 * z + 1): + U = 2 * z * k + k * k + 1 + u = isqrt(U) + if u * u != U or (z + k - u) % 2: + continue + a = (z + k - u) // 2 + c = (z + k + u) // 2 + if a > 0 and c > 0 and 2 * a < z - 1 and z + 1 < 4 * a: + found.append([a, z, c]) + return sorted(found) + + +def solve_normalized(L): + """Return all optimum residuals and a replayable search certificate.""" + checked_int(L, 0, MAX_L, "L") + common = {"schema": 1, "normalized_budget": L} + if L < 31: + return dict(common, status="infeasible", residuals=[]) + if L < 35: + return dict(common, status="optimal", discriminant=5, z_star=15, + residuals=[[5, 15, 11]], score=[1, 45], + seed_trace=None, excluded_odd_traces=[]) + n = isqrt((L + 1) // 4) + z0 = 2 * n * n - 1 + Z = (L - 1) // 2 + top = Z if Z % 2 else Z - 1 + excluded = [] + for z in range(top, z0 - 1, -2): + found = residuals_from_squares(L, z) + if found: + return dict(common, status="optimal", discriminant=1, z_star=z, + residuals=found, score=[1, z * z], seed_trace=z0, + excluded_odd_traces=excluded) + excluded.append(z) + raise ArithmeticError("proved seed was not found") + + +def solve_budget(h, N): + checked_int(h, 1, MAX_H, "h") + S = 6 ** h // 2 + checked_int(N, 1, S * (MAX_L + 1) - 1, "N") + cert = solve_normalized(N // S) + return {"h": h, "per_profile_budget": N, "normalization": S, + "normalized_certificate": cert, + "residual_counts": [S * sum(row) for row in cert["residuals"]]} + + +def divisor_residuals(L, z): + """Separate certificate check using divisors of t(t+1), not square tests.""" + t = (z - 1) // 2 + product = t * (t + 1) + found = [] + for a in range((t + 1) // 2 + 1, t): + c, rem = divmod(product, a) + if rem == 0 and a + z + c <= L: + found.append([a, z, c]) + return found + + +def verify_certificate(cert): + """Recompute all exclusions and all winners with the divisor oracle. + + This verifies the finite certificate given the uniform proof in PROOF.md. + It is not a proof-kernel implementation of that proof. + """ + require(type(cert) is dict, "certificate must be a dictionary") + require(type(cert.get("schema")) is int and cert["schema"] == 1, "schema") + L = checked_int(cert.get("normalized_budget"), 0, MAX_L, "L") + if L < 31: + expected = {"schema": 1, "normalized_budget": L, + "status": "infeasible", "residuals": []} + elif L < 35: + expected = {"schema": 1, "normalized_budget": L, "status": "optimal", + "discriminant": 5, "z_star": 15, "residuals": [[5, 15, 11]], + "score": [1, 45], "seed_trace": None, "excluded_odd_traces": []} + else: + z = checked_int(cert.get("z_star"), 1, (L - 1) // 2, "z_star") + require(z % 2 == 1, "trace must be odd") + n = isqrt((L + 1) // 4) + z0 = 2 * n * n - 1 + require(z >= z0, "trace worse than available seed") + excluded = list(range(((L - 1) // 2 - 1) // 2 * 2 + 1, z, -2)) + for higher in excluded: + require(not divisor_residuals(L, higher), "a better residual exists") + winners = divisor_residuals(L, z) + require(bool(winners), "claimed trace has no eligible residual") + expected = {"schema": 1, "normalized_budget": L, "status": "optimal", + "discriminant": 1, "z_star": z, "residuals": winners, + "score": [1, z * z], "seed_trace": z0, + "excluded_odd_traces": excluded} + # Canonical JSON comparison also distinguishes bool from integers. + require(json.dumps(cert, sort_keys=True) == json.dumps(expected, sort_keys=True), + "certificate fields or complete residual list disagree") + return True + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + group = parser.add_mutually_exclusive_group(required=True) + group.add_argument("--normalized-budget", type=int) + group.add_argument("--budget", type=int, help="per-profile budget N") + parser.add_argument("--h", type=int, default=1) + args = parser.parse_args() + if args.normalized_budget is not None: + result = solve_normalized(args.normalized_budget) + verify_certificate(result) + else: + result = solve_budget(args.h, args.budget) + verify_certificate(result["normalized_certificate"]) + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/hidden-window-optima/verify.py b/research/hidden-window-optima/verify.py new file mode 100644 index 0000000000..0300b33ddc --- /dev/null +++ b/research/hidden-window-optima/verify.py @@ -0,0 +1,287 @@ +#!/usr/bin/env python3 +"""Bounded exact corroboration; no network, subprocesses, or file writes. + +Substantial OpenAI Codex assistance. Apache-2.0. +All scientific checks remain active under python -O. +""" + +import copy +import hashlib +import json +from fractions import Fraction +from math import comb, isqrt +from pathlib import Path +import platform +import time +import types + +ROOT = Path(__file__).resolve().parent +OPTIMUM_PATH = ROOT / "optimum.py" +OPTIMUM_SOURCE = OPTIMUM_PATH.read_bytes() +opt = types.ModuleType("window_optimum") +opt.__file__ = str(OPTIMUM_PATH) +# Compile the same bytes bound by the receipt, never an adjacent cached .pyc. +exec(compile(OPTIMUM_SOURCE, str(OPTIMUM_PATH), "exec", dont_inherit=True), opt.__dict__) + + +def check(condition, message): + if not condition: + raise RuntimeError(message) + + +def eligible(a, z, c): + return (a > 0 and z > 0 and c > 0 and z * z > 4 * a * c + and 2 * a < z < 4 * a and a - z + c > 0 + and 4 * a - 2 * z + c > 0) + + +def update(record, row): + a, z, c = row + score = (z * z - 4 * a * c, z * z) + if record is None or score[0] * record[0][1] < record[0][0] * score[1]: + return (score, [list(row)]) + if score[0] * record[0][1] == record[0][0] * score[1]: + return (record[0], record[1] + [list(row)]) + return record + + +def compare_certificate(cert, record, label): + if record is None: + check(cert["status"] == "infeasible", label + " feasibility") + return + check(cert["status"] == "optimal", label + " status") + num, den = cert["score"] + check(num * record[0][1] == record[0][0] * den, label + " score") + check(cert["residuals"] == sorted(record[1]), label + " all minimizers") + + +def literal_simplex(cap): + """Every positive triple a+z+c<=cap, no discriminant or trace pruning.""" + buckets = [[] for _ in range(cap + 1)] + trials = 0 + for a in range(1, cap - 1): + for z in range(1, cap - a): + for c in range(1, cap - a - z + 1): + trials += 1 + if eligible(a, z, c): + buckets[a + z + c].append([a, z, c]) + check(trials == comb(cap, 3), "literal domain cardinality") + record = None + eligible_count = 0 + predecessor_count = None + small = [] + for L, rows in enumerate(buckets): + for row in rows: + eligible_count += 1 + record = update(record, row) + if L <= 34: + small.append(row) + compare_certificate(opt.solve_normalized(L), record, "literal L=" + str(L)) + if L == 333: + predecessor_count = eligible_count + check(small == [[5, 15, 11]], "complete small-budget exception") + check(predecessor_count == 8158, "PR6139 N=1000 residual count") + return {"max_L": cap, "triples": trials, "eligible_residuals": eligible_count, + "budgets_checked": cap + 1, "eligible_through_34": small, + "eligible_at_L333": predecessor_count} + + +def divisor_census(cap): + """All Delta=1 triples through cap using a divisibility census.""" + buckets = [[] for _ in range(cap + 1)] + trials = 0 + for t in range(1, ((cap - 1) // 2 - 1) // 2 + 1): + z = 2 * t + 1 + for a in range((t + 1) // 2 + 1, t): + trials += 1 + c, rem = divmod(t * (t + 1), a) + if not rem and a + z + c <= cap: + check(eligible(a, z, c), "divisor root condition") + buckets[a + z + c].append([a, z, c]) + record = None + residual_count = 0 + multi = 0 + for L, rows in enumerate(buckets): + for row in rows: + residual_count += 1 + record = update(record, row) + if L >= 35: + cert = opt.solve_normalized(L) + compare_certificate(cert, record, "divisor L=" + str(L)) + check(opt.verify_certificate(cert), "certificate rejected") + multi += len(cert["residuals"]) > 1 + return {"max_L": cap, "divisor_trials": trials, "residuals": residual_count, + "budgets_checked": cap - 34, "budgets_with_multiple_optimizers": multi} + + +def largest_c_oracle(L): + """All discriminants, selecting the best c for each fixed a,z.""" + record = None + pairs = eligible_pairs = 0 + for z in range(1, (L - 1) // 2 + 1): + for a in range(z // 4 + 1, (z - 1) // 2 + 1): + pairs += 1 + c = min(L - a - z, (z * z - 1) // (4 * a)) + if c > max(0, z - a, 2 * z - 4 * a): + eligible_pairs += 1 + check(eligible(a, z, c), "largest-c root predicate") + record = update(record, [a, z, c]) + cert = opt.solve_normalized(L) + compare_certificate(cert, record, "largest-c L=" + str(L)) + return {"L": L, "pairs": pairs, "eligible_pairs": eligible_pairs, + "certificate": cert} + + +def multiply(P, Q): + result = [0] * (len(P) + len(Q) - 1) + for i, p in enumerate(P): + for j, q in enumerate(Q): + result[i + j] += p * q + return result + + +def evaluate(P, x): + result = 0 + for p in reversed(P): + result = result * x + p + return result + + +def derivative(P): + return [i * P[i] for i in range(1, len(P))] + + +def profiles_and_padding(): + count = padding_count = 0 + for L in (31, 34, 35, 37, 40, 62, 63, 144, 333, 1000): + cert = opt.solve_normalized(L) + for a, z, c in cert["residuals"]: + delta = z * z - 4 * a * c + for h in range(1, 7): + Q = [c, -z, a] + for _ in range(h): + Q = multiply(Q, [2, -3, 1]) + Q = [(-1) ** (h + 1) * q for q in Q] + A = [max(-q, 0) for q in Q] + B = [max(q, 0) for q in Q] + S = 6 ** h // 2 + W = S * (a + z + c) + check(len(Q) == 2 * h + 3, "support size") + check(sum(A) == sum(B) == W, "per-side count") + check(sum(q * (2 ** j) for j, q in enumerate(Q)) == 0, "rank mass") + derivative_Q = Q + for _ in range(h): + check(evaluate(derivative_Q, 1) == evaluate(derivative_Q, 2) == 0, + "endpoint multiplicity") + derivative_Q = derivative(derivative_Q) + check(evaluate(derivative_Q, 1) != 0 and evaluate(derivative_Q, 2) != 0, + "multiplicity is exact") + midpoint = Fraction(z, 2 * a) + check(1 < midpoint < 2 and evaluate(Q, midpoint) > 0, "window sign") + if delta == 1: + r, s = Fraction(z - 1, 2 * a), Fraction(z + 1, 2 * a) + check(1 < r < s < 2, "strict rational roots") + check(evaluate(Q, r) == evaluate(Q, s) == 0, "interior roots") + check(evaluate(Q, (1 + r) / 2) < 0 and evaluate(Q, (s + 2) / 2) < 0, + "outside window signs") + count += 1 + for rho in (0, S - 1): + N = S * L + rho + allowance = N - W + check(allowance >= 0, "budget") + padded_A, padded_B = A[:], B[:] + padded_A[0] += allowance + padded_B[0] += allowance + check(sum(padded_A) == sum(padded_B) == N, "full common padding") + check([b - a0 for a0, b in zip(padded_A, padded_B)] == Q, + "padding leaves polynomial unchanged") + check(sum(padded_A) + 1 > N, "overbudget padding rejected") + actual = opt.solve_budget(h, N) + check(actual["normalized_certificate"] == cert, "h and remainder scaling") + padding_count += 1 + return {"signed_profiles": count, "padding_and_scaling_cases": padding_count} + + +def rejection_controls(): + controls = [] + + def rejected(label, call): + try: + call() + except (ValueError, ArithmeticError): + controls.append(label) + else: + raise RuntimeError("control was accepted: " + label) + + for x in (-1, True, 3.5, "35", opt.MAX_L + 1): + rejected("invalid L " + repr(x), lambda x=x: opt.solve_normalized(x)) + for h, N in ((0, 100), (17, 100), (True, 100), (1, 0), (1, True), (1, 300003)): + rejected("invalid h,N " + repr((h, N)), lambda h=h, N=N: opt.solve_budget(h, N)) + for label, source_L, edit in ( + ("missing tied optimizer", 144, lambda c: c["residuals"].pop()), + ("wrong discriminant", 333, lambda c: c.update(discriminant=4)), + ("missing excluded trace", 333, lambda c: c["excluded_odd_traces"].pop()), + ("wrong coefficient", 333, lambda c: c["residuals"][0].__setitem__(0, 61)), + ("wrong exact score", 333, lambda c: c.update(score=[1, 25920])), + ("boolean masquerading as discriminant", 333, lambda c: c.update(discriminant=True)), + ("extra unverified metadata", 333, lambda c: c.update(unchecked=True)), + ("false small-budget feasibility", 30, lambda c: c.update(status="optimal")), + ("false rational small-budget claim", 31, lambda c: c.update(discriminant=1)), + ("looser budget with better optimizer", 35, lambda c: c.update(normalized_budget=40)), + ): + cert = copy.deepcopy(opt.solve_normalized(source_L)) + edit(cert) + rejected(label, lambda cert=cert: opt.verify_certificate(cert)) + # Valid algebraic discriminant-one triples at the excluded boundary roots. + for row in ([2, 7, 6], [3, 11, 10]): + check(row[1] ** 2 - 4 * row[0] * row[2] == 1, "boundary fixture Delta") + check(not eligible(*row), "root at x=2 must be excluded") + # The seed family alone does not solve the intermediate budgets. + check(opt.solve_normalized(40)["z_star"] == 19 > 17, "seed-only false conclusion") + return {"rejected_inputs_and_certificates": len(controls), "labels": controls, + "boundary_fixtures": 2, "seed_only_counterexample": 40} + + +def dominance_fixtures(): + count = 0 + for n in list(range(3, 1001)) + [10 ** 10, 10 ** 50, 10 ** 100]: + for L in (4 * n * n - 1, 4 * (n + 1) ** 2 - 2): + z0 = 2 * n * n - 1 + Z = (L - 1) // 2 + check(isqrt((L + 1) // 4) == n, "integer seed selection") + check(2 * z0 > Z and 4 * z0 * z0 > Z * Z, "strict domination") + check(2 * n * n - 4 * n - 2 > 0, "uniform polynomial sign") + count += 1 + return {"endpoint_and_large_integer_fixtures": count, + "uniformity_depends_on_written_proof": True} + + +def main(): + started = time.perf_counter() + report = {"claim_type": "proposed proof with exact finite corroboration", + "python": platform.python_version(), + "literal_simplex": literal_simplex(400), + "divisor_census": divisor_census(4096), + "all_discriminant_oracles": [largest_c_oracle(L) for L in + (31, 34, 35, 40, 144, 333, 401, 512, + 777, 1000, 2048, 4096, 8192)], + "profiles": profiles_and_padding(), + "controls": rejection_controls(), + "dominance": dominance_fixtures()} + report["large_reference_cases"] = [] + for L in (9999, 10000, 99999, 100000): + cert = opt.solve_normalized(L) + check(opt.verify_certificate(cert), "large certificate") + report["large_reference_cases"].append(cert) + report["source_sha256"] = {p.name: hashlib.sha256( + OPTIMUM_SOURCE if p == OPTIMUM_PATH else p.read_bytes() + ).hexdigest() + for p in sorted(ROOT.iterdir()) + if p.suffix in (".py", ".md", ".json")} + report["elapsed_seconds"] = round(time.perf_counter() - started, 6) + report["marker"] = "PASS_EXACT_HIDDEN_WINDOW_OPTIMA" + print(json.dumps(report, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()