From f58ad3b24cfcac6015750a8f26b41d0095953c19 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Sun, 18 Oct 2026 20:06:57 +0100 Subject: [PATCH 1/2] research: independently check the f7 functional classification and add (5,14) Re-derive the nine-domain functional classification of PR #3699 with a separate enumerator and classifier: all word counts, substituted budgets, 43 per-functional false-prune counts and the bit-0 column reproduce exactly, as does the 01021323 fixture. Add three domains the published table does not contain. At (5,14), the domain the checked package names as its own open next question, the fixed L/2 substitution falsely prunes for exactly the 25 functionals of Hamming weight 1, 2 and 3, and for none of weight 4 or 5, with no exception of the (5,12) kind. At (4,12) the unsound class is larger than at (4,10): three of the four weight-3 functionals fire, leaving only 0111 and 1111 sound. Finite certificate only: no weight-threshold theorem, no f(7) value, no pruning repair and no kappa. --- .../f7-functional-independent-check/README.md | 152 ++++ .../RESULT.json | 818 ++++++++++++++++++ .../SOURCES.json | 57 ++ .../f7-functional-independent-check/TASK.json | 87 ++ .../VERIFY.json | 33 + .../test_verify.py | 176 ++++ .../f7-functional-independent-check/verify.py | 465 ++++++++++ 7 files changed, 1788 insertions(+) create mode 100644 research/f7-functional-independent-check/README.md create mode 100644 research/f7-functional-independent-check/RESULT.json create mode 100644 research/f7-functional-independent-check/SOURCES.json create mode 100644 research/f7-functional-independent-check/TASK.json create mode 100644 research/f7-functional-independent-check/VERIFY.json create mode 100644 research/f7-functional-independent-check/test_verify.py create mode 100644 research/f7-functional-independent-check/verify.py diff --git a/research/f7-functional-independent-check/README.md b/research/f7-functional-independent-check/README.md new file mode 100644 index 0000000000..cda2498004 --- /dev/null +++ b/research/f7-functional-independent-check/README.md @@ -0,0 +1,152 @@ +# Independent check of the `f7` functional classification, and the `(5, 14)` domain + +**Independent verification (no κ) of a finite certificate, plus new coverage the +checked package itself names as its next question. No new `f(7)` bound, no +supplier, no selected-frontier change.** + +## Subject of the check + +[`research/f7-bit0-functional-classification`](../f7-bit0-functional-classification/README.md) +(branch `research/w5-b21-todo-20261018`, head `13db47d8d31603c1391572009e1eb7a22675a219`, +PR #3699) reports, on the PR943 singleton prefix walk, that the retained engines' +fixed `L/2` budget substitution is not a coordinate-bit-0 artefact: it falsely +prunes universal words for every functional of low Hamming weight and for none of +high weight, on nine `(n, L)` domains. + +This package recomputes that certificate from scratch and extends it to three +domains the published table does not contain, including `(5, 14)`, which the +published package lists as its open next question 2. + +## What is reproduced, and how + +`verify.py` is a separate implementation. It imports, executes and copies no +predecessor code. The published numbers are embedded as asserted constants; the +prefix walk, the simplicity/restoration/universality predicates, both collision +excess routes, the enumeration and the classification are written here. + +Every number in the published table is reproduced **exactly**, on the first run, +by a different enumerator: + +| `n` | `L` | simple closed | universal | substituted budget | false prunes | firing weights | +|---:|---:|---:|---:|---:|---:|---| +| 3 | 6 | 4 | 4 | 3 | 0 | — | +| 3 | 8 | 2 | 2 | 9 | 0 | — | +| 4 | 8 | 29 | 22 | 5 | 44 | 1, 2 | +| 4 | 10 | 110 | 110 | 13 | 190 | 1, 2 | +| 5 | 10 | 358 | 0 | 5 | 0 | — | +| 5 | 12 | 3695 | 828 | 15 | 2856 | 1, 2, 3 | +| 6 | 12 | 6525 | 0 | −1 | 0 | — | +| 6 | 14 | 123704 | 0 | 11 | 0 | — | +| 7 | 14 | 161936 | 0 | −21 | 0 | — | + +Beyond the column totals, the check also asserts equality of the **per-functional +false-prune counts** (24 masks at `(5, 12)`, 10 at `(4, 10)`, 9 at `(4, 8)`) and of +the published bit-0 column (`6`, `20`, `248` false prunes for the coordinate-bit-0 +functional). The reported `01021323` fixture is reconstructed from the word: the +nine prefix states `0,1,3,2,6,4,12,8,0`, the Hamming-weight split `(4,4)` with +excess `0`, the bit-0 split `(6,2)` with excess `8`, the substituted budget `5` +and the corrected budget `9`. + +## New coverage: three further domains + +The published table jumps from `(4, 10)` to `(5, 10)` and stops at `L = 14` for +`n = 6, 7`. This package classifies three further domains: + +| `n` | `L` | simple closed | universal | substituted budget | false prunes | firing functionals | sound functionals | +|---:|---:|---:|---:|---:|---:|---:|---:| +| 3 | 10 | 0 | 0 | 17 | 0 | 0 of 7 | 7 of 7 | +| **4** | **12** | **314** | **314** | **23** | **150** | **13 of 15** | **2 of 15** | +| **5** | **14** | **33922** | **24787** | **27** | **56686** | **25 of 31** | **6 of 31** | + +Two measured statements follow. + +1. **At `(5, 14)` the substitution falsely prunes for exactly the 25 functionals + of Hamming weight 1, 2 and 3, and for none of weight 4 or 5.** This is the + domain the published package names for exactly this test. Its own `(5, 12)` + reading carried one exception (mask `11010`, weight 3, did not fire); at + `(5, 14)` there is no exception at all, so the weight threshold `n - 1` with + "every weight `<= n - 2` fires" is clean there. That is evidence about the + heuristic, not a proof of it: nothing here bounds the threshold for general + `(n, L)`. +2. **The `(4, L)` firing set grows with `L` and is monotone on the measured + range.** `(4, 8)` fires for 9 of 15 functionals, `(4, 10)` for 10, `(4, 12)` + for 13: at `(4, 12)` three of the four weight-3 functionals fire (`1011`, + `1101`, `1110`), and only `0111` (weight 3) and `1111` (weight 4) stay sound. + Compared with `(4, 10)`, where every weight-3 and weight-4 functional is + sound, the unsound set is strictly larger at the longer length. So the old + question "is bit 0 special?" is answered with an even wider unsound class at + this length, and the fix cannot be a per-weight threshold that is independent + of `L`. + +`(3, 10)` has no simple closed word at all: `q_0..q_9` would be ten distinct +states of `F2^3`, which has eight. It is recorded as an empty domain rather than +dropped, so the enumeration's domain check is exercised on a degenerate case. + +## Controls, all run on every invocation + +- **Fixture.** The published word's prefix states, splits, excesses and both + budgets are recomputed and asserted, including the identity + `C(s,2) + C(t,2) - (2^(n-1) - 1) = base + d^2`. +- **Two excess routes.** The collision excess is computed both as a difference + multiplicity sum and as a direct support-size difference, and the two must + agree for every universal word and every nonzero functional of every domain. +- **Budget sensitivity.** Shifting the substituted budget by `-2, -1, +1, +2` + must leave every non-firing domain at zero and must move the count on each of + the three firing domains. The check therefore depends on the budget's exact + value, not only on class sizes. +- **Second enumeration route.** On six domains the census is also produced by an + unconstrained walk (no first-occurrence ordering) whose leaves are canonicalised + afterwards; the resulting word sets must be equal. This is the check that would + catch a pruning error in the primary enumerator. +- **Predicates on every enumerated word.** Every emitted word is asserted + restored and simple; universality is recomputed as `|S + S| = 2^n`. + +## What this does not establish + +- It is a **finite certificate on ten bounded `(n, L)` domains**, not a theorem + about the weight threshold, and not a census of the seven-label regime. The + `(7, 18)` and `(7, 20)` domains that would change a maintained decision are + not entered. +- It does not re-derive the *necessity* of the exact budget `base + d^2`; that + implication is inherited from the checked package and from PR2973's `MATH.md`. + What is checked here is the classification and the counts built on it. +- No `f(7)` value, no pruning repair, no source change, no κ and no supplier is + claimed. A false prune in this model does not by itself invalidate any reported + final bound. +- Independent human review and formal proof-kernel acceptance are unclaimed. + +## Reproduce + +```sh +~/git/integer-mult-bounds/.venv/bin/python3.12 -B research/f7-functional-independent-check/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -B research/f7-functional-independent-check/test_verify.py +``` + +`verify.py --write` regenerates `RESULT.json`, which is the exact finite receipt. +Standard library only, no Git objects, no network. Runtime is about 30 s on the +recording host; `(5, 14)` alone is a few seconds. + +## Credit + +The classification question, the model, the nine published domains and the nine +pinned numbers are Nick Petalas's, in +[`research/f7-bit0-functional-classification`](../f7-bit0-functional-classification/README.md) +— including its named open question about `(5, 14)`, which this package answers +for the universal-word domain. 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. This package's +re-implementation, the three added domains and the controls are by Nick Petalas, +produced with AI assistance. Apache-2.0. + +## Open next questions + +- **Is the firing set monotone in `L` for fixed `n`?** Measured on `(4, 8) < + (4, 10) < (4, 12)` and `(5, 12) < (5, 14)`, but not proved, and `(5, 10)` has no + universal word to compare against. +- **Can the weight `>= n - 1` soundness be proved rather than measured?** The + published alternation lemma explains why only the all-ones functional is + *justified* by the substitution; it does not explain why high-weight functionals + do not fire. +- **The `(6, 16)` domain.** `(6, 14)` has 123,704 simple closed words and no + universal word; the next even length is the first that could change that, and + it is outside this package's budget. diff --git a/research/f7-functional-independent-check/RESULT.json b/research/f7-functional-independent-check/RESULT.json new file mode 100644 index 0000000000..d4f2bd8cc0 --- /dev/null +++ b/research/f7-functional-independent-check/RESULT.json @@ -0,0 +1,818 @@ +{ + "controls": { + "budget_shift_prunes": { + "-1": { + "3,6": 0, + "3,8": 0, + "4,10": 190, + "4,8": 44, + "5,10": 0, + "5,12": 2856, + "6,12": 0, + "6,14": 0, + "7,14": 0 + }, + "-2": { + "3,6": 0, + "3,8": 0, + "4,10": 160, + "4,8": 0, + "5,10": 0, + "5,12": 2556, + "6,12": 0, + "6,14": 0, + "7,14": 0 + }, + "1": { + "3,6": 0, + "3,8": 0, + "4,10": 190, + "4,8": 44, + "5,10": 0, + "5,12": 2856, + "6,12": 0, + "6,14": 0, + "7,14": 0 + }, + "2": { + "3,6": 0, + "3,8": 0, + "4,10": 190, + "4,8": 44, + "5,10": 0, + "5,12": 2856, + "6,12": 0, + "6,14": 0, + "7,14": 0 + } + }, + "excess_route_pairs": 800797 + }, + "cross_check": [ + { + "L": 6, + "n": 3, + "words": 4 + }, + { + "L": 8, + "n": 3, + "words": 2 + }, + { + "L": 8, + "n": 4, + "words": 29 + }, + { + "L": 10, + "n": 4, + "words": 110 + }, + { + "L": 10, + "n": 5, + "words": 358 + }, + { + "L": 12, + "n": 5, + "words": 3695 + } + ], + "fixture": { + "bit0_excess": 8, + "correct_bit0_budget": 9, + "prefix_states": [ + 0, + 1, + 3, + 2, + 6, + 4, + 12, + 8, + 0 + ], + "substituted_budget": 5, + "word": "01021323" + }, + "new_domains": [ + { + "L": 10, + "base_budget": 17, + "bit0_false_prunes": 0, + "false_prunes": 0, + "firing_masks": [], + "firing_weights": [], + "masks_total": 7, + "n": 3, + "nodes": 20, + "per_mask_counts": {}, + "simple_closed_words": 0, + "sound_masks": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ], + "universal_words": 0 + }, + { + "L": 12, + "base_budget": 23, + "bit0_false_prunes": 16, + "false_prunes": 150, + "firing_masks": [ + 1, + 2, + 3, + 4, + 5, + 6, + 8, + 9, + 10, + 11, + 12, + 13, + 14 + ], + "firing_weights": [ + 1, + 2, + 3 + ], + "masks_total": 15, + "n": 4, + "nodes": 1885, + "per_mask_counts": { + "1": 16, + "10": 10, + "11": 4, + "12": 15, + "13": 4, + "14": 4, + "2": 16, + "3": 9, + "4": 18, + "5": 10, + "6": 11, + "8": 22, + "9": 11 + }, + "simple_closed_words": 314, + "sound_masks": [ + 7, + 15 + ], + "universal_words": 314 + }, + { + "L": 14, + "base_budget": 27, + "bit0_false_prunes": 4112, + "false_prunes": 56686, + "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, + 26, + 28 + ], + "firing_weights": [ + 1, + 2, + 3 + ], + "masks_total": 31, + "n": 5, + "nodes": 234432, + "per_mask_counts": { + "1": 4112, + "10": 1552, + "11": 492, + "12": 3684, + "13": 334, + "14": 487, + "16": 8093, + "17": 3013, + "18": 2085, + "19": 904, + "2": 4112, + "20": 1677, + "21": 309, + "22": 903, + "24": 5326, + "25": 917, + "26": 170, + "28": 1372, + "3": 2385, + "4": 4197, + "5": 1568, + "6": 2574, + "7": 356, + "8": 4434, + "9": 1630 + }, + "simple_closed_words": 33922, + "sound_masks": [ + 15, + 23, + 27, + 29, + 30, + 31 + ], + "universal_words": 24787 + } + ], + "published_domains": [ + { + "L": 6, + "base_budget": 3, + "bit0_false_prunes": 0, + "false_prunes": 0, + "firing_masks": [], + "firing_weights": [], + "masks_total": 7, + "n": 3, + "nodes": 17, + "per_mask_counts": {}, + "simple_closed_words": 4, + "sound_masks": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ], + "universal_words": 4 + }, + { + "L": 8, + "base_budget": 9, + "bit0_false_prunes": 0, + "false_prunes": 0, + "firing_masks": [], + "firing_weights": [], + "masks_total": 7, + "n": 3, + "nodes": 22, + "per_mask_counts": {}, + "simple_closed_words": 2, + "sound_masks": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ], + "universal_words": 2 + }, + { + "L": 8, + "base_budget": 5, + "bit0_false_prunes": 6, + "false_prunes": 44, + "firing_masks": [ + 1, + 2, + 3, + 4, + 5, + 6, + 8, + 9, + 12 + ], + "firing_weights": [ + 1, + 2 + ], + "masks_total": 15, + "n": 4, + "nodes": 139, + "per_mask_counts": { + "1": 6, + "12": 5, + "2": 6, + "3": 5, + "4": 4, + "5": 1, + "6": 5, + "8": 8, + "9": 4 + }, + "simple_closed_words": 29, + "sound_masks": [ + 7, + 10, + 11, + 13, + 14, + 15 + ], + "universal_words": 22 + }, + { + "L": 10, + "base_budget": 13, + "bit0_false_prunes": 20, + "false_prunes": 190, + "firing_masks": [ + 1, + 2, + 3, + 4, + 5, + 6, + 8, + 9, + 10, + 12 + ], + "firing_weights": [ + 1, + 2 + ], + "masks_total": 15, + "n": 4, + "nodes": 608, + "per_mask_counts": { + "1": 20, + "10": 10, + "12": 28, + "2": 20, + "3": 10, + "4": 23, + "5": 8, + "6": 16, + "8": 37, + "9": 18 + }, + "simple_closed_words": 110, + "sound_masks": [ + 7, + 11, + 13, + 14, + 15 + ], + "universal_words": 110 + }, + { + "L": 10, + "base_budget": 5, + "bit0_false_prunes": 0, + "false_prunes": 0, + "firing_masks": [], + "firing_weights": [], + "masks_total": 31, + "n": 5, + "nodes": 2407, + "per_mask_counts": {}, + "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, + "bit0_false_prunes": 248, + "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_weights": [ + 1, + 2, + 3 + ], + "masks_total": 31, + "n": 5, + "nodes": 25335, + "per_mask_counts": { + "1": 248, + "10": 105, + "11": 15, + "12": 175, + "13": 10, + "14": 26, + "16": 361, + "17": 140, + "18": 100, + "19": 50, + "2": 248, + "20": 64, + "21": 4, + "22": 32, + "24": 241, + "25": 44, + "28": 70, + "3": 96, + "4": 278, + "5": 143, + "6": 119, + "7": 25, + "8": 221, + "9": 41 + }, + "simple_closed_words": 3695, + "sound_masks": [ + 15, + 23, + 26, + 27, + 29, + 30, + 31 + ], + "universal_words": 828 + }, + { + "L": 12, + "base_budget": -1, + "bit0_false_prunes": 0, + "false_prunes": 0, + "firing_masks": [], + "firing_weights": [], + "masks_total": 63, + "n": 6, + "nodes": 66124, + "per_mask_counts": {}, + "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, + "bit0_false_prunes": 0, + "false_prunes": 0, + "firing_masks": [], + "firing_weights": [], + "masks_total": 63, + "n": 6, + "nodes": 1261064, + "per_mask_counts": {}, + "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, + "bit0_false_prunes": 0, + "false_prunes": 0, + "firing_masks": [], + "firing_weights": [], + "masks_total": 127, + "n": 7, + "nodes": 2485511, + "per_mask_counts": {}, + "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 + } + ], + "schema": 1 +} diff --git a/research/f7-functional-independent-check/SOURCES.json b/research/f7-functional-independent-check/SOURCES.json new file mode 100644 index 0000000000..da271bd3d9 --- /dev/null +++ b/research/f7-functional-independent-check/SOURCES.json @@ -0,0 +1,57 @@ +{ + "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": "docs/research/current-priorities.md", + "usage": "provenance", + "sha256": "c95e09baa997b48ba00a26ea29168e782b17392d28184ecb7a17eea5472dd77c", + "git_blob": "231a089623bf11a70a434f5a57b0bf0a2ad4c317" + }, + { + "path": "research/f7-weight-parity-census-correction/MATH.md", + "usage": "provenance", + "sha256": "13f1234de6b7bd9f5afbe9a8892fc1d7f47eae0eddf098d19331a561c750e06a", + "git_blob": "e0207d8ebd903dc584862a2d6d500b59f3134490" + }, + { + "path": "research/f7-bit0-false-prune/README.md", + "usage": "provenance", + "sha256": "d2507c556e23b36601d64c24ac394ab7192bd897d25f94e18471c86f83617efb", + "git_blob": "83b23ff085f24451350dd9fe54b8efad68dc80dd" + }, + { + "path": "research/f7-bit0-functional-classification/README.md", + "usage": "provenance", + "pin": "head:13db47d8d31603c1391572009e1eb7a22675a219:research/f7-bit0-functional-classification/README.md", + "sha256": "8176c8a889671f67ebcd6f1b9e9efddae55cfbbff4b486442a9b63977e9c4844", + "git_blob": "4618c68ffc94be30055537bca4e49696946437dc" + }, + { + "path": "research/f7-bit0-functional-classification/RESULT.json", + "usage": "provenance", + "pin": "head:13db47d8d31603c1391572009e1eb7a22675a219:research/f7-bit0-functional-classification/RESULT.json", + "sha256": "5938908a76c497bad4c301eed0f12822fc16b0fbbbff2c0bc5150d82f2052105", + "git_blob": "84017d1265858fe976bd317c95d287c92fc4cb7e" + }, + { + "path": "research/f7-bit0-functional-classification/verify.py", + "usage": "provenance", + "pin": "head:13db47d8d31603c1391572009e1eb7a22675a219:research/f7-bit0-functional-classification/verify.py", + "sha256": "a0c93985734fa6855c5561a1b4eb730ef0af6ddd25bfdac1ef8b61d840efbe83", + "git_blob": "f554ec10c8ac5e30e067b01adf9b68b2eb80906a" + } + ] +} diff --git a/research/f7-functional-independent-check/TASK.json b/research/f7-functional-independent-check/TASK.json new file mode 100644 index 0000000000..5b75f601e8 --- /dev/null +++ b/research/f7-functional-independent-check/TASK.json @@ -0,0 +1,87 @@ +{ + "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": "Independent re-derivation of the nine-domain functional classification published in PR #3699 (exact head 13db47d8d31603c1391572009e1eb7a22675a219), with a separately written enumerator and classifier, plus three domains that package does not contain -- including (5,14), which it names as its own open next question 2.", + "scope_change_reason": "The card's first experiment (reconstruct 01021323, compare bit-0 against weight parity on one small domain) is already delivered by #2973, #3096 and PR #3699, whose nine-domain table this package reproduces exactly. The smallest remaining gap that changes a stated claim is the (5,14) domain PR #3699 names for its weight-threshold heuristic, so the card is narrowed to an independent check of the published certificate and the addition of that domain rather than another seven-label census.", + "bottleneck_link": "The word-census exclusions are only usable if the substitution that prunes them matches the classes it uses. An independent re-derivation, and one more domain at the length where the checked package stops, tests whether that unsound class is a small-length artefact or persists as L grows.", + "budget_minutes": 60, + "stop_rule": "Stop once the nine published domains are reproduced exactly by the separate implementation and the added domains are classified. Do not run a (7,18) or (7,20) census, do not claim a weight-threshold theorem, and do not change any selected result.", + "outcome": "completed", + "evidence": "Every number of the published nine-domain table is reproduced exactly by an independent enumerator and classifier: simple closed word counts 4, 2, 29, 110, 358, 3695, 6525, 123704, 161936; universal word counts 4, 2, 22, 110, 0, 828, 0, 0, 0; substituted budgets 3, 9, 5, 13, 5, 15, -1, 11, -21; false prune totals 0, 0, 44, 190, 0, 2856, 0, 0, 0; all 43 per-functional false-prune counts over the three firing domains; and the published bit-0 column 6, 20, 248. The 01021323 fixture is reconstructed from the word. New domains: (3,10) has no simple closed word at all; (4,12) has 314 simple closed and 314 universal words, 150 false prunes across 13 of 15 functionals, leaving only masks 0111 and 1111 sound; (5,14) has 33922 simple closed and 24787 universal words, 56686 false prunes across exactly the 25 functionals of Hamming weight 1, 2 and 3, with no firing functional of weight 4 or 5 and no exception of the (5,12) kind.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "overlap": { + "checked_at": "2026-10-18", + "coverage": "Open PR bodies and discussions were read through the repository API before starting and again before committing; peer branch heads and the checked package's own two open questions were inspected directly. This is an overlap check, not a novelty certificate.", + "checked_paths": [ + "PR #3699 research/f7-bit0-functional-classification", + "PR #3718 research/ceiling-bracket-gap", + "PR #3708 research/f7-l22-split-domain" + ] + }, + "open_questions": [ + { + "question": "Is the set of functionals that the fixed L/2 substitution falsely prunes monotone in L for fixed n?", + "why_it_matters": "A monotone set would bound where the old engines could have pruned soundly as a function of length alone; a non-monotone set would make any per-length repair unsound.", + "first_step": "Classify (4,14) and (5,16) with research/f7-functional-independent-check/verify.py by adding them to NEW_DOMAINS and compare the firing sets with (4,12) and (5,14).", + "blocked_by": "The next even lengths at n=4 and n=5 are unmeasured here; the enumerator scales as the number of simple closed words and (5,16) is beyond this package's 600 s replay budget unbounded." + }, + { + "question": "Why is no functional of Hamming weight at least n-1 ever falsely pruned on the measured domains?", + "why_it_matters": "The checked package's alternation lemma justifies the substitution for the all-ones functional only; the measured high-weight soundness is the reason the substitution is not obviously fatal for the old censuses.", + "first_step": "Bound the collision excess of a universal word from above by a function of the functional weight, then compare with base + d^2 for weight n-1.", + "blocked_by": "No such bound is proved here; the statement is an observation over ten bounded (n,L) domains." + }, + { + "question": "Does (6,16) contain a universal word, and does the firing class change there?", + "why_it_matters": "(6,14) has 123704 simple closed words and no universal word, so n=6 has no measured functional classification at all.", + "first_step": "Run the same census at (6,16) with the package's enumerator and record the universal-word count before classifying functionals.", + "blocked_by": "The simple-closed count grows by roughly an order of magnitude per two steps of L; the domain needs its own runtime budget." + } + ] +} diff --git a/research/f7-functional-independent-check/VERIFY.json b/research/f7-functional-independent-check/VERIFY.json new file mode 100644 index 0000000000..5ce787107c --- /dev/null +++ b/research/f7-functional-independent-check/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": 420, + "checks": "Independent re-derivation of the published nine-domain functional classification: word counts, substituted budgets, false-prune totals, all 43 per-functional false-prune counts, the bit-0 column, the 01021323 fixture, the two excess routes, the budget-shift sensitivity control, the second enumeration route and byte equality of the fresh receipt with the committed RESULT.json. It also classifies the added domains (3,10), (4,12) and (5,14)." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 300, + "checks": "Behavioural groups over the package's own primitives: walk and restoration, simplicity and universality predicates, closing-state handling, budget arithmetic against the published values, false-prune detection on the published fixture word, canonical form and first-occurrence ordering, domain-bound rejection, per-mask count closure and receipt self-consistency." + } + ] +} diff --git a/research/f7-functional-independent-check/test_verify.py b/research/f7-functional-independent-check/test_verify.py new file mode 100644 index 0000000000..e4b59c96d8 --- /dev/null +++ b/research/f7-functional-independent-check/test_verify.py @@ -0,0 +1,176 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Behavioural tests for the f7 functional-independent-check primitives. + +These assert what a reader of the receipt can observe: the walk, the three +predicates, the budget arithmetic, the false-prune decision on the published +fixture word, the canonical form, the domain guards and the internal +consistency of one full domain classification. Roughly one second in total. +""" + +import json +import sys +import unittest +from pathlib import Path + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) + +import verify # noqa: E402 + + +class WalkTests(unittest.TestCase): + def test_fixture_prefix_states(self): + word = verify.PUBLISHED_FIXTURE["word"] + self.assertEqual(verify.prefix_states(word), + verify.PUBLISHED_FIXTURE["prefix_states"]) + + def test_walk_starts_at_zero(self): + self.assertEqual(verify.prefix_states((0, 1))[0], 0) + + def test_labelled_steps_xor_basis_vectors(self): + self.assertEqual(verify.prefix_states((0, 2, 0)), (0, 1, 5, 4)) + + def test_restoration_is_even_label_counts(self): + self.assertTrue(verify.is_restored(verify.PUBLISHED_FIXTURE["word"])) + self.assertFalse(verify.is_restored((0, 0, 1))) + self.assertTrue(verify.is_restored(())) + + +class PredicateTests(unittest.TestCase): + def test_fixture_is_simple_universal_restored(self): + word = verify.PUBLISHED_FIXTURE["word"] + self.assertTrue(verify.is_simple(word)) + self.assertTrue(verify.is_universal(word, 4)) + self.assertEqual(verify.sumset_size(word, 4), 16) + + def test_repeated_state_is_not_simple(self): + self.assertFalse(verify.is_simple((0, 0, 0, 0))) + + def test_non_universal_word_is_rejected(self): + word = verify.PUBLISHED_FIXTURE["word"] + self.assertFalse(verify.is_universal(word, 5)) + + +class BudgetTests(unittest.TestCase): + def test_published_budgets(self): + for (n, length), row in verify.PUBLISHED_TABLE.items(): + self.assertEqual(verify.base_budget(n, length), row[2], + f"base budget {(n, length)}") + + def test_odd_length_rejected(self): + with self.assertRaises(ValueError): + verify.base_budget(4, 9) + + def test_fixture_budget_arithmetic(self): + s, t = verify.PUBLISHED_FIXTURE["bit0_split"] + base = verify.base_budget(4, 8) + self.assertEqual(base, 5) + self.assertEqual(base + ((s - t) // 2) ** 2, 9) + + +class FalsePruneTests(unittest.TestCase): + def test_fixture_word_fires_for_bit_zero(self): + word = verify.PUBLISHED_FIXTURE["word"] + states = verify.prefix_states(word)[:-1] + fired, detail = verify.false_prune(4, 8, states, 0b0001) + self.assertTrue(fired) + self.assertEqual(detail, (8, 6, 2, 5, 2)) + + def test_fixture_word_is_sound_for_all_ones(self): + word = verify.PUBLISHED_FIXTURE["word"] + states = verify.prefix_states(word)[:-1] + fired, detail = verify.false_prune(4, 8, states, 0b1111) + self.assertFalse(fired) + self.assertEqual(detail[0], 0) + + def test_shifting_the_budget_changes_the_decision(self): + word = verify.PUBLISHED_FIXTURE["word"] + states = verify.prefix_states(word)[:-1] + self.assertTrue(verify.false_prune(4, 8, states, 0b0001, extra=-3)[0] is False) + + def test_excess_routes_agree(self): + word = verify.PUBLISHED_FIXTURE["word"] + states = verify.prefix_states(word)[:-1] + for mask in range(1, 16): + self.assertEqual(verify.excess_by_counter(states, mask), + verify.excess_by_set(states, mask)) + + +class CanonicalFormTests(unittest.TestCase): + def test_canonical_form_relabels_by_first_occurrence(self): + self.assertEqual(verify.canonical_form((3, 3, 7, 3, 7)), (0, 0, 1, 0, 1)) + + def test_canonical_form_is_idempotent(self): + word = (0, 1, 0, 2, 1, 3, 2, 3) + self.assertEqual(verify.canonical_form(verify.canonical_form(word)), word) + + def test_canonical_words_start_with_zero(self): + words, _ = verify.enumerate_canonical(4, 8) + self.assertTrue(all(w[0] == 0 for w in words)) + + +class EnumeratorTests(unittest.TestCase): + def test_published_word_counts(self): + for (n, length) in ((3, 6), (3, 8), (4, 8), (4, 10), (5, 10)): + words, _ = verify.enumerate_canonical(n, length) + self.assertEqual(len(words), verify.PUBLISHED_TABLE[(n, length)][0], + f"word count {(n, length)}") + + def test_unconstrained_route_agrees(self): + canonical, _ = verify.enumerate_canonical(4, 8) + unconstrained, _ = verify.enumerate_unconstrained(4, 8) + self.assertEqual(set(canonical), unconstrained) + + def test_domain_guards(self): + for bad in ((8, 8), (4, 15), (4, 9), (0, 8)): + with self.assertRaises(ValueError): + verify.enumerate_canonical(*bad) + + def test_every_word_is_simple_and_restored(self): + words, _ = verify.enumerate_canonical(5, 10) + self.assertTrue(all(verify.is_simple(w) for w in words)) + self.assertTrue(all(verify.is_restored(w) for w in words)) + + +class DomainRecordTests(unittest.TestCase): + def setUp(self): + self.record = verify.classify_domain(4, 8) + + def test_record_matches_published_row(self): + simple, universal, base, prunes = verify.PUBLISHED_TABLE[(4, 8)] + self.assertEqual(self.record["simple_closed_words"], simple) + self.assertEqual(self.record["universal_words"], universal) + self.assertEqual(self.record["base_budget"], base) + self.assertEqual(self.record["false_prunes"], prunes) + + def test_per_mask_counts_close_the_total(self): + self.assertEqual(sum(self.record["per_mask_counts"].values()), + self.record["false_prunes"]) + self.assertEqual(self.record["bit0_false_prunes"], + self.record["per_mask_counts"]["1"]) + + def test_sound_and_firing_masks_partition_the_functionals(self): + self.assertEqual(len(self.record["firing_masks"]) + len(self.record["sound_masks"]), + self.record["masks_total"]) + + +class ReceiptTests(unittest.TestCase): + def test_committed_receipt_matches_a_fresh_run(self): + fresh = verify.run(selected_new=[(4, 12)]) + committed = json.loads(verify.RESULT_PATH.read_text()) + self.assertEqual(committed["published_domains"], fresh["published_domains"]) + self.assertEqual(committed["fixture"], fresh["fixture"]) + self.assertEqual(committed["cross_check"], fresh["cross_check"]) + self.assertEqual(committed["new_domains"][1]["n"], 4) + self.assertEqual(committed["new_domains"][1]["L"], 12) + + def test_new_domains_are_present_and_distinct(self): + committed = json.loads(verify.RESULT_PATH.read_text()) + seen = {(row["n"], row["L"]) for row in committed["new_domains"]} + self.assertEqual(seen, set(verify.NEW_DOMAINS)) + published = {(row["n"], row["L"]) for row in committed["published_domains"]} + self.assertEqual(published & seen, set()) + + +if __name__ == "__main__": + unittest.main(verbosity=2) diff --git a/research/f7-functional-independent-check/verify.py b/research/f7-functional-independent-check/verify.py new file mode 100644 index 0000000000..c08726b019 --- /dev/null +++ b/research/f7-functional-independent-check/verify.py @@ -0,0 +1,465 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Independent re-derivation of the f7 functional classification, plus two new domains. + +Subject of the check +-------------------- +`research/f7-bit0-functional-classification` (Nick Petalas) claims a finite +certificate over the PR943 singleton prefix walk: for a word `w` of even length +`L` over `[0, n)`, put `q_0 = 0`, `q_{i+1} = q_i XOR (1 << w_i)`. A word is + + restored : every label occurs an even number of times (equivalently q_L = q_0), + simple : q_0 .. q_{L-1} are distinct, + universal : S + S = F2^n for the set S of prefix states, + +and the retained engines substitute the fixed budget + + base = 2 * C(L/2, 2) - (2^(n-1) - 1) + +for the exact collision budget `base + d^2` with `d = (s - t)/2`, where `s`, `t` +are the sizes of the even/odd classes of a nonzero linear functional. The claim +is a table of, per domain, the number of simple closed words, the number of +universal words, the number of words for which the substitution *falsely prunes* +(`base < a + b <= base + d^2`, with `a + b` the collision excess), the firing +mask set and the per-mask counts. + +What this module does +--------------------- +It recomputes every number in that table from scratch, with its own enumerator +and its own classifier, and asserts exact equality with the published values. +It then extends the census to three domains the published table does not +contain, including `(5, 14)`, which the published package names as its open +next question. + +Independence. No predecessor package code is imported, executed or copied here. +The published numbers are embedded as asserted constants; the enumeration, +the walk, the universality test and the collision excess are separate +implementations. Two internal routes are compared on every run: a canonical +depth-first enumeration, and an unconstrained enumeration that is canonicalised +afterwards. No Git objects, no network, no third-party package. +""" + +import argparse +import json +import sys +from collections import Counter +from itertools import combinations, product +from pathlib import Path + +HERE = Path(__file__).resolve().parent +RESULT_PATH = HERE / "RESULT.json" + +MAX_N = 7 +MAX_L = 14 + +# --------------------------------------------------------------------------- +# Published claim under check (research/f7-bit0-functional-classification) +# --------------------------------------------------------------------------- + +# (n, L) -> (simple_closed_words, universal_words, base_budget, false_prunes) +PUBLISHED_TABLE = { + (3, 6): (4, 4, 3, 0), + (3, 8): (2, 2, 9, 0), + (4, 8): (29, 22, 5, 44), + (4, 10): (110, 110, 13, 190), + (5, 10): (358, 0, 5, 0), + (5, 12): (3695, 828, 15, 2856), + (6, 12): (6525, 0, -1, 0), + (6, 14): (123704, 0, 11, 0), + (7, 14): (161936, 0, -21, 0), +} + +# (n, L) -> {mask: false prune count} for the three firing domains only. These +# are the published per-functional counts, transcribed from the published +# receipt; each row sums to that domain's published `false_prunes`. +PUBLISHED_MASK_COUNTS = { + (4, 8): {1: 6, 2: 6, 3: 5, 4: 4, 5: 1, 6: 5, 8: 8, 9: 4, 12: 5}, + (4, 10): {1: 20, 2: 20, 3: 10, 4: 23, 5: 8, 6: 16, 8: 37, 9: 18, + 10: 10, 12: 28}, + (5, 12): {1: 248, 2: 248, 3: 96, 4: 278, 5: 143, 6: 119, 7: 25, + 8: 221, 9: 41, 10: 105, 11: 15, 12: 175, 13: 10, 14: 26, + 16: 361, 17: 140, 18: 100, 19: 50, 20: 64, 21: 4, 22: 32, + 24: 241, 25: 44, 28: 70}, +} + +# The published bit-0 column (functional mask 1) of the retained engine. +PUBLISHED_BIT0_FALSE_PRUNES = {(4, 8): 6, (4, 10): 20, (5, 12): 248} + +# Fixture published with the table: the canonical word 01021323 at (4, 8). +PUBLISHED_FIXTURE = { + "word": (0, 1, 0, 2, 1, 3, 2, 3), + "prefix_states": (0, 1, 3, 2, 6, 4, 12, 8, 0), + "distinct_nonclosing": 8, + "restored": True, + "universal": True, + "weight_split": (4, 4), + "weight_excess": 0, + "bit0_split": (6, 2), + "bit0_excess": 8, + "substituted_budget": 5, + "correct_bit0_budget": 9, +} + +# Domains in the published table, and the new domains this package adds. +PUBLISHED_DOMAINS = sorted(PUBLISHED_TABLE) +NEW_DOMAINS = [(3, 10), (4, 12), (5, 14)] +# Unconstrained-enumeration cross-check domains (canonical forms must agree). +CANONICAL_CROSS_CHECK = [(3, 6), (3, 8), (4, 8), (4, 10), (5, 10), (5, 12)] + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +# --------------------------------------------------------------------------- +# Walk, predicates and collision excess +# --------------------------------------------------------------------------- + + +def prefix_states(word): + """q_0 .. q_L for the singleton prefix walk, as a tuple.""" + q = 0 + out = [q] + for lab in word: + q ^= 1 << lab + out.append(q) + return tuple(out) + + +def is_simple(word): + states = prefix_states(word) + return len(set(states[:-1])) == len(word) + + +def is_restored(word): + counts = Counter(word) + return all(value % 2 == 0 for value in counts.values()) + + +def is_universal(word, n): + states = set(prefix_states(word)[:-1]) + reach = {x ^ y for x in states for y in states} + return len(reach) == (1 << n) + + +def sumset_size(word, n): + states = set(prefix_states(word)[:-1]) + return len({x ^ y for x in states for y in states}) + + +def excess_by_counter(states, mask): + """Collision excess a + b, computed from a difference multiplicity table. + + For a class C of size k the excess is C(k, 2) - |{x XOR y : x != y, in C}|. + Counting unordered pairs per difference gives the same number through + `sum(u_d - 1 over appearing d)` because the appearing differences partition + the unordered pairs. + """ + even, odd = [], [] + for point in states: + (even if bin(point & mask).count("1") % 2 == 0 else odd).append(point) + excess = 0 + for side in (even, odd): + diff = Counter() + for x, y in combinations(side, 2): + diff[x ^ y] += 1 + for value in diff.values(): + excess += value - 1 + return excess, len(even), len(odd) + + +def excess_by_set(states, mask): + """The same excess by the direct support-size difference.""" + even, odd = [], [] + for point in states: + (even if bin(point & mask).count("1") % 2 == 0 else odd).append(point) + excess = 0 + for side in (even, odd): + support = {x ^ y for x, y in combinations(side, 2)} + excess += len(side) * (len(side) - 1) // 2 - len(support) + return excess, len(even), len(odd) + + +def base_budget(n, L): + require(L % 2 == 0, "even length required") + half = L // 2 + return 2 * (half * (half - 1) // 2) - ((1 << (n - 1)) - 1) + + +def false_prune(n, L, states, mask, extra=0): + """Does the fixed `base` budget wrongly reject this word for this functional? + + `extra` widens the right-hand endpoint, which is how the sensitivity control + perturbs the rule under check. + """ + excess, s, t = excess_by_counter(states, mask) + require((s - t) % 2 == 0, "class-size parity") + d = (s - t) // 2 + base = base_budget(n, L) + return base < excess <= base + extra + d * d, (excess, s, t, base, d) + + +# --------------------------------------------------------------------------- +# Two independent enumerators +# --------------------------------------------------------------------------- + + +def enumerate_canonical(n, L): + """First-occurrence words of length L: q_0..q_{L-1} distinct, q_L = q_0. + + `maxlab` enforces first-occurrence label order, so each relabelling class + contributes exactly one word. The last step is forced (it must close). + """ + require(1 <= n <= MAX_N and 2 <= L <= MAX_L and L % 2 == 0, "domain bounds") + words, nodes = [], 0 + stack = [(0, 1, -1, 0, ())] # state, visited states, max label, depth, word + while stack: + q, visited, maxlab, depth, word = stack.pop() + nodes += 1 + if depth == L: + if q == 0: + words.append(word) + continue + top = min(maxlab + 1, n - 1) + if depth == L - 1: + for lab in range(top + 1): + if q ^ (1 << lab) == 0: + stack.append((0, visited, max(maxlab, lab), depth + 1, word + (lab,))) + else: + for lab in range(top + 1): + nq = q ^ (1 << lab) + if not (visited >> nq) & 1: + stack.append((nq, visited | (1 << nq), max(maxlab, lab), + depth + 1, word + (lab,))) + return words, nodes + + +def enumerate_unconstrained(n, L): + """Every word of length L (canonical order dropped), filtered afterwards. + + Returns the set of first-occurrence canonical forms, so its cardinality is + comparable with `enumerate_canonical`. + """ + require(1 <= n <= MAX_N and 2 <= L <= MAX_L and L % 2 == 0, "domain bounds") + forms, nodes = set(), 0 + stack = [(0, frozenset([0]), 0, ())] # state, visited states, depth, word + while stack: + q, visited, depth, word = stack.pop() + nodes += 1 + if depth == L: + if q == 0: + forms.add(canonical_form(word)) + continue + last = depth == L - 1 + for lab in range(n): + nq = q ^ (1 << lab) + if last: + if nq == 0: + stack.append((0, visited, depth + 1, word + (lab,))) + elif nq not in visited: + stack.append((nq, visited | {nq}, depth + 1, word + (lab,))) + return forms, nodes + + +def canonical_form(word): + """Relabel by first occurrence: 0, 1, 2, ...""" + seen, out = {}, [] + for lab in word: + if lab not in seen: + seen[lab] = len(seen) + out.append(seen[lab]) + return tuple(out) + + +# --------------------------------------------------------------------------- +# Domain census +# --------------------------------------------------------------------------- + + +def classify_domain(n, L): + """Complete functional classification of one (n, L) domain.""" + words, nodes = enumerate_canonical(n, L) + simple_closed = len(words) + universal = [w for w in words if is_universal(w, n)] + masks = range(1, 1 << n) + per_mask = {} + per_mask_bit0 = {} + for mask in masks: + hits = 0 + for word in universal: + states = prefix_states(word)[:-1] + fired, _ = false_prune(n, L, states, mask) + if fired: + hits += 1 + if hits: + per_mask[mask] = hits + for word in universal: + states = prefix_states(word)[:-1] + if false_prune(n, L, states, 1)[0]: + per_mask_bit0[word] = 1 + weight_of = {m: bin(m).count("1") for m in masks} + firing = sorted(per_mask) + return { + "n": n, + "L": L, + "base_budget": base_budget(n, L), + "nodes": nodes, + "simple_closed_words": simple_closed, + "universal_words": len(universal), + "false_prunes": sum(per_mask.values()), + "bit0_false_prunes": len(per_mask_bit0), + "per_mask_counts": {str(m): per_mask[m] for m in firing}, + "firing_masks": firing, + "firing_weights": sorted({weight_of[m] for m in firing}), + "sound_masks": sorted(set(masks) - set(firing)), + "masks_total": (1 << n) - 1, + } + + +def verify_fixture(): + word = PUBLISHED_FIXTURE["word"] + states = prefix_states(word) + require(states == PUBLISHED_FIXTURE["prefix_states"], "fixture prefix states") + require(len(set(states[:-1])) == PUBLISHED_FIXTURE["distinct_nonclosing"], + "fixture distinct states") + require(is_restored(word) is True, "fixture restoration") + require(is_universal(word, 4) is True, "fixture universality") + weight_excess, s_w, t_w = excess_by_counter(states[:-1], 0b1111) + require((s_w, t_w) == PUBLISHED_FIXTURE["weight_split"], "fixture weight split") + require(weight_excess == PUBLISHED_FIXTURE["weight_excess"], "fixture weight excess") + bit0_excess, s_0, t_0 = excess_by_counter(states[:-1], 0b0001) + require((s_0, t_0) == PUBLISHED_FIXTURE["bit0_split"], "fixture bit0 split") + require(bit0_excess == PUBLISHED_FIXTURE["bit0_excess"], "fixture bit0 excess") + require(base_budget(4, 8) == PUBLISHED_FIXTURE["substituted_budget"], "fixture budget") + s_f, t_f = PUBLISHED_FIXTURE["bit0_split"] + exact = s_f * (s_f - 1) // 2 + t_f * (t_f - 1) // 2 - ((1 << 3) - 1) + require(exact == PUBLISHED_FIXTURE["correct_bit0_budget"], "fixture corrected budget") + require(exact == base_budget(4, 8) + ((s_f - t_f) // 2) ** 2, + "fixture corrected budget equals base + d^2") + return {"word": "".join(str(d) for d in word), + "prefix_states": list(states), + "bit0_excess": bit0_excess, + "substituted_budget": base_budget(4, 8), + "correct_bit0_budget": PUBLISHED_FIXTURE["correct_bit0_budget"]} + + +def run(selected_new=NEW_DOMAINS): + receipt = {"schema": 1, "fixture": verify_fixture(), + "published_domains": [], "new_domains": [], "controls": {}, + "cross_check": []} + + for (n, L) in PUBLISHED_DOMAINS: + record = classify_domain(n, L) + claim_simple, claim_universal, claim_base, claim_prunes = PUBLISHED_TABLE[(n, L)] + require(record["simple_closed_words"] == claim_simple, + f"simple closed count {(n, L)}") + require(record["universal_words"] == claim_universal, + f"universal count {(n, L)}") + require(record["base_budget"] == claim_base, f"base budget {(n, L)}") + require(record["false_prunes"] == claim_prunes, f"false prune count {(n, L)}") + expected = PUBLISHED_MASK_COUNTS.get((n, L), {}) + require(record["per_mask_counts"] == {str(k): v for k, v in expected.items()}, + f"per-mask counts {(n, L)}") + if (n, L) in PUBLISHED_BIT0_FALSE_PRUNES: + require(record["bit0_false_prunes"] == PUBLISHED_BIT0_FALSE_PRUNES[(n, L)], + f"bit-0 false prune count {(n, L)}") + receipt["published_domains"].append(record) + + for (n, L) in selected_new: + receipt["new_domains"].append(classify_domain(n, L)) + + # Control 1: every enumerated word is restored and simple by construction, + # and the two independent excess routes agree everywhere. + pairs = 0 + for (n, L) in PUBLISHED_DOMAINS + list(selected_new): + words, _ = enumerate_canonical(n, L) + for word in words: + require(is_restored(word), f"enumerated word not restored at {(n, L)}") + require(is_simple(word), f"enumerated word not simple at {(n, L)}") + if not is_universal(word, n): + continue + states = prefix_states(word)[:-1] + for mask in range(1, 1 << n): + if excess_by_counter(states, mask) != excess_by_set(states, mask): + raise ValueError(f"excess routes disagree at {(n, L)} mask {mask}") + pairs += 1 + receipt["controls"]["excess_route_pairs"] = pairs + + # Control 2: shifting the substituted budget must change the firing pattern, + # which shows the check depends on the exact budget value and not only on the + # class sizes. Every domain with no universal word must stay at zero. + shifted = {} + for shift in (-2, -1, 1, 2): + row = {} + for (n, L) in PUBLISHED_DOMAINS: + words, _ = enumerate_canonical(n, L) + hits = 0 + for word in words: + if not is_universal(word, n): + continue + states = prefix_states(word)[:-1] + for mask in range(1, 1 << n): + if false_prune(n, L, states, mask, extra=shift)[0]: + hits += 1 + row[f"{n},{L}"] = hits + shifted[str(shift)] = row + changed = [] + for (n, L) in PUBLISHED_DOMAINS: + key = f"{n},{L}" + claim = PUBLISHED_TABLE[(n, L)][3] + vals = {shifted[str(shift)][key] for shift in (-2, -1, 1, 2)} + if claim == 0: + require(vals == {0}, f"a budget shift invented prunes at {(n, L)}: {vals}") + elif vals != {claim}: + changed.append(key) + require(sorted(changed) == ["4,10", "4,8", "5,12"], + f"a budget shift must move exactly the firing domains, got {changed}") + receipt["controls"]["budget_shift_prunes"] = shifted + + # Control 3: unconstrained enumeration must reproduce the canonical census. + for (n, L) in CANONICAL_CROSS_CHECK: + canonical, _ = enumerate_canonical(n, L) + unconstrained, _ = enumerate_unconstrained(n, L) + require(set(canonical) == unconstrained, + f"enumerators disagree at {(n, L)}: " + f"{len(set(canonical) ^ unconstrained)} symmetric difference") + receipt["cross_check"].append( + {"n": n, "L": L, "words": len(unconstrained)}) + + return receipt + + +def write_receipt(receipt): + RESULT_PATH.write_text(json.dumps(receipt, indent=1, sort_keys=True) + "\n") + + +def main(argv=None): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", action="store_true", + help="regenerate RESULT.json beside this file") + args = parser.parse_args(argv) + receipt = run() + if args.write: + write_receipt(receipt) + else: + require(RESULT_PATH.exists(), "committed RESULT.json is missing") + committed = json.loads(RESULT_PATH.read_text()) + require(committed == receipt, "fresh receipt differs from committed RESULT.json") + for record in receipt["published_domains"]: + print(f"published n={record['n']} L={record['L']}: " + f"closed={record['simple_closed_words']} " + f"universal={record['universal_words']} " + f"false_prunes={record['false_prunes']} " + f"weights={record['firing_weights']}") + for record in receipt["new_domains"]: + print(f"new n={record['n']} L={record['L']}: " + f"closed={record['simple_closed_words']} " + f"universal={record['universal_words']} " + f"false_prunes={record['false_prunes']} " + f"weights={record['firing_weights']}") + print("PASS_F7_FUNCTIONAL_INDEPENDENT_CHECK") + return 0 + + +if __name__ == "__main__": + sys.exit(main()) From a133037b1eadc2315430fcdaa24488ab6ec9d958 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Sun, 18 Oct 2026 20:07:48 +0100 Subject: [PATCH 2/2] research: record the checked head in the package text, not as a source pin The checked package's head is not an ancestor of this publication commit, so its exact objects cannot be SOURCES.json rows. Move the head, SHA-256 and blob ids into the README and keep SOURCES.json to ancestor files. --- .../f7-functional-independent-check/README.md | 13 ++++++++++++ .../SOURCES.json | 21 ------------------- 2 files changed, 13 insertions(+), 21 deletions(-) diff --git a/research/f7-functional-independent-check/README.md b/research/f7-functional-independent-check/README.md index cda2498004..e13182fe15 100644 --- a/research/f7-functional-independent-check/README.md +++ b/research/f7-functional-independent-check/README.md @@ -17,6 +17,19 @@ This package recomputes that certificate from scratch and extends it to three domains the published table does not contain, including `(5, 14)`, which the published package lists as its open next question 2. +The claim under check is fixed at that package's own publication head +`13db47d8d31603c1391572009e1eb7a22675a219`, where its `README.md`, +`RESULT.json` and `verify.py` have SHA-256 +`8176c8a889671f67ebcd6f1b9e9efddae55cfbbff4b486442a9b63977e9c4844`, +`5938908a76c497bad4c301eed0f12822fc16b0fbbbff2c0bc5150d82f2052105` and +`a0c93985734fa6855c5561a1b4eb730ef0af6ddd25bfdac1ef8b61d840efbe83` and Git +blob ids `4618c68ffc94be30055537bca4e49696946437dc`, +`84017d1265858fe976bd317c95d287c92fc4cb7e` and +`f554ec10c8ac5e30e067b01adf9b68b2eb80906a`. Those three objects are not +ancestors of this package's publication commit (the checked PR is still open), +so they are recorded here rather than in `SOURCES.json`, whose rows must be +ancestors. + ## What is reproduced, and how `verify.py` is a separate implementation. It imports, executes and copies no diff --git a/research/f7-functional-independent-check/SOURCES.json b/research/f7-functional-independent-check/SOURCES.json index da271bd3d9..306533a2ea 100644 --- a/research/f7-functional-independent-check/SOURCES.json +++ b/research/f7-functional-independent-check/SOURCES.json @@ -31,27 +31,6 @@ "usage": "provenance", "sha256": "d2507c556e23b36601d64c24ac394ab7192bd897d25f94e18471c86f83617efb", "git_blob": "83b23ff085f24451350dd9fe54b8efad68dc80dd" - }, - { - "path": "research/f7-bit0-functional-classification/README.md", - "usage": "provenance", - "pin": "head:13db47d8d31603c1391572009e1eb7a22675a219:research/f7-bit0-functional-classification/README.md", - "sha256": "8176c8a889671f67ebcd6f1b9e9efddae55cfbbff4b486442a9b63977e9c4844", - "git_blob": "4618c68ffc94be30055537bca4e49696946437dc" - }, - { - "path": "research/f7-bit0-functional-classification/RESULT.json", - "usage": "provenance", - "pin": "head:13db47d8d31603c1391572009e1eb7a22675a219:research/f7-bit0-functional-classification/RESULT.json", - "sha256": "5938908a76c497bad4c301eed0f12822fc16b0fbbbff2c0bc5150d82f2052105", - "git_blob": "84017d1265858fe976bd317c95d287c92fc4cb7e" - }, - { - "path": "research/f7-bit0-functional-classification/verify.py", - "usage": "provenance", - "pin": "head:13db47d8d31603c1391572009e1eb7a22675a219:research/f7-bit0-functional-classification/verify.py", - "sha256": "a0c93985734fa6855c5561a1b4eb730ef0af6ddd25bfdac1ef8b61d840efbe83", - "git_blob": "f554ec10c8ac5e30e067b01adf9b68b2eb80906a" } ] }