diff --git a/research/b2-tripartite-edge-counterexample/README.md b/research/b2-tripartite-edge-counterexample/README.md new file mode 100644 index 0000000000..e124dc0598 --- /dev/null +++ b/research/b2-tripartite-edge-counterexample/README.md @@ -0,0 +1,164 @@ +# Nine lines refute the B2 acyclic-edge strengthening + +An admissible three-total configuration has + +```text +v = 9, H = empty, |F| = 9, +cost(B) = 21 < masE(W[F]) = 27. +``` + +This settles **open next question 1** of Aaron Wang's +[CR2/B2 audit #2293](https://github.com/CrocSwap/integer-mult-bounds/pull/2293). +The valid vertex version of DreamingOfClouds's +[Theorem B2, section 2.2](https://github.com/CrocSwap/integer-mult-bounds/blob/113a718265c62aec301c5695f4bfb9c421bef7ab/research/char2-jets/README.md) +uses the **number of vertices in a largest induced acyclic subgraph**, not +the number of edges in a largest acyclic edge subset. For this witness the +two numbers are 3 and 27. The full wild pattern equals B's off-diagonal +support, so restricting wild edges to the chosen pairing does not repair +the edge version. The selected frontier is unchanged. + +## Inspect or replay + +[WITNESS.json](WITNESS.json) contains all nine integer vector pairs and +the complete binary pairing. From the repository root: + +```sh +python3 -B research/b2-tripartite-edge-counterexample/verify.py +python3.12 scripts/research_package.py --package research/b2-tripartite-edge-counterexample +``` + +Expected status: `PASS_B2_TRIPARTITE_EDGE_COUNTEREXAMPLE`. The registered +replay runs normal and optimized Python; its acceptance predicates remain +active under `-O`. Only the standard library is needed. + +## Construction in the stated model + +PR #2162 uses indexed rational vectors p(t), q(t) in Q^3 with nonzero +diagonal dot products. A binary B is admissible when its diagonal is one +and every off-diagonal one occurs at a zero rational dot product. For +coordinate supports R_j and A_j, + +```text +cost(B) = sum_(j=1)^3 rank_F2 B[R_j, A_j]. +``` + +H consists of harmonic lines with two equal diagonal contributions; F +contains indices where both vectors have full support. A wild incidence +is a zero off-diagonal dot product using all three coordinates. Configurations +are indexed lists; the stated model does not require distinct points or lines. + +Take k copies of each pair, indexed by (i,a), with i in {1,2,3}, 1<=a<=k: + +| i | p_i | q_i | +|---|---|---| +| 1 | (1,1,1) | (6,-5,1) | +| 2 | (1,2,4) | (3,-4,1) | +| 3 | (1,3,9) | (2,-3,1) | + +The cross-dot matrix is diag(2,-1,2): evaluate (x-2)(x-3), (x-1)(x-3) +and (x-1)(x-2) at x=1,2,3. Precisely the cross-type pairs are incidences. +All vectors have full support, so H is empty and |F|=v=3k. +With I_k the identity and J_k the all-ones matrix, choose + +```text + [ I_k J_k J_k ] +B_k = [ J_k I_k J_k ]. + [ J_k J_k I_k ] +``` + +Its off-diagonal ones are exactly the cross-type incidences, so B_k is +admissible. Each of its three coordinate-support blocks is the whole B_k. + +## Rank and acyclic counts: proof for every k + +Write x in three length-k blocks x_i, and let s_i be the coordinate sum +of x_i in F2. The equation B_k x=0 says + +```text +x_1 = (s_2+s_3) 1_k, +x_2 = (s_1+s_3) 1_k, +x_3 = (s_1+s_2) 1_k. +``` + +For even k, summing each block gives s_i=0, hence x=0. For odd k, the +equations are equivalent to x_i=s_i 1_k and s_1+s_2+s_3=0. Every such +triple is a kernel vector, giving nullity two. Therefore + +```text +rank_F2(B_k) = 3k for even k, + 3k - 2 for odd k; +cost(B_k) = 3 rank_F2(B_k). +``` + +The wild graph is complete bidirected tripartite with three parts of size k. +An acyclic edge set retains at most one direction of each cross-part pair, +or it would contain a 2-cycle. There are 3k^2 such pairs; ordering the parts +and keeping every forward edge attains that bound. Thus masE=3k^2. +An induced acyclic vertex set lies in one part, since any cross-part pair +forms a 2-cycle; thus masV=k. + +Since v-|H|-|F|=0, the proposed edge bound exceeds the actual cost by + +```text +masE - cost(B_k) = 3k(k-3) for even k, + 3(k-1)(k-2) for odd k. +``` + +This is positive for every k>=3. At k=3, rank=7, cost=21, masE=27, +masV=3 and there are 54 directed wild edges. At k=1 the edge inequality +is tight (3=3); k=2 does not violate it (18>12). Thus k=3 is the first +counterexample **in this equal-multiplicity family**. + +Repeating the three rational types makes the edge count quadratic but +the rank cost only linear. The proven vertex bound respects repetition. +Neither the vertex theorem nor target (A), cost(B)>=v, is contradicted. + +## Independent checks and limits + +The verifier imports no predecessor implementation. It checks every rational +dot product, admissibility and actual coordinate support. It derives each +block rank twice: by pivot elimination and by enumerating its entire F2 row +space. It computes masE by exact subset dynamic programming over all vertex +orders and masV by induced-subgraph cycle tests. Both graph searches cover +512 subsets at v=9 without assuming tripartite structure. + +Controls reject a zero B diagonal, a within-type nonincidence, a perturbed +rational point and a zero rational diagonal. A directed 2-cycle and dependent +binary rows check the graph/rank primitives. Two simultaneous reindexings +preserve all results; k=1,2 are tight/nonviolating controls. Elimination also +checks the proved rank formula for k=1,...,16; the all-k conclusion rests on +the proof above, not on those finite checks. + +This evaluates an explicit B, not its globally minimum cost. No globally +smallest-v claim, physical supplier construction or new kappa follows. +Local normal/optimized replay evidence and environment are recorded in +[TASK.json](TASK.json); maintainer review and hosted CI are separate. + +## Coordination and credit + +Canonical investigation: [Discussion #2331](https://github.com/CrocSwap/integer-mult-bounds/discussions/2331). +Base main: `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`, priority revision 4. +TASK.json records the changed scope from `uniform-transfer-audit` to the +named decoder-bound handoff. [SOURCES.json](SOURCES.json) pins the model and +audit references; the self-contained verifier has no external data inputs. + +Aaron Wang's [contemporaneous smaller-core search](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18941591) +received this complementary analytic family in +[a coordination reply](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18941680). +The separate split-minmax audit is outside this package. + +The model and B2 are DreamingOfClouds's (#2162, following #2111/#1590). +Aaron Wang, assisted by opencode, identified the edge/vertex distinction and +posed this question in #2293. This counterexample, family proof and verifier +were prepared by ROTl24 with substantial OpenAI Codex assistance. +Checked by the contributing agent; independent human and proof-assistant review remain open. +New work is Apache-2.0. + +## Open next questions + +The named edge-form question is settled. The downstream correction is to +define MAS explicitly as a maximum **induced acyclic vertex-set cardinality** +when using B2(iii). No further search is required for that correction. +The general three-total target (A) remains open; a smaller counterexample +or a restriction forbidding repeated vectors is not needed to decide this +stated model. This package therefore proposes no additional search. diff --git a/research/b2-tripartite-edge-counterexample/SOURCES.json b/research/b2-tripartite-edge-counterexample/SOURCES.json new file mode 100644 index 0000000000..42597aa2c6 --- /dev/null +++ b/research/b2-tripartite-edge-counterexample/SOURCES.json @@ -0,0 +1,39 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + } + ], + "references": [ + { + "pr": 2162, + "author": "DreamingOfClouds", + "commit": "113a718265c62aec301c5695f4bfb9c421bef7ab", + "path": "research/char2-jets/README.md", + "git_blob": "1f4ae89f74c1318d95e25e8e1f56bd66405f0b48", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/113a718265c62aec301c5695f4bfb9c421bef7ab/research/char2-jets/README.md", + "use": "Model section 1 and Theorem B2 section 2.2. Mathematical reference only; no predecessor code is imported." + }, + { + "pr": 2293, + "author": "Aaron Wang (navinor), assisted by opencode", + "commit": "6bc48613ed1c71e5d2e88994235e9e8629129b9c", + "path": "research/cr2-b2-audit-seed4f435ab7/README.md", + "git_blob": "266ec5872511a3fc71bdc0a2e3b4db590cc494f6", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/6bc48613ed1c71e5d2e88994235e9e8629129b9c/research/cr2-b2-audit-seed4f435ab7/README.md", + "use": "Result 4 distinguishes masE from masV; Open next questions item 1 requests the edge-form decision. Mathematical reference only." + } + ], + "reference_scope": "Exact source references were read at the listed commits. The generic runner validates files provenance; references are citations, not runtime inputs. The new proof and verifier restate their model and use only WITNESS.json." +} diff --git a/research/b2-tripartite-edge-counterexample/TASK.json b/research/b2-tripartite-edge-counterexample/TASK.json new file mode 100644 index 0000000000..ada79e7edc --- /dev/null +++ b/research/b2-tripartite-edge-counterexample/TASK.json @@ -0,0 +1,150 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one exact all-size/compiler, precision, hosting or restoration implication be proved or falsified?", + "starting_points": [ + "certificates/selected-result.json", + "docs/audit.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the selected review scope and choose one exact all-size or precision implication.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write its quantified inputs and conclusion; find a missing hypothesis or construct a minimal exact adversarial instance.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "Choose one tape, precision, hosting or restoration lemma." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision" + ] + }, + "scope_status": "changed", + "actual_scope": "Refute the acyclic-edge-count strengthening of Theorem B2(iii), using a nine-line admissible rational three-total configuration and an all-k repeated-three-type proof.", + "scope_change_reason": "The catalogue drew an all-size uniform-transfer audit. After orienting on the pending outer-transfer handoff, the live #2293 audit supplied a more decisive named question: whether the edge reading of MAS holds. This changes the audited object to a decoder lower bound; it does not purport to discharge a selected transfer obligation. The independently derived v=9 blow-up family complements the live v<=8 search rather than rerunning it.", + "bottleneck_link": "The three-total decoder pairing-cost problem is a structural route beyond packing. Resolving a false strengthening prevents an unsupported obstruction from being used to reject decoder candidates. This is an algebraic audit, not a new physical supplier.", + "budget_minutes": 60, + "stop_rule": "Stop after one exact admissible counterexample, its analytic family proof, independent rank/acyclicity checks and a public handoff. No exhaustive pairing search or global-minimality claim.", + "outcome": "negative-result", + "evidence": "WITNESS.json and verify.py independently derive ranks [7,7,7], cost 21, 54 wild edges, masE 27 and masV 3. README.md proves the family for every positive k. Four malformed fixtures reject; graph/rank controls, two reindexings and k=1,2 positive controls pass. Rank formula checked for k=1..16.", + "author": "ROTl24", + "ai_assistance": "Substantial OpenAI Codex assistance in research, proof development, implementation, verification and writing; checked by the contributing agent, with no independent human or proof-assistant review claimed.", + "open_questions": [], + "no_open_questions_reason": "The named edge-form question is settled. Defining MAS as an induced acyclic vertex-set cardinality is the immediate correction; no further search is needed to use this result. The general three-total target (A) remains outside this package.", + "selection": { + "nonce": "7f2fe94ff4c0c5cf3c947e11d7a05396", + "track": "adversarial-audit", + "drawn_task": "uniform-transfer-audit", + "drawn_scope_key": "603f341b99f590f17a76", + "actual_scope_key": "b2-mas-edge-tripartite-equal-multiplicity" + }, + "coordination": { + "canonical_discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2331", + "status": "FINDING; no retrospective advance reservation", + "related_live_claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18941591", + "finding_delivered_to_claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18941680", + "predecessors": [ + 2162, + 2293 + ], + "overlap_entry": { + "open_prs": { + "records": 540, + "fetched_at": "2026-10-15T05:27:06Z", + "complete_pagination": true + }, + "discussions": { + "records": 1039, + "fetched_at": "2026-10-15T05:31:22Z", + "complete_pagination": true + }, + "local_records": 1538, + "additional_live_check": "The active edge-form claim was read directly after the cached full snapshot.", + "limits": "PR titles/bodies, Discussion text, top-level local README/TASK metadata and ledger; no arbitrary code-diff coverage." + }, + "overlap_before_submission": { + "searched_at_utc": "2026-10-15T05:47:14.987231+00:00", + "terms": [ + "masE", + "edge-form", + "tripartite" + ], + "coverage": { + "open_prs": { + "fetched_at": "2026-10-15T05:43:02.542803+00:00", + "complete_pagination": true, + "records": 546 + }, + "discussions": { + "fetched_at": "2026-10-15T05:47:14.858580+00:00", + "complete_pagination": true, + "records": 1051 + } + }, + "local_records": 1538, + "warnings": [], + "limits": "Remote PR scope is open PRs including drafts. Closed work is searched through local READMEs, TASK metadata and ledger only. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission.", + "assessment": "Nearest predecessor remains #2293; the live smaller-core claimant has received the analytic witness. No acknowledgment was present at the direct pre-submission check. The added value is the v=9 counterexample and all-k family, not a repeat of the smaller-core search." + } + }, + "upstream_checkpoint": { + "canonical_remote": "https://github.com/CrocSwap/integer-mult-bounds.git", + "main_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "priority_revision": 4, + "decision": "Canonical main, priorities and selected record are unchanged; continue the isolated package without rebasing or repinning.", + "predecessor_heads_unchanged": [ + 2162, + 2293 + ], + "recorded_at_utc": "2026-10-15T05:48:56+00:00", + "predecessor_check": "Direct GitHub query before final packaging returned both pinned heads unchanged and both PRs open." + }, + "validation": { + "environment": "Windows x86-64; CPython 3.12.13 for package checks; standard library only. Baseline orientation used CPython 3.13.15.", + "commands": [ + { + "command": "python -B scripts/research_baseline.py", + "result": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY; source-bound orientation, not a complete cold replay" + }, + { + "command": "{python3.12.13} -B research/b2-tripartite-edge-counterexample/verify.py", + "result": "PASS_B2_TRIPARTITE_EDGE_COUNTEREXAMPLE" + }, + { + "command": "{python3.12.13} -B scripts/research_package.py --package research/b2-tripartite-edge-counterexample --check-only", + "result": "PASS_PACKAGE_METADATA_AND_PINS" + }, + { + "command": "{python3.12.13} -B scripts/research_package.py --package research/b2-tripartite-edge-counterexample", + "result": "PASS_REGISTERED_RESEARCH_PACKAGE; both normal and -O VERIFY.json commands passed" + } + ], + "command_notation": "{python3.12.13} denotes the CPython 3.12.13 executable; VERIFY.json uses the runner-selected interpreter.", + "not_run": [ + "Independent human review", + "Proof-assistant formalization", + "Full selected-frontier cold replay (no selected artifacts changed)" + ], + "hosted_ci": "Not run at the local evidence checkpoint; consult the eventual PR checks for current status." + } +} diff --git a/research/b2-tripartite-edge-counterexample/VERIFY.json b/research/b2-tripartite-edge-counterexample/VERIFY.json new file mode 100644 index 0000000000..044eff5272 --- /dev/null +++ b/research/b2-tripartite-edge-counterexample/VERIFY.json @@ -0,0 +1,28 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exact admissibility, independent F2 rank engines, acyclic-edge DP, induced-vertex census, malformed controls and family rank checks." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "The same witness and all failure controls with Python assertions disabled; explicit require predicates retain coverage." + } + ] +} diff --git a/research/b2-tripartite-edge-counterexample/WITNESS.json b/research/b2-tripartite-edge-counterexample/WITNESS.json new file mode 100644 index 0000000000..46553ba6b0 --- /dev/null +++ b/research/b2-tripartite-edge-counterexample/WITNESS.json @@ -0,0 +1,36 @@ +{ + "p": [ + [1, 1, 1], [1, 1, 1], [1, 1, 1], + [1, 2, 4], [1, 2, 4], [1, 2, 4], + [1, 3, 9], [1, 3, 9], [1, 3, 9] + ], + "q": [ + [6, -5, 1], [6, -5, 1], [6, -5, 1], + [3, -4, 1], [3, -4, 1], [3, -4, 1], + [2, -3, 1], [2, -3, 1], [2, -3, 1] + ], + "B": [ + [1,0,0,1,1,1,1,1,1], + [0,1,0,1,1,1,1,1,1], + [0,0,1,1,1,1,1,1,1], + [1,1,1,1,0,0,1,1,1], + [1,1,1,0,1,0,1,1,1], + [1,1,1,0,0,1,1,1,1], + [1,1,1,1,1,1,1,0,0], + [1,1,1,1,1,1,0,1,0], + [1,1,1,1,1,1,0,0,1] + ], + "expected": { + "v": 9, + "harmonic_lines": 0, + "full_support_lines": 9, + "wild_edges": 54, + "block_ranks": [7, 7, 7], + "cost": 21, + "mas_edges": 27, + "mas_vertices": 3, + "edge_bound": 27, + "vertex_bound": 3, + "edge_gap": 6 + } +} diff --git a/research/b2-tripartite-edge-counterexample/verify.py b/research/b2-tripartite-edge-counterexample/verify.py new file mode 100644 index 0000000000..ada1bdaaae --- /dev/null +++ b/research/b2-tripartite-edge-counterexample/verify.py @@ -0,0 +1,218 @@ +#!/usr/bin/env python3 +"""Exact independent check of the B2 edge-count counterexample. + +ROTl24, with substantial OpenAI Codex assistance. Apache-2.0. +Standard library only; no predecessor implementation is imported. +""" + +from copy import deepcopy +import json +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def rank_binary(rows): + """Eliminate binary row bitsets without using the block formula.""" + pivots = {} + for row in rows: + while row: + pivot = row.bit_length() - 1 + if pivot not in pivots: + pivots[pivot] = row + break + row ^= pivots[pivot] + return len(pivots) + + +def rank_by_span(rows): + """Independent small-matrix oracle: enumerate the complete row space.""" + span = {0} + for row in rows: + span |= {value ^ row for value in span} + return len(span).bit_length() - 1 + + +def row_bits(matrix): + return [sum(value << j for j, value in enumerate(row)) for row in matrix] + + +def acyclic(vertices, edges): + remaining = set(vertices) + while remaining: + sources = {v for v in remaining + if not any(u in remaining and w == v for u, w in edges)} + if not sources: + return False + remaining -= sources + return True + + +def acyclic_extrema(n, edges): + """Exact edge optimum over all topological orders, and vertex optimum. + + An acyclic edge set has a topological order. For any order all forward + edges can be retained, so maximizing forward edges is exactly masE. + """ + incoming = [0] * n + for u, v in edges: + incoming[v] |= 1 << u + dp = [0] * (1 << n) + last = [0] * (1 << n) + vertex_max = 0 + for mask in range(1, 1 << n): + vertices = [v for v in range(n) if mask >> v & 1] + choices = [(dp[mask ^ (1 << v)] + + (incoming[v] & (mask ^ (1 << v))).bit_count(), v) + for v in vertices] + dp[mask], last[mask] = max(choices) + if len(vertices) > vertex_max and acyclic(vertices, edges): + vertex_max = len(vertices) + order = [] + mask = (1 << n) - 1 + while mask: + v = last[mask] + order.append(v) + mask ^= 1 << v + order.reverse() + positions = {v: i for i, v in enumerate(order)} + forward = {(u, v) for u, v in edges if positions[u] < positions[v]} + require(acyclic(range(n), forward), "edge certificate contains a cycle") + require(len(forward) == dp[-1], "edge certificate size disagrees with DP") + return dp[-1], vertex_max + + +def model(p, q, matrix): + n = len(p) + require(n > 0 and len(q) == len(matrix) == n, "inconsistent dimensions") + require(all(len(row) == 3 and all(type(x) is int for x in row) + for row in p + q), "fixture must have integer triples") + require(all(len(row) == n and all(type(x) is int and x in (0, 1) + for x in row) for row in matrix), + "pairing must be a square binary matrix") + dots = [[sum(a * b for a, b in zip(pt, qs)) for qs in q] for pt in p] + require(all(dots[t][t] != 0 for t in range(n)), "zero rational diagonal") + require(all(matrix[t][t] == 1 for t in range(n)), "pairing diagonal is not one") + require(all(t == s or matrix[t][s] == 0 or dots[t][s] == 0 + for t in range(n) for s in range(n)), + "pairing uses a nonincidence") + ps = [{j for j in range(3) if row[j] != 0} for row in p] + qs = [{j for j in range(3) if row[j] != 0} for row in q] + harmonic = [] + for t in range(n): + terms = [p[t][j] * q[t][j] for j in sorted(ps[t] & qs[t])] + if len(terms) == 2 and terms[0] == terms[1]: + harmonic.append(t) + full = [t for t in range(n) if len(ps[t]) == len(qs[t]) == 3] + wild = {(t, s) for t in range(n) for s in range(n) + if t != s and dots[t][s] == 0 and len(ps[t] & qs[s]) == 3} + supported = {(t, s) for t in range(n) for s in range(n) + if t != s and matrix[t][s] == 1} + ranks = [] + for j in range(3): + columns = [s for s in range(n) if j in qs[s]] + block = [[matrix[t][s] for s in columns] + for t in range(n) if j in ps[t]] + bits = row_bits(block) + rank = rank_binary(bits) + require(rank == rank_by_span(bits), "independent rank oracles disagree") + ranks.append(rank) + return harmonic, full, wild, supported, ranks + + +def audit(p, q, matrix): + harmonic, full, wild, supported, ranks = model(p, q, matrix) + n = len(p) + # The delivered witness deliberately makes these two conventions equal. + require(wild == supported, "wild pattern differs from pairing support") + index = {v: i for i, v in enumerate(full)} + edges = {(index[u], index[v]) for u, v in wild if u in index and v in index} + edge_max, vertex_max = acyclic_extrema(len(full), edges) + offset = n - len(harmonic) - len(full) + cost = sum(ranks) + return {"v": n, "harmonic_lines": len(harmonic), "full_support_lines": len(full), + "wild_edges": len(wild), "block_ranks": ranks, "cost": cost, + "mas_edges": edge_max, "mas_vertices": vertex_max, + "edge_bound": offset + edge_max, "vertex_bound": offset + vertex_max, + "edge_gap": offset + edge_max - cost} + + +def pairing(k): + return [[int(t == s or t // k != s // k) for s in range(3 * k)] + for t in range(3 * k)] + + +def expect_rejection(action, expected_message): + try: + action() + except ValueError as exc: + require(str(exc) == expected_message, "control failed for the wrong reason") + else: + raise ValueError("malformed control was accepted: " + expected_message) + + +def controls(fixture, expected): + p, q, matrix = (fixture[key] for key in ("p", "q", "B")) + bad = deepcopy(matrix) + bad[0][0] = 0 + expect_rejection(lambda: audit(p, q, bad), "pairing diagonal is not one") + bad = deepcopy(matrix) + bad[0][1] = 1 + expect_rejection(lambda: audit(p, q, bad), "pairing uses a nonincidence") + bad_p = deepcopy(p) + bad_p[0][0] += 1 + expect_rejection(lambda: audit(bad_p, q, matrix), "pairing uses a nonincidence") + bad_q = deepcopy(q) + bad_q[0] = list(q[3]) + expect_rejection(lambda: audit(p, bad_q, matrix), "zero rational diagonal") + require(not acyclic([0, 1], {(0, 1), (1, 0)}), "2-cycle was accepted") + require(rank_binary([0b101, 0b110, 0b011]) == 2 + and rank_by_span([0b101, 0b110, 0b011]) == 2, + "dependent rows were counted as independent") + + # Reindexing must not turn a block-structure assumption into an oracle. + for order in ([0, 3, 6, 1, 4, 7, 2, 5, 8], list(reversed(range(9)))): + report = audit([p[i] for i in order], [q[i] for i in order], + [[matrix[i][j] for j in order] for i in order]) + require(report == expected, "simultaneous reindexing changed the result") + + prototypes_p, prototypes_q = p[::3], q[::3] + small = [] + for k in (1, 2): + report = audit([row for row in prototypes_p for _ in range(k)], + [row for row in prototypes_q for _ in range(k)], pairing(k)) + require(report["edge_gap"] <= 0, "positive control became a counterexample") + require(report["mas_edges"] == 3 * k * k + and report["mas_vertices"] == k, "small graph oracle mismatch") + small.append({"k": k, "cost": report["cost"], "mas_edges": report["mas_edges"]}) + require(small == [{"k": 1, "cost": 3, "mas_edges": 3}, + {"k": 2, "cost": 18, "mas_edges": 12}], + "tight/nonviolating controls changed") + return small + + +def main(): + fixture = json.loads(Path(__file__).with_name("WITNESS.json").read_text(encoding="utf-8")) + report = audit(fixture["p"], fixture["q"], fixture["B"]) + require(report == fixture["expected"], "witness claim differs from exact calculation") + require(report["edge_gap"] > 0, "edge bound is not falsified") + require(report["cost"] >= report["vertex_bound"], "vertex bound is violated") + small = controls(fixture, report) + family = [] + for k in range(1, 17): + rank = rank_binary(row_bits(pairing(k))) + require(rank == 3 * k - (2 if k % 2 else 0), "family rank formula failed") + gap = 3 * k * k - 3 * rank + require((gap > 0) == (k >= 3), "family threshold failed") + family.append({"k": k, "rank": rank, "edge_gap": gap}) + print(json.dumps({"status": "PASS_B2_TRIPARTITE_EDGE_COUNTEREXAMPLE", + "witness": report, "positive_controls": small, + "rejection_controls": 4, "graph_and_rank_controls": 2, + "reindexings": 2, "family_rank_checks": family}, indent=2)) + + +if __name__ == "__main__": + main()