Prove sharp divergence windows for observed coupled bills (no new κ)

research/observable-forced-recurrence/PROOF.md

@@ -0,0 +1,179 @@
+# Observed coupled bills and a sharp divergence window
+
+Let A be an n by n nonnegative rational matrix and let b,c be nonnegative
+rational column vectors. Define
+
+\[
+ a_k=c^T A^k b,\qquad S_N=\sum_{k=0}^{N-1}a_k,\qquad S_0=0.
+\]
+
+The graph convention is j -> i when A_ij>0. A path of length zero is allowed.
+Let H be the intersection of the vertices reachable from supp(b) and the
+vertices that can reach supp(c). Put r=|H|, B=A[H,H], beta=b[H], gamma=c[H].
+All statements below concern this declared nonnegative linear model. They
+do not establish that a proposed matrix bounds any actual supplier.
+
+## Theorem
+
+If H is empty, every a_k is zero. Otherwise exactly one of the following holds.
+
+1. There are positive rational p and rational 0<=q<1 with Bp<=qp. The bill is
+   finite. Its exact value is gamma^T u, where u is the unique solution of
+   u=Bu+beta. Moreover, for every integer K>=0,
+
+   \[
+   \sum_{k=K}^{\infty}a_k=\gamma^T B^K u
+   \le \alpha q^K\gamma^T p,
+   \qquad \alpha=\max_i u_i/p_i.
+   \]
+
+2. There is a nonzero rational v>=0 with Bv>=v and gamma^T v>0. Define
+
+   \[
+   z=\sum_{t=0}^{r-1}B^t\beta,\qquad
+   \delta=\min_{i:v_i>0}z_i/v_i,\qquad h=\delta\gamma^T v.
+   \]
+
+   Then z>0, delta>0, h>0, and for every integer N>=0,
+
+   \[
+   \boxed{S_N\ge\lfloor N/r\rfloor h.}
+   \]
+
+Both alternatives have rational certificates checked by graph closure and
+matrix-vector arithmetic. No eigenvalue approximation is needed. The window
+r in the second alternative is the smallest universal dimension-only window
+for a positive bound of this form without an additive delay. In fact the
+stated bound can be an equality for every N.
+
+## Path reduction
+
+Expand c^T A^k b as the sum of the weights of all length-k paths from a vertex
+with b_j>0 to a vertex with c_i>0. The weight includes both endpoint weights.
+Every vertex on every contributing path is in H. Conversely, restricting to
+H removes no contributing path. Thus
+
+\[
+a_k=\gamma^T B^k\beta\quad\hbox{for every }k\ge0.
+\]
+
+For every vertex in H there is an input-to-vertex path entirely in H and a
+vertex-to-output path entirely in H. Choose simple paths, each of length at
+most r-1. Therefore z>0. The analogous row vector
+
+\[
+w^T=\sum_{t=0}^{r-1}\gamma^T B^t
+\]
+
+is strictly positive as well. These assertions concern all vertices in H,
+including ones with beta_i=0 or gamma_i=0.
+
+## The classical alternative used here
+
+For completeness, the following argument states the classical nonsingular
+M-matrix alternative used by Ali Romman's #5785. Its mathematical priority
+is not claimed here.
+
+Set M=I-B. Its off-diagonal entries are nonpositive. Eliminate columns in
+order, without row swaps, as long as the diagonal pivot is positive.
+Every remaining Schur complement has nonpositive off-diagonal entries.
+
+If all pivots are positive, forward and backward substitution on Mp=1
+give p>0. Substitution preserves nonnegativity because the relevant
+off-diagonal entries are nonpositive. Thus Bp=p-1<p. In particular
+q=max_i (Bp)_i/p_i is rational and belongs to [0,1). The same substitutions
+give u>=0 from Mu=beta.
+
+If the first nonpositive pivot is at k, set v_k=1 and v_i=0 for i>k, then
+back-substitute the first k homogeneous equations. All v_i are nonnegative.
+The first k rows of Mv are zero. The remaining rows of Mv are nonpositive.
+To see the latter in the original rows, every earlier elimination step only
+added a multiple of a row whose value on v is zero. In the reduced rows,
+row k has its nonpositive pivot and every later row has a nonpositive
+coefficient in column k. Hence Mv<=0, so Bv>=v.
+
+The alternatives are exclusive. If p>0 and Bp<p while v>=0 is nonzero and
+Bv>=v, take t=max_i v_i/p_i>0. At an index attaining the maximum,
+(Bv)_i<=t(Bp)_i<t p_i=v_i, a contradiction.
+
+The small-matrix verification uses a separate principal-minor criterion.
+All principal minors of I-B are positive exactly in the positive alternative.
+In one direction, positive leading minors give positive Gaussian pivots.
+In the other, any principal submatrix inherits strict contraction weights
+by restriction. Its negative alternative is impossible by the same maximum
+ratio argument, so all its pivots and its determinant are positive. Computing
+these minors by permutation expansion is independent of the producer's
+elimination implementation. Cramer's rule then independently computes each
+finite observed total.
+
+## Finite bill and exact tail
+
+The weighted maximum norm with weights p contracts under B by q<1.
+Consequently sum B^k beta converges and equals the unique solution u of
+u=Bu+beta. The identity for the tail follows by factoring out B^K.
+Since 0<=u<=alpha p, monotonicity gives
+B^K u<=alpha B^K p<=alpha q^K p, proving the tail bound.
+
+This proof also covers q=0, using q^0=1.
+
+## Observable divergence certificate
+
+Suppose the classical alternative gives v>=0, v!=0 and Bv>=v, possibly
+with gamma^T v=0. The sequence B^j v is coordinatewise nondecreasing.
+Since w>0 and v is nonzero, gamma^T B^s v>0 for some 0<=s<=r-1.
+Replace v by B^(r-1)v. This preserves nonnegativity and Bv>=v, and makes
+gamma^T v>0. All entries remain rational.
+
+Because z>0, the defined delta is positive and z>=delta v. For each integer
+m>=0,
+
+\[
+\begin{aligned}
+\sum_{t=0}^{r-1}a_{mr+t}
+ &=\gamma^T B^{mr}z\\
+ &\ge\delta\gamma^T B^{mr}v\\
+ &\ge\delta\gamma^T v=h.
+\end{aligned}
+\]
+
+There are floor(N/r) disjoint complete windows in the first N terms.
+All remaining terms are nonnegative. Summing gives the stated lower bound,
+and therefore divergence. This proves necessity of the positive alternative
+for finiteness as well as sufficiency.
+
+## Sharpness
+
+For every r>=1 take the directed r-cycle, with unit edge weights. In matrix
+notation B e_j=e_((j+1) mod r). Set beta=e_0 and gamma=e_(r-1). Then
+
+\[
+a_k=1\ \Longleftrightarrow\ k\equiv r-1\pmod r,
+\qquad S_N=\lfloor N/r\rfloor.
+\]
+
+The certificate v=1 has z=1, delta=1 and h=1. The lower bound is an equality
+at every N. For any integer window L<r, S_L=0, so no bound
+S_N>=floor(N/L)h' with h'>0 can hold for this example at every N.
+
+## What the extension changes
+
+The #5785 whole-matrix alternative certifies or excludes a global strict
+contraction. It explicitly warns that zero or unreachable forcing can miss
+a bad component. Here the exact object being decided is the specified
+scalar input/output bill. The path intersection is sufficient and necessary;
+an unstable component outside it may be both forced and harmless to that
+particular output. The new quantitative witness converts an applicable
+noncontraction alternative into an observable divergent bill, with a sharp
+universal depth window.
+
+Classical nonnegative matrix, path expansion and M-matrix theory underlie
+the proof. The contribution is this explicit output-specific contract and
+its finite-depth certificate in the repository's budget setting. It is not
+a claim of new general Perron-Frobenius theory.
+
+If A is only a componentwise upper bound for actual costs, the finite
+alternative supplies a sufficient upper bound. The divergent alternative
+does not disprove the actual caller in that case. A negative conclusion
+needs an exact recurrence or a justified componentwise lower bound, together
+with compatible forcing and observed-cost inequalities. An omitted real
+adapter or restoration cost cannot be assigned c_i=0 merely to pass this test.

research/observable-forced-recurrence/README.md

@@ -0,0 +1,127 @@
+# Exact observed coupled bills
+
+This package proves a scoped mathematical result with exact finite
+corroboration. For a nonnegative rational recurrence, the specified scalar
+bill can converge even when the full coupling matrix fails contraction.
+It suffices, and is necessary, to test the vertices on a path from the
+forcing to an observed cost.
+
+For A>=0, b>=0, c>=0, let H contain exactly those vertices and set
+B=A[H,H], beta=b[H], gamma=c[H], r=|H|. The result is
+
+```text
+sum c^T A^k b is finite
+  iff H is empty or B admits positive strict contraction weights.
+
+otherwise an exact rational observable witness gives, for every N>=0,
+  sum_(k<N) c^T A^k b >= floor(N/r) h, with h>0.
+
+An r-cycle attains equality at every N. The universal window r is sharp.
+```
+
+[PROOF.md](PROOF.md) gives the path reduction, constructive alternatives,
+exact finite total, geometric tail bound and sharpness proof.
+[model.py](model.py) implements a bounded reference producer and separate
+checker. The checker uses graph closure and matrix-vector identities, with
+no linear solve or elimination.
+
+## Relation to the predecessor
+
+Ali Romman's [PR #5785](https://github.com/CrocSwap/integer-mult-bounds/pull/5785),
+head `c047cb85ff5957f09afdcad3a8b16b637fbb5380`, provides the whole-matrix
+M-matrix alternative and states the forcing/reachability gap. This package
+extends that boundary to a specified observed bill and supplies a positive
+finite-depth divergence certificate when the obstruction is applicable.
+It does not recheck the predecessor's fixture, implementation or counts.
+The proof includes the classical alternative so replay has no unmerged Git
+dependency. The predecessor link is a scholarly citation, not a runtime input.
+
+The source question is the forcing/reachability gap in #5785. Classical
+M-matrix and nonnegative matrix theory retain their mathematical credit.
+The application and certificate contract here do not claim a new
+Perron-Frobenius theorem.
+
+## Reproduce
+
+From the repository root, run
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B research/observable-forced-recurrence/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/observable-forced-recurrence
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/observable-forced-recurrence --check-source-history
+```
+
+The verifier prints a generated JSON receipt bound to every package file's
+SHA-256. Redirect it outside the checkout if retaining it. CPython 3.12 and
+the standard library suffice. The registered normal and optimized commands
+perform the same checks; no network, predecessor code or external solver is used.
+
+The exact census covers all 4,096 two-type cases with matrix entries in
+{0,1/2,1,2} and binary forcing/output vectors, and all 32,768 three-type cases
+with binary matrices and binary forcing/output vectors. A separate
+permutation-determinant oracle checks the principal-minor criterion, and
+Cramer's rule independently checks every finite total. Additional fixtures
+check hidden unstable components, exact tails, divergence bounds and critical
+cycle sharpness. Forged-certificate and input-boundary controls remain active
+under optimized execution. The receipt reports the enumerated outcomes.
+Every census case also compares the first seven literal full-matrix terms
+with the restricted terms and checks the corresponding prefix bound.
+
+## Scope and limitations
+
+The written proof holds in every finite dimension. The reference code accepts
+one to eight types and nonnegative rational input parts of at most 16 bits.
+It is a reference certificate implementation, not a complexity or performance
+claim. Its exact finite census corroborates the proof; it does not substitute
+for the quantified argument. Independent human and formal proof-kernel review
+are unclaimed.
+
+No complete source recurrence has been bound, and no supplier, native action,
+compiler, restoration, stock, precision, tape or outer theorem is admitted.
+An unstable upper-bound matrix cannot by itself disprove an actual caller.
+No new kappa or selected-frontier change is claimed.
+
+The task's generic baseline binding control passed at canonical main
+`de5ec2e7a6074068452f45b1a191b5c72832df4a`, priority revision 8.
+This is an explicit change from the decoder card's physical itinerary to an
+analytical budget lemma. It can prevent an invalid negative inference from
+an irrelevant unstable block and can certify an actual observed divergence.
+Binding every real child, adapter and restoration cost is still required.
+
+## Open next questions
+
+1. Bind one complete source recurrence, its forcing and every genuinely billed
+   output to this criterion. Begin with a declared type graph and justify
+   each nonnegative coefficient and cost. Missing source/cost bounds are the
+   blocker; an abstract passing certificate is not a supplier result.
+2. For a divergent observed bill, determine its exact polynomial or exponential
+   growth rather than the universal linear lower bound. Begin with a chain
+   of critical strongly connected components. No such growth classification
+   is proved here.
+
+## Implementation bounds
+
+All matrix loops have the explicit eight-type bound. The exhaustive verifier
+fixes dimensions two and three. There is no recursion, dynamic evaluation,
+network access or subprocess creation. Functions stay below 60 physical lines.
+Checks use explicit exceptions so optimization does not remove them.
+
+Power-of-Ten rule 3 has a managed-runtime deviation: Python allocates Fraction
+and container objects during arithmetic. The scope is this finite reference
+replay. Enforced type/input bounds and fixed census grids bound live state;
+no census history is retained. The checker caps certificate vector parts at
+8,192 bits. Static inspection and both registered replays check these controls.
+A fixed-capacity arithmetic backend is a follow-up only if this becomes a
+production implementation. Rule 9's test callbacks have exactly one of the
+16 explicit rejection calls as their target and do not escape the verifier.
+The registered warning-as-error runs supply the interpreted diagnostics.
+
+## Credit
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+The question and whole-matrix alternative come from Ali Romman #5785.
+The classical M-matrix, nonnegative-matrix, path-expansion and Cramer's-rule
+ingredients retain their prior mathematical credit. #5785's historical fixture
+credits Nick Petalas, Ali Romman, David Ganz / Dugongue, Jose Manuel and their
+retained predecessor lineage; that fixture is not an input to this package.

research/observable-forced-recurrence/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "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"
+    }
+  ]
+}