diff --git a/research/dyadic-aligned-window-guard/PROOF.md b/research/dyadic-aligned-window-guard/PROOF.md new file mode 100644 index 0000000000..5728679164 --- /dev/null +++ b/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. diff --git a/research/dyadic-aligned-window-guard/README.md b/research/dyadic-aligned-window-guard/README.md new file mode 100644 index 0000000000..23e8b2b42c --- /dev/null +++ b/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. diff --git a/research/dyadic-aligned-window-guard/SOURCES.json b/research/dyadic-aligned-window-guard/SOURCES.json new file mode 100644 index 0000000000..b5857683a4 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/dyadic-aligned-window-guard/TASK.json b/research/dyadic-aligned-window-guard/TASK.json new file mode 100644 index 0000000000..1b2876bdab --- /dev/null +++ b/research/dyadic-aligned-window-guard/TASK.json @@ -0,0 +1,95 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "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": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "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": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "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": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "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 exactly when every aligned window of a dyadic instance (N = S+e and L powers of two, starts divisible by L) of the capped Gaussian source has longest selected run above 6W, under S >= e(6W+1); answer whether the uniform length condition L >= 12W+2 of research/core-production-nonempty can be sharpened on dyadic sections.", + "scope_change_reason": "The card asks whether one of the five inherited assumptions can be proved at its actual caller. This package settles one source-geometry question left open by PR6972 (dyadic aligned sections of its guard). It discharges no inherited assumption and proves nothing about the numerical, compiler or native obligations.", + "bottleneck_link": "Side result on source geometry for analytic_recovery and compiler: PR6972 needs the source partition at every original complete context. This decides exactly which dyadic aligned sections have a nonempty interior and which are empty, for the length half of its guard.", + "budget_minutes": 60, + "stop_rule": "Stop after the exact classification, the sharpness theorem and one exhaustive finite check; do not extend to non-dyadic periods or to S/e below 6W+1.", + "outcome": "completed", + "evidence": "research/dyadic-aligned-window-guard/verify.py prints PASS_DYADIC_ALIGNED_WINDOW_GUARD; PROOF.md gives Theorems 1 to 3.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Which aligned windows fail in dyadic instances with floor(S/e) <= 6W?", + "why_it_matters": "This is the S/e half of the guard in PR6972; its one-unit adverse family never occurs dyadically (N would be odd), and the next case S = e(6W+1)-2 is untouched here.", + "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.", + "blocked_by": "The positions of the (6W+1)-cells form a Sturmian pattern; their offsets modulo L need a separate argument." + }, + { + "question": "What replaces the periodicity lemma when N is not a power of two but L divides N?", + "why_it_matters": "The Core's actual periods need not be powers of two; the classification then no longer applies as stated.", + "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.", + "blocked_by": "L | N no longer forces the hole offsets modulo L to depend only on the odd part of e and on L." + }, + { + "question": "Can the classification of empty short aligned sections be used for the zero-dimensional branch of PR6972's open question 3?", + "why_it_matters": "It names exactly which aligned short sections are genuinely empty.", + "first_step": "Take one bad aligned section from verify.py (for example W = 1, L = 8, e = 8, N = 64) and trace it through the source, numerical, ownership and cost contracts.", + "blocked_by": "No native empty-interior service is supplied by either package." + } + ] +} diff --git a/research/dyadic-aligned-window-guard/VERIFY.json b/research/dyadic-aligned-window-guard/VERIFY.json new file mode 100644 index 0000000000..613541ce98 --- /dev/null +++ b/research/dyadic-aligned-window-guard/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/core-production-nonempty/guard.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Literal coordinate walk against the cited longest-run formula (72,611 windows), hole and run lemmas, periodicity, the single-hole band and the closed-form classification for every dyadic N <= 4096, the sharpness family, the parity remark, and seven rejected wrong variants." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat with assertions disabled (the checker uses explicit need() calls)." + } + ] +} diff --git a/research/dyadic-aligned-window-guard/verify.py b/research/dyadic-aligned-window-guard/verify.py new file mode 100644 index 0000000000..c86e198167 --- /dev/null +++ b/research/dyadic-aligned-window-guard/verify.py @@ -0,0 +1,440 @@ +#!/usr/bin/env python3 +"""Exact checks for the dyadic aligned-window guard (PROOF.md). + +Standard library only. Scoped finite certificate for one source-geometry statement; +no kappa, no supplier admission. Produced by Nick Petalas. Apache-2.0. + +The independent oracle is a literal coordinate walk of the source rule +q(j) = j + floor(e*j/S + 1/2). Every closed form below is compared with it, and +every mutated closed form must be rejected by the same oracle. +""" +import hashlib +import importlib.util +import json +import os +import sys +from bisect import bisect_left + +PKG = os.path.dirname(os.path.abspath(__file__)) +ROOT = os.path.dirname(os.path.dirname(PKG)) +MARK = "PASS_DYADIC_ALIGNED_WINDOW_GUARD" + + +def need(ok, message): + """Explicit check that stays active under python -O.""" + if not ok: + raise SystemExit("FAIL: " + message) + + +# ---------------------------------------------------------------- literal oracle +def literal_selected(S, e): + """Boolean list over target coordinates: True where some j has q(j) = coordinate.""" + N = S + e + sel = [False] * N + for j in range(S): + sel[j + (2 * e * j + S) // (2 * S)] = True # floor(e*j/S + 1/2) = (2ej+S)//(2S) + return sel + + +def literal_run(sel, a, length): + """Longest run of selected coordinates inside [a, a+length), by direct scan.""" + best = cur = 0 + for t in range(a, a + length): + cur = cur + 1 if sel[t] else 0 + if cur > best: + best = cur + return best + + +# ------------------------------------------------------------------ closed forms +def hole_positions(N, e): + """Lemma 1: H_c = floor(((2c-1)N + e - 1) / (2e)), c = 1..e.""" + return [((2 * c - 1) * N + e - 1) // (2 * e) for c in range(1, e + 1)] + + +def odd_part(e): + j = 0 + while e % 2 == 0: + e //= 2 + j += 1 + return j, e + + +def run_from_holes(H, a, length): + """Lemma 2: longest selected run of the window [a, a+length) from the hole list H.""" + lo = bisect_left(H, a) + hi = bisect_left(H, a + length) + if lo == hi: + return length + best = max(H[lo] - a, a + length - 1 - H[hi - 1]) + for k in range(lo + 1, hi): + d = H[k] - H[k - 1] - 1 + if d > best: + best = d + return best + + +def aligned_min_run(H, N, length): + """Minimum over the aligned windows [kL, (k+1)L) of the longest selected run.""" + best = None + i = 0 + e = len(H) + for a in range(0, N, length): + b = a + length + j = i + while j < e and H[j] < b: + j += 1 + if j == i: + m = length + else: + m = max(H[i] - a, b - 1 - H[j - 1]) + for k in range(i + 1, j): + d = H[k] - H[k - 1] - 1 + if d > m: + m = d + i = j + if best is None or m < best: + best = m + return best + + +def band_prediction(H, length, W): + """Theorem 1: with S >= e(6W+1), all aligned windows are good iff L >= 6W+1 and + no hole offset modulo L lies in [L-1-6W, 6W].""" + if length < 6 * W + 1: + return False + lo, hi = length - 1 - 6 * W, 6 * W + return not any(lo <= h % length <= hi for h in H) + + +def classify(n, e, ell, W): + """Theorem 2: are all aligned windows of length 2^ell good, for N = 2^n and e, + under the hypothesis N >= e(6W+2)? (Closed form in the odd part t of e.)""" + length = 1 << ell + j, t = odd_part(e) + m = n - j + if ell > m: # case I: every window holds two whole blocks + return True + if ell == m: # case II: windows are the blocks + return t >= 3 or length >= 12 * W + 2 + return (t + 1) * length > t * (12 * W + 3) # case III + + +def classify_mutants(): + """Deliberately wrong closed forms; each must disagree with the oracle somewhere.""" + def m_const(n, e, ell, W): # 12W+2 in place of 12W+3 + j, t = odd_part(e) + m = n - j + L = 1 << ell + if ell > m: + return True + if ell == m: + return t >= 3 or L >= 12 * W + 2 + return (t + 1) * L > t * (12 * W + 2) + + def m_no_block(n, e, ell, W): # case II treated as case III + j, t = odd_part(e) + m = n - j + L = 1 << ell + if ell > m: + return True + return (t + 1) * L > t * (12 * W + 3) + + def m_use_e(n, e, ell, W): # e in place of its odd part + j, t = odd_part(e) + m = n - j + L = 1 << ell + if ell > m: + return True + if ell == m: + return t >= 3 or L >= 12 * W + 2 + return (e + 1) * L > e * (12 * W + 3) + + def m_uniform(n, e, ell, W): # only the uniform length guard + return (1 << ell) >= 12 * W + 2 + + def m_block_free(n, e, ell, W): # case II declared always admissible + j, t = odd_part(e) + m = n - j + L = 1 << ell + if ell >= m: + return True + return (t + 1) * L > t * (12 * W + 3) + + return {"threshold 12W+2": m_const, "case II merged": m_no_block, + "odd part replaced by e": m_use_e, "uniform guard only": m_uniform, + "case II always admissible": m_block_free} + + +# ------------------------------------------------------------------------ checks +def check_pinned_source(): + """Bind the fidelity cross-check to the exact pinned #6972 file bytes.""" + with open(os.path.join(PKG, "SOURCES.json"), "rb") as f: + pins = json.load(f)["files"] + rows = {p["path"]: p for p in pins} + rel = "research/core-production-nonempty/guard.py" + need(rel in rows and rows[rel]["usage"] == "input", "guard.py is a declared live input") + with open(os.path.join(ROOT, rel), "rb") as f: + data = f.read() + need(hashlib.sha256(data).hexdigest() == rows[rel]["sha256"], "guard.py bytes match their pin") + spec = importlib.util.spec_from_file_location("pinned_guard", os.path.join(ROOT, rel)) + mod = importlib.util.module_from_spec(spec) + sys.modules["pinned_guard"] = mod # dataclass resolution needs the module registered + spec.loader.exec_module(mod) + return mod + + +def check_oracle_against_cited_formula(guard, smax=22): + """Fidelity control for the oracle: the literal walk reproduces #6972's closed-form + longest run on every ordinary window. This checks our model of M, not their theorem.""" + windows = 0 + for S in range(2, smax + 1): + for e in range(1, S): + N = S + e + sel = literal_selected(S, e) + for a in range(N): + for b in range(a + 1, N + 1): + want = guard.longest_run(guard.Window(S, e, a, b - a))["maximum"] + need(literal_run(sel, a, b - a) == want, + "literal run equals the cited formula at S=%d e=%d a=%d b=%d" % (S, e, a, b)) + windows += 1 + return windows + + +def check_lemma_holes_and_runs(smax=40): + """Lemma 1 and Lemma 2 against the literal walk on every S <= smax with S >= 2e.""" + pairs = windows = 0 + for S in range(2, smax + 1): + for e in range(1, S): + if S < 2 * e: + continue + N = S + e + sel = literal_selected(S, e) + lit_holes = [t for t in range(N) if not sel[t]] + H = hole_positions(N, e) + need(H == lit_holes, "hole formula at S=%d e=%d" % (S, e)) + cells = {H[i + 1] - H[i] - 1 for i in range(len(H) - 1)} + need(cells <= {S // e, -(-S // e)}, "cell lengths are floor/ceil of S/e at S=%d e=%d" % (S, e)) + for a in range(N): + for b in range(a + 1, N + 1): + need(run_from_holes(H, a, b - a) == literal_run(sel, a, b - a), + "Lemma 2 run at S=%d e=%d a=%d b=%d" % (S, e, a, b)) + windows += 1 + pairs += 1 + return pairs, windows + + +def check_periodicity(nmax=12): + """Lemma P for every e < N, N = 2^n: H_{c+t} = H_c + N/2^j.""" + cases = 0 + for n in range(1, nmax + 1): + N = 1 << n + for e in range(1, N): + j, t = odd_part(e) + g = N >> j + H = hole_positions(N, e) + for c in range(e - t): + need(H[c + t] == H[c] + g, "periodicity at N=%d e=%d c=%d" % (N, e, c)) + cases += 1 + return cases + + +def check_literal_aligned(nmax=8): + """Theorems 1 and 2 against the literal walk: all e and all aligned windows for + N = 2^n <= 2^nmax, every W allowed by the hypothesis N >= e(6W+2).""" + cases = bad = 0 + for n in range(1, nmax + 1): + N = 1 << n + for e in range(1, N): + S = N - e + if N < 8 * e: # no width W >= 1 satisfies the hypothesis + continue + sel = literal_selected(S, e) + H = hole_positions(N, e) + for ell in range(0, n + 1): + L = 1 << ell + m_al = min(literal_run(sel, a, L) for a in range(0, N, L)) + for W in range(1, (N - 2 * e) // (6 * e) + 1): + exact = m_al > 6 * W + need(band_prediction(H, L, W) == exact, "band criterion at N=%d e=%d L=%d W=%d" % (N, e, L, W)) + need(classify(n, e, ell, W) == exact, "classification at N=%d e=%d L=%d W=%d" % (N, e, L, W)) + cases += 1 + bad += (not exact) + return cases, bad + + +def check_hole_array_aligned(nmin, nmax): + """Same comparison from the validated hole list, for larger N. Returns counts, + including the cases where an aligned length below 12W+2 is exactly admissible.""" + cases = bad = gain = 0 + sharp_by_class = {} + for n in range(nmin, nmax + 1): + N = 1 << n + for e in range(1, N // 8 + 1): + H = hole_positions(N, e) + wmax = (N - 2 * e) // (6 * e) + if wmax < 1: + continue + j, t = odd_part(e) + for ell in range(0, n + 1): + L = 1 << ell + m_al = aligned_min_run(H, N, L) + for W in range(1, wmax + 1): + exact = m_al > 6 * W + need(band_prediction(H, L, W) == exact, "band criterion at N=%d e=%d L=%d W=%d" % (N, e, L, W)) + need(classify(n, e, ell, W) == exact, "classification at N=%d e=%d L=%d W=%d" % (N, e, L, W)) + cases += 1 + bad += (not exact) + if exact and L < 12 * W + 2: + gain += 1 + key = "t=1" if t == 1 else "t>=3" + sharp_by_class[key] = sharp_by_class.get(key, 0) + 1 + return cases, bad, gain, sharp_by_class + + +def check_mutants_rejected(nmax=11): + """Each wrong closed form must contradict the oracle on at least one case.""" + results = {} + mutants = classify_mutants() + for name in mutants: + results[name] = 0 + for n in range(1, nmax + 1): + N = 1 << n + for e in range(1, N // 8 + 1): + H = hole_positions(N, e) + wmax = (N - 2 * e) // (6 * e) + for ell in range(0, n + 1): + L = 1 << ell + m_al = aligned_min_run(H, N, L) + for W in range(1, wmax + 1): + exact = m_al > 6 * W + for name, fn in mutants.items(): + if fn(n, e, ell, W) != exact: + results[name] += 1 + for name, count in results.items(): + need(count > 0, "mutant '%s' was not rejected" % name) + # band mutants: lower end off by one in either direction + for shift in (-1, 1): + wrong = 0 + for n in range(1, 9): + N = 1 << n + for e in range(1, N // 8 + 1): + H = hole_positions(N, e) + for ell in range(0, n + 1): + L = 1 << ell + m_al = aligned_min_run(H, N, L) + for W in range(1, (N - 2 * e) // (6 * e) + 1): + lo, hi = L - 1 - 6 * W + shift, 6 * W + pred = L >= 6 * W + 1 and not any(lo <= h % L <= hi for h in H) + if pred != (m_al > 6 * W): + wrong += 1 + results["band end shifted by %+d" % shift] = wrong + need(wrong > 0, "band mutant shift %+d was not rejected" % shift) + return results + + +def check_sharpness(wmax=64): + """Theorem 3: for every W and every dyadic L <= 12W there is a dyadic instance with + N >= e(6W+2) whose aligned windows of length L are all bad.""" + families = 0 + for W in range(1, wmax + 1): + ell = 1 + while (1 << ell) <= 12 * W: + L = 1 << ell + if L >= 6 * W + 2: + n = ell + 3 # e = N / L = 8 + N = 1 << n + e = N // L + need(N >= e * (6 * W + 2), "hypothesis holds on the e = N/L family") + S = N - e + sel = literal_selected(S, e) + runs = {literal_run(sel, a, L) for a in range(0, N, L)} + need(runs == {L // 2}, "every aligned window has longest run L/2 at W=%d L=%d" % (W, L)) + need(L // 2 <= 6 * W, "L/2 <= 6W") + need(N - L >= W, "complementary gap holds") + else: # L <= 6W + 1, so L <= 6W for a power of two + need(L <= 6 * W, "L = 6W+1 is odd, hence not a power of two") + n = max(ell, (6 * W + 2).bit_length()) + N = 1 << n + e = 1 + need(N >= e * (6 * W + 2), "hypothesis holds for e = 1") + sel = literal_selected(N - e, e) + need(max(literal_run(sel, a, L) for a in range(0, N, L)) <= L <= 6 * W, + "windows no longer than 6W are bad") + families += 1 + ell += 1 + # the smallest dyadic length meeting the uniform guard is exactly admissible + ell = (12 * W + 2 - 1).bit_length() + need((1 << ell) >= 12 * W + 2 and (1 << (ell - 1)) < 12 * W + 2, "least dyadic L >= 12W+2") + return families + + +def check_parity_remark(wmax=200): + """Neither sharpness family of #6972 is dyadic: L = 12W+1 is odd, N = 18W+5 is odd, + and N = 18W+6 = 3(6W+2) is divisible by 3.""" + for W in range(1, wmax + 1): + need((12 * W + 1) % 2 == 1, "family one has odd length") + need((18 * W + 5) % 2 == 1, "family two has odd period") + need((18 * W + 6) % 3 == 0, "family one period has factor 3") + # In a dyadic instance S = e(6W+1)-1 would force N = e(6W+2)-1 odd. + for n in range(1, 13): + N = 1 << n + for e in range(1, N): + for W in range(1, 40): + need(N - e != e * (6 * W + 1) - 1, "S = e(6W+1)-1 is never dyadic") + return wmax + + +def threshold_table(wmax=6, tmax=15): + """Least dyadic L (case III) for each W and odd t, beside the uniform guard's dyadic L.""" + header = ["W", "uniform 12W+2"] + ["t=%d" % t for t in range(1, tmax + 1, 2)] + rows = [] + for W in range(1, wmax + 1): + row = [W] + L = 1 + while L < 12 * W + 2: + L *= 2 + row.append(L) + for t in range(1, tmax + 1, 2): + L = 1 + while (t + 1) * L <= t * (12 * W + 3): + L *= 2 + row.append(L) + rows.append(row) + return {"header": header, "rows": rows} + + +def main(): + cert = {} + guard = check_pinned_source() + cert["pinned_guard_bytes"] = True + cert["oracle_vs_cited_formula_windows"] = check_oracle_against_cited_formula(guard) + pairs, windows = check_lemma_holes_and_runs() + cert["lemma_pairs"], cert["lemma_windows"] = pairs, windows + cert["periodicity_cases"] = check_periodicity() + cases, bad = check_literal_aligned() + cert["literal_aligned_cases"], cert["literal_aligned_bad"] = cases, bad + cases2, bad2, gain, by_class = check_hole_array_aligned(9, 12) + cert["hole_array_cases"], cert["hole_array_bad"] = cases2, bad2 + cert["gain_cases_below_uniform_length"] = gain + cert["gain_by_odd_part"] = by_class + cert["mutant_mismatch_counts"] = check_mutants_rejected() + cert["sharpness_families"] = check_sharpness() + cert["parity_remark_W_values"] = check_parity_remark() + cert["threshold_table"] = threshold_table() + if "--json" in sys.argv: + print(json.dumps(cert, indent=1, sort_keys=True)) + else: + print("oracle agrees with the cited longest-run formula on %d windows" % cert["oracle_vs_cited_formula_windows"]) + print("Lemma 1/2: %d (S,e) pairs, %d windows" % (pairs, windows)) + print("Lemma P periodicity: %d (N,e) cases up to N=4096" % cert["periodicity_cases"]) + print("literal aligned check (N<=256): %d cases, %d bad, band and closed form agree" % (cases, bad)) + print("hole-array aligned check (512<=N<=4096): %d cases, %d bad, band and closed form agree" % (cases2, bad2)) + print("exactly admissible aligned lengths below 12W+2: %d cases %s" % (gain, by_class)) + print("mutants rejected: %s" % cert["mutant_mismatch_counts"]) + print("sharpness families checked: %d" % cert["sharpness_families"]) + print(MARK) + + +if __name__ == "__main__": + main()