From 7c49d1da1af141de374ec4c2267192b4d381a601 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 19:03:47 +0000 Subject: [PATCH] feat(research): require a shared odd cycle for plane-port clique savings On a clique of the strict plane-port mask, the cross-term sum equals the identity minus the diagonal-term sum. Its support therefore lies in both term graphs, so a bipartite diagonal-term graph already excludes a saving. This sharpens spectral condition E3 of PR #5560. --- research/plane-port-clique-odd-cycle/PROOF.md | 88 ++++++++++ .../plane-port-clique-odd-cycle/README.md | 80 +++++++++ .../plane-port-clique-odd-cycle/SOURCES.json | 24 +++ .../plane-port-clique-odd-cycle/TASK.json | 87 ++++++++++ .../plane-port-clique-odd-cycle/VERIFY.json | 30 ++++ .../plane-port-clique-odd-cycle/verify.py | 156 ++++++++++++++++++ 6 files changed, 465 insertions(+) create mode 100644 research/plane-port-clique-odd-cycle/PROOF.md create mode 100644 research/plane-port-clique-odd-cycle/README.md create mode 100644 research/plane-port-clique-odd-cycle/SOURCES.json create mode 100644 research/plane-port-clique-odd-cycle/TASK.json create mode 100644 research/plane-port-clique-odd-cycle/VERIFY.json create mode 100644 research/plane-port-clique-odd-cycle/verify.py diff --git a/research/plane-port-clique-odd-cycle/PROOF.md b/research/plane-port-clique-odd-cycle/PROOF.md new file mode 100644 index 0000000000..f93c3110e3 --- /dev/null +++ b/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 κ. diff --git a/research/plane-port-clique-odd-cycle/README.md b/research/plane-port-clique-odd-cycle/README.md new file mode 100644 index 0000000000..069dfe9019 --- /dev/null +++ b/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. diff --git a/research/plane-port-clique-odd-cycle/SOURCES.json b/research/plane-port-clique-odd-cycle/SOURCES.json new file mode 100644 index 0000000000..de67542b5c --- /dev/null +++ b/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" + } + ] +} diff --git a/research/plane-port-clique-odd-cycle/TASK.json b/research/plane-port-clique-odd-cycle/TASK.json new file mode 100644 index 0000000000..088b05a6cf --- /dev/null +++ b/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" + } + ] +} diff --git a/research/plane-port-clique-odd-cycle/VERIFY.json b/research/plane-port-clique-odd-cycle/VERIFY.json new file mode 100644 index 0000000000..32eb22be03 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/plane-port-clique-odd-cycle/verify.py b/research/plane-port-clique-odd-cycle/verify.py new file mode 100644 index 0000000000..6a5390c61b --- /dev/null +++ b/research/plane-port-clique-odd-cycle/verify.py @@ -0,0 +1,156 @@ +#!/usr/bin/env python3 +"""Exact checks for the plane-port clique odd-cycle lemma (see PROOF.md). + +The lemma is proved in PROOF.md. This script authenticates the E3 source +sentence it sharpens, corroborates the lemma on exact rational +decompositions of the identity, and checks that the conditions it imposes are +not vacuous: a triangle can satisfy E3's spectral inequality. +""" +from fractions import Fraction +from pathlib import Path +import hashlib +import random + +PLANES = 3 +DIM = 2 * PLANES +THEORY = Path(__file__).resolve().parents[1] / "plane-port-global-rank-dual" / "THEORY.md" +THEORY_SHA256 = "dab2db4431bc6e75b48fcce4dc4a0d7a0bf1fc65a26b4e3dce2cdf7689d963b8" +E3_SENTENCE = "If the cross terms are bipartite" +TRIALS = 400 + + +def require(ok, message="check failed"): + if not ok: + raise SystemExit("FAIL: " + message) + + +def rank(rows): + m = [list(r) for r in rows] + r = 0 + for c in range(len(m[0]) if m else 0): + piv = next((i for i in range(r, len(m)) if m[i][c] != 0), None) + if piv is None: + continue + m[r], m[piv] = m[piv], m[r] + for i in range(len(m)): + if i != r and m[i][c] != 0: + f = m[i][c] / m[r][c] + m[i] = [a - f * b for a, b in zip(m[i], m[r])] + r += 1 + return r + + +def rank_one_factors(mat): + """Exact rank factorization: mat = sum of outer(u, v).""" + m = [list(r) for r in mat] + terms = [] + while any(x != 0 for row in m for x in row): + i, j = next((i, j) for i in range(DIM) for j in range(DIM) if m[i][j] != 0) + u = [m[k][j] for k in range(DIM)] + v = [m[i][k] / m[i][j] for k in range(DIM)] + terms.append((u, v)) + m = [[m[a][b] - u[a] * v[b] for b in range(DIM)] for a in range(DIM)] + return terms + + +def planes_of(vec): + return frozenset(p for p in range(PLANES) if vec[2 * p] != 0 or vec[2 * p + 1] != 0) + + +def outer_sum(terms): + return [[sum((u[a] * v[b] for u, v in terms), Fraction(0)) for b in range(DIM)] for a in range(DIM)] + + +def block_support(mat): + return {(p, q) for p in range(PLANES) for q in range(PLANES) if p != q + and any(mat[2 * p + a][2 * q + b] != 0 for a in (0, 1) for b in (0, 1))} + + +def bipartite(edges): + side = {} + for start in range(PLANES): + if start in side: + continue + side[start], stack = 0, [start] + while stack: + p = stack.pop() + for a, b in edges: + for x, y in ((a, b), (b, a)): + if x == p: + if y not in side: + side[y] = 1 - side[p] + stack.append(y) + elif side[y] == side[p]: + return False + return True + + +def random_term(rng): + s = rng.sample(range(PLANES), rng.randint(1, PLANES)) + t = rng.sample(range(PLANES), rng.randint(1, PLANES)) + u = [Fraction(rng.randint(-3, 3)) if k // 2 in s else Fraction(0) for k in range(DIM)] + v = [Fraction(rng.randint(-3, 3), rng.choice((1, 2))) if k // 2 in t else Fraction(0) for k in range(DIM)] + return u, v + + +def check_decompositions(): + rng = random.Random(20261027) + identity = [[Fraction(int(a == b)) for b in range(DIM)] for a in range(DIM)] + bip = saving_shaped = 0 + for _ in range(TRIALS): + terms = [t for t in (random_term(rng) for _ in range(rng.randint(1, 6))) + if planes_of(t[0]) and planes_of(t[1])] + rest = [[identity[a][b] - x for b, x in enumerate(row)] for a, row in enumerate(outer_sum(terms))] + terms += rank_one_factors(rest) + require(outer_sum(terms) == identity) + diag = [t for t in terms if planes_of(t[0]) & planes_of(t[1])] + cross = [t for t in terms if not planes_of(t[0]) & planes_of(t[1])] + n = outer_sum(cross) + g = {(p, q) for u, v in cross for p in planes_of(u) for q in planes_of(v)} + h = {(p, q) for u, v in diag for p in planes_of(u) for q in planes_of(v) if p != q} + supp = block_support(n) + require(supp <= g & h, "support of N must lie in both term graphs") + m = DIM - rank([[identity[a][b] - n[a][b] for b in range(DIM)] for a in range(DIM)]) + require(len(diag) >= DIM - m) + if bipartite(supp): + bip += 1 + plus = DIM - rank([[identity[a][b] + n[a][b] for b in range(DIM)] for a in range(DIM)]) + require(plus == m and 2 * m <= rank(n)) + if 2 * m > len(cross): + saving_shaped += 1 + require(not bipartite(g & h)) + return bip, saving_shaped + + +def check_triangle_control(): + """Three single-source cross terms whose sum has 2m = 4 > rank 3.""" + m_mat = [[Fraction(int(i == j)) - 1 for j in range(3)] for i in range(3)] # I - J + cross = [] + for j in range(3): + u = [Fraction(int(k == 2 * j)) for k in range(DIM)] + v = [m_mat[j][k // 2] if k % 2 == 0 else Fraction(0) for k in range(DIM)] + cross.append((u, v)) + require(all(not planes_of(u) & planes_of(v) for u, v in cross)) + n = outer_sum(cross) + one = [[Fraction(int(a == b)) - n[a][b] for b in range(DIM)] for a in range(DIM)] + m = DIM - rank(one) + require((rank(n), m) == (3, 2) and 2 * m > len(cross)) + require(not bipartite(block_support(n)) and len(block_support(n)) == 6) + # Any completion must put diagonal terms on all six directed pairs. + return block_support(n) + + +def main(): + data = THEORY.read_bytes() + require(hashlib.sha256(data).hexdigest() == THEORY_SHA256) + require(E3_SENTENCE in data.decode()) + bip, saving_shaped = check_decompositions() + pairs = check_triangle_control() + require(bip > 0) + print(f"decompositions={TRIALS} bipartite_supports={bip} spectral_saving_shapes={saving_shaped}") + print(f"triangle_control rank=3 m=2 directed_pairs={len(pairs)}") + print("PASS_PLANE_PORT_CLIQUE_ODD_CYCLE") + + +if __name__ == "__main__": + main()