diff --git a/research/p112-walsh-gl2-strata/PROOF.md b/research/p112-walsh-gl2-strata/PROOF.md new file mode 100644 index 0000000000..3fdf8192de --- /dev/null +++ b/research/p112-walsh-gl2-strata/PROOF.md @@ -0,0 +1,115 @@ +# Continuous Walsh-plane gauge obstruction + +This is a scoped computer-assisted proof. Its universal step is the support +partition below; its finite geometric statements are exact rank certificates +computed by `verify.py`. It is not formal-kernel or independent human review. + +## Model and theorem + +Use the P112 matrix `X` and nine-bit source labels `p_i` and reader labels `q_i` +from Mihir Srivastava's `p112-single-lift/geometry.py`, following +DreamingOfClouds' PR717 geometry. The 112 rows of X have eight coordinates. +For two real 112-vectors define the support tariff + +``` +beta(d,t) = rank_F2 ((q_i dot p_j)_(d_i != 0, t_j != 0)). +``` + +This is the inherited pairing-rank tariff, not a physical execution invoice. +For `a,b` in F2^3 set `chi_a(b)=(-1)^(a dot b)`, with b in binary order. +Choose any two distinct characters for each ordered pair of columns of the +8-by-2 matrices U and V. For every M in GL2(R), set + +``` +U' = U M, V' = V M^(-T), +D = [X, XU'], T = [X(I - V'U'^T), XV']. +``` + +**Theorem.** Every such ten-term factorization has the pairing-rank profile +`{8:8, 9:2}`. Its total tariff is exactly 82. In particular no rational or +real invertible basis change in these fixed Walsh planes improves PR2042's +finite-domain profile. The exact power tariff is `8*8^s + 2*9^s` for every +real exponent s, since the whole rank multiset is unchanged. + +This extends Cinna Davis's PR2042 family from five matrices to all GL2(R). +It does not decide the arbitrary overlapping rank-two problem posed in +mightyOil's PR1197: U and V must still have the specified Walsh column spaces +and the rank-two product UV^T must stay fixed during the basis change. + +## Algebraic identity + +The inverse transpose gives `U'V'^T = UV^T`. Therefore + +``` +DT^T = X(I - U'V'^T)X^T + XU'V'^T X^T = XX^T. +``` + +The eight original reader columns are the columns of X. Their source columns +are independent of M, since `V'U'^T = VU^T`. The remaining reader columns +are nonzero linear combinations of the two columns of XU; the remaining +source columns are nonzero combinations of the two columns of XV. Invertibility +of M and the full rank of the character pairs ensure nonzero coefficient +vectors on both sides. + +## The complete support partition + +Write u and v for the two columns of XU. For each row i, the vanishing equation +for a combination `z u + w v` is `z*u_i + w*v_i = 0`. If both coefficients +are zero it vanishes for every direction. Otherwise it has exactly one zero +direction in the real projective line. The verifier enumerates these directions +as primitive integer pairs `(v_i,-u_i)`, with a fixed overall sign. + +For each of the 56 ordered character pairs, the entire set of zero directions +is exactly + +``` +(1,0), (0,1), (1,1), (1,-1). +``` + +Each exceptional point has its own support. At every other real projective +point the support is exactly `supp(u) union supp(v)`. Thus the four points +and the generic representative `(1,2)` are exhaustive, including irrational +slopes. They are not a bounded coefficient search. The same statement applies +to the V planes. There is no assumption that the four entries of M have small +height or that its determinant is a unit. + +## Finite certificates + +The standalone verifier imports only the exact pinned geometry constructor. +It uses a separate nine-bit elimination routine with nine explicitly bounded +pivot steps per input row. It checks: + +1. For each of the eight coordinate reader supports, the span of q_i has + dimension 8. +2. For every ordered character pair and each of its five support strata, + both the p_i span and q_i span on that support have dimension 9. This is + 280 support certificates, each with both ranks checked. +3. For all 56 choices of U and 56 choices of V, each of the eight corrected + source columns `X_j - U_(j,0)*(XV)_0 - U_(j,1)*(XV)_1` has p_i span of + dimension 9. This is 25,088 corrected-source certificates. + +All rows and labels are reconstructed from the pinned constructor. The support +receipt is hashed in deterministic order and printed with hashes of package +files. No stored predecessor rank receipt is consumed. + +The standard binary dot product is nondegenerate. If the source labels span +all F2^9, the restricted pairing has rank equal to the dimension of the +reader-label span. Statement 1 and statement 3 therefore give rank 8 to +each original term. Statement 2 gives rank 9 to each added term, for every +nonzero real coefficient direction on either side. This proves the theorem. + +The checker also verifies literal 112-by-112 factor identities for a +determinant-minus-two gauge and a determinant-one gauge. These are corroborating +endpoint fixtures, not the justification of the infinite quantifier. A +singular gauge and a dropped added term are rejected. A wrong inverse is +separated from the required inverse transpose. + +## Scope and cost boundary + +The result rules out further basis searches while these Walsh planes and their +fixed product are retained. It gives no exclusion for different planes, +simultaneous mixing with the original eight channels, changed geometry, +masked endpoints, or a different tariff. It does not supply preparation, +source access, frame transport, dirty restoration, hosting, native operations, +precision, stock, a recursive compiler, or a complete multiplication theorem. +No historical packing ceiling is transferred to the selected P104 supplier. diff --git a/research/p112-walsh-gl2-strata/README.md b/research/p112-walsh-gl2-strata/README.md new file mode 100644 index 0000000000..c4d2e8812a --- /dev/null +++ b/research/p112-walsh-gl2-strata/README.md @@ -0,0 +1,85 @@ +# Every continuous Walsh two-total basis gauge still costs 82 + +Scoped computer-assisted proof, produced by Nick Petalas. Apache-2.0. + +For all 3,136 ordered choices of two distinct Walsh characters on each side +of Cinna Davis's PR2042 P112 ten-term factorization, every invertible real +or rational 2-by-2 basis change `U -> UM, V -> VM^(-T)` has exactly the +pairing-rank profile `{8:8,9:2}` and total tariff 82. The power tariff is +therefore always `8*8^s + 2*9^s`. This replaces a finite five-basis search +with an exact classification of the entire continuous basis orbit. + +The new proof is in [PROOF.md](PROOF.md). Every Walsh plane has exactly four +projective support-zero directions; all other real directions share one +support. The verifier checks both label spans on all 280 plane/support cases, +the eight original reader spans, and all 25,088 corrected source-column spans. +The nondegenerate binary pairing then gives every term's exact rank. No +predecessor rank receipt or verifier is replayed as evidence for this result. + +This is a decoder side result, with no new kappa or selected-frontier change. +It shows that further basis searches in these fixed Walsh planes cannot lower +their invoice. Arbitrary changed planes, changed rank-two products and physical +supplier realization remain open. The historical P112 packing ceiling is not +an applicable ceiling on the current selected P104 construction. + +## Reproduction + +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/p112-walsh-gl2-strata/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/p112-walsh-gl2-strata/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p112-walsh-gl2-strata +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p112-walsh-gl2-strata --check-source-history +``` + +Other machines can substitute their CPython 3.12 executable. The verifier prints +`PASS_P112_WALSH_GL2_STRATA` in JSON with the complete certificate counts, +support digest and package hashes. It writes no files. Both registered checks +have a 120-second limit. `SOURCES.json` pins the sole executable external input, +Mihir Srivastava's exact P112 geometry constructor, to canonical main +`721c03822c421b7f7fcbb2598993b947c4d88419`. Source hashes are checked before import. + +Finite fixtures also check complete 112-by-112 identities under determinant +minus two and determinant one. Singular gauges, a missing total, empty support, +a missing label direction and the wrong inverse are rejected or separated by +explicit controls. The universal claim rests on the written support partition +and complete finite rank certificate, rather than these sample matrices. + +## Relation to prior work + +- Cinna Davis, [PR2042](https://github.com/CrocSwap/integer-mult-bounds/pull/2042), + supplies the asymmetric Walsh family and its finite five-basis result. + This package extends the basis domain to all GL2(R). +- DreamingOfClouds, PR717, and Mihir Srivastava, PR845 and + `p112-single-lift/geometry.py`, supply the P112 coordinates and pairing tariff. +- Philipp / mightyOil, PR1197, poses the general coupled overlapping-lift case. + This result closes only the specified Walsh-plane basis orbit. +- Gonzalo Mier, [PR4020](https://github.com/CrocSwap/integer-mult-bounds/pull/4020), + uses projective support strata for arbitrary rational pair gauges on a + different 34-channel factorization. The support-stratum method is credited; + this package's new result concerns the two-added-total Walsh family. +- DreamingOfClouds, PR2338, establishes broader baseline decoder floors under + its stated format. A floor of 64 does not determine the exact value 82 here. + +The source files and predecessor credit remain unchanged. No claim of a new +support-stratification method or independent human review is made. + +## Limitations and next decision + +Source preparation, adapters, frame transport, dirty restoration, native +execution, hosting, precision, stock, uniform compilation and outer recovery +are unpriced. No full supplier replay, Lean proof or Docker run is claimed. +The result is a scoped exact exclusion, not a search failure or a complete +integer multiplication theorem. Python uses managed allocations, bounded here +by 112 geometry rows, 56 plane records, nine-bit rank workspaces and a fixed +25,088-case loop. No unbounded search, recursion or external solver is used. + +## Open next questions + +Can changing the rational planes and their product `UV^T`, rather than only +their bases, lower the profile? Start with one explicitly different overlapping +plane pair and its complete support arrangement. This matters because the +arbitrary rank-two branch of PR1197 remains open. A favorable example and +its physical source/frame/restoration bill are still missing. The structured +question is retained in `TASK.json`; this package stops at the classification. diff --git a/research/p112-walsh-gl2-strata/SOURCES.json b/research/p112-walsh-gl2-strata/SOURCES.json new file mode 100644 index 0000000000..6fbcb864b7 --- /dev/null +++ b/research/p112-walsh-gl2-strata/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/p112-single-lift/geometry.py", + "usage": "input", + "git_blob": "34c1abf059d7be5fe5e5044cf01a09b843071c68", + "sha256": "3857c11ec731a602b8059d85d58fbb3b641bab687bb33016a0e54f7567752c8a" + }, + { + "path": "research/p112-walsh-two-total-seed6ed83d/README.md", + "usage": "provenance", + "git_blob": "97193e7f6fe31fd3b96d1ff543ea12a3352de9ca", + "sha256": "ffcfee6e621118d244326023589589b01440648f077e07ee793ee7738630e458" + } + ] +} diff --git a/research/p112-walsh-gl2-strata/TASK.json b/research/p112-walsh-gl2-strata/TASK.json new file mode 100644 index 0000000000..5fff619969 --- /dev/null +++ b/research/p112-walsh-gl2-strata/TASK.json @@ -0,0 +1,87 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "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": "Classify every real or rational GL2 basis change on every ordered pair of the PR2042 Walsh lift planes.", + "scope_change_reason": "Replace the current supplier-itinerary experiment with the explicitly open continuous coupled-lift side question in PR2042. This is an infinite-domain extension, not a replay or audit of its finite census.", + "bottleneck_link": "Scoped decoder exclusion: changing bases inside these Walsh planes cannot lower their pairing-rank invoice. A useful replacement must change the planes, their product, or the channel family. This does not claim a selected P104 improvement.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified complete support classification; do not search changed planes or optimize downstream bills.", + "outcome": "negative-result", + "evidence": "PROOF.md and exact support certificate computed by verify.py; no predecessor result receipt is read.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a changed rational two-plane product UV^T, outside the paired Walsh family, improve the ten-term pairing-rank profile?", + "why_it_matters": "The present obstruction fixes the product; the general overlapping rank-two branch of PR1197 stays open.", + "first_step": "Enumerate exact support-zero strata for one explicitly different rational plane pair and price all ten terms.", + "blocked_by": "A favorable example and complete physical source/frame/restoration costs are not supplied." + } + ], + "source_question": { + "pr": 2042, + "author": "1337isnot1337", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19246923" + }, + "environment": { + "python": "3.12.15", + "implementation": "CPython", + "platform": "Darwin", + "machine": "arm64" + }, + "claim_type": "scoped computer-assisted proof" +} diff --git a/research/p112-walsh-gl2-strata/VERIFY.json b/research/p112-walsh-gl2-strata/VERIFY.json new file mode 100644 index 0000000000..64585825bd --- /dev/null +++ b/research/p112-walsh-gl2-strata/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p112-single-lift/geometry.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete real-projective support strata, exact binary ranks, literal endpoints and rejecting controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same complete certificate with assertions disabled." + } + ] +} diff --git a/research/p112-walsh-gl2-strata/verify.py b/research/p112-walsh-gl2-strata/verify.py new file mode 100644 index 0000000000..fbb4bec5bf --- /dev/null +++ b/research/p112-walsh-gl2-strata/verify.py @@ -0,0 +1,207 @@ +#!/usr/bin/env python3 +"""Certify the continuous P112 Walsh-plane gauge obstruction. Apache-2.0.""" +from fractions import Fraction +from hashlib import sha256 +from itertools import permutations +from pathlib import Path +import importlib.util +import json +import math +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +DIRECTIONS = ((1, 0), (0, 1), (1, 1), (1, -1), (1, 2)) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def rank(rows): + """Nine-column elimination, with a bound independent of pivot values.""" + pivots = [0] * 9 + for value in rows: + need(0 <= value < 512, 'nine-bit rank row') + for bit in range(8, -1, -1): + if value >> bit & 1: + if pivots[bit]: + value ^= pivots[bit] + else: + pivots[bit] = value + break + return sum(bool(value) for value in pivots) + + +def pinned_geometry(): + sources = json.loads((HERE / 'SOURCES.json').read_text(encoding='utf-8')) + for row in sources['files']: + if row['usage'] == 'input': + need(sha256((ROOT / row['path']).read_bytes()).hexdigest() == row['sha256'], + 'source hash: ' + row['path']) + path = ROOT / 'research/p112-single-lift/geometry.py' + spec = importlib.util.spec_from_file_location('walsh_strata_geometry', path) + need(spec is not None and spec.loader is not None, 'geometry loader') + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + data = module.build() + need(len(data['X']) == len(data['labels']) == len(data['duals']) == 112, + 'P112 geometry dimensions') + need(all(len(row) == 8 for row in data['X']), 'eight frame coordinates') + return data + + +def normalize(a, b): + divisor = math.gcd(a, b) + need(divisor > 0, 'nonzero projective direction') + a, b = a // divisor, b // divisor + return (-a, -b) if a < 0 or (a == 0 and b < 0) else (a, b) + + +def mask(values): + return sum(1 << i for i, value in enumerate(values) if value) + + +def support_ranks(bits, data): + return tuple(rank(values[i] for i in range(112) if bits >> i & 1) + for values in (data['labels'], data['duals'])) + + +def lifts_and_strata(data, characters, pairs, digest): + lifts = {} + masks = 0 + for pair in pairs: + vectors = tuple(tuple(sum(row[j] * characters[a][j] for j in range(8)) + for row in data['X']) for a in pair) + exceptional = {normalize(b, -a) for a, b in zip(*vectors) if a or b} + need(exceptional == set(DIRECTIONS[:4]), 'complete support-zero directions') + generic = mask(a or b for a, b in zip(*vectors)) + for direction in DIRECTIONS: + a, b = direction + bits = mask(a * x + b * y for x, y in zip(*vectors)) + need(support_ranks(bits, data) == (9, 9), 'full lift support spans') + if direction == DIRECTIONS[-1]: + need(bits == generic, 'generic support is the support union') + digest.update(f'{pair}:{direction}:{bits:x}\n'.encode('ascii')) + masks += 1 + lifts[pair] = vectors + return lifts, masks + + +def corrected_columns(data, characters, pairs, lifts, digest): + checks = 0 + for up in pairs: + for vp in pairs: + v0, v1 = lifts[vp] + for j in range(8): + values = tuple(data['X'][i][j] - characters[up[0]][j] * v0[i] + - characters[up[1]][j] * v1[i] for i in range(112)) + bits = mask(values) + need(support_ranks(bits, data)[0] == 9, 'corrected source span') + digest.update(f'{up}:{vp}:{j}:{bits:x}\n'.encode('ascii')) + checks += 1 + return checks + + +def factor_identity(characters, up, vp, matrix, data): + """Check the literal ten-term 112-by-112 identity at one rational gauge.""" + a, b, c, d = map(Fraction, matrix) + det = a * d - b * c + need(bool(det), 'invertible gauge') + u0, u1 = (characters[k] for k in up) + v0, v1 = (characters[k] for k in vp) + us = (tuple(a*x+c*y for x, y in zip(u0, u1)), + tuple(b*x+d*y for x, y in zip(u0, u1))) + vs = (tuple((d*x-b*y)/det for x, y in zip(v0, v1)), + tuple((-c*x+a*y)/det for x, y in zip(v0, v1))) + for i in range(8): + for j in range(8): + need(sum(u[i]*v[j] for u, v in zip(us, vs)) == + u0[i]*v0[j]+u1[i]*v1[j], 'inverse-transpose product') + x = data['X'] + ul = [tuple(sum(row[k]*u[k] for k in range(8)) for row in x) for u in us] + vl = [tuple(sum(row[k]*v[k] for k in range(8)) for row in x) for v in vs] + dc = [tuple(row[j] for row in x) for j in range(8)] + ul + tc = [tuple(x[i][j]-sum(us[k][j]*vl[k][i] for k in range(2)) + for i in range(112)) for j in range(8)] + vl + check_endpoint(dc, tc, data) + return dc, tc + + +def check_endpoint(dc, tc, data): + need(len(dc) == len(tc) == 10, 'ten factor columns') + x = data['X'] + for i in range(112): + for j in range(112): + need(sum(left[i]*right[j] for left, right in zip(dc, tc)) == + sum(x[i][k]*x[j][k] for k in range(8)), 'literal factor endpoint') + + +def controls(data, characters): + rejected = 0 + for invalid in ((0, 0),): + try: + normalize(*invalid) + except ValueError: + rejected += 1 + else: + raise ValueError('zero-direction control accepted') + try: + factor_identity(characters, (0, 1), (2, 3), (1, 2, 2, 4), data) + except ValueError as error: + need(str(error) == 'invertible gauge', 'singular rejection reason') + rejected += 1 + else: + raise ValueError('singular gauge accepted') + need(support_ranks(0, data) == (0, 0), 'empty support is not full span') + need(rank([1 << i for i in range(8)]) == 8, 'missing-axis control') + # A wrong inverse uses M^{-1}, rather than M^{-T}, on the second lift. + a, b, c, d = 1, 2, 3, 7 + need(a*d-b*c == 1, 'wrong-inverse fixture is nonsingular') + wrong = ((a*d-b*b, -a*c+a*b), (c*d-d*b, -c*c+d*a)) + need(wrong != ((1, 0), (0, 1)), 'wrong inverse differs from endpoint') + dc, tc = factor_identity(characters, (0, 1), (2, 3), (1, 2, 3, 7), data) + tc[-1] = (0,) * 112 + try: + check_endpoint(dc, tc, data) + except ValueError as error: + need(str(error) == 'literal factor endpoint', 'dropped-total rejection reason') + rejected += 1 + else: + raise ValueError('dropped total accepted') + return rejected + 3 + + +def compute(): + data = pinned_geometry() + characters = tuple(tuple(1 - 2*((a & b).bit_count() % 2) for b in range(8)) + for a in range(8)) + pairs = tuple(permutations(range(8), 2)) + digest = sha256() + coordinate_ranks = tuple(support_ranks(mask(row[j] for row in data['X']), data)[1] + for j in range(8)) + need(coordinate_ranks == (8,) * 8, 'coordinate reader ranks') + lifts, masks = lifts_and_strata(data, characters, pairs, digest) + columns = corrected_columns(data, characters, pairs, lifts, digest) + for matrix in ((1, 1, 1, -1), (1, 2, 3, 7)): + factor_identity(characters, (0, 1), (2, 3), matrix, data) + rejected = controls(data, characters) + need(masks == 280 and columns == 25088, 'complete finite certificate coverage') + files = {p.name: sha256(p.read_bytes()).hexdigest() + for p in sorted(HERE.iterdir()) if p.is_file()} + return {'status': 'PASS_P112_WALSH_GL2_STRATA', 'claim_type': 'scoped proof', + 'coefficient_fields': ['real', 'rational'], 'ordered_plane_pairs': 3136, + 'lift_support_certificates': masks, 'corrected_source_certificates': columns, + 'coordinate_reader_certificates': 8, 'literal_endpoint_entries': 37632, + 'controls': rejected, 'support_certificate_sha256': digest.hexdigest(), + 'profile': {'8': 8, '9': 2}, 'invoice': 82, 'package_sha256': files} + + +def main(): + need(len(sys.argv) == 1, 'usage: verify.py') + print(json.dumps(compute(), sort_keys=True, indent=2)) + + +if __name__ == '__main__': + main()