diff --git a/research/support-cycle-resolvent/README.md b/research/support-cycle-resolvent/README.md new file mode 100644 index 0000000000..0589240bd1 --- /dev/null +++ b/research/support-cycle-resolvent/README.md @@ -0,0 +1,221 @@ +# Sharp inverse bounds with forbidden diagonal entries + +This contribution was produced by Nick Petalas. Apache-2.0. + +The exact inverse envelope under unequal row contraction budgets remains +computable when arbitrary diagonal entries are forbidden. A maximum-product +return cycle replaces the root self-loop in the denominator. In a two-vertex +example the sharp bound is **14/5**, whereas allowing the diagonals gives **6**. + +This is a scoped algebraic proof with exact finite corroboration. It claims +neither a new multiplication exponent nor a Gaussian-specific bound. The new +step removes the all-diagonals-allowed hypothesis of Ali Romman's +[PR #5306](https://github.com/CrocSwap/integer-mult-bounds/pull/5306) and +[PR #5255](https://github.com/CrocSwap/integer-mult-bounds/pull/5255). +Those predecessor theorems are cited, not audited or replayed. + +## Statement + +Let G be any finite directed graph on n >= 1 vertices, with self-loops +optional. Fix real row budgets 0 < r_i < 1. Admit all complex n by n matrices +E satisfying + +```text +E_ik = 0 unless i -> k is an edge of G, +sum_k |E_ik| <= r_i. +``` + +An allowed entry may be zero. The matrix norm below is the induced 1-norm, +the largest absolute column sum. + +For each root j, put w_jj = 1. For i != j, let w_ij be the largest product of +row budgets along a simple directed path from i to j, excluding the terminal +vertex j. If there is no path, put w_ij = 0. Let q_j be the largest product of +row budgets around a simple directed cycle containing j. A self-loop at j +counts as a cycle of length one. If no such cycle exists, put q_j = 0. + +Then every inverse exists and + +```text +max_E sum_i |((I-E)^-1)_ij| = sum_i w_ij / (1-q_j), + +max_E ||(I-E)^-1||_1 = max_j [sum_i w_ij / (1-q_j)]. +``` + +For every root, one nonnegative real matrix attains the entire displayed +column entry by entry. Each row of an attaining matrix has at most one +nonzero entry, equal to that row's budget. The attaining matrix can depend +on the root; simultaneous attainment of all columns is not asserted. + +## Proof + +Fix j and abbreviate w_i = w_ij. The weight of every nonempty directed cycle +is strictly less than one. Removing a cycle from a walk therefore increases +its weight. Maximum-product walks from i to j can be taken simple, stopping +at their first arrival at j. In particular 0 <= w_i < 1 for i != j. + +With the maximum of an empty set defined as zero, these weights satisfy + +```text +w_i = r_i max_(i -> k) w_k for i != j, +q_j = r_j max_(j -> k) w_k. +``` + +For the first identity, prefixing an edge to a maximizing path gives a walk; +removing any repeated cycle can only improve it. Conversely every maximizing +nonempty simple path begins with an allowed edge. For the second identity, +an edge out of j followed by a simple path back to j is a simple cycle +through j. The self-loop case uses w_j = 1. A cycle elsewhere cannot replace +this root-specific return cycle. All factors are below one, so 0 <= q_j < 1. + +Set h_i = w_i/(1-q_j). The preceding identities give + +```text +h_i = r_i max_(i -> k) h_k for i != j, +h_j = 1 + r_j max_(j -> k) h_k. +``` + +For any admitted E, put B = |E| entrywise. The row budgets imply +B h <= h-e_j, where e_j is the j-th coordinate vector. Because the graph is +finite, rho = max_i r_i < 1. Thus ||B||_infinity <= rho < 1, and its Neumann +inverse is nonnegative. Multiplying the last inequality by that inverse gives + +```text +(I-B)^-1 e_j <= h. +``` + +The absolutely convergent Neumann series also gives +`|(I-E)^-1| <= (I-B)^-1` entrywise. This proves the claimed upper bound for +every entry in column j, including arbitrary complex phases and diffuse rows. + +For attainment, at every i != j with w_i > 0, choose one allowed successor +k satisfying w_i = r_i w_k and set E_ik = r_i. Put zero in all other entries +of that row. When w_i = 0 use the zero row. At the root, if q_j > 0 choose a +successor satisfying q_j = r_j w_k and set E_jk = r_j; when q_j = 0 use the +zero row. Every choice exists by the finite maximum identities. + +This matrix is nonnegative, obeys the support and row budgets, and satisfies +`(I-E)h = e_j` exactly. Since ||E||_infinity < 1, its inverse exists, and its +j-th column equals h. This proves full-column attainment. Choosing a root +maximizing the finite column formula proves the matrix norm formula. + +## Strict improvement and examples + +Adding self-loops does not change any maximum-product path weight, because +loops only reduce walk weights. If the loop at j is allowed, q_j = r_j. If it +is forbidden, q_j < r_j: every possible return cycle has at least one +additional factor strictly below one, and there are finitely many simple +cycles. Consequently, forbidding that loop strictly lowers the sharp bound +for column j relative to diagonal completion. If G has no self-loops, the +sharp matrix 1-norm is strictly below its diagonal-completed counterpart. +This is a comparison of two admitted matrix classes, not a source mutation. + +For edges 0 -> 1 and 1 -> 0 with budgets 1/2 and 3/4, the attaining matrix is + +```text +E = [[0, 1/2], [3/4, 0]], +(I-E)^-1 = [[8/5, 4/5], [6/5, 8/5]]. +``` + +Both return factors are 3/8. The column sums are 14/5 and 12/5, so the exact +norm envelope is 14/5. Allowing both diagonals gives the larger envelope 6. + +For the acyclic path 0 -> 1 -> 2 with budgets 1/2, 3/4, 1/4, every q_j is +zero. The sharp norm is 17/8, the sum 1 + 3/4 + 3/8 in the final column. + +With unequal budgets, the maximizing return cycle need not be the shortest. +For edges 0 -> 1 -> 0 and 0 -> 2 -> 3 -> 0, with budgets +1/2, 1/10, 9/10, 9/10, the longer return product 81/200 exceeds 1/20. The +root-0 column envelope is 562/119. This fixture rejects a shortest-cycle +substitution in the unequal-budget formula. + +## Exact finite evidence + +The standalone [verifier](verify.py) uses maximum-product dynamic programming +for the formula and separate rational Gauss-Jordan inversion for observations. +It enumerates every directed support on one through three vertices with at +least one forbidden diagonal, and every row-budget assignment from {1/3,2/3}. +Thus it spends its main enumeration on the changed hypothesis. + +The complete run checks 3,634 support/budget cases, 50,334 zero-or-saturated +single-successor policy matrices, 10,850 constructed attaining columns, and +10,902 diffuse signed or nonnegative matrix evaluations. Counts are evaluations +in their declared graph/budget domains, not counts of distinct matrices after +deduplication. The policy oracle compares every entry maximum with the proposed +full column, and a single constructed witness is inverted to check simultaneous +attainment within that column. The continuum upper bound is the written proof, +not an inference that policy enumeration covers arbitrary diffuse matrices. + +The explicit examples above and a root-disconnected cycle fixture distinguish +self-loop, zero-return, unequal-cycle and root-specific behavior. Ten rejection +controls cover invalid dimensions/budgets/neighbors/root, forbidden diagonal +entries and overspent rows. Checks use explicit exceptions and remain enabled +under optimized Python. No predecessor verifier is imported or executed. + +From the repository root, using CPython 3.12 and only its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/support-cycle-resolvent/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/support-cycle-resolvent/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/support-cycle-resolvent +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/support-cycle-resolvent --check-source-history +``` + +Any CPython 3.12 executable can replace the displayed path. Each direct run +prints `PASS_SUPPORT_CYCLE_RESOLVENT` inside a generated JSON receipt binding +all five package files by SHA256. Optional `--receipt /absolute/external/path` +exclusively creates that receipt outside the checkout. Normal replay writes +no files. The registered runner prints `PASS_REGISTERED_RESEARCH_PACKAGE`. +The standalone checker also works from a Git-free package export. + +## Scope and credit + +This is a changed conditioning side question under `uniform-transfer-audit`, +not discharge of a selected framework assumption. Base main is +`de5ec2e7a6074068452f45b1a191b5c72832df4a`, priority revision 8. The card's +selected source-binding orientation passed after sparse inputs were materialized. +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19213524) +records the optional-diagonal premise and overlap coverage. Current scientific +sources remain governed by `certificates/selected-result.json`. + +Credit Ali Romman for #5255's common-row support optimum and #5306's unequal-row +extension with diagonal entries allowed. Credit Cinna Davis #4100 for the +conditioning context and James Reed #4282 for periodic sections. William +Lawyer #852 treats different bounded weighted cycles. Their results and all +retained source notices remain unchanged. Neumann comparison, discounted-path +and maximum-principle methods are classical; general literature priority is +unclaimed. [SOURCES.json](SOURCES.json) pins the two cited predecessor READMEs +as provenance, with no runtime dependency or imported scientific evidence. + +The theorem is finite-dimensional with every r_i strictly between zero and +one. It permits arbitrary complex coefficients and arbitrary support, but does +not settle row budgets equal to or above one, mandatory nonzero edges, a +Gaussian-specific class, operator 2-norm optima or infinite graphs. Source-bound +row estimates and physical preparation, native operations, compiler, ownership, +precision/tape, stock and analytic recovery remain outside scope. No selected +cold replay, native replay, Lean, Docker or predecessor scientific suite was +run. Independent human and formal proof-kernel review are unclaimed. + +Power-of-ten inspection: no recursion or dynamic code generation; loops have +fixed finite fixture bounds, graph dimension is capped at six in internal +helpers, exhaustive graph tests use n <= 3, and the policy oracle uses n <= 4. +Every function is below 60 lines. Python Fraction arithmetic and collection +allocation are a managed-runtime deviation from fixed allocation. Fixed fixture +dimensions and fixed rational budgets bound live data and coefficient sizes; +there is no externally supplied graph. The ten failure controls use a bounded +list of local callables, a deviation from avoiding indirect calls that keeps +rejection cases explicit. Warning-strict normal and optimized replay provide +the available standard-library diagnostics. A larger public solver would need +new input/resource contracts and dedicated static analysis. + +## Open next questions + +- Can one emitted rounded coefficient matrix provide both a proven sparse + support with missing diagonal entries and heterogeneous row budgets? Extract + the exact support and rational budgets, then apply the return-cycle formula + and charge their preparation. Actual source binding and physical costs are + missing; this abstract improvement alone does not admit a supplier. +- Which additional entrywise constraints prevent the concentrating attaining + policies? Begin with one actual matrix class and its per-entry bounds. + The current envelope permits each row to concentrate its entire budget on + one allowed edge, so it cannot price a restriction that forbids concentration. diff --git a/research/support-cycle-resolvent/SOURCES.json b/research/support-cycle-resolvent/SOURCES.json new file mode 100644 index 0000000000..ea20e9416a --- /dev/null +++ b/research/support-cycle-resolvent/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/unequal-row-resolvent/README.md", + "usage": "provenance", + "git_blob": "5ef2cafa9b856a081e9ef616ccea6a61d3efba36", + "sha256": "bb1730cc7977d54828f178becc3e381d378343a723521516a4a4d09af6f294e9" + }, + { + "path": "research/sharp-banded-resolvent/README.md", + "usage": "provenance", + "git_blob": "d68fc9625e7c74e7aacc8e684b5188be3300dd9e", + "sha256": "e3f97c0ee5dde9c2ac56bd1922ee3dba86f047d17bde9e502ca2fc73cd859ba6" + } + ] +} diff --git a/research/support-cycle-resolvent/TASK.json b/research/support-cycle-resolvent/TASK.json new file mode 100644 index 0000000000..a46ea7ea3f --- /dev/null +++ b/research/support-cycle-resolvent/TASK.json @@ -0,0 +1,100 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact inverse 1-norm envelope for arbitrary finite directed supports, including forbidden diagonals, under unequal strict row contraction budgets; constructive full-column attainment.", + "scope_change_reason": "An original conditioning side theorem changes the all-diagonals-allowed hypothesis of PR5306. It is not an audit or discharge of the selected framework assumptions.", + "bottleneck_link": "Missing self-loops can strictly lower inverse amplification bounds before rounding precision is priced; actual caller support and budgets remain unbound.", + "budget_minutes": 60, + "stop_rule": "Ship the optional-diagonal theorem after exact finite checks; do not extend to physical implementation or chase another result.", + "outcome": "completed", + "evidence": "Written proof; 3634 support/budget cases, 50334 policy matrices, 10850 attaining columns, 10902 diffuse matrix evaluations, 10 rejection controls, and explicit rational fixtures.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can one emitted rounded coefficient matrix supply a sparse support with missing diagonals and unequal row budgets?", + "why_it_matters": "The exact abstract improvement becomes useful for precision only after source binding and complete preparation costs.", + "first_step": "Extract exact support and rational row bounds from one source matrix, compute maximum-product paths and return cycles, and price preparation.", + "blocked_by": "No actual caller or physical preparation model is supplied." + }, + { + "question": "What is the sharp inverse envelope with additional per-entry bounds that forbid row concentration?", + "why_it_matters": "The present attaining policies may be excluded by a physical matrix class.", + "first_step": "Fix one source-compatible set of entrywise bounds and compare its Bellman feasible set.", + "blocked_by": "No source-specific entrywise constraint class is fixed." + } + ], + "upstream_checkpoint": { + "commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "priority_revision": 8, + "checked_at": "2026-10-27T09:10:41.548316+00:00" + }, + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19213524", + "verification_environment": { + "python": "3.12.15 (main, Oct 14 2026, 00:55:37) [Clang 23.1.3 ]", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "dependencies": "Python standard library only" + } +} diff --git a/research/support-cycle-resolvent/VERIFY.json b/research/support-cycle-resolvent/VERIFY.json new file mode 100644 index 0000000000..6e4be5076c --- /dev/null +++ b/research/support-cycle-resolvent/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Exact policy oracle, full-column attaining inverses, diffuse bounds, rational fixtures and rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Exact policy oracle, full-column attaining inverses, diffuse bounds, rational fixtures and rejection controls." + } + ] +} diff --git a/research/support-cycle-resolvent/verify.py b/research/support-cycle-resolvent/verify.py new file mode 100644 index 0000000000..1af69aaa30 --- /dev/null +++ b/research/support-cycle-resolvent/verify.py @@ -0,0 +1,258 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the optional-diagonal inverse envelope.""" + +from __future__ import annotations + +import argparse +import hashlib +import itertools +import json +from fractions import Fraction as F +from pathlib import Path + +MAX_DIMENSION = 6 + + +def check(condition: bool, message: str) -> None: + if not condition: + raise AssertionError(message) + + +def validate(graph: tuple[tuple[int, ...], ...], budgets: tuple[F, ...]) -> int: + n = len(graph) + if not 1 <= n <= MAX_DIMENSION or len(budgets) != n: + raise ValueError("dimension must be between one and six") + if any(type(r) is not F or not 0 < r < 1 for r in budgets): + raise ValueError("budgets must be rational and strictly between zero and one") + for row in graph: + if tuple(sorted(set(row))) != row: + raise ValueError("neighbors must be sorted and distinct") + if any(type(k) is not int or not 0 <= k < n for k in row): + raise ValueError("neighbor outside the graph") + return n + + +def column_bound(graph: tuple[tuple[int, ...], ...], budgets: tuple[F, ...], + root: int) -> tuple[tuple[F, ...], tuple[F, ...], F]: + n = validate(graph, budgets) + if type(root) is not int or not 0 <= root < n: + raise ValueError("invalid root") + weights = tuple(F(i == root) for i in range(n)) + # Walks of length at most n-1 suffice: deleting a cycle raises its weight. + for _ in range(n - 1): + weights = tuple( + F(1) if i == root else max( + [weights[i]] + [budgets[i] * weights[k] for k in graph[i]]) + for i in range(n)) + cycle = max([F(0)] + [budgets[root] * weights[k] for k in graph[root]]) + check(0 <= cycle < 1 and weights[root] == 1, "invalid return factor") + bound = tuple(w / (1 - cycle) for w in weights) + return bound, weights, cycle + + +def attaining_matrix(graph: tuple[tuple[int, ...], ...], budgets: tuple[F, ...], + root: int) -> list[list[F]]: + bound, weights, cycle = column_bound(graph, budgets, root) + n = len(graph) + matrix = [[F(0) for _ in range(n)] for _ in range(n)] + for i in range(n): + target = cycle if i == root else weights[i] + if target == 0: + continue + options = [k for k in graph[i] if budgets[i] * weights[k] == target] + check(bool(options), "missing maximizing successor") + matrix[i][options[0]] = budgets[i] + validate_matrix(matrix, graph, budgets) + for i in range(n): + check(bound[i] - sum(matrix[i][k] * bound[k] for k in range(n)) + == F(i == root), "attaining Bellman residual") + return matrix + + +def validate_matrix(matrix: list[list[F]], graph: tuple[tuple[int, ...], ...], + budgets: tuple[F, ...]) -> None: + n = validate(graph, budgets) + check(len(matrix) == n and all(len(row) == n for row in matrix), "matrix shape") + for i, row in enumerate(matrix): + check(all(type(x) is F for x in row), "nonrational matrix") + check(sum(abs(x) for x in row) <= budgets[i], "row budget exceeded") + check(all(x == 0 or k in graph[i] for k, x in enumerate(row)), + "forbidden nonzero entry") + + +def inverse(matrix: list[list[F]]) -> list[list[F]]: + """Literal Gauss-Jordan inverse of I-E, independent of graph formulas.""" + n = len(matrix) + check(1 <= n <= MAX_DIMENSION, "inverse dimension") + work = [[F(i == j) - matrix[i][j] for j in range(n)] + + [F(i == j) for j in range(n)] for i in range(n)] + for j in range(n): + pivots = [i for i in range(j, n) if work[i][j] != 0] + check(bool(pivots), "singular inverse fixture") + pivot = pivots[0] + work[j], work[pivot] = work[pivot], work[j] + scale = work[j][j] + work[j] = [x / scale for x in work[j]] + for i in range(n): + if i != j: + scale = work[i][j] + work[i] = [a - scale * b for a, b in zip(work[i], work[j])] + return [row[n:] for row in work] + + +def policy_maxima(graph: tuple[tuple[int, ...], ...], budgets: tuple[F, ...] + ) -> tuple[list[list[F]], int]: + """Enumerate every zero-or-saturated single-successor row policy.""" + n = validate(graph, budgets) + check(n <= 4, "policy oracle limited to four vertices") + best = [[F(0) for _ in range(n)] for _ in range(n)] + count = 0 + for choices in itertools.product(*(tuple([-1]) + row for row in graph)): + matrix = [[F(0) for _ in range(n)] for _ in range(n)] + for i, k in enumerate(choices): + if k >= 0: + matrix[i][k] = budgets[i] + actual = inverse(matrix) + for i in range(n): + for j in range(n): + best[i][j] = max(best[i][j], actual[i][j]) + count += 1 + check(count <= (n + 1) ** n, "policy capacity") + return best, count + + +def support_graph(n: int, mask: int) -> tuple[tuple[int, ...], ...]: + check(1 <= n <= 3 and 0 <= mask < 2 ** (n * n), "support domain") + return tuple(tuple(k for k in range(n) if mask & (1 << (i * n + k))) + for i in range(n)) + + +def diffuse_checks(graph: tuple[tuple[int, ...], ...], budgets: tuple[F, ...], + bounds: list[tuple[F, ...]]) -> int: + n = len(graph) + for pattern in range(3): + matrix = [[F(0) for _ in range(n)] for _ in range(n)] + for i, row in enumerate(graph): + for k in row: + sign = -1 if pattern and (i + (pattern + 1) * k) % 3 else 1 + matrix[i][k] = sign * budgets[i] / len(row) + validate_matrix(matrix, graph, budgets) + actual = inverse(matrix) + for j in range(n): + check(all(abs(actual[i][j]) <= bounds[j][i] for i in range(n)), + "diffuse entry exceeded envelope") + return 3 + + +def exhaustive_checks() -> dict[str, int]: + counts = dict(support_budget_cases=0, policy_matrices=0, + attaining_columns=0, diffuse_matrices=0) + for n in range(1, 4): + for mask in range(2 ** (n * n)): + graph = support_graph(n, mask) + # Only changed-hypothesis cases: at least one diagonal is forbidden. + if all(i in graph[i] for i in range(n)): + continue + for budgets in itertools.product((F(1, 3), F(2, 3)), repeat=n): + best, policies = policy_maxima(graph, budgets) + bounds = [column_bound(graph, budgets, j)[0] for j in range(n)] + for j in range(n): + check(tuple(best[i][j] for i in range(n)) == bounds[j], + "complete policy oracle disagrees") + actual = inverse(attaining_matrix(graph, budgets, j)) + check(tuple(actual[i][j] for i in range(n)) == bounds[j], + "literal attaining inverse disagrees") + counts['attaining_columns'] += 1 + counts['support_budget_cases'] += 1 + counts['policy_matrices'] += policies + counts['diffuse_matrices'] += diffuse_checks(graph, budgets, bounds) + return counts + + +def reject(call, label: str) -> None: + try: + call() + except (AssertionError, ValueError): + return + raise AssertionError("control accepted: " + label) + + +def fixture_checks() -> dict[str, str]: + graph = ((1,), (0,)) + budgets = (F(1, 2), F(3, 4)) + bound0, _, q0 = column_bound(graph, budgets, 0) + bound1, _, q1 = column_bound(graph, budgets, 1) + check(q0 == q1 == F(3, 8), "two-cycle return product") + check(sum(bound0) == F(14, 5) and sum(bound1) == F(12, 5), "two-cycle columns") + check(max(map(sum, (bound0, bound1))) == F(14, 5), "two-cycle norm") + completed = ((0, 1), (0, 1)) + old = max(sum(column_bound(completed, budgets, j)[0]) for j in range(2)) + check(old == 6, "diagonal-completion comparison") + check(sum(bound0) != F(7, 2), "root-loop denominator mutant escaped") + dag = ((1,), (2,), ()) + dag_r = (F(1, 2), F(3, 4), F(1, 4)) + check(max(sum(column_bound(dag, dag_r, j)[0]) for j in range(3)) == F(17, 8), + "acyclic exact norm") + check(all(column_bound(dag, dag_r, j)[2] == 0 for j in range(3)), "acyclic return") + figure8 = ((1, 2), (0,), (3,), (0,)) + r8 = (F(1, 2), F(1, 10), F(9, 10), F(9, 10)) + bound8, _, q8 = column_bound(figure8, r8, 0) + check(q8 == F(81, 200) and sum(bound8) == F(562, 119), "weighted return cycle") + best8, count8 = policy_maxima(figure8, r8) + check(tuple(best8[i][0] for i in range(4)) == bound8, "figure-eight oracle") + check(count8 == 24 and q8 != r8[0] * r8[1], "shortest-cycle mutant escaped") + # A cycle elsewhere cannot be used as this root's return factor. + disconnected = ((1,), (), (2,)) + check(column_bound(disconnected, (F(1, 2),) * 3, 0)[2] == 0, + "unrelated cycle contaminated root") + return dict(two_cycle_norm="14/5", diagonal_completion_norm="6", + acyclic_norm="17/8", longer_return_column="562/119") + + +def failure_controls() -> int: + graph, budgets = ((1,), (0,)), (F(1, 2), F(3, 4)) + invalid = [lambda: column_bound((), (), 0), + lambda: column_bound(graph, (F(1), F(1, 2)), 0), + lambda: column_bound(graph, (F(0), F(1, 2)), 0), + lambda: column_bound(graph, (F(-1, 2), F(1, 2)), 0), + lambda: column_bound(graph, (0.5, F(1, 2)), 0), + lambda: column_bound(((1, 1), (0,)), budgets, 0), + lambda: column_bound(((2,), (0,)), budgets, 0), + lambda: column_bound(graph, budgets, 2)] + for call in invalid: + reject(call, "invalid graph/budget/root") + matrix = attaining_matrix(graph, budgets, 0) + matrix[0][0] = F(1, 10) + matrix[0][1] = F(0) + reject(lambda: validate_matrix(matrix, graph, budgets), "forbidden diagonal") + matrix[0][0], matrix[0][1] = F(0), F(3, 4) + reject(lambda: validate_matrix(matrix, graph, budgets), "overspent row") + return len(invalid) + 2 + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--receipt', type=Path) + args = parser.parse_args() + counts = exhaustive_checks() + fixtures = fixture_checks() + counts['rejection_controls'] = failure_controls() + package = Path(__file__).resolve().parent + names = ('README.md', 'TASK.json', 'SOURCES.json', 'VERIFY.json', 'verify.py') + hashes = {name: hashlib.sha256((package / name).read_bytes()).hexdigest() + for name in names} + receipt = dict(status='PASS_SUPPORT_CYCLE_RESOLVENT', counts=counts, + fixtures=fixtures, source_sha256=hashes, + scope='Exact finite corroboration; the universal result is the written proof.') + rendered = json.dumps(receipt, indent=2, sort_keys=True) + '\n' + if args.receipt is not None: + target = args.receipt.resolve() + if target.is_relative_to(package.parents[1]): + raise ValueError('receipt must be outside the checkout or export') + with target.open('x', encoding='utf-8') as stream: + check(stream.write(rendered) == len(rendered), 'partial receipt write') + print(rendered, end='') + + +if __name__ == '__main__': + main()