diff --git a/research/finite-menu-adaptivity/PROOF.md b/research/finite-menu-adaptivity/PROOF.md new file mode 100644 index 0000000000..8288f6ed5c --- /dev/null +++ b/research/finite-menu-adaptivity/PROOF.md @@ -0,0 +1,163 @@ +# Finite-menu adaptivity for an exact linear endpoint + +This scoped proof was produced by Nick Petalas. The polynomial root bound, +finite-union argument, Cartesian fiber bound and weighted matroid greedy +method are classical. The contribution is their explicit application to the +finite-template exact helper interface, with a bounded witness constructor +and a rank-sensitive finite-grid certificate. No priority is claimed for +those general mathematical methods. + +Sagar Thakrar / thakrarsagar's [PR1133](https://github.com/CrocSwap/integer-mult-bounds/pull/1133), +retained `rational-lift-descent-seed95/PROOF.md`, already uses the same +N(d-1)+1 polynomial-avoidance bound for support descent. That bound is +credited and reused below, not claimed as new. The new application concerns +full endpoint menus; the support-descent theorem is not replayed or audited. + +## Exact interface + +Let K be an infinite field, d,m positive integers, and T:K^d -> K^m linear. +Fix a finite menu A_1,...,A_N of linear maps with the same domain and codomain. +A selector s:K^d -> {1,...,N} may be arbitrary, with no computability, +continuity or observation restriction. Its output is A_{s(x)}x. Coefficients +inside the A_j are fixed independently of x. + +Every arbitrary initial helper coordinate belongs to the domain. Every +required dirty restoration coordinate belongs to the codomain. A fixed +program can have temporary scratch, provided its complete specified output +is a linear function of this domain and its required initial scratch state +is fixed. This theorem asserts no physical legality of any such program. + +## Finite-menu obstruction + +**Theorem 1.** The selector can satisfy A_{s(x)}x=Tx for every x in K^d if +and only if A_j=T for at least one j. + +The reverse implication uses a constant selector. For the forward direction, +suppose every D_j=A_j-T is nonzero and choose a nonzero row l_j of each D_j. +The polynomial product P(x)=product_j l_j(x) is nonzero because K[x_1,...,x_d] +is an integral domain. A nonzero polynomial over an infinite field cannot +vanish at every point. This last fact follows by induction on the number +of variables, using the univariate root bound for each coefficient. +There is therefore an x with every l_j(x) nonzero. Each D_j x is nonzero, +contradicting the selector's claimed endpoint at that x. + +An equivalent proof says that finitely many proper linear subspaces cannot +cover a vector space over an infinite field. This is a classical lemma; +its use here concerns a complete arbitrary-input endpoint, not the +information available to a branching controller. + +**Cost corollary.** Fix any finite menu of globally legal programs for one +input/output contract. Let B be any allowed set of their complete invoices, +including physical charges already required by that contract. If a selector +uses only entries with invoices in B and achieves T on every input, one +fixed entry with an invoice in B already achieves T. This holds for a scalar +budget or for several simultaneous resource bounds. It proves no new lower +bound on the fixed programs themselves. It prevents finite-menu selection +alone from escaping an already established fixed-menu exclusion. + +Apply the corollary only when the fixed entry is legal for the full input +domain. A native operation legal only on its selected branch does not meet +this premise. An instruction-count bound with a finite fixed-coefficient +alphabet gives finitely many words. A paid-call bound alone does not give +a finite menu if unbounded free arithmetic is allowed. + +## Explicit rational counterexample + +**Theorem 2.** Over Q, when every D_j is nonzero, some integer +0 <= t <= N(d-1) makes x(t)=(1,t,t^2,...,t^(d-1)) a counterexample to every +menu entry simultaneously. Every coordinate has magnitude at most +max(1,[N(d-1)]^(d-1)); for d=1 take x=(1) separately. + +A chosen nonzero row of D_j gives a nonzero polynomial l_j(x(t)) of degree +at most d-1. At most N(d-1) distinct integers can be roots of any of those +N polynomials. The N(d-1)+1 tested integers contain a common nonroot. +Testing the entire D_j x(t), rather than just that row, is also sound. +The implementation stops at its first simultaneous counterexample. It +uses exact rational arithmetic and does not enumerate branch predicates. + +The number of curve tests cannot be reduced in general for this curve and +test order. Take d=3, N=4, T=0, with the four scalar-output rows equal to +the coefficient vectors of (t-2j)(t-2j-1), j=0,1,2,3. Every t=0,...,7 is +a root of some row, and t=8 is a common nonroot. The returned vector is +(1,8,64). This sharpness example concerns general linear endpoints; it +claims no optimality of a physical helper program or of all witness methods. + +## Rank-sensitive Cartesian-grid obstruction + +Let S_i be nonempty finite subsets of a field K and s_i=|S_i|. Here K may +be finite. For a nonzero defect D_j of rank r_j, define + + W_j = max product_{i in B} s_i, + +where B ranges over the r_j-element independent column bases of D_j. +Then + + |ker(D_j) intersect product_i S_i| <= product_i s_i / W_j. + +To prove this, fix all coordinates outside one such B. The independent +columns in B make the remaining coordinates uniquely determined if a +solution exists. There are product_{i outside B} s_i outside assignments. +Choose B with the largest product to obtain the bound. + +The union bound now gives **Theorem 3**: + + sum_j 1/W_j < 1 + +implies that some point of the Cartesian grid defeats every menu entry, +regardless of the selector. For equal sizes s this becomes +sum_j s^(-r_j)<1. In particular, N entries each having defect rank at +least r cannot cover such a grid when N (x,y,z+x-a*y), a in F_p, + (x,y,z) -> (x,y,z+y) + +collectively implement I_3 under a suitable selector on every input. If +y is nonzero choose a=x/y; otherwise choose the final shear. Each individual +map is different from I_3. This example changes the field premise. + +Finiteness also matters over Q. The shears with every nonzero rational +normal (a,b), changing z to z+a*x+b*y, form an infinite menu. For each +(x,y) choose (a,b)=(y,-x), except choose (1,0) at (0,0). One shear acts +as identity at each point, but no fixed shear is identity on all of Q^3. + +For a finite-template complex helper proposal, write every full leaf map +and its required input/output coordinates before applying Theorem 1. If +all leaves miss the endpoint, arbitrary data-dependent branching cannot +repair that menu. Theorem 2 supplies a small exact failing input when the +maps are rational. Theorem 3 can obstruct a bounded-grid claim even over +finite fields. These results can stop this specific proposed escape route +before a physical implementation campaign. + +Restricted reachable inputs, approximate endpoints, rounded arithmetic, +nonlinear leaf maps, infinitely many coefficient choices, extra retained +branch outputs and a changed consumer are outside the exact interface. +The theorem neither excludes these alternatives nor asserts they are free. +It does not establish the fixed maps, an actual selected P104 menu, +compiler closure, native costs, a complete supplier or a new kappa. diff --git a/research/finite-menu-adaptivity/README.md b/research/finite-menu-adaptivity/README.md new file mode 100644 index 0000000000..934a49d389 --- /dev/null +++ b/research/finite-menu-adaptivity/README.md @@ -0,0 +1,114 @@ +# Finite-menu adaptivity cannot repair an exact helper endpoint + +Scoped mathematical obstruction, with finite exact corroboration. Over an +infinite field, arbitrary data-dependent selection among finitely many fixed +linear helper programs implements an exact arbitrary-input endpoint only if +one fixed program already implements it. Every dirty input and every required +restoration output must be part of the same contract. + +For N wrong rational maps on d inputs, the explicit witness constructor finds +one input missed by every map after at most N(d-1)+1 tests of +(1,t,...,t^(d-1)). The polynomial-avoidance bound is already used in Sagar +Thakrar / thakrarsagar's [PR1133](https://github.com/CrocSwap/integer-mult-bounds/pull/1133) +for support descent and is credited here. A four-map example needs all nine tests and +returns (1,8,64). For a Cartesian grid with coordinate sizes s_i, a stronger +rank-sensitive obstruction is + + sum_j 1/W_j < 1, + W_j = maximum product of s_i over a column basis of A_j-T. + +For equal sizes s, this is sum_j s^(-rank(A_j-T)) < 1. Maximum-product bases +use exact greedy independence tests. The grid statement holds over any field; +the whole-space finite-menu statement requires an infinite field. +[PROOF.md](PROOF.md) gives the proofs, cost corollary and sharpness examples. + +This supplies a screening rule for a proposed finite-menu escape from a +complex helper or decoder exclusion. It does not establish an exclusion for +any actual P104 menu. A paid-call cap alone need not make the menu finite. +Every fixed word must also be globally legal before the cost corollary applies. +No physical caller, complete supplier, new kappa or selected-frontier change +is claimed. The original construction card has explicitly changed scope. + +## Evidence and reproduction + +Use CPython 3.12 and its standard library, from the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/finite-menu-adaptivity/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/finite-menu-adaptivity/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/finite-menu-adaptivity +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/finite-menu-adaptivity --check-source-history +``` + +Another installed CPython 3.12 may replace that executable. Expected direct +status is `PASS_FINITE_MENU_ADAPTIVITY`. The verifier writes only stdout, +including generated SHA256 bindings to all six package files. No receipt is +handwritten and no predecessor executable or mathematical receipt is consumed. +Catalogue and selected-record pins are historical provenance in SOURCES.json. + +The exact checks enumerate all 729 two-by-three matrices with entries in +{-1,0,1}, all 2,187 declared weighted grids and their 11,139 output fibers. +Rational elimination agrees with a separate determinant/permutation rank +oracle. Exhaustive column bases confirm greedy maximum products. All 2,600 +three-element menus of nonzero ternary rows receive simultaneous witnesses; +their success unions are enumerated on 166,400 grid points. Scope controls +include a tight eight-point restricted grid, all 503 points of F_p^3 for +p=2,3,5,7, an infinite-menu construction on 81 rational fixtures, preservation +of required dirty outputs, rational coefficients and dimension one. Ten +invalid-domain calls reject. Checks remain active with optimization enabled. +These finite enumerations corroborate the written proof; they do not replace it. + +## Scope and overlap + +The scientific base is canonical main +19fdb086ea96af9a9f87936a2b888e10af4ed810, priority revision 8. The +[advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19228363) +specifies the original question and its limits. Search covered live open PRs, +recent account work, handoffs, active Discussions, distinctive main README and +proof terms, and merged-PR terms. The overlap helper reported 393 open PRs and +5,630 Discussion records with complete remote pagination. Sparse local notes +and arbitrary code diffs were incomplete; no search proves novelty. + +Related work has different contracts. PR5997 bounds adaptive observation +capacity with a cited missing-dimension premise. PR5961 counts finite-field +minor selection. The retained centre-nonlinear-fresh-floor uses topological +dimension for continuous or semialgebraic observations. This package concerns +selection among fixed full endpoint maps, allows an arbitrary selector and +supplies no observation-capacity or header-price theorem. Those results are +context, not dependencies being replayed or verified. + +## Open next questions + +1. Apply the certificate to one actual source-bound complex helper menu. + Export every globally legal leaf's full endpoint and complete invoice, + then run the witness constructor. The missing menu and physical contract + block a source-specific exclusion. +2. Bound approximate finite-menu endpoints under a physical norm and a bounded + magnitude domain. This could inform rounded execution, but first needs a + priced error tolerance and restoration contract. The exact theorem does + not provide either. Structured questions are in TASK.json. + +## Implementation limits and credit + +The checker has no recursion or unbounded loop. The public matrix boundary caps dimensions +at eight, menus at 32 entries and input rational components at 64 bits. +The witness loop has at most 225 iterations. Minor enumeration is separately +capped at four by four, and every fixture domain is explicitly finite. All +functions are shorter than 60 physical lines. Internal checks use exceptions. + +Managed-runtime allocation is a Power of Ten rule 3 deviation. Exact integers, +fractions and bounded containers allocate during this offline checker; no +fixed byte allocation guarantee is claimed. Input dimensions and coefficients, +fixed fixture inventories and 120-second registered timeouts bound the work. +Rule 9 has ten explicitly listed invalid-domain callbacks, used only by the +negative-control loop. The call targets and lifetimes are fixed. Warning-strict +normal and optimized execution and in-memory syntax inspection provide the +available diagnostics; no standalone static analyzer or global CI change is +introduced. + +This contribution was produced by Nick Petalas. Classical finite-union, +polynomial-root, Cartesian-fiber and column-matroid arguments are credited +as methods rather than new general mathematics. The contribution is the +specified exact-interface application and its bounded certificate tools. +New proof and code are Apache-2.0. Independent human and formal proof-kernel +review are unclaimed. diff --git a/research/finite-menu-adaptivity/SOURCES.json b/research/finite-menu-adaptivity/SOURCES.json new file mode 100644 index 0000000000..0fa52eaaca --- /dev/null +++ b/research/finite-menu-adaptivity/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "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/rational-lift-descent-seed95/PROOF.md", + "usage": "provenance", + "git_blob": "51775d18c09eb4b5f3b1b0be42388ac2041efa1f", + "sha256": "5ab2bab295bd3a2dc5202f90606235776e6354ade301edf8e23fc63344c4c15e" + } + ] +} diff --git a/research/finite-menu-adaptivity/TASK.json b/research/finite-menu-adaptivity/TASK.json new file mode 100644 index 0000000000..47ebd1be26 --- /dev/null +++ b/research/finite-menu-adaptivity/TASK.json @@ -0,0 +1,80 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "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": "Finite-menu data-dependent selection for an exact arbitrary-input linear helper endpoint; rational counterexample construction and rank-sensitive Cartesian-grid certificate.", + "scope_change_reason": "Replace helper construction with a scoped obstruction to finite-menu adaptive scheduling. No selected-word census or new supplier is claimed.", + "bottleneck_link": "Finite-template selection alone cannot bypass a fixed-menu complex helper or decoder endpoint exclusion. Complete dirty inputs, restoration outputs, global legality and every invoice charge remain required.", + "budget_minutes": 60, + "stop_rule": "Stop after the finite-menu proof, rational witness and bounded exact corroboration; leave physical P104 application and approximate variants open.", + "outcome": "negative-result", + "evidence": "PROOF.md gives three all-dimension statements and scope counterexamples. verify.py checks 729 small matrices, weighted grids, all 2600 three-row menus and the sharp witness/search boundary, with generated source-bound output.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Which actual source-bound complex helper menu can be rejected by this certificate?", + "why_it_matters": "It would turn the abstract obstruction into a decision about a specific proposed adaptive split or decoder.", + "first_step": "Export the complete rational endpoint of each globally legal schedule, retaining every arbitrary dirty coordinate, and run the witness constructor.", + "blocked_by": "A complete actual menu and paid boundary contract have not been supplied." + }, + { + "question": "Can an approximate finite-menu endpoint beat every fixed program under one specified norm and magnitude domain?", + "why_it_matters": "The exact equality argument does not quantify approximation and rounded callers need an error budget.", + "first_step": "Fix a physical norm, bounded input domain, complete restoration tolerance and finite menu, then minimize the largest distance from its union of success regions.", + "blocked_by": "No source-specific error tolerance or magnitude allowance is priced here." + } + ] +} diff --git a/research/finite-menu-adaptivity/VERIFY.json b/research/finite-menu-adaptivity/VERIFY.json new file mode 100644 index 0000000000..d5ba5588e1 --- /dev/null +++ b/research/finite-menu-adaptivity/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": 120, + "checks": "Exact rational witnesses, independent minor ranks, maximum-product column bases, enumerated Cartesian fibers and menu unions, strictness and field/menu scope controls, invalid domains." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same mathematical checks with optimization enabled; every contract uses explicit exceptions." + } + ] +} diff --git a/research/finite-menu-adaptivity/verify.py b/research/finite-menu-adaptivity/verify.py new file mode 100644 index 0000000000..805f2d64bb --- /dev/null +++ b/research/finite-menu-adaptivity/verify.py @@ -0,0 +1,243 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration and rational witnesses for the written theorem.""" + +from fractions import Fraction +from hashlib import sha256 +from itertools import combinations, permutations, product +import json +from math import prod +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def matrix(rows): + require(isinstance(rows, (list, tuple)) and 1 <= len(rows) <= 8, + "expected one to eight rows") + require(all(isinstance(row, (list, tuple)) for row in rows), "invalid row") + width = len(rows[0]) + require(1 <= width <= 8 and all(len(row) == width for row in rows), + "expected a rectangular matrix of width at most eight") + require(all(type(x) is int or isinstance(x, Fraction) for row in rows for x in row), + "expected exact rational coefficients") + result = tuple(tuple(Fraction(x) for x in row) for row in rows) + require(all(x.numerator.bit_length() <= 64 and x.denominator.bit_length() <= 64 + for row in result for x in row), "coefficient limit") + return result + + +def difference(left, right): + require(len(left) == len(right) and len(left[0]) == len(right[0]), + "shape mismatch") + return tuple(tuple(a - b for a, b in zip(x, y)) for x, y in zip(left, right)) + + +def image(operator, vector): + require(len(operator[0]) == len(vector), "vector shape mismatch") + return tuple(sum(a * b for a, b in zip(row, vector)) for row in operator) + + +def rank(rows): + if not rows or not rows[0]: + return 0 + work = [list(map(Fraction, row)) for row in rows] + pivot = 0 + for column in range(len(work[0])): + candidates = [i for i in range(pivot, len(work)) if work[i][column]] + if not candidates: + continue + selected = candidates[0] + work[pivot], work[selected] = work[selected], work[pivot] + scale = work[pivot][column] + work[pivot] = [x / scale for x in work[pivot]] + for i in range(pivot + 1, len(work)): + scale = work[i][column] + work[i] = [x - scale * y for x, y in zip(work[i], work[pivot])] + pivot += 1 + if pivot == len(work): + break + return pivot + + +def escape(target_rows, menu_rows): + """Return an input missed by every entry, or reject a menu containing target.""" + target = matrix(target_rows) + require(isinstance(menu_rows, (list, tuple)) and 1 <= len(menu_rows) <= 32, + "expected one to 32 menu entries") + defects = [difference(matrix(entry), target) for entry in menu_rows] + require(all(any(x for row in defect for x in row) for defect in defects), + "menu already contains target") + dimension = len(target[0]) + limit = len(defects) * (dimension - 1) + 1 + for t in range(limit): + vector = tuple(Fraction(t**j) for j in range(dimension)) + if all(any(image(defect, vector)) for defect in defects): + return vector, t, limit + raise ValueError("moment-curve theorem violated") + + +def weighted_basis(defect, sizes): + require(len(sizes) == len(defect[0]) and + all(type(s) is int and 1 <= s <= 32 for s in sizes), "grid size limit") + selected = [] + for column in sorted(range(len(sizes)), key=lambda j: (-sizes[j], j)): + trial = selected + [column] + submatrix = [[row[j] for j in trial] for row in defect] + if rank(submatrix) == len(trial): + selected.append(column) + require(len(selected) == rank(defect), "incomplete column basis") + return tuple(selected), prod(sizes[j] for j in selected) + + +def coverage_bound(target_rows, menu_rows, sizes): + target = matrix(target_rows) + require(isinstance(menu_rows, (list, tuple)) and 1 <= len(menu_rows) <= 32, + "expected one to 32 menu entries") + defects = [difference(matrix(entry), target) for entry in menu_rows] + return sum((Fraction(1, weighted_basis(defect, sizes)[1]) for defect in defects), + Fraction(0)) + + +def minor_rank(rows): + """Independent determinant/permutation oracle, limited to four by four.""" + height, width = len(rows), len(rows[0]) + require(max(height, width) <= 4, "minor oracle limit") + answer = 0 + for size in range(1, min(height, width) + 1): + for rr in combinations(range(height), size): + for cc in combinations(range(width), size): + value = Fraction(0) + for order in permutations(range(size)): + inversions = sum(order[i] > order[j] + for i in range(size) for j in range(i + 1, size)) + value += (-1)**inversions * prod(rows[rr[i]][cc[order[i]]] + for i in range(size)) + if value: + answer = size + return answer + + +def check_grids(): + matrices = [matrix([bits[:3], bits[3:]]) + for bits in product((-1, 0, 1), repeat=6)] + sizes_cases = ((1, 2, 3), (3, 2, 1), (2, 2, 2)) + fibers = 0 + for operator in matrices: + expected_rank = minor_rank(operator) + require(rank(operator) == expected_rank, "rank oracle disagreement") + for sizes in sizes_cases: + basis, weight = weighted_basis(operator, sizes) + weights = [] + for columns in combinations(range(3), expected_rank): + sub = [[row[j] for j in columns] for row in operator] + if not columns or minor_rank(sub) == expected_rank: + weights.append(prod(sizes[j] for j in columns)) + require(weight == max(weights), "weighted-basis optimum failed") + require(len(basis) == expected_rank, "basis rank changed") + points = list(product(*(range(s) for s in sizes))) + outcomes = {} + for point in points: + value = image(operator, point) + outcomes[value] = outcomes.get(value, 0) + 1 + require(all(count * weight <= prod(sizes) for count in outcomes.values()), + "Cartesian fiber bound failed") + fibers += len(outcomes) + return {"matrices": len(matrices), "weighted_grids": len(matrices) * 3, + "enumerated_fibers": fibers} + + +def check_witnesses(): + rows = [row for row in product((-1, 0, 1), repeat=3) if any(row)] + target = [[0, 0, 0]] + grid = tuple(product(range(4), repeat=3)) + witnesses = 0 + for family in combinations(rows, 3): + vector, t, limit = escape(target, [[row] for row in family]) + require(t < limit == 7, "wrong witness budget") + require(all(image([row], vector) != (0,) for row in family), + "returned vector is not a simultaneous witness") + bound = coverage_bound(target, [[row] for row in family], (4, 4, 4)) + covered = sum(any(image([row], point) == (0,) for row in family) + for point in grid) + require(bound == Fraction(3, 4) and covered <= bound * len(grid), + "menu coverage exceeds strict grid bound") + witnesses += 1 + family = [[[2*j*(2*j + 1), -(4*j + 1), 1]] for j in range(4)] + vector, t, limit = escape(target, family) + require((vector, t, limit) == ((1, 8, 64), 8, 9), "sharp curve fixture") + require(escape([[0]], [[[1]], [[-1]]]) == ((1,), 0, 1), "dimension one") + rational = [[[Fraction(1, 3), 0]], [[0, Fraction(2, 5)]]] + require(escape([[0, 0]], rational)[0] == (1, 1), "rational coefficients") + return {"three_entry_menus": witnesses, "sharp_curve_tests": 9, + "menu_grid_points": witnesses * len(grid), + "rational_and_dimension_one_controls": 2} + + +def check_scope(): + identity = matrix([[1, 0, 0], [0, 1, 0], [0, 0, 1]]) + menus = [matrix([[1, 0, 0], [0, 1, 0], [1, sign, 1]]) for sign in (-1, 1)] + grid = list(product((-1, 1), repeat=3)) + require(all(any(image(entry, x) == x for entry in menus) for x in grid), + "strict-inequality boundary fixture") + require(coverage_bound(identity, menus, (2, 2, 2)) == 1, + "strictness boundary has incorrect weight") + vector, _, _ = escape(identity, menus) + require(all(image(entry, vector) != vector for entry in menus), "full dirty endpoint") + require(all(entry[:2] == identity[:2] for entry in menus), "projection control") + finite_points = 0 + for p in (2, 3, 5, 7): + normals = [(1, -a) for a in range(p)] + [(0, 1)] + for x, y, z in product(range(p), repeat=3): + require(any((a*x + b*y) % p == 0 for a, b in normals), "finite field cover") + finite_points += 1 + require(all(any((a*x + b*y) % p for x, y in product(range(p), repeat=2)) + for a, b in normals), "finite leaf unexpectedly equals identity") + rational_points = 0 + for x, y in product(range(-4, 5), repeat=2): + normal = (y, -x) if (x or y) else (1, 0) + require(any(normal) and normal[0]*x + normal[1]*y == 0, "infinite menu") + rational_points += 1 + return {"sharp_restricted_grid_points": len(grid), + "finite_field_points": finite_points, "infinite_menu_controls": rational_points, + "dirty_projection_control": 1} + + +def check_rejections(): + cases = ( + lambda: escape([[0]], []), + lambda: escape([[0]], [[[0]]]), + lambda: escape([[0]], [[[1, 0]]]), + lambda: escape([[0]], [[[1]]] * 33), + lambda: matrix([[0.0]]), + lambda: matrix([[True]]), + lambda: matrix([[2**65]]), + lambda: matrix([[1], [1, 2]]), + lambda: weighted_basis(matrix([[1]]), (0,)), + lambda: weighted_basis(matrix([[1]]), (True,)), + ) + for case in cases: + try: + case() + except ValueError: + continue + raise ValueError("invalid domain was accepted") + return len(cases) + + +def main(): + results = {"grid_checks": check_grids(), "witness_checks": check_witnesses(), + "scope_checks": check_scope(), "domain_rejections": check_rejections()} + package = Path(__file__).resolve().parent + results["source_sha256"] = { + name: sha256((package / name).read_bytes()).hexdigest() + for name in ("README.md", "PROOF.md", "verify.py", "TASK.json", + "SOURCES.json", "VERIFY.json")} + results["status"] = "PASS_FINITE_MENU_ADAPTIVITY" + print(json.dumps(results, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()