From 1edca15a2cf7a47c1959fe60489fcf6f3eee0e58 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Mon, 2 Nov 2026 22:19:16 +0000 Subject: [PATCH 1/2] docs(research): refute the quotient-direction edge bound --- .../README.md | 211 ++++++++++++++++++ .../SOURCES.json | 30 +++ .../TASK.json | 88 ++++++++ .../VERIFY.json | 34 +++ .../verify.py | 193 ++++++++++++++++ 5 files changed, 556 insertions(+) create mode 100644 research/quotient-direction-edge-counterexample/README.md create mode 100644 research/quotient-direction-edge-counterexample/SOURCES.json create mode 100644 research/quotient-direction-edge-counterexample/TASK.json create mode 100644 research/quotient-direction-edge-counterexample/VERIFY.json create mode 100644 research/quotient-direction-edge-counterexample/verify.py diff --git a/research/quotient-direction-edge-counterexample/README.md b/research/quotient-direction-edge-counterexample/README.md new file mode 100644 index 0000000000..ee6c5f7d26 --- /dev/null +++ b/research/quotient-direction-edge-counterexample/README.md @@ -0,0 +1,211 @@ +# Distinct directions do not repair the B2 acyclic-edge bound + +A six-line rational configuration has six distinct projective directions in +**each** factor family, exact minimum binary pairing cost **6**, and maximum +acyclic edge count **9**. Collapsing proportional `q` directions therefore +leaves a false lower bound. This answers Open next question 1 of +[Aaron Wang's PR2340](https://github.com/CrocSwap/integer-mult-bounds/pull/2340). + +Claim type: a finite counterexample with an exact scoped proof and exhaustive +finite corroboration. No new kappa, physical supplier or selected-frontier +change follows. This contribution is produced by Nick Petalas. +Independent human and formal proof-kernel review are unclaimed. + +## Model and proposed repair + +Use DreamingOfClouds's rank-three decoder model from +[PR2162](https://github.com/CrocSwap/integer-mult-bounds/pull/2162). +There are rational vectors `p_i,q_i` in `Q^3`, with `p_i.q_i != 0`. +An admissible binary matrix `B` has diagonal one and can have an off-diagonal +one at `(i,j)` only when `p_i.q_j=0`. Its cost is + +```text +cost(B) = sum_(a=0)^2 rank_F2 B[R_a,A_a], +R_a = {i : p_i[a] != 0}, A_a = {j : q_j[a] != 0}. +``` + +A wild edge `i -> j` is a zero off-diagonal dot product using all three +coordinates. `F` consists of lines with both supports full; `H` consists of +the harmonic lines with two equal diagonal coordinate contributions. +PR2340 distinguishes the valid maximum induced acyclic **vertex** count from +the false maximum acyclic **edge** count. Its proposed repair is to collapse +proportional `q` directions before counting edges, and ask whether + +```text +cost(B) >= v - |H| - |F| + masE_quotient. +``` + +For definiteness, quotient vertices are the equivalence classes under rational +proportionality of `q`; an edge exists if a wild edge connects those classes, +and loops are discarded. Every class below is a singleton, so representative, +edge-multiplicity and loop conventions cannot affect this counterexample. + +## Literal witness + +All coordinates are nonzero. Indices start at zero. + +| i | p_i | q_i | +|---:|---|---| +| 0 | (6,-5,1) | (1,1,1) | +| 1 | (-6,8,-2) | (1,2,4) | +| 2 | (2,-3,1) | (1,3,9) | +| 3 | (-2,6,-2) | (2,3,5) | +| 4 | (-10,10,-2) | (2,5,13) | +| 5 | (14,-16,4) | (2,4,10) | + +Direct multiplication gives the complete dot matrix + +```text + q0 q1 q2 q3 q4 q5 +p0 2 0 0 2 0 2 +p1 0 2 0 2 2 0 +p2 0 0 2 0 2 2 +p3 2 2 -2 4 0 0 +p4 -2 2 2 0 4 0 +p5 2 -2 2 0 0 4 +``` + +Its leading three-by-three block is `2I`, so the factorization has rank +exactly three. Divide `p0,p1,p2` by 2 and `p3,p4,p5` by 4 if a unit rational +diagonal is desired. This changes no support, direction, zero or admissible +binary pairing. + +For `q`, normalization to first coordinate one gives + +```text +(1,1,1), (1,2,4), (1,3,9), (1,3/2,5/2), (1,5/2,13/2), (1,2,5). +``` + +These are distinct. Primitive signed integer normalization of the `p` rows +gives `(6,-5,1),(3,-4,1),(2,-3,1),(1,-3,1),(5,-5,1),(7,-8,2)`, also distinct. +Thus there are no repeated projective points in either family. Since every +support is full, `F` has size six, `H` is empty, and all three cost blocks +are the entire matrix `B`. + +Choose `B=diag(J3,J3)`, with `J3` the three-by-three all-ones binary matrix. +Its literal rows are + +```text +111000 +111000 +111000 +000111 +000111 +000111 +``` + +Each off-diagonal one lies at a displayed zero dot product. Its two disjoint +nonzero row types are independent over `F2`, so `rank(B)=2` and `cost(B)=6`. +This is also the exact minimum. A binary rank-one matrix with every diagonal +entry one must be the all-ones matrix: writing it `u v^T`, every `u_i=v_i=1`. +That matrix is inadmissible, since `p0.q3=2 != 0`. Rank zero is incompatible +with the diagonal. Every admissible pairing therefore costs at least six. + +## Exact quotient edge count + +The complete wild graph consists of two bidirected triangles on `{0,1,2}` +and `{3,4,5}`, together with three additional edges + +```text +0 -> 4, 1 -> 5, 2 -> 3. +``` + +An acyclic edge set contains at most one orientation of each triangle pair, +for at most three edges per triangle. There are only three other edges, +so its size is at most nine. Put the first triangle before the second in a +total order and keep every forward edge. This retains all three extra edges +and three internal edges per triangle, attaining nine. + +The direction quotient changes nothing. Consequently + +```text +minimum cost = 6 < 0 + masE_quotient = 9. +``` + +The valid vertex bound is unaffected. An induced acyclic vertex set contains +at most one vertex per bidirected triangle, and any one from each triangle +is acyclic, giving vertex count two. The example also satisfies `cost(B)>=v`. +It does not refute that separate decoder target or the printed vertex theorem. + +The extra wild edges are absent from the attaining `B`. This identifies a +failure of the proposed direction-only repair that does not use duplicated +vectors. It is not a counterexample to an additional restriction that counts +only wild edges selected by `B`, with both factor families distinct. + +## Verification + +The standalone standard-library verifier imports no predecessor code and +executes no predecessor scientific suite. It checks every dot product, +actual coordinate support, primitive projective direction and selected pairing. +It enumerates all `2^15=32,768` admissible pairings and compares binary pivot +elimination with explicit row-space generation for every one. The exact cost +histogram is + +```text +cost 6 9 12 15 18 +pairings 1 119 4260 19140 9248 +``` + +All 720 vertex orders independently corroborate a 64-subset dynamic program +for the acyclic-edge optimum. Their forward-edge counts have histogram +`6:90, 7:270, 8:270, 9:90`. Ten controls reject seven malformed witnesses, +check sensitivity to removing a cross-triangle edge, and check identity and +all-ones ranks. Acceptance uses explicit exceptions and remains active under +optimized Python. + +From the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/quotient-direction-edge-counterexample/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/quotient-direction-edge-counterexample/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/quotient-direction-edge-counterexample +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/quotient-direction-edge-counterexample --check-source-history +``` + +Use any CPython 3.12 executable in place of the absolute interpreter elsewhere. +Direct runs print `PASS_QUOTIENT_DIRECTION_EDGE_COUNTEREXAMPLE` and a generated +exact summary. Optional `--receipt /absolute/external/path.json` creates a new +receipt with the result, interpreter version and hashes of all package files. +No receipt is hand-written or committed. + +The proof is self-contained. The runner authenticates the exact historical +source documents through [SOURCES.json](SOURCES.json); they are provenance, +not imported executable dependencies. Selected-source metadata orientation +passed. No selected scientific replay, native caller, dirty restoration, +compiler/hosting/precision/tape construction, supplier admission, Lean or +complete multiplication theorem was run or established. + +Managed Python allocations are bounded by this fixed six-line domain; a +row space has at most 64 elements, the census has 32,768 iterations, and graph +checks have 720 orders and 64 subsets. Every function is under 60 lines. +The verifier uses no recursion, dynamic code loading or third-party package. +Warning-strict normal and optimized runs provide the available diagnostics. + +## Open next questions + +Does the edge inequality hold when both factor families are projectively +distinct and the wild graph is restricted to off-diagonal ones of `B`? +This witness needs its three unselected edges for the gap. First derive a +rank-sensitive constraint for that changed graph; direction collapsing alone +is insufficient. PR2334 already rules out unrestricted selected-edge bounds +when repeated directions are allowed, so that predecessor must be retained. +A proof or a new counterexample for the combined restrictions remains absent. +This package stops at the first explicit quotient-repair counterexample. + +## Provenance and credit + +Scientific base: canonical main `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, +priority revision eight. [TASK.json](TASK.json) records the change from a +current-supplier decoder experiment to the explicit historical repair question. +This is a decoder-bound side result, with no current paid-profile improvement. +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19361606) +records the precise scope and checked overlap limits. + +Aaron Wang / navinor posed the quotient-direction question in PR2340 and +identified the edge/vertex distinction in PR2293. DreamingOfClouds supplies +the rank-three model and valid B2 vertex theorem in PR2162, following the +retained PR2111/PR1590 lineage. ROTl24's PR2334 supplies a separate repeated- +direction family with unbounded gaps and a selected-edge counterexample. +The new six-line witness, exact minimum and quotient-edge calculation are +produced by Nick Petalas. No predecessor credit or frozen source is changed. +Apache-2.0. diff --git a/research/quotient-direction-edge-counterexample/SOURCES.json b/research/quotient-direction-edge-counterexample/SOURCES.json new file mode 100644 index 0000000000..6db96a3b5f --- /dev/null +++ b/research/quotient-direction-edge-counterexample/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/b2-mas-edge-form-seed3609249d/README.md", + "usage": "provenance", + "git_blob": "eb176d74764853c8474087e15ede590f5e93e19b", + "sha256": "91f8775bd16b6a6392d9c5a48a252f6631e2b8cac1c3364f6efbd55583751463" + }, + { + "path": "research/char2-jets/README.md", + "usage": "provenance", + "git_blob": "38c80ad34faae0cb636825a92922fc889b190b44", + "sha256": "c1f20a1e7afb7eded3ff0ab765975f62466c5464ccaec143656319cdd4091945" + } + ] +} diff --git a/research/quotient-direction-edge-counterexample/TASK.json b/research/quotient-direction-edge-counterexample/TASK.json new file mode 100644 index 0000000000..28ae61c701 --- /dev/null +++ b/research/quotient-direction-edge-counterexample/TASK.json @@ -0,0 +1,88 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "docs/research/recursive-invoice-preflight.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "coframe", + "signed moment", + "5693", + "5698" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Refute PR2340 Open next question 1: collapsing proportional q directions does not repair the rank-three decoder acyclic-edge lower bound. Give one six-line configuration with both factor families projectively distinct, exact minimum cost six and quotient acyclic-edge count nine.", + "scope_change_reason": "The selected baseline first step passed. Instead of a current native coframe search, take the explicit external decoder-bound repair question left by PR2340. This is a scoped algebraic side result, not a completed supplier or signed-moment improvement.", + "bottleneck_link": "A direction-only repair cannot provide the proposed stronger decoder lower bound. The new obstruction tells a subsequent rank-aware certificate to account for unselected incidences or additional pairing constraints; it does not change the selected supplier.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified original quotient-repair counterexample. Do not seek a smaller witness, a larger gap or a family.", + "outcome": "completed", + "evidence": "Written six-line rational witness and exact proof: min cost six versus quotient-edge count nine. Self-contained enumeration checks all 32768 admissible pairings with two rank algorithms, all 720 orders against a 64-subset graph DP, and ten controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does the edge inequality hold for projectively distinct p and q families when the wild graph counts only the off-diagonal ones of the chosen B?", + "why_it_matters": "The present quotient-repair counterexample uses three unselected wild edges, while PR2334 excludes a selected-edge bound if repeated directions are allowed.", + "first_step": "Retain both distinctness hypotheses and derive a rank-sensitive bound for the selected-edge graph before searching.", + "blocked_by": "No proof or counterexample for the combined restrictions is supplied." + } + ], + "coordination_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19361606", + "claim_type": "finite counterexample with exact scoped proof", + "source_pr": { + "number": 2340, + "author": "navinor", + "inspected_head": "42a683190722292143e9b16716bc3baaba12e46f" + }, + "freshness": { + "canonical_main": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "priority_revision": 8, + "checked_utc": "2026-11-02T22:15:00Z", + "coverage": "Live open PRs, recent account work, active Discussions and latest handoffs, main README searches, merged distinctive-term searches and cached card overlap. Arbitrary diffs and unpublished work remain outside coverage." + } +} diff --git a/research/quotient-direction-edge-counterexample/VERIFY.json b/research/quotient-direction-edge-counterexample/VERIFY.json new file mode 100644 index 0000000000..053aa2299b --- /dev/null +++ b/research/quotient-direction-edge-counterexample/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": 120, + "checks": "Every dot, full support and projective direction; all 32768 admissible pairings with elimination/rowspace ranks; all 720 orders against subset DP; ten controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Identical complete finite coverage with optimization; explicit acceptance exceptions remain enabled." + } + ] +} diff --git a/research/quotient-direction-edge-counterexample/verify.py b/research/quotient-direction-edge-counterexample/verify.py new file mode 100644 index 0000000000..62112299e8 --- /dev/null +++ b/research/quotient-direction-edge-counterexample/verify.py @@ -0,0 +1,193 @@ +#!/usr/bin/env python3 +"""Exact six-line certificate for the failed q-direction quotient bound.""" + +import argparse +from collections import Counter +import hashlib +from itertools import permutations +import json +from math import gcd +from pathlib import Path +import sys + + +P = ((6, -5, 1), (-6, 8, -2), (2, -3, 1), + (-2, 6, -2), (-10, 10, -2), (14, -16, 4)) +Q = ((1, 1, 1), (1, 2, 4), (1, 3, 9), + (2, 3, 5), (2, 5, 13), (2, 4, 10)) +B = (7, 7, 7, 56, 56, 56) +SIZE = 6 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def direction(vector): + require(len(vector) == 3 and all(type(x) is int for x in vector), + "integer three-vector required") + divisor = gcd(*vector) + require(divisor != 0, "nonzero vector required") + first = next(x for x in vector if x) + return tuple(x // (divisor if first > 0 else -divisor) for x in vector) + + +def validate(p, q, rows): + require(len(p) == len(q) == len(rows) == SIZE, "six lines required") + for family in (p, q): + require(len({direction(v) for v in family}) == SIZE, + "projectively distinct directions required") + require(all(all(x != 0 for x in v) for v in family), + "full coordinate supports required") + dots = tuple(tuple(sum(a * b for a, b in zip(x, y)) for y in q) for x in p) + for i, row in enumerate(rows): + require(type(row) is int and 0 <= row < 1 << SIZE, "binary row required") + require(dots[i][i] != 0, "nonzero rational diagonal required") + require((row >> i) & 1, "unit binary diagonal required") + for j in range(SIZE): + if i != j and (row >> j) & 1: + require(dots[i][j] == 0, "inadmissible off-diagonal one") + return dots + + +def binary_rank(rows): + basis = [0] * SIZE + result = 0 + for row in rows: + value = row + for pivot in range(SIZE - 1, -1, -1): + if (value >> pivot) & 1: + if basis[pivot]: + value ^= basis[pivot] + else: + basis[pivot] = value + result += 1 + break + return result + + +def rowspace_rank(rows): + space = {0} + for row in rows: + space |= {x ^ row for x in tuple(space)} + require(len(space) & (len(space) - 1) == 0, "row space size is a power of two") + return len(space).bit_length() - 1 + + +def edge_optimum(edges): + best = [-1] * (1 << SIZE) + best[0] = 0 + for mask in range(1 << SIZE): + for last in range(SIZE): + if (mask >> last) & 1: + previous = mask ^ (1 << last) + incoming = sum(((previous >> i) & 1) for i, j in edges if j == last) + best[mask] = max(best[mask], best[previous] + incoming) + return best[-1] + + +def graph_checks(edges): + scores = Counter() + for order in permutations(range(SIZE)): + position = {v: i for i, v in enumerate(order)} + scores[sum(position[i] < position[j] for i, j in edges)] += 1 + require(sum(scores.values()) == 720, "all six-vertex orders enumerated") + require(max(scores) == edge_optimum(edges) == 9, "acyclic edge optimum nine") + return dict(sorted(scores.items())) + + +def pairing_census(edges): + require(len(edges) == 15, "fifteen admissible off-diagonal bits") + histogram = Counter() + for mask in range(1 << len(edges)): + rows = [1 << i for i in range(SIZE)] + for bit, (i, j) in enumerate(edges): + if (mask >> bit) & 1: + rows[i] |= 1 << j + rank = binary_rank(rows) + require(rank == rowspace_rank(rows), "elimination and row-space ranks agree") + histogram[3 * rank] += 1 + require(sum(histogram.values()) == 32768, "all admissible pairings enumerated") + require(min(histogram) == 6, "minimum coordinate-block rank cost six") + return dict(sorted(histogram.items())) + + +def rejection_controls(): + cases = [] + repeated = list(Q) + repeated[5] = tuple(2 * x for x in Q[0]) + cases.append((P, repeated, B)) + sparse = list(P) + sparse[0] = (0, -5, 1) + cases.append((sparse, Q, B)) + zero = list(Q) + zero[0] = (0, 0, 0) + cases.append((P, zero, B)) + orthogonal = list(P) + orthogonal[0] = (1, 1, -2) + cases.append((orthogonal, Q, B)) + missing = list(B) + missing[0] ^= 1 + cases.append((P, Q, missing)) + illegal = list(B) + illegal[0] |= 1 << 3 + cases.append((P, Q, illegal)) + bad_type = list(B) + bad_type[0] = True + cases.append((P, Q, bad_type)) + for p, q, rows in cases: + try: + validate(p, q, rows) + except ValueError: + continue + raise ValueError("invalid witness accepted") + return len(cases) + + +def certificate(): + dots = validate(P, Q, B) + edges = tuple((i, j) for i in range(SIZE) for j in range(SIZE) + if i != j and dots[i][j] == 0) + internal = {(i, j) for i in range(SIZE) for j in range(SIZE) + if i != j and i // 3 == j // 3} + require(set(edges) == internal | {(0, 4), (1, 5), (2, 3)}, "literal wild graph") + require(binary_rank(B) == rowspace_rank(B) == 2, "attaining pairing rank two") + orders = graph_checks(edges) + census = pairing_census(edges) + controls = rejection_controls() + reduced = tuple(edge for edge in edges if edge != (0, 4)) + require(edge_optimum(reduced) == 8, "deleted cross edge changes optimum") + require(binary_rank((1, 2, 4, 8, 16, 32)) == 6, "identity rank control") + require(binary_rank((63,) * SIZE) == 1, "all-ones rank control") + return {"lines": SIZE, "distinct_p_directions": SIZE, "distinct_q_directions": SIZE, + "dot_matrix": dots, "wild_edges": edges, "pairing_rows": B, + "minimum_cost": 6, "quotient_acyclic_edges": 9, "gap": 3, + "order_score_histogram": orders, "pairing_cost_histogram": census, + "orders": 720, "admissible_pairings": 32768, + "rank_crosschecks": 32768, "controls": controls + 3} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path) + args = parser.parse_args() + result = certificate() + here = Path(__file__).resolve().parent + hashes = {p.name: hashlib.sha256(p.read_bytes()).hexdigest() + for p in sorted(here.iterdir()) if p.is_file()} + receipt = {"status": "PASS_QUOTIENT_DIRECTION_EDGE_COUNTEREXAMPLE", + "claim_type": "finite counterexample with exact scoped proof", + "result": result, "package_sha256": hashes, + "python": sys.version.split()[0]} + encoded = json.dumps(receipt, sort_keys=True, indent=2) + "\n" + if args.receipt is not None: + require(here not in args.receipt.resolve().parents, "receipt must be outside package") + with args.receipt.open("x", encoding="utf-8") as stream: + stream.write(encoded) + print(receipt["status"]) + print(json.dumps(result, sort_keys=True)) + + +if __name__ == "__main__": + main() From 090953af3c999a33ff4ed1f9e7dbf53c2dba3f56 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Mon, 2 Nov 2026 22:20:27 +0000 Subject: [PATCH 2/2] docs(research): clarify the remaining rank-aware question --- research/quotient-direction-edge-counterexample/README.md | 4 +++- research/quotient-direction-edge-counterexample/TASK.json | 2 +- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/research/quotient-direction-edge-counterexample/README.md b/research/quotient-direction-edge-counterexample/README.md index ee6c5f7d26..7155c75b01 100644 --- a/research/quotient-direction-edge-counterexample/README.md +++ b/research/quotient-direction-edge-counterexample/README.md @@ -3,7 +3,8 @@ A six-line rational configuration has six distinct projective directions in **each** factor family, exact minimum binary pairing cost **6**, and maximum acyclic edge count **9**. Collapsing proportional `q` directions therefore -leaves a false lower bound. This answers Open next question 1 of +leaves a false lower bound. This refutes the repair proposed as the first step in +Open next question 1 of [Aaron Wang's PR2340](https://github.com/CrocSwap/integer-mult-bounds/pull/2340). Claim type: a finite counterexample with an exact scoped proof and exhaustive @@ -190,6 +191,7 @@ rank-sensitive constraint for that changed graph; direction collapsing alone is insufficient. PR2334 already rules out unrestricted selected-edge bounds when repeated directions are allowed, so that predecessor must be retained. A proof or a new counterexample for the combined restrictions remains absent. +PR2340's broader request for the strongest rank-aware replacement remains open. This package stops at the first explicit quotient-repair counterexample. ## Provenance and credit diff --git a/research/quotient-direction-edge-counterexample/TASK.json b/research/quotient-direction-edge-counterexample/TASK.json index 28ae61c701..5108651dbb 100644 --- a/research/quotient-direction-edge-counterexample/TASK.json +++ b/research/quotient-direction-edge-counterexample/TASK.json @@ -55,7 +55,7 @@ ] }, "scope_status": "changed", - "actual_scope": "Refute PR2340 Open next question 1: collapsing proportional q directions does not repair the rank-three decoder acyclic-edge lower bound. Give one six-line configuration with both factor families projectively distinct, exact minimum cost six and quotient acyclic-edge count nine.", + "actual_scope": "Refute the quotient-direction repair proposed as the first step in PR2340 Open next question 1: collapsing proportional q directions does not repair the rank-three decoder acyclic-edge lower bound. Give one six-line configuration with both factor families projectively distinct, exact minimum cost six and quotient acyclic-edge count nine. The strongest rank-aware replacement remains open.", "scope_change_reason": "The selected baseline first step passed. Instead of a current native coframe search, take the explicit external decoder-bound repair question left by PR2340. This is a scoped algebraic side result, not a completed supplier or signed-moment improvement.", "bottleneck_link": "A direction-only repair cannot provide the proposed stronger decoder lower bound. The new obstruction tells a subsequent rank-aware certificate to account for unselected incidences or additional pairing constraints; it does not change the selected supplier.", "budget_minutes": 60,