From 421b53ef3ff32c7aa0c058109fbb8e2bb1271902 Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Fri, 23 Oct 2026 00:35:16 -0500 Subject: [PATCH 1/2] Prove the sharp five-label length-twelve excess cap --- research/f7-five-label-sharp-cap/README.md | 267 ++++++++++++++++++ research/f7-five-label-sharp-cap/RESULT.json | 85 ++++++ research/f7-five-label-sharp-cap/SOURCES.json | 30 ++ research/f7-five-label-sharp-cap/TASK.json | 135 +++++++++ research/f7-five-label-sharp-cap/VERIFY.json | 34 +++ research/f7-five-label-sharp-cap/verify.py | 228 +++++++++++++++ 6 files changed, 779 insertions(+) create mode 100644 research/f7-five-label-sharp-cap/README.md create mode 100644 research/f7-five-label-sharp-cap/RESULT.json create mode 100644 research/f7-five-label-sharp-cap/SOURCES.json create mode 100644 research/f7-five-label-sharp-cap/TASK.json create mode 100644 research/f7-five-label-sharp-cap/VERIFY.json create mode 100644 research/f7-five-label-sharp-cap/verify.py diff --git a/research/f7-five-label-sharp-cap/README.md b/research/f7-five-label-sharp-cap/README.md new file mode 100644 index 0000000000..a7502283bd --- /dev/null +++ b/research/f7-five-label-sharp-cap/README.md @@ -0,0 +1,267 @@ +# Sharp high-weight excess at five labels and length twelve + +**Scoped combinatorial proof; no new kappa.** Every simple restored universal +singleton-prefix walk of length twelve on F2^5 has separate-class pair-sum +excess at most **11** for every functional of weight four or five. The bound +is attained at each such weight. A weight-four functional cannot have an +(8,4) class split. + +This closes Open next question 1 of Mihir Srivastava's +[PR #4907](https://github.com/CrocSwap/integer-mult-bounds/pull/4907). +That proof gave the sufficient cap 15 and excluded planar (8,4) minorities. +Its finite checks already measured the cap 11 and found no (8,4) walk. +Those measurements are prior work. The new result is the proof for every +minority shape, followed by the sharp support bound. The complete +multiplication exponent and selected frontier do not change. + +Prepared for Ali Romman with substantial OpenAI Codex assistance. +Apache-2.0. No independent human or formal proof-kernel review is claimed. + +## Definitions + +Let q_0=0 and q_(i+1)=q_i+e_(w_i) in F2^5, where the twelve labels w_i +are in {0,...,4}. Restoration means q_12=0. Simplicity means that the +nonclosing states q_0,...,q_11 are distinct. Let S be this twelve-point +set. Universality means S+S=F2^5. In particular, all five labels occur. +Addition below is XOR. For a point set C, put + +```text +D(C) = {x+y : x,y in C, x != y}. +X_f = choose(|A|,2) + choose(|B|,2) - |D(A)| - |D(B)|, +``` + +where A and B are the two classes of f in S. A difference in both +supports is counted in both. Universality gives +D(A) union D(B) = ker(f) minus {0}, a set of size 15. + +## 1. Matching balance and the forced quotient cycle + +Use Nick Petalas's matching-balance lemma from +[PR #4894](https://github.com/CrocSwap/integer-mult-bounds/pull/4894), +as used in PR #4907. For completeness, if f has weight four, let v be +the omitted coordinate vector. Let a and b be the numbers of cycle +edges within A and B, and c the number between them. Only v-edges stay +in a class, and these edges form a matching. With s=|A| and t=|B|, + +```text +2s = 2a+c, 2t = 2b+c, s-t = a-b, 2a <= s, 2b <= t. +``` + +Thus max(s,t) <= 2 min(s,t). The only unordered splits are (6,6), +(7,5), and (8,4). Weight five flips at every edge and gives (6,6). + +Suppose the split is (8,4), with A the larger class. Equality forces +a=4, b=0, c=8. Every A vertex has its v-partner in A and exactly one +cycle neighbor in B. The cycle consists of four blocks + +```text +B -- A --v-- A -- B. +``` + +Delete the v coordinate. After a translation, the projection T of A is +a four-point set in the even-parity subspace E of F2^4. Each point of T +labels exactly one block. Every block changes the v-level once. The +four B vertices therefore alternate v-levels: two at level 0, two at +level 1. The two crossing edges of a block preserve the v-level. + +## 2. Universality forces an impossible neighbor count + +A four-point set has either three or six nonzero differences. If T +has three, then D(A) has 1+2*3=7 elements. Four B vertices supply at +most six more, fewer than the required fifteen. Therefore |D(T)|=6. + +Translate one point of T to zero. The other three are independent in +E. Let z be their sum, or equivalently the sum of all four original +points of T. Then z is the unique nonzero element of E absent from +D(T), and + +```text +T and T+z are disjoint, and their union is E. +``` + +The lift formula is D(A) = {(0,1)} union {(d,0),(d,1): d in D(T)}. +Thus the two differences missing from D(A) are the lifts (z,0) and (z,1). +Universality requires both to occur in D(B). The first comes from two +B vertices at the same v-level. Call their projections u and w=u+z. +They use both vertices at that level. The second difference comes +from opposite levels. It cannot use two new endpoints: only the other +level is left. Thus one of its endpoints is a vertex already chosen, +and the other level contains a second lift of u or of w. Rename them +so that u occurs at both levels. Write the fourth projection as y. + +Up to reversal and rotation, the alternating-level B order is + +```text +u_0, u_1, w_0, y_1. +``` + +Here y != u, since B is a set; y=w is allowed. The four distinct block +labels t_0,t_1,t_2,t_3 in T must respectively be common cube neighbors of + +```text +(u,u), (u,w), (w,y), (y,u). +``` + +Consequently u has at least three neighbors in T (t_0,t_1,t_3), and w +has at least two (t_1,t_2). Let N(x) be the four neighbors of x in Q4. +Since w=u+z, N(w)=N(u)+z. The partition E=T disjoint-union (T+z) gives + +```text +|N(u) intersect T| + |N(w) intersect T| = |N(u)| = 4. +``` + +The cycle needs a sum of at least five. This is a contradiction. It +excludes every (8,4) minority, with no planarity assumption. + +## 3. Small support bounds in F2^4 + +The remaining splits use these elementary bounds. Translation does +not change differences; affine dimension means the dimension after +one point is translated to zero. + +| Size of C | If affine dimension is three | If affine dimension is four | +|---|---|---| +| 5 | 7 | 10 | +| 6 | 7 | at least 12 | +| 7 | 7 | at least 13 | + +The table entries give the support size. These sets have affine dimension at least three. In dimension three, +more than half of the eight-point space is present. For each nonzero +h, one of the four pairs {x,x+h} is fully present, so all seven +nonzero differences occur. + +In dimension four, choose an affine basis and send it to +{0,1,2,4,8}, using binary notation for F2^4. It has ten differences. +A sixth point has Hamming weight two, three, or four. The first two +cases give twelve differences; weight four gives fifteen. For weight +three, translate by one of its three basis vectors and choose the +translated basis. This makes the sixth point have weight two. +Coordinate permutations then put either twelve-difference case in the +form + +```text +C6 = {0,1,2,3,4,8}, D(C6) = {1,...,12}. +``` + +Every possible seventh point gives a new difference. The following +four rows cover the complement of C6; each listed s belongs to C6. + +| New point y | Choose s | New difference y+s | +|---|---|---| +| 5, 6, 7 | 8 | 13, 14, 15, respectively | +| 9, 10, 11 | 4 | 13, 14, 15, respectively | +| 12 | 1 | 13 | +| 13, 14, 15 | 0 | 13, 14, 15, respectively | + +This proves the bound thirteen. If the chosen six-point set already +has fifteen differences, the claim also follows. + +## 4. The sharp cap + +Translate each functional class into ker(f), which is F2^4. +For (6,6), both supports have size at least seven. They cannot both +have size seven, since their union has size fifteen. Thus one has +size at least twelve, by section 3, and + +```text +X_f <= 2*choose(6,2) - 12 - 7 = 11. +``` + +For (7,5), suppose the seven-point class lies in an affine +three-dimensional space with direction H. Its support is H minus {0}. +The five-point class would have to supply all eight differences outside +H. If it has k points in one H-coset and 5-k in the other, it supplies +at most k(5-k) <= 6 such differences. Universality rules this out. +The seven-point class therefore has affine dimension four. Section 3 +gives support sizes at least thirteen and seven, so + +```text +X_f <= choose(7,2) + choose(5,2) - 13 - 7 = 11. +``` + +Together with section 2, this proves the theorem. Sharpness follows +from the explicit universal simple restored words + +```text +weight four: 012343234031, mask 10111, X_f=11; +weight five: 012343103432, mask 11111, X_f=11. +``` + +Coordinate permutations send the first mask to every weight-four mask +and preserve the hypotheses and excess. The first witness is retained +from PR #4907. The second was selected from its existing measured census; +we claim no new witness search result. + +## Reproduction and evidence + +Use Python 3.12 or later and the standard library: + +```sh +python3 -I -B research/f7-five-label-sharp-cap/verify.py +python3 -I -O -W error -B research/f7-five-label-sharp-cap/verify.py +python3 -B scripts/research_package.py --package research/f7-five-label-sharp-cap +``` + +The standalone verifier imports no predecessor program. It checks all +23,816 subsets of sizes five, six and seven in F2^4. It also checks all +127,400 v-invariant (8,4) set pairs at f=01111, including all 13,664 +universal sets. A second method searches the literal twelve-vertex +cube graph for a Hamiltonian cycle for each universal set. This method +does not use the quotient proof or its degree-sum contradiction. +Translation and coordinate symmetry cover the other weight-four masks. +The set counts repeat the predecessor domain; the new tests corroborate +the stronger exclusion and its proof steps. + +The verifier checks both equality witnesses, invalid-input controls, +a cap-ten rejection, a low-weight boundary, and a universal set that +has no required cycle. It also checks nonuniversal (8,4) cycles as +positive controls for the graph search. Normal replay recomputes the +complete receipt and compares it with RESULT.json. `--emit-receipt` +prints the calculated receipt for explicit authoring. It writes no files. +The receipt binds all five source files in this package. The standalone +check needs neither Git nor network access. + +Local checks passed with CPython 3.12.13 and 3.14.7 on macOS. Both +registered Python 3.12 commands passed. Eight separate code mutations +failed in optimized mode with receipt comparison disabled: wrong affine +dimension, a lost difference, graph search forced false or true, omitted +universality, low-weight admission, cap ten, and merged class supports. +The controls test semantic behavior, not only source hashes. + +## Scope, provenance and credit + +Base: `b91956876e5b4122fd89179f1b57557ff8378f15`, priority revision 7. +The selected kappa is 60403/20000000. SOURCES.json binds predecessor +proof documents as historical provenance. They are not runtime inputs. +This is the handoff-first refinement of the census-pruning-audit card, +with its original card retained in TASK.json. The +[canonical claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/4903#discussioncomment-19138640) +records the bounded assignment and overlap limits. + +Credit Mihir Srivastava (@mihir-s-05) for PR #4907's theorem, quotient +setup, prior measured cap and open question. Credit Nick Petalas for +PR #4894's matching-balance lemma and the earlier measured classifications. +Retain unpaidmoon's question and excess convention from +[PR #4148](https://github.com/CrocSwap/integer-mult-bounds/pull/4148), +Nicholas Stone's parity correction from +[PR #2973](https://github.com/CrocSwap/integer-mult-bounds/pull/2973), +James Reed's boundary audit from +[PR #3096](https://github.com/CrocSwap/integer-mult-bounds/pull/3096), +and Ross Richardson's singleton-prefix model from +[PR #943](https://github.com/CrocSwap/integer-mult-bounds/pull/943). +The new neighbor-count proof and support argument are stated in full. +No predecessor source or license notice is changed. + +The result does not cover other dimensions or lengths, partial prefixes, +low-weight functionals, nonsimple walks, nonuniversal sets or arbitrary +point sets without a cycle. No engine integration, seven-label census, +supplier admission, selected cold replay, Lean or Docker run is claimed. +It gives no new multiplication exponent or practical speedup. The proof +and code are author-checked; independent review remains open. + +## Open next questions + +Can the sharper complete-walk bound support a useful partial-prefix prune? +First derive a completion bound from the remaining edges and prove that +it preserves every universal completion. Then measure it in a maintained +engine. No such completion contract or runtime result is supplied here. diff --git a/research/f7-five-label-sharp-cap/RESULT.json b/research/f7-five-label-sharp-cap/RESULT.json new file mode 100644 index 0000000000..f6bbfee4ff --- /dev/null +++ b/research/f7-five-label-sharp-cap/RESULT.json @@ -0,0 +1,85 @@ +{ + "controls": { + "low_weight_excess": 21, + "semantic_rejections": 12, + "set_only_excess": 18, + "sharp_value": 11, + "weight_five_witness": [ + 0, + 1, + 2, + 3, + 4, + 3, + 1, + 0, + 3, + 4, + 3, + 2 + ], + "weight_four_witness": [ + 0, + 1, + 2, + 3, + 4, + 3, + 2, + 3, + 4, + 0, + 3, + 1 + ] + }, + "proved_cap": 11, + "schema": "f7-five-label-sharp-cap/v1", + "sets": { + "balanced_levels": 5600, + "literal_graph_rejections": 13664, + "nonuniversal_cycle_control": [ + 0, + 3, + 5, + 6, + 16, + 19, + 21, + 22, + 1, + 2, + 17, + 18 + ], + "set_pairs": 127400, + "unequal_levels": 8064, + "universal_sets": 13664 + }, + "source_sha256": { + "README.md": "8d3703e4502e45b7423dc65e0e56b16eebc472c0f78412d262d340f640e0aa9c", + "SOURCES.json": "28f1729a2e27ccd772130e68ff7e6fc3faa210b0af077ca1b7423c4249916665", + "TASK.json": "794d695cc1ee03e4ad8f87bc3f2f9988ee0210823f8d0f53c163f4f67b434677", + "VERIFY.json": "61e345716563180730fd324bf9d6bd12074d6fccaabe63a0a4b76cb2ad2657bc", + "verify.py": "035687ed280ac001fc29c24f36ee7974966011206e11140891f9312ccefd69fb" + }, + "supports": { + "histograms": { + "5": { + "10": 2688, + "7": 1680 + }, + "6": { + "12": 6720, + "15": 448, + "7": 840 + }, + "7": { + "13": 6720, + "15": 4480, + "7": 240 + } + }, + "subsets": 23816 + } +} diff --git a/research/f7-five-label-sharp-cap/SOURCES.json b/research/f7-five-label-sharp-cap/SOURCES.json new file mode 100644 index 0000000000..ea29431f31 --- /dev/null +++ b/research/f7-five-label-sharp-cap/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "b91956876e5b4122fd89179f1b57557ff8378f15", + "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-pruning-proof/README.md", + "usage": "provenance", + "git_blob": "5d7494c9ace1c7f032f1a4f41d775c1b8df65e16", + "sha256": "143ea4f63ee5d7f054adf63a21194b84ca0daacb84a76cbcc96298424edc7893" + }, + { + "path": "research/f7-four-stay-pruning/README.md", + "usage": "provenance", + "git_blob": "3521be1e9e02a4cacd3db17c80a2688e01973dee", + "sha256": "f46da8777226abf77c3ca51fbb2c6420cee6e1e5ea104ac976be07f80c8f1405" + } + ] +} diff --git a/research/f7-five-label-sharp-cap/TASK.json b/research/f7-five-label-sharp-cap/TASK.json new file mode 100644 index 0000000000..cba4eb49d7 --- /dev/null +++ b/research/f7-five-label-sharp-cap/TASK.json @@ -0,0 +1,135 @@ +{ + "schema_version": 1, + "task_id": "census-pruning-audit", + "priority_revision": 7, + "base_commit": "b91956876e5b4122fd89179f1b57557ff8378f15", + "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": "Prove the sharp high-weight excess cap 11 and exclude every (8,4) split for simple restored universal length-twelve walks on F2^5.", + "scope_change_reason": "Take PR4907 Open next question 1. The existing measurements are prior evidence; this contribution supplies the missing proof.", + "bottleneck_link": "This proves the exact validity boundary of one small census-pruning model. It is a scoped side result, with no supplier or complete kappa gain.", + "budget_minutes": 60, + "stop_rule": "Stop after the sharp bound, bounded exact checks, controls and publication. No larger census or engine integration.", + "outcome": "completed", + "evidence": "Self-contained proof; all 23816 small support sets and 127400 (8,4) set pairs; independent literal Hamiltonian search on 13664 universal sets; sharp witnesses and rejection controls.", + "author": "Ali Romman", + "ai_assistance": "Substantial OpenAI Codex assistance for proof, code, checks and publication. No independent human or formal proof-kernel review.", + "open_questions": [ + { + "question": "Can the sharp complete-walk bound give a useful partial-prefix prune?", + "why_it_matters": "A sound completion bound could reduce a maintained census without dropping universal completions.", + "first_step": "State the remaining-edge contract and derive a bound valid for every completion before measuring runtime.", + "blocked_by": "No partial-prefix completion contract or engine performance evidence is supplied." + } + ], + "canonical_discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4903#discussioncomment-19138640", + "environment": { + "python": "3.14.7", + "platform": "Darwin", + "dependencies": "standard library only", + "registered_python": "3.12.13", + "additional_direct_python": "3.14.7" + }, + "selection": { + "mode": "handoff-first", + "source_pr": 4907, + "source_head": "faf51ea356b9b5d5ce00c141124e4fc3fcefce73", + "priority_revision": 7 + }, + "unrun_obligations": [ + "Independent human review", + "Formal proof-kernel check", + "Pruning-engine integration", + "Seven-label census", + "Supplier admission", + "Selected cold replay" + ], + "overlap": { + "searched_at": "2026-10-23T05:23:51.228413+00:00", + "coverage": { + "local": { + "head": "b91956876e5b4122fd89179f1b57557ff8378f15", + "records": 63, + "head_records": 6636, + "complete_head_inventory": false + }, + "open_prs": { + "fetched_at": "2026-10-23T05:21:44.772891+00:00", + "complete_pagination": true, + "records": 329 + }, + "discussions": { + "fetched_at": "2026-10-23T05:22:41.947907+00:00", + "complete_pagination": true, + "records": 4081 + } + }, + "limits": "Sparse local corpus; no arbitrary diff search or unpublished-work coverage. Related f7 notes and the live handoff were read." + }, + "submission_refresh": { + "checked_at": "2026-10-23T05:33:52.552943+00:00", + "canonical_main": "b91956876e5b4122fd89179f1b57557ff8378f15", + "priority_revision": 7, + "guidance_change": false, + "coverage": { + "local": { + "head": "b91956876e5b4122fd89179f1b57557ff8378f15", + "records": 65, + "head_records": 6636, + "complete_head_inventory": false + }, + "open_prs": { + "fetched_at": "2026-10-23T05:32:56.294616+00:00", + "complete_pagination": true, + "records": 333 + }, + "discussions": { + "fetched_at": "2026-10-23T05:33:52.412453+00:00", + "complete_pagination": true, + "records": 4085 + } + }, + "decision": "Continue the same proof. No competing result was found in the stated coverage." + } +} diff --git a/research/f7-five-label-sharp-cap/VERIFY.json b/research/f7-five-label-sharp-cap/VERIFY.json new file mode 100644 index 0000000000..25e09d2bb8 --- /dev/null +++ b/research/f7-five-label-sharp-cap/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exact support and quotient proof checks, independent literal cube-graph search, sharpness, failure controls, and full receipt comparison." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "The same checks with Python assertions disabled." + } + ] +} diff --git a/research/f7-five-label-sharp-cap/verify.py b/research/f7-five-label-sharp-cap/verify.py new file mode 100644 index 0000000000..d5491b092b --- /dev/null +++ b/research/f7-five-label-sharp-cap/verify.py @@ -0,0 +1,228 @@ +#!/usr/bin/env python3 +"""Check the sharp five-label cap and its finite proof steps. + +Prepared for Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +from collections import Counter +from functools import lru_cache, reduce +from hashlib import sha256 +from itertools import combinations, permutations +import json +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +FILES = ("README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py") +W4 = tuple(map(int, "012343234031")) +W5 = tuple(map(int, "012343103432")) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def differences(points): + return {a ^ b for a, b in combinations(points, 2)} + + +def affine_rank(points): + basis = {} + for p in points: + x = p ^ points[0] + while x: + bit = x.bit_length() - 1 + if bit not in basis: + basis[bit] = x + break + x ^= basis[bit] + return len(basis) + + +def support_checks(): + histograms = {} + count = 0 + for size, allowed in ((5, {3: {7}, 4: {10}}), + (6, {3: {7}, 4: {12, 15}}), + (7, {3: {7}, 4: {13, 15}})): + histogram = Counter() + for points in combinations(range(16), size): + rank = affine_rank(points) + support = len(differences(points)) + require(rank in allowed and support in allowed[rank], "support lemma") + histogram[support] += 1 + count += 1 + histograms[str(size)] = {str(k): v for k, v in sorted(histogram.items())} + require(count == 23816, "support domain count") + return {"subsets": count, "histograms": histograms} + + +def hamiltonian_cycle(points): + """Search the literal cube graph, without the quotient or excess rules.""" + points = tuple(sorted(points)) + size = len(points) + neighbors = [sum(1 << j for j, b in enumerate(points) + if (a ^ b).bit_count() == 1) for a in points] + if any(mask.bit_count() < 2 for mask in neighbors): + return False + full = (1 << size) - 1 + + @lru_cache(None) + def visit(last, used): + if used == full: + return bool(neighbors[last] & 1) + candidates = neighbors[last] & ~used + while candidates: + bit = candidates & -candidates + candidates ^= bit + if visit(bit.bit_length() - 1, used | bit): + return True + return False + + return visit(0, 1) + + +def quotient_check(projected, minority): + z = reduce(int.__xor__, projected) + even = {x for x in range(16) if x.bit_count() % 2 == 0} + require(z != 0 and z not in differences(projected), "missing direction") + shifted = {x ^ z for x in projected} + require(set(projected).isdisjoint(shifted) and set(projected) | shifted == even, + "quotient partition") + degrees = {u: sum((u ^ t).bit_count() == 1 for t in projected) + for u in range(16) if u.bit_count() % 2} + require(all(degrees[u] + degrees[u ^ z] == 4 for u in degrees), "degree sum") + require({z, z ^ 16} <= differences(minority), "missing lifts not covered") + levels = tuple(tuple(b & 15 for b in minority if b >> 4 == level) + for level in (0, 1)) + if tuple(map(len, levels)) != (2, 2): + return "unequal_levels" + same = next((level for level in (0, 1) if levels[level][0] ^ levels[level][1] == z), None) + require(same is not None, "same-level missing lift") + repeated = set(levels[0]) & set(levels[1]) + require(repeated, "repeated projection") + require(any(u in levels[same] and u ^ z in levels[same] for u in repeated), + "repeated projection lacks partner") + # Test every alternating order and injective block assignment directly. + for left in permutations(levels[0]): + for right in permutations(levels[1]): + cycle = (left[0], right[0], left[1], right[1]) + for blocks in permutations(projected): + legal = all((blocks[i] ^ cycle[i]).bit_count() == 1 and + (blocks[i] ^ cycle[(i + 1) % 4]).bit_count() == 1 + for i in range(4)) + require(not legal, "universal quotient cycle") + return "balanced_levels" + + +def set_checks(): + even = tuple(x for x in range(16) if x.bit_count() % 2 == 0) + odd_lifts = tuple(x for x in range(32) if (x & 15).bit_count() % 2) + counts = Counter() + control = None + for projected in combinations(even, 4): + majority = projected + tuple(t ^ 16 for t in projected) + da = differences(majority) + for minority in combinations(odd_lifts, 4): + counts["set_pairs"] += 1 + points = majority + minority + universal = len(differences(points)) == 31 + if not universal: + if control is None and hamiltonian_cycle(points): + control = list(points) + continue + counts["universal_sets"] += 1 + require(len(da) == 13, "universal majority support") + counts[quotient_check(projected, minority)] += 1 + require(not hamiltonian_cycle(points), "literal universal cube cycle") + counts["literal_graph_rejections"] += 1 + require(counts["set_pairs"] == 127400 and counts["universal_sets"] == 13664, + "set domain count") + require(control is not None, "missing nonuniversal positive graph control") + return {**dict(sorted(counts.items())), "nonuniversal_cycle_control": control} + + +def word_points(word): + require(len(word) == 12, "length") + require(all(type(label) is int and 0 <= label < 5 for label in word), "label") + points = [] + state = 0 + for label in word: + points.append(state) + state ^= 1 << label + require(state == 0, "restoration") + require(len(set(points)) == 12, "simplicity") + require(len(differences(points)) == 31, "universality") + return tuple(points) + + +def excess(points, mask): + classes = [tuple(x for x in points if (x & mask).bit_count() % 2 == bit) + for bit in (0, 1)] + return sum(len(c) * (len(c) - 1) // 2 - len(differences(c)) for c in classes) + + +def check_word(word, mask, cap=11): + require(type(mask) is int and 0 < mask < 32 and mask.bit_count() >= 4, "mask") + points = word_points(word) + value = excess(points, mask) + require(value <= cap, "cap") + require(hamiltonian_cycle(points), "positive graph control") + return value + + +def reject(action, reason): + try: + action() + except ValueError as error: + require(reason in str(error), "wrong rejection: " + str(error)) + return + raise ValueError("accepted control: " + reason) + + +def controls(): + require(check_word(W4, 23) == check_word(W5, 31) == 11, "sharpness") + for mask in (0, 1, 32, True): + reject(lambda: check_word(W4, mask), "mask") + for word, reason in ((W4[:-1], "length"), ((True,) + W4[1:], "label"), + ((5,) + W4[1:], "label"), (W4[:-1] + (0,), "restoration"), + ((0, 0, 1, 1, 2, 2, 3, 3, 4, 4, 0, 0), "simplicity"), + (tuple(map(int, "010201030203")), "universality")): + reject(lambda: word_points(word), reason) + reject(lambda: check_word(W4, 23, 10), "cap") + require(excess(word_points(W4), 1) == 21, "low-weight boundary") + points = (0, 3, 5, 9, 16, 19, 21, 25, 1, 14, 17, 30) + require(len(differences(points)) == 31 and excess(points, 15) == 18, + "set-only boundary") + require(not hamiltonian_cycle(points), "set-only graph boundary") + reject(lambda: require(excess(points, 15) <= 11, "set-only cap"), "set-only cap") + return {"semantic_rejections": 12, "weight_four_witness": W4, + "weight_five_witness": W5, "sharp_value": 11, + "low_weight_excess": 21, "set_only_excess": 18} + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit-receipt", action="store_true") + args = parser.parse_args() + actual = {"schema": "f7-five-label-sharp-cap/v1", "proved_cap": 11, + "supports": support_checks(), "sets": set_checks(), "controls": controls(), + "source_sha256": {f: sha256((PACKAGE / f).read_bytes()).hexdigest() for f in FILES}} + if args.emit_receipt: + print(json.dumps(actual, indent=2, sort_keys=True)) + return + stored = json.loads((PACKAGE / "RESULT.json").read_text(encoding="utf-8")) + require(canonical(actual) == canonical(stored), "receipt") + for value in (10, True): + changed = dict(actual, proved_cap=value) + reject(lambda: require(canonical(changed) == canonical(stored), "receipt"), "receipt") + print("PASS_F7_FIVE_LABEL_SHARP_CAP cap=11 support_sets=23816 " + "set_pairs=127400 universal_graphs=13664") + + +if __name__ == "__main__": + main() From 12a0105150f5f44a19a2199db8506d1aa44b009a Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Fri, 23 Oct 2026 00:41:58 -0500 Subject: [PATCH 2/2] Clarify the registered replay Python requirement --- research/f7-five-label-sharp-cap/README.md | 9 +++++---- research/f7-five-label-sharp-cap/RESULT.json | 2 +- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/research/f7-five-label-sharp-cap/README.md b/research/f7-five-label-sharp-cap/README.md index a7502283bd..1b80ac2196 100644 --- a/research/f7-five-label-sharp-cap/README.md +++ b/research/f7-five-label-sharp-cap/README.md @@ -194,12 +194,13 @@ we claim no new witness search result. ## Reproduction and evidence -Use Python 3.12 or later and the standard library: +Use Python 3.12 for the registered runner. The standalone verifier supports +Python 3.12 or later. Both use only the standard library: ```sh python3 -I -B research/f7-five-label-sharp-cap/verify.py python3 -I -O -W error -B research/f7-five-label-sharp-cap/verify.py -python3 -B scripts/research_package.py --package research/f7-five-label-sharp-cap +python3.12 -B scripts/research_package.py --package research/f7-five-label-sharp-cap ``` The standalone verifier imports no predecessor program. It checks all @@ -214,8 +215,8 @@ the stronger exclusion and its proof steps. The verifier checks both equality witnesses, invalid-input controls, a cap-ten rejection, a low-weight boundary, and a universal set that -has no required cycle. It also checks nonuniversal (8,4) cycles as -positive controls for the graph search. Normal replay recomputes the +has no required cycle. It also checks a nonuniversal (8,4) cycle as +a positive control for the graph search. Normal replay recomputes the complete receipt and compares it with RESULT.json. `--emit-receipt` prints the calculated receipt for explicit authoring. It writes no files. The receipt binds all five source files in this package. The standalone diff --git a/research/f7-five-label-sharp-cap/RESULT.json b/research/f7-five-label-sharp-cap/RESULT.json index f6bbfee4ff..3fd9c9609b 100644 --- a/research/f7-five-label-sharp-cap/RESULT.json +++ b/research/f7-five-label-sharp-cap/RESULT.json @@ -57,7 +57,7 @@ "universal_sets": 13664 }, "source_sha256": { - "README.md": "8d3703e4502e45b7423dc65e0e56b16eebc472c0f78412d262d340f640e0aa9c", + "README.md": "c03f524035f4abeb9103e7e43486ee75b83538e41abb50cd3beaecd01119f871", "SOURCES.json": "28f1729a2e27ccd772130e68ff7e6fc3faa210b0af077ca1b7423c4249916665", "TASK.json": "794d695cc1ee03e4ad8f87bc3f2f9988ee0210823f8d0f53c163f4f67b434677", "VERIFY.json": "61e345716563180730fd324bf9d6bd12074d6fccaabe63a0a4b76cb2ad2657bc",