diff --git a/research/f7-l22-confinement-audit/README.md b/research/f7-l22-confinement-audit/README.md new file mode 100644 index 0000000000..f90b6cd79c --- /dev/null +++ b/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. diff --git a/research/f7-l22-confinement-audit/SOURCES.json b/research/f7-l22-confinement-audit/SOURCES.json new file mode 100644 index 0000000000..9b116159a4 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/f7-l22-confinement-audit/TASK.json b/research/f7-l22-confinement-audit/TASK.json new file mode 100644 index 0000000000..ffee137ed9 --- /dev/null +++ b/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." + } + ] +} diff --git a/research/f7-l22-confinement-audit/VERIFY.json b/research/f7-l22-confinement-audit/VERIFY.json new file mode 100644 index 0000000000..9b81670728 --- /dev/null +++ b/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." + } + ] +} diff --git a/research/f7-l22-confinement-audit/search_words.py b/research/f7-l22-confinement-audit/search_words.py new file mode 100644 index 0000000000..b9a3d5d082 --- /dev/null +++ b/research/f7-l22-confinement-audit/search_words.py @@ -0,0 +1,94 @@ +#!/usr/bin/env python3 +"""Stochastic word-level search in the PR943 singleton prefix-walk model. + +Fixed multiset of positive even label counts; moves are transpositions; +objective is the number of masks of F2^n realised as XOR of a contiguous +subword, i.e. |P + P|. The search is a heuristic: it certifies nothing it does +not print, and a rerun need not reproduce the same best coverage. Its purpose +in this package is the positive control at length 24, where a universal word is +known to exist. +""" + +import argparse +import sys +from itertools import combinations_with_replacement + +N = 7 +FULL = (1 << N) - 1 + + +def coverage(digits): + q = 0 + states = [0] + for d in digits: + q ^= 1 << d + states.append(q) + return len({a ^ b for a in states for b in states}) + + +class Lcg: + def __init__(self, seed): + self.s = seed & ((1 << 64) - 1) + + def next(self): + self.s = (self.s * 6364136223846793005 + 1442695040888963407) & ((1 << 64) - 1) + return self.s >> 16 + + def randrange(self, n): + return self.next() % n + + +def search(counts, seconds, seed, report=print): + import time + rng = Lcg(seed) + length = sum(counts) + best, bestw = -1, None + deadline = time.time() + seconds + runs = 0 + while time.time() < deadline: + runs += 1 + word = [] + for i, c in enumerate(counts): + word += [i] * c + for i in range(length - 1, 0, -1): + j = rng.randrange(i + 1) + word[i], word[j] = word[j], word[i] + cur = coverage(word) + stall = 0 + while stall < 4000 and time.time() < deadline: + i, j = rng.randrange(length), rng.randrange(length) + if i == j: + continue + word[i], word[j] = word[j], word[i] + new = coverage(word) + if new >= cur: + if new > cur: + cur, stall = new, 0 + else: + stall += 1 + if new > best: + best, bestw = new, list(word) + report(f"best={new} word={''.join(map(str, word))}") + else: + word[i], word[j] = word[j], word[i] + stall += 1 + return best, bestw, runs + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument("--seconds", type=float, default=60.0, help="budget per pattern") + ap.add_argument("--length", type=int, default=24, choices=(18, 20, 22, 24)) + ap.add_argument("--seed", type=int, default=20261018) + args = ap.parse_args() + patterns = [c for c in combinations_with_replacement(range(2, args.length + 1, 2), N) + if sum(c) == args.length] + print(f"length {args.length}: {len(patterns)} multiplicity patterns") + for k, counts in enumerate(patterns): + best, word, runs = search(list(counts), args.seconds, args.seed + k) + print(f"pattern {counts}: best={best}/128 restarts={runs} " + f"word={''.join(map(str, word)) if word else None}", flush=True) + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/research/f7-l22-confinement-audit/verify.py b/research/f7-l22-confinement-audit/verify.py new file mode 100644 index 0000000000..7e306e19d4 --- /dev/null +++ b/research/f7-l22-confinement-audit/verify.py @@ -0,0 +1,246 @@ +#!/usr/bin/env python3 +"""Independent audit of the 20-prefix confinement step in the f(7)=24 chain. + +Scope. PR #3058 (research/connector-covering-code) proves f(7)=24 in the +PR943 singleton prefix-walk model. Its length-22 argument needs three steps +for a 22-step word: |P| >= 20 (covering bound, imported), |P| = 20 impossible, +|P| = 21 impossible (its section 3), |P| = 22 impossible (its sections 4-5). +This verifier re-checks ONE of those steps with its own code: no 22-step word +can have exactly twenty distinct prefixes. + +Argument re-derived here. If |P| = 20 then every position of the walk lies in +the twenty-point set T = P, so the walk is a closed walk spanning T; the graph +G(T, D) induced on T by the walk's seven directions D must then be connected. +Directions come from a basis D of F2^7, and for a basis D the edge set of +G(T, D) is contained in the union of at most seven difference classes +diff(T) = {x XOR y : x, y in T}, one per basis vector. So + + edges(G(T, D)) <= sum of the seven largest difference multiplicities, + +and a graph on twenty vertices with at most two components needs at least +eighteen edges. When the seven largest multiplicities sum below eighteen, +G(T, D) has at least three components for EVERY basis D, with no enumeration. + +Every 20-point cover is an affine image of {0} u S for one of the five +19-point representatives in table6.json (imported classification), and +G(M T + b, D) = G(T, M^-1 D), so the check over all bases covers every cover. + +What this verifier does NOT do: it does not re-prove the classification it +imports, it does not exclude |P| = 21 or |P| = 22, and it does not re-prove +f(7) = 24. For the three representatives where the arithmetic bound is weaker +than eighteen edges it reports a sampled component count and marks the case +open, rather than claiming an exclusion. + +Standard library only. Deterministic: the sampling uses a fixed seed. +""" + +import hashlib +import json +import sys +from itertools import combinations, combinations_with_replacement +from pathlib import Path + +N = 7 +FULL = (1 << N) - 1 +ROOT = Path(__file__).resolve().parents[2] +TABLE6 = ROOT / "research/connector-covering-code/table6.json" + +# Recorded word-level artifacts from the documented search runs in this +# package's SEARCH.md (stochastic search, positive control included). +W24 = "145164232614626031626540" +W22_B = "1206231531046325014203" +W22_A = "2130240236105010621045" + +# Imported constants (credited, not re-proved here). +F5, F6 = 12, 16 + + +def sha256_file(path): + return hashlib.sha256(Path(path).read_bytes()).hexdigest() + + +def prefix_states(word): + q = 0 + states = [0] + for w in word: + q ^= 1 << w + states.append(q) + return states + + +def pair_sums(points): + return {a ^ b for a in points for b in points} + + +def is_universal_word(digits, n=N): + """A restored word is universal iff its prefix set P satisfies P+P=F2^n.""" + if len(digits) % 2: + return False, "odd_length" + if not all(0 <= d < n for d in digits): + return False, "label_out_of_range" + states = prefix_states(digits) + if states[-1] != 0: + return False, "not_restored" + counts = [0] * n + for d in digits: + counts[d] += 1 + if any(c == 0 or c % 2 for c in counts): + return False, "usage_not_positive_even" + return len(pair_sums(set(states))) == (1 << n), "ok" + + +def components(points, dirs): + pts = sorted(points) + idx = {p: i for i, p in enumerate(pts)} + parent = list(range(len(pts))) + + def find(x): + while parent[x] != x: + parent[x] = parent[parent[x]] + x = parent[x] + return x + + for d in dirs: + for p in pts: + j = idx.get(p ^ d) + if j is not None and idx[p] < j: + a, b = find(idx[p]), find(j) + if a != b: + parent[a] = b + return len({find(i) for i in range(len(pts))}) + + +def difference_histogram(points): + hist = {} + for a, b in combinations(sorted(points), 2): + hist[a ^ b] = hist.get(a ^ b, 0) + 1 + hist.pop(0, None) + return hist + + +class Lcg: + """Small deterministic generator: no dependence on CPython's RNG stream.""" + + def __init__(self, seed): + self.s = seed & ((1 << 64) - 1) + + def next(self): + self.s = (self.s * 6364136223846793005 + 1442695040888963407) & ((1 << 64) - 1) + return self.s >> 16 + + def randrange(self, n): + return self.next() % n + + def basis(self): + cols, span = [], {0} + while len(cols) < N: + v = 1 + self.randrange(FULL) + if v not in span: + span |= {s ^ v for s in span} + cols.append(v) + return cols + + +def main(): + failures = [] + notes = [] + + def check(name, ok, detail=""): + print(("PASS " if ok else "FAIL ") + name + (" :: " + detail if detail else "")) + if not ok: + failures.append(name) + + check("input_table6_present", TABLE6.is_file(), sha256_file(TABLE6) if TABLE6.is_file() else "missing") + data = json.loads(TABLE6.read_text()) + reps = data["representatives"] + check("five_representatives", len(reps) == 5, str([r["id"] for r in reps])) + + # ---- coverage oracle controls ------------------------------------------- + d24 = [int(c) for c in W24] + ok, why = is_universal_word(d24) + check("positive_control_w24_universal", ok, why) + check("positive_control_w24_length", len(d24) == 24, str(len(d24))) + d22b = [int(c) for c in W22_B] + okb, whyb = is_universal_word(d22b) + check("non_vacuity_w22_not_universal", (not okb) and whyb == "ok", whyb) + covered = len(pair_sums(set(prefix_states(d22b)))) + check("non_vacuity_w22_coverage", covered == 126, f"covered={covered}/128") + d22a = [int(c) for c in W22_A] + oka, whya = is_universal_word(d22a) + covered_a = len(pair_sums(set(prefix_states(d22a)))) + check("non_vacuity_w22_pattern_a", (not oka) and covered_a == 125, f"covered={covered_a}/128") + check("mutant_w24_breaks", not is_universal_word([0] + d24[1:])[0], "prepended label") + check("small_connected_control", components({0, 1, 2, 3, 4, 5, 6, 7}, + [1 << i for i in range(N)]) <= 2, + "routine can see near-connectivity") + + # ---- confinement arithmetic -------------------------------------------- + open_reps, excluded_reps = [], [] + lcg = Lcg(20261018) + results = {} + for r in reps: + T = sorted({0} | set(r["columns"])) + check(f"rep{r['id']}_twenty_points", len(T) == 20, str(len(T))) + check(f"rep{r['id']}_covers", len(pair_sums(T)) == 1 << N, "P+P=F2^7") + hist = difference_histogram(T) + top7 = sorted(hist.values(), reverse=True)[:7] + need = len(T) - 2 # edges needed for at most two components + bound_excludes = sum(top7) < need + std = components(T, [1 << i for i in range(N)]) + samples = [] + for _ in range(200): + samples.append(components(T, lcg.basis())) + results[str(r["id"])] = { + "distinct_differences": len(hist), + "top7_multiplicity_sum": sum(top7), + "edges_needed_for_two_components": need, + "arithmetic_excludes_two_components": bound_excludes, + "components_standard_basis": std, + "components_min_over_200_sampled_bases": min(samples), + } + check(f"rep{r['id']}_standard_basis_ge3", std >= 3, f"components={std}") + check(f"rep{r['id']}_sampled_bases_ge3", min(samples) >= 3, + f"min over 200 bases={min(samples)}") + if bound_excludes: + excluded_reps.append(r["id"]) + else: + open_reps.append(r["id"]) + + complete = all(results[str(i)]["arithmetic_excludes_two_components"] for i in excluded_reps) + notes.append(f"arithmetic exclusion complete for representatives {excluded_reps}") + notes.append(f"remaining representatives {open_reps} carry sampled evidence only") + + # ---- simple-cycle multiplicity arithmetic ------------------------------ + patterns = [] + for counts in combinations_with_replacement(range(2, 23, 2), 7): + if sum(counts) != 22: + continue + if max(counts) > 22 - F6: + continue + if any(a + b > 22 - F5 for a, b in combinations(counts, 2)): + continue + patterns.append(tuple(sorted(counts, reverse=True))) + check("l22_simple_cycle_patterns", patterns == [(6, 4, 4, 2, 2, 2, 2), (4, 4, 4, 4, 2, 2, 2)], + str(patterns)) + + report = { + "checked": "20-prefix confinement arithmetic for 20-point covers", + "representatives": results, + "arithmetic_excluded_representatives": excluded_reps, + "sampled_only_representatives": open_reps, + "l22_simple_cycle_multiplicity_patterns": patterns, + "word_artifacts": {"universal_24_word": W24, "best_22_pattern_a": W22_A, + "best_22_pattern_b": W22_B}, + } + print(json.dumps(report, indent=1, sort_keys=True)) + if failures: + print("FAILED_CHECKS " + ",".join(failures)) + return 1 + print("PASS_F7_L22_CONFINEMENT_AUDIT " + f"arithmetic_complete={len(excluded_reps)}/5 sampled_only={len(open_reps)} " + f"f7_untouched") + return 0 + + +if __name__ == "__main__": + sys.exit(main())