diff --git a/research/f7-bit0-functional-classification/MATH.md b/research/f7-bit0-functional-classification/MATH.md new file mode 100644 index 0000000000..61ef5cd0c6 --- /dev/null +++ b/research/f7-bit0-functional-classification/MATH.md @@ -0,0 +1,101 @@ +# Why the fixed `L/2` substitution has a justification for one functional + +This note is local to the PR943 singleton prefix-walk model used by +PR2542/PR2634/PR2691 and corrected by #2973. It is the mathematical content of +`verify.py`; the numeric receipt is in [RESULT.json](RESULT.json). + +## 1. Setup + +For a word `w` of length `L` over `[0, n)`, put `q_0 = 0` and + +``` +q_{i+1} = q_i XOR (1 << w_i), +``` + +and let `S` be the **set** of distinct prefix states. Restoration means every +label occurs a positive even number of times, so `q_L = q_0` and `L` is even. +Universality is `S + S = F2^n`. A walk is *simple* when `q_0 .. q_{L-1}` are +distinct; the closing state adds no new point. + +A nonzero linear functional `l` with indicator vector `v in F2^n` partitions `S` +into its kernel class `E` and other coset `O`. Write `s = |E|`, `t = |O|`, and + +``` +a = C(s,2) - |{x XOR y : x != y, x, y in E}|, +b = C(t,2) - |{x XOR y : x != y, x, y in O}|. +``` + +## 2. The correct budget, for any functional + +`E` is a linear subspace of codimension one, so `E \ {0}` has `Q - 1` elements +with `Q = 2^(n-1)`, and `O + O` lands in `O` while `E + E` lands in `E`. If `S` is +universal then every nonzero kernel-coset mask is a sum of two distinct points of +`E`, and every mask of the other coset is a sum of a point of `E` and one of `O`. +Hence + +``` +a + b <= C(s,2) + C(t,2) - (Q - 1). +``` + +Nothing in this argument mentions weight parity. Setting `s = L/2 + d` and +`t = L/2 - d` and using `C(m+d,2) + C(m-d,2) = 2C(m,2) + d^2`, define + +``` +base(n, L) = 2C(L/2, 2) - (Q - 1), +correct budget = base(n, L) + d^2. +``` + +**The word-level defect in the retained engines is substituting `L/2, L/2` while +grouping by some functional `l`.** That substitution is valid exactly when +`s <= L/2` and `t <= L/2`; it is *stronger* than the true budget by exactly the +slack `d^2`, and it is sound for a given word only when + +``` +a + b <= base(n, L). +``` + +A word is **falsely pruned** when `base < a + b <= base + d^2`: the substituted +budget rejects a universal word that the correct budget admits. + +## 3. The alternation lemma + +**Lemma.** For every `i in [0, L)` and every functional `l_v`, + +``` +l_v(q_{i+1}) XOR l_v(q_i) = v_{w_i}. +``` + +*Proof.* `q_{i+1} XOR q_i = 1 << w_i = e_{w_i}`, and `l_v` is linear, so +`l_v(q_{i+1}) XOR l_v(q_i) = l_v(e_{w_i}) = v_{w_i}`. Done. + +`verify.py` checks this identity on every emitted word at `(4, 8)` for all 15 +nonzero `v` (3480 checks) and raises on any violation. + +**Corollary.** `l_v(q_i) = i mod 2` for all `i` if and only if `v = 1^n`. + +*Proof.* The forward direction forces `v_{w_i} = 1` for every `i`, so every label +of `w` lies in `supp(v)`; that alone does not give `v = 1^n`. The statement that +matters is the other one: `l_v(q_i) = i mod 2` holds for **every** walk only when +`v = 1^n`, because then each step flips the value. For any other `v` the class +value is constant across a step whose label lies outside `supp(v)`, so no +alternation is available. Formally: for `v != 1^n` pick a coordinate `j` outside +`supp(v)` and the walk that places label `j` on its first step; the value does not +flip there. Equivalently, weight parity *is* the all-ones functional. QED. + +## 4. What follows + +The bound `s, t <= L/2` used by the substitution is the statement that the two +classes are the time-parity classes. By the corollary that is available for +exactly one functional, the all-ones one `v = 1^n`. For every other functional +the class sizes are produced by the walk and are bounded only by `|S|`, so the +substitution can understate the budget by `d^2` and reject a universal word. + +That is a mechanism, not a census. Whether it actually fires, and for which +functionals, is measured in [RESULT.json](RESULT.json) and summarised in the +README table. The measured `weight >= n - 1` regularity is **not** derived here. + +## 5. Scope + +This is a scoped lemma plus a finite certificate on nine small `(n, L)` domains, +`n <= 7` and `L <= 14`. It is not a corrected seven-label census, does not decide +`f(7)`, and does not change any selected result, supplier or kappa. \ No newline at end of file diff --git a/research/f7-bit0-functional-classification/README.md b/research/f7-bit0-functional-classification/README.md new file mode 100644 index 0000000000..4618c68ffc --- /dev/null +++ b/research/f7-bit0-functional-classification/README.md @@ -0,0 +1,187 @@ +# Independent functional classification of the fixed `L/2` word budget + +**Partial result. No new `f(7)` bound, no kappa, no selected-frontier change.** + +[PR2973](https://github.com/CrocSwap/integer-mult-bounds/pull/2973) (Nicholas Stone) +corrected the word-census engines retained by PR2542, PR2634 and PR2691. They group +prefix states by **coordinate bit 0** but apply a collision budget derived for +**Hamming-weight parity**, whose `s, t` are bounded by `L/2`. This package asks a +narrower and, so far as I can find, unanswered question: **is the bit-0 grouping +special, or is the substitution wrong for every non-parity functional?** + +Answer, measured exhaustively on a stated domain: **the substitution is not a +bit-0 artifact.** At `(n, L) = (4, 10)` and `(5, 12)` it falsely prunes a +universal word for **every** nonzero linear functional of Hamming weight `<= n - 2`, +and for **none** of weight `>= n - 1`. At `(4, 8)` the same holds except for one +weight-2 functional (`1010`). Bit 0 is simply the first member of that class. + +The regime the old seven-label censuses actually ran is **not** reached here. +See *Scope* below. + +## What is established, at the strength proved + +### 1. Independent reconstruction of the retained counterexample (measured) + +The canonical word `01021323` at `n = 4, L = 8` has prefix states + +``` +q_0..q_8 = 0, 1, 3, 2, 6, 4, 12, 8, 0 +``` + +All eight nonclosing states are distinct, every label occurs exactly twice, and +`S + S = F2^4` (the sumset has all 16 elements). Grouping by Hamming weight gives +the split `(4, 4)` with collision excess `0`. Grouping by coordinate bit 0 gives +the split `(6, 2)` with collision excess `8`. The substituted budget is +`C(4,2) + C(4,2) - 7 = 5`, so `8 > 5` rejects a universal word; the correct +budget for the actual bit-0 sizes is `C(6,2) + C(2,2) - 7 = 9`, and `8 <= 9`. +These are exactly the numbers in PR2973 section 4, reproduced here from scratch. + +### 2. The defect is not specific to bit 0 (finite certificate, exhaustive) + +Over **every** restricted-growth word of length `L` over `[0, n)` whose prefix +states `q_0 .. q_{L-1}` are distinct and whose last step returns to `q_0`, the +verifier classifies all `2^n - 1` nonzero linear functionals. + +| `n` | `L` | universal words | substituted budget | functionals that falsely prune | false prunes | +|---:|---:|---:|---:|---:|---:| +| 3 | 6 | 4 | 3 | none | 0 | +| 3 | 8 | 2 | 9 | none | 0 | +| 4 | 8 | 22 | 5 | 9 of 15 | 44 | +| 4 | 10 | 110 | 13 | 10 of 15 | 190 | +| 5 | 10 | 0 | 5 | none | 0 | +| 5 | 12 | 828 | 15 | 24 of 31 | 2856 | +| 6 | 12 | 0 | -1 | none | 0 | +| 6 | 14 | 0 | 11 | none | 0 | +| 7 | 14 | 0 | -21 | none | 0 | + +The functional weight pattern, measured: + +| domain | firing weights | sound weights | exception | +|---|---|---|---| +| `(4, 8)` | 1, 2 | 2, 3, 4 | mask `1010` (weight 2) does not fire | +| `(4, 10)` | 1, 2 | 3, 4 | none | +| `(5, 12)` | 1, 2, 3 | 3, 4, 5 | mask `11010` (weight 3) does not fire | + +At `(4, 8)` the verifier also finds **6** false prunes under bit 0 specifically, +and 22 universal simple words. Both figures agree with the independent +[PR3096 audit](../f7-bit0-false-prune/README.md) ("leaves 6", "22 simple canonical +universal words"), which I did not consult while writing this enumerator. + +### 3. Why the substitution has a justification for exactly one functional + +**Lemma (machine-checked on every word at `(4, 8)`, 3480 checks).** For a +nonzero linear functional with indicator vector `v`, + +``` +l(q_{i+1}) XOR l(q_i) = v_{w_i}. +``` + +So the class value flips at step `i` exactly when the label placed at step `i` +lies in the support of `v`. For `v = 1^n` every step flips, so `l(q_i) = i mod 2` +and the two classes *are* the weight-parity classes, whose sizes are bounded by +`L/2`. The `L/2` substitution therefore rests on an identity that holds for the +all-ones functional and for **no** other. For every other functional the class +sizes are whatever the word happens to produce, which is what the `d*d` slack +term measures. + +The measured `weight >= n - 1` safety in the table above is *not* proved by this +lemma. It is an empirical regularity of these two domains. See open questions. + +## Scope, and what is deliberately not claimed + +- This is a **finite certificate on a stated small domain plus one scoped + lemma**. It is not a new `f(7)` bound, not a corrected seven-label census, and + not a proof that any old exclusion is wrong or right. +- **The seven-label decision regime is not reached.** PR2542's decisive call is + `cyclic_census(7, 18, budget=9, simple=True)` and PR2634/PR2691 extend to + `L = 20`. The only seven-label domain here is `(7, 14)`, which has **zero** + universal simple words, so it is vacuous. A `(7, 18)` or `(7, 20)` functional + census is a separate resource budget and a separate named decision; this + package does not decide whether the old exclusion would have changed there. +- Rows `(5, 10)`, `(6, 12)`, `(6, 14)` and `(7, 14)` have zero universal simple + words, so "no false prune" there is a statement about an empty set. +- `substituted budget = -1` at `(6, 12)` and `-21` at `(7, 14)` is a measured + observation: at those parameters the old substitution is negative, so it would + reject every candidate immediately. This is not offered as a correction. +- Nothing here revives or refutes PR2542's counting bound, pair identity, + restoration parity or the verified Gray constructions, and nothing here revives + the later set-level work (#2773, #2870, #2911, #2933, #2961) on its own + hypotheses. +- Universality is `S + S = F2^n` over the **distinct** prefix states. The closing + state `q_L = q_0` is not counted as a second point; that deduplication is + explicit in `split_stats`. + +## Reproduce + +Python 3.12 standard library only, from the repository root: + +```sh +python3 -I -B research/f7-bit0-functional-classification/verify.py +python3 -I -O -Werror -B research/f7-bit0-functional-classification/test_verify.py +``` + +The first command re-runs all nine domains, the separately written brute-force +cross-check at `(3,6)`, `(3,8)` and `(4,8)`, the `01021323` fixture and the +alternation lemma, then requires the freshly computed receipt to equal the +committed `RESULT.json` byte-for-byte after JSON canonicalisation. Its marker is +`PASS_F7_BIT0_FUNCTIONAL_CLASSIFICATION`. `--emit` rewrites `RESULT.json`. + +`test_verify.py` adds 18 behavioural tests, including negative controls for the +domain bounds, the restoration predicate, the closing-state deduplication and +the receipt's internal consistency. + +Runtime on the recorded host (Apple arm64) is about 1.5 s for the tests and +about 5 s for the verifier. Host and interpreter affect timing, not the counts. + +**Executed interpreter.** These two commands were run locally under CPython +**3.15.0**, not 3.12: `python3.12` is not installed on this host. The code is +standard library only and uses no version-specific syntax, but the repository's +registered replay hook requires 3.12, so +`python3 -B scripts/research_package.py --package research/f7-bit0-functional-classification` +was **not** executed here. `scripts/research_package.py --package +research/f7-bit0-functional-classification --check-only` was executed and returns +`PASS_PACKAGE_METADATA_AND_PINS`. + +## Implementation notes + +`verify.py` is an independent implementation. No predecessor package code is +imported or executed; `SOURCES.json` pins the reference documents by hash and +marks them `usage: reference`. + +The primary enumerator prunes on prefix-state distinctness and forces the final +step to land on `q_0`. The cross-check enumerator walks `product(range(n), +repeat=L)` with no pruning and filters afterwards. Agreement of +`simple_closed_words` and `universal_words` on three domains is asserted on every +run; it is the check that caught an off-by-one in the walk's starting step during +development. + +## Open next questions + +1. **The `(7, 18)` and `(7, 20)` functional census.** This is the only domain that + changes a maintained decision. It needs its own budget; the enumerator is + reusable but the state count at seven labels is large. +2. **Why weight `>= n - 1` is safe in these domains.** The alternation lemma + explains why the `L/2` substitution is *justified* only for the all-ones + functional. It does not explain why high-weight functionals happen not to + *fire*. A proof or a counterexample at `(5, 14)` would settle it. +3. **The two exceptions**, masks `1010` at `(4, 8)` and `11010` at `(5, 12)`. + If a weight-2 functional can be safe at one length and unsafe at another, the + weight threshold is a heuristic, not a rule, and should not be generalised. +4. **Whether a repair can keep the bit-0 grouping.** Using the actual class sizes + is sound for any functional, so the old traversal code could be repaired by + one substitution instead of being rewritten. That is a source-change question + for the maintainers, not a claim here. + +## Credit and scope + +Nicholas Stone wrote the word-census correction (#2973) and its `MATH.md`; +James Reed wrote the bit-0 small-domain audit (#3096); Ross Richardson supplied +the PR943 singleton prefix-walk model; Douglas Colkitt supplied the selected +source bindings and review. This package independently re-derives the retained +numbers and adds the functional classification and the alternation lemma. It does +not replace any of them. + +Nick Petalas. Apache-2.0. Substantial automated assistance in research, +implementation, checking and writing. Separate internal source inspection and +review do not constitute independent human or proof-assistant review. Full +selected replay, all-size transfer and hosted CI are not claimed. \ No newline at end of file diff --git a/research/f7-bit0-functional-classification/RESULT.json b/research/f7-bit0-functional-classification/RESULT.json new file mode 100644 index 0000000000..84017d1265 --- /dev/null +++ b/research/f7-bit0-functional-classification/RESULT.json @@ -0,0 +1,1438 @@ +{ + "alternation_checks": 3480, + "cross_check": [ + { + "L": 6, + "n": 3, + "universal": 4, + "words": 4 + }, + { + "L": 8, + "n": 3, + "universal": 2, + "words": 2 + }, + { + "L": 8, + "n": 4, + "universal": 22, + "words": 29 + } + ], + "domains": [ + { + "L": 6, + "base_budget": 3, + "false_prunes": 0, + "firing_masks": [], + "firing_weight_max": 0, + "n": 3, + "records": {}, + "simple_closed_words": 4, + "sound_masks": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ], + "universal_words": 4 + }, + { + "L": 8, + "base_budget": 9, + "false_prunes": 0, + "firing_masks": [], + "firing_weight_max": 0, + "n": 3, + "records": {}, + "simple_closed_words": 2, + "sound_masks": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ], + "universal_words": 2 + }, + { + "L": 8, + "base_budget": 5, + "false_prunes": 44, + "firing_masks": [ + 1, + 2, + 3, + 4, + 5, + 6, + 8, + 9, + 12 + ], + "firing_weight_max": 2, + "n": 4, + "records": { + "1": { + "count": 6, + "examples": [ + { + "correct_budget": 9, + "excess": 8, + "s": 6, + "substituted_budget": 5, + "t": 2, + "word": "01021323" + }, + { + "correct_budget": 9, + "excess": 8, + "s": 6, + "substituted_budget": 5, + "t": 2, + "word": "01023123" + } + ] + }, + "2": { + "count": 6, + "examples": [ + { + "correct_budget": 9, + "excess": 8, + "s": 2, + "substituted_budget": 5, + "t": 6, + "word": "01203231" + }, + { + "correct_budget": 9, + "excess": 8, + "s": 6, + "substituted_budget": 5, + "t": 2, + "word": "01213023" + } + ] + }, + "3": { + "count": 5, + "examples": [ + { + "correct_budget": 9, + "excess": 8, + "s": 6, + "substituted_budget": 5, + "t": 2, + "word": "01201323" + }, + { + "correct_budget": 9, + "excess": 8, + "s": 6, + "substituted_budget": 5, + "t": 2, + "word": "01230132" + } + ] + }, + "4": { + "count": 4, + "examples": [ + { + "correct_budget": 9, + "excess": 8, + "s": 6, + "substituted_budget": 5, + "t": 2, + "word": "01023213" + }, + { + "correct_budget": 9, + "excess": 8, + "s": 6, + "substituted_budget": 5, + "t": 2, + "word": "01202313" + } + ] + }, + "5": { + "count": 1, + "examples": [ + { + "correct_budget": 9, + "excess": 8, + "s": 2, + "substituted_budget": 5, + "t": 6, + "word": "01203132" + } + ] + }, + "6": { + "count": 5, + "examples": [ + { + "correct_budget": 9, + "excess": 8, + "s": 6, + "substituted_budget": 5, + "t": 2, + "word": "01203123" + }, + { + "correct_budget": 9, + "excess": 8, + "s": 6, + "substituted_budget": 5, + "t": 2, + "word": "01203213" + } + ] + }, + "8": { + "count": 8, + "examples": [ + { + "correct_budget": 9, + "excess": 8, + "s": 6, + "substituted_budget": 5, + "t": 2, + "word": "01021323" + }, + { + "correct_budget": 9, + "excess": 8, + "s": 6, + "substituted_budget": 5, + "t": 2, + "word": "01201323" + } + ] + }, + "9": { + "count": 4, + "examples": [ + { + "correct_budget": 9, + "excess": 8, + "s": 2, + "substituted_budget": 5, + "t": 6, + "word": "01203123" + }, + { + "correct_budget": 9, + "excess": 8, + "s": 2, + "substituted_budget": 5, + "t": 6, + "word": "01203213" + } + ] + }, + "12": { + "count": 5, + "examples": [ + { + "correct_budget": 9, + "excess": 8, + "s": 6, + "substituted_budget": 5, + "t": 2, + "word": "01023123" + }, + { + "correct_budget": 9, + "excess": 8, + "s": 6, + "substituted_budget": 5, + "t": 2, + "word": "01230132" + } + ] + } + }, + "simple_closed_words": 29, + "sound_masks": [ + 7, + 10, + 11, + 13, + 14, + 15 + ], + "universal_words": 22 + }, + { + "L": 10, + "base_budget": 13, + "false_prunes": 190, + "firing_masks": [ + 1, + 2, + 3, + 4, + 5, + 6, + 8, + 9, + 10, + 12 + ], + "firing_weight_max": 2, + "n": 4, + "records": { + "1": { + "count": 20, + "examples": [ + { + "correct_budget": 22, + "excess": 21, + "s": 8, + "substituted_budget": 13, + "t": 2, + "word": "0102131213" + }, + { + "correct_budget": 22, + "excess": 21, + "s": 8, + "substituted_budget": 13, + "t": 2, + "word": "0102321232" + } + ] + }, + "2": { + "count": 20, + "examples": [ + { + "correct_budget": 17, + "excess": 14, + "s": 3, + "substituted_budget": 13, + "t": 7, + "word": "0102030213" + }, + { + "correct_budget": 17, + "excess": 14, + "s": 3, + "substituted_budget": 13, + "t": 7, + "word": "0102032013" + } + ] + }, + "3": { + "count": 10, + "examples": [ + { + "correct_budget": 17, + "excess": 14, + "s": 7, + "substituted_budget": 13, + "t": 3, + "word": "0123021232" + }, + { + "correct_budget": 17, + "excess": 14, + "s": 7, + "substituted_budget": 13, + "t": 3, + "word": "0123031323" + } + ] + }, + "4": { + "count": 23, + "examples": [ + { + "correct_budget": 17, + "excess": 14, + "s": 7, + "substituted_budget": 13, + "t": 3, + "word": "0102032013" + }, + { + "correct_budget": 17, + "excess": 14, + "s": 7, + "substituted_budget": 13, + "t": 3, + "word": "0102032103" + } + ] + }, + "5": { + "count": 8, + "examples": [ + { + "correct_budget": 17, + "excess": 14, + "s": 7, + "substituted_budget": 13, + "t": 3, + "word": "0121302131" + }, + { + "correct_budget": 17, + "excess": 14, + "s": 7, + "substituted_budget": 13, + "t": 3, + "word": "0121310213" + } + ] + }, + "6": { + "count": 16, + "examples": [ + { + "correct_budget": 17, + "excess": 14, + "s": 7, + "substituted_budget": 13, + "t": 3, + "word": "0102030123" + }, + { + "correct_budget": 17, + "excess": 14, + "s": 7, + "substituted_budget": 13, + "t": 3, + "word": "0102030213" + } + ] + }, + "8": { + "count": 37, + "examples": [ + { + "correct_budget": 22, + "excess": 21, + "s": 8, + "substituted_budget": 13, + "t": 2, + "word": "0102010323" + }, + { + "correct_budget": 17, + "excess": 14, + "s": 7, + "substituted_budget": 13, + "t": 3, + "word": "0102013023" + } + ] + }, + "9": { + "count": 18, + "examples": [ + { + "correct_budget": 17, + "excess": 14, + "s": 3, + "substituted_budget": 13, + "t": 7, + "word": "0120131213" + }, + { + "correct_budget": 17, + "excess": 14, + "s": 3, + "substituted_budget": 13, + "t": 7, + "word": "0120232123" + } + ] + }, + "10": { + "count": 10, + "examples": [ + { + "correct_budget": 17, + "excess": 14, + "s": 3, + "substituted_budget": 13, + "t": 7, + "word": "0102013023" + }, + { + "correct_budget": 17, + "excess": 14, + "s": 3, + "substituted_budget": 13, + "t": 7, + "word": "0102013203" + } + ] + }, + "12": { + "count": 28, + "examples": [ + { + "correct_budget": 17, + "excess": 14, + "s": 7, + "substituted_budget": 13, + "t": 3, + "word": "0102030123" + }, + { + "correct_budget": 17, + "excess": 14, + "s": 7, + "substituted_budget": 13, + "t": 3, + "word": "0102030132" + } + ] + } + }, + "simple_closed_words": 110, + "sound_masks": [ + 7, + 11, + 13, + 14, + 15 + ], + "universal_words": 110 + }, + { + "L": 10, + "base_budget": 5, + "false_prunes": 0, + "firing_masks": [], + "firing_weight_max": 0, + "n": 5, + "records": {}, + "simple_closed_words": 358, + "sound_masks": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 20, + 21, + 22, + 23, + 24, + 25, + 26, + 27, + 28, + 29, + 30, + 31 + ], + "universal_words": 0 + }, + { + "L": 12, + "base_budget": 15, + "false_prunes": 2856, + "firing_masks": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 16, + 17, + 18, + 19, + 20, + 21, + 22, + 24, + 25, + 28 + ], + "firing_weight_max": 3, + "n": 5, + "records": { + "1": { + "count": 248, + "examples": [ + { + "correct_budget": 19, + "excess": 16, + "s": 8, + "substituted_budget": 15, + "t": 4, + "word": "010201032434" + }, + { + "correct_budget": 19, + "excess": 16, + "s": 8, + "substituted_budget": 15, + "t": 4, + "word": "010201034234" + } + ] + }, + "2": { + "count": 248, + "examples": [ + { + "correct_budget": 19, + "excess": 16, + "s": 8, + "substituted_budget": 15, + "t": 4, + "word": "010201032434" + }, + { + "correct_budget": 19, + "excess": 16, + "s": 8, + "substituted_budget": 15, + "t": 4, + "word": "010201034234" + } + ] + }, + "3": { + "count": 96, + "examples": [ + { + "correct_budget": 19, + "excess": 16, + "s": 8, + "substituted_budget": 15, + "t": 4, + "word": "010201032434" + }, + { + "correct_budget": 19, + "excess": 16, + "s": 8, + "substituted_budget": 15, + "t": 4, + "word": "010201034234" + } + ] + }, + "4": { + "count": 278, + "examples": [ + { + "correct_budget": 19, + "excess": 16, + "s": 4, + "substituted_budget": 15, + "t": 8, + "word": "010201304342" + }, + { + "correct_budget": 19, + "excess": 16, + "s": 4, + "substituted_budget": 15, + "t": 8, + "word": "010201340342" + } + ] + }, + "5": { + "count": 143, + "examples": [ + { + "correct_budget": 19, + "excess": 16, + "s": 8, + "substituted_budget": 15, + "t": 4, + "word": "010203143402" + }, + { + "correct_budget": 19, + "excess": 16, + "s": 8, + "substituted_budget": 15, + "t": 4, + "word": "010203413402" + } + ] + }, + "6": { + "count": 119, + "examples": [ + { + "correct_budget": 19, + "excess": 16, + "s": 4, + "substituted_budget": 15, + "t": 8, + "word": "010201304342" + }, + { + "correct_budget": 19, + "excess": 16, + "s": 4, + "substituted_budget": 15, + "t": 8, + "word": "010201340342" + } + ] + }, + "7": { + "count": 25, + "examples": [ + { + "correct_budget": 19, + "excess": 16, + "s": 8, + "substituted_budget": 15, + "t": 4, + "word": "010230102434" + }, + { + "correct_budget": 19, + "excess": 16, + "s": 8, + "substituted_budget": 15, + "t": 4, + "word": "010234010243" + } + ] + }, + "8": { + "count": 221, + "examples": [ + { + "correct_budget": 24, + "excess": 21, + "s": 9, + "substituted_budget": 15, + "t": 3, + "word": "010201032434" + }, + { + "correct_budget": 24, + "excess": 21, + "s": 9, + "substituted_budget": 15, + "t": 3, + "word": "010201034234" + } + ] + }, + "9": { + "count": 41, + "examples": [ + { + "correct_budget": 19, + "excess": 16, + "s": 8, + "substituted_budget": 15, + "t": 4, + "word": "010230103424" + }, + { + "correct_budget": 24, + "excess": 21, + "s": 3, + "substituted_budget": 15, + "t": 9, + "word": "012103121434" + } + ] + }, + "10": { + "count": 105, + "examples": [ + { + "correct_budget": 19, + "excess": 16, + "s": 4, + "substituted_budget": 15, + "t": 8, + "word": "010230104243" + }, + { + "correct_budget": 19, + "excess": 16, + "s": 4, + "substituted_budget": 15, + "t": 8, + "word": "010230140243" + } + ] + }, + "11": { + "count": 15, + "examples": [ + { + "correct_budget": 19, + "excess": 16, + "s": 4, + "substituted_budget": 15, + "t": 8, + "word": "010230104243" + }, + { + "correct_budget": 19, + "excess": 16, + "s": 8, + "substituted_budget": 15, + "t": 4, + "word": "012030142403" + } + ] + }, + "12": { + "count": 175, + "examples": [ + { + "correct_budget": 24, + "excess": 21, + "s": 9, + "substituted_budget": 15, + "t": 3, + "word": "010203104234" + }, + { + "correct_budget": 24, + "excess": 21, + "s": 9, + "substituted_budget": 15, + "t": 3, + "word": "010203104324" + } + ] + }, + "13": { + "count": 10, + "examples": [ + { + "correct_budget": 19, + "excess": 16, + "s": 4, + "substituted_budget": 15, + "t": 8, + "word": "012030414203" + }, + { + "correct_budget": 24, + "excess": 21, + "s": 3, + "substituted_budget": 15, + "t": 9, + "word": "012314021413" + } + ] + }, + "14": { + "count": 26, + "examples": [ + { + "correct_budget": 24, + "excess": 21, + "s": 9, + "substituted_budget": 15, + "t": 3, + "word": "012013040324" + }, + { + "correct_budget": 24, + "excess": 21, + "s": 9, + "substituted_budget": 15, + "t": 3, + "word": "012013042304" + } + ] + }, + "16": { + "count": 361, + "examples": [ + { + "correct_budget": 31, + "excess": 30, + "s": 10, + "substituted_budget": 15, + "t": 2, + "word": "010201032434" + }, + { + "correct_budget": 24, + "excess": 21, + "s": 9, + "substituted_budget": 15, + "t": 3, + "word": "010201034234" + } + ] + }, + "17": { + "count": 140, + "examples": [ + { + "correct_budget": 19, + "excess": 16, + "s": 8, + "substituted_budget": 15, + "t": 4, + "word": "010232401043" + }, + { + "correct_budget": 19, + "excess": 16, + "s": 8, + "substituted_budget": 15, + "t": 4, + "word": "010234010423" + } + ] + }, + "18": { + "count": 100, + "examples": [ + { + "correct_budget": 24, + "excess": 21, + "s": 3, + "substituted_budget": 15, + "t": 9, + "word": "010203024134" + }, + { + "correct_budget": 19, + "excess": 16, + "s": 4, + "substituted_budget": 15, + "t": 8, + "word": "010203104234" + } + ] + }, + "19": { + "count": 50, + "examples": [ + { + "correct_budget": 19, + "excess": 16, + "s": 4, + "substituted_budget": 15, + "t": 8, + "word": "010230104234" + }, + { + "correct_budget": 19, + "excess": 16, + "s": 4, + "substituted_budget": 15, + "t": 8, + "word": "010230104324" + } + ] + }, + "20": { + "count": 64, + "examples": [ + { + "correct_budget": 19, + "excess": 16, + "s": 8, + "substituted_budget": 15, + "t": 4, + "word": "010232142324" + }, + { + "correct_budget": 24, + "excess": 21, + "s": 9, + "substituted_budget": 15, + "t": 3, + "word": "010234010243" + } + ] + }, + "21": { + "count": 4, + "examples": [ + { + "correct_budget": 24, + "excess": 21, + "s": 3, + "substituted_budget": 15, + "t": 9, + "word": "012013142314" + }, + { + "correct_budget": 24, + "excess": 21, + "s": 3, + "substituted_budget": 15, + "t": 9, + "word": "012013241314" + } + ] + }, + "22": { + "count": 32, + "examples": [ + { + "correct_budget": 24, + "excess": 21, + "s": 9, + "substituted_budget": 15, + "t": 3, + "word": "012030140243" + }, + { + "correct_budget": 24, + "excess": 21, + "s": 9, + "substituted_budget": 15, + "t": 3, + "word": "012030142403" + } + ] + }, + "24": { + "count": 241, + "examples": [ + { + "correct_budget": 24, + "excess": 21, + "s": 9, + "substituted_budget": 15, + "t": 3, + "word": "010201032434" + }, + { + "correct_budget": 31, + "excess": 30, + "s": 10, + "substituted_budget": 15, + "t": 2, + "word": "010201034234" + } + ] + }, + "25": { + "count": 44, + "examples": [ + { + "correct_budget": 19, + "excess": 16, + "s": 4, + "substituted_budget": 15, + "t": 8, + "word": "012030412403" + }, + { + "correct_budget": 19, + "excess": 16, + "s": 4, + "substituted_budget": 15, + "t": 8, + "word": "012030421403" + } + ] + }, + "28": { + "count": 70, + "examples": [ + { + "correct_budget": 24, + "excess": 21, + "s": 9, + "substituted_budget": 15, + "t": 3, + "word": "010230102434" + }, + { + "correct_budget": 24, + "excess": 21, + "s": 9, + "substituted_budget": 15, + "t": 3, + "word": "010230103424" + } + ] + } + }, + "simple_closed_words": 3695, + "sound_masks": [ + 15, + 23, + 26, + 27, + 29, + 30, + 31 + ], + "universal_words": 828 + }, + { + "L": 12, + "base_budget": -1, + "false_prunes": 0, + "firing_masks": [], + "firing_weight_max": 0, + "n": 6, + "records": {}, + "simple_closed_words": 6525, + "sound_masks": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 20, + 21, + 22, + 23, + 24, + 25, + 26, + 27, + 28, + 29, + 30, + 31, + 32, + 33, + 34, + 35, + 36, + 37, + 38, + 39, + 40, + 41, + 42, + 43, + 44, + 45, + 46, + 47, + 48, + 49, + 50, + 51, + 52, + 53, + 54, + 55, + 56, + 57, + 58, + 59, + 60, + 61, + 62, + 63 + ], + "universal_words": 0 + }, + { + "L": 14, + "base_budget": 11, + "false_prunes": 0, + "firing_masks": [], + "firing_weight_max": 0, + "n": 6, + "records": {}, + "simple_closed_words": 123704, + "sound_masks": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 20, + 21, + 22, + 23, + 24, + 25, + 26, + 27, + 28, + 29, + 30, + 31, + 32, + 33, + 34, + 35, + 36, + 37, + 38, + 39, + 40, + 41, + 42, + 43, + 44, + 45, + 46, + 47, + 48, + 49, + 50, + 51, + 52, + 53, + 54, + 55, + 56, + 57, + 58, + 59, + 60, + 61, + 62, + 63 + ], + "universal_words": 0 + }, + { + "L": 14, + "base_budget": -21, + "false_prunes": 0, + "firing_masks": [], + "firing_weight_max": 0, + "n": 7, + "records": {}, + "simple_closed_words": 161936, + "sound_masks": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 20, + 21, + 22, + 23, + 24, + 25, + 26, + 27, + 28, + 29, + 30, + 31, + 32, + 33, + 34, + 35, + 36, + 37, + 38, + 39, + 40, + 41, + 42, + 43, + 44, + 45, + 46, + 47, + 48, + 49, + 50, + 51, + 52, + 53, + 54, + 55, + 56, + 57, + 58, + 59, + 60, + 61, + 62, + 63, + 64, + 65, + 66, + 67, + 68, + 69, + 70, + 71, + 72, + 73, + 74, + 75, + 76, + 77, + 78, + 79, + 80, + 81, + 82, + 83, + 84, + 85, + 86, + 87, + 88, + 89, + 90, + 91, + 92, + 93, + 94, + 95, + 96, + 97, + 98, + 99, + 100, + 101, + 102, + 103, + 104, + 105, + 106, + 107, + 108, + 109, + 110, + 111, + 112, + 113, + 114, + 115, + 116, + 117, + 118, + 119, + 120, + 121, + 122, + 123, + 124, + 125, + 126, + 127 + ], + "universal_words": 0 + } + ], + "fixture": { + "bit0_excess": 8, + "bit0_split": [ + 6, + 2 + ], + "bit3_excess": 8, + "bit3_split": [ + 6, + 2 + ], + "correct_bit0_budget": 9, + "distinct_nonclosing": 8, + "prefix_states": [ + 0, + 1, + 3, + 2, + 6, + 4, + 12, + 8, + 0 + ], + "restored": true, + "substituted_budget": 5, + "universal": true, + "weight_excess": 0, + "weight_split": [ + 4, + 4 + ], + "word": "01021323" + }, + "model": "PR943 singleton prefix walk", + "schema": 1 +} diff --git a/research/f7-bit0-functional-classification/SOURCES.json b/research/f7-bit0-functional-classification/SOURCES.json new file mode 100644 index 0000000000..6e1eb7cd7d --- /dev/null +++ b/research/f7-bit0-functional-classification/SOURCES.json @@ -0,0 +1,43 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5" + }, + { + "path": "docs/research/research-family-status.md", + "usage": "provenance", + "sha256": "9b98ab42364e90588e90410fd2773f9bc4bf5050f514101bed0a0246881b5b7e", + "git_blob": "9b7d65650d8fcd6247a758936b24426b40e40efa" + }, + { + "path": "research/f7-weight-parity-census-correction/MATH.md", + "usage": "provenance", + "sha256": "13f1234de6b7bd9f5afbe9a8892fc1d7f47eae0eddf098d19331a561c750e06a", + "git_blob": "e0207d8ebd903dc584862a2d6d500b59f3134490" + }, + { + "path": "research/f7-weight-parity-census-correction/README.md", + "usage": "provenance", + "sha256": "9bc7867ccfa97a682e4683052647d4bf8f191da5a219271f87d3e0a10de1446a", + "git_blob": "0221748ce35d4a2dc6ee5ce61be210eb34a2ea83" + }, + { + "path": "research/f7-bit0-false-prune/README.md", + "usage": "provenance", + "sha256": "d2507c556e23b36601d64c24ac394ab7192bd897d25f94e18471c86f83617efb", + "git_blob": "83b23ff085f24451350dd9fe54b8efad68dc80dd" + }, + { + "path": "research/f7-set-word-pruning-boundary/README.md", + "usage": "provenance", + "sha256": "dd51ed24c9176e0930f7e83de7955b9796e31f23c4a9828ae3d82c7491b7dbc3", + "git_blob": "2cab2ebb47ca1311e53a2c11afdc616ac262963b" + } + ], + "note": "All rows are provenance only. verify.py imports no predecessor code and reads no repository file; it is a self-contained standard-library recomputation. Pins bind the documents this package was derived from and checked against." +} diff --git a/research/f7-bit0-functional-classification/TASK.json b/research/f7-bit0-functional-classification/TASK.json new file mode 100644 index 0000000000..78fa8d9f97 --- /dev/null +++ b/research/f7-bit0-functional-classification/TASK.json @@ -0,0 +1,97 @@ +{ + "schema_version": 1, + "task_id": "census-pruning-audit", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "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": "Is the fixed L/2 budget substitution a coordinate-bit-0 artifact, or is it unsound for every linear functional other than the parity one? Exhaustive classification of all nonzero functionals on nine small singleton prefix-walk domains with n<=7 and L<=14, plus a machine-checked alternation lemma.", + "scope_change_reason": "The card's own first experiment (reconstruct 01021323, compare bit-0 against weight parity on one small domain) is already delivered by #2973 and #3096, which agree with this package's recomputation. The question those leave open is whether bit 0 is special, so the card is narrowed to one complete functional classification on a stated domain. The seven-label decision regime is deliberately not entered, per the card's own scope-change trigger.", + "bottleneck_link": "A word-census exclusion is usable only if its prune matches the partition that justifies the budget. Naming every functional for which the substitution is unsound, and showing which single functional justifies it, localises the defect without replaying the seven-label census.", + "budget_minutes": 60, + "stop_rule": "Stop once the fixture is independently reconstructed, all 2^n-1 functionals are classified on the small domains, and the alternation lemma is machine-checked. Do not run a (7,18) or (7,20) census, do not search for a new kappa, and do not change any selected result.", + "outcome": "partial", + "evidence": "Fixture recomputed from scratch: prefix states 0,1,3,2,6,4,12,8,0; eight distinct nonclosing states; every label twice; S+S = F2^4; weight split (4,4) with excess 0; bit-0 split (6,2) with excess 8; substituted budget 5; correct budget 9. Census over nine domains: at (4,8), (4,10) and (5,12) the substitution falsely prunes universal words for 9, 10 and 24 of the nonzero functionals respectively, with firing weights exactly 1-2, 1-2 and 1-3; at (3,6), (3,8), (5,10), (6,12), (6,14) and (7,14) there are no false prunes, and the last four of those contain no universal word at all. The count of 22 universal simple words and 6 bit-0 false prunes at (4,8) matches the independent #3096 audit. Lemma l(q_{i+1}) XOR l(q_i) = v_{w_i} holds on 3480 checked instances, giving the all-ones functional as the unique functional whose class value alternates with time.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "overlap": { + "checked_at": "2026-10-18", + "coverage": "python3 -B scripts/find_overlap.py --task census-pruning-audit reported 402 open PR bodies and 2471 discussions with complete pagination, fetched 2026-10-18T17:02Z. The tool states this is not a novelty certificate.", + "predecessors_checked": [ + "PR2973 / research/f7-weight-parity-census-correction", + "PR3096 / research/f7-bit0-false-prune", + "research/f7-set-word-pruning-boundary", + "research/f7-independent-full-replay", + "research/scatter-export-parity-audit (inspected and rejected as a different boundary)", + "open PR3678 research/scatter-basis-identity (inspected, different question)" + ], + "sibling_batch_prs_avoided": [ + "3593 encoded twiddle shape control", + "3591 rooted-minor closure of marked support-transfer obstructions", + "3596 residual floor attainment for different block bases", + "3589 uniform 11t/5 mixed-negative Q8 lower bound", + "3590 amortizing synthetic twiddle headers across physical address streams" + ] + }, + "open_questions": [ + { + "question": "At seven labels and L = 18 or L = 20, does the fixed L/2 substitution falsely prune a universal word, and which functionals?", + "why_it_matters": "PR2542's decisive call cyclic_census(7, 18, budget=9, simple=True) and the PR2634/PR2691 length-20 shards use the unsound substitution. This is the only domain that changes a maintained decision about which old exclusions need replacement evidence.", + "first_step": "Reuse survey(7, 18) and survey(7, 20) from verify.py with the functional loop already in place; the only cost is the state count at seven labels.", + "blocked_by": "A seven-label census needs its own resource budget and a named research decision, which the card's scope-change trigger puts outside this session." + }, + { + "question": "Why do functionals of Hamming weight >= n-1 never fire in the measured domains, while weight <= n-2 do?", + "why_it_matters": "If the threshold is a theorem, the defect has a clean characterisation; if it is a coincidence of these domains, the weight pattern must not be generalised and the two exceptions become informative.", + "first_step": "Prove a bound relating the class imbalance d of a weight-(n-1) functional to the attainable excess a+b, or find a counterexample at (5, 14).", + "blocked_by": "No proof attempted; the classification at (5,14) and above was out of budget." + }, + { + "question": "Can the bit-0 grouping be repaired by substituting the actual class sizes into the budget, instead of rewriting the traversal to weight parity?", + "why_it_matters": "The budget algebra is valid for any functional with its own class sizes, so a one-substitution repair would let the retained PR2542/PR2634/PR2691 traversal code run again with sound pruning and a directly comparable receipt.", + "first_step": "Replace the substituted s,t with the enumerated class cardinalities in the pinned engine and replay (4,8) to confirm no universal word is lost.", + "blocked_by": "That is a change to frozen predecessor sources and needs maintainer authorization." + } + ] +} diff --git a/research/f7-bit0-functional-classification/VERIFY.json b/research/f7-bit0-functional-classification/VERIFY.json new file mode 100644 index 0000000000..539d369206 --- /dev/null +++ b/research/f7-bit0-functional-classification/VERIFY.json @@ -0,0 +1,33 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Nine exhaustive (n,L) domains, all 2^n-1 nonzero linear functionals per domain, the 01021323 fixture reconstruction, the machine-checked alternation lemma, the separately written brute-force cross-check at three domains, and byte equality of the fresh receipt with the committed RESULT.json." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 300, + "checks": "Eighteen behavioural groups: restoration, universality, closing-state deduplication, the published fixture numbers, budget arithmetic, the alternation lemma and its failure case for a non-parity functional, functional-count closure, the bit-0 counterexample count, cross-enumerator agreement, canonical-form filter, domain-bound rejection and receipt self-consistency." + } + ] +} \ No newline at end of file diff --git a/research/f7-bit0-functional-classification/test_verify.py b/research/f7-bit0-functional-classification/test_verify.py new file mode 100644 index 0000000000..5062ed6298 --- /dev/null +++ b/research/f7-bit0-functional-classification/test_verify.py @@ -0,0 +1,126 @@ +"""Behavioural tests for the fixed-L/2 functional classification. + +Nick Petalas, with substantial automated assistance. Apache-2.0. +""" + +import json +import sys +import unittest +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).resolve().parent)) + +import verify as V # noqa: E402 + + +class ModelTest(unittest.TestCase): + def test_01021323_is_restored_and_universal(self): + word = (0, 1, 0, 2, 1, 3, 2, 3) + states = V.prefix_states(word) + self.assertTrue(V.restored(word)) + self.assertEqual(len(set(states[:-1])), 8) + self.assertEqual(len(states), 9) + self.assertTrue(V.is_universal(states, 4)) + + def test_prefix_states_close_to_zero(self): + for word in [(0, 1, 0, 1), (0, 0), (0, 1, 2, 0, 1, 2)]: + self.assertEqual(V.prefix_states(word)[-1], 0) + + def test_non_restored_word_is_rejected(self): + self.assertFalse(V.restored((0, 1, 2))) + self.assertFalse(V.restored((0, 1))) + + def test_all_labels_even_but_a_label_used_once_fails(self): + self.assertTrue(V.restored((0, 0, 1, 1))) + self.assertFalse(V.restored((0, 0, 1, 2))) + + def test_split_stats_ignores_the_closing_repeat(self): + word = (0, 1, 0, 2, 1, 3, 2, 3) + raw = V.prefix_states(word) + self.assertEqual(V.split_stats(raw, 0b0001), V.split_stats(raw[:-1], 0b0001)) + self.assertEqual(V.split_stats(raw[:-1], 0b0001), (6, 2, 8)) + + def test_fixture_matches_the_published_numbers(self): + f = V.fixture_01021323() + self.assertEqual(f["weight_split"], [4, 4]) + self.assertEqual(f["weight_excess"], 0) + self.assertEqual(f["bit0_split"], [6, 2]) + self.assertEqual(f["bit0_excess"], 8) + self.assertEqual(f["substituted_budget"], 5) + self.assertEqual(f["correct_bit0_budget"], 9) + + def test_budget_terms(self): + self.assertEqual(V.budget_terms(4, 8), 5) + self.assertEqual(V.budget_terms(7, 18), 9) + self.assertEqual(V.budget_terms(7, 20), 27) + self.assertEqual(V.budget_terms(7, 14), -21) + + +class AlternationTest(unittest.TestCase): + def test_lemma_holds_on_every_word_at_4_8(self): + self.assertGreater(V.alternation_holds(4, 8), 0) + + def test_all_ones_functional_alternates_every_step(self): + word = (0, 1, 0, 2, 1, 3, 2, 3) + states = V.prefix_states(word) + vals = [V.parity(p & 0b1111) for p in states] + self.assertEqual(vals, [i % 2 for i in range(len(states))]) + + def test_non_all_ones_functional_need_not_alternate(self): + word = (0, 1, 0, 2, 1, 3, 2, 3) + states = V.prefix_states(word) + vals = [V.parity(p & 0b0001) for p in states] + self.assertNotEqual(vals, [i % 2 for i in range(len(states))]) + + +class CensusTest(unittest.TestCase): + def test_small_domain_is_non_trivial(self): + r = V.survey(3, 6) + self.assertEqual(r["simple_closed_words"], 4) + self.assertEqual(r["universal_words"], 4) + self.assertEqual(r["false_prunes"], 0) + + def test_all_15_functionals_are_tested_at_n4(self): + r = V.survey(4, 8) + self.assertEqual(len(r["firing_masks"]) + len(r["sound_masks"]), 15) + + def test_bit0_counterexample_is_present(self): + r = V.survey(4, 8) + self.assertIn(1, r["firing_masks"]) + self.assertEqual(r["records"][1]["count"], 6) + + def test_cross_check_enumerator_agrees(self): + for n, L in V.CROSS_CHECK: + fast = V.survey(n, L) + words, universal = V.brute_survey(n, L) + self.assertEqual(words, fast["simple_closed_words"], f"{n},{L}") + self.assertEqual(universal, fast["universal_words"], f"{n},{L}") + + def test_canonical_filter(self): + self.assertTrue(V.canonical((0, 1, 0, 2))) + self.assertFalse(V.canonical((1, 0, 0))) + self.assertFalse(V.canonical((0, 2, 0))) + + def test_bounds_are_enforced(self): + for bad in [(0, 8), (9, 8), (4, 1), (4, 17)]: + with self.assertRaises(ValueError): + list(V.enumerate_words(*bad)) + + +class ReceiptTest(unittest.TestCase): + def test_receipt_is_reproducible(self): + r = V.run() + self.assertGreater(r["alternation_checks"], 0) + for d in r["domains"]: + self.assertEqual( + d["false_prunes"], sum(v["count"] for v in d["records"].values()) + ) + + def test_stored_receipt_is_valid_json(self): + stored = json.loads((V.PACKAGE / "RESULT.json").read_bytes()) + self.assertEqual(stored["schema"], 1) + self.assertTrue(stored["domains"]) + + +if __name__ == "__main__": + unittest.main() \ No newline at end of file diff --git a/research/f7-bit0-functional-classification/verify.py b/research/f7-bit0-functional-classification/verify.py new file mode 100644 index 0000000000..f554ec10c8 --- /dev/null +++ b/research/f7-bit0-functional-classification/verify.py @@ -0,0 +1,313 @@ +"""Independent functional classification of the fixed L/2 bit-0 word budget. + +Model (PR943 singleton prefix walk): q_0 = 0, q_{i+1} = q_i XOR (1 << w_i). + restoration : every label occurs a positive even number of times + universal : the set S of distinct prefix states satisfies S + S = F2^n + simple : q_0 .. q_{L-1} are distinct (the closing q_L = q_0 adds no point) + +For a nonzero linear functional with indicator mask `m`, write + E = {p in S : parity(p & m) == 0}, O = S - E, s = |E|, t = |O|, + a = C(s,2) - |{x XOR y : x != y, x,y in E}|, b = analogously for O. +Universality forces a + b <= C(s,2) + C(t,2) - (Q - 1) with Q = 2^(n-1). +The old engine groups by coordinate bit 0 but substitutes the time-parity sizes +L/2, L/2. Write base = C(L/2,2)*2 - (Q-1) and d = |s - t| / 2; then the +correct budget is exactly base + d*d. The substitution is *false* for one word +when base < a + b <= base + d*d. + +Nick Petalas, with substantial automated assistance. Apache-2.0. +Independent implementation: no predecessor package code is imported. +""" + +import argparse +import json +import sys +from itertools import combinations, product +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent + +DOMAINS = [ + (3, 6), + (3, 8), + (4, 8), + (4, 10), + (5, 10), + (5, 12), + (6, 12), + (6, 14), + (7, 14), +] +CROSS_CHECK = [(3, 6), (3, 8), (4, 8)] +MAX_N = 8 +MAX_L = 16 +MAX_EXAMPLES = 2 +# Bound for the unpruned cross-check enumerator only; the primary enumerator +# prunes on prefix-state distinctness and is bounded by MAX_N and MAX_L. +MAX_BRUTE_WORDS = 6_553_600 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def parity(v): + return bin(v).count("1") & 1 + + +def binom2(k): + return k * (k - 1) // 2 + + +def prefix_states(word): + q = 0 + states = [0] + for lab in word: + q ^= 1 << lab + states.append(q) + return states + + +def restored(word): + counts = {} + for lab in word: + counts[lab] = counts.get(lab, 0) + 1 + return all(c % 2 == 0 for c in counts.values()) + + +def is_universal(states, n): + S = set(states) + return {x ^ y for x in S for y in S} == set(range(1 << n)) + + +def split_stats(states, mask): + """Class sizes and collision excess for the functional with indicator mask. + + Inputs are deduplicated first: the closing state q_L equals q_0 and must not + be counted as a second point of the prefix set. + """ + states = sorted(set(states)) + E = [p for p in states if parity(p & mask) == 0] + O = [p for p in states if parity(p & mask) == 1] + supp_e = {x ^ y for x, y in combinations(E, 2)} + supp_o = {x ^ y for x, y in combinations(O, 2)} + a = binom2(len(E)) - len(supp_e) + b = binom2(len(O)) - len(supp_o) + return len(E), len(O), a + b + + +def budget_terms(n, L): + """(base, d) for the fixed L/2 substitution at (n, L).""" + require(L % 2 == 0, "even length") + half = L // 2 + base = 2 * binom2(half) - ((1 << (n - 1)) - 1) + return base + + +def is_false_prune(n, L, states, mask): + s, t, exc = split_stats(states, mask) + base = budget_terms(n, L) + d = (s - t) // 2 + return base < exc <= base + d * d, (s, t, exc, base, base + d * d) + + +def enumerate_words(n, L): + """Restricted-growth words of length L over [0, n) with distinct prefix states. + + The closing step is forced to land back on q_0, so every emitted word is + self-avoiding up to q_{L-1}. Leaf words are additionally checked for + restoration and universality by the caller. + """ + require(1 <= n <= MAX_N and 2 <= L <= MAX_L, "bounded domain") + seen = {0} + word = [] + + def walk(i, q, maxlab): + """Place label w_i; `q` is the prefix state q_i before the placement.""" + if i == L: + yield tuple(word), tuple(sorted(seen)) + return + for lab in range(min(maxlab + 2, n)): + nq = q ^ (1 << lab) + if i == L - 1: + if nq == 0: + word.append(lab) + yield from walk(i + 1, 0, max(maxlab, lab)) + word.pop() + continue + if nq in seen: + continue + seen.add(nq) + word.append(lab) + yield from walk(i + 1, nq, max(maxlab, lab)) + word.pop() + seen.discard(nq) + + yield from walk(0, 0, -1) + + +def survey(n, L): + """Exhaustive record for one (n, L) domain.""" + require(1 <= n <= MAX_N and 2 <= L <= MAX_L, "bounded domain") + masks = list(range(1, 1 << n)) + words = 0 + universal = 0 + firing = {} + for word, states in enumerate_words(n, L): + words += 1 + if not restored(word): + continue + if not is_universal(states, n): + continue + universal += 1 + for mask in masks: + hit, detail = is_false_prune(n, L, states, mask) + if not hit: + continue + entry = firing.setdefault(mask, {"count": 0, "examples": []}) + entry["count"] += 1 + if len(entry["examples"]) < MAX_EXAMPLES: + entry["examples"].append( + { + "word": "".join(map(str, word)), + "s": detail[0], + "t": detail[1], + "excess": detail[2], + "substituted_budget": detail[3], + "correct_budget": detail[4], + } + ) + return { + "n": n, + "L": L, + "simple_closed_words": words, + "universal_words": universal, + "base_budget": budget_terms(n, L), + "firing_masks": sorted(firing), + "sound_masks": [m for m in masks if m not in firing], + "firing_weight_max": max((bin(m).count("1") for m in firing), default=0), + "false_prunes": sum(v["count"] for v in firing.values()), + "records": firing, + } + + +def canonical(word): + """Restricted-growth form: first label 0, each later label at most max+1.""" + if word[0] != 0: + return False + high = 0 + for lab in word[1:]: + if lab > high + 1: + return False + high = max(high, lab) + return True + + +def brute_survey(n, L): + """Separately written enumerator: every label sequence, filtered, no pruning.""" + require(1 <= n <= MAX_N and 2 <= L <= MAX_L, "bounded domain") + require(n ** L <= MAX_BRUTE_WORDS, "bounded brute-force search space") + words = 0 + universal = 0 + for word in product(range(n), repeat=L): + if not canonical(word) or not restored(word): + continue + states = prefix_states(word) + if len(set(states[:-1])) != L or states[-1] != states[0]: + continue + words += 1 + if is_universal(states, n): + universal += 1 + return words, universal + + +def alternation_holds(n, L): + """Machine check of the lemma: l(q_{i+1}) XOR l(q_i) == v_{w_i}.""" + require(1 <= n <= MAX_N and 2 <= L <= MAX_L, "bounded domain") + checked = 0 + for word, _states in enumerate_words(n, L): + for mask in range(1, 1 << n): + states = prefix_states(word) + for i in range(1, L + 1): + step = parity(states[i] & mask) ^ parity(states[i - 1] & mask) + require( + step == ((mask >> word[i - 1]) & 1), + f"alternation identity: word={word} mask={mask} i={i}", + ) + checked += 1 + return checked + + +def fixture_01021323(): + """Exact independent reconstruction of the retained n=4 counterexample.""" + word = (0, 1, 0, 2, 1, 3, 2, 3) + states = prefix_states(word) + record = { + "word": "".join(map(str, word)), + "prefix_states": states, + "distinct_nonclosing": len(set(states[:-1])), + "restored": restored(word), + "universal": is_universal(states, 4), + } + weight = split_stats(states, 0b1111) + bit0 = split_stats(states, 0b0001) + bit0_high = split_stats(states, 0b1000) + base = budget_terms(4, 8) + record["weight_split"] = [weight[0], weight[1]] + record["weight_excess"] = weight[2] + record["bit0_split"] = [bit0[0], bit0[1]] + record["bit0_excess"] = bit0[2] + record["bit3_split"] = [bit0_high[0], bit0_high[1]] + record["bit3_excess"] = bit0_high[2] + record["substituted_budget"] = base + record["correct_bit0_budget"] = base + ((bit0[0] - bit0[1]) // 2) ** 2 + return record + + +def run(refresh=False): + receipt = { + "schema": 1, + "model": "PR943 singleton prefix walk", + "domains": [], + "cross_check": [], + "fixture": fixture_01021323(), + "alternation_checks": 0, + } + for n, L in DOMAINS: + receipt["domains"].append(survey(n, L)) + print(f"n={n} L={L} done", file=sys.stderr) + for n, L in CROSS_CHECK: + words, universal = brute_survey(n, L) + fast = survey(n, L) + require( + (words, universal) == (fast["simple_closed_words"], fast["universal_words"]), + f"cross-check mismatch at ({n},{L})", + ) + receipt["cross_check"].append({"n": n, "L": L, "words": words, "universal": universal}) + receipt["alternation_checks"] = alternation_holds(4, 8) + path = PACKAGE / "RESULT.json" + if refresh or not path.exists(): + path.write_text(json.dumps(receipt, indent=1, sort_keys=True) + "\n") + print(f"wrote {path}", file=sys.stderr) + stored = json.loads(path.read_bytes()) + canonical = json.loads(json.dumps(receipt, sort_keys=True)) + require(canonical == stored, "receipt mismatch: stored RESULT.json differs from a fresh run") + return canonical + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument("--emit", action="store_true", help="rewrite RESULT.json") + args = ap.parse_args() + receipt = run(refresh=args.emit) + hits = [ + (d["n"], d["L"], d["false_prunes"]) + for d in receipt["domains"] + if d["false_prunes"] + ] + print("domains_with_false_prunes", hits) + print("PASS_F7_BIT0_FUNCTIONAL_CLASSIFICATION") + + +if __name__ == "__main__": + main() \ No newline at end of file