Prove the paired-root floor for three-shear cycles off tsu = ±1 (no κ)

research/dn-three-cycle-floor/PROOF.md

@@ -0,0 +1,110 @@
+# Three-cycle obstruction outside two product loci
+
+This proof was produced by Nick Petalas. Apache-2.0.
+
+## Statement
+
+Let G be any finite simple graph on n >= 3 coordinates. On every edge
+{i,k}, i<k, retain both rows e_i+e_k and e_i-e_k, forming a rational
+matrix R with v=2|E(G)| rows. Isolated coordinates are permitted. A fitting
+binary matrix B has B_ii=1 and B_ik=0 for distinct rows whose rational inner
+product is nonzero. The other directed entries are arbitrary, independently.
+For rational factors P,Q with P Q^T=R R^T, their algebraic COPY bill is
+
+    C_B(P,Q) = sum_j rank_F2 B[supp(P_j), supp(Q_j)].
+
+Fix distinct a,b,c, rational t,s,u, and set
+
+    M = (I+t E_ab)(I+s E_bc)(I+u E_ca),
+    P = R M, Q = R M^(-T), h = tsu.
+
+If h is neither 1 nor -1, then for every common fitting directed B,
+
+    rank_F2 B[supp(P_j),supp(Q_j)] >= degree_G(j) for every j,
+    C_B(P,Q) >= 2|E(G)| = v.
+
+The statement includes zero coefficients and arbitrary additional coordinates.
+It excludes this ordered coordinate-cycle family away from h=+/-1. It does
+not exclude savings on those two loci or for other three-shear patterns.
+
+## Common sign roots and the credited forced minor
+
+For rational vectors p,q and edge {j,k}, the two sign-root products satisfy
+
+    (p_j+p_k)(q_j+q_k) + (p_j-p_k)(q_j-q_k)
+        = 2(p_j q_j + p_k q_k).                         (1)
+
+Thus a nonzero right side guarantees at least one sign root in both
+supports of R p and R q. For each edge incident to j, choose one such
+root as both a row and a column of the support rectangle. Distinct chosen
+roots share exactly coordinate j and have inner product +1 or -1. Their
+B off-diagonal entries are forced to zero and their diagonals are one.
+They therefore form an identity minor of size degree_G(j).
+
+This common-support degree argument is the lemma of JoyboyBrian's #5214,
+building on Nick Petalas's #5176. It is cited and restated to make the new
+application readable. No new general rank-minor principle is claimed.
+
+## New cycle calculation
+
+Relabel a,b,c as 0,1,2. The affected blocks are exactly
+
+    M = [ 1+h   t   ts ],       M^(-T) = [  1   0   -u ],
+        [  su   1    s ]                    [ -t   1   tu ]
+        [   u   0    1 ]                    [  0  -s    1 ]
+
+and both matrices are identity on other coordinates. The factors are
+reciprocal, so P Q^T=R M M^-1 R^T=R R^T on every input.
+
+For column j, write w_k=M_kj (M^(-T))_kj. These products, not the separate
+entries, decide the right side of (1). The three changed columns give
+
+| Column j | w_a | w_b | w_c | All other w_k |
+| --- | ---: | ---: | ---: | ---: |
+| a | 1+h | -h | 0 | 0 |
+| b | 0 | 1 | 0 | 0 |
+| c | -h | h | 1 | 0 |
+
+For the a-term, an edge to b has w_a+w_b=1. Any other incident edge has
+sum 1+h. For the b-term, every incident edge has sum 1. For the c-term,
+an edge to a has sum 1-h, an edge to b has sum 1+h, and every other
+incident edge has sum 1. An unchanged coordinate has w_j=1 and all other
+w_k=0, so its incident sums are also 1.
+
+All listed sums are nonzero when h is neither 1 nor -1. Equation (1) and
+the degree lemma therefore give the asserted termwise bounds. Summing the
+degrees counts each edge twice and proves the complete bill floor. The
+empty-edge graph has zero bill and satisfies the theorem trivially.
+
+At zero coefficients the coordinate basis and the common pairing B_*
+with all-ones 2-by-2 blocks on each sign pair attain v. Hence the joint
+minimum over this allowed family and all pairings is v. This is not a
+claim that every fixed nonzero M attains its lower bound.
+
+## Why the excluded loci remain open
+
+At t=s=u=1, take the single edge {a,c}. The c-term's P values on its two
+roots are (2,0), and its Q values are (0,-2). No common sign root survives.
+At t=s=1,u=-1, the same failure occurs on edge {b,c} in the c-term, with
+P values (2,0) and Q values (0,-2).
+
+These are failures of this particular degree minor. Neither is a
+counterexample to the complete bill floor: other terms and common-pairing
+constraints still contribute. In particular the theorem makes no claim
+that either exceptional locus supplies an improvement.
+
+## Evidence and limits
+
+The standalone verifier builds M by literal shear multiplication and
+obtains its dual by rational Gaussian elimination. It compares both with
+the displayed matrices, checks every Gram entry and chosen identity minor,
+and enumerates every fitting directed B on the stated three-coordinate
+domains. A separate set-of-span oracle checks every small binary rank.
+Finite tests corroborate this proof; they are not its universal quantifier.
+
+The proof concerns rational Gram factors, paired sign roots, a fixed square
+factor count and one common directed fitting binary pairing. It gives no
+physical coefficient arithmetic, native implementation, producer/consumer,
+dirty-restoration program, stock, precision, tape or recursive invoice.
+No new kappa, supplier admission or complete multiplication theorem follows.
+Independent human and formal proof-kernel review are unclaimed.

research/dn-three-cycle-floor/README.md

@@ -0,0 +1,132 @@
+# Three-shear cycles need exceptional products to escape the paired-root floor
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+Independent human and formal proof-kernel review are unclaimed.
+
+Claim type: scoped written proof with exact finite corroboration. For every
+finite simple graph, retain both roots e_i+e_j and e_i-e_j on each edge.
+Let R contain those rows, and change the Gram factor basis by
+
+    M=(I+t E_ab)(I+s E_bc)(I+u E_ca),
+    P=R M, Q=R M^(-T), with distinct a,b,c and rational t,s,u.
+
+Whenever tsu is neither 1 nor -1, every common directed fitting binary
+pairing B has the complete algebraic COPY bill
+
+    sum_j rank_F2 B[supp(P_j),supp(Q_j)] >= 2|E|.
+
+In fact every term costs at least its coordinate's graph degree. The
+coordinate basis attains the bound, so the joint optimum over this allowed
+family is exactly the number of live roots. A fixed nonzero basis can cost
+more. Isolated coordinates and zero shear coefficients are included.
+
+This extends the two-interacting-shear obstruction of JoyboyBrian's
+[PR5214](https://github.com/CrocSwap/integer-mult-bounds/pull/5214) into the
+three-coordinate-cycle case. That package explicitly leaves three interacting
+shears open. Its forced identity-minor lemma is a cited predecessor; the new
+step is the cycle calculation and its all-graph application. The result
+narrows this cycle family to two exceptional product loci for any possible
+saving. Neither locus is claimed to save anything.
+
+[PROOF.md](PROOF.md) gives the universal proof and two explicit lost-minor
+examples on tsu=+/-1. Those examples explain the proof boundary; a missing
+minor alone is not a favorable complete invoice.
+
+## Reproduce
+
+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/dn-three-cycle-floor/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/dn-three-cycle-floor/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/dn-three-cycle-floor
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/dn-three-cycle-floor --check-source-history
+```
+
+Any other CPython 3.12 executable can replace the local path. The direct
+marker is PASS_DN_THREE_CYCLE_FLOOR. Each direct run prints a generated JSON
+receipt bound to all six package files. It writes no files, imports no
+predecessor executable and works outside a Git checkout. The generic runner
+separately validates exact historical source pins.
+
+The finite corroboration checks every nonempty graph on three coordinates
+and every coefficient triple in {-2,-1,-1/2,0,1/2,1,2} outside the two excluded
+product loci. There are 2,009 exact factorizations and 35,588 complete common
+pairing bills, with all admissible directed pairing entries enumerated.
+It checks 309,960 identity-minor entries and 106,764 comparisons against a
+separately implemented set-of-span rank oracle. The 56 excluded coefficient
+triples are counted as excluded, rather than accepted by the theorem.
+
+Another 24 factorizations in dimensions four, five and eight include external
+edges, isolated coordinates, zero coefficients and rational coefficients.
+They check 168 complete directed-pairing bills and 2,856 minor entries. On
+PR5214's actual 12-root D5 graph, t=2,s=u=1 has edge-block bill
+(4,3,5,2,2), total 16. This is an explicit complete bill, not its optimized
+minimum. Eight rejecting domain, fitting and false-minor controls and two
+exceptional-locus witnesses pass. Rational elimination derives the dual
+separately from the displayed formula; every Gram entry is checked.
+
+## Scope and provenance
+
+The scientific base is canonical main e54523517d0f03e58352e647c403a5af3e525a57,
+priority revision 8, selected #7000. TASK.json records a changed
+complex-rank-shape-decoder scope to this algebraic side result. The selected
+source-binding first example passed; no selected scientific replay ran.
+SOURCES.json pins PR5214's incorporated proof and README as provenance.
+No predecessor proof, result or frozen source is changed or scientifically
+replayed.
+
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19539403)
+records the scope. Live PR and handoff checks, batch reservations, main README
+searches and merged-PR searches found no matching cycle theorem in the
+checked coverage. The cached overlap report covers 489 open PRs and 7,156
+Discussion records with complete pagination, but only 207 of 10,178 tracked
+local notes were materialized at its first task scan. Main-tree searches and
+the relevant source reads supplemented that sparse coverage. Unpublished
+work and arbitrary historical diffs are not covered; global literature
+priority is unclaimed.
+
+The theorem concerns rational paired roots and this ordered shear cycle.
+Other three-shear patterns, either exceptional product locus, single-sign
+deletions, larger basis families, extra terms and factors outside the root
+code remain outside it. The physical coefficient arithmetic, producer and
+consumer, dirty restoration, frames, native alignment, storage, precision,
+tape movement and full recursive bill are unpriced. No new kappa, physical
+supplier, complete multiplication theorem, selected-frontier change or
+framework-assumption discharge is claimed. No Lean or Docker check ran.
+
+## Open next questions
+
+1. Can tsu=1 or tsu=-1 lower the complete common-pairing bill on an actual
+   paired graph? Start with the two lost-minor fixtures and then price all
+   terms on a paired D5 graph using one fitting B. The lost minor is the
+   current proof gap, not evidence of a saving.
+2. Can a different three-shear index pattern or basis family give an actual
+   paid decoder improvement? Start with full Gram equality, one common
+   fitting pairing and a complete coefficient/restoration/frame invoice.
+   The physical producer/consumer and recursive budget remain blockers.
+
+## Credit and implementation constraints
+
+JoyboyBrian #5214 supplies the explicit next question, common-support degree
+lemma and two-shear boundary. Nick Petalas #5176 supplies the fixed-split
+predecessor; ywz65 #2536/#2719 supplies coordinate pairing and full-Dn
+root-code results; Aaron Wang / navinor #2272/#2518 supplies the small-T
+screens; DreamingOfClouds supplies the retained Gram/COPY model and root-code
+lineage. Their results are cited, not audited here. The new cycle obstruction,
+proof and finite checker were produced by Nick Petalas. Classical matrix
+multiplication, Gaussian elimination and binary rank retain their status as
+classical tools.
+
+The verifier has no recursion, process launch, network access, mutable global
+cache or dynamic code. All loops run over fixed finite fixture collections
+or dimensions bounded by eight; each binary reduction has a 57-step cap.
+Functions are at most 31 physical lines. Explicit exceptions remain enabled
+under -O. CPython's managed Fraction, integer and container allocation is a
+deviation from fixed allocation. Coordinate matrices have at most eight rows
+and columns, root matrices have at most 56 rows and eight columns, and Gram
+matrices have at most 56 rows and columns. Actual fixtures have at most 12
+root rows. Pairing enumeration uses at most six free bits. The independent
+span oracle has at most six rows and 64 states. No allocation-free runtime claim
+is made. Warning-strict normal/optimized execution and AST inspection are
+the available diagnostics; separate type or lint analysis is unclaimed.

research/dn-three-cycle-floor/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8",
+      "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/dn-two-shear-pairing-floor/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "e04b2a8d0e932fc47a99ec45977262243f524f86",
+      "sha256": "93053bfceb52f228028f5b8fb9d2c0cf3cf4cc2275af7955230095137c177280"
+    },
+    {
+      "path": "research/dn-two-shear-pairing-floor/README.md",
+      "usage": "provenance",
+      "git_blob": "97a575117ce72b03aa300bc98f48effd00c245bd",
+      "sha256": "bb28ba388668915b0fbe35843174f2b4fc5d1c45daeab1e028784b3f779a29eb"
+    }
+  ]
+}

research/dn-three-cycle-floor/TASK.json

@@ -0,0 +1,83 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-rank-shape-decoder",
+  "priority_revision": 8,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "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": "Universal paired-root algebraic COPY floor for a three-shear coordinate cycle whenever tsu is neither 1 nor -1.",
+  "scope_change_reason": "Takes the three-interacting-shear open question of JoyboyBrian PR5214. This is an algebraic side obstruction, without a legal physical producer/consumer or complete recursive invoice.",
+  "bottleneck_link": "Excludes the stated open part of a changed-basis decoder family from lowering its complete common-pairing algebraic COPY bill. Physical supplier obligations remain separate.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first proved extension; do not pursue the exceptional product loci or another basis family.",
+  "outcome": "completed",
+  "evidence": "PROOF.md gives the all-graph rational theorem; verify.py gives exact Gram identities, complete small pairing censuses, forced minors, independent span ranks and rejecting controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can either exceptional product locus tsu=1 or tsu=-1 lower the complete common-pairing bill on a paired graph?",
+      "why_it_matters": "The new proof excludes the complementary parameter domain. Its lost minor alone does not decide the exceptional loci.",
+      "first_step": "Use the two explicit lost-minor fixtures, then price every term with one common fitting pairing on an actual paired D5 graph.",
+      "blocked_by": "No complete favorable common-pairing invoice or uniform replacement lower bound is supplied."
+    },
+    {
+      "question": "Can a fully priced actual decoder use a different three-shear index pattern or another basis family?",
+      "why_it_matters": "The ordered coordinate cycle and paired-sign hypotheses delimit this obstruction.",
+      "first_step": "Write one exact Gram factorization, one common fitting pairing and the complete coefficient, restoration, frame and recursive invoice.",
+      "blocked_by": "Physical producer/consumer and complete bill remain unknown."
+    }
+  ],
+  "claim_type": "scoped written proof with exact finite corroboration",
+  "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19539403"
+}