Prove functional decoder pairings cost at least v over every field

research/functional-pairing-lift/PROOF.md

@@ -0,0 +1,130 @@
+# A simultaneous lift for functional decoder pairings
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+Claim type: scoped proof, with finite exact corroboration.
+
+## Statement
+
+Let B be a v-by-v binary matrix with B_ii=1. Suppose each row has at most
+one off-diagonal one. There is an integer matrix S with the same support,
+diagonal one, and all nonzero entries in {1,-1}, such that every square
+minor of S is 0, 1 or -1. Consequently, for every pair of row and column
+sets R,A and every field K,
+
+    rank_K S[R,A] = rank_F2 B[R,A].
+
+The same conclusion holds when the column condition replaces the row
+condition. One signing works simultaneously for all rectangular blocks.
+No support sets need to be supplied to the construction.
+
+For any field K, let p_t,q_t belong to K^T, with finite T, and suppose
+
+    p_t dot q_t != 0,
+    p_t dot q_s = 0 whenever t != s and B_ts = 1.
+
+Put R_j={t:p_tj != 0}, A_j={t:q_tj != 0}. Then
+
+    sum_j rank_F2 B[R_j,A_j] >= v.
+
+For each B in the stated class the bound is attained if the number of
+totals is unrestricted. This does not assert attainment with T=3.
+
+## Constructing the signing
+
+Write f(i)=j for the off-diagonal one in row i, leaving f(i) undefined
+when there is none. Its directed cycles have distinct vertices and length
+k>=2. Distinct cycles are vertex-disjoint because each vertex has at most
+one successor.
+
+Start with S=B over the integers. On each directed cycle of length k,
+choose its least-indexed vertex i and replace S_i,f(i) by (-1)^k.
+All other supported entries remain one. In particular, even cycles need
+no change; odd cycles receive one minus sign. The cycle-edge product is
+always (-1)^k.
+
+The implementation first removes vertices of indegree zero, then walks
+the remaining cycles. Each vertex enters the removal queue at most once,
+and each remaining vertex is walked once. Given successor lists this is
+linear work and storage in v. Reading and returning a dense matrix takes
+O(v^2) work and storage. The implementation caps v at 256; the written
+theorem has no such bound.
+
+## Every minor is zero or a unit
+
+Consider any square submatrix. If it has a zero row or column its
+determinant is zero. If a row or column has just one nonzero, expand along
+it. The multiplier is 1 or -1. Repeat, reducing the order each time.
+The empty determinant is one.
+
+If a nonempty square core remains with every row and column of degree at
+least two, each row has exactly two nonzeros, since every original row
+had at most two. Counting entries shows that each column also has degree
+exactly two. Both supported entries of every remaining row are present,
+including its original diagonal. Thus the remaining row set is contained
+in the remaining column set. Equal cardinalities make those sets equal.
+The remaining successor map is a permutation without fixed points.
+Its components are complete directed cycles from the original f.
+
+For a cycle of length k, the corresponding block has precisely two
+nonzero determinant terms: the diagonal product 1 and the cycle product
+with permutation sign (-1)^(k-1). Its determinant is
+
+    1 + (-1)^(k-1) (-1)^k = 0.
+
+After simultaneous row and column reordering the core is a nonempty
+block diagonal union of such blocks, so its determinant is zero.
+Undoing the leaf expansions proves that every minor is 0, 1 or -1.
+
+This is an elementary total-unimodularity argument. No historical novelty
+is claimed for total unimodularity or the leaf-expansion method. The new
+decoder reduction is the simultaneous functional-pairing lift and its
+all-T consequence in the retained cost model.
+
+## Field-independent ranks
+
+Reduction of S modulo two is B. A nonzero integer minor of S is 1 or -1,
+which stays nonzero in every field. A zero minor stays zero. The largest
+nonzero minor therefore has the same order over every field, including
+F2. Apply this separately to every rectangular submatrix. The empty-row
+and empty-column cases have rank zero. Transposition proves the column
+version without a new signing argument.
+
+## The decoder cost floor
+
+This step is the Hadamard/lift rank argument credited to #1590 and #2111.
+It is included to state exactly what the new sufficient lift permits.
+Let M_ts=p_t dot q_s. The matrix M Hadamard S is diagonal with nonzero
+diagonal, hence has rank v over K. It is also
+
+    sum_j diag(p_:j) S diag(q_:j).
+
+The j-th summand has rank rank_K S[R_j,A_j]: removing its zero rows and
+columns leaves invertible diagonal rescalings. Rank subadditivity and
+the simultaneous rank identity give
+
+    v <= sum_j rank_K S[R_j,A_j]
+      = sum_j rank_F2 B[R_j,A_j].
+
+For tightness with unrestricted T, choose T=v and p_t=q_t=e_t. Then
+M=I is compatible with every unit-diagonal B, and each of the v terms
+has binary block rank one. This only establishes tightness of the bound
+over the union of all finite-T decoder classes.
+
+## Scope and consequences
+
+The theorem excludes every pairing in this sparse class from beating v,
+including three-total configurations with full-support points, arbitrary
+coefficients and repeated geometric points or lines. It strengthens the
+available list of sufficient reductions; it does not solve #2111's
+general lift problem or claim a new theorem for arbitrary pairings.
+
+The condition is on the chosen pairing B, not just a selected subset of
+its incidences. A configuration whose entire allowed off-diagonal pattern
+has outdegree at most one inherits the bound for every admissible B.
+Otherwise, excluding its functional pairings alone need not exclude a
+cheaper nonfunctional pairing. No decoder, native word, paid supplier,
+physical restoration, recursive invoice or improvement to kappa follows.
+
+The full multiplication theorem's native, ownership, compiler,
+precision/tape and analytic assumptions are not discharged. No formal
+proof-kernel or independent human review is claimed.

research/functional-pairing-lift/README.md

@@ -0,0 +1,107 @@
+# Functional decoder pairings cannot beat cost v
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+Claim type: scoped proof with exact finite corroboration. Independent human
+and formal proof-kernel review are unclaimed.
+
+For every binary pairing B with unit diagonal and at most one off-diagonal
+one per row, an explicit integer signing preserves the rank of every
+rectangular submatrix, simultaneously, over every field. The transposed
+class has the same property. Consequently every exact decoder compatible
+with B has total binary COPY-rank cost at least v, for any finite number
+of totals and over any coefficient field. The bound is attained with v
+coordinate totals. Attainment with three totals is not asserted.
+
+The construction puts one minus sign on each odd directed successor cycle.
+Every square minor of the resulting matrix is 0, 1 or -1. The proof uses
+leaf expansion and the retained Hadamard/lift rank argument. See
+[PROOF.md](PROOF.md) for all quantifiers and the field-independent proof.
+
+This adds a sufficient reduction to DreamingOfClouds's PR #2111, Open next
+question 8. It does not replay its examples or signing searches. Classical
+total unimodularity and the predecessor's Hadamard rank argument retain
+their credit; no historical novelty is claimed for those tools. The new
+contribution is this explicit sparse-class reduction and its checker.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/functional-pairing-lift/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/functional-pairing-lift/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/functional-pairing-lift
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/functional-pairing-lift --check-source-history
+```
+
+Another CPython 3.12 path may replace the local interpreter. The scientific
+marker is `PASS_FUNCTIONAL_PAIRING_LIFT`. Direct replay reads the pinned
+PR2111 README but executes no predecessor code. It needs no Git or network.
+The generic source-history check additionally needs the retained Git history.
+
+Every functional matrix of orders one through four is enumerated. The
+checker compares binary and exact rational ranks on all rectangular
+submatrices and computes every square minor by an independent Leibniz
+formula. Larger cycles, paths, stars and disjoint-pair families through
+order sixteen have prefix/suffix rectangular-rank checks. Nontrivial
+two-total cycle decoders and coordinate-total attainments are checked.
+Malformed inputs, the capacity boundary and an unsigned odd-cycle lift
+distinguish the hypotheses. The generated [RESULT.json](RESULT.json)
+records counts and binds every proof, code and metadata file by SHA256.
+Normal replay writes no files. `--emit NEW_EXTERNAL_PATH` creates a new
+receipt without overwriting an existing file.
+
+## Limits and implementation bounds
+
+The row or column condition is imposed on the complete chosen pairing,
+not a subset of its edges. General pairings and the general three-total
+lift conjecture remain open. This is a mathematical cost obstruction,
+not a new decoder, native word, supplier invoice, kappa or selected-frontier
+update. Physical ownership, restoration, routing, precision, compiler and
+analytic recovery obligations remain separate. No selected cold replay,
+Lean or Docker run is part of the claim.
+
+The signer caps dense input order at 256 and uses no recursion, subprocess,
+network, mutable global cache or predecessor import. All loops have bounds
+from that cap or fixed census limits. Each function is below sixty lines.
+Explicit exceptions remain active under `-O`; warning errors are enabled
+in both registered commands. No external static analyzer is claimed.
+
+Power of Ten rule 3 deviation: CPython allocates integer, Fraction and
+collection objects during execution. This one-shot exact checker cannot
+disable those allocations. The signer retains O(256^2) cells, the complete
+census works on matrices of order at most four, and the larger fixtures
+have order at most sixteen. It retains one current submatrix at a time.
+The endpoint and oversize controls check the input bound. A future native
+steady-operation implementation would need fixed-capacity storage before
+removing this deviation.
+
+## Sources and overlap
+
+The exact base is `3f0152a32eeebac0df11946dbd50cabe5a7f7839`, priority revision
+8. [SOURCES.json](SOURCES.json) pins the source README, historical card and
+selected record. The current baseline binding check passed; it is not a
+scientific supplier replay. The card's scope change is in [TASK.json](TASK.json).
+
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19267785)
+and reservation followed live open-PR, recent-account, handoff, main README
+and merged-PR searches. Targeted terms included functional pairing,
+pseudoforest, cactus, one off-diagonal contact and directed-cycle decoder.
+The cached overlap scan omits sparse local notes; explicit Git searches
+covered all main README paths for the distinctive terms. This is bounded
+overlap evidence, not a novelty certificate or coverage of unpublished work.
+
+Credit DreamingOfClouds #2111 for the model, lift hierarchy and open reduction
+question; #1590 for the exact decoder and Hadamard/lift lemma; and #446/#595
+for the underlying cost model. The E8/P104, native, helper, caller and
+compiler sources retain their predecessor credit. Existing files and
+their credit lines are unchanged.
+
+## Open next questions
+
+1. Can a named second contact preserve simultaneous ranks? Specify its
+   entire pairing graph and first overlapping cycles. The one-successor
+   argument does not decide this larger class.
+2. Can the reduction prune a new decoder search? Start with its complete
+   chosen pairing and preserve all nonfunctional candidates. This package
+   supplies no search integration or physical supplier.

research/functional-pairing-lift/RESULT.json

@@ -0,0 +1,28 @@
+{
+  "claim_type": "scoped-proof",
+  "controls": 9,
+  "exhaustive": {
+    "cycles": 146,
+    "identity_decoder_attainments": 288,
+    "matrices": 288,
+    "rectangular_ranks": 67332,
+    "square_minors": 18486
+  },
+  "larger": {
+    "matrices": 48,
+    "rectangular_ranks": 27680,
+    "two_total_decoders": 12
+  },
+  "schema": "functional-pairing-lift/v1",
+  "sha256": {
+    "PROOF.md": "396d3f4e5bb8feac2651f4ee8b751201f4d114609b87df0f9c101b362550b6ea",
+    "README.md": "a41871da12d74573f36ee387538fb2e30b9ffa3374af0c862c7c80b608a13d04",
+    "SOURCES.json": "b36c6bfc31466eb8d52fe37ee03a5fc59f48fda17257eaf44be4ad7fb6b46a69",
+    "TASK.json": "5a302b775567ade9fad1eccdb2006adba5e855b19287e6186b82c28ed9136abb",
+    "VERIFY.json": "24f0f9ab9d61c6dc66a10b580c140d83c59f3f71b34f8801654f4dd1806415db",
+    "verify.py": "f270f69f3b82f09fb56f886f4841f2148c776c7a91d809cf37a69e334272d8bd"
+  },
+  "source_sha256": {
+    "research/three-total-decoders/README.md": "a812bb80e480a3f2f446e0f0f77300606e4337e4a888c141a7f4380ca15bef07"
+  }
+}

research/functional-pairing-lift/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "3f0152a32eeebac0df11946dbd50cabe5a7f7839",
+  "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/three-total-decoders/README.md",
+      "usage": "input",
+      "git_blob": "229c79d6e9908b3cd2508206d711b5b3dd44c4ea",
+      "sha256": "a812bb80e480a3f2f446e0f0f77300606e4337e4a888c141a7f4380ca15bef07"
+    }
+  ]
+}

research/functional-pairing-lift/TASK.json

@@ -0,0 +1,81 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-rank-shape-decoder",
+  "priority_revision": 8,
+  "base_commit": "3f0152a32eeebac0df11946dbd50cabe5a7f7839",
+  "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": "Construct a simultaneous rank-preserving integer signing for unit-diagonal binary pairings with at most one off-diagonal one per row or per column; deduce cost at least v for every finite number of exact decoder totals over every field.",
+  "scope_change_reason": "A new algebraic sufficient reduction answers a bounded part of PR2111 Open next question 8. It is a scoped side result, not a complete changed supplier itinerary.",
+  "bottleneck_link": "Exclude a precisely stated sparse pairing class from attempts to reduce the decoder COPY-rank bill; dense pairings and physical realization remain open.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first proved sparse-class lift and its decoder consequence, after bounded exact corroboration and package checks. Do not extend the class.",
+  "outcome": "completed",
+  "evidence": "PROOF.md gives the unbounded theorem. verify.py enumerates every functional matrix through order four, every rectangular submatrix rank and every square minor, plus larger families and rejecting controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can one add a second off-diagonal contact in a named row while retaining a simultaneous rank-preserving lift?",
+      "why_it_matters": "This would exclude a larger sparse decoder class.",
+      "first_step": "Specify the entire new pairing graph and inspect its first overlapping cycles.",
+      "blocked_by": "The one-successor leaf/cycle proof no longer applies."
+    },
+    {
+      "question": "Can the functional-pairing reduction prune a new decoder synthesis search without losing better nonfunctional pairings?",
+      "why_it_matters": "It could reduce search work on low-cost decoder candidates.",
+      "first_step": "Declare the search domain and use this theorem only on complete chosen pairing matrices.",
+      "blocked_by": "No synthesis integration or physical supplier is provided."
+    }
+  ]
+}