From 88dda3534071442773106e9c0b941b9d39a3cea8 Mon Sep 17 00:00:00 2001 From: Nicholas Stone Date: Fri, 16 Oct 2026 01:31:52 +0800 Subject: [PATCH] Independent audit of PR2634 census + completion of the (10,10) exclusion at L=20 Independently written C engine reproduces all 11 completed shard counts exactly (incl. heavy shard 0102: 798,901,031 nodes / 67,674,177 cycles / 0 hits) and 5M-node capped probes on four prefixes. The four remaining shards 0120-0123 complete the resumable simple-20-cycle census: 6,305,209,079 nodes, 597,148,314 simple 20-cycles, zero universal words. Scoped finite exclusion inside the PR943 model; gap 20 <= f(7) <= 24 unchanged; no kappa, supplier or selected-frontier change. --- .../AUDIT-RESULT.json | 71 ++++++++ .../README.md | 136 +++++++++++++++ .../SOURCES.json | 44 +++++ .../TASK.json | 100 +++++++++++ .../VERIFY.json | 20 +++ .../f7_census.c | 160 ++++++++++++++++++ .../verify.py | 108 ++++++++++++ 7 files changed, 639 insertions(+) create mode 100644 research/universal-f7-singleton-l20-census-complete-seedfd938f30/AUDIT-RESULT.json create mode 100644 research/universal-f7-singleton-l20-census-complete-seedfd938f30/README.md create mode 100644 research/universal-f7-singleton-l20-census-complete-seedfd938f30/SOURCES.json create mode 100644 research/universal-f7-singleton-l20-census-complete-seedfd938f30/TASK.json create mode 100644 research/universal-f7-singleton-l20-census-complete-seedfd938f30/VERIFY.json create mode 100644 research/universal-f7-singleton-l20-census-complete-seedfd938f30/f7_census.c create mode 100644 research/universal-f7-singleton-l20-census-complete-seedfd938f30/verify.py diff --git a/research/universal-f7-singleton-l20-census-complete-seedfd938f30/AUDIT-RESULT.json b/research/universal-f7-singleton-l20-census-complete-seedfd938f30/AUDIT-RESULT.json new file mode 100644 index 0000000000..16e222a841 --- /dev/null +++ b/research/universal-f7-singleton-l20-census-complete-seedfd938f30/AUDIT-RESULT.json @@ -0,0 +1,71 @@ +{ + "schema": "independent-audit-result/v1", + "audited": { + "pr": 2634, + "head": "e2f30d93efbef5658334072aa855aa95e795e394", + "package": "research/universal-f7-singleton-l20-seed06704c39", + "checkpoint_file": "research/universal-f7-singleton-l20-seed06704c39/CENSUS20-PROGRESS.json" + }, + "base_commit": "b4560d9e7216f72b73c5aa940ac099c05e33ccf9", + "priority_revision": 5, + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18953986", + "author_checks_replayed": { + "verify.py": "PASS_F7_L20_VERIFY (L20=120 L22=126; census partial 11/15 reproduced from checkpoint)", + "independent.py": "PASS_F7_L20_INDEPENDENT", + "test_engine.py": "14 tests OK" + }, + "cross_validation": { + "completed_shards_reproduced_exactly": { + "0000": {"nodes": 2, "leaves": 0, "hits": 0}, + "0001": {"nodes": 2, "leaves": 0, "hits": 0}, + "0010": {"nodes": 2, "leaves": 0, "hits": 0}, + "0011": {"nodes": 2, "leaves": 0, "hits": 0}, + "0012": {"nodes": 2, "leaves": 0, "hits": 0}, + "0100": {"nodes": 4, "leaves": 0, "hits": 0}, + "0101": {"nodes": 4, "leaves": 0, "hits": 0}, + "0102": {"nodes": 798901031, "leaves": 67674177, "hits": 0}, + "0110": {"nodes": 3, "leaves": 0, "hits": 0}, + "0111": {"nodes": 3, "leaves": 0, "hits": 0}, + "0112": {"nodes": 3, "leaves": 0, "hits": 0} + }, + "capped_probe_agreement_max_nodes_5000000": [ + {"prefix": "0102", "nodes": 5000001, "leaves": 418619, "hits": 0}, + {"prefix": "0123", "nodes": 5000001, "leaves": 483870, "hits": 0}, + {"prefix": "01230", "nodes": 5000001, "leaves": 483870, "hits": 0}, + {"prefix": "01232", "nodes": 5000001, "leaves": 450641, "hits": 0} + ], + "note": "Capped probes compare this engine against the reference engine (copied to /tmp with the OverflowError patched to carry partial counts; original untouched)." + }, + "new_shard_results": { + "0120": {"nodes": 951630113, "leaves": 88700116, "hits": 0}, + "0121": {"nodes": 552149367, "leaves": 50308509, "hits": 0}, + "0122": {"nodes": 4, "leaves": 0, "hits": 0}, + "0123": {"nodes": 4002528537, "leaves": 390465512, "hits": 0} + }, + "census_total_15_of_15_shards": { + "nodes": 6305209079, + "simple_20_cycles": 597148314, + "universal_words": 0 + }, + "depth5_consistency_check_0123": { + "subshard_nodes": {"01230": 803327055, "01231": 502126395, "01232": 413775220, "01233": 5, "01234": 2283299882}, + "subshard_cycles": {"01230": 79211054, "01231": 47872485, "01232": 38541037, "01233": 0, "01234": 224840936}, + "node_sum_minus_depth4_total": 20, + "expected_duplicated_ancestor_calls": 20, + "cycle_sum_equals_depth4_total": true + }, + "auxiliary_independent_checks": { + "cover20_points": [2, 4, 8, 9, 14, 25, 26, 30, 31, 42, 49, 51, 60, 67, 77, 82, 100, 108, 109, 113], + "cover20_pair_xor_coverage": 128, + "cover20_degree_histogram": [0, 0, 0, 0, 0, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1, 2, 2, 2, 2, 3], + "parity_rederived": "restored word => all label counts even => even length; micro-check at n=3: restored words only at even lengths (L=6: 90 words; all odd L: 0)" + }, + "conclusion": "No universal restored length-20 word with 20 distinct prefix states exists at n = 7; the (10,10) simple-20-cycle census is complete (15/15 shards). Gap 20 <= f(7) <= 24 unchanged; repeated-state splits (10,9), (10,8), (9,9), (10,7) remain open, as recorded in PR2634.", + "environment": { + "compiler": "Apple clang version 21.0.0 (clang-2100.1.1.101)", + "python": "3.12.15", + "platform": "Darwin 25.5.0 arm64", + "full_census_wall_seconds_approx": 165 + }, + "ai_assistance": "Substantial AI assistance (Kimi) in scoping, implementation, verification and writing; no independent human review claimed." +} diff --git a/research/universal-f7-singleton-l20-census-complete-seedfd938f30/README.md b/research/universal-f7-singleton-l20-census-complete-seedfd938f30/README.md new file mode 100644 index 0000000000..293dd05060 --- /dev/null +++ b/research/universal-f7-singleton-l20-census-complete-seedfd938f30/README.md @@ -0,0 +1,136 @@ +# Independent audit of PR2634's resumable 20-cycle census, and completion of the (10,10) exclusion at L = 20 + +Contributor: **Nicholas Stone** (Kimi agent; substantial AI assistance in scoping, +implementation, verification and writing; no independent human review claimed). +No kappa, supplier, certificate or selected-frontier change. Base: main +`b4560d9e7216f72b73c5aa940ac099c05e33ccf9`, priority revision 5. +Claim: https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18953986 + +## Scope + +An independent audit (own engine, no shared code) of +[PR2634](https://github.com/CrocSwap/integer-mult-bounds/pull/2634) at head +`e2f30d93efbef5658334072aa855aa95e795e394` +(`research/universal-f7-singleton-l20-seed06704c39`), plus the completion of +its resumable restricted-growth simple-20-cycle census at `n = 7`, split +`(10,10)`, collision budget `e_ex + b_ex <= 27`, which stood at 11/15 shards +(798,901,058 nodes, 67,674,177 simple cycles, zero universal words). + +The census scope is unchanged: canonical (restricted-growth) restored words of +length 20 whose 20 prefix parity states are distinct. Words with repeated +boundary states (`|P|` in `{17,18,19}`) remain outside this census, exactly as +recorded in the audited package. Nothing here bears on those open splits. + +## Audit result: all checked statements reproduce exactly + +1. **Author's own checks re-run at the pinned head**: + `verify.py` → `PASS_F7_L20_VERIFY ... L20=120 L22=126`; + `independent.py` → `PASS_F7_L20_INDEPENDENT`; + `test_engine.py` → 14 tests OK. +2. **Independent engine** (`f7_census.c`, C, written from the mathematical + statement of the scope and the three proved-necessary prunes — multiplicity + room, self-avoidance justified by `|P| = L = 20`, and the split-identity + collision budget `45 + 45 - 63 = 27`; exact 128-bit masks): + reproduces **all 11 completed shard counts exactly**, including the heavy + shard `0102` at **798,901,031 nodes / 67,674,177 leaves / 0 hits** + (20.1 s vs ~57 min for the reference Python engine, a ~170x rate + difference with bitwise-identical counts). +3. **Mid-stream traversal agreement on new territory**: capped probes + (`max_nodes = 5,000,000`, reference engine vs this engine) agree exactly on + `0102` (5,000,001 / 418,619 / 0), `0123` (5,000,001 / 483,870 / 0), + `01230` (5,000,001 / 483,870 / 0) and `01232` (5,000,001 / 450,641 / 0), + covering the label-3 prefix region that no completed shard exercised. +4. **Auxiliary claims independently re-derived** (own formulation): + the pinned 20-point cover of `F2^7` indeed satisfies `P + P = F2^7` (all + 128 masks) and has induced-degree histogram + `[0,0,0,0,0,0,1,1,1,1,1,1,1,1,1,2,2,2,2,3]` — six isolated vertices, so no + closed walk spans it; the parity fact (restored ⇒ all label counts even ⇒ + even length, hence `L = 19` dead) re-derived and micro-checked at `n = 3` + (restored words exist only at even lengths). + +No discrepancy found in any checked statement of PR2634. + +## New result: the (10,10) census is complete — zero universal words + +The four remaining shards, run with the same independently written engine: + +| Shard | Nodes | Simple 20-cycles | Universal words | +|---|---:|---:|---:| +| 0120 | 951,630,113 | 88,700,116 | 0 | +| 0121 | 552,149,367 | 50,308,509 | 0 | +| 0122 | 4 | 0 | 0 | +| 0123 | 4,002,528,537 | 390,465,512 | 0 | + +Combined with the audited 11 shards: + +| Census total (15/15 shards) | Value | +|---|---:| +| Nodes | **6,305,209,079** | +| Simple 20-cycles checked | **597,148,314** | +| Universal words | **0** | + +**Conclusion (scoped):** no universal restored length-20 word with 20 +distinct prefix states exists at `n = 7`. Within the PR943 prefix-walk model +this closes the `(10,10)` split at `L = 20`. Together with PR2542's +length-18 exclusion and the parity fact (odd lengths dead), the only +length-20 cases left open are words with repeated boundary states, splits +`(10,9)`, `(10,8)`, `(9,9)`, `(10,7)` as recorded in PR2634's open questions. +The recorded gap `20 <= f(7) <= 24` is unchanged: this is a finite exclusion +inside one split, not a bound on all length-20 words. + +Internal consistency: the depth-5 sub-shards of `0123` +(803,327,055 + 502,126,395 + 413,775,220 + 5 + 2,283,299,882 nodes, +79,211,054 + 47,872,485 + 38,541,037 + 0 + 224,840,936 cycles) equal the +depth-4 totals up to exactly the 20 duplicated ancestor calls +(5 sub-shards x 4 shared prefix nodes), and the cycle counts match exactly. + +## Reproduction + +Requires a C compiler with `unsigned __int128` (GCC/Clang); no third-party +dependencies. Reference replay of the audited package requires Python 3.12, +standard library only. + +```sh +# This package: full 15-shard census (~3 min on Apple Silicon) +cc -O2 -o f7_census research/universal-f7-singleton-l20-census-complete-seedfd938f30/f7_census.c +./f7_census # prints one SHARD line per shard; hits.txt stays empty + +# Cross-validation replay (audited package, at PR2634 head e2f30d93) +python3 -I -B research/universal-f7-singleton-l20-seed06704c39/verify.py +python3 -I -B research/universal-f7-singleton-l20-seed06704c39/independent.py +python3 -I -B research/universal-f7-singleton-l20-seed06704c39/test_engine.py +``` + +Expected: per-shard `(nodes, leaves, hits)` exactly as in +[AUDIT-RESULT.json](AUDIT-RESULT.json); total 6,305,209,079 nodes, +597,148,314 cycles, 0 universal words. Observed environment: Apple clang +21.0.0, Darwin 25.5.0 arm64, Python 3.12.15. + +## Open next questions + +1. **Do repeated-state length-20 words (splits `(10,9)`, `(10,8)`, `(9,9)`, + `(10,7)`) admit a universal word?** This is now the *only* open family at + `L = 20`; settling it (either way) decides whether the census step-up from + PR2542 moves to `L = 22`. First step: extend this exact enumeration with + multiset collision semantics — revisit bookkeeping per boundary state with + per-split budgets from `lemma_a_table` rows — sharded the same way. + Blocker: revisit-aware prunes are weaker (self-avoidance is unavailable), + so per-split node counts will be substantially larger; the budget + derivation per split must be redone, not copied from the `(10,10)` value. +2. **Is the simple `(11,11)` census at `L = 22` feasible with the same + method?** First step: derive the `(11,11)` collision budget + (`C(11,2)+C(11,2)-63 = 47`) and probe one depth-5 shard for its node rate. + Blocker: expected tree size grows by roughly an order of magnitude over + `L = 20`; likely needs the shard-parallel run rather than a single process. + +## Credit + +PR943 model and first exact values: Ross Richardson +(`research/universal-connector-boundary`). Pinned five/six-source record: +Douglas Colkitt (`research/universal-connector-six-source`, PR1185). +Length-18 exclusion and the restricted-growth cycle census design: Aaron Wang +with opencode (PR2542). The audited 11-shard checkpoint, the parity closure +of `L = 19`, the template lemmas, the cover witnesses and the search +campaign: Aaron Wang with opencode (PR2634). This package contributes only +the independent audit and the completion of the remaining four shards; +no result of PR2634 is restated as new here. Apache-2.0. diff --git a/research/universal-f7-singleton-l20-census-complete-seedfd938f30/SOURCES.json b/research/universal-f7-singleton-l20-census-complete-seedfd938f30/SOURCES.json new file mode 100644 index 0000000000..a7cbf485c2 --- /dev/null +++ b/research/universal-f7-singleton-l20-census-complete-seedfd938f30/SOURCES.json @@ -0,0 +1,44 @@ +{ + "schema_version": 1, + "base_commit": "b4560d9e7216f72b73c5aa940ac099c05e33ccf9", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "889b95d936746df124872133ae1e7cc339adcb92", + "sha256": "7d185cd8c2af35988d638d969748ad7b670f902606444dbfc748e4402c340df6" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + } + ], + "references": [ + { + "pr": 2634, + "source_path": "research/universal-f7-singleton-l20-seed06704c39/CENSUS20-PROGRESS.json", + "head": "e2f30d93efbef5658334072aa855aa95e795e394", + "git_blob": "371970feb5350ade3a50fa0564168fa371553701", + "sha256": "226c94916281aa8febbef2fe4e12806affe798f136155fa5e0e92e8d00201ebd", + "note": "Audited input: the 11/15-shard checkpoint whose counts this audit reproduces and extends. Not vendored; pinned at the PR head." + }, + { + "pr": 2634, + "source_path": "research/universal-f7-singleton-l20-seed06704c39/engine.py", + "head": "e2f30d93efbef5658334072aa855aa95e795e394", + "git_blob": "210bd817b19beb20ed474d8946ea87a22121ac1c", + "sha256": "82e4c407b58864c74ffd14d47f00b6b1675005ee0e0173909b7bd092491175e4", + "note": "Audited reference engine. Read-only; a patched /tmp copy (OverflowError carrying partial counts) was used for capped probes; the original is untouched." + }, + { + "pr": 2634, + "source_path": "research/universal-f7-singleton-l20-seed06704c39/CERTIFICATE.json", + "head": "e2f30d93efbef5658334072aa855aa95e795e394", + "git_blob": "514ae7436b29e7cbdb5b1932a3b6cb6ecfe19ee4", + "sha256": "59b4d3cd991395dee0acbe54c766698bbf78d77e66ff9b7564d4e71476426664", + "note": "Audited input: source of the cover20 witness and the search-campaign claims independently re-checked here." + } + ] +} diff --git a/research/universal-f7-singleton-l20-census-complete-seedfd938f30/TASK.json b/research/universal-f7-singleton-l20-census-complete-seedfd938f30/TASK.json new file mode 100644 index 0000000000..c15b38cea3 --- /dev/null +++ b/research/universal-f7-singleton-l20-census-complete-seedfd938f30/TASK.json @@ -0,0 +1,100 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 5, + "base_commit": "b4560d9e7216f72b73c5aa940ac099c05e33ccf9", + "session_seed": "fd938f301313957624c8510f1045d5e0", + "track": "recursive-interfaces (drawn); scope changed to an independent audit of PR2634 plus completion of its resumable census", + "scope_key": "b8872a10540bed52f194", + "catalog_sha256": "7d185cd8c2af35988d638d969748ad7b670f902606444dbfc748e4402c340df6", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18953986", + "original_card": { + "id": "joint-query-controller", + "question": "Can one unresolved retention, output-consumer, hosting or physical-cost obligation complete a pinned QQ16 controller proposal within budget?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/joint-query/README.md", + "research/joint-query/evidence/QQ16-SELECTED-WITNESS.md", + "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Design and price one consumer or retained-state boundary for a pinned local decoder, including final restoration.", + "Audit one claimed physical invoice or prove a target-specific obstruction for its explicit retention/hosting contract." + ], + "acceptance_gate": "Name the changed premise of the fixed F0/B1 observation obstruction. Show exactly which query is recovered, legal native reads and restoration, and a full favorable budget including cover maps, helpers and endpoints. Local inverse identities alone do not close the global controller. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the QQ16 row in research-family-status.md. The fixed-first-pair witness remains scoped; pending #2540 adds early records and claims a complete local native decoder, but not a favorable global controller. Read its output-frame and ownership contract before designing another inverse.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "Check live claims and pin the newest relevant completed local word (starting lead #2540). Choose one unresolved consumer, retention, whole-cover movement, hosting or precision obligation. Price the complete proposal and test that obligation; do not repeat its claimed local inverse or native reconstruction unless providing distinct independent verification.", + "bottleneck_link": "The native local words exist; retained query information and its physical access are the missing link to a composed recursive interface.", + "allowed_variations": [ + "One paid query, one changed first pair, or one precisely specified affine helper state.", + "A counterexample or lower bound for that exact proposed repair.", + "One unresolved obligation of a newer local decoder, with exact source heads and a distinct claim/domain." + ], + "scope_change_triggers": [ + "Retaining the fixed first pair and ordinary schedule while allowing only homogeneous selected-only control, already excluded by the witness.", + "Treating cover-map counts as zero-cost physical address operations.", + "Recreating the pending complete local decoder or early-record/output-bank coalescing already under investigation without a distinct audit or changed premise." + ], + "overlap_terms": [ + "QQ16", + "joint-query", + "changing-chart controller", + "selected observation", + "1969", + "2540", + "early record", + "output-bank retention", + "complete native decoder" + ] + }, + "scope_status": "changed", + "actual_scope": "Independent audit of PR2634 (head e2f30d93efbef5658334072aa855aa95e795e394, package research/universal-f7-singleton-l20-seed06704c39) with an independently written engine (no shared code): (1) replay the author's own verify/independent/test suites at the pinned head; (2) reproduce all 11 completed per-shard census counts exactly, including heavy shard 0102; (3) confirm mid-stream traversal agreement via capped probes, covering the label-3 prefix region no completed shard exercised; (4) independently re-derive the cover20 witness properties and the parity fact; (5) complete the remaining shards 0120, 0121, 0122, 0123 of the resumable (10,10) simple-20-cycle census at n = 7.", + "scope_change_reason": "The chooser (OS seed fd938f301313957624c8510f1045d5e0) drew track recursive-interfaces with cards coverage-law-change / centre-path-sharing / joint-query-controller; find_overlap.py showed dense live claims and PRs on all three. Per autoresearch.md (prefer a live, unclaimed central handoff over a generic card; independent audits explicitly welcome when identified), the session took the unclaimed next step recorded in PR2634 itself ('completing the (10,10) exclusion needs several more hours of the same exact enumeration; the checkpoint is resumable') as an explicitly identified independent audit plus completion. Overlap checked: open PR list sorted by updatedAt at 2026-10-15T16:55Z showed no claim on the census remainder; claim posted in discussion 1166 before work began.", + "bottleneck_link": "A verified finite exclusion inside the PR943 query model sharpens the recorded singleton f(7) gap (20 <= f(7) <= 24) that downstream batch bills cite. It changes no supplier, tariff or kappa and instantiates no physical interface.", + "object_synonyms_used_in_overlap": [ + "universal source path", + "universal word", + "restored source word", + "singleton alphabet", + "seven-source", + "Gray bound", + "f(7)", + "restricted-growth", + "prefix walk", + "simple 20-cycle census", + "census20", + "hypercube closed walk", + "KB3b" + ], + "smallest_falsifying_instance_first": "Cross-validation gate before any new result: the independent engine had to reproduce all 11 completed shard counts exactly (including 798,901,031 / 67,674,177 / 0 on shard 0102) and the 5,000,000-node capped probes on four prefixes, before the four new shards were accepted. A depth-5 vs depth-4 internal consistency check on shard 0123 (exact cycle-sum equality; node delta exactly the 20 duplicated ancestor calls) guards against shard-initialization errors.", + "stop_rule": "Stop at the first of: (a) any mismatch against the author's completed shard counts (audit failure, report the discrepancy), (b) a universal word found (report the witness), (c) all 15 shards complete (report totals), (d) session budget expiry with exact partial counts recorded. Outcome: (c).", + "outcome": "completed", + "evidence": "AUDIT-RESULT.json records: the replayed author checks (PASS_F7_L20_VERIFY, PASS_F7_L20_INDEPENDENT, 14 tests OK); exact reproduction of all 11 completed shard counts; exact capped-probe agreement on 0102/0123/01230/01232 at 5,000,000 nodes; the four new shard counts; census totals 6,305,209,079 nodes / 597,148,314 simple 20-cycles / 0 universal words; the depth-5 consistency check; independent re-derivation of the cover20 coverage (128 masks), its degree histogram (six isolated vertices), and the parity fact. f7_census.c is the independent engine; README.md has reproduction commands and open next questions. No kappa claim; no supplier claim; the recorded gap 20 <= f(7) <= 24 is unchanged.", + "author": "Nicholas Stone", + "ai_assistance": "Substantial AI assistance (Kimi agent) in scoping, implementation, verification and writing; no independent human review claimed.", + "open_questions": [ + { + "question": "Do repeated-state length-20 words (splits (10,9), (10,8), (9,9), (10,7)) admit a universal word?", + "why_it_matters": "It is now the only open family at L = 20; settling it decides whether the census step-up from PR2542 moves to L = 22.", + "first_step": "Extend this exact enumeration with multiset collision semantics and per-split budgets derived from lemma_a_table rows, sharded the same way.", + "blocked_by": "Revisit-aware prunes are weaker (self-avoidance unavailable); per-split node counts will be substantially larger and each split's collision budget must be re-derived." + }, + { + "question": "Is the simple (11,11) census at L = 22 feasible with the same method?", + "why_it_matters": "Combined with the walk-shape obstruction question it is on the path to deciding whether the Gray bound 24 is sharp.", + "first_step": "Derive the (11,11) collision budget (C(11,2)+C(11,2)-63 = 47) and probe one depth-5 shard for its node rate.", + "blocked_by": "Expected tree size grows by roughly an order of magnitude over L = 20; likely needs a shard-parallel run." + } + ] +} diff --git a/research/universal-f7-singleton-l20-census-complete-seedfd938f30/VERIFY.json b/research/universal-f7-singleton-l20-census-complete-seedfd938f30/VERIFY.json new file mode 100644 index 0000000000..808927be90 --- /dev/null +++ b/research/universal-f7-singleton-l20-census-complete-seedfd938f30/VERIFY.json @@ -0,0 +1,20 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": ["{python}", "-I", "-B", "{package}/verify.py"], + "timeout_seconds": 120, + "checks": "Quick mode: compiles the independent C engine and checks the ten small completed shards plus the four 5,000,000-node capped probes (0102, 0123, 01230, 01232) exactly against AUDIT-RESULT.json. Expected marker: PASS_F7_L20_CENSUS_AUDIT_QUICK nodes=6305209079 cycles=597148314 universal_words=0" + }, + { + "argv": ["{python}", "-I", "-B", "{package}/verify.py", "--full"], + "timeout_seconds": 600, + "checks": "Full mode: complete 15-shard census with the independent engine; every per-shard (nodes, leaves, hits) must equal AUDIT-RESULT.json, with totals 6,305,209,079 nodes, 597,148,314 simple 20-cycles, 0 universal words. Expected marker: PASS_F7_L20_CENSUS_AUDIT_FULL nodes=6305209079 cycles=597148314 universal_words=0" + } + ], + "notes": "Requires a C compiler supporting unsigned __int128 (GCC/Clang). Reference replay of the audited PR2634 package (verify.py / independent.py / test_engine.py) is documented in the README and was run at head e2f30d93efbef5658334072aa855aa95e795e394; it is not re-run by this manifest because that package is not part of this base commit." +} diff --git a/research/universal-f7-singleton-l20-census-complete-seedfd938f30/f7_census.c b/research/universal-f7-singleton-l20-census-complete-seedfd938f30/f7_census.c new file mode 100644 index 0000000000..37d1c1ecfb --- /dev/null +++ b/research/universal-f7-singleton-l20-census-complete-seedfd938f30/f7_census.c @@ -0,0 +1,160 @@ +// Independent audit engine: (10,10) simple-20-cycle census at n = 7. +// +// Re-implements, from scratch, the exact census scope of +// research/universal-f7-singleton-l20-seed06704c39 (PR2634, head e2f30d93): +// restricted-growth restored words of length 20 over 7 singleton labels whose +// 20 prefix parity states are distinct (|P| = 20 forces the (10,10) split). +// +// Only proved-necessary prunes are applied: +// 1. multiplicity room: odd + 2*(n-used) <= L - i, and per-label count < L-2*(n-1); +// 2. self-avoidance of prefix states (justified by |P| = L = 20); +// 3. pair-representation collision budget e_ex + b_ex <= C(10,2)+C(10,2)-63 = 27 +// (full coverage needs all 63 nonzero even masks from E+E and O+O). +// +// Universality at a closed leaf: P + P = F2^7 over the 20 prefix states. +// Exact 128-bit integer masks; no floating point; no shared code with the +// audited package. Cross-validation gate: reproduces the author's 11 +// completed per-shard (nodes, leaves, hits) exactly before any new result. +// +// Usage: +// cc -O2 -o f7_census f7_census.c +// ./f7_census # all 15 shards (~165 s on Apple Silicon) +// ./f7_census 0102 0123 # selected shards +// ./f7_census 0123:5000000 # capped probe (aborts whole traversal, like +// # the reference engine's OverflowError at max_nodes) +#include +#include +#include +#include +#include + +#define N 7 +#define L 20 +#define BUDGET 27 + +static int prefix[8], preflen; +static uint64_t nodes, leaves, hits; +static int cnt[N]; +static int qstate, coll, used, odd; +static unsigned __int128 seen, e_supp, o_supp; +static int E[L], O[L], e_len, o_len; +static int word[L]; +static FILE *hitout; +static uint64_t node_cap; /* 0 = no cap; aborts whole traversal when exceeded (mirrors OverflowError) */ +static int aborted; + +static inline int pop128(unsigned __int128 x) { + return __builtin_popcountll((uint64_t)x) + __builtin_popcountll((uint64_t)(x >> 64)); +} + +static void rec(int i) { + nodes++; + if (node_cap && nodes > node_cap) { aborted = 1; return; } + if (i == L) { + if (qstate != 0) return; + leaves++; + int pts[2 * L], m = 0; + for (int a = 0; a < e_len; a++) pts[m++] = E[a]; + for (int a = 0; a < o_len; a++) pts[m++] = O[a]; + unsigned __int128 cov = 0; + for (int a = 0; a < m; a++) + for (int b = a; b < m; b++) + cov |= (unsigned __int128)1 << (pts[a] ^ pts[b]); + if (pop128(cov) == (1 << N)) { + hits++; + if (hitout) { + for (int k = 0; k < L; k++) fprintf(hitout, "%d", word[k]); + fprintf(hitout, "\n"); + fflush(hitout); + } + } + return; + } + if (odd + 2 * (N - used) > L - i) return; + const int room = L - 2 * (N - 1); + const int limit = (used + 1 < N) ? used + 1 : N; + for (int j = 0; j < limit; j++) { + if (aborted) return; + if (cnt[j] >= room) continue; + if (i < preflen && j != prefix[i]) continue; + int nq = qstate ^ (1 << j); + int closing = (i == L - 1 && nq == 0); + if (!closing && (seen >> nq) & 1) continue; + unsigned __int128 add = 0; + int newcoll = 0; + if (!closing) { + if (nq & 1) { + for (int a = 0; a < o_len; a++) add |= (unsigned __int128)1 << (nq ^ O[a]); + newcoll = pop128(add & o_supp); + } else { + for (int a = 0; a < e_len; a++) add |= (unsigned __int128)1 << (nq ^ E[a]); + newcoll = pop128(add & e_supp); + } + if (coll + newcoll > BUDGET) continue; + } + /* save */ + unsigned __int128 s_seen = seen, s_es = e_supp, s_os = o_supp; + int s_q = qstate, s_coll = coll, s_used = used, s_odd = odd, s_cnt = cnt[j]; + word[i] = j; + cnt[j]++; + odd += (cnt[j] & 1) ? 1 : -1; + qstate = nq; + coll += newcoll; + if (!closing) { + seen |= (unsigned __int128)1 << nq; + if (nq & 1) { o_supp |= add; O[o_len++] = nq; } + else { e_supp |= add; E[e_len++] = nq; } + } + if (j == s_used) used++; + rec(i + 1); + /* restore */ + if (!closing) { if (nq & 1) o_len--; else e_len--; } + seen = s_seen; e_supp = s_es; o_supp = s_os; + qstate = s_q; coll = s_coll; used = s_used; odd = s_odd; cnt[j] = s_cnt; + } +} + +static void run_shard(const char *key) { + preflen = 0; + node_cap = 0; + const char *colon = strchr(key, ':'); + char kbuf[16]; + if (colon) { + size_t kl = (size_t)(colon - key); + memcpy(kbuf, key, kl); kbuf[kl] = 0; + node_cap = strtoull(colon + 1, NULL, 10); + key = kbuf; + } + preflen = (int)strlen(key); + for (int i = 0; i < preflen; i++) prefix[i] = key[i] - '0'; + nodes = leaves = hits = 0; + aborted = 0; + qstate = 0; seen = 1; e_supp = 0; o_supp = 0; + coll = 0; used = 0; odd = 0; + e_len = 1; E[0] = 0; o_len = 0; + memset(cnt, 0, sizeof cnt); + struct timespec t0, t1; + clock_gettime(CLOCK_MONOTONIC, &t0); + rec(0); + clock_gettime(CLOCK_MONOTONIC, &t1); + double secs = (double)(t1.tv_sec - t0.tv_sec) + 1e-9 * (double)(t1.tv_nsec - t0.tv_nsec); + printf("SHARD %s nodes=%llu leaves=%llu hits=%llu secs=%.1f\n", + key, (unsigned long long)nodes, (unsigned long long)leaves, + (unsigned long long)hits, secs); + fflush(stdout); +} + +int main(int argc, char **argv) { + hitout = fopen("hits.txt", "w"); + if (argc > 1) { + for (int a = 1; a < argc; a++) run_shard(argv[a]); + } else { + /* all 15 restricted-growth prefixes of depth 4 */ + const char *shards[] = {"0000","0001","0010","0011","0012", + "0100","0101","0102","0110","0111","0112", + "0120","0121","0122","0123"}; + for (int s = 0; s < 15; s++) run_shard(shards[s]); + } + if (hitout) fclose(hitout); + return 0; +} diff --git a/research/universal-f7-singleton-l20-census-complete-seedfd938f30/verify.py b/research/universal-f7-singleton-l20-census-complete-seedfd938f30/verify.py new file mode 100644 index 0000000000..80bbf55f9a --- /dev/null +++ b/research/universal-f7-singleton-l20-census-complete-seedfd938f30/verify.py @@ -0,0 +1,108 @@ +#!/usr/bin/env python3 +"""Verification driver for the PR2634 census audit package. + +Quick mode (default, ~2 s): compiles f7_census.c and checks the ten small +shards plus the four 5,000,000-node capped probes against AUDIT-RESULT.json. +Full mode (--full, ~3 min): runs the complete 15-shard census and checks +every shard count and the totals. + +Standard library only; requires a C compiler with unsigned __int128. +""" +import json +import re +import subprocess +import sys +import tempfile +from pathlib import Path + +HERE = Path(__file__).resolve().parent +RESULT = json.loads((HERE / "AUDIT-RESULT.json").read_text(encoding="utf-8")) + +SHARD_LINE = re.compile( + r"SHARD (\S+) nodes=(\d+) leaves=(\d+) hits=(\d+)") + + +def build(workdir): + exe = Path(workdir) / "f7_census" + subprocess.run( + ["cc", "-O2", "-o", str(exe), str(HERE / "f7_census.c")], + check=True) + return exe + + +def run_shards(exe, workdir, specs): + out = {} + for spec in specs: + proc = subprocess.run([str(exe), spec], cwd=workdir, check=True, + capture_output=True, text=True) + m = SHARD_LINE.search(proc.stdout) + assert m, f"no SHARD line for {spec}: {proc.stdout!r}" + key = m.group(1) + out[key] = dict(nodes=int(m.group(2)), leaves=int(m.group(3)), + hits=int(m.group(4))) + return out + + +def main(): + full = "--full" in sys.argv + with tempfile.TemporaryDirectory() as workdir: + exe = build(workdir) + + # Capped probes: exact agreement with the reference engine's + # max_nodes semantics, including label-3 prefix territory. + probes = {p["prefix"]: p for p in + RESULT["cross_validation"] + ["capped_probe_agreement_max_nodes_5000000"]} + got = run_shards(exe, workdir, + [f"{k}:5000000" for k in sorted(probes)]) + for k, want in probes.items(): + g = got[k] + assert (g["nodes"], g["leaves"], g["hits"]) == ( + want["nodes"], want["leaves"], want["hits"]), (k, g, want) + + # Small completed shards (instant). + small = [k for k, v in RESULT["cross_validation"] + ["completed_shards_reproduced_exactly"].items() + if v["nodes"] < 100] + want_small = RESULT["cross_validation"][ + "completed_shards_reproduced_exactly"] + got = run_shards(exe, workdir, small) + for k in small: + w = want_small[k] + g = got[k] + assert (g["nodes"], g["leaves"], g["hits"]) == ( + w["nodes"], w["leaves"], w["hits"]), (k, g, w) + + if full: + all_shards = sorted( + set(RESULT["cross_validation"] + ["completed_shards_reproduced_exactly"]) + | set(RESULT["new_shard_results"])) + want_all = dict(RESULT["cross_validation"] + ["completed_shards_reproduced_exactly"]) + want_all.update(RESULT["new_shard_results"]) + got = run_shards(exe, workdir, all_shards) + tn = tl = th = 0 + for k in all_shards: + w = want_all[k] + g = got[k] + assert (g["nodes"], g["leaves"], g["hits"]) == ( + w["nodes"], w["leaves"], w["hits"]), (k, g, w) + tn += g["nodes"] + tl += g["leaves"] + th += g["hits"] + tot = RESULT["census_total_15_of_15_shards"] + assert tn == tot["nodes"], (tn, tot) + assert tl == tot["simple_20_cycles"], (tl, tot) + assert th == tot["universal_words"], (th, tot) + + mode = "FULL" if full else "QUICK" + print(f"PASS_F7_L20_CENSUS_AUDIT_{mode} " + f"nodes={RESULT['census_total_15_of_15_shards']['nodes']} " + f"cycles={RESULT['census_total_15_of_15_shards']['simple_20_cycles']} " + f"universal_words=0") + return 0 + + +if __name__ == "__main__": + sys.exit(main())