Prove the binary-affine call floor with clean erasure (no new κ)

research/clean-affine-erasure-floor/PROOF.md

@@ -0,0 +1,124 @@
+# Clean workspace and erasure preserve the affine rank floor
+
+This is a scoped written proof, with finite corroboration in `verify.py`.
+It is not a complete multiplication theorem or a proof-kernel certificate.
+
+## The changed boundary
+
+Fix `d >= 1`, `G = AGL_d(F2)` and the formal group algebra `R = F2[G]`.
+Write `H(g) = [[A,b],[0,1]]` for `g(x)=Ax+b`, and
+`r(g)=rank_F2([A-I | b])`. All compositions act rightmost first.
+
+There are `W >= 1` arbitrary input data registers. A finite circuit may
+change its number of live registers. Every free instruction is an arbitrary
+rectangular binary scalar matrix, acting identically on the address space.
+This includes scalar mixing, singular maps, copying, zero allocation, reset
+and discarding. Ancillas created in this way enter at zero. Arbitrarily many
+initial dirty registers may also be present, provided the designated outputs
+have the specified action for all their initial values.
+
+A paid instruction at any current width is exactly #1333's instruction
+
+`D_N(g)=I+([g]+1)N`, with `N=uv^T`, `v^T u=1`, `r(g)=1`.
+
+Each occurrence costs one. The `W` designated output registers must equal
+`[g_j]` times input register `j`, with no other data or dirty-input dependence.
+Other outputs may contain arbitrary garbage and may be discarded. This is
+an identity of the retained output rows over the full formal algebra.
+Initial clean allocation and final output selection are free rectangular maps.
+No nonlinear, input-dependent, address-dependent or postselected free operation
+is included. The schedule is a fixed finite linear circuit.
+
+**Theorem.** Even with this enlarged free-operation class, the exact minimum
+paid-call count is `sum_j r(g_j)` for every finite tuple of affine targets.
+
+The predecessor, Gareth Davidson's #1333, proves this value when all free
+maps are invertible and every auxiliary input is arbitrary and restored.
+Its direct attaining factorization is used below as a cited premise.
+The new assertion is the lower bound under the changed clean/erasing boundary.
+
+## A rectangular defect invariant
+
+Let `epsilon:R -> F2` be augmentation, sending every `[g]` to `1`.
+Extend `H` linearly to `R`, and entrywise to rectangular matrices.
+For `M` of size `a` by `b`, put
+
+`M_hat = H(M)`, `M_bar = epsilon(M) tensor I_(d+1)`,
+
+`delta(M) = rank_F2(M_hat - M_bar)`.
+
+These are ordinary rectangular binary matrices of size `a(d+1)` by
+`b(d+1)`. Both hat and bar preserve every compatible product.
+For an `a` by `b` matrix `U` and a `b` by `c` matrix `V`,
+
+```
+(UV)_hat - (UV)_bar
+  = (U_hat-U_bar) V_hat + U_bar (V_hat-V_bar).
+delta(UV) <= delta(U) + delta(V).
+```
+
+This uses rank subadditivity and the fact that multiplication on either
+side cannot increase rank. It needs neither inverses nor square matrices.
+In particular, any scalar rectangular map `S` has `S_hat=S_bar` and
+`delta(S)=0`, even if it is singular. For a paid instruction,
+
+```
+epsilon(D_N(g)) = I,
+D_hat - D_bar = N tensor (H(g)-I),
+delta(D_N(g)) = rank(N) rank(H(g)-I) = 1.
+```
+
+The tensor-rank equality here is ordinary matrix rank over a field.
+Induction through the actual sequence of compatible dimensions therefore
+gives `delta(F) <= q` for every circuit operator `F` using `q` paid calls.
+
+## Reading only the required outputs is enough
+
+First omit initial dirty registers. Include clean allocation and final
+selection in the circuit. The complete retained operator on the `W` data
+inputs is then the formal square matrix `T=diag([g_1],...,[g_W])`.
+It has augmentation `I`, so
+
+```
+delta(T) = rank(diag(H(g_1)-I,...,H(g_W)-I))
+         = sum_j r(g_j).
+```
+
+Consequently `q >= sum_j r(g_j)`. Garbage is irrelevant because output
+selection was already included as a free rectangular instruction. Clean
+helpers need not be restored, and no assertion about their endpoint columns
+was used.
+
+If initial dirty registers are supplied, restrict their initial values to
+zero by a scalar input embedding. A circuit correct for every dirty input
+is correct under this restriction, with the same paid count. The preceding
+argument applies. This is a lower-bound restriction, not a permission to
+erase unknown data in a physical construction.
+
+For the matching upper bound, use #1333, PROOF.md Section 4: each affine
+`g_j` is a product of exactly `r(g_j)` displacement-one affine labels.
+Apply that factorization on its coordinate projector. It is a formal
+group-algebra identity, uses no auxiliary register and belongs to the
+enlarged model. Thus the enlarged model has the same exact optimum.
+The predecessor's factorization and original tariff are not new claims here.
+
+## Scope of the inference
+
+The defect inequality itself also holds for other group representations
+and for a sum of paid defect ranks. This proof uses it only for the stated
+binary-affine model and does not identify its rank with a recursive child
+tariff or a physical cost. In particular, a free address map has nonzero
+defect in general and cannot be added to the free scalar class silently.
+
+The homogeneous representation is not faithful on `F2[G]`. Formal equality
+implies the represented boundary used for the lower bound. Represented
+equality alone cannot accept an attaining circuit. The upper theorem is
+cited in the full formal algebra; every new clean/erasing finite fixture is
+checked there and by a separate faithful regular-action interpretation.
+
+Credit Gareth Davidson #1333 for the model, homogeneous displacement method
+and direct affine factorization, and its eumemic #288, Ali Romman #468,
+David Govea #720 and classical rank-method lineage. Rank subadditivity is
+classical. No general literature-priority claim is made. This extension was
+produced by Nick Petalas. Independent human and formal proof-kernel review
+are unclaimed. Apache-2.0.

research/clean-affine-erasure-floor/README.md

@@ -0,0 +1,55 @@
+# Clean copying and erasure cannot beat the binary-affine tariff
+
+This scoped algebraic proof extends Gareth Davidson's [#1333](https://github.com/CrocSwap/integer-mult-bounds/pull/1333). Its exact binary-affine paid-call floor survives arbitrary clean helpers, free scalar copying and reset, discarded garbage, and a changing number of live registers:
+
+```
+minimum paid calls = sum_j rank_F2([A_j-I | b_j]).
+```
+
+The paid alphabet is unchanged. Each call is `I+([g]+1)uv^T` over the full formal algebra `F2[AGL_d(F2)]`, with `v^T u=1` and `rank([A_g-I | b_g])=1`. Every free operation is an arbitrary rectangular binary scalar map. The retained outputs must implement the independent target maps `g_j(x)=A_j x+b_j` on arbitrary inputs. Helpers need not return to zero, garbage may be discarded, and any supplied dirty inputs must not affect the retained answer. The schedule is finite and fixed.
+
+The new [proof](PROOF.md) avoids inverse normalization. For a rectangular formal matrix `M`, define
+
+```
+delta(M) = rank(H(M) - epsilon(M) tensor I),
+delta(UV) <= delta(U) + delta(V).
+```
+
+Here `H` is the homogeneous affine representation and `epsilon` is augmentation. Every free rectangular scalar map has defect zero; every paid call has defect one. The selected output rows have defect equal to the displayed target bill. This proves the enlarged-model lower bound. The matching upper construction is cited directly from #1333, PROOF.md Section 4; no predecessor census or verifier is replayed.
+
+This closes a clean/erasing-workspace loophole for this specified alphabet. It is a side result under `bit-new-register-model`, with changed free-operation and output hypotheses. It supplies no physical supplier, recursive moment, new kappa or complete multiplication theorem. The selected frontier is unchanged.
+
+## Reproduction and evidence
+
+From the repository root:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/clean-affine-erasure-floor/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/clean-affine-erasure-floor/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/clean-affine-erasure-floor
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/clean-affine-erasure-floor --check-source-history
+```
+
+Substitute another CPython 3.12 executable elsewhere. The standard library suffices. Verification writes only a generated JSON receipt to stdout, bound to the six package source hashes. The direct marker is `PASS_CLEAN_AFFINE_ERASURE_FLOOR`; the runner and publication preflight print `PASS_REGISTERED_RESEARCH_PACKAGE` and `PASS_RESEARCH_COMMIT_BYTES`.
+
+The finite corroboration checks 74,384 compatible rectangular products, 682 free scalar maps, 315 paid factors, 48 clean/erasing circuits, 2,304 faithful basis columns, 192 omitted-call controls and eight boundary controls. It exhausts every compatible pair of rectangular matrices with one or two rows/columns over `F2[C2]`. It separately checks all binary scalar maps of shapes one through three and every allowed paid factor through three roles in the dimension-two affine group. New clean copy/compute/reset/discard circuits use two arbitrary data inputs, two zero helpers, four paid calls and two retained outputs. Full formal multiplication and a separate set-based faithful regular-action interpreter check their endpoints, including every group/data basis column. Single-call omissions, dirty-helper leakage, illegal free addresses, rank undercharging, a nonfaithful representation kernel and invalid domains are controls. The proof covers unbounded finite parameters; this finite domain does not enumerate arbitrary circuit words.
+
+The card's first working command, `scripts/research_selected_baseline.py`, passed with `PASS_RESEARCH_BASELINE_BINDINGS_ONLY`. This was orientation only. No selected scientific replay, native/tape execution, Lean or Docker check was run. Hosted CI is separate from local evidence.
+
+## Implementation scope
+
+The checker has no external executable, dynamic imports, recursion or filesystem mutations. Its finite group bound is 24, scalar width is at most four, represented matrices have at most twelve rows/columns, and all enumeration products have fixed limits visible in the code. All mathematical acceptance checks remain enabled under `-O`.
+
+Power of Ten rule 3 deviation: CPython and its standard library allocate managed objects during verification. This six-file standalone checker bounds live mathematical data by the complete 292-entry small-matrix inventory and the fixed four-role/24-element domains; it streams composition checks and faithful basis inputs. Runtime/library allocation is not statically controlled. Follow-up is required if these limits are enlarged. Other checks include a separately enumerated row-span rank oracle, explicit domain rejection, functions below sixty lines and warning-strict normal/optimized execution. No standalone linter is installed in this environment; AST inspection and both interpreter modes are the available diagnostics. No repository-wide diagnostic configuration is changed.
+
+## Sources and overlap
+
+[SOURCES.json](SOURCES.json) pins the unchanged predecessor README and proof at canonical main `de5ec2e7a6074068452f45b1a191b5c72832df4a`. They are cited inputs, not scientific replay targets. [TASK.json](TASK.json) records the changed hypothesis, exact claim and bounded overlap coverage. Live PRs, recent handoffs, local question reservations, merged-PR searches and all-main README terms were checked before claiming and before publication. These searches do not exclude unpublished work or establish literature priority.
+
+Credit Gareth Davidson #1333 for the binary-affine model, homogeneous displacement method, exact original tariff and direct attaining factorization. Its eumemic #288, Ali Romman #468, David Govea #720 and classical rank/reflection lineage retain credit. The new contribution is the rectangular augmentation-defect lower bound and its clean/erasing boundary application. This contribution was produced by Nick Petalas. Independent human and formal proof-kernel review are unclaimed. Apache-2.0.
+
+## Open next questions
+
+Can a physically justified free operation escape this defect bound while its complete cost remains favorable? Start with one actual native address-dependent operation and compute its represented defect and complete input/output invoice. The current theorem excludes only scalar free maps; physical legality, movement, ownership, precision and recursive charges remain blockers. Adding a nonzero-defect address operation at zero price changes the model rather than supplying an improvement.
+
+Can the same rectangular invariant give a sharp tariff for another specified group representation with clean/erasing workspace? Start with a cited direct construction whose representation-rank bill is attained, then state the retained output contract. A matching upper construction is necessary; a generic lower bound alone is not an exact tariff.

research/clean-affine-erasure-floor/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "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/binary-affine-register-bound/PROOF.md",
+      "usage": "input",
+      "git_blob": "b1152a39b559f7a058489ec74231488e4f8edd83",
+      "sha256": "36a33434222798434b0a17476ae5f9bc8a2a3891871c46e77cc50ce2e132206b"
+    },
+    {
+      "path": "research/binary-affine-register-bound/README.md",
+      "usage": "input",
+      "git_blob": "7b68583becf8be6f3cf666b05b0943e7eb99270c",
+      "sha256": "7951868efdf35fdb2aacdd302ca825cbde0586a5fae6df23aee78e29f30c332a"
+    }
+  ]
+}