diff --git a/research/repeat-matching-debt/PROOF.md b/research/repeat-matching-debt/PROOF.md new file mode 100644 index 0000000000..6d626a18fc --- /dev/null +++ b/research/repeat-matching-debt/PROOF.md @@ -0,0 +1,119 @@ +# Matching balance with repeated visits + +This scoped proof was produced by Nick Petalas. Apache-2.0. + +## Statement + +Let n>=2, choose a coordinate v, and put + + f(x) = sum_{i != v} x_i mod 2. + +Let q_0,...,q_L=q_0 be a closed walk in Q_n. Every step flips exactly +one coordinate. Repeated vertices and repeated edges are permitted. Count +the L positions q_0,...,q_(L-1), excluding the final closing occurrence. +Let V be their distinct support. Assume V meets at least two pairs of +the coordinate-v matching. No universality assumption is needed. + +For j=0,1, let s_j be the number of vertices of V with f(x)=j, m_j the +number of coordinate-v edges whose two endpoints both lie in that class +of V, and R_j the number of occurrences in that class beyond its s_j +distinct vertices. Put c_j=s_j-m_j. Then + + R_0 >= max(0, c_1-s_0), + R_1 >= max(0, c_0-s_1). (1) + +Consequently, with D the sum of the two right sides, + + L-|V| >= D, + L-|V| == |V| mod 2. (2) + +The congruence uses the fact that Q_n is bipartite, so L is even. Thus +one may round D upward to the next integer of the parity of |V|. +These are necessary conditions and need not imply a completion. + +## Proof of the bounds + +Contract every coordinate-v matching edge in the entire cube. Each pair +becomes one quotient vertex. Its color f is well defined, and every +remaining edge changes that color. An occupied quotient vertex contains +one or two vertices of V. A fully occupied pair saves one quotient vertex +relative to s_j, so there are exactly c_j occupied quotient vertices of +color j. + +Delete the stationary steps from the projected closed walk. Since V +meets at least two matching pairs, the resulting closed walk has a +positive number C of edges and visits every occupied quotient vertex. +Every visited vertex of a nonempty closed walk has at least one arrival +and one departure, counting edge multiplicity. Each crossing edge has +exactly one endpoint of each color. Therefore + + C >= 2c_0, C >= 2c_1. + +In the original walk there are a_j=s_j+R_j occurrences of color j. +Each contributes two incident edge occurrences. Every projected edge +uses one incidence in each color, whereas a stationary step contributes +no crossing incidence. Hence + + C <= 2a_0, C <= 2a_1. + +Combining the lower bound from the opposite color with these upper +bounds gives c_1<=s_0+R_0 and c_0<=s_1+R_1. This proves (1). +Summing proves the inequality in (2). Bipartiteness proves its congruence. + +The two-pair hypothesis matters. A two-step walk on a single matching +edge has s_0=2,m_0=1,s_1=0 and no repetitions, contrary to the proposed +bound if that hypothesis were removed. Such a support is rejected by +the executable interface rather than silently treated by the formula. + +For a simple cycle R_0=R_1=0, so (1) implies c_0<=s_1 and c_1<=s_0. +Since m_j<=floor(s_j/2), this includes the familiar s_0<=2s_1 and +s_1<=2s_0 simple matching balance. The new bounds retain actual occupied +pairs and quantify how repeats pay for imbalance. + +## Prefix corollary with a prescribed final support + +Fix V, L and a prefix q_0,...,q_(k-1) contained in V. It may repeat. +Let r_j be the prefix's occurrence count in class j minus its distinct +count in that class. For any completion visiting exactly V, + + ell_0 = max(r_0, 0, c_1-s_0), + ell_1 = max(r_1, 0, c_0-s_1), + ell_0 <= R_0 <= L-|V|-ell_1. (3) + +Each repeated occurrence already in the prefix remains a repeated +occurrence in any extension. Apply (1) as well, then use +R_0+R_1=L-|V|. An empty interval in (3) rejects that specified completion +support. A nonempty interval leaves all other walk conditions open. +The support V must be prescribed or independently bounded. Substituting +the current partial support for an unknown final support is unjustified. + +## An unbounded attaining family + +For k>=1 use coordinates 0,1,...,k and omit coordinate 0. Set + + V_k = {0,e_0} union {e_i,e_i+e_0 : 1<=i<=k}. + +This is a book of k squares sharing edge {0,e_0}. Its distinct size is +2k+2. Class zero consists of the two hubs, so s_0=2,m_0=1,c_0=1. +Class one consists of the leaf pairs, so s_1=2k,m_1=k,c_1=k. For k>=2, +the bound is R_0>=k-2 and R_1>=0. For k=1 both right sides are zero. +Since |V_k| is even, the minimum permitted repetition total is + + 0 if k=1, + k-2+(k mod 2) if k>=2. + +Traverse the k paths + + 0 -> e_i -> e_i+e_0 -> e_0 + +in alternating orientations. If k is odd, close by the shared hub edge. +For even k the last path already returns to zero. The resulting walk +visits exactly V_k and has length 3k+(k mod 2). It attains the rounded +bound in every k>=1. Thus the minimum length among closed walks with +exactly this support is 3k+(k mod 2). Embedding the support in a larger +cube preserves the argument if the visited support remains V_k. + +No universal prefix-cover property is asserted for this family. Its role +is to show that the repeat-aware bound has sharp, arbitrarily large debt. +The contribution stops at this lemma and prefix corollary; it supplies +neither an unknown-support completion algorithm nor a census integration. diff --git a/research/repeat-matching-debt/README.md b/research/repeat-matching-debt/README.md new file mode 100644 index 0000000000..c9b9ad1b48 --- /dev/null +++ b/research/repeat-matching-debt/README.md @@ -0,0 +1,49 @@ +# Repeated-visit debt for omitted-coordinate matching cuts + +This scoped written proof and exact finite evidence were produced by Nick Petalas. Apache-2.0. + +For a closed singleton walk in Q_n, omit one coordinate v from the parity functional. Let s_j be the distinct visited vertices in class j, m_j the occupied coordinate-v matching pairs in that class, and R_j its repeated occurrences. Provided the support meets at least two matching components, + +```text +R_0 >= max(0, s_1-m_1-s_0) +R_1 >= max(0, s_0-m_0-s_1). +``` + +The proof contracts the coordinate matching and counts crossing incidences. It permits repeated vertices and edges, in every dimension and length. With a prescribed final support, already consumed prefix repetitions give a necessary interval for the remaining repetition allocation. This supplies one new part of the repeat-capable contract explicitly left open in [JoyboyBrian's PR5033](https://github.com/CrocSwap/integer-mult-bounds/pull/5033). It does not provide the full missing capacity predicate. + +A k-page hypercube book attains the parity-rounded repetition bound for every k>=1. Its support has 2k+2 vertices and exact minimum closed covering length 3k+(k mod 2). These witnesses establish sharpness of the new bound. They are not asserted to be universal paired-readout covers. + +[PROOF.md](PROOF.md) gives the full argument, the necessary two-component hypothesis, the prefix corollary and the attaining walks. [TASK.json](TASK.json) records the explicit change from the audit card to original combinatorial work and the structured Open next questions. + +## Evidence and reproduction + +The standard-library verifier enumerates every labeled closed singleton word in ten fixed domains with n=2,3,4 and lengths through ten, including repeated vertices. For every supported coordinate omission it checks the inequality and every prefix against its literal completion. The generated [RESULT.json](RESULT.json) gives exact enumerated counts and hashes of all seven source files. It also records sixteen attaining book fixtures. A separate breadth-first state search finds the optimum closed covering length for the first five book supports. Neither checker imports predecessor code or replays predecessor scientific suites. + +From the worktree root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/repeat-matching-debt/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/repeat-matching-debt/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/repeat-matching-debt +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/repeat-matching-debt --check-source-history +``` + +An installed CPython 3.12 can replace the recorded interpreter path. Expected markers are `PASS_REPEAT_MATCHING_DEBT`, `PASS_REGISTERED_RESEARCH_PACKAGE` and `PASS_RESEARCH_COMMIT_BYTES`. Direct checks need no Git or network and write no files. `--emit-receipt` prints regenerated, source-hash-bound JSON to stdout. Normal and optimized executions use explicit exceptions. + +## Scope and credit + +Claim type: scoped combinatorial proof with exact finite corroboration. No new kappa, f(7) decision, seven-label exclusion, census runtime gain, physical/native supplier, selected-frontier change or complete multiplication theorem is claimed. Unknown final supports cannot be silently replaced by the current prefix support. Completion adjacency, universality, dirty restoration, paid invoices and all five framework assumptions remain separate. Independent human and formal proof-kernel review are unclaimed. + +Credit JoyboyBrian / PR5033 for the explicit repeat-capable question and engine gate; Ali Romman / PR5001 for simple-prefix capacity; Nick Petalas / PR4894 for simple matching balance; Mihir Srivastava / PR4907, Ross Richardson / PR943, Nicholas Stone / PR2973 and the retained singleton-walk lineage. Matching contraction and closed-walk degree counting are classical. No global literature-priority claim is made. Exact predecessor README pins in SOURCES.json are provenance only. Existing predecessor credits are unchanged. + +Canonical main was checked at 7c49fe32c55de02c2c873655c804b16e4c3fef0a, priority revision 8, selected PR6030. The card's baseline command passed source-binding orientation only. Live claims, reservations, main object/formula terms, open and merged work and recent account work were checked. Sparse notes, arbitrary historical diffs and unpublished work remain coverage limits. [Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19361705). + +## Open next questions + +Can one derive final-support bounds from a repeat-capable census target and maintain them cheaply enough to use the new inequality? Begin with one exact target split. The prescribed-support condition alone does not authorize the old simple-prefix gate or a larger census. + +## Verifier constraints + +The executable accepts n<=17, at most 64 support vertices and length<=64. The mathematical proof has no such caps. Exhaustion checks use ten fixed Cartesian-product domains, each at most 4^8 or 3^10 words. The independent breadth-first oracle has at most 12*2^12 states; its five supports are fixed. File reads are capped at two MiB per named package source. No recursion, subprocesses, network access, dynamic evaluation or background work occurs. Every function is under sixty physical lines. + +Power-of-ten rule 3 deviation: CPython allocates managed integers, tuples, sets and queue entries during replay. Fixed domains and explicit state bounds limit live storage; this is not a fixed-allocation implementation. Python has no compiler warning mode; both registered checks use warning-strict execution and retain contracts under optimization. One explicit local import path makes the same package module available under isolated Python; no external package is loaded. No shared code or frozen evidence is changed. diff --git a/research/repeat-matching-debt/RESULT.json b/research/repeat-matching-debt/RESULT.json new file mode 100644 index 0000000000..aa89c521e2 --- /dev/null +++ b/research/repeat-matching-debt/RESULT.json @@ -0,0 +1,230 @@ +{ + "controls": 15, + "schema_version": 1, + "sharp_family": [ + { + "debt": 0, + "distinct": 4, + "length": 4, + "pages": 1, + "repetitions": 0 + }, + { + "debt": 0, + "distinct": 6, + "length": 6, + "pages": 2, + "repetitions": 0 + }, + { + "debt": 1, + "distinct": 8, + "length": 10, + "pages": 3, + "repetitions": 2 + }, + { + "debt": 2, + "distinct": 10, + "length": 12, + "pages": 4, + "repetitions": 2 + }, + { + "debt": 3, + "distinct": 12, + "length": 16, + "pages": 5, + "repetitions": 4 + }, + { + "debt": 4, + "distinct": 14, + "length": 18, + "pages": 6, + "repetitions": 4 + }, + { + "debt": 5, + "distinct": 16, + "length": 22, + "pages": 7, + "repetitions": 6 + }, + { + "debt": 6, + "distinct": 18, + "length": 24, + "pages": 8, + "repetitions": 6 + }, + { + "debt": 7, + "distinct": 20, + "length": 28, + "pages": 9, + "repetitions": 8 + }, + { + "debt": 8, + "distinct": 22, + "length": 30, + "pages": 10, + "repetitions": 8 + }, + { + "debt": 9, + "distinct": 24, + "length": 34, + "pages": 11, + "repetitions": 10 + }, + { + "debt": 10, + "distinct": 26, + "length": 36, + "pages": 12, + "repetitions": 10 + }, + { + "debt": 11, + "distinct": 28, + "length": 40, + "pages": 13, + "repetitions": 12 + }, + { + "debt": 12, + "distinct": 30, + "length": 42, + "pages": 14, + "repetitions": 12 + }, + { + "debt": 13, + "distinct": 32, + "length": 46, + "pages": 15, + "repetitions": 14 + }, + { + "debt": 14, + "distinct": 34, + "length": 48, + "pages": 16, + "repetitions": 14 + } + ], + "source_sha256": { + "PROOF.md": "fccea905ccf974a0fad56eb0551c63c68ec48fa9354ccf523af66fa3e04648e0", + "README.md": "b7f13c0123dc304edb2072e439588850b6e4e04a038821dcb46c37e0ebd60856", + "SOURCES.json": "4463f6a51aa9e89696902f8ad7d0a6dbdd9480e5d7256a37fbf87d83a2ba1b50", + "TASK.json": "518d871493b4f2ed8b28933b37822db708397d416ab5d3228fa87fc2a588152d", + "VERIFY.json": "b458598205203e6d3c1ee4e0110a74663a6a088f40764a99300d70889e54db9d", + "model.py": "13619a011af26aaf8d3f820b13fea7395177c7bd1f2c5d1ec5c229ff6f2d2196", + "verify.py": "976ae8e195fd545855622c1d0577f402c4575180b79bcb30119bfaf726b24f79" + }, + "status": "PASS_REPEAT_MATCHING_DEBT", + "walk_domains": [ + { + "closed_words": 8, + "excluded_one_component": 2, + "length": 4, + "n": 2, + "prefix_omissions": 56, + "repeated_words": 6, + "universal_words": 6, + "walk_omissions": 14 + }, + { + "closed_words": 32, + "excluded_one_component": 2, + "length": 6, + "n": 2, + "prefix_omissions": 372, + "repeated_words": 32, + "universal_words": 30, + "walk_omissions": 62 + }, + { + "closed_words": 128, + "excluded_one_component": 2, + "length": 8, + "n": 2, + "prefix_omissions": 2032, + "repeated_words": 128, + "universal_words": 126, + "walk_omissions": 254 + }, + { + "closed_words": 21, + "excluded_one_component": 3, + "length": 4, + "n": 3, + "prefix_omissions": 240, + "repeated_words": 15, + "universal_words": 0, + "walk_omissions": 60 + }, + { + "closed_words": 183, + "excluded_one_component": 3, + "length": 6, + "n": 3, + "prefix_omissions": 3276, + "repeated_words": 159, + "universal_words": 60, + "walk_omissions": 546 + }, + { + "closed_words": 1641, + "excluded_one_component": 3, + "length": 8, + "n": 3, + "prefix_omissions": 39360, + "repeated_words": 1629, + "universal_words": 1092, + "walk_omissions": 4920 + }, + { + "closed_words": 14763, + "excluded_one_component": 3, + "length": 10, + "n": 3, + "prefix_omissions": 442860, + "repeated_words": 14763, + "universal_words": 12570, + "walk_omissions": 44286 + }, + { + "closed_words": 40, + "excluded_one_component": 4, + "length": 4, + "n": 4, + "prefix_omissions": 624, + "repeated_words": 28, + "universal_words": 0, + "walk_omissions": 156 + }, + { + "closed_words": 544, + "excluded_one_component": 4, + "length": 6, + "n": 4, + "prefix_omissions": 13032, + "repeated_words": 448, + "universal_words": 0, + "walk_omissions": 2172 + }, + { + "closed_words": 8320, + "excluded_one_component": 4, + "length": 8, + "n": 4, + "prefix_omissions": 266208, + "repeated_words": 7624, + "universal_words": 624, + "walk_omissions": 33276 + } + ] +} diff --git a/research/repeat-matching-debt/SOURCES.json b/research/repeat-matching-debt/SOURCES.json new file mode 100644 index 0000000000..98012c250a --- /dev/null +++ b/research/repeat-matching-debt/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/f7-prefix-capacity-engine/README.md", + "usage": "provenance", + "git_blob": "c3d6678f2f563f366a109d1d92262bb8ee02116b", + "sha256": "ab5ed05ef6d649c784732a82de9ac00b2cc96d5a322b6e76d3edd0800d1badef" + }, + { + "path": "research/f7-prefix-matching-capacity/README.md", + "usage": "provenance", + "git_blob": "f5251a7b370d791c1aff734ef805271b807eadfb", + "sha256": "dfaacf1af0c1c4f4365f8c03fdcb03a28d7b90e601e8a1204f71b9cab6bfd26c" + } + ] +} diff --git a/research/repeat-matching-debt/TASK.json b/research/repeat-matching-debt/TASK.json new file mode 100644 index 0000000000..b105211665 --- /dev/null +++ b/research/repeat-matching-debt/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "census-pruning-audit", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "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": "A repeat-aware matching-balance theorem and prescribed-support prefix corollary for closed singleton walks, with an unbounded attaining family.", + "scope_change_reason": "The assignment requires original research rather than a parity-pruning audit. Take the distinct repeat-capable contract explicitly left open by JoyboyBrian PR5033; do not audit or modify an existing engine.", + "bottleneck_link": "Necessary completion inequalities can constrain repeated-prefix searches for cheaper paired-readout connector words. This is a local combinatorial enabling result, not a changed supplier invoice.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved repeat-aware bound and bounded exact evidence. No larger census or engine integration.", + "outcome": "completed", + "evidence": "Written uniform proof, exhaustive closed-walk and prefix checks, attaining book walks and independent small shortest-cover searches; generated counts are in RESULT.json.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can the prescribed-support repetition bound become a useful unknown-support prefix condition in a repeat-capable census?", + "why_it_matters": "The present inequality does not by itself justify enabling the existing simple-prefix capacity gate.", + "first_step": "Derive sound lower bounds on final component counts and class sizes from one exact repeat-capable target split. Price the per-node maintenance before integration.", + "blocked_by": "The final support is not prescribed in the maintained census; completion adjacency and universality remain separate." + } + ], + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19361705", + "upstream_checkpoint": { + "commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "priority_revision": 8, + "checked_at": "2026-11-02T22:20:00Z" + } +} diff --git a/research/repeat-matching-debt/VERIFY.json b/research/repeat-matching-debt/VERIFY.json new file mode 100644 index 0000000000..a75675ba09 --- /dev/null +++ b/research/repeat-matching-debt/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 240, + "checks": "New repetition theorem, prescribed-support prefix corollary, complete bounded repeated-walk domains, sharp family, shortest-cover oracles and rejecting controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 240, + "checks": "The same complete checks with assertions disabled; executable contracts must remain active." + } + ] +} diff --git a/research/repeat-matching-debt/model.py b/research/repeat-matching-debt/model.py new file mode 100644 index 0000000000..e81fc367b4 --- /dev/null +++ b/research/repeat-matching-debt/model.py @@ -0,0 +1,71 @@ +"""Repeat-aware matching balance. Produced by Nick Petalas. Apache-2.0. + +The written theorem has no dimension or length cap; these caps bound replay. +""" + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def color(vertex: int, omitted: int) -> int: + return (vertex & ~(1 << omitted)).bit_count() & 1 + + +def support_data(n: int, omitted: int, support: frozenset[int]) -> dict: + require(type(n) is int and 2 <= n <= 17, "dimension outside 2..17") + require(type(omitted) is int and 0 <= omitted < n, "invalid omission") + require(isinstance(support, frozenset), "support must be a frozenset") + require(2 <= len(support) <= 64, "support size outside 2..64") + require(all(type(x) is int and 0 <= x < 1 << n for x in support), + "vertex outside cube") + projected = {x & ~(1 << omitted) for x in support} + require(len(projected) >= 2, "support lies in one matching component") + sizes = tuple(sum(color(x, omitted) == j for x in support) for j in (0, 1)) + pairs = tuple(sum(color(x, omitted) == j and x ^ (1 << omitted) in support + for x in support) // 2 for j in (0, 1)) + components = tuple(sizes[j] - pairs[j] for j in (0, 1)) + debt = (max(0, components[1] - sizes[0]), + max(0, components[0] - sizes[1])) + return {"sizes": sizes, "pairs": pairs, "components": components, + "debt": debt} + + +def prefix_budget(n: int, omitted: int, support: frozenset[int], + length: int, prefix: tuple[int, ...]) -> dict: + """Necessary budgets for completions with exactly this visited support. + + Prefix positions exclude the final closing occurrence. Repeats are allowed. + Passing this check does not promise a completion. + """ + data = support_data(n, omitted, support) + require(type(length) is int and 4 <= length <= 64 and length % 2 == 0, + "length must be even in 4..64") + require(len(support) <= length, "more distinct vertices than positions") + require(isinstance(prefix, tuple) and 1 <= len(prefix) <= length, + "invalid prefix size") + require(all(type(x) is int and x in support for x in prefix), + "prefix outside prescribed support") + require(all((x ^ y).bit_count() == 1 for x, y in zip(prefix, prefix[1:])), + "prefix contains a nonedge") + counts = tuple(sum(color(x, omitted) == j for x in prefix) for j in (0, 1)) + unique = frozenset(prefix) + seen = tuple(sum(color(x, omitted) == j for x in unique) for j in (0, 1)) + used = tuple(counts[j] - seen[j] for j in (0, 1)) + lower = tuple(max(used[j], data["debt"][j]) for j in (0, 1)) + total = length - len(support) + interval = (lower[0], total - lower[1]) + return {**data, "used": used, "lower": lower, "total": total, + "repeat_zero_interval": interval, "possible": interval[0] <= interval[1]} + + +def book_walk(pages: int) -> tuple[int, ...]: + require(type(pages) is int and 1 <= pages <= 16, "pages outside 1..16") + walk = [0] + for i in range(pages): + leaf = 1 << (i + 1) + walk.extend((leaf, leaf | 1, 1) if i % 2 == 0 else (leaf | 1, leaf, 0)) + if walk[-1] != 0: + walk.append(0) + return tuple(walk) diff --git a/research/repeat-matching-debt/verify.py b/research/repeat-matching-debt/verify.py new file mode 100644 index 0000000000..2eadac0838 --- /dev/null +++ b/research/repeat-matching-debt/verify.py @@ -0,0 +1,190 @@ +"""Exact new-result checks. Produced by Nick Petalas. Apache-2.0.""" + +import argparse +from collections import deque +import hashlib +from itertools import product +import json +from pathlib import Path +import sys + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +from model import book_walk, color, prefix_budget, require, support_data + + +def walk(word: tuple[int, ...]) -> tuple[int, ...]: + path = [0] + for bit in word: + path.append(path[-1] ^ (1 << bit)) + require(path[-1] == 0, "fixture does not close") + return tuple(path) + + +def check_walk(n: int, path: tuple[int, ...], omitted: int) -> int: + positions = path[:-1] + support = frozenset(positions) + projected = {x & ~(1 << omitted) for x in support} + if len(projected) < 2: + return 0 # Explicitly excluded domain, counted separately. + data = support_data(n, omitted, support) + # Independent contraction by set pairs, without the model's pair formula. + cells = {frozenset((x, x ^ (1 << omitted))) for x in support} + components = tuple(sum(color(min(cell), omitted) == j for cell in cells) + for j in (0, 1)) + require(components == data["components"], "component count mismatch") + occurrences = tuple(sum(color(x, omitted) == j for x in positions) + for j in (0, 1)) + repeats = tuple(occurrences[j] - data["sizes"][j] for j in (0, 1)) + crossing = sum(color(x, omitted) != color(y, omitted) + for x, y in zip(path, path[1:])) + require(crossing % 2 == 0, "odd closed-cut crossing count") + require(crossing >= 2 * max(components), "component crossing floor") + require(all(repeats[j] >= data["debt"][j] for j in (0, 1)), + "repetition bound failed") + for k in range(1, len(path)): + budget = prefix_budget(n, omitted, support, len(positions), positions[:k]) + lo, hi = budget["repeat_zero_interval"] + require(budget["possible"] and lo <= repeats[0] <= hi, + "a literal completion was rejected") + return len(positions) + + +def exhaustive_walks() -> list[dict]: + results = [] + domains = ((2, 4), (2, 6), (2, 8), (3, 4), (3, 6), (3, 8), + (3, 10), (4, 4), (4, 6), (4, 8)) + for n, length in domains: + closed = checked = excluded = prefixes = repeated = universal = 0 + for word in product(range(n), repeat=length): + if any(word.count(j) % 2 for j in range(n)): + continue + path = walk(word) + support = frozenset(path[:-1]) + closed += 1 + repeated += len(support) < length + universal += len({x ^ y for x in support for y in support}) == 1 << n + for omitted in range(n): + count = check_walk(n, path, omitted) + checked += count != 0 + excluded += count == 0 + prefixes += count + results.append({"n": n, "length": length, "closed_words": closed, + "repeated_words": repeated, "universal_words": universal, + "walk_omissions": checked, "excluded_one_component": excluded, + "prefix_omissions": prefixes}) + return results + + +def shortest_cover(support: frozenset[int], n: int) -> int: + """Independent BFS over every support-restricted walk, including repeats.""" + vertices = sorted(support) + require(len(vertices) <= 12, "BFS fixture exceeds twelve vertices") + bit = {x: 1 << i for i, x in enumerate(vertices)} + full = (1 << len(vertices)) - 1 + initial = (bit[0], 0) + queue = deque([(initial, 0)]) + seen = {initial} + capacity = len(vertices) * (1 << len(vertices)) + for _ in range(capacity): + if not queue: + break + (mask, x), distance = queue.popleft() + if mask == full and x.bit_count() == 1: + return distance + 1 + for axis in range(n): + y = x ^ (1 << axis) + if y in support: + state = (mask | bit[y], y) + if state not in seen: + seen.add(state) + queue.append((state, distance + 1)) + raise ValueError("BFS found no closed covering walk") + + +def sharp_family() -> list[dict]: + rows = [] + for pages in range(1, 17): + path = book_walk(pages) + length = len(path) - 1 + support = frozenset(path[:-1]) + require(length == 3 * pages + pages % 2, "book length") + require(len(support) == 2 * pages + 2, "book support") + check_walk(pages + 1, path, 0) + data = support_data(pages + 1, 0, support) + debt = sum(data["debt"]) + rounded = debt + ((debt - len(support)) % 2) + require(length - len(support) == rounded, "unattained rounded debt") + if pages <= 5: + require(shortest_cover(support, pages + 1) == length, "BFS optimum") + rows.append({"pages": pages, "length": length, "distinct": len(support), + "debt": debt, "repetitions": length - len(support)}) + return rows + + +def controls() -> int: + path = book_walk(3) + support = frozenset(path[:-1]) + rejected = 0 + cases = ((1, 0, support, 10, (0,)), (4, 4, support, 10, (0,)), + (4, 0, support, 9, (0,)), (4, 0, support, 6, (0,)), + (4, 0, support, 66, (0,)), (4, 0, support, 10, (0, 3)), + (4, 0, support, 10, (0, 16)), (4, 0, support, 10, ()), + (4, 0, frozenset((0, 1)), 4, (0,))) + for args in cases: + try: + prefix_budget(*args) + except ValueError: + rejected += 1 + else: + raise ValueError("malformed input was accepted") + require(not prefix_budget(4, 0, support, 8, (0,))["possible"], "lost debt") + square = frozenset((0, 1, 2, 3)) + require(not prefix_budget(2, 0, square, 4, (0, 1, 0))["possible"], + "lost prefix repeats") + require(prefix_budget(4, 0, support, 10, (0,))["possible"], "positive budget") + require(not prefix_budget(4, 0, support, 10, (0, 2, 0, 2, 0))["possible"], + "lost class-specific budget") + simple = book_walk(2) + data = support_data(3, 0, frozenset(simple[:-1])) + require(sum(data["debt"]) == 0, "simple positive control") + require(data["sizes"][1] - data["sizes"][0] == 2, + "pair-omission mutation not detected") + return rejected + 6 + + +def receipt() -> dict: + root = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", + "model.py", "verify.py") + hashes = {} + for name in names: + raw = (root / name).read_bytes() + require(len(raw) <= 2 * 1024 * 1024, "oversized package source") + hashes[name] = hashlib.sha256(raw).hexdigest() + return {"schema_version": 1, "source_sha256": hashes, + "walk_domains": exhaustive_walks(), "sharp_family": sharp_family(), + "controls": controls(), "status": "PASS_REPEAT_MATCHING_DEBT"} + + +def main() -> None: + parser = argparse.ArgumentParser() + parser.add_argument("--emit-receipt", action="store_true") + args = parser.parse_args() + result = receipt() + if args.emit_receipt: + print(json.dumps(result, indent=2, sort_keys=True)) + else: + root = Path(__file__).resolve().parent + raw = (root / "RESULT.json").read_bytes() + require(len(raw) <= 2 * 1024 * 1024, "oversized receipt") + require(json.loads(raw) == result, "receipt or source mismatch") + print(result["status"]) + print(json.dumps({"closed_words": sum(x["closed_words"] for x in result["walk_domains"]), + "walk_omissions": sum(x["walk_omissions"] for x in result["walk_domains"]), + "prefix_omissions": sum(x["prefix_omissions"] for x in result["walk_domains"]), + "attaining_fixtures": len(result["sharp_family"]), + "controls": result["controls"]}, sort_keys=True)) + + +if __name__ == "__main__": + main()