From 8f26fda2e817be8dc5ed3bf1edcde774b9f20f7c Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 23 Oct 2026 12:04:55 +0100 Subject: [PATCH] feat(research): prove the P112 exceptional-hull COPY floor --- research/p112-exceptional-hull-floor/PROOF.md | 132 +++++++++++++ .../p112-exceptional-hull-floor/README.md | 105 +++++++++++ .../p112-exceptional-hull-floor/SOURCES.json | 30 +++ .../p112-exceptional-hull-floor/TASK.json | 101 ++++++++++ .../p112-exceptional-hull-floor/VERIFY.json | 35 ++++ .../p112-exceptional-hull-floor/verify.py | 176 ++++++++++++++++++ 6 files changed, 579 insertions(+) create mode 100644 research/p112-exceptional-hull-floor/PROOF.md create mode 100644 research/p112-exceptional-hull-floor/README.md create mode 100644 research/p112-exceptional-hull-floor/SOURCES.json create mode 100644 research/p112-exceptional-hull-floor/TASK.json create mode 100644 research/p112-exceptional-hull-floor/VERIFY.json create mode 100644 research/p112-exceptional-hull-floor/verify.py diff --git a/research/p112-exceptional-hull-floor/PROOF.md b/research/p112-exceptional-hull-floor/PROOF.md new file mode 100644 index 0000000000..801f5cf840 --- /dev/null +++ b/research/p112-exceptional-hull-floor/PROOF.md @@ -0,0 +1,132 @@ +# Exceptional-hull cross forms keep the P112 two-call floor + +## Statement and inherited model + +Use the arbitrary directed cross-form model of Sagar Thakrar's PR2294, +with the support theorem and incidence count stated in commdata2338's +[PR2395 proof](../p112-cross-form-rank-tradeoff/PROOF.md). These results are +premises, not new results of this package. + +The reader and source label spaces are both F2^9, with the ordinary dot +product as the within-call pairing. Every nonzero P112 root-code coefficient +vector has label span F2^9 or one of eight coordinate-support hyperplanes. +Write the reader hyperplanes as U_a = r_a^perp and the source hyperplanes +as V_b = s_b^perp. Their pairings have rank eight. Equivalently, + + r_a dot s_b = 1 for every a,b in {0,...,7}. (1) + +Let S = span_F2{s_0,...,s_7}. Take any nonzero binary vector v, any +i in {0,...,7}, and independent directed cross forms + + beta01 = r_i v^T, + beta10 = C, with every row of C in S. (2) + +**Theorem.** Every exact two-call root-code factorization in this model +has total union COPY-rank price at least 128. The minimum is exactly 128. +There is no restriction on the number of terms or their complex scalars. +The reverse form C may have rank greater than one. + +## New transfer step + +Take any double term, meaning that both reader blocks and both source +blocks are nonzero. Restrict its four support spans to coordinate +hyperplanes U_a,V_b,U_c,V_d. This is possible by the inherited support +theorem. Restricting a matrix cannot increase its rank. + +The within-call pairing on U_a x V_b is nonsingular. The vector in V_b +representing the functional x -> x dot r_i on U_a is + + z = r_i + (r_i dot s_b) r_a = r_i + r_a. (3) + +Indeed, z dot s_b = 1+1 = 0, so z is in V_b. Also x dot z = x dot r_i +for x in U_a. Nonsingularity gives uniqueness. + +Every exceptional source normal kills z, since + + s_j dot z = s_j dot r_i + s_j dot r_a = 1+1 = 0. (4) + +By linearity, every vector of S kills z. The row-space hypothesis on C +therefore implies C z = 0. + +Write the restricted double pairing in block form as [A B; E D], with +A and D nonsingular eight-by-eight matrices. For a source vector y in +V_d, the vector representing B's functional on U_a is z (v dot y). +Equation (4) gives E A^-1 B = 0. Block elimination now gives + + rank_F2 [A B; E D] = 8 + rank_F2(D - E A^-1 B) = 16. (5) + +Thus every double term has price at least 16. This is the new step. +In particular, it applies when C is a sum of independent exceptional +source functionals, rather than one rank-one cross form. + +## From term prices to the sharp floor + +The inherited coefficient identity is sum_j a_j c_j^T = I_16 over C, +with ordinary transpose. Discard terms having a zero entire factor. +Call a term pure if it has a reader in one call and a source only in the +other. Let n count all non-pure terms and d count the double terms. + +Each diagonal identity block has complex rank eight and therefore needs +at least eight diagonal-contributing terms. A double contributes to both +blocks; every other non-pure term contributes to exactly one. Hence + + n + d >= 16. (6) + +Every non-pure term has price at least eight from its within-call block. +Equation (5) raises the double-term charge to sixteen. Pure prices are +nonnegative, so the complete separate-total COPY price is at least + + 8(n-d) + 16d = 8(n+d) >= 128. (7) + +The sixteen separate coordinate terms give I_16 and cost 16*8 = 128, +independently of the cross forms. This proves attainment. + +## An explicit case outside the prior sufficient test + +Use the actual retained geometry. Its annihilators, as nine-bit integers, +are + + r = [129,65,209,17,197,5,149,85], + s = [33,289,297,41,267,11,3,259]. + +Let e = 1, the first binary coordinate vector, and set + + beta01 = r_0 e^T, + beta10 = r_1 s_0^T + e s_1^T. + +Their row arrays are respectively + + [1,0,0,0,0,0,0,1,0], + [256,0,0,0,0,0,33,0,0]. + +The global ranks are (1,2), while both minimum coordinate-support cross +ranks are zero. The forward restriction vanishes on U_0. The reverse +restriction vanishes on U_1 x V_1. Its two left vectors and two right +vectors are independent, so its global rank is two. PR2395's sufficient +test c01+c10 >= min(8,r01,r10) reads 0 >= 1 and abstains here. The theorem +above proves the exact minimum 128 for this example and its whole family. + +This does not settle the entire rank-(1,2) class. It excludes this +exceptional-hull way of exploiting the zero pure prices. + +## Evidence boundary and credit + +The arbitrary-complex-factorization theorem is a written scoped proof. +The verifier derives the eight normals from the pinned geometry, checks +8,192 transfer instances and all 6,561 choices of the fixture's four +support spans, including full spans. It checks the fixture's ranks and +zero minima, the coordinate attainer, and two actual price-15 doubles +after removing the respective geometric hypotheses. It does not rerun +the inherited complete support census or enumerate complex decoders. + +JoyboyBrian's adjacent PR5141, head +`b75399c455aa24f21ec9c78c337c3c277efd177d`, proves the full rank-(1,1) +floor. Its mixed-orientation argument covers a rank-one reverse form +with one exceptional source functional. Equations (3)-(5) extend that +argument to a reverse row space in their linear span, giving new +higher-rank cases. No PR5141 code or theorem is a runtime dependency. + +The inherited model and support/count lemmas retain Sagar Thakrar, +commdata2338, alephnan, Mihir Srivastava and Adam Gall's credit. The new +exceptional-hull extension and package were produced by Nick Petalas. +Apache-2.0. Independent human and formal proof-kernel review are unclaimed. diff --git a/research/p112-exceptional-hull-floor/README.md b/research/p112-exceptional-hull-floor/README.md new file mode 100644 index 0000000000..45f7e15180 --- /dev/null +++ b/research/p112-exceptional-hull-floor/README.md @@ -0,0 +1,105 @@ +# A sharp P112 floor for exceptional-hull cross forms + +The new [scoped proof](PROOF.md) gives exact two-call COPY cost **128** when +`beta01 = r_i v^T` and the reverse form's row space lies in the binary span +of the eight exceptional source annihilators. The reverse form may have +rank greater than one. Every double term then costs at least 16, because +its Schur feedback vanishes. + +The explicit rank-(1,2) fixture has minimum pure cross prices `(0,0)`. +Thus commdata2338's [PR2395](https://github.com/CrocSwap/integer-mult-bounds/pull/2395) +sufficient test abstains, while this theorem proves the sharp floor. +The new result excludes this exceptional-hull subfamily of PR2395's open +rank-(1,2) cases. It does not settle that entire rank pair. + +This contribution was produced by Nick Petalas. Apache-2.0. +Independent human and formal proof-kernel review are unclaimed. + +## Reproduction and evidence + +From the repository root, use CPython 3.12, standard library only: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B scripts/research_package.py --package research/p112-exceptional-hull-floor +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/p112-exceptional-hull-floor/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B scripts/check_research_commit.py --package research/p112-exceptional-hull-floor --check-source-history +``` + +The portable interpreter spelling is `python3.12 -W error -B`. Run the +publication preflight after committing. The registered normal and optimized +commands print a generated JSON receipt bound to the package and live-source +hashes, followed by + +```text +PASS_P112_EXCEPTIONAL_HULL transfer=8192 doubles=6561 floor=128 controls=2 +``` + +Local replay used CPython 3.12.15 on macOS arm64. Both registered commands +passed. Hosted CI is recorded in the PR body when available. + +The 8,192 transfer checks cover all eight forward exceptional choices, +eight reader restrictions, eight source restrictions and sixteen elements +of the source-normal span. The 6,561 double cases cover all nine possible +support spans in each of four positions for the explicit fixture. They +have minimum price 16. The sixteen coordinate terms attain 128. + +Two hypothesis-removal controls exhibit actual price-15 doubles. They +show why the new double-price argument needs its geometric hypotheses; +they do not exhibit a sub-128 exact decoder. The written proof supplies +the universal implication for arbitrary complex factors. No solver, Lean, +native operator replay or multiplier replay is required or claimed. + +## Sources and related work + +The base is `a5df48c55ea806d7952b65acc9c76d878ff09b13`, priority revision 7. +[SOURCES.json](SOURCES.json) pins the actual geometry and PR2395 proof. +PR2395, head `361de309e5fc05f83862f0b6c611210eda9837a1`, supplies the support +classification, within-call floor and coefficient incidence count. Sagar +Thakrar's [PR2294](https://github.com/CrocSwap/integer-mult-bounds/pull/2294) +supplies the arbitrary directed cross-form model, following alephnan's +PR1714 and the support work of Mihir Srivastava and Adam Gall. + +JoyboyBrian's [PR5141](https://github.com/CrocSwap/integer-mult-bounds/pull/5141), +head `b75399c455aa24f21ec9c78c337c3c277efd177d`, settles rank-(1,1). Its +mixed-orientation calculation is the adjacent rank-one predecessor. The +new step closes the reverse functional under linear span and thereby +allows higher reverse rank. Its proof and verifier are not imported. + +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19144293) +is the canonical investigation record. The catalogue card +`formal-interface-lemma` is changed to this written interface proof, with +no claim of proof-assistant formalization. + +## Limitations + +The inherited support theorem is a cited premise. This package computes +only the geometry needed for the new transfer and fixture, rather than +rechecking that theorem. The union rank price is the separate-total +two-call root-code model. Physical chart realization, dirty restoration, +hosting, precision, rank-power costs, recursive admission and integer +multiplication remain outside scope. The selected frontier is unchanged. + +## Open next questions + +1. Settle the rank-(1,2) cases outside this exceptional-hull family. First + classify which coordinate restrictions give nonzero Schur feedback; + then couple those discounts to the paid pure terms. Arbitrary complex + coefficient cancellation remains the obstacle. +2. Can a legal physical cross-form interface realize any surviving + discounted pairing? Start with one explicit form and charge its chart + conversions and cleanup. A binary form alone supplies no implementation. + +## Verifier bounds + +The verifier uses structured control flow, fixed finite domains and no +recursion or code generation. Every function is shorter than 60 lines. +Checks use explicit exceptions and remain active under optimization. +The diagnostics command is Python's warning-strict replay in both modes. + +Power-of-ten rule 3 has a CPython runtime deviation in `verify.py`. +Integers, JSON parsing and lists allocate dynamically. Input files are capped +at 2 MiB; the root table is 112-by-8, and the largest pairing is 18-by-18 +binary. The 6,561-case enumeration retains one pairing at a time. The +normal and optimized replays exercise this bound. A fixed-memory port +would be needed only if this finite offline verifier becomes an embedded +runtime requirement. No shared library or predecessor file is changed. diff --git a/research/p112-exceptional-hull-floor/SOURCES.json b/research/p112-exceptional-hull-floor/SOURCES.json new file mode 100644 index 0000000000..4b50fae344 --- /dev/null +++ b/research/p112-exceptional-hull-floor/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13", + "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/p112-cross-form-rank-tradeoff/PROOF.md", + "usage": "input", + "git_blob": "f29d1c7c189e2c1addb81001b7266a80a828db47", + "sha256": "91c7e68d2b93354a5a041e62408ec592e73167c7176816e7e53f6ae27c3b9bfb" + }, + { + "path": "research/p112-single-lift/reference-geometry.json", + "usage": "input", + "git_blob": "d862663d3c0ffe3c72df510e89997beb85cef640", + "sha256": "4f44af368e046002553d632ee90c6470990827cea3fae41f0f54018522d7a080" + } + ] +} diff --git a/research/p112-exceptional-hull-floor/TASK.json b/research/p112-exceptional-hull-floor/TASK.json new file mode 100644 index 0000000000..c7d84f49ec --- /dev/null +++ b/research/p112-exceptional-hull-floor/TASK.json @@ -0,0 +1,101 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove a sharp 128 COPY-rank floor for two-call P112 cross forms beta01=r_i v^T and rowspace(beta10) contained in the exceptional source-normal span, including an undecided rank-(1,2) fixture.", + "scope_change_reason": "The card asks for formalization. This contribution instead proves a new scoped binary transfer implication left open by PR2395, with a written proof and exact finite evidence. No kernel formalization is claimed.", + "bottleneck_link": "The new double-term price rules out an exceptional-hull route to sub-128 two-call COPY, directing residual searches toward cross forms outside this family.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved higher-rank case and package it; do not extend to arbitrary residual rank pairs.", + "outcome": "completed", + "evidence": "Written Schur-feedback proof; 8192 transfer instances; 6561 support-span double matrices for a rank-(1,2), minimum-(0,0) fixture; sharp 128 coordinate attainer; two price-15 hypothesis-removal controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can rank-(1,2) cross forms outside the exceptional-hull family beat total COPY price 128?", + "why_it_matters": "The new theorem excludes a subfamily but leaves the full residual pair open.", + "first_step": "Classify nonzero Schur feedback at coordinate restrictions, then couple double discounts to pure coefficient ranks.", + "blocked_by": "Arbitrary complex coefficient cancellation and support-price coupling." + }, + { + "question": "Can a surviving discounted cross form be realized by a legal paid physical interface?", + "why_it_matters": "Binary rank prices alone do not give a supplier or kappa improvement.", + "first_step": "Name one explicit cross form and charge chart conversions and dirty cleanup.", + "blocked_by": "A physical realization and complete producer/consumer bill are absent." + } + ] +} diff --git a/research/p112-exceptional-hull-floor/VERIFY.json b/research/p112-exceptional-hull-floor/VERIFY.json new file mode 100644 index 0000000000..0b73b6a200 --- /dev/null +++ b/research/p112-exceptional-hull-floor/VERIFY.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p112-cross-form-rank-tradeoff/PROOF.md", + "research/p112-single-lift/reference-geometry.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "New exceptional-hull transfer, rank-(1,2) fixture over all 6561 support choices, sharp coordinate attainer, two hypothesis-removal controls and hash-bound generated receipt." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same new proof evidence with optimization enabled and explicit checks retained." + } + ] +} diff --git a/research/p112-exceptional-hull-floor/verify.py b/research/p112-exceptional-hull-floor/verify.py new file mode 100644 index 0000000000..2bdece390c --- /dev/null +++ b/research/p112-exceptional-hull-floor/verify.py @@ -0,0 +1,176 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Exact new transfer checks; the inherited support theorem is a premise.""" + +import hashlib +import itertools +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +WIDTH = 9 +MASK = (1 << WIDTH) - 1 +MAX_FILE_BYTES = 2 * 1024 * 1024 + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def parity(value): + return value.bit_count() & 1 + + +def read_bytes(path): + need(path.stat().st_size <= MAX_FILE_BYTES, "input exceeds 2 MiB") + return path.read_bytes() + + +def basis(rows, width=WIDTH): + """At most len(rows)*width eliminations, with bounded integer rows.""" + pivots = [0] * width + for original in rows: + need(0 <= original < (1 << width), "row range") + row = original + for bit in range(width - 1, -1, -1): + if (row >> bit) & 1: + if pivots[bit]: + row ^= pivots[bit] + else: + pivots[bit] = row + break + return tuple(row for row in pivots if row) + + +def outer(left, right): + return tuple(right if (left >> bit) & 1 else 0 for bit in range(WIDTH)) + + +def form(matrix, left, right): + image = sum(parity(row & right) << bit for bit, row in enumerate(matrix)) + return parity(left & image) + + +def block_rows(matrix, readers, sources): + return tuple(sum(form(matrix, left, right) << bit + for bit, right in enumerate(sources)) for left in readers) + + +def restricted_rank(matrix, readers, sources): + return len(basis(block_rows(matrix, readers, sources))) + + +def double_rank(forward, reverse, u0, v0, u1, v1): + ident = tuple(1 << bit for bit in range(WIDTH)) + a, b = block_rows(ident, u0, v0), block_rows(forward, u0, v1) + c, d = block_rows(reverse, u1, v0), block_rows(ident, u1, v1) + rows = tuple(x | (y << len(v0)) for x, y in zip(a, b)) + rows += tuple(x | (y << len(v0)) for x, y in zip(c, d)) + return len(basis(rows, 2 * WIDTH)) + + +def inputs(): + manifest = json.loads(read_bytes(HERE / "SOURCES.json")) + for item in manifest["files"]: + if item["usage"] == "input": + digest = hashlib.sha256(read_bytes(ROOT / item["path"])).hexdigest() + need(digest == item["sha256"], "source hash: " + item["path"]) + data = json.loads(read_bytes(ROOT / "research/p112-single-lift/reference-geometry.json")) + roots, readers, sources = data["X"], data["duals"], data["labels"] + need(len(roots) == len(readers) == len(sources) == 112, "geometry shape") + need(all(len(row) == 8 for row in roots), "root width") + u = tuple(basis([label for row, label in zip(roots, readers) if row[j]]) + for j in range(8)) + v = tuple(basis([label for row, label in zip(roots, sources) if row[j]]) + for j in range(8)) + r, s = [], [] + for spaces, normals in ((u, r), (v, s)): + for space in spaces: + need(len(space) == 8, "coordinate support dimension") + annihilators = [h for h in range(1, MASK + 1) + if all(parity(h & row) == 0 for row in space)] + need(len(annihilators) == 1, "unique coordinate annihilator") + normals.append(annihilators[0]) + return u, v, tuple(r), tuple(s) + + +def transfer_checks(r, s): + hull = basis(s) + span = tuple(value for value in range(MASK + 1) + if len(basis(hull + (value,))) == len(hull)) + need(len(span) == 16, "exceptional source hull size") + checks = 0 + for reader, row_normal, source_normal, source in itertools.product(r, r, s, span): + z = reader ^ (row_normal if parity(reader & source_normal) else 0) + need(parity(z & source_normal) == 0, "projected vector is in source space") + need(parity(source & z) == 0, "reverse Schur transfer vanishes") + checks += 1 + return checks + + +def fixture_checks(u, v, r, s): + forward = outer(r[0], 1) + reverse = tuple(a ^ b for a, b in zip(outer(r[1], s[0]), outer(1, s[1]))) + need((len(basis(forward)), len(basis(reverse))) == (1, 2), "fixture global ranks") + minima = tuple(min(restricted_rank(matrix, left, right) for left in u for right in v) + for matrix in (forward, reverse)) + need(minima == (0, 0), "prior sufficient test must abstain") + full = tuple(1 << bit for bit in range(WIDTH)) + count, minimum = 0, 2 * WIDTH + for u0, v0, u1, v1 in itertools.product(u + (full,), v + (full,), repeat=2): + cost = double_rank(forward, reverse, u0, v0, u1, v1) + need(cost >= 16, "fixture double price") + minimum = min(minimum, cost) + count += 1 + need(count == 6561 and minimum == 16, "fixture domain and sharp double price") + ident = tuple(1 << bit for bit in range(WIDTH)) + attainer = sum(restricted_rank(ident, u[j], v[j]) for j in range(8)) * 2 + need(attainer == 128, "sixteen coordinate-term attainer") + return {"forward": list(forward), "reverse": list(reverse), + "ranks": [1, 2], "minima": list(minima), "double_cases": count, + "minimum_double_price": minimum, "attaining_cost": attainer} + + +def controls(u, v, r, s): + # Each removed geometric hypothesis admits an actual price-15 double. + off_source = next(1 << bit for bit in range(WIDTH) + if any(parity((1 << bit) & (r[0] ^ row)) for row in r)) + off_reader = next(1 << bit for bit in range(WIDTH) + if any(parity((1 << bit) & (s[0] ^ row)) for row in s)) + pairs = ((outer(r[0], off_source), outer(r[1], off_source)), + (outer(off_reader, s[0]), outer(off_reader, s[1]))) + witnesses = [] + for forward, reverse in pairs: + witness = None + for indices in itertools.product(range(8), repeat=4): + a, b, c, d = indices + if double_rank(forward, reverse, u[a], v[b], u[c], v[d]) == 15: + witness = list(indices) + break + need(witness is not None, "hypothesis-removal price-15 control") + witnesses.append(witness) + return witnesses + + +def main(): + u, v, r, s = inputs() + need(all(parity(a & b) == 1 for a in r for b in s), "exceptional cross pairings") + result = {"reader_normals": list(r), "source_normals": list(s), + "transfer_checks": transfer_checks(r, s), + "fixture": fixture_checks(u, v, r, s), + "control_witnesses": controls(u, v, r, s)} + need(result["transfer_checks"] == 8192, "transfer domain size") + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + hashes = {name: hashlib.sha256(read_bytes(HERE / name)).hexdigest() for name in names} + manifest = json.loads(read_bytes(HERE / "SOURCES.json")) + for item in manifest["files"]: + if item["usage"] == "input": + hashes[item["path"]] = hashlib.sha256(read_bytes(ROOT / item["path"])).hexdigest() + print(json.dumps({"result": result, "sha256": hashes}, sort_keys=True)) + print("PASS_P112_EXCEPTIONAL_HULL transfer=8192 doubles=6561 floor=128 controls=2") + + +if __name__ == "__main__": + main()