Prove plane-port clique savings need an odd cycle in both term graphs (no new κ)

research/plane-port-clique-odd-cycle/PROOF.md

@@ -0,0 +1,88 @@
+# A clique saving needs an odd cycle shared by cross and diagonal terms
+
+Contract and notation are those of `research/plane-port-global-rank-dual`
+(PR #5560, Mark / Matarener), which uses CubeJerry's #4365 contract. A term
+`u_k v_kᵀ` touches plane sets `A_k` (rows) and `R_k` (columns). Its tariff is
+the binary pairing rank of the generated spans. Coefficients lie in a field of
+characteristic other than 2. Characteristic 2 already has the floor 224.
+
+## Setting (THEORY.md, E3)
+
+Let `S` be a clique of pairwise non-orthogonal planes, so the mask restricted to
+the `2|S|` ports of `S` is the identity. Restrict every term that touches `S` on
+both sides to `S × S`. Other terms contribute nothing to this block. A term is
+*diagonal* when `A_k ∩ R_k ∩ S` is nonempty, which forces tariff at least 2. It
+is *cross* when `A_k ∩ S` and `R_k ∩ S` are disjoint, with tariff `t_j ≥ 1`. Let
+`N` be the sum of the cross terms on `S` and `m = dim ker(I - N)`. E3 proves
+
+    cost on S  >=  4|S| - 2m + Σ_j t_j,
+
+and, when `N` is supported on a bipartite plane graph, `2m <= rank N`, hence no
+saving.
+
+## Lemma
+
+Define two directed graphs on the planes of `S`:
+
+- `G`: `(P, Q)` with `P ≠ Q` is an edge when some cross term has `P ∈ A_k` and
+  `Q ∈ R_k`;
+- `H`: `(P, Q)` with `P ≠ Q` is an edge when some diagonal term has `P ∈ A_k`
+  and `Q ∈ R_k`.
+
+Let `supp N` be the set of `(P, Q)` with `P ≠ Q` and nonzero block `N_PQ`. Then
+
+    supp N  ⊆  G ∩ H.
+
+If the undirected graph underlying `G ∩ H` is bipartite, the cost on `S` is at
+least `4|S|`. Equivalently, a saving on `S` requires an odd cycle of planes
+each of whose consecutive pairs is reached, in some orientation, by a cross
+term **and** by a diagonal term.
+
+## Proof
+
+The block `N_PQ` is a sum of the `P × Q` blocks of cross terms. A cross term
+contributes to it only when `P ∈ A_k` and `Q ∈ R_k`, so `supp N ⊆ G`.
+
+On `S × S` the diagonal and cross terms sum to the identity, so
+`N = I - D`, where `D` is the diagonal-term sum. For `P ≠ Q` the identity block
+`I_PQ` is zero, so `N_PQ = -D_PQ`. A diagonal term contributes to `D_PQ` only
+when `P ∈ A_k` and `Q ∈ R_k`. Hence `N_PQ ≠ 0` gives an edge of `H`, and
+`supp N ⊆ H`.
+
+Also `N_PP = 0`, because a cross term never has the same plane on both sides.
+If the underlying graph of `G ∩ H` is bipartite, choose sides and let `Σ` be the
+diagonal matrix with `+1` on the ports of one side and `-1` on the other. Every
+nonzero block of `N` joins the two sides, so `Σ N Σ = -N`. Then `Σ` maps
+`ker(I - N)` onto `ker(I + N)`. Both kernels lie in the range of `N`
+(`x = ±N x`), and they meet only in 0 since `1 ≠ -1`. Thus
+`2m <= rank N <= #cross terms <= Σ_j t_j`, and E3's inequality gives cost at
+least `4|S|`. ∎
+
+The bipartite step is E3's argument. The new content is the inclusion
+`supp N ⊆ H`. Bipartiteness of the diagonal-term graph alone now excludes a
+saving, whatever the cross terms do.
+
+## Consequences
+
+1. **Triangles.** For `|S| = 3` the only odd cycle is the triangle. A saving on
+   a 3-clique needs diagonal terms reaching all three plane pairs, and cross
+   terms reaching all three. A diagonal term reaching the pair `{P, Q}` touches
+   `P` and `Q` across its two sides and shares a plane between them. Its
+   tariff is therefore the pairing rank of a span containing a full plane on
+   both sides together with a second plane on one side.
+2. **Search pruning.** An exact or numerical escape search may discard every
+   support pattern whose diagonal-term graph is bipartite, independently of the
+   cross terms and of the coefficients.
+3. **Not vacuous.** The spectral inequality alone does allow a triangle. Three
+   cross terms with sources in distinct planes realize `N` equal to `I - J` on
+   the first coordinate of each plane. Then `rank N = 3` and `m = 2`, so
+   `2m > Σ t_j` is possible when each `t_j = 1`. The lemma then forces the
+   diagonal part `I - N` to reach all six directed plane pairs.
+   `verify.py` checks this example exactly.
+
+## Not proved
+
+The lemma gives a necessary condition only. It does not decide the 224
+conjecture, any open triple or quadruple class, or the global floor 140. It
+does not price the diagonal terms that the triangle condition forces, and it
+says nothing about native realization or κ.

research/plane-port-clique-odd-cycle/README.md

@@ -0,0 +1,80 @@
+# Plane-port clique savings need an odd cycle shared by both term types
+
+**Scoped proof. No new κ.** The selected conditional exponent is unchanged.
+
+For the strict plane-port decoder of Mark (Matarener)'s
+[PR #5560](https://github.com/CrocSwap/integer-mult-bounds/pull/5560)
+(`research/plane-port-global-rank-dual`), spectral condition E3 shows that a
+clique `S` cannot save below 2 per port when its cross terms are bipartite.
+This package sharpens that condition. On `S` the cross sum `N` equals `I`
+minus the diagonal-term sum. Every nonzero off-diagonal block of `N` is
+therefore reached by a cross term **and** by a diagonal term with the same
+orientation:
+
+    supp N  ⊆  G_cross ∩ H_diag.
+
+A saving on a clique therefore needs an odd cycle of planes in both term
+graphs. In particular, a bipartite diagonal-term graph excludes a saving,
+whatever the cross terms and coefficients, in every characteristic other
+than 2. On a 3-clique, diagonal terms must reach all three plane pairs.
+
+The statement and proof are in [PROOF.md](PROOF.md). The bipartite step is
+E3's argument. The inclusion into the diagonal graph is new.
+
+## Evidence
+
+[verify.py](verify.py) authenticates the E3 text it sharpens by SHA256. Over
+exact rationals it then:
+
+- builds 400 seeded decompositions of `I_6` on three planes. Each has random
+  multi-plane terms, completed by an exact rank factorization of the
+  remainder. For every decomposition it checks `supp N ⊆ G ∩ H`, at least
+  `6 - m` diagonal terms, and, when `supp N` is bipartite, `dim ker(I+N) = m`
+  and `2m <= rank N`;
+- checks a triangle control. Three single-source cross terms with
+  `N = I - J` on one coordinate per plane give `rank N = 3` and `m = 2`. The
+  spectral inequality alone therefore admits a triangle, and the lemma forces
+  diagonal terms on all six directed pairs.
+
+The random decompositions corroborate the proof. They are not a census.
+
+## Reproduce
+
+From the repository root, Python 3.12, standard library only:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/plane-port-clique-odd-cycle
+python3.12 -B research/plane-port-clique-odd-cycle/verify.py
+python3.12 -O -B research/plane-port-clique-odd-cycle/verify.py
+```
+
+Each prints `PASS_PLANE_PORT_CLIQUE_ODD_CYCLE` in well under a second.
+
+## Limitations
+
+This is a necessary condition only. It does not decide the 224 conjecture, the
+global floor 140, or any open three- or four-plane class. It does not price
+the multi-plane diagonal terms that a triangle forces, and it does not cover
+native realization, hosting or κ. The proof is written and has not been
+checked in a proof kernel.
+
+## Open next questions
+
+1. **Price the forced diagonal terms.** On the open three-plane classes of
+   `three-plane-rank-dual`, a saving now needs diagonal terms reaching the
+   expensive plane pair. Bound their tariff excess against `2m - Σ t_j`.
+   First tabulate, for each open class, the cheapest diagonal support reaching
+   each pair.
+2. **Directed refinement.** The inclusion is directed. Does a saving need a
+   directed odd cycle, or can the eigenvalue argument use orientation
+   further?
+3. **Global use.** Feed the bipartite-diagonal exclusion into a clique
+   programme as a structural cut, rather than another LP column.
+
+## Credit
+
+The contract is CubeJerry's (#4365). The global floor, spectral condition E3
+and the 224 conjecture are Mark (Matarener)'s PR #5560. The three-plane
+classes are Ryanson Jonathan's `three-plane-rank-dual`. This package, produced
+by Nick Petalas, adds only the diagonal-graph inclusion and its consequences.
+Apache-2.0.

research/plane-port-clique-odd-cycle/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "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/plane-port-global-rank-dual/THEORY.md",
+      "usage": "input",
+      "git_blob": "bfa8755cae4f883bdd1c863c5fc821d481341519",
+      "sha256": "dab2db4431bc6e75b48fcce4dc4a0d7a0bf1fc65a26b4e3dce2cdf7689d963b8"
+    }
+  ]
+}

research/plane-port-clique-odd-cycle/TASK.json

@@ -0,0 +1,87 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-rank-shape-decoder",
+  "priority_revision": 8,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "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": "Sharpen PR5560 spectral condition E3 for the strict plane-port decoder: on a clique, the cross sum is supported inside both the cross-term and diagonal-term plane graphs, so a saving needs an odd cycle in both.",
+  "scope_change_reason": "The card asks for a complete changed decoder invoice. This is a structural lemma on the plane-port decoder contract that restricts where a decoder saving can occur; it does not price a supplier.",
+  "bottleneck_link": "Side result for the plane-port decoder lever: it restricts which support patterns can beat 2 per port, toward the all-field 224 conjecture. No complete invoice or kappa change.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the written necessary condition and exact corroboration; do not start a class census or LP within this session.",
+  "outcome": "completed",
+  "evidence": "PROOF.md; verify.py checks 400 exact rational decompositions of I6 on three planes and a triangle control.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "What tariff excess do the forced diagonal terms carry on the open three-plane classes?",
+      "why_it_matters": "Comparing it with 2m - sum t_j could settle those classes over every field.",
+      "first_step": "Tabulate the cheapest diagonal support reaching each plane pair in each open class.",
+      "blocked_by": "nothing"
+    },
+    {
+      "question": "Does a saving need a directed odd cycle?",
+      "why_it_matters": "A directed condition would prune more support patterns.",
+      "first_step": "Test the signature argument on directed-acyclic supports.",
+      "blocked_by": "nothing"
+    },
+    {
+      "question": "Can the bipartite-diagonal exclusion act as a structural cut in a global clique programme?",
+      "why_it_matters": "It could raise the all-field floor above 140 without new LP columns.",
+      "first_step": "Express the exclusion per clique as a constraint on term supports.",
+      "blocked_by": "no formulation yet"
+    }
+  ]
+}

research/plane-port-clique-odd-cycle/VERIFY.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/plane-port-global-rank-dual/THEORY.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "E3 source hash, 400 exact decompositions of I6 checking supp N within both term graphs and the bipartite spectral bound, triangle control"
+    },
+    {
+      "argv": [
+        "{python}",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "same checks with assertions disabled; the verifier does not use assert"
+    }
+  ]
+}