From 19f6c9e5962ae11519661d070c3bdcd3aa6537a3 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Wed, 11 Nov 2026 13:27:36 +0000 Subject: [PATCH] feat(research): prove sharp two-for-one terminal exchange --- research/bit-terminal-two-for-one/PROOF.md | 124 +++++++++++ research/bit-terminal-two-for-one/README.md | 70 ++++++ .../bit-terminal-two-for-one/SOURCES.json | 28 +++ research/bit-terminal-two-for-one/TASK.json | 77 +++++++ research/bit-terminal-two-for-one/VERIFY.json | 32 +++ research/bit-terminal-two-for-one/verify.py | 205 ++++++++++++++++++ 6 files changed, 536 insertions(+) create mode 100644 research/bit-terminal-two-for-one/PROOF.md create mode 100644 research/bit-terminal-two-for-one/README.md create mode 100644 research/bit-terminal-two-for-one/SOURCES.json create mode 100644 research/bit-terminal-two-for-one/TASK.json create mode 100644 research/bit-terminal-two-for-one/VERIFY.json create mode 100644 research/bit-terminal-two-for-one/verify.py diff --git a/research/bit-terminal-two-for-one/PROOF.md b/research/bit-terminal-two-for-one/PROOF.md new file mode 100644 index 0000000000..d49af4cb43 --- /dev/null +++ b/research/bit-terminal-two-for-one/PROOF.md @@ -0,0 +1,124 @@ +# Sharp terminal capacity with changed unmarked arrivals + +This theorem concerns a binary rank relaxation. It constructs synthetic source +libraries. It neither implements a native operation nor changes the selected frontier. + +## Model + +Work over F_2. An old terminal basis of W consists of n unmarked vectors +u_1,...,u_n, b base vectors a_1,...,a_b, and s singleton vectors p_1,...,p_s. +Write U=span(u), B=span(a), and m=b+s. A marked payload changes from v to v+d_v. +The fixed allowed difference libraries obey + +* d_a belongs to U+B for each of the b base positions; +* d_pi belongs to U+span(p_i) for each singleton position. + +These are containment hypotheses. Libraries may be proper subspaces. At most h +of the n unmarked arrivals may change arbitrarily within W. All n+m final +arrivals must form a basis of W. Let U' span the n final unmarked arrivals. +Return stock is the dimension of the span of the marked differences in W/U'. +Reconstruction from the final basis is free. The model promises no chronological +program, restored named output or paid realization. + +## Upper bound, credited context + +ToikY's [PR #7258 NEXT.md](https://github.com/ToikY/integer-mult-bounds/blob/90a63fbefcf79c3e0c0453ef0741dff8517b6167/research/bit-fixed-payload-quotient-bound/NEXT.md) +gives the b=12, s=10 instance of this dimension bound. Its literal library census +and prices are cited results, not verified here. The short argument below fixes +the exact abstraction for the new sharpness theorem. + +Let k count singleton differences whose image in W/U is p_i. Their new marked +arrivals vanish in W/U, since p_i+p_i=0. Other marked arrivals have joint quotient +rank at most b+s-k. The h changed unmarked arrivals add at most h quotient +dimensions. Full terminal rank implies k<=h. + +All differences have rank at most b+k modulo U. Both U and U' have dimension n +and share the n-h unchanged unmarked basis vectors. Thus dim(U/(U intersect U'))<=h. +For every subspace X of W, + + dim((X+U')/U') <= dim((X+U)/U) + dim(U/(U intersect U')). + +Indeed, project (X+U+U')/U' onto (X+U+U')/(U+U'). Its kernel has dimension +dim(U/(U intersect U')); its image is a quotient of (X+U)/U. Apply this to the +span of the differences. Return stock is at most b+k+h, hence min(m,b+2h). + +F_2 matters. Over F_3 even a lone marked position with d=p has a nonzero new +arrival 2p, without any changed unmarked arrival. + +## New attaining construction + +For every even b>=0, every n,s>=0 and 0<=h<=n, the upper bound + + maximum return stock = min(b+s, b+2h) + +is attained with the fixed maximal libraries U+B and U+span(p_i). The same +libraries serve every budget h. Only the chosen payloads and unmarked arrivals +vary. There is no stronger universal bound from these dimension and singleton +containment hypotheses alone. + +For one unmarked vector u and two singleton vectors p,q, choose + + old unmarked u -> new unmarked p+q + marked p -> new marked u with d_p=p+u + marked q -> new marked q+u with d_q=u. + +Both differences belong to their fixed singleton libraries. The new arrivals +(p+q,u,q+u) are a basis. From their values (x,y,z), recover + + u=y, q=z+y, p=x+z+y. + +Modulo U'=span(p+q), the differences p+u and u are independent. In an equality +alpha(p+u)+beta u=gamma(p+q), the q coefficient forces gamma=0, then the p +coefficient forces alpha=0, and finally beta=0. One changed unmarked arrival +therefore earns two independent difference directions. + +For one remaining singleton p, use u->p and p->u, with d_p=p+u. This earns one +direction modulo the new unmarked span. Leave other singletons and unmarked +arrivals unchanged. Use min(h,floor(s/2)) disjoint three-vector gadgets, followed +by the two-vector gadget only when s is odd and budget remains. They earn exactly +min(s,2h) directions. Disjoint supports make both the endpoint bases and quotient +directions combine by direct sum. + +For every pair of base vectors a,c, choose d_a=c and d_c=a+c. New arrivals are +a+c and a. Both difference and arrival pairs are bases. These disjoint blocks earn +all b base directions with no unmarked changes and no intersection with the +singleton gadgets. This proves the formula. + +## The 523+22 shape and its boundary + +For n=523, b=12 and s=10, the synthetic construction has terminal rank 545 and +return stocks 12,14,16,18,20,22 at budgets h=0,1,2,3,4,5. All 523 new unmarked +arrivals remain independent. No extra arrival slot is used. + +It can retain the base support partition 3+3+2+4 reported by #7258. A three-vector +base block uses differences (c,d,a+c) on (a,c,d). New arrivals are +(a+c,c+d,a+c+d); both triples have determinant one. The two-vector block above +and its direct sum handle sizes two and four. The partition itself therefore +cannot exclude the synthetic attainment. + +Five changed unmarked arrivals suffice for stock 21 or 22 in this abstraction, +and four cannot suffice. This proves sharpness of the source's dimension-only +necessary condition. It does not assert that five actual BIT arrivals have these +payloads, that actual singleton libraries contain the required u components, or +that free basis reconstruction has an affordable legal caller. Those are the next +discriminating constraints. This package does not enumerate the source's 523 ports +or recheck its stock values. + +## Finite corroboration and implementation bounds + +The verifier checks every constructed endpoint and quotient stock by binary +elimination. Small instances also use an independent span-cardinality oracle. +It enumerates every unmarked replacement and allowed difference in ten complete +small maximal-singleton models. These are complete finite certificates for their +declared domains; the written direct-sum argument supplies the all-size scoped proof. + +Every loop has a finite domain. Ambient dimension is at most 545; rank calls have +at most 1,090 rows. Span sets have at most 64 elements in the construction checks +and 32 in the complete models. The largest complete model has 16,384 assignments. The construction +sweep fixes n<=4, b in {0,2,4,6,12}, s<=10, h<=n, then checks six 545-dimensional +witnesses. Functions stay below 60 lines. Explicit exceptions keep checks active +under optimized Python. Python integer, container, JSON and hashing allocation is +a managed-runtime deviation from fixed steady-state allocation; the finite +dimensions above bound live mathematical state. No recursion, dynamic code, +external process or third-party dependency is used. Warning-strict execution +supplies interpreted diagnostics. diff --git a/research/bit-terminal-two-for-one/README.md b/research/bit-terminal-two-for-one/README.md new file mode 100644 index 0000000000..e7367124a2 --- /dev/null +++ b/research/bit-terminal-two-for-one/README.md @@ -0,0 +1,70 @@ +# Sharp two-for-one terminal exchange + +Scoped written proof with exact finite corroboration, produced by Nick Petalas. + +In the binary terminal-rank relaxation with n unmarked arrivals, b base marked +directions, s singleton marked directions and at most h changed unmarked +arrivals, the universal stock bound min(b+s,b+2h) is sharp for every even b. +One three-vector exchange earns two independent marked differences while +changing one unmarked arrival. Fixed libraries suffice for every budget. + +For the synthetic 523+22 shape with b=12 and s=10, five changed unmarked +arrivals attain stock 22 and preserve terminal rank 545. The construction also +respects the base support partition 3+3+2+4. Consequently the dimension-only +argument in [ToikY #7258](https://github.com/CrocSwap/integer-mult-bounds/pull/7258) +cannot raise its five-arrival necessary condition. An obstruction beyond it must +use actual source libraries, donor projections, scheduling or costs. + +These are synthetic libraries. No claim of stock 22 on the literal BIT word, +physical delivery, native admission, complete multiplication theorem or new +kappa follows. The selected frontier and its five assumptions are unchanged. + +The [proof](PROOF.md) defines the relaxation, credits the predecessor upper bound, +and proves attainment. The standalone verifier constructs endpoints, checks full +rank and quotient rank, and exhausts every assignment in ten small singleton +models with an independent span oracle. It generates a receipt with source +hashes. No predecessor scientific verifier runs. + +Local CPython 3.12.15 verification covers 825 small construction cases, six +545-dimensional witnesses and all 26,286 assignments in the ten complete models. +Four mathematical controls and three invalid-parameter controls pass. + +## Reproduce + +From the repository root, using CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error scripts/research_package.py --package research/bit-terminal-two-for-one +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/bit-terminal-two-for-one/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/bit-terminal-two-for-one --check-modes --check-source-history +``` + +Registered normal and optimized checks have 120-second bounds. Direct verification +prints its generated hash-bound receipt. An optional `--receipt` path must be +outside the checkout. Runtime needs only the standard library and package files; +the source-history check additionally needs full Git history. + +## Open next questions + +Determine whether funded changed paths or expanded marked libraries can realize +even one three-vector gadget with the required shared U component and quotient +projection. Concurrent [#7260](https://github.com/CrocSwap/integer-mult-bounds/pull/7260) +studies actual old-source donor constraints, unlike this maximal-library relaxation. +Use its source-pinned donor map as a cited starting point rather than repeating +its census. A legal paid schedule, joint endpoint, ownership, restoration and +the complete invoice remain separate obligations. +The structured question is in [TASK.json](TASK.json). + +## Credit and source context + +The new exchange, sharpness theorem and verifier were produced by Nick Petalas. +Credit ToikY's #7258, exact head `90a63fbefcf79c3e0c0453ef0741dff8517b6167`, +for the 12+2h upper bound, singleton/base partition and altered-unmarked-arrival +route. Its census and prices are cited inputs, not deliverables rechecked here. +Credit Jerry Chen / CubeJerry #7001/#6726 and their retained contributors for the +BIT word motivating that route, and Clear1nsight #7244 for its complete comparison. +Binary elimination, rank-nullity and direct sums are classical methods. + +[SOURCES.json](SOURCES.json) records immutable main provenance and the exact public +predecessor path and hash. There are no external runtime inputs. Independent human +and formal proof-kernel review are unclaimed. New work is Apache-2.0. diff --git a/research/bit-terminal-two-for-one/SOURCES.json b/research/bit-terminal-two-for-one/SOURCES.json new file mode 100644 index 0000000000..16ad5b8b40 --- /dev/null +++ b/research/bit-terminal-two-for-one/SOURCES.json @@ -0,0 +1,28 @@ +{ + "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" + } + ], + "external_provenance": [ + { + "repository": "ToikY/integer-mult-bounds", + "commit": "90a63fbefcf79c3e0c0453ef0741dff8517b6167", + "path": "research/bit-fixed-payload-quotient-bound/NEXT.md", + "url": "https://github.com/ToikY/integer-mult-bounds/blob/90a63fbefcf79c3e0c0453ef0741dff8517b6167/research/bit-fixed-payload-quotient-bound/NEXT.md", + "sha256": "67e11381abef156fb3d24da94c53a4ee74fbbc2140638be98278a49c67b8a364", + "usage": "credited mathematical context; no runtime import or predecessor replay" + } + ] +} diff --git a/research/bit-terminal-two-for-one/TASK.json b/research/bit-terminal-two-for-one/TASK.json new file mode 100644 index 0000000000..602b96472b --- /dev/null +++ b/research/bit-terminal-two-for-one/TASK.json @@ -0,0 +1,77 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "bit-helper-contract", + "question": "Can a changed G20 helper path or independent-target split improve the complete BIT moment without losing its physical endpoint?", + "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", + "research/g20-helper-split/README.md", + "research/g20-conjugation-admission/README.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 full boundary contract and paid profile; unchanged scalar counts alone are insufficient. 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", + "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": "First read #5679/#5708 and their audits as pending component proposals. Choose one uncovered helper group/cut on an exact word; compare arbitrary-input native action, targets, owned storage, both orientations and full signed bill. Stop if the gain is only a scalar count or repaid by lost targets. Do not rerun the frozen #5609 common-frame domain without changing its hypothesis.", + "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": [ + "G20", + "helper split", + "5679", + "5708", + "independent target" + ], + "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": "Prove sharpness of the binary dimension-only terminal stock bound min(b+s,b+2h) by a fixed-library exchange construction.", + "scope_change_reason": "The predecessor leaves altered unmarked arrivals open. This isolates the rank relaxation before any actual donor census, rather than auditing the predecessor or attempting an unpriced native construction.", + "bottleneck_link": "A stronger BIT terminal obstruction must use actual source libraries, donor projections or costs if the dimension-only relaxation is sharp. This is a local interface result, not a complete supplier.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified exchange and sharpness theorem; do not extend to the actual port census.", + "outcome": "completed", + "evidence": "PROOF.md and the standalone exhaustive verifier. Generated hash-bound receipts print to stdout or an external path.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can funded changed paths or expanded marked libraries realize a three-vector exchange with the required shared U component and distinct terminal ports?", + "why_it_matters": "The abstract dimension bound cannot distinguish this route from a feasible rank endpoint.", + "first_step": "Use the exact source-constrained donor map in concurrent PR7260 as a cited input, then test funded new paths or changed marked libraries against the explicit gadget and full endpoint. Do not repeat its census.", + "blocked_by": "Actual fixed marked libraries, donor projections, eligible distinct funded slots, legal chronology, ownership, restoration and complete costs." + } + ] +} diff --git a/research/bit-terminal-two-for-one/VERIFY.json b/research/bit-terminal-two-for-one/VERIFY.json new file mode 100644 index 0000000000..27cc03d10f --- /dev/null +++ b/research/bit-terminal-two-for-one/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Construct full-rank terminal bases and sharp quotient stock; exhaust ten small singleton models with independent elimination/span ranks; reject invalid parameters and lost endpoint rank." + }, + { + "argv": [ + "{python}", + "-B", + "-O", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat every mathematical check with optimized Python; explicit exceptions must retain all checks." + } + ] +} diff --git a/research/bit-terminal-two-for-one/verify.py b/research/bit-terminal-two-for-one/verify.py new file mode 100644 index 0000000000..848f98d170 --- /dev/null +++ b/research/bit-terminal-two-for-one/verify.py @@ -0,0 +1,205 @@ +#!/usr/bin/env python3 +"""Exact binary endpoint constructions and complete small singleton models.""" + +import argparse +import hashlib +import itertools +import json +from pathlib import Path +import platform + +MAX_DIMENSION = 545 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def rank(rows, width): + require(0 <= width <= MAX_DIMENSION, "rank width outside finite check domain") + require(len(rows) <= 2 * MAX_DIMENSION, "too many rank rows") + pivots = [0] * width + result = 0 + for original in rows: + require(isinstance(original, int) and 0 <= original < 1 << width, + "rank row outside binary ambient space") + row = original + for bit in range(width - 1, -1, -1): + if not row >> bit & 1: + continue + if pivots[bit]: + row ^= pivots[bit] + else: + pivots[bit] = row + result += 1 + break + return result + + +def span_rank(rows, width): + """Independent exhaustive span cardinality, only in small ambient spaces.""" + require(0 <= width <= 6, "span oracle is restricted to six dimensions") + span = {0} + for row in rows: + require(0 <= row < 1 << width, "span row outside binary space") + span |= {value ^ row for value in span} + size = len(span) + require(size & (size - 1) == 0, "binary span size must be a power of two") + return size.bit_length() - 1 + + +def base_differences(n, b): + """Use the predecessor support partition 3+3+2+4 when b=12.""" + blocks = (3, 3, 2, 4) if b == 12 else (2,) * (b // 2) + differences = [] + offset = n + for size in blocks: + if size == 3: + a, c, d = (1 << (offset + j) for j in range(3)) + differences.extend((c, d, a ^ c)) + else: + for j in range(0, size, 2): + a, c = 1 << (offset + j), 1 << (offset + j + 1) + differences.extend((c, a ^ c)) + offset += size + require(len(differences) == b, "base block dimension mismatch") + return tuple(differences) + + +def construction(n, b, s, h): + require(0 <= h <= n <= 523 and b in (0, 2, 4, 6, 12), + "construction parameters outside the registered check domain") + width = n + b + s + require(0 <= s <= 10 and width <= MAX_DIMENSION, "invalid singleton count") + unmarked = [1 << j for j in range(n)] + differences = list(base_differences(n, b)) + [0] * s + pairs = min(h, s // 2) + for j in range(pairs): + u = 1 << j + a, c = 1 << (n + b + 2 * j), 1 << (n + b + 2 * j + 1) + unmarked[j] = a ^ c + differences[b + 2 * j] = a ^ u + differences[b + 2 * j + 1] = u + if s % 2 and h > pairs: + u, a = 1 << pairs, 1 << (n + b + 2 * pairs) + unmarked[pairs] = a + differences[b + 2 * pairs] = a ^ u + marked = tuple((1 << (n + j)) ^ d for j, d in enumerate(differences)) + return tuple(unmarked), marked, tuple(differences) + + +def check_construction(n, b, s, h): + unmarked, marked, differences = construction(n, b, s, h) + width = n + b + s + require(rank(unmarked, width) == n, "unmarked arrivals lost rank") + require(rank(unmarked + marked, width) == width, "terminal endpoint lost rank") + changed = sum(row != 1 << j for j, row in enumerate(unmarked)) + require(changed <= h, "unmarked change budget exceeded") + base_mask = (1 << (n + b)) - 1 + require(all(row & ~base_mask == 0 for row in differences[:b]), + "base difference escaped its fixed library") + for j in range(s): + allowed = ((1 << n) - 1) | (1 << (n + b + j)) + require(differences[b + j] & ~allowed == 0, "singleton library escaped") + stock = rank(unmarked + differences, width) - n + require(stock == min(b + s, b + 2 * h), "sharp construction missed capacity") + if width <= 6: + require(span_rank(unmarked + marked, width) == width, + "independent span oracle rejects endpoint") + require(span_rank(unmarked + differences, width) - n == stock, + "independent span oracle rejects stock") + return {"unmarked": n, "base": b, "singletons": s, "budget": h, + "changed": changed, "stock": stock} + + +def exhaustive_singletons(n, s): + """Enumerate every unmarked replacement and every maximal-library choice.""" + width = n + s + require((n == 0 and 1 <= s <= 4) or (n == 1 and 1 <= s <= 4) + or (n == 2 and 1 <= s <= 2), "unregistered exhaustive domain") + libraries = tuple(tuple(u | (coefficient << (n + j)) + for coefficient in range(2) for u in range(1 << n)) + for j in range(s)) + maxima = [-1] * (n + 1) + endpoints = [0] * (n + 1) + checked = 0 + for unmarked in itertools.product(range(1 << width), repeat=n): + changed = sum(row != 1 << j for j, row in enumerate(unmarked)) + for differences in itertools.product(*libraries): + checked += 1 + marked = tuple((1 << (n + j)) ^ d for j, d in enumerate(differences)) + endpoint_rank = span_rank(unmarked + marked, width) + if endpoint_rank != width: + continue + require(rank(unmarked + marked, width) == endpoint_rank, + "independent endpoint ranks disagree") + stock = span_rank(unmarked + differences, width) - n + require(rank(unmarked + differences, width) - n == stock, + "independent difference ranks disagree") + endpoints[changed] += 1 + for budget in range(changed, n + 1): + maxima[budget] = max(maxima[budget], stock) + expected = [min(s, 2 * h) for h in range(n + 1)] + require(maxima == expected, "complete singleton model disagrees with theorem") + require(checked == (1 << (width * n)) * (1 << ((n + 1) * s)), + "incomplete enumeration") + return {"unmarked": n, "singletons": s, "assignments": checked, + "endpoints_by_exact_changes": endpoints, "maxima_by_budget": maxima} + + +def controls(): + require(rank((0, 1, 2), 3) == 2, "own-pivot cancellation was accepted") + # Two marked cancellations cannot be rescued by a single changed arrival. + require(rank((6, 1, 1), 3) < 3, "two cancelled singleton pivots accepted") + # With the old unmarked arrival, differences inside U earn no quotient rank. + require(rank((1, 1, 1), 3) - 1 == 0, "old-U payload was credited twice") + # F_3 escapes the binary theorem: d=p keeps p+d nonzero. + require((1 + 1) % 3 == 2, "characteristic-three scope control failed") + rejected = 0 + for arguments in ((1, 0, 2, 2), (1, 1, 2, 0), (524, 0, 0, 0)): + try: + construction(*arguments) + except ValueError: + rejected += 1 + require(rejected == 3, "out-of-domain construction accepted") + return {"mathematical_controls": 4, "invalid_parameter_controls": rejected} + + +def certificate(): + small = [] + for n, b, s in itertools.product(range(5), (0, 2, 4, 6, 12), range(11)): + for h in range(n + 1): + small.append(check_construction(n, b, s, h)) + actual_shape = [check_construction(523, 12, 10, h) for h in range(6)] + census = [exhaustive_singletons(n, s) + for n, upper in ((0, 4), (1, 4), (2, 2)) + for s in range(1, upper + 1)] + return {"schema_version": 1, "claim_type": "scoped proof with finite corroboration", + "construction_cases": len(small), "complete_small_models": census, + "complete_assignments": sum(row["assignments"] for row in census), + "same_dimension_synthetic_witnesses": actual_shape, "controls": controls()} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path) + args = parser.parse_args() + result = certificate() + package = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + hashes = {name: hashlib.sha256((package / name).read_bytes()).hexdigest() for name in names} + payload = json.dumps(result, sort_keys=True, separators=(",", ":")).encode() + receipt = {"result": result, "result_sha256": hashlib.sha256(payload).hexdigest(), + "source_sha256": hashes, "python": platform.python_version()} + rendered = json.dumps(receipt, indent=2, sort_keys=True) + "\n" + if args.receipt: + require(not args.receipt.resolve().is_relative_to(package.parents[1]), + "generated receipts must stay outside the checkout") + require(args.receipt.write_text(rendered, encoding="utf-8") == len(rendered), + "receipt write incomplete") + print("PASS_BIT_TERMINAL_TWO_FOR_ONE " + json.dumps(receipt, sort_keys=True)) + + +if __name__ == "__main__": + main()