From 4fece6ddc4dff91ea1bbfd820f6c447c9a38387c Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Wed, 28 Oct 2026 16:27:18 +0000 Subject: [PATCH] feat(research): prove exact odd-cycle target deletion budgets --- research/odd-unicyclic-star-budgets/PROOF.md | 161 ++++++++++ research/odd-unicyclic-star-budgets/README.md | 112 +++++++ .../odd-unicyclic-star-budgets/SOURCES.json | 24 ++ research/odd-unicyclic-star-budgets/TASK.json | 76 +++++ .../odd-unicyclic-star-budgets/VERIFY.json | 34 ++ research/odd-unicyclic-star-budgets/verify.py | 296 ++++++++++++++++++ 6 files changed, 703 insertions(+) create mode 100644 research/odd-unicyclic-star-budgets/PROOF.md create mode 100644 research/odd-unicyclic-star-budgets/README.md create mode 100644 research/odd-unicyclic-star-budgets/SOURCES.json create mode 100644 research/odd-unicyclic-star-budgets/TASK.json create mode 100644 research/odd-unicyclic-star-budgets/VERIFY.json create mode 100644 research/odd-unicyclic-star-budgets/verify.py diff --git a/research/odd-unicyclic-star-budgets/PROOF.md b/research/odd-unicyclic-star-budgets/PROOF.md new file mode 100644 index 0000000000..5e62a69e8d --- /dev/null +++ b/research/odd-unicyclic-star-budgets/PROOF.md @@ -0,0 +1,161 @@ +# Exact budgets for prescribed targets with one odd cycle + +This scoped theorem was produced by Nick Petalas. It extends Sam Sung's +[graph-target note](../asymmetric-hypercube-decoder/GRAPH-TARGETS.md), from +PR #669. That note supplies the observation model, the unit-row criterion, +the general nonzero-constant lower bound, and the triangle specialization. +The new contribution is attainment for every prescribed target set with +exactly one cycle in total, provided that cycle is odd. The lower-bound +argument is included to make the extension readable on its own. + +## Statement + +Let p >= 3, and let G be the complete graph on n = 2p vertices with a +perfect matching removed. Its E = 2p(p-1) edges are the signed two-ports. +All vector spaces in this note are over F2. + +For a retained edge set F, the available observations are the vertex sums + + star_v(F) = sum_{e in F, v in e} x_e + +and the empty star `sum_{e in F} x_e`. This is the source's C+ code. At k=2, +the permitted overlap correction for target uv is star_u + star_v and +therefore adds no observation. Every retained input x_e is arbitrary and +independent. + +Let T be a prescribed target edge set. Assume the spanning graph with edges +T has exactly one cycle in total, of odd length. It may also have trees +attached to that cycle, other tree components and isolated vertices. +Write r = |T| and s = n-r+1, the number of components of T, including +isolated vertices. Then the minimum number of deleted edges disjoint from +T that makes every x_t, t in T, individually recoverable is + + delta_+(T) = 2p(p-1) - r - floor((2p-r+1)^2 / 4). (1) + +In particular, the optimum depends only on p and r within this class. +Formula (1) applies to every p, with no upper bound imposed by the finite +checker. Without the empty star such a cyclic target set is infeasible, +as already proved in the source's feasibility criterion. + +## The inherited lower bound + +Combine r individual unit decoders into a vector decoder. It assigns each +vertex v a coefficient a_v in F2^r and the empty star a coefficient b. +At a retained edge uv the coefficient is a_u + a_v + b. It must be the +corresponding standard basis vector e_t for t in T and zero on every +retained nontarget edge. If recovery uses arbitrary exact postprocessing of +these linear observations, the same criterion still applies: an input +coordinate recoverable on every input vanishes on the observation kernel, +and hence belongs to its row space. + +Summing the target equations around the unique odd cycle gives + + b = sum_{t on the cycle} e_t != 0. (2) + +Let H be the retained nontarget graph, with h components including isolated +vertices. On every edge of H, a_u + a_v = b. Thus H is bipartite. In each +component choose a root with coefficient c_i and write +a_v = c_i + sigma_v b, where sigma_v is the path parity from that root. +The target coefficients all lie in the span of b and the vectors c_i+c_j. +This span has dimension at most h, because the latter vectors are spanned +by c_i+c_1 for 2 <= i <= h. The r target coefficients are independent, so +h >= r. + +A bipartite component with v vertices has at most f(v)=floor(v^2/4) edges. +Put g(t)=f(t+1) for integers t >= 0. Then g(0)=0, and the successive +increments of g are 1,1,2,2,3,3,... . They are nondecreasing, so +g(a)+g(b) <= g(a+b) for a,b >= 0. Consequently, for component sizes v_i, + + |H| <= sum_i g(v_i-1) + <= g(n-h) + <= g(n-r) = floor(s^2/4). (3) + +At most r+floor(s^2/4) edges can remain. Subtracting from E proves the +lower bound in (1). This is the source's nonzero-constant bound applied +to a target set that forces b != 0, rather than a new lower-bound method. + +## Choosing a balanced root set despite the missing matching + +Choose one root from each component of T. We need a choice R of s roots +and a partition R=A disjoint-union B with + + |A|=floor(s/2), |B|=ceil(s/2), + +such that no removed matching edge has one endpoint in each part. + +For any root set, group its complete matched pairs into atoms of size two, +and its unmatched root vertices into atoms of size one. Keeping each atom +in one part prevents every forbidden crossing. + +If there is at least one singleton atom, every integer size from zero to s +is a sum of atom sizes. Indeed, if there are a double atoms and b >= 1 +singletons, the intervals [2j,2j+b], for 0 <= j <= a, cover all integers +from zero to 2a+b. Thus the balanced partition exists. If every atom has +size two and s is divisible by four, it also exists. + +The only remaining case is a root set made entirely of complete matched +pairs, with s congruent to 2 modulo 4. There is a nontrivial target +component, since T contains an odd cycle. Replace its chosen root v by +another vertex w in that component. Initially R is a union of complete +matched pairs. Since w was not a root, neither was its mate. Since v was +a root, its mate was a root in another component. After the replacement, +w and the mate of v are singleton atoms. The preceding argument applies. +The replacement preserves one root per target component. + +This proves the required root-selection statement for all s >= 1. When +s=1, A is empty and B consists of the sole root. + +## Attaining the bound with literal decoder coefficients + +Take R,A,B as above, and let H contain every edge between A and B. All +these edges exist in G. They are nontarget edges because distinct roots +belong to distinct target components. Therefore + + |H|=|A||B|=floor(s^2/4), F=T disjoint-union H. + +Here is a direct construction of the unit decoders, including their empty +star coefficients. Define b by (2). Set a_v=b at every root in A and +a_v=0 at every root in B. Remove one edge t_0 of the target cycle, leaving +a spanning tree in each target component. Traverse those trees outward +from the selected roots. For a tree edge t=uv, with u already assigned, set + + a_v = a_u + b + e_t. (4) + +All retained tree edges now have their desired coefficient. Along the +path replacing t_0 there are an even number of edges, because the removed +cycle is odd. Summing (4) along that path gives + + a_u + a_v + b = sum_{t on cycle, t != t_0} e_t + b + = e_(t_0). + +So the omitted cycle edge also has its unit coefficient. At any edge of +H, one root has label b and the other zero, giving coefficient b+0+b=0. +Each coordinate of this vector identity is an actual decoder for one +prescribed target using the allowed observations on F. Every retained +nontarget input has coefficient zero, without an input restriction. + +Exactly r+floor(s^2/4) edges remain. Together with (3), this proves (1). + +## A first case beyond the source's triangle formula + +At p=3 let T be the five-cycle 0,2,1,4,3,0, with vertex 5 isolated. All +five target edges are allowed. Here r=5, s=2 and E=12. Take roots 0 and 5, +so H consists of the single edge 05. The construction retains six edges +and deletes six. Bound (3) proves that fewer than six deletions cannot +suffice. No triangle is present in this target graph. + +For a triangle with all other vertices isolated, r=3 gives +delta_+=p^2-4, recovering the source's already proved result with credit. +The added scope includes longer odd cycles and arbitrary tree additions. + +## Scope + +This is a uniform algebraic proof with finite corroboration. The code +constructs coefficients; it does not implement the observations as paid +native operations. Physical frames, helper acquisition, dirty restoration, +tape movement, precision, recursive prices and the complete multiplication +theorem remain separate obligations. No new kappa is claimed. + +New proof and checker are Apache-2.0. The source credits the graph-incidence +bridge to Martinez-Bernal, Valencia-Bucio and Villarreal, and retains Joel +Pulikkan / GamingPuzzled, icekylinx and eumemic's paired-cube lineage. diff --git a/research/odd-unicyclic-star-budgets/README.md b/research/odd-unicyclic-star-budgets/README.md new file mode 100644 index 0000000000..125ed50041 --- /dev/null +++ b/research/odd-unicyclic-star-budgets/README.md @@ -0,0 +1,112 @@ +# Exact star budgets for prescribed targets with one odd cycle + +Scoped uniform proof with finite exact corroboration. In the binary signed +two-port observation model of [Sam Sung's PR #669](https://github.com/CrocSwap/integer-mult-bounds/pull/669), +allow every vertex star and the empty star. If the prescribed target graph +has exactly one cycle in total, and that cycle is odd, its exact deletion +budget is + +```text +delta_+(T) = 2p(p-1) - r - floor((2p-r+1)^2/4), r = |T|. +``` + +Attached trees, other tree components and isolated vertices are allowed. +The theorem holds for every p >= 3. A five-cycle on six vertices needs +exactly six deletions; the source's triangle formula is the r=3 special +case. Within this class, the optimum depends only on p and r. + +The source already supplies the general nonzero-constant lower bound and +the triangle optimum. The new step is a balanced root construction that +attains that bound for the whole odd-unicyclic class, despite the removed +perfect matching. [PROOF.md](PROOF.md) supplies the uniform argument and +literal vector-valued decoder coefficients. Predecessor results are cited, +not audited or replayed as the contribution. + +This is a scalar observation result. It supplies no paid supplier, physical +frame schedule, helper preparation, dirty restoration, precision/tape bill +or new kappa. The selected result and its five framework assumptions remain +unchanged. Independent human and formal proof-kernel review are unclaimed. + +## Evidence + +The independent small-instance oracle enumerates all 4,096 retained graphs +at p=3, computes their observation row spaces, and optimizes every target +set by a superset transform. All 864 eligible target sets agree with the +formula and the constructed coefficients. By target count r=3,4,5,6 there +are respectively 8,72,288,496 sets. The matching obstruction triggers the +root replacement on 128 of these sets. + +The constructor also checks 2,704 fixed fixtures at p=4,...,16, covering +every odd cycle length from 3 through 31, attachments and separate tree +components. These are fixture cases, with repetition allowed, rather than +a census of all larger target graphs. Every one of their 101,231 retained +input columns has its literal required coefficient. + +Controls reject five invalid target inputs, three decoder mutations and +all twelve single-edge restorations of the displayed p=4 triangle witness. +The component-concentration inequality is also checked on 1,600 integer +pairs. These finite checks corroborate the written proof; they do not +replace its all-size quantifiers. The verifier imports no predecessor code. + +## Reproduce + +From the repository root, using CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/odd-unicyclic-star-budgets/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/odd-unicyclic-star-budgets/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/odd-unicyclic-star-budgets +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/odd-unicyclic-star-budgets --check-source-history +``` + +Another CPython 3.12 executable can replace that local interpreter path. +The marker is `PASS_ODD_UNICYCLIC_STAR_BUDGETS`, followed by enumerated +coverage and SHA256 hashes. `--receipt /absolute/new/file.json` writes a +new source-bound receipt outside the package and refuses overwrite. +The default verifier writes nothing. Registered normal and optimized +commands each have a 120-second limit. + +[SOURCES.json](SOURCES.json) pins the exact main-branch predecessor note; +the shared metadata runner authenticates its working bytes and historical +provenance. The direct mathematical checker needs only this package and +does not consume the predecessor's implementation. The original catalogue +card and selected record are retained as historical provenance. The changed +scope from a native-register construction to an algebraic side result is +explicit in [TASK.json](TASK.json). + +## Open next questions + +What is the exact C+ budget for a prescribed forest with r>p? The source +gives a C- matching formula and a uniform no-benefit result for C+ when +p>=6 and r<=p. Start with one p>=6 forest above that range and compare +the matching optimum with the nonzero-constant bipartite bound. A forest +does not force a nonzero empty-star coefficient, so both decoder types +must be considered. This question is left unclaimed. + +## Engineering limits + +All scientific loops have explicit finite domains. Constructor fixtures +validate 2<=p<=20, giving at most forty vertices and 760 edges. The largest +exhaustive arrays have 4,096 entries. The proof has no such p limit. +Functions are below sixty lines; all checks use exceptions and remain +active under optimization. No recursion or subprocess is used. + +Power-of-Ten rule 3 has a managed-runtime deviation: CPython and its standard +library allocate during replay. Live collections are bounded by the above +input limits, receipts contain bounded aggregates, and the shared runner +enforces the timeout. Extending the finite domain requires reassessing +those capacities. Rule 9 has a bounded test-only dispatch deviation: +rejection controls call the local analyze and endpoint functions through +fixed lambdas. The target set of those callbacks is explicit and contains +no external code. Warning-strict normal and optimized execution provide +the available interpreter diagnostics; no external linter is required. + +## Credit + +This contribution was produced by Nick Petalas. Sam Sung / +the-missionary-company retains credit for PR #669's observation model, +graph-target reductions, inherited lower bound and triangle result. +The graph-incidence bridge retains Martinez-Bernal, Valencia-Bucio and +Villarreal's credit. Joel Pulikkan / GamingPuzzled, icekylinx and eumemic +retain the paired-cube lineage. The new attainment proof, constructor and +independent finite oracle are the contribution here. New work is Apache-2.0. diff --git a/research/odd-unicyclic-star-budgets/SOURCES.json b/research/odd-unicyclic-star-budgets/SOURCES.json new file mode 100644 index 0000000000..d36582488a --- /dev/null +++ b/research/odd-unicyclic-star-budgets/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "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/asymmetric-hypercube-decoder/GRAPH-TARGETS.md", + "usage": "input", + "git_blob": "65b566326ebb213ff013b3825ce9f432dfff5bae", + "sha256": "a9f14398ccf6490af546becb4ef744217594650bbb68450665ff47ccc14397f5" + } + ] +} diff --git a/research/odd-unicyclic-star-budgets/TASK.json b/research/odd-unicyclic-star-budgets/TASK.json new file mode 100644 index 0000000000..c93b546d2c --- /dev/null +++ b/research/odd-unicyclic-star-budgets/TASK.json @@ -0,0 +1,76 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_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": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Exact prescribed-target deletion budgets in the binary signed two-port C+ observation code, for every target graph with exactly one odd cycle in total.", + "scope_change_reason": "The native larger-register card is changed to a self-contained algebraic decoder side result. PR669 gives exact forest and triangle budgets but not the attaining construction for general odd-unicyclic targets.", + "bottleneck_link": "A sharp scalar observation threshold constrains which prescribed jobs can share these observations before a physical supplier is priced. This does not change the actual selected E8 or BIT supplier.", + "budget_minutes": 60, + "stop_rule": "Stop after the first uniform exact budget is proved and independently corroborated on every six-vertex retained graph; package it without extending to other target classes.", + "outcome": "completed", + "evidence": "PROOF.md, exact exhaustive p=3 oracle, literal larger-fixture decoder columns and rejection controls in verify.py.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the exact C+ deletion budget for a prescribed target forest with r>p?", + "why_it_matters": "PR669 supplies a general partition optimization and a C- matching formula, while its uniform no-benefit result for C+ covers r<=p at p>=6.", + "first_step": "Compare the nonzero-constant bipartite bound against the C- matching optimum for one p>=6 forest with r>p.", + "blocked_by": "A forest does not force the empty-star coefficient to be nonzero, so both decoder types must be optimized." + } + ], + "predecessor_credit": { + "source": "PR #669, Sam Sung / the-missionary-company", + "new_step": "Uniform attainment of the inherited nonzero-constant bound for every odd-unicyclic prescribed target set." + }, + "orientation": "research_selected_baseline.py passed source bindings for selected PR6030, kappa 781451/250000000; no scientific replay.", + "environment": { + "python": "3.12.15", + "implementation": "CPython", + "system": "Darwin", + "machine": "arm64", + "dependencies": "standard library only" + } +} diff --git a/research/odd-unicyclic-star-budgets/VERIFY.json b/research/odd-unicyclic-star-budgets/VERIFY.json new file mode 100644 index 0000000000..e2f24d2682 --- /dev/null +++ b/research/odd-unicyclic-star-budgets/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/asymmetric-hypercube-decoder/GRAPH-TARGETS.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Every p=3 retained graph and eligible prescribed target set, larger literal decoder columns, matching-root adjustment and semantic rejection controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same scientific checks with optimization enabled; all acceptance checks use explicit exceptions." + } + ] +} diff --git a/research/odd-unicyclic-star-budgets/verify.py b/research/odd-unicyclic-star-budgets/verify.py new file mode 100644 index 0000000000..a60c4c323e --- /dev/null +++ b/research/odd-unicyclic-star-budgets/verify.py @@ -0,0 +1,296 @@ +"""Exact constructive and exhaustive checks for PROOF.md; standard library only.""" + +import argparse +import hashlib +import json +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def graph(p): + require(type(p) is int and 2 <= p <= 20, "fixture p outside [2,20]") + return tuple((u, v) for u in range(2 * p) for v in range(u + 1, 2 * p) + if u // 2 != v // 2) + + +def components(n, edges): + adjacency = [[] for _ in range(n)] + for u, v in edges: + adjacency[u].append(v) + adjacency[v].append(u) + seen = set() + result = [] + for root in range(n): + if root in seen: + continue + queue = [root] + seen.add(root) + for head in range(n): + if head == len(queue): + break + for v in adjacency[queue[head]]: + if v not in seen: + seen.add(v) + queue.append(v) + result.append(tuple(sorted(queue))) + require(sum(map(len, result)) == n, "component partition") + return tuple(result), adjacency + + +def analyze(p, targets): + available = set(graph(p)) + require(len(targets) == len(set(targets)), "duplicate target") + require(all(e in available for e in targets), "invalid target edge") + comps, adjacency = components(2 * p, targets) + require(len(targets) - 2 * p + len(comps) == 1, "not one cycle in total") + core = set(range(2 * p)) + for _ in range(2 * p): + leaves = {v for v in core if sum(w in core for w in adjacency[v]) <= 1} + if not leaves: + break + core.difference_update(leaves) + cycle = tuple(i for i, (u, v) in enumerate(targets) if u in core and v in core) + require(len(cycle) >= 3 and len(cycle) % 2 == 1, "cycle is not odd") + require(len(core) == len(cycle), "cycle core mismatch") + return comps, cycle + + +def root_colors(comps): + roots = [c[0] for c in comps] + root_set = set(roots) + adjusted = False + if len(roots) % 4 == 2 and all((v ^ 1) in root_set for v in roots): + index = next(i for i, c in enumerate(comps) if len(c) > 1) + roots[index] = comps[index][1] + root_set = set(roots) + adjusted = True + pairs = tuple((v, v ^ 1) for v in sorted(root_set) + if v % 2 == 0 and (v ^ 1) in root_set) + singles = tuple(v for v in sorted(root_set) if (v ^ 1) not in root_set) + half = len(roots) // 2 + choices = [j for j in range(len(singles) + 1) + if 0 <= half - j <= 2 * len(pairs) and (half - j) % 2 == 0] + require(bool(choices), "balanced root coloring absent") + j = choices[0] + left = set(singles[:j]) + for pair in pairs[:(half - j) // 2]: + left.update(pair) + require(len(left) == half, "unbalanced root coloring") + require(all((u in left) == (v in left) for u, v in pairs), "split missing edge") + return tuple(roots), frozenset(left), adjusted + + +def construct(p, targets): + """Return actual vector-valued star coefficients and the retained graph.""" + comps, cycle = analyze(p, targets) + roots, left, adjusted = root_colors(comps) + constant = sum(1 << i for i in cycle) + labels = [None] * (2 * p) + adjacency = [[] for _ in labels] + for i, (u, v) in enumerate(targets): + if i != cycle[0]: + adjacency[u].append((v, i)) + adjacency[v].append((u, i)) + queue = list(roots) + for root in roots: + labels[root] = constant if root in left else 0 + for head in range(2 * p): + if head == len(queue): + break + u = queue[head] + for v, i in adjacency[u]: + if labels[v] is None: + labels[v] = labels[u] ^ constant ^ (1 << i) + queue.append(v) + require(all(a is not None for a in labels), "unreached target vertex") + zero_edges = frozenset((min(u, v), max(u, v)) for u in left + for v in roots if v not in left) + retained = frozenset(targets) | zero_edges + s = 2 * p - len(targets) + 1 + require(len(zero_edges) == s * s // 4, "wrong zero-edge count") + require(zero_edges <= set(graph(p)), "unavailable root edge") + return tuple(labels), constant, retained, adjusted + + +def endpoint(p, targets, labels, constant, retained): + """Check every retained input column against the literal unit decoders.""" + require(len(labels) == 2 * p, "wrong coefficient count") + require(retained <= set(graph(p)), "invalid retained edge") + require(set(targets) <= retained, "target deleted") + units = {e: 1 << i for i, e in enumerate(targets)} + for u, v in retained: + require(labels[u] ^ labels[v] ^ constant == units.get((u, v), 0), + "wrong retained input column") + return True + + +def binary_basis(rows, width): + basis = [0] * width + for row in rows: + value = row + for bit in range(width - 1, -1, -1): + if value & (1 << bit): + if basis[bit]: + value ^= basis[bit] + else: + basis[bit] = value + break + return basis + + +def in_span(value, basis): + for bit in range(len(basis) - 1, -1, -1): + if value & (1 << bit): + value ^= basis[bit] + return value == 0 + + +def all_retained_oracle(): + """Enumerate every p=3 retained graph, then optimize every target set.""" + edges = graph(3) + width = len(edges) + rows = [sum(1 << i for i, e in enumerate(edges) if v in e) for v in range(6)] + rows.append((1 << width) - 1) + best = [-1] * (1 << width) + for mask in range(1 << width): + basis = binary_basis((row & mask for row in rows), width) + decodable = sum(1 << i for i in range(width) + if mask & (1 << i) and in_span(1 << i, basis)) + best[decodable] = max(best[decodable], mask.bit_count()) + for i in range(width): + for mask in range(1 << width): + if not mask & (1 << i): + best[mask] = max(best[mask], best[mask | (1 << i)]) + return edges, best + + +def exhaustive_check(): + edges, best = all_retained_oracle() + cases = adjusted = 0 + by_r = {} + digest = hashlib.sha256() + for mask in range(1 << len(edges)): + targets = tuple(e for i, e in enumerate(edges) if mask & (1 << i)) + try: + analyze(3, targets) + except ValueError: + continue + labels, constant, retained, changed = construct(3, targets) + endpoint(3, targets, labels, constant, retained) + expected = len(targets) + (7 - len(targets)) ** 2 // 4 + require(best[mask] == expected == len(retained), "exhaustive optimum differs") + cases += 1 + adjusted += changed + by_r[len(targets)] = by_r.get(len(targets), 0) + 1 + digest.update(f"{mask}:{best[mask]}:{labels}:{constant}\n".encode()) + require(cases > 0 and adjusted > 0, "exhaustive coverage absent") + return {"retained_graphs": len(best), "target_sets": cases, + "targets_by_r": by_r, "root_adjustments": adjusted, + "sha256": digest.hexdigest()} + + +def cycle_fixture(p, length, attached, mode): + vertices = tuple(range(0, 2 * p, 2)) + tuple(range(1, 2 * p, 2)) + cycle = list(vertices[:length]) + if cycle[-1] // 2 == cycle[0] // 2: + cycle[-1], cycle[-2] = cycle[-2], cycle[-1] + edges = {(min(u, v), max(u, v)) + for u, v in zip(cycle, cycle[1:] + cycle[:1])} + rest = vertices[length:] + active = list(cycle) + for v in rest[:attached]: + parent = next(u for u in reversed(active) if u // 2 != v // 2) + edges.add((min(parent, v), max(parent, v))) + active.append(v) + if mode: + remaining = rest[attached:] + for u, v in zip(remaining[::2], remaining[1::2]): + if u // 2 != v // 2: + edges.add((min(u, v), max(u, v))) + return tuple(sorted(edges)) + + +def fixture_check(): + cases = columns = adjusted = 0 + cycle_lengths = set() + digest = hashlib.sha256() + for p in range(4, 17): + for length in range(3, 2 * p, 2): + for attached in range(2 * p - length + 1): + for mode in (0, 1): + targets = cycle_fixture(p, length, attached, mode) + labels, constant, retained, changed = construct(p, targets) + endpoint(p, targets, labels, constant, retained) + s = 2 * p - len(targets) + 1 + require(len(retained) == len(targets) + s * s // 4, "fixture size") + cases += 1 + columns += len(retained) + adjusted += changed + cycle_lengths.add(length) + digest.update(f"{p}:{targets}:{labels}:{constant}\n".encode()) + return {"cases": cases, "retained_columns": columns, + "cycle_lengths": sorted(cycle_lengths), "root_adjustments": adjusted, + "sha256": digest.hexdigest()} + + +def expect_rejection(operation): + try: + operation() + except ValueError: + return + raise ValueError("control unexpectedly accepted") + + +def controls(): + triangle = ((0, 2), (0, 4), (2, 4)) + invalid = [(), ((0, 1),), triangle + (triangle[0],), + ((0, 2), (0, 3), (1, 2), (1, 3)), + triangle + ((1, 3), (1, 5), (3, 5))] + for targets in invalid: + expect_rejection(lambda: analyze(3, targets)) + labels, constant, retained, _ = construct(4, triangle) + expect_rejection(lambda: endpoint(4, triangle, labels, 0, retained)) + bad_labels = list(labels) + bad_labels[0] ^= 1 + expect_rejection(lambda: endpoint(4, triangle, bad_labels, constant, retained)) + expect_rejection(lambda: endpoint(4, triangle, labels, constant, + retained - {triangle[0]})) + deleted = set(graph(4)) - retained + require(bool(deleted), "no deletion-restoration control") + for edge in sorted(deleted): + expect_rejection(lambda: endpoint(4, triangle, labels, constant, retained | {edge})) + for a in range(1, 41): + for b in range(1, 41): + require(a * a // 4 + b * b // 4 <= (a + b - 1) ** 2 // 4, + "component concentration inequality") + require(12 - 3 - 4 == 5 and 24 - 3 - 9 == 12, "triangle specialization") + return {"invalid_inputs": len(invalid), "decoder_mutants": 3, + "restored_deleted_edges": len(deleted), "concentration_pairs": 1600} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path, help="write a new source-bound JSON receipt") + args = parser.parse_args() + result = {"claim_type": "scoped proof with finite corroboration", + "exhaustive_p3": exhaustive_check(), "constructive": fixture_check(), + "controls": controls()} + package = Path(__file__).resolve().parent + result["source_sha256"] = { + name: hashlib.sha256((package / name).read_bytes()).hexdigest() + for name in ("verify.py", "PROOF.md", "README.md", "TASK.json", "SOURCES.json", "VERIFY.json")} + encoded = json.dumps(result, sort_keys=True, indent=2) + "\n" + if args.receipt: + require(args.receipt.resolve().parent != package, "receipt must be outside package") + with args.receipt.open("x", encoding="utf-8") as output: + require(output.write(encoded) == len(encoded), "incomplete receipt write") + print("PASS_ODD_UNICYCLIC_STAR_BUDGETS") + print(encoded, end="") + + +if __name__ == "__main__": + main()