diff --git a/research/f7-five-label-independent-audit/README.md b/research/f7-five-label-independent-audit/README.md new file mode 100644 index 0000000000..f16e73c1a5 --- /dev/null +++ b/research/f7-five-label-independent-audit/README.md @@ -0,0 +1,216 @@ +# Independent complete-word audit of the five-label sharp cap + +**No correctness gap found in the stated PR4992 argument.** A separate exact +checker corroborates the sharp excess cap **11** and the exclusion of universal +`(8,4)` splits for simple restored length-twelve singleton walks on `F2^5`. +The result belongs to Ali Romman's [PR #4992](https://github.com/CrocSwap/integer-mult-bounds/pull/4992). +This contribution answers its independent-review handoff with a proof review +and a different complete-domain enumeration; it claims no new bound or kappa. + +Reviewed author head: `12a0105150f5f44a19a2199db8506d1aa44b009a`. The reviewed +README is Git blob `1b80ac21964baf508859127126baac595dc9cdba`, identical at that +head and this package's canonical-main base +`f259dabc7d70e0db8d6d36bfda888f008bbfecc1`. [SOURCES.json](SOURCES.json) pins its +SHA256, the selected record and revision-7 task catalogue as provenance. +No predecessor program is imported by the new checker. The source documents +are not runtime inputs; direct replay is self-contained and needs no Git. + +This is a fresh solo agent/code check of the successor. The submitting account +also authored predecessor #4907; that relationship is disclosed rather than +claiming an independent human review. Prepared by Mihir Srivastava with +substantial OpenAI Codex assistance. No proof-kernel or maintainer acceptance +is asserted; the central review ledger is unchanged. + +## Exact question and definitions + +For labels `w_i` in `{0,1,2,3,4}`, put `q_0=0` and +`q_(i+1)=q_i XOR (1 << w_i)`. The twelve nonclosing states form `S`. +Restoration means `q_12=0`; simplicity means those twelve states are distinct; +universality means `{x XOR y: x,y in S}=F2^5`. +For a nonzero functional mask `f`, split `S` into its two parity classes `A,B`. +Writing `D(C)` for the distinct pair sums of unequal points in `C`, the quantity is + +```text +X_f = choose(|A|,2) + choose(|B|,2) - |D(A)| - |D(B)|. +``` + +Overlapping supports must be subtracted separately. For weight four or five, +the claim is `X_f <= 11`; weight four additionally excludes split `(8,4)`. +This audit checks that exact domain, not partial prefixes or a production prune. + +## Review of the written proof + +The following checks address the logical implications, separately from running +the author's verifier. Symbols below agree with PR4992's README. + +1. **The matching equality is sufficient to force the block cycle.** If `f` + has weight four, its omitted coordinate `v` is the only preserving edge. + Those edges form a matching. From `s-t=a-b`, `2a<=s`, and `2b<=t`, an `(8,4)` + split forces `a=4,b=0,c=8`. Thus every majority vertex has exactly one + preserving edge and one crossing edge. The four distinct majority pairs + occur as `B-A-A-B` blocks. Each block flips the `v` level once, so the four + minority vertices have alternating levels, two at each level. This uses + simplicity and a complete cycle, including the closing edge. + +2. **The complement really is one translation.** Project the majority to the + four-dimensional cube and translate it into the even subspace `E` of size + eight. A four-point projection `T` has three or six nonzero differences. + The three-difference case supplies only `1+2*3=7` lifted differences; + four minority vertices supply at most six, so it cannot cover the fifteen + required kernel differences. In the six-difference case, translate one + point to zero. The other three form a basis of `E`. Their sum `z` is the + unique missing nonzero difference. Therefore `T` and `T+z` partition `E`. + +3. **Universality forces the repeated projection used in the contradiction.** + Both missing majority differences `(z,0)` and `(z,1)` must occur in `D(B)`. + The first uses both minority vertices at one level, with projections `u` + and `w=u+z`. Every cross-level pair uses one of those two vertices. To + obtain difference `(z,1)`, the other level must therefore contain a second + lift of `u` or `w`. Renaming gives the alternating order + `u_0,u_1,w_0,y_1`, up to rotation/reversal. The four distinct block labels + force at least three neighbors of `u` in `T` and at least two of `w`. + The case `y=w` remains covered; no distinctness of all four projections + was assumed. Translation by `z` sends `N(u)` to `N(w)` and `T` to its + complement in `E`. Hence the two neighbor counts sum to exactly four, + contradicting the required five. This closes the nonplanar case too. + +4. **The support classification does not omit a six-point type.** Five to + seven points in affine dimension three occupy more than half their + eight-point affine space, so all seven nonzero differences occur. + In dimension four, an affine basis is `{0,e1,e2,e3,e4}`. An added point + of weight two or three yields twelve differences; one of weight four + yields fifteen. For the weight-three case, translate by `e1`: use basis + `{e1,e1+e2,e1+e3,e1+e4}`. The extra point `e2+e3` is the sum of the middle + two basis vectors, so this is indeed the weight-two normal form. + Thus the stated `C6={0,1,2,3,4,8}` case and the fifteen-difference case + exhaust the possibilities. Each possible seventh point in the displayed + table adds a difference outside `1,...,12`, establishing at least thirteen. + +5. **Both final class splits have the claimed bound.** For `(6,6)`, both + supports cannot have size seven because their union must have size fifteen; + one therefore has size at least twelve. The bound is `30-7-12=11`. + For `(7,5)`, if the seven-point class had affine dimension three with + direction `H`, the other class would have to supply all eight differences + outside `H`. Five points split into the two `H` cosets have only + `k(5-k)<=6` cross-coset pairs. Thus its seven-point partner has dimension + four and support at least thirteen, giving `31-13-7=11`. The explicit + witnesses attain eleven. Coordinate permutations cover every weight-four + mask, and weight five is the alternating `(6,6)` case. + +No larger-dimensional, other-length, partial-prefix or arbitrary-point-set +claim is inferred from these steps. + +## Different complete-domain oracle + +The new `verify.py` does not traverse a pruned cube-path tree. Restoration +forces every label multiplicity to be even; universality forces all five +labels to appear. With twelve positions, the multiplicities are necessarily +`(4,2,2,2,2)`. Normalize the unique four-occurrence label to zero. + +Choose its four positions in `choose(12,4)=495` ways. Partition the remaining +eight positions into unordered pairs: there are `8!/(2^4*4!)=105` perfect +matchings. Give the four pairs labels one through four in order of their +smallest positions. This has exactly one representative per coordinate-label +permutation orbit. All six high-weight masks are checked, so the normalization +does not discard a functional. Neither rotations nor reversals are quotiented. +Every required word is represented; absent-label words cannot be universal. + +All **51,975** candidates are generated before any geometric filtering. Only +literal simplicity and the full 32-element pair-sum test select the universal +domain. No excess threshold, class split, support bound, matching balance, +Hamiltonian search or quotient argument prunes candidate generation. +The split and cap are checked as conclusions on every admitted word. + +| Stage | Exact count | +|---|---:| +| Coordinate-normalized multiplicity words | 51,975 | +| Nonsimple words | 48,594 | +| Simple words | 3,381 | +| Simple but nonuniversal words | 2,553 | +| Universal words | 828 | +| Universal word / high-weight functional pairs | 4,968 | +| Weight-four cases attaining eleven | 444 | +| Weight-five cases attaining eleven | 36 | +| Universal `(8,4)` cases | 0 | + +The complete histograms agree with #4907's previously measured census. Those +counts and the bound are prior results, not new discoveries. The additional +evidence is an implementation using positions/perfect matchings, its domain +completeness argument, and the explicit review above. [RESULT.json](RESULT.json) +retains the histogram and SHA256 digests of both sorted candidate lists +(ASCII words separated by LF, including the final LF). + +Controls check both literal sharp witnesses, 64 translated starts, 48 rotated +or reversed witnesses, and reject cap ten, invalid lengths/labels, a nonrestored +word, a nonsimple word and a low-weight mask. The simple restored word +`012013024034` has an `(8,4)` split at mask 30 but is not universal: it is +retained as a discriminating boundary case. Merging the two class supports +would give fifteen rather than eleven on the weight-five witness. +`mutations.py` rejects eight actual code changes, under `-O` and with stored +receipt comparison disabled; it also runs an unmodified positive control. + +## Reproduction and evidence + +From the repository root, with CPython 3.12 and no third-party dependencies: + +```sh +python3.12 -B scripts/research_package.py --package research/f7-five-label-independent-audit +python3.12 -I -O -W error -B research/f7-five-label-independent-audit/verify.py +``` + +The registered replay checks normal and optimized modes plus all eight mutations. +Direct `--emit-receipt` prints the recomputed result for inspection; ordinary +replay compares it exactly with `RESULT.json` and writes no package files. +The complete registered replay is expected to take under ten seconds locally. + +On Windows 11 / CPython 3.12.0, the predecessor's own registered normal/optimized +replay also passed: 23,816 support sets, 127,400 invariant-majority set pairs +and 13,664 universal graphs. This is additional replay evidence, distinct from +the new algorithm. Source equality was checked against both canonical main +and the exact public author head. The optional full-history preflight is not +claimed in this shallow partial clone. The package pins only its main ancestor; +the author's separate fetched commit is not a runtime or provenance dependency. + +## Coordination, limits and credit + +The [canonical investigation](https://github.com/CrocSwap/integer-mult-bounds/discussions/4903#discussioncomment-19140259) +takes the independent-review part of the +[handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19138920). +Entry overlap covered 323 open PRs and 4,134 Discussion records with complete +remote pagination at 2026-10-23 07:04 UTC. Initial local coverage was 7 of +6,710 note records, followed by direct reads/materialization of the relevant +f7 predecessors and successor. Omitted notes, arbitrary diffs and unpublished +work remain limits. [TASK.json](TASK.json) records the changed card scope. + +Submission refresh at 07:16 UTC retained the same main and guidance and covered +329 open PRs and 4,150 Discussion records. It found a concurrent +[six-plus-six path-join audit](https://github.com/CrocSwap/integer-mult-bounds/discussions/4903#discussioncomment-19140301) +under the same account. This package retains the already completed, different +position/perfect-matching method. The concurrent audit is acknowledged, not +treated as absent; neither claims the predecessor's cap or census as new. +The local refresh searched 47 records with 6,665 tracked notes omitted. + +No maintained engine, seven-label census, supplier admission, selected cold +replay or complete multiplication theorem was checked. The selected exponent +remains `60403/20000000`. This audit does not promote an archive into a selected +result or modify its recorded scientific acceptance status. + +Credit Ali Romman for #4992's sharp proof; Mihir Srivastava for +[#4907](https://github.com/CrocSwap/integer-mult-bounds/pull/4907)'s cap-15 proof, +measured sharp cap and handoff; Nick Petalas for +[#4894](https://github.com/CrocSwap/integer-mult-bounds/pull/4894)'s matching +balance; unpaidmoon for [#4148](https://github.com/CrocSwap/integer-mult-bounds/pull/4148); +Nicholas Stone for [#2973](https://github.com/CrocSwap/integer-mult-bounds/pull/2973); +James Reed for [#3096](https://github.com/CrocSwap/integer-mult-bounds/pull/3096); +and Ross Richardson for [#943](https://github.com/CrocSwap/integer-mult-bounds/pull/943). +New code and review are Apache-2.0; predecessor files and notices are unchanged. + +## Open next questions + +The complete-walk proof does not supply a partial-prefix runtime improvement. +Ali Romman's #5001 supplies a separate completion condition, and JoyboyBrian +has already [claimed its maintained-engine integration](https://github.com/CrocSwap/integer-mult-bounds/discussions/4903#discussioncomment-19139518). +The next useful check is exact equality of the implementation's prune-off/on +leaf multisets, followed by measured runtime. Follow that existing claim; +this audit neither duplicates nor reserves it. An independent human or formal +proof-kernel review of the written sharp-cap argument also remains welcome. diff --git a/research/f7-five-label-independent-audit/RESULT.json b/research/f7-five-label-independent-audit/RESULT.json new file mode 100644 index 0000000000..fb8759d65e --- /dev/null +++ b/research/f7-five-label-independent-audit/RESULT.json @@ -0,0 +1,47 @@ +{ + "candidates_sha256": "28f12826f3487f2ac715db0ee97e03282590b4a8ce07745552a2ff5ae932cbb7", + "controls": [ + "translation_checks=64", + "dihedral_checks=48", + "cap_ten", + "wrong_length", + "out_of_range_label", + "negative_label", + "nonintegral_label", + "not_restored", + "nonsimple", + "low_weight", + "nonuniversal_84", + "merged_supports_distinguished" + ], + "counts": { + "candidates": 51975, + "nonsimple": 48594, + "simple": 3381, + "simple_nonuniversal": 2553, + "universal": 828 + }, + "histograms": { + "4": { + "6,6:X=11": 132, + "6,6:X=3": 432, + "6,6:X=6": 1392, + "6,6:X=8": 96, + "7,5:X=11": 312, + "7,5:X=6": 528, + "7,5:X=8": 816, + "7,5:X=9": 432 + }, + "5": { + "6,6:X=11": 36, + "6,6:X=3": 192, + "6,6:X=6": 552, + "6,6:X=8": 48 + } + }, + "nonuniversal_84": { + "mask": 30, + "word": "012013024034" + }, + "universal_words_sha256": "297ea97dcc78952379d84054e19e01fd3280bfdab7669855dd382accca827984" +} diff --git a/research/f7-five-label-independent-audit/SOURCES.json b/research/f7-five-label-independent-audit/SOURCES.json new file mode 100644 index 0000000000..6055848d27 --- /dev/null +++ b/research/f7-five-label-independent-audit/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "f259dabc7d70e0db8d6d36bfda888f008bbfecc1", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/f7-five-label-sharp-cap/README.md", + "usage": "provenance", + "git_blob": "1b80ac21964baf508859127126baac595dc9cdba", + "sha256": "c03f524035f4abeb9103e7e43486ee75b83538e41abb50cd3beaecd01119f871" + } + ] +} diff --git a/research/f7-five-label-independent-audit/TASK.json b/research/f7-five-label-independent-audit/TASK.json new file mode 100644 index 0000000000..91126ad6a7 --- /dev/null +++ b/research/f7-five-label-independent-audit/TASK.json @@ -0,0 +1,87 @@ +{ + "schema_version": 1, + "task_id": "census-pruning-audit", + "priority_revision": 7, + "base_commit": "f259dabc7d70e0db8d6d36bfda888f008bbfecc1", + "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": "changed", + "actual_scope": "Independent review of PR4992 sharp high-weight cap and (8,4) exclusion, using a complete multiplicity-word oracle with no geometric or excess pruning.", + "scope_change_reason": "Take the independent-review part of the PR4992 handoff in Discussion1166 comment19138920. The maintained-engine integration of PR5001 is a separate active claim.", + "bottleneck_link": "A scoped audit of a pruning premise; independent corroboration is requested by the archive-only review ledger. No supplier or exponent improvement is claimed.", + "budget_minutes": 60, + "stop_rule": "Stop after proof review, complete five-label length-twelve checks, semantic controls and a focused publication. No larger census or engine integration.", + "outcome": "completed", + "evidence": "Proof review finds no correctness gap in the stated scope. Position/perfect-matching enumeration checks all 51975 coordinate-normalized words, 3381 simple walks, 828 universal walks and 4968 functionals; exact cap11 and no universal (8,4). Twelve control groups and eight semantic mutations.", + "author": "Mihir Srivastava", + "ai_assistance": "Substantial OpenAI Codex assistance for proof review, independent code, verification and publication. A fresh solo agent/code check of Ali Romman's successor; not independent human or proof-kernel acceptance. The account also authored predecessor PR4907.", + "open_questions": [ + { + "question": "Does the separately claimed PR5001 maintained-engine integration preserve the complete leaf multiset and improve runtime?", + "why_it_matters": "A proved complete-walk bound does not by itself justify a partial-prefix prune or a runtime claim.", + "first_step": "Follow the existing Discussion4903 comment19139518; compare pruning off/on against the same complete small-domain leaf oracle when its implementation is published.", + "blocked_by": "This audit does not inspect or reserve the ongoing maintained-engine implementation." + } + ], + "canonical_discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4903#discussioncomment-19140259", + "selection": { + "mode": "handoff-first", + "source_pr": 4992, + "source_head": "12a0105150f5f44a19a2199db8506d1aa44b009a", + "priority_revision": 7 + }, + "environment": { + "python": "3.12.0", + "platform": "Windows 11", + "dependencies": "standard library only" + }, + "unrun_obligations": [ + "Independent human review", + "Formal proof-kernel verification", + "Maintained-engine integration", + "Seven-label census", + "Supplier admission", + "Selected cold replay", + "Optional full-history source preflight" + ] +} diff --git a/research/f7-five-label-independent-audit/VERIFY.json b/research/f7-five-label-independent-audit/VERIFY.json new file mode 100644 index 0000000000..94508e5252 --- /dev/null +++ b/research/f7-five-label-independent-audit/VERIFY.json @@ -0,0 +1,46 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Complete position/matching domain, literal walk and pair-sum checks, sharpness, controls, and exact receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Identical exact checks with assertions disabled." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/mutations.py" + ], + "timeout_seconds": 120, + "checks": "A positive emitted-receipt replay and eight semantically rejected code mutations, without stored-receipt comparison." + } + ] +} diff --git a/research/f7-five-label-independent-audit/mutations.py b/research/f7-five-label-independent-audit/mutations.py new file mode 100644 index 0000000000..66c2d20c92 --- /dev/null +++ b/research/f7-five-label-independent-audit/mutations.py @@ -0,0 +1,48 @@ +#!/usr/bin/env python3 +"""Reject semantic mutations without relying on the stored receipt or hashes. + +Mihir Srivastava, with substantial OpenAI Codex assistance. Apache-2.0. +""" +from pathlib import Path +import subprocess +import sys +import tempfile + + +def main(): + source = (Path(__file__).resolve().parent / "verify.py").read_text(encoding="utf-8") + mutations = { + "missing_position": ("combinations(range(12), 4)", "combinations(range(11), 4)"), + "missing_pairings": ("enumerate(rest):", "enumerate(rest[:1]):"), + "early_simple_filter_removed": ("if len(set(points)) != 12:", "if False:"), + "universality_as_cardinality": ( + "return {x ^ y for x in points for y in points} == set(range(32))", + "return len(set(points)) == 12"), + "merged_class_supports": ( + "sum(comb(n, 2) for n in sizes) - sum(supports)", + "sum(comb(n, 2) for n in sizes) - len(support(classes[0]) | support(classes[1]))"), + "cap_ten": ("def check_target(word, mask=31, cap=11):", "def check_target(word, mask=31, cap=10):"), + "low_weight_admitted": ("require(mask in MASKS, \"weight\")", "require(0 < mask < 32, \"weight\")"), + "class_zero_only": ("for parity in (0, 1)]", "for parity in (0, 0)]"), + } + with tempfile.TemporaryDirectory(prefix="five-label-audit-") as directory: + path = Path(directory) / "verify.py" + # Both positive and negative runs use --emit-receipt, bypassing RESULT. + path.write_text(source, encoding="utf-8", newline="\n") + command = [sys.executable, "-I", "-O", "-W", "error", "-B", str(path), "--emit-receipt"] + baseline = subprocess.run(command, capture_output=True, timeout=30) + if baseline.returncode: + raise ValueError("positive control failed: " + baseline.stderr.decode(errors="replace")) + for name, (old, new) in mutations.items(): + if source.count(old) != 1: + raise ValueError("mutation target is not unique: " + name) + path.write_text(source.replace(old, new), encoding="utf-8", newline="\n") + result = subprocess.run(command, capture_output=True, timeout=30) + if result.returncode == 0 or b"ValueError:" not in result.stderr: + raise ValueError("mutation was not semantically rejected: " + name) + print("REJECTED", name, result.stderr.decode(errors="replace").splitlines()[-1]) + print("PASS_F7_INDEPENDENT_MUTATIONS count=8 receipt_comparison=disabled") + + +if __name__ == "__main__": + main() diff --git a/research/f7-five-label-independent-audit/verify.py b/research/f7-five-label-independent-audit/verify.py new file mode 100644 index 0000000000..688d55c47a --- /dev/null +++ b/research/f7-five-label-independent-audit/verify.py @@ -0,0 +1,194 @@ +#!/usr/bin/env python3 +"""Complete-word audit of PR4992; no predecessor code imports. + +Mihir Srivastava, with substantial OpenAI Codex assistance. Apache-2.0. +Candidates are generated from positions and perfect matchings, not cube walks. +""" +from collections import Counter +from hashlib import sha256 +from itertools import combinations +from math import comb, factorial +from pathlib import Path +import argparse +import json + +HERE = Path(__file__).resolve().parent +MASKS = (15, 23, 27, 29, 30, 31) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def matchings(items): + """Every perfect matching once, paired by its smallest unused position.""" + if not items: + yield () + return + first, rest = items[0], items[1:] + for index, partner in enumerate(rest): + for tail in matchings(rest[:index] + rest[index + 1:]): + yield ((first, partner),) + tail + + +def candidates(): + """One representative per coordinate-permutation orbit, before tests.""" + for repeated in combinations(range(12), 4): + remaining = tuple(p for p in range(12) if p not in repeated) + for pairs in matchings(remaining): + word = [0] * 12 + for label, pair in enumerate(pairs, start=1): + for position in pair: + word[position] = label + yield tuple(word) + + +def prefixes(word): + require(len(word) == 12, "length") + require(all(type(label) is int and 0 <= label < 5 for label in word), "label") + point, states = 0, [] + for label in word: + states.append(point) + point ^= 1 << label + require(point == 0, "restoration") + return states + + +def support(points): + return {x ^ y for x, y in combinations(points, 2)} + + +def universal(points): + # Count ordered pair sums, including zero; no span surrogate. + return {x ^ y for x in points for y in points} == set(range(32)) + + +def measure(points, mask): + classes = [[x for x in points if (x & mask).bit_count() % 2 == parity] + for parity in (0, 1)] + sizes = [len(part) for part in classes] + supports = [len(support(part)) for part in classes] + return (tuple(sorted(sizes, reverse=True)), tuple(supports), + sum(comb(n, 2) for n in sizes) - sum(supports)) + + +def check_target(word, mask=31, cap=11): + require(mask in MASKS, "weight") + points = prefixes(word) + require(len(set(points)) == 12, "simplicity") + require(universal(points), "universality") + split, sizes, excess = measure(points, mask) + require(split in ((6, 6), (7, 5)), "split") + require(excess <= cap, "cap") + return split, sizes, excess + + +def audit(): + counts, histograms = Counter(), {4: Counter(), 5: Counter()} + all_words, universal_words, boundary = set(), [], None + for word in candidates(): + require(word not in all_words, "duplicate candidate") + all_words.add(word) + counts["candidates"] += 1 + require(tuple(word.count(i) for i in range(5)) == (4, 2, 2, 2, 2), "multiplicity") + points = prefixes(word) + if len(set(points)) != 12: + counts["nonsimple"] += 1 + continue + counts["simple"] += 1 + if not universal(points): + counts["simple_nonuniversal"] += 1 + if boundary is None: + for mask in MASKS[:-1]: + if measure(points, mask)[0] == (8, 4): + boundary = {"word": "".join(map(str, word)), "mask": mask} + break + continue + counts["universal"] += 1 + universal_words.append("".join(map(str, word))) + for mask in MASKS: + split, sizes, excess = check_target(word, mask) + histograms[mask.bit_count()][f"{split[0]},{split[1]}:X={excess}"] += 1 + even = [x for x in points if (x & mask).bit_count() % 2 == 0] + odd = [x for x in points if (x & mask).bit_count() % 2 == 1] + require(len(support(even) | support(odd)) == 15, "kernel coverage") + require(sum(sizes) >= 19, "separate supports") + expected_count = comb(12, 4) * factorial(8) // (2**4 * factorial(4)) + require(counts["candidates"] == expected_count == 51975, "domain count") + require(counts["simple"] + counts["nonsimple"] == expected_count, "partition") + require(boundary is not None, "missing nonuniversal boundary fixture") + for weight in (4, 5): + require(max(int(k.split("=")[1]) for k in histograms[weight]) == 11, "sharpness") + return { + "counts": dict(sorted(counts.items())), + "histograms": {str(w): dict(sorted(h.items())) for w, h in histograms.items()}, + "candidates_sha256": sha256(("\n".join(sorted("".join(map(str, w)) for w in all_words)) + "\n").encode()).hexdigest(), + "universal_words_sha256": sha256(("\n".join(sorted(universal_words)) + "\n").encode()).hexdigest(), + "nonuniversal_84": boundary, + "controls": controls(boundary), + } + + +def controls(boundary): + results = [] + + def reject(name, call, reason): + try: + call() + except ValueError as exc: + require(str(exc) == reason, f"wrong rejection for {name}: {exc}") + else: + raise ValueError(f"accepted negative control: {name}") + results.append(name) + + witness4 = tuple(map(int, "012343234031")) + witness5 = tuple(map(int, "012343103432")) + require(check_target(witness4, 23) == ((7, 5), (7, 13), 11), "literal weight-four witness") + require(check_target(witness5, 31) == ((6, 6), (7, 12), 11), "literal weight-five witness") + for witness, mask in ((witness4, 23), (witness5, 31)): + original = measure(prefixes(witness), mask) + for shift in range(32): + shifted = [point ^ shift for point in prefixes(witness)] + current = measure(shifted, mask) + require(current[0] == original[0] and sorted(current[1]) == sorted(original[1]) + and current[2] == original[2] and universal(shifted), "translation") + for offset in range(12): + rotated = witness[offset:] + witness[:offset] + for orientation in (rotated, rotated[::-1]): + require(check_target(orientation, mask)[2] == 11, "dihedral witness") + results.extend(["translation_checks=64", "dihedral_checks=48"]) + reject("cap_ten", lambda: check_target(witness5, 31, 10), "cap") + reject("wrong_length", lambda: check_target(witness5[:-1]), "length") + reject("out_of_range_label", lambda: check_target((5,) + witness5[1:]), "label") + reject("negative_label", lambda: check_target((-1,) + witness5[1:]), "label") + reject("nonintegral_label", lambda: check_target((0.0,) + witness5[1:]), "label") + reject("not_restored", lambda: check_target(witness5[:-1] + (0,)), "restoration") + reject("nonsimple", lambda: check_target(tuple(map(int, "000011223344"))), "simplicity") + reject("low_weight", lambda: check_target(witness5, 7), "weight") + boundary_word = tuple(map(int, boundary["word"])) + require(measure(prefixes(boundary_word), boundary["mask"])[0] == (8, 4), "boundary split") + reject("nonuniversal_84", lambda: check_target(boundary_word, boundary["mask"]), "universality") + require(2 * comb(6, 2) - 15 == 15 and measure(prefixes(witness5), 31)[2] == 11, + "merged-support discriminant") + results.append("merged_supports_distinguished") + return results + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit-receipt", action="store_true") + args = parser.parse_args() + receipt = audit() + if args.emit_receipt: + print(json.dumps(receipt, indent=2, sort_keys=True)) + else: + expected = json.loads((HERE / "RESULT.json").read_text(encoding="utf-8")) + require(receipt == expected, "receipt mismatch") + print("PASS_F7_FIVE_LABEL_INDEPENDENT_AUDIT " + f"candidates={receipt['counts']['candidates']} " + f"universal={receipt['counts']['universal']} cap=11") + + +if __name__ == "__main__": + main()