diff --git a/research/five-label-prefix-completion/.gitattributes b/research/five-label-prefix-completion/.gitattributes new file mode 100644 index 0000000000..1790f24748 --- /dev/null +++ b/research/five-label-prefix-completion/.gitattributes @@ -0,0 +1,2 @@ +* text eol=lf +reference5001.* -text diff --git a/research/five-label-prefix-completion/LICENSE b/research/five-label-prefix-completion/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/five-label-prefix-completion/LICENSE @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/research/five-label-prefix-completion/OVERLAP.json b/research/five-label-prefix-completion/OVERLAP.json new file mode 100644 index 0000000000..0982374a25 --- /dev/null +++ b/research/five-label-prefix-completion/OVERLAP.json @@ -0,0 +1,54 @@ +{ + "status": "POSSIBLE_OVERLAP_NOT_A_NOVELTY_CERTIFICATE", + "searched_at": "2026-10-23T06:08:41.222792+00:00", + "terms": [ + "partial-prefix", + "completion bound", + "restored universal", + "4907", + "4992" + ], + "coverage": { + "local": { + "head": "bee95ce88f9f19802f0613f92838895cd0e14a1f", + "records": 6690, + "head_records": 6690, + "complete_head_inventory": true, + "unsearched_head_paths": [] + }, + "open_prs": { + "fetched_at": "2026-10-23T06:05:40.770277+00:00", + "complete_pagination": true, + "records": 309 + }, + "discussions": { + "fetched_at": "2026-10-23T06:08:40.832430+00:00", + "complete_pagination": true, + "records": 4096 + } + }, + "warnings": [], + "limits": "Remote PR scope is open PRs including drafts. Closed work is searched through local READMEs, TASK metadata and ledger only. Local coverage compares searched working-tree notes with regular note paths at coverage.local.head; it does not certify HEAD contents or historical coverage. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission.", + "active_related_claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4903#discussioncomment-19139042", + "scope_separation": "That claim bounds preserving edges and endpoint degrees; this study bounds jointly reachable future-pair XOR support. Neither condition is assumed to dominate the other.", + "extra_reads": [ + "PR4992 exact head 12a0105150f5f44a19a2199db8506d1aa44b009a", + "PR4907", + "PR3899", + "research/f7-union-support-audit/README.md", + "research/f7-one-point-pair-ceiling/README.md", + "research/f7-firing-threshold-all-n/README.md", + "research/f7-monotone-firing-classification/README.md", + "research/prefix-budget-counterexample/README.md" + ], + "dedup_limit": "No competing exact reachable-tail pair envelope identified in inspected metadata/notes. Arbitrary diffs, unpublished work and all closed PR bodies were not fully searched. Literal numeric terms generated unrelated matches and were manually filtered.", + "final_targeted_refresh": { + "at": "2026-10-23T06:37:34Z", + "main": "f259dabc7d70e0db8d6d36bfda888f008bbfecc1", + "guidance_and_selection_changed": false, + "matching_pr": 5001, + "matching_head": "fe3226ea4e36469f43c6b116c5b98cc221a9b1af", + "integration_claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4903#discussioncomment-19139518", + "scope": "Latest Discussion4903 comments, exact PR4992/5000 states and recent 100 open PR metadata; not a second complete remote census." + } +} diff --git a/research/five-label-prefix-completion/PROOF.md b/research/five-label-prefix-completion/PROOF.md new file mode 100644 index 0000000000..1f504817b2 --- /dev/null +++ b/research/five-label-prefix-completion/PROOF.md @@ -0,0 +1,184 @@ +# Remaining-tail pair-support envelope + +Prepared for SHIN09-git with substantial OpenAI Codex assistance. Apache-2.0. +This is a scoped elementary lemma and finite corroboration, not proof-kernel or +independent human acceptance. + +## Contract + +Let q_0=0,q_1,...,q_k be a simple path in the n-dimensional binary cube: +each edge flips one coordinate and all displayed vertices are distinct. +Seek a simple closed walk of total length L extending this prefix, with q_L=0 +and all L nonclosing vertices distinct. Put r=L-k and m=r-1. A universal +completion requires every vector to be a pairwise XOR of its nonclosing vertices. +The closing zero is already present; it is not an additional new point. + +Write d for Hamming distance, P={q_0,...,q_k}, and + + U = {x not in P : d(q_k,x) + d(x,0) <= r}. + +For distinct x,y in U, put + + T(x,y) = d(x,y) + min(d(q_k,x)+d(y,0), d(q_k,y)+d(x,0)). + +Define the nonzero difference envelope + + E2 = D(P) + union {p XOR x : p in P, x in U} + union {x XOR y : distinct x,y in U, T(x,y) <= r}, + +where D(P) is the set of differences of distinct points. The one-vertex +relaxation E1=D(P union U) ignores the shared tail budget of two future points. + +**Necessary completion condition:** |U| >= m and E2 contains every nonzero +vector. Therefore a strict failure of either condition safely rejects the prefix. +Passing is inconclusive. E2 is a subset of E1. + +## Proof + +Every new nonclosing vertex x lies after q_k and before the final zero. The +numbers of edges on those two subpaths sum to r and dominate their Hamming +distances. Thus x belongs to U. Simplicity requires m distinct new vertices +outside P, proving the cardinality condition. + +Consider any difference in an actual completion. Two old endpoints contribute +to D(P). An old and new endpoint contribute to the second set. For two new +endpoints, one occurs first on the suffix. If x precedes y, the three consecutive +subpaths q_k to x, x to y, and y to zero have total length r. Their distances sum +to at most r, so T(x,y)<=r. The opposite order is the second term of the minimum. +Thus every actual nonzero difference is in E2. Universality requires all of them. + +The argument uses only necessary distance inequalities. It does not assert that +the vertices or pair choices in the envelope can be realized together. It may +allow repeated vertices, nonchronological choices and mutually incompatible +tails in its relaxation. Those permissions enlarge the envelope and cannot +produce a false rejection. Coordinate relabeling preserves all these conditions. + +This proof does not use a functional partition, the cap 11, matching-edge +capacities, or any selected multiplication construction. The exposed verifier +enforces small bounded inputs; the finite evidence below is not a general +performance claim. + +## Simplification and a strict three-edge witness + +### Exact simplification: no future-pair loop is needed + +In fact E2 equals D(P) union {p XOR x : p in P, x in U}. +For any compatible future pair, put z=x XOR y and t=q_k XOR z. +If x occurs first, the triangle inequality gives + + d(q_k,t)+d(t,0) + = weight(z)+weight(q_k XOR x XOR y) + <= d(x,y)+d(q_k,x)+d(y,0) <= r. + +The reversed order gives the same conclusion. If t is already in P, z is +an old-old difference (t is not q_k because z is nonzero). Otherwise t belongs +to U, so z=q_k XOR t is an old-new difference. Thus every term added by the +joint future-pair loop is already present. Removing that loop is an exact +algebraic simplification, not an additional prune or weakened condition. + +The final implementation uses this formula. A separate ordered-route checker +reconstructs the original E2 at all 21,640 prefixes and checks exact equality. +This simplification was found when a max-instead-of-min pair-route mutation +survived full envelope checks: any subset of the redundant pair terms gives +the same union. That mutation is correctly excluded from the final mutation +suite; the suite tests the actual simplified predicate's behavior instead. + +### Literal witness + +At the prefix word 010201320, + + P = (0,1,3,2,6,7,5,13,9,8), q_k=8, r=3, + U = (4,10,12,16,24). + +The one-vertex envelope covers all 31 nonzero masks. The only distinct future +pairs with T(x,y)<=3 are {4,12} and {16,24}. The two-vertex envelope misses +20 and 28. For example, the tempting pair {4,16} has T=5, so its difference +20 cannot be generated by two new points within the three remaining edges. + +The only simple restored three-step suffixes are 232 and 434. Neither +completion is universal; the first uses four labels and the second five. +The verifier checks all 5^3 suffixes. Existing remaining-label, parity-union +and cap-11 tests pass this prefix. + +## Auxiliary excess lower bound, with no incremental benefit in this domain + +This separate trial DOES depend on the final class sizes supplied by the +five-label cap context: (6,6) at weight five; (5,7),(6,6),(7,5) at weight four. +It is not part of E2's proof or timed traversal. + +For each functional class b, let a_b=|P_b|, d_b=|D(P_b)| and +h_b=|D(P_b union U_b)|. For a possible final size s_b, its support is at most + + v_b = min(h_b, d_b + C(s_b,2)-C(a_b,2)). + +The second bound holds because each additional pair introduces at most one +new difference. Hence final separate-class excess is at least + + sum_b C(s_b,2) - sum_b v_b. + +Minimize this lower bound over the listed size assignments with +a_b <= s_b <= a_b+|U_b|. No assignment means no completion in that stated +class-size contract. A minimum greater than 11 is a necessary rejection. + +This trial rejects no additional prefix beyond the remaining-label, parity-union, +cap-11 and E1 controls on the complete 21,640-prefix domain. Its code and exact +negative classification remain reproducible; no engine integration is justified +by that trial. + +## Comparison premises and enumeration completeness + +The cheap comparison uses the credited PR3005 union-capacity inequalities. +At weight parity, a length-12 simple cycle has final class sizes (6,6). +Current sizes a,b and support union V require + + |V| + 30 - C(a,2)-C(b,2) >= 15, + |cross_support| + 36 - a*b >= 16. + +Restoration and use of every coordinate also require +popcount(q_k)+2*(5-used_labels)<=r. These are existing necessary conditions. + +The cap-11 comparison is explicitly limited to five labels, length twelve +and weight-four/five functionals. It is credited to Ali Romman's PR4992 +(exact head 12a0105150f5f44a19a2199db8506d1aa44b009a), following Mihir Srivastava +and Nick Petalas. Adding a point cannot lower pair excess: it adds a pairs and +at most a new differences. Therefore a complete-walk upper cap may reject a +prefix already exceeding it. The cap itself is not a new result here, and +our distance lemma does not inherit its proof obligations. + +The DFS uses first-occurrence label order, simplicity and the forced final +singleton edge. Every labeled word has one representative under coordinate +permutation. No rotation/reversal quotient is used. The independent oracle +instead partitions the twelve positions into at most five nonempty even blocks, +ordered by their first positions. Restoration is equivalent to even block +sizes, so this enumerates every canonical restored word without a prefix +feasibility rule. Literal simple-state and XOR-coverage checks then select its +closed and universal sets. The entire sets, not just their counts, must match. +This representation is credited to Nick Petalas's PR3005; this implementation +does not import his code. + +Every actual completion's future points and pair differences are checked against +E2 at every prefix. Additional raw-word controls scan 3^6 and 4^8 words without +canonical symmetry reduction. None of this runs or validates a seven-label +census, a maintained engine, a supplier, or the full multiplication theorem. + + +## Exact comparison boundary for the later matching-capacity result + +PR5001 was completed during this session's initial snapshot and discovered at +the final targeted refresh. Its original full source and proof are retained +byte-for-byte. Only feasible_splits is invoked; this is not its registered replay. + +compare_matching.py independently transcribes the stated finite predicate. +It enumerates the even final crossing count C, checks c<=C<=c+r+1 and at least +two crossings when both final classes are nonempty, and checks the required +stay counts s_j-C/2 against existing stays plus available matching edges. +Its edge-capacity calculation maximizes over how many one-new-vertex edges +are chosen, instead of copying the original greedy expression. All 108,195 +predicate outputs agree exactly. The complete actual simple-cycle splits are +also checked for containment. + +The 67 earlier strict examples all pass this matching predicate. No claim is +made that the predicates are incomparable in every dimension, or that their +combination improves runtime. The maintained-engine integration claimed in +Discussion4903 comment19139518 is another contributor's task. diff --git a/research/five-label-prefix-completion/PUBLICATION.md b/research/five-label-prefix-completion/PUBLICATION.md new file mode 100644 index 0000000000..9213cd93af --- /dev/null +++ b/research/five-label-prefix-completion/PUBLICATION.md @@ -0,0 +1,23 @@ +# Publication checkpoint — October 28, 2026 + +This directory preserves the October 23 research session and its source-bound +receipt unchanged. In particular, TASK.json's `local-only` publication field +and priority revision 7 describe that original checkpoint; they are historical, +not a statement that the present contribution remains unpublished. + +The contribution is now prepared on canonical main +`721c03822c421b7f7fcbb2598993b947c4d88419` (priority revision 8). The selected +record is now PR6030, kappa 781451/250000000. This package makes no claim about +that construction and does not change the selected record or maintained census. + +The registered normal and optimized verifiers were freshly replayed on this +base on October 28, both returning +`PASS_FIVE_LABEL_PREFIX_COMPLETION prefixes=21640 universal=828 joint_extra=67`. +The original 19 package files passed the committed-byte check before this note +was added. This note adds no scientific input or changed experimental result. + +The October 23 timings remain historical local measurements: the simplified +predicate is 9.25% slower than the cheap-bound baseline in the median adjacent +paired comparison. No current-machine retiming or practical speedup is claimed. +Original credit, frozen PR5001 comparison, full-domain proof and stop decision +remain in README.md, PROOF.md, SOURCES.json and RESULT.json. diff --git a/research/five-label-prefix-completion/README.md b/research/five-label-prefix-completion/README.md new file mode 100644 index 0000000000..1f3be2eab0 --- /dev/null +++ b/research/five-label-prefix-completion/README.md @@ -0,0 +1,180 @@ +# A two-vertex tail envelope for five-label prefix completion + +Local research prepared for SHIN09-git with substantial OpenAI Codex assistance. +Apache-2.0. No new kappa, supplier, seven-label census or maintained-engine change. + +## Result + +A remaining-edge distance bound can safely reject a partial singleton walk +when it can no longer supply every required pairwise XOR. Checking two future +points against their **shared** tail budget is stronger than checking their +individual reachability. [PROOF.md](PROOF.md) gives the full implication and +the explicit prefix 010201320, which passes the old controls but cannot supply +masks 20 and 28. + +The pair constraint has an exact simplification: every jointly reachable +future-pair difference already equals a difference between the current endpoint +and a point that is either old or individually reachable. The final kernel +therefore needs no future-pair loop. The original ordered-route formula is +checked separately for equality on all 21,640 prefixes. + +At five labels and length twelve: + +| Standalone comparison traversal | Entered prefixes | Universal words | +|---|---:|---:| +| Unpruned canonical traversal | 21,640 | 828 | +| Existing remaining-label and parity-union bounds | 14,317 | 828 | +| Those bounds plus credited cap 11 | 13,990 | 828 | +| Also individual future-vertex reachability | 7,519 | 828 | +| Also the shared two-vertex tail constraint | 7,326 | 828 | +| Cheap bounds plus individual reachability, without cap 11 | 7,543 | 828 | +| Cheap bounds plus shared tail constraint, without cap 11 | 7,350 | 828 | + +The two-vertex rule rejects 67 partial prefixes that pass the remaining-label, +union, cap-11 and individual-vertex tests in the full prefix domain. In the +pruned traversal this removes 193 additional entered nodes (2.57% relative to +7,519). Prefix counts are exact; they are not elapsed-time savings. + +The separately implemented even-position-block oracle checks 139,954 restored +canonical words using at most five labels. It independently returns the same +3,695 simple closed words and all 828 universal words. The full witness sets +are compared and their hashes recorded. Every complete simple word is checked +at all twelve prefix depths: 44,340 completion checks, including 9,936 universal +completion checks and 2,427 distinct live prefixes. + +A second trial converts possible per-class difference support into a lower +bound on final collision excess. It adds zero rejections beyond the existing +controls and the individual-vertex envelope in this complete domain. It is +retained as a negative result, not integrated into the traversal. + +## Scope and decision + +The core distance lemma needs a simple path, singleton coordinate steps, +a fixed closing vertex and total length, and pair-XOR universality. Its proof +does not use cap 11 or the concurrently claimed matching-capacity lemma. +Passing the bound does not construct a completion. No claim of mathematical +novelty for triangle inequalities is made. + +The executable study is bounded to the five-label, length-twelve comparison +and raw controls at (3,6) and (4,8). It does not establish practical usefulness +at seven labels. The stronger predicate is sound but is not recommended for integration in its current implementation; the complete timing comparison below is negative. + +## Complete runtime measurements and stop decision + +TIMINGS-FINAL.json records 147 sequential fresh Python processes: 21 adjacent +blocks of seven modes, with rotating/reversed order. Startup, imports, source +reading, full traversal and output are included. No verification suite ran +concurrently. OS caches were not flushed; other host contention was uncontrolled. +These are descriptive local measurements, not timing thresholds. + +| Mode | Median full process time | +|---|---:| +| Unpruned | 0.180372 s | +| Existing cheap bounds | 0.209854 s | +| Cheap bounds plus cap 11 | 0.354314 s | +| Cheap bounds plus cap 11 plus individual reachability | 0.361713 s | +| Cheap bounds plus cap 11 plus shared tail (simplified) | 0.351661 s | +| Cheap bounds plus individual reachability, no cap 11 | 0.237047 s | +| Cheap bounds plus shared tail (simplified), no cap 11 | 0.228014 s | + +Without cap 11, the simplified shared-tail version takes a median paired +**9.25% more** time than the cheap bounds (faster in 1/21 pairs), **3.02% less** +than the individual-vertex version (18/21), and **27.76% more** than unpruned +traversal (0/21). The 48.66% reduction in entered nodes versus the cheap bounds +still does not pay for filtering. With cap 11 retained, the shared-tail version +saves 2.60% relative to individual reachability (18/21 faster pairs). +All 147 processes return the identical 828-word hash. + +Ratios are medians of adjacent paired ratios, not ratios of separate medians. +Host speed varied across exploratory batches; only the final source-bound +within-block comparisons above support these percentages. The unpruned mode +also beats cheap rules in this tiny Python domain. That does not refute their +usefulness in other engines or dimensions. Individual reachability computes +only its needed pair support and pays no unused joint-distance work. + +**Stop:** retain the simplified lemma, strict witness and negative integration +evidence. Do not patch a maintained engine or launch a larger census on this +basis. A distinct implementation must demonstrate improved complete caller +runtime before integration is justified. + +## Reproduce + +Python 3.12, standard library only. Download this directory, then run: + +~~~sh +python -I -B verify.py +python -I -O -B verify.py +python -I -O -B test_mutations.py +python -I -B benchmark.py --pairs 21 --output NEW-TIMINGS.json +~~~ + +The verifier checks the complete expected receipt and source hashes. It reads +local Python source directly, without accepting existing bytecode. It changes +no files; --emit-receipt is an explicit authoring path that prints a new receipt. +Benchmarking refuses to overwrite its output. No Git, network, GPU or compiler +is needed for these direct commands. + +From the repository root: + +~~~sh +python -B scripts/research_package.py --package research/five-label-prefix-completion +~~~ + +## Overlap, provenance and credit + +Base bee95ce88f9f19802f0613f92838895cd0e14a1f, priority revision 7, +selected kappa 60403/20000000. Handoff-first selection followed +[PR4992](https://github.com/CrocSwap/integer-mult-bounds/pull/4992). +The initial fresh search found Ali Romman's active +[matching-capacity claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/4903#discussioncomment-19139042). +This study therefore takes the separate reachable pair-support contract, with +no endpoint-degree or preserving-edge matching theorem. The complete overlap +coverage and limitations are in OVERLAP.json. + +Credit Ali Romman / PR4992 for the sharp cap and current handoff; Mihir Srivastava / +PR4907 for the five-label proof and explicit partial-prefix question; Nick Petalas / +PR4894 for matching balance and / PR3005 for union support and the position-block +oracle representation. Retain Ross Richardson / PR943 for the prefix-walk model, +Nicholas Stone / PR2973 for the corrected parity boundary, unpaidmoon / PR4148 +for the high-weight question, and James Reed / PR3096 for the audit lineage. + +The core distance rule and both enumerators import no predecessor executable. +The final overlap comparison alone calls the unchanged PR5001 feasible_splits +function, frozen as reference5001.py with its original notice and full proof +in reference5001.md. SOURCES.json binds those bytes at the refreshed main; all +consumed runtime bytes are package-local. The rest of that verifier is not run. +The PR4992 head is an attributed cap comparison source, not a live Git dependency +or a selected-theorem endorsement. +The independently enumerated full small-domain witness set also checks the +cap-11 comparison's safety in exactly this domain. No independent human, +second-agent, or formal proof-kernel review is claimed. + +## Final overlap comparison with PR5001 + +A 06:37 UTC refresh found PR5001 completed and retained at main +f259dabc7d70e0db8d6d36bfda888f008bbfecc1. Its source head is +fe3226ea4e36469f43c6b116c5b98cc221a9b1af. The scientific baseline and timing +sources are unchanged; this branch was advanced to the refreshed main, whose +priority revision and selected record match the starting base. + +The separately transcribed matching-capacity test agrees with the author's +frozen function on all **108,195** nonempty-prefix/omitted-coordinate cases. +All actual completed-cycle splits remain admitted in 203,225 comparisons. +Every one of the **67** strict shared-tail prefixes still passes the matching +condition. Thus those cases are complementary to that exact predicate, not +rediscoveries of its rejections. This does not establish general dominance, +complete PR5001 replay, or a combined maintained-engine runtime result. +The timings above do not include the matching test. + +## Open next questions + +First profile a maintained small-domain caller before attempting integration: +can incremental bitsets or cached Hamming envelopes amortize the filtering +cost while retaining exact full-set equality? Stop if complete caller runtime +does not improve. A larger seven-label census needs a separate budget and is +not justified by fewer nodes in this tiny experiment. + +A separate maintained-engine integration of PR5001 was claimed by JoyboyBrian +at the final refresh. This package does not enter that task. Any future joint +integration needs a pinned caller, full unchanged leaf receipts and a new +complete runtime comparison. diff --git a/research/five-label-prefix-completion/RESULT.json b/research/five-label-prefix-completion/RESULT.json new file mode 100644 index 0000000000..ab8a5d7ac5 --- /dev/null +++ b/research/five-label-prefix-completion/RESULT.json @@ -0,0 +1,239 @@ +{ + "additional_by_depth": { + "8": 26, + "9": 41 + }, + "additional_joint_prefixes": [ + "010201320", + "010203120", + "01020321", + "010230120", + "010230130", + "01023021", + "01023031", + "01023201", + "01023210", + "012010302", + "012010320", + "012013020", + "01202301", + "01202310", + "012030102", + "012030120", + "012030130", + "01203021", + "012031020", + "01203201", + "01203210", + "012101312", + "012103432", + "012130342", + "012130432", + "012131012", + "012131013", + "012131021", + "012131031", + "01213120", + "01213201", + "01213202", + "01213210", + "012134042", + "012134043", + "012301020", + "012301030", + "01230201", + "01230210", + "01230310", + "012310342", + "012310432", + "01231201", + "01231202", + "01231210", + "01231301", + "01231303", + "012313042", + "012314043", + "01232010", + "012320341", + "012320431", + "01232101", + "01232102", + "01232120", + "012321430", + "012324043", + "012341032", + "012341043", + "012341230", + "012341403", + "012341430", + "012342043", + "012342403", + "012343012", + "012343042", + "012343210" + ], + "class_lower_additional": [], + "controls": { + "coordinate_permuted_prefixes": 1440, + "credited_low_weight_excess": 8, + "invalid_inputs": 8, + "restored_simple_suffixes": [ + { + "labels": 4, + "universal": false, + "word": "010201320232" + }, + { + "labels": 5, + "universal": false, + "word": "010201320434" + } + ], + "strict_witness": { + "future": [ + 4, + 10, + 12, + 16, + 24 + ], + "missing": [ + 20, + 28 + ], + "prefix": "010201320", + "reject": true + } + }, + "matching_comparison": { + "actual_split_containment_checks": 203225, + "joint_strict_prefixes_also_matching_rejected": [], + "joint_strict_prefixes_passing_matching": 67, + "literal_predicate_comparisons": 108195 + }, + "modes": { + "cap11": { + "closed": 828, + "entered": 13990, + "pruned": 8878, + "universal": 828, + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727" + }, + "cheap": { + "closed": 828, + "entered": 14317, + "pruned": 9117, + "universal": 828, + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727" + }, + "none": { + "closed": 3695, + "entered": 21640, + "pruned": 0, + "universal": 828, + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727" + }, + "one_vertex": { + "closed": 828, + "entered": 7519, + "pruned": 4489, + "universal": 828, + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727" + }, + "one_without_cap": { + "closed": 828, + "entered": 7543, + "pruned": 4507, + "universal": 828, + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727" + }, + "two_vertex": { + "closed": 828, + "entered": 7326, + "pruned": 4363, + "universal": 828, + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727" + }, + "two_without_cap": { + "closed": 828, + "entered": 7350, + "pruned": 4381, + "universal": 828, + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727" + } + }, + "oracle": { + "restored_partitions": 139954, + "simple_closed": 3695, + "simple_closed_sha256": "ff3a2b81868354be17a3e48bc75cad14c9177b9f5df41a068e1947790ca79347", + "simple_universal": 828, + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727" + }, + "prefixes": { + "by_depth": { + "0": 1, + "1": 1, + "10": 4626, + "11": 14965, + "2": 1, + "3": 2, + "4": 4, + "5": 12, + "6": 36, + "7": 125, + "8": 420, + "9": 1447 + }, + "closed_completion_checks": 44340, + "literal_envelope_equalities": 21640, + "live": 2427, + "predicate_rejections_on_full_domain": { + "cap11": 4999, + "class_lower": 7340, + "one_vertex": 16311, + "remaining": 13887, + "two_vertex": 16379, + "union": 12255 + }, + "reflected_ordered_pairs": 39381, + "total": 21640, + "universal_completion_checks": 9936 + }, + "schema": "five-label-prefix-completion/v1", + "small_raw_controls": [ + { + "length": 6, + "n": 3, + "prefix_checks": 144, + "raw_words": 729, + "simple_restored": 24, + "universal": 24 + }, + { + "length": 8, + "n": 4, + "prefix_checks": 5568, + "raw_words": 65536, + "simple_restored": 696, + "universal": 528 + } + ], + "source_sha256": { + "LICENSE": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "OVERLAP.json": "47854bd10ee2f0190ddee22b0f65ebdc9cb60978bdec4b6dff7f7f60b92df335", + "PROOF.md": "54731461e8636b0048bb01ad6bde4b92ce718959923a5cb58e888a519d94ac9d", + "README.md": "591816a89f4f733b69fe218a66efd9f396e3c260ee2f3c0f4a8cdcd893571c83", + "SOURCES.json": "8db77f2d7b81480afd73c4cdba33400840a644e55ca209d71c05b43603a53053", + "TASK.json": "345c1ab9efbb4a5306505130389ea2935015c500cb2742fbb661ba1d1a7caa24", + "TIMINGS-FINAL.json": "829b3483ff480de40e78916325bbe0a32e28ec5fcb67ab490028601444b9edb9", + "VERIFY.json": "4c36e66a64fb0d3b4506ac61a96093b378a080d60ab8fd54f6610c8872772154", + "benchmark.py": "f869ece229620c3d44f0322b8b7595c12b23cf92dc37551a6c56c28fb7c2a8a0", + "bounds.py": "e9023abd49e92ae4c5d0bcbf265ad0883d9408a51bab5354e321102f2f20f522", + "compare_matching.py": "33eaee0c0868a1ba61a7b1758d968a0c5b3b3f72cce5912e84d141be90372e87", + "oracle.py": "f9a5200d459cc00ad93f01846b568959452ca98f64748de2cf8fa5f7742902f2", + "reference5001.md": "dfaacf1af0c1c4f4365f8c03fdcb03a28d7b90e601e8a1204f71b9cab6bfd26c", + "reference5001.py": "cfb771bcb19eae1d268a45d89bc10acdf56158403b60fdd2e14c8565b5181301", + "test_mutations.py": "1fd0c4af0d866484492e746af3a096b688d2131589888621706c99f815d599a6", + "verify.py": "dba9c826204760a6bfa43ac51fce19f56d352104772296b6e3a3a6a1daaf379e" + } +} diff --git a/research/five-label-prefix-completion/SOURCES.json b/research/five-label-prefix-completion/SOURCES.json new file mode 100644 index 0000000000..fccc8a22e9 --- /dev/null +++ b/research/five-label-prefix-completion/SOURCES.json @@ -0,0 +1,52 @@ +{ + "schema_version": 1, + "base_commit": "bee95ce88f9f19802f0613f92838895cd0e14a1f", + "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" + }, + { + "path": "research/f7-union-support-audit/README.md", + "usage": "provenance", + "git_blob": "2c913f603f4190a15eda7fbe3def58524e0826dd", + "sha256": "41eb7cfb56c593482fe1654c136ea755d780aa94d23075e255727b326739784a" + }, + { + "path": "research/f7-prefix-matching-capacity/verify.py", + "usage": "provenance", + "pin": "head:f259dabc7d70e0db8d6d36bfda888f008bbfecc1:research/f7-prefix-matching-capacity/verify.py", + "git_blob": "d09ac1fe4364b4f25b16f42483ada0cb331496df", + "sha256": "cfb771bcb19eae1d268a45d89bc10acdf56158403b60fdd2e14c8565b5181301", + "vendored_as": "reference5001.py" + }, + { + "path": "research/f7-prefix-matching-capacity/README.md", + "usage": "provenance", + "pin": "head:f259dabc7d70e0db8d6d36bfda888f008bbfecc1:research/f7-prefix-matching-capacity/README.md", + "git_blob": "f5251a7b370d791c1aff734ef805271b807eadfb", + "sha256": "dfaacf1af0c1c4f4365f8c03fdcb03a28d7b90e601e8a1204f71b9cab6bfd26c", + "vendored_as": "reference5001.md" + } + ] +} diff --git a/research/five-label-prefix-completion/TASK.json b/research/five-label-prefix-completion/TASK.json new file mode 100644 index 0000000000..ded041aeb5 --- /dev/null +++ b/research/five-label-prefix-completion/TASK.json @@ -0,0 +1,84 @@ +{ + "schema_version": 1, + "task_id": "census-pruning-audit", + "priority_revision": 7, + "base_commit": "bee95ce88f9f19802f0613f92838895cd0e14a1f", + "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 and simplify a remaining-tail pair-XOR support envelope at five labels and length twelve; compare full exact sets, the later PR5001 predicate and complete local runtime.", + "scope_change_reason": "Handoff-first continuation after PR4992; the historical parity counterexample is already covered. Active matching-capacity work is left to its author. This experiment bounds reachable pair support instead.", + "bottleneck_link": "A sound necessary completion test may reduce abstract word search; exact overhead must be measured before any engine integration.", + "budget_minutes": 60, + "stop_rule": "Stop after one sound implication and full small-domain differential evidence. Do not expand to seven labels or integrate a slower rule.", + "outcome": "completed", + "evidence": "RESULT.json: full sets, literal/simplified envelope equality, 67 strict cases and exact PR5001 comparison; TIMINGS-FINAL.json: 147 fresh runs, 9.25% median paired overhead versus cheap bounds; VALIDATION.json: final checks.", + "author": "SHIN09-git", + "ai_assistance": "Substantial OpenAI Codex assistance for proof, implementation, checks and writing; one assistant, no subagents or independent human review.", + "open_questions": [ + { + "question": "Can incremental implementation improve complete maintained-caller runtime?", + "why_it_matters": "Fewer search nodes alone do not establish a speedup.", + "first_step": "Profile one pinned small-domain caller and compare complete witness sets and total cost.", + "blocked_by": "No maintained caller integration or larger-domain runtime evidence." + } + ], + "session_started_at": "2026-10-23T06:02:55Z", + "related_work": [ + { + "pr": 4992, + "head": "12a0105150f5f44a19a2199db8506d1aa44b009a", + "role": "Credited cap-11 comparison and handoff; not a runtime dependency" + }, + { + "pr": 5001, + "head": "fe3226ea4e36469f43c6b116c5b98cc221a9b1af", + "retained_at": "f259dabc7d70e0db8d6d36bfda888f008bbfecc1", + "role": "Exact frozen predicate comparison only; 67 strict joint-envelope cases still pass it." + } + ], + "result_type": "Scoped necessary-completion lemma with a negative integration/performance decision.", + "publication_status": "local-only, not submitted as a second PR", + "publication_base": "f259dabc7d70e0db8d6d36bfda888f008bbfecc1", + "final_refresh_at": "2026-10-23T06:37:34Z" +} diff --git a/research/five-label-prefix-completion/TIMINGS-FINAL.json b/research/five-label-prefix-completion/TIMINGS-FINAL.json new file mode 100644 index 0000000000..1eab4d7256 --- /dev/null +++ b/research/five-label-prefix-completion/TIMINGS-FINAL.json @@ -0,0 +1,2157 @@ +{ + "schema": "five-label-prefix-completion-timing/v1", + "started_at": "2026-10-23T06:49:18.922021+00:00", + "finished_at": "2026-10-23T06:50:00.343368+00:00", + "python": "3.12.10 (tags/v3.12.10:0cc8128, Apr 8 2025, 12:21:36) [MSC v.1943 64 bit (AMD64)]", + "platform": "Windows-11-10.0.26100-SP0", + "processes": 147, + "source_sha256": { + "bounds.py": "e9023abd49e92ae4c5d0bcbf265ad0883d9408a51bab5354e321102f2f20f522", + "benchmark.py": "f869ece229620c3d44f0322b8b7595c12b23cf92dc37551a6c56c28fb7c2a8a0" + }, + "context": "Sequential fresh processes, startup/import/source read/traversal/output included; rotating and reversing order. OS caches not flushed, host contention uncontrolled. Descriptive timings, never acceptance thresholds.", + "summaries": { + "none": { + "median_wall_seconds": 0.1803724, + "minimum_wall_seconds": 0.1531176, + "maximum_wall_seconds": 0.3387005 + }, + "cheap": { + "median_wall_seconds": 0.2098538, + "minimum_wall_seconds": 0.187619, + "maximum_wall_seconds": 0.3163076 + }, + "cap11": { + "median_wall_seconds": 0.354314, + "minimum_wall_seconds": 0.2990172, + "maximum_wall_seconds": 0.517931 + }, + "one_vertex": { + "median_wall_seconds": 0.3617133, + "minimum_wall_seconds": 0.3023299, + "maximum_wall_seconds": 0.5428762 + }, + "two_vertex": { + "median_wall_seconds": 0.3516609, + "minimum_wall_seconds": 0.2924626, + "maximum_wall_seconds": 0.507527 + }, + "one_without_cap": { + "median_wall_seconds": 0.2370475, + "minimum_wall_seconds": 0.1988335, + "maximum_wall_seconds": 0.4217523 + }, + "two_without_cap": { + "median_wall_seconds": 0.2280137, + "minimum_wall_seconds": 0.1996879, + "maximum_wall_seconds": 0.3938434 + } + }, + "comparisons": { + "cap11_over_cheap": { + "median_paired_ratio": 1.6924772563851056, + "faster_pairs": 0, + "pairs": 21 + }, + "one_vertex_over_cap11": { + "median_paired_ratio": 1.0250314143663244, + "faster_pairs": 5, + "pairs": 21 + }, + "two_vertex_over_one_vertex": { + "median_paired_ratio": 0.9739575331058009, + "faster_pairs": 18, + "pairs": 21 + }, + "two_vertex_over_cheap": { + "median_paired_ratio": 1.6680055873794544, + "faster_pairs": 1, + "pairs": 21 + }, + "two_vertex_over_none": { + "median_paired_ratio": 1.9263586414163156, + "faster_pairs": 0, + "pairs": 21 + }, + "one_without_cap_over_cheap": { + "median_paired_ratio": 1.126542388475642, + "faster_pairs": 1, + "pairs": 21 + }, + "two_without_cap_over_cheap": { + "median_paired_ratio": 1.0925138582165257, + "faster_pairs": 1, + "pairs": 21 + }, + "two_without_cap_over_one_without_cap": { + "median_paired_ratio": 0.9698358348310304, + "faster_pairs": 18, + "pairs": 21 + }, + "two_without_cap_over_none": { + "median_paired_ratio": 1.2776412279938594, + "faster_pairs": 0, + "pairs": 21 + } + }, + "rows": [ + { + "pair": 0, + "position": 0, + "wall_ns": 187019200, + "counts": { + "closed": 3695, + "entered": 21640, + "pruned": 0, + "universal": 828 + }, + "mode": "none", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 37383800 + }, + { + "pair": 0, + "position": 1, + "wall_ns": 187619000, + "counts": { + "closed": 828, + "entered": 14317, + "pruned": 9117, + "universal": 828 + }, + "mode": "cheap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 54099700 + }, + { + "pair": 0, + "position": 2, + "wall_ns": 304319900, + "counts": { + "closed": 828, + "entered": 13990, + "pruned": 8878, + "universal": 828 + }, + "mode": "cap11", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 175752900 + }, + { + "pair": 0, + "position": 3, + "wall_ns": 419518500, + "counts": { + "closed": 828, + "entered": 7519, + "pruned": 4489, + "universal": 828 + }, + "mode": "one_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 259651000 + }, + { + "pair": 0, + "position": 4, + "wall_ns": 306043200, + "counts": { + "closed": 828, + "entered": 7326, + "pruned": 4363, + "universal": 828 + }, + "mode": "two_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 169322600 + }, + { + "pair": 0, + "position": 5, + "wall_ns": 206512600, + "counts": { + "closed": 828, + "entered": 7543, + "pruned": 4507, + "universal": 828 + }, + "mode": "one_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 79226700 + }, + { + "pair": 0, + "position": 6, + "wall_ns": 199687900, + "counts": { + "closed": 828, + "entered": 7350, + "pruned": 4381, + "universal": 828 + }, + "mode": "two_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 71702000 + }, + { + "pair": 1, + "position": 0, + "wall_ns": 153117600, + "counts": { + "closed": 3695, + "entered": 21640, + "pruned": 0, + "universal": 828 + }, + "mode": "none", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 31379300 + }, + { + "pair": 1, + "position": 1, + "wall_ns": 207409900, + "counts": { + "closed": 828, + "entered": 7350, + "pruned": 4381, + "universal": 828 + }, + "mode": "two_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 83004200 + }, + { + "pair": 1, + "position": 2, + "wall_ns": 198833500, + "counts": { + "closed": 828, + "entered": 7543, + "pruned": 4507, + "universal": 828 + }, + "mode": "one_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 76482200 + }, + { + "pair": 1, + "position": 3, + "wall_ns": 292462600, + "counts": { + "closed": 828, + "entered": 7326, + "pruned": 4363, + "universal": 828 + }, + "mode": "two_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 169169600 + }, + { + "pair": 1, + "position": 4, + "wall_ns": 302329900, + "counts": { + "closed": 828, + "entered": 7519, + "pruned": 4489, + "universal": 828 + }, + "mode": "one_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 180536400 + }, + { + "pair": 1, + "position": 5, + "wall_ns": 299017200, + "counts": { + "closed": 828, + "entered": 13990, + "pruned": 8878, + "universal": 828 + }, + "mode": "cap11", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 176084000 + }, + { + "pair": 1, + "position": 6, + "wall_ns": 296849800, + "counts": { + "closed": 828, + "entered": 14317, + "pruned": 9117, + "universal": 828 + }, + "mode": "cheap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 101085900 + }, + { + "pair": 2, + "position": 0, + "wall_ns": 517931000, + "counts": { + "closed": 828, + "entered": 13990, + "pruned": 8878, + "universal": 828 + }, + "mode": "cap11", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 285254000 + }, + { + "pair": 2, + "position": 1, + "wall_ns": 542876200, + "counts": { + "closed": 828, + "entered": 7519, + "pruned": 4489, + "universal": 828 + }, + "mode": "one_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 305131200 + }, + { + "pair": 2, + "position": 2, + "wall_ns": 507527000, + "counts": { + "closed": 828, + "entered": 7326, + "pruned": 4363, + "universal": 828 + }, + "mode": "two_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 293186800 + }, + { + "pair": 2, + "position": 3, + "wall_ns": 421752300, + "counts": { + "closed": 828, + "entered": 7543, + "pruned": 4507, + "universal": 828 + }, + "mode": "one_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 146337200 + }, + { + "pair": 2, + "position": 4, + "wall_ns": 393843400, + "counts": { + "closed": 828, + "entered": 7350, + "pruned": 4381, + "universal": 828 + }, + "mode": "two_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 128803500 + }, + { + "pair": 2, + "position": 5, + "wall_ns": 338700500, + "counts": { + "closed": 3695, + "entered": 21640, + "pruned": 0, + "universal": 828 + }, + "mode": "none", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 88109300 + }, + { + "pair": 2, + "position": 6, + "wall_ns": 316307600, + "counts": { + "closed": 828, + "entered": 14317, + "pruned": 9117, + "universal": 828 + }, + "mode": "cheap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 87981600 + }, + { + "pair": 3, + "position": 0, + "wall_ns": 482171900, + "counts": { + "closed": 828, + "entered": 13990, + "pruned": 8878, + "universal": 828 + }, + "mode": "cap11", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 290394000 + }, + { + "pair": 3, + "position": 1, + "wall_ns": 216566800, + "counts": { + "closed": 828, + "entered": 14317, + "pruned": 9117, + "universal": 828 + }, + "mode": "cheap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 68466800 + }, + { + "pair": 3, + "position": 2, + "wall_ns": 180752600, + "counts": { + "closed": 3695, + "entered": 21640, + "pruned": 0, + "universal": 828 + }, + "mode": "none", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 35054600 + }, + { + "pair": 3, + "position": 3, + "wall_ns": 237736500, + "counts": { + "closed": 828, + "entered": 7350, + "pruned": 4381, + "universal": 828 + }, + "mode": "two_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 95215100 + }, + { + "pair": 3, + "position": 4, + "wall_ns": 236888300, + "counts": { + "closed": 828, + "entered": 7543, + "pruned": 4507, + "universal": 828 + }, + "mode": "one_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 96283800 + }, + { + "pair": 3, + "position": 5, + "wall_ns": 351660900, + "counts": { + "closed": 828, + "entered": 7326, + "pruned": 4363, + "universal": 828 + }, + "mode": "two_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 211027500 + }, + { + "pair": 3, + "position": 6, + "wall_ns": 368033500, + "counts": { + "closed": 828, + "entered": 7519, + "pruned": 4489, + "universal": 828 + }, + "mode": "one_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 225472000 + }, + { + "pair": 4, + "position": 0, + "wall_ns": 353086000, + "counts": { + "closed": 828, + "entered": 7326, + "pruned": 4363, + "universal": 828 + }, + "mode": "two_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 208844900 + }, + { + "pair": 4, + "position": 1, + "wall_ns": 237208600, + "counts": { + "closed": 828, + "entered": 7543, + "pruned": 4507, + "universal": 828 + }, + "mode": "one_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 95822600 + }, + { + "pair": 4, + "position": 2, + "wall_ns": 242339300, + "counts": { + "closed": 828, + "entered": 7350, + "pruned": 4381, + "universal": 828 + }, + "mode": "two_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 95291000 + }, + { + "pair": 4, + "position": 3, + "wall_ns": 207667800, + "counts": { + "closed": 3695, + "entered": 21640, + "pruned": 0, + "universal": 828 + }, + "mode": "none", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 41287800 + }, + { + "pair": 4, + "position": 4, + "wall_ns": 211841400, + "counts": { + "closed": 828, + "entered": 14317, + "pruned": 9117, + "universal": 828 + }, + "mode": "cheap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 66978200 + }, + { + "pair": 4, + "position": 5, + "wall_ns": 349295200, + "counts": { + "closed": 828, + "entered": 13990, + "pruned": 8878, + "universal": 828 + }, + "mode": "cap11", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 206695500 + }, + { + "pair": 4, + "position": 6, + "wall_ns": 362527100, + "counts": { + "closed": 828, + "entered": 7519, + "pruned": 4489, + "universal": 828 + }, + "mode": "one_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 221421600 + }, + { + "pair": 5, + "position": 0, + "wall_ns": 350739600, + "counts": { + "closed": 828, + "entered": 7326, + "pruned": 4363, + "universal": 828 + }, + "mode": "two_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 207636700 + }, + { + "pair": 5, + "position": 1, + "wall_ns": 357098100, + "counts": { + "closed": 828, + "entered": 7519, + "pruned": 4489, + "universal": 828 + }, + "mode": "one_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 217599800 + }, + { + "pair": 5, + "position": 2, + "wall_ns": 365736500, + "counts": { + "closed": 828, + "entered": 13990, + "pruned": 8878, + "universal": 828 + }, + "mode": "cap11", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 225864000 + }, + { + "pair": 5, + "position": 3, + "wall_ns": 209853800, + "counts": { + "closed": 828, + "entered": 14317, + "pruned": 9117, + "universal": 828 + }, + "mode": "cheap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 69858300 + }, + { + "pair": 5, + "position": 4, + "wall_ns": 182655200, + "counts": { + "closed": 3695, + "entered": 21640, + "pruned": 0, + "universal": 828 + }, + "mode": "none", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 45165200 + }, + { + "pair": 5, + "position": 5, + "wall_ns": 235329500, + "counts": { + "closed": 828, + "entered": 7350, + "pruned": 4381, + "universal": 828 + }, + "mode": "two_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 89523500 + }, + { + "pair": 5, + "position": 6, + "wall_ns": 235961800, + "counts": { + "closed": 828, + "entered": 7543, + "pruned": 4507, + "universal": 828 + }, + "mode": "one_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 94906600 + }, + { + "pair": 6, + "position": 0, + "wall_ns": 226507600, + "counts": { + "closed": 828, + "entered": 7350, + "pruned": 4381, + "universal": 828 + }, + "mode": "two_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 82978500 + }, + { + "pair": 6, + "position": 1, + "wall_ns": 181380400, + "counts": { + "closed": 3695, + "entered": 21640, + "pruned": 0, + "universal": 828 + }, + "mode": "none", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 40346500 + }, + { + "pair": 6, + "position": 2, + "wall_ns": 208037100, + "counts": { + "closed": 828, + "entered": 14317, + "pruned": 9117, + "universal": 828 + }, + "mode": "cheap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 66663400 + }, + { + "pair": 6, + "position": 3, + "wall_ns": 359685800, + "counts": { + "closed": 828, + "entered": 13990, + "pruned": 8878, + "universal": 828 + }, + "mode": "cap11", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 217310600 + }, + { + "pair": 6, + "position": 4, + "wall_ns": 356100600, + "counts": { + "closed": 828, + "entered": 7519, + "pruned": 4489, + "universal": 828 + }, + "mode": "one_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 212347200 + }, + { + "pair": 6, + "position": 5, + "wall_ns": 350742700, + "counts": { + "closed": 828, + "entered": 7326, + "pruned": 4363, + "universal": 828 + }, + "mode": "two_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 208756300 + }, + { + "pair": 6, + "position": 6, + "wall_ns": 237868900, + "counts": { + "closed": 828, + "entered": 7543, + "pruned": 4507, + "universal": 828 + }, + "mode": "one_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 97520500 + }, + { + "pair": 7, + "position": 0, + "wall_ns": 235323300, + "counts": { + "closed": 828, + "entered": 7350, + "pruned": 4381, + "universal": 828 + }, + "mode": "two_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 89608500 + }, + { + "pair": 7, + "position": 1, + "wall_ns": 240768200, + "counts": { + "closed": 828, + "entered": 7543, + "pruned": 4507, + "universal": 828 + }, + "mode": "one_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 95084800 + }, + { + "pair": 7, + "position": 2, + "wall_ns": 355122000, + "counts": { + "closed": 828, + "entered": 7326, + "pruned": 4363, + "universal": 828 + }, + "mode": "two_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 209431000 + }, + { + "pair": 7, + "position": 3, + "wall_ns": 351167700, + "counts": { + "closed": 828, + "entered": 7519, + "pruned": 4489, + "universal": 828 + }, + "mode": "one_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 210774100 + }, + { + "pair": 7, + "position": 4, + "wall_ns": 354136000, + "counts": { + "closed": 828, + "entered": 13990, + "pruned": 8878, + "universal": 828 + }, + "mode": "cap11", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 212080500 + }, + { + "pair": 7, + "position": 5, + "wall_ns": 209050400, + "counts": { + "closed": 828, + "entered": 14317, + "pruned": 9117, + "universal": 828 + }, + "mode": "cheap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 65687200 + }, + { + "pair": 7, + "position": 6, + "wall_ns": 180372400, + "counts": { + "closed": 3695, + "entered": 21640, + "pruned": 0, + "universal": 828 + }, + "mode": "none", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 38922500 + }, + { + "pair": 8, + "position": 0, + "wall_ns": 208004900, + "counts": { + "closed": 828, + "entered": 14317, + "pruned": 9117, + "universal": 828 + }, + "mode": "cheap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 65218800 + }, + { + "pair": 8, + "position": 1, + "wall_ns": 354568400, + "counts": { + "closed": 828, + "entered": 13990, + "pruned": 8878, + "universal": 828 + }, + "mode": "cap11", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 211287400 + }, + { + "pair": 8, + "position": 2, + "wall_ns": 363508900, + "counts": { + "closed": 828, + "entered": 7519, + "pruned": 4489, + "universal": 828 + }, + "mode": "one_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 220446600 + }, + { + "pair": 8, + "position": 3, + "wall_ns": 341132800, + "counts": { + "closed": 828, + "entered": 7326, + "pruned": 4363, + "universal": 828 + }, + "mode": "two_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 200541400 + }, + { + "pair": 8, + "position": 4, + "wall_ns": 238581200, + "counts": { + "closed": 828, + "entered": 7543, + "pruned": 4507, + "universal": 828 + }, + "mode": "one_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 98851900 + }, + { + "pair": 8, + "position": 5, + "wall_ns": 227090500, + "counts": { + "closed": 828, + "entered": 7350, + "pruned": 4381, + "universal": 828 + }, + "mode": "two_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 83907000 + }, + { + "pair": 8, + "position": 6, + "wall_ns": 178613300, + "counts": { + "closed": 3695, + "entered": 21640, + "pruned": 0, + "universal": 828 + }, + "mode": "none", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 37412400 + }, + { + "pair": 9, + "position": 0, + "wall_ns": 210420400, + "counts": { + "closed": 828, + "entered": 14317, + "pruned": 9117, + "universal": 828 + }, + "mode": "cheap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 69832700 + }, + { + "pair": 9, + "position": 1, + "wall_ns": 178280200, + "counts": { + "closed": 3695, + "entered": 21640, + "pruned": 0, + "universal": 828 + }, + "mode": "none", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 35402400 + }, + { + "pair": 9, + "position": 2, + "wall_ns": 228013700, + "counts": { + "closed": 828, + "entered": 7350, + "pruned": 4381, + "universal": 828 + }, + "mode": "two_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 88419000 + }, + { + "pair": 9, + "position": 3, + "wall_ns": 237047500, + "counts": { + "closed": 828, + "entered": 7543, + "pruned": 4507, + "universal": 828 + }, + "mode": "one_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 95313900 + }, + { + "pair": 9, + "position": 4, + "wall_ns": 359166100, + "counts": { + "closed": 828, + "entered": 7326, + "pruned": 4363, + "universal": 828 + }, + "mode": "two_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 216219400 + }, + { + "pair": 9, + "position": 5, + "wall_ns": 360037500, + "counts": { + "closed": 828, + "entered": 7519, + "pruned": 4489, + "universal": 828 + }, + "mode": "one_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 217181900 + }, + { + "pair": 9, + "position": 6, + "wall_ns": 354314000, + "counts": { + "closed": 828, + "entered": 13990, + "pruned": 8878, + "universal": 828 + }, + "mode": "cap11", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 212272700 + }, + { + "pair": 10, + "position": 0, + "wall_ns": 357669800, + "counts": { + "closed": 828, + "entered": 7519, + "pruned": 4489, + "universal": 828 + }, + "mode": "one_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 217181400 + }, + { + "pair": 10, + "position": 1, + "wall_ns": 358133600, + "counts": { + "closed": 828, + "entered": 7326, + "pruned": 4363, + "universal": 828 + }, + "mode": "two_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 213234400 + }, + { + "pair": 10, + "position": 2, + "wall_ns": 235584000, + "counts": { + "closed": 828, + "entered": 7543, + "pruned": 4507, + "universal": 828 + }, + "mode": "one_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 95016000 + }, + { + "pair": 10, + "position": 3, + "wall_ns": 226545900, + "counts": { + "closed": 828, + "entered": 7350, + "pruned": 4381, + "universal": 828 + }, + "mode": "two_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 86935500 + }, + { + "pair": 10, + "position": 4, + "wall_ns": 186242300, + "counts": { + "closed": 3695, + "entered": 21640, + "pruned": 0, + "universal": 828 + }, + "mode": "none", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 40928400 + }, + { + "pair": 10, + "position": 5, + "wall_ns": 214993500, + "counts": { + "closed": 828, + "entered": 14317, + "pruned": 9117, + "universal": 828 + }, + "mode": "cheap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 72506000 + }, + { + "pair": 10, + "position": 6, + "wall_ns": 351517900, + "counts": { + "closed": 828, + "entered": 13990, + "pruned": 8878, + "universal": 828 + }, + "mode": "cap11", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 210689800 + }, + { + "pair": 11, + "position": 0, + "wall_ns": 351893200, + "counts": { + "closed": 828, + "entered": 7519, + "pruned": 4489, + "universal": 828 + }, + "mode": "one_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 207170600 + }, + { + "pair": 11, + "position": 1, + "wall_ns": 347800000, + "counts": { + "closed": 828, + "entered": 13990, + "pruned": 8878, + "universal": 828 + }, + "mode": "cap11", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 207150900 + }, + { + "pair": 11, + "position": 2, + "wall_ns": 203698600, + "counts": { + "closed": 828, + "entered": 14317, + "pruned": 9117, + "universal": 828 + }, + "mode": "cheap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 63220400 + }, + { + "pair": 11, + "position": 3, + "wall_ns": 174911000, + "counts": { + "closed": 3695, + "entered": 21640, + "pruned": 0, + "universal": 828 + }, + "mode": "none", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 34091000 + }, + { + "pair": 11, + "position": 4, + "wall_ns": 222392700, + "counts": { + "closed": 828, + "entered": 7350, + "pruned": 4381, + "universal": 828 + }, + "mode": "two_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 83747600 + }, + { + "pair": 11, + "position": 5, + "wall_ns": 233526900, + "counts": { + "closed": 828, + "entered": 7543, + "pruned": 4507, + "universal": 828 + }, + "mode": "one_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 94083200 + }, + { + "pair": 11, + "position": 6, + "wall_ns": 352337400, + "counts": { + "closed": 828, + "entered": 7326, + "pruned": 4363, + "universal": 828 + }, + "mode": "two_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 213020600 + }, + { + "pair": 12, + "position": 0, + "wall_ns": 238632600, + "counts": { + "closed": 828, + "entered": 7543, + "pruned": 4507, + "universal": 828 + }, + "mode": "one_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 97808900 + }, + { + "pair": 12, + "position": 1, + "wall_ns": 227679100, + "counts": { + "closed": 828, + "entered": 7350, + "pruned": 4381, + "universal": 828 + }, + "mode": "two_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 86554500 + }, + { + "pair": 12, + "position": 2, + "wall_ns": 179976200, + "counts": { + "closed": 3695, + "entered": 21640, + "pruned": 0, + "universal": 828 + }, + "mode": "none", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 38587300 + }, + { + "pair": 12, + "position": 3, + "wall_ns": 211555000, + "counts": { + "closed": 828, + "entered": 14317, + "pruned": 9117, + "universal": 828 + }, + "mode": "cheap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 68575900 + }, + { + "pair": 12, + "position": 4, + "wall_ns": 356534500, + "counts": { + "closed": 828, + "entered": 13990, + "pruned": 8878, + "universal": 828 + }, + "mode": "cap11", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 214254900 + }, + { + "pair": 12, + "position": 5, + "wall_ns": 371610300, + "counts": { + "closed": 828, + "entered": 7519, + "pruned": 4489, + "universal": 828 + }, + "mode": "one_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 226447900 + }, + { + "pair": 12, + "position": 6, + "wall_ns": 369282100, + "counts": { + "closed": 828, + "entered": 7326, + "pruned": 4363, + "universal": 828 + }, + "mode": "two_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 220700800 + }, + { + "pair": 13, + "position": 0, + "wall_ns": 235305700, + "counts": { + "closed": 828, + "entered": 7543, + "pruned": 4507, + "universal": 828 + }, + "mode": "one_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 94463000 + }, + { + "pair": 13, + "position": 1, + "wall_ns": 339011700, + "counts": { + "closed": 828, + "entered": 7326, + "pruned": 4363, + "universal": 828 + }, + "mode": "two_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 200092800 + }, + { + "pair": 13, + "position": 2, + "wall_ns": 364934300, + "counts": { + "closed": 828, + "entered": 7519, + "pruned": 4489, + "universal": 828 + }, + "mode": "one_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 227516200 + }, + { + "pair": 13, + "position": 3, + "wall_ns": 355153400, + "counts": { + "closed": 828, + "entered": 13990, + "pruned": 8878, + "universal": 828 + }, + "mode": "cap11", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 214895100 + }, + { + "pair": 13, + "position": 4, + "wall_ns": 208883300, + "counts": { + "closed": 828, + "entered": 14317, + "pruned": 9117, + "universal": 828 + }, + "mode": "cheap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 67040300 + }, + { + "pair": 13, + "position": 5, + "wall_ns": 180075900, + "counts": { + "closed": 3695, + "entered": 21640, + "pruned": 0, + "universal": 828 + }, + "mode": "none", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 39268600 + }, + { + "pair": 13, + "position": 6, + "wall_ns": 228207900, + "counts": { + "closed": 828, + "entered": 7350, + "pruned": 4381, + "universal": 828 + }, + "mode": "two_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 85089500 + }, + { + "pair": 14, + "position": 0, + "wall_ns": 176369900, + "counts": { + "closed": 3695, + "entered": 21640, + "pruned": 0, + "universal": 828 + }, + "mode": "none", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 38382900 + }, + { + "pair": 14, + "position": 1, + "wall_ns": 209255400, + "counts": { + "closed": 828, + "entered": 14317, + "pruned": 9117, + "universal": 828 + }, + "mode": "cheap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 69056600 + }, + { + "pair": 14, + "position": 2, + "wall_ns": 350026300, + "counts": { + "closed": 828, + "entered": 13990, + "pruned": 8878, + "universal": 828 + }, + "mode": "cap11", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 210334700 + }, + { + "pair": 14, + "position": 3, + "wall_ns": 362161100, + "counts": { + "closed": 828, + "entered": 7519, + "pruned": 4489, + "universal": 828 + }, + "mode": "one_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 220199700 + }, + { + "pair": 14, + "position": 4, + "wall_ns": 351428200, + "counts": { + "closed": 828, + "entered": 7326, + "pruned": 4363, + "universal": 828 + }, + "mode": "two_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 210829900 + }, + { + "pair": 14, + "position": 5, + "wall_ns": 231605800, + "counts": { + "closed": 828, + "entered": 7543, + "pruned": 4507, + "universal": 828 + }, + "mode": "one_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 89191100 + }, + { + "pair": 14, + "position": 6, + "wall_ns": 226639200, + "counts": { + "closed": 828, + "entered": 7350, + "pruned": 4381, + "universal": 828 + }, + "mode": "two_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 83190600 + }, + { + "pair": 15, + "position": 0, + "wall_ns": 178160500, + "counts": { + "closed": 3695, + "entered": 21640, + "pruned": 0, + "universal": 828 + }, + "mode": "none", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 38373200 + }, + { + "pair": 15, + "position": 1, + "wall_ns": 227625200, + "counts": { + "closed": 828, + "entered": 7350, + "pruned": 4381, + "universal": 828 + }, + "mode": "two_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 85631800 + }, + { + "pair": 15, + "position": 2, + "wall_ns": 238738300, + "counts": { + "closed": 828, + "entered": 7543, + "pruned": 4507, + "universal": 828 + }, + "mode": "one_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 93334200 + }, + { + "pair": 15, + "position": 3, + "wall_ns": 347834200, + "counts": { + "closed": 828, + "entered": 7326, + "pruned": 4363, + "universal": 828 + }, + "mode": "two_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 205764600 + }, + { + "pair": 15, + "position": 4, + "wall_ns": 366672700, + "counts": { + "closed": 828, + "entered": 7519, + "pruned": 4489, + "universal": 828 + }, + "mode": "one_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 225621800 + }, + { + "pair": 15, + "position": 5, + "wall_ns": 357718500, + "counts": { + "closed": 828, + "entered": 13990, + "pruned": 8878, + "universal": 828 + }, + "mode": "cap11", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 217870900 + }, + { + "pair": 15, + "position": 6, + "wall_ns": 207871600, + "counts": { + "closed": 828, + "entered": 14317, + "pruned": 9117, + "universal": 828 + }, + "mode": "cheap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 68010500 + }, + { + "pair": 16, + "position": 0, + "wall_ns": 351650400, + "counts": { + "closed": 828, + "entered": 13990, + "pruned": 8878, + "universal": 828 + }, + "mode": "cap11", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 207089100 + }, + { + "pair": 16, + "position": 1, + "wall_ns": 360567300, + "counts": { + "closed": 828, + "entered": 7519, + "pruned": 4489, + "universal": 828 + }, + "mode": "one_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 218741000 + }, + { + "pair": 16, + "position": 2, + "wall_ns": 351848800, + "counts": { + "closed": 828, + "entered": 7326, + "pruned": 4363, + "universal": 828 + }, + "mode": "two_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 208547600 + }, + { + "pair": 16, + "position": 3, + "wall_ns": 241935200, + "counts": { + "closed": 828, + "entered": 7543, + "pruned": 4507, + "universal": 828 + }, + "mode": "one_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 94850100 + }, + { + "pair": 16, + "position": 4, + "wall_ns": 227761000, + "counts": { + "closed": 828, + "entered": 7350, + "pruned": 4381, + "universal": 828 + }, + "mode": "two_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 85515400 + }, + { + "pair": 16, + "position": 5, + "wall_ns": 176118600, + "counts": { + "closed": 3695, + "entered": 21640, + "pruned": 0, + "universal": 828 + }, + "mode": "none", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 37030200 + }, + { + "pair": 16, + "position": 6, + "wall_ns": 207772600, + "counts": { + "closed": 828, + "entered": 14317, + "pruned": 9117, + "universal": 828 + }, + "mode": "cheap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 67900600 + }, + { + "pair": 17, + "position": 0, + "wall_ns": 356501100, + "counts": { + "closed": 828, + "entered": 13990, + "pruned": 8878, + "universal": 828 + }, + "mode": "cap11", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 211532900 + }, + { + "pair": 17, + "position": 1, + "wall_ns": 205589000, + "counts": { + "closed": 828, + "entered": 14317, + "pruned": 9117, + "universal": 828 + }, + "mode": "cheap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 65677000 + }, + { + "pair": 17, + "position": 2, + "wall_ns": 177546000, + "counts": { + "closed": 3695, + "entered": 21640, + "pruned": 0, + "universal": 828 + }, + "mode": "none", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 35382300 + }, + { + "pair": 17, + "position": 3, + "wall_ns": 229333300, + "counts": { + "closed": 828, + "entered": 7350, + "pruned": 4381, + "universal": 828 + }, + "mode": "two_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 87409200 + }, + { + "pair": 17, + "position": 4, + "wall_ns": 234722400, + "counts": { + "closed": 828, + "entered": 7543, + "pruned": 4507, + "universal": 828 + }, + "mode": "one_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 95985400 + }, + { + "pair": 17, + "position": 5, + "wall_ns": 352337100, + "counts": { + "closed": 828, + "entered": 7326, + "pruned": 4363, + "universal": 828 + }, + "mode": "two_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 210226400 + }, + { + "pair": 17, + "position": 6, + "wall_ns": 361344300, + "counts": { + "closed": 828, + "entered": 7519, + "pruned": 4489, + "universal": 828 + }, + "mode": "one_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 221188000 + }, + { + "pair": 18, + "position": 0, + "wall_ns": 351895700, + "counts": { + "closed": 828, + "entered": 7326, + "pruned": 4363, + "universal": 828 + }, + "mode": "two_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 210887700 + }, + { + "pair": 18, + "position": 1, + "wall_ns": 241243500, + "counts": { + "closed": 828, + "entered": 7543, + "pruned": 4507, + "universal": 828 + }, + "mode": "one_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 97552200 + }, + { + "pair": 18, + "position": 2, + "wall_ns": 238240300, + "counts": { + "closed": 828, + "entered": 7350, + "pruned": 4381, + "universal": 828 + }, + "mode": "two_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 95334300 + }, + { + "pair": 18, + "position": 3, + "wall_ns": 186012800, + "counts": { + "closed": 3695, + "entered": 21640, + "pruned": 0, + "universal": 828 + }, + "mode": "none", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 40745000 + }, + { + "pair": 18, + "position": 4, + "wall_ns": 217258700, + "counts": { + "closed": 828, + "entered": 14317, + "pruned": 9117, + "universal": 828 + }, + "mode": "cheap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 69964700 + }, + { + "pair": 18, + "position": 5, + "wall_ns": 350249400, + "counts": { + "closed": 828, + "entered": 13990, + "pruned": 8878, + "universal": 828 + }, + "mode": "cap11", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 209321500 + }, + { + "pair": 18, + "position": 6, + "wall_ns": 367945000, + "counts": { + "closed": 828, + "entered": 7519, + "pruned": 4489, + "universal": 828 + }, + "mode": "one_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 224524900 + }, + { + "pair": 19, + "position": 0, + "wall_ns": 350355900, + "counts": { + "closed": 828, + "entered": 7326, + "pruned": 4363, + "universal": 828 + }, + "mode": "two_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 207342900 + }, + { + "pair": 19, + "position": 1, + "wall_ns": 353120600, + "counts": { + "closed": 828, + "entered": 7519, + "pruned": 4489, + "universal": 828 + }, + "mode": "one_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 208669800 + }, + { + "pair": 19, + "position": 2, + "wall_ns": 369960700, + "counts": { + "closed": 828, + "entered": 13990, + "pruned": 8878, + "universal": 828 + }, + "mode": "cap11", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 223288500 + }, + { + "pair": 19, + "position": 3, + "wall_ns": 210044800, + "counts": { + "closed": 828, + "entered": 14317, + "pruned": 9117, + "universal": 828 + }, + "mode": "cheap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 66046500 + }, + { + "pair": 19, + "position": 4, + "wall_ns": 181874700, + "counts": { + "closed": 3695, + "entered": 21640, + "pruned": 0, + "universal": 828 + }, + "mode": "none", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 41674200 + }, + { + "pair": 19, + "position": 5, + "wall_ns": 230668200, + "counts": { + "closed": 828, + "entered": 7350, + "pruned": 4381, + "universal": 828 + }, + "mode": "two_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 91054500 + }, + { + "pair": 19, + "position": 6, + "wall_ns": 237402600, + "counts": { + "closed": 828, + "entered": 7543, + "pruned": 4507, + "universal": 828 + }, + "mode": "one_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 95635600 + }, + { + "pair": 20, + "position": 0, + "wall_ns": 233854800, + "counts": { + "closed": 828, + "entered": 7350, + "pruned": 4381, + "universal": 828 + }, + "mode": "two_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 91777000 + }, + { + "pair": 20, + "position": 1, + "wall_ns": 180672300, + "counts": { + "closed": 3695, + "entered": 21640, + "pruned": 0, + "universal": 828 + }, + "mode": "none", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 38266800 + }, + { + "pair": 20, + "position": 2, + "wall_ns": 216950000, + "counts": { + "closed": 828, + "entered": 14317, + "pruned": 9117, + "universal": 828 + }, + "mode": "cheap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 70631100 + }, + { + "pair": 20, + "position": 3, + "wall_ns": 346652100, + "counts": { + "closed": 828, + "entered": 13990, + "pruned": 8878, + "universal": 828 + }, + "mode": "cap11", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 206088200 + }, + { + "pair": 20, + "position": 4, + "wall_ns": 361713300, + "counts": { + "closed": 828, + "entered": 7519, + "pruned": 4489, + "universal": 828 + }, + "mode": "one_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 218718600 + }, + { + "pair": 20, + "position": 5, + "wall_ns": 345436900, + "counts": { + "closed": 828, + "entered": 7326, + "pruned": 4363, + "universal": 828 + }, + "mode": "two_vertex", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 203127500 + }, + { + "pair": 20, + "position": 6, + "wall_ns": 234632300, + "counts": { + "closed": 828, + "entered": 7543, + "pruned": 4507, + "universal": 828 + }, + "mode": "one_without_cap", + "universal_sha256": "2e64b75bdd56124eb0993e0dcb2b79f849435465c32bdc9329ea2c171b506727", + "worker_ns": 94188600 + } + ] +} diff --git a/research/five-label-prefix-completion/VALIDATION.json b/research/five-label-prefix-completion/VALIDATION.json new file mode 100644 index 0000000000..c034f13790 --- /dev/null +++ b/research/five-label-prefix-completion/VALIDATION.json @@ -0,0 +1,65 @@ +{ + "recorded_at": "2026-10-23T06:54:14.223597+00:00", + "python": "3.12.10 (tags/v3.12.10:0cc8128, Apr 8 2025, 12:21:36) [MSC v.1943 64 bit (AMD64)]", + "platform": "Windows-11-10.0.26100-SP0", + "registered_replay": "PASS: normal and optimized, complete deterministic receipt equality", + "registered_log_sha256": "69e4d53fc52a6d1ea80cccfa6f65f373cb373e3852881eb2448fd15be2c3db30", + "source_only_optimized_and_mutations": { + "positive_source_only_optimized": "PASS", + "controls": [ + { + "name": "independent_future_pairs", + "rejected": true, + "last_error": "ValueError: simplified/literal pair envelope equality" + }, + { + "name": "drop_old_pairs", + "rejected": true, + "last_error": "ValueError: complete universal word set: one_vertex" + }, + { + "name": "drop_old_new_pairs", + "rejected": true, + "last_error": "ValueError: complete universal word set: one_vertex" + }, + { + "name": "strict_vertex_boundary", + "rejected": true, + "last_error": "ValueError: complete universal word set: one_vertex" + }, + { + "name": "omit_closing_edge", + "rejected": true, + "last_error": "ValueError: complete universal word set: one_vertex" + }, + { + "name": "omit_return_distance", + "rejected": true, + "last_error": "ValueError: simplified/literal pair envelope equality" + }, + { + "name": "disable_geometric_traversal_filter", + "rejected": true, + "last_error": "ValueError: paired-envelope traversal counts" + }, + { + "name": "typed_receipt_boolean", + "rejected": true + }, + { + "name": "proof_byte_binding", + "rejected": true + } + ] + }, + "fresh_processes": 147, + "timed_sources_match": true, + "reference5001_github_head": "fe3226ea4e36469f43c6b116c5b98cc221a9b1af", + "reference5001_live_pr_blobs_matched": { + "verify.py": "d09ac1fe4364b4f25b16f42483ada0cb331496df", + "README.md": "f5251a7b370d791c1aff734ef805271b807eadfb" + }, + "scope": "Local bounded proof/finite differential/runtime evidence. No maintained engine, hosted CI, seven-label census, selected cold replay, supplier, full theorem or independent human/formal-kernel review.", + "history": "Checkout is shallow. Optional full-history wrapper is not claimed; declared source commits are explicitly checked as publication ancestors in the external final record.", + "publication_whitespace": "Git diff --check with core.whitespace=-blank-at-eof; final empty source lines are retained to preserve the exact verified and timed bytes." +} diff --git a/research/five-label-prefix-completion/VERIFY.json b/research/five-label-prefix-completion/VERIFY.json new file mode 100644 index 0000000000..a251805243 --- /dev/null +++ b/research/five-label-prefix-completion/VERIFY.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Full independent small-domain word sets, all-prefix containment, controls and deterministic source-bound receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Same complete checks with assertions disabled." + } + ] +} diff --git a/research/five-label-prefix-completion/benchmark.py b/research/five-label-prefix-completion/benchmark.py new file mode 100644 index 0000000000..574f90ab38 --- /dev/null +++ b/research/five-label-prefix-completion/benchmark.py @@ -0,0 +1,102 @@ +#!/usr/bin/env python3 +"""Fresh-process complete small-domain traversal timings; no hosted CI claim. +Prepared for SHIN09-git with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +from datetime import datetime, timezone +from hashlib import sha256 +import json +import os +from pathlib import Path +import platform +import statistics +import subprocess +import sys +import time +from types import ModuleType + +HERE = Path(__file__).resolve().parent +MODES = ("none", "cheap", "cap11", "one_vertex", "two_vertex", "one_without_cap", "two_without_cap") + + +def core(): + path = HERE / "bounds.py" + module = ModuleType("bounds") + exec(compile(path.read_bytes(), str(path), "exec"), module.__dict__) + return module + + +def worker(mode): + started = time.perf_counter_ns() + counts, _, hits = core().search(mode) + digest = sha256("".join("".join(map(str, w)) + "\n" for w in hits).encode()).hexdigest() + return {"mode": mode, "counts": counts, "universal_sha256": digest, + "worker_ns": time.perf_counter_ns() - started} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--worker", choices=MODES) + parser.add_argument("--pairs", type=int, default=21) + parser.add_argument("--output", type=Path) + args = parser.parse_args() + if args.worker: + print(json.dumps(worker(args.worker), sort_keys=True)) + return + if not 1 <= args.pairs <= 100 or args.output is None: + parser.error("provide --output and 1 <= --pairs <= 100") + if args.output.exists(): + parser.error("output already exists") + expected = json.loads((HERE / "RESULT.json").read_bytes())["oracle"]["universal_sha256"] + pins = {name: sha256((HERE / name).read_bytes()).hexdigest() for name in ("bounds.py", "benchmark.py")} + started = datetime.now(timezone.utc).isoformat() + rows = [] + env = dict(os.environ) + env.pop("PYTHONOPTIMIZE", None) + for pair in range(args.pairs): + order = list(MODES[pair % len(MODES):] + MODES[:pair % len(MODES)]) + if pair % 2: + order.reverse() + for position, mode in enumerate(order): + before = time.perf_counter_ns() + run = subprocess.run([sys.executable, "-I", "-B", str(Path(__file__).resolve()), + "--worker", mode], cwd=HERE, env=env, capture_output=True, + check=True, timeout=30) + elapsed = time.perf_counter_ns() - before + result = json.loads(run.stdout) + if result["universal_sha256"] != expected or result["counts"]["universal"] != 828: + raise ValueError("complete witness set mismatch") + rows.append({"pair": pair, "position": position, "wall_ns": elapsed, **result}) + if pins != {name: sha256((HERE / name).read_bytes()).hexdigest() for name in pins}: + raise ValueError("timed source changed") + summaries = {} + for mode in MODES: + samples = [r["wall_ns"] / 1e9 for r in rows if r["mode"] == mode] + summaries[mode] = {"median_wall_seconds": statistics.median(samples), + "minimum_wall_seconds": min(samples), "maximum_wall_seconds": max(samples)} + comparisons = {} + for candidate, baseline in (("cap11", "cheap"), ("one_vertex", "cap11"), + ("two_vertex", "one_vertex"), ("two_vertex", "cheap"), ("two_vertex", "none"), + ("one_without_cap", "cheap"), ("two_without_cap", "cheap"), + ("two_without_cap", "one_without_cap"), ("two_without_cap", "none")): + ratios = [] + for pair in range(args.pairs): + block = {r["mode"]: r["wall_ns"] for r in rows if r["pair"] == pair} + ratios.append(block[candidate] / block[baseline]) + comparisons[candidate + "_over_" + baseline] = { + "median_paired_ratio": statistics.median(ratios), + "faster_pairs": sum(x < 1 for x in ratios), "pairs": args.pairs} + output = {"schema": "five-label-prefix-completion-timing/v1", "started_at": started, + "finished_at": datetime.now(timezone.utc).isoformat(), "python": sys.version, + "platform": platform.platform(), "processes": len(rows), "source_sha256": pins, + "context": "Sequential fresh processes, startup/import/source read/traversal/output included; rotating and reversing order. OS caches not flushed, host contention uncontrolled. Descriptive timings, never acceptance thresholds.", + "summaries": summaries, "comparisons": comparisons, "rows": rows} + with args.output.open("x", encoding="utf-8", newline="\n") as stream: + json.dump(output, stream, indent=2) + stream.write("\n") + print(json.dumps({"processes": len(rows), "comparisons": comparisons}, indent=2)) + + +if __name__ == "__main__": + main() + diff --git a/research/five-label-prefix-completion/bounds.py b/research/five-label-prefix-completion/bounds.py new file mode 100644 index 0000000000..3022224471 --- /dev/null +++ b/research/five-label-prefix-completion/bounds.py @@ -0,0 +1,157 @@ +"""Sound outward tail envelopes, fixed-domain comparison traversal. + +Prepared for SHIN09-git with substantial OpenAI Codex assistance. Apache-2.0. +The new geometric rule does not depend on the cap-11 comparison rule. +""" +from collections import Counter +from itertools import combinations + +MASKS = (15, 23, 27, 29, 30, 31) +MODES = ("none", "cheap", "cap11", "one_vertex", "two_vertex", "one_without_cap", "two_without_cap") + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def pair_support(points): + bits = 0 + for a, b in combinations(points, 2): + bits |= 1 << (a ^ b) + return bits + + +def choose2(n): + return n * (n - 1) // 2 + + +def prefix_from_word(word, n=5, length=12): + require(type(n) is int and 2 <= n <= 5, "dimension") + require(type(length) is int and length % 2 == 0 and 2 * n <= length <= 12, "length") + require(len(word) < length, "partial prefix required") + points = [0] + for label in word: + require(type(label) is int and 0 <= label < n, "label") + value = points[-1] ^ (1 << label) + require(value not in points, "simple prefix required") + points.append(value) + return tuple(points) + + +def tail_envelope(points, n=5, length=12, joint=True): + """Internal kernel: points must be a validated simple prefix starting at 0.""" + remaining = length - len(points) + 1 + last = points[-1] + visited = set(points) + future = tuple(x for x in range(1 << n) if x not in visited + and (last ^ x).bit_count() + x.bit_count() <= remaining) + possible = pair_support(points) + for old in points: + for new in future: + possible |= 1 << (old ^ new) + if not joint: + return future, possible | pair_support(future) + # Every jointly reachable future-pair difference z already occurs as + # last XOR (last XOR z): the second endpoint is old or belongs to U. + # PROOF.md derives this equality; verify.py checks the literal pair formula. + return future, possible + + +def completion_bound(word, n=5, length=12, joint=True): + points = prefix_from_word(word, n, length) + future, support = tail_envelope(points, n, length, joint) + needed = length - len(points) + full = (1 << (1 << n)) - 2 + return {"reject": len(future) < needed or support != full, + "future": future, + "missing": tuple(x for x in range(1, 1 << n) if not support >> x & 1)} + + +def remaining_reject(points, highest, length=12): + return points[-1].bit_count() + 2 * (5 - highest - 1) > length - len(points) + 1 + + +def union_reject(points): + """Credited PR3005 same/cross pair-count bound at final parity split (6,6).""" + classes = [tuple(x for x in points if x.bit_count() % 2 == bit) for bit in (0, 1)] + a, b = map(len, classes) + same = (pair_support(classes[0]) | pair_support(classes[1])).bit_count() + cross = len({x ^ y for x in classes[0] for y in classes[1]}) + return a > 6 or b > 6 or same + 30 - choose2(a) - choose2(b) < 15 or cross + 36 - a * b < 16 + + +def excess(points, mask): + total = 0 + for bit in (0, 1): + values = tuple(x for x in points if (x & mask).bit_count() % 2 == bit) + total += choose2(len(values)) - pair_support(values).bit_count() + return total + + +def cap_reject(points): + """Only for five-label length-12 simple universal completions (PR4992).""" + return any(excess(points, mask) > 11 for mask in MASKS) + + +def class_completion_lower(points, future, mask): + """Exploratory cap-11 completion bound; not used by the geometric kernel.""" + classes = [tuple(x for x in points if (x & mask).bit_count() % 2 == bit) for bit in (0, 1)] + pools = [tuple(x for x in future if (x & mask).bit_count() % 2 == bit) for bit in (0, 1)] + sizes = list(map(len, classes)) + supports = [pair_support(c).bit_count() for c in classes] + limits = [pair_support(classes[b] + pools[b]).bit_count() for b in (0, 1)] + candidates = [] + for size in ((6,) if mask == 31 else (5, 6, 7)): + final = (size, 12 - size) + if any(not sizes[b] <= final[b] <= sizes[b] + len(pools[b]) for b in (0, 1)): + continue + upper = [min(limits[b], supports[b] + choose2(final[b]) - choose2(sizes[b])) for b in (0, 1)] + candidates.append(sum(map(choose2, final)) - sum(upper)) + return min(candidates) if candidates else None + + +def reject(points, highest, mode): + require(mode in MODES, "mode") + if mode == "none": + return False + if remaining_reject(points, highest) or union_reject(points): + return True + if mode == "cheap": + return False + if mode not in ("one_without_cap", "two_without_cap") and cap_reject(points): + return True + if mode == "cap11": + return False + future, possible = tail_envelope(points, joint=mode in ("two_vertex", "two_without_cap")) + return len(future) < 12 - len(points) or possible != (1 << 32) - 2 + + +def search(mode="none"): + """Canonical DFS; no rotation, reversal or closed-word equivalence pruning.""" + counts = Counter() + closed = [] + hits = [] + + def visit(word, points, highest, seen): + counts["entered"] += 1 + if reject(points, highest, mode): + counts["pruned"] += 1 + return + if len(word) == 11: + last = points[-1] + if last and last & (last - 1) == 0: + completed = word + (last.bit_length() - 1,) + closed.append(completed) + if pair_support(points) == (1 << 32) - 2: + hits.append(completed) + return + for label in range(min(highest + 1, 4) + 1): + value = points[-1] ^ (1 << label) + if not seen >> value & 1: + visit(word + (label,), points + (value,), max(highest, label), seen | (1 << value)) + + visit((), (0,), -1, 1) + return {"entered": counts["entered"], "pruned": counts["pruned"], + "closed": len(closed), "universal": len(hits)}, tuple(sorted(closed)), tuple(sorted(hits)) + diff --git a/research/five-label-prefix-completion/compare_matching.py b/research/five-label-prefix-completion/compare_matching.py new file mode 100644 index 0000000000..cda65277d4 --- /dev/null +++ b/research/five-label-prefix-completion/compare_matching.py @@ -0,0 +1,44 @@ +"""PR5001 comparison, transcribed from its stated matching-capacity theorem. +Prepared for SHIN09-git with substantial OpenAI Codex assistance. Apache-2.0. +Ali Romman retains the theorem and original implementation credit. +""" + + +def splits(points, omitted): + # This comparison is deliberately fixed to n=5, L=12. + n, length = 5, 12 + mask = 31 ^ (1 << omitted) + side = lambda x: (x & mask).bit_count() % 2 + remaining = length - len(points) + sizes = [sum(side(x) == j for x in points) for j in (0, 1)] + if remaining == 0: + return {tuple(sizes)} if (points[0] ^ points[-1]).bit_count() == 1 else set() + used = set(points) + ends = {points[0], points[-1]} + stay = [0, 0] + for left, right in zip(points, points[1:]): + if side(left) == side(right): + stay[side(left)] += 1 + crossing = len(points) - 1 - sum(stay) + pools = [{x for x in range(32) if x not in used and side(x) == j} for j in (0, 1)] + one = [sum(x ^ (1 << omitted) in ends for x in pool) for pool in pools] + two = [sum(x ^ (1 << omitted) in pool for x in pool) // 2 for pool in pools] + answer = set() + for added0 in range(remaining + 1): + added = (added0, remaining - added0) + if any(added[j] > len(pools[j]) for j in (0, 1)): + continue + totals = tuple(sizes[j] + added[j] for j in (0, 1)) + max_new_stay = [max(i + min(two[j], (added[j] - i) // 2) + for i in range(min(one[j], added[j]) + 1)) for j in (0, 1)] + for final_crossing in range(0, length + 1, 2): + if not crossing <= final_crossing <= crossing + remaining + 1: + continue + if min(totals) and final_crossing < 2: + continue + required_stay = [totals[j] - final_crossing // 2 for j in (0, 1)] + if all(stay[j] <= required_stay[j] <= stay[j] + max_new_stay[j] for j in (0, 1)): + answer.add(totals) + break + return answer + diff --git a/research/five-label-prefix-completion/oracle.py b/research/five-label-prefix-completion/oracle.py new file mode 100644 index 0000000000..c38d99396e --- /dev/null +++ b/research/five-label-prefix-completion/oracle.py @@ -0,0 +1,57 @@ +"""Separate restored-word oracle: even set partitions, no prefix prune. + +The even-position-block method is credited to Nick Petalas's PR3005. +This implementation imports neither bounds.py nor a predecessor executable. +Prepared for SHIN09-git with substantial OpenAI Codex assistance. Apache-2.0. +""" +from itertools import combinations + + +def restored_partitions(n=5, length=12): + word = [-1] * length + + def partition(positions, label): + if not positions: + yield tuple(word) + return + if label == n: + return + first, rest = positions[0], positions[1:] + for size in range(2, len(positions) + 1, 2): + for other in combinations(rest, size - 1): + block = (first,) + other + selected = set(block) + for index in block: + word[index] = label + yield from partition(tuple(i for i in rest if i not in selected), label + 1) + + yield from partition(tuple(range(length)), 0) + + +def inspect(word, n=5): + location = 0 + points = [] + for label in word: + points.append(location) + location ^= 2 ** label + if location != 0: + raise ValueError("oracle restoration") + simple = len(set(points)) == len(points) + covered = {left ^ right for left in points for right in points} + universal = covered == set(range(2 ** n)) + return tuple(points), simple, universal + + +def census(n=5, length=12): + restored = 0 + closed, universal = [], [] + for word in restored_partitions(n, length): + restored += 1 + _, simple, cover = inspect(word, n) + if simple: + closed.append(word) + if cover: + universal.append(word) + return {"restored_partitions": restored, "simple_closed": len(closed), + "simple_universal": len(universal)}, tuple(sorted(closed)), tuple(sorted(universal)) + diff --git a/research/five-label-prefix-completion/reference5001.md b/research/five-label-prefix-completion/reference5001.md new file mode 100644 index 0000000000..f5251a7b37 --- /dev/null +++ b/research/five-label-prefix-completion/reference5001.md @@ -0,0 +1,147 @@ +# Matching capacity for a partial hypercube cycle + +**Enabling combinatorial proof with bounded exact checks; no new kappa.** +This package gives a necessary completion condition for a simple path in +`Q_n` when a linear functional omits one coordinate. It uses the unused +matching edges and the two path endpoints. It can reject a prefix that +passes the complete-cycle matching-balance bound and the return-distance +bound. It does not change a maintained census engine. + +This answers Open next question 2 of +[PR #4907](https://github.com/CrocSwap/integer-mult-bounds/pull/4907). +[PR #4992](https://github.com/CrocSwap/integer-mult-bounds/pull/4992) gives the +related sharp five-label cap. That cap is not an assumption of this proof. +The selected kappa remains `60403/20000000`. + +## Contract and theorem + +Let `n >= 2`. Let `L` be even, with `4 <= L <= 2^n`. +The input is a simple path `q_0,...,q_(k-1)` in `Q_n`, with `2 <= k <= L`. +A completion adds `r=L-k` new vertices, then an edge to `q_0`, to form a +simple cycle. Repeated interior vertices are not permitted. +Let `v` be one coordinate. The functional `f` has coefficient zero at `v` +and coefficient one at every other coordinate. Thus only `v` edges stay +in a functional class. They form a matching on the cube. + +Let `a,b` be the current class sizes; let `e_0,e_1` count existing stay +edges in each class; let `c` count existing crossing edges. If `r=0`, +check the closing edge directly. The statements below concern `r>0`. +For each class `j`, count: + +- `p_j`: unused vertices whose `v` neighbor is a path endpoint; +- `q_j`: unordered `v` pairs with both vertices unused; +- `u_j`: all unused vertices in that class. + +For a proposed number `x` of new vertices in class zero, require +`0 <= x <= u_0` and `0 <= r-x <= u_1`. Put + +```text +x_0=x, x_1=r-x, s_0=a+x, s_1=b+r-x, +t_j=min(p_j,x_j), +M_j(x_j)=t_j+min(q_j,floor((x_j-t_j)/2)), +lo=max(c, 2 if s_0*s_1>0 else 0, + 2s_0-2(e_0+M_0(x_0)), 2s_1-2(e_1+M_1(x_1))), +hi=min(c+r+1, 2s_0-2e_0, 2s_1-2e_1). +``` + +**Every simple completion has an even integer in `[lo,hi]`.** +Consequently, reject the prefix if no feasible `x` has such an integer. +The `+1` in `c+r+1` counts the final edge to the start. It is required. +The returned split set is an outer bound; membership does not prove that +a completion exists. Universality is not needed for the theorem. + +## Proof + +Every internal path vertex already has its two cycle edges. A new stay +edge can therefore join an endpoint to an unused vertex, or join two +unused vertices. A stay edge between the two endpoints would close the +cycle before the `r>0` new vertices enter. Such an edge is not available. +An endpoint whose stay edge is already used has no unused `v` neighbor. + +All candidate stay edges are disjoint, since the `v` edges form a matching. +The first type costs one new vertex and the second costs two. With a +budget of `x_j` vertices, select as many one-vertex edges as possible, +then two-vertex edges. Exchanging a selected two-vertex edge for an +available one-vertex edge cannot decrease the edge count. This proves the +upper bound `M_j`. Ignoring other path constraints can only enlarge this +bound. Extra vertices need not contribute stay edges. + +Let `S_j` be the final stay counts and `C` the final crossing count. +Cycle degrees give `2s_j=2S_j+C`. We have +`e_j <= S_j <= e_j+M_j`, and `c <= C <= c+r+1`. +The final cycle crosses a cut an even number of times. If both classes +are nonempty, it crosses at least twice. Combining these inequalities +proves the interval test. The complete `r=0` case is a direct edge check. + +The input validation and proof explicitly exclude repeated vertices, +nonedges and the premature endpoint closure. The result applies to any +translated start vertex. The finite traversal fixes the start at zero, +which loses no cycle by cube translation. + +## Evidence + +The verifier visits every restricted-growth simple path through the target +length. It does not use the proposed condition to control traversal. At +each prefix it collects the exact set of final class splits from all +closed descendants, then checks containment in the proposed split set. +Every coordinate omission is checked. First-occurrence relabeling covers +every labeled word and preserves the complete family of these functionals. + +The domains `(n,L)` are `(3,6)`, `(4,8)`, `(4,10)` and `(5,12)`. +Their closed-cycle counts are `4,29,110,3695`. A second method enumerates +all literal words in the first two domains and agrees after canonical +relabeling. Exact counts and strict rejection witnesses are in +[RESULT.json](RESULT.json). The strict test compares with matching balance +and return distance; it does not assert a gain over every existing prune. + +An independent subset enumeration checks the greedy capacity formula. +Invalid-input controls test repeated vertices, a nonedge, an odd target, +an oversized target, an invalid coordinate, an out-of-cube vertex and a +one-vertex prefix. Both crossing and preserving closing edges pass, while +a nonedge closure fails. All checks use explicit exceptions under `-O`. + +## Reproduce + +Use CPython 3.12 and the standard library: + +```sh +python3.12 -B scripts/research_package.py --package research/f7-prefix-matching-capacity +python3.12 -I -W error -B research/f7-prefix-matching-capacity/verify.py +python3.12 -I -W error -O -B research/f7-prefix-matching-capacity/verify.py +``` + +Expected markers: `PASS_REGISTERED_RESEARCH_PACKAGE` and +`PASS_F7_PREFIX_MATCHING_CAPACITY`. Direct checks need no Git or network. +`--emit-receipt` writes regenerated JSON to standard output; ordinary +replay compares the exact receipt and writes no files. The receipt binds +all five source files by SHA-256. Source documents are provenance only. + +## Limits + +The written theorem is uniform in `n,L`; the exhaustive corroboration is +limited to the four listed domains. No formal proof kernel, independent +human proof review, seven-label census, supplier admission or selected +cold replay is claimed. The condition ignores most cross-edge adjacency +and can accept impossible completions. + +## Open next questions + +Does this condition reduce runtime in a maintained census? Start with an +opt-in implementation and compare full leaf receipts and measured time +against the unchanged traversal. The cost of the bound can exceed the +work saved. No performance or integration claim is made here. + +## Credit and sources + +Prepared for Ali Romman with substantial OpenAI Codex assistance. +New work is Apache-2.0. Nick Petalas supplied the matching-balance lemma in +[PR #4894](https://github.com/CrocSwap/integer-mult-bounds/pull/4894). +Mihir Srivastava supplied the explicit prefix-capacity question in +[PR #4907](https://github.com/CrocSwap/integer-mult-bounds/pull/4907). +Ross Richardson supplied the singleton-prefix model in +[PR #943](https://github.com/CrocSwap/integer-mult-bounds/pull/943), and +Nicholas Stone supplied the parity-prune correction in +[PR #2973](https://github.com/CrocSwap/integer-mult-bounds/pull/2973). +Their retained notices remain unchanged. Exact main-branch source pins +are in [SOURCES.json](SOURCES.json); no predecessor code is imported. +The base is `bee95ce88f9f19802f0613f92838895cd0e14a1f`, priority revision 7. diff --git a/research/five-label-prefix-completion/reference5001.py b/research/five-label-prefix-completion/reference5001.py new file mode 100644 index 0000000000..d09ac1fe43 --- /dev/null +++ b/research/five-label-prefix-completion/reference5001.py @@ -0,0 +1,206 @@ +#!/usr/bin/env python3 +"""Check the partial-prefix matching condition. Ali Romman, Codex assistance. + +Apache-2.0. Use explicit exceptions so checks remain active under -O. +""" +from collections import Counter +from itertools import product +from pathlib import Path +import hashlib +import json +import sys + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def feasible_splits(points, n, length, omitted): + require(type(n) is int and n >= 2 and type(length) is int + and 4 <= length <= 1 << n and length % 2 == 0, "invalid cycle domain") + require(type(omitted) is int and 0 <= omitted < n, "invalid omitted coordinate") + require(2 <= len(points) <= length and len(set(points)) == len(points), + "invalid prefix size") + require(all(type(q) is int and 0 <= q < 1 << n for q in points), "invalid vertex") + require(all((p ^ q).bit_count() == 1 for p, q in zip(points, points[1:])), + "invalid path edge") + remaining = length - len(points) + seen = set(points) + mask = ((1 << n) - 1) ^ (1 << omitted) + + def side(q): + return (q & mask).bit_count() % 2 + + a = sum(side(q) == 0 for q in points) + b = len(points) - a + stays = [0, 0] + crossing = 0 + for p, q in zip(points, points[1:]): + if side(p) == side(q): + stays[side(p)] += 1 + else: + crossing += 1 + if remaining == 0: + return {(a, b)} if (points[-1] ^ points[0]).bit_count() == 1 else set() + endpoints = {points[0], points[-1]} + cheap = [0, 0] + pairs = [0, 0] + available = [0, 0] + for q in range(1 << n): + if q not in seen: + j = side(q) + available[j] += 1 + mate = q ^ (1 << omitted) + if mate in endpoints: + cheap[j] += 1 + elif mate not in seen and q < mate: + pairs[j] += 1 + result = set() + for x in range(max(0, remaining-available[1]), min(remaining, available[0])+1): + totals = (a+x, b+remaining-x) + added = (x, remaining-x) + upper = [] + for j in (0, 1): + one = min(cheap[j], added[j]) + upper.append(stays[j] + one + min(pairs[j], (added[j]-one)//2)) + low = max(crossing, 2 if min(totals) > 0 else 0, + *(2*totals[j]-2*upper[j] for j in (0, 1))) + high = min(crossing+remaining+1, + *(2*totals[j]-2*stays[j] for j in (0, 1))) + low += low % 2 + if low <= high: + result.add(totals) + return result + + +def canonical(word): + names = {} + return tuple(names.setdefault(d, len(names)) for d in word) + + +def direct_words(n, length): + found = set() + for word in product(range(n), repeat=length): + points = [0] + for d in word: + points.append(points[-1] ^ (1 << d)) + if points[-1] == 0 and len(set(points[:-1])) == length: + found.add(canonical(word)) + return found + + +def scan(n, length): + counts = Counter() + witness = None + closed = set() + controls = {} + + def walk(word, points, highest): + nonlocal witness + counts["prefixes"] += 1 + actual = [set() for _ in range(n)] + if len(points) == length: + if points[-1].bit_count() == 1: + counts["cycles"] += 1 + closed.add(word + (points[-1].bit_length() - 1,)) + for v in range(n): + mask = ((1 << n) - 1) ^ (1 << v) + a = sum((q & mask).bit_count() % 2 == 0 for q in points) + actual[v].add((a, length - a)) + else: + for d in range(min(highest + 1, n - 1) + 1): + q = points[-1] ^ (1 << d) + if q not in points: + child = walk(word + (d,), points + (q,), max(highest, d)) + for v in range(n): + actual[v].update(child[v]) + if len(points) >= 2: + for v in range(n): + proposed = feasible_splits(points, n, length, v) + counts["split_checks"] += 1 + require(actual[v] <= proposed, "false completion prune") + counts["realizable_split_checks"] += len(actual[v]) + if not proposed: + counts["rejected_prefix_functionals"] += 1 + r = length - len(points) + mask = ((1 << n) - 1) ^ (1 << v) + a = sum((q & mask).bit_count() % 2 == 0 for q in points) + b = len(points) - a + global_ok = any(max(a+x, b+r-x) <= 2*min(a+x, b+r-x) + for x in range(r+1)) + if r > 0 and points[-1].bit_count() <= r+1 and global_ok: + counts["strict_rejections_before_leaf"] += 1 + if witness is None: + witness = {"word": word, "omitted": v, "points": points} + if actual[v] and any(a != b for a,b in actual[v]): + controls.setdefault("unbalanced_completion", (word, v)) + return actual + + walk((), (0,), -1) + if n <= 4 and length <= 8: + require(closed == direct_words(n, length), "independent word enumeration differs") + return {"n": n, "length": length, **dict(counts), "strict_witness": witness, + "unbalanced_completion_control": controls.get("unbalanced_completion")} + + +def capacity_checks(): + # Enumerate choices independently of the greedy capacity formula. + checked = 0 + for cheap in range(4): + for pairs in range(5): + for singles in range(4): + costs = (1,) * cheap + (2,) * pairs + for budget in range(cheap + 2*pairs + singles + 1): + best = max((sum(chosen) for chosen in product((0, 1), repeat=len(costs)) + if sum(c*t for c,t in zip(costs, chosen)) <= budget), default=0) + one = min(cheap, budget) + greedy = one + min(pairs, (budget-one)//2) + require(best == greedy, "matching capacity differs") + checked += 1 + return checked + + +def invalid_controls(): + cases = [((0,1,0),3,6,0), ((0,3),3,6,0), ((0,1),3,5,0), + ((0,1),3,10,0), ((0,1),3,6,3), ((0,8),3,6,0), ((0,),3,6,0)] + for args in cases: + try: + feasible_splits(*args) + except ValueError: + continue + raise ValueError("invalid input accepted") + # Both types of final edge remain legal. Reusing an old interior does not. + require(feasible_splits((0,1,3,2),2,4,0) == {(2,2)}, "crossing closure rejected") + require(feasible_splits((0,2,3,1),2,4,0) == {(2,2)}, "preserving closure rejected") + require(not feasible_splits((0,1,3,7),3,4,0), "non-edge closure accepted") + return len(cases) + 3 + + +def evidence(): + rows = [scan(n, length) for n,length in ((3,6),(4,8),(4,10),(5,12))] + require([r["cycles"] for r in rows] == [4,29,110,3695], "cycle counts changed") + require(all(r["strict_rejections_before_leaf"] > 0 for r in rows[1:]), "no strict gain") + result = {"schema": "f7-prefix-matching-capacity/v1", "scope": "simple cycles only", + "domains": rows, "capacity_cases": capacity_checks(), + "semantic_controls": invalid_controls()} + here = Path(__file__).resolve().parent + result["source_sha256"] = {name: hashlib.sha256((here/name).read_bytes()).hexdigest() + for name in ("README.md", "verify.py", "TASK.json", "VERIFY.json", "SOURCES.json")} + return result + + +def main(): + result = evidence() + encoded = json.dumps(result, indent=2, sort_keys=True) + "\n" + if sys.argv[1:] == ["--emit-receipt"]: + print(encoded, end="") + else: + require(not sys.argv[1:], "unexpected argument") + path = Path(__file__).resolve().with_name("RESULT.json") + require(path.read_text(encoding="utf-8") == encoded, "receipt differs") + print("PASS_F7_PREFIX_MATCHING_CAPACITY") + + +if __name__ == "__main__": + main() diff --git a/research/five-label-prefix-completion/test_mutations.py b/research/five-label-prefix-completion/test_mutations.py new file mode 100644 index 0000000000..bb72ef770c --- /dev/null +++ b/research/five-label-prefix-completion/test_mutations.py @@ -0,0 +1,73 @@ +#!/usr/bin/env python3 +"""Actual optimized-Python mutants with receipt comparison disabled. +Prepared for SHIN09-git with substantial OpenAI Codex assistance. Apache-2.0. +""" +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +MUTATIONS = ( + ("independent_future_pairs", "if not joint:", "if True:"), + ("drop_old_pairs", "possible = pair_support(points)", "possible = 0"), + ("drop_old_new_pairs", "possible |= 1 << (old ^ new)", "possible |= 0"), + ("strict_vertex_boundary", "+ x.bit_count() <= remaining)", "+ x.bit_count() < remaining)"), + ("omit_closing_edge", "remaining = length - len(points) + 1", "remaining = length - len(points)"), + ("omit_return_distance", "and (last ^ x).bit_count() + x.bit_count() <= remaining)", "and (last ^ x).bit_count() <= remaining)"), + ("disable_geometric_traversal_filter", + "return len(future) < 12 - len(points) or possible != (1 << 32) - 2", "return False"), +) + + +def run(directory, emit=False): + args = [sys.executable, "-I", "-O", "-B", str(directory / "verify.py")] + if emit: + args.append("--emit-receipt") + return subprocess.run(args, cwd=directory, capture_output=True, timeout=60) + + +def main(): + results = [] + with tempfile.TemporaryDirectory(prefix="five-label-prefix-") as temp: + root = Path(temp) + for source in HERE.iterdir(): + if source.is_file(): + shutil.copyfile(source, root / source.name) + positive = run(root) + if positive.returncode != 0 or b"PASS_FIVE_LABEL_PREFIX_COMPLETION" not in positive.stdout: + raise ValueError("source-only optimized positive control: " + positive.stderr.decode(errors="replace")) + original = (root / "bounds.py").read_text(encoding="utf-8") + for name, before, after in MUTATIONS: + if original.count(before) != 1: + raise ValueError("mutation target not unique: " + name) + (root / "bounds.py").write_text(original.replace(before, after), encoding="utf-8", newline="\n") + result = run(root, emit=True) + if result.returncode == 0: + raise ValueError("surviving semantic/claim mutant: " + name) + results.append({"name": name, "rejected": True, + "last_error": result.stderr.decode(errors="replace").splitlines()[-1]}) + (root / "bounds.py").write_text(original, encoding="utf-8", newline="\n") + receipt = (root / "RESULT.json").read_bytes() + altered = json.loads(receipt) + altered["oracle"]["simple_universal"] = True + (root / "RESULT.json").write_text(json.dumps(altered), encoding="utf-8") + result = run(root) + if result.returncode == 0 or b"complete deterministic receipt equality" not in result.stderr: + raise ValueError("typed receipt mutation not rejected by equality") + results.append({"name": "typed_receipt_boolean", "rejected": True}) + (root / "RESULT.json").write_bytes(receipt) + proof = root / "PROOF.md" + proof.write_bytes(proof.read_bytes() + b"\n") + result = run(root) + if result.returncode == 0 or b"complete deterministic receipt equality" not in result.stderr: + raise ValueError("proof-byte mutation not rejected by binding") + results.append({"name": "proof_byte_binding", "rejected": True}) + print(json.dumps({"positive_source_only_optimized": "PASS", "controls": results}, indent=2)) + + +if __name__ == "__main__": + main() + diff --git a/research/five-label-prefix-completion/verify.py b/research/five-label-prefix-completion/verify.py new file mode 100644 index 0000000000..45293496b9 --- /dev/null +++ b/research/five-label-prefix-completion/verify.py @@ -0,0 +1,282 @@ +#!/usr/bin/env python3 +"""Independent completion checks and a deterministic research receipt. +Prepared for SHIN09-git with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +from collections import Counter +from hashlib import sha256 +from itertools import permutations, product +import json +from pathlib import Path +from types import ModuleType + +HERE = Path(__file__).resolve().parent +BOUND_FILES = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", + "bounds.py", "oracle.py", "verify.py", "benchmark.py", "test_mutations.py", "OVERLAP.json", "TIMINGS-FINAL.json", + "compare_matching.py", "reference5001.py", "reference5001.md", "LICENSE") + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def load_source(name): + module = ModuleType(name) + path = HERE / (name + ".py") + module.__file__ = str(path) + exec(compile(path.read_bytes(), str(path), "exec"), module.__dict__) + return module + + +def digest(words): + return sha256("".join("".join(map(str, word)) + "\n" for word in sorted(words)).encode()).hexdigest() + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")) + + +def prefix_nodes(): + def walk(word, points, highest): + yield word, points, highest + if len(word) == 11: + return + for label in range(min(highest + 1, 4) + 1): + value = points[-1] ^ (1 << label) + if value not in points: + yield from walk(word + (label,), points + (value,), max(label, highest)) + yield from walk((), (0,), -1) + + +def independent_excess(points, mask): + value = 0 + for bit in (0, 1): + group = [x for x in points if sum((x >> j) & 1 for j in range(5) if mask >> j & 1) % 2 == bit] + multiplicities = Counter(x ^ y for x in group for y in group if x != y) + value += sum(count // 2 - 1 for count in multiplicities.values()) + return value + + +def literal_pair_envelope(points): + """Separate ordered-route implementation of the original E2 formula.""" + remaining = 13 - len(points) + last = points[-1] + pool = {x for x in range(32) if x not in points + and sum(v.bit_count() for v in (last ^ x, x)) <= remaining} + supported = {a ^ b for a in points for b in points if a != b} + supported.update(a ^ x for a in points for x in pool) + checked = 0 + for x in pool: + for y in pool: + if x != y and sum(v.bit_count() for v in (last ^ x, x ^ y, y)) <= remaining: + reflected = last ^ x ^ y + need(reflected in points or reflected in pool, "reflected endpoint lemma") + supported.add(x ^ y) + checked += 1 + return tuple(sorted(pool)), sum(1 << z for z in supported), checked + + +def small_raw_controls(bounds, oracle): + rows = [] + for n, length in ((3, 6), (4, 8)): + simple = universal = checks = 0 + for word in product(range(n), repeat=length): + state = 0 + for label in word: + state ^= 1 << label + if state: + continue + points, is_simple, is_universal = oracle.inspect(word, n) + if not is_simple: + continue + simple += 1 + universal += is_universal + actual = {a ^ b for a in points for b in points if a != b} + for depth in range(length): + prefix = points[:depth + 1] + pool, mask = bounds.tail_envelope(prefix, n, length) + need(set(points[depth + 1:]) <= set(pool), "small raw future containment") + need(all(mask >> value & 1 for value in actual), "small raw pair containment") + checks += 1 + rows.append({"n": n, "length": length, "raw_words": n ** length, + "simple_restored": simple, "universal": universal, "prefix_checks": checks}) + return rows + + +def semantic_controls(bounds, oracle): + errors = 0 + for word, n, length, token in ( + ((0, 0), 5, 12, "simple"), ((True,), 5, 12, "label"), + ((5,), 5, 12, "label"), ((-1,), 5, 12, "label"), + ((), True, 12, "dimension"), ((), 6, 12, "dimension"), + ((), 5, 11, "length"), (tuple(range(5)) * 3, 5, 12, "partial"), + ): + try: + bounds.completion_bound(word, n, length) + except ValueError as error: + need(token in str(error), "wrong invalid-input rejection") + errors += 1 + else: + raise ValueError("invalid-input accepted") + witness = tuple(map(int, "010201320")) + one = bounds.completion_bound(witness, joint=False) + two = bounds.completion_bound(witness, joint=True) + need(not one["reject"] and two["reject"], "strict envelope improvement") + need(two["future"] == (4, 10, 12, 16, 24) and two["missing"] == (20, 28), "literal missing-mask witness") + words = [] + for tail in product(range(5), repeat=3): + word = witness + tail + if any(word.count(j) % 2 for j in range(5)): + continue + points, simple, universal = oracle.inspect(word) + if simple: + words.append({"word": "".join(map(str, word)), "universal": universal, "labels": len(set(word))}) + need([x["word"] for x in words] == ["010201320232", "010201320434"], "literal suffix enumeration") + need(not any(x["universal"] for x in words), "witness universal suffix") + permutations_checked = 0 + sharp = tuple(map(int, "012343234031")) + for labels in permutations(range(5)): + word = tuple(labels[i] for i in sharp) + for depth in range(12): + need(not bounds.completion_bound(word[:depth])["reject"], "coordinate-permuted positive witness") + permutations_checked += 1 + p, simple, universal = oracle.inspect(tuple(map(int, "01021323")), 4) + bit0 = sum(len(g) * (len(g) - 1) // 2 - len({a ^ b for a in g for b in g if a != b}) + for g in ([x for x in p if x & 1 == b] for b in (0, 1))) + need(simple and universal and bit0 == 8 and 8 > 5, "credited bit-0 scope control") + return {"invalid_inputs": errors, "strict_witness": {"prefix": "010201320", **two}, + "restored_simple_suffixes": words, "coordinate_permuted_prefixes": permutations_checked, + "credited_low_weight_excess": bit0} + + +def calculate(): + sources = json.loads((HERE / "SOURCES.json").read_bytes()) + for row in sources["files"]: + if "vendored_as" in row: + need(sha256((HERE / row["vendored_as"]).read_bytes()).hexdigest() == row["sha256"], "frozen PR5001 bytes") + bounds = load_source("bounds") + oracle = load_source("oracle") + matching = load_source("compare_matching") + reference = load_source("reference5001") + oracle_counts, reference_closed, reference_hits = oracle.census() + modes = {} + for mode in bounds.MODES: + counts, closed, hits = bounds.search(mode) + need(hits == reference_hits, "complete universal word set: " + mode) + if mode == "none": + need(closed == reference_closed, "independent simple closed word set") + modes[mode] = {**counts, "universal_sha256": digest(hits)} + need((len(reference_closed), len(reference_hits)) == (3695, 828), "credited census calibration") + + table = {} + depths, rejections, extra_depths = Counter(), Counter(), Counter() + additional, class_additional = [], [] + matching_comparisons = 0 + reflected_pairs = 0 + also_matching_rejected = [] + for word, points, highest in prefix_nodes(): + first, one = bounds.tail_envelope(points, joint=False) + second, two = bounds.tail_envelope(points, joint=True) + need(first == second and two & ~one == 0, "nested envelope") + literal_pool, literal_support, pair_checks = literal_pair_envelope(points) + need(second == literal_pool and two == literal_support, "simplified/literal pair envelope equality") + reflected_pairs += pair_checks + flags = { + "remaining": bounds.remaining_reject(points, highest), + "union": bounds.union_reject(points), + "cap11": bounds.cap_reject(points), + "one_vertex": len(first) < 12 - len(points) or one != (1 << 32) - 2, + "two_vertex": len(second) < 12 - len(points) or two != (1 << 32) - 2, + } + lower = {mask: bounds.class_completion_lower(points, first, mask) for mask in bounds.MASKS} + flags["class_lower"] = any(x is None or x > 11 for x in lower.values()) + matching_splits = [] + if word: + for omitted in range(5): + proposed = matching.splits(points, omitted) + need(proposed == reference.feasible_splits(points, 5, 12, omitted), "literal PR5001 predicate equality") + matching_splits.append(proposed) + matching_comparisons += 1 + depths[len(word)] += 1 + for name, fired in flags.items(): + rejections[name] += fired + if flags["two_vertex"] and not any(flags[name] for name in ("remaining", "union", "cap11", "one_vertex")): + additional.append("".join(map(str, word))) + extra_depths[len(word)] += 1 + if any(not values for values in matching_splits): + also_matching_rejected.append("".join(map(str, word))) + if flags["class_lower"] and not any(flags[name] for name in ("remaining", "union", "cap11", "one_vertex")): + class_additional.append("".join(map(str, word))) + table[word] = (first, two, flags, lower, matching_splits) + + completion_checks = universal_checks = 0 + matching_containment_checks = 0 + live = set() + for word in reference_closed: + points, simple, universal = oracle.inspect(word) + need(simple, "oracle simple") + actual = {a ^ b for a in points for b in points if a != b} + final_excess = {mask: independent_excess(points, mask) for mask in bounds.MASKS} + if universal: + need(max(final_excess.values()) <= 11, "independent cap-11 domain check") + for depth in range(12): + key = word[:depth] + future, possible, flags, lower, matching_splits = table[key] + need(set(points[depth + 1:]) <= set(future), "actual future containment") + need(all(possible >> value & 1 for value in actual), "actual pair containment") + completion_checks += 1 + for omitted, splits in enumerate(matching_splits): + mask = 31 ^ (1 << omitted) + left = sum((x & mask).bit_count() % 2 == 0 for x in points) + need((left, 12 - left) in splits, "matching actual split containment") + matching_containment_checks += 1 + if universal: + need(not any(flags.values()), "false prune of universal completion") + need(all(lower[mask] is not None and lower[mask] <= final_excess[mask] for mask in bounds.MASKS), "excess completion lower bound") + universal_checks += 1 + live.add(key) + need(len(table) == 21640 and len(live) == 2427, "prefix coverage counts") + need(len(additional) == 67 and not class_additional, "incremental bound classification") + need(matching_comparisons == 108195 and not also_matching_rejected, "matching overlap classification") + need(modes["one_vertex"]["entered"] == 7519 and modes["two_vertex"]["entered"] == 7326, "paired-envelope traversal counts") + + return {"schema": "five-label-prefix-completion/v1", + "oracle": {**oracle_counts, "simple_closed_sha256": digest(reference_closed), + "universal_sha256": digest(reference_hits)}, + "prefixes": {"total": len(table), "by_depth": {str(k): v for k, v in depths.items()}, "live": len(live), + "literal_envelope_equalities": len(table), "reflected_ordered_pairs": reflected_pairs, + "closed_completion_checks": completion_checks, + "universal_completion_checks": universal_checks, + "predicate_rejections_on_full_domain": dict(rejections)}, + "modes": modes, "additional_joint_prefixes": additional, + "matching_comparison": {"literal_predicate_comparisons": matching_comparisons, + "actual_split_containment_checks": matching_containment_checks, + "joint_strict_prefixes_also_matching_rejected": also_matching_rejected, + "joint_strict_prefixes_passing_matching": len(additional)}, + "additional_by_depth": {str(k): v for k, v in extra_depths.items()}, "class_lower_additional": class_additional, + "small_raw_controls": small_raw_controls(bounds, oracle), + "controls": semantic_controls(bounds, oracle), + "source_sha256": {name: sha256((HERE / name).read_bytes()).hexdigest() for name in BOUND_FILES}} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit-receipt", action="store_true", help="Explicit authoring output; no files are changed.") + args = parser.parse_args() + actual = calculate() + if args.emit_receipt: + print(json.dumps(actual, indent=2, sort_keys=True)) + return + expected = json.loads((HERE / "RESULT.json").read_text(encoding="utf-8")) + need(canonical(actual) == canonical(expected), "complete deterministic receipt equality") + for corrupt in (True, 827): + changed = json.loads(canonical(actual)) + changed["oracle"]["simple_universal"] = corrupt + need(canonical(changed) != canonical(expected), "typed receipt control") + print("PASS_FIVE_LABEL_PREFIX_COMPLETION prefixes=21640 universal=828 joint_extra=67") + + +if __name__ == "__main__": + main() +