[petalas]

Result

Claim type: scoped proof with an exhaustive finite certificate. No new κ, no supplier admission, no selected-frontier change. It is not a search failure and not a complete multiplication theorem.

It answers the open question of CubeJerry's merged #6972 (research/core-production-nonempty): whether its uniform guard S >= e(6W+1), L >= 12W+2 can be sharpened on dyadic aligned sections (N = S+e and L powers of two, every window starting at a multiple of L). Write e = 2^j t with t odd, N = 2^n, L = 2^l, and assume S >= e(6W+1).

1. Exact classification. All aligned windows of length L have longest selected run M > 6W if and only if (I) l >= n-j+1; or (II) l = n-j and (t >= 3 or L >= 12W+2); or (III) l <= n-j-1 and (t+1)L > t(12W+3). The odd part t of e and n-j decide, not S/e. The source's holes repeat with period N/2^j, and in case (III) their offsets modulo L are exactly the nearest integers to L rho/t.
2. Single-hole band. For any window (aligned or not) of length L >= 6W+1: bad iff it contains a hole at offset in [L-1-6W, 6W], and such a hole is automatically alone in its window.
3. The length threshold cannot be lowered on dyadic sections. For every W >= 1 and every power of two L <= 12W there is a dyadic instance with S >= e(6W+1) in which every aligned window of length L is bad. For L <= 6W, this follows from M <= L. For 6W+2 <= L <= 12W, take N = 8L, e = N/L = 8: each aligned window has one hole at offset L/2 and M = L/2. So L >= 12W+2 is exactly the universal dyadic length condition.
4. It does sharpen for particular e. For e a power of two in case (III), L >= 6W+2 is necessary and sufficient, half the uniform length. At W = 1 that is L = 8 instead of 16; the table of least dyadic L per odd part is in the README.
5. Neither adverse family of Research: Nonempty production windows #6972 is dyadic (odd length 12W+1; odd period 18W+5). In a dyadic instance S = e(6W+1)-1 never occurs.

The proofs are in PROOF.md, written by hand.

Evidence

verify.py is standard-library only. Its independent oracle is a literal coordinate walk of q(j) = j + floor(e j/S + 1/2).

• Oracle fidelity: the literal walk equals Research: Nonempty production windows #6972's closed-form longest run on all 72,611 ordinary windows with S <= 22 (the pinned guard.py bytes are hash-checked). This checks my model of M; it does not re-check Research: Nonempty production windows #6972's carve theorem.
• Hole formula, cell lengths and run formula: 400 pairs (S,e) with S >= 2e, S <= 40, 273,910 windows.
• Periodicity of the hole pattern for every e < N, N = 2^n <= 4096: 8,178 cases.
• Band criterion and the closed form of Theorem 2 against the oracle, every e with N >= 8e, every l, every allowed W: 2,070 cases for N <= 256 (1,415 bad) with the literal walk, and 90,820 cases for 512 <= N <= 4096 (57,364 bad) from the validated hole list. Zero disagreements.
• 1,858 of the latter cases are exactly admissible with L < 12W+2 (1,260 with t = 1, 598 with t >= 3).
• Theorem 3's family, checked literally for W <= 64 (495 families); the parity remark for W <= 200.
• Seven wrong variants (threshold 12W+2; case II merged; e in place of its odd part; uniform guard only; case II always admissible; band end shifted by one in each direction) each contradict the oracle in at least one case, so the test domain separates them from the truth.

Reproduction

From the repository root. Local interpreter: CPython 3.12.15 at ~/git/integer-mult-bounds/.venv/bin/python3.12.

~/git/integer-mult-bounds/.venv/bin/python3.12 -I -B research/dyadic-aligned-window-guard/verify.py
~/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -B research/dyadic-aligned-window-guard/verify.py
~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/dyadic-aligned-window-guard
~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/dyadic-aligned-window-guard --check-source-history

Local verification at f4314807884fdddd8727a55285ed5442b865306c with CPython 3.12.15 passed all four reproduction commands above. Both registered commands and both direct runs printed PASS_DYADIC_ALIGNED_WINDOW_GUARD; the runner printed PASS_REGISTERED_RESEARCH_PACKAGE research/dyadic-aligned-window-guard outcome=completed; the commit check printed PASS_RESEARCH_COMMIT_BYTES. The normal and optimized direct checks each completed in under 3 seconds, and the registered runner completed in under 6 seconds. Each registered command has a 120-second timeout.

Commit ed5835451d21335d283ad1236cba43293e6fc076 only clarifies the README's summary of Theorem 3: the e = N/L witness applies for 6W+2 <= L <= 12W; the smaller lengths use M <= L. The proof already distinguishes these cases. The proof, verifier, manifests and pinned inputs are unchanged. The commit-byte/source-history check passed again at this head.

Limitations and unrun obligations

• Everything is under S >= e(6W+1), i.e. floor(S/e) >= 6W+1. Dyadic instances below it are not classified here.
• Research: Nonempty production windows #6972's equivalence "interior nonempty iff M > 6W", its cap and width admissions, source accuracy, the complementary gap N-L >= W in applications, and every numerical, compiler and native obligation are cited and untouched.
• The finite check covers N <= 4096 for the classification and W <= 64 for the sharpness family; the all-n statements rest on the written proofs (Lemma P and Theorems 1 to 3). No proof-kernel check was run and no independent human review is claimed.
• In Research: Nonempty production windows #6972's own asymptotic family (L >= p^400, W = O(sqrt(p) polylog p)), L already exceeds 12W+2, so this classification changes nothing there. It decides finite short dyadic sections, and so says exactly which of them are genuinely empty.

Open next questions

1. Which aligned windows fail in dyadic instances with floor(S/e) <= 6W? This is the S/e half of the guard. First step: repeat the hole-offset method with internal cells of length 6W or 6W+1 and test which aligned windows contain no (6W+1)-cell. Blocker: those cells form a Sturmian pattern whose offsets modulo L need a separate argument.
2. What replaces the periodicity lemma when N is not a power of two but L | N? First step: for N = 2^a b with b odd, test whether the holes repeat with period N/2^j times a factor of b.
3. Can the exact list of empty short aligned sections feed the zero-dimensional branch of Research: Nonempty production windows #6972's open question 3? First step: take one bad section, for example W = 1, L = 8, e = 8, N = 64, through the source, numerical, ownership and cost contracts. Blocker: no native empty-interior service exists in either package.

Related open work

The earlier title/body search covered all 466 then-open PRs for core-production-nonempty, #6972, longest selected run, capped carve, dyadic aligned windows and nonempty interior, and found no related open result. This search coverage is not proof of novelty.

The final own-account check read the open PRs created since the CLAIM at 2026-11-10 22:14:26 UTC. The six other PRs are #7132 (BIT stock fit threshold), #7134 (odd-rectangle residual rank), #7135 (net-split quotient staircase), #7167 (P104 frame-indicator hosting), #7168 (E8 Gram-class deletion minimum) and #7169 (one-sided completion at a fixed first-failure boundary). Their titles and bodies study different objects and quantities. No shared numerical result requires comparison.

Credit

Produced by Nick Petalas. The source rule, the longest-run formula, the carve equivalence and the guard S >= e(6W+1), L >= 12W+2 are CubeJerry's #6972, with the lineage credited there. New work is Apache-2.0.

CI notes

At head ed5835451d21335d283ad1236cba43293e6fc076, run 42983300354, plan job 130398516852, failed in Onboarding helper tests on exactly test_research_current_status.CurrentCiNavigationTests.test_current_ci_section_matches_selected_record. The log reports 760 tests, one failure and 24 skipped. Its assertion cannot find `make frontier7000-verify` in docs/ci-verification.md, whose current section still describes #6030 and make frontier6030-verify.

The package replay job 130400298460 was skipped after plan failed. CI certified nothing for this package at ed5835451d21335d283ad1236cba43293e6fc076. The result and finite checks retain the local evidence and limitations above.

At head f4314807884fdddd8727a55285ed5442b865306c, run 42914729845, plan job 130174114868, failed in Onboarding helper tests on exactly test_research_current_status.CurrentCiNavigationTests.test_current_ci_section_matches_selected_record. The log reports 760 tests, one failure and 24 skipped. The assertion was that 'make frontier7000-verify' was absent from docs/ci-verification.md.

The mismatch is present on canonical main e54523517d0f03e58352e647c403a5af3e525a57: certificates/selected-result.json specifies make frontier7000-verify, while the current section of docs/ci-verification.md describes #6030 and make frontier6030-verify. This PR changes neither file nor the failing test.

The job logs of run 42905094314, run 42903313790, #7132's run 42914704054, #7134's run 42914997118, and #7135's run 42914936342 each show the same failing test, missing command and 760-test summary with one failure and 24 skipped.

The package replay job was also skipped at the original head. CI certified nothing for this package at f4314807884fdddd8727a55285ed5442b865306c either. The evidence above is local. No failed job was rerun and no repository-level CI fix is included.