diff --git a/research/dn-three-cycle-floor/PROOF.md b/research/dn-three-cycle-floor/PROOF.md new file mode 100644 index 0000000000..0ca7a8455e --- /dev/null +++ b/research/dn-three-cycle-floor/PROOF.md @@ -0,0 +1,110 @@ +# Three-cycle obstruction outside two product loci + +This proof was produced by Nick Petalas. Apache-2.0. + +## Statement + +Let G be any finite simple graph on n >= 3 coordinates. On every edge +{i,k}, i= degree_G(j) for every j, + C_B(P,Q) >= 2|E(G)| = v. + +The statement includes zero coefficients and arbitrary additional coordinates. +It excludes this ordered coordinate-cycle family away from h=+/-1. It does +not exclude savings on those two loci or for other three-shear patterns. + +## Common sign roots and the credited forced minor + +For rational vectors p,q and edge {j,k}, the two sign-root products satisfy + + (p_j+p_k)(q_j+q_k) + (p_j-p_k)(q_j-q_k) + = 2(p_j q_j + p_k q_k). (1) + +Thus a nonzero right side guarantees at least one sign root in both +supports of R p and R q. For each edge incident to j, choose one such +root as both a row and a column of the support rectangle. Distinct chosen +roots share exactly coordinate j and have inner product +1 or -1. Their +B off-diagonal entries are forced to zero and their diagonals are one. +They therefore form an identity minor of size degree_G(j). + +This common-support degree argument is the lemma of JoyboyBrian's #5214, +building on Nick Petalas's #5176. It is cited and restated to make the new +application readable. No new general rank-minor principle is claimed. + +## New cycle calculation + +Relabel a,b,c as 0,1,2. The affected blocks are exactly + + M = [ 1+h t ts ], M^(-T) = [ 1 0 -u ], + [ su 1 s ] [ -t 1 tu ] + [ u 0 1 ] [ 0 -s 1 ] + +and both matrices are identity on other coordinates. The factors are +reciprocal, so P Q^T=R M M^-1 R^T=R R^T on every input. + +For column j, write w_k=M_kj (M^(-T))_kj. These products, not the separate +entries, decide the right side of (1). The three changed columns give + +| Column j | w_a | w_b | w_c | All other w_k | +| --- | ---: | ---: | ---: | ---: | +| a | 1+h | -h | 0 | 0 | +| b | 0 | 1 | 0 | 0 | +| c | -h | h | 1 | 0 | + +For the a-term, an edge to b has w_a+w_b=1. Any other incident edge has +sum 1+h. For the b-term, every incident edge has sum 1. For the c-term, +an edge to a has sum 1-h, an edge to b has sum 1+h, and every other +incident edge has sum 1. An unchanged coordinate has w_j=1 and all other +w_k=0, so its incident sums are also 1. + +All listed sums are nonzero when h is neither 1 nor -1. Equation (1) and +the degree lemma therefore give the asserted termwise bounds. Summing the +degrees counts each edge twice and proves the complete bill floor. The +empty-edge graph has zero bill and satisfies the theorem trivially. + +At zero coefficients the coordinate basis and the common pairing B_* +with all-ones 2-by-2 blocks on each sign pair attain v. Hence the joint +minimum over this allowed family and all pairings is v. This is not a +claim that every fixed nonzero M attains its lower bound. + +## Why the excluded loci remain open + +At t=s=u=1, take the single edge {a,c}. The c-term's P values on its two +roots are (2,0), and its Q values are (0,-2). No common sign root survives. +At t=s=1,u=-1, the same failure occurs on edge {b,c} in the c-term, with +P values (2,0) and Q values (0,-2). + +These are failures of this particular degree minor. Neither is a +counterexample to the complete bill floor: other terms and common-pairing +constraints still contribute. In particular the theorem makes no claim +that either exceptional locus supplies an improvement. + +## Evidence and limits + +The standalone verifier builds M by literal shear multiplication and +obtains its dual by rational Gaussian elimination. It compares both with +the displayed matrices, checks every Gram entry and chosen identity minor, +and enumerates every fitting directed B on the stated three-coordinate +domains. A separate set-of-span oracle checks every small binary rank. +Finite tests corroborate this proof; they are not its universal quantifier. + +The proof concerns rational Gram factors, paired sign roots, a fixed square +factor count and one common directed fitting binary pairing. It gives no +physical coefficient arithmetic, native implementation, producer/consumer, +dirty-restoration program, stock, precision, tape or recursive invoice. +No new kappa, supplier admission or complete multiplication theorem follows. +Independent human and formal proof-kernel review are unclaimed. diff --git a/research/dn-three-cycle-floor/README.md b/research/dn-three-cycle-floor/README.md new file mode 100644 index 0000000000..2c45729a15 --- /dev/null +++ b/research/dn-three-cycle-floor/README.md @@ -0,0 +1,132 @@ +# Three-shear cycles need exceptional products to escape the paired-root floor + +This contribution was produced by Nick Petalas. Apache-2.0. +Independent human and formal proof-kernel review are unclaimed. + +Claim type: scoped written proof with exact finite corroboration. For every +finite simple graph, retain both roots e_i+e_j and e_i-e_j on each edge. +Let R contain those rows, and change the Gram factor basis by + + M=(I+t E_ab)(I+s E_bc)(I+u E_ca), + P=R M, Q=R M^(-T), with distinct a,b,c and rational t,s,u. + +Whenever tsu is neither 1 nor -1, every common directed fitting binary +pairing B has the complete algebraic COPY bill + + sum_j rank_F2 B[supp(P_j),supp(Q_j)] >= 2|E|. + +In fact every term costs at least its coordinate's graph degree. The +coordinate basis attains the bound, so the joint optimum over this allowed +family is exactly the number of live roots. A fixed nonzero basis can cost +more. Isolated coordinates and zero shear coefficients are included. + +This extends the two-interacting-shear obstruction of JoyboyBrian's +[PR5214](https://github.com/CrocSwap/integer-mult-bounds/pull/5214) into the +three-coordinate-cycle case. That package explicitly leaves three interacting +shears open. Its forced identity-minor lemma is a cited predecessor; the new +step is the cycle calculation and its all-graph application. The result +narrows this cycle family to two exceptional product loci for any possible +saving. Neither locus is claimed to save anything. + +[PROOF.md](PROOF.md) gives the universal proof and two explicit lost-minor +examples on tsu=+/-1. Those examples explain the proof boundary; a missing +minor alone is not a favorable complete invoice. + +## Reproduce + +From the repository root, with CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/dn-three-cycle-floor/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/dn-three-cycle-floor/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/dn-three-cycle-floor +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/dn-three-cycle-floor --check-source-history +``` + +Any other CPython 3.12 executable can replace the local path. The direct +marker is PASS_DN_THREE_CYCLE_FLOOR. Each direct run prints a generated JSON +receipt bound to all six package files. It writes no files, imports no +predecessor executable and works outside a Git checkout. The generic runner +separately validates exact historical source pins. + +The finite corroboration checks every nonempty graph on three coordinates +and every coefficient triple in {-2,-1,-1/2,0,1/2,1,2} outside the two excluded +product loci. There are 2,009 exact factorizations and 35,588 complete common +pairing bills, with all admissible directed pairing entries enumerated. +It checks 309,960 identity-minor entries and 106,764 comparisons against a +separately implemented set-of-span rank oracle. The 56 excluded coefficient +triples are counted as excluded, rather than accepted by the theorem. + +Another 24 factorizations in dimensions four, five and eight include external +edges, isolated coordinates, zero coefficients and rational coefficients. +They check 168 complete directed-pairing bills and 2,856 minor entries. On +PR5214's actual 12-root D5 graph, t=2,s=u=1 has edge-block bill +(4,3,5,2,2), total 16. This is an explicit complete bill, not its optimized +minimum. Eight rejecting domain, fitting and false-minor controls and two +exceptional-locus witnesses pass. Rational elimination derives the dual +separately from the displayed formula; every Gram entry is checked. + +## Scope and provenance + +The scientific base is canonical main e54523517d0f03e58352e647c403a5af3e525a57, +priority revision 8, selected #7000. TASK.json records a changed +complex-rank-shape-decoder scope to this algebraic side result. The selected +source-binding first example passed; no selected scientific replay ran. +SOURCES.json pins PR5214's incorporated proof and README as provenance. +No predecessor proof, result or frozen source is changed or scientifically +replayed. + +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19539403) +records the scope. Live PR and handoff checks, batch reservations, main README +searches and merged-PR searches found no matching cycle theorem in the +checked coverage. The cached overlap report covers 489 open PRs and 7,156 +Discussion records with complete pagination, but only 207 of 10,178 tracked +local notes were materialized at its first task scan. Main-tree searches and +the relevant source reads supplemented that sparse coverage. Unpublished +work and arbitrary historical diffs are not covered; global literature +priority is unclaimed. + +The theorem concerns rational paired roots and this ordered shear cycle. +Other three-shear patterns, either exceptional product locus, single-sign +deletions, larger basis families, extra terms and factors outside the root +code remain outside it. The physical coefficient arithmetic, producer and +consumer, dirty restoration, frames, native alignment, storage, precision, +tape movement and full recursive bill are unpriced. No new kappa, physical +supplier, complete multiplication theorem, selected-frontier change or +framework-assumption discharge is claimed. No Lean or Docker check ran. + +## Open next questions + +1. Can tsu=1 or tsu=-1 lower the complete common-pairing bill on an actual + paired graph? Start with the two lost-minor fixtures and then price all + terms on a paired D5 graph using one fitting B. The lost minor is the + current proof gap, not evidence of a saving. +2. Can a different three-shear index pattern or basis family give an actual + paid decoder improvement? Start with full Gram equality, one common + fitting pairing and a complete coefficient/restoration/frame invoice. + The physical producer/consumer and recursive budget remain blockers. + +## Credit and implementation constraints + +JoyboyBrian #5214 supplies the explicit next question, common-support degree +lemma and two-shear boundary. Nick Petalas #5176 supplies the fixed-split +predecessor; ywz65 #2536/#2719 supplies coordinate pairing and full-Dn +root-code results; Aaron Wang / navinor #2272/#2518 supplies the small-T +screens; DreamingOfClouds supplies the retained Gram/COPY model and root-code +lineage. Their results are cited, not audited here. The new cycle obstruction, +proof and finite checker were produced by Nick Petalas. Classical matrix +multiplication, Gaussian elimination and binary rank retain their status as +classical tools. + +The verifier has no recursion, process launch, network access, mutable global +cache or dynamic code. All loops run over fixed finite fixture collections +or dimensions bounded by eight; each binary reduction has a 57-step cap. +Functions are at most 31 physical lines. Explicit exceptions remain enabled +under -O. CPython's managed Fraction, integer and container allocation is a +deviation from fixed allocation. Coordinate matrices have at most eight rows +and columns, root matrices have at most 56 rows and eight columns, and Gram +matrices have at most 56 rows and columns. Actual fixtures have at most 12 +root rows. Pairing enumeration uses at most six free bits. The independent +span oracle has at most six rows and 64 states. No allocation-free runtime claim +is made. Warning-strict normal/optimized execution and AST inspection are +the available diagnostics; separate type or lint analysis is unclaimed. diff --git a/research/dn-three-cycle-floor/SOURCES.json b/research/dn-three-cycle-floor/SOURCES.json new file mode 100644 index 0000000000..27312e5abf --- /dev/null +++ b/research/dn-three-cycle-floor/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/dn-two-shear-pairing-floor/PROOF.md", + "usage": "provenance", + "git_blob": "e04b2a8d0e932fc47a99ec45977262243f524f86", + "sha256": "93053bfceb52f228028f5b8fb9d2c0cf3cf4cc2275af7955230095137c177280" + }, + { + "path": "research/dn-two-shear-pairing-floor/README.md", + "usage": "provenance", + "git_blob": "97a575117ce72b03aa300bc98f48effd00c245bd", + "sha256": "bb28ba388668915b0fbe35843174f2b4fc5d1c45daeab1e028784b3f779a29eb" + } + ] +} diff --git a/research/dn-three-cycle-floor/TASK.json b/research/dn-three-cycle-floor/TASK.json new file mode 100644 index 0000000000..b548b05409 --- /dev/null +++ b/research/dn-three-cycle-floor/TASK.json @@ -0,0 +1,83 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "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": "Universal paired-root algebraic COPY floor for a three-shear coordinate cycle whenever tsu is neither 1 nor -1.", + "scope_change_reason": "Takes the three-interacting-shear open question of JoyboyBrian PR5214. This is an algebraic side obstruction, without a legal physical producer/consumer or complete recursive invoice.", + "bottleneck_link": "Excludes the stated open part of a changed-basis decoder family from lowering its complete common-pairing algebraic COPY bill. Physical supplier obligations remain separate.", + "budget_minutes": 60, + "stop_rule": "Ship the first proved extension; do not pursue the exceptional product loci or another basis family.", + "outcome": "completed", + "evidence": "PROOF.md gives the all-graph rational theorem; verify.py gives exact Gram identities, complete small pairing censuses, forced minors, independent span ranks and rejecting controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can either exceptional product locus tsu=1 or tsu=-1 lower the complete common-pairing bill on a paired graph?", + "why_it_matters": "The new proof excludes the complementary parameter domain. Its lost minor alone does not decide the exceptional loci.", + "first_step": "Use the two explicit lost-minor fixtures, then price every term with one common fitting pairing on an actual paired D5 graph.", + "blocked_by": "No complete favorable common-pairing invoice or uniform replacement lower bound is supplied." + }, + { + "question": "Can a fully priced actual decoder use a different three-shear index pattern or another basis family?", + "why_it_matters": "The ordered coordinate cycle and paired-sign hypotheses delimit this obstruction.", + "first_step": "Write one exact Gram factorization, one common fitting pairing and the complete coefficient, restoration, frame and recursive invoice.", + "blocked_by": "Physical producer/consumer and complete bill remain unknown." + } + ], + "claim_type": "scoped written proof with exact finite corroboration", + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19539403" +} diff --git a/research/dn-three-cycle-floor/VERIFY.json b/research/dn-three-cycle-floor/VERIFY.json new file mode 100644 index 0000000000..cd55106674 --- /dev/null +++ b/research/dn-three-cycle-floor/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": "Exact cycle factors, complete small common-pairing invoices, forced identity minors, independent span ranks and semantic rejection controls" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same scientific and rejection checks with Python assertions disabled" + } + ] +} diff --git a/research/dn-three-cycle-floor/verify.py b/research/dn-three-cycle-floor/verify.py new file mode 100644 index 0000000000..c9a89c4561 --- /dev/null +++ b/research/dn-three-cycle-floor/verify.py @@ -0,0 +1,281 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the paired-root three-cycle theorem.""" +from fractions import Fraction as F +from hashlib import sha256 +from itertools import combinations, product +import json +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def identity(n): + require(type(n) is int and 1 <= n <= 8, "dimension outside 1..8") + return [[F(i == j) for j in range(n)] for i in range(n)] + + +def transpose(a): + require(a and a[0] and all(len(r) == len(a[0]) for r in a), "bad matrix") + return [list(c) for c in zip(*a)] + + +def multiply(a, b): + require(a and b and len(a[0]) == len(b), "bad product dimensions") + bt = transpose(b) + return [[sum((x * y for x, y in zip(r, c)), F(0)) for c in bt] for r in a] + + +def inverse(a): + n = len(a) + require(1 <= n <= 8 and all(len(r) == n for r in a), "bad square matrix") + w = [list(r) + e for r, e in zip(a, identity(n))] + for j in range(n): + k = next((k for k in range(j, n) if w[k][j]), None) + require(k is not None, "singular matrix") + w[j], w[k] = w[k], w[j] + w[j] = [x / w[j][j] for x in w[j]] + for k in range(n): + if k != j: + scale = w[k][j] + w[k] = [x - scale * y for x, y in zip(w[k], w[j])] + require([r[:n] for r in w] == identity(n), "inverse elimination failed") + return [r[n:] for r in w] + + +def roots(n, edges): + identity(n) + require(edges and len(edges) <= 28 and len(set(edges)) == len(edges), "bad edges") + require(all(type(i) is int and type(j) is int and 0 <= i < j < n + for i, j in edges), "bad edge endpoints") + rows = [] + for i, j in edges: + for sign in (1, -1): + row = [F(0)] * n + row[i], row[j] = F(1), F(sign) + rows.append(row) + return rows + + +def cycle(n, t, s, u): + require(n >= 3, "cycle needs three coordinates") + require(all(type(x) in (int, F) and abs(x) <= 8 for x in (t, s, u)), + "bad cycle coefficient") + t, s, u = F(t), F(s), F(u) + m = identity(n) + for a, b, x in ((0, 1, t), (1, 2, s), (2, 0, u)): + h = identity(n) + h[a][b] = x + m = multiply(m, h) + dual = transpose(inverse(m)) + closed_m, closed_q = identity(n), identity(n) + closed_m[:3] = [r + [F(0)] * (n - 3) for r in + ([1 + t*s*u, t, t*s], [s*u, 1, s], [u, 0, 1])] + closed_q[:3] = [r + [F(0)] * (n - 3) for r in + ([1, 0, -u], [-t, 1, t*u], [0, -s, 1])] + require(m == closed_m and dual == closed_q, "closed cycle formula mismatch") + return m, dual + + +def factors(n, edges, coeffs): + r = roots(n, edges) + m, dual = cycle(n, *coeffs) + p, q = multiply(r, m), multiply(r, dual) + require(multiply(p, transpose(q)) == multiply(r, transpose(r)), "wrong Gram endpoint") + return r, p, q + + +def star_witnesses(n, edges, p, q): + witnesses = [] + for j in range(n): + chosen = [] + for e, edge in enumerate(edges): + if j in edge: + choices = [k for k in (2*e, 2*e+1) if p[k][j] and q[k][j]] + require(choices, "missing common sign root") + chosen.append(choices[0]) + witnesses.append(chosen) + return witnesses + + +def fitting(r, b): + v = len(r) + require(len(b) == v and all(type(row) is int and 0 <= row < 1 << v for row in b), + "bad binary matrix") + for i in range(v): + require(b[i] >> i & 1, "missing diagonal one") + for j in range(v): + if i != j and sum(x*y for x, y in zip(r[i], r[j])): + require(not (b[i] >> j & 1), "forbidden nonorthogonal entry") + + +def pairings(r): + v = len(r) + free = [(i, j) for i in range(v) for j in range(v) if i != j + and sum(x*y for x, y in zip(r[i], r[j])) == 0] + require(len(free) <= 6, "complete census limited to six free bits") + for bits in range(1 << len(free)): + b = [1 << i for i in range(v)] + for k, (i, j) in enumerate(free): + b[i] |= (bits >> k & 1) << j + yield b + + +def rank(rows): + pivots = {} + for row in rows: + for _ in range(57): + if not row: + break + j = row.bit_length() - 1 + if j not in pivots: + pivots[j] = row + break + row ^= pivots[j] + else: + raise ValueError("rank iteration bound exhausted") + return len(pivots) + + +def span_rank(rows): + require(len(rows) <= 6, "span oracle limited to six rows") + space = {0} + for row in rows: + space |= {x ^ row for x in space} + require(len(space).bit_count() == 1, "span size is not a power of two") + return len(space).bit_length() - 1 + + +def bill(p, q, b, oracle=False): + costs = [] + for j in range(len(p[0])): + cols = sum(1 << k for k in range(len(q)) if q[k][j]) + rows = [b[k] & cols for k in range(len(p)) if p[k][j]] + cost = rank(rows) + if oracle: + require(cost == span_rank(rows), "rank and span disagree") + costs.append(cost) + return costs + + +def check_minors(r, b, witnesses): + count = 0 + for chosen in witnesses: + for i in chosen: + for j in chosen: + require((b[i] >> j & 1) == (i == j), "forced minor is not identity") + count += 1 + return count + + +def small_census(): + alphabet = tuple(map(F, (-2, -1, 0, 1, 2))) + (F(-1, 2), F(1, 2)) + all_edges = list(combinations(range(3), 2)) + totals = dict(factorizations=0, common_pairing_bills=0, identity_entries=0, + span_comparisons=0, excluded_parameter_triples=0) + for coeffs in product(alphabet, repeat=3): + if coeffs[0]*coeffs[1]*coeffs[2] in (-1, 1): + totals["excluded_parameter_triples"] += 1 + continue + for mask in range(1, 8): + edges = [e for k, e in enumerate(all_edges) if mask >> k & 1] + r, p, q = factors(3, edges, coeffs) + witnesses = star_witnesses(3, edges, p, q) + totals["factorizations"] += 1 + for b in pairings(r): + fitting(r, b) + costs = bill(p, q, b, oracle=True) + require(all(c >= len(w) for c, w in zip(costs, witnesses)), + "term fell below its degree") + require(sum(costs) >= len(r), "complete bill below root count") + totals["identity_entries"] += check_minors(r, b, witnesses) + totals["common_pairing_bills"] += 1 + totals["span_comparisons"] += 3 + return totals + + +def sampled_pairing(r, seed): + v = len(r) + return [sum(1 << j for j in range(v) if i == j or + (sum(x*y for x, y in zip(r[i], r[j])) == 0 and + ((i+1)*17 + (j+1)*31 + seed*13) % 7 < 3)) for i in range(v)] + + +def larger_fixtures(): + graphs = [(4, [(0, 1), (1, 2), (2, 3)]), + (5, [(0, 1), (0, 2), (0, 4), (1, 2), (2, 3), (3, 4)]), + (8, [(0, 3), (0, 4), (1, 4), (2, 5), (2, 6)]), + (8, [(0, 1), (0, 2), (1, 2)])] + triples = [(F(2), F(1), F(1)), (F(-2), F(1), F(1)), + (F(1, 2), F(1, 2), F(1, 2)), (F(0), F(2), F(-1)), + (F(-2), F(-2), F(2)), (F(1), F(-1, 2), F(1))] + totals = dict(factorizations=0, common_pairing_bills=0, identity_entries=0) + first_fixture = None + for n, edges in graphs: + for coeffs in triples: + r, p, q = factors(n, edges, coeffs) + witnesses = star_witnesses(n, edges, p, q) + for seed in range(7): + b = sampled_pairing(r, seed) + fitting(r, b) + costs = bill(p, q, b) + require(all(c >= len(w) for c, w in zip(costs, witnesses)), + "large term below degree") + totals["identity_entries"] += check_minors(r, b, witnesses) + totals["common_pairing_bills"] += 1 + if n == 5 and coeffs == triples[0]: + b = [(3 << (2*(i//2))) for i in range(len(r))] + fitting(r, b) + first_fixture = bill(p, q, b) + totals["factorizations"] += 1 + require(first_fixture is not None, "missing actual D5 example") + totals["actual_D5_edge_block_bill"] = first_fixture + return totals + + +def rejected_controls(): + probes = [(1, (1, 1, 1), (0, 2)), (-1, (1, 1, -1), (1, 2))] + for value, coeffs, edge in probes: + _, p, q = factors(3, [edge], coeffs) + require(coeffs[0]*coeffs[1]*coeffs[2] == value, "wrong exceptional fixture") + require(all(not (p[k][2] and q[k][2]) for k in range(2)), + "exceptional minor unexpectedly survives") + rejected = 0 + for mode in range(8): + try: + if mode == 0: + roots(3, [(1, 0)]) + elif mode == 1: + roots(3, [(0, 1), (0, 1)]) + elif mode == 2: + cycle(2, 1, 1, 1) + elif mode == 3: + cycle(3, 9, 1, 1) + elif mode == 4: + inverse([[F(0), F(0)], [F(0), F(0)]]) + elif mode == 5: + fitting(roots(3, [(0, 1)]), [0, 0]) + elif mode == 6: + fitting(roots(3, [(0, 1), (1, 2)]), [5, 2, 4, 8]) + else: + _, p, q = factors(3, [(0, 2)], (1, 1, 1)) + star_witnesses(3, [(0, 2)], p, q) + except ValueError: + rejected += 1 + require(rejected == 8, "a rejecting control was accepted") + return dict(rejected_inputs_and_false_minors=rejected, exceptional_locus_witnesses=2) + + +def main(): + result = dict(small=small_census(), larger=larger_fixtures(), controls=rejected_controls()) + package = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + result["sha256"] = {name: sha256((package/name).read_bytes()).hexdigest() for name in names} + result["status"] = "PASS_DN_THREE_CYCLE_FLOOR" + print(json.dumps(result, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()