Five ranks suffice to hide a losing κ interval from every fixed sampling grid

docs/ci-verification.md

@@ -1,6 +1,23 @@
 # CI verification
 
-## Current selected-family replay: #5599
+## Current selected-family replay: #6030
+
+The [selected record](../certificates/selected-result.json) binds conditional
+κ = 0.003125804 to the [proof review](research/pr-intake-evidence/pr6030-audit/PROOF-REVIEW.md),
+[validation receipts](research/pr-intake-evidence/pr6030-audit/VALIDATION.json),
+and [explicit source closure](../certificates/frontier6030-source.json).
+`make frontier6030-verify` follows that source-bound selected replay. The review
+separates retained normal primary macOS/Linux evidence from fresh independent
+word/invoice/native, original caller, adapted caller and optimized primary checks.
+Consult its receipts for exact commands, source heads and limits; the #5599
+checkpoint below retains its own historical replay details.
+
+The five inherited framework assumptions remain. Neither the full uniform word
+nor a complete rounded multiplier is materialized. A source/metadata check is
+not an operator replay or a formal theorem proof. Routine research submissions
+do not need to rerun this selected-family replay.
+
+## Historical selected-family replay: #5599
 
 The [selected record](../certificates/selected-result.json) binds conditional
 κ = 0.00310045 to the [proof review](research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md)

docs/research/current-status.md

@@ -1,6 +1,6 @@
 # Current reviewed status
 
-Selected conditional κ: **0.003125804 = 781451/250000000**, DreamingOfClouds'
+Selected conditional κ: **0.003125804** = 781451/250000000, DreamingOfClouds'
 PR6030 on the cumulative P104 construction. The complete caller counts 13,444
 productive fields and 66,834 paid calls. The saving is about 0.81775% above the
 preceding selected PR5599 claim 0.00310045.

research/hidden-power-windows/README.md

@@ -0,0 +1,155 @@
+# Five ranks can hide a losing power window from any fixed finite grid
+
+Equal call count and rank mass, a fixed five-rank support, and favorable signs
+at every member of an arbitrarily large finite sample do not certify a favorable
+power-moment comparison. There is a losing open interval between samples.
+Five is the smallest possible support for a difference with this two-crossing
+sign pattern and the two equalities. This is a scoped algebraic theorem,
+with exact finite checks, not a supplier or new kappa.
+
+The theorem extends [Nick Petalas](https://github.com/petalas)'s one-threshold
+[PR #5174](https://github.com/CrocSwap/integer-mult-bounds/pull/5174) rank-exchange construction (pinned in SOURCES.json). The existing exact
+[root-budget tool](../../docs/research/recursive-power-variation.md) already
+handles multiple crossings; no defect in that tool is alleged. The new result
+is the sharp fixed-support impossibility of replacing a complete certificate
+by any fixed finite grid. The construction also matches any prescribed finite
+number of endpoint derivatives, with a sharp larger support bound.
+
+## Theorem and construction
+
+Let S be any finite subset of (0,1). Let J be any nonempty open subinterval
+of (0,1) avoiding S, and let h>=1 be an integer. There are two nonnegative
+integer paid profiles A,B, whose combined support consists of exactly the ranks
+
+```
+1, 2, 4, ..., 2^(2h+2),
+```
+
+whose difference F(p)=sum_r (B_r-A_r) r^p has these properties:
+
+1. F and its first h-1 derivatives vanish at both p=0 and p=1.
+2. There are alpha<beta in J with F>0 on (alpha,beta) and F<0 everywhere
+   else in (0,1), except for its two zeros alpha,beta.
+3. Their count and rank mass agree. Each has paid ranks below a common
+   productive target, so subtracting that same target changes none of the signs.
+4. The 2h+3 nonzero ranks in the difference are minimal for this sign pattern
+   and these endpoint multiplicities, among arbitrary distinct positive ranks.
+
+Choose positive rationals u=a/b and v=c/d with
+`1<u<v<2` and `[log_2 u, log_2 v]` contained in J. Such choices exist because
+p -> 2^p is continuous and strictly increasing and the rationals are dense.
+Expand the integer polynomial
+
+```
+Q(x) = (-1)^(h+1) (x-1)^h (x-2)^h (b*x-a) (d*x-c)
+     = sum_(j=0)^(2h+2) q_j x^j.
+```
+
+At rank 2^j put max(-q_j,0) calls in A and max(q_j,0) calls in B. Then
+`F(p)=Q(2^p)` exactly. For 1<x<2, the endpoint factors have sign (-1)^h.
+The two rational factors have positive product outside (u,v) and negative
+product inside. The prefactor therefore gives precisely the asserted signs.
+The substitution has nonzero derivative, so endpoint zeros have multiplicity
+exactly h and the two interior zeros are simple. Every root of Q is positive;
+its coefficients alternate and no elementary symmetric coefficient vanishes.
+Thus every one of the 2h+3 displayed ranks occurs in the difference.
+
+In particular F(0)=0 gives equal counts, and F(1)=0 gives equal rank mass M.
+Take H_M as the common productive target. Each profile has at least two
+positive terms, and the side containing the largest rank has further positive
+mass. Hence M exceeds every paid rank. The theorem supplies arithmetic
+invoices, with no assertion of a common physical implementation.
+
+### Sharp support bound
+
+A nonzero sum of s exponentials with distinct real exponents has at most s-1
+real zeros counted with multiplicity. Here is the needed elementary proof.
+For s=1 it has none. Divide by the smallest exponential, which preserves zeros.
+The derivative has at most s-1 exponential terms; by induction it has at most
+s-2 zeros. Rolle's theorem, including repeated-zero multiplicities, gives at
+least N-1 derivative zeros if the original has N zeros. Thus N<=s-1. Apply
+this on a finite interval containing any proposed set of zeros; it proves the
+same global bound. Zero coefficients are omitted first.
+
+F has at least h zeros at each endpoint and two distinct interior zeros, so
+`s-1 >= 2h+2`, or **s>=2h+3**. The construction attains equality. For h=1,
+the fixed support is {1,2,4,8,16}, independently of sample count or gap width.
+Large or narrowly placed samples can require large **multiplicities**; this
+result does not hold under a separately fixed coefficient budget.
+
+## Small explicit failed sampling construction
+
+Take h=1,u=5/4,v=3/2. Then
+
+```
+Q(x) = 8*x^4 - 46*x^3 + 97*x^2 - 89*x + 30,
+A = 89 H_2 + 46 H_8,
+B = 30 H_1 + 97 H_4 + 8 H_16.
+```
+
+Both profiles have 135 calls and rank mass 546. Their difference is negative
+at p=1/4 and 3/4 but positive at p=1/2. Exactly,
+`F(1/2)=256-181*sqrt(2)>0`, since `256^2 > 2*181^2`.
+Thus the sampled cheaper candidate is dearer inside the missed interval.
+A multiplier saving C uses p=1-C, which just reverses interval order.
+
+No finite sample set alone certifies a comparison on the entire interval;
+a proved root budget, a sign enclosure on every cell, or a structural order
+can do so. The selected source's exact interval checks are not replaced by
+this example. No sampled native search is declared invalid merely because
+it uses samples for discovery.
+
+## Evidence and reproduction
+
+```
+python3.12 -B scripts/research_package.py --package research/hidden-power-windows
+python3.12 -B scripts/check_research_commit.py --package research/hidden-power-windows
+```
+
+The standard-library verifier builds gap witnesses for every interior gap in
+uniform grids with denominator 2..24, and narrow root brackets around p=319/320 (saving .003125).
+It checks every grid sample using exact integer comparisons of factored
+rational roots, reconstructs all integer coefficients, count/mass and endpoint
+multiplicity, and verifies the hidden sign at an intervening rational exponent.
+Exponent denominators are capped at 2,048 before integer powering; the first
+authoring run exceeded its intended memory bound with a large denominator and
+was terminated, then replaced by these bounded fixtures. Higher multiplicity
+h=1..8 and independent expanded-polynomial interval checks
+on the small explicit example are included. Reversed signs, wrong roots, missing
+coefficients and false multiplicities are rejected. Normal and optimized modes
+are registered and write no package files. The written proof is uniform in S,J,h;
+the finite checks corroborate its implementation.
+
+Base: canonical main 721c03822c421b7f7fcbb2598993b947c4d88419, revision 8,
+refreshed on 2026-10-28 UTC. Full selected-supplier replay was not run. The
+optional full-source-history check refuses this shallow repository; every pin
+is at the immediate main-branch base. No full-history pass is claimed.
+
+## Significance for researchers
+
+Even a small rank alphabet with conservation laws can require an interval-wide
+power certificate. This gives a sharp adversarial fixture for proposed search
+screens and makes the missing hypothesis explicit: sample density alone is
+insufficient when integer multiplicities are unbounded. It explains when the
+power reduction in [PR #6047](https://github.com/CrocSwap/integer-mult-bounds/pull/6047) needs its ordered-spread premise.
+
+## Open next questions
+
+With a fixed maximum coefficient or total-call budget, how narrow can the hidden
+window be? First bound the separation of two rational roots of this quadratic
+interior factor at that budget, then compare general exponential sums. The
+unbounded-multiplicity theorem provides no finite-budget lower bound.
+
+Can a legal supplier realize a two-crossing exchange? Extract a source-bound
+five-rank change with a complete common boundary and all fees. These synthetic
+profiles supply no physical construction, restoration, compiler or outer admission.
+
+## Credit
+
+Prepared by [zxv](https://github.com/zxv) with substantial OpenAI Codex assistance.
+[Nick Petalas](https://github.com/petalas)'s rational-threshold construction
+supplies the polynomial-to-invoice precursor. [Ali Romman](https://github.com/aliromman)
+supplies the root-budget tool and its retained predecessors; the exponential
+zero bound, Rolle argument and polynomial factorization are classical. The
+sharp hidden-window formulation and endpoint-matching extension are the scoped
+contribution. No independent human or proof-assistant review is claimed. Apache-2.0.

research/hidden-power-windows/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "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-power-variation.md",
+      "usage": "input",
+      "git_blob": "462c6334d7881e42879a4945e636c6dd993eeb20",
+      "sha256": "62904cd17e1861edb524b60884d78b7adbf510a4b06490e0a64c4acdc8c1ccf1"
+    },
+    {
+      "path": "research/rational-threshold-rank-exchange/README.md",
+      "usage": "input",
+      "git_blob": "6da386f0af3c35bdde4356ce140719b7103819d8",
+      "sha256": "7b0fdef1cc7d9e8c6b93ac4fc11081ba85e6d043a085645863457ac98d803827"
+    }
+  ]
+}

research/hidden-power-windows/TASK.json

@@ -0,0 +1,79 @@
+{
+  "schema_version": 1,
+  "task_id": "coverage-law-change",
+  "priority_revision": 8,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "original_card": {
+    "id": "coverage-law-change",
+    "question": "Can a completed call earn more independent productive target credit without an offsetting paid bill?",
+    "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"
+    ],
+    "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": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.",
+    "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": "Use #5599 as a completed positive control, then choose one uncovered cut/module beyond an applicable frozen exclusion. Derive independence, saturation and chronological availability rather than counting rational rank alone. Price target credits and all new jobs together, then check compiler and actual caller compatibility. Stop on a nonphysical credit or an unfavorable complete relaxation.",
+    "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": [
+      "target credit",
+      "helper split",
+      "coverage law"
+    ],
+    "existing_checks": [
+      {
+        "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": "Sharp minimal-support hidden power window theorem for arbitrary finite exponent samples and endpoint multiplicity constraints.",
+  "scope_change_reason": "Accounting side theorem under the lateral-thinking assignment; not a physical target-split construction.",
+  "bottleneck_link": "Identifies when sampled moment screening cannot establish an interval-wide gain even under conservation laws.",
+  "budget_minutes": 15,
+  "stop_rule": "Uniform proof plus bounded exact witnesses; no wider physical search.",
+  "outcome": "completed",
+  "evidence": "README.md proof and verify.py exact integer/rational checks.",
+  "author": "zxv (https://github.com/zxv), with substantial OpenAI Codex assistance",
+  "ai_assistance": "Substantial OpenAI Codex assistance.",
+  "open_questions": [
+    {
+      "question": "What window-width bound follows from bounded call multiplicities?",
+      "why_it_matters": "Could justify a finite-budget interval search resolution.",
+      "first_step": "Bound rational-root separation for the displayed quadratic factor.",
+      "blocked_by": "No multiplicity budget is fixed in this theorem."
+    },
+    {
+      "question": "Can a legal supplier realize a two-crossing five-rank exchange?",
+      "why_it_matters": "Would test the phenomenon in a physical search family.",
+      "first_step": "Extract one source-bound complete five-rank edit.",
+      "blocked_by": "Synthetic profiles provide no implementation or common boundary."
+    }
+  ]
+}

research/hidden-power-windows/VERIFY.json

@@ -0,0 +1,33 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "docs/research/recursive-power-variation.md",
+    "research/rational-threshold-rank-exchange/README.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact polynomial identities, endpoint multiplicities, hidden windows and every sample in grids through denominator 24, narrow current-saving fixtures, rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Identical checks with assertions disabled."
+    }
+  ]
+}