Prove exact vector-label Heisenberg central tariffs (no κ)

research/heisenberg-vector-central-tariff/PROOF.md

@@ -0,0 +1,146 @@
+# Exact central-target tariff with vector labels
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Model and statement
+
+All vectors and matrices in this note are binary. For positive integers m,n,
+let H(m,n) consist of triples (u,v,Z) in F2^m × F2^n × M_(m,n)(F2), with
+
+    (u,v,Z)(p,q,W) = (u+p,v+q,Z+W+u q^T).
+
+Write x(u)=(u,0,0), y(v)=(0,v,0), and z(Z)=(0,0,Z). A paid call is
+
+    D_N(g) = I_r + ([g]+[1])N,
+
+in M_r(F2[H(m,n)]), where N is any nonzero rank-one binary r×r matrix and
+g is any x(u) with u≠0 or any y(v) with v≠0. Every such vector label costs
+one paid call. In particular, its coordinate decomposition is not separately
+charged. Arbitrary invertible binary scalar mixing is free. All r input
+roles may be dirty and no clean initialization, erasure or free address map
+is available. Equality means equality in the full formal group algebra.
+
+Choose nonzero matrices Z_1,...,Z_P and r≥P. The target has [z(Z_t)] on
+role t for 1≤t≤P and [1] on every other diagonal entry; off-diagonal entries
+are zero. Put K=Σ_t rank(Z_t).
+
+**Theorem.** The exact minimum number of paid calls is 2(K+P), for every
+finite r≥P. Zero target matrices may be omitted. The identity target costs
+zero. Arbitrary restored dirty spectator roles do not lower this minimum.
+
+The changed alphabet is essential. Cinna Davis's PR2258 proves a coordinate
+edge tariff in this same group family. Its calls only allow x(e_i),y(e_j),
+and its outputs are distinct edge coordinates. Here both the allowed labels
+and the central targets change: an entire arbitrary vector is one label,
+and a target may have any matrix rank. The new result is the matching
+tariff for that explicitly enlarged alphabet. It does not contradict the
+coordinate-edge theorem or price vector-label production in a bit supplier.
+
+## Upper bound by a closed vector walk
+
+For nonzero Z of rank k, take a rank factorization
+
+    Z = Σ_(i=1)^k u_i v_i^T,
+
+where both lists are linearly independent. Let u_0=0 and V=Σ_i v_i. Use
+
+    x(u_1)y(v_1)x(u_1+u_2)y(v_2)...x(u_(k-1)+u_k)y(v_k)x(u_k)y(V).
+
+There are k+1 x-labels and k+1 y-labels. Every label is nonzero by
+independence, including V. Immediately before the i-th y(v_i), the running
+u coordinate is u_i; after the last x(u_k), it is zero. The group law
+therefore gives final coordinates u=v=0 and central coordinate
+Σ_i u_i v_i^T=Z. This proves the full group identity, not just an identity
+in a representation.
+
+Apply this word to coordinate projector E_tt for each target t. The product
+acts by [z(Z_t)] on that role and identically on every other role. All calls
+are counted and every dirty spectator is restored. Total length is 2(K+P).
+For Z=I_2, the word is x(e_1)y(e_1)x(e_1+e_2)y(e_2)x(e_2)y(e_1+e_2),
+of length six, versus eight for two separate rank-one commutators.
+
+## Lower bound
+
+First normalize free scalar maps by pushing them through the paid calls.
+Conjugation preserves rank one. Augmentation sends every paid call and
+the target to I_r, so the final scalar map is I_r. It suffices to bound a
+pure paid word. Each factor is invertible, even for nilpotent N: g is an
+involution, so ([g]+[1])²=0 and D_N(g)²=I_r.
+
+Use the natural representation and its contragredient:
+
+    rho(u,v,Z) = [ I_m  u  Z  ]       rho_dual(g) = rho(g)^(-T).
+                 [  0   1  v^T]
+                 [  0   0  I_n]
+
+These are group homomorphisms. In rho, x(u) has only the off-diagonal block
+u at position (1,2), and y(v) only v^T at (2,3). The central target is Z
+at (1,3). In rho_dual, x(u) has only u^T at (2,1), y(v) only v at (3,2),
+and z(Z) only Z^T at (3,1). Signs disappear in characteristic two.
+Apply each representation entrywise to the full register matrix.
+
+For each x-labelled occurrence s, write N_s=a_s b_s^T and let u_s be its
+label vector. Define
+
+    A = [u_s ⊗ a_s]_s,       B = [b_s^T]_s.
+
+The target has zero (1,2) block. In the natural representation this block
+is exactly Σ_s u_s⊗N_s=AB. No product of two strictly upper blocks can
+contribute to (1,2). Thus AB=0 and
+
+    rank(A)+rank(B) ≤ n_x,
+
+where n_x is the number of x-labelled calls. Its central block C is the
+ordered sum of x-then-y products. Consequently im(C)⊆im(A). After a
+permutation of tensor coordinates, the target C is the block diagonal
+matrix with blocks Z_t and zero spectator blocks. Hence rank(C)=K and
+rank(A)≥K.
+
+In the dual representation, the central block C_dual is a sum of y-then-x
+products. Its row space is contained in the span of all rows
+u_s^T⊗b_s^T. For each nonzero target Z_t, the row space of C_dual contains
+a nonzero row q^T⊗e_t^T. Choose a nonzero coordinate of q and contract the
+address tensor coordinate there. This yields e_t^T. Applying the same
+contraction to any u_s^T⊗b_s^T yields either zero or b_s^T. Thus every
+active e_t^T belongs to row(B). The P active coordinate vectors are
+independent, so rank(B)≥P. Therefore n_x≥K+P.
+
+For completeness, the y-labelled argument uses
+
+    A_y=[a_s]_s,       B_y=[v_s^T⊗b_s^T]_s.
+
+The natural (2,3) block gives A_y B_y=0. Its central block has row space
+inside row(B_y), giving rank(B_y)≥K. The dual central block has column
+space inside the span of v_s⊗a_s. Contracting a nonzero address coordinate
+in each active target column gives e_t in im(A_y), so rank(A_y)≥P. It
+follows that n_y≥K+P. Every paid call is of exactly one label type, whence
+
+    length = n_x+n_y ≥ 2(K+P).
+
+Together with the explicit full-formal word, this proves the theorem for
+all finite dimensions and every finite number of dirty spectators. No
+finite search supplies this universal quantifier.
+
+## Evidence and scope
+
+The standalone verifier enumerates bounded central matrices, independently
+computes their ranks by minors, constructs full group endpoints, and obtains
+their exact one-role word distances by complete Cayley BFS. It also excludes
+every normalized word of length at most five for the new rank-two target
+with a restored second dirty role, using exact full-formal balls of radii
+three and two. Arbitrary rank-one binary couplings, including nilpotents,
+are present in that finite exclusion. Literal four-role formal matrices
+check heterogeneous targets and dirty spectator restoration.
+
+The theorem counts only this abstract alphabet. Producing arbitrary vector
+labels, native implementations, scalar mixing costs, physical read/write
+access, caller scheduling, hosting, precision, tapes, compiler closure,
+recursive moments and outer recovery remain unproved. It establishes no
+new κ and leaves all five selected framework assumptions intact.
+
+Credit Cinna Davis / 1337isnot1337, PR2258, for the H(m,n) coordinate-edge
+model and natural/contragredient rank-nullity strategy. That package credits
+the eumemic / woklerx normalized register model and preceding UT3/UT4
+shared-middle tariffs. Rank factorization, unitriangular representations,
+rank-nullity and closed-walk accumulation are classical. No broad
+literature-priority claim or independent human/kernel review is made.

research/heisenberg-vector-central-tariff/README.md

@@ -0,0 +1,130 @@
+# Exact vector-label Heisenberg central-target tariff
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+**Scoped proof with exact finite corroboration; no new κ.** In the binary
+group algebra of H(m,n), allow a paid rank-one register call to carry any
+nonzero vector label x(u) or y(v), at one call per vector. For nonzero
+central targets Z_t on P independent dirty roles, put K=Σ_t rank(Z_t).
+The exact minimum is
+
+    2(K+P) = 2 Σ_t (rank(Z_t)+1),
+
+for every finite number of exactly restored dirty spectator roles.
+Arbitrary invertible scalar mixing and nilpotent rank-one couplings are
+allowed. Zero target matrices need no calls.
+
+The [written proof](PROOF.md) gives an explicit closed vector walk of this
+length in the full group, and matching natural/contragredient rank-nullity
+bounds. Its rank-two example takes six calls instead of the eight needed
+by two separate rank-one commutator words:
+
+    x(e1) y(e1) x(e1+e2) y(e2) x(e2) y(e1+e2) = z(I2).
+
+This is a new tariff for an enlarged alphabet. Cinna Davis's
+[PR2258](https://github.com/CrocSwap/integer-mult-bounds/pull/2258) supplies
+the coordinate-edge H(m,n) model and proof strategy. Its edge theorem is
+cited, not audited or replayed. The cost of producing a vector label from
+coordinate operations is outside the changed unit-call model. In
+particular, this is no claim of a physical supplier saving.
+
+## Evidence
+
+The standard-library [verifier](verify.py) is standalone and read-only:
+
+- It enumerates all 682 central matrices for 1≤m,n≤3. Independent minor
+  ranks agree with the constructive decomposition. Complete Cayley BFS
+  covers 37,448 group elements across these nine groups and proves the
+  predicted one-role minimum for every central matrix in that domain.
+- For Z=I2 with a restored second dirty role, its 54 generators include all
+  nine nonzero rank-one binary 2×2 matrices and all six vector labels.
+  Exact full-formal balls have layers 1, 54, 1,971 and 64,044. All 2,026
+  radius-two join queries have no radius-three hit for the target. This
+  covers every normalized word of length at most five. The explicit
+  six-call witness is also found by the same join adapter at split 3+3.
+- Five literal four-role formal endpoint fixtures include different target
+  ranks, zero targets and arbitrary restored dirty spectators, through a
+  rank-four central matrix. Every one of the 56 single-call omissions is
+  rejected. Four invalid matrices and a chronology mutation are rejected;
+  reversal is checked as a valid inverse control.
+
+Finite checks corroborate the proof; they do not establish its universal
+quantifier. Each invocation prints a generated JSON record with source
+hashes for the verifier and proof, followed by
+`PASS_HEISENBERG_VECTOR_CENTRAL_TARIFF`. No receipt is hand-written.
+
+## Reproduce
+
+From the repository root, with CPython 3.12 and no third-party dependencies:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -B -W error research/heisenberg-vector-central-tariff/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -B -W error research/heisenberg-vector-central-tariff/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/heisenberg-vector-central-tariff
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/heisenberg-vector-central-tariff --check-source-history
+```
+
+Any CPython 3.12 path may replace the local interpreter above. Normal and
+optimized scientific replays are registered separately in [VERIFY.json](VERIFY.json).
+The source/history check requires the package to have been committed.
+The optional `--skip-mixed` direct mode omits the finite two-role search
+and is not the registered complete replay.
+
+## Limits and credit
+
+This counts formal paid calls. Arbitrary vector labels cost one by
+hypothesis; their production, physical scalar mixing, native implementation,
+source access, hosting, caller scheduling, precision/tapes, compiler closure,
+recursive invoices and recovery are unproved. All five selected framework
+assumptions remain. No selected record is changed. Independent human and
+formal proof-kernel review are unclaimed.
+
+Credit Cinna Davis / 1337isnot1337, PR2258, for the main predecessor,
+including its eumemic / woklerx normalized-register and UT3/UT4
+shared-middle lineage. Rank factorization, unitriangular representations,
+rank-nullity and closed-walk accumulation are classical. No general
+literature-priority claim is made. [SOURCES.json](SOURCES.json) pins the
+predecessor proof and README as provenance, not scientific replay inputs.
+
+The `bit-new-register-model` card has changed scope to a formal
+changed-alphabet cost theorem. The selected binding-only first example
+passes. This is a small mechanism/obstruction result rather than a native
+implementation or complete multiplication theorem. The
+[advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19376637)
+records the proposed formula before the checks.
+
+Overlap checks inspected canonical main
+`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, live open/account PR lists,
+recent handoffs, active Discussions, targeted all-state/merged searches,
+and a complete cached scan of 598 open PRs and 6,673 discussion records.
+Distinctive and general-form terms included Heisenberg, vector labels,
+compound labels, central matrices and rank-based commutator tariffs.
+The cached scan is timestamped November 3, 2026, 14:58 UTC. Closed PRs
+outside targeted searches, arbitrary diffs and unpublished work remain
+coverage limits; no-match searches are not novelty certificates.
+
+## Open next questions
+
+1. What is the exact tariff when label costs depend on the support size of
+   u or v? The unit-vector-label assumption is the unpriced physical step.
+   Start with the rank-two six-call word and charge each coordinate
+   constituent, then seek a weighted lower bound. The blocker is a specified
+   native vector-label interface and cost model.
+2. Can a concrete bit supplier realize these labels and central outputs at
+   a favorable complete signed bill? Start by binding the six-call rank-two
+   word to one exact source/consumer boundary, including every dirty return.
+   No such mapping or caller invoice is supplied here.
+
+## Verification design
+
+The verifier has no recursion, subprocesses, network, dynamic code or writes.
+Its fixed replay dimensions bound every loop: the largest Cayley domain is
+32,768 elements, the mixed search has at most 1+54+54²+54³ stored states,
+and formal fixtures have four roles with m,n≤4. Python allocates integers
+and collections dynamically, a managed-runtime deviation from Power of Ten
+rule 3. Live memory is bounded by these finite capacities; formal group
+supports have at most 2^24 bits per matrix entry. Increasing these domains
+requires a new capacity review. Functions fit within 60 physical lines;
+explicit `require` checks remain active under optimized Python. Strict
+warnings and AST compilation provide available interpreter diagnostics;
+no additional static analyzer is installed in the command environment.

research/heisenberg-vector-central-tariff/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "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/heisenberg-commutator-incidence-seedb054/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "8cbd78b3790f6dfc50cc74d3f6057457d14a1fc9",
+      "sha256": "dfb7bb979c11ba895f0e0efb38028195f1c8c050a14e1961dc2c675012ddea7b"
+    },
+    {
+      "path": "research/heisenberg-commutator-incidence-seedb054/README.md",
+      "usage": "provenance",
+      "git_blob": "af9d60e661168678bb286e4987788f850824107f",
+      "sha256": "e55bec07f4b542c6c7d2690f4d13244b7a9a7d53f83063dddee17c6c9f1474f0"
+    }
+  ]
+}