Prove exact minimum persistent stock for query streams (no κ)

research/causal-query-cache-stock/PROOF.md

@@ -0,0 +1,178 @@
+# Minimum persistent cache at the minimum acquisition count
+
+This scoped proof and its compiler were produced by Nick Petalas.
+
+## Contract and statement
+
+Let K be any field. Fix a finite list of row vectors v_1,...,v_m in K^n.
+There is an immutable bank x of n arbitrary independent payload fields.
+At request i the value v_i x is available, and the requested answer is
+Q(v_i x), for one common K-linear query Q and one common physical ABI.
+The response is delivered before request i+1. Delivered responses cannot
+be read again. Any copy retained by the responder counts as cache.
+
+Ordinary instructions take scalar K-linear combinations. An acquisition
+applies Q to an ordinary combination of the original bank and returns one
+payload field. Queries never take query-dependent data as their inputs.
+For the lower bound, arbitrary prefetch of available ordinary combinations
+is permitted. The upper construction only queries the current request.
+The word and its coefficients are fixed independently of payload contents.
+No external query-dependent advice or consumer feedback is available.
+
+We require formal query correctness: ordinary and queried coefficients
+are distinguished. Equivalently analyze values as a x + b Qx with the two
+coefficient rows independent. This is justified by a faithful formal
+operator model, or by requiring the same scalar protocol to work for all
+linear Q and all payloads. It is not justified for a fixed scalar Q.
+No second nonordinary operator or non-scalar ordinary address algebra is
+admitted here.
+
+Owned cache fields and one response/work field may be initialized and
+erased, at positive cost. Original sources are unchanged. Dirty spectators
+are untouched. This is the observational owned-erasure contract, not a
+reversible dirty-workspace theorem. Ordinary arithmetic, moves, entry
+scrubs, output delivery and all clears must be charged by an installation.
+
+Set, at the cut after response i has been delivered,
+
+    V_i = span(v_1,...,v_i),
+    W_i = span(v_(i+1),...,v_m),
+    r   = dim span(v_1,...,v_m),
+    d_i = dim(V_i intersect W_i)
+        = dim V_i + dim W_i - r.
+
+The empty spans at i=0,m are zero. Persistent cache counts all owned
+query-dependent state across these cuts. A response/work field is empty
+at every cut and is counted separately during a request.
+
+**Theorem.** The minimum number of acquisitions is r. Among protocols
+using exactly r acquisitions, every cut needs at least d_i persistent
+fields. One causal protocol attains all these lower bounds simultaneously.
+Consequently the exact minimum persistent capacity is
+
+    b = max_(0 <= i <= m) d_i.
+
+The same protocol can be implemented using b cache fields and one
+response/work field, with scalar ADD, nonzero SCALE, SWAP and owned CLEAR.
+It uses no additional payload field for a basis conversion. This b+1
+upper bound on total temporary fields is not claimed optimal.
+
+## The new lower bound
+
+Each acquired answer contributes one queried coefficient row. Ordinary
+instructions can only combine those rows. All delivered answers together
+have row span of dimension r, so at least r acquisitions are necessary.
+
+Consider an arbitrary correct protocol using exactly r acquisitions.
+Let p_i be the number acquired by cut i. Past answers span V_i, so
+p_i >= dim V_i, even if the protocol prefetched future rows or discarded
+old answers. Let C_i be the span of queried coefficient rows in its
+persistent state at that cut. If k_i fields persist, dim C_i <= k_i.
+Ordinary parts in the same fields do not increase this queried dimension.
+
+Only the persistent state and r-p_i subsequent acquisitions can supply
+queried coefficients to future answers. Past consumer outputs are
+unavailable by contract. Therefore
+
+    dim W_i <= dim C_i + (r-p_i),
+
+and hence
+
+    k_i >= dim W_i-r+p_i
+        >= dim W_i-r+dim V_i
+         = d_i.
+
+This argument permits arbitrary linear cache encodings, discarded cache
+values, prefetch, raw-source retention and scalar computation on raw
+sources. None of them supplies an additional queried coefficient row.
+It does not cover query feedback or free access to past consumer outputs.
+
+## A single schedule attains every cut bound
+
+Retain answers for a basis of U_i=V_i intersect W_i after cut i.
+Initially U_0=0. At request i, write v=v_i.
+
+If v belongs to V_(i-1), it also belongs to W_(i-1), since it is a current
+or future request at the preceding cut. Thus v belongs to U_(i-1), and
+its answer is reconstructed from the cache with no query. Otherwise query
+the actually available v x once. The number of such rank increases is r.
+
+For the transition to U_i, observe
+
+    U_i is a subspace of U_(i-1) + span(v).
+
+Indeed write u=a+c v with u in U_i and a in V_(i-1). Both u and v belong
+to W_(i-1), so a belongs to V_(i-1) intersect W_(i-1). Every new basis
+answer can therefore be formed from the old cache and the response.
+After conversion, deliver the response and clear the response/work field.
+Only dim U_i=d_i independent cache answers remain. At the final cut U_m=0,
+so the cache is empty. This proves simultaneous attainment and the theorem.
+
+The basis choice and causal reconstruction build on Dugongue's #5803,
+volume-scheduling S12-S13. The contribution here is the matching per-cut
+lower bound, its global minimum-capacity consequence, and the bounded
+instruction-emitting compiler. The dimension identity is classical linear
+algebra and is the usual connectivity function of the represented matroid;
+no worldwide priority claim for that function is made. Request order is
+fixed. Optimizing order is a different problem.
+
+## Why basis conversion needs no second payload bank
+
+Pad the old cache by zero fields to b entries and append the current
+response. Express each new cache basis row in the old basis plus v.
+These coefficients and a last row preserving the response give a square
+(b+1)-by-(b+1) scalar matrix T. The unwanted cache rows are zero.
+
+Two-sided Gaussian elimination constructs invertible L,R with
+
+    L T R = diag(I_s,0).
+
+Execute R^-1 on the existing bank, clear the last b+1-s transformed
+coordinates, and execute L^-1. These operations realize T on every bank
+input. Each elementary matrix is a scalar ADD, nonzero SCALE or SWAP.
+No temporary payload field is used. The response may move during this
+conversion but is restored before delivery. The compiler emits those
+individual instructions, not a simultaneous-assignment oracle.
+
+For a bank of h=b+1 fields, the reduction uses at most h pivot steps,
+h row swaps, h column swaps, h scales, h(h-1) row ADDs and h(h-1) column
+ADDs. Its emitted inverse factors and clears have at most 2h^2+2h
+instructions. Preparing a dependent response uses at most b ADDs, and
+its post-delivery clear uses one. Entry scrubbing uses h clears.
+Thus an installation may charge at most
+
+    h + m (2h^2+2h+b+1)
+
+such ordinary instructions, in addition to r acquisitions, current-source
+assembly, descriptor construction and access, coefficient arithmetic,
+output transport, and their physical routing/precision costs. Scalars
+must actually be admitted at the common chart. Elimination over a field
+does not prove a dyadic-only implementation or a uniform physical tariff.
+
+## An unbounded strict stock improvement over retaining named answers
+
+For n>=1 request e_1,...,e_n, followed by e_1+...+e_n. The total rank is n.
+For each cut 1<=i<=n, U_i is the line spanned by e_1+...+e_i. Hence b=1.
+The responder accumulates the queried running sum and uses exactly n
+queries. Keeping every individually acquired answer until its final use
+would instead retain n fields at the cut before the last response.
+That fixed-value policy is a comparator, not a lower bound for general
+cache encodings. The new theorem supplies the latter lower bound of one.
+
+## Boundaries that matter
+
+- If previous responses remain readable, the width formula can overcharge
+  the responder's private cache. Those responses are additional state.
+- If reacquisitions are allowed, b need not be necessary. Requesting one
+  nonzero row twice uses one query and one persistent field at the optimum;
+  two queries use zero persistent fields.
+- If Q is an ordinary scalar, queried and ordinary rows are not independent,
+  and the acquisition lower bound can fail entirely.
+- Query feedback, noncommuting ordinary operators, differing frames,
+  source mutations, input-dependent control and dirty-return-only work
+  fields have different contracts.
+
+The proof is all-size within this contract. The executable compiler and
+finite checks have the separate bounded domains stated in README.md.
+No selected supplier installation, new kappa, full multiplication theorem,
+independent human review or formal proof-kernel acceptance is claimed.

research/causal-query-cache-stock/README.md

@@ -0,0 +1,186 @@
+# Exact persistent stock for minimum-query streams
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+For a fixed chronological list of common-query requests, let V_i and W_i
+be the scalar row spans of past and future requests at cut i. Put
+r=rank(all requests). The exact minimum persistent cache, among protocols
+using the minimum r acquisitions, is
+
+```text
+b = max_i dim(V_i intersect W_i)
+  = max_i (rank(V_i) + rank(W_i) - r).
+```
+
+One causal program attains every cut lower bound simultaneously. The
+[proof](PROOF.md) allows arbitrary linear cache encodings and legal prefetch
+in the lower bound. The upper construction only queries the current
+request. [compile.py](compile.py) emits individual scalar ADD, nonzero
+SCALE, SWAP and owned CLEAR instructions using b cache fields plus one
+response/work field. No second conversion bank is hidden.
+
+Claim type: scoped written proof with exact finite corroboration and a
+bounded constructive compiler. This is a new matching stock lower bound
+and compiler for the common-query observational interface. Dugongue's
+[#5803](https://github.com/CrocSwap/integer-mult-bounds/pull/5803), scheduling
+S12-S13, supplies the causal query-basis and one-cut intersection
+compression constructions. Those are cited predecessors, not audit targets.
+The rank identity and represented-matroid connectivity function are
+classical. No claim of worldwide novelty for those ingredients is made.
+
+For example, request e_1,...,e_n and then their sum. Exactly n acquisitions
+and one persistent field suffice for every n>=1. Retaining the individually
+acquired answers until their last use would use n persistent fields.
+This construction changes the retained values. It does not merely reassign
+fixed lifetimes to fewer slots.
+
+## Exact boundary
+
+Sources are immutable and arbitrary. Every request is an ordinary scalar
+row on that source bank, available at its request time. Answers are
+observational outputs, delivered in order and inaccessible after delivery.
+All query-dependent state crossing a cut counts toward the cache. A copy
+kept by the responder counts too. Ordinary and queried coefficients must
+be formally distinguishable. A scalar Q is outside the lower bound.
+
+Queries take only ordinary source combinations. Query feedback,
+non-scalar ordinary operator algebras, source mutations, consumer feedback,
+different charts and read-access to past outputs have different contracts.
+Owned erasure is permitted and charged. Original sources and arbitrary
+dirty spectators are preserved. This is not a dirty-return-only workspace
+construction. The exact result concerns persistent stock at delivery cuts;
+b+1 is an upper bound on total temporary payload fields, not a claimed
+minimum for every microstep.
+
+An installation must pay all ordinary instructions, current-source
+assembly, initial scrubs, delivery, routing, coefficients, descriptors,
+clears and physical access. With h=b+1, the proof gives an ordinary scalar
+instruction bound h+m(2h^2+2h+b+1), separately from the r acquisitions.
+General field elimination does not automatically give dyadic scalar
+recipes. No selected supplier region is installed or repriced here.
+No new kappa, selected-frontier change or full multiplication theorem is
+claimed. The five selected framework assumptions remain.
+
+## Reproduce
+
+From the repository root, with CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/causal-query-cache-stock/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/causal-query-cache-stock/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/causal-query-cache-stock
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/causal-query-cache-stock --check-source-history
+```
+
+Another CPython 3.12 may replace the absolute interpreter path. The direct
+verifier emits `PASS_CAUSAL_QUERY_CACHE_STOCK` in a generated JSON receipt
+bound to SHA256 hashes of all package files. It writes nothing. Registered
+replay also prints `PASS_REGISTERED_RESEARCH_PACKAGE`; publication checking
+prints `PASS_RESEARCH_COMMIT_BYTES`. No receipt is hand-authored or trusted
+as an input. Redirect output into a scratch directory if a saved receipt
+is wanted.
+
+The compiler accepts a JSON object with exactly `prime`, `dimension` and
+`rows`. Its executable domain is at most 24 requests on 1..8 sources over
+F_2, F_3, F_5, F_7 or F_11, with canonical integer residue entries. Empty
+streams and zero rows are accepted. For example:
+
+```json
+{"prime": 3, "dimension": 2, "rows": [[1,0], [0,1], [1,1]]}
+```
+
+Save that object outside the checkout and run:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -B research/causal-query-cache-stock/compile.py /absolute/path/problem.json
+```
+
+The result has two acquisitions, persistent width one and a two-field bank.
+Its cuts, acquisition decisions and literal ordinary instructions are
+included. Compilation chooses a basis from the supplied coefficient rows;
+it is offline metadata work, not a free physical source observer.
+
+## Evidence
+
+The independent finite-state oracle enumerates every subspace as a subset
+of its finite vector space and tests additive closure. For each capacity,
+it tries every available retained subspace and minimizes acquisition count.
+It uses no elimination or intersection routine from the compiler.
+The complete domains, including zero rows and empty streams, are:
+
+| Field and source dimension | Maximum request length | Streams | Subspaces |
+| --- | ---: | ---: | ---: |
+| F_2, dimension 2 | 6 | 5,461 | 5 |
+| F_2, dimension 3 | 4 | 4,681 | 16 |
+| F_3, dimension 2 | 4 | 7,381 | 6 |
+
+All 17,523 oracle optima match the emitted persistent width and minimum
+query count. Literal instruction replay checks every delivered formal
+answer, each retained basis, entry scrubbing, exit zero and two independent
+dirty spectators. Separate complete matrix tests check all 2-by-2 matrices
+over F_2,F_3,F_5 and all 3-by-3 matrices over F_2, totaling 1,234 matrices.
+Forty running-sum family cases cover all five supported fields and source
+dimensions 1..8. Six boundary cases exercise the full 24-request and
+nine-field-bank limits, including rank zero.
+
+Twenty-one rejection controls cover invalid domains, deleted acquisition,
+missing entry scrub, false query count, destroyed output, a spectator
+address, changed cache basis, aliased ADD, zero SCALE, Boolean address and
+unknown instruction. The finite oracle restricts acquisitions to the
+current request; the written lower proof additionally permits legal
+prefetch. Neither finite enumeration nor Python execution proves all-size
+physical implementation or formal-kernel acceptance.
+
+## Verification scope and code constraints
+
+Scientific base is canonical main
+e54523517d0f03e58352e647c403a5af3e525a57, priority revision 8, with selected
+conditional kappa 0.00363005817 from #7000. The first baseline example passed
+as source-binding orientation only. [SOURCES.json](SOURCES.json) pins the
+selected record, catalogue, priorities and the two predecessor prose files
+as historical provenance. No predecessor mathematical suite is imported or
+replayed. [TASK.json](TASK.json) records the changed card scope and
+[advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19539387).
+
+The original caller/native acceptance gate remains unmet. Native operators,
+matched physical ABIs, supported scalar recipes, owned erasure, compiler,
+precision/tape, stock and analytic recovery require a separate installation.
+Selected cold replay, Lean, Docker, supplier admission, independent human
+review and proof-kernel review are unrun and unclaimed.
+
+New code is nonrecursive and functions are shorter than 60 lines. Compiler
+inputs bound requests by 24 and source dimension by eight; derived matrices
+have at most sixteen unknowns or nine bank rows. Finite oracle spaces have
+at most nine elements, so it enumerates at most 512 subsets. All failures
+use explicit exceptions that remain active under optimization.
+
+Power of Ten rule 3 has a managed-runtime deviation: Python allocates
+lists, dictionaries and integers during these bounded computations.
+Streams are checked one at a time and only a digest and counts persist.
+Rule 8/9 has a fixed-source loading deviation: the verifier executes only
+the package-local compile.py through runpy, with a fixed finite callable
+set. No external source or input-provided code is loaded. Warning-strict
+normal/optimized replay, in-memory syntax parsing and whitespace checks
+supply the available diagnostics. No new external dependency or shared
+configuration is introduced.
+
+## Open next questions
+
+1. Does an actual common-ABI source request stream have a smaller b than
+   its retained-answer bank? Export its literal immutable source rows and
+   delivery cuts first, then price every coefficient conversion, route and
+   clear. The missing blocker is an installed physical request stream.
+2. What is the exact stock versus reacquisition tradeoff when more than r
+   queries are allowed? Start with an independently enumerated small stream
+   where capacity b-1 needs additional queries. The theorem fixes the
+   minimum query count and supplies no global tradeoff formula.
+
+## Credit
+
+Credit David Ganz / Dugongue and #5803 S12-S13 for causal basis acquisition
+and sufficient future-demand intersection compression. Retain that
+package's credit to Ali Romman, ToikY, zxv, Cinna Davis, Cao Yifan,
+Ryanson Jonathan, Jacob Alan Sussman and the native/ownership/compiler
+lineage. Classical span, dimension and Gaussian-elimination methods are
+not claimed as new. The matching lower bound, scoped synthesis and finite
+checks were produced by Nick Petalas. Predecessor files are unchanged.