Audit the 20-prefix confinement step of the length-22 exclusion (no new kappa)

research/f7-l22-confinement-audit/README.md

@@ -0,0 +1,143 @@
+# An independent audit of the 20-prefix confinement step in `f(7) = 24`
+
+**Bounded independent verification, no kappa, no frontier change.** This
+package re-derives and re-checks one step of the length-22 argument in
+[PR #3058](../../research/connector-covering-code/README.md) (*the minimum
+universal restored seven-source singleton word has 24 steps*), and records a
+word-level search with a validated positive control. It does **not** re-prove
+`f(7) = 24`; the part it leaves open is named below.
+
+## What is checked, and at what strength
+
+In PR943's singleton prefix-walk model a word of even length `L` is restored
+when every label appears a positive even number of times, and universal exactly
+when its **set** of prefix states `P` satisfies `P + P = F2^7`. A 22-step word
+therefore has `20 <= |P| <= 22` (the covering bound `ell(7,2) = 19` and the
+size-21 and size-22 arguments are **imported**, not re-proved here).
+
+**Step audited: `|P| = 20` is impossible.** If `|P| = 20`, every position of
+the walk lies in the twenty-point set `T = P`, so the walk would be a closed
+walk spanning `T`; the graph induced on `T` by the walk's seven directions `D`
+must then be connected. Each direction of `D` contributes only the pairs of `T`
+at that one difference, so
+
+```
+edges(G(T, D)) <= (sum of the seven largest multiplicity classes of diff(T)),
+```
+
+while a graph on twenty vertices with at most two components needs at least
+eighteen edges. Every 20-point cover is an affine image of `{0} u S` for one of
+the five 19-point representatives classified in DMP's Table 1 (imported), and
+`G(M T + b, D) = G(T, M^-1 D)`, so one inequality per representative covers
+every basis and every cover.
+
+| Representative | largest 7 difference multiplicities | their sum | edges for <= 2 components | verdict |
+|---|---:|---:|---:|---|
+| 1 | 3,3,3,3,3,3,3 | 21 | 18 | arithmetic bound insufficient |
+| 2 | 3,3,3,3,3,3,3 | 21 | 18 | arithmetic bound insufficient |
+| 3 | 3,3,3,3,3,3,3 | 21 | 18 | arithmetic bound insufficient |
+| 4 | 2,2,2,2,2,2,2 | **14** | 18 | **excluded for every basis, by arithmetic** |
+| 5 | 2,2,2,2,2,2,2 | **14** | 18 | **excluded for every basis, by arithmetic** |
+
+For representatives 1-3 the inequality does not decide the case. The verifier
+therefore reports them as **open**, with two pieces of bounded evidence only:
+the exact component count in the canonical basis is 9, 12 and 4 respectively,
+and over 200 deterministic pseudo-random bases per representative the minimum
+component counts are 6, 5 and 5. No sampled basis produced two components, but
+sampling is not a proof and this package does not claim one.
+
+So the deliverable is: a complete, enumeration-free exclusion of `|P| = 20`
+for two of the five cover classes, a reproducible partial record for the other
+three, and the arithmetic that reduces a simple 22-cycle to exactly two
+multiplicity patterns. This is a **bounded audit**, not a replacement for
+PR #3058's own component/rank argument, which it neither confirms nor refutes
+in the three open classes.
+
+## Word-level search with a positive control
+
+`search_words.py` is a deterministic-seed simulated-annealing search over
+arrangements of a fixed multiset of even label counts, maximising the number of
+masks of `F2^7` realised as `XOR` of a contiguous subword. It is calibrated on
+the one case where a universal word is known to exist.
+
+| Length | multiplicity pattern | best coverage found | word | verdict |
+|---:|---|---:|---|---|
+| 24 | `(6,4,4,4,2,2,2)` | **128/128** | `145164232614626031626540` | universal, restored, `|P| = 24` (positive control) |
+| 22 | `(4,4,4,4,2,2,2)` (pattern B) | 126/128 | `1206231531046325014203` | near miss; masks 82 and 120 unrealised |
+| 22 | `(6,4,4,2,2,2,2)` (pattern A) | 125/128 | `2130240236105010621045` | near miss; masks 50, 73 and 92 unrealised |
+| 22 | unrestricted | 126/128 | (pattern B word) | no universal 22-step word in ~6.2M evaluations |
+
+The 24-step word is a second, independently found universal construction in the
+PR943 model, so the search method is not one-sided; `f(7) <= 24` is therefore
+recertified here by an explicit certificate rather than imported. The 126/128
+pattern-B word is a simple 22-cycle (|P| = 22) with no repeated prefix, so it
+lives in the exact case PR #3058's section 5 claims to exhaust; it is a
+two-mask near miss, which is what an exclusion there would have to survive. The
+search is stochastic: the table records verified words, and a rerun is not
+guaranteed to reproduce the same best coverage.
+
+The two simple-cycle multiplicity patterns `(6,4,4,2,2,2,2)` and
+`(4,4,4,4,2,2,2)` are re-derived in the verifier from the imported projections
+`f(6) = 16` and `f(5) = 12`: deleting one or two source coordinates projects a
+universal word to a universal word on fewer sources, so every multiplicity is
+at most six and every pair sums to at most ten.
+
+## Reproduce
+
+Python 3.12, standard library only, from the repository root:
+
+```sh
+python3 -I -B research/f7-l22-confinement-audit/verify.py
+python3 -B research/f7-l22-confinement-audit/search_words.py --seconds 60
+```
+
+Expected marker from the verifier:
+
+```
+PASS_F7_L22_CONFINEMENT_AUDIT arithmetic_complete=2/5 sampled_only=3 f7_untouched
+```
+
+The verifier runs in well under a second. `search_words.py` is the stochastic
+search of the table above; its default budget is one minute per pattern and it
+prints every verified improvement.
+
+## Open next questions
+
+1. **Do representatives 1-3 admit a basis with three components or fewer?** The
+   counting inequality is short by three edges (21 against 18). `first_step`:
+   search bases that use the three-edge multiplicity classes greedily, and
+   decide the 2-component case for one representative completely.
+   `blocked_by`: the naive independent-subset enumeration did not finish inside
+   this session's budget; a smarter connectivity-only search is needed.
+2. **Is the near-miss pattern-B word two masks short of an impossibility
+   certificate?** `first_step`: run PR #3058's `verify_cycles.py` search on the
+   two masks 82 and 120 and report which structural condition rejects exactly
+   those two.
+   `blocked_by`: it is a 760-line C++ search; this session did not run it.
+3. **Does an unrestricted-multiset 22-step word ever exceed 126/128?**
+   `first_step`: repeat the search with the three-edge classes forced early.
+   `blocked_by`: none; it is a longer stochastic run, not a proof.
+
+## Scope, credit and verification limits
+
+No supplier, tariff, kappa, certificate, frozen input or selected result is
+changed; `certificates/selected-result.json` is untouched.
+
+Credit Ross Richardson for the PR943 prefix-walk model; Alexander Davydov,
+Stefano Marcugini and Fernanda Pambianco for the published covering-code facts
+and the minimal 1-saturating classifications transcribed in
+`research/connector-covering-code/table6.json`; Nicholas Stone for the corrected
+word-census budgets in PR #2973; and the PR #3058 contributor for the `f(7)=24`
+theorem, its component/rank argument and its section 4 multiplicity reduction,
+which this audit re-derives independently rather than assuming. Douglas Colkitt
+for the selected source bindings and review.
+
+This contribution was produced by Nick Petalas with AI assistance. Independent
+human and formal proof-kernel review are unclaimed.
+
+Three obligations are not discharged. The classification of 20-point covers,
+the covering bound `|P| >= 20`, `f(5) = 12`, `f(6) = 16`, the size-21 argument
+and the size-22 simple-cycle exhaustion are **imported**, so nothing here
+re-establishes `f(7) = 24` on its own. Representatives 1-3 carry sampled
+evidence, not proof. And no hosted CI replay or registered-launcher 3.12 run is
+claimed unless the PR records one.

research/f7-l22-confinement-audit/SOURCES.json

@@ -0,0 +1,30 @@
+{
+ "schema_version": 1,
+ "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+ "files": [
+  {
+   "path": "research/connector-covering-code/table6.json",
+   "git_blob": "8670e44048422431efdb2d315535a5d54b492adb",
+   "sha256": "fbf0f123bb6c037ce990c0a527f1aafbb30a70da0a941ac1eec894ea6166f88c",
+   "usage": "input"
+  },
+  {
+   "path": "research/connector-covering-code/README.md",
+   "git_blob": "c194503e34e43988d5f83fec70a6f94e89e3db5d",
+   "sha256": "35252e16e58481df87fc7ac3eb7326bf87e991f9fd8f7e30d14716c16f2152e4",
+   "usage": "provenance"
+  },
+  {
+   "path": "certificates/selected-result.json",
+   "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+   "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129",
+   "usage": "provenance"
+  },
+  {
+   "path": "docs/research/agent-task-catalog.json",
+   "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5",
+   "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0",
+   "usage": "provenance"
+  }
+ ]
+}

research/f7-l22-confinement-audit/TASK.json

@@ -0,0 +1,78 @@
+{
+ "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": "Independently audit one link of the length-22 argument in PR #3058's f(7)=24 theorem: the claim that a 22-step restored seven-source word cannot have exactly 20 distinct prefixes. Re-derive the confinement obstruction as an explicit edge-count inequality on the five classified 20-point minimum covers, run the arithmetic completely for the two representatives where it decides the case, record bounded sampled evidence for the other three, and re-derive the two simple-cycle multiplicity patterns from the imported f(5)=12 and f(6)=16 values. No length-22 word census, no re-proof of f(7)=24, no frontier change.",
+ "scope_change_reason": "The card asks whether a reported census pruning error invalidates a specific exclusion we still rely on and what bounded repair is justified. The predecessor package in this worker slot (research/f7-l22-split-domain, PR #3708) already derived the complete length-22 parity-split domain and handed off three bounded questions. The deciding downstream exclusion is now PR #3058's length-22 exclusion, whose |P|=20 step is the one that carries a set-level confinement claim rather than a census. Auditing that step is the bounded repair of the dependency boundary the card asks for, and it is a different deliverable from #2973's bit-0 prune reconstruction.",
+ "bottleneck_link": "An unsound length-22 exclusion would wrongly close the f(7) question in the PR943 word model. This package narrows the reviewed dependency to two of five cover classes by arithmetic and states precisely which three remain sampled, so a later reader knows where to spend a complete replay.",
+ "budget_minutes": 60,
+ "stop_rule": "Stop after the edge-count derivation, the five-representative arithmetic, the sampled component counts, the multiplicity-pattern re-derivation and the word-level search controls. No complete basis enumeration for representatives 1-3, no PR #3058 replay, no f(7) claim.",
+ "outcome": "completed",
+ "evidence": "python3 -I -B research/f7-l22-confinement-audit/verify.py prints PASS_F7_L22_CONFINEMENT_AUDIT arithmetic_complete=2/5 sampled_only=3 f7_untouched in well under a second on macOS arm64 / CPython 3.12. It rebuilds the twenty-point covers {0} u S from the five 19-point representatives in research/connector-covering-code/table6.json, requires each to satisfy P+P=F2^7, computes the seven largest difference multiplicities (21,21,21,14,14 against the 18 edges a two-component graph on twenty vertices needs), and therefore excludes |P|=20 for every basis in representatives 4 and 5 with no enumeration; representatives 1-3 are reported open with exact canonical-basis component counts 9, 12, 4 and deterministic 200-base sample minima 6, 5, 5. It also re-derives that a simple 22-cycle has exactly the multiplicity patterns (6,4,4,2,2,2,2) and (4,4,4,4,2,2,2) from the imported projections f(6)=16 and f(5)=12, and checks the recorded word artifacts: a universal 24-step word found by the package's own search (145164232614626031626540, 128/128, |P|=24, restored) as a positive control, plus two simple 22-cycles covering 126/128 and 125/128 as non-vacuity controls.",
+ "author": "Nick Petalas",
+ "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+ "open_questions": [
+  {
+   "question": "Do cover representatives 1-3 admit a basis whose confinement graph has at most two components?",
+   "why_it_matters": "A witness would remove the |P|=20 step of PR #3058's length-22 exclusion for that class and reopen a 22-step search route; exhaustion would complete the audit for all five classes.",
+   "first_step": "Search bases that use the three-edge difference classes first and decide the two-component case for representative 3, whose canonical basis already gives only four components.",
+   "blocked_by": "The naive independent-subset enumeration did not finish inside this session's budget; a connectivity-only search is required."
+  },
+  {
+   "question": "Which structural condition rejects exactly the two masks 82 and 120 of the pattern-B near-miss word?",
+   "why_it_matters": "The near miss is two masks from a length-22 universal word, so it is the sharpest available calibration for PR #3058's section 5 exhaustion.",
+   "first_step": "Run research/connector-covering-code/verify_cycles.py on this word and report which pruning rule fires.",
+   "blocked_by": "It is a 760-line C++ search and was not run in this session."
+  },
+  {
+   "question": "Does the restriction to a simple 22-cycle hold without the imported f(5)=12 and f(6)=16 values?",
+   "why_it_matters": "The two multiplicity patterns that section 4 searches depend on those credited values; an independent f(5)=12 or f(6)=16 replay would make the reduction self-contained.",
+   "first_step": "Reproduce f(6)=16 from PR1185's construction and a bounded lower-bound argument.",
+   "blocked_by": "Out of this package's stated budget."
+  }
+ ]
+}

research/f7-l22-confinement-audit/VERIFY.json

@@ -0,0 +1,24 @@
+{
+ "schema_version": 1,
+ "status": "ready",
+ "python": "3.12",
+ "requirements": [],
+ "inputs": [
+  "research/connector-covering-code/table6.json",
+  "research/connector-covering-code/README.md",
+  "certificates/selected-result.json",
+  "docs/research/agent-task-catalog.json"
+ ],
+ "commands": [
+  {
+   "argv": [
+    "{python}",
+    "-I",
+    "-B",
+    "{package}/verify.py"
+   ],
+   "timeout_seconds": 120,
+   "checks": "Rebuilds the five twenty-point covers from table6.json and requires each to satisfy P+P=F2^7; computes the seven largest difference multiplicities and the eighteen-edge bound for a two-component graph on twenty vertices; excludes |P|=20 for every basis in representatives 4 and 5 by arithmetic and records exact and sampled component counts for 1-3; re-derives the two simple-cycle multiplicity patterns at length 22 from the imported f(5) and f(6) values; and verifies the recorded 24-step universal word plus two non-universal 22-step controls with their exact coverage."
+  }
+ ]
+}