Classify exact fixed-budget hidden-window optima (no new kappa)

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 alpha<beta, and F>0 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,
+    1<r<s<2,  Delta=z^2-4ac>0.
+
+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;
+    2a<z<4a; a-z+c>0; 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,  2a<z-1,  z+1<4a.        (C)
+
+   Then the exact minimum width is log_2((z_star+1)/(z_star-1)).
+   All minimizing residuals are precisely all triples satisfying (C) with
+   z=z_star. Every minimizing profile is their signed-coefficient construction
+   with any identical padding of total at most N-S*(a+z+c).
+
+The theorem is uniform in h,N. The search characterization of z_star is exact;
+it is not claimed to be an elementary closed expression in L.
+
+## Small budgets, by endpoint coordinates
+
+A separate adversarial AI review supplied a direct algebraic argument, removing
+any dependence of this base case on a finite table. Define
+
+    k=R(1)=a-z+c,  ell=R(2)=4a-2z+c,  v=3z-4a-2c.
+
+Then the exact identity is
+
+    R(x)=k(2-x)^2-v(x-1)(2-x)+ell(x-1)^2.
+
+The increasing substitution y=(x-1)/(2-x) maps (1,2) bijectively onto
+(0,infinity), with x=(1+2y)/(1+y). Consequently
+
+    (1+y)^2 R((1+2y)/(1+y)) = ell*y^2-v*y+k.
+
+The two roots of R are distinct and strictly interior precisely when
+k,ell,v are positive integers and v^2>4*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.

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.