diff --git a/research/height-one-shear-bicliques/PROOF.md b/research/height-one-shear-bicliques/PROOF.md new file mode 100644 index 0000000000..e45d05a291 --- /dev/null +++ b/research/height-one-shear-bicliques/PROOF.md @@ -0,0 +1,117 @@ +# Exact balanced optimum at coefficient height one + +All ranks in this note are over the rationals. Let + +```text +D = {M in Mat_2(Z) : every entry belongs to {-1,0,1}}. +``` + +A balanced rank-distance biclique of order r consists of two r-element +subsets E and O of D. Distinct matrices in the same part have difference +rank two; every cross-part difference has rank one. + +**Result.** The maximum r is exactly six. The lower bound has a written +construction. The upper bound is an exact finite enumeration with two +implementations and the coverage argument below. No formal-kernel acceptance +of that finite computation is claimed. + +## Six-by-six construction + +Write q(a,b)=a^2+ab+b^2 and take + +```text +S = {(-1,0), (-1,1), (0,-1), (0,1), (1,-1), (1,0)}. +E(a,b) = [[a,b],[-a-b,a]] +O(a,b) = [[a,b],[b,-a-b]] for (a,b) in S. +``` + +Every point in S satisfies q=1 and every displayed entry is in {-1,0,1}. +The determinant identities are + +```text +det(E(a,b)-E(u,v)) = q(a-u,b-v) +det(O(a,b)-O(u,v)) = -q(a-u,b-v) +det(E(a,b)-O(u,v)) = q(a,b)-q(u,v) = 0. +``` + +The identity `4q(a,b)=(2a+b)^2+3b^2` proves strict positivity away from +zero over Q. Thus distinct same-part differences have rank two. The parts +are disjoint because E has determinant one and O has determinant minus one. +Consequently every cross difference is nonzero and singular, with rank one. + +For the actual shear frames + +```text +Phi(M) = [[I_2,M],[0,I_2]], +``` + +we have `Phi(M)Phi(N)=Phi(M+N)` and +`rank(Phi(M)-Phi(N))=rank(M-N)`. Hence these twelve commuting integral +four-by-four frames have the rank-distance metric K_(6,6). + +## Upper bound by a complete finite certificate + +For every unordered triple {A,B,C} of distinct matrices in D whose three +pairwise differences have rank two, count + +```text +N(A,B,C) = #{X in D : rank(X-A)=rank(X-B)=rank(X-C)=1}. +``` + +The enumeration gives the following complete distribution. + +| N(A,B,C) | Number of triples | +|---:|---:| +| 0 | 1,480 | +| 1 | 4,368 | +| 2 | 9,624 | +| 3 | 5,760 | +| 4 | 2,096 | +| 6 | 160 | + +There are 23,488 such triples. In particular each has at most six common +rank-one contacts. A purported K_(7,7) contains three matrices in its first +part, while all seven matrices of its second part would be contacts of that +triple. This contradicts the certified ceiling six. Any larger balanced +biclique contains a K_(7,7), so it is excluded as well. + +This upper certificate does not assume that the contacts themselves have +pairwise rank-two differences. Its relaxation is sufficient for the ceiling. + +## Why both enumerations cover the domain + +`verify.py` creates exactly the 3^4=81 lexicographically ordered matrices. +For every ordered matrix pair, it computes rank from its determinant and +whether the difference is zero. It visits each of the binomial(81,3)=85,320 +unordered triples once. Rank-two adjacency selects the admissible triples; +intersection of three 81-bit rank-one neighbor sets counts their contacts. +It checks the complete histogram and emits a hash of every retained triple +and its full contact bitset, in order. + +`ceiling.py` imports no scientific code from the first verifier. It derives +all pair ranks by exact Fraction Gaussian elimination. Two matrices with +the same first row cannot have rank-two difference. An admissible triple +therefore uses three distinct first rows among the nine possible rows. +For each of the binomial(9,3) choices, it tries all 9^3 second-row choices, +giving 61,236 candidates. Sorting first rows gives every admissible triple +exactly once, even though this ordering differs from the first enumeration. +For each accepted triple it scans all 81 matrices and tests the three +contact ranks individually. It recovers the same complete histogram. +It also checks all 144 ordered differences of the twelve four-by-four +shear frames by Fraction elimination, covering attainment directly. + +The first verifier rejects a missing witness matrix, duplicates, a height +violation, Boolean or noninteger entries, a malformed shape, overlapping +parts, a same-part rank-one change, and missing/repeated domain vertices. +The second verifier checks elimination on zero, singular, nonsingular, +pivot-swap and rational fixtures. All acceptance checks remain enabled under +optimized Python. + +## Scope + +This is an exact finite result for D, with a rational construction proof. +It does not bound larger coefficient heights, rational entries of bounded +denominator, different matrix orders, or other fields. The elementary +determinant and rank arguments are classical. No literature-priority claim +is made for them. The new claim is the specified height-one optimum and +its twelve-matrix attaining configuration. diff --git a/research/height-one-shear-bicliques/README.md b/research/height-one-shear-bicliques/README.md new file mode 100644 index 0000000000..a54e81528b --- /dev/null +++ b/research/height-one-shear-bicliques/README.md @@ -0,0 +1,108 @@ +# Height-one integral shear bicliques have exact balanced optimum six + +The largest balanced rank-distance biclique among the 81 two-by-two integer +matrices with entries in {-1,0,1} is exactly **K_(6,6)**. Distinct matrices +within each part have rank-two difference; every cross-part difference has +rank one. The twelve associated integral four-by-four shear frames commute. + +Claim type: **exact finite certificate**, with a written construction and +a proof reducing the ceiling to a complete finite enumeration. +This contribution was produced by Nick Petalas. No new kappa is claimed. + +## Construction and ceiling + +For the six integer solutions used here of `a^2+ab+b^2=1`, take + +```text +E(a,b) = [[a,b],[-a-b,a]], O(a,b) = [[a,b],[b,-a-b]]. +``` + +Their determinant identities prove attainment. For the ceiling, every +pairwise rank-two triple in the complete 81-matrix inventory has at most +six common rank-one contacts. Thus a K_(7,7) is impossible. Two separate +enumerations agree on all 23,488 admissible triples and their complete +contact-count histogram. [PROOF.md](PROOF.md) gives the identities, histogram +and coverage arguments. + +Nick Petalas / petalas [#6174](https://github.com/CrocSwap/integer-mult-bounds/pull/6174) +asks how coefficient height limits integral bicliques. Its all-size construction +gives a quadratic-height upper bound and no exact height-one ceiling. +This settles that first bounded inventory. Jerry Chen / CubeJerry +[#907](https://github.com/CrocSwap/integer-mult-bounds/pull/907) supplies the +earlier eight-frame example and the abstract distortion formula +`c_1(K_(r,r))=2(r-1)/r`. Applying that cited theorem gives distortion 5/3 +for this new twelve-frame configuration; its cut proof is not replayed here. +The rational shear model originates in eumemic +[#288](https://github.com/CrocSwap/integer-mult-bounds/pull/288). +The separate common-flag and signed-rank obstructions of navinor #825 and +Jeremy Diviney #836 remain relevant. All predecessor attribution is retained +in the unchanged source packages. Apache-2.0. + +Base main is `e54523517d0f03e58352e647c403a5af3e525a57`. The full original +`complex-rank-shape-decoder` card is pinned in TASK.json. Its scope changes +to a coefficient-inventory side result. Rank geometry and distortion alone +do not supply a decoder, productive credit or a favorable complete invoice. +The contextual picker reports its historical #5599 assessment differs from +the selected #7000 record. Selected kappa `363005817/100000000000` is unchanged. +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19572817) +reserves this exact height-one question. + +## Reproduce + +From the repository root, with CPython 3.12 and only its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/height-one-shear-bicliques/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/height-one-shear-bicliques/ceiling.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/height-one-shear-bicliques +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/height-one-shear-bicliques --check-source-history --check-modes +``` + +A CPython 3.12 executable at another path can replace the local interpreter. +VERIFY.json registers warning-strict normal and optimized runs of both +verifiers, each with a 60-second timeout. Both commands are read-only and +work without Git or predecessor files. The source pins are provenance only. +No predecessor scientific executable is imported or replayed. + +The expected direct markers are `PASS_HEIGHT_ONE_SHEAR_BICLIQUES` and +`PASS_FIRST_ROW_SHEAR_CEILING`. The primary JSON receipt includes the complete +witness, histogram, ordered triple-trace hash and SHA256 of all seven package +files. It is generated on every run. The separate checker uses Fraction +elimination, a first-row enumeration and the actual four-by-four shear ranks. +Ten rejection controls and five elimination fixtures test the stated boundary. + +## Limits + +Only the height-one integral two-by-two inventory is optimized. There is no +physical native implementation, complete caller, dirty restoration, paid +supplier invoice, compiler closure, tape/precision realization, complete +multiplication theorem or discharge of any selected framework assumption. +No selected cold replay, Lean or Docker run is relevant to this certificate. +Independent human and formal proof-kernel review are unclaimed. + +## Open next questions + +1. What is the balanced optimum at height two? Start by reducing the contact + equations for its 625 matrices; a larger exact enumeration or a general + coefficient-height theorem is missing. +2. Can these twelve frames participate in a favorable completed interface? + First specify legal gates, targets, arbitrary dirty inputs and paid cleanup, + and identify a hypothesis escaping the common-flag obstruction. None is + supplied here; the metric example alone does not imply a coding gain. + +## Verification-code bounds + +Both scripts use bounded loops and no recursion or subprocesses. The primary +stores two 81-entry bitset graphs; the other stores an 81-by-81 rank table. +No triple list is retained. Every function is below sixty physical lines. +Errors propagate as exceptions, and checks do not depend on assertions. + +Power-of-Ten rule 3 has a managed-runtime deviation in both scripts. Python +and Fraction allocate during enumeration. Input domains are fixed to 81 +four-entry integer matrices, matrices of order at most four for elimination, +85,320 primary triple visits and 61,236 secondary candidates. Only the fixed +graphs, one matrix/triple at a time and a histogram of at most 82 bins remain +live. Normal and optimized replays verify those enforced domains. A port to +fixed-capacity arithmetic would be needed for allocation-free execution. +Python's dynamic dispatch is a runtime constraint; all scientific calls have +fixed, direct targets and no callbacks, plugins or dynamic evaluation. diff --git a/research/height-one-shear-bicliques/SOURCES.json b/research/height-one-shear-bicliques/SOURCES.json new file mode 100644 index 0000000000..c78fc55833 --- /dev/null +++ b/research/height-one-shear-bicliques/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/abelian-cayley-metric-scope/README.md", + "usage": "provenance", + "git_blob": "bb598f97cadc32f5da271a1f2da6bb2dc17c469c", + "sha256": "4e74affa1e0239b84da1c8fef25b88aabef8a655047854e04d14d35c981dfac2" + }, + { + "path": "research/unbounded-shear-bicliques/README.md", + "usage": "provenance", + "git_blob": "6fd50ccfce6ab1ec54ed29685fb57d81639886e0", + "sha256": "ca992f0f87ab78f2572566c202ff25b59aee30fcf528ffba28631a83ff5f861d" + } + ] +} diff --git a/research/height-one-shear-bicliques/TASK.json b/research/height-one-shear-bicliques/TASK.json new file mode 100644 index 0000000000..4d8f1e30df --- /dev/null +++ b/research/height-one-shear-bicliques/TASK.json @@ -0,0 +1,89 @@ +{ + "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": "Determine the exact largest balanced rank-distance biclique in the height-one integral two-by-two matrix inventory.", + "scope_change_reason": "This answers the first coefficient-height case of PR6174 Open next question 2. It is a frame-alphabet side result, not a decoder or complete signed-moment improvement.", + "bottleneck_link": "A changed frame alphabet must have explicit coefficient and rank costs. This settles its smallest nontrivial bounded inventory; non-L1 geometry alone does not escape the common-flag obstruction or earn productive credit.", + "budget_minutes": 60, + "stop_rule": "Stop at the first exact height-one optimum with an attaining configuration and independent finite ceiling; leave larger heights and physical realization open.", + "outcome": "completed", + "evidence": "PROOF.md gives the six-by-six construction and finite ceiling reduction. verify.py enumerates every matrix triple; ceiling.py separately uses rational elimination and first-row buckets.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the balanced optimum at coefficient height two?", + "why_it_matters": "The height-one ceiling does not quantify how the inventory grows with coefficient storage.", + "first_step": "Use rank-one contact equations to reduce the 625-matrix inventory before a bounded exact search.", + "blocked_by": "No larger-height enumeration or general height theorem is supplied." + }, + { + "question": "Can the twelve-frame configuration participate in a favorable completed interface?", + "why_it_matters": "The charged metric and its distortion do not imply a coding or multiplication gain.", + "first_step": "Specify legal gates, target jobs, arbitrary dirty inputs and all cleanup costs, identifying a hypothesis outside the existing common-flag obstruction.", + "blocked_by": "No physical caller, native realization or complete supplier invoice is supplied." + } + ], + "environment": { + "python": "3.12.15", + "implementation": "CPython", + "system": "Darwin", + "release": "27.0.0", + "machine": "arm64", + "dependencies": "standard library only" + } +} diff --git a/research/height-one-shear-bicliques/VERIFY.json b/research/height-one-shear-bicliques/VERIFY.json new file mode 100644 index 0000000000..f75062f705 --- /dev/null +++ b/research/height-one-shear-bicliques/VERIFY.json @@ -0,0 +1,59 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Complete determinant rank graph, all triples, attaining witness and ten rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Complete determinant rank graph, all triples, attaining witness and ten rejection controls. Assertions disabled." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/ceiling.py" + ], + "timeout_seconds": 60, + "checks": "Separate rational-elimination rank table, complete first-row triple enumeration, actual shear ranks and elimination controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/ceiling.py" + ], + "timeout_seconds": 60, + "checks": "Separate rational-elimination rank table, complete first-row triple enumeration, actual shear ranks and elimination controls. Assertions disabled." + } + ] +} diff --git a/research/height-one-shear-bicliques/ceiling.py b/research/height-one-shear-bicliques/ceiling.py new file mode 100644 index 0000000000..ae100b5444 --- /dev/null +++ b/research/height-one-shear-bicliques/ceiling.py @@ -0,0 +1,118 @@ +"""Separate rational-elimination and first-row enumeration. Apache-2.0.""" + +from collections import Counter +from fractions import Fraction +from hashlib import sha256 +from itertools import combinations, product +import json +from pathlib import Path +import sys + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def rank(rows: list) -> int: + size = len(rows) + require(size in (2, 4) and all(len(row) == size for row in rows), + "only square matrices of order two or four are supported") + matrix = [[Fraction(x) for x in row] for row in rows] + pivot_row = 0 + for col in range(size): + candidates = [r for r in range(pivot_row, size) if matrix[r][col]] + if not candidates: + continue + chosen = candidates[0] + matrix[pivot_row], matrix[chosen] = matrix[chosen], matrix[pivot_row] + scale = matrix[pivot_row][col] + matrix[pivot_row] = [x / scale for x in matrix[pivot_row]] + for r in range(pivot_row + 1, size): + factor = matrix[r][col] + matrix[r] = [x - factor * y + for x, y in zip(matrix[r], matrix[pivot_row])] + pivot_row += 1 + return pivot_row + + +def rank_table(matrices: tuple) -> list: + table = [[0] * 81 for _ in range(81)] + for i, a in enumerate(matrices): + for j, b in enumerate(matrices): + delta = [x - y for x, y in zip(a, b)] + table[i][j] = rank([delta[:2], delta[2:]]) + return table + + +def first_row_ceiling(table: list) -> tuple: + histogram = Counter() + inspected = 0 + for first_rows in combinations(range(9), 3): + for second_rows in product(range(9), repeat=3): + a, b, c = tuple(9 * u + v for u, v in zip(first_rows, second_rows)) + inspected += 1 + if table[a][b] == table[a][c] == table[b][c] == 2: + common = sum(table[a][j] == table[b][j] == table[c][j] == 1 + for j in range(81)) + require(common <= 6, "seven common contacts found") + histogram[common] += 1 + require(inspected == 61236, "first-row enumeration is incomplete") + return dict(sorted(histogram.items())), inspected + + +def shear(matrix: tuple) -> list: + a, b, c, d = matrix + return [[1, 0, a, b], [0, 1, c, d], [0, 0, 1, 0], [0, 0, 0, 1]] + + +def check_attainment() -> int: + roots = ((-1, 0), (-1, 1), (0, -1), (0, 1), (1, -1), (1, 0)) + left = tuple((a, b, -a - b, a) for a, b in roots) + right = tuple((a, b, b, -a - b) for a, b in roots) + pairs = 0 + for side_a, side_b in product(range(2), repeat=2): + for i, j in product(range(6), repeat=2): + a, b = (left, right)[side_a][i], (left, right)[side_b][j] + sa, sb = shear(a), shear(b) + delta = [[x - y for x, y in zip(row_a, row_b)] + for row_a, row_b in zip(sa, sb)] + expected = 1 if side_a != side_b else (0 if i == j else 2) + require(rank(delta) == expected, "shear witness rank differs") + pairs += 1 + return pairs + + +def rank_controls() -> int: + controls = ( + ([[0, 0], [0, 0]], 0), + ([[1, 2], [2, 4]], 1), + ([[0, 1], [1, 0]], 2), + ([[1, 1], [1, 2]], 2), + ([[Fraction(1, 2), 1], [1, 2]], 1), + ) + for matrix, expected in controls: + require(rank(matrix) == expected, "elimination control failed") + return len(controls) + + +def main() -> None: + require(len(sys.argv) == 1, "this verifier accepts no arguments") + matrices = tuple(product((-1, 0, 1), repeat=4)) + histogram, inspected = first_row_ceiling(rank_table(matrices)) + require(sum(histogram.values()) == 23488, "rank-two triple census differs") + root = Path(__file__).resolve().parent + print(json.dumps({ + "status": "PASS_FIRST_ROW_SHEAR_CEILING", + "balanced_optimum": 6, + "first_row_candidates": inspected, + "rank_two_triples": sum(histogram.values()), + "common_rank_one_histogram": histogram, + "ordered_shear_pairs": check_attainment(), + "elimination_controls": rank_controls(), + "source_sha256": sha256((root / "ceiling.py").read_bytes()).hexdigest(), + }, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/height-one-shear-bicliques/verify.py b/research/height-one-shear-bicliques/verify.py new file mode 100644 index 0000000000..6b6090faa0 --- /dev/null +++ b/research/height-one-shear-bicliques/verify.py @@ -0,0 +1,137 @@ +"""Exact height-one construction and complete rank-graph ceiling. Apache-2.0.""" + +from collections import Counter +from hashlib import sha256 +from itertools import combinations, product +import json +from pathlib import Path +import sys + + +ROOTS = ((-1, 0), (-1, 1), (0, -1), (0, 1), (1, -1), (1, 0)) +FILES = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", + "verify.py", "ceiling.py") +EXPECTED = {0: 1480, 1: 4368, 2: 9624, 3: 5760, 4: 2096, 6: 160} + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def difference_rank(left: tuple, right: tuple) -> int: + a, b, c, d = (x - y for x, y in zip(left, right)) + return 2 if a * d != b * c else int(any((a, b, c, d))) + + +def witness() -> tuple: + even = tuple((a, b, -a - b, a) for a, b in ROOTS) + odd = tuple((a, b, b, -a - b) for a, b in ROOTS) + return even, odd + + +def validate_witness(parts: tuple) -> None: + require(len(parts) == 2, "two parts required") + for part in parts: + require(len(part) == 6, "each part must contain six matrices") + for matrix in part: + require(len(matrix) == 4, "matrix must have four entries") + require(all(type(x) is int and -1 <= x <= 1 for x in matrix), + "entries must be height-one integers") + for a, b in combinations(part, 2): + require(difference_rank(a, b) == 2, "within-part rank must be two") + for a, b in product(*parts): + require(difference_rank(a, b) == 1, "cross-part rank must be one") + + +def rank_graph(matrices: tuple) -> tuple: + require(matrices == tuple(product((-1, 0, 1), repeat=4)), + "complete lexicographic height-one inventory required") + near, far = [0] * 81, [0] * 81 + for i, a in enumerate(matrices): + for j, b in enumerate(matrices): + rank = difference_rank(a, b) + if rank == 1: + near[i] |= 1 << j + elif rank == 2: + far[i] |= 1 << j + return near, far + + +def triple_ceiling(near: list, far: list) -> tuple: + histogram = Counter() + digest = sha256() + candidates = 0 + for a, b, c in combinations(range(81), 3): + candidates += 1 + if (far[a] >> b & 1) and (far[a] >> c & 1) and (far[b] >> c & 1): + common = near[a] & near[b] & near[c] + count = common.bit_count() + require(count <= 6, "rank-two triple has more than six contacts") + histogram[count] += 1 + digest.update(f"{a},{b},{c}:{common:x}\n".encode("ascii")) + require(dict(histogram) == EXPECTED, "complete triple histogram differs") + require(candidates == 85320, "complete triple inventory differs") + return dict(sorted(histogram.items())), digest.hexdigest(), candidates + + +def rejection_controls() -> list: + even, odd = witness() + cases = ( + ("missing_matrix", (even[:-1], odd)), + ("duplicate_matrix", (even[:-1] + even[:1], odd)), + ("wrong_height", (((2, 0, 1, -1),) + even[1:], odd)), + ("boolean_entry", (((True, 0, 1, -1),) + even[1:], odd)), + ("noninteger_entry", (((-1.0, 0, 1, -1),) + even[1:], odd)), + ("wrong_shape", (((-1, 0, 1),) + even[1:], odd)), + ("overlapping_parts", (even, even)), + ("rank_one_inside", (((0, 0, 1, -1),) + even[1:], odd)), + ) + passed = [] + for name, bad in cases: + try: + validate_witness(bad) + except ValueError: + passed.append(name) + else: + raise ValueError(f"control accepted: {name}") + domain = tuple(product((-1, 0, 1), repeat=4)) + for name, bad in (("missing_vertex", domain[:-1]), + ("repeated_vertex", domain[:-1] + domain[:1])): + try: + rank_graph(bad) + except ValueError: + passed.append(name) + else: + raise ValueError(f"control accepted: {name}") + return passed + + +def main() -> None: + require(len(sys.argv) == 1, "this verifier accepts no arguments") + matrices = tuple(product((-1, 0, 1), repeat=4)) + parts = witness() + validate_witness(parts) + near, far = rank_graph(matrices) + histogram, digest, candidates = triple_ceiling(near, far) + root = Path(__file__).resolve().parent + result = { + "status": "PASS_HEIGHT_ONE_SHEAR_BICLIQUES", + "claim_type": "exact finite certificate", + "balanced_optimum": 6, + "matrices": len(matrices), + "ordered_rank_pairs": len(matrices) ** 2, + "candidate_triples": candidates, + "rank_two_triples": sum(histogram.values()), + "common_rank_one_histogram": histogram, + "triple_trace_sha256": digest, + "witness": parts, + "rejection_controls": rejection_controls(), + "sources_sha256": {name: sha256((root / name).read_bytes()).hexdigest() + for name in FILES}, + } + print(json.dumps(result, sort_keys=True)) + + +if __name__ == "__main__": + main()