From 44640c4a9538d5565d33e6dc218889f130143ce7 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 22 Oct 2026 10:22:30 +0100 Subject: [PATCH] feat(research): prove the two-short-row connector obstruction --- research/depth4-two-row-obstruction/README.md | 200 +++++++++++++++++ .../depth4-two-row-obstruction/SOURCES.json | 36 +++ research/depth4-two-row-obstruction/TASK.json | 74 ++++++ .../depth4-two-row-obstruction/VERIFY.json | 36 +++ research/depth4-two-row-obstruction/verify.py | 211 ++++++++++++++++++ 5 files changed, 557 insertions(+) create mode 100644 research/depth4-two-row-obstruction/README.md create mode 100644 research/depth4-two-row-obstruction/SOURCES.json create mode 100644 research/depth4-two-row-obstruction/TASK.json create mode 100644 research/depth4-two-row-obstruction/VERIFY.json create mode 100644 research/depth4-two-row-obstruction/verify.py diff --git a/research/depth4-two-row-obstruction/README.md b/research/depth4-two-row-obstruction/README.md new file mode 100644 index 0000000000..ddb766ede9 --- /dev/null +++ b/research/depth4-two-row-obstruction/README.md @@ -0,0 +1,200 @@ +# Two short rows cannot realize a unit coefficient in any characteristic + +This contribution was produced by Nick Petalas. It extends the prime-modulus +row obstruction in [#4280](https://github.com/CrocSwap/integer-mult-bounds/pull/4280) +to every modulus, and gives a composite-characteristic family showing why the +unit-coefficient restriction matters. + +Claim type: **scoped proof**, with finite executable checks. The new results are: + +1. If a balanced depth-four chain word realizes a nonzero coefficient c with + at most two short rows, each short-row length L satisfies `m | cL`. + Equivalently, `m/gcd(m,c) | L`. In particular, every unit coefficient needs + at least three short rows, including when m is composite. +2. For every integer t >= 1, at `m = 8t` and `c = 4t`, exactly two short rows + suffice and the shortest word has **4m calls**. This is an infinite family, + not an extrapolation from the finite checks. + +The annihilator condition is necessary; sufficiency is not claimed. No new +kappa, supplier admission or complete multiplication theorem is supplied. + +## Model and inherited criterion + +The unsigned complete calls are `z_l += B_l z_(l-1)` for l = 1, 2, 3, 4. +The source x = z_0 is immutable; z_1, z_2, z_3 and y = z_4 initially hold +arbitrary dirty data. The maps B_l are arbitrary, with coefficients in a +nonzero unital ring of exact characteristic m. The word must restore the +intermediates and add `c B4 B3 B2 B1 x` to y. Each call is fully charged. + +A balanced word uses each call exactly m times. The inherited interval-count +criterion of [#4249](https://github.com/CrocSwap/integer-mult-bounds/pull/4249) +gives a floor of 4m for every nonzero c. This package uses #4280's row model: + +- The partition lambda lies in the m by m box and describes the 2/3 path. + Its row lengths are L_q in nonincreasing order. +- The nonincreasing profile rho records the levels of the m calls 1. +- The nonincreasing profile beta records the levels of the m calls 4. + Set `B(L) = beta(1) + ... + beta(L)`, with `B(0) = 0`. + +Every such triple of profiles, with entries between 0 and m, comes from a +balanced word. By #4280, Lemma 2, it is correct exactly when + +```text +sum L_q = sum rho_q = sum beta_p = 0 (mod m), +sum rho_q L_q = sum B(L_q) = 0 (mod m), +sum rho_q B(L_q) = -c (mod m). +``` + +A short row has `0 < L_q < m`. Full and zero rows drop out of all displayed +congruences involving L_q, because `B(m) = sum beta_p = 0 (mod m)`. +They may still affect `sum rho_q`. These statements are inherited tools, +not new results or a re-verification of #4280's witness tables. + +## Proof of the annihilator obstruction + +With no short rows the target coefficient is zero. Exactly one short row +contradicts `sum L_q = 0 (mod m)`. With exactly two, let their lengths be +L_1 >= L_2 and their rho values be r_1 >= r_2. Their lengths satisfy +`L_1 + L_2 = m`, since each is strictly between 0 and m. The inherited +congruences reduce to + +```text +(r_1 - r_2) L_1 = 0, +B(L_1) + B(L_2) = 0, +c = -(r_1 - r_2) B(L_1) (mod m). +``` + +Multiply the first identity by `-B(L_1)` and use the third to obtain +`c L_1 = 0 (mod m)`. Since `L_2 = m - L_1`, also `c L_2 = 0 (mod m)`. +Writing `g = gcd(m,c)` and cancelling g in the integer divisibility relation +gives `m/g | L_i`. If c is a unit, this forces `m | L_i`, contrary to the +definition of a short row. This proves the result for every modulus. + +For prime m every nonzero c is a unit, recovering #4280's Lemma 3 as a +special case. The new content is the all-modulus annihilator condition and +its restriction on unit coefficients in composite characteristic. + +## A two-row family in every characteristic divisible by eight + +Fix t >= 1 and m = 8t. Take the following profiles, padded with zeros: + +```text +lambda = (m, 6t, 2t, 0, ..., 0), +rho = (m-4, 4, 0, 0, ..., 0), +beta = (5 repeated t times, 4 repeated t times, + 2 repeated 2t times, 1 repeated 3t times, 0 repeated t times). +``` + +They have m entries, are nonincreasing and lie in [0,m], because m >= 8. +There are exactly two short rows. The five sums that must vanish are + +```text +sum L_q = 16t = 2m, +sum rho_q = m, +sum beta_p = 16t = 2m, +sum rho_q L_q = (m-4)m + 24t = (m-1)m, +sum B(L_q) = 16t + 15t + 9t = 40t = 5m. +``` + +The target sum is + +```text +sum rho_q B(L_q) = (m-4)16t + 4(15t) = 16tm - 4t = -4t (mod m). +``` + +Thus the word realizes c = 4t, which is nonzero modulo 8t. The row-model +converse supplies a balanced word of length 4m, meeting the inherited +per-call floor. Fewer than two short rows cannot realize any nonzero target, +as proved above. Hence two is the exact minimum short-row count for this +family, and 4m is its exact minimum call count. + +For example, t = 1 uses lambda = (8,6,2), rho = (4,4,0), and +beta = (5,4,2,2,1,1,1,0). Its 32-call word is +`44422222343442111133433234321111`. The verifier constructs the chronological +word from the profile definitions and checks the actual dirty action. + +## Reproduce and evidence + +From the repository root, using CPython 3.12 and only its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/depth4-two-row-obstruction/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/depth4-two-row-obstruction/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/depth4-two-row-obstruction +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/depth4-two-row-obstruction --check-source-history +``` + +Any CPython 3.12 can replace the local interpreter path. The verifier imports +no predecessor code and writes no files. It prints a generated receipt bound +to every package file and live input hash, followed by +`PASS_DEPTH4_TWO_ROW_OBSTRUCTION`. It checks: + +- The 64 new family words for t = 1..64, hence m = 8..512 in steps of eight. + Every word has exactly m copies of each call, passes all ten chronological + interval conditions and separately has UT5 product `I + c E_(1,5)`. +- Two literal dirty-register replays per word with 2 by 2 maps. The first + two maps are a fixed noncommuting pair; the others and all initial registers + use reproducible random data. All intermediates restore and y gains exactly + the ordered four-map composition multiplied by c. +- Every residue triple `(L, delta, b)` with `2 <= m <= 96`, + `ceil(m/2) <= L < m`, `0 <= delta,b < m` and `delta L = 0 (mod m)`. + For `c = -delta b`, it checks the annihilator and divisibility conclusions + and the exclusion of nonzero unit c. This is an algebraic relaxation; + it does not claim the triples have realizable monotone profiles. +- Rejection of a wrong coefficient, dropped and extra calls, a changed rho + profile and all detected action-changing adjacent swaps of the t = 1 word. + +The written proofs carry the unbounded statements. The finite checks support +the construction and catch implementation or chronology errors. +The bounded algebra check enumerates 436,358 tuples, including 235,610 with +nonzero c. The replay reports 17 rejection controls. Both registered commands +ran locally in less than one second each. + +## Limits and implementation constraints + +This is a result about balanced unsigned depth-four words and their row-model +complexity. It does not classify all two-row nonunit coefficients, supply +three-row unit constructions, or settle the 4m conjecture for every m and c. +Admission, dispatch, routing, intermediate storage, precision, physical +compiler and recursive caller costs remain unpriced. The selected frontier +is unchanged. Independent human and formal proof-kernel review are unclaimed. + +The replay has no recursion or unbounded retry. Its largest profiles have +512 entries and its largest word has 2,048 calls; the algebra loop bounds +are explicit in the code. Each function is below 60 lines. Internal and +input contracts use explicit exceptions, so optimized Python retains them. +The managed Python runtime allocates objects during the checks; fixed +allocation is unavailable here. Live storage is bounded by the fixed replay +domains and no run output is written into the checkout. A lower-level +fixed-capacity implementation is only needed if those domains become a +resource limit. Strict-warning normal and optimized replay are registered +in [VERIFY.json](VERIFY.json); no external static analyzer is required. + +## Open next questions + +The structured questions, relevance, first steps and blockers are in +[TASK.json](TASK.json). + +1. Which nonzero coefficients admit exactly two short rows? Enumerate the + monotone profiles for a fixed pair L and m-L. The annihilator condition + prunes the domain but is not proved sufficient. +2. Can three short rows realize every unit coefficient for every m >= 6? + The new obstruction proves necessity. Seek a uniform construction using + the three-row examples in #4280 while retaining both profile budgets. + +## Attribution and scope + +The row model and its prime-modulus obstruction are from #4280, produced by +Nick Petalas. The chain model and interval-count floor come from #4249; +the three-interleaving formulation and the earlier depth-four witnesses +come from [#4263](https://github.com/CrocSwap/integer-mult-bounds/pull/4263). +Ross Richardson's [#943/#934 lineage](../universal-connector-boundary/README.md) +supplies the complete-call dirty-connector interface. Divisibility and +unitriangular matrices are classical tools. The new results here are the +all-modulus annihilator obstruction and the two-short-row family above. +Exact source pins are in [SOURCES.json](SOURCES.json). + +The `connector-alphabet-change` card is explicitly changed to this scoped +successor question. The alphabet stays fixed. This is a small search-pruning +and construction result, with no inferred improvement to a complete supplier. +Apache-2.0. diff --git a/research/depth4-two-row-obstruction/SOURCES.json b/research/depth4-two-row-obstruction/SOURCES.json new file mode 100644 index 0000000000..abde323e6c --- /dev/null +++ b/research/depth4-two-row-obstruction/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40", + "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/depth3-chain-connector/README.md", + "usage": "input", + "git_blob": "4254083a4adc178e048b7b2d48d4f3e9bddfb8eb", + "sha256": "a9666ad1d44f4b4b4e7331813c56054efbb49aaebc3e3bd7dd6a6d27fc810043" + }, + { + "path": "research/depth4-chain-rowmodel/README.md", + "usage": "input", + "git_blob": "f7b9166b7e19076012279a75f1e7214840931d58", + "sha256": "a5894d985857d4771e927342a188970fd761c9a8cdcea2e564025d69cd80afe1" + }, + { + "path": "research/universal-connector-boundary/README.md", + "usage": "input", + "git_blob": "d277f7c5830b1f2bc42e1ff41ab86e7d7564929f", + "sha256": "23415f7829ab8d80a783142f10f7d31abbce84579362769984680af3df954476" + } + ] +} diff --git a/research/depth4-two-row-obstruction/TASK.json b/research/depth4-two-row-obstruction/TASK.json new file mode 100644 index 0000000000..b11c4a1fd7 --- /dev/null +++ b/research/depth4-two-row-obstruction/TASK.json @@ -0,0 +1,74 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 7, + "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1", + "original_card": { + "id": "connector-alphabet-change", + "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/universal-connector-boundary/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Construct and charge a legal extra operation on a minimal instance.", + "Prove a target-specific bound after adding one specified operation family." + ], + "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/universal-connector-boundary/verify.py" + ], + "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY", + "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.", + "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.", + "allowed_variations": [ + "Choose one additional operation and a small source count for its first counterexample." + ], + "scope_change_triggers": [ + "Keeping the alphabet and only increasing the source count; record this as a changed assignment.", + "Extending a source-count census without naming a supplier/interface decision it could change; audit #2973 pruning concerns before relying on the affected predecessor exclusions." + ], + "overlap_terms": [ + "universal connector", + "source-toggle", + "connector alphabet" + ] + }, + "scope_status": "changed", + "actual_scope": "Prove the all-modulus two-short-row annihilator obstruction for balanced depth-four chain connectors, and give an exact 4m construction with two short rows at m=8t, c=4t for every t>=1.", + "scope_change_reason": "The alphabet remains unsigned and complete. This extends the open row-complexity question of PR4280 rather than adding a connector operation; it distinguishes unit coefficients from composite-characteristic exceptions.", + "bottleneck_link": "Scoped side result: it prunes row-model searches for unit coefficients in composite characteristic and supplies a minimal-call infinite subfamily for nonunit coefficients. No physical supplier saving is inferred.", + "budget_minutes": 60, + "stop_rule": "Stop after the first verified original extension of the row obstruction and a sharp composite family. Leave classification and general unit constructions open.", + "outcome": "completed", + "evidence": "Written all-modulus proofs in README.md; standalone exact checks of 64 new family words, chronological counts, UT5 matrices, 128 dirty-register replays, a bounded annihilator relaxation and rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Which nonzero coefficients admit a balanced depth-four connector with exactly two short rows?", + "why_it_matters": "The annihilator condition is necessary but does not enforce the monotone profile budgets; a classification would identify when a two-row search is justified.", + "first_step": "Fix m, the pair L and m-L, and enumerate the admissible beta and rho profiles subject to the five vanishing congruences.", + "blocked_by": "The new necessary condition is not claimed sufficient." + }, + { + "question": "Can three short rows realize every unit coefficient for every m>=6?", + "why_it_matters": "The obstruction proves three are necessary for units in all characteristics; an upper construction would close that row-complexity gap.", + "first_step": "Use the three-short-row instances in PR4280 as design examples and seek a parametric family satisfying the profile budgets.", + "blocked_by": "A uniform construction for unit coefficients remains unknown here." + } + ], + "coordination": { + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19119351", + "upstream_checked_at": "2026-10-22T09:12:47Z", + "upstream_commit": "f626db5c3a3d781d8f7695038776c621651f75e1", + "scope": "Live open PRs, own recent PRs, latest handoff comments, cached complete remote overlap, and targeted main/merged searches; sparse local note coverage is incomplete." + } +} diff --git a/research/depth4-two-row-obstruction/VERIFY.json b/research/depth4-two-row-obstruction/VERIFY.json new file mode 100644 index 0000000000..b18aa3462f --- /dev/null +++ b/research/depth4-two-row-obstruction/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/depth3-chain-connector/README.md", + "research/depth4-chain-rowmodel/README.md", + "research/universal-connector-boundary/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "New characteristic-8t family: row congruences, two short rows, balanced calls, chronological intervals, UT5 product, dirty restoration; annihilator relaxation and corruption controls." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same exact checks with optimized Python; correctness checks use explicit exceptions." + } + ] +} diff --git a/research/depth4-two-row-obstruction/verify.py b/research/depth4-two-row-obstruction/verify.py new file mode 100644 index 0000000000..46bf039802 --- /dev/null +++ b/research/depth4-two-row-obstruction/verify.py @@ -0,0 +1,211 @@ +#!/usr/bin/env python3 +"""Check the new two-short-row obstruction and its characteristic-8t family. + +The all-modulus statements are proved in README.md. This bounded replay checks +the arithmetic relaxation and new words, without importing predecessor code. +""" +import hashlib +import json +import math +import random +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +MAX_T = 64 +MAX_MODULUS = 96 +FILES = ("README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py") +INPUTS = ("research/depth3-chain-connector/README.md", + "research/depth4-chain-rowmodel/README.md", + "research/universal-connector-boundary/README.md") + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def family(t: int) -> tuple[int, list[int], list[int], list[int]]: + require(type(t) is int and 1 <= t <= MAX_T, "t outside replay domain") + m = 8 * t + rows = [m, 6 * t, 2 * t] + [0] * (m - 3) + rho = [m - 4, 4, 0] + [0] * (m - 3) + beta = [v for v in (5, 4, 2, 2, 1, 1, 1, 0) for _ in range(t)] + return m, rows, rho, beta + + +def row_conditions(m: int, rows: list[int], rho: list[int], + beta: list[int]) -> tuple[tuple[int, ...], int]: + require(2 <= m <= 8 * MAX_T, "modulus outside replay domain") + for profile in (rows, rho, beta): + require(len(profile) == m, "profile length") + require(all(type(v) is int and 0 <= v <= m for v in profile), "profile range") + require(all(profile[i] >= profile[i + 1] for i in range(m - 1)), "profile order") + cumulative = [0] * (m + 1) + for i in range(m): + cumulative[i + 1] = cumulative[i] + beta[i] + vanish = (sum(rows), sum(rho), sum(beta), + sum(r * length for r, length in zip(rho, rows)), + sum(cumulative[length] for length in rows)) + coefficient = -sum(r * cumulative[length] for r, length in zip(rho, rows)) % m + return tuple(v % m for v in vanish), coefficient + + +def build_word(m: int, rows: list[int], rho: list[int], beta: list[int]) -> list[int]: + """Place calls at the levels in #4280's row-model definitions.""" + ones = [0] * (m + 1) + fours = [0] * (m + 1) + for q in range(1, m + 1): + following = rho[q] if q < m else 0 + ones[m - q] = rho[q - 1] - following + following_beta = beta[q] if q < m else 0 + fours[q] = beta[q - 1] - following_beta + ones[m] = m - rho[0] + fours[0] = m - beta[0] + word = [1] * ones[0] + [4] * fours[0] + previous_twos = 0 + for p in range(1, m + 1): + twos = m - sum(length >= p for length in rows) + for level in range(previous_twos + 1, twos + 1): + word.extend([2] + [1] * ones[level]) + word.extend([3] + [4] * fours[p]) + previous_twos = twos + for level in range(previous_twos + 1, m + 1): + word.extend([2] + [1] * ones[level]) + require(len(word) == 4 * m, "decoded word budget") + return word + + +def interval_counts(word: list[int], m: int) -> dict[tuple[int, int], int]: + require(len(word) <= 4 * m + 1, "word exceeds replay capacity") + count = {(i, j): 0 for i in range(1, 5) for j in range(i, 5)} + for letter in word: + require(type(letter) is int and 1 <= letter <= 4, "unknown call") + for start in range(1, letter + 1): + gain = 1 if start == letter else count[start, letter - 1] + count[start, letter] = (count[start, letter] + gain) % m + return count + + +def correct_word(word: list[int], m: int, c: int) -> bool: + count = interval_counts(word, m) + return (len(word) == 4 * m and all(word.count(i) == m for i in range(1, 5)) + and all(value == (c if key == (1, 4) else 0) + for key, value in count.items())) + + +def check_matrix(word: list[int], m: int, c: int) -> None: + """Right multiply upper-unitriangular matrices, separately from counts.""" + product = [[int(i == j) for j in range(5)] for i in range(5)] + for letter in word: + for i in range(5): + product[i][letter] = (product[i][letter] + product[i][letter - 1]) % m + expected = [[int(i == j) for j in range(5)] for i in range(5)] + expected[0][4] = c + require(product == expected, "UT5 product") + + +def apply(matrix: list[list[int]], vector: list[int], m: int) -> list[int]: + return [sum(matrix[i][j] * vector[j] for j in range(2)) % m for i in range(2)] + + +def check_dirty(word: list[int], m: int, c: int, rng: random.Random) -> None: + """Literal calls on arbitrary dirty vectors with noncommuting maps.""" + maps = [[[1, 1], [0, 1]], [[1, 0], [1, 1]]] + maps.extend([[[rng.randrange(m) for _ in range(2)] for _ in range(2)] + for _ in range(2)]) + initial = [[rng.randrange(m) for _ in range(2)] for _ in range(5)] + state = [v.copy() for v in initial] + for letter in word: + gain = apply(maps[letter - 1], state[letter - 1], m) + state[letter] = [(state[letter][i] + gain[i]) % m for i in range(2)] + composed = initial[0] + for matrix in maps: + composed = apply(matrix, composed, m) + expected_y = [(initial[4][i] + c * composed[i]) % m for i in range(2)] + require(state[:4] == initial[:4], "dirty intermediates not restored") + require(state[4] == expected_y, "literal target gain") + + +def check_annihilator() -> tuple[int, int]: + """Exhaust the necessary two-row algebra, relaxing profile realizability.""" + cases = 0 + nonzero = 0 + for m in range(2, MAX_MODULUS + 1): + for length in range((m + 1) // 2, m): + for delta in range(m): + if delta * length % m: + continue + for prefix_sum in range(m): + c = -delta * prefix_sum % m + require(c * length % m == 0, "short-row annihilator") + require(length % (m // math.gcd(m, c)) == 0, "divisibility form") + if c: + require(math.gcd(c, m) > 1, "unit escaped two-row obstruction") + nonzero += 1 + cases += 1 + require(nonzero > 0, "composite relaxation must remain nonempty") + return cases, nonzero + + +def check_controls() -> int: + m, rows, rho, beta = family(1) + word = build_word(m, rows, rho, beta) + require(not correct_word(word, m, 1), "wrong coefficient accepted") + require(not correct_word(word[:-1], m, 4), "dropped call accepted") + require(not correct_word(word + [1], m, 4), "extra call accepted") + changed_rho = rho.copy() + changed_rho[1] -= 1 + vanish, _ = row_conditions(m, rows, changed_rho, beta) + require(any(vanish), "changed rho passed row conditions") + swaps_rejected = 0 + for i in range(len(word) - 1): + changed = word.copy() + changed[i], changed[i + 1] = changed[i + 1], changed[i] + swaps_rejected += not correct_word(changed, m, 4) + require(swaps_rejected > 0, "chronology control did not detect any swap") + return 4 + swaps_rejected + + +def receipt() -> dict[str, dict[str, str]]: + source_path = PACKAGE / "SOURCES.json" + require(source_path.stat().st_size <= 65536, "source manifest capacity") + sources = json.loads(source_path.read_text(encoding="utf-8")) + rows = sources["files"] + require(len(rows) == 5, "source inventory size") + live = {row["path"]: row["sha256"] for row in rows if row["usage"] == "input"} + require(set(live) == set(INPUTS), "live input inventory") + inputs = {} + for name in INPUTS: + digest = hashlib.sha256((ROOT / name).read_bytes()).hexdigest() + require(digest == live[name], "source mismatch: " + name) + inputs[name] = digest + package = {name: hashlib.sha256((PACKAGE / name).read_bytes()).hexdigest() for name in FILES} + return {"package_sha256": package, "input_sha256": inputs} + + +def main() -> None: + hashes = receipt() + rng = random.Random(4280) + for t in range(1, MAX_T + 1): + m, rows, rho, beta = family(t) + c = 4 * t + vanish, actual_c = row_conditions(m, rows, rho, beta) + require(not any(vanish) and actual_c == c, "family row congruences") + require(sum(0 < length < m for length in rows) == 2, "short-row count") + word = build_word(m, rows, rho, beta) + require(correct_word(word, m, c), "chronological interval counts") + check_matrix(word, m, c) + for _ in range(2): + check_dirty(word, m, c, rng) + cases, nonzero = check_annihilator() + controls = check_controls() + print(json.dumps({**hashes, "family_cases": MAX_T, "dirty_replays": 2 * MAX_T, + "algebra_cases": cases, "nonzero_algebra_cases": nonzero, + "rejection_controls": controls}, sort_keys=True)) + print(f"PASS_DEPTH4_TWO_ROW_OBSTRUCTION family_cases={MAX_T} " + f"algebra_cases={cases} controls={controls}") + + +if __name__ == "__main__": + main()