Prove the fixed L/2 firing set's first all-sound length for every n >= 5: L*(n) = 2^n - 2 floor(sqrt(2^(n-1)-1)), with explicit firing words one step below (no new κ)

research/f7-firing-threshold-all-n/README.md

@@ -0,0 +1,142 @@
+# The first all-sound length of the fixed L/2 substitution, for every n ≥ 5
+
+**Claim type: a proof for every n ≥ 5, with finite checks and explicit
+witnesses. No new κ.** The selected conditional κ stays
+`0.001672660197076918`.
+
+## Object
+
+[PR #4322](https://github.com/CrocSwap/integer-mult-bounds/pull/4322)
+(unpaidmoon) studies the fixed `L/2` substitution on prefix walks of `F_2^n`.
+A nonzero mask fires on a universal simple restored word when
+
+```text
+base < excess <= base + d^2,     base(n, L) = (L/2)(L/2 - 1) - (2^(n-1) - 1).
+```
+
+It found that the firing set is empty from `L = 14` at `n = 4`, and it left
+three questions open:
+
+- the first all-sound length at `n = 5`;
+- whether larger `n` repeat the collapse;
+- whether "the firing set eventually becomes empty for every n" (it says
+  neither of its results shows this).
+
+[#4348](https://github.com/CrocSwap/integer-mult-bounds/pull/4348) answered
+the first by census: the answer is 26.
+
+## Theorem
+
+For every `n ≥ 5`, the first even length at which no mask fires on any
+universal canonical word is exactly
+
+```text
+L*(n) = 2^n - 2 floor(sqrt(2^(n-1) - 1)).
+```
+
+From `L*(n)` up to `2^n`, every functional is sound on **every** `L`-point
+subset of `F_2^n`. At `L*(n) − 2` a weight-one mask fires on an explicit
+word. Values:
+
+| n | 4 | 5 | 6 | 7 | 8 | 9 | 10 | 12 | 16 | 20 |
+|---|---:|---:|---:|---:|---:|---:|---:|---:|---:|---:|
+| `L*` | 14* | 26 | 54 | 114 | 234 | 482 | 980 | 4006 | 65174 | 1047128 |
+
+`n = 4` (marked *) is #4322's theorem: there the closed form would give 12,
+but another split binds. `2^n − L*(n) ≈ 2^((n+1)/2)`. The answer at `n = 5`
+agrees with #4348's census.
+
+So the collapse recurs for every `n`, and only near-Hamiltonian lengths are
+safe for large `n`.
+
+## Proof
+
+**1. Min-sumset cap.** For `A ⊆ F_2^k` with `|A| > 2^(d−1)`,
+`|A + A| ≥ 2^d`.
+
+By Kneser's theorem, `|A+A| ≥ 2|A+H| − |H|`, where `H` is the stabilizer of
+`A+A`, of order `2^h`.
+
+- If `h ≥ d`, then `|A+A| ≥ |H| ≥ 2^d`.
+- Otherwise `A+H` has `a > 2^(d−1−h)` cosets, so
+  `|A+A| ≥ (2a−1)2^h ≥ 2^d + 2^h`.
+
+Equality holds for `A` inside a subgroup of order `2^d`.
+
+A level set of a nonzero functional is an affine flat, and differences in
+characteristic 2 are sums. So a `k`-point side has excess at most
+`e(k) = C(k,2) − 2^⌈log₂k⌉ + 1`, and a split `(s,t)` has excess at most
+`e(s) + e(t)`.
+
+**2. The binding split.** Write `s = 2^(n−1)` and `L = 2(s − j)`.
+
+For the split `(s, s − 2j)`, a full level set against the rest, with
+`s − 2j > 2^(n−2)`, direct expansion gives
+
+```text
+base(n, L) − (e(s) + e(s − 2j)) = (s − 1) − j².
+```
+
+Take `L ≥ L*(n)`, so `j ≤ ⌊√(s−1)⌋`. For `n ≥ 6`, every split `(s', L−s')`
+then has both parts in `(2^(n−2), 2^(n−1)]`. On that range `e` is
+`C(·,2)` minus a constant, which is convex, so the split cap is largest at
+the extreme split. Hence the cap is at most `base`, and nothing fires on any
+subset. `n = 5` is covered by the full scan.
+
+**3. Sharpness.** Take `j = ⌊√(s−1)⌋ + 1` and `t = s − 2j`. The walk is built
+in two halves, using bit 1 as `x_1`:
+
+- **The half `x_1 = 0`.** All of it is traversed along the reflected Gray
+  cycle of the other `n − 1` bits, cut at its closing edge.
+- **The half `x_1 = 1`.** A "ladder" path through exactly `t` points: the
+  first `t/2` rows of the lower Gray cycle, on both values of the top bit.
+- **The halves join** at the two ends of the cut edge.
+
+The result is a simple closed walk of length `L*(n) − 2`, and it is
+universal. For the mask `e_1`:
+
+- the full side has excess `e(s)` exactly;
+- the other side has `t > 2^(n−2)` points of one coset, so its sum set is
+  the whole subgroup and its excess is `e(t)` exactly;
+- the total exceeds `base` by `j² − (s−1) > 0` and is at most `base + j²`,
+  so `e_1` fires. The canonical relabeling carries this to a mask of the
+  canonical word.
+
+## Checks in `verify.py`
+
+| Check | Result |
+| --- | --- |
+| `|A+A| ≥ 2^⌈log₂|A|⌉` and the cap `e(k)` | exhaustive in `F_2^k`, `k ≤ 4` (all 65,536 subsets at `k = 4`); the cap is attained exactly |
+| Cap threshold by a full split scan | 6, 14, then exactly the closed form for every `5 ≤ n ≤ 22` |
+| `t > 2^(n−2)` at `L*` | every `6 ≤ n < 40` |
+| Explicit word at `L*(n) − 2`, `n = 5..11` | simple, closed, universal; `e_1` fires; the canonical word fires its relabeled mask |
+| Controls of length `L*(n)` | nothing fires: every mask for `n ≤ 8`, `e_1` for `n ≤ 11` |
+| #3733's `(4,12)` on main | still fires, so the `n = 4` threshold 14 is attained |
+
+## Not covered
+
+- Which masks fire below `L*(n) − 2`, and whether the firing set is
+  monotone below that.
+- `(7, 18)` and `(7, 20)`. Those are far below `L*(7) = 114`, so this theorem
+  says nothing there.
+- Any change to a retained exclusion.
+
+## Reproduce
+
+```sh
+python3.12 -B research/f7-firing-threshold-all-n/verify.py
+```
+
+It prints `PASS_F7_FIRING_THRESHOLD_ALL_N` in about 6 seconds, using only the
+standard library.
+
+## Open next questions
+
+None for the first all-sound length; it is decided for every `n ≥ 4`.
+
+## Credit
+
+The model and the `n = 4` theorem are unpaidmoon's (#4322), building on Nick
+Petalas's #3699 and #3733. Kneser's theorem is classical. Prepared by Ryanson
+Jonathan with substantial Claude Code (Claude Opus 5.5) assistance.
+Apache-2.0.

research/f7-firing-threshold-all-n/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65",
+      "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96"
+    },
+    {
+      "path": "research/f7-functional-independent-check/RESULT.json",
+      "usage": "input",
+      "git_blob": "d4f2bd8cc0bfb19ebc4d2c3212170472c690779b",
+      "sha256": "a94ad29fbaaf908ebb64b12d6270402cf8aef6f5f24b3babb1152ecabe44cb3f"
+    }
+  ]
+}

research/f7-firing-threshold-all-n/TASK.json

@@ -0,0 +1,60 @@
+{
+  "schema_version": 1,
+  "task_id": "census-pruning-audit",
+  "priority_revision": 7,
+  "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+  "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": "Decide, for every n >= 5, the first even length at which the fixed L/2 substitution fires on no universal canonical word, answering #4322's open question 3 and its 'eventually empty for every n' remark.",
+  "scope_change_reason": "#4322 and #4348 settle n = 4 and n = 5 by census; a min-sumset cap and an explicit construction settle every n.",
+  "bottleneck_link": "Where the fixed substitution is sound decides which census exclusions it can shortcut at each dimension.",
+  "budget_minutes": 40,
+  "stop_rule": "Stop once the threshold is proved for every n and checked against the census values.",
+  "outcome": "completed",
+  "evidence": "verify.py: |A+A| >= 2^ceil(log2|A|) exhaustive in F_2^k, k <= 4, with the cap attained; full split scan gives 6, 14 and exactly L*(n) for 5 <= n <= 22; explicit universal words of length L*(n) - 2 fire mask e_1 for 5 <= n <= 11, also after canonical relabeling; length-L* controls fire nothing; #3733's (4,12) fires on main.",
+  "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance",
+  "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance in reading, verifier implementation and writing; no independent human or proof-kernel review.",
+  "open_questions": [],
+  "no_open_questions_reason": "The first all-sound length is decided for every n >= 4."
+}

research/f7-firing-threshold-all-n/VERIFY.json

@@ -0,0 +1,20 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/f7-functional-independent-check/RESULT.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Min-sumset lemma and cap exhaustive in F_2^k (k <= 4); cap threshold scan vs closed form (5 <= n <= 22); split-range condition; explicit firing walks at L*(n) - 2 (n = 5..11) simple, closed, universal and firing, with canonical relabeling; length-L* controls; #3733 (4,12) on main."
+    }
+  ]
+}