diff --git a/research/observable-forced-recurrence/PROOF.md b/research/observable-forced-recurrence/PROOF.md
new file mode 100644
index 0000000000..478a3acff8
--- /dev/null
+++ b/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.
diff --git a/research/observable-forced-recurrence/README.md b/research/observable-forced-recurrence/README.md
new file mode 100644
index 0000000000..502d64b446
--- /dev/null
+++ b/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.
diff --git a/research/observable-forced-recurrence/SOURCES.json b/research/observable-forced-recurrence/SOURCES.json
new file mode 100644
index 0000000000..fdb80ada25
--- /dev/null
+++ b/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"
+    }
+  ]
+}
diff --git a/research/observable-forced-recurrence/TASK.json b/research/observable-forced-recurrence/TASK.json
new file mode 100644
index 0000000000..1aef81b220
--- /dev/null
+++ b/research/observable-forced-recurrence/TASK.json
@@ -0,0 +1,89 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-rank-shape-decoder",
+  "priority_revision": 8,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "original_card": {
+    "id": "complex-rank-shape-decoder",
+    "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+      "docs/research/recursive-invoice-preflight.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "coframe",
+      "signed moment",
+      "5693",
+      "5698"
+    ],
+    "existing_checks": [
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Exact convergence and sharp finite-depth divergence certificates for the specified nonnegative scalar bill sum c^T A^k b.",
+  "scope_change_reason": "Replace a physical decoder itinerary by the forcing/reachability gap in PR #5785. This is a source-independent analytical budget lemma, not a new supplier.",
+  "bottleneck_link": "Complete coupled budgets must distinguish globally unstable blocks from blocks both activated by the declared forcing and observable in the actual bill. The new criterion and quantitative obstruction apply only after all real costs are included.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship this first scoped theorem after its exact census and rejection controls pass; do not extend to source integration or a general growth classification.",
+  "outcome": "completed",
+  "evidence": "PROOF.md; model.py; verify.py generated receipt, exact principal-minor and Cramer oracles, sharp critical cycles, tails and semantic controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Bind one complete source recurrence and its actual forcing and observed bill.",
+      "why_it_matters": "An abstract certificate does not cover omitted children, adapters or restoration.",
+      "first_step": "Write the type graph and justify every nonnegative matrix coefficient and cost.",
+      "blocked_by": "No complete source recurrence or cost bound is supplied here."
+    },
+    {
+      "question": "Classify exact growth of divergent observed bills.",
+      "why_it_matters": "The universal linear lower bound need not identify polynomial degree or exponential rate.",
+      "first_step": "Study a chain of critical strongly connected components.",
+      "blocked_by": "Critical-component growth and periodicity are outside this proof."
+    }
+  ],
+  "predecessors": [
+    {
+      "pr": 5785,
+      "head": "c047cb85ff5957f09afdcad3a8b16b637fbb5380",
+      "role": "Question source and classical whole-matrix alternative; citation only, no runtime dependency."
+    }
+  ],
+  "claim_type": "scoped mathematical proof with exact finite corroboration"
+}
diff --git a/research/observable-forced-recurrence/VERIFY.json b/research/observable-forced-recurrence/VERIFY.json
new file mode 100644
index 0000000000..6a953d90f6
--- /dev/null
+++ b/research/observable-forced-recurrence/VERIFY.json
@@ -0,0 +1,32 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 240,
+      "checks": "Exact observed-bill reduction, 36,864 enumerated cases, independent determinant/Cramer oracles, tails, sharp cycles and explicit rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 240,
+      "checks": "The same exact mathematical and rejection checks with assertions disabled."
+    }
+  ]
+}
diff --git a/research/observable-forced-recurrence/model.py b/research/observable-forced-recurrence/model.py
new file mode 100644
index 0000000000..66ef43ab04
--- /dev/null
+++ b/research/observable-forced-recurrence/model.py
@@ -0,0 +1,222 @@
+"""Exact reference certificates for an observed nonnegative recurrence.
+
+The mathematical statement has arbitrary finite dimension. This reference
+implementation accepts at most eight types and 16-bit rational input parts.
+"""
+
+from dataclasses import dataclass
+from fractions import Fraction
+
+Vector = tuple[Fraction, ...]
+Matrix = tuple[Vector, ...]
+MAX_TYPES = 8
+INPUT_BITS = 16
+
+
+def require(condition: bool, message: str) -> None:
+    if not condition:
+        raise ValueError(message)
+
+
+def dot(left: Vector, right: Vector) -> Fraction:
+    require(len(left) == len(right) <= MAX_TYPES, "dot dimensions")
+    return sum((x * y for x, y in zip(left, right)), Fraction(0))
+
+
+def multiply(matrix: Matrix, vector: Vector) -> Vector:
+    return tuple(dot(row, vector) for row in matrix)
+
+
+def validate(matrix: Matrix, forcing: Vector, costs: Vector) -> None:
+    size = len(matrix)
+    require(1 <= size <= MAX_TYPES, "type capacity")
+    require(len(forcing) == len(costs) == size, "vector dimensions")
+    require(all(len(row) == size for row in matrix), "square matrix")
+    entries = tuple(x for row in matrix for x in row) + forcing + costs
+    for value in entries:
+        require(isinstance(value, Fraction), "exact rational inputs required")
+        require(value >= 0, "nonnegative inputs required")
+        require(value.numerator.bit_length() <= INPUT_BITS, "numerator capacity")
+        require(value.denominator.bit_length() <= INPUT_BITS, "denominator capacity")
+
+
+def relevant(matrix: Matrix, forcing: Vector, costs: Vector) -> tuple[int, ...]:
+    """Forward and backward closure, with edge j -> i for matrix[i][j]>0."""
+    size = len(matrix)
+    forward = {i for i in range(size) if forcing[i] > 0}
+    backward = {i for i in range(size) if costs[i] > 0}
+    for _ in range(size):
+        forward |= {i for i in range(size)
+                    if any(matrix[i][j] > 0 for j in forward)}
+        backward |= {j for j in range(size)
+                     if any(matrix[i][j] > 0 for i in backward)}
+    return tuple(sorted(forward & backward))
+
+
+def closure_relevant(matrix: Matrix, forcing: Vector, costs: Vector) -> tuple[int, ...]:
+    """Checker's independent all-pairs reachability implementation."""
+    size = len(matrix)
+    paths = [[i == j or matrix[i][j] > 0 for j in range(size)]
+             for i in range(size)]
+    for middle in range(size):
+        for end in range(size):
+            for start in range(size):
+                paths[end][start] |= paths[end][middle] and paths[middle][start]
+    return tuple(i for i in range(size)
+                 if any(forcing[j] > 0 and paths[i][j] for j in range(size))
+                 and any(costs[j] > 0 and paths[j][i] for j in range(size)))
+
+
+def restrict(matrix: Matrix, vector: Vector, indices: tuple[int, ...]) -> tuple[Matrix, Vector]:
+    return (tuple(tuple(matrix[i][j] for j in indices) for i in indices),
+            tuple(vector[i] for i in indices))
+
+
+def identity_minus(matrix: Matrix) -> Matrix:
+    return tuple(tuple(Fraction(i == j) - value for j, value in enumerate(row))
+                 for i, row in enumerate(matrix))
+
+
+def back_substitute(upper: list[list[Fraction]], rhs: list[Fraction]) -> Vector:
+    size = len(rhs)
+    result = [Fraction(0)] * size
+    for i in reversed(range(size)):
+        require(upper[i][i] != 0, "nonzero pivot")
+        result[i] = (rhs[i] - sum(upper[i][j] * result[j]
+                                  for j in range(i + 1, size))) / upper[i][i]
+    return tuple(result)
+
+
+def alternative(matrix: Matrix) -> tuple[bool, Vector]:
+    """Classical sign-preserving M-matrix alternative, credited in PROOF.md."""
+    size = len(matrix)
+    upper = [list(row) for row in identity_minus(matrix)]
+    rhs = [Fraction(1)] * size
+    for pivot in range(size):
+        if upper[pivot][pivot] <= 0:
+            witness = [Fraction(0)] * size
+            witness[pivot] = Fraction(1)
+            for i in reversed(range(pivot)):
+                witness[i] = -sum(upper[i][j] * witness[j]
+                                  for j in range(i + 1, pivot + 1)) / upper[i][i]
+            return False, tuple(witness)
+        for i in range(pivot + 1, size):
+            factor = upper[i][pivot] / upper[pivot][pivot]
+            for j in range(pivot, size):
+                upper[i][j] -= factor * upper[pivot][j]
+            rhs[i] -= factor * rhs[pivot]
+    return True, back_substitute(upper, rhs)
+
+
+def solve(matrix: Matrix, rhs: Vector) -> Vector:
+    size = len(rhs)
+    upper = [list(row) for row in matrix]
+    values = list(rhs)
+    for k in range(size):
+        pivot = next((i for i in range(k, size) if upper[i][k] != 0), None)
+        require(pivot is not None, "invertible finite system")
+        upper[k], upper[pivot] = upper[pivot], upper[k]
+        values[k], values[pivot] = values[pivot], values[k]
+        for i in range(k + 1, size):
+            factor = upper[i][k] / upper[k][k]
+            for j in range(k, size):
+                upper[i][j] -= factor * upper[k][j]
+            values[i] -= factor * values[k]
+    return back_substitute(upper, values)
+
+
+@dataclass(frozen=True)
+class Zero:
+    retained: tuple[int, ...] = ()
+
+
+@dataclass(frozen=True)
+class Finite:
+    retained: tuple[int, ...]
+    weights: Vector
+    total: Vector
+    ratio: Fraction
+
+
+@dataclass(frozen=True)
+class Divergent:
+    retained: tuple[int, ...]
+    witness: Vector
+    block_gain: Fraction
+
+
+Certificate = Zero | Finite | Divergent
+
+
+def activation(matrix: Matrix, forcing: Vector) -> Vector:
+    result = (Fraction(0),) * len(forcing)
+    term = forcing
+    for _ in range(len(forcing)):
+        result = tuple(x + y for x, y in zip(result, term))
+        term = multiply(matrix, term)
+    return result
+
+
+def certify(matrix: Matrix, forcing: Vector, costs: Vector) -> Certificate:
+    validate(matrix, forcing, costs)
+    kept = relevant(matrix, forcing, costs)
+    if not kept:
+        return Zero()
+    reduced, beta = restrict(matrix, forcing, kept)
+    gamma = tuple(costs[i] for i in kept)
+    finite, vector = alternative(reduced)
+    if finite:
+        weights = vector
+        ratio = max(x / y for x, y in zip(multiply(reduced, weights), weights))
+        total = solve(identity_minus(reduced), beta)
+        return Finite(kept, weights, total, ratio)
+    for _ in range(len(kept) - 1):
+        vector = multiply(reduced, vector)
+    z = activation(reduced, beta)
+    delta = min(x / y for x, y in zip(z, vector) if y > 0)
+    return Divergent(kept, vector, delta * dot(gamma, vector))
+
+
+def check_vector(vector: Vector, size: int, positive: bool = False) -> None:
+    require(len(vector) == size, "certificate vector dimensions")
+    for value in vector:
+        require(isinstance(value, Fraction), "rational certificate vector")
+        require(value > 0 if positive else value >= 0, "certificate vector sign")
+        require(max(value.numerator.bit_length(), value.denominator.bit_length())
+                <= 8192, "certificate arithmetic capacity")
+
+
+def check(matrix: Matrix, forcing: Vector, costs: Vector, cert: Certificate) -> None:
+    """Verify using only graph closure and matrix-vector arithmetic, no solve."""
+    validate(matrix, forcing, costs)
+    kept = closure_relevant(matrix, forcing, costs)
+    require(cert.retained == kept, "exact input-output support")
+    if not kept:
+        require(isinstance(cert, Zero), "zero certificate type")
+        return
+    reduced, beta = restrict(matrix, forcing, kept)
+    gamma = tuple(costs[i] for i in kept)
+    size = len(kept)
+    if isinstance(cert, Finite):
+        check_vector(cert.weights, size, positive=True)
+        check_vector(cert.total, size)
+        require(isinstance(cert.ratio, Fraction) and 0 <= cert.ratio < 1,
+                "strict rational contraction")
+        require(all(x <= cert.ratio * y for x, y in
+                    zip(multiply(reduced, cert.weights), cert.weights)),
+                "contraction inequality")
+        fixed = tuple(x + y for x, y in zip(multiply(reduced, cert.total), beta))
+        require(fixed == cert.total, "total fixed point")
+        return
+    require(isinstance(cert, Divergent), "nonempty certificate type")
+    check_vector(cert.witness, size)
+    require(any(cert.witness), "nonzero subeigenvector")
+    require(all(x >= y for x, y in zip(multiply(reduced, cert.witness), cert.witness)),
+            "subeigenvector inequality")
+    require(dot(gamma, cert.witness) > 0, "observable subeigenvector")
+    z = activation(reduced, beta)
+    require(all(value > 0 for value in z), "positive reachable activation")
+    delta = min(x / y for x, y in zip(z, cert.witness) if y > 0)
+    require(isinstance(cert.block_gain, Fraction) and cert.block_gain > 0,
+            "positive rational block gain")
+    require(cert.block_gain == delta * dot(gamma, cert.witness), "exact block gain")
diff --git a/research/observable-forced-recurrence/verify.py b/research/observable-forced-recurrence/verify.py
new file mode 100644
index 0000000000..64721c8a82
--- /dev/null
+++ b/research/observable-forced-recurrence/verify.py
@@ -0,0 +1,230 @@
+#!/usr/bin/env python3
+"""Enumerate new input/output reductions and exact certificate controls."""
+
+import hashlib
+import itertools
+import json
+import platform
+import sys
+from dataclasses import replace
+from fractions import Fraction
+from pathlib import Path
+
+from model import (Divergent, Finite, Zero, certify, check, closure_relevant,
+                   dot, identity_minus, multiply, require, restrict)
+
+
+def matrix(rows):
+    return tuple(tuple(Fraction(value) for value in row) for row in rows)
+
+
+def vector(values):
+    return tuple(Fraction(value) for value in values)
+
+
+def determinant(rows):
+    """Independent permutation formula, only used for orders at most three."""
+    size = len(rows)
+    require(size <= 3, "determinant oracle capacity")
+    result = Fraction(0)
+    for permutation in itertools.permutations(range(size)):
+        inversions = sum(permutation[i] > permutation[j]
+                         for i in range(size) for j in range(i + 1, size))
+        term = Fraction((-1) ** inversions)
+        for i in range(size):
+            term *= rows[i][permutation[i]]
+        result += term
+    return result
+
+
+def finite_oracle(a, b, c):
+    kept = closure_relevant(a, b, c)
+    reduced, _ = restrict(a, b, kept)
+    m = identity_minus(reduced)
+    for mask in range(1, 1 << len(kept)):
+        indices = tuple(i for i in range(len(kept)) if mask & (1 << i))
+        minor = tuple(tuple(m[i][j] for j in indices) for i in indices)
+        if determinant(minor) <= 0:
+            return False
+    return True
+
+
+def cramer_total(a, b, c, cert):
+    reduced, beta = restrict(a, b, cert.retained)
+    gamma = tuple(c[i] for i in cert.retained)
+    m = identity_minus(reduced)
+    denominator = determinant(m)
+    values = []
+    for column in range(len(m)):
+        replaced = tuple(tuple(beta[i] if j == column else m[i][j]
+                               for j in range(len(m))) for i in range(len(m)))
+        values.append(determinant(replaced) / denominator)
+    require(dot(gamma, tuple(values)) == dot(gamma, cert.total), "Cramer total")
+
+
+def path_and_prefix_checks(a, b, c, cert):
+    reduced, term = restrict(a, b, cert.retained)
+    gamma = tuple(c[i] for i in cert.retained)
+    full = b
+    prefix = Fraction(0)
+    for depth in range(7):
+        value = dot(c, full)
+        require(value == dot(gamma, term), "literal path reduction")
+        prefix += value
+        if isinstance(cert, Divergent):
+            require(prefix >= ((depth + 1) // len(cert.retained)) * cert.block_gain,
+                    "exhaustive finite-depth lower bound")
+        elif isinstance(cert, Finite):
+            require(prefix <= dot(gamma, cert.total), "observed finite prefix")
+        full = multiply(a, full)
+        term = multiply(reduced, term)
+
+
+def census(size, alphabet):
+    require(size in (2, 3) and 1 <= len(alphabet) <= 4, "census capacity")
+    counts = {"zero": 0, "finite": 0, "divergent": 0}
+    masks = tuple(vector((mask >> i) & 1 for i in range(size))
+                  for mask in range(1 << size))
+    for entries in itertools.product(alphabet, repeat=size * size):
+        a = matrix(tuple(entries[size * i:size * (i + 1)] for i in range(size)))
+        for b, c in itertools.product(masks, repeat=2):
+            cert = certify(a, b, c)
+            check(a, b, c, cert)
+            path_and_prefix_checks(a, b, c, cert)
+            finite = finite_oracle(a, b, c)
+            require(finite == (not isinstance(cert, Divergent)), "minor oracle")
+            if isinstance(cert, Zero):
+                counts["zero"] += 1
+            elif isinstance(cert, Finite):
+                cramer_total(a, b, c, cert)
+                counts["finite"] += 1
+            else:
+                counts["divergent"] += 1
+    require(sum(counts.values()) == len(alphabet) ** (size * size) * 4 ** size,
+            "exhaustive census size")
+    return counts
+
+
+def partial(a, b, c, depth):
+    term = b
+    total = Fraction(0)
+    for _ in range(depth):
+        total += dot(c, term)
+        term = multiply(a, term)
+    return total
+
+
+def examples():
+    fixtures = (
+        (matrix(((Fraction(1, 2), 0), (0, 2))), vector((1, 1)), vector((1, 0))),
+        (matrix(((2, 0), (0, Fraction(1, 2)))), vector((0, 1)), vector((1, 1))),
+        (matrix(((0, 0, 0), (1, 1, 0), (0, 1, 0))), vector((1, 0, 0)), vector((0, 0, 1))),
+        (matrix(((0, 0), (1, 0))), vector((1, 0)), vector((0, 1))),
+    )
+    for index, (a, b, c) in enumerate(fixtures):
+        cert = certify(a, b, c)
+        check(a, b, c, cert)
+        if index < 2:
+            require(isinstance(cert, Finite), "irrelevant unstable component")
+            require(len(cert.retained) == 1 and dot(vector((1,)), cert.total) == 2,
+                    "exact observed total two")
+        for depth in range(25):
+            observed = partial(a, b, c, depth)
+            if isinstance(cert, Divergent):
+                require(observed >= (depth // len(cert.retained)) * cert.block_gain,
+                        "divergence bound")
+            elif isinstance(cert, Finite):
+                reduced, beta = restrict(a, b, cert.retained)
+                gamma = tuple(c[i] for i in cert.retained)
+                tail_vector = cert.total
+                for _ in range(depth):
+                    tail_vector = multiply(reduced, tail_vector)
+                tail = dot(gamma, cert.total) - observed
+                require(tail == dot(gamma, tail_vector), "exact tail identity")
+                alpha = max(x / y for x, y in zip(cert.total, cert.weights))
+                require(tail <= alpha * cert.ratio ** depth * dot(gamma, cert.weights),
+                        "geometric tail bound")
+    return len(fixtures)
+
+
+def cycles():
+    checked = 0
+    for size in range(1, 9):
+        a = matrix(tuple(tuple(int(i == (j + 1) % size) for j in range(size))
+                         for i in range(size)))
+        b = vector(int(i == 0) for i in range(size))
+        c = vector(int(i == size - 1) for i in range(size))
+        cert = certify(a, b, c)
+        check(a, b, c, cert)
+        require(isinstance(cert, Divergent) and cert.block_gain == 1,
+                "critical cycle block gain")
+        for depth in range(4 * size + 1):
+            require(partial(a, b, c, depth) == depth // size,
+                    "sharp all-depth cycle formula")
+            checked += 1
+    return {"cycles": 8, "depths": checked}
+
+
+def rejected(call):
+    try:
+        call()
+    except ValueError:
+        return
+    raise ValueError("forged certificate or invalid input accepted")
+
+
+def controls():
+    a = matrix(((Fraction(1, 2), 0), (0, 2)))
+    b, c = vector((1, 1)), vector((1, 0))
+    finite = certify(a, b, c)
+    require(isinstance(finite, Finite), "finite control fixture")
+    forged = (
+        Zero(), replace(finite, retained=(0, 1)),
+        replace(finite, weights=vector((0,))),
+        replace(finite, total=vector((3,))),
+        replace(finite, ratio=Fraction(1)),
+        replace(finite, ratio=Fraction(0)),
+        replace(finite, total=vector((-1,))),
+    )
+    for cert in forged:
+        rejected(lambda: check(a, b, c, cert))
+    d = matrix(((0, 0, 0), (1, 1, 0), (0, 1, 0)))
+    db, dc = vector((1, 0, 0)), vector((0, 0, 1))
+    divergent = certify(d, db, dc)
+    require(isinstance(divergent, Divergent), "divergent control fixture")
+    false = (
+        replace(divergent, witness=vector((0, 0, 0))),
+        replace(divergent, witness=vector((0, -1, 1))),
+        replace(divergent, witness=vector((0, 1, 0))),
+        replace(divergent, witness=vector((0, 0, 1))),
+        replace(divergent, block_gain=2 * divergent.block_gain),
+    )
+    for cert in false:
+        rejected(lambda: check(d, db, dc, cert))
+    rejected(lambda: certify(matrix(((-1,),)), vector((1,)), vector((1,))))
+    rejected(lambda: certify(matrix(((0,),)), vector((1, 0)), vector((1,))))
+    rejected(lambda: certify(matrix(((2 ** 16,),)), vector((1,)), vector((1,))))
+    rejected(lambda: certify(matrix(((0,) * 9,) * 9), vector((0,) * 9), vector((0,) * 9)))
+    return {"certificate_mutants": len(forged) + len(false), "input_rejections": 4}
+
+
+def main():
+    require(sys.version_info[:2] == (3, 12), "registered CPython 3.12 required")
+    result = {
+        "status": "PASS_OBSERVABLE_FORCED_RECURRENCE",
+        "claim_type": "scoped proof with exact finite corroboration",
+        "python": platform.python_version(),
+        "two_type_rational_census": census(2, (0, Fraction(1, 2), 1, 2)),
+        "three_type_binary_census": census(3, (0, 1)),
+        "tail_and_hidden_component_fixtures": examples(),
+        "sharpness": cycles(),
+        "controls": controls(),
+    }
+    package = Path(__file__).resolve().parent
+    result["files_sha256"] = {path.name: hashlib.sha256(path.read_bytes()).hexdigest()
+                              for path in sorted(package.iterdir()) if path.is_file()}
+    print(json.dumps(result, sort_keys=True, indent=2))
+
+
+if __name__ == "__main__":
+    main()