Prove exact joint Gaussian transition cost with dirty workspace (no new κ)

research/joint-gaussian-transition-floor/PROOF.md

@@ -0,0 +1,147 @@
+# Exact joint transition cost
+
+This proof was produced by Nick Petalas. Apache-2.0.
+
+## Contract and theorem
+
+Take any finite number h of independent complex helpers. Write helper j as
+two real coordinates and prescribe multiplication by
+
+`g_j = 2^(a_j) (1 + epsilon_j i)^(b_j)`,
+
+where a_j is any integer, b_j belongs to {0,1}, and epsilon_j belongs to
+{-1,1}. The complete required real map is block diagonal, with blocks
+
+`T_j = 2^a [[1, -epsilon*b], [epsilon*b, 1]]`.
+
+Any finite number of extra real registers may contain arbitrary independent
+dirty inputs. They must return exactly unchanged, without leaking into or
+receiving data from the helpers at exit. Thus the complete endpoint is
+`T = diag(T_1,...,T_h,I_dirty)` on every real input.
+
+The charged elementary operations are signed unit ADDs `x_r += +/- x_s`
+with r != s, and individual doublings or halvings. Each costs one. Coordinate
+permutations and negations are granted free. Every operation may connect any
+two registers, including workspace. No other scalar coefficients, constants,
+COPY, clear, nonlinear operation, or larger native map is free.
+
+Every implementing word needs at least
+
+`S = sum_j |2a_j+b_j|` doublings/halvings, and
+`A = 2 sum_j b_j` signed ADDs.
+
+One explicit word attains both bounds simultaneously. Consequently its exact
+minimum total charge is `S+A`, even with arbitrary cross-helper mixing and
+any finite restored dirty workspace. The inverse endpoint has exactly the
+same two minima.
+
+This answers the pure joint-transition question of Sagar Thakrar's PR1566.
+It does not price a transition fused with a different surrounding operation.
+
+## A lattice-index distance counts scales
+
+For two full rational lattices L,M in Q^n, define
+
+`d(L,M) = log_2([L:L intersect M] [M:L intersect M])`.
+
+All these indices are finite. Applying the same invertible rational map to
+both lattices preserves them. Also d satisfies the triangle inequality.
+Indeed, for a third lattice N,
+
+`[L:L intersect N] <= [L:L intersect M] [M:M intersect N]`.
+
+To see this, insert the smaller subgroup L intersect M intersect N, split
+its index at L intersect M, and inject the latter quotient into
+M/(M intersect N). Apply the same inequality with L and N exchanged and
+multiply the two bounds. Taking logarithms proves the triangle inequality.
+This is a standard lattice-index argument, not a claimed new metric.
+
+Let Z denote Z^n and let P be the current rational matrix. A next gate G
+satisfies
+
+`d(GPZ,Z) <= d(GPZ,GZ) + d(GZ,Z) = d(PZ,Z) + d(GZ,Z)`.
+
+A signed ADD, permutation or negation maps Z onto itself and has last term
+zero. A single doubling or halving has last term one. Starting from P=I
+therefore gives
+
+`number of scales >= d(TZ,Z)`.
+
+This uses a distance between lattices, rather than the absolute valuation of
+the determinant. Opposite expansions and contractions cannot cancel it.
+
+For b=0, the two-coordinate block lattice is 2^a Z^2. Its distance from
+Z^2 is 2|a|. For b=1 put
+
+`B_epsilon = [[1,-epsilon],[epsilon,1]]`,
+`B_epsilon^-1 = (1/2) [[1,epsilon],[-epsilon,1]]`.
+
+If a >= 0, `2^a B_epsilon Z^2` lies inside Z^2 with index
+`2^(2a+1)`. If a <= -1, its inverse matrix is integral, so the block lattice
+contains Z^2, with index in the opposite direction `2^(-2a-1)`.
+In either case the distance is |2a+1|. Intersections of direct-product
+lattices are direct products and their indices multiply. Restored dirty
+registers contribute zero. Hence `d(TZ,Z)=S` as asserted.
+
+## Row support counts ADDs
+
+Call a row mixed when it has at least two nonzero entries. The initial
+identity has no mixed rows. A doubling, halving, negation or coordinate
+permutation preserves the number of mixed rows. A signed ADD changes only
+one row and can increase that number by at most one. At the required
+endpoint exactly the two rows of each b=1 block are mixed; the other helper
+and dirty rows each have support one. Thus every word needs at least A ADDs.
+
+This argument remains valid when temporary rows have large support, when
+mixing is undone, and when arbitrary dirty registers are used. The scale
+and ADD arguments apply to disjoint charged gate types, so their bounds add.
+
+## Simultaneous attainment
+
+For b=0, scale both coordinates by 2^a, using 2|a| individual scales.
+For b=1 and a >= 0, the three operations
+
+```text
+x -= epsilon*y
+y *= 2
+y += epsilon*x
+```
+
+produce `(x-epsilon*y, epsilon*x+y)`. Scale both outputs by 2^a.
+There are two ADDs and 2a+1 scales.
+
+For b=1 and a <= -1, instead use
+
+```text
+x -= epsilon*y
+x /= 2
+y += epsilon*x
+```
+
+This produces half of that same block. Scale both outputs by 2^(a+1).
+There are two ADDs and -2a-1 scales. Execute these words independently on
+all helpers and leave all workspace unchanged. They attain S and A.
+
+The inverse of a b=0 block replaces a by -a. The inverse of a b=1 block
+replaces `(a,epsilon)` by `(-a-1,-epsilon)`. This stays in the stated
+family and preserves |2a+b| and b, proving the inverse claim.
+
+## The requested reciprocal boundary
+
+For `(g_1,g_2) = (1+i, (1+i)^-1)`, the parameters are
+`(a,b,epsilon)=(0,1,1),(-1,1,-1)`. Thus S=2, A=4 and the exact cost is
+six. The determinant of the combined four-coordinate map is one, so its
+determinant valuation alone gives zero. The lattice distance is two.
+Arbitrary dirty workspace cannot lower six; a separately required return
+costs six more. This is a boundary cost, not a lower bound on a fused round
+trip whose only required endpoint is the identity.
+
+## Scope of the conclusion
+
+The quantified result is this written proof; finite software checks are
+corroboration. General unit phases beyond the stated conjugate family,
+nonunit odd coefficients, singular clean workspace, COPY/clear, alternative
+native primitives and endpoints fused with an original SCALE or ADD require
+separate analysis. Physical routing, precision, coefficient production,
+compiler admission, productive targets and recursive costs are not supplied.
+No new kappa or complete multiplication theorem is claimed.

research/joint-gaussian-transition-floor/README.md

@@ -0,0 +1,140 @@
+# Joint Gaussian transitions cannot cancel their scale charges
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+For any finite set of complex helpers, prescribe multiplication of helper j
+by `2^(a_j) (1+epsilon_j*i)^(b_j)`, where a_j is an integer, b_j is zero or
+one, and epsilon_j is either sign. Permit arbitrary signed unit ADDs between
+any real coordinates, doublings and halvings, with free permutations and
+negations and any finite amount of restored dirty workspace. The exact
+minimum is
+
+```text
+doublings/halvings = sum_j |2a_j+b_j|
+signed ADDs        = 2 sum_j b_j
+total             = their sum
+```
+
+Both lower bounds are attained by the same word, and apply separately to
+its inverse. This is a **scoped proof with exact finite corroboration**.
+It answers Open next question 2 of Sagar Thakrar's
+[PR #1566](https://github.com/CrocSwap/integer-mult-bounds/pull/1566), which
+leaves joint Gaussian transitions outside its separate-transition theorem.
+The new result is the joint lower bound; the standalone transition words and
+Gaussian-gauge setting retain their predecessor credit.
+
+In particular, the requested reciprocal pair `(1+i), (1+i)^-1` costs exactly
+six primitives, comprising four ADDs and two scales. Its determinant is one.
+Using only the total determinant valuation would miss both necessary scales.
+The same endpoint cost applies to the return; a round trip with no required
+intermediate boundary can of course be the empty word.
+
+## Proof and finite evidence
+
+[PROOF.md](PROOF.md) uses the classical index distance between rational
+lattices. A signed ADD preserves the integer lattice; a scale changes the
+distance by at most one. The final block-product distance adds the absolute
+block valuations, including opposite signs. Separately, each odd Gaussian
+block needs two mixed rows and every ADD can create at most one. Explicit
+three-operation words plus scalar powers attain both bounds. The proof
+covers all integer exponents, helper counts and finite restored dirty
+workspace. It does not depend on a finite search or a predecessor replay.
+
+The standalone verifier checks exact rational matrices, all-input inverse
+restoration and literal primitive counts. A separate finite quotient enumerates
+the lattice intersections directly. Short arbitrary words test both invariants
+on endpoints outside the target family. Controls remove a scale or ADD,
+change the conjugate, leave workspace unrestored, or violate the input domain.
+The fixed run checks 1,011 attaining endpoints, 42 finite lattices, 216 lattice
+triangles, all 4,681 short words and 14 rejecting controls. The largest
+checked attaining word has eighteen gates. Counts come from enumeration;
+the universal theorem comes from the written proof.
+[RESULT.json](RESULT.json) is generated by the verifier and binds every other
+package file by SHA256; default replay compares the entire generated result.
+
+## Reproduction
+
+From the repository root, CPython 3.12 and its standard library suffice:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/joint-gaussian-transition-floor/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/joint-gaussian-transition-floor/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/joint-gaussian-transition-floor
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/joint-gaussian-transition-floor --check-source-history
+```
+
+Other machines may substitute their CPython 3.12 interpreter. Expected marker
+is `PASS_JOINT_GAUSSIAN_TRANSITION_FLOOR no_new_kappa`. Both normal and
+optimized checks are registered with a 120-second timeout. To regenerate
+the receipt without changing package files, add `--emit-result` and redirect
+stdout to an external file. No Git, network, solver or imported predecessor
+code is needed by the scientific verifier. SOURCES.json pins the predecessor
+README, catalogue and selected record as historical provenance at canonical
+main `19fdb086ea96af9a9f87936a2b888e10af4ed810`; there are no live inputs.
+
+## Scope and implementation limits
+
+The `complex-new-helper-inventory` card is explicitly changed to this scalar
+compiler side question. The selected baseline binding control passed; this
+was orientation, not a scientific selected replay. Pure joint transitions
+cannot evade the stated charge through cross-helper determinant cancellation.
+The result stops here; it does not justify more gauge searches in this class.
+
+General phases outside the conjugate family, nonunit odd coefficients,
+clean initialized workspace with singular operations, COPY/clear and fused
+non-block-diagonal endpoints are outside scope. So are rounding, routing,
+coefficient production, physical ownership, native admission, full-word
+scalar optimization, complete paid profiles, compiler/stock/outer premises
+and a complete multiplication theorem. No new kappa or selected-frontier
+change is claimed. Independent human and formal proof-kernel review are
+unclaimed. No Lean, Docker or selected cold replay was run.
+
+The finite checker allows at most four helpers, four extra real coordinates,
+dimension twelve and even-block exponents from -8 through 8. Odd-block
+exponents run from -8 through 7, a domain closed under inversion. Stored words
+are capped at 256 gates; the fixed tests use a smaller domain. The lattice
+enumerator uses at most 4^4 residue points, and the short-word census uses
+eight gates through length four. There is no recursion, subprocess, network,
+dynamic code evaluation or shared mutable output. Functions fit in 60 lines.
+Input receipts and each source file are capped at one MiB.
+
+Power of Ten rule 3 has a managed-runtime deviation in verify.py. Python
+allocates exact integers, fractions, lists and sets during this offline
+finite check. The preceding enforced bounds cap all live data; only one
+case or short word is processed at a time. Warning-strict normal and
+optimized replays check the same bounded path. A fixed-buffer implementation
+would be required if allocation guarantees become a caller requirement.
+Rule 9 has the corresponding standard-library arithmetic-dispatch deviation,
+limited to integers and Fractions with visible direct calls. No separate
+static type checker or linter is a dependency; warning-strict execution is
+registered in CI. No shared build settings are changed.
+
+Local execution used CPython 3.12.15 on macOS 27.0.1 arm64. Hosted replay
+and source-history availability are separate publication checks.
+
+## Open next questions
+
+Can a transition fused with an actual signed SCALE or ADD beat the complete
+corresponding real-gauge invoice? This would change the pure block-diagonal
+endpoint, which is the boundary of this proof. Start with one literal
+surrounding operation, its complete dirty-input map and an attaining word.
+A source-bound fused endpoint and complete caller invoice remain missing.
+The same question and blockers are recorded in TASK.json.
+
+## Credit and coordination
+
+Sagar Thakrar / thakrarsagar supplies PR1566's temporal-gauge setting,
+standalone bounds and explicit joint-transition question. Hanson Sun /
+bbMisk's PR1490 supplies the static Gaussian common-rounding argument and
+unit classification. PR1259/1380 and the scalar PR696 lowerer retain their
+temporal and coefficient lineage. The lattice-index argument, row-support
+count and elementary butterfly identities are classical methods; only their
+joint arbitrary-dirty-workspace consequence for this interface is claimed
+here. No predecessor result is audited or reverified.
+
+The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19227539)
+followed live PR/Discussion and batch reservations, searches of main READMEs,
+merged-PR searches and recent account contributions. The cached scan covered
+377 open PRs and 5,597 Discussion records with complete remote pagination;
+sparse local notes and unsearched diffs limit that coverage. No literature-wide
+novelty or acceptance is inferred from it.

research/joint-gaussian-transition-floor/RESULT.json

@@ -0,0 +1,22 @@
+{
+  "attaining_cases": 1011,
+  "claim_type": "scoped proof with exact finite corroboration",
+  "finite_lattices": 42,
+  "lattice_triangles": 216,
+  "maximum_checked_word_length": 18,
+  "reciprocal_pair": {
+    "adds": 4,
+    "scales": 2,
+    "total": 6
+  },
+  "rejecting_controls": 14,
+  "short_words": 4681,
+  "source_sha256": {
+    "PROOF.md": "e2e2f759f99f43b3be361f0c603c4491a6d685940f390e114ff816a2a730dec9",
+    "README.md": "29c75fd37cb4a32287bf51f5b834c06019e2182417f053e9e1c59c705ff2b4da",
+    "SOURCES.json": "8c9df4284591c98f29881ef2b36c75cffe38e3bbaa934c07a0804cabac85937b",
+    "TASK.json": "f76f4f99f94baeb2eb2f9ebc9b3a9e026a2d996de08a4bb902487e4cba5aa6ca",
+    "VERIFY.json": "6eccb9abad76892b8ac6e50f94daea8da558fbd19a0d2d0f663d1f10978b78b7",
+    "verify.py": "f5b60c589e6522997d24e1f2a51d7c360fd1d48d975f9aee294e719a64de7915"
+  }
+}

research/joint-gaussian-transition-floor/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/temporal-gaussian-rounding-seed22/README.md",
+      "usage": "provenance",
+      "git_blob": "aec4f45e0ff936fce434c3293670ecbfdcfdd4c9",
+      "sha256": "49f0bf08574a36e2810bcbea99ab60d3550cd043f8c2f0339fbe5a1780bed4cf"
+    }
+  ]
+}