diff --git a/research/projector-anchored-paired-lattices/PROOF.md b/research/projector-anchored-paired-lattices/PROOF.md new file mode 100644 index 0000000000..f57d551e81 --- /dev/null +++ b/research/projector-anchored-paired-lattices/PROOF.md @@ -0,0 +1,142 @@ +# Complete paired-lattice feasibility with projector anchors + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped algebraic proof, with finite executable corroboration. +No multiplication theorem or new kappa is claimed. + +## Interface and theorem + +Put R=Z_(2)={a/b in Q : b is odd}, and v2(2)=1. A full R-lattice Lambda +in Q^m is the R-span of a rational basis. A paired lattice is Lambda direct-sum +Lambda, with H before D. Supply a finite list of rational 2m by 2m applied +matrices G_k. Include every inverse actually applied. Stability means inclusion, +not equality; an unapplied inverse need not preserve the lattice. + +The additional hypothesis is an explicit complete family of anchors: + +```text +rank(P_i)=1, P_i^2=P_i, +P_i P_j=0 for i != j, sum_(i=1..m) P_i=I. +``` + +Every P_i must occur as one of the four m by m blocks of an actually applied +G_k. For example, an actual paid label n_(P_i) supplies such an upper-right +block. An unapplied projector is not an anchor. + +Choose a nonzero rational c_i in image(P_i) and form C=[c_1 ... c_m]. +The identities imply C is invertible and C^-1 P_i C=E_ii. For every nonzero +entry t at row r, column s of diag(C,C)^-1 G_k diag(C,C), retain the edge + +```text +s mod m -> r mod m, weight v2(t). +``` + +Parallel edges and self loops are allowed. The following are equivalent: + +1. Some full common paired R-lattice is stable under every G_k. +2. Integers a_i satisfy a_(r mod m)-a_(s mod m)<=v2(t) on every edge. +3. The graph has no negative directed cycle. + +A feasible potential supplies Lambda=C diag(2^a_i) R^m. A negative cycle +excludes every full common paired rational lattice under the anchor hypothesis, +including non-diagonal lattices. This strengthens rejection of diagonal gauges +in the original coordinates. + +## Proof of completeness + +Stability of Lambda^2 under a block matrix implies stability of Lambda under +each block: apply it to (x,0) and (0,x). Hence every P_i preserves Lambda, and + +```text +Lambda = direct-sum_i P_i Lambda. +``` + +Each summand is finitely generated over R on the line Q c_i. Write its +generators as q_j c_i. The minimum valuation a_i of the nonzero q_j exists. +A generator attaining it is 2^a_i u c_i with u and u^-1 in R. Thus the +module contains 2^a_i c_i, and every generator belongs to 2^a_i R c_i. +Consequently P_i Lambda=2^a_i R c_i. Every possible invariant lattice +therefore has the displayed form. This is the new completeness step. + +In that basis the entry t becomes t*2^(a_s-a_r), with indices reduced +modulo m. It is in R exactly when its edge inequality holds, proving 1 iff 2. +Summing inequalities around a negative cycle is impossible. Conversely, add +a source with zero-weight edges to every vertex. Without negative cycles, +minimum paths can be chosen simple by removing repeated-vertex cycles. +Their integer distances satisfy every edge inequality, proving 2 iff 3. +Subtracting a_1 from all a_i preserves the inequalities. + +The graph argument is the classical difference-constraint argument already +used by ywz65's [PR #2671](https://github.com/CrocSwap/integer-mult-bounds/pull/2671). +The contribution here is completeness over all common paired lattices in the +anchored class. Decomposition by orthogonal idempotents and the rank-one +ideal calculation are classical ingredients, not new general invariants. +Bellman-Ford takes O(m E) relaxations for E nonzero entries, in addition to +exact rational basis construction and conjugation. This is an arithmetic +operation bound, not a bit-time or fixed-tape tariff. + +## An unbounded separation from original-coordinate diagonal gauges + +For m=2^k, k>=1, let H be the Sylvester Walsh matrix: + +```text +H[x,y]=(-1)^(binary_dot(x,y)), H^-1=H/m, +P_i=H E_ii H^-1, G_i=n_(P_i)=[[I,P_i],[0,I]]. +``` + +For distinct column labels, pairing summands differing in a bit where the +labels differ proves H^T H=mI. Thus the P_i are complete orthogonal rank-one +projectors. Every diagonal entry of every P_i is 1/m. A diagonal similarity +leaves these entries unchanged. No original-coordinate paired-diagonal basis +can therefore make all G_i 2-integral: every projector gives negative self +loops of weight -k. + +The non-diagonal paired basis diag(H,H) sends G_i to n_(E_ii), an integral +matrix. The anchored test accepts. This holds in unbounded dimension, beyond +the checked m=2,4,8 examples. + +There is no paid-rank saving in this family. The exact rational group-label +identity is + +```text +n_(P_m) ... n_(P_1) = n_(sum_i P_i) = n_I. +``` + +Each paid upper block has rank one. Running this independently on W data +roles costs mW paid rank, with no auxiliary scalar role. This is a literal +rational group-label identity, not an inference from a finite representation +of a formal group algebra. A failed diagonal filter can miss an applicable +obstruction; it is not itself evidence of a saving. + +## Existing Borel bound and its boundaries + +Only after the source-model premises of +[PR #2613](https://github.com/CrocSwap/integer-mult-bounds/pull/2613) and +[PR #2671](https://github.com/CrocSwap/integer-mult-bounds/pull/2671) are supplied, +the certified basis may be used in their existing rank-functional argument. +Apply the same paired basis to every scalar role. It commutes with scalar +mixing, preserves block-lower free maps, and preserves paid rational ranks. +Unit labels n_I remain exactly n_I. The source's reduction then gives +total paid rank >=mW for W such unit targets, including its permitted finite +scalar workspace. The rank functional, auxiliary allowance and allowance +for singular reductions of free maps retain the source authors' credit. +This package proves the common-lattice premise on a larger decidable class; +it does not re-audit that rank bound or its predecessors. + +For a general target, integrality of its transformed HD block does not imply +invertibility modulo two. For example n_(2I) is integral with zero HD block +modulo two. Rational invertibility of an applied matrix likewise does not +imply integrality of its inverse. + +The theorem requires one paired lattice shared across scalar roles and a +complete actual rank-one anchor family. Different H/D lattices, role-specific +lattices, non-lattice representations and unanchored inputs are outside its +completeness claim. A failed anchor premise is an unsupported input, not an +impossibility certificate. The complete applied list, legal native/model +operations and a formal word's full endpoint are separate caller obligations. + +This analytic basis is not executed or declared free. Physical conversion, +stock, precision, tape movement, native lowering, recursive compiler closure +and analytic recovery remain implementation obligations. No selected supplier +is mapped into this class, and no complete supplier invoice is supplied. diff --git a/research/projector-anchored-paired-lattices/README.md b/research/projector-anchored-paired-lattices/README.md new file mode 100644 index 0000000000..f41634f35d --- /dev/null +++ b/research/projector-anchored-paired-lattices/README.md @@ -0,0 +1,110 @@ +# Complete paired-lattice tests with projector anchors + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped algebraic proof with exact finite corroboration. No new kappa. + +A complete family of rank-one projector blocks makes the common paired-lattice +problem decidable by one graph test. This extends the diagonal-only filter in +ywz65's [PR #2671](https://github.com/CrocSwap/integer-mult-bounds/pull/2671) to +every common paired rational lattice under an explicit anchor hypothesis. +The predecessor's test and rank bound are cited, not re-audited. + +Put R=Z_(2), the rationals with odd denominators. Supply m orthogonal rank-one +projectors summing to I, each present as an actual block of an applied 2m by 2m +matrix. Every invariant lattice splits along their eigenlines. In an eigenbasis +C it is C diag(2^a_i) R^m, so existence is equivalent to the absence of a negative +cycle in the valuation graph. A checked negative cycle excludes every common +paired lattice in this anchored class. [PROOF.md](PROOF.md) proves this for every +finite rational input and gives the source-model boundaries. + +The Walsh-projector family separates the two filters for every m=2^k>=2. +All projector diagonals are 1/m, so every original-coordinate diagonal gauge +fails. The non-diagonal Walsh basis makes all projectors integral. The m +rank-one paid labels multiply exactly to n_I. The existing mW rank floor +applies when its complete Borel-model premises are supplied. This is a family +missed by the diagonal filter, not a paid-rank improvement. + +## Reproduction and evidence + +From the repository root, with CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/projector-anchored-paired-lattices/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/projector-anchored-paired-lattices/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/projector-anchored-paired-lattices +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/projector-anchored-paired-lattices --check-source-history +``` + +Another CPython 3.12 path can replace the absolute path. The direct marker is +`PASS_PROJECTOR_ANCHORED_PAIRED_LATTICES`; registered replay also prints +`PASS_REGISTERED_RESEARCH_PACKAGE`. Each direct run generates a JSON stdout +receipt bound to every package file's SHA256, without writing files or importing +predecessor executables. All contracts remain enabled under optimized Python. + +The replay enumerates all 256 directed two-vertex graphs with each edge weight +in {absent,-1,0,1}. Independent min-plus closure and all three normalized +potentials (0,-1),(0,0),(0,1) agree. Four rational charts and all four matrix +block placements, with diagonal placements restricted to invertible graph +matrices, give 3,552 certificate problems: 1,528 feasible and 2,024 infeasible. +The separate checker reads original matrix entries and imports no graph solver. +The replay also checks Walsh dimensions 2,4,8, thirteen rejected input/certificate +controls and three scope controls. The generated receipt records these counts. +The quantified proof, rather than this finite corpus, establishes completeness. + +The controls cover omitted precision shifts, wrong eigenbases, malformed cycles, +unapplied anchors in both producer and checker, non-projector anchor families, +inexact or oversized inputs, singular free reductions, an actually applied +inverse and the difference between integral and unit targets. + +The public interfaces are `lattice.solve(anchors, applied)` and +`check.check(anchors, applied, certificate)`. The checker returns True for a +checked invariant lattice and False for a checked impossibility cycle. +Invalid inputs or certificates raise ValueError. The implementation accepts +1<=m<=8, at most 64 applied matrices, and integer/Fraction entries with numerator +and denominator lengths at most 64 bits. Rejected bounds are unsupported inputs, +not negative mathematical results. Certificates contain exact Fraction bases +and Python integers; a JSON interchange API is not supplied. + +## Scope, sources and credit + +The `bit-new-register-model` card is changed to an analytic obstruction filter +for rational Borel words. This is a side result on a register-model blocker, +without a new native alphabet or selected supplier. The base is canonical main +`19fdb086ea96af9a9f87936a2b888e10af4ed810`, priority revision 8. +[SOURCES.json](SOURCES.json) pins the predecessor proof and README, catalogue and +selected record. The source's explicit non-diagonal-lattice direction motivates +the question; its original diagonal-only statement retains its scope. + +Credit ywz65 for #2671's paired-diagonal graph filter, Sagar Thakrar for +#2613's 2-integral Borel corollary, eumemic for #288's general lattice method, +and Swapnil Jain for the retained rank functional. Orthogonal-idempotent +decomposition, the rank-one ideal calculation, Walsh orthogonality and graph +feasibility are classical. The contribution is the complete anchored interface, +separating family and certificate implementation. No literature-priority claim +is made for those ingredients. Existing files and credit remain unchanged. + +The theorem requires one paired lattice shared across scalar roles and a +complete actual anchor family. The caller must supply the full applied list, +legal operations and formal endpoint. General unanchored inputs, distinct H/D +lattices and non-lattice representations are not decided. No physical basis +conversion, precision/stock/tape bill, native realization, selected scientific +replay, compiler or outer admission is supplied. The five selected framework +assumptions remain. Independent human and formal proof-kernel review are unclaimed. + +All loops are bounded by the fixed corpus, matrix dimensions, applied-list limit +or at most m graph passes/cycle edges. Functions stay below 60 physical lines. +Python's dynamic exact arithmetic is a managed-allocation deviation from fixed +memory discipline; finite dimensions, input bit bounds and corpus bound live +resources. There is no recursion, dynamic code generation, network access or +scientific subprocess. Warning-strict execution and package replay are the +applicable diagnostics. + +## Open next questions + +1. Does an actual candidate Borel word expose a complete family of projector + blocks at legal contacts? Extract its whole applied list and actual anchors + before testing it. Native membership and endpoint validity remain prerequisites. +2. Can completeness extend to higher-rank orthogonal projectors? Start with two + rank-two blocks. Their invariant summands need internal lattices, so scalar + potentials alone no longer prove completeness. diff --git a/research/projector-anchored-paired-lattices/SOURCES.json b/research/projector-anchored-paired-lattices/SOURCES.json new file mode 100644 index 0000000000..d41b0d6b1a --- /dev/null +++ b/research/projector-anchored-paired-lattices/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/paired-diagonal-borel-gauge/PROOF.md", + "usage": "input", + "git_blob": "90fa58a4496cc854e05ae5ad4805e9c247fc960d", + "sha256": "6494c51a3c9d66033b5c5904ab5eef19ad93f2c41a3ced022003c20c2b5837f9" + }, + { + "path": "research/paired-diagonal-borel-gauge/README.md", + "usage": "input", + "git_blob": "55788f0f6b209d800f19cf53a29403500071e1d5", + "sha256": "beb65171fd265dfaadef59aa778c5192d9880217a2c10d88c48184a8b25972f1" + } + ] +} diff --git a/research/projector-anchored-paired-lattices/TASK.json b/research/projector-anchored-paired-lattices/TASK.json new file mode 100644 index 0000000000..0dc289f330 --- /dev/null +++ b/research/projector-anchored-paired-lattices/TASK.json @@ -0,0 +1,75 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Decide existence of every common paired 2-integral lattice for rational applied matrices anchored by a complete rank-one projector family; give a Walsh separation from original-coordinate diagonal gauges.", + "scope_change_reason": "PR2671 explicitly leaves non-diagonal lattices open. Rank-one projector anchors force every invariant lattice into a known eigenbasis with scalar valuations, giving a complete scoped test rather than another native-word census.", + "bottleneck_link": "Analytic register-model obstruction filter. It closes the common-lattice premise on an anchored class, without claiming a physical supplier or changed selected frontier.", + "budget_minutes": 60, + "stop_rule": "Ship the first proved completeness result and separating family; do not extend to higher-rank anchors or a candidate census.", + "outcome": "completed", + "evidence": "PROOF.md and generated verify.py receipt; independent graph oracle, original-matrix certificate checker and hypothesis controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does an actual candidate Borel word expose a complete family of projector blocks at legal contacts?", + "why_it_matters": "This could certify the common-lattice premise of the existing rank obstruction for a concrete candidate.", + "first_step": "Extract its full applied-matrix list and actual rank-one projector blocks.", + "blocked_by": "Legal source-model membership and full endpoint must be supplied independently." + }, + { + "question": "Can completeness extend to higher-rank orthogonal projector anchors?", + "why_it_matters": "This would cover words without one-dimensional anchor summands.", + "first_step": "Analyze two rank-two invariant summands before a larger search.", + "blocked_by": "Internal lattices of higher-rank summands are not determined by scalar valuations." + } + ], + "source_question": { + "source": "PR #2671", + "author": "ywz65", + "question": "A distinct full-Borel construction or an explicit non-diagonal lattice could change the diagonal-only decision." + } +} diff --git a/research/projector-anchored-paired-lattices/VERIFY.json b/research/projector-anchored-paired-lattices/VERIFY.json new file mode 100644 index 0000000000..27a79a4ddc --- /dev/null +++ b/research/projector-anchored-paired-lattices/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/paired-diagonal-borel-gauge/PROOF.md", + "research/paired-diagonal-borel-gauge/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All two-vertex valuation graphs, four rational charts, four block placements where invertible, original-matrix certificate checks, Walsh separation and rejecting controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same exact corroboration and rejecting controls under optimized Python." + } + ] +} diff --git a/research/projector-anchored-paired-lattices/check.py b/research/projector-anchored-paired-lattices/check.py new file mode 100644 index 0000000000..d76802a955 --- /dev/null +++ b/research/projector-anchored-paired-lattices/check.py @@ -0,0 +1,81 @@ +"""Check certificates directly against original matrices, without the solver. + +Produced by Nick Petalas. Apache-2.0. +""" + +from linear import (block_at, inverse, matrix, multiply, paired, power_two, + require, valuation) + + +def check_eigenbasis(anchors, basis): + size = len(anchors) + basis = matrix(basis, size) + inverse(basis) + for i, projector in enumerate(anchors): + expected = tuple(tuple(basis[r][c] if c == i else 0 for c in range(size)) + for r in range(size)) + require(multiply(projector, basis) == expected, "basis does not diagonalize anchors") + return basis + + +def check_potential(basis, applied, exponents): + size = len(basis) + require(isinstance(exponents, (list, tuple)) and len(exponents) == size, + "potential size") + require(all(type(x) is int and abs(x) <= 100000 for x in exponents), + "invalid potential") + scaled = tuple(tuple(basis[i][j] * power_two(exponents[j]) for j in range(size)) + for i in range(size)) + change = paired(scaled) + undo = inverse(change) + for value in applied: + changed = multiply(multiply(undo, value), change) + require(all(not x or valuation(x) >= 0 for row in changed for x in row), + "nonintegral applied matrix") + return True + + +def check_cycle(basis, applied, entries): + size = len(basis) + require(isinstance(entries, (list, tuple)) and 1 <= len(entries) <= size, + "cycle length") + change = paired(basis) + undo = inverse(change) + first, previous, total = None, None, 0 + for entry in entries: + require(isinstance(entry, (list, tuple)) and len(entry) == 3 + and all(type(x) is int for x in entry), "cycle entry shape") + index, row, column = entry + require(0 <= index < len(applied) and 0 <= row < 2 * size + and 0 <= column < 2 * size, "cycle index") + changed = multiply(multiply(undo, applied[index]), change) + value = changed[row][column] + require(value != 0, "cycle uses zero entry") + source, target = column % size, row % size + if first is None: + first = source + else: + require(source == previous, "cycle disconnected") + previous, total = target, total + valuation(value) + require(previous == first and total < 0, "cycle not closed and negative") + return False + + +def check(anchors, applied, certificate): + require(isinstance(anchors, (list, tuple)) and 1 <= len(anchors) <= 8, + "anchor count") + size = len(anchors) + require(isinstance(applied, (list, tuple)) and 1 <= len(applied) <= 64, + "applied count") + anchors = tuple(matrix(p, size) for p in anchors) + applied = tuple(matrix(g, 2 * size) for g in applied) + require(isinstance(certificate, dict), "certificate must be a mapping") + basis = check_eigenbasis(anchors, certificate.get("basis")) + blocks = tuple(block_at(g, r, c, size) for g in applied for r in range(2) + for c in range(2)) + require(all(p in blocks for p in anchors), "unapplied anchor") + kind = certificate.get("kind") + if kind == "potential": + return check_potential(basis, applied, certificate.get("exponents")) + require(kind == "cycle", "unknown certificate kind") + return check_cycle(basis, applied, certificate.get("entries")) diff --git a/research/projector-anchored-paired-lattices/lattice.py b/research/projector-anchored-paired-lattices/lattice.py new file mode 100644 index 0000000000..efbb174181 --- /dev/null +++ b/research/projector-anchored-paired-lattices/lattice.py @@ -0,0 +1,95 @@ +"""Construct a complete paired-lattice certificate in the anchored class. + +Produced by Nick Petalas. Apache-2.0. +""" + +from linear import (block_at, identity, inverse, matrix, multiply, paired, + require, valuation, zero) + +MAX_ADDRESS_DIM = 8 +MAX_APPLIED = 64 + + +def validate(anchors, applied): + require(isinstance(anchors, (list, tuple)), "anchor sequence required") + size = len(anchors) + require(1 <= size <= MAX_ADDRESS_DIM, "unsupported anchor count") + require(isinstance(applied, (list, tuple)) and 1 <= len(applied) <= MAX_APPLIED, + "unsupported applied-matrix count") + anchors = tuple(matrix(value, size) for value in anchors) + applied = tuple(matrix(value, 2 * size) for value in applied) + for i, projector in enumerate(anchors): + require(multiply(projector, projector) == projector, "anchor not idempotent") + require(sum(projector[j][j] for j in range(size)) == 1, "anchor not rank one") + for j, other in enumerate(anchors): + if i != j: + require(multiply(projector, other) == zero(size), "anchors not orthogonal") + total = tuple(tuple(sum(p[i][j] for p in anchors) for j in range(size)) + for i in range(size)) + require(total == identity(size), "anchors not complete") + blocks = tuple(block_at(g, r, c, size) for g in applied for r in range(2) + for c in range(2)) + require(all(p in blocks for p in anchors), "anchor absent from applied blocks") + return anchors, applied + + +def anchor_basis(anchors): + size = len(anchors) + columns = [] + for projector in anchors: + column = next(j for j in range(size) if any(projector[i][j] for i in range(size))) + columns.append(tuple(projector[i][column] for i in range(size))) + basis = tuple(tuple(columns[j][i] for j in range(size)) for i in range(size)) + inverse(basis) # Check the full eigenbasis before graph construction. + return basis + + +def edges_for(basis, applied): + size = len(basis) + change = paired(basis) + undo = inverse(change) + edges = [] + for index, value in enumerate(applied): + changed = multiply(multiply(undo, value), change) + for i in range(2 * size): + for j in range(2 * size): + if changed[i][j]: + edges.append((j % size, i % size, valuation(changed[i][j]), index, i, j)) + return tuple(edges) + + +def solve_edges(size, edges): + distances, predecessor = [0] * size, [None] * size + changed = None + for _ in range(size): + changed = None + for index, (source, target, weight, *_) in enumerate(edges): + if distances[target] > distances[source] + weight: + distances[target] = distances[source] + weight + predecessor[target] = index + changed = target + if changed is None: + return {"kind": "potential", "exponents": [x - distances[0] for x in distances]} + vertex = changed + for _ in range(size): + require(predecessor[vertex] is not None, "broken negative-cycle predecessor") + vertex = edges[predecessor[vertex]][0] + start, reverse_cycle = vertex, [] + for _ in range(size): + index = predecessor[vertex] + require(index is not None, "broken cycle") + reverse_cycle.append(index) + vertex = edges[index][0] + if vertex == start: + cycle = list(reversed(reverse_cycle)) + require(sum(edges[index][2] for index in cycle) < 0, "cycle not negative") + return {"kind": "cycle", "entries": [list(edges[index][3:]) for index in cycle]} + raise ValueError("negative-cycle extraction exceeded dimension") + + +def solve(anchors, applied): + anchors, applied = validate(anchors, applied) + basis = anchor_basis(anchors) + certificate = solve_edges(len(anchors), edges_for(basis, applied)) + certificate["basis"] = basis + return certificate diff --git a/research/projector-anchored-paired-lattices/linear.py b/research/projector-anchored-paired-lattices/linear.py new file mode 100644 index 0000000000..26387bcb2f --- /dev/null +++ b/research/projector-anchored-paired-lattices/linear.py @@ -0,0 +1,94 @@ +"""Small exact matrix operations for the paired-lattice certificate. + +Produced by Nick Petalas. Apache-2.0. +""" + +from fractions import Fraction + +MAX_DIM = 16 +MAX_INPUT_BITS = 64 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def matrix(rows, size): + require(type(size) is int and 1 <= size <= MAX_DIM, "unsupported dimension") + require(isinstance(rows, (list, tuple)) and len(rows) == size, "row count") + result = [] + for row in rows: + require(isinstance(row, (list, tuple)) and len(row) == size, "column count") + converted = [] + for value in row: + require(type(value) in (int, Fraction), "exact rational entries required") + value = Fraction(value) + require(max(abs(value.numerator).bit_length(), value.denominator.bit_length()) + <= MAX_INPUT_BITS, "input coefficient too large") + converted.append(value) + result.append(tuple(converted)) + return tuple(result) + + +def identity(size): + return tuple(tuple(Fraction(i == j) for j in range(size)) for i in range(size)) + + +def zero(size): + return tuple(tuple(Fraction(0) for _ in range(size)) for _ in range(size)) + + +def multiply(left, right): + size = len(left) + require(size == len(right), "matrix size mismatch") + return tuple(tuple(sum((left[i][k] * right[k][j] for k in range(size)), Fraction(0)) + for j in range(size)) for i in range(size)) + + +def inverse(value): + size = len(value) + rows = [[Fraction(entry) for entry in value[i]] + list(identity(size)[i]) + for i in range(size)] + for column in range(size): + pivot = next((i for i in range(column, size) if rows[i][column]), None) + require(pivot is not None, "singular basis") + rows[column], rows[pivot] = rows[pivot], rows[column] + divisor = rows[column][column] + rows[column] = [entry / divisor for entry in rows[column]] + for i in range(size): + if i != column: + factor = rows[i][column] + rows[i] = [x - factor * y for x, y in zip(rows[i], rows[column])] + result = tuple(tuple(row[size:]) for row in rows) + require(multiply(value, result) == identity(size), "inverse identity") + return result + + +def valuation(value): + require(value != 0, "zero has no finite valuation") + numerator, denominator = abs(value.numerator), value.denominator + return ((numerator & -numerator).bit_length() + - (denominator & -denominator).bit_length()) + + +def power_two(exponent): + return Fraction(2 ** exponent) if exponent >= 0 else Fraction(1, 2 ** -exponent) + + +def paired(basis): + size = len(basis) + return tuple(tuple(basis[i % size][j % size] if i // size == j // size else Fraction(0) + for j in range(2 * size)) for i in range(2 * size)) + + +def upper(block): + size = len(block) + return tuple(tuple(Fraction(i == j) + (block[i][j - size] + if i < size <= j else 0) + for j in range(2 * size)) for i in range(2 * size)) + + +def block_at(value, row, column, size): + return tuple(tuple(value[row * size + i][column * size + j] + for j in range(size)) for i in range(size)) diff --git a/research/projector-anchored-paired-lattices/verify.py b/research/projector-anchored-paired-lattices/verify.py new file mode 100644 index 0000000000..3ee58a0310 --- /dev/null +++ b/research/projector-anchored-paired-lattices/verify.py @@ -0,0 +1,205 @@ +"""Exact corroboration of projector-anchored paired-lattice completeness. + +Produced by Nick Petalas. Apache-2.0. No predecessor executable is imported. +""" + +from copy import deepcopy +from fractions import Fraction +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path +import sys + +PACKAGE = Path(__file__).resolve().parent +sys.path.insert(0, str(PACKAGE)) +from check import check # noqa: E402 +from lattice import solve, validate # noqa: E402 +from linear import (block_at, identity, inverse, multiply, paired, power_two, + require, upper, valuation, zero) # noqa: E402 + + +def projectors(size): + return tuple(tuple(tuple(Fraction(r == i == c) for c in range(size)) + for r in range(size)) for i in range(size)) + + +def conjugate(value, basis): + return multiply(multiply(basis, value), inverse(basis)) + + +def problem(basis, blocks): + size = len(basis) + anchors = tuple(conjugate(p, basis) for p in projectors(size)) + applied = tuple(upper(p) for p in anchors) + tuple( + upper(conjugate(a, basis)) for a in blocks) + return validate(anchors, applied) + + +def graph_oracle(weights): + # Independent min-plus closure on the originally specified graph. + size = len(weights) + distance = [[0 if i == j else None for j in range(size)] for i in range(size)] + for target in range(size): + for source in range(size): + weight = weights[target][source] + if weight is not None: + old = distance[source][target] + distance[source][target] = weight if old is None else min(old, weight) + for middle in range(size): + for source in range(size): + for target in range(size): + left, right = distance[source][middle], distance[middle][target] + if left is not None and right is not None: + old = distance[source][target] + distance[source][target] = left + right if old is None else min(old, left + right) + return all(distance[i][i] >= 0 for i in range(size)) + + +def placements(block): + size = len(block) + values = [upper(block)] + values.append(tuple(tuple(Fraction(i == j) + (block[i - size][j] + if j < size <= i else 0) + for j in range(2 * size)) for i in range(2 * size))) + if block[0][0] * block[1][1] != block[0][1] * block[1][0]: + for half in range(2): + values.append(tuple(tuple(block[i % size][j % size] + if i // size == j // size == half else Fraction(i == j) + for j in range(2 * size)) for i in range(2 * size))) + return values + + +def graph_corpus(): + charts = (identity(2), ((1, 1), (1, -1)), + ((1, Fraction(1, 2)), (0, 1)), + ((Fraction(1, 3), 1), (1, Fraction(2, 5)))) + counts = {"graphs": 0, "chart_problems": 0, "feasible": 0, "infeasible": 0} + for entries in product((None, -1, 0, 1), repeat=4): + weights = (entries[:2], entries[2:]) + expected = graph_oracle(weights) + bounded = any(all(weights[i][j] is None or a[i] - a[j] <= weights[i][j] + for i in range(2) for j in range(2)) + for a in ((0, -1), (0, 0), (0, 1))) + require(expected == bounded, "closure disagrees with complete normalized potentials") + block = tuple(tuple(Fraction(0) if x is None else power_two(x) for x in row) + for row in weights) + counts["graphs"] += 1 + for chart in charts: + anchors, base = problem(chart, ()) + for placement in placements(block): + applied = base + (conjugate(placement, paired(chart)),) + certificate = solve(anchors, applied) + observed = check(anchors, applied, certificate) + require(observed == expected, "anchored test disagrees with graph oracle") + counts["chart_problems"] += 1 + counts["feasible" if observed else "infeasible"] += 1 + return counts + + +def walsh(size): + return tuple(tuple(Fraction(-1 if (i & j).bit_count() % 2 else 1) + for j in range(size)) for i in range(size)) + + +def walsh_separation(): + rows = [] + for size in (2, 4, 8): + basis = walsh(size) + anchors, applied = problem(basis, ()) + require(all(p[i][i] == Fraction(1, size) for p in anchors for i in range(size)), + "Walsh diagonal formula") + require(all(valuation(p[i][i]) < 0 for p in anchors for i in range(size)), + "standard diagonal-gauge self-loop obstruction") + certificate = solve(anchors, applied) + require(check(anchors, applied, certificate), "non-diagonal lattice rejected") + endpoint = identity(2 * size) + for gate in applied: + endpoint = multiply(gate, endpoint) + require(endpoint == upper(identity(size)), "complete paid label is not n_I") + change = paired(basis) + require(multiply(multiply(inverse(change), endpoint), change) == endpoint, + "paired basis changed unit target") + rows.append({"dimension": size, "paid_rank": size, + "diagonal_obstruction_valuation": -((size - 1).bit_length()), + "certificate_exponents": certificate["exponents"]}) + return rows + + +def rejection(call, message): + try: + call() + except (ValueError, TypeError): + return 1 + raise ValueError("accepted invalid control: " + message) + + +def controls(): + anchors, applied = problem(identity(2), (((0, Fraction(1, 2)), (0, 0)),)) + positive = solve(anchors, applied) + require(check(anchors, applied, positive), "positive control") + cases = [] + bad = deepcopy(positive) + bad["exponents"] = [0, 0] + cases.append((lambda: check(anchors, applied, bad), "omitted precision shift")) + bad_basis = deepcopy(positive) + bad_basis["basis"] = ((1, 1), (1, 2)) + cases.append((lambda: check(anchors, applied, bad_basis), "wrong eigenbasis")) + bad_type = deepcopy(positive) + bad_type["exponents"] = [False, 1] + cases.append((lambda: check(anchors, applied, bad_type), "Boolean exponent")) + cyclic = applied + (upper(((0, 0), (Fraction(1, 2), 0))),) + negative = solve(anchors, cyclic) + require(not check(anchors, cyclic, negative), "negative-cycle control") + bad_cycle = deepcopy(negative) + bad_cycle["entries"] = [[0, 0, 0]] + cases.append((lambda: check(anchors, cyclic, bad_cycle), "nonnegative cycle")) + disconnected = deepcopy(negative) + disconnected["entries"] = disconnected["entries"][:1] + cases.append((lambda: check(anchors, cyclic, disconnected), "unclosed cycle")) + cases.append((lambda: solve(anchors, applied[:1]), "unapplied anchor")) + cases.append((lambda: check(anchors, applied[:1], positive), "checker unapplied anchor")) + cases.append((lambda: solve((anchors[0], anchors[0]), applied), "duplicate anchors")) + cases.append((lambda: solve((identity(2), zero(2)), applied), "higher-rank anchor")) + cases.append((lambda: solve(anchors[:1], applied), "incomplete anchor family")) + cases.append((lambda: solve(anchors, (upper(((0, 0.5), (0, 0))),)), "float input")) + cases.append((lambda: solve(anchors * 5, applied), "dimension limit")) + cases.append((lambda: solve(anchors, applied * 22), "applied-matrix limit")) + count = sum(rejection(call, message) for call, message in cases) + # Dropping the offending applied inverse changes the problem, not the theorem. + free = ((1, 0, 0, 0), (0, 1, 0, 0), (0, 0, 2, 0), (0, 0, 0, 1)) + require(check(anchors, applied + (free,), solve(anchors, applied + (free,))), + "singular reduction must remain allowed") + with_inverse = applied + (free, inverse(free)) + require(not check(anchors, with_inverse, solve(anchors, with_inverse)), + "applied inverse omitted") + even_hd = block_at(upper(((2, 0), (0, 2))), 0, 1, 2) + require(all(not x or valuation(x) > 0 for row in even_hd for x in row), + "even target has nonzero mod-two HD block") + return {"rejected": count, "scope_controls": 3} + + +def source_hashes(): + manifest = json.loads((PACKAGE / "SOURCES.json").read_text()) + root = PACKAGE.parents[1] + for row in manifest["files"]: + if row["usage"] == "input": + require(sha256((root / row["path"]).read_bytes()).hexdigest() == row["sha256"], + "changed predecessor text") + return {p.name: sha256(p.read_bytes()).hexdigest() + for p in sorted(PACKAGE.iterdir()) if p.is_file()} + + +def main(): + require(len(sys.argv) == 1, "this verifier accepts no arguments") + hashes = source_hashes() + report = {"status": "PASS_PROJECTOR_ANCHORED_PAIRED_LATTICES", + "claim_type": "scoped proof with finite corroboration", + "graphs": graph_corpus(), "walsh_separation": walsh_separation(), + "controls": controls(), "package_sha256": hashes, + "python": sys.version.split()[0]} + print(json.dumps(report, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()