diff --git a/research/even-window-saturation-gap/PROOF.md b/research/even-window-saturation-gap/PROOF.md new file mode 100644 index 0000000000..246a8ccc5f --- /dev/null +++ b/research/even-window-saturation-gap/PROOF.md @@ -0,0 +1,139 @@ +# Even-window saturation is impossible from window six onward + +## Statement + +Let `k >= 3`, `T >= 1`, and let `r_1,...,r_v` be nonzero vectors in a real or +complex inner-product space of dimension `T`. Assume there are labels +`p_i` in a `2k`-dimensional symplectic vector space `V` over `F_2` and a nonzero +`w` such that + +1. `b(p_i,w)=1` for every `i`; +2. for distinct `i,j`, `b(p_i,p_j)=0` implies `=0`. + +Repeated labels are allowed. Then + +```text +v <= 2^k T - 1. (1) +``` + +In particular, for the exact nonorthogonality adjacency `A` of a real line +system, if `rank_F2 A=2k` and `1` belongs to `col A`, its even window is `h=2k` +and (1) applies. At `h=6` and `h=8`, respectively, `v=8T` and `v=16T` are +impossible. This answers PR5282's first open next question in the negative. + +The label reduction and the upper bound `v <= 2^k T` are prior work of +DreamingOfClouds in PR2244. Matarener's PR5282 poses the equality question and +explains its relevance to short-window decoder screens. We use those statements +as premises. The new step is the complementary-label projection identity (5). +The proof below also derives the needed counting bound to make its equality +conditions explicit; predecessor vector systems or invoices are not replayed. + +## Affine basis equations + +Put `H={p in V: b(p,w)=1}`. A generator is a maximal totally isotropic +subspace of `V`, hence has dimension `k`. Let `N_j` be the number of generators +in symplectic dimension `2j`, with `N_0=1`. Counting incident nonzero points +and generators gives + +```text +N_j (2^j-1) = (2^(2j)-1) N_(j-1), +N_j = product_(a=1..j) (2^a+1). +``` + +Here generators containing a point correspond to generators of its symplectic +quotient. Write `r=N_(k-1)` and `s=N_(k-2)`, so `r=(2^(k-1)+1)s`. + +Let `G` be the family of generators not containing `w`. Its size is + +```text +|G| = N_k-N_(k-1) = 2^k r. +``` + +Each `L` in `G` meets `H` in an affine hyperplane of `L`, of size `2^(k-1)`. +Indeed, `L=L^perp`, so `w not in L` makes `b(-,w)` a nonzero functional on `L`. +Each point of `H` belongs to `r` members of `G`. Distinct `p,q` in `H` belong +together to `s` members exactly when `b(p,q)=0`, and to none otherwise. +The former count uses the symplectic quotient of the isotropic plane +`span(p,q)`. None of these generators can contain `w`, since `b(p,w)=1`. + +The vectors whose labels lie in any `L` are pairwise orthogonal, including +vectors of the same label. There are at most `T` of them. Sum this inequality +over `G`. Each vector occurs `r` times, so `rv <= 2^k r T`. + +Suppose equality `v=2^k T` holds. Then every one of these finite inequalities +is an equality. The vectors with labels in `L` form an orthogonal basis of +the ambient space for every `L` in `G`. + +For each `p` in `H`, let `E_p` be the orthogonal projection onto the span of +the vectors carrying label `p`. Set it to zero for an unused label. The basis +condition says + +```text +sum_(p in L intersect H) E_p = I for every L in G. (2) +``` + +Summing (2) over all generators gives + +```text +sum_(p in H) E_p = 2^k I. (3) +``` + +## Complementary labels force an impossible projection sum + +Fix `p` in `H` and write `p'=p+w`. These are distinct points of `H` and +`b(p,p')=1`, so no generator contains both. For any other `q` in `H`, + +```text +b(p',q) = b(p,q)+1 in F_2. +``` + +Consequently exactly one of `p,p'` is orthogonal to `q`. Sum equations (2) +over the `2r` generators containing either `p` or `p'`. The two selected labels +occur `r` times each, and every other label occurs `s` times. Therefore + +```text +(r-s)(E_p+E_p') + s sum_(q in H) E_q = 2r I. (4) +``` + +Substitute (3), use `r=(2^(k-1)+1)s`, and divide by `r-s`: + +```text +E_p + E_(p+w) = 2^(2-k) I. (5) +``` + +For `k>=3` the scalar `c=2^(2-k)` lies strictly between zero and one. +Choose any occupied label `p` and a unit vector `x` in the range of `E_p`. +Since orthogonal projections are positive semidefinite, (5) gives + +```text +c = = 1 + >= 1, +``` + +a contradiction. There is an occupied label because `v=2^k T>0`. +Thus equality cannot hold. Since `v` is an integer, (1) follows. + +The restriction `k>=3` matters. At `k=2`, (5) has scalar one and two +complementary nonzero projections satisfy it. The proof makes no assertion +that they extend to an exact line system. This is an algebraic exception, +not a claimed attaining construction. + +## Checkable linear certificate + +The verifier enumerates maximal isotropic subspaces by unique reduced row +echelon bases for `k=2,3,4`. For every unordered pair `{p,p+w}`, it forms an +integer linear combination of the incidence rows of (2): + +```text +r * sum_(L contains p or p+w) row(L) - s * sum_(L in G) row(L). +``` + +Its left side has coefficient `r(r-s)` at the two selected labels and zero +elsewhere. Its right side is `2r^2-s|G|=2rs`. Division gives exactly (5). +This is a finite certificate of the elimination step at the two windows in +the question and the exceptional window four. The all-`k` result comes from +the written incidence argument, not extrapolation from those computations. + +No optimal asymptotic replacement for `2^k` is established. A sequence with +`v/T` tending to `2^k` as `T` increases is not excluded by (1). This result +does not close short windows below their cap, address arbitrary pairings, or +supply a native word, restoration schedule, complete signed invoice or new κ. diff --git a/research/even-window-saturation-gap/README.md b/research/even-window-saturation-gap/README.md new file mode 100644 index 0000000000..a4cc95bfef --- /dev/null +++ b/research/even-window-saturation-gap/README.md @@ -0,0 +1,110 @@ +# No saturated even-window Gram systems at h >= 6 + +Scoped proof with exact finite corroboration, produced by Nick Petalas. + +For a real or complex Gram line system of dimension `T >= 1`, suppose its +nonorthogonality adjacency `A` has `rank_F2 A=2k` and `1 in col A`. For every +`k >= 3`, + +```text +v <= 2^k T - 1. +``` + +Thus a saturated system with `v=8T` at `h=6`, or `v=16T` at `h=8`, does not +exist. This answers [Matarener's PR5282, open question 1](https://github.com/CrocSwap/integer-mult-bounds/pull/5282). +The [proof](PROOF.md) establishes the stronger label-based statement even when +additional orthogonalities are permitted. + +The new step is an equality obstruction. Saturation makes each affine +Lagrangian class an orthogonal basis. Summing those basis equations forces +`E_p + E_(p+w) = 2^(2-k) I` for orthogonal projections onto complementary label +classes. A nonzero projection cannot lie below a scalar smaller than one. + +The prior cap `v <= 2^k T`, its label reduction and the Lagrangian counting +framework belong to DreamingOfClouds's [PR2244](https://github.com/CrocSwap/integer-mult-bounds/pull/2244). +PR5282 poses the equality question and supplies its historical decoder-screen +motivation. Those results are cited premises; no predecessor construction, +invoice or numerical result is audited or replayed here. + +## Evidence and reproduction + +The all-`k` theorem is a written proof. The standard-library verifier constructs +integer linear elimination certificates from independently enumerated RREF +generators. It returns the following finite data: + +- `k=2`: 8 labels, 12 affine generators, 4 pair certificates, scalar `1`. +- `k=3`: 32 labels, 120 affine generators, 16 pair certificates, scalar `1/2`. +- `k=4`: 128 labels, 2160 affine generators, 64 pair certificates, scalar `1/4`. + +It also checks a complementary-projection exception at `k=2`, 30 exact scalar +instances of the idempotent obstruction, and nine rejecting cases. The cases +remove or duplicate a generator, change the partner or scalar, or supply one +of five invalid dimension contracts. Checks use explicit exceptions and remain +active under optimized Python. + +From the repository root, run: + +```sh +~/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/even-window-saturation-gap/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/even-window-saturation-gap/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/even-window-saturation-gap +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/even-window-saturation-gap --check-source-history +``` + +Expected tokens are `PASS_EVEN_WINDOW_SATURATION_GAP`, +`PASS_REGISTERED_RESEARCH_PACKAGE`, and `PASS_RESEARCH_COMMIT_BYTES`. +CPython 3.12 or later suffices; the interpreter path above records the +local environment. The two registered checks each take less than one second +on the local macOS run. This is a runtime bound for these checks, not a claimed +speed improvement. + +An optional `--receipt /absolute/path/outside-the-checkout.json` writes a +generated receipt containing the enumerated data, source hashes, package hashes +and interpreter version. Normal runs only print their result. The contextual +source documents, base commit, catalogue and selected record are pinned in +[SOURCES.json](SOURCES.json). No external library, solver or network is needed. + +## Limits + +This excludes equality, with an integer gap of one. It does not prove an +optimal dimension-independent density gap or exclude near-saturation as `T` +increases. The exception `k=2` is an algebra control, not an attaining exact +line-system construction. Arbitrary pairings and non-Gram decoder matrices are +outside the claim. + +There is no native word, physical delivery, dirty restoration, complete current +signed invoice, supplier admission or new κ. PR5282's historical invoice is not +repriced. The selected frontier and all five retained assumptions are unchanged. +Independent human and formal proof-kernel review are unclaimed. + +## Open next questions + +The structured questions are in [TASK.json](TASK.json). + +- Determine the optimal supremum of `v/T` at `h=6` or `h=8`. Begin with positive + semidefinite deficits in the affine-basis equations. A quantitative deficit + bound is missing; the integer gap here need not survive division by `T`. +- Test a concrete nonsaturated even-window system against a current complex + caller. First specify its literal decoder, targets, paid children and + restoration contract. Native realization, uniform closure and a complete + signed invoice remain blockers. + +## Implementation bounds + +The verifier has no recursion or background processes. The RREF search is +restricted to `2 <= k <= 4`, with at most `256 * 2^16` candidates and at most +256 labels. Functions are below 60 lines and checks survive `-O`. Runtime +allocation is a Python deviation from the fixed-allocation rule. Live storage +is bounded by the finite RREF candidate and generator collections; no unbounded +input can expand the search. A systems-language fixed-buffer implementation +would be needed only if this verifier becomes a memory-constrained component. +Warnings-as-errors, syntax inspection and both registered commands are the +available local diagnostics; no dedicated Python linter or type checker is +installed on PATH. This package changes no shared build configuration. + +## Credit + +The complementary-label equality obstruction, proof and standalone verifier were +produced by Nick Petalas. Credit Matarener for PR5282's question and screen, +DreamingOfClouds for PR2244's line-count and label framework, and the decoder +lineage credited in those unchanged source documents. New work is Apache-2.0. diff --git a/research/even-window-saturation-gap/SOURCES.json b/research/even-window-saturation-gap/SOURCES.json new file mode 100644 index 0000000000..723675da56 --- /dev/null +++ b/research/even-window-saturation-gap/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/line-system-saturation/README.md", + "usage": "input", + "git_blob": "8e998ee15db765ce90d52d53d4a61f3fd75e5dae", + "sha256": "a99a58bc58e42348596534ce8f73809255ac89b330589b0f4d9cf2199d669e87" + }, + { + "path": "research/window-break-even-4470/README.md", + "usage": "input", + "git_blob": "89b5e4150e7dfe9804b7e1a65fba1fea8d77da8b", + "sha256": "103d9cd0943958115007cff7b2451da15182c6036be3320fa811b867d9d94ffd" + } + ] +} diff --git a/research/even-window-saturation-gap/TASK.json b/research/even-window-saturation-gap/TASK.json new file mode 100644 index 0000000000..5d8cc442e6 --- /dev/null +++ b/research/even-window-saturation-gap/TASK.json @@ -0,0 +1,87 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 8, + "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "original_card": { + "id": "complex-new-helper-inventory", + "question": "Can a changed helper inventory earn productive credit that survives completion, compilation and the 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": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Specify all arbitrary inputs, owned fields, restored outputs and a physically legal consumer. Compare complete P and T, including target debits and precision/stock costs. #5599 is a positive control for target refinement, not permission to split every helper for free. #5614 is a hypothetical compiler budget, not an emitted 145-split word. Stop at the first unpaid boundary or a failing optimistic full bill.", + "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": [ + "productive helper", + "target refinement", + "5599", + "5614" + ], + "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 that the even-window Lagrangian line-count cap cannot be attained for k >= 3, resolving PR5282 open question 1 at h=6 and h=8.", + "scope_change_reason": "Replace the current card's source-bound productive-helper first experiment with PR5282's explicit even-window line-system equality question. This excludes a proposed complex-decoder inventory premise; it does not construct or price a new helper caller.", + "bottleneck_link": "A saturated h=6 or h=8 line system is an explicitly proposed input to a cheaper complex decoder. The new projection identity excludes equality in this branch while leaving nonsaturated constructions and the selected invoice open.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified original obstruction; do not optimize a stronger ratio or a new construction.", + "outcome": "completed", + "evidence": "PROOF.md proves v <= 2^k T - 1 for every k >= 3 under the affine symplectic label contract. verify.py constructs exact incidence elimination certificates at k=2,3,4 and tests the scalar obstruction and rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the optimal supremum of v/T at even windows h=6 and h=8?", + "why_it_matters": "An integer gap of one excludes saturation but does not remove near-saturated systems from a complete supplier screen.", + "first_step": "Use the same affine-generator equations with positive semidefinite basis deficits instead of setting all deficits to zero.", + "blocked_by": "No dimension-independent quantitative deficit bound is proved here." + }, + { + "question": "Can a nonsaturated even-window system produce a favorable complete paid profile on a current complex caller?", + "why_it_matters": "The selected complex supplier binds, but the historical PR5282 scaled invoice does not certify a current native supplier.", + "first_step": "Specify one concrete line system, its literal decoder and its full current target, paid-child and restoration contract before a search.", + "blocked_by": "Native realization, dirty restoration, compiler closure and a complete signed invoice are absent." + } + ], + "coordination": { + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19294714", + "question_source": "PR #5282, Open next questions 1", + "source_author": "Matarener", + "upstream_checked": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "overlap_limitations": "Open PR titles and relevant bodies, latest handoffs and active Discussions, recent account PR bodies, merged searches and main README terms were checked. Search coverage is not a novelty proof." + } +} diff --git a/research/even-window-saturation-gap/VERIFY.json b/research/even-window-saturation-gap/VERIFY.json new file mode 100644 index 0000000000..2034bbcc71 --- /dev/null +++ b/research/even-window-saturation-gap/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/line-system-saturation/README.md", + "research/window-break-even-4470/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact RREF affine-generator elimination certificates for k=2,3,4; exceptional complementary projections, exact scalar obstruction, nine rejecting mutations/contracts and pinned contextual source bytes." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same certificate and rejection controls with Python assertions disabled; verification uses explicit exceptions." + } + ] +} diff --git a/research/even-window-saturation-gap/verify.py b/research/even-window-saturation-gap/verify.py new file mode 100644 index 0000000000..deb0c32aa1 --- /dev/null +++ b/research/even-window-saturation-gap/verify.py @@ -0,0 +1,202 @@ +#!/usr/bin/env python3 +"""Exact affine-generator certificates for the even-window equality obstruction. + +Produced by Nick Petalas. Apache-2.0. +The all-k result is a written proof; this program corroborates k = 2, 3, 4. +""" + +import argparse +from fractions import Fraction +import hashlib +from itertools import combinations +import json +from pathlib import Path +import platform + + +PACKAGE = Path(__file__).resolve().parent + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def pairing(x: int, y: int, k: int) -> int: + """Standard alternating form with consecutive coordinate pairs.""" + return sum( + ((x >> (2 * j)) & 1) * ((y >> (2 * j + 1)) & 1) + + ((x >> (2 * j + 1)) & 1) * ((y >> (2 * j)) & 1) + for j in range(k) + ) % 2 + + +def generators(k: int) -> tuple[tuple[int, ...], ...]: + """Enumerate each maximal isotropic subspace by its unique RREF basis.""" + require(type(k) is int and 2 <= k <= 4, "k must be an integer in 2..4") + result = [] + candidates = 0 + for pivots in combinations(range(2 * k), k): + free = tuple( + (i, j) for i, p in enumerate(pivots) + for j in range(p + 1, 2 * k) if j not in pivots + ) + require(len(free) <= k * k, "RREF free-bit bound") + for mask in range(1 << len(free)): + candidates += 1 + rows = [1 << p for p in pivots] + for bit, (i, j) in enumerate(free): + rows[i] |= ((mask >> bit) & 1) << j + if any(pairing(x, y, k) for x, y in combinations(rows, 2)): + continue + span = [0] + for row in rows: + span += [x ^ row for x in span] + result.append(tuple(sorted(span))) + require(candidates <= 256 * (1 << (k * k)), "candidate bound") + require(len(result) == len(set(result)), "duplicate RREF subspace") + return tuple(result) + + +def incidence_data(k: int) -> tuple[tuple[int, ...], tuple[tuple[int, ...], ...]]: + """Fix w=1, so the affine hyperplane b(p,w)=1 is bit 1 = 1.""" + labels = tuple(p for p in range(1 << (2 * k)) if pairing(p, 1, k)) + family = tuple(tuple(p for p in g if p in labels) + for g in generators(k) if 1 not in g) + require(len(labels) == 1 << (2 * k - 1), "hyperplane size") + for block in family: + require(len(block) == 1 << (k - 1), "affine generator size") + require(all(not pairing(p, q, k) for p, q in combinations(block, 2)), + "nonorthogonal affine generator") + return labels, family + + +def certificate(k: int, labels: tuple[int, ...], family: tuple[tuple[int, ...], ...], + partner_delta: int = 1, scalar: Fraction | None = None) -> int: + """Eliminate all other projection symbols from affine basis equations.""" + r = 1 + s = 1 + for j in range(1, k): + r *= (1 << j) + 1 + for j in range(1, k - 1): + s *= (1 << j) + 1 + require(len(family) == (1 << k) * r, "family count") + total = {q: sum(q in block for block in family) for q in labels} + require(all(value == r for value in total.values()), "point incidence") + rhs = 2 * r * r - s * len(family) + denominator = r * (r - s) + expected_scalar = Fraction(1, 1 << (k - 2)) if scalar is None else scalar + require(Fraction(rhs, denominator) == expected_scalar, "wrong scalar") + checked = 0 + for p in labels: + partner = p ^ partner_delta + if p > partner: + continue + require(partner in total and partner != p, "invalid partner") + selected = tuple(block for block in family if p in block or partner in block) + require(len(selected) == 2 * r, "pair incidence") + for q in labels: + coefficient = r * sum(q in block for block in selected) - s * total[q] + expected = denominator if q in (p, partner) else 0 + require(coefficient == expected, "projection elimination failed") + checked += 1 + require(checked * 2 == len(labels), "partner partition") + return checked + + +def multiply(a: tuple[tuple[Fraction, ...], ...], + b: tuple[tuple[Fraction, ...], ...]) -> tuple[tuple[Fraction, ...], ...]: + return tuple(tuple(sum(a[i][j] * b[j][l] for j in range(2)) + for l in range(2)) for i in range(2)) + + +def algebra_controls() -> dict[str, int]: + """Check the exact idempotent reduction and its exceptional scalars.""" + identity = ((Fraction(1), Fraction(0)), (Fraction(0), Fraction(1))) + p = ((Fraction(1), Fraction(0)), (Fraction(0), Fraction(0))) + q = ((Fraction(0), Fraction(0)), (Fraction(0), Fraction(1))) + require(multiply(p, p) == p and multiply(q, q) == q, "complement fixture") + require(tuple(tuple(p[i][j] + q[i][j] for j in range(2)) + for i in range(2)) == identity, "k=2 exception must survive") + # For Q=cI-P and P^2=P, Q^2-Q=(c^2-c)I+(2-2c)P. + # At c!=1 it forces P=(c/2)I. The latter is not idempotent for 0 int: + rejected = 0 + cases = ( + (family[:-1], 1, None), + (family + (family[0],), 1, None), + (family, 4, None), + (family, 1, Fraction(1, 4)), + ) + for blocks, delta, scalar in cases: + try: + certificate(3, labels, blocks, delta, scalar) + except ValueError: + rejected += 1 + require(rejected == len(cases), "a false incidence certificate passed") + for invalid in (0, 1, 5, True, Fraction(3)): + try: + generators(invalid) + except ValueError: + rejected += 1 + require(rejected == 9, "invalid dimension accepted") + return rejected + + +def source_hashes() -> dict[str, str]: + root = PACKAGE.parent.parent + metadata = json.loads((PACKAGE / "SOURCES.json").read_text()) + hashes = {} + for row in metadata["files"]: + if row["usage"] == "input": + digest = hashlib.sha256((root / row["path"]).read_bytes()).hexdigest() + require(digest == row["sha256"], "changed predecessor input") + hashes[row["path"]] = digest + return hashes + + +def run() -> dict: + hashes = source_hashes() + rows = [] + for k in range(2, 5): + labels, family = incidence_data(k) + pairs = certificate(k, labels, family) + rows.append({"k": k, "labels": len(labels), "affine_generators": len(family), + "pair_certificates": pairs, "forced_pair_scalar": str(Fraction(1, 1 << (k - 2)))}) + if k == 3: + rejected = rejection_controls(labels, family) + return {"status": "PASS_EVEN_WINDOW_SATURATION_GAP", "instances": rows, + "algebra_controls": algebra_controls(), "rejections": rejected, + "source_sha256": hashes} + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path, + help="write a generated source-bound receipt outside the checkout") + args = parser.parse_args() + if args.receipt is not None: + root = PACKAGE.parent.parent + require(not args.receipt.resolve().is_relative_to(root), "receipt must be outside checkout") + result = run() + if args.receipt is not None: + receipt = dict(result, python=platform.python_version(), package_sha256={ + p.name: hashlib.sha256(p.read_bytes()).hexdigest() + for p in sorted(PACKAGE.iterdir()) if p.is_file() + }) + args.receipt.write_text(json.dumps(receipt, indent=2, sort_keys=True) + "\n") + print(json.dumps(result, sort_keys=True)) + + +if __name__ == "__main__": + main()