Record the coset-wide one-point pair ceiling

research/f7-one-point-pair-ceiling/PROOF.md

@@ -0,0 +1,196 @@
+# Coset-wide one-point pair ceiling
+
+## Statement
+
+Work in `F_2^7`. Let `Q = 64` be the size of each weight-parity coset. For integers
+`s, t` with `0 <= s <= Q` and `1 <= t <= Q`, write
+
+```
+B0 = C(s,2) + C(t,2) - (Q-1),
+need = ceil((s*t - Q) / 2).
+```
+
+The split survives the basic pair test when `s*t >= Q`, `B0 >= 0`, and there
+exist integers `a, b >= 0` with `a + b <= B0` and `B0 + a*b >= need`. Equivalently,
+`B0 + floor(B0/2)*ceil(B0/2) >= need`.
+
+Let `E` be an `s`-point subset of the even-weight coset and `O` a `(t-1)`-point
+subset of the odd-weight coset. Let `S = sum_x A_x B_x` be the pair product of
+that partial pair of sets, and for an odd point `p` not in `O` let `f(p)` be the
+product added by inserting `p`. Then
+
+```
+max_p (S + f(p)) >= need.
+```
+
+In particular the strict pruning test `max_p (S + f(p)) < need` deletes no such
+branch. Both orientations are included: the missing point may lie on either side.
+The parts-at-most-11 window, which contains every ordered length-22 split with
+both parts at most 11 and the length-20 representatives other than `(8,9)`, is
+the row table in `verify.py`.
+
+This is a necessary-condition bound on sets. It is not a prefix-walk search, not
+a two-point bound, and not a determination of `f(7)`.
+
+## Pair product and the one-point increment
+
+For a nonzero even mask `x`, `A_x` (respectively `B_x`) counts unordered pairs
+inside `E` (respectively `O`) with difference `x`. For an odd mask `y`, `r_y`
+counts ordered cross pairs from `E x O` with difference `y`. The identity
+
+```
+sum_y C(r_y, 2) = 2 S
+```
+
+is the double count in `research/f7-weight-parity-census-correction/MATH.md`
+section 3: each even pair and odd pair with the same difference determines two
+cross-pair collisions. Consequently `sum_y r_y^2 = 4S + |E|·|O|`.
+
+Adding an odd point `p` not in `O` creates one new odd pair `{p, q}` for each
+`q` in `O`. These differences `p xor q` are nonzero and pairwise distinct, and
+`E` is unchanged, so the pair product increases by exactly
+
+```
+f(p) = sum_{q in O} A_{p xor q}.
+```
+
+The completed product is `S + f(p)`.
+
+## Two sums of f
+
+Summing over the whole odd coset, each fixed `q` makes `p xor q` run through
+every even vector exactly once. The zero mask contributes nothing, and the
+remaining masks contribute `C(|E|, 2)`. Hence
+
+```
+sum_{p odd} f(p) = |O| · C(|E|, 2) =: alpha.
+```
+
+Summing only over `p` in `O`, each unordered odd pair `{p, q}` contributes
+`A_{p xor q}` once to `f(p)` and once to `f(q)`, so
+
+```
+sum_{p in O} f(p) = 2S.
+```
+
+The outside sum is `alpha - 2S`. If it is negative, no such pair of sets exists.
+If `M = Q - |O|` outside points remain and the outside sum `T` is nonnegative,
+those `M` nonnegative integers have maximum at least `ceil(T / M)`. Therefore
+
+```
+max_p (S + f(p)) >= S + ceil((alpha - 2S) / M)
+```
+
+whenever `T >= 0` and `M >= 1`. For `M = 1` the single outside value equals `T`,
+so the completed product equals `alpha - S` exactly.
+
+## Flattening lower bound
+
+`sum_y r_y = |E|·|O| = N` and `sum_y r_y^2 = 4S + N`. Among nonnegative integer
+vectors of length `Q` with sum `N`, the sum of squares is minimized when the
+parts differ by at most one. If that minimum is `sigma`, then `4S = sum r^2 - N
+>= sigma - N`, so
+
+```
+S >= S_min = ceil((sigma - N) / 4).
+```
+
+The flat vector need not itself satisfy `sum r^2 ≡ N (mod 4)`. The ceiling still
+lower-bounds every realizable `S`, because every realizable sum of squares is at
+least `sigma` and the corresponding `S` is an integer.
+
+An upper bound used only for the one-outside-point case is the opposite extreme:
+one bin holds all `N` crosses, so `S <= (N^2 - N) / 4`.
+
+## Monotonicity for at least two outside points
+
+Let `h(S) = S + ceil((alpha - 2S) / M)` for integers `S` with `alpha - 2S >= 0`.
+Increasing `S` by one decreases the numerator by two. For `M >= 2` and numerator
+`T >= 2`,
+
+```
+ceil(T/M) - ceil((T-2)/M) <= 1,
+```
+
+so `h` does not fall. Write `T = qM + r` with `0 <= r < M`.
+
+- If `r >= 2`, then `T - 2` has remainder `r - 2` and the same quotient, and the
+  ceilings differ by at most one.
+- If `r = 1`, then `T - 2` has quotient `q - 1` and remainder `M - 1`, and both
+  ceilings equal `q` and `q + 1` in that order.
+- If `r = 0`, then `ceil(T/M) = q` and `T - 2` has quotient `q - 1` and remainder
+  `M - 2`. For `M > 2` the new ceiling is `q`. For `M = 2` the remainder is `0`
+  and the new ceiling is `q - 1`.
+
+In every case the drop is at most one, so `h(S+1) >= h(S)`. The weakest value on
+the feasible range is therefore `h(S_min)`. The verifier also checks the drop on
+every residue for every `M` from 2 through 64.
+
+For `M = 1`, `h(S) = alpha - S` decreases, and the weakest value is `alpha`
+minus the largest conceivable `S`. That case is `t = Q`, far outside the
+parts-at-most-11 window (`M >= 54` there). It is included in the full rectangle
+so the boundary is not omitted.
+
+## Finite certificate
+
+For every basic-identity survivor with `n = 7` and both parts at most 64, the
+bound just described is at least `need`. There are 3820 such survivors. The same
+closed form was evaluated for `n = 3, 4, 5, 6` over the whole coset rectangle;
+none fell below `need`. Those smaller checks are arithmetic, not a substitute
+for the set identities.
+
+The set identities, the outside-sum split, the averaging step, and one fresh
+completion increment were checked on every even/odd subset pair in `F_2^3` and
+`F_2^4`. The collision identity `sum C(r_y, 2) = 2S` on `F_2^4` is already
+recorded by PR #3827; it is rechecked here only as a lemma of this argument.
+The `f` sums and the completion increment are the part used below.
+
+## Equality at (9, 9)
+
+Here `need = 9`, `B0 = 9`, and the basic test survives. With one odd point
+missing, `|O| = 8`, `alpha = 288`, `M = 56`, `N = 72`, `sigma = 88`, and
+`S_min = 4`. Then `T = 280` and `ceil(T/M) = 5`, so `h = 9`.
+
+The even set
+
+```
+{0, 3, 5, 9, 10, 33, 34, 40, 43}
+```
+
+and the odd set produced by the greedy below,
+
+```
+{1, 4, 16, 21, 64, 69, 81, 84},
+```
+
+realize `S = 4` with `f(p) = 5` at every odd `p` outside the odd set. Every
+legal one-point completion therefore has pair product exactly 9. The greedy
+scans the odd coset in increasing order and keeps a candidate only when
+`(S, max outside f, index)` strictly improves. The verifier reruns it and
+recomputes every completion from pair counts. Replacing `84` by `2` raises the
+ceiling from 9 to 17.
+
+`(7,11)` and `(11,7)` also have `h(S_min) = need` under ceiling division. No
+realized set is claimed for those two rows. Replacing the ceiling by the floor
+drops both arithmetic bounds from 7 to 6, so the integer lift is necessary for
+this writeup. `(9,9)` is an exact division and is unchanged by that swap.
+`(8,9)` and `(9,8)` do not reach this test: `B0 = 1` and `need = 4`, so
+`B0 + a*b <= 1`.
+
+## What the maximum does not say
+
+The maximum is over the whole odd coset. A prefix walk may add only a neighbor
+of the current vertex. That restricted maximum is at most the coset-wide maximum,
+so a neighbor test can still fall below `need` on a branch where the coset-wide
+test cannot. This package does not search walks.
+
+A two-point window is the next partial test. One greedy sample on `(9,9)` reached
+17, which is above `need` and is not a lower bound.
+
+The `(9,9)` witness is a parity-legal pair of sets, not a prefix walk, so it is
+not a counterexample to a walk-level exclusion. PR #3818 claims a different
+union-support exclusion of `(9,9)`. PR #3731 claims census exclusions of
+`(11,7)`, `(10,8)`, and `(11,8)`. Nothing here confirms or revisits those claims.
+PR #3821 and PR #3699 already record the word
+`01021323`; the fixture in `verify.py` only recomputes the split `(4,4)`, the
+bit-0 split `(6,2)`, the excess 8, and the budgets 5 and 9 from MATH.md.

research/f7-one-point-pair-ceiling/README.md

@@ -0,0 +1,130 @@
+# One-point pair ceiling on n=7 weight splits
+
+**Negative result.** On every basic-identity survivor in `F_2^7`, the coset-wide
+one-point completion of the pair product is at least `need`. The strict test
+that rejects a branch when every missing parity-legal point leaves the product
+below `need` therefore deletes nothing. The bound is realized at `(9,9)`.
+
+Selected frontier, κ, and `f(7)` are unchanged. A finite certificate is not a
+length-22 census and not a multiplication theorem.
+
+Original card: `census-pruning-audit` (priority revision 6, base
+`bb4bccbf42844d2801487450727c2f63e10d1d0f`). Scope is **refined**. The card's
+first experiment, the word `01021323`, is already in open PRs #3821 and #3699.
+This package takes the next uncovered obligation from the length-22 handoff: a
+partial form of the pair identity in
+[MATH.md](../f7-weight-parity-census-correction/MATH.md) section 3. The delivered
+form is the exact one-point window, not another enumeration. Details, the
+monotonicity case split, and the witness are in [PROOF.md](PROOF.md). Source
+pins are in [SOURCES.json](SOURCES.json).
+
+## Result
+
+For a surviving split `(s, t)`, with `E` already of size `s` and `O` of size
+`t - 1`,
+
+```
+max_{p not in O} (S + f(p)) >= need = ceil((s*t - Q) / 2),
+```
+
+where `Q = 64`, `S` is the partial pair product, and `f(p)` is the product added
+by one new odd point. The missing point may sit on either side; both
+orientations are rows.
+
+The proof has four pieces.
+
+1. Inserting `p` increases the product by `f(p) = sum_{q in O} A_{p xor q}`.
+2. `sum f = |O|·C(|E|,2)` over the odd coset and `sum f = 2S` over `O`, so the
+   outside average is exact.
+3. `S` is at least the integer flattening bound coming from `sum C(r_y, 2) = 2S`.
+4. While at least two outside points remain, that lower bound is weakest at the
+   smallest admissible `S`, because raising `S` by one drops the ceiling by at
+   most one.
+
+Every survivor with both parts at most 64 satisfies the resulting inequality
+(3820 rows). In the parts-at-most-11 window the bound is:
+
+| split | need | h | split | need | h |
+|---|---:|---:|---|---:|---:|
+| (6,11) | 1 | 3 | (10,8) | 8 | 9 |
+| (7,10) | 3 | 4 | (10,9) | 13 | 15 |
+| (7,11) | 7 | 7 | (10,10) | 18 | 20 |
+| (8,10) | 8 | 9 | (10,11) | 23 | 26 |
+| (8,11) | 12 | 13 | (11,6) | 1 | 5 |
+| (9,9) | 9 | 9 | (11,7) | 7 | 7 |
+| (9,10) | 13 | 15 | (11,8) | 12 | 14 |
+| (9,11) | 18 | 20 | (11,9) | 18 | 20 |
+| (10,7) | 3 | 5 | (11,10) | 23 | 27 |
+|  |  |  | (11,11) | 29 | 33 |
+
+`(8,9)` and `(9,8)` never enter the table: `B0 = 1` and `need = 4`.
+
+### Equality witness
+
+`E = {0, 3, 5, 9, 10, 33, 34, 40, 43}` and
+`O = {1, 4, 16, 21, 64, 69, 81, 84}` have `|E| = 9`, `|O| = 8`, `S = 4`, and
+`f(p) = 5` at every remaining odd point. Every one-point completion has product
+9, which equals `need` for `(9,9)`. `O` is rebuilt by a deterministic greedy
+scan (increasing odd pool, strict improvement of `(S, max f, index)`). Replacing
+`84` by `2` moves the ceiling to 17.
+
+`(7,11)` and `(11,7)` meet `need` only after the integer ceiling. The floor of
+the same quotient is 6, which is below 7. No realized set is claimed for those
+two rows. `(9,9)` divides exactly, so the floor swap does not move it.
+
+## Limitations
+
+- The maximum is over the whole odd coset. A prefix walk can add only a neighbor
+  of the current vertex, and that smaller maximum can still lie below `need`.
+- States in which both sides are more than one point short are not bounded here.
+- The `F_2^4` check of `sum C(r_y, 2) = 2S` repeats a lemma already in PR #3827.
+  The new exhaustive checks are the sums of `f` and the completion increment.
+- The `(9,9)` witness is a parity-legal pair of sets, not a prefix walk. It shows
+  the coset-wide one-point test is sharp. It is not a counterexample to a
+  walk-level exclusion. PR #3818 claims a different union-support exclusion of
+  `(9,9)`, and PR #3731 claims census exclusions of `(11,7)`, `(10,8)`, and
+  `(11,8)`. This package does not confirm or revisit those claims.
+- The word `01021323` is recomputed only as a fixture of the pinned MATH.md
+  example (weight split `(4,4)`, bit-0 split `(6,2)`, excess 8). It is not a new
+  reconstruction.
+- No length-22 census was run. Nothing here places `f(7)` in `{22, 24}`.
+
+## Reproduce
+
+Python 3.12, standard library only, from the repository root:
+
+```sh
+python3 scripts/research_package.py --package research/f7-one-point-pair-ceiling --check-only
+python3.12 scripts/research_package.py --package research/f7-one-point-pair-ceiling
+```
+
+`verify.py` recomputes the survivor table, the monotonicity residues, the
+witness and its greedy odd set, exhaustive subset checks for `n = 3` and `n = 4`,
+and the `01021323` fixture. `test_verify.py` repeats the `(9,9)` and `(7,11)`
+arithmetic with literals, rejects the floor swap, and rejects the edited witness.
+Checks raise `CheckFailure` rather than using `assert`.
+
+## Open next questions
+
+1. Does the same ceiling, restricted to the `n` hypercube neighbors of the current
+   prefix vertex, fall below `need` on any open length-22 split? The coset-wide
+   maximum is an upper bound on that walk-legal maximum, so a neighbor
+   restriction can still prune. First step: on one open split, evaluate `S + f(p)`
+   only at the neighbors of each vertex of an explicit partial prefix whose
+   coset-wide ceiling equals `need`. Blocked here because legal extensions are
+   walk steps and this package does not search walks.
+2. Does an exact two-point completion ceiling strictly prune `(9,9)`? One point
+   before the leaf is the strongest exact window that still never prunes. First
+   step: lower-bound `S + f(p) + f(r) + A_{p xor r}` over odd pairs outside a
+   7-point odd set paired with a 9-point even set. A greedy sample reached 17,
+   above `need` 9, and that sample is not a lower bound.
+
+## Credit
+
+The pair identity, the basic row test, and the word `01021323` come from Nicholas
+Stone's package `research/f7-weight-parity-census-correction` (substantial
+OpenAI Codex assistance; Apache-2.0). The length-22 partial-identity request is
+the handoff in discussion #1166. Parallel census PRs #3821, #3699, #3827, and
+#3818 were left in place. Prepared by unpaidmoon with substantial AI assistance
+(Cursor Grok), including the averaging argument and this verifier. No independent
+human or formal-kernel review.

research/f7-one-point-pair-ceiling/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5",
+      "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0"
+    },
+    {
+      "path": "research/f7-weight-parity-census-correction/MATH.md",
+      "usage": "input",
+      "git_blob": "e0207d8ebd903dc584862a2d6d500b59f3134490",
+      "sha256": "13f1234de6b7bd9f5afbe9a8892fc1d7f47eae0eddf098d19331a561c750e06a"
+    }
+  ]
+}