From a2f593e60346aaed903425c3bac84eb250b07972 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Wed, 11 Nov 2026 11:35:05 +0000 Subject: [PATCH] feat(research): certify one filled three-dimensional mode shadow --- research/mode-rank-five-shadow/PROOF.md | 172 ++++++++++++++ research/mode-rank-five-shadow/README.md | 79 +++++++ research/mode-rank-five-shadow/SOURCES.json | 42 ++++ research/mode-rank-five-shadow/TASK.json | 94 ++++++++ research/mode-rank-five-shadow/VERIFY.json | 36 +++ research/mode-rank-five-shadow/verify.py | 235 ++++++++++++++++++++ 6 files changed, 658 insertions(+) create mode 100644 research/mode-rank-five-shadow/PROOF.md create mode 100644 research/mode-rank-five-shadow/README.md create mode 100644 research/mode-rank-five-shadow/SOURCES.json create mode 100644 research/mode-rank-five-shadow/TASK.json create mode 100644 research/mode-rank-five-shadow/VERIFY.json create mode 100644 research/mode-rank-five-shadow/verify.py diff --git a/research/mode-rank-five-shadow/PROOF.md b/research/mode-rank-five-shadow/PROOF.md new file mode 100644 index 0000000000..0ba3641f09 --- /dev/null +++ b/research/mode-rank-five-shadow/PROOF.md @@ -0,0 +1,172 @@ +# One rank-five flat has a filled three-dimensional mode shadow + +The proof and finite certificate were produced by Nick Petalas. New work is +Apache-2.0. This is an exact finite result for one fixed mode matrix. +Independent human and formal proof-kernel review are unclaimed. + +## Statement + +Let the rows of the 112-by-8 integer mode matrix in Dillon Amburgey's +`research/coded-native-caller/NORMALIZERS.json` be `m_0,...,m_111`, indexed +from zero. Put `L = span_Z {m_i}` and `Z = sum_i [0,1] m_i`. +Let `F = span_R {m_0,...,m_4}`. These five rows are + +```text +1 1 1 1 0 0 0 0 +1 1 0 0 1 1 0 0 +1 0 1 0 1 0 1 0 +1 0 0 1 0 1 1 0 +1 0 0 1 1 0 0 1 +``` + +Define the rational quotient map `pi(x) = B x / 2`, with + +```text +B = [-2 0 1 1 1 1 0 0] + [-2 1 0 1 1 0 1 0] + [ 1 0 0 -1 -1 0 0 1]. +``` + +**Finite theorem.** `ker(pi) = F`, `pi(L) = Z^3`, and + +```text +pi(Z) intersect Z^3 = { sum_i epsilon_i pi(m_i) : epsilon_i in {0,1} }. +``` + +The left-hand side has exactly **103,333** points. Exactly **94,599** are +strictly interior, and **8,734** are on the boundary. Thus this particular +three-dimensional shadow has no lattice hole, even on its boundary. + +## Quotient and row flat + +Exact rational row reduction gives rank five for the five displayed rows +and rank three for B. Each displayed row is annihilated by B, so F is exactly +the kernel. Of the 112 rows, exactly 15 are annihilated. Their rank is five. +They form the closed row flat with span F. A generic functional in F's +three-dimensional annihilator exposes a face parallel to F, so this is a +shadow along a codimension-three face in the sense of apoursh's #6829. + +The verifier computes every `B m_i`, checks divisibility by two, and sets +`q_i = pi(m_i)`. Some q_i are the signed coordinate unit vectors. Hence +`span_Z {q_i} = Z^3`, without any lattice saturation or index assumption. + +For enumeration, replace each q_i whose first nonzero coordinate is negative +by `p_i = -q_i`; leave the others unchanged. Let t be the sum of the q_i +that were replaced. Then both the zonotope and its subset sums translate +by the same integer vector: + +```text +sum_i [0,1] q_i = t + sum_i [0,1] p_i, +{sum_i epsilon_i q_i} = t + {sum_i epsilon_i p_i}. +``` + +Consequently filling can be checked for the p_i. This reorientation leaves +15 zero generators. The 14 distinct nonzero generators and multiplicities +are emitted in the computed receipt. The exact coordinate bounding box is + +```text +[0,86] x [-1,85] x [-49,5], +``` + +which contains 416,295 integer points. + +## Complete finite certificate + +The verifier uses two different representations of subset sums. First, +encode a point in that box as + +```text +index(x,y,z) = x + 87(y+1) + 87^2(z+49). +``` + +Starting with the bit for the origin, update `S <- S union (S+p_i)` for +each of the 112 generators. A signed integer bit shift implements this +update. At every prefix, each genuine subset sum lies in the global box, +because the sum of coordinatewise negative contributions is a lower bound +and the sum of positive contributions is an upper bound. Thus no encoded +shift crosses a coordinate boundary, wraps, or discards a genuine point. +The final set has 103,333 bits. A separate tuple-set recurrence computes +all subset sums and agrees with every bit, without integer encoding. + +The closed three-dimensional zonotope has a complete facet description +obtained as follows. For each pair of distinct generator directions, take +their cross product. Discard zero products, divide by the gcd, and identify +opposite normals. There are exactly 25 resulting normal pairs. For each +primitive normal n, the exact support inequalities are + +```text +sum_i min(0,n.p_i) <= n.x <= sum_i max(0,n.p_i). +``` + +These inequalities define the zonotope. Indeed, each facet's parallel +generators span a two-dimensional plane, so two independent generators +produce its normal in the cross-product list. Conversely every listed +inequality is valid. A bounded full-dimensional polytope is the +intersection of its facet half-spaces. No floating-point hull computation +or predecessor facet census is used here. + +For each of the 87-by-55 possible pairs `(y,z)`, intersect these 25 +inequalities to obtain the exact integer x interval. The closed intervals +contain 103,333 points, each present in the subset bitset. Replacing each +primitive integral support inequality by its strict version gives 94,599 +interior points, also all present. A separate pointwise scan tests all +416,295 points against all 25 inequalities and compares every closed +membership decision with the tuple set. It independently reproduces both +counts. Their difference is the boundary count. + +The receipt is computed at execution time and binds the six package files +and the subset bitset by SHA256. It is not a handwritten or committed log. + +## Controls and implementation bounds + +Removing one actually reached interior point creates exactly one detected +hole in both the closed and interior scans. A small full-rank integer +zonotope with generators `(1,-3,0),(1,-2,0),(1,0,0),(0,0,1),(0,0,1)` has +holes; the verifier checks their exact counts rather than assuming every +zonotope fills. An independent tuple encoding of that example checks signed +shifts. These are five explicit control predicates, counted in the receipt. + +The verifier is nonrecursive and read-only. The source boundary checks eight +columns, 112 rows, entries in {-1,0,1}, and its pinned SHA256. Geometry accepts +at most 112 three-coordinate generators, coordinates bounded by eight, and +a box of at most 500,000 points. Every enumeration is bounded by these +finite dimensions. No function exceeds 60 physical lines. + +Power-of-ten rule 3 deviation applies to Python integers, Fractions, JSON, +sets and tuples: CPython allocates managed objects during the calculation. +The scope is this finite verifier. The enforced box capacity bounds each +reachable set by 500,000 tuples; at most the existing and one shifted set +are live during an update. The bitset has at most 500,000 bits. File inputs +are pinned and bounded. Both normal and optimized warning-strict replay +exercise the same checks, which use explicit exceptions rather than Python +assertions. Follow-up if the input family grows is to retain explicit +capacity bounds or switch the tuple cross-check to fixed packed storage. +Separate compiler/type analysis is not supplied for this standard-library +Python research script. + +## Scope and predecessors + +Armin Pourshafeie / apoursh's #6829 poses the codimension-three question +and proves filling of every facet and ridge shadow. Those results are cited, +not rechecked. The new calculation begins in a different quotient and proves +the displayed one-flat statement only. Dillon Amburgey's #4933 supplies M. +Nick Petalas's #6312 defines the exact-mode rounding radius, and apoursh's +#6320 reduces radius one to full eight-dimensional lattice filling; #6333 +gives the retained upper bound three halves. Cross products, zonotope support +functions, exact elimination and subset-sum dynamic programming are classical. + +This does not classify rank-five flats, prove filling for every +three-dimensional shadow, or settle full eight-dimensional filling or R=1. +No physical rounder, compiler, precision, tape, ownership, stock, supplier +admission, new kappa, selected-frontier change or complete multiplication +theorem follows. All five selected framework assumptions remain. + +## Open next questions + +- Classify rank-five row flats up to the mode matrix's signed code symmetries. + Begin by mapping the 15-row flat above into that catalogue. A complete + orbit inventory is not supplied here. +- Test a different rank-five-flat orbit with the same lattice-index and + full-membership checks. Larger quotient boxes may need a different exact + representation. Filling every such shadow would still leave higher + codimensions and full R=1 open. diff --git a/research/mode-rank-five-shadow/README.md b/research/mode-rank-five-shadow/README.md new file mode 100644 index 0000000000..22b659fc18 --- /dev/null +++ b/research/mode-rank-five-shadow/README.md @@ -0,0 +1,79 @@ +# A filled three-dimensional mode shadow along one rank-five flat + +This contribution was produced by Nick Petalas. New work is Apache-2.0. +Independent human and formal proof-kernel review are unclaimed. + +**Exact finite certificate with a scoped proof; no new kappa.** For the +112-by-8 mode matrix of Dillon Amburgey's #4933, the row flat generated by +rows 0 through 4 has a three-dimensional quotient whose entire closed +zonotope is lattice-filled. Every one of its **103,333** lattice points is +a subset sum of the projected modes. Exactly **94,599** are interior and +**8,734** are boundary points. Row numbering starts at zero. + +This supplies one explicit case of Open next question 1 in Armin +Pourshafeie / apoursh's [#6829](https://github.com/CrocSwap/integer-mult-bounds/pull/6829). +That package establishes facet and ridge filling and leaves three-dimensional +shadows open. Its scientific verifier is not replayed here. + +[PROOF.md](PROOF.md) gives the quotient map, lattice basis, complete exact +facet description and finite enumeration argument. The new verifier reads +the pinned original matrix, checks the flat, computes all subset sums twice, +and compares them with every lattice point in the quotient zonotope. + +## 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/mode-rank-five-shadow/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/mode-rank-five-shadow/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/mode-rank-five-shadow +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/mode-rank-five-shadow --check-source-history +``` + +Substitute another CPython 3.12 path on other machines. Expected markers are +`PASS_MODE_RANK_FIVE_SHADOW`, `PASS_REGISTERED_RESEARCH_PACKAGE`, and +`PASS_RESEARCH_COMMIT_BYTES`. A sparse checkout needs this package and +`research/coded-native-caller/NORMALIZERS.json` materialized before replay. + +The verifier enumerates a box of 416,295 integer points, 25 facet-normal +pairs, and all 103,333 distinct subset sums. Independent bitset and tuple-set +recurrences agree exactly; independent interval and pointwise scans agree +on closed and interior membership. Five control predicates detect a removed +interior subset sum and holes in a small counterexample. Receipts are +generated from the current file hashes and bitset; no receipt is handwritten. + +## Limitations + +Only one rank-five row flat is covered. There is no all-orbit census, +universal three-dimensional filling theorem, or proof of R=1. The current +rounding-radius interval remains 1 to 3/2. Exact-mode rounding itself is an +abstract interface. No physical rounder or complete multiplication theorem +is supplied; kappa, selected frontier and the five assumptions are unchanged. +Native/caller implementation, ownership, compiler, precision/tape and stock +costs remain open. No predecessor scientific replay, full selected cold +replay, Lean, Docker or separate type/lint analysis was run. Hosted CI is +separate from local finite verification. + +The `uniform-transfer-audit` card has explicitly changed scope to this +analytic-recovery side result. Its actual-caller acceptance gate is unmet. +The source-binding baseline passed and is only metadata orientation. + +## Open next questions + +- Locate this 15-row flat in a complete signed-symmetry orbit catalogue of + rank-five row flats. A complete catalogue is not part of this certificate. +- Test another orbit using an exact quotient-lattice basis and full lattice + membership scan. Larger quotient boxes may need another representation. +- Connect any eventual full-dimensional filling result to a physical + rounder and its complete caller costs. Shadow filling alone is insufficient. + +## Credit + +Credit Armin Pourshafeie / apoursh #6829 for the open three-dimensional +question and facet/ridge results, #6320 for the full-dimensional finite +reduction, and #6333 for R <= 3/2. Dillon Amburgey #4933 supplies the unchanged +mode matrix. Nick Petalas #6312 supplies the exact-mode radius definition +and lower bound. Exact elimination, zonotope support functions and subset-sum +dynamic programming are classical. The new quotient calculation, finite +certificate, proof and verifier were produced by Nick Petalas. diff --git a/research/mode-rank-five-shadow/SOURCES.json b/research/mode-rank-five-shadow/SOURCES.json new file mode 100644 index 0000000000..7f2af57b38 --- /dev/null +++ b/research/mode-rank-five-shadow/SOURCES.json @@ -0,0 +1,42 @@ +{ + "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/coded-native-caller/NORMALIZERS.json", + "usage": "input", + "git_blob": "bca92c222c395d3d75c047fbb678f3cd0947c60f", + "sha256": "ae8aad06aa5d1811d725895b3ab5a4f4daa9dcdd88294aa0d5f723e78bb1e0da" + }, + { + "path": "research/mode-fiber-facet-depth/README.md", + "usage": "provenance", + "git_blob": "68505da8c65b7423a06df844b19cf0c16addb793", + "sha256": "42ff56e9ecee6e256991d58e679d86e9bfde50a20e2cfb64deaf2e2500470b84" + }, + { + "path": "research/mode-fiber-facet-depth/PROOF.md", + "usage": "provenance", + "git_blob": "b0cdd56c3cc16415983e5e9bd6f3ddccf9112b73", + "sha256": "ee436e8f10f6170123e686d3b96e96cafda40ffb93380ac7284d6d055ce21742" + }, + { + "path": "research/mode-fiber-radius-bounds/PROOF.md", + "usage": "provenance", + "git_blob": "ba8a3da373a2bc9cf7c499681e2f3bd0145b45a8", + "sha256": "9793a4418f5e24f3577c166640906260913ebf7da3011559abdf175be3e6e341" + } + ] +} diff --git a/research/mode-rank-five-shadow/TASK.json b/research/mode-rank-five-shadow/TASK.json new file mode 100644 index 0000000000..3f939448fd --- /dev/null +++ b/research/mode-rank-five-shadow/TASK.json @@ -0,0 +1,94 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "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" + ], + "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": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "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": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "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": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "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": "Exact lattice filling of the three-dimensional shadow along the rank-five flat generated by mode rows 0 through 4.", + "scope_change_reason": "The donated task requests original work; this answers one case of apoursh PR6829 Open next question 1 instead of auditing a predecessor or claiming actual-caller assumption discharge.", + "bottleneck_link": "Analytic-recovery side result: removes one possible projected lattice-hole obstruction to exact mode-preserving radius-one rounding. No actual caller or physical rounder follows.", + "budget_minutes": 60, + "stop_rule": "Stop at the first exact original one-flat filling certificate or a precise hole/handoff.", + "outcome": "completed", + "evidence": "Exact quotient lattice and rank-five flat; 103333 closed lattice points, 94599 interior and 8734 boundary, all subset sums. Bitset/tuple and interval/pointwise enumerations agree. Five control predicates.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Classify rank-five row-flat orbits and identify the displayed 15-row flat.", + "why_it_matters": "One case does not cover every codimension-three shadow.", + "first_step": "Apply the retained signed code symmetries to the closed flat.", + "blocked_by": "No complete rank-five orbit inventory is supplied." + }, + { + "question": "Does another rank-five-flat orbit have a lattice hole?", + "why_it_matters": "A missing projected subset sum could obstruct radius-one rounding.", + "first_step": "Compute an exact quotient-lattice basis and scan the complete projected box.", + "blocked_by": "Larger quotient boxes may require a different finite representation." + } + ], + "environment": { + "python": "3.12.15", + "requirements": "standard library only" + }, + "claim_type": "Exact finite certificate with a scoped proof for one fixed row flat." +} diff --git a/research/mode-rank-five-shadow/VERIFY.json b/research/mode-rank-five-shadow/VERIFY.json new file mode 100644 index 0000000000..c10f830a0d --- /dev/null +++ b/research/mode-rank-five-shadow/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/coded-native-caller/NORMALIZERS.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact flat and quotient lattice, complete independent subset and zonotope scans, five controls and computed source-bound receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat every finite predicate with assertions disabled; identical computed receipt required." + } + ] +} diff --git a/research/mode-rank-five-shadow/verify.py b/research/mode-rank-five-shadow/verify.py new file mode 100644 index 0000000000..30c2169500 --- /dev/null +++ b/research/mode-rank-five-shadow/verify.py @@ -0,0 +1,235 @@ +"""Exact finite certificate for one rank-five-flat mode shadow.""" + +from collections import Counter +from fractions import Fraction +from hashlib import sha256 +from itertools import combinations, product +import json +from math import gcd +from pathlib import Path + + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +PROJECTION = ( + (-2, 0, 1, 1, 1, 1, 0, 0), + (-2, 1, 0, 1, 1, 0, 1, 0), + (1, 0, 0, -1, -1, 0, 0, 1), +) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def dot(left, right): + return sum(a * b for a, b in zip(left, right, strict=True)) + + +def rank(rows): + matrix = [list(map(Fraction, row)) for row in rows] + pivot = 0 + for column in range(len(matrix[0])): + found = next((i for i in range(pivot, len(matrix)) + if matrix[i][column]), None) + if found is None: + continue + matrix[pivot], matrix[found] = matrix[found], matrix[pivot] + scale = matrix[pivot][column] + matrix[pivot] = [x / scale for x in matrix[pivot]] + for i in range(pivot + 1, len(matrix)): + scale = matrix[i][column] + matrix[i] = [x - scale * y + for x, y in zip(matrix[i], matrix[pivot], strict=True)] + pivot += 1 + if pivot == len(matrix): + break + return pivot + + +def load_rows(): + sources = json.loads((PACKAGE / "SOURCES.json").read_text()) + source = next(row for row in sources["files"] if row["usage"] == "input") + source_path = ROOT / source["path"] + require(source_path.stat().st_size < 2_000_000, "source exceeds input bound") + payload = source_path.read_bytes() + require(sha256(payload).hexdigest() == source["sha256"], "source hash") + columns = json.loads(payload)["mode_columns"] + require(len(columns) == 8, "eight modes required") + require(all(len(c) == 112 for c in columns), "112 ports required") + require(all(type(x) is int and x in (-1, 0, 1) + for c in columns for x in c), "mode entry") + return tuple(zip(*columns, strict=True)) + + +def project(rows): + require(rank(PROJECTION) == 3, "projection rank") + require(rank(rows[:5]) == 5, "flat basis rank") + raw = [tuple(dot(n, row) for n in PROJECTION) for row in rows] + require(all(x % 2 == 0 for p in raw for x in p), "even projection") + require(all(not any(p) for p in raw[:5]), "flat annihilation") + flat = [i for i, p in enumerate(raw) if not any(p)] + require(len(flat) == 15 and rank([rows[i] for i in flat]) == 5, + "closed flat rank and cardinality") + points, translation = [], [0, 0, 0] + for p in raw: + q = tuple(x // 2 for x in p) + if next((x for x in q if x), 0) < 0: + translation = [a + b for a, b in zip(translation, q, strict=True)] + q = tuple(-x for x in q) + points.append(q) + require(all(tuple(int(i == j) for i in range(3)) in points + for j in range(3)), "quotient lattice is Z^3") + return points, flat, translation + + +def product_size(sizes): + return sizes[0] * sizes[1] * sizes[2] + + +def geometry(points): + require(3 <= len(points) <= 112, "generator bound") + require(all(len(p) == 3 and all(type(x) is int and abs(x) <= 8 for x in p) + for p in points), "bounded integer generators") + lo = tuple(sum(min(0, p[i]) for p in points) for i in range(3)) + hi = tuple(sum(max(0, p[i]) for p in points) for i in range(3)) + sizes = tuple(b - a + 1 for a, b in zip(lo, hi, strict=True)) + require(product_size(sizes) <= 500_000, "box capacity") + strides = (1, sizes[0], sizes[0] * sizes[1]) + normals = set() + for a, b in combinations(sorted(set(points)), 2): + n = (a[1]*b[2] - a[2]*b[1], a[2]*b[0] - a[0]*b[2], + a[0]*b[1] - a[1]*b[0]) + divisor = gcd(*n) + if divisor: + n = tuple(x // divisor for x in n) + if next(x for x in n if x) < 0: + n = tuple(-x for x in n) + normals.add(n) + require(rank(sorted(normals)) == 3, "full-dimensional zonotope") + facets = [] + for n in sorted(normals): + values = [dot(n, p) for p in points] + facets.append((n, sum(min(0, x) for x in values), + sum(max(0, x) for x in values))) + return lo, hi, sizes, strides, facets + + +def encode(point, lo, strides): + return sum((x - a) * s for x, a, s in zip(point, lo, strides, strict=True)) + + +def subset_bits(points, geo): + lo, _, sizes, strides, _ = geo + bits = 1 << encode((0, 0, 0), lo, strides) + for point in points: + shift = dot(point, strides) + bits |= bits << shift if shift >= 0 else bits >> -shift + require(bits.bit_length() <= product_size(sizes), "subset box overflow") + return bits + + +def subset_set(points): + reached = {(0, 0, 0)} + for a, b, c in points: + shifted = {(x+a, y+b, z+c) for x, y, z in reached} + reached.update(shifted) + require(len(reached) <= 500_000, "subset set capacity") + return reached + + +def scan(geo, bits, strict): + lo, hi, _, strides, facets = geo + count = holes = 0 + first = None + for z in range(lo[2], hi[2] + 1): + for y in range(lo[1], hi[1] + 1): + left, right = lo[0], hi[0] + for (a, b, c), low, high in facets: + low, high = low + strict, high - strict + offset = b*y + c*z + if a == 0: + if not low <= offset <= high: + left, right = 1, 0 + break + else: + if a < 0: + a, low, high, offset = -a, -high, -low, -offset + left = max(left, -((offset-low) // a)) + right = min(right, (high-offset) // a) + if left <= right: + width = right - left + 1 + mask = (1 << width) - 1 + position = encode((left, y, z), lo, strides) + count += width + holes += (mask ^ ((bits >> position) & mask)).bit_count() + if first is None: + first = position + return count, holes, first + + +def direct_scan(geo, reached): + lo, hi, _, _, facets = geo + closed = interior = 0 + for p in product(*(range(a, b+1) for a, b in zip(lo, hi, strict=True))): + values = [(dot(n, p), low, high) for n, low, high in facets] + inside = all(low <= v <= high for v, low, high in values) + require(inside == (p in reached), "direct point membership") + closed += inside + interior += all(low < v < high for v, low, high in values) + return closed, interior + + +def controls(geo, bits, interior): + position = interior[2] + require(position is not None and (bits >> position) & 1, "interior fixture") + damaged = bits ^ (1 << position) + require(scan(geo, damaged, 0)[1] == 1, "deleted subset, closed control") + require(scan(geo, damaged, 1)[1] == 1, "deleted subset, interior control") + toy = [(1, -3, 0), (1, -2, 0), (1, 0, 0), (0, 0, 1), (0, 0, 1)] + toy_geo = geometry(toy) + toy_bits = subset_bits(toy, toy_geo) + require(scan(toy_geo, toy_bits, 0)[:2] == (30, 6), "closed holes control") + require(scan(toy_geo, toy_bits, 1)[:2] == (4, 2), "interior holes control") + reached = subset_set(toy) + lo, _, _, strides, _ = toy_geo + require(sum(1 << encode(p, lo, strides) for p in reached) == toy_bits, + "signed shifts control") + return 5 + + +def main(): + rows = load_rows() + points, flat, translation = project(rows) + geo = geometry(points) + require(geo[:3] == ((0, -1, -49), (86, 85, 5), (87, 87, 55)), "box") + require(len(geo[4]) == 25, "facet-normal count") + bits = subset_bits(points, geo) + reached = subset_set(points) + lo, _, _, strides, _ = geo + independent_bits = sum(1 << encode(p, lo, strides) for p in reached) + require(bits == independent_bits, "independent subset enumeration") + closed, interior = scan(geo, bits, 0), scan(geo, bits, 1) + require(closed[:2] == (103333, 0), "closed filling certificate") + require(interior[:2] == (94599, 0), "interior filling certificate") + require(direct_scan(geo, reached) == (103333, 94599), "independent scan") + control_count = controls(geo, bits, interior) + files = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", + "VERIFY.json", "verify.py") + receipt = { + "status": "PASS_MODE_RANK_FIVE_SHADOW", "flat_indices": flat, + "translation": translation, "closed_points": closed[0], + "interior_points": interior[0], "subset_sums": len(reached), + "box_points": product_size(geo[2]), "facet_normal_pairs": len(geo[4]), + "controls": control_count, + "generator_histogram": [[list(p), n] for p, n in sorted(Counter(points).items())], + "subset_sha256": sha256(bits.to_bytes((bits.bit_length()+7)//8, "little")).hexdigest(), + "package_sha256": {name: sha256((PACKAGE/name).read_bytes()).hexdigest() + for name in files}, + } + print(json.dumps(receipt, sort_keys=True)) + + +if __name__ == "__main__": + main()