Prove one lower-only phase cannot change an upper-shear endpoint (no new κ)

research/single-lower-phase-deletion/PROOF.md

@@ -0,0 +1,183 @@
+# Deleting one lower-only phase
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Exact model and statement
+
+Fix a field k, a positive width m and a finite number R of scalar registers.
+Write
+
+\[
+ u_A=\begin{pmatrix}I&A\\0&I\end{pmatrix},\qquad
+ v_K=\begin{pmatrix}I&0\\K&I\end{pmatrix},\qquad
+ U=\{u_A:A\in M_m(k)\},\quad V=\{v_K:K\in M_m(k)\}.
+\]
+
+Let C be any commutative coefficient ring. The application here is k=Q and
+C=F2, with rational or dyadic address matrices and free binary register
+mixing. Brackets denote *formal group-algebra labels*, not evaluation of
+an address matrix in characteristic two.
+
+Consider a state matrix
+
+\[
+ X=LFB,\qquad L,B\in M_R(C[U]),\qquad F\in M_R(C[V]).
+\]
+
+Let epsilon:C[V]->C be augmentation, sending every [v_K] to 1.
+For any chosen set of matrix entries J, assume X_ij belongs to C[U] for
+every (i,j) in J. Then
+
+\[
+ \boxed{X_{ij}=(L\,\epsilon(F)\,B)_{ij}\quad((i,j)\in J).}
+\]
+
+Thus the lower-only phase can be replaced by its scalar augmentation
+without changing any required upper-supported entry. No condition is
+imposed on other entries. With clean auxiliaries initially zero, J can be
+just the data-to-data block and auxiliary outputs can be garbage. With
+arbitrary dirty auxiliaries, J must also include each required data-from-
+auxiliary zero entry. Any required restoration entries must likewise be
+included. If every entry is upper-supported, the entire formal endpoint
+is unchanged.
+
+For a circuit, L and B consist of upper-shear paid calls and scalar mixing.
+F consists of any finite sequence of lower-left updates on individual
+registers and scalar mixing, with no intervening upper call. Its
+augmentation is precisely the product of the scalar mixing matrices in
+that phase. Every lower update augments to identity. If those mixing
+matrices are invertible, their product is an allowed free mixing map.
+Deleting the lower updates preserves every paid call and its rational rank.
+
+This is a scoped reduction. Internal register-dependent Levi maps,
+additional alternating lower phases and endpoints with non-upper labels
+are not covered. General full-Borel words remain open.
+
+## The label lemma
+
+Direct multiplication over k gives
+
+\[
+ u_Av_Ku_D=
+ \begin{pmatrix}
+ I+AK&A+D+AKD\\K&I+KD
+ \end{pmatrix}.                                      \tag{1}
+\]
+
+Suppose u_A v_K u_D = u_(A') v_(K') u_(D'). The lower-left
+block gives K=K'. The two diagonal blocks give AK=A'K and KD=KD'.
+Consequently
+
+\[
+ AKD=A'KD=A'KD',
+\]
+
+and comparison of the upper-right blocks gives A+D=A'+D'.
+No inverse of K, integrality condition or rank assumption was used.
+This includes K=0, when the label is simply u_(A+D).
+
+Therefore the following map on the *set of distinct group labels* is
+well-defined:
+
+\[
+ f:UVU\longrightarrow U,\qquad f(u_Av_Ku_D)=u_{A+D}.   \tag{2}
+\]
+
+It is identity on U. For all E,H it satisfies
+
+\[
+ f(u_E g u_H)=u_E f(g)u_H.                            \tag{3}
+\]
+
+Indeed prefixing and suffixing just replace A,D by E+A,D+H.
+The additive identity u_E u_A=u_(E+A) proves (3).
+
+Extend f C-linearly to the free C-module spanned by UVU, calling the map
+P. Equal labels have equal images by the lemma, so cancellations in the
+formal group algebra are respected. Equation (3) makes P a C[U]-bimodule
+map, and P fixes C[U]. It is not asserted to be a ring homomorphism or to
+extend to the entire group algebra.
+
+## Circuit reduction
+
+Every entry of LFB lies in the span of UVU. Expand its finite sums and
+apply (2) term by term. For upper labels a,b and a lower label v,
+
+\[
+ P([a][v][b])=[a][b].
+\]
+
+Linearity and matrix multiplication therefore give
+
+\[
+ P(LFB)=L\,\epsilon(F)\,B.                           \tag{4}
+\]
+
+At each required entry, the upper-support assumption gives P(X_ij)=X_ij.
+Equation (4) proves the statement. This works over every C, in particular
+the binary superposition algebra, without reducing rational addresses
+modulo two. Arbitrarily many registers do not change the argument.
+
+A contiguous phase in an ordinary left-multiplication circuit has the
+required factorization. The analogous right-multiplication circuit also
+does. If a model allows both left and right moves, the assertion requires
+the displayed *final factorization*, not just contiguity in wall-clock
+order. A phase acting on both sides of an existing upper word can leave
+two lower factors separated by that word. No reduction for that broader
+bidirectional case is asserted.
+
+## What changes for the source question
+
+Sagar Thakrar's [PR2613](https://github.com/CrocSwap/integer-mult-bounds/pull/2613)
+asks whether inserting D+=K H can escape the upper-shear superposition
+obstruction, beginning with one such update. The theorem above removes
+*every* contiguous lower-only phase under the explicit upper-supported
+endpoint and alphabet conditions. It covers singular K and even
+denominators, which a mod-two natural-representation argument cannot
+automatically cover.
+
+Any obstruction already established for the remaining upper-only word
+therefore transfers without changing its paid profile. The existing
+width-two abelian floor, when its full target hypotheses are supplied, is
+a predecessor premise from eumemic's PR288 as cited by PR2613. No new
+derivation or replay of that floor is claimed here. In particular, this
+package's new theorem is not a new census of three-call words or a claim
+about every full-Borel word. dcharb78's PR3183 separately reports a finite
+width-two block-Borel screen; it is not used in this proof.
+
+## Why the hypotheses matter
+
+If a required entry may retain a lower label, deletion need not preserve
+it: the one-register word v_1 differs from identity.
+
+Allowing an additional internal Levi factor also breaks naive deletion.
+In one dimension let d=diag(2,1). Then
+
+\[
+ u_1\,d\,u_{-1/2}\,d^{-1}=I,
+\]
+
+but deleting d and d^-1 leaves u_(1/2). This is a control on enlarging the
+middle alphabet, not a counterexample to the lower-unipotent theorem.
+
+Nor may one apply P as an unrestricted multiplicative map across many
+alternating lower phases. In one address dimension,
+
+\[
+ u_1v_1u_1v_{-1/3}u_{-3}v_{-1/3}=I,                 \tag{5}
+\]
+
+whereas deleting the three separated lower factors leaves u_-1.
+Equation (5) follows by direct 2-by-2 multiplication. It supplies no
+profitable paid word and no physical construction; it rejects a false
+unrestricted deletion rule.
+
+## Evidence boundary
+
+The universal result is the algebraic proof above. The standalone verifier
+checks literal matrix products, complete small finite-field collision
+classes, singular rational fixtures, and full formal superposition words.
+It imports no predecessor executable and supplies no finite-to-universal
+inference. Physical legality, native realization, chronological compiler,
+restoration outside the declared endpoint, precision/tape/stock and the
+complete signed invoice remain separate. No new kappa is claimed.

research/single-lower-phase-deletion/README.md

@@ -0,0 +1,155 @@
+# One lower-only phase cannot change an upper-shear endpoint
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+A contiguous phase of lower-left updates and binary register mixing can be
+deleted from a rational upper-shear superposition word whenever its required
+data entries are supported on upper-shear labels. The replacement preserves
+those entries and every paid call, including its rational rank. Width,
+register count, rational denominators and the rank of each lower update are
+unrestricted in the written theorem.
+
+This is a **scoped proof with exact finite corroboration**, not a search
+failure, new finite supplier or complete multiplication theorem. No new
+kappa is claimed.
+
+## The new reduction
+
+For upper shears u_A and lower shears v_K, the map
+
+\[
+ [u_Av_Ku_B]\longmapsto[u_{A+B}]
+\]
+
+is well-defined on distinct formal labels. This remains true for singular
+K. Its linear extension is an upper-shear bimodule retraction. Therefore,
+if X=L F B with L,B over the upper-shear group algebra and F over the
+lower-shear group algebra, then
+
+\[
+ P(X)=L\,\epsilon(F)\,B.
+\]
+
+At every required entry already supported on upper labels, P is identity.
+The scalar augmentation epsilon(F) is exactly the phase's binary mixing
+after all lower updates are deleted. [PROOF.md](PROOF.md) gives the full
+argument over any address field and any commutative coefficient ring.
+
+For ordinary circuits with all moves multiplying on one side, a contiguous
+lower-only phase has this factorization. In a model with both left and
+right actions, the final factorization must be supplied separately.
+Contiguity in chronological order alone is insufficient for this argument.
+
+## Reproduce
+
+From the repository root, with CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/single-lower-phase-deletion/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/single-lower-phase-deletion/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/single-lower-phase-deletion
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/single-lower-phase-deletion --check-source-history
+```
+
+Any CPython 3.12 executable may replace the displayed path. Each direct run
+prints `PASS_SINGLE_LOWER_PHASE_DELETION` in a generated JSON receipt bound
+to the package files by SHA256. Default replay writes no files. The same
+standalone check works without Git or predecessor packages.
+
+The verifier checks:
+
+- All 4,256 triples in four complete finite-field domains: width one over
+  F2, F3 and F5, and width two over F2. It compares all 1,420 repeated labels
+  with their previously computed A+B. The respective distinct-label counts
+  are 6, 21, 105 and 2,704.
+- 144 literal rational triples at widths one through three, including 92
+  singular K matrices, and 144 outer bimodule identities. An independent
+  recovery formula uses a checked inner inverse H with K H K=K, rather
+  than the generating A and B.
+- 24 complete binary group-algebra factorizations, containing 112 entries.
+  Projection agrees with phase deletion throughout; all 42 upper-supported
+  entries agree directly.
+- Six hypothesis or mutation controls and three invalid-dimension
+  rejections. These distinguish a singular-K collision, an incorrect raw
+  upper-right-block rule, a non-upper endpoint, internal Levi maps,
+  separated lower phases and unconstrained auxiliary output. Checks remain
+  enabled under optimized Python.
+
+Finite checks corroborate the written proof. No finite enumeration is used
+to infer its all-width conclusion.
+
+## Scope and predecessor credit
+
+The source question is the first open question of Sagar Thakrar's
+[PR2613](https://github.com/CrocSwap/integer-mult-bounds/pull/2613), which
+proposes one inserted lower-left update in a rational shear superposition
+word. That package supplies the model and the distinct 2-integral
+obstruction. eumemic's PR288 supplies the original register model and
+upper-only width-two obstruction; Swapnil Jain's framework supplies the
+credited related rank functional and free class. Their scientific results
+are cited as premises, not replayed or claimed as new here.
+
+ywz65's [PR2671](https://github.com/CrocSwap/integer-mult-bounds/pull/2671)
+and Nick Petalas's
+[PR6027](https://github.com/CrocSwap/integer-mult-bounds/pull/6027) concern
+common invariant lattice filters. This theorem uses no integrality or
+lattice-feasibility assumption and does not extend those filters.
+dcharb78's [PR3183](https://github.com/CrocSwap/integer-mult-bounds/pull/3183)
+reports a separate finite width-two block-Borel screen. This contribution
+neither audits that screen nor claims its call-count result. Exact main
+READMEs and the source proof are pinned as provenance in
+[SOURCES.json](SOURCES.json); no predecessor executable is imported.
+
+The active card is `bit-helper-contract`, changed from G20 helper
+construction to the explicit full-Borel handoff. This is a local interface
+obstruction relevant to a proposed way around paid-call floors. Its new
+step is the single-phase deletion theorem. General literature priority
+for elementary block multiplication or bimodule methods is unclaimed.
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19246973)
+records the question and source baseline.
+
+Required endpoints must be supported on upper labels. Arbitrary independent
+internal Levi maps, multiple alternating lower phases and an arbitrary
+bidirectional chronological phase are outside the theorem. The supplied
+Levi and three-phase identities reject broader naive deletion rules.
+No complete full-Borel impossibility result is claimed. The reduction
+preserves an existing paid profile; it does not produce an improved one.
+
+Physical lower-update legality, native operators, boundary conversions,
+dirty restoration beyond the declared data block, stock, precision/tape,
+uniform compiler and the full signed invoice remain separate obligations.
+No selected-word replay, native replay, Lean, Docker or complete multiplier
+ran. Independent human and formal proof-kernel review are unclaimed.
+
+## Open next questions
+
+- Can separated lower-only phases provide a favorable completed rational
+  superposition word? Start with a width-two word with two such phases,
+  its full formal data block and complete paid/target invoice. No such
+  saving word or physical caller is supplied here; the projection cannot
+  be multiplied across arbitrary phases.
+- What deletion criterion survives internal register-dependent Levi maps?
+  Specify the enlarged middle alphabet and test equality of double-coset
+  labels against the proposed deleted labels. The simple Levi identity
+  already rejects naive deletion, so another search needs a changed
+  reduction and full boundary accounting.
+
+Structured first steps and blockers are in [TASK.json](TASK.json).
+
+## Implementation bounds
+
+The executable is a bounded verifier, not a public matrix solver. Its
+largest address matrix is 6 by 6, scalar register count is at most three,
+and group-algebra support is capped at 256 labels per entry. Finite-field
+enumeration has at most 16^3 triples per domain. Functions remain below
+60 physical lines, control flow is nonrecursive, and invariant checks use
+explicit exceptions that survive `-O`.
+
+Power-of-ten rule 3 has a managed-runtime deviation in `verify.py`.
+CPython allocates exact Fraction values, tuples and sets during checking.
+Fixed dimensions, fixture counts, rational input alphabets and support
+caps bound the computation and live data. No external matrix or circuit
+is read. Each declared replay has a 60-second timeout. A public solver
+would require separate bit-size and memory budgets. Warning-strict normal
+and optimized runs provide the available standard-library diagnostics;
+there is no project Python type-checker configuration for this package.

research/single-lower-phase-deletion/SOURCES.json

@@ -0,0 +1,48 @@
+{
+  "schema_version": 1,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "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/bit-full-borel-2adic-floor/README.md",
+      "usage": "provenance",
+      "git_blob": "7ab7cdc4fab95a91939eef7fe1a220fa6a02343f",
+      "sha256": "9237eae400e6d63ee1f3f53bf75ff29b4136d9d1d354c3a8d25a691711813af2"
+    },
+    {
+      "path": "research/bit-full-borel-2adic-floor/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "f5b6ff4c8ce068a3f31d9dfa55b9c92daf2bc3de",
+      "sha256": "c88a75a10400b931c604c30c0d84395966c4c10cfe39b1f9ee15ac8a565aa8de"
+    },
+    {
+      "path": "research/paired-diagonal-borel-gauge/README.md",
+      "usage": "provenance",
+      "git_blob": "55788f0f6b209d800f19cf53a29403500071e1d5",
+      "sha256": "beb65171fd265dfaadef59aa778c5192d9880217a2c10d88c48184a8b25972f1"
+    },
+    {
+      "path": "research/projector-anchored-paired-lattices/README.md",
+      "usage": "provenance",
+      "git_blob": "f41634f35d442bf5f9c0426904f5c145f6f561da",
+      "sha256": "85f055f11f6932a0e11f7d85c9481d920a9e452f9dbbf13375b279bc464e3338"
+    },
+    {
+      "path": "research/r439-sub10k-sixway-and-star-dual-witnesses/README.md",
+      "usage": "provenance",
+      "git_blob": "3425f0ac5f6e53f421f33519f2e7a5eb532b427e",
+      "sha256": "55c39aa7aa4ac2096d7086a8847c3a06d471c5c90928862f6fe1265b536bdb21"
+    }
+  ]
+}