Prove strict traps for exact rank-one projection cuts (no new κ)

research/projection-local-trap/PROOF.md

@@ -0,0 +1,109 @@
+# A strict local trap for projection cuts
+
+Let K be any field, V=K^2, and 0<t<1. Write h=2^t, so 1<h<2.
+Consider a directed multigraph with fixed vertices carrying 0 and V and
+one free vertex carrying a subspace S of V. There are a parallel edges
+0 -> S and b parallel edges S -> V, where a,b are positive integers.
+Every edge is charged its dimension gap to power t, with 0^t=0.
+Every subspace S is legal. Boundaries stay fixed during a projection move.
+
+The complete objective of this graph is
+
+    E(S) = a (dim S)^t + b (2-dim S)^t.
+
+There are precisely three possible objective values:
+
+    E(V)=a h,       E(line)=a+b,       E(0)=b h.
+
+These formulas retain every edge, including parallel multiplicity. There
+are no productive credits or unpriced terms in this abstract objective.
+
+## Strict local trap and joint escape
+
+By a rank-one projection move we mean the choice, at each free vertex,
+between its current frame F and P(F), for one linear idempotent P whose
+kernel has dimension one. This is the move in Dugongue's PR556. In this
+two-dimensional space, P has rank one and maps V to a line. There is only
+one free vertex, so optimizing all subsets for any such P compares just
+E(V) and E(line).
+
+The initial frame V is strictly worse than the zero frame and strictly
+better than every changed single-projection frame if and only if
+
+    a>b and a+b>a h.                                      (1)
+
+Under (1), every nontrivial rank-one projection move increases the entire
+objective. Exhaustively optimizing each binary move therefore retains V.
+This remains true under any sequence that accepts only nonincreasing
+objectives. It is a strict local minimum with respect to these moves.
+
+Take P(x,y)=(0,y) and Q(x,y)=(x,0). They are idempotent, have one-dimensional
+kernels, commute, and PQ=QP=0. Their joint action sends the free frame to 0.
+Every intermediate frame remains between the fixed boundary frames, hence
+legal. The joint objective decreases by exactly (a-b)h. The first step
+must increase the objective; that is the obstruction to monotone descent.
+Since a+b>a h>b h, the zero frame is also the global optimum over all S.
+
+This proves existence over every field. It does not use a finite-field
+extrapolation or the correctness of a predecessor's implementation.
+
+## Sharp number of edges in this class
+
+Set delta=2-h, with 0<delta<1, and d=a-b, a positive integer. Condition (1)
+is exactly
+
+    a delta>d.
+
+For a fixed d the least possible a is floor(d/delta)+1. This choice has
+b=a-d>=1 because delta<1. Therefore the least edge count at that d is
+
+    N_d = 2 floor(d/delta)+2-d.
+
+As 1/delta>1, increasing d by one increases floor(d/delta) by at least one.
+Thus N_(d+1)-N_d>=1. The global minimum occurs at d=1 and is exactly
+
+    N_min(t) = 2 floor(1/(2-2^t))+1.                       (2)
+
+It is attained by a=floor(1/(2-2^t))+1 and b=a-1. The strict inequality
+matters when the reciprocal is an integer. A tie at a smaller a is not a
+strict trap. This is a minimum only within the specified three-vertex,
+two-boundary, positive-parallel-multiplicity class. It is not a minimum
+over arbitrary frame graphs or physical scalar programs.
+
+## An exact 481-edge example
+
+At t=997/1000, the following strict integer inequalities hold:
+
+    2^997 * 240^1000 > 479^1000,
+    2^997 * 241^1000 < 481^1000.
+
+Taking positive thousandth roots gives
+
+    479/240 < h < 481/241.
+
+It follows that 240 < 1/(2-h) < 241. Formula (2) gives N_min=481,
+attained by a=241 and b=240. Its profiles are
+
+    initial V:  241 rank-two edges, 240 rank-zero edges;
+    any line:   481 rank-one edges;
+    final 0:    240 rank-two edges, 241 rank-zero edges.
+
+For every 0<t<=997/1000 the same graph remains a strict trap: h decreases,
+so 481>241h persists, while 241h>240h. The 481-edge minimality is asserted
+only at t=997/1000. At the linear tariff t=1 there is no trap in this
+class: a+b>2a would require b>a, contradicting the cheaper-zero condition.
+
+The pinned selected complex supplier uses C=10940329/3500000000, so its
+power exponent t=1-C lies in this interval. This arithmetic comparison
+only locates the abstract example in a relevant power range. It does not
+embed these parallel edges in the selected supplier, transfer its caller
+contract, change its signed invoice or establish a kappa gain.
+
+## What changes for the next search
+
+The binary optimum for one projection can be exact and still provide no
+certificate of a joint optimum. To escape this example, a search must
+allow a simultaneous corank-two image or temporarily accept a worse
+intermediate frame. A richer move must still retain fixed observations,
+productive targets, dirty restoration and every physical cost. No such
+supplier implementation is established here.

research/projection-local-trap/README.md

@@ -0,0 +1,134 @@
+# Exact projection cuts can stop at a strict local minimum
+
+Scoped proof with exact finite corroboration. For every field K and every
+power tariff f(r)=r^t, 0<t<1, a legal three-vertex frame graph can be a
+strict local minimum for every rank-one projection move while two commuting
+projections lower its complete paid objective. The exact minimum number of
+parallel edges in the stated two-boundary class is
+
+    2 floor(1/(2-2^t))+1.
+
+At t=997/1000 this minimum is 481. Fix boundary frames 0 and K^2, give one
+free frame S 241 incoming and 240 outgoing edges, and charge every edge:
+
+| Free frame | Complete paid objective |
+|---|---|
+| Initial K^2 | 241 * 2^t |
+| Any line, after one projection | 481, strictly larger |
+| Zero, after two complementary projections | 240 * 2^t, strictly smaller |
+
+The same graph is a strict trap for 0<t<=997/1000. Its minimality is claimed
+only at t=997/1000. [PROOF.md](PROOF.md) proves the all-field, all-power
+construction and sharp threshold. Two exact integer inequalities certify
+the numerical example without floating point or an exponential oracle.
+
+## Why this matters
+
+David Ganz / Dugongue's [PR556](https://github.com/CrocSwap/integer-mult-bounds/pull/556)
+optimizes every legal binary choice for one rank-one projection by a
+minimum cut. This example shows that even an exhaustive collection of
+those exact moves does not certify a joint optimum. A search needs richer
+simultaneous moves or permission to cross an intermediate increase.
+The predecessor theorem and implementation are cited, not reverified.
+
+This is an abstract frame-search obstruction. It supplies no scalar word,
+productive target map, arbitrary-dirt physical implementation, phases,
+restoration, owner/stock/precision/tape costs, complete signed caller bill
+or uniform compiler. No new kappa or multiplication theorem is claimed.
+The five selected framework assumptions remain. The selected source pin
+places its complex exponent inside the example's interval; no embedding
+in that supplier or gain in its actual invoice follows.
+The free vertex has 481 incident edges. It is not identified with an
+ordinary bounded-arity scalar instruction.
+
+The complex-rank-shape-decoder card is explicitly changed to this side
+question. The source-bound baseline passed. No selected scientific replay,
+Lean or Docker run was performed.
+
+## 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/projection-local-trap/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/projection-local-trap/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/projection-local-trap
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/projection-local-trap --check-source-history
+```
+
+A reviewer may substitute a local CPython 3.12 path. The direct checker
+writes nothing, recomputes the receipt, and requires exact agreement with
+[RESULT.json](RESULT.json), including SHA256 of the six scientific and
+metadata files. `--generate` emits a fresh computed receipt to stdout.
+This is not a formal proof-kernel certificate.
+
+Finite corroboration covers every positive a,b<=40 for every distinct
+rational h=1+n/d, 1<=n<d<=32, plus every pair below each predicted minimum.
+The checker enumerates all 2-by-2 matrices over F2,F3,F5,F7,F11, filters
+rank-one idempotents, checks every ordered pair of them, and literally
+retains all 481 edges for every subspace. The universal statement rests on
+the written proof, not these finite domains. Exact power comparisons also
+exclude every smaller incoming multiplicity at t=997/1000.
+
+The generated receipt records 323 rational tariffs and 516800 multiplicity
+pairs, with 125663 strict traps and 614 ties having a cheaper zero frame.
+It also checks 28047 pairs below the predicted graph minima, 17764 field
+matrices, 236 projectors, 21640 ordered projector pairs and 236 joint
+escapes. All 43 subspaces retain 20683 literal edge occurrences in total.
+The exact-power check rejects 28680 pairs with a<241. Fifteen named controls
+cover tariff and multiplicity domains, strict boundaries, non-idempotent
+maps, a noncomplementary pair, invalid powers and altered receipts.
+
+## Verification design
+
+All loops have fixed finite bounds. The largest matrix inventory is
+11^4=14641, with 132 retained projectors; the scalar grid stores only its
+tariffs and running counts. No recursion, subprocess, dynamic import,
+network, predecessor execution or filesystem write is used. Functions
+remain below 60 physical lines. Invariants and rejection controls remain
+active under optimized Python.
+
+Power-of-ten rule 3 deviation: CPython and Fraction allocate dynamically.
+The scope is this terminating checker. Fixed field/grid bounds, at most
+121 vectors and 132 projectors per field, and at most 1000 in power
+denominators bound retained data and integer sizes. Normal and optimized
+replays exercise these maxima. A runtime with static allocation would be
+needed for literal allocation-free compliance. No shared runtime is changed.
+Warning-strict replay is the available interpreted-language diagnostic;
+no additional static analyzer is required by this isolated package.
+
+## Open next questions
+
+1. Can a legal selected scalar-word neighborhood realize this coordinated
+   projection advantage after every productive target and restoration fee?
+   Start with one actual frame neighborhood, retain its fixed observations,
+   and produce both complete signed invoices. The present abstract graph
+   does not supply independent physical data paths.
+2. Can a two-projection move be optimized with an exact certificate on a
+   useful restricted class of frame graphs? Start with two specified
+   commuting projections and four image choices per event. Their mixed
+   inclusion rules and full paid/target objective remain to be derived.
+
+## Credit and overlap
+
+This contribution was produced by Nick Petalas. David Ganz / Dugongue
+retains the binary projection-cut theorem, frame-graph contract and search
+implementation in PR556. That theorem credits standard graph-cut methods
+to Picard and Kolmogorov/Zabih; rank-nullity and concavity are standard.
+The new contribution is the all-field strict trap, sharp multiplicity
+formula and exact 481-edge witness in this specific frame-search model.
+No general literature-priority claim is made for local-search traps.
+
+Base: a5bff3bf133e482541c09eba4e773884bdb2b1b7, priority revision 8.
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19272058)
+and local reservation identify this question. Live PR/discussion searches,
+merged README/formula searches and recent account contributions found no
+matching result. The overlap helper reported 310 open PRs and 5900
+discussion records, but only 92 of 8623 local notes were materialized;
+separate Git searches covered main READMEs. This is bounded coverage, not
+proof of novelty. PR5428's superoptimizer proposal is related motivation;
+it supplies no strict-trap threshold. PR563 uses contextual provider
+selection and cites PR556; it computes a different construction.
+
+Independent human and formal proof-kernel review are unclaimed. New files
+are Apache-2.0. Predecessor source bytes and credit are unchanged.

research/projection-local-trap/RESULT.json

@@ -0,0 +1,92 @@
+{
+  "claim_type": "scoped proof with exact finite corroboration",
+  "controls": [
+    "invalid tariff 1",
+    "invalid tariff 2",
+    "invalid tariff 0",
+    "invalid tariff 3",
+    "invalid multiplicity (0, 1)",
+    "invalid multiplicity (1, 0)",
+    "invalid multiplicity (1001, 1)",
+    "invalid multiplicity (True, 1)",
+    "non-strict boundary",
+    "integer reciprocal boundary",
+    "non-idempotent rank-one map",
+    "noncomplementary pair",
+    "invalid power",
+    "changed receipt count",
+    "changed receipt hash"
+  ],
+  "fields": [
+    {
+      "frames": 5,
+      "joint_escapes": 6,
+      "literal_edges": 2405,
+      "matrices": 16,
+      "p": 2,
+      "pairs": 36,
+      "projectors": 6
+    },
+    {
+      "frames": 6,
+      "joint_escapes": 12,
+      "literal_edges": 2886,
+      "matrices": 81,
+      "p": 3,
+      "pairs": 144,
+      "projectors": 12
+    },
+    {
+      "frames": 8,
+      "joint_escapes": 30,
+      "literal_edges": 3848,
+      "matrices": 625,
+      "p": 5,
+      "pairs": 900,
+      "projectors": 30
+    },
+    {
+      "frames": 10,
+      "joint_escapes": 56,
+      "literal_edges": 4810,
+      "matrices": 2401,
+      "p": 7,
+      "pairs": 3136,
+      "projectors": 56
+    },
+    {
+      "frames": 14,
+      "joint_escapes": 132,
+      "literal_edges": 6734,
+      "matrices": 14641,
+      "p": 11,
+      "pairs": 17424,
+      "projectors": 132
+    }
+  ],
+  "new_kappa": false,
+  "power": {
+    "a": 241,
+    "b": 240,
+    "current_complex_C_provenance": "10940329/3500000000",
+    "exponent": "997/1000",
+    "minimum_edges": 481,
+    "smaller_a_pairs": 28680
+  },
+  "scalar_grid": {
+    "pairs": 516800,
+    "smaller_graph_pairs": 28047,
+    "strict_traps": 125663,
+    "tariffs": 323,
+    "ties_with_cheaper_zero": 614
+  },
+  "sha256": {
+    "PROOF.md": "3df62146f0aafe401cee058f0d209e7972527877c5b857ea1cbdd16d67e93a58",
+    "README.md": "8484ea6e0ad5738c1434368307d939e44c8be695e3d62c4c93de2e500c5b8b1e",
+    "SOURCES.json": "c2a143f19cd065260f2a04cfeb91ba76046cdc08bed8ca925c3e85a4d03290da",
+    "TASK.json": "0f660ce835f7b0d28604d6fa6d37cd8eaa9d61a59f4dcab068651daad48d40b6",
+    "VERIFY.json": "1135b880c0d4e13afe920c56b9b8a07454c25f1a50e38b50e7a5f3dbc5602e33",
+    "verify.py": "760cdc92242d30fe6d13598c7e09569761e7856fd26dad98991846b9cbfdedab"
+  },
+  "status": "PASS_PROJECTION_LOCAL_TRAP"
+}

research/projection-local-trap/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7",
+  "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/projection-cut-toolkit/PROJECTION-CUT-THEOREM.md",
+      "usage": "provenance",
+      "git_blob": "2e1e3d129399026a804ddf23c0ec7fc48a99d939",
+      "sha256": "bf647c60a16d8331368f2839224d8036ddc052ea19d4ce35cac9656702c48eab"
+    }
+  ]
+}