Prove a Fibonacci paid-scan floor for two dense dirty outputs (no κ)

research/fibonacci-scan-floor/PROOF.md

@@ -0,0 +1,134 @@
+# A Fibonacci support bound for two output banks
+
+## Exact model
+
+Let K be a field and let m>=2 banks each contain N coordinates. All mN
+initial coordinates are independent variables. In particular, extra banks
+contain arbitrary dirty data. A program is a finite composition of these gates:
+
+1. A monomial map within one bank, and a permutation of whole banks. These
+   may be arbitrary and may depend on N. We grant them zero cost in the bound.
+2. A charged ADD scan `x_i <- x_i + c M x_j`, with i distinct from j, c in K
+   and M monomial. It changes only bank i. Let S count these gates.
+3. A unary gate `x_i <- U x_i`, where every row of U has at most `2^r`
+   nonzero entries, for an assigned nonnegative integer r. Let R be the sum
+   of these assigned exponents. Unary native gates are covered when their
+   actual row supports satisfy this hypothesis.
+
+Monomial means a permutation times an invertible diagonal matrix. Each gate
+acts on the full bank volume. Invertibility of the unary gates is unnecessary
+for the lower bound, although reversible applications require it. General
+free bank GL, additions with source and destination in the same bank,
+multi-bank native gates and partial-volume operations are outside this model.
+An ADD with several summands must count each separate scan.
+
+For each bank i, let sigma_i be the maximum number of nonzero coefficients
+in any scalar row of its current linear map from all initial coordinates.
+Write A and B for the largest and second largest sigma_i, counting banks
+with multiplicity. Thus two equally large banks give A=B. Initially A=B=1.
+Zero rows are permitted later. Define F_0=0, F_1=1 and F_(k+2)=F_(k+1)+F_k.
+
+## Theorem
+
+At every program cut,
+
+```
+A <= 2^R F_(S+2),          B <= 2^R F_(S+1).                 (1)
+```
+
+Consequently, if each of two distinct required output banks has a row with
+at least D nonzero old-input coefficients, every implementation satisfies
+
+```
+2^R F_(S+1) >= D.                                           (2)
+```
+
+This holds for every finite m. Restoring arbitrary dirty helpers only adds
+endpoint requirements, so cannot invalidate the necessary inequality.
+The count S is a serial gate count, not a parallel depth or a count of
+traversals that fuse several ADDs.
+
+## Proof
+
+A monomial map only reorders and rescales scalar rows, so preserves sigma_i.
+A bank permutation preserves the sorted support profile.
+
+Consider one ADD with distinct banks i,j. Each new row of bank i is the sum
+of one old row of i and one scaled old row of j. Cancellations can only
+decrease support. Thus sigma_i' <= sigma_i+sigma_j <= A+B. All other bank
+support sizes are unchanged. After changing one bank, the second largest
+size is at most A, regardless of whether the changed bank becomes largest.
+Therefore
+
+```
+A' <= A+B,                 B' <= A.
+```
+
+If (1) holds before this gate, the Fibonacci recurrence proves it afterwards
+with S replaced by S+1 and R unchanged.
+
+A unary gate of exponent r replaces each scalar row by a linear combination
+of at most 2^r old rows of its own bank. Its support size grows by at most
+2^r. Every bank's size is therefore bounded by 2^r times its previous size,
+including the unchanged banks. Sorting preserves componentwise inequalities,
+so A'<=2^r A and B'<=2^r B. This proves (1) after replacing R by R+r.
+The initial profile satisfies (1) with S=R=0. Induction over the finite gate
+list proves (1). Two required dense banks force B>=D and give (2).
+
+The argument applies to total row support across all initial banks. If the
+required density is already present in one particular old-input block, it
+also lower-bounds this total support. Unknown dirty inputs cannot be treated
+as zero to erase those coefficients.
+
+## Two full chirps
+
+The paid scan escape in Ross Richardson's #4023 uses, on L internal bits,
+
+```
+alpha=(1+i)/2, beta=(1-i)/2,
+C=[[alpha,beta],[beta,alpha]],    C_L=C tensor ... tensor C.
+```
+
+Both alpha and beta are nonzero. Every row of C_L has exactly 2^L nonzero
+entries. The inverse exchanges alpha and beta and has the same density.
+Thus either endpoint `diag(C_L,C_L)` or `diag(C_L^-1,C_L)` on two arbitrary
+independent banks, with restored dirty helpers if used, requires
+
+```
+2^R F_(S+1) >= 2^L.                                        (3)
+```
+
+With no unary native gates, define
+`s_L=min { s>=0 : F_(s+1)>=2^L }`. Then S>=s_L. The first working example
+is L=3: F_4=3, F_5=5, F_6=8, so S>=5. The earlier single-maximum
+support argument gives S>=3 here. Since F_(L+1)<2^L for every L>=1,
+the new integer floor strictly improves that estimate. We claim no
+implementation attaining s_L.
+
+For L>=1, the elementary induction F_(s+1)<=phi^s, where
+`phi=(1+sqrt(5))/2`, gives the exact real inequality
+`S >= L log(2)/log(phi)` when R=0. The displayed integer minimum is the
+stronger usable statement. Hence no number of these inter-bank ADD scans
+bounded independently of L can produce both chirps without native queries.
+For general R, (3) is a necessary tradeoff, not an independent native-query
+optimum. Any separate query lower bound keeps its own alphabet hypotheses.
+
+## Why the distinct-bank premise matters
+
+Allow a buffered same-bank update `x <- (I+2X_j)x` over F5, where X_j flips
+address bit j. It is invertible because its two eigenvalues are 3 and -1.
+Three such updates on one eight-coordinate bank give row support eight.
+One inter-bank ADD into a second independent bank gives supports 8 and 9.
+If all four updates were charged as the theorem's ADDs with R=0, its second
+support bound would be F_5=5, which fails. Those first three gates instead
+have to be excluded or counted as unary support exponents. This is an
+explicit alphabet boundary, not a counterexample to (1).
+
+## Evidence boundary
+
+This is a scoped written proof. The finite verifier enumerates support-size
+relaxations and executes separate exact F5 matrices as corroboration.
+Neither establishes a complete multiplication theorem or a physical tape
+cost. The chirp tensor is used only for its density, with its predecessor
+construction and invoice cited rather than replayed. Formal proof-kernel
+and independent human review are unclaimed.

research/fibonacci-scan-floor/README.md

@@ -0,0 +1,102 @@
+# A Fibonacci paid-scan floor for two dense dirty outputs
+
+For any finite number of arbitrary dirty banks, S inter-bank monomial ADD
+scans and unary gates of total row-support exponent R can produce two
+output banks of row support D only if
+
+```
+2^R F_(S+1) >= D,      F_0=0, F_1=F_2=1.
+```
+
+This scoped proof strengthens the earlier single-maximum support bound by
+tracking the two largest bank support sizes. Arbitrary per-bank monomial
+address/phase maps and permutations of whole banks are granted free. Every
+ADD has distinct source and destination banks. [PROOF.md](PROOF.md) states
+the full alphabet, induction and its same-bank boundary.
+
+For the two full L-bit chirps in Ross Richardson's #4023, D=2^L. With no
+native gates the necessary scan count is the least s with F_(s+1)>=2^L.
+For L=3 this gives five ADDs instead of the inherited support-doubling floor
+of three. This is a lower bound; no matching optimal word is claimed.
+The selected kappa is unchanged.
+
+## Evidence and reproduction
+
+From the repository root, use CPython 3.12 and the standard library:
+
+```sh
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/fibonacci-scan-floor
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/fibonacci-scan-floor --check-source-history
+~/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/fibonacci-scan-floor/verify.py
+~/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/fibonacci-scan-floor/verify.py
+```
+
+Expected markers are `PASS_FIBONACCI_SCAN_FLOOR` and
+`PASS_REGISTERED_RESEARCH_PACKAGE`. The generated [RESULT.json](RESULT.json)
+contains all finite counts and SHA256 hashes of the proof, verifier and
+metadata. Default replay compares the complete receipt, including JSON
+types, and writes nothing. The verifier works in a Git-free package copy.
+
+The finite evidence includes every distinct sorted support-size relaxation
+profile through seven gates for two through five banks, with unary exponents
+one and two and total exponent at most four. Distinct-bank shears include
+every ordered bank choice. Independent dense F5 executions test actual
+cancellation, address permutations and unary operations. Tensor entries
+corroborate chirp density through seven internal bits. One-fewer-scan,
+invalid-input and same-bank-alphabet controls must reject.
+
+The all-parameter conclusion rests on the written induction. No predecessor
+verifier, native recipe, complete supplier, selected cold replay or proof
+assistant is run. General free bank GL, buffered same-bank ADDs counted as
+ordinary scans, multi-bank native gates, variable bank volumes and fused
+traversals require separate models. Physical routing, precision, restoration
+cost and actual runtime remain separate obligations.
+
+## Scope and sources
+
+Canonical base `624de9dc66858af0945e5f8a0942488d62280d43`, priority revision 7.
+The connector-alphabet-change card changes scope to its cost-aware controller
+boundary. Its old connector pairing fixture is not relevant to this alphabet
+and is not replayed. The first new fixture is L=3 with two output banks.
+The family decision is narrow: retain this quantitative obstruction and stop;
+no further construction campaign or frontier change follows from it.
+
+Ross Richardson's [#4023](https://github.com/CrocSwap/integer-mult-bounds/pull/4023)
+supplies the paid two-chirp escape and its explicitly open constant-scan
+question. His [#4082](https://github.com/CrocSwap/integer-mult-bounds/pull/4082)
+and [#4057](https://github.com/CrocSwap/integer-mult-bounds/pull/4057) supply
+the earlier support-doubling and paid-endpoint bounds in their respective
+models. The standard union-of-support argument and Fibonacci recurrence
+are not claimed as new methods. The new step is the two-bank order-statistic
+invariant and the resulting paid-scan/native-support tradeoff.
+[SOURCES.json](SOURCES.json) pins predecessor documentation as historical
+provenance; no executable predecessor dependency is imported.
+
+The live overlap scan covered 411 open PRs and 3,920 Discussion records at
+2026-10-22 23:04 UTC. Sparse local notes were incomplete. Separate all-main
+README and merged-PR searches covered the distinctive object and Fibonacci
+terms. This coverage is not a novelty certificate. The canonical
+[claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19134252)
+records the question and scope.
+
+## Open next questions
+
+1. Find the exact ADD optimum between this lower bound and #4023's cited
+   six-per-bit construction. Start at L=1 with two banks and explicit
+   monomial shears. Exact feasibility may depend on available coefficients;
+   no matching construction is supplied here.
+2. Derive a weighted support bound for partial-volume or fused traversals.
+   Start with a declared row-update and movement tariff. The present count
+   charges full-bank serial shears, so supplies no runtime price in that model.
+
+## Credit
+
+This contribution was produced by Nick Petalas. Apache-2.0. Credit Ross
+Richardson for the predecessor constructions, support arguments and open
+question, with their retained native and compiler lineage. Independent human
+and formal proof-kernel review are unclaimed.
+
+The verifier uses managed Python allocations. Its fixed finite domains and
+explicit profile-capacity check bound live data; no constant-allocation
+claim is made. All loops have finite domain bounds and no recursion is used.
+Warning-strict normal and optimized replay check the committed artifact.