diff --git a/research/sparse-dyadic-normalization/PROOF.md b/research/sparse-dyadic-normalization/PROOF.md new file mode 100644 index 0000000000..d915d8977b --- /dev/null +++ b/research/sparse-dyadic-normalization/PROOF.md @@ -0,0 +1,135 @@ +# Sparse dyadic normalization at rational rank one + +Let R = Z[1/2]. One arbitrary scalar x is observed through the mandatory +coefficient a > 0 and selected eligible coefficients b_i in Z. The decoder +must have the form + + x = c_0 (a x) + sum_{i in J} c_i (b_i x), c_i in R, + +as an identity for every x. Each acquired menu entry i has its declared +positive cost w_i. The mandatory observation is already present and is not +included in this incremental charge. No other observation or arbitrary new +linear combination is available for free. + +## 1. Exact scalar criterion + +Such a decoder exists if and only if + + gcd(a, (b_i)_{i in J}) is a power of two. + +For necessity, clear a common power-of-two denominator from a proposed decoder +identity at x = 1. The integer gcd must divide that power of two. For +sufficiency, integer Bezout coefficients express the positive gcd g as a +combination of the observed coefficients. If g is a power of two, dividing +those coefficients by g gives an allowed decoder. This also handles an empty +selection, zero menu entries and negative menu entries. The condition is on +the odd part of the gcd, not on rational rank or on whether one entry is a +dyadic unit. + +The identity is valid over any R-module. Necessity already holds when x ranges +over R. This is not a statement for fields in which every odd prime is inverted. +Rational observation coefficients whose denominators are powers of two reduce +to the same integer criterion by clearing a common power of two. + +## 2. Exact encoding of a finite weighted cover problem + +Take any finite universe U, distinct odd primes p_u for its elements, and an +indexed menu of subsets S_i of U. Repeated subsets and the empty subset are +allowed. Define + + a = product_{u in U} p_u, + b_i = product_{u in U minus S_i} p_u. + +Empty products are one. For every selected index set J, unique prime +factorization gives the exact identity + + gcd(a, (b_i)_{i in J}) = product_{u not in union_{i in J} S_i} p_u. + +Indeed, p_u divides a and every selected b_i precisely when no selected S_i +contains u. All coefficients are positive squarefree divisors of the same odd +integer a. Therefore J permits dyadic decoding if and only if its sets cover +U. Feasibility, every feasible index set, all positive additive costs, all +optimum costs and every optimum index set are preserved exactly. If no cover +exists, no allowed acquisition menu decodes. If U is empty, the mandatory +unit coefficient already decodes and the optimum incremental charge is zero. + +Thus the menu-selection problem contains arbitrary finite weighted Set Cover +already at rational rank one. This is an exact finite optimization encoding; +no new complexity-theory classification or approximation lower bound is +needed for the obstruction claimed here. + +## 3. Sharp unbounded acquisition count with rank unchanged + +For any integer n >= 1, choose n distinct odd primes and let S_i = {i}. Then + + a = p_1 ... p_n, b_i = a / p_i. + +Every menu entry is necessary. If entry i is missing, every available observed +coefficient is divisible by p_i. Clearing dyadic denominators would force +p_i to divide a power of two, which is impossible. All n entries suffice +because the gcd is one, so the exact minimum incremental acquisition count +is n. For arbitrary positive prices the exact optimum is sum_i w_i. + +The observation matrix has one column and rational rank one before any +acquisition, after every partial acquisition, and after completion. The +rational decoder (a x)/a therefore sees no rank deficit, while the constrained +dyadic decoder can require arbitrarily many acquisitions. The cheapest +unrestricted added observation would be x itself and would require one +acquisition; it is not in the declared singleton menu when n >= 2. + +For example, a = 105 and the menu is 35, 21, 15. Every two-entry selection +leaves one odd prime in the gcd. All three decode with the literal identity + + -105 + 2*35 + 21 + 15 = 1. + +This is the first delivered obstruction. No larger construction is pursued. + +## 4. Connection and limits + +Ali Romman's [PR #5789](https://github.com/CrocSwap/integer-mult-bounds/pull/5789) +explicitly distinguishes rational rank certificates from dyadic completion +and legal delivery. The new step is the sparse eligible-menu acquisition +obstruction, not another rank certificate or an audit of that tool. Bezout, +prime factorization and weighted Set Cover are classical ingredients. + +The result concerns the existence of a decoder under a declared menu. It +does not construct a physical source, prove that any current caller realizes +these coefficients, price coefficient synthesis, constrain intermediate +magnitudes, restore dirty helpers, or admit an integer-multiplication supplier. +In particular it is not an n-call lower bound for unrestricted circuits, free +mixing of unacquired rows, nonlinear decoders, or a changed coefficient ring. +It changes no selected frontier or inherited framework assumption. + +## 5. What the executable checks + +The all-n result above is a written proof. The independent executable +corroborates a finite domain. It constructs menu coefficients from subset +complements, computes gcds with the standard-library integer oracle, produces +Bezout coefficients with a separate bounded Euclidean algorithm, and replays +the decoder at three exact rational scalar inputs. It compares optimum costs +with literal subset-union enumeration for every price tuple in {1,2,3}^m. + +The complete menu domain is 0 <= |U| <= 3, 0 <= m <= 3, with every ordered +menu, including repetitions. Separately it checks every selection of the +singleton family for 1 <= n <= 12 and a modular missing-prime obstruction for +each infeasible selection. Signed, zero, non-squarefree and dyadic-unit +boundaries, invalid inputs, forged coefficients and rational-only decoding +controls are included. The report enumerates its actual counts and binds all +six package files by SHA256. It is generated on stdout, never hand-written. + +## 6. Verification implementation bounds + +The executable has no recursion, external dependencies or file writes. It +reads only the six package files for its generated hash receipt. Fixed test +domains bound every enumeration. The decoder permits at most 16 optional rows +of at most 4096 bits each. Extended Euclid has at most twice the larger input +bit length plus two iterations, since every two divisions at least halve the +positive remainder. Functions stay below 60 physical lines. + +Python's integer and Fraction operations allocate dynamically. This is a +managed-runtime deviation from fixed-allocation rules, bounded here by the +finite domains and input limits. Iterative Bezout coefficient growth is bounded +by a product of at most 17 input magnitudes. Negative controls intentionally +pass one of a fixed set of direct functions as a callback. Production checking +does not use dynamic dispatch. Explicit ValueError checks remain enabled under +-O. No compiler, external linter, proof kernel, Lean or Docker is required. diff --git a/research/sparse-dyadic-normalization/README.md b/research/sparse-dyadic-normalization/README.md new file mode 100644 index 0000000000..9b2f8dff28 --- /dev/null +++ b/research/sparse-dyadic-normalization/README.md @@ -0,0 +1,89 @@ +# Rational rank one does not bound sparse dyadic acquisition + +Claim type: scoped algebraic obstruction with finite corroboration. +For every n >= 1 there is one scalar source, one mandatory observation and +an n-entry eligible menu whose exact minimum incremental acquisition count is +n, although the rational observation rank is one throughout. + +Take distinct odd primes p_i, mandatory coefficient a = product_i p_i, and +eligible coefficients b_i = a/p_i. Every entry is necessary and all suffice. +The three-entry example observes 105x and may acquire 35x, 21x, 15x. Its exact +decoder is -105x + 2*35x + 21x + 15x = x. Any missing entry leaves an odd-prime +obstruction to all coefficients in Z[1/2]. + +More generally, any finite weighted Set Cover instance embeds exactly by +setting b_i = product of the primes outside set S_i. The feasible selections, +their complete declared acquisition charges, every optimum and infeasibility +are preserved. [PROOF.md](PROOF.md) gives the criterion, construction and +scope. No new complexity-theory classification is claimed. + +This answers an eligible-menu version of the rational-versus-dyadic boundary +in Ali Romman's [PR #5789](https://github.com/CrocSwap/integer-mult-bounds/pull/5789). +Its rational-rank implementation is cited, not replayed or audited. The +contribution concerns a constrained acquisition interface; no current physical +caller is asserted to realize this synthetic menu. + +## Reproduce + +From the repository root, using CPython 3.12 and only its standard library: + +```sh +PY=/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 +"$PY" -W error -B research/sparse-dyadic-normalization/verify.py +"$PY" -W error -B -O research/sparse-dyadic-normalization/verify.py +"$PY" -B scripts/research_package.py --package research/sparse-dyadic-normalization +"$PY" -B scripts/check_research_commit.py --package research/sparse-dyadic-normalization --check-source-history +``` + +Any CPython 3.12 path can replace the local interpreter path. The direct marker +is `PASS_SPARSE_DYADIC_NORMALIZATION`. Each direct invocation emits actual +enumeration counts and a generated SHA256 receipt for all six package files, +without writing outputs into the checkout. The registered commands run the +normal and optimized checks separately. The source-history preflight requires +the package to be committed first. + +The executable covers all ordered menus of at most three subsets of a universe +of size at most three, including duplicate and empty sets, and all positive +integer prices in {1,2,3}. It independently checks subset coverage, integer +gcd, constructed Bezout decoding and literal scalar outputs. It also checks +all selections in the singleton family through n=12, plus failure and boundary +controls. Finite execution corroborates the proof; it does not prove the +unbounded theorem by enumeration. + +## Limitations + +Acquisition means selecting one declared observation. Mixing an unacquired +row, inventing a coefficient-one observation or using an odd denominator is +outside the interface. Coefficient production, magnitude, basis changes, +dirty-state restoration, source realization and a complete physical invoice +remain unpriced. The result supplies no new kappa, physical supplier, selected +frontier update, complete multiplication theorem or proof-kernel validation. + +The formal-interface card was changed to an informal eligible-menu obstruction +because the cited rational tool explicitly leaves dyadic/physical completion +open. The selected-baseline orientation passed. The implementation contains no +predecessor code or live external input. SOURCES.json pins only historical +orientation and card provenance; TASK.json records the contextual predecessor +head and guide hash. Current tool limits in that PR are not hypotheses of the +unbounded theorem. + +## Open next questions + +- Find a named physical cut with several odd-prime losses and a priced eligible + menu. First derive its coefficients from the actual producer and consumer. + Without this source adapter the result is an algebraic interface obstruction. +- Identify a useful restriction on physical eligible menus that makes minimum + acquisition tractable or bounded. First test whether prime-loss sets are + nested, disjoint, or subject to a proved bounded-incidence condition. Generic + rational rank supplies none of these hypotheses. + +TASK.json records relevance, first steps and blockers for both questions. + +## Credit + +This contribution was produced by Nick Petalas. Credit Ali Romman #5789 for +the rational-certificate interface and its explicit completion boundary. +Bezout identities, ideal localization, prime factorization and weighted Set +Cover are classical. The new contribution is their exact sparse acquisition +encoding and sharp unbounded rank-one family in this interface. Apache-2.0. +Independent human and formal proof-kernel review are unclaimed. diff --git a/research/sparse-dyadic-normalization/SOURCES.json b/research/sparse-dyadic-normalization/SOURCES.json new file mode 100644 index 0000000000..fdb80ada25 --- /dev/null +++ b/research/sparse-dyadic-normalization/SOURCES.json @@ -0,0 +1,18 @@ +{ + "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" + } + ] +} diff --git a/research/sparse-dyadic-normalization/TASK.json b/research/sparse-dyadic-normalization/TASK.json new file mode 100644 index 0000000000..cf8779d197 --- /dev/null +++ b/research/sparse-dyadic-normalization/TASK.json @@ -0,0 +1,127 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact weighted prime-cover encoding for selecting scalar observations admitting a Z[1/2] decoder; sharp unbounded acquisition count at rational rank one.", + "scope_change_reason": "The user requests original research rather than audit. PR5789 explicitly leaves dyadic completion and physical delivery outside rational rank; this changes formalization to a self-contained informal sparse-menu obstruction.", + "bottleneck_link": "Rational rank alone cannot price which eligible observations must be acquired for a dyadic decoder. This side result prevents zero-cost sparse-completion assumptions; it supplies no physical supplier.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified prime-cover obstruction and rank-one family; stop extending after its bounded replay passes.", + "outcome": "completed", + "evidence": "PROOF.md gives the arbitrary-size proof. verify.py independently enumerates subset covers, computes integer gcd and Bezout decoders, checks weighted optima and literal exact scalar outputs.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does a named physical cut realize a nontrivial prime-loss menu?", + "why_it_matters": "Only a source adapter can turn this synthetic obstruction into a physical acquisition bill.", + "first_step": "Derive coefficients and eligible observations from one actual producer/consumer cut.", + "blocked_by": "No source-bound physical cut or complete restoration cost is supplied." + }, + { + "question": "Which proved physical menu restrictions make minimum acquisition tractable or bounded?", + "why_it_matters": "The generic rank-one interface preserves arbitrary finite weighted cover problems.", + "first_step": "Test a source-derived menu for nested, disjoint or bounded-incidence prime-loss sets.", + "blocked_by": "Physical menu restrictions and coefficient-generation costs are unknown." + } + ], + "claim_type": "scoped algebraic obstruction with finite corroboration", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19216201", + "predecessor": { + "pr": 5789, + "author": "Ali Romman", + "head": "c282c77bf89c001816c241a013e16441a649936e", + "guide_path": "docs/research/rational-rank-certificates.md", + "guide_sha256": "6f2ce4b63b58379e674dd23c403098219211727dbd9ec190b4134ad6f691efd6", + "usage": "Context and question source only. No predecessor executable or theorem is needed for the self-contained proof." + }, + "environment": { + "python": "3.12.15", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "dependencies": "standard library only" + }, + "finite_evidence": { + "menus": 689, + "menu_selections": 5054, + "weighted_menus": 16609, + "literal_decodings": 4530, + "sharp_family_sizes": 12, + "sharp_family_selections": 8190, + "rejection_controls": 15, + "boundary_controls": 4, + "semantic_controls": 3 + } +} diff --git a/research/sparse-dyadic-normalization/VERIFY.json b/research/sparse-dyadic-normalization/VERIFY.json new file mode 100644 index 0000000000..7a6104d17f --- /dev/null +++ b/research/sparse-dyadic-normalization/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete small prime-cover/gcd/Bezout/weighted-optimum domain, sharp family through twelve, literal scalar replay and rejection controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same complete domain with interpreter assertions disabled; explicit invariant and failure checks remain active." + } + ] +} diff --git a/research/sparse-dyadic-normalization/verify.py b/research/sparse-dyadic-normalization/verify.py new file mode 100644 index 0000000000..8b422c1699 --- /dev/null +++ b/research/sparse-dyadic-normalization/verify.py @@ -0,0 +1,190 @@ +#!/usr/bin/env python3 +"""Exact new-domain corroboration; no predecessor code is imported.""" + +from fractions import Fraction +from hashlib import sha256 +from itertools import product +import json +from math import gcd, prod +from pathlib import Path + + +PRIMES = (3, 5, 7, 11, 13, 17, 19, 23, 29, 31, 37, 41) +MAX_ROWS = 16 +MAX_BITS = 4096 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def is_dyadic(value): + denominator = Fraction(value).denominator + return denominator & (denominator - 1) == 0 + + +def bezout_pair(left, right): + """Bounded extended Euclid, including zero and signed right operands.""" + old_r, r = abs(left), abs(right) + old_s, s, old_t, t = 1, 0, 0, 1 + limit = 2 * max(abs(left).bit_length(), abs(right).bit_length()) + 2 + for _ in range(limit): + if r == 0: + u = old_s if left >= 0 else -old_s + v = old_t if right >= 0 else -old_t + require(u * left + v * right == old_r, "Bezout invariant") + return old_r, u, v + quotient = old_r // r + old_r, r = r, old_r - quotient * r + old_s, s = s, old_s - quotient * s + old_t, t = t, old_t - quotient * t + raise ValueError("Euclid iteration bound exhausted") + + +def decoder(base, rows): + require(type(base) is int and 0 < base < 1 << MAX_BITS, "invalid base") + require(len(rows) <= MAX_ROWS, "too many rows") + require(all(type(v) is int and abs(v) < 1 << MAX_BITS for v in rows), + "invalid row") + coefficients = [1] + common = base + for row in rows: + common, u, v = bezout_pair(common, row) + coefficients = [u * coefficient for coefficient in coefficients] + [v] + if common & (common - 1): + return None + answer = tuple(Fraction(coefficient, common) for coefficient in coefficients) + check_decoder(base, rows, answer) + return answer + + +def check_decoder(base, rows, coefficients): + require(len(coefficients) == len(rows) + 1, "wrong coefficient count") + require(all(is_dyadic(c) for c in coefficients), "non-dyadic coefficient") + require(sum(c * value for c, value in zip(coefficients, (base, *rows))) == 1, + "decoder identity failed") + + +def encode(universe_size, masks): + require(type(universe_size) is int and 0 <= universe_size <= len(PRIMES), + "invalid universe") + require(len(masks) <= MAX_ROWS, "too many masks") + require(all(type(m) is int and 0 <= m < 1 << universe_size for m in masks), + "invalid mask") + primes = PRIMES[:universe_size] + base = prod(primes) + rows = tuple(prod(p for j, p in enumerate(primes) if not (mask >> j & 1)) + for mask in masks) + return base, rows + + +def selected_indices(size, mask): + return tuple(index for index in range(size) if mask >> index & 1) + + +def check_menu(universe_size, masks, counts): + base, rows = encode(universe_size, masks) + feasible = [] + for selection in range(1 << len(masks)): + indices = selected_indices(len(masks), selection) + union = 0 + for index in indices: + union |= masks[index] + chosen = tuple(rows[index] for index in indices) + common = gcd(base, *chosen) + expected_gcd = prod(PRIMES[j] for j in range(universe_size) + if not (union >> j & 1)) + require(common == expected_gcd, "uncovered-prime product") + coefficients = decoder(base, chosen) + covered = union == (1 << universe_size) - 1 + require((coefficients is not None) == covered, "cover equivalence") + if coefficients is not None: + for scalar in (Fraction(-3, 2), Fraction(0), Fraction(7, 3)): + output = sum(c * value * scalar for c, value in + zip(coefficients, (base, *chosen))) + require(output == scalar, "literal scalar decoding") + counts["literal_decodings"] += 1 + feasible.append((indices, covered, common == 1)) + counts["menu_selections"] += 1 + for costs in product((1, 2, 3), repeat=len(masks)): + cover_costs = [sum(costs[i] for i in ix) for ix, cover, _ in feasible if cover] + gcd_costs = [sum(costs[i] for i in ix) for ix, _, unit in feasible if unit] + require(min(cover_costs, default=None) == min(gcd_costs, default=None), + "weighted optimum") + counts["weighted_menus"] += 1 + counts["menus"] += 1 + + +def check_unbounded_family(counts): + for size in range(1, len(PRIMES) + 1): + base, rows = encode(size, tuple(1 << j for j in range(size))) + require(decoder(base, rows) is not None, "full family must decode") + for selection in range(1 << size): + indices = selected_indices(size, selection) + common = gcd(base, *(rows[j] for j in indices)) + require((common == 1) == (len(indices) == size), "sharp acquisition floor") + if len(indices) < size: + missing = next(j for j in range(size) if not (selection >> j & 1)) + require(all(value % PRIMES[missing] == 0 for value in + (base, *(rows[j] for j in indices))), "modular obstruction") + counts["sharp_family_selections"] += 1 + counts["sharp_family_sizes"] += 1 + + +def must_reject(function, *arguments): + try: + function(*arguments) + except ValueError: + return + raise ValueError("negative control was accepted") + + +def check_controls(counts): + for base, rows in ((0, ()), (-1, ()), (True, ()), (1 << MAX_BITS, ()), + (1, (True,)), (1, (Fraction(1, 2),)), + (1, (0,) * (MAX_ROWS + 1)), (1, (1 << MAX_BITS,))): + must_reject(decoder, base, rows) + counts["rejection_controls"] += 1 + for size, masks in ((-1, ()), (13, ()), (1, (2,)), (1, (-1,))): + must_reject(encode, size, masks) + counts["rejection_controls"] += 1 + for base, rows, coefficients in ((3, (), (Fraction(1, 3),)), + (3, (5,), (1, 0)), + (3, (5,), (1,))): + must_reject(check_decoder, base, rows, coefficients) + counts["rejection_controls"] += 1 + for base, rows in ((8, ()), (12, (-20, 0)), (12, (18, 0)), (45, (0, -14))): + result = decoder(base, rows) + common = gcd(base, *rows) + require((result is not None) == (common & (common - 1) == 0), + "signed/non-squarefree boundary") + counts["boundary_controls"] += 1 + base, rows = encode(3, (1, 2, 4)) + require((base, rows) == (105, (35, 21, 15)), "complement convention") + require(all(decoder(base, (row,)) is None for row in rows), "rational rank mutant") + require(all(decoder(base, rows[:j] + rows[j + 1:]) is None for j in range(3)), + "two-observation mutant") + counts["semantic_controls"] = 3 + + +def main(): + counts = dict.fromkeys(("menus", "menu_selections", "weighted_menus", + "literal_decodings", "sharp_family_sizes", + "sharp_family_selections", "rejection_controls", + "boundary_controls", "semantic_controls"), 0) + for size in range(4): + for length in range(4): + for masks in product(range(1 << size), repeat=length): + check_menu(size, masks, counts) + check_unbounded_family(counts) + check_controls(counts) + root = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + hashes = {name: sha256((root / name).read_bytes()).hexdigest() for name in names} + print(json.dumps({"status": "PASS_SPARSE_DYADIC_NORMALIZATION", "counts": counts, + "source_sha256": hashes}, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()