Classify dyadic aligned windows of the capped source guard and prove its length bound sharp (no κ)

research/dyadic-aligned-window-guard/PROOF.md

@@ -0,0 +1,174 @@
+# Exact admission of dyadic aligned target windows
+
+Produced by Nick Petalas. **Scoped proof with an exact finite check. No new κ,
+no supplier admission, no change to the selected frontier.** Apache-2.0.
+
+## 0. What is cited and what is new
+
+CubeJerry's merged [PR #6972](https://github.com/CrocSwap/integer-mult-bounds/pull/6972)
+(`research/core-production-nonempty`) supplies, and this document **cites without
+replaying**:
+
+* the source rule `q(j) = j + floor(e j / S + 1/2)`, `N = S + e`, with the other
+  target coordinates identity holes;
+* its Section 3: for an integer width `W >= 1`, the unchanged capped carve has a
+  nonempty interior in a target window **iff** the longest selected run `M` of that
+  window exceeds `6W`;
+* its Section 4 guard (6): `S >= e(6W+1)` and `L >= 12W+2` give `M > 6W` in every
+  ordinary window of length `L`, with one-unit adverse families for arbitrary
+  integer windows. It leaves open whether a sharper guard exists for dyadic aligned
+  sections (`N`, `L` powers of two, every window starting at a multiple of `L`).
+
+New here: an exact classification of the dyadic aligned family, and the answer to
+that question. A window with `M > 6W` is called **good**, otherwise **bad**.
+
+**Hypothesis (G).** `S >= e(6W+1)`, equivalently `N >= e(6W+2)`. It implies
+`S >= 7e >= 2e` and `floor(S/e) >= 6W+1`.
+
+**Dyadic notation.** `N = 2^n`, `L = 2^l` with `0 <= l <= n`, aligned windows
+`[kL, (k+1)L)`. Write `e = 2^j t` with `t` odd; then `j < n`, and put `g = 2^(n-j)`.
+
+## 1. Holes and runs
+
+**Lemma 1.** If `S >= 2e`, the unselected coordinates ("holes") are exactly
+`H_c = ceil(S(2c-1)/(2e)) + c - 1 = floor(((2c-1)N + e - 1)/(2e))`, `1 <= c <= e`.
+Consecutive holes differ by `floor(N/e)` or `ceil(N/e)`, so the selected cell between
+two consecutive holes has length `floor(S/e)` or `ceil(S/e)`.
+
+*Proof.* Put `phi(j) = floor(e j/S + 1/2)`. Then `phi(j) >= c` iff `j >= A_c :=
+ceil(S(2c-1)/(2e))`, `phi(0) = 0`, and `phi` rises by at most 1 per step because
+`e < S`. So `q` is strictly increasing with steps 1 or 2, and a step of 2 occurs
+exactly into `j = A_c`, skipping `q(A_c - 1) + 1 = A_c + c - 1`. The index `A_e`
+is at most `S - 1` iff `S >= 2e`, which gives `q(S-1) = N - 1`; with `q(0) = 0` there
+are no holes before the first or after the last selected coordinate. This gives the
+`e` holes `H_c = A_c + c - 1`. Since `2(c-1) = u - 1` for `u = 2c-1`,
+`H_c = ceil((uS + e(u-1))/(2e)) = ceil((uN - e)/(2e)) = floor((uN + e - 1)/(2e))`.
+Finally `A_(c+1) - A_c = ceil(x + S/e) - ceil(x) in {floor(S/e), ceil(S/e)}`. ∎
+
+**Lemma 2.** Let a window of length `L` inside `[0,N)` contain `r` holes at offsets
+`p_1 < ... < p_r`. If `r = 0` then `M = L`. Otherwise `M` is the largest of
+`p_1`, `p_(i+1) - p_i - 1`, and `L - 1 - p_r`. Under (G): `r >= 2` implies
+`M >= floor(S/e) >= 6W+1`; `r = 1` gives `M = max(p, L-1-p)`.
+
+*Proof.* The selected coordinates of the window are its non-holes, and `M` is the
+longest stretch between consecutive marks (window ends and holes). Two consecutive
+holes enclose a whole cell of length at least `floor(S/e)` (Lemma 1). ∎
+
+## 2. The single-hole band
+
+**Theorem 1.** Assume (G) and a window of length `L >= 6W+1`. Let
+`B = [L-1-6W, 6W]` (empty when `L >= 12W+2`). The window is bad iff it contains a hole
+whose offset lies in `B`. If `L <= 6W`, every window is bad.
+
+*Proof.* If `L <= 6W` then `M <= L <= 6W`. Let `L >= 6W+1`. If the window is bad then
+`r = 0` is impossible (`M = L`), and `r >= 2` is impossible (Lemma 2), so `r = 1`, and
+`max(p, L-1-p) <= 6W` says `p in B`. Conversely let a hole sit at offset `p in B`. A
+second hole in the window would be at distance at least `floor(N/e) = floor(S/e)+1 >=
+6W+2` from the first. Above it, its offset would be at least `(L-1-6W) + 6W + 2 = L+1`;
+below it, at most `6W - (6W+2) = -2`. Both are outside the window, so `r = 1` and
+`M = max(p, L-1-p) <= 6W`. ∎
+
+**Corollary 1.** Under (G) and `L >= 6W+1`, all aligned windows of length `L` are good
+iff no hole `H_c` satisfies `H_c mod L in B`. (Hole `H_c` lies in the aligned window
+`k = floor(H_c / L)` at offset `H_c mod L`.) For `L >= 12W+2` the band is empty and every
+aligned window is good, which is #6972's length condition for dyadic sections.
+
+## 3. Periodicity of the hole pattern
+
+**Lemma P.** For `e = 2^j t` with `t` odd and `N = 2^n`, put `g = N/2^j`. Then
+`H_(c+t) = H_c + g` for `1 <= c <= e - t`. Under (G), `H_t < g`, so block
+`[ig, (i+1)g)` contains exactly the `t` holes `H_(it+1), ..., H_((i+1)t)`, the same
+pattern in every block.
+
+*Proof.* With `u = 2c-1`, `N = 2^j g`, `e = 2^j t`:
+`(uN + e - 1)/(2e) = (ug + t - 2^(-j))/(2t)`. For an integer `m` and `0 < d <= 1`,
+`floor((m - d)/(2t)) = floor((m-1)/(2t))`, because no multiple of `2t` lies in
+`(m-1, m)`. Hence `H_c = floor((ug + t - 1)/(2t))`. Replacing `u` by `u + 2t` (that is,
+`c` by `c + t`) adds `g`. Also `H_t < g` iff `(2t-1)g + t - 1 < 2tg` iff `t - 1 < g`,
+which holds because (G) gives `g >= t(6W+2)`. ∎
+
+## 4. The classification
+
+**Theorem 2.** Let `N = 2^n`, `1 <= e < N`, `e = 2^j t` with `t` odd, `L = 2^l` with
+`0 <= l <= n`, `W >= 1`, and assume (G). All aligned windows of length `L` are good 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)`.
+
+*Proof.* **(I)** `L >= 2g`: an aligned window is a union of `L/g >= 2` blocks, so it
+holds at least `2t >= 2` holes and is good by Lemma 2.
+
+**(II)** `L = g`: the aligned windows are the blocks. If `t >= 3` each holds at least
+three holes: good. If `t = 1` each holds the single hole `H_1 = floor(g/2) = L/2` at
+offset `L/2`, so `M = L/2`, good iff `L >= 12W+2`.
+
+**(III)** `L` divides `g/2`, so the aligned windows split each block into `g/L >= 2`
+windows, and the offsets of all holes modulo `L` are those of block 0:
+`R = {H_c mod L : 1 <= c <= t}`. Write `g = 2Lm` with `m = 2^(n-j-l-1)` and `u = 2c-1`.
+By Lemma P, `H_c = floor(Lmu/t + (t-1)/(2t))`. Writing `mu = tq + rho` with
+`0 <= rho < t`, `H_c = Lq + floor(L rho/t + (t-1)/(2t))`, and for `t` odd
+`floor(L rho/t + (t-1)/(2t))` is the nearest integer `nu(rho)` to `L rho/t`: with
+`L rho = kt + s` it equals `k + [2s >= t+1]`, and `s = t/2` cannot occur. As `c` runs
+over `1..t`, `u = 2c-1` runs over all residues modulo `t` (2 is a unit), hence so does
+`rho = mu mod t` (`m` is a power of 2, a unit). Therefore
+`R = { nu(rho) mod L : 0 <= rho < t }`.
+Because `nu(t - rho) = L - nu(rho)` (no ties), `R` is symmetric under `r -> L - r`.
+
+Now apply Corollary 1.
+
+* `L <= 6W`: every window is bad, and the inequality `(t+1)L > t(12W+3)` fails, since
+  `(t+1)L <= 6W(t+1) <= t(12W+3)`.
+* `L >= 12W+2`: every window is good by Corollary 1. A power of two is even and `12W+2`
+  is not a power of two for `W >= 1`, so `L >= 12W+4` and
+  `(t+1)L >= (t+1)(12W+4) > t(12W+3)`.
+* `6W+1 <= L <= 12W` (a power of two is not `12W+1`, which is odd, nor `6W+1`): put
+  `nu_max = nu((t-1)/2)`, the largest `nu(rho)` with `rho <= (t-1)/2`; all of them are at
+  most `L/2 <= 6W`. A lower-half residue `r = nu(rho)` lies in `B` iff `r >= L-1-6W`
+  (its upper end `6W` is automatic). An upper-half residue `r = L - s`, `s = nu(rho)`
+  with `1 <= s <= L/2`, lies in `B` iff `L-6W <= s <= 6W+1`, that is iff `s >= L-6W`,
+  which implies `s >= L-1-6W`. Hence `R` meets `B` iff `nu_max >= L-1-6W`. Now
+  `L - nu_max = D` := the nearest integer to `L(t+1)/(2t)`, so `R` meets `B` iff
+  `D <= 6W+1`. All windows are therefore good iff `D >= 6W+2` iff
+  `L(t+1)/(2t) > 6W + 3/2` (equality would force `t | L`, so `t = 1`, and then
+  `L(t+1)/(2t) = L` is an integer) iff `(t+1)L > t(12W+3)`. ∎
+
+**Corollary 2 (the guard for dyadic aligned windows).** Under (G): `L >= 12W+2` always
+admits (so #6972's length condition holds on dyadic sections); for `e = 2^j` (`t = 1`)
+with `l <= n-j-1`, `L >= 6W+2` is necessary and sufficient, half of the uniform length;
+for `t >= 3` in case (III) the least admissible `L` is the least power of two with
+`L > t(12W+3)/(t+1)`, which tends to `12W+3` as `t` grows. The odd part `t` of `e`
+and `n - j` decide, not `S/e`.
+
+## 5. The uniform length threshold cannot be lowered on dyadic sections
+
+**Theorem 3.** For every `W >= 1` and every power of two `L <= 12W` there is a dyadic
+instance satisfying (G) and `N - L >= W` in which every aligned window of length `L` is
+bad. So no dyadic `L <= 12W` is admissible uniformly in `e`; the least admissible
+dyadic length is the least power of two `>= 12W+2`, exactly the length condition of
+#6972's guard.
+
+*Proof.* If `L <= 6W`, any instance with (G) works (`M <= L <= 6W`), for example
+`e = 1` and `N` a power of two with `N >= 6W+2`. A power of two is never `6W+1`. If
+`6W+2 <= L <= 12W`, take `N = 8L`, `e = N/L = 8`: (G) holds because `L >= 6W+2`, and
+`H_c = (2c-1)L/2` exactly, one hole at offset `L/2` in every window, so `M = L/2 <= 6W`
+in all windows, with `N - L >= L >= W`. ∎ (This is case (II) with `t = 1`; the verifier
+checks this family literally for `W <= 64`.)
+
+**Remark (the two adverse families of #6972 are not dyadic).** The first has length
+`L = 12W+1`, odd. The second has `N = 18W+5`, odd. In a dyadic instance `N` and `e(6W+2)`
+are both even, so `S = e(6W+1) - 1` never occurs, and `S >= e(6W+1)` is the same as
+`S >= e(6W+1) - 1`. Whether an aligned window can fail for a dyadic instance with
+`floor(S/e) <= 6W` is not settled here (Open next questions).
+
+## 6. What is not claimed
+
+* The equivalence "interior nonempty iff `M > 6W`", the cap and width admissions, source
+  accuracy, `N - L >= W` in applications, row gaps and every native, compiler or
+  precision obligation are #6972's or remain open; none is touched.
+* Everything here is under (G), i.e. `floor(S/e) >= 6W+1`. Instances with
+  `floor(S/e) <= 6W` are outside; they are not shown to fail or to succeed.
+* The proofs above are written by hand. The finite check (`verify.py`) corroborates them
+  but is not a proof; no proof-kernel check was run and no independent human review is
+  claimed.

research/dyadic-aligned-window-guard/README.md

@@ -0,0 +1,114 @@
+# An exact guard for dyadic aligned target windows
+
+**Scoped proof with an exact finite check. No new κ, no supplier admission; the
+selected frontier is unchanged.**
+
+CubeJerry's merged [PR #6972](https://github.com/CrocSwap/integer-mult-bounds/pull/6972)
+(`research/core-production-nonempty`) shows that the capped carve has a nonempty
+interior in a target window iff the longest selected run `M` exceeds `6W`, and that
+`S >= e(6W+1)` with `L >= 12W+2` admits every original start. Its open question 2 asks
+whether a sharper guard exists for **dyadic aligned sections**: `N = S+e` and the
+window length `L` powers of two, every window starting at a multiple of `L`.
+This package answers it in full for the length half of the guard.
+
+## Results
+
+Write `e = 2^j t` with `t` odd, `N = 2^n`, `L = 2^l`, and assume `S >= e(6W+1)`.
+
+1. **Exact classification (Theorem 2).** All aligned windows of length `L` have
+   `M > 6W` if and only if one of: **(I)** `l >= n-j+1`; **(II)** `l = n-j` and (`t >= 3`
+   or `L >= 12W+2`); **(III)** `l <= n-j-1` and `(t+1) L > t(12W+3)`. The deciding data
+   are the odd part `t` of `e` and `n-j`, not `S/e`. The proof reduces to where the
+   `e` holes of the source sit modulo `L`: they repeat with period `N/2^j`, and in
+   case (III) their offsets modulo `L` are exactly the nearest integers to `L rho/t`.
+2. **The single-hole band (Theorem 1).** Under `S >= e(6W+1)`, a window of length
+   `L >= 6W+1` is bad iff it holds a hole at offset in `[L-1-6W, 6W]`; such a hole is
+   automatically the only one in its window. This holds for every window, aligned or not.
+3. **The length threshold cannot be lowered (Theorem 3).** 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 of #6972's guard.
+4. **The guard 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. Least dyadic `L`
+   in case (III), generated by `verify.py`:
+
+   | W | uniform 12W+2 | t=1 | t=3 | t=5 | t=7 | t=9 | t=11 | t=13 | t=15 |
+   |---|---|---|---|---|---|---|---|---|---|
+   | 1 | 16 | 8 | 16 | 16 | 16 | 16 | 16 | 16 | 16 |
+   | 2 | 32 | 16 | 32 | 32 | 32 | 32 | 32 | 32 | 32 |
+   | 3 | 64 | 32 | 32 | 64 | 64 | 64 | 64 | 64 | 64 |
+   | 4 | 64 | 32 | 64 | 64 | 64 | 64 | 64 | 64 | 64 |
+   | 5 | 64 | 32 | 64 | 64 | 64 | 64 | 64 | 64 | 64 |
+   | 6 | 128 | 64 | 64 | 64 | 128 | 128 | 128 | 128 | 128 |
+
+5. **Neither adverse family of #6972 is dyadic.** One has odd length `12W+1`, the other
+   odd period `18W+5`. In a dyadic instance `S = e(6W+1)-1` never occurs.
+
+[PROOF.md](PROOF.md) has the statements and proofs.
+
+## Evidence
+
+`verify.py` uses a literal coordinate walk of `q(j) = j + floor(e j/S + 1/2)` as the
+independent oracle. All counts below are reproduced by the script.
+
+| Check | Coverage |
+|---|---|
+| Oracle fidelity | The literal walk equals #6972's closed-form longest run on all 72,611 ordinary windows with `S <= 22` (the pinned `guard.py` is hash-checked) |
+| Lemmas 1 and 2 | Hole formula, cell lengths and run formula against the literal walk: 400 pairs `(S,e)` with `S >= 2e`, `S <= 40`, 273,910 windows |
+| Lemma P | The periodicity `H_(c+t) = H_c + N/2^j` for every `e < N`, `N = 2^n <= 4096`: 8,178 cases |
+| Theorems 1 and 2, literal | Every `e` with `N >= 8e`, every `l`, every allowed `W`, for `N <= 256`: 2,070 cases, 1,415 bad; the band criterion and the closed form both equal the oracle |
+| Theorems 1 and 2, hole list | The same for `512 <= N <= 4096`: 90,820 cases, 57,364 bad |
+| Gain over the uniform length | 1,858 of those cases are exactly admissible with `L < 12W+2` (1,260 with `t = 1`, 598 with `t >= 3`) |
+| Theorem 3 | 495 families for `W <= 64`, checked literally; parity remark for `W <= 200` |
+| Controls | Seven wrong variants (threshold `12W+2`, case II merged, `e` for 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 |
+
+The check runs in about 6 seconds.
+
+## Reproduce
+
+From the repository root, with CPython 3.12:
+
+```sh
+python3.12 -I -B research/dyadic-aligned-window-guard/verify.py
+python3.12 -I -O -B research/dyadic-aligned-window-guard/verify.py
+python3.12 -B scripts/research_package.py --package research/dyadic-aligned-window-guard
+```
+
+Each verifier run ends with `PASS_DYADIC_ALIGNED_WINDOW_GUARD`; add `--json` for the
+certificate.
+
+## Scope and limits
+
+Everything is under `S >= e(6W+1)`, that is `floor(S/e) >= 6W+1`. The equivalence
+"interior nonempty iff `M > 6W`", the cap and width admissions, source accuracy,
+`N - L >= W` in applications and every native, compiler and precision obligation stay
+as in #6972. In #6972's asymptotic family (`L >= p^400`, `W = O(sqrt(p) polylog p)`) the
+length `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. The proofs are written by hand; the finite check corroborates them and is not a
+proof. No proof-kernel check was run and no independent human review is claimed.
+
+## Open next questions
+
+1. **Dyadic instances with `floor(S/e) <= 6W`.** Which aligned windows fail there?
+   Why it matters: this is the `S/e` half of the guard, which this package does not
+   touch; the parity remark shows #6972's one-unit family never occurs dyadically, but
+   the next case `S = e(6W+1)-2` is open. First step: apply the same hole-offset
+   method with internal cells of length `6W` or `6W+1`, and test which aligned windows
+   see no `(6W+1)`-cell. Blocker: the positions of the `(6W+1)`-cells form a Sturmian
+   pattern whose offsets modulo `L` need a separate argument.
+2. **Aligned windows when `N` is not a power of two.** The periodicity lemma uses
+   `N = 2^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`. Blocker: `L | N` then no longer forces
+   the residues to depend only on `t` and `L`.
+3. **Use in #6972's open question 3.** The classification names the empty short
+   aligned sections exactly; whether the zero-dimensional branch can be implemented at
+   those sections is a native question, outside this package.
+
+## Credit
+
+Produced by Nick Petalas. The source rule, the longest-run formula, the carve
+equivalence `interior nonempty iff M > 6W` and the guard `S >= e(6W+1)`, `L >= 12W+2`
+are CubeJerry's PR #6972, with the lineage credited there. New work is Apache-2.0.

research/dyadic-aligned-window-guard/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8",
+      "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/core-production-nonempty/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "596ac2951fffd910e1a20ca2c4a5533037962fd3",
+      "sha256": "5b5fece3bc8966c1d9b4558a0bb62fdd914d0028c903d637f832e8439b9db85a"
+    },
+    {
+      "path": "research/core-production-nonempty/guard.py",
+      "usage": "input",
+      "git_blob": "5f72c9aca81dbda4b3820b4adfe36e3eb3bd9541",
+      "sha256": "93e361ae536129a3ace39edbeed404decf2930d0547ce9fc119bccded32eacab"
+    }
+  ]
+}