diff --git a/research/ternary-moving-frame-floor/PROOF.md b/research/ternary-moving-frame-floor/PROOF.md new file mode 100644 index 0000000000..753125edfb --- /dev/null +++ b/research/ternary-moving-frame-floor/PROOF.md @@ -0,0 +1,165 @@ +# Four unrestricted terms cannot beat thirteen ternary lines + +## Statement and contract + +Let K be any field of characteristic zero. Let P contain the thirteen vectors +in {-1,0,1}^3 whose first nonzero coordinate is 1, in lexicographic order. +Let X be the 13 by 3 matrix with those rows and G = X X^T. Define the binary +13 by 13 matrix B by + +```text +B_st = 1 if s=t or p_s dot p_t=0, and 0 otherwise. +``` + +For an exact decomposition G = sum_j u_j v_j^T over K, set R_j = supp u_j, +A_j = supp v_j, and charge + +```text +C = sum_j rank_F2 B[R_j,A_j]. +``` + +The factors may leave the evaluation code, use arbitrary characteristic-zero +coefficients and cancel. Frames are unrestricted. The pairing B and the +thirteen ports are fixed. No nonnegativity or Gram-factor constraint is +imposed on the factors. + +**Theorem.** Every decomposition with at most four terms has C >= 14. +Every decomposition with at most three terms has C >= 18. The latter bound +is attained by the coordinate decomposition. No attainment of 14, or exact +four-term optimum, is asserted. + +The below-thirteen four-term question of Aaron Wang's PR2518 is therefore +settled negatively for its full-orthogonality pairing. This is a scoped +mathematical obstruction, with a finite exact rank lemma. It is not a search +failure, physical decoder construction or complete multiplication theorem. + +## 1. The exact restriction-rank lemma + +Write E = im X. For 0 <= n <= 13 define + +```text +e(n) = min rank_F2 B[supp(Xa),A], + over nonzero a in K^3 and A subset of P with |A|=n. +``` + +The exact values, in increasing n, are + +```text +n 0 1 2 3 4 5 6 7 8 9 10 11 12 13 +e(n) 0 1 2 3 3 4 4 5 5 6 6 6 7 7. +``` + +Here is a complete finite reduction, including extension fields K. The zero +ports of Xa are the rational vectors p in P satisfying p dot a = 0. +If there are at least two, take two distinct zero ports p,q. They are +linearly independent, and a is a nonzero K-multiple of their rational cross +product d = p cross q. The zero-port set is exactly that of d. Three +independent zero ports would force a=0, which is excluded. + +If there is one zero port p, choose any other port q. The cross product d +vanishes at p, so supp(Xd) is a subset of supp(Xa). If there are no zero +ports, choose any two distinct ports. The same support containment holds. +Deleting rows cannot increase binary rank. Consequently it suffices to +check primitive cross products of all 78 unordered port pairs. + +After division by the coordinate gcd and a sign change making the first +nonzero coordinate positive, there are exactly 25 distinct cross products +and 25 distinct supports. Their support sizes are 9, 10 or 11. The checker +independently reconstructs these directions from primitive vectors in +[-2,2]^3 having at least two zero ports. This box is complete because every +cross-product coordinate is a difference of two products in {-1,0,1}. +Distinct ports are never proportional, so two zero ports are independent. + +For every one of these 25 supports and every one of the 8,192 subsets A, +the checker computes the binary rank twice, using row elimination with high +pivots and transposed-column elimination with low pivots. All 204,800 +comparisons agree. Minimizing by |A| gives the displayed table. The generated +receipt includes an attaining support/subset witness for each entry. +Every listed direction is rational and hence belongs to K, so these +witnesses establish equality as well as the lower bounds. In particular, +every nonzero vector in E has at least nine nonzero entries. + +This finite lemma is the only exhaustive premise. The argument below +quantifies over all decompositions, rather than enumerating frames. + +## 2. A code side is forced at four terms + +The rows of X include the coordinate vectors, so X has rank three. Direct +summation also gives X^T X = 9 I_3. Thus G has rank three over K, its column +and row spaces equal E, and its thirteen columns are pairwise nonproportional. +The last assertion follows from the injectivity of X and the distinct +projective representatives p_t, since G[:,t] = X p_t. + +Remove every zero outer product, leaving k active terms. Necessarily k>=3. +Write U and V for the 13 by k factor matrices, so G=UV^T. Both have rank +at least three. When k=3 both have rank three and both column spaces equal E. + +When k=4, U and V cannot both have rank four: U would be injective as a map +K^4 to K^13 and V^T would be onto K^4, making UV^T have rank four. At least +one therefore has rank three. Its column space equals E, because it contains +the rank-three column space of G or G^T. The symmetry of B makes the tariff +unchanged by transposing the decomposition. We may take the code side to be U. + +This permits arbitrary vectors outside E on the other side. It is precisely +why the result covers moving-frame decompositions beyond a fixed one-extra +identity family. The rank argument is classical and is consistent with +joaqcoo's PR1224 one-sided representation context; that general observation +is not claimed as new. + +## 3. Three active terms + +For k=3, each nonzero v_j lies in E and has support size at least nine. +Each u_j is also a nonzero code vector. The finite lemma therefore gives +rank_F2 B[R_j,A_j] >= min_{9<=n<=13} e(n) = 6. Summing gives C>=18. + +The coordinate decomposition uses u_j=v_j=X e_j. Direct evaluation gives +three tariff ranks of six, so it attains 18. This elementary fixture is +constructed from the definitions; no predecessor census is replayed. + +## 4. Four active terms + +Let n_j=|A_j|. Each n_j is between 1 and 13. Each column of G needs at least +one nonzero coefficient among the corresponding rows of V. If a column uses +only one term, it is proportional to that term's u_j. Because the thirteen +columns of G are pairwise nonproportional, each u_j can serve at most one +such column. At most four columns use only one term; every other column uses +at least two. Therefore + +```text +n_1+n_2+n_3+n_4 >= 4 + 2*9 = 22. +``` + +The restriction-rank lemma gives C >= sum_j e(n_j). Exhausting the 13^4 +ordered size tuples, retaining those with sum at least 22, gives + +```text +min sum_j e(n_j) = 14, +``` + +with one attaining relaxation tuple (1,1,7,13). The checker enumerates every +tuple. This tuple is not asserted to come from an actual factorization. +For a short direct confirmation, e(n)>=(n+1)/2 for 1<=n<=13, with equality +only at n in {1,11,13}. A bill below 14 would be at most 13, hence would +require sum n_j=22 and four equality sizes. Four members of {1,11,13} +cannot sum to 22. Thus C>=14. Combining with the three-term case proves +the theorem for every decomposition with at most four terms. + +## Scope and credit + +Aaron Wang / navinor's PR2518 poses the unrestricted four-term question, +building on his PR2272 screen. DreamingOfClouds's PR2125, PR2228 and PR2111 +supply the dense-polar/COPY model; Cinna Davis's PR2240 supplies the narrower +one-extra fixed-frame construction; joaqcoo's PR1224 supplies the retained +one-sided factorization context. The source packages retain their credit. +The new result is this complete 25-direction restriction-rank certificate +and its application to all four-term factorizations on the thirteen ports. + +The fixed pairing, characteristic zero and at-most-four-term restrictions +are essential to the proved scope. Five factors can have both factor +matrices of rank four, so the forced-code-side argument does not extend +automatically. Changed pairings, masked identities, shared delivery and +physical/native/ownership/restoration/compiler/precision/stock/outer costs +are outside this theorem. No new kappa or selected-frontier change follows. +Independent human and formal proof-kernel review are unclaimed. + +This proof was produced by Nick Petalas. Apache-2.0. diff --git a/research/ternary-moving-frame-floor/README.md b/research/ternary-moving-frame-floor/README.md new file mode 100644 index 0000000000..1445ebd90b --- /dev/null +++ b/research/ternary-moving-frame-floor/README.md @@ -0,0 +1,132 @@ +# A moving-frame COPY floor for thirteen ternary lines + +Every exact factorization of the Gram matrix on the thirteen projective +nonzero lines of {-1,0,1}^3 into at most four scalar outer products has +full-orthogonality binary COPY cost at least **14**. This settles the +below-thirteen question in Aaron Wang / navinor's +[PR2518](https://github.com/CrocSwap/integer-mult-bounds/pull/2518), Open next +question 2. Factors may move freely, leave the evaluation code on one side, +and use arbitrary coefficients over any characteristic-zero field. + +Claim type: scoped written mathematical proof with an exact finite rank +certificate. The minimum with at most four terms lies between 14 and 18; no claim +of sharpness at 14 is made. Three terms have sharp cost 18. No new kappa, +physical decoder, supplier admission or selected-frontier change is claimed. +This contribution was produced by Nick Petalas. Independent human and formal +proof-kernel review are unclaimed. Apache-2.0. + +[PROOF.md](PROOF.md) gives the full contract and argument. At four terms, +rank forces one factor side into the three-dimensional evaluation code. +All code supports reduce to 25 rational intersection directions. Their +complete restriction-rank envelope, combined with the thirteen pairwise +nonproportional Gram columns, forces the lower bound. No predecessor +census or scientific verifier is executed. + +## Reproduce + +Run from the repository root with the standard library only: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/ternary-moving-frame-floor/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/ternary-moving-frame-floor/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/ternary-moving-frame-floor +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/ternary-moving-frame-floor --check-source-history +``` + +Any CPython 3.12 interpreter can replace the absolute local path. The direct +verifier reads only these six package files, writes nothing and prints a +generated receipt binding their SHA256 hashes, followed by + +```text +PASS_TERNARY_MOVING_FRAME_FLOOR four_term_cost>=14 three_term_cost>=18 +``` + +The checker reconstructs the thirteen ports and independently enumerates the +25 intersection directions. It compares row and transposed-column binary +elimination on all 25*8192 restrictions. It then enumerates all 13^4 ordered +support-size tuples. Exact new factorization fixtures include three examples +whose non-code side has rank four, together with their transposes. The +coordinate fixture attains the three-term bill 18. Seven rejection controls +cover a zero direction, rank capacity, omitted direction, changed pairing, +underpriced envelope, failed scalar identity and excess term count. A +separate fixture distinguishes characteristic-zero scalar rank from binary +tariff rank. No enumeration of all coefficient tuples is claimed or needed. + +Both normal and optimized registered commands use explicit exceptions, so +optimization does not disable the checks. The generic runner checks metadata +and source pins separately. The source-history preflight requires the +retained Git history; direct mathematical replay needs no Git or network. + +## Scope and implementation bounds + +The exact pairing has unit diagonal and off-diagonal one precisely when the +original port vectors are orthogonal. Changed pairings, masked exactness, +shared-copy prices, other geometries, positive characteristic and five or +more active factors are not covered. The support relaxation's attaining +size tuple is not asserted to be a realizable factorization. + +The written reduction is a proof over all stated fields and decompositions. +The finite replay certifies its restriction-rank premise and corroborates +the algebraic fixtures. It is not a complete multiplication theorem or +independent human/proof-kernel acceptance. Physical acquisition, delivery, +native realization, arbitrary dirty-helper restoration, ownership, routing, +compiler closure, precision, stock, BIT compatibility and the outer bill +remain unpriced. No selected cold replay, Lean or Docker run was performed. + +The standalone verifier has no recursion, subprocesses, network access, +writes or mutable global cache. Each function is below sixty physical lines. +Its main exact loop is bounded by 25 directions and 8192 subsets. The size +loop has 28561 tuples. Matrices have at most 13 rows and 13 columns; factor +fixtures have at most four terms. The registered command timeout is 120 +seconds. Power of Ten rule 3 has a managed-runtime deviation: CPython +allocates integer, Fraction and collection objects while running. Live +mathematical state is bounded by these fixed dimensions, with one current +restriction retained at a time. Fixed-capacity storage would be required +for a native steady-operation implementation. The rejection helper has seven fixed local callable targets, a bounded +Power of Ten rule 9 deviation used only for failure controls. +Warnings-as-errors execution is the applicable diagnostic check; no external static analyzer is claimed. + +## Sources, overlap and family decision + +Base main is `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8, +selected PR6030. [SOURCES.json](SOURCES.json) pins the question README, +catalogue and selected record as historical provenance. There are no live +external mathematical inputs. [TASK.json](TASK.json) retains the complete +card and explains the changed scope. The selected binding baseline passed +as orientation, without a supplier replay. + +The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19362906) +followed checks of live handoffs, local reservations, open and recent-account +PRs, all-main README object/formula searches, merged/general-form searches +and the cached card report. The cached scan covered 406 open PRs and 6355 +Discussion records but only 111 local note records of 8917 HEAD notes. +Explicit Git searches covered all main README paths for the distinctive +object and formula terms. Sparse notes, arbitrary historical diffs and +unpublished work remain coverage limits. This is bounded overlap evidence, +not a novelty certificate or a literature-priority claim. + +Credit Aaron Wang / navinor's PR2518 and PR2272 for the exact open question +and fixed dense-polar contract; DreamingOfClouds's PR2125, PR2228, PR2111, +PR446, PR595 and PR1590 for the retained COPY/polar-law model; Cinna Davis / +1337isnot1337's PR2240 for the fixed-frame one-extra family; and joaqcoo's +PR1224 for the one-sided factorization context. Rank factorization, +projective intersections and binary elimination are classical. The new step +is the complete restriction-rank lemma and its all-moving-frame four-term +consequence on these thirteen ports. Predecessor results and credit lines +remain unchanged. + +The family decision is to stop this below-thirteen four-term route at its +algebraic cost gate. An exact cheaper decoder under a changed term count, +pairing or delivery contract would reopen a different question. A new +physical construction campaign is not justified by this negative result. + +## Open next questions + +1. What is the exact minimum with at most four terms, between 14 and 18? First seek a + complete exact factorization costing 14 through 17, allowing the other + factor side to leave the code. The support-size relaxation alone need + not be realizable. +2. Can five terms beat thirteen with this pairing? First specify the two + rank-four factor spaces and enforce a rank-three product. Neither side + must then equal the evaluation code, so the present reduction is not a + five-term exclusion. diff --git a/research/ternary-moving-frame-floor/SOURCES.json b/research/ternary-moving-frame-floor/SOURCES.json new file mode 100644 index 0000000000..15acf77450 --- /dev/null +++ b/research/ternary-moving-frame-floor/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/polar-law-t7-overcomplete-screen/README.md", + "usage": "provenance", + "git_blob": "3d7a42855310f5251452bdb003300275b538efc3", + "sha256": "ed9c61d8616fa4bc86a9d28d66f49aa774ef25fe56a4e3c895b69bf784e7880f" + } + ] +} diff --git a/research/ternary-moving-frame-floor/TASK.json b/research/ternary-moving-frame-floor/TASK.json new file mode 100644 index 0000000000..464d0f58ef --- /dev/null +++ b/research/ternary-moving-frame-floor/TASK.json @@ -0,0 +1,83 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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": "Prove that every at-most-four-term exact factorization of the thirteen-line ternary Gram matrix over a characteristic-zero field has full-orthogonality binary COPY cost at least 14; construct an exact finite support-rank certificate. Three terms have sharp cost 18.", + "scope_change_reason": "Take Aaron Wang / navinor PR2518 Open next question 2. This changes the current supplier-level card to a self-contained decoder cost obstruction with arbitrary moving frames. It does not meet the physical supplier acceptance gate or claim a complete signed invoice.", + "bottleneck_link": "This settles a proposed low-cost decoder escape at its algebraic COPY gate before any physical expansion. The fixed ternary geometry is a side result, not an improvement of the current selected P104 supplier.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified original support bound. Do not optimize the four-term floor or expand to another geometry or term count.", + "outcome": "negative-result", + "evidence": "PROOF.md; verify.py reconstructs 13 ports and 25 directions, compares two binary-rank eliminations on 204800 restrictions, enumerates all 28561 ordered support-size tuples, checks new exact factorization controls and seven rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the exact minimum with at most four terms between 14 and the three-term upper bound 18?", + "why_it_matters": "The present theorem closes every below-thirteen escape but does not classify the remaining tariff gap.", + "first_step": "Seek one exact four-term factorization with cost 14 through 17, allowing the non-code factor side to leave the evaluation code.", + "blocked_by": "The support-size relaxation need not be simultaneously realizable by an exact factorization." + }, + { + "question": "Can five terms beat thirteen under this same pairing?", + "why_it_matters": "Both factor matrices can have rank four at five terms, escaping the forced-code-side proof.", + "first_step": "Specify both four-dimensional factor spaces and enforce their product rank three before support pricing.", + "blocked_by": "Neither factor side must equal the ternary evaluation code; the present 25-direction reduction does not apply." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19362906", + "predecessor_credit": "Aaron Wang / navinor PR2518 and PR2272; DreamingOfClouds PR2125, PR2228, PR2111, PR446, PR595 and PR1590; Cinna Davis / 1337isnot1337 PR2240; joaqcoo PR1224. Their results are cited rather than audited." +} diff --git a/research/ternary-moving-frame-floor/VERIFY.json b/research/ternary-moving-frame-floor/VERIFY.json new file mode 100644 index 0000000000..33fe68b932 --- /dev/null +++ b/research/ternary-moving-frame-floor/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": "Complete restriction-rank certificate, support lower bound, exact factorization controls and semantic rejections." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same complete checks under optimized execution; all checks use explicit exceptions." + } + ] +} diff --git a/research/ternary-moving-frame-floor/verify.py b/research/ternary-moving-frame-floor/verify.py new file mode 100644 index 0000000000..31a7e8b9f8 --- /dev/null +++ b/research/ternary-moving-frame-floor/verify.py @@ -0,0 +1,243 @@ +#!/usr/bin/env python3 +"""Exact finite premises for the moving-frame four-term COPY bound. + +Produced by Nick Petalas. Apache-2.0. See README.md for predecessor credit. +""" +import hashlib +import json +from fractions import Fraction +from itertools import combinations, product +from math import gcd +from pathlib import Path +import platform +import sys + + +EXPECTED = (0, 1, 2, 3, 3, 4, 4, 5, 5, 6, 6, 6, 7, 7) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def dot(a, b): + return sum(x * y for x, y in zip(a, b, strict=True)) + + +def primitive(vector): + divisor = gcd(*vector) + require(divisor != 0, "zero projective direction") + sign = next(x for x in vector if x) + if sign < 0: + divisor = -divisor + return tuple(x // divisor for x in vector) + + +def geometry(): + ports = tuple(v for v in product((-1, 0, 1), repeat=3) + if next((x for x in v if x), 0) == 1) + require(len(ports) == 13 and len(set(ports)) == 13, "port inventory") + directions = set() + for a, b in combinations(ports, 2): + cross = (a[1]*b[2] - a[2]*b[1], a[2]*b[0] - a[0]*b[2], + a[0]*b[1] - a[1]*b[0]) + directions.add(primitive(cross)) + rebuilt = set() + for v in product(range(-2, 3), repeat=3): + if not any(v) or primitive(v) != v: + continue + zeros = [p for p in ports if dot(p, v) == 0] + if len(zeros) >= 2: + rebuilt.add(v) + require(directions == rebuilt and len(directions) == 25, + "independent direction inventory") + pairing = tuple(sum(1 << j for j, q in enumerate(ports) + if i == j or dot(p, q) == 0) + for i, p in enumerate(ports)) + supports = tuple(sum(1 << i for i, p in enumerate(ports) if dot(p, d)) + for d in sorted(directions)) + require(len(set(supports)) == 25, "distinct direction supports") + return ports, tuple(sorted(directions)), pairing, supports + + +def binary_rank(rows): + require(len(rows) <= 13 and all(0 <= r < 8192 for r in rows), + "binary matrix capacity") + basis = [0] * 13 + for value in rows: + for pivot in range(12, -1, -1): + if value & (1 << pivot): + if basis[pivot]: + value ^= basis[pivot] + else: + basis[pivot] = value + break + return sum(bool(row) for row in basis) + + +def column_rank(rows): + """A separate low-pivot elimination of explicit transposed columns.""" + columns = [sum(((row >> j) & 1) << i for i, row in enumerate(rows)) + for j in range(13)] + pivots = {} + for column in columns: + for index in range(len(rows)): + if column & (1 << index): + if index in pivots: + column ^= pivots[index] + else: + pivots[index] = column + break + return len(pivots) + + +def envelope(pairing, supports): + require(len(pairing) == 13 and len(supports) == 25, "envelope capacity") + result = [13] * 14 + witnesses = [None] * 14 + checks = 0 + for support in supports: + selected = [row for i, row in enumerate(pairing) if support >> i & 1] + for mask in range(8192): + rows = [row & mask for row in selected] + value = binary_rank(rows) + require(value == column_rank(rows), "row/column rank disagreement") + size = mask.bit_count() + if value < result[size]: + result[size] = value + witnesses[size] = [support, mask] + checks += 1 + require(tuple(result) == EXPECTED, "restriction-rank envelope") + require(checks == 204800, "complete restriction inventory") + return result, witnesses, checks + + +def support_relaxation(values): + best = 53 + witness = None + feasible = 0 + for sizes in product(range(1, 14), repeat=4): + if sum(sizes) < 22: + continue + feasible += 1 + value = sum(values[n] for n in sizes) + if value < best: + best, witness = value, sizes + require(best == 14 and witness == (1, 1, 7, 13), + "four-term support relaxation") + require(min(values[9:]) == 6, "three-term code support bound") + return {"minimum": best, "witness_sizes": witness, + "tuples_checked": 13**4, "feasible_tuples": feasible, + "three_term_floor": 18} + + +def rational_rank(matrix): + require(len(matrix) <= 13 and all(len(r) <= 13 for r in matrix), + "rational matrix capacity") + rows = [[Fraction(x) for x in row] for row in matrix] + rank = 0 + for column in range(len(rows[0])): + pivot = next((i for i in range(rank, len(rows)) if rows[i][column]), None) + if pivot is None: + continue + rows[rank], rows[pivot] = rows[pivot], rows[rank] + scale = rows[rank][column] + rows[rank] = [x / scale for x in rows[rank]] + for i in range(len(rows)): + if i != rank and rows[i][column]: + factor = rows[i][column] + rows[i] = [x-factor*y for x, y in zip(rows[i], rows[rank], strict=True)] + rank += 1 + return rank + + +def factor_cost(left, right, gram, pairing): + require(len(left) == len(right) == 13, "factor row count") + width = len(left[0]) + require(1 <= width <= 4 and all(len(r) == width for r in left+right), + "one through four factors required") + for i, j in product(range(13), repeat=2): + require(dot(left[i], right[j]) == gram[i][j], "factorization identity") + cost = 0 + for term in range(width): + active = sum(1 << i for i in range(13) if right[i][term]) + rows = [pairing[i] & active for i in range(13) if left[i][term]] + cost += binary_rank(rows) + require(cost >= 14, "four-term theorem violated") + return cost + + +def positive_fixtures(ports, pairing): + gram = [[dot(p, q) for q in ports] for p in ports] + require(rational_rank(gram) == 3, "Gram rank") + require(all(dot([p[i] for p in ports], [p[j] for p in ports]) + == (9 if i == j else 0) for i, j in product(range(3), repeat=2)), + "evaluation code Gram") + coordinate = [list(p) for p in ports] + costs = [factor_cost(coordinate, coordinate, gram, pairing)] + for chosen in (0, 4, 12): + left = [list(p) + [p[0]] for p in ports] + right = [[p[0] - int(i == chosen), p[1], p[2], int(i == chosen)] + for i, p in enumerate(ports)] + require(rational_rank(left) == 3 and rational_rank(right) == 4, + "one-sided outside-code fixture") + costs.append(factor_cost(left, right, gram, pairing)) + costs.append(factor_cost(right, left, gram, pairing)) + require(costs[0] == 18, "coordinate control") + return gram, coordinate, costs + + +def expect_rejection(operation, message): + try: + operation() + except ValueError: + return + raise ValueError("ineffective rejection control: " + message) + + +def rejection_controls(ports, directions, pairing, supports, gram, coordinate): + expect_rejection(lambda: primitive((0, 0, 0)), "zero direction") + expect_rejection(lambda: binary_rank([8192]), "rank capacity") + expect_rejection(lambda: envelope(pairing, supports[:-1]), "missing direction") + identity = tuple(1 << i for i in range(13)) + expect_rejection(lambda: envelope(identity, supports), "changed pairing") + lowered = list(EXPECTED) + lowered[13] = 6 + expect_rejection(lambda: support_relaxation(lowered), "underpriced envelope") + bad = [r.copy() for r in coordinate] + bad[0][0] += 1 + expect_rejection(lambda: factor_cost(bad, coordinate, gram, pairing), "bad identity") + five = [list(p) + [0, 0] for p in ports] + expect_rejection(lambda: factor_cost(five, five, gram, pairing), "five factors") + require(binary_rank([3, 5, 6]) == 2 and + rational_rank([[1, 1, 0], [1, 0, 1], [0, 1, 1]]) == 3, + "binary tariff versus rational scalar rank") + require(all(sum(dot(p, d) == 0 for p in ports) >= 2 for d in directions), + "direction intersection condition") + return 7 + + +def main(): + require(len(sys.argv) == 1, "this verifier accepts no arguments") + ports, directions, pairing, supports = geometry() + values, witnesses, checked = envelope(pairing, supports) + relaxation = support_relaxation(values) + gram, coordinate, costs = positive_fixtures(ports, pairing) + controls = rejection_controls(ports, directions, pairing, supports, gram, coordinate) + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + root = Path(__file__).resolve().parent + receipt = {"status": "PASS_TERNARY_MOVING_FRAME_FLOOR", "claim_type": "scoped proof", + "ports": ports, "directions": directions, "support_sizes": sorted(set( + mask.bit_count() for mask in supports)), "rank_envelope": values, + "envelope_witnesses": witnesses, "restrictions_checked": checked, + "relaxation": relaxation, "fixture_costs": costs, + "rejected_controls": controls, "python": platform.python_version(), + "source_sha256": {name: hashlib.sha256((root/name).read_bytes()).hexdigest() + for name in names}} + print(json.dumps(receipt, indent=2, sort_keys=True)) + print("PASS_TERNARY_MOVING_FRAME_FLOOR four_term_cost>=14 three_term_cost>=18") + + +if __name__ == "__main__": + main()