diff --git a/research/f7-five-label-pruning-proof/README.md b/research/f7-five-label-pruning-proof/README.md new file mode 100644 index 0000000000..5d7494c9ac --- /dev/null +++ b/research/f7-five-label-pruning-proof/README.md @@ -0,0 +1,247 @@ +# Five-label high-weight pruning has a structural soundness proof + +**Scoped combinatorial proof with finite corroboration; no new kappa.** +For every simple restored universal singleton-prefix walk of length twelve +on F2^5, every label-basis functional of weight at least four has +separate-class pair-sum excess at most **15**. Thus the fixed L/2 +substitution cannot falsely prune such a word. + +This resolves the remaining (5,12) case of unpaidmoon's +[PR4148 Open next question 3](https://github.com/CrocSwap/integer-mult-bounds/pull/4148), +also handed off by Nick Petalas in +[PR4894](https://github.com/CrocSwap/integer-mult-bounds/pull/4894). +The new step is the quotient-cycle obstruction in the (8,4) split. +The earlier packages already measured soundness: that measurement is credited, +not presented as a new census result. + +Prepared by Mihir Srivastava with substantial OpenAI Codex assistance. +Apache-2.0. No independent human or formal proof-kernel review is claimed. + +## Definitions and theorem + +Let q_0=0 and q_(i+1)=q_i XOR e_(w_i), for twelve labels w_i in {0,...,4}. +Restored means q_12=0 and every coordinate is used; simple means +q_0,...,q_11 are distinct. Write S for these twelve states. +Universal means S+S=F2^5. For a nonzero functional f, let A and B be its +two classes in S and define + +```text +D(C) = {x XOR y : x,y in C, x != y} +X_f = C(|A|,2) + C(|B|,2) - |D(A)| - |D(B)|. +base(5,12) = 2 C(6,2) - (2^4-1) = 15. +``` + +A difference present in both classes is counted once in each support. +Universality implies D(A) union D(B) = ker(f) minus {0}, of size 15. +The claim is X_f <= 15 for weight(f) in {4,5}. It concerns complete +universal walks, not arbitrary twelve-point sets. + +## Proof + +**1. Matching balance, credited to PR4894.** +If f has weight four, let v be its omitted coordinate vector. +Exactly the v-edges preserve f, and those cube edges form a matching. +Let s=|A| >= t=|B|, let a,b count preserving cycle edges in A,B, +and let c count crossing edges. Cycle degrees give + +```text +2s = 2a+c, 2t = 2b+c, s-t = a-b, +2a <= s, 2b <= t. +``` + +Hence s-t <= a <= s/2, so s <= 2t. Since s+t=12, the only +unordered splits are (6,6), (7,5), (8,4). +If f has weight five, every edge flips f and its split is (6,6). +This restates the predecessor lemma so the proof is self-contained. + +**2. The (6,6) and (7,5) cases.** +At (6,6), the union of the two supports has size 15, so X_f <= 30-15=15. + +At (7,5), the 35 ordered cross pairs (a,b) have their sums in one +16-element coset. Two distinct pairs therefore have the same sum. +They must differ in both entries, and their equality supplies a nonzero +difference in D(A) intersect D(B). Consequently the sum of support +sizes is at least 15+1=16, and X_f <= 21+10-16=15. + +**3. Equality in matching balance fixes the (8,4) shape.** +Here a-b=4 and a<=4, forcing a=4, b=0 and c=8. +Every vertex of A is on one of four disjoint v-edges. Every vertex of B +has two crossing edges, so cyclic order consists of four blocks + +```text +B vertex -- A vertex --v-- A vertex -- B vertex. +``` + +In particular A is invariant under translation by v. +Delete the v coordinate. The projection T of A has four distinct points +in a parity coset of F2^4, an affine three-dimensional space. +After a cube translation, take that parity coset to be even. + +For any four distinct points, the six unordered pair sums are either +all distinct or have exactly three values. Equality between two pair +sums cannot share an endpoint, and is equivalent to XOR of all four +points being zero. In that case the points form an affine plane. +Thus |D(T)| is either 3 or 6, and lifting both v-levels gives + +```text +D(A) = {v} union {both v-lifts of each element of D(T)}, +|D(A)| = 1 + 2 |D(T)|. +``` + +If |D(T)|=3, then |D(A)|=7. Since four points B supply at most six +differences, their union has at most 13 elements. This contradicts +universality. Hence |D(T)|=6 and |D(A)|=13. + +If B is not an affine plane, |D(B)|=6 and +X_f = C(8,2)+C(4,2)-13-6 = 15. +It remains to exclude an affine-plane B. + +**4. A planar B contradicts the projected cycle.** +Suppose B is an affine plane, with three nonzero differences. +The two elements missing from D(A) in ker(f) minus {0} are a v-pair, +say z and z+v. Universality forces both into D(B). The three nonzero +differences of an affine plane are closed under addition, so its third +difference is v. Therefore B is also v-invariant. + +Its projection consists of two distinct odd vertices u,w in F2^4, and +u+w is the unique nonzero even direction missing from D(T). +Each u and w has two lifts among the four B vertices. +In the cyclic sequence of these four projected B vertices, there are +at least two transitions between u and w: a closed cycle visiting both +values must enter and leave each value. + +Each such transition passes through one of the four distinct projected +A vertices in T. That vertex is adjacent in the four-dimensional cube +to both u and w, since the two crossing edges toggle coordinates other +than v. Thus T contains at least two distinct common neighbors of u,w. + +Two distinct vertices of a cube have common neighbors only when their +Hamming distance is two. Then there are exactly two common neighbors, +and their XOR equals u+w. Both would lie in T, implying u+w in D(T). +This contradicts the missing direction. Planar B is impossible. + +All cases give X_f <= 15, proving soundness. The argument does not +assert that the upper bound 15 is attained by a universal walk. + +## Exact corroboration and boundaries + +The standalone verifier is written here without importing or executing +predecessor programs. It checks: + +- All 3,695 first-occurrence canonical simple closed words of length twelve + over at most five labels. Of these, 3,381 use all five labels and 828 + are universal. The other 314 closed words use four labels and cannot + cover F2^5. This explains the distinction between the two closed counts. +- All six high-weight functionals on the 828 universal words: + **4,968 cases**. Ordered-pair multiplicity and unordered-support + calculations agree. Matching and degree identities are checked on + all **22,170** closed-word/functional cases. +- All **127,400** v-invariant (8,4) set pairs for f=01111: + 70 projected majority subsets times 1,820 minority subsets. + Translation and coordinate symmetry cover the other orientations. + There are 13,664 universal sets. Of these, **224** have planar + minorities: 32 have zero and 192 have one projected common neighbor, + so none can realize the required two transitions. +- All **120** distinct vertex pairs in the four-dimensional cube check + the common-neighbor count and XOR identity used in the obstruction. +- Ten invalid-input or lowered-cap rejections, the low-weight boundary + below, the arbitrary-set boundary below, and two typed receipt mutations. + +The word enumeration uses only first-occurrence relabeling, simplicity and +the forced closing singleton edge. Every labeled word has a canonical +representative; all six masks are checked, so relabeling loses no functional. +There is no universality/excess prune or rotation reduction. +The verifier rechecks restoration and prefix sets separately. + +The measured maximum is **11 for each of the six masks**, consistent with +the predecessor soundness measurement. No universal (8,4) word occurs. +Those stronger observations remain finite evidence; the written theorem +proves the sufficient bound 15. + +The universal word `012343234031` has excess 11 at mask 10111 and +excess **21 > 15** at mask 00001. Dropping the weight hypothesis is invalid. +Dropping the cycle hypothesis is also invalid: the set with classes + +```text +A = {0,3,5,9,16,19,21,25} +B = {1,14,17,30}, f = 01111 +``` + +is universal, but its excess is **18 > 15**. Its projected minority vertices +have no common neighbor. This is a control for the exact step that +distinguishes the new proof from a false unrestricted set theorem. + +## Reproduction + +Use CPython 3.12 and the standard library, from the repository root: + +```sh +python -X utf8 -B scripts/research_package.py --package research/f7-five-label-pruning-proof +python -X utf8 -W error -I -B research/f7-five-label-pruning-proof/verify.py +python -X utf8 -W error -I -O -B research/f7-five-label-pruning-proof/verify.py +python -X utf8 -B scripts/check_research_commit.py --package research/f7-five-label-pruning-proof --check-source-history +``` + +Expected markers are `PASS_F7_FIVE_LABEL_PRUNING_PROOF`, +`PASS_REGISTERED_RESEARCH_PACKAGE` and `PASS_RESEARCH_COMMIT_BYTES`. +The normal and optimized commands recompute the evidence and compare the +entire canonical JSON payload to generated RESULT.json, including hashes of +the five source files. `--emit-receipt` emits a freshly calculated receipt +to stdout for explicit authoring; normal replay writes no files. +The standalone verifier needs neither Git nor network access. + +Checks ran locally on Windows with CPython 3.12.0. The small checks take +approximately one second each; this is not a performance improvement claim. +Enumeration uses a bounded iterative stack (depth eleven, at most five +extensions per node) and streams its domains. Python collections and +interpreter allocations are not instrumented. Explicit exceptions remain +active under -O. No Lean, Docker, seven-label census or selected cold replay +is required or claimed. + +## Provenance, overlap and remaining scope + +Canonical base is `624de9dc66858af0945e5f8a0942488d62280d43`, priority +revision 7. The `census-pruning-audit` card changes scope to this handoff's +missing structural implication. The current selected-source baseline +passed after materializing its sparse inputs. It is only source-binding +orientation. Selected kappa remains 60403/20000000. + +Credit unpaidmoon for PR4148's question, double-transversal proof and +excess convention; Nick Petalas for PR4894's matching-balance lemma and +PR3699/PR3733's measured classification; Nicholas Stone for PR2973's +parity correction; James Reed for PR3096's boundary audit; and Ross +Richardson for PR943's singleton-prefix model. The later five-label +length census retains unpaidmoon's credit. Merged documents are pinned +as provenance in SOURCES.json. The pending PR4894 README is an external +cited document at head `2e95d12a8f1557a90102314a773c74420bcbd4fe`; +it is not a runtime input or an unmerged Git-history dependency. + +The [canonical claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/4903) +records the handoff. Initial overlap coverage included 424 open PRs and +3,950 Discussion records with complete remote pagination. The sparse +initial scan covered only 5 of 6,319 local notes; relevant omitted f7 +successors were subsequently read. Live PR4894 and recent handoffs were +checked. PR4871 concerns receipt-domain binding at length 22, and PR3899 +concerns a partial union prune at (4,8); neither proves this statement. +The submission refresh covered 425 open PRs and 3,957 Discussion records, +with 51 of 6,319 local notes searched. No competing scoped proof was found. +Omitted notes, arbitrary diffs and unpublished work remain coverage limits. + +This result adds no engine change, seven-label exclusion, supplier +admission, all-size multiplication theorem or new kappa. The hypothesis +is simple restored universal length-twelve words in dimension five. +The 224 rejected set configurations show why adjacency and chronology +cannot be removed from this particular argument. + +## Open next questions + +1. Can one prove the measured sharper cap 11 and the absence of universal + (8,4) walks structurally? This would explain the remaining gap in the + sufficient bound. Start by analyzing nonplanar four-point minorities + in the same quotient cycle. The current proof permits excess 15 and + does not exclude all such configurations. +2. Can the matching-balance constraint produce a useful partial-prefix + prune in a maintained engine? First state the remaining-edge capacity + contract and prove that it retains every universal completion. + Correct completion bounds and a measured runtime benefit are absent; + this package does not enable a new pruning rule. diff --git a/research/f7-five-label-pruning-proof/RESULT.json b/research/f7-five-label-pruning-proof/RESULT.json new file mode 100644 index 0000000000..998371ad6e --- /dev/null +++ b/research/f7-five-label-pruning-proof/RESULT.json @@ -0,0 +1,166 @@ +{ + "controls": { + "input_and_cap_rejections": 10, + "low_weight_excess": 21, + "positive_mask": 23, + "positive_word": [ + 0, + 1, + 2, + 3, + 4, + 3, + 2, + 3, + 4, + 0, + 3, + 1 + ], + "set_only_excess": 18 + }, + "cube_neighbor_pairs": 120, + "proved_budget": 15, + "schema": "f7-five-label-pruning-proof/v1", + "set_envelope": { + "common_neighbors": { + "0": 32, + "1": 192 + }, + "pairs": 127400, + "universal_planar_minority": 224, + "universal_sets": 13664 + }, + "source_sha256": { + "README.md": "143ea4f63ee5d7f054adf63a21194b84ca0daacb84a76cbcc96298424edc7893", + "SOURCES.json": "9ae45f0810e826c40448fb42b04424a10cad373b2dd7aa3c04f7557064d31c3d", + "TASK.json": "87bf93561a480f1f7ad52d76b1bb1884da293ca2d55ef2c1195f9492b9a2b8d5", + "VERIFY.json": "75f8d72e62000b01454f334206803c6613e602a3bf669ff7a8f8ee6b69a7c2b2", + "verify.py": "c29fcc318796756e0454bf3377530207d8d6795d6748a82bffa3598ad4d8e6ae" + }, + "walks": { + "all_five_labels": 3381, + "canonical_closed": 3695, + "functional_checks": 4968, + "histogram": [ + { + "count": 432, + "excess": 3, + "split": [ + 6, + 6 + ], + "weight": 4 + }, + { + "count": 1392, + "excess": 6, + "split": [ + 6, + 6 + ], + "weight": 4 + }, + { + "count": 96, + "excess": 8, + "split": [ + 6, + 6 + ], + "weight": 4 + }, + { + "count": 132, + "excess": 11, + "split": [ + 6, + 6 + ], + "weight": 4 + }, + { + "count": 528, + "excess": 6, + "split": [ + 7, + 5 + ], + "weight": 4 + }, + { + "count": 816, + "excess": 8, + "split": [ + 7, + 5 + ], + "weight": 4 + }, + { + "count": 432, + "excess": 9, + "split": [ + 7, + 5 + ], + "weight": 4 + }, + { + "count": 312, + "excess": 11, + "split": [ + 7, + 5 + ], + "weight": 4 + }, + { + "count": 192, + "excess": 3, + "split": [ + 6, + 6 + ], + "weight": 5 + }, + { + "count": 552, + "excess": 6, + "split": [ + 6, + 6 + ], + "weight": 5 + }, + { + "count": 48, + "excess": 8, + "split": [ + 6, + 6 + ], + "weight": 5 + }, + { + "count": 36, + "excess": 11, + "split": [ + 6, + 6 + ], + "weight": 5 + } + ], + "matching_checks": 22170, + "maxima_by_mask": { + "15": 11, + "23": 11, + "27": 11, + "29": 11, + "30": 11, + "31": 11 + }, + "universal": 828 + } +} diff --git a/research/f7-five-label-pruning-proof/SOURCES.json b/research/f7-five-label-pruning-proof/SOURCES.json new file mode 100644 index 0000000000..4806d55bff --- /dev/null +++ b/research/f7-five-label-pruning-proof/SOURCES.json @@ -0,0 +1,63 @@ +{ + "schema_version": 1, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "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-codim-one-substitution-soundness/PROOF.md", + "usage": "provenance", + "git_blob": "0df5ca372839f27f1dc6c3b953c8766fde510ac7", + "sha256": "1f5b5fc5706a428411908db87cb6ff553d98afdbfda7bd95df6d4a4d9d855037" + }, + { + "path": "research/f7-codim-one-substitution-soundness/README.md", + "usage": "provenance", + "git_blob": "4abeb11e029017d6d9815cba0728fc65bfa2a5f2", + "sha256": "634d348ebc54fcf9437dc7844a70d6b56c68eb7b61990fb028f3ea6e0710f50c" + }, + { + "path": "research/f7-weight-parity-census-correction/MATH.md", + "usage": "provenance", + "git_blob": "e0207d8ebd903dc584862a2d6d500b59f3134490", + "sha256": "13f1234de6b7bd9f5afbe9a8892fc1d7f47eae0eddf098d19331a561c750e06a" + }, + { + "path": "research/f7-bit0-functional-classification/README.md", + "usage": "provenance", + "git_blob": "4618c68ffc94be30055537bca4e49696946437dc", + "sha256": "8176c8a889671f67ebcd6f1b9e9efddae55cfbbff4b486442a9b63977e9c4844" + }, + { + "path": "research/f7-functional-independent-check/README.md", + "usage": "provenance", + "git_blob": "e13182fe15b3fb0c253bc02e272fcab61b46b354", + "sha256": "418af63ad914cea3a5935b8c66bd32f9a91b8db25a958fc71b6d6096a3dac5f3" + }, + { + "path": "research/f7-firing-n5-length-census/README.md", + "usage": "provenance", + "git_blob": "d44d8dfeb22a32d8d290f9ef8ee70362a8709489", + "sha256": "50416cd940c1db7acc738c9819ae6ce680d32c0e1e147bbc19ed2ccfa7f8e4b5" + } + ], + "cited_external_document": { + "pr": 4894, + "author": "Nick Petalas", + "head": "2e95d12a8f1557a90102314a773c74420bcbd4fe", + "path": "research/f7-four-stay-pruning/README.md", + "git_blob": "3521be1e9e02a4cacd3db17c80a2688e01973dee", + "url": "https://github.com/petalas/integer-mult-bounds/blob/2e95d12a8f1557a90102314a773c74420bcbd4fe/research/f7-four-stay-pruning/README.md", + "usage": "Attribution for matching balance and the live handoff only. The lemma is restated and proved locally. No executable or source-history dependency." + } +} diff --git a/research/f7-five-label-pruning-proof/TASK.json b/research/f7-five-label-pruning-proof/TASK.json new file mode 100644 index 0000000000..baa9697f23 --- /dev/null +++ b/research/f7-five-label-pruning-proof/TASK.json @@ -0,0 +1,141 @@ +{ + "schema_version": 1, + "task_id": "census-pruning-audit", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "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 high-weight fixed L/2 substitution soundness for simple restored universal five-label length-twelve walks.", + "scope_change_reason": "Take the explicit remaining (5,12) proof handoff in #4894 and #4148, rather than replaying an old seven-label engine or its existing measured table.", + "bottleneck_link": "A scoped proof explains one validity boundary of the erroneous fixed-budget substitution; it does not revalidate the seven-label exclusions or improve a supplier.", + "budget_minutes": 60, + "stop_rule": "Stop after the structural bound 15, bounded exact corroboration and meaningful controls. No seven-label census, engine integration or selected-frontier change.", + "outcome": "completed", + "evidence": "Written quotient-cycle proof; 3695 canonical closed words, 828 universal words and 4968 functional checks; 127400 set pairs and 224 planar-minority obstructions; normal/optimized registered checks and source-bound generated RESULT.json.", + "author": "Mihir Srivastava", + "ai_assistance": "Substantial OpenAI Codex assistance for research, proof writing, implementation, verification and publication. No independent human or formal proof-kernel review.", + "open_questions": [ + { + "question": "Can the measured sharp cap 11 and absence of universal (8,4) walks be proved structurally?", + "why_it_matters": "Closes the gap between the sufficient soundness proof and the bounded observations.", + "first_step": "Analyze nonplanar four-point minorities in the same quotient cycle.", + "blocked_by": "The present argument permits excess 15 in this case." + }, + { + "question": "Can matching balance improve a maintained partial-prefix prune?", + "why_it_matters": "Might reduce future enumeration without rejecting a universal completion.", + "first_step": "Specify remaining-edge capacities and prove a completion bound before integration.", + "blocked_by": "No partial-prefix contract or measured runtime benefit is supplied." + } + ], + "canonical_discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4903", + "environment": { + "python": "3.12.0", + "platform": "win32", + "dependencies": "standard library only" + }, + "selection": { + "mode": "handoff-first", + "handoff": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19134387", + "source_pr": 4894, + "source_head": "2e95d12a8f1557a90102314a773c74420bcbd4fe", + "priority_revision": 7 + }, + "unrun_obligations": [ + "Independent human proof review", + "Formal proof-kernel verification", + "Seven-label census", + "Pruning-engine integration", + "Selected cold replay", + "Supplier admission" + ], + "overlap": { + "searched_at": "2026-10-22T23:22:49.586554+00:00", + "coverage": { + "open_prs": { + "fetched_at": "2026-10-22T23:21:25.061403+00:00", + "complete_pagination": true, + "records": 424 + }, + "discussions": { + "fetched_at": "2026-10-22T23:22:47.832426+00:00", + "complete_pagination": true, + "records": 3950 + } + }, + "local_initial": { + "head": "624de9dc66858af0945e5f8a0942488d62280d43", + "records": 5, + "head_records": 6319, + "complete_head_inventory": false + }, + "followup": "Materialized and read f7 classification, independent check, codimension-one proof, later five-label census, threshold and set/word boundary notes; read live #4894 and latest handoffs.", + "limits": "Sparse omitted notes, arbitrary diffs and unpublished work." + }, + "submission_refresh": { + "checked_at": "2026-10-22T23:34:21.334238+00:00", + "canonical_main": "624de9dc66858af0945e5f8a0942488d62280d43", + "priority_revision": 7, + "guidance_change": false, + "coverage": { + "local": { + "head": "624de9dc66858af0945e5f8a0942488d62280d43", + "records": 51, + "head_records": 6319, + "complete_head_inventory": false + }, + "open_prs": { + "fetched_at": "2026-10-22T23:33:00.814843+00:00", + "complete_pagination": true, + "records": 425 + }, + "discussions": { + "fetched_at": "2026-10-22T23:34:21.146031+00:00", + "complete_pagination": true, + "records": 3957 + } + }, + "decision": "Continue the same claimed proof; no competing scoped result found." + } +} diff --git a/research/f7-five-label-pruning-proof/VERIFY.json b/research/f7-five-label-pruning-proof/VERIFY.json new file mode 100644 index 0000000000..fd39b5df20 --- /dev/null +++ b/research/f7-five-label-pruning-proof/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-X", + "utf8", + "-W", + "error", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Written-proof corroboration: complete bounded word and set domains, positive and negative semantic controls, typed full source-bound receipt comparison." + }, + { + "argv": [ + "{python}", + "-X", + "utf8", + "-W", + "error", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "The same evidence and failure controls with Python assertions disabled." + } + ] +} diff --git a/research/f7-five-label-pruning-proof/verify.py b/research/f7-five-label-pruning-proof/verify.py new file mode 100644 index 0000000000..8051c7ac37 --- /dev/null +++ b/research/f7-five-label-pruning-proof/verify.py @@ -0,0 +1,264 @@ +#!/usr/bin/env python3 +"""Exact corroboration of the five-label proof; no predecessor code is used. + +Mihir Srivastava, with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +from collections import Counter +from hashlib import sha256 +from itertools import combinations +import json +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +MASKS = (15, 23, 27, 29, 30, 31) +SOURCE_FILES = ("README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py") +WITNESS = (0, 1, 2, 3, 4, 3, 2, 3, 4, 0, 3, 1) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def differences(points): + return {x ^ y for x, y in combinations(points, 2)} + + +def excess(points, mask): + classes = tuple(tuple(x for x in points if (x & mask).bit_count() % 2 == bit) + for bit in (0, 1)) + supports = tuple(differences(c) for c in classes) + value = sum(len(c) * (len(c) - 1) // 2 - len(d) + for c, d in zip(classes, supports)) + return value, classes, supports + + +def prefix_points(word): + require(len(word) == 12, "length must be twelve") + require(all(type(c) is int and 0 <= c < 5 for c in word), "invalid label") + require(set(word) == set(range(5)), "all five labels must occur") + points = [0] + state = 0 + for label in word: + state ^= 1 << label + points.append(state) + require(state == 0, "word is not restored") + require(len(set(points[:-1])) == 12, "word is not simple") + return tuple(points[:-1]) + + +def check_word(word, mask, cap=15): + require(type(mask) is int and mask in MASKS, "functional must have weight >=4") + points = prefix_points(word) + require(len(differences(points)) == 31, "word is not universal") + value, classes, _ = excess(points, mask) + require(value <= cap, "excess exceeds claimed cap") + # A separate ordered-pair multiplicity calculation checks the definition. + ordered = sum(sum(count // 2 - 1 for count in Counter( + x ^ y for x in c for y in c if x != y).values()) for c in classes) + require(value == ordered, "unordered and ordered excess disagree") + return value, classes + + +def canonical_cycles(): + """Every length-12 simple closed word up to first-occurrence relabeling. + + Only simplicity and the forced final singleton edge filter the traversal. + No excess, universality, parity-budget or rotation prune is used. + """ + stack = [((), (0,), 1, -1)] + while stack: + word, points, seen, highest = stack.pop() + if len(word) == 11: + last = points[-1] + if last and last & (last - 1) == 0: + yield word + (last.bit_length() - 1,), points + continue + for label in range(min(highest + 1, 4) + 1): + state = points[-1] ^ (1 << label) + if not (seen >> state) & 1: + stack.append((word + (label,), points + (state,), + seen | (1 << state), max(highest, label))) + + +def matching_identities(word, points, mask): + _, classes, _ = excess(points, mask) + sizes = tuple(map(len, classes)) + stays = [0, 0] + crossing = 0 + for index, label in enumerate(word): + bit = (points[index] & mask).bit_count() % 2 + if mask & (1 << label): + crossing += 1 + else: + stays[bit] += 1 + require(all(2 * sizes[b] == 2 * stays[b] + crossing for b in (0, 1)), + "cycle degree identity failed") + if mask != 31: + require(all(2 * stays[b] <= sizes[b] for b in (0, 1)), "not a matching") + require(max(sizes) <= 2 * min(sizes), "matching balance failed") + else: + require(sizes == (6, 6), "all-ones functional must alternate") + + +def walk_checks(): + closed = full_alphabet = universal = checks = 0 + histogram = Counter() + maxima = {mask: -1 for mask in MASKS} + for word, points in canonical_cycles(): + closed += 1 + full_alphabet += len(set(word)) == 5 + for mask in MASKS: + matching_identities(word, points, mask) + if len(differences(points)) != 31: + continue + universal += 1 + require(prefix_points(word) == points, "enumeration prefix mismatch") + for mask in MASKS: + value, classes = check_word(word, mask) + split = tuple(sorted(map(len, classes), reverse=True)) + histogram[(mask.bit_count(), split, value)] += 1 + maxima[mask] = max(maxima[mask], value) + checks += 1 + require((closed, full_alphabet, universal, checks) == (3695, 3381, 828, 4968), + "bounded walk census changed") + require(set(maxima.values()) == {11}, "measured high-weight maximum changed") + return {"canonical_closed": closed, "all_five_labels": full_alphabet, + "universal": universal, "functional_checks": checks, + "matching_checks": closed * 6, "maxima_by_mask": maxima, + "histogram": [{"weight": key[0], "split": key[1], "excess": key[2], + "count": count} for key, count in sorted(histogram.items())]} + + +def projected_plane_obstruction(majority, minority): + """Check the finite ingredients of the proof's planar-minority contradiction.""" + v = 16 + require({x ^ v for x in majority} == set(majority), "majority not v-invariant") + require(len(differences(majority)) == 13, "wrong majority support") + require(len(differences(minority)) == 3, "minority is not an affine plane") + require({x ^ v for x in minority} == set(minority), "minority not v-invariant") + projected = {x & 15 for x in majority} + endpoints = sorted({x & 15 for x in minority}) + require(len(endpoints) == 2, "expected two projected minority vertices") + z = endpoints[0] ^ endpoints[1] + require(z not in differences(projected), "missing direction is already present") + common = {x for x in projected if all((x ^ u).bit_count() == 1 for u in endpoints)} + require(len(common) < 2, "two cross-fiber transitions would be possible") + return len(common) + + +def cube_neighbor_checks(): + pairs = 0 + for u, w in combinations(range(16), 2): + common = [x for x in range(16) + if (x ^ u).bit_count() == 1 and (x ^ w).bit_count() == 1] + require(len(common) == (2 if (u ^ w).bit_count() == 2 else 0), + "cube common-neighbor count") + if common: + require(common[0] ^ common[1] == u ^ w, "common-neighbor difference") + pairs += 1 + return pairs + + +def set_checks(): + """All v-invariant (8,4) pairs at f=01111; coordinate symmetry covers the rest.""" + even = [x for x in range(16) if x.bit_count() % 2 == 0] + odd = [x for x in range(32) if (x & 15).bit_count() % 2 == 1] + cases = universal = planes = 0 + common_counts = Counter() + for projected in combinations(even, 4): + majority = projected + tuple(x ^ 16 for x in projected) + da = differences(majority) + require(len(differences(projected)) in (3, 6), "four-point support lemma") + require(len(da) == 1 + 2 * len(differences(projected)), "lift support lemma") + for minority in combinations(odd, 4): + cases += 1 + db = differences(minority) + require(len(db) in (3, 6), "four-point support dichotomy failed") + if len(da | db) != 15 or len({a ^ b for a in majority for b in minority}) != 16: + continue + universal += 1 + require(len(da) == 13, "planar majority cannot be universal") + if len(db) == 3: + planes += 1 + common_counts[projected_plane_obstruction(majority, minority)] += 1 + else: + require(34 - len(da) - len(db) == 15, "nonplanar split cap") + require((cases, universal, planes) == (127400, 13664, 224), "set envelope changed") + require(common_counts == {0: 32, 1: 192}, "planar obstruction counts changed") + return {"pairs": cases, "universal_sets": universal, + "universal_planar_minority": planes, "common_neighbors": common_counts} + + +def must_reject(action, reason): + try: + action() + except ValueError as error: + require(reason in str(error), "rejected for the wrong reason: " + str(error)) + return + raise ValueError("negative control was accepted: " + reason) + + +def controls(): + for mask in (0, 1, 32, True): + must_reject(lambda: check_word(WITNESS, mask), "functional") + for word, reason in ( + (WITNESS[:-1], "length"), ((True,) + WITNESS[1:], "label"), + ((5,) + WITNESS[1:], "label"), (WITNESS[:-1] + (0,), "restored"), + ((0, 0, 1, 1, 2, 2, 3, 3, 4, 4, 0, 0), "simple"), + ): + must_reject(lambda: check_word(word, 23), reason) + must_reject(lambda: check_word(WITNESS, 23, cap=10), "cap") + points = prefix_points(WITNESS) + require(check_word(WITNESS, 23)[0] == 11, "positive fixture") + require(excess(points, 1)[0] == 21, "low-weight boundary control") + majority = (0, 3, 5, 9, 16, 19, 21, 25) + minority = (1, 14, 17, 30) + require(len(differences(majority + minority)) == 31, "set control not universal") + value = excess(majority + minority, 15)[0] + require(value == 18, "set-only counterexample changed") + must_reject(lambda: require(value <= 15, "set-only cap"), "set-only cap") + require(projected_plane_obstruction(majority, minority) == 0, "set obstruction") + return {"input_and_cap_rejections": 10, "low_weight_excess": 21, + "set_only_excess": 18, "positive_word": WITNESS, "positive_mask": 23} + + +def payload(): + return {"schema": "f7-five-label-pruning-proof/v1", "proved_budget": 15, + "walks": walk_checks(), "set_envelope": set_checks(), "controls": controls(), + "cube_neighbor_pairs": cube_neighbor_checks(), + "source_sha256": {name: sha256((PACKAGE / name).read_bytes()).hexdigest() + for name in SOURCE_FILES}} + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")) + + +def check_receipt(actual, expected): + # Canonical JSON comparison also distinguishes bool from int and int from float. + require(canonical(actual) == canonical(expected), "receipt differs from fresh evidence") + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit-receipt", action="store_true") + args = parser.parse_args() + actual = payload() + if args.emit_receipt: + print(json.dumps(actual, indent=2, sort_keys=True)) + return + receipt = (PACKAGE / "RESULT.json").read_bytes() + require(len(receipt) < 65536, "receipt too large") + check_receipt(actual, json.loads(receipt)) + for key, value in (("proved_budget", 14), ("proved_budget", True)): + mutant = dict(actual) + mutant[key] = value + must_reject(lambda: check_receipt(actual, mutant), "receipt") + print("PASS_F7_FIVE_LABEL_PRUNING_PROOF universal=828 functionals=4968 " + "set_pairs=127400 planar_obstructions=224 proved_budget=15 measured_max=11") + + +if __name__ == "__main__": + main()