diff --git a/research/theta-compressed-constructor/PROOF.md b/research/theta-compressed-constructor/PROOF.md new file mode 100644 index 0000000000..fb56228366 --- /dev/null +++ b/research/theta-compressed-constructor/PROOF.md @@ -0,0 +1,194 @@ +# An encoded-width constructor for theta(2,3,3) + +This scoped proof and constructor were produced by Nick Petalas. Apache-2.0. +Independent human and formal proof-kernel review are unclaimed. + +## Contract and new result + +Use vertex order `(u,v,a,b,c,d,e)` and edge order +`(ua,av,ub,bc,cv,ud,de,ev)`. A width vector `d` consists of seven arbitrary +nonnegative integers. Put `S=sum(d)` and + +``` +nu(d) = max sum_e x_e + over integer x_e >= 0 with sum_(e incident v) x_e <= d_v. +``` + +JoyboyBrian's [PR #5218](https://github.com/CrocSwap/integer-mult-bounds/pull/5218), +retained in `research/theta-query-capacity`, proves that the exact fitting +rank is `S-nu(d)` over every field. Its contract has identity diagonal blocks, +zeros on both ordered nonedge blocks, and arbitrary directed rectangular +edge blocks. We cite that theorem. We do not replay its proof or verifier. +Its attaining residual-state dynamic program has a stated bound +`product_v(d_v+1)` on its states. + +The new result is an optimal compressed constructor whose number of integer +arithmetic operations is bounded independently of `d`. If +`B=max(1,bit_length(max(d)))`, its bit complexity and working storage are +`O(B)` for this fixed graph. Output consists of eight shared-coordinate +counts, seven private counts, seven half-cover coefficients, and the rank. +No payload coordinates need to be expanded. This is a theoretical encoded-width +improvement, not a measured runtime comparison or a new fitting-rank theorem. + +Define the fixed set + +``` +Y = { y in {0,1,2}^7 : y_u+y_v >= 2 for every edge uv }. +``` + +An additional explicit value formula is + +``` +nu(d) = floor( min_(y in Y) sum_v d_v*y_v / 2 ). (1) +minimum fitting rank = S - floor(min_(y in Y) d dot y / 2). (2) +``` + +There are 267 vectors in `Y`, enumerated by the verifier. Neither (1) nor the +constructor requires the predecessor's residual-state table. The classical +ingredients are LP strong duality, incidence-matrix basis enumeration and +half-integral matching/vertex-cover structure. Their application here is the +new compressed implementation and certificate, not a claim to invent them. +For classical context see Alexander Schrijver's *Combinatorial Optimization*, +sections 30.2 and 31, in the author's +[official contents](https://homepages.cwi.nl/~lex/files/book.pdf). +The structural arguments needed here follow below. + +## Fractional matching structure + +Let `A` be the seven-by-eight unsigned vertex-edge incidence matrix and +consider the bounded nonempty polytope `P={x>=0: Ax<=d}`. Choose any extreme +point and let `F` be its positive edge support. Restrict `A` to rows whose +capacity inequalities are tight and columns in `F`. These columns are +independent. Otherwise a nonzero null vector on `F` could be added and +subtracted with sufficiently small magnitude. Positive edges remain positive, +tight equations remain equalities and all slack inequalities remain valid, +contradicting extremality. + +Consequently every connected support component has at most as many edges +as vertices. It is a tree or is unicyclic. In a tree on `n` vertices there +are `n-1` columns, so at least `n-1` vertex rows must be tight. Root at the +possibly slack vertex, or any vertex if all are tight. Eliminate leaves +toward the root. Each eliminated edge equals an integer capacity minus +previous integer edge values, so every tree edge is integral. + +A unicyclic component has as many edges as vertices and therefore every +vertex row is tight. Remove its attached trees by the same leaf elimination. +An even cycle has an alternating column dependence, so the remaining cycle +must be odd. On that cycle, consecutive edge sums are integers. Solving the +odd cyclic system shows that all edge values are half-integers, and their +fractional parts are either all zero or all one half. Thus the nonintegral +edges of any extreme point are a vertex-disjoint union of odd cycles. + +The only odd cycles in this theta graph are +`u-a-v-c-b-u` and `u-a-v-e-d-u`. They share `u,a,v`, so at most one can occur +in the nonintegral support of an extreme point. The other simple cycle has +length six. This statement follows by taking two of the three internally +disjoint u-v paths. A simple cycle cannot use three paths without revisiting +an endpoint. + +## Rounding is exact for the objective + +Choose an extreme point maximizing `sum(x)`, with value `L`. If it is integral, +it already gives an integral optimum. Otherwise exactly one odd cycle has +half-integer edge values, while every other edge is integral. Round alternately +down and up along the cycle, starting and ending with down. At every cycle +vertex the incident total remains unchanged except at the meeting point of +the two down edges, where it decreases by one. All capacity inequalities and +nonnegativity are preserved. The objective decreases by exactly one half. +Since the cycle has odd length, `L` itself is then an integer plus one half. +In both cases the rounded integer matching has value `floor(L)`. Conversely +every integer matching has value at most `floor(L)`. Hence + +``` +nu(d) = floor(L). (3) +``` + +Zero widths, disconnected positive supports and `d=0` are included. No +positive-width or nondegeneracy assumption enters the rounding argument. + +## A fixed cover formula and small optimality certificate + +The fractional matching LP has dual + +``` +min sum_v d_v*z_v, with z_v>=0 and z_u+z_v>=1 on each edge. +``` + +Truncate every `z_v` at one. Feasibility remains valid and the objective +does not increase, since capacities are nonnegative. There is therefore an +optimum in the compact polytope with `0<=z_v<=1`. Its vertices are half-integral. +To see this, inspect the graph of active edge equalities between fractional +coordinates. An active edge to an integral coordinate would force its other +coordinate to be integral. In a bipartite fractional component, alternating +small plus/minus perturbations preserve every active equality, all box bounds +and every slack inequality, contradicting extremality. Every fractional +component must therefore contain an odd cycle, whose alternating equations +force all its coordinates to one half. All coordinates belong to `{0,1/2,1}`. + +LP strong duality now gives `L=min_(y in Y) d dot y / 2` and (3) proves (1). +The constructor returns an integral matching `x`, private counts +`p_v=d_v-sum_(e incident v)x_e`, and a vector `y in Y` satisfying + +``` +x_e,p_v >= 0; p_v + sum_(e incident v)x_e = d_v; +sum_e x_e = floor(d dot y / 2). (4) +``` + +These are independently checkable optimality certificates. Indeed every +integer matching `w` satisfies +`2 sum(w) <= sum_e w_e*(y_u+y_v) <= sum_v d_v*y_v`. +Thus (4) proves optimality using only integer sums, even if the constructor +were replaced by an untrusted program. The all-field fitting-rank conclusion +then uses the cited #5218 theorem. The certificate alone is a matching result. + +## Enumerating a fractional optimum without width expansion + +For an extreme point with `k` positive edges, column independence supplies +`k` tight rows forming a nonsingular square incidence submatrix `C`. In +particular `k<=7`. Enumerate all choices of `k` edges and `k` vertices, +for `1<=k<=7`. For each nonsingular `C`, precompute `2*C^-1`. Its entries +are integers. One direct justification is to solve each connected component +of this square restricted incidence system. A component with as many columns +as rows is a tree with one omitted vertex equation, or an odd unicyclic +component with every vertex equation retained; leaf elimination and the odd +cycle equation give denominators dividing two. An even cycle is singular. +Equivalently these are the tree/odd-cycle bases of an unsigned incidence matrix. + +Evaluate that fixed linear template at the corresponding widths. Put zero +on edges outside its chosen support and reject negative or over-capacity +values. Include the all-zero point explicitly. The list contains every +extreme point and hence an optimum. The implementation compares doubled +integer objective values and then rounds the sole fractional cycle as above. +It enumerates `Y` independently and checks equality of the fractional primal +and dual objectives before accepting. Finally it checks (4). + +There are fewer than 6,435 square submatrix candidates and exactly 1,583 +nonsingular templates for this graph. Initialization uses only fixed small +rational matrices of order at most seven. Evaluating a template, checking its +capacities, comparing objectives and checking a cover use a fixed number of +additions, comparisons and multiplications by fixed integers. All intermediate +integers have `B+O(1)` bits. Division by two is a shift. Thus the constructor +and its optimality certificate require `O(B)` bit operations and `O(B)` +working bits, with constants depending on this seven-vertex graph. +Parsing/printing and coordinate expansion are separate interfaces. In +particular a full fitting matrix has `S^2` entries and is not claimed to be +produced in encoded-width time. + +## Evidence and limitations + +The verifier independently computes optimal copy matchings on all 2,187 +width vectors in `{0,1,2}^7`, including every zero-width support. It compares +the new constructor's certificates on all of them. It checks 130 explicitly +expanded attaining matrices in three characteristics, giving 390 rank +calculations, and checks all 2,109 matrix entries against the fitting contract. +There are 76 half-integer fractional optima in this domain. Nine additional +fixtures use widths up to 4,099 bits without coordinate expansion. Fourteen +controls reject malformed inputs, damaged certificates and a missing basis +family. These finite checks corroborate the written all-width proof. + +The source theorem and its proof remain cited premises, rather than new +results or independently revalidated claims. Physical copies, coefficient +delivery, frames, restoration, owner lifetimes, precision, fixed tapes, +compiler/supplier admission and a complete multiplication theorem are outside +scope. No new kappa or selected-frontier change is claimed. We stop at this +constructor and do not start a larger graph or physical implementation search. diff --git a/research/theta-compressed-constructor/README.md b/research/theta-compressed-constructor/README.md new file mode 100644 index 0000000000..01f4e95556 --- /dev/null +++ b/research/theta-compressed-constructor/README.md @@ -0,0 +1,125 @@ +# Construct optimal theta sharing in encoded-width time + +Scoped proof and deterministic constructor, produced by Nick Petalas. +Apache-2.0. Independent human and formal proof-kernel review are unclaimed. + +For the fixed seven-vertex theta(2,3,3) query mask, an optimal coordinate-sharing +recipe can be computed with a number of integer arithmetic operations independent +of the seven payload widths. If the largest width has B bits, construction and +working storage use O(B) bit operations and bits. The output is eight shared +counts, seven private counts, a seven-entry half-cover and the exact fitting rank. + +This replaces the `product_i(d_i+1)` residual-state algorithm in JoyboyBrian's +[PR #5218](https://github.com/CrocSwap/integer-mult-bounds/pull/5218). +Its all-field fitting-rank theorem is cited, not replayed or audited. The +new contribution is the compressed constructor and its integer optimality +certificate. This is a theoretical complexity improvement, with no measured +runtime comparison and no new kappa. + +Write `S=sum(d)` and let `Y` contain the 267 vectors `y in {0,1,2}^7` with +`y_u+y_v>=2` on every edge. The implementation also gives the value formula + +``` +maximum shared pairs = floor(min_(y in Y) d dot y / 2) +minimum fitting rank = S - maximum shared pairs +``` + +[PROOF.md](PROOF.md) proves the all-width constructor. A fractional matching +extreme point has at most one half-integral odd cycle because the theta graph's +odd cycles share endpoints. Alternating rounding loses at most one half and +attains the integer optimum. A fixed family of 1,583 incidence-matrix templates +constructs a fractional optimum without expanding any coordinates. The returned +integer matching and half-cover certify optimality using only integer sums. + +The complete ordered fitting contract retains identity diagonal blocks and +zeros on both ordered nonedges. Allowed rectangular blocks may be nonsymmetric +and noncommuting. The compressed recipe constructs a block-diagonal sum of +two-coordinate all-ones channels and private coordinates when expansion is +desired. Writing a full matrix still costs its full output size. + +## Reproduction and evidence + +From the repository root, use CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/theta-compressed-constructor/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/theta-compressed-constructor/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/theta-compressed-constructor +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/theta-compressed-constructor --check-source-history +``` + +The direct checks print `PASS_THETA_COMPRESSED_CONSTRUCTOR`. They cover all +2,187 vectors in `{0,1,2}^7` against an independent one-copy matching recurrence, +390 rank calculations over F2, F3 and F101 on 130 attaining matrices, all 2,109 +fitting entries, nine large-width fixtures up to 4,099 bits, and fourteen +rejection controls. The small domain contains 76 half-integer fractional optima. +The finite checks corroborate the written proof; they do not prove it by census. + +Pass `--receipt /absolute/path/outside/checkout.json` to either direct check +for a generated receipt binding counts and every package file's SHA256. +Default verification writes nothing. It hashes the two cited source documents; +it imports no predecessor executable and repeats no predecessor census. + +To use the constructor from this package directory: + +```python +from constructor import compile_templates, construct, validate + +templates = compile_templates() # graph-only initialization, reusable +widths = (2**4096,) * 7 +certificate = construct(widths, templates) +validate(widths, certificate) +``` + +## Scope, credit and overlap + +The revision-8 `complex-rank-shape-decoder` card is changed to this scoped +algorithmic side result. The selected baseline reported +`PASS_RESEARCH_BASELINE_BINDINGS_ONLY`; no selected supplier replay was run. +The selected conditional kappa and all five framework assumptions remain. +There is no physical supplier, complete invoice, native execution, precision, +fixed-tape, restoration, owner-lifetime or compiler admission claim. + +Credit JoyboyBrian #5218 for the exact theta fitting-rank theorem, matching +reduction and earlier constructor; JoyboyBrian #5023, Tekalign #3362, Nick +Petalas #4909, Sagar Thakrar #2484 and the retained query-mask lineage. +LP duality, half-integrality and incidence basis methods are classical. +No general matching-theory or literature-wide priority is claimed. +The predecessor package and its attribution remain unchanged. + +The advance [CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19221484) +records the target. Overlap checking read live PRs, this account's recent +contributions, active Discussions, local reservations, all-main README terms +and merged-PR searches. The cached task scan reports its own freshness and +sparse omissions. These checks do not exclude unpublished or unindexed work. +The predecessor's current Open next questions concern physical callers; this +constructor improvement is a new algorithmic extension, not a claim to answer +that physical question. There is no automatic wider graph search. + +## Open next questions + +Can an actual recursive caller supply this theta ordered read mask with a +favorable complete invoice? First identify its literal incidence map and +charge copies, coefficient delivery, owner lifetimes and restoration. A +source-bound producer/consumer and a physical tariff remain missing. +The structured question is in [TASK.json](TASK.json). Stop this contribution +at the compressed constructor. + +## Implementation constraints + +The two new Python files use bounded structured iteration and no recursion. +All functions are under 60 physical lines. Constructor loops have fixed bounds +from the seven vertices and eight edges; matrix checks enforce at most fourteen +coordinates. Exhaustive verification has exactly 3^7 small width vectors and +nine large fixtures. Explicit `ValueError` contracts remain active under `-O`. + +Power-of-ten rule 3 has a managed-runtime deviation in both files. Python +allocates arbitrary-precision integers and finite collections dynamically. +The constructor keeps a fixed number of O(B)-bit integers and graph-only +templates; the verifier bounds its table at 2,187 entries and matrices at +14 by 14. No fixed-allocation claim is made. A fixed-storage port would be +needed only for a runtime requiring it. Rule 9 has a bounded standard-library +callback deviation for `min`/`sorted` keys and the rejection-test callable; +targets and lifetimes are local and explicit. There is no dynamic code +generation or external solver. Warning-strict normal and optimized execution +and source compilation provide the applicable interpreter diagnostics. diff --git a/research/theta-compressed-constructor/SOURCES.json b/research/theta-compressed-constructor/SOURCES.json new file mode 100644 index 0000000000..4a73558b7f --- /dev/null +++ b/research/theta-compressed-constructor/SOURCES.json @@ -0,0 +1,30 @@ +{ + "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/theta-query-capacity/PROOF.md", + "usage": "input", + "git_blob": "bd2cadc9f05068a9adcd8b2ce27c4fe915631bd6", + "sha256": "aae3fdfef618b31db7ac21fb8a67a13c34dfda2e8f0bc305507443297083da26" + }, + { + "path": "research/theta-query-capacity/README.md", + "usage": "input", + "git_blob": "55f64a7ff4a5966a20edf9363c079fb66172a14a", + "sha256": "f6a02a1e66d7a2062573477a799b997ca0580bf426b22f00829dcab7a7ca7528" + } + ] +} diff --git a/research/theta-compressed-constructor/TASK.json b/research/theta-compressed-constructor/TASK.json new file mode 100644 index 0000000000..f1930eb1fd --- /dev/null +++ b/research/theta-compressed-constructor/TASK.json @@ -0,0 +1,92 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?", + "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", + "docs/research/recursive-invoice-preflight.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": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.", + "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": [ + "coframe", + "signed moment", + "5693", + "5698" + ], + "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": "Encoded-width exact theta(2,3,3) matching constructor and integer optimality certificates", + "scope_change_reason": "A scoped algorithmic side result on the exact query-mask contract of JoyboyBrian PR5218; replace its pseudopolynomial residual-state constructor rather than claiming a current supplier invoice gain.", + "bottleneck_link": "Width-compressed coordinate-sharing counts make the cited decoder-query dimension contract constructible at recursively large payloads. Physical supplier costs remain unpriced; this is a side result.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified compressed constructor; no wider graph or physical supplier campaign.", + "outcome": "completed", + "evidence": "PROOF.md; constructor.py; independent copy-matching verifier and generated source-hash receipts", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can this fixed theta constructor be connected to an actual ordered-read-mask caller with a favorable complete invoice?", + "why_it_matters": "An exact query dimension and a compressed recipe do not establish physical supplier savings.", + "first_step": "Identify a literal source incidence map and charge copies, coefficient delivery, owner lifetimes and restoration.", + "blocked_by": "No source-bound producer/consumer or physical tariff is supplied." + } + ], + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19221484", + "source_question": { + "source": "PR #5218", + "author": "JoyboyBrian", + "kind": "new algorithmic extension, not a claimed predecessor open question" + }, + "overlap": { + "canonical_main": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "checked_utc": "2026-10-27T16:16:00Z", + "coverage": "100 recent open PRs with bodies; 200 account PRs; 100 latest handoff comments and 15 active discussions; all-main README key terms and merged-PR searches; cached task overlap scan", + "limits": "Arbitrary diffs, older account PR bodies, unpublished work and sparse local notes may overlap." + }, + "environment": { + "python": "3.12.15", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "dependencies": "Python standard library only" + } +} diff --git a/research/theta-compressed-constructor/VERIFY.json b/research/theta-compressed-constructor/VERIFY.json new file mode 100644 index 0000000000..0546df189b --- /dev/null +++ b/research/theta-compressed-constructor/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/theta-query-capacity/PROOF.md", + "research/theta-query-capacity/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All 2187 small width vectors against independent copy matching; attaining matrix ranks in three fields; large-width certificates and rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat all checks with optimization; validation does not depend on assert." + } + ] +} diff --git a/research/theta-compressed-constructor/constructor.py b/research/theta-compressed-constructor/constructor.py new file mode 100644 index 0000000000..c4b661eb6a --- /dev/null +++ b/research/theta-compressed-constructor/constructor.py @@ -0,0 +1,123 @@ +"""Exact compressed coordinate sharing on theta(2,3,3), Apache-2.0.""" + +from fractions import Fraction +from itertools import combinations, product + + +EDGES = ((0, 2), (2, 1), (0, 3), (3, 4), (4, 1), (0, 5), (5, 6), (6, 1)) +ODD_CYCLES = ((0, 1, 4, 3, 2), (0, 1, 7, 6, 5)) + + +def need(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def integers(values: tuple, size: int) -> None: + need(isinstance(values, tuple) and len(values) == size, "wrong tuple shape") + need(all(type(x) is int and x >= 0 for x in values), "invalid nonnegative integer") + + +def doubled_inverse(matrix: tuple) -> tuple | None: + """Return 2*A^-1, or None for a singular incidence submatrix.""" + n = len(matrix) + need(1 <= n <= 7, "inverse dimension") + rows = [[Fraction(x) for x in row] + [Fraction(i == j) for j in range(n)] + for i, row in enumerate(matrix)] + for column in range(n): + pivot = next((i for i in range(column, n) if rows[i][column]), None) + if pivot is None: + return None + rows[column], rows[pivot] = rows[pivot], rows[column] + scale = rows[column][column] + rows[column] = [x / scale for x in rows[column]] + for i in range(n): + if i != column: + scale = rows[i][column] + rows[i] = [x - scale * y for x, y in zip(rows[i], rows[column])] + result = tuple(tuple(2 * x for x in row[n:]) for row in rows) + need(all(x.denominator == 1 for row in result for x in row), "non-half-integral basis") + return tuple(tuple(int(x) for x in row) for row in result) + + +def compile_templates() -> tuple: + """A fixed graph-only enumeration; never loops over payload coordinates.""" + templates = [] + for size in range(1, 8): + for edge_ids in combinations(range(8), size): + for vertex_ids in combinations(range(7), size): + matrix = tuple(tuple(int(v in EDGES[e]) for e in edge_ids) + for v in vertex_ids) + inverse = doubled_inverse(matrix) + if inverse is not None: + templates.append((edge_ids, vertex_ids, inverse)) + need(len(templates) <= 6435, "template enumeration bound") + return tuple(templates) + + +def covers() -> tuple: + return tuple(y for y in product(range(3), repeat=7) + if all(y[u] + y[v] >= 2 for u, v in EDGES)) + + +def fractional_optimum(widths: tuple, templates: tuple) -> tuple: + integers(widths, 7) + best = (0,) * 8 + for edge_ids, vertex_ids, inverse in templates: + values = tuple(sum(c * widths[v] for c, v in zip(row, vertex_ids)) + for row in inverse) + if min(values) < 0: + continue + candidate = [0] * 8 + for edge, value in zip(edge_ids, values): + candidate[edge] = value + if any(sum(candidate[e] for e in range(8) if v in EDGES[e]) > 2 * widths[v] + for v in range(7)): + continue + if sum(candidate) > sum(best): + best = tuple(candidate) + dual = min(covers(), key=lambda y: sum(a * b for a, b in zip(widths, y))) + need(sum(best) == sum(a * b for a, b in zip(widths, dual)), "primal/dual gap") + return best, dual + + +def round_cycle(doubled: tuple) -> tuple: + integers(doubled, 8) + odd = {e for e in range(8) if doubled[e] % 2} + result = [x // 2 for x in doubled] + if odd: + cycle = next((cycle for cycle in ODD_CYCLES if set(cycle) == odd), None) + need(cycle is not None, "fractional edges are not one odd cycle") + for position in (1, 3): + result[cycle[position]] += 1 + return tuple(result) + + +def validate(widths: tuple, certificate: dict) -> None: + """Check an integer matching against a half-integral cover upper bound.""" + integers(widths, 7) + need(type(certificate) is dict and set(certificate) == + {"shared", "private", "dual", "rank"}, "certificate fields") + shared, private, dual = (certificate[key] for key in ("shared", "private", "dual")) + integers(shared, 8) + integers(private, 7) + integers(dual, 7) + need(all(x <= 2 for x in dual), "dual alphabet") + need(all(dual[u] + dual[v] >= 2 for u, v in EDGES), "uncovered edge") + need(all(private[v] + sum(shared[e] for e in range(8) if v in EDGES[e]) == widths[v] + for v in range(7)), "coordinate capacity equation") + bound = sum(a * b for a, b in zip(widths, dual)) // 2 + need(sum(shared) == bound, "nonoptimal matching certificate") + need(type(certificate["rank"]) is int and + certificate["rank"] == sum(widths) - sum(shared), "wrong fitting rank") + + +def construct(widths: tuple, templates: tuple) -> dict: + doubled, dual = fractional_optimum(widths, templates) + shared = round_cycle(doubled) + private = tuple(widths[v] - sum(shared[e] for e in range(8) if v in EDGES[e]) + for v in range(7)) + result = {"shared": shared, "private": private, "dual": dual, + "rank": sum(widths) - sum(shared)} + validate(widths, result) + return result diff --git a/research/theta-compressed-constructor/verify.py b/research/theta-compressed-constructor/verify.py new file mode 100644 index 0000000000..ca56030066 --- /dev/null +++ b/research/theta-compressed-constructor/verify.py @@ -0,0 +1,196 @@ +"""Independent bounded checks for the compressed theta constructor.""" + +import argparse +import hashlib +import json +from itertools import product +from pathlib import Path +import sys + + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +sys.path.insert(0, str(PACKAGE)) +from constructor import EDGES, compile_templates, construct, covers, need, validate + + +def authenticate_sources() -> int: + manifest = json.loads((PACKAGE / "SOURCES.json").read_text()) + count = 0 + for row in manifest["files"]: + if row["usage"] == "input": + payload = (ROOT / row["path"]).read_bytes() + need(hashlib.sha256(payload).hexdigest() == row["sha256"], "source drift") + count += 1 + need(count == 2, "source inventory") + return count + + +def copy_matching_table() -> dict: + """Independent one-copy deletion recurrence on all widths in {0,1,2}^7.""" + table = {} + for widths in sorted(product(range(3), repeat=7), key=sum): + if not any(widths): + table[widths] = 0 + continue + vertex = next(i for i in range(7) if widths[i]) + remainder = list(widths) + remainder[vertex] -= 1 + best = table[tuple(remainder)] + for u, v in EDGES: + if vertex not in (u, v): + continue + neighbor = v if vertex == u else u + if remainder[neighbor]: + paired = remainder.copy() + paired[neighbor] -= 1 + best = max(best, 1 + table[tuple(paired)]) + table[widths] = best + return table + + +def matrix_for(widths: tuple, certificate: dict) -> list: + offsets = [sum(widths[:i]) for i in range(7)] + used = [0] * 7 + n = sum(widths) + need(n <= 14, "bounded matrix fixture") + matrix = [[int(i == j) for j in range(n)] for i in range(n)] + for edge, (u, v) in enumerate(EDGES): + for _ in range(certificate["shared"][edge]): + a, b = offsets[u] + used[u], offsets[v] + used[v] + matrix[a][b] = matrix[b][a] = 1 + used[u] += 1 + used[v] += 1 + for i in range(7): + need(used[i] + certificate["private"][i] == widths[i], "matrix coverage") + return matrix + + +def rank_mod(matrix: list, prime: int) -> int: + n = len(matrix) + work = [[x % prime for x in row] for row in matrix] + rank = 0 + for column in range(n): + pivot = next((i for i in range(rank, n) if work[i][column]), None) + if pivot is None: + continue + work[pivot], work[rank] = work[rank], work[pivot] + scale = pow(work[rank][column], -1, prime) + work[rank] = [x * scale % prime for x in work[rank]] + for i in range(rank + 1, n): + scale = work[i][column] + work[i] = [(x - scale * y) % prime for x, y in zip(work[i], work[rank])] + rank += 1 + return rank + + +def fitting_entries(widths: tuple, matrix: list) -> int: + labels = tuple(i for i in range(7) for _ in range(widths[i])) + edges = {frozenset(edge) for edge in EDGES} + count = 0 + for i, u in enumerate(labels): + for j, v in enumerate(labels): + if i == j: + need(matrix[i][j] == 1, "missing diagonal") + elif u == v or frozenset((u, v)) not in edges: + need(matrix[i][j] == 0, "forbidden ordered entry") + count += 1 + return count + + +def check_small(templates: tuple) -> dict: + table = copy_matching_table() + digest = hashlib.sha256() + matrix_count = entry_count = fractional_count = 0 + for widths, optimum in table.items(): + certificate = construct(widths, templates) + need(sum(certificate["shared"]) == optimum, "copy-matching disagreement") + dual_cost = sum(a * b for a, b in zip(widths, certificate["dual"])) + fractional_count += dual_cost % 2 + digest.update(json.dumps([widths, certificate], sort_keys=True).encode()) + if max(widths) <= 1 or widths in ((2,) * 7, (2, 1, 2, 1, 2, 1, 2)): + matrix = matrix_for(widths, certificate) + entry_count += fitting_entries(widths, matrix) + for prime in (2, 3, 101): + need(rank_mod(matrix, prime) == certificate["rank"], "attaining rank") + matrix_count += 1 + return {"width_vectors": len(table), "matrix_ranks": matrix_count, + "fitting_entries": entry_count, "half_integer_optima": fractional_count, + "recipe_sha256": digest.hexdigest()} + + +def check_large(templates: tuple) -> dict: + fixtures = [] + for bits in (64, 257, 4096): + n = 1 << bits + fixtures.extend(((n,) * 7, (n + 1,) * 7, + (n, 1, n + 3, 0, 5 * n, 7, 2 * n + 1))) + ranks = [] + largest = 0 + for widths in fixtures: + certificate = construct(widths, templates) + validate(widths, certificate) + largest = max(largest, max(widths).bit_length()) + if len(set(widths)) == 1: + need(certificate["rank"] == (sum(widths) + 1) // 2, "uniform large rank") + ranks.append(certificate["rank"].bit_length()) + return {"large_fixtures": len(fixtures), "largest_width_bits": largest, + "rank_bit_lengths": ranks} + + +def rejects(function, *arguments) -> None: + try: + function(*arguments) + except ValueError: + return + raise ValueError("negative control accepted") + + +def check_controls(templates: tuple) -> int: + controls = 0 + for widths in ((1,) * 6, (-1,) + (1,) * 6, (True,) + (1,) * 6, + (1.0,) + (1,) * 6, [1] * 7): + rejects(construct, widths, templates) + controls += 1 + widths = (1,) * 7 + certificate = construct(widths, templates) + changes = (("private", (2,) * 7), ("shared", (1,) * 8), + ("dual", (0,) * 7), ("dual", (True,) * 7), + ("rank", certificate["rank"] + 1), ("rank", True)) + for key, value in changes: + damaged = dict(certificate) + damaged[key] = value + rejects(validate, widths, damaged) + controls += 1 + damaged = dict(certificate) + damaged.update(shared=(0,) * 8, private=widths, rank=7) + rejects(validate, widths, damaged) + rejects(validate, widths, {}) + rejects(construct, widths, ()) + return controls + 3 + + +def main() -> None: + parser = argparse.ArgumentParser() + parser.add_argument("--receipt", type=Path) + args = parser.parse_args() + sources = authenticate_sources() + templates = compile_templates() + need(len(templates) == 1583 and len(covers()) == 267, "fixed enumeration inventory") + result = {"sources": sources, "templates": len(templates), "covers": len(covers())} + result.update(check_small(templates)) + result.update(check_large(templates)) + result["rejection_controls"] = check_controls(templates) + result["file_sha256"] = {p.name: hashlib.sha256(p.read_bytes()).hexdigest() + for p in sorted(PACKAGE.iterdir()) if p.is_file()} + payload = json.dumps(result, sort_keys=True, indent=2) + "\n" + if args.receipt: + destination = args.receipt.resolve() + need(not destination.is_relative_to(ROOT), "receipt must be outside checkout") + destination.write_text(payload) + print(payload, end="") + print("PASS_THETA_COMPRESSED_CONSTRUCTOR") + + +if __name__ == "__main__": + main()