diff --git a/research/f7-one-point-pair-ceiling/PROOF.md b/research/f7-one-point-pair-ceiling/PROOF.md new file mode 100644 index 0000000000..045ee50463 --- /dev/null +++ b/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. diff --git a/research/f7-one-point-pair-ceiling/README.md b/research/f7-one-point-pair-ceiling/README.md new file mode 100644 index 0000000000..6371a43e7b --- /dev/null +++ b/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. diff --git a/research/f7-one-point-pair-ceiling/SOURCES.json b/research/f7-one-point-pair-ceiling/SOURCES.json new file mode 100644 index 0000000000..6051566fcc --- /dev/null +++ b/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" + } + ] +} diff --git a/research/f7-one-point-pair-ceiling/TASK.json b/research/f7-one-point-pair-ceiling/TASK.json new file mode 100644 index 0000000000..28e85a9773 --- /dev/null +++ b/research/f7-one-point-pair-ceiling/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "census-pruning-audit", + "priority_revision": 6, + "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f", + "original_card": { + "id": "census-pruning-audit", + "question": "Does the reported word-census parity-pruning error invalidate a specific exclusion we still rely on, and what bounded repair is justified?", + "starting_points": [ + "research/f7-weight-parity-census-correction/README.md", + "docs/research/research-family-status.md" + ], + "methods": [ + "Independently reconstruct the tiny counterexample and trace one affected exclusion to its exact pruning code.", + "Compare corrected and unpruned enumeration on a small exhaustive domain, then audit the changed pruning implication." + ], + "acceptance_gate": "Pin the old and proposed corrected engines, distinguish a disproved pruning rule from a disproved final bound, and state exactly which downstream exclusions need revalidation. #2973 is an author-checked source archive; neither its new f(7) claim nor all old conclusions are automatically accepted or rejected.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #2973 error description and MATH.md; manually reconstruct the prefix states of 01021323 before running any large census.", + "scope": "Source-binding orientation only; no full enumeration or mathematical validation." + }, + "first_experiment": "Reconstruct the eight prefix states of 01021323 and compare bit-0 versus Hamming-weight parity budgets independently. Trace the reported false prune to one pinned predecessor (#2542, #2634 or #2691), then test a small exhaustive domain. Stop after a source-impact handoff or corrected-prune proof; a full seven-label replay needs a separate resource budget and a named research decision it can change.", + "bottleneck_link": "An unsound exclusion can wrongly close a mechanism; correcting its dependency boundary is more useful than extending the same census.", + "allowed_variations": [ + "One predecessor pruning rule, one independently exhaustive small domain, or one downstream dependency audit." + ], + "scope_change_triggers": [ + "Launching a larger census before validating the prune and explaining which active decision it changes.", + "Treating a small-domain counterexample to the old rule as a counterexample to every reported seven-label bound." + ], + "overlap_terms": [ + "2973", + "2542", + "2634", + "2691", + "weight parity", + "bit-0", + "01021323", + "census pruning" + ] + }, + "scope_status": "refined", + "actual_scope": "Exact one-point partial form of the length-22 pair identity: for every n=7 weight split with parts at most 11 that survives B0+a*b>=need, the maximum pair product after adding one missing parity-legal point is at least need. The strict one-point prune therefore deletes no branch of those splits.", + "scope_change_reason": "The card's first experiment, reconstructing 01021323, is already recorded in open PRs #3821 and #3699. This package takes the next uncovered census-pruning obligation from the length-22 handoff: a monotone partial form of the pair identity in MATH.md section 3. The delivered statement is a sharp non-pruning theorem for that one-point form, not another enumeration.", + "bottleneck_link": "A corrected length-22 exclusion would pin f(7) to {22,24} in the PR943 word model. This does not decide that exclusion. It shows one proposed partial pair-identity prune cannot delete a branch on any basic-identity survivor, so engine work should not be spent on the coset-wide one-point test.", + "budget_minutes": 60, + "stop_rule": "Stop once the one-point floor is proved for every basic-identity survivor and the (9,9) equality witness is recomputed. Do not run a length-22 census.", + "outcome": "negative-result", + "evidence": "verify.py recomputes every n=7 basic-identity survivor (3820 rows, parts at most 64), checks h(S_min) >= need, checks the ceil-drop lemma for M=2..64, rebuilds the (9,9) witness with outside f identically 5, and checks the f-sum identities on every subset pair in F_2^3 and F_2^4. test_verify.py repeats the (9,9) and (7,11) arithmetic with literals and shows that the floor swap drops (7,11) from 7 to 6.", + "author": "unpaidmoon", + "ai_assistance": "Substantial AI assistance (Cursor Grok), including the averaging argument, the verifier, and overlap checks. No independent human or formal-kernel review.", + "open_questions": [ + { + "question": "Does restricting the same one-point maximum to the n hypercube neighbors of the current prefix vertex strictly prune any open length-22 split?", + "why_it_matters": "The coset-wide maximum proved here is at least the walk-legal maximum. A neighbor restriction could still fall below need even though the coset-wide test never does.", + "first_step": "On one open split, evaluate S+f(p) only at the neighbors of each vertex of an explicit partial prefix set whose coset-wide ceiling equals need.", + "blocked_by": "Legal extensions are walk steps, not arbitrary coset points. This package does not search walks." + }, + { + "question": "Does an exact two-point completion ceiling strictly prune the (9,9) split?", + "why_it_matters": "One point before the leaf is the strongest exact window that still never prunes. Two points is the next place a partial pair test could delete branches.", + "first_step": "Minimize, or lower-bound, the maximum of S+f(p)+f(r)+A_{p xor r} over odd pairs outside an 7-point odd set paired with a 9-point even set.", + "blocked_by": "A greedy sample reached 17, above need 9. That sample is not a lower bound." + } + ] +} diff --git a/research/f7-one-point-pair-ceiling/VERIFY.json b/research/f7-one-point-pair-ceiling/VERIFY.json new file mode 100644 index 0000000000..e593f8234c --- /dev/null +++ b/research/f7-one-point-pair-ceiling/VERIFY.json @@ -0,0 +1,31 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/f7-weight-parity-census-correction/MATH.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Recompute the n=7 survivor table and checksum, monotonicity residues, the (9,9) witness and greedy odd set, exhaustive f-sum checks for n=3 and n=4, and the 01021323 fixture against the pinned MATH.md." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 60, + "checks": "Literal (9,9) and (7,11) arithmetic, floor-for-ceil failure on (7,11) and (11,7), rejection of the witness with 84 replaced by 2, and a three-point completion increment." + } + ] +} diff --git a/research/f7-one-point-pair-ceiling/test_verify.py b/research/f7-one-point-pair-ceiling/test_verify.py new file mode 100644 index 0000000000..829b2c87ce --- /dev/null +++ b/research/f7-one-point-pair-ceiling/test_verify.py @@ -0,0 +1,88 @@ +#!/usr/bin/env python3 +"""Failure controls for the one-point pair ceiling. Explicit exceptions, not assert.""" + +import importlib.util +from pathlib import Path + + +HERE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location("one_point_ceiling", HERE / "verify.py") +ceiling = importlib.util.module_from_spec(spec) +spec.loader.exec_module(ceiling) + +MARKER = "PASS_F7_ONE_POINT_PAIR_CEILING_CONTROLS" + + +def require(condition, message): + if not condition: + raise ceiling.CheckFailure(message) + + +def hand_arithmetic(): + """Literals only, so a bug copied into verify.py is not the sole source.""" + # (9, 9), one odd point missing. + need = (81 - 64 + 1) // 2 + require(need == 9, "(9,9) need") + # N=9*8=72 over 64 bins: eight 2s and fifty-six 1s. + sum_squares = 8 * 4 + 56 * 1 + smallest = (sum_squares - 72 + 3) // 4 + require(sum_squares == 88 and smallest == 4, "(9,9) flattening") + height = smallest + (8 * 36 - 2 * smallest + 56 - 1) // 56 + require(height == 9, "(9,9) ceiling") + # (7, 11). Floor loses the integer lift; ceil meets need. + need_711 = (77 - 64 + 1) // 2 + require(need_711 == 7, "(7,11) need") + # |O|=10, N=70 = 64+6: six 2s and fifty-eight 1s. + sum_squares = 6 * 4 + 58 * 1 + smallest = (sum_squares - 70) // 4 + require(sum_squares == 82 and smallest == 3, "(7,11) flattening") + slack = 10 * 21 - 2 * smallest + require(slack == 204, "(7,11) outside sum") + ceil_lift = (slack + 54 - 1) // 54 + floor_lift = slack // 54 + require(ceil_lift == 4 and smallest + ceil_lift == 7, "(7,11) ceil bound") + require(floor_lift == 3 and smallest + floor_lift == 6, "(7,11) floor bound falls below need") + + +def corrupted_witness(): + even_points = list(ceiling.WITNESS_EVEN) + odds = [point for point in range(128) if point.bit_count() % 2 == 1] + odd_points = [point for point in ceiling.WITNESS_ODD if point != 84] + [2] + require(2 not in ceiling.WITNESS_ODD and 2 in odds, "edit point 2 is not a fresh odd point") + product, even_counts = ceiling.product_sum(even_points, odd_points) + values = ceiling.link_values(even_counts, odd_points, odds) + present = set(odd_points) + peak = max(values[point] for point in odds if point not in present) + require(product + peak != 9, "replacing 84 by 2 still met the (9,9) equality") + + +def direct_completion(): + """S + f(p) equals the pair product of the enlarged set, on a 3-point example.""" + even_points = [0, 3] + odd_points = [1] + added = 2 + product, even_counts = ceiling.product_sum(even_points, odd_points) + odds = [point for point in range(128) if point.bit_count() % 2 == 1] + values = ceiling.link_values(even_counts, odd_points, odds) + enlarged, _counts = ceiling.product_sum(even_points, odd_points + [added]) + require(product == 0 and values[added] == 1 and enlarged == 1, + "three-point completion did not increase the product by f(p)") + + +def floor_rows_match_the_hand_calculation(): + floors = {(row[0], row[1]): row for row in ceiling.survivor_rows(7, 11, "floor")} + require(floors[(7, 11)][3] == 6 and floors[(7, 11)][2] == 7, "module floor row drifted") + require(floors[(11, 7)][3] < floors[(11, 7)][2], "(11,7) floor row still meets need") + require(ceiling.basic_rows(8, 9, 64) is None, "(8,9) was treated as a survivor") + + +def main(): + hand_arithmetic() + corrupted_witness() + direct_completion() + floor_rows_match_the_hand_calculation() + print(MARKER) + + +if __name__ == "__main__": + main() diff --git a/research/f7-one-point-pair-ceiling/verify.py b/research/f7-one-point-pair-ceiling/verify.py new file mode 100644 index 0000000000..ce0e786cc0 --- /dev/null +++ b/research/f7-one-point-pair-ceiling/verify.py @@ -0,0 +1,399 @@ +#!/usr/bin/env python3 +"""Coset-wide one-point pair ceiling for n=7 weight splits. + +The strict test "every one-point completion has pair product < need" deletes +no branch on a basic-identity survivor. This is a finite certificate plus one +equality witness. It does not decide f(7). + +Apache-2.0. Prepared by unpaidmoon with substantial Cursor Grok assistance. +""" + +from collections import Counter +from hashlib import sha256 +import json +from math import comb +from pathlib import Path + + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +MATH = "research/f7-weight-parity-census-correction/MATH.md" +MARKER = "PASS_F7_ONE_POINT_PAIR_CEILING" + +# Parts at most 11. Columns are s, t, need, h, S_min. +# h is the coset-wide one-point lower bound with the missing point on the +# t side. Both orientations are rows. +FROZEN_PARTS_AT_MOST_11 = ( + (6, 11, 1, 3, 0), + (7, 10, 3, 4, 0), + (7, 11, 7, 7, 3), + (8, 10, 8, 9, 4), + (8, 11, 12, 13, 8), + (9, 9, 9, 9, 4), + (9, 10, 13, 15, 9), + (9, 11, 18, 20, 13), + (10, 7, 3, 5, 0), + (10, 8, 8, 9, 3), + (10, 9, 13, 15, 8), + (10, 10, 18, 20, 13), + (10, 11, 23, 26, 18), + (11, 6, 1, 5, 0), + (11, 7, 7, 7, 1), + (11, 8, 12, 14, 7), + (11, 9, 18, 20, 12), + (11, 10, 23, 27, 18), + (11, 11, 29, 33, 23), +) + +# Equality witness for the completed split (9, 9): |E|=9, |O|=8. +# Outside f is identically 5, so every legal one-point completion has +# pair product 4+5=9=need. E is explicit. O is rebuilt by greedy_odd. +WITNESS_EVEN = (0, 3, 5, 9, 10, 33, 34, 40, 43) +WITNESS_ODD = (1, 4, 16, 21, 64, 69, 81, 84) + +# Checksum of every n=7 survivor row with 0<=s<=64 and 1<=t<=64. +# A changed rounding rule or domain moves this value. +FULL_RECTANGLE_CHECKSUM = 7722612959244201139 +FULL_RECTANGLE_SURVIVORS = 3820 + + +class CheckFailure(Exception): + """Explicit failure. Raised under -O as well as ordinary execution.""" + + +def require(condition, message): + if not condition: + raise CheckFailure(message) + + +def popcount(value): + return value.bit_count() + + +def even_odd(dimension): + limit = 1 << dimension + evens = tuple(x for x in range(limit) if popcount(x) % 2 == 0) + odds = tuple(x for x in range(limit) if popcount(x) % 2 == 1) + return evens, odds + + +def pair_counts(points): + counts = Counter() + for index, left in enumerate(points): + for right in points[index + 1:]: + counts[left ^ right] += 1 + return counts + + +def product_sum(even_points, odd_points): + even_counts = pair_counts(even_points) + odd_counts = pair_counts(odd_points) + total = 0 + for mask, count in even_counts.items(): + total += count * odd_counts[mask] + return total, even_counts + + +def cross_pair_collisions(even_points, odd_points): + occupancy = Counter(left ^ right for left in even_points for right in odd_points) + return sum(count * (count - 1) // 2 for count in occupancy.values()) + + +def link_values(even_counts, odd_points, odd_universe): + """f(p) = sum_{q in O} A_{p xor q}, for every odd universe point.""" + values = {} + for point in odd_universe: + total = 0 + for other in odd_points: + total += even_counts[point ^ other] + values[point] = total + return values + + +def square_minimum(total, bins): + """Minimum of sum r_i^2 for nonnegative integers summing to total.""" + quotient, remainder = divmod(total, bins) + return remainder * (quotient + 1) * (quotient + 1) + (bins - remainder) * quotient * quotient + + +def integer_s_min(even_size, odd_size, half_dimension): + """Ceil of (min sum r^2 - N) / 4. Valid even when the flat vector is not a legal S.""" + occupied = even_size * odd_size + gap = square_minimum(occupied, half_dimension) - occupied + require(gap >= 0, "sum of squares dropped below the occupation count") + return (gap + 3) // 4 + + +def basic_rows(even_size, odd_size, half_dimension): + budget = comb(even_size, 2) + comb(odd_size, 2) - (half_dimension - 1) + product = even_size * odd_size + if product < half_dimension or budget < 0: + return None + need = (product - half_dimension + 1) // 2 + largest_product = (budget // 2) * ((budget + 1) // 2) + if budget + largest_product < need: + return None + return budget, need + + +def one_point_bound(even_size, completed_odd, half_dimension, rounding): + """Lower bound on max_p (S + f(p)) for |O| = completed_odd - 1. + + Returns None when no partial state can have a nonnegative outside sum. + rounding is "ceil" for the theorem and "floor" for the failure control. + """ + require(rounding in ("ceil", "floor"), "unknown rounding " + rounding) + require(1 <= completed_odd <= half_dimension, "odd side is outside the coset") + missing = completed_odd - 1 + outside = half_dimension - missing + alpha = missing * comb(even_size, 2) + smallest = integer_s_min(even_size, missing, half_dimension) + largest_nonnegative = alpha // 2 + if smallest > largest_nonnegative: + return None + if outside >= 2: + slack = alpha - 2 * smallest + if rounding == "ceil": + lift = (slack + outside - 1) // outside + else: + lift = slack // outside + return smallest + lift, smallest, outside + # One admissible completion point: its f equals the whole outside sum, + # so the product is alpha - S and the weakest value uses the largest + # conceivable S. The sum-of-squares maximum is one bin holding every cross pair. + occupied = even_size * missing + square_cap = (occupied * occupied - occupied) // 4 + cap = min(largest_nonnegative, square_cap) + require(cap >= smallest, "square upper bound fell below S_min") + # Floor versus ceil does not apply: f is exact. Both modes return alpha - cap. + return alpha - cap, smallest, outside + + +def survivor_rows(dimension, part_limit, rounding): + half = 1 << (dimension - 1) + rows = [] + for even_size in range(part_limit + 1): + for odd_size in range(1, part_limit + 1): + basic = basic_rows(even_size, odd_size, half) + if basic is None: + continue + bound = one_point_bound(even_size, odd_size, half, rounding) + if bound is None: + continue + height, smallest, _outside = bound + rows.append((even_size, odd_size, basic[1], height, smallest)) + return tuple(rows) + + +def rectangle_checksum(dimension, rounding): + half = 1 << (dimension - 1) + rows = survivor_rows(dimension, half, rounding) + digest = 0 + for even_size, odd_size, need, height, smallest in rows: + require(height >= need, "one-point bound fell below need at (%d,%d)" % (even_size, odd_size)) + digest = (digest * 1000003 + even_size * 1009 + odd_size * 17 + height + smallest) % (1 << 63) + return len(rows), digest + + +def ceil_drop_at_most_one(): + """For M>=2 and T>=2, ceil(T/M) - ceil((T-2)/M) is 0 or 1. + + The difference depends on T mod M, so one full set of residues is a proof + for every M that occurs at n<=7. + """ + for outside in range(2, 65): + for slack in range(2, outside + 3): + current = (slack + outside - 1) // outside + dropped = (slack - 2 + outside - 1) // outside + gap = current - dropped + require(0 <= gap <= 1, "ceil drop %d at T=%d M=%d" % (gap, slack, outside)) + + +def check_math_input(): + manifest = json.loads((HERE / "SOURCES.json").read_text(encoding="utf-8")) + pinned = None + for row in manifest["files"]: + if row["path"] == MATH and row["usage"] == "input": + pinned = row["sha256"] + require(pinned is not None, "MATH.md input pin missing from SOURCES.json") + text = (ROOT / MATH).read_text(encoding="utf-8") + require(sha256(text.encode("utf-8")).hexdigest() == pinned, "MATH.md sha256 does not match SOURCES.json") + require("sum_y C(r_y,2) = 2 * sum_x A_x*B_x." in text, "pair identity line missing from MATH.md") + require("sum_x A_x*B_x >= ceil((s*t-Q)/2) =: need." in text, "need definition missing from MATH.md") + require("canonical word 01021323" in text, "01021323 fixture missing from MATH.md") + return text + + +def check_word_fixture(): + dimension = 4 + state = 0 + seen = [state] + for label in (0, 1, 0, 2, 1, 3, 2, 3): + state ^= 1 << label + seen.append(state) + require(seen == [0, 1, 3, 2, 6, 4, 12, 8, 0], "01021323 prefix walk changed") + points = set(seen) + require(points == {0, 1, 2, 3, 4, 6, 8, 12}, "01021323 prefix set changed") + even = sum(popcount(point) % 2 == 0 for point in points) + odd = len(points) - even + require((even, odd) == (4, 4), "weight split is not (4,4)") + low_bit = sum(point & 1 for point in points) + require((len(points) - low_bit, low_bit) == (6, 2), "bit-0 split is not (6,2)") + half = 1 << (dimension - 1) + balanced = comb(4, 2) + comb(4, 2) - (half - 1) + actual_bit = comb(6, 2) + comb(2, 2) - (half - 1) + require(balanced == 5 and actual_bit == 9, "documented budgets 5 and 9 were not recomputed") + coverage = {left ^ right for left in points for right in points} + require(coverage == set(range(1 << dimension)), "01021323 does not cover every mask") + # The old prune compares bit-0 excess 8 with the balanced budget 5. + kernel = [point for point in points if (point & 1) == 0] + coset = [point for point in points if (point & 1) == 1] + require((len(kernel), len(coset)) == (6, 2), "bit-0 classes drifted") + kernel_pairs = pair_counts(kernel) + coset_pairs = pair_counts(coset) + bit_excess = (comb(6, 2) - len(kernel_pairs)) + (comb(2, 2) - len(coset_pairs)) + require(bit_excess == 8, "bit-0 collision excess is not 8") + + +def check_witness(): + dimension = 7 + _evens, odds = even_odd(dimension) + even_points = list(WITNESS_EVEN) + require(len(even_points) == len(set(even_points)) == 9, "witness even set is not 9 distinct points") + require(all(popcount(point) % 2 == 0 and 0 <= point < 128 for point in even_points), + "witness even set leaves the even coset") + rebuilt = greedy_odd(even_points, 8) + require(tuple(sorted(rebuilt)) == tuple(sorted(WITNESS_ODD)), + "greedy odd extension did not rebuild the pinned witness") + odd_points = list(rebuilt) + require(all(popcount(point) % 2 == 1 for point in odd_points), "greedy left the odd coset") + product, even_counts = product_sum(even_points, odd_points) + values = link_values(even_counts, odd_points, odds) + odd_set = set(odd_points) + outside = [values[point] for point in odds if point not in odd_set] + alpha = len(odd_points) * comb(len(even_points), 2) + require(product == 4, "witness pair product is not 4") + require(outside and min(outside) == max(outside) == 5, "witness outside f is not identically 5") + require(sum(values.values()) == alpha, "sum of f over the odd coset is not |O|*C(|E|,2)") + require(sum(values[point] for point in odd_points) == 2 * product, "sum of f over O is not 2S") + require(cross_pair_collisions(even_points, odd_points) == 2 * product, + "sum C(r_y,2) is not 2S on the witness") + # Every one-point completion, recomputed from the enlarged odd set. + for point in odds: + if point in odd_set: + continue + enlarged, _counts = product_sum(even_points, odd_points + [point]) + require(enlarged == product + values[point] == 9, + "completion product drifted at %d" % point) + half = 1 << (dimension - 1) + basic = basic_rows(9, 9, half) + require(basic is not None and basic[1] == 9, "(9,9) need is not 9") + bound = one_point_bound(9, 9, half, "ceil") + require(bound is not None and bound[0] == 9 and bound[1] == 4, "(9,9) arithmetic bound is not 9") + + +def greedy_odd(even_points, target): + """Increasing odd pool. Keep a candidate only on a strict improvement of (S, max f, index).""" + _evens, odds = even_odd(7) + chosen = [] + chosen_set = set() + while len(chosen) < target: + best = None + best_key = None + for point in odds: + if point in chosen_set: + continue + trial = chosen + [point] + product, even_counts = product_sum(even_points, trial) + values = link_values(even_counts, trial, odds) + present = set(trial) + outside = [values[candidate] for candidate in odds if candidate not in present] + peak = max(outside) if outside else 0 + key = (product, peak, point) + if best_key is None or key < best_key: + best_key = key + best = point + require(best is not None, "greedy found no odd candidate") + chosen.append(best) + chosen_set.add(best) + return chosen + + +def exhaustive_small(dimension): + """Every even/odd subset pair: pair identity, f-sums, and the averaging step.""" + half = 1 << (dimension - 1) + evens, odds = even_odd(dimension) + require(len(evens) == len(odds) == half, "coset split is not equal") + subset_count = 1 << half + for even_mask in range(subset_count): + even_points = [evens[index] for index in range(half) if even_mask >> index & 1] + even_counts = pair_counts(even_points) + even_pairs = len(even_points) * (len(even_points) - 1) // 2 + for odd_mask in range(subset_count): + odd_points = [odds[index] for index in range(half) if odd_mask >> index & 1] + odd_counts = pair_counts(odd_points) + product = sum(count * odd_counts[mask] for mask, count in even_counts.items()) + require(cross_pair_collisions(even_points, odd_points) == 2 * product, + "pair identity failed on n=%d" % dimension) + values = link_values(even_counts, odd_points, odds) + alpha = len(odd_points) * even_pairs + require(sum(values.values()) == alpha, "coset sum of f failed") + require(sum(values[point] for point in odd_points) == 2 * product, "inside sum of f failed") + outside_points = [point for point in odds if point not in set(odd_points)] + if not outside_points: + continue + outside_sum = alpha - 2 * product + require(outside_sum == sum(values[point] for point in outside_points), "outside sum split failed") + if outside_sum < 0: + continue + peak = max(values[point] for point in outside_points) + require(peak >= (outside_sum + len(outside_points) - 1) // len(outside_points), + "averaging lower bound failed") + # One fresh completion, the smallest outside point, recomputed from pairs. + point = outside_points[0] + enlarged, _counts = product_sum(even_points, odd_points + [point]) + require(enlarged == product + values[point], "completion increment failed") + + +def check_parts_and_rectangle(): + ceil_rows = survivor_rows(7, 11, "ceil") + require(ceil_rows == FROZEN_PARTS_AT_MOST_11, "parts<=11 survivor table changed: %s" % (ceil_rows,)) + for even_size, odd_size, need, height, _smallest in ceil_rows: + require(height >= need, "frozen row (%d,%d) has h < need" % (even_size, odd_size)) + # (8,9) and (9,8) are the length-20 basic-identity exclusions. They are not in the table. + half = 64 + require(basic_rows(8, 9, half) is None and basic_rows(9, 8, half) is None, + "(8,9) survived the basic identity") + budget = comb(8, 2) + comb(9, 2) - 63 + require(budget == 1 and (8 * 9 - 64 + 1) // 2 == 4, "(8,9) budget/need drifted") + count, digest = rectangle_checksum(7, "ceil") + require(count == FULL_RECTANGLE_SURVIVORS, "survivor count %d" % count) + require(digest == FULL_RECTANGLE_CHECKSUM, "rectangle checksum %d" % digest) + # Same closed form on the smaller cubes, still only the arithmetic certificate. + for dimension in (3, 4, 5, 6): + small_count, _small_digest = rectangle_checksum(dimension, "ceil") + require(small_count > 0, "no survivors at n=%d" % dimension) + + +def check_floor_control_is_real(): + """The theorem uses ceil. Floor drops (7,11) and (11,7) strictly below need.""" + floors = { (row[0], row[1]): row for row in survivor_rows(7, 11, "floor") } + dropped = sorted(key for key, row in floors.items() if row[3] < row[2]) + require(dropped == [(7, 11), (11, 7)], "floor mutation did not fail exactly the two sharp rows") + require(floors[(9, 9)][3] == 9, "exact division at (9,9) should be stable under floor") + + +def main(): + check_math_input() + check_word_fixture() + ceil_drop_at_most_one() + check_witness() + exhaustive_small(3) + exhaustive_small(4) + check_parts_and_rectangle() + check_floor_control_is_real() + print(MARKER) + + +if __name__ == "__main__": + main()