Decide paired lattices with rank-one projector anchors (no new κ)

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.

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.

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"
+    }
+  ]
+}

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."
+  }
+}