From daaa8d8ec52204e5d5ab76bb574ec8f3136a65f4 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Tue, 20 Oct 2026 02:56:21 +0000 Subject: [PATCH] Prove codimension-one L/2 substitution soundness on double transversals. On simple restored universal words with n in {3,4} and L=2n, every label-basis functional of weight at least n-1 is sound for the fixed substitution. The same weight pattern fails at (4,12). No new kappa. Co-authored-by: unpaidmoon --- .../PROOF.md | 157 ++++++++++ .../README.md | 130 +++++++++ .../SOURCES.json | 18 ++ .../TASK.json | 78 +++++ .../VERIFY.json | 27 ++ .../test_verify.py | 43 +++ .../verify.py | 275 ++++++++++++++++++ 7 files changed, 728 insertions(+) create mode 100644 research/f7-codim-one-substitution-soundness/PROOF.md create mode 100644 research/f7-codim-one-substitution-soundness/README.md create mode 100644 research/f7-codim-one-substitution-soundness/SOURCES.json create mode 100644 research/f7-codim-one-substitution-soundness/TASK.json create mode 100644 research/f7-codim-one-substitution-soundness/VERIFY.json create mode 100644 research/f7-codim-one-substitution-soundness/test_verify.py create mode 100644 research/f7-codim-one-substitution-soundness/verify.py diff --git a/research/f7-codim-one-substitution-soundness/PROOF.md b/research/f7-codim-one-substitution-soundness/PROOF.md new file mode 100644 index 0000000000..0df5ca3728 --- /dev/null +++ b/research/f7-codim-one-substitution-soundness/PROOF.md @@ -0,0 +1,157 @@ +# Codimension-one soundness of the fixed `L/2` substitution + +The model is the PR943 singleton prefix walk, as corrected by #2973 and +classified on small domains by #3699. For a word `w` of length `L` over +`[0, n)`, + +``` +q_0 = 0, q_{i+1} = q_i XOR e_{w_i}. +``` + +The prefix set `S` is `{q_0, ..., q_{L-1}}`. The word is **simple** when these +`L` states are distinct, **restored** when every label occurs a positive even +number of times, and **universal** when `S + S = F_2^n`. A nonzero linear +functional `f` has kernel `K` of size `Q = 2^{n-1}`. Write `E = S ∩ K`, +`O = S \ E`, `s = |E|`, `t = |O|`, and + +``` +a = C(s, 2) - |{x + y : x ≠ y in E}|, +b = C(t, 2) - |{x + y : x ≠ y in O}|. +``` + +Pair sums of either class land in `K`. Universality forces `a + b ≤ base + d²`, +where `d = (s - t) / 2` and + +``` +base(n, L) = 2 C(L/2, 2) - (Q - 1). +``` + +The fixed substitution uses budget `base`. It **falsely prunes** a universal +word when `base < a + b ≤ base + d²`. + +#3699 measured that, on its firing domains, no functional of Hamming weight at +least `n - 1` falsely prunes, and said that regularity was not a theorem. +#3733 then showed the regularity is not a weight law: at `(4, 12)` three +weight-3 masks do fire. This note proves the measured statement in the one +range where every label occurs twice. + +## 1. Two preserving steps + +**Lemma.** Let `L` be even and let exactly two steps of the walk preserve a +linear functional `f` with `f(q_0) = 0`. Among `q_0, ..., q_{L-1}`, the two +level sets of `f` differ in size by at most 2. + +*Proof.* A preserving step is a stay and every other step flips `f`. Let the +stays be at indices `i < j`. Then `f(q_k)` equals `k mod 2` for `k ≤ i` and for +`k > j`, and equals `(k - 1) mod 2` for `i < k ≤ j`. The comparison pattern +`k mod 2` has exactly `L/2` zeros. The two patterns differ exactly on the +integer interval `(i, j]`. On any integer interval the numbers of even and odd +points differ by at most 1, so replacing one count by the other changes the +zero count by at most 1. Therefore `|s - L/2| ≤ 1` and `|s - t| ≤ 2`. + +The hypothesis is sharp: four stays can produce a difference of 4. The +verifier checks every stay pair for `L ∈ {6, 8, 10, 12, 14}` against this +interval formula, and checks one four-stay pattern that leaves the bound. + +## 2. Pair sums in small spaces + +**Lemma.** Any three distinct vectors have three distinct pairwise sums, none +of them zero. + +*Proof.* If `a + b = a + c` then `b = c`. The other two identifications are the +same argument. + +**Lemma.** Every 5-subset `E` of `F_2^3` has `{x + y : x ≠ y in E}` equal to +all seven nonzero vectors. + +*Proof.* A nonzero `v` that is missed meets `E` in at most one point of each +coset of `{0, v}`. There are four such cosets, so `|E| ≤ 4`. The verifier +enumerates all `C(8, 5) = 56` subsets and one 4-subset that misses a direction. + +An affine coset `v + K` has the same pair-sum set as its translate inside `K`, +because `(v + a) + (v + b) = a + b`. + +## 3. Double transversals, `n ≤ 4` + +**Theorem.** Let `n ∈ {3, 4}` and `L = 2n`. On every simple restored universal +word, every functional of weight at least `n - 1` is sound for the substituted +budget: it does not falsely prune. + +*Proof.* Length `2n` and positive even label counts force every label to occur +exactly twice. + +The all-ones functional has weight `n`. Every step flips it, so its level sets +are the two time-parity classes and `s = t = n`. Then `d = 0`, the correct +budget equals `base`, and `a + b ≤ base`. The substitution does not reject a +word the correct budget admits. + +A weight-`(n - 1)` functional misses exactly one label. That label occurs +twice, so exactly two steps preserve the functional. The first lemma gives +`|s - t| ≤ 2`. If `s = t`, then again `d = 0` and there is no false prune. +If `|s - t| = 2`, the class sizes are `n + 1` and `n - 1`. + +For `n = 4` those sizes are 5 and 3, and the kernel is a 3-dimensional space. +The size-5 class lies in one coset of the kernel. By the five-point lemma its +pair sums are all seven nonzero kernel vectors. The size-3 class contributes +three further pair sums. Pair slots number `C(5, 2) + C(3, 2) = 13`, so + +``` +a + b = 13 - (7 + 3) = 3. +``` + +Here `base(4, 8) = 5`, and `3 ≤ 5`, so the strict false-prune inequality fails. + +For `n = 3` the sizes are 4 and 2, and the kernel is `F_2^2`. The size-4 class +is a whole coset, whose pair sums are all three nonzero kernel vectors. The +size-2 class contributes one pair sum. Pair slots number `C(4, 2) + C(2, 2) = 7`, +so `a + b = 7 - 4 = 3`. Here `base(3, 6) = 3`. Equality does not satisfy +`base < a + b`, so the word is not falsely pruned. + +The verifier recomputes every restricted-growth simple universal word in both +domains (4 words at `(3, 6)`, 22 at `(4, 8)`) and checks the size and excess +claims for every mask of weight at least `n - 1`. Restricted growth is a +label-introduction normal form: it does not drop a geometric word, and the +masks are the functionals in that normal form. The predicate is not vacuous. +The word `01021323` is universal and the coordinate-bit-0 functional falsely +prunes it, with split `(6, 2)` and excess 8 against base 5. + +## 4. The weight pattern is not a law + +At `(4, 12)` the positive even compositions of 12 into four parts are +`4, 4, 2, 2` and `6, 2, 2, 2`. A weight-3 functional that omits a label of +count 4 or 6 therefore preserves four or six steps, and the two-stay lemma +no longer caps `d`. An independent enumeration of the 314 restricted-growth +simple universal words finds: + +| mask | omitted label | false prunes | +|---:|---:|---:| +| `0111` | 3 | 0 | +| `1011` | 2 | 4 | +| `1101` | 1 | 4 | +| `1110` | 0 | 4 | + +Weight at least `n - 1` is not a soundness law once a label may occur four +times. #3733 measured this domain first, including the further fact that only +`0111` and `1111` stay sound among the high-weight masks. The count above is +recomputed here and is not imported from that package. The four firing words +for each of the three masks are the explicit reason not to generalise the +`(4, 8)` and `(5, 12)` tables. + +## 5. The two weight-`(n - 2)` exceptions are finite + +#3699's other open description is that mask `1010` does not fire at `(4, 8)` +and mask `11010` does not fire at `(5, 12)`, although every other mask of the +same weight does. Both masks have weight `n - 2`, so Section 3 does not apply. + +On all 22 universal words at `(4, 8)`, mask `1010` has excess at most 3, and +`3 ≤ base = 5`. On all 828 universal words at `(5, 12)`, mask `11010` has +excess at most 14, and `14 ≤ base = 15`. Both statements are enumerations. +The second is tight by one unit. Neither enumeration is a structural proof, +and neither is the `(7, 18)` census. + +## 6. What is not claimed + +This does not run `survey(7, 18)` or `survey(7, 20)`, does not decide `f(7)`, +and does not repair a retained engine. Rows with no universal word support no +prune conclusion. Nothing here changes a supplier, a tariff, or the selected +conditional `κ`. diff --git a/research/f7-codim-one-substitution-soundness/README.md b/research/f7-codim-one-substitution-soundness/README.md new file mode 100644 index 0000000000..4abeb11e02 --- /dev/null +++ b/research/f7-codim-one-substitution-soundness/README.md @@ -0,0 +1,130 @@ +# Codimension-one soundness of the fixed `L/2` substitution + +**Proof for double transversals, plus two finite ledgers. No new κ.** + +On simple restored universal words with `n ∈ {3, 4}` and `L = 2n`, every +label-basis linear functional of Hamming weight at least `n - 1` is sound for +the substituted budget `base(n, L)`. It does not falsely prune. The argument +is in [PROOF.md](PROOF.md). The same weight pattern is not a law: at `(4, 12)` +three of the four weight-3 masks do falsely prune. + +Selected conditional κ stays `0.001672660197076918`. This does not change the +frontier, does not decide `f(7)`, and does not run `survey(7, 18)`. + +## Scope + +Catalogue card: `census-pruning-audit` (priority revision 6). Scope status: +**refined**. + +The fourteenth session slot fell on a 12-item handoff list by +`(14 - 1) mod 12 = 1`. That item is [Discussion #1166 comment +19021170](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19021170), +question 1: the `(7, 18)` / `(7, 20)` functional census. This package answers +question 2 of the same comment instead. #3699 measured that weight at least +`n - 1` does not fire on its small domains and wrote that the regularity was +not a theorem. #3733 then showed it is not a weight-threshold law. + +The card's premise is unchanged in this narrower sense: the object is still +the word-census parity substitution, and the bit-0 witness `01021323` is +retained as the control that the predicate still detects a false prune. +Launching the seven-label census is a scope-change trigger on the card, so +that census stays an open question. + +Base commit: `bb4bccbf42844d2801487450727c2f63e10d1d0f`. Provenance pins are in +[SOURCES.json](SOURCES.json). No live inputs. The predecessor enumerators are +not imported. + +## Result + +The walk is `q_0 = 0`, `q_{i+1} = q_i XOR e_{w_i}`. A word is simple when the +`L` prefix states are distinct, restored when every label occurs a positive +even number of times, and universal when those states sum to `F_2^n`. False +pruning means `base < a + b ≤ base + d²`, with `d = (s - t) / 2` and + +``` +base(n, L) = 2 C(L/2, 2) - (2^{n-1} - 1). +``` + +For `L = 2n` every label occurs twice. The all-ones functional alternates, so +`d = 0`. A weight-`(n - 1)` functional has exactly two preserving steps, hence +`|s - t| ≤ 2`. The unbalanced classes have sizes `n + 1` and `n - 1`. Their +excess is exactly 3. That equals `base(3, 6) = 3` and is strictly below +`base(4, 8) = 5`. Equality is not a false prune. + +The weight pattern stops as soon as a label may occur four times. An +independent enumeration of the 314 restricted-growth universal words at +`(4, 12)` gives: + +| mask | omitted label | false prunes | +|---:|---:|---:| +| `0111` | 3 | 0 | +| `1011` | 2 | 4 | +| `1101` | 1 | 4 | +| `1110` | 0 | 4 | + +Two further statements are finite ledgers, not theorems. Mask `1010` has +excess at most 3 on all 22 words at `(4, 8)`, and `3 ≤ base = 5`. Mask +`11010` has excess at most 14 on all 828 words at `(5, 12)`, and +`14 ≤ base = 15`. + +## Reproduce + +Python 3.12, standard library only. From the repository root: + +```sh +python3 scripts/research_package.py --package research/f7-codim-one-substitution-soundness --check-only +python3.12 scripts/research_package.py --package research/f7-codim-one-substitution-soundness +``` + +Direct commands: + +```sh +python3 -B research/f7-codim-one-substitution-soundness/verify.py +python3 -B research/f7-codim-one-substitution-soundness/test_verify.py +``` + +The first prints `PASS_F7_CODIM_ONE_SUBSTITUTION_SOUNDNESS` and a JSON receipt. +The second prints `PASS_F7_CODIM_ONE_SUBSTITUTION_TESTS groups=4`. A local run +finished in well under a second. That runtime is not a portability claim. + +The restricted-growth enumerator is a cross-check. The inequality for +`n ≤ 4` and `L = 2n` is proved for every word, not only for the normal form. +Rows with no universal word would not support a prune conclusion; both theorem +domains are nonempty. Nothing here was run under a proof assistant. + +## Open next questions + +1. **Which functionals fire at `(7, 18)` and `(7, 20)`?** Comment 19021170 + names this as the census that can change a maintained exclusion. The + enumerator in #3699 has `survey(7, 18)` wired and not run. This package + does not run it. Blocker: seven-label state count and a separate resource + budget. + +2. **Why are masks `1010` at `(4, 8)` and `11010` at `(5, 12)` the only + weight-`(n - 2)` exceptions?** The second ledger is tight by one unit + (excess 14 against base 15). A first step is to list the words that meet + excess 14 and compare them with a firing neighbor such as mask `10101`. + Blocker: no structural classification; the ledgers are enumerations. + +3. **For which lengths above `2n` does weight at least `n - 1` stay sound?** + `(4, 12)` is already a counterexample to a general law. `(4, 10)` and the + weight-at-least-4 masks at `(5, 12)` were measured sound by #3699 and #3733 + and are not proved here. The obstruction is that four preserving steps can + change the class sizes by 4, and `n + 1 > 2^{n-2}` only for `n ≤ 4`, so the + pair-sum closure used above stops there. + +## Credit + +The singleton prefix walk is the PR943 model used by #2542, #2634 and #2691. +Nicholas Stone wrote the word-census correction and its `MATH.md` (#2973). +The false-prune predicate and the measured weight table, including the two +exceptions and the statement that they were not a theorem, are from #3699 +(`research/f7-bit0-functional-classification`). #3733 +(`research/f7-functional-independent-check`) first recorded that `(4, 12)` +breaks a weight threshold; the counts in this package were recomputed and not +imported. James Reed's bit-0 audit is #3096. Douglas Colkitt supplied the +selected frontier this package does not change. + +Prepared by unpaidmoon. Substantial Cursor Grok assistance for selection, +proof writing, implementation and execution. No independent human or +formal-kernel review is claimed. New work is Apache-2.0. diff --git a/research/f7-codim-one-substitution-soundness/SOURCES.json b/research/f7-codim-one-substitution-soundness/SOURCES.json new file mode 100644 index 0000000000..a604c6a640 --- /dev/null +++ b/research/f7-codim-one-substitution-soundness/SOURCES.json @@ -0,0 +1,18 @@ +{ + "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" + } + ] +} diff --git a/research/f7-codim-one-substitution-soundness/TASK.json b/research/f7-codim-one-substitution-soundness/TASK.json new file mode 100644 index 0000000000..733ae19076 --- /dev/null +++ b/research/f7-codim-one-substitution-soundness/TASK.json @@ -0,0 +1,78 @@ +{ + "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": "Prove that, on simple restored universal words with n in {3,4} and L=2n, every label-basis functional of Hamming weight at least n-1 is sound for the fixed L/2 substitution, and record that this weight pattern is not a general law.", + "scope_change_reason": "Session item 14 fell on a 12-item handoff list by (14-1) mod 12 = 1, which is Discussion #1166 comment 19021170 question 1, the (7,18)/(7,20) functional census. That census is left open. This package answers question 2 of the same comment: why weight at least n-1 does not falsely prune on the double-transversal domains, which #3699 measured and explicitly did not prove. It does not rerun survey(7,18) or survey(7,20).", + "bottleneck_link": "Side result on the prune's dependency boundary. Soundness of the L/2 substitution for weight at least n-1 on double transversals does not by itself invalidate or repair a retained exclusion. It separates those functionals from the bit-0 defect on 01021323, which still falsely prunes.", + "budget_minutes": 60, + "stop_rule": "Stop after the n in {3,4}, L=2n proof, the independent (4,12) counterexample to a weight-threshold law, and finite ledgers of the two weight-(n-2) exceptions. Do not launch the seven-label census.", + "outcome": "completed", + "evidence": "PROOF.md is the argument. verify.py recomputes it: 245 two-stay pairs, 560 triples, 56 five-subsets, 4 universal words at (3,6) and 22 at (4,8) with no weight >= n-1 false prune, witness 01021323 still false-pruned by bit 0 at split (6,2) excess 8 against base 5, 314 words at (4,12) with weight-3 fires {0111:0, 1011:4, 1101:4, 1110:4}, and exception maxima 3 and 14. Author-checked executable proof plus finite certificates. No human or formal-kernel review. No new kappa.", + "author": "unpaidmoon", + "ai_assistance": "Substantial Cursor Grok assistance for selection, proof writing, implementation and execution. No independent human or formal-kernel review claimed.", + "open_questions": [ + { + "question": "Which nonzero functionals falsely prune simple restored universal words at (7,18) and (7,20)?", + "why_it_matters": "Comment 19021170 identifies that census as the domain that can change a maintained exclusion. This package deliberately does not run it.", + "first_step": "Budget a separate replay of the survey(7,18) and survey(7,20) entry points already named by #3699, and compare firing functionals with the corrected weight-parity budgets.", + "blocked_by": "The seven-label state count. No resource budget is claimed here, and survey(7,18) is not executed." + }, + { + "question": "Is there a structural reason that mask 1010 is sound at (4,8) and mask 11010 is sound at (5,12), while every other mask of weight n-2 fires?", + "why_it_matters": "These are the two exceptions #3699 left open. The (5,12) ledger is tight by one unit, so a weight-(n-2) threshold would be false, and a one-line slack argument would also be false.", + "first_step": "List the (5,12) words whose mask-11010 excess equals 14 and compare their class sizes with a firing neighbor such as mask 10101.", + "blocked_by": "No structural classification yet. The ledgers in this package are finite enumerations only." + }, + { + "question": "For which lengths above 2n does weight at least n-1 remain sound?", + "why_it_matters": "The two-stay proof uses that every label occurs twice. At (4,12) three weight-3 masks already fire, so the pattern is not a law. (4,10) and the weight >=4 masks at (5,12) were measured sound by #3699 and #3733 and are still unproved.", + "first_step": "Case-split a weight-(n-1) functional by the omitted label's multiplicity at (4,10), where four stays are possible but the measured excess never exceeds the base.", + "blocked_by": "Four stays can change the class sizes by 4, and a class of size n+1 need not cover every nonzero kernel sum once n>4, since n+1 > 2^{n-2} holds only for n<=4." + } + ] +} diff --git a/research/f7-codim-one-substitution-soundness/VERIFY.json b/research/f7-codim-one-substitution-soundness/VERIFY.json new file mode 100644 index 0000000000..4e86ca8f49 --- /dev/null +++ b/research/f7-codim-one-substitution-soundness/VERIFY.json @@ -0,0 +1,27 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Two-stay interval lemma, three-point sums, five-point cover of F_2^3, exact excess for every weight >= n-1 mask on the (3,6) and (4,8) universal words, bit-0 false prune of 01021323, independent (4,12) weight-3 firing counts, and the two weight-(n-2) exception ledgers." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 60, + "checks": "Failure controls: a 4-subset of F_2^3 misses a direction, four preserving steps can unbalance by at least 2, and on 01021323 bit 0 falsely prunes while mask 1110 does not." + } + ] +} diff --git a/research/f7-codim-one-substitution-soundness/test_verify.py b/research/f7-codim-one-substitution-soundness/test_verify.py new file mode 100644 index 0000000000..9c532c81d4 --- /dev/null +++ b/research/f7-codim-one-substitution-soundness/test_verify.py @@ -0,0 +1,43 @@ +#!/usr/bin/env python3 +"""Failure controls for the codimension-one substitution argument.""" + +import importlib.util +from pathlib import Path + + +def load(): + path = Path(__file__).with_name("verify.py") + spec = importlib.util.spec_from_file_location("codim_one", path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def require(condition, message): + if not condition: + raise SystemExit(message) + + +def main(): + module = load() + missed = {left ^ right for left, right in ((0, 1), (0, 2), (0, 3), (1, 2), (1, 3), (2, 3))} + require(1 not in missed or missed != set(range(1, 8)), "control setup") + require(len(missed) < 7, "a 4-subset of F_2^3 need not cover every direction") + + wide = module.kernel_count(8, (0, 1, 2, 3)) + require(abs(wide - 4) >= 2, "four preserving steps can unbalance by more than two") + + witness = (0, 1, 0, 2, 1, 3, 2, 3) + states = module.prefix_states(witness) + require(module.restored(witness, 4) and module.universal(states, 4), "fixture") + bit0, _ = module.falsely_pruned(4, 8, states, 0b0001) + high, _ = module.falsely_pruned(4, 8, states, 0b1110) + require(bit0 and not high, "bit 0 fires on the fixture and a weight-3 mask does not") + + module.two_stay_lemma() + module.five_point_cover() + print("PASS_F7_CODIM_ONE_SUBSTITUTION_TESTS groups=4") + + +if __name__ == "__main__": + main() diff --git a/research/f7-codim-one-substitution-soundness/verify.py b/research/f7-codim-one-substitution-soundness/verify.py new file mode 100644 index 0000000000..fa7dac78e5 --- /dev/null +++ b/research/f7-codim-one-substitution-soundness/verify.py @@ -0,0 +1,275 @@ +#!/usr/bin/env python3 +"""Codimension-one soundness of the fixed L/2 substitution on double transversals. + +The walk is the PR943 singleton prefix model: q_0 = 0 and +q_{i+1} = q_i XOR (1 << w_i). A word is restored when every label occurs a +positive even number of times, simple when q_0, ..., q_{L-1} are distinct, and +universal when the sumset of those states is F_2^n. + +False pruning means the substituted budget base(n, L) rejects a universal word +that the actual class sizes still admit. This verifier checks the written +argument in PROOF.md. It does not import a predecessor enumerator. + +Apache-2.0. +""" + +import json +from itertools import combinations + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def binom2(k): + return k * (k - 1) // 2 + + +def parity(value): + return bin(value).count("1") & 1 + + +def base_budget(n, length): + require(length % 2 == 0 and length > 0, "even positive length") + half = length // 2 + return 2 * binom2(half) - ((1 << (n - 1)) - 1) + + +def kernel_count(length, stays): + """Number of prefix states q_0, ..., q_{L-1} in the kernel of f. + + `stays` are the step indices that preserve f. Every other step flips f, + and f(q_0) = 0. + """ + stay = set(stays) + require(len(stay) == len(stays), "duplicate stay") + bit = 0 + zeros = 0 + for index in range(length): + if bit == 0: + zeros += 1 + if index not in stay: + bit ^= 1 + return zeros + + +def two_stay_lemma(lengths=(6, 8, 10, 12, 14)): + """Exactly two preserving steps change the zero count by at most one.""" + checked = 0 + for length in lengths: + require(length % 2 == 0, "even length") + balanced = length // 2 + for i, j in combinations(range(length), 2): + zeros = kernel_count(length, (i, j)) + require(abs(zeros - balanced) <= 1, f"two-stay imbalance {length} {i} {j}") + # The patterns differ from k |-> k mod 2 exactly on (i, j]. + interval = range(i + 1, j + 1) + evens = sum(1 for k in interval if k % 2 == 0) + odds = sum(1 for k in interval if k % 2 == 1) + require(zeros - balanced == odds - evens, "interval delta") + checked += 1 + four_stay = kernel_count(8, (1, 2, 3, 4)) + require(abs(four_stay - 4) == 2, "four stays can leave the two-stay bound") + return checked + + +def three_point_sums(dimension=4): + """Any three distinct vectors have three distinct pairwise sums.""" + space = range(1 << dimension) + checked = 0 + for triple in combinations(space, 3): + sums = {triple[0] ^ triple[1], triple[0] ^ triple[2], triple[1] ^ triple[2]} + require(len(sums) == 3 and 0 not in sums, "three-point sums") + checked += 1 + return checked + + +def five_point_cover(): + """Every 5-subset of F_2^3 meets every nonzero direction.""" + space = range(8) + checked = 0 + for subset in combinations(space, 5): + sums = {left ^ right for left, right in combinations(subset, 2)} + require(sums == set(range(1, 8)), "five-point cover") + checked += 1 + # Sharpness: some 4-subset misses a direction. + missed = {left ^ right for left, right in combinations((0, 1, 2, 3), 2)} + require(missed != set(range(1, 8)), "four-point cover is not forced") + return checked + + +def prefix_states(word): + state = 0 + states = [0] + for label in word: + state ^= 1 << label + states.append(state) + return states + + +def restored(word, n): + counts = [0] * n + for label in word: + counts[label] += 1 + return all(count > 0 and count % 2 == 0 for count in counts) + + +def universal(states, n): + occupied = set(states[:-1]) + require(len(occupied) == len(states) - 1, "simple prefix") + return {left ^ right for left in occupied for right in occupied} == set(range(1 << n)) + + +def class_excess(states, mask): + occupied = set(states[:-1]) + even = [point for point in occupied if parity(point & mask) == 0] + odd = [point for point in occupied if parity(point & mask) == 1] + even_sums = {left ^ right for left, right in combinations(even, 2)} + odd_sums = {left ^ right for left, right in combinations(odd, 2)} + excess = binom2(len(even)) + binom2(len(odd)) - len(even_sums) - len(odd_sums) + return len(even), len(odd), excess + + +def falsely_pruned(n, length, states, mask): + even, odd, excess = class_excess(states, mask) + base = base_budget(n, length) + slack = ((even - odd) // 2) ** 2 + return base < excess <= base + slack, (even, odd, excess, base, base + slack) + + +def enumerate_words(n, length): + seen = {0} + word = [] + + def walk(index, state, max_label): + if index == length: + yield tuple(word) + return + for label in range(min(max_label + 2, n)): + nxt = state ^ (1 << label) + if index == length - 1: + if nxt == 0: + word.append(label) + yield from walk(index + 1, 0, max(max_label, label)) + word.pop() + continue + if nxt in seen: + continue + seen.add(nxt) + word.append(label) + yield from walk(index + 1, nxt, max(max_label, label)) + word.pop() + seen.discard(nxt) + + yield from walk(0, 0, -1) + + +def universal_words(n, length): + words = [] + for word in enumerate_words(n, length): + if not restored(word, n): + continue + states = prefix_states(word) + if universal(states, n): + words.append(word) + return words + + +def weight_masks(n, weight): + return [mask for mask in range(1, 1 << n) if bin(mask).count("1") == weight] + + +def double_transversal_theorem(): + """Weight at least n-1 is sound for every simple universal word of length 2n, n<=4.""" + summary = {} + for n in (3, 4): + length = 2 * n + words = universal_words(n, length) + base = base_budget(n, length) + per_weight = {} + for weight in range(n - 1, n + 1): + fires = {} + for mask in weight_masks(n, weight): + fires[mask] = 0 + for word in words: + states = prefix_states(word) + hit, detail = falsely_pruned(n, length, states, mask) + even, odd, excess, got_base, _correct = detail + require(got_base == base, "base") + require(not hit, f"codimension-one false prune n={n} mask={mask}") + if weight == n: + require(even == odd == n, "all-ones classes are time parity") + require(excess <= base, "all-ones excess") + else: + require(abs(even - odd) <= 2, "two-stay size bound") + if abs(even - odd) == 2: + if n == 4: + require(excess == 3, "exact five-plus-three excess") + if n == 3: + require(excess == base, "tight n=3 excess") + fires[mask] += int(hit) + require(all(count == 0 for count in fires.values()), "no fires") + per_weight[weight] = len(fires) + summary[f"{n},{length}"] = {"universal": len(words), "weights": per_weight, "base": base} + require(summary["4,8"]["universal"] == 22, "published (4,8) universal count") + require(summary["3,6"]["universal"] == 4, "published (3,6) universal count") + # Known bit-0 false prune, so the predicate is not vacuously strict. + witness = (0, 1, 0, 2, 1, 3, 2, 3) + hit, detail = falsely_pruned(4, 8, prefix_states(witness), 0b0001) + require(hit and detail == (6, 2, 8, 5, 9), "bit-0 witness still false-prunes") + return summary + + +def weight_law_fails_at_four_twelve(): + """Three weight-3 masks fire at (4, 12); omitting only the last label does not.""" + words = universal_words(4, 12) + counts = {} + for mask in weight_masks(4, 3): + counts[mask] = sum( + falsely_pruned(4, 12, prefix_states(word), mask)[0] for word in words + ) + require(counts[0b0111] == 0, "last-coordinate omission stays sound") + require(counts[0b1011] == 4 and counts[0b1101] == 4 and counts[0b1110] == 4, + "the other three weight-3 masks fire") + require(len(words) == 314, "published (4,12) universal count") + return {"universal": len(words), "weight3_fires": counts} + + +def exception_ledger(): + """Finite soundness of the two published weight-(n-2) exceptions. Not a theorem.""" + rows = [] + for n, length, mask, expected_words, expected_max in ( + (4, 8, 0b1010, 22, 3), + (5, 12, 0b11010, 828, 14), + ): + words = universal_words(n, length) + require(len(words) == expected_words, "exception domain count") + base = base_budget(n, length) + max_excess = 0 + fires = 0 + for word in words: + hit, detail = falsely_pruned(n, length, prefix_states(word), mask) + fires += int(hit) + max_excess = max(max_excess, detail[2]) + require(fires == 0 and max_excess == expected_max and max_excess <= base, + "exception ledger") + rows.append({"n": n, "L": length, "mask": mask, "max_excess": max_excess, "base": base}) + return rows + + +def main(): + receipt = { + "two_stay_pairs": two_stay_lemma(), + "three_point_triples": three_point_sums(), + "five_point_subsets": five_point_cover(), + "double_transversal": double_transversal_theorem(), + "four_twelve": weight_law_fails_at_four_twelve(), + "exceptions": exception_ledger(), + "new_kappa": False, + } + print("PASS_F7_CODIM_ONE_SUBSTITUTION_SOUNDNESS " + json.dumps(receipt, sort_keys=True)) + + +if __name__ == "__main__": + main()