Prove sharp signed tensor gap with variable target boundaries (no new κ)

research/signed-triangle-tensor-gap/PROOF.md

@@ -0,0 +1,154 @@
+# Exact signed subspace triangle
+
+This is a scoped theorem in a rank-distance relaxation. It does not assert
+that the graph below is the contact graph of a legal scalar word. In
+particular, its three negative edges are variable productive credits, not
+three already implemented independent recursive targets.
+
+## Contract
+
+Let K be any field, let H=K^m with m a positive integer, and let S1,S2,S3
+be arbitrary subspaces. Write
+
+```math
+d(A,B)=\dim A+\dim B-2\dim(A\cap B).
+```
+
+There are four vertices, 0,S1,S2,S3. Three positive edges join 0 to Si;
+three negative edges join every pair Si,Sj. For 0<t<=1 define
+
+```math
+J_t(S_1,S_2,S_3)
+=\sum_i (\dim S_i)^t-\sum_{i<j} d(S_i,S_j)^t,
+\qquad 0^t=0.
+```
+
+This uses the canonical subspace charts and Fourier-rank convention of
+Ali Romman's [PR6171](https://github.com/CrocSwap/integer-mult-bounds/pull/6171),
+at `343232cdf5273d1f77569de390f0977b46916644`, sections 1 and 2.
+The distance identification is inherited, not a new native-operator lemma.
+The normalization at m copies is J_t/m^t. All six graph terms are included;
+physical realization costs have not been supplied by this relaxation.
+
+## Linear optimum and every equality case
+
+For every field and m>=1,
+
+```math
+\min J_1=-\lfloor3m/2\rfloor.
+```
+
+The minimizers are exactly the pairwise-disjoint triples with dimensions
+(k,k,k) for m=2k, and a permutation of (k,k,k+1) for m=2k+1.
+Pairwise-disjoint means each pair intersects only at zero. The sum of all
+three spaces need not be direct.
+
+Put x_i=dim Si, D=x1+x2+x3, and
+I=sum_(i<j) dim(Si intersect Sj), a nonnegative integer. Directly,
+
+```math
+J_1=-D+2I.
+```
+
+Each pair has sum dimension at most m. Summing those three inequalities,
+
+```math
+2D-I\leq3m,
+\qquad D-2I\leq\frac{3m}{2}-\frac{3I}{2}.
+```
+
+The integral left side is at most floor(3m/2). This proves the lower bound.
+If I>=1, the right side is at most 3m/2-3/2, strictly smaller than
+floor(3m/2). Thus equality forces I=0 and D=floor(3m/2).
+Now xi+xj<=m implies each xi>=D-m. For m=2k this forces all three
+dimensions to be k. For m=2k+1 it forces all three to be at least k and
+their sum to be 3k+1, hence the claimed permutation. Conversely those
+dimensions and zero pairwise intersections give equality in J1.
+
+For attainment, split H=U plus W with dimensions k and m-k. Choose an
+injective linear map f:U->W. Set S1=U, S2=W, and S3=graph(f).
+The three intersections are zero, and their dimensions are k,m-k,k.
+This works over every field, including characteristic two and k=0.
+
+Consequently the normalized linear optimum is
+-floor(3m/2)/m. It is -1 at one copy, -3/2 at every positive even width,
+and -3/2+1/(2m) at odd width. The advantage is established in the signed
+graph model; a supplier or exponent improvement does not follow.
+
+## Exact two-copy power optimum
+
+For m=2 let a=2^t, so 1<a<=2. Every nonzero proper subspace is a line.
+Two distinct lines have distance two; a line and the full plane have
+distance one. The following table exhausts unordered triples. A repeated
+letter means the same subspace; L,M,N are distinct lines, and H is the
+full plane.
+
+| Triple | J_t |
+|---|---:|
+| 0,0,0 | 0 |
+| 0,0,L | -1 |
+| 0,0,H | -a |
+| 0,L,L | 0 |
+| 0,L,M | -a |
+| 0,L,H | -1 |
+| 0,H,H | 0 |
+| L,L,L | 3 |
+| L,L,M | 3-2a |
+| L,M,N | 3-3a |
+| L,L,H | a |
+| L,M,H | 0 |
+| L,H,H | 2a-1 |
+| H,H,H | 3a |
+
+Every field has at least three lines in K^2, so all rows exist. Comparing
+these affine functions on 1<a<=2 gives
+
+```math
+\min J_t=\min(-a,3-3a),
+\qquad \min J_t/2^t=\min(-1,3/2^t-3).
+```
+
+At one copy the only spaces are zero and K. If exactly h of the three
+spaces are K, the signed cost is h-h(3-h)=h(h-2), independent of t.
+Its minimum is -1. Thus two copies beat the best one-copy assignment
+exactly when 2^t>3/2, equivalently t>log_2(3/2). Equality holds at the
+threshold. The threshold lies below 3/4 because 2^3>(3/2)^4.
+
+## What changes relative to fixed-boundary reduction
+
+PR6171 fixes each productive endpoint to a repeated space U^m. Here all
+three productive pairs vary. At m=2, the attaining linear triple consists
+of the three distinct lines of F2^2. No line is a repeated scalar boundary:
+the repeated one-dimensional scalar choices are only zero and F2^2.
+The coupled triple has three full-distance productive pairs. A one-copy
+assignment has at most two nonzero pair distances. Their negative credits
+therefore cannot be held constant during the common-copy choice.
+
+This gives an exact optimality gap and threshold, beyond the predecessor's
+arithmetic control that negative terms can reverse an averaging inequality.
+It neither contradicts that theorem nor extends the graph into a physical
+construction. In particular, pairwise graph edges do not establish three
+independent targets on arbitrary dirty inputs. Producing such a caller,
+or proving that its legal graph constraints forbid this configuration,
+is a separate question.
+
+## Verification boundary
+
+The written dimension argument and exhaustive two-dimensional table give
+the all-field statements. The checker enumerates actual small subspaces,
+checks every ordered triple, and compares all equality cases. Its binary
+RREF inventory is independently checked by closure under adjoining vectors.
+It also constructs the attaining binary triples at widths 1 through 64.
+These are finite corroboration, not a proof-kernel formalization.
+
+The code uses finite, explicit bounds. Its managed-runtime allocations
+are a Power of Ten deviation: finite calibration sizes bound the lists,
+tables and loops. No recursion, external solver, network access, imported
+predecessor executable or persistent mutable state is needed.
+
+This proof and verifier were produced by Nick Petalas. Standard dimension
+identities, graph subspaces and affine-envelope comparisons are background;
+no literature-priority claim is made. PR6171 retains its tensor-reduction
+credit; Cinna Davis retains the projection inequality, icekylinx retains
+the canonical subspace-frame construction, and all retained P104/native/
+helper/caller/compiler contributors retain their predecessor credit.

research/signed-triangle-tensor-gap/README.md

@@ -0,0 +1,90 @@
+# Sharp tensor gap with variable productive boundaries
+
+This scoped proof determines a signed subspace-distance invoice over every
+field. Three variable spaces each pay their distance from zero and receive
+credit for their three pairwise distances. The exact linear optimum in
+ambient dimension m is `-floor(3m/2)`. Every minimizer is classified.
+
+At two copies the normalized power-tariff optimum is
+`min(-1, 3/2^t - 3)`, for `0<t<=1`; the one-copy optimum is `-1`.
+Coupling therefore helps exactly when `2^t > 3/2`. At the linear tariff,
+the normalized optimum drops from `-1` to `-3/2`.
+
+This is an exact gap in an abstract signed graph, with finite corroboration.
+It supplies neither a physical scalar word nor a new kappa. In particular,
+the three graph credits are not claimed to be independently delivered
+recursive targets on arbitrary dirty inputs.
+
+## Proof and context
+
+[PROOF.md](PROOF.md) gives the dimension bound, attainment, all equality
+cases and the exhaustive two-dimensional affine table. This extends the
+variable-boundary question left open by Ali Romman's
+[PR6171](https://github.com/CrocSwap/integer-mult-bounds/pull/6171), at
+`343232cdf5273d1f77569de390f0977b46916644`. That result fixes every productive
+boundary to a repeated space. This package makes those boundaries variable
+and proves an exact optimum, beyond its arithmetic warning about negative
+credits. It does not audit or contradict the fixed-boundary theorem.
+
+Base main is `3f0152a32eeebac0df11946dbd50cabe5a7f7839`, priority revision 8.
+The selected `0.003125804` frontier is unchanged. The card's first selected
+source-binding control passed; no predecessor scientific replay was run.
+The source PR is cited as conceptual context. No pending executable or Git
+object is needed for the proof or replay.
+
+## Reproduce
+
+From the repository root, with CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -B research/signed-triangle-tensor-gap/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -O -B research/signed-triangle-tensor-gap/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/signed-triangle-tensor-gap
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/signed-triangle-tensor-gap --check-source-history
+```
+
+A clean `python3.12` executable can replace the local interpreter path.
+The direct marker is `PASS_SIGNED_TRIANGLE_TENSOR_GAP`.
+[RESULT.json](RESULT.json) records every finite domain, minimizer count and
+ordered trace digest, and binds all six source files by SHA256. Replays are
+read-only. To regenerate a receipt, supply `--output /absolute/scratch/result.json`
+with a new output filename, then compare it with the committed receipt.
+
+The verifier enumerates all ordered triples over F2 in dimensions 0 through
+4 and over F3 and F5 in dimension 2. A separate closure inventory checks the
+binary RREF enumeration. It checks the attaining construction at widths
+1 through 64 and the nine affine costs at all three relevant envelope
+endpoints. Missing/spurious table rows, intersecting-plane equality and the
+strict threshold have explicit controls. The written proof supplies the
+unbounded all-field claim; the finite checks do not replace it.
+
+## Limitations
+
+The domain consists of canonical subspace charts. General Lagrangian charts,
+a prescribed scalar contact graph and actual native phases are outside it.
+A legal dirty-input circuit, independence of physical targets, restoration,
+owned storage, movement, adapters, precision, compiler closure, BIT and outer
+admission remain open and unpriced. No selected cold replay, Lean or Docker
+run is needed for this scoped theorem. Independent human and formal
+proof-kernel review are unclaimed.
+
+## Open next questions
+
+- Can a legal arbitrary-dirty-input scalar circuit realize this signed graph,
+  or is there a contact/path invariant that excludes it? First assign the
+  three productive pairs to distinct logical lifetimes and account for every
+  paid transition. Independent target delivery and restoration are blockers.
+- What is the all-width optimum for `0<t<1`? Start with the signed distance
+  objective itself, allowing unequal dimensions and nonzero intersections.
+  The linear dimension bound and the two-copy table do not settle that domain.
+  Such a relaxation result would still need a complete physical invoice.
+
+## Credit
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+Ali Romman retains PR6171's graph model, normalization and fixed-boundary
+reduction. Cinna Davis retains the projection inequality, icekylinx retains
+the canonical subspace-frame construction, and the P104/native/helper/caller/
+compiler contributors retain their predecessor credit. Standard dimension,
+graph-subspace and affine-envelope facts are background. No predecessor
+code is copied and no literature-priority claim is made.

research/signed-triangle-tensor-gap/RESULT.json

@@ -0,0 +1,89 @@
+{
+  "binary_constructions": 64,
+  "cases": [
+    {
+      "dimension": 0,
+      "linear_minimum": 0,
+      "minimizers": 1,
+      "ordered_triples": 1,
+      "prime": 2,
+      "spaces": 1,
+      "trace_sha256": "f140c0d7b2f22c9df53573612688f73d31488faf0c5708a82fa5b3ee1773bc02"
+    },
+    {
+      "dimension": 1,
+      "linear_minimum": -1,
+      "minimizers": 3,
+      "ordered_triples": 8,
+      "prime": 2,
+      "spaces": 2,
+      "trace_sha256": "d1177d807d1e40f2b513d48d9662aa4899215118c9ab1e912bccbbeeff5dcac8"
+    },
+    {
+      "dimension": 2,
+      "linear_minimum": -3,
+      "minimizers": 6,
+      "ordered_triples": 125,
+      "prime": 2,
+      "spaces": 5,
+      "trace_sha256": "41d50aad30aa3d2a4cbb8eb48164df1ca558b19c2f484efa30ab4d2556503318"
+    },
+    {
+      "dimension": 3,
+      "linear_minimum": -4,
+      "minimizers": 252,
+      "ordered_triples": 4096,
+      "prime": 2,
+      "spaces": 16,
+      "trace_sha256": "0a3fe03f16566df2225ca2ebfc65d4a1df6b3d026daed41a9232a2da50d6d5ab"
+    },
+    {
+      "dimension": 4,
+      "linear_minimum": -6,
+      "minimizers": 3360,
+      "ordered_triples": 300763,
+      "prime": 2,
+      "spaces": 67,
+      "trace_sha256": "d869de5d54dba1d9fc333afd1924443049c0dd627a1c71c1dde97924514b658c"
+    },
+    {
+      "dimension": 2,
+      "linear_minimum": -3,
+      "minimizers": 24,
+      "ordered_triples": 216,
+      "prime": 3,
+      "spaces": 6,
+      "trace_sha256": "01b479d4f51ec5569d403728ee3129933648c527143844cf4b119fd6ede25530"
+    },
+    {
+      "dimension": 2,
+      "linear_minimum": -3,
+      "minimizers": 120,
+      "ordered_triples": 512,
+      "prime": 5,
+      "spaces": 8,
+      "trace_sha256": "3ce9b96120352e1d1b617118062191939617ee1bcf1275cf4206da488010ccd5"
+    }
+  ],
+  "claim_type": "scoped proof with finite corroboration",
+  "controls": [
+    "omitted_table_row",
+    "spurious_table_row",
+    "distinct_is_not_disjoint",
+    "strict_threshold"
+  ],
+  "kappa_improvement": false,
+  "linear_optimum": "-floor(3m/2)",
+  "ordered_triples": 305721,
+  "power_endpoint_checks": 27,
+  "schema_version": 1,
+  "source_sha256": {
+    "PROOF.md": "9b1db9a18553e526f78a56b88f78cdbffce6c0e6fed55834780b164d37158e71",
+    "README.md": "0327e3f077638714181c96923cfba8a7fcc89082f2b4c59cc4933092389b5e7e",
+    "SOURCES.json": "8a73be5ac120fd4b2086d12242428e4522dd39e7a4b481d10fa26198887fc169",
+    "TASK.json": "1cdeafe3fd9711ff5c968d3fa34bfec1d1daefc6397f510e4afee80413fdf5b1",
+    "VERIFY.json": "5a8f9be44c2eeee382471e5675d5bdd32cdab9816d7f964333a9ea6b1f38ef98",
+    "verify.py": "51d8420fc4d04d3f527d649386d664058df8e8030655a2ce7c4fe88cfa74f4bd"
+  },
+  "two_copy_normalized_power_optimum": "min(-1,3/2^t-3), 0<t<=1"
+}

research/signed-triangle-tensor-gap/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "3f0152a32eeebac0df11946dbd50cabe5a7f7839",
+  "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"
+    }
+  ]
+}