Classify every budget attaining the hidden-window bound (no new κ)

research/hidden-window-attainment-budgets/PROOF.md

@@ -0,0 +1,131 @@
+# Exactly which budgets attain the hidden-window bound
+
+This scoped proof was produced by Nick Petalas. Apache-2.0.
+
+## Model and predecessor
+
+Fix integers h>=1 and N>=1. On ranks 2^j for 0<=j<=2h+2, let A_j,B_j
+be nonnegative integer call multiplicities, at most N calls per profile.
+Set Q(x)=sum_j(B_j-A_j)x^j and F(p)=Q(2^p). Require endpoint zeros of
+multiplicity at least h at p=0,1 and two distinct interior zeros alpha<beta,
+with F positive between them. Write w=beta-alpha.
+
+Karnaugh33's [PR6139 proof](https://github.com/CrocSwap/integer-mult-bounds/blob/3b9de03623e8bf05af49f9f9c5fc7a426cbde9e5/research/fixed-budget-hidden-windows/PROOF.md)
+supplies this reduction and bound:
+
+```text
+S=6^h/2,  L=floor(N/S),  Z=floor((L-1)/2),
+Q(x)=(-1)^(h+1)(x-1)^h(x-2)^h R(x),
+R(x)=a x^2-z x+c=a(x-r)(x-s),
+a,z,c positive integers,  1<r<s<2,
+Delta=z^2-4ac positive integer,
+D=a+z+c,  W=SD<=N,
+w >= log_2((Z+1)/(Z-1)).
+```
+
+W counts calls on each side after cancelling common calls. It is not the
+combined count. Eligible profiles have Z>1. The source supplies the bound,
+one infinite attaining family and one further example. Its Open next
+question 1 asks for the complete attainment classification. Our result
+answers that question; no source executable or census is replayed.
+
+## Classification
+
+The bound is attainable at budget N if and only if L belongs to
+
+```text
+{4n^2-1, 4n^2 : n>=3} union {2n(n+1) : n>=4}.
+```
+
+All attaining residuals are as follows, with the positive leading coefficient
+convention above. Include both when both tests hold.
+
+```text
+L=4n^2-1 or 4n^2, n>=3:
+  (a,z,c)=(n(n-1), 2n^2-1, n(n+1)),  D=4n^2-1;
+
+L=2n(n+1), n>=4:
+  (a,z,c)=(n(n-1)/2, n^2+n-1, (n+1)(n+2)/2),  D=L.
+```
+
+This is an existence statement at a budget. Other profiles at that budget
+may have strictly wider windows. Elsewhere the bound is unattainable; this
+does not identify the true optimum or imply that no eligible profile exists.
+
+## Necessity
+
+The quadratic formula gives s/r=(z+sqrt(Delta))/(z-sqrt(Delta)). Its
+denominator is positive since c>0. Put k=R(1)=a+c-z. Strict interior
+roots imply that k is a positive integer. Since D=2z+k<=L, we have 0<z<=Z.
+Thus sqrt(Delta)/z>=1/Z. Strict monotonicity of (1+t)/(1-t) on 0<t<1
+shows that equality in the bound is equivalent to Z^2 Delta=z^2.
+Because Delta>=1 and 0<z<=Z, this means exactly Delta=1 and z=Z.
+No irrational-root residual or integer scaling greater than one can attain it.
+
+Now L is 2z+1 or 2z+2, so D=2z+k<=L forces k in {1,2}. Also
+c/a=rs>1, hence u=c-a is a positive integer. Using a+c=z+k yields
+
+```text
+u^2=(a+c)^2-4ac=2kz+k^2+1.
+```
+
+For k=1, u^2=2z+2 is even. Write u=2n, n>=1. Then
+
+```text
+z=2n^2-1,  a=n(n-1),  c=n(n+1),  D=4n^2-1.
+r=(n+1)/n,  s=n/(n-1).
+```
+
+Positivity and s<2 force n>=3. From z=Z and D<=L, exactly
+L=4n^2-1 and L=4n^2 remain.
+
+For k=2, u^2=4z+5 is odd. Write u=2n+1, n>=0. Then
+
+```text
+z=n^2+n-1,  a=n(n-1)/2,  c=(n+1)(n+2)/2,
+D=2n(n+1)=2z+2,  r=(n+2)/n,  s=(n+1)/(n-1).
+```
+
+Positivity and s<2 force n>=4. Now D<=L leaves only L=2n(n+1).
+These cases exhaust k and prove necessity.
+
+## Sufficiency and every profile realization
+
+Each listed triple has positive integer coefficients, Delta=1, strict
+interior roots, z=Z and SD<=N. Form Q using the endpoint factors above.
+All its roots are positive, so its coefficients alternate strictly in sign.
+Let A be its negative coefficient part and B its positive coefficient part.
+Then Q(1)=Q(2)=0 gives equal counts and rank masses, and
+
+```text
+sum A_j = sum B_j = |Q(-1)|/2 = S(a+z+c) = SD.
+```
+
+The orientation makes Q positive on (r,s) and negative on (1,r) and (s,2).
+Thus these profiles satisfy the premises and attain the bound.
+
+Every profile pair giving this Q is obtained by adding the same nonnegative
+integer vector H to both disjoint coefficient parts. It is permitted exactly
+when sum H_j<=N-SD. Writing N=SL+rho with 0<=rho<S, the maximum common
+count is rho at L=4n^2-1, S+rho at L=4n^2, and rho for the second family.
+Padding changes neither Q nor R and creates no other residuals.
+
+An even L can belong to both families. At L=144 the two residuals are
+(30,71,42) and (28,71,45). A construction must return both. Classifying
+all overlap indices is unnecessary for the theorem.
+
+## Credit and limits
+
+The reduction, bound, first family at L=4n^2-1 and second family's n=4
+example belong to Karnaugh33. The new part is the exhaustive equality
+classification, adjacent normalized budgets 4n^2, the full second family
+and explicit padding allowances. zxv's [PR6049](https://github.com/CrocSwap/integer-mult-bounds/pull/6049)
+supplies the hidden-window/minimal-support framework and credits Nick
+Petalas's PR5174 and Ali Romman's rank-budget lineage. The quadratic formula,
+integer discriminants and positive-root coefficient signs are classical.
+
+The proof is uniform in h,N. Finite checks corroborate it; no formal
+proof-kernel certification is claimed. Arithmetic call profiles do not
+establish legal native realization, source compatibility, independent targets,
+dirty restoration, compiler, stock, precision/tape or the complete caller.
+No new kappa or complete multiplication theorem follows.

research/hidden-window-attainment-budgets/README.md

@@ -0,0 +1,101 @@
+# Exact attainment budgets for hidden power windows
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped mathematical proof with exact finite corroboration.
+It answers Open next question 1 of Karnaugh33's
+[PR6139](https://github.com/CrocSwap/integer-mult-bounds/pull/6139), at head
+`3b9de03623e8bf05af49f9f9c5fc7a426cbde9e5`. No new kappa is claimed.
+
+For h>=1, take integer call profiles on ranks 2^j, 0<=j<=2h+2, with at
+most N calls per profile. Require h-fold endpoint zeros at p=0,1 and a
+positive window between two interior roots. Put
+
+```text
+S=6^h/2,  L=floor(N/S),  Z=floor((L-1)/2).
+```
+
+The predecessor's window-width bound is `w >= log_2((Z+1)/(Z-1))`.
+We prove it is attainable exactly when
+
+```text
+L in {4n^2-1, 4n^2 : n>=3} union {2n(n+1) : n>=4}.
+```
+
+[PROOF.md](PROOF.md) gives every attaining residual quadratic and its
+allowed common padding. At h=1,N=432 there are two residuals,
+`30x^2-71x+42` and `28x^2-71x+45`. Outside the listed set, the cited bound
+is unattainable; the actual optimum there remains open. Attainability does
+not say every profile at that budget attains the bound.
+
+## Evidence and reproduction
+
+The exact verifier compares the classification with a divisor oracle through
+L=4096 and a complete positive-coefficient oracle through L=96. It constructs
+signed profiles and checks counts, rank mass, exact endpoint multiplicities,
+window signs, budget remainders, both families and rejection controls. It uses
+only integers and fractions, with no repository imports, network or predecessor
+execution. It finds 100 attaining normalized budgets and 101 residuals, builds
+606 profiles and checks 768 padding cases. The full small oracle enumerates
+142880 triples and makes 2760 eligible residual/budget comparisons. Controls
+include 19 rejected inputs, five semantic cases and nine large-integer cases.
+A generated stdout receipt binds all six package files by SHA256.
+
+From the repository root:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/hidden-window-attainment-budgets/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/hidden-window-attainment-budgets/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/hidden-window-attainment-budgets
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/hidden-window-attainment-budgets --check-source-history
+```
+
+Another CPython 3.12 path may replace the displayed interpreter. The direct
+marker is `PASS_HIDDEN_WINDOW_ATTAINMENT_BUDGETS`. Registered replay and
+committed bytes/source ancestry are separate checks. Hosted CI status is
+recorded in the PR body.
+
+## Scope, sources and limits
+
+This is an arithmetic side result about exact signed power invoices, explicitly
+changed from the source-recount card in [TASK.json](TASK.json). It identifies
+exactly when the available fixed-budget lower bound is sharp. It does not
+re-evaluate the predecessor's N=1000 census.
+
+The source bound and question are cited at their exact public head. They are
+written context, not runtime imports or foreign Git dependencies. The new
+classification proof is self-contained. Base catalogue, selected record and
+accounting documentation are provenance-only pins in [SOURCES.json](SOURCES.json).
+[VERIFY.json](VERIFY.json) has no external live inputs. Base main is
+`721c03822c421b7f7fcbb2598993b947c4d88419`, priority 8.
+
+The theorem holds for all positive integer h,N. The reusable reference functions
+accept 1<=h<=16 and 1<=N<=2^256 and reject larger inputs. Finite verification
+uses fixed smaller domains. Managed Python allocation and function dispatch in
+rejection controls are documented Power of Ten deviations. Every loop is bounded
+by the declared domains; the largest oracle has 4097 buckets. Checks remain
+active under `-O`. Warning-strict replay is registered for both modes; no shared
+diagnostic configuration changes.
+
+No native word, independent targets, source compatibility, restoration, compiler,
+stock, precision/tape or complete consumer is supplied. The five framework
+assumptions remain. Selected cold replay, predecessor scientific replays, Lean
+and Docker were not run. Independent human and formal proof-kernel review are
+unclaimed.
+
+## Open next questions
+
+Determine the exact minimum width at normalized budgets outside the classified
+set. Begin with discriminant-sensitive optimization of `Delta/z^2` and a
+certificate of its minimum. That integer optimization remains the blocker;
+the present result only settles equality in the cited bound. This follow-on
+is not pursued here.
+
+## Credit
+
+Karnaugh33 supplies the bound, the first family at L=4n^2-1 and the second
+family's n=4 example. The complete classification, adjacent budgets and general
+second family are the new contribution. zxv's PR6049 supplies the minimal-support
+framework and retains Nick Petalas's PR5174 and Ali Romman's rank-budget lineage.
+Classical quadratic/discriminant identities retain their credit. No global
+literature-priority claim is made.

research/hidden-window-attainment-budgets/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "docs/research/recursive-invoice-preflight.md",
+      "usage": "provenance",
+      "git_blob": "3ea54e719c3e01031ad5e75945e524b6f6929806",
+      "sha256": "6e21a610efff4aaf07e2c6f7ee60b832ddc4386a648fcb8b3a5ce969661dfba8"
+    }
+  ]
+}

research/hidden-window-attainment-budgets/TASK.json

@@ -0,0 +1,99 @@
+{
+  "schema_version": 1,
+  "task_id": "independent-moment",
+  "priority_revision": 8,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "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": "Classify every finite call budget attaining the hidden-window discrete lower bound in PR6139, and all attaining residual quadratics.",
+  "scope_change_reason": "The assigned goal asks for original research, not an audit. This is a self-contained arithmetic equality-case theorem answering another contributor's explicit Open next question 1; no predecessor census or source result is replayed.",
+  "bottleneck_link": "Arithmetic side result for fixed-budget signed-moment certification. It determines when the available lower bound is sharp and when a stronger bound is required; no physical supplier is supplied.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first verified equality classification. Do not pursue the optimum at other budgets or the larger-support problem.",
+  "outcome": "completed",
+  "evidence": "PROOF.md and standalone exact verify.py; registered warning-strict normal and optimized commands. Runtime receipts enumerate checks and bind the six package files.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "What is the exact minimum window width at normalized budgets outside the classified set?",
+      "why_it_matters": "The published discrete lower bound is then unattainable, so it does not give the exact fixed-budget optimum.",
+      "first_step": "Minimize the exact rational Delta/z^2 under the quadratic endpoint and count inequalities, and certify the integer optimum.",
+      "blocked_by": "No all-budget integer optimization theorem is supplied by this equality classification."
+    }
+  ]
+}

research/hidden-window-attainment-budgets/VERIFY.json

@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "New equality classification against two exact finite oracles, signed profile construction, floors/padding, endpoint and semantic rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Repeat all checks under optimized Python with explicit contracts active."
+    }
+  ]
+}