Prove one-axis transported coframe optimization is NP-hard

research/transported-coframe-hardness/PROOF.md

@@ -0,0 +1,156 @@
+# A one-axis hardness obstruction for transported coframe optimization
+
+This scoped proof and construction were produced by Nick Petalas. Apache-2.0.
+
+## Statement and cost model
+
+For a fixed finite logical linear program, choose one coframe from a supplied
+two-element menu at each field. Conjugate each logical instruction by the
+chosen coframes. Charge the Gaussian rank power `r^t` of every resulting
+transition, including entrance and exit adapters, with `0^t=0` and `0<t<=1`.
+Main entrance and exit charts are fixed to identity. Any productive endpoint
+credit is fixed across choices and can therefore be subtracted as a constant.
+
+**Theorem.** Minimizing this rank-moment bill is NP-hard even when every field
+has one Gaussian axis, every menu is the same two-element menu, every paid
+rank is one, and all instructions have a fixed explicit chronology. The
+threshold problem for the constructed family is NP-complete. This holds for
+every `0<t<=1`, with exactly the same integer objective for every such `t`.
+
+The theorem concerns this finite rank objective. It does not assert hardness
+of the already submodular common-anchor family, a particular repository word,
+or a full physical cost model. Ordinary work is not included in `r^t`.
+
+## Phase-exact axis
+
+Work over the Gaussian dyadics `Z[i,1/2]`, or over the complex numbers. Set
+
+```text
+W = [[1,1],[1,-1]],       F = W/(1+i).
+F^2 = -i I,              F^-1 = i F.
+```
+
+This is a phase-exact Fourier Clifford axis. Its computational symplectic
+action interchanges the two coordinate axes, so its Gaussian rank is one.
+`I` and `-i I` are monomial maps of Gaussian rank zero. All coefficients are
+Gaussian dyadics. No square root or ignored global phase is required.
+
+Use coframe `F^x` for a bit `x`. On a directed logical shear
+`z_v += F z_u`, the coframe-conjugated response is
+
+```text
+K(x_u,x_v) = F^x_v F F^-x_u = F^(1+x_v-x_u).
+
+                 x_v=0       x_v=1
+x_u=0              F          -i I
+x_u=1              I            F
+```
+
+Its Gaussian rank is `1[x_u=x_v]`. Each entrance adapter `F^x` and exit
+adapter `F^-x` has rank `x`, giving total boundary charge `2x`.
+
+The table is supermodular, with interaction `1+1-0-0=2`. Complementing one
+endpoint reverses its sign. On a triangle, no vertex complements make all
+three edges submodular: the number of edges whose endpoint complements agree
+is always odd. This is an explicit one-axis instance of the signed-cycle
+obstruction in David Ganz's #5693, not a new signed-switching theorem.
+
+## An exact finite program with fixed main boundaries
+
+Let `G=(V,E)` be an arbitrary finite simple graph with `n>=1` vertices and
+`m` edges. Each vertex is a distinct arbitrary main input in a two-coordinate
+payload field. Orient each edge from its smaller vertex to its larger vertex.
+Set `M=2n+1`. In lexicographic edge order, execute the logical shear
+`z_v += F z_u` exactly `M` times per edge. This defines a fixed invertible
+logical program `P_G`, independently of any coframe assignment.
+
+For a chosen vector `x`, apply `F^x_v` once on entrance to each field. Replace
+each shear response by the literal `K(x_u,x_v)` above. On exit apply `F^-x_v`
+to every field. At every instruction the physical field is `F^x_v` times its
+logical field. Substitution proves this invariant and the fixed final endpoint
+`P_G` by induction on chronology. In particular, every main input is arbitrary
+and independent; none is silently zeroed or identified with another input.
+
+For the rank accounting, the source-preserving implementation of a response
+shear is the ordinary owned copy, transform, add and clear construction of
+#5693, coframe-cut.md. Here the transform is exactly one rank-one axis or the
+explicit ordinary monomial map. Its ordinary work and storage remain separate
+from the rank moment. The construction's correctness also follows directly
+from the block shear matrix and does not need an optimizer's certificate.
+
+All main charts at the external boundary are identity. Both adapter charges
+are retained. The endpoint, and hence any declared productive credit, is the
+same for every `x`. A parent-grade legality rule can use any parent grade at
+least two; all positive children have rank one. No actual selected recursive
+caller or productive supplier is asserted here.
+
+## Recovery of Simple Max Cut
+
+Write `c_G(x)` for the number of graph edges whose endpoint bits differ, and
+`|x|` for the number of one bits. The complete rank bill of the constructed
+word is exactly
+
+```text
+B_G(x) = M (m-c_G(x)) + 2|x|.
+```
+
+Every rank is zero or one, so raising ranks to `t` changes no term. There are
+no other Gaussian transitions in this declared word.
+
+Let `c*` be the maximum cut size, and let `s*` be the smallest number of one
+bits among assignments attaining `c*`. Since `0<=2|x|<=2n<M`, the objective
+first minimizes `m-c_G(x)`, then minimizes `|x|`. Consequently
+
+```text
+min_x B_G(x) = M(m-c*) + 2s*,
+c* = m - floor((min_x B_G(x))/M).
+```
+
+More explicitly, for any integer `k` with `0<=k<=m`,
+
+```text
+c* >= k  iff  min_x B_G(x) <= M(m-k)+2n.
+```
+
+The forward implication uses a cut of size at least `k`. For the converse,
+every assignment with `c_G(x)<=k-1` has bill at least `M(m-k+1)`, strictly
+larger than the displayed threshold. This proves a many-one reduction of the
+Simple Max Cut decision problem, whose NP-completeness is due to Garey,
+Johnson and Stockmeyer. The emitted word has `M m` shears and at most `2n`
+adapters, hence polynomial length. A bit assignment lets a verifier compute
+its integer bill in polynomial time. This proves the stated hardness and
+NP-completeness. No power comparison, numerical tolerance or algebraic-number
+oracle occurs in this reduction.
+
+For `G=K3`, `M=7`, `c*=2`, and `s*=1`, so the minimum bill is nine. Dropping
+both adapters would incorrectly give seven; dropping one gives eight. These
+are different objectives. For `G=K5`, the minimum bill is 48.
+
+## Attribution, consequence and limits
+
+Ali Romman's [#5783](https://github.com/CrocSwap/integer-mult-bounds/pull/5783)
+provides the exact submodular binary-table solver and explicitly leaves
+unsupported pair laws outside it. David Ganz's
+[#5693](https://github.com/CrocSwap/integer-mult-bounds/pull/5693), retained in
+`research/joint-gaussian-coframe-search`, supplies the coframe-conjugation,
+fixed-transport and signed-switching framework. Those results are cited as
+predecessors. Their verifiers and actual source instances are not replayed.
+The new step is this explicit one-axis reduction, with fixed main boundaries,
+both adapter charges, phase-exact matrices and a common integer objective for
+the full power interval.
+
+Classical complexity input: M. R. Garey, D. S. Johnson and L. Stockmeyer,
+[Some simplified NP-complete graph problems](https://doi.org/10.1016/0304-3975(76)90059-1),
+Theoretical Computer Science 1, 1976, 237-267, Simple Max Cut. Fourier Clifford
+identities and graph-cut/signed-switching facts retain their classical credit.
+No worldwide novelty is asserted for those components.
+
+The consequence is a worst-case obstruction to a polynomial exact extension
+covering all transported binary menus, unless P=NP. Special source structure,
+small exceptional deletion sets and branch-specific cuts remain valid routes.
+The rank-one family here is deliberately constructed and does not establish
+that any retained supplier has a hard optimization instance. It also gives no
+runtime lower bound for executing its fixed linear map, no claim against
+resynthesis of repeated shears, no complete paid physical invoice, no new
+kappa and no change to the selected frontier. Formal proof-kernel and
+independent human review remain unclaimed.

research/transported-coframe-hardness/README.md

@@ -0,0 +1,110 @@
+# One-axis transported coframe optimization is NP-hard
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Result and scope
+
+**Claim type: scoped mathematical proof, with exact finite corroboration.**
+The rank-moment optimization problem for transported binary coframe choices
+can encode Simple Max Cut. The reduction uses one Gaussian axis per field,
+the identical two-choice menu everywhere, rank-zero/rank-one transitions,
+fixed external main charts, and both entrance and exit adapter charges.
+Its constructed-family decision problem is NP-complete. All power tariffs
+`r^t`, `0<t<=1`, give the same integer objective.
+
+For a graph with `n` vertices and `m` edges, put `M=2n+1`. The explicit word
+has bill
+
+```text
+B(x) = M (m-cut(x)) + 2|x|,
+maxcut(G) = m - floor(min_x B(x)/M).
+```
+
+The phase-exact Gaussian-dyadic Fourier axis is
+`F=[[1,1],[1,-1]]/(1+i)`, with `F^2=-i I` and `F^-1=i F`.
+A transported edge has rank table `[[1,0],[0,1]]`. A triangle gives an
+explicit unswitchable interaction graph, with minimum bill nine including
+all adapter ranks. See [PROOF.md](PROOF.md) for the universal argument,
+literal matrices, chronology, exact threshold reduction and limitations.
+
+This adds an explicit worst-case complexity obstruction beyond the
+submodular solver in Ali Romman's [#5783](https://github.com/CrocSwap/integer-mult-bounds/pull/5783).
+It builds on David Ganz's [#5693](https://github.com/CrocSwap/integer-mult-bounds/pull/5693)
+coframe conjugation and fixed transports. Classical Simple Max Cut hardness
+is due to Garey, Johnson and Stockmeyer. Fourier Clifford identities,
+graph-cut reductions and signed switching retain their established credit.
+The predecessor instances are cited, not audited or replayed.
+
+## Reproduce
+
+From the repository root:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/transported-coframe-hardness/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B -O research/transported-coframe-hardness/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/transported-coframe-hardness
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/transported-coframe-hardness --check-source-history --check-modes
+```
+
+Any CPython 3.12 interpreter with the standard library can replace the absolute
+path. The standalone verifier also runs from a Git-free export. It writes
+only standard output, including a generated receipt with SHA256 hashes of
+all six package files. No committed receipt is hand-authored or trusted.
+
+Expected direct status is `PASS_TRANSPORTED_COFRAME_HARDNESS`. Both registered
+commands also require `PASS_REGISTERED_RESEARCH_PACKAGE`. Exact checks cover:
+
+- 1,099 simple labeled graphs on one through five vertices and all 33,866
+  coframe assignments, with 7,523 separate decision-threshold comparisons.
+- Complete phase-exact logical/physical endpoints for all graphs through
+  three vertices, all choices and all 420 basis columns, giving 2,440 scalar
+  output equalities over Gaussian rationals.
+- Seven invalid-graph rejections, six hypothesis mutants and all eight
+  triangle complements. The mutants remove one or both adapter charges,
+  remove the logical transport, reduce replication, use the wrong inverse,
+  or discard the scalar phase.
+
+The complete-graph minimum bills for one through five vertices are
+`0,2,9,22,48`. Finite enumeration corroborates the written reduction; it
+does not prove the general complexity theorem by testing.
+
+## Limitations
+
+This is a theorem about the declared rank moment. Ordinary work, precision,
+tape movement and storage have no prices in that objective. No complete
+physical invoice, source-specific supplier gain, new kappa, selected-frontier
+change, all-size multiplication theorem or proof-kernel certificate is
+claimed. Independent human and formal proof-kernel review are unclaimed.
+
+The word is constructed for the reduction. Its hardness does not transfer
+to the actual 423-choice source, to common-anchor identity transports, or
+to unrestricted synthesis of the final linear map. Repeated shears may be
+resynthesized in another family; optimizing that changed family is outside
+this claim. Structured exceptional sets can still make exact search useful.
+
+## Verifier bounds and diagnostics
+
+The verifier has no recursion, subprocesses, imports of predecessor code or
+external inputs. The graph census is bounded by five vertices and ten edges;
+the endpoint census is bounded by three vertices, three edges and seven
+repetitions. Every failure raises an exception also under `-O`. Every function
+is under 60 physical lines. Normal and optimized replay enable warnings as
+errors. No separate static analyzer is installed in the local environment.
+
+Power-of-ten managed-runtime deviation, rules 3 and 9: Python fractions,
+tuples, iteration and standard-library dispatch allocate during verification.
+The fixed finite domains bound live data and call targets; the largest
+assignment collection has 32 entries and the largest endpoint state has six
+Gaussian-rational scalars. Package hashing reads exactly six named files.
+There are no callbacks supplied by inputs. A fixed-capacity implementation
+would be a separate port if these limits were expanded.
+
+## Open next questions
+
+Which actual transported coframe incidence graphs have small signed-cycle
+deletion sets? This matters because the worst-case obstruction leaves
+structured exact cut algorithms useful. Begin by extracting and aggregating
+all signed pair tables of one named source word, retaining every fixed
+transport and target debit. A specific source-bound instance and its full
+physical legality contract are prerequisites. The structured question is
+also recorded in [TASK.json](TASK.json).

research/transported-coframe-hardness/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "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/joint-gaussian-coframe-search/coframe-cut.md",
+      "usage": "provenance",
+      "git_blob": "84b6c8bebf930c1527dd927deda6abc9956429ca",
+      "sha256": "0ad0af8fcdebb1b80bea90ce2dc99c5817923578bfbb26a85a7f53f002825662"
+    },
+    {
+      "path": "research/joint-gaussian-coframe-search/coupled-labels.md",
+      "usage": "provenance",
+      "git_blob": "fbb17555408690f1677a0bdeb962c6305bedf1da",
+      "sha256": "4f6abc8c531f65053130558bb7033a2f15365170d1771df410a3c1c8388ad74f"
+    }
+  ]
+}