[Karnaugh33]

This proposes a solution to the exact finite-budget optimization question left open by PR6153, following PR6139. It adds a scoped proof, a complete optimizer/certificate procedure, and separately written bounded checkers. It makes no claim of a faster multiplication algorithm or improved kappa.

Precise claim

Fix integers h,N >= 1, the minimal rank alphabet 2^j for 0 <= j <= 2h+2, and nonnegative integer profiles A_j,B_j, each with at most N calls including common padding. Require F(p)=sum_j (B_j-A_j) 2^(jp) to have zeros of multiplicity at least h at p=0,1, two distinct zeros 0 < alpha < beta < 1, and F>0 between them. Minimize beta-alpha.

With S=6^h/2, L=floor(N/S), and the inherited residual R(x)=a*x^2-z*x+c, the proposed theorem is:

• L < 31: no eligible profile pair exists.
• 31 <= L <= 34: the unique oriented residual is (a,z,c)=(5,15,11), with discriminant 5.
• L >= 35: every optimizer has discriminant 1. If z_star is the largest odd trace with positive integers a,c satisfying 4ac=z_star^2-1, a+z_star+c <= L, 2a < z_star-1, and z_star+1 < 4a, the exact minimum width is log_2((z_star+1)/(z_star-1)). The procedure returns every tied residual and characterizes all permitted common padding.

The all-budget conclusion rests on a strict domination proof using PR6139's seed family. A new endpoint-coordinate argument proves the small-budget classification algebraically. The finite search is exact and terminating; no elementary closed formula or runtime improvement is claimed. Reference code is capped at L <= 100000 and h <= 16; the written theorem is uncapped.

Credit, evidence and limits

PR6139 supplies the normalization, comparison statistic and seeds. Nick Petalas's PR6153 supplies the complete bound-attainment classification and already contains (5,15,11) as a verifier control; this contribution claims its threshold classification, not discovery of the example. zxv's PR6049, Petalas's PR5174 and Ali Romman's rank-budget lineage retain credit. The predecessors remain partially reviewed. Base provenance is pinned to a5bff3bf133e482541c09eba4e773884bdb2b1b7 in SOURCES.json.

All six direct normal/optimized checker runs passed on CPython 3.14.7. Author checks include 10,586,800 positive coefficient triples through L=400, complete discriminant-one census through L=4096, and all-discriminant oracles at 13 budgets through L=8192. Separate reviewers added 13,590,150 signed-quartic/Sturm trials through h=1,N=150, a Farey-root census through L=4096, 741 malformed-certificate controls, and an endpoint-coordinate census through L=512.

From research/hidden-window-optima, run:

python3 -I -W error -B verify.py
python3 -I -W error -B independent_check.py --package .
python3 -I -W error -B endpoint_coordinate_check.py

Repeat with -O; VERIFY.json registers all six commands. Repository metadata/source-pin validation passed. Its Python 3.12 managed replay was not run locally because that interpreter was unavailable. Selected scientific replay, Lean, Docker and hosted CI were not run.

Substantial OpenAI Codex assistance produced the proof, code, checks and separate AI reviews. The reviewers found no mathematical defect, supplied the analytic small-budget proof, and reproduced then verified a fix for stale-bytecode/source-receipt binding. These are independent AI reviews, not human or proof-kernel validation; common reasoning errors remain possible. A bounded upstream audit found no blocking overlap in the inspected records, without asserting global novelty.

Please review the all-profile reduction, strict domination inequality and certificate completeness. The exact alphabet and root hypotheses are essential. No supplier, arbitrary-rank, compiler, restoration, stock, precision/tape or analytic-recovery obligation is discharged. The selected kappa and all five framework assumptions are unchanged. All ten new files are confined to research/hidden-window-optima/; predecessor packages and shared code are untouched. Apache-2.0, with retained attribution.