diff --git a/research/four-plane-integral-shadow/README.md b/research/four-plane-integral-shadow/README.md new file mode 100644 index 0000000000..d38fc86051 --- /dev/null +++ b/research/four-plane-integral-shadow/README.md @@ -0,0 +1,233 @@ +# One open four-plane class has exact COPY mass sixteen + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Scoped proof with a finite exact certificate.** For the four matched planes +`(0,1,44,49)` in the pinned PR1825 ordering, every finite scalar rank-one +factorization of `I_8` has additive full-plane COPY mass at least **16**, over +**every coefficient field**. Eight coordinate messages attain sixteen. + +This settles one concrete quadruple marked uncertified in Ryanson Jonathan's +[PR4454](https://github.com/CrocSwap/integer-mult-bounds/pull/4454). +The new artifact is an integral pairing-matrix witness and its rank proof. +No predecessor census or certificate replay is a deliverable here. The +other quadruples and tariff classes are not classified. + +## Exact object and tariff + +The planes have ordered port pairs `(0,1),(2,3),(63,66),(72,75)` and ordered +binary labels + +```text +11 19 | 35 67 | 296 392 | 400 416 +``` + +Write `p(i)=floor(i/2)` for the plane of scalar coordinate `i`, with +`0<=i<8`. The integer zero-one matrix `G` is obtained by taking the binary +dot products of these labels and then interpreting the resulting bits as +integers: + +```text +1 0 0 0 1 1 0 0 +0 1 0 0 0 0 1 0 +0 0 1 0 1 0 0 1 +0 0 0 1 0 0 0 0 +1 0 1 0 1 0 1 0 +1 0 0 0 0 1 0 0 +0 1 0 0 1 0 1 0 +0 0 1 0 0 0 0 1 +``` + +Every diagonal plane block is `I_2`. For nonempty subsets `S,T` of the four +planes, let `G[S,T]` contain their complete two-coordinate blocks and put +`t(S,T)=rank_F2 G[S,T]`. This is CubeJerry's PR4365 tariff, retained by +PR4454. Coefficient-field rank and binary tariff rank are different notions. + +For vectors `u,v` in `K^8`, let `S(u)` contain every plane with at least one +nonzero coordinate of `u`, and similarly define `T(v)`. The charge of a +nonzero scalar message `u v^T` is `t(S(u),T(v))`. Zero messages may be +omitted. Charges add. The endpoint is exactly + +```text +sum_j u_j v_j^T = I_8. +``` + +There is no bound on the finite term count, and cancellation is permitted. +This fixes the identity endpoint; it does not assert a result for every +strict scalar fitting matrix or for shared native operations. + +## Integral rank certificate + +For all 225 ordered nonempty closure pairs, the finite certificate establishes + +```text +rank_Q G[S,T] = rank_F2 G[S,T] = t(S,T). +``` + +The tariff histogram, indexed by rank zero through six, is +`(2,26,80,40,55,13,9)`. The checker uses rational elimination separately from +binary elimination. More directly, it runs 697 minor checks of order +`t(S,T)+1` and finds each determinant exactly zero in `Z`. These count a +minor again when it belongs to another closure pair. When the order exceeds +a block dimension there is no +minor to check. Vanishing of these integer minors implies + +```text +rank_K G[S,T] <= t(S,T) +``` + +in every field `K`, including characteristics in which the rank drops. +This implication uses integer determinants, not numerical sampling or an +assumption that rational rank is invariant under specialization. + +## Proof of the mass floor + +Partition `G` into two-by-two plane blocks `G_ab`. Define a linear map from +`8 x 8` scalar matrices to `16 x 16` matrices by replacing each entry with +its plane block: + +```text +Phi(M)[(i,a),(j,b)] = M[i,j] G[(2p(i)+a),(2p(j)+b)], +0<=i,j<8, 0<=a,b<2. +``` + +This map is defined over every field by the displayed integer matrix. Since +every `G_aa=I_2`, it sends `I_8` to `I_16`. + +For one message `u v^T`, define `A_u` with rows `(i,a)` and columns `(c,b)` by + +```text +(A_u)[(i,a),(c,b)] = u_i [c=p(i)] [a=b]. +``` + +Then direct entrywise multiplication gives + +```text +Phi(u v^T) = A_u G A_v^T. +``` + +All block columns outside `S(u)` vanish in `A_u`, and all block rows outside +`T(v)` vanish in `A_v^T`. Consequently + +```text +rank_K Phi(u v^T) <= rank_K G[S(u),T(v)] <= t(S(u),T(v)). +``` + +Apply linearity and rank subadditivity to the complete endpoint: + +```text +16 = rank_K I_16 + = rank_K sum_j Phi(u_j v_j^T) + <= sum_j rank_K Phi(u_j v_j^T) + <= sum_j t(S(u_j),T(v_j)). +``` + +This includes arbitrary coefficients and any finite number of cancelling +terms. For attainment, take `u_j=v_j=e_j` for `j=0,...,7`. Every message +uses one plane on both sides and costs `rank I_2=2`. The sum is `I_8`, so +the total is sixteen. This proves the exact optimum. + +The linear-map/rank argument is the established expanded-identity or +Hadamard rank method. Philippe Van Velzen's expanded-identity lineage, +DreamingOfClouds's PR2111 rank-preserving lifting route and Nick Petalas's +PR3505 reader-transfer discussion retain that credit. The new claim is this +explicit integral witness and its all-field consequence for the named open +quadruple, not a new general rank method or a claim of literature priority. + +## Reproduce + +From the repository root, using CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -B -W error research/four-plane-integral-shadow/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -B -W error research/four-plane-integral-shadow/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/four-plane-integral-shadow +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/four-plane-integral-shadow --check-source-history +``` + +Any CPython 3.12 installation can replace the absolute local path. Expected +marker: `PASS_FOUR_PLANE_INTEGRAL_SHADOW`, with `closure_pairs=225`, +`vanishing_integer_minors=697`, `literal_atoms=6400` and `minimum_mass=16`. +Both registered commands run the complete checker with assertions disabled +in the second command. Each has a 60-second limit. + +Besides the rank certificate, the checker constructs all 6,400 literal +rank-one fixtures in which each touched plane contributes one of its two +coordinate vectors on each side. It computes their full `16 x 16` shadows +and checks the rank bound over `F_3`. These fixtures corroborate the map; +the written factorization proves the arbitrary-field atom inequality. +The eight-term coordinate endpoint and a ten-term endpoint with a cancelling +dense pair check attainment and linearity. Six rejecting controls cover an +empty mask, a Boolean mask, an omitted endpoint term, an underpriced self-plane +message, a false rational lift and a missing diagonal normalization. A free +cross-plane atom is a positive control whose ordinary scalar rank is one but +whose shadow is zero. + +The printed receipt is freshly generated from the actual checks. It hashes +all five package files and both ordered result streams. It is not handwritten +or stored as a claimed execution record. Default replay writes no files and +works from a standalone export without Git or network access. + +## Source and scope boundaries + +Canonical base is `ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c`, priority revision 7. +`SOURCES.json` pins the catalogue, selected record, source archive, matching, +PR4454 README and open-index bytes as historical provenance. The archive's +`candidate/strict/global/base/work/complex-nine-native/DATA-PHASES.json` +member has SHA256 +`c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa`. +The matching and that label inventory identify the displayed ports and labels. +In the pinned PR4454 index, zero-based lexicographic combination position +1369 has the two-byte index zero. Only that identification was read; the +predecessor's scientific replay was not run. + +The original card is explicitly changed from a new helper construction to a +scoped obstruction in an existing complete-plane interface. Its historical +first command fails at `KeyError: 'complex_profile'` under the current +selected schema. The current `research_selected_baseline.py` orientation +passes. Neither command supplies evidence for this new theorem. +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19146140) +initially targeted characteristic three. Its +[progress update](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19146177) +records that the same first witness has an integral all-field certificate. +No wider class search followed that witness. + +No physical preparation, coefficient execution, frames, routing, dirty-private +restoration, stock, precision, recursive caller, supplier, outer theorem or +new kappa is supplied. Concave power tariffs and other endpoints are outside +scope. Independent human and formal proof-kernel review are unclaimed. Lean, +Docker, the selected cold replay and historical scientific suites were not run. + +The checker has no recursion, subprocesses or dynamic code. All matrices have +at most sixteen rows and columns; minors have order at most eight. Loops are +bounded by 225 closure pairs, the finite minor combinations, 80-by-80 atom +fixtures and ten endpoint terms. Functions are below sixty physical lines. +Power-of-Ten rule 3 has a managed-runtime deviation for Python integers, +fractions and collections within those fixed domains. Six local rejection +callbacks have fixed visible targets. File reads are capped at one MiB per +file, and warning errors are enabled in both registered commands. No native +fixed-memory guarantee or unavailable static analyzer is claimed. + +## Open next questions + +Can another specifically uncertified quadruple admit a signed or rational +block matrix with the same diagonal normalization and all closure ranks +bounded by the binary tariffs? First name one remaining index-zero quadruple +and check its complete closure table. Existence of such a witness is the +blocker; no general four-plane theorem follows from the present example. + +Can the same rank-map certificate constrain a different actual scalar endpoint +at a paid caller boundary? First state that endpoint and compute the rank of +its image. Source access, native realization and its complete physical bill +remain additional blockers. This package stops at its first proved result. + +## Credit + +The new contribution was produced by Nick Petalas. Credit Ryanson Jonathan +for PR4454's open four-plane problem and PR4421's earlier rank duals; +CubeJerry for PR4365's contract and two-plane theorem; Cinna Davis for +PR1825/2126's plane data; Gonzalo Mier for PR3990/3997's support screens; +and Philippe Van Velzen, ctoth and the retained paired-plane/native/E8 +lineage for the endpoint and expanded-identity context. Existing credit and +frozen evidence are unchanged. The lifting-method predecessors are credited +in the proof above. New material is Apache-2.0. diff --git a/research/four-plane-integral-shadow/SOURCES.json b/research/four-plane-integral-shadow/SOURCES.json new file mode 100644 index 0000000000..cac3c38e8f --- /dev/null +++ b/research/four-plane-integral-shadow/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/community-frontier1094-audit/selected-replay.tar.gz", + "usage": "provenance", + "git_blob": "c24daf067f9c543421d89ca2eeaa4eb78a57fb6f", + "sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6" + }, + { + "path": "research/four-plane-rank-dual/CERT-INDEX.bin.gz", + "usage": "provenance", + "git_blob": "7c525e1ed8af5069c8bb28cac9fefe40406a9261", + "sha256": "b66ba05b1b37a1be42c85ce855eca387a822df9d0b5d93a2d46d8c46d84ad7b1" + }, + { + "path": "research/four-plane-rank-dual/README.md", + "usage": "provenance", + "git_blob": "fd831e263b03b50804d87ab578c02cb7dec3ace7", + "sha256": "cb58edd08645cd4ed3b010b35cdef9704464f12b8b660c3d9f5da4a4aa2622bc" + }, + { + "path": "research/paired-plane-port-matching-seed6c563a/CERTIFICATE.json", + "usage": "provenance", + "git_blob": "7ca668d7d50c7276e89b0f6f9575e1b9f1ad9ef6", + "sha256": "4fd648f7b5178bff5441bf364d58234b7bc1a43b924bc6da03013c948f1473b1" + } + ] +} diff --git a/research/four-plane-integral-shadow/TASK.json b/research/four-plane-integral-shadow/TASK.json new file mode 100644 index 0000000000..b8db0c82b1 --- /dev/null +++ b/research/four-plane-integral-shadow/TASK.json @@ -0,0 +1,86 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 7, + "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "original_card": { + "id": "complex-new-helper-inventory", + "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/heterogeneous-owner-assembly/README.md", + "certificates/selected-result.json", + "research/selected-k8-unrestricted-ends/README.md" + ], + "methods": [ + "Propose a changed helper inventory and derive an optimistic exact moment.", + "Design a small completed instance and independently verify its endpoint and rank bill." + ], + "acceptance_gate": "A new physically realizable contract outside the frozen catalogue whose per-call profile, screened with ceiling.ceiling(), beats the selected word's packing ceiling; a lower cap does not establish identical circuitry or order attainable optima, and is insufficient to pass the stronger-budget target under this model. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin.", + "bottleneck_link": "Packing of the selected word is capped at +0.87% (ceiling model); only a lower local excess spend or a changed coverage law raises the cap.", + "allowed_variations": [ + "Narrow to one changed boundary or helper type with explicit counts.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Mixing only providers already inside the pinned catalogue.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "helper inventory", + "heterogeneous-owner", + "mutable leaver" + ] + }, + "scope_status": "changed", + "actual_scope": "Exact all-field additive full-plane COPY mass sixteen for the identity endpoint on the previously uncertified quadruple (0,1,44,49), via an integral rank-map certificate.", + "scope_change_reason": "Take another contributor's explicit four-plane remainder as a self-contained obstruction question. This supplies no new helper inventory, physical construction or supplier admission.", + "bottleneck_link": "Side result for the complete-plane decoder interface. It excludes an additive COPY-mass gain on one formerly uncertified four-plane identity endpoint.", + "budget_minutes": 60, + "stop_rule": "Stop at the first exact new witness and package it; do not expand the scan to further quadruples or native construction.", + "outcome": "completed", + "evidence": "README.md proof; verify.py checks all 225 closure pairs, 697 vanishing integer minors, 6400 literal atom shadows, attaining and cancelling endpoints, six rejecting controls and a fresh file-bound receipt.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does a signed or rational block matrix certify another specified index-zero four-plane quadruple?", + "why_it_matters": "It could exclude another additive mass gain outside the existing rank-dual coverage.", + "first_step": "Name one remaining uncertified quadruple and test every closure rank against its binary tariff.", + "blocked_by": "A suitable rank-preserving block matrix is not known for that new object." + }, + { + "question": "Does this rank map constrain a different scalar endpoint at a named actual caller boundary?", + "why_it_matters": "A caller-specific obstruction would distinguish a formal identity endpoint from the demanded operator.", + "first_step": "Specify the complete endpoint and compute the rank of its image under the displayed map.", + "blocked_by": "The actual source/consumer contract and full native physical invoice are absent." + } + ], + "coordination_claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19146140", + "coordination_progress": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19146177", + "environment": { + "interpreter": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12", + "version": "3.12.15", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "dependencies": "Python standard library only" + }, + "orientation": { + "historical_command": "research/complex-local-word-ceiling/verify.py", + "historical_result": "KeyError: 'complex_profile'", + "current_command": "scripts/research_selected_baseline.py", + "current_result": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY" + } +} diff --git a/research/four-plane-integral-shadow/VERIFY.json b/research/four-plane-integral-shadow/VERIFY.json new file mode 100644 index 0000000000..6bcbe039b3 --- /dev/null +++ b/research/four-plane-integral-shadow/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "All ordered closure ranks, exact vanishing integer minors, literal atom shadows, coordinate/cancelling endpoints, rejecting controls and generated file-bound receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "The same complete certificate and semantic controls with Python assertions disabled." + } + ] +} diff --git a/research/four-plane-integral-shadow/verify.py b/research/four-plane-integral-shadow/verify.py new file mode 100644 index 0000000000..f971419dfd --- /dev/null +++ b/research/four-plane-integral-shadow/verify.py @@ -0,0 +1,258 @@ +#!/usr/bin/env python3 +"""Check one integral four-plane COPY certificate. Apache-2.0.""" +from collections import Counter +from fractions import Fraction +import hashlib +from itertools import combinations, product +import json +from pathlib import Path + + +LABELS = (11, 19, 35, 67, 296, 392, 400, 416) +QUADRUPLE = (0, 1, 44, 49) +FILES = ("README.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + + +class CheckFailure(ValueError): + """A certificate or semantic control failed.""" + + +def need(condition, message): + if not condition: + raise CheckFailure(message) + + +def identity(n): + need(1 <= n <= 16, "identity dimension") + return [[int(i == j) for j in range(n)] for i in range(n)] + + +def pairing(): + return [[(a & b).bit_count() % 2 for b in LABELS] for a in LABELS] + + +def indices(mask): + need(type(mask) is int and 1 <= mask < 16, "nonempty plane mask") + return [i for i in range(8) if mask >> (i // 2) & 1] + + +def rectangle(matrix, rows, columns): + return [[matrix[i][j] for j in columns] for i in rows] + + +def binary_rank(matrix): + basis = [0] * 8 + for row in matrix: + value = sum(x << j for j, x in enumerate(row)) + for j in range(7, -1, -1): + if not value >> j & 1: + continue + if basis[j]: + value ^= basis[j] + else: + basis[j] = value + break + return sum(bool(x) for x in basis) + + +def rational_rank(matrix): + work = [[Fraction(x) for x in row] for row in matrix] + rank = 0 + for column in range(len(work[0])): + pivot = next((i for i in range(rank, len(work)) if work[i][column]), None) + if pivot is None: + continue + work[rank], work[pivot] = work[pivot], work[rank] + value = work[rank][column] + work[rank] = [x / value for x in work[rank]] + for i in range(rank + 1, len(work)): + value = work[i][column] + work[i] = [x - value * y for x, y in zip(work[i], work[rank])] + rank += 1 + if rank == len(work): + break + return rank + + +def determinant(matrix): + """Integer Bareiss elimination, independent of the rational rank engine.""" + work = [row[:] for row in matrix] + n = len(work) + need(1 <= n <= 8 and all(len(row) == n for row in work), "minor shape") + previous, sign = 1, 1 + for column in range(n - 1): + pivot = next((i for i in range(column, n) if work[i][column]), None) + if pivot is None: + return 0 + if pivot != column: + work[column], work[pivot] = work[pivot], work[column] + sign = -sign + value = work[column][column] + for i in range(column + 1, n): + for j in range(column + 1, n): + numerator = work[i][j] * value - work[i][column] * work[column][j] + need(numerator % previous == 0, "exact Bareiss division") + work[i][j] = numerator // previous + work[i][column] = 0 + previous = value + return sign * work[-1][-1] + + +def upper_minors(matrix, rank): + """Every (rank+1)-minor vanishes in Z, hence in every field.""" + count = 0 + for rows in combinations(range(len(matrix)), rank + 1): + for columns in combinations(range(len(matrix[0])), rank + 1): + need(determinant(rectangle(matrix, rows, columns)) == 0, + "nonzero integer minor exceeds the binary tariff") + count += 1 + return count + + +def certificate(gram): + for plane in range(4): + local = (2 * plane, 2 * plane + 1) + need(rectangle(gram, local, local) == identity(2), "Gram-I2 plane") + tariffs, histogram, minors = {}, Counter(), 0 + stream = hashlib.sha256() + for source, reader in product(range(1, 16), repeat=2): + block = rectangle(gram, indices(source), indices(reader)) + tariff = binary_rank(block) + need(rational_rank(block) == tariff, "rational/binary rank equality") + minors += upper_minors(block, tariff) + tariffs[source, reader] = tariff + histogram[tariff] += 1 + stream.update(bytes((source, reader, tariff))) + need(len(tariffs) == 225, "all ordered closure pairs") + return tariffs, dict(sorted(histogram.items())), minors, stream.hexdigest() + + +def outer(left, right): + return [[a * b for b in right] for a in left] + + +def shadow(matrix, gram): + """Phi(M)[(i,a),(j,b)] = M[i,j] G[(plane(i),a),(plane(j),b)].""" + return [[matrix[i][j] * gram[2 * (i // 2) + a][2 * (j // 2) + b] + for j in range(8) for b in range(2)] + for i in range(8) for a in range(2)] + + +def rank_three(matrix): + work = [[x % 3 for x in row] for row in matrix] + rank = 0 + for column in range(len(work[0])): + pivot = next((i for i in range(rank, len(work)) if work[i][column]), None) + if pivot is None: + continue + work[rank], work[pivot] = work[pivot], work[rank] + inverse = pow(work[rank][column], -1, 3) + work[rank] = [x * inverse % 3 for x in work[rank]] + for i in range(rank + 1, len(work)): + value = work[i][column] + work[i] = [(x - value * y) % 3 for x, y in zip(work[i], work[rank])] + rank += 1 + if rank == len(work): + break + return rank + + +def vectors(): + out = [] + for choices in product(range(3), repeat=4): + if not any(choices): + continue + vector = [0] * 8 + mask = 0 + for plane, choice in enumerate(choices): + if choice: + vector[2 * plane + choice - 1] = 1 + mask |= 1 << plane + out.append((vector, mask)) + need(len(out) == 80, "one-coordinate-per-touched-plane domain") + return out + + +def atom_checks(gram, tariffs): + cases, stream = 0, hashlib.sha256() + choices = vectors() + for (left, source), (right, reader) in product(choices, repeat=2): + lifted = shadow(outer(left, right), gram) + need(rank_three(lifted) <= tariffs[source, reader], "literal atom bound") + stream.update(bytes(x % 3 for row in lifted for x in row)) + cases += 1 + return cases, stream.hexdigest() + + +def total(matrices, size): + need(len(matrices) <= 10, "finite endpoint fixture") + return [[sum(matrix[i][j] for matrix in matrices) for j in range(size)] + for i in range(size)] + + +def endpoints(gram, tariffs): + coordinate = [outer(row, row) for row in identity(8)] + need(total(coordinate, 8) == identity(8), "coordinate identity endpoint") + need(sum(tariffs[1 << (i // 2), 1 << (i // 2)] for i in range(8)) == 16, + "attaining coordinate tariff") + need(shadow(identity(8), gram) == identity(16), "full-rank identity shadow") + dense = outer([1] * 8, [1, -1] * 4) + negative = [[-x for x in row] for row in dense] + overcomplete = coordinate + [dense, negative] + need(total(overcomplete, 8) == identity(8), "ten-term cancellation endpoint") + need(total([shadow(m, gram) for m in overcomplete], 16) == identity(16), + "shadow linearity includes cancelling terms") + return coordinate + + +def rejects(check): + try: + check() + except CheckFailure: + return + raise CheckFailure("semantic mutation was accepted") + + +def controls(gram, coordinate): + rejects(lambda: indices(0)) + rejects(lambda: indices(True)) + rejects(lambda: need(total(coordinate[:-1], 8) == identity(8), "omitted term")) + rejects(lambda: need(rank_three(shadow(coordinate[0], gram)) <= 1, + "underpriced self-plane COPY")) + nonlift = [[1, 1, 0], [1, 0, 1], [0, 1, 1]] + need(binary_rank(nonlift) == 2 and rational_rank(nonlift) == 3, + "characteristic-sensitive rank control") + rejects(lambda: upper_minors(nonlift, 2)) + wrong = [row[:] for row in gram] + wrong[0][0] = 0 + rejects(lambda: need(shadow(identity(8), wrong) == identity(16), + "missing diagonal normalization")) + free = outer(identity(8)[0], identity(8)[2]) + need(rank_three(free) == 1 and rank_three(shadow(free, gram)) == 0, + "free cross atom must vanish in the shadow") + return 6 + + +def main(): + gram = pairing() + tariffs, histogram, minors, tariff_digest = certificate(gram) + atom_cases, atom_digest = atom_checks(gram, tariffs) + coordinate = endpoints(gram, tariffs) + control_count = controls(gram, coordinate) + hashes = {} + for name in FILES: + with Path(__file__).with_name(name).open("rb") as source: + data = source.read(1_000_001) + need(len(data) <= 1_000_000, "bounded package file") + hashes[name] = hashlib.sha256(data).hexdigest() + result = {"status": "PASS_FOUR_PLANE_INTEGRAL_SHADOW", "quadruple": QUADRUPLE, + "closure_pairs": len(tariffs), "rank_histogram": histogram, + "vanishing_integer_minors": minors, "tariff_sha256": tariff_digest, + "literal_atoms": atom_cases, "atom_sha256": atom_digest, + "minimum_mass": 16, "coefficient_fields": "all", + "rejecting_controls": control_count, "files": hashes} + print(json.dumps(result, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()