diff --git a/docs/ci-verification.md b/docs/ci-verification.md
index 006bf5a3d5..63ba3e9aa8 100644
--- a/docs/ci-verification.md
+++ b/docs/ci-verification.md
@@ -1,6 +1,23 @@
 # CI verification
 
-## Current selected-family replay: #5599
+## Current selected-family replay: #6030
+
+The [selected record](../certificates/selected-result.json) binds conditional
+κ = 0.003125804 to the [proof review](research/pr-intake-evidence/pr6030-audit/PROOF-REVIEW.md),
+[validation receipts](research/pr-intake-evidence/pr6030-audit/VALIDATION.json),
+and [explicit source closure](../certificates/frontier6030-source.json).
+`make frontier6030-verify` follows that source-bound selected replay. The review
+separates retained normal primary macOS/Linux evidence from fresh independent
+word/invoice/native, original caller, adapted caller and optimized primary checks.
+Consult its receipts for exact commands, source heads and limits; the #5599
+checkpoint below retains its own historical replay details.
+
+The five inherited framework assumptions remain. Neither the full uniform word
+nor a complete rounded multiplier is materialized. A source/metadata check is
+not an operator replay or a formal theorem proof. Routine research submissions
+do not need to rerun this selected-family replay.
+
+## Historical selected-family replay: #5599
 
 The [selected record](../certificates/selected-result.json) binds conditional
 κ = 0.00310045 to the [proof review](research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md)
diff --git a/docs/research/current-status.md b/docs/research/current-status.md
index a84ac12213..c49a245adc 100644
--- a/docs/research/current-status.md
+++ b/docs/research/current-status.md
@@ -1,6 +1,6 @@
 # Current reviewed status
 
-Selected conditional κ: **0.003125804 = 781451/250000000**, DreamingOfClouds'
+Selected conditional κ: **0.003125804** = 781451/250000000, DreamingOfClouds'
 PR6030 on the cumulative P104 construction. The complete caller counts 13,444
 productive fields and 66,834 paid calls. The saving is about 0.81775% above the
 preceding selected PR5599 claim 0.00310045.
diff --git a/research/odd-denominator-rounding-budget/README.md b/research/odd-denominator-rounding-budget/README.md
new file mode 100644
index 0000000000..b3fbcba1f3
--- /dev/null
+++ b/research/odd-denominator-rounding-budget/README.md
@@ -0,0 +1,205 @@
+# A bounded fair-bit cap cannot exactly round the denominator-13 inverse
+
+A stochastic extension of the retained denominator-13 inverse cannot use a
+hard cap of fair bits, always return a rounded integer, and remain exactly
+unbiased. A bounded sampler can instead accept a quantified bias or return
+an explicit failure. Both tradeoffs have sharp closed forms.
+
+There is an exact standalone sampler with expected draw count two, and that
+expectation is optimal. Its worst-case draw count is unbounded. A tempting
+bounded retry construction fails: cap that sampler at four bits, restart its
+unfinished branch, and the desired probability **1/13 becomes 1/15**.
+The correct exact conditional sampler needs abort probability at least **3/16**.
+
+This is a scoped arithmetic/randomness theorem and failed-construction analysis,
+not a new inverse implementation, native supplier or κ. The denominator-13
+service in the pinned source is deterministic; it does not claim the stochastic
+substitution tested here.
+
+## Source-relative changed contract
+
+[PR #5069](https://github.com/CrocSwap/integer-mult-bounds/pull/5069)'s physical
+inverse-coded pair uses the exact mode identity
+
+$$
+A=I-MM^T/4,\qquad M^TM=56I,\qquad A^{-1}=I-MM^T/52.
+$$
+
+In particular $A^{-1}M=-M/13$. Its retained
+[PR #5037](https://github.com/CrocSwap/integer-mult-bounds/pull/5037) grid kernel
+uses deterministic approximation and does not give reversible cleanup.
+The proposed change is to use unbiased stochastic grid rounding of a
+non-dyadic scalar value, motivated by
+[Nick Petalas](https://github.com/petalas)'s
+[PR #6026](https://github.com/CrocSwap/integer-mult-bounds/pull/6026) dyadic
+stochastic prefix and the coupled inverse ABI in
+[PR #6066](https://github.com/CrocSwap/integer-mult-bounds/pull/6066).
+
+For a scalar value whose fractional part is $a/b$, adjacent-grid stochastic
+rounding must choose the upper grid point with exactly that probability.
+The calibration $a/b=1/13$ tests a denominator intrinsic to the inverse, not a
+claim that every reached service operand has that fraction. Actual reachable
+residue classes and caller propagation still need a separate source-bound
+analysis. No defect in the deterministic predecessor is alleged.
+
+## Sharp finite-bit bias bound
+
+Fix coprime integers $0<a<b$, with odd $b>1$. A standalone algorithm has a
+fixed input, no free initial random state, and at most $R$ fresh independent
+fair bits. It may branch adaptively and stop early, but always returns zero
+or one. Pad every early termination with unused bits. It is now a function of
+exactly $N=2^R$ equally likely strings. Its success probability is $k/N$ for an
+integer $0\leq k\leq N$.
+
+Let $r$ be the remainder of $aN$ upon division by $b$. The best possible total
+variation error from the desired Bernoulli law is
+
+$$
+\boxed{\epsilon_R=\frac{\min(r,b-r)}{bN}>0.}
+$$
+
+Indeed the closest integer to $aN/b$ is one of its floor and ceiling, at distances
+$r/b$ and $(b-r)/b$. Choosing the corresponding number of successful bit strings
+attains the bound. Since $b$ is odd and $a,b$ are coprime, $r$ cannot be zero.
+The same lattice argument rules out an exactly unbiased integer-valued result
+even if nonadjacent output integers are allowed: its mean is still an integer
+divided by $N$.
+
+This is a theorem about a **hard** fair-bit cap. A non-fair primitive, an
+uncharged random reservoir, an explicit failure or an unbounded stopping time
+changes the hypotheses. It is not a lower bound on amortized randomness across
+an arbitrarily large batch.
+
+## Sharp abort bound with exact conditional output
+
+Now allow a third outcome, abort, but demand that the accepted zero/one result
+has exactly the desired law. Let $\alpha$ strings return one and $\beta$ return
+zero. Exact conditional probability requires
+
+$$
+\frac{\alpha}{\alpha+\beta}=\frac{a}{b}.
+$$
+
+Coprimality forces $\alpha=at$ and $\beta=(b-a)t$ for an integer $t$. Therefore
+at most $b\lfloor N/b\rfloor$ strings can be accepted, and
+
+$$
+\boxed{\delta_R=\frac{N-b\lfloor N/b\rfloor}{N}}
+$$
+
+is the smallest possible abort probability. It is attained by accepting that
+many full $b$-sized groups, partitioning each in the ratio $a:(b-a)$ and aborting
+the rest. If $N<b$, no positive acceptance probability is possible; the formula
+then gives abort probability one. Repeating a correct accepted-law block until
+success is exact, but its total worst-case draw count is unbounded.
+
+For probability $1/13$:
+
+| Fair-bit cap $R$ | Best unavoidable bias | Minimum abort for exact accepted law |
+|---:|---:|---:|
+| 4 | 3/208 | 3/16 |
+| 8 | 1/832 | 9/256 |
+| 12 | 1/53248 | 1/4096 |
+| 16 | 3/851968 | 3/65536 |
+
+Over all twelve nonzero residue probabilities $a/13$, the sharp worst-case
+best bias at cap $R$ is $6/(13\cdot2^R)$. Multiplication by $2^R$ permutes the
+nonzero residues modulo 13, so the largest distance to an integer is $6/13$.
+These are sampling-law bounds, not propagated native-output errors.
+
+## Exact two-draw expectation, and why naive retries change the law
+
+Compare an infinite uniform binary fraction with the binary expansion of
+$a/b$, stopping at the first unequal bit. Output one if the random bit is
+smaller and zero if it is larger. The threshold digits are generated exactly
+by integer residue doubling modulo $b$.
+
+Because the threshold is non-dyadic, exactly one binary prefix is unresolved
+at every depth $k$. Thus the probability of needing more than $k$ bits is
+$2^{-k}$, and
+
+$$
+E[T]=\sum_{k\geq0}2^{-k}=2.
+$$
+
+The sampler terminates with probability one, but not on the single infinite
+tape equal to the threshold expansion. Hence there is no finite worst-case
+bound or all-tape completion guarantee. Any exact almost-surely terminating
+standalone fair-bit sampler must leave at least one prefix unresolved at every
+depth: otherwise the success probability would be dyadic. Its expected draw
+count is consequently at least the same sum. The comparison sampler attains it.
+
+After a cap of $R$ bits, the comparison sampler has exactly one unresolved
+string. The accepted success count is $\lfloor aN/b\rfloor$, among $N-1$
+completed strings. Restarting on the unresolved string therefore samples
+
+$$
+\frac{\lfloor aN/b\rfloor}{N-1},
+$$
+
+which equals $a/b$ **if and only if** $b$ divides $N-1$. Necessity follows
+because $a(N-1)/b$ must be an integer; sufficiency follows by taking the floor
+of that integer plus $a/b$.
+
+For $a/b=1/13$ and $R=4$, there is one success, fourteen failures and one
+unfinished string. Repeated cap-and-retry returns one with probability $1/15$.
+An exact bounded conditional sampler must also reject two of those fourteen
+completed failures, reaching the optimal three aborts out of sixteen.
+This is the explicit failed construction, with its corrected resource choice.
+
+## Evidence and reproduction
+
+```
+python3.12 -B scripts/research_package.py --package research/odd-denominator-rounding-budget
+python3.12 -B scripts/check_research_commit.py --package research/odd-denominator-rounding-budget
+```
+
+The standalone verifier authenticates the source context, compares the sharp
+bias formula with every attainable integer success count on bounded odd
+probabilities, exhausts accepted/failure/abort count triples, independently
+enumerates literal fair-bit tapes against exact comparison trees, checks the
+capped-retry congruence and the denominator-13 table, and verifies the exact
+truncated expectation identity. No random sampling or floating point is used.
+Normal and optimized modes keep all checks active and write no package files.
+
+The written counting and stopping-time proofs are uniform; finite checks are
+corroboration, not a classification of every sampler implementation. No new
+physical inverse, stochastic service integration, precision/guard budget,
+reversible sampler, complete caller, selected replay or formal proof is supplied.
+The optional full-history check is unavailable in this shallow repository;
+all declared pins use its reachable base. The navigation repair from
+[PR #6050](https://github.com/CrocSwap/integer-mult-bounds/pull/6050) is included.
+Main was refreshed at 721c03822c421b7f7fcbb2598993b947c4d88419, priority 8,
+on 2026-10-28 UTC. Frozen inputs and the selected result remain unchanged.
+
+## Significance for researchers
+
+The finite fair-bit ABI of a dyadic stochastic prefix cannot simply be reused
+for an odd-denominator inverse. The complete design must choose and pay for
+bias, an explicit failure contract, or unbounded stopping. Expected two draws
+cannot be entered as a deterministic worst-case tariff, and truncation followed
+by retry does not generally preserve the desired stochastic law.
+
+## Open next questions
+
+Can the sharp bounded bias fit a concrete inverse caller's full error budget?
+First identify its reached residue classes and propagate their exact bias through
+the actual suffix. This package supplies neither that reachability proof nor
+an admissible precision saving.
+
+Can a variable-time sampler be hosted with a retained random tape, reversible
+cleanup and a complete runtime/stock contract? Start with the comparison loop
+modulo thirteen and its stopping record. Mean two draws alone does not supply
+bounded latency, tape movement or all-tape termination.
+
+## Credit
+
+Prepared by [zxv](https://github.com/zxv) with substantial OpenAI Codex assistance.
+[JoyboyBrian](https://github.com/JoyboyBrian)'s #5069/#5037 lineage supplies the
+retained denominator-13 inverse and deterministic grid context.
+[Nick Petalas](https://github.com/petalas)'s #6026 supplies the dyadic stochastic
+rounding comparison. Finite probability counting and binary comparison sampling
+are classical. The scoped contribution is the exact source-relative
+bias/abort/runtime decision and the failed capped-retry substitution here.
+Predecessor sources and attribution remain unchanged. Apache-2.0; no independent
+human or proof-assistant review is claimed.
diff --git a/research/odd-denominator-rounding-budget/SOURCES.json b/research/odd-denominator-rounding-budget/SOURCES.json
new file mode 100644
index 0000000000..519921dcc8
--- /dev/null
+++ b/research/odd-denominator-rounding-budget/SOURCES.json
@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "6ff6b63a4d5dea676f31a1771002eccf8e78b3c0",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/p104-stochastic-prefix/PROOF.md",
+      "usage": "input",
+      "git_blob": "0db45191676cb037fca76e7a781e02670fcc4078",
+      "sha256": "db1640be6eade5955320c106ef4d0666742c195560402d0067fa0ee3648bbeca"
+    },
+    {
+      "path": "research/physical-inverse-pair/README.md",
+      "usage": "input",
+      "git_blob": "a4ed4756eaa2e2e1fe3d91f2d8c7f1d682d8185b",
+      "sha256": "32505039ae7289b6358de5ec9d83a8bb63b76140209b521c7e8c82e8e0000783"
+    }
+  ]
+}
diff --git a/research/odd-denominator-rounding-budget/TASK.json b/research/odd-denominator-rounding-budget/TASK.json
new file mode 100644
index 0000000000..15600c8622
--- /dev/null
+++ b/research/odd-denominator-rounding-budget/TASK.json
@@ -0,0 +1,89 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 8,
+  "base_commit": "6ff6b63a4d5dea676f31a1771002eccf8e78b3c0",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?",
+    "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"
+    ],
+    "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": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.",
+    "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": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.",
+    "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": [
+      "native_all_columns",
+      "owned_erasure",
+      "compiler",
+      "precision_tape",
+      "analytic_recovery"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "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": "Sharp fair-bit bias/abort/expected-runtime bounds for a proposed stochastic denominator-13 inverse, including exact failure of capped binary-comparison retry.",
+  "scope_change_reason": "Broader lateral research changes the coefficient and randomness contract beyond the dyadic scalar prefix. The deterministic predecessor is not alleged defective.",
+  "bottleneck_link": "Prevents treating a finite dyadic sampler or an expected draw count as a complete exact odd-denominator inverse ABI.",
+  "budget_minutes": 15,
+  "stop_rule": "Stop after uniform counting/stopping proofs and exact bounded corroboration; no physical inverse integration campaign.",
+  "outcome": "completed",
+  "evidence": "README.md proofs and explicit 1/13 to 1/15 counterexample; verify.py exact lattice, abort and literal-tree checks.",
+  "author": "zxv (https://github.com/zxv), with substantial OpenAI Codex assistance",
+  "ai_assistance": "Substantial OpenAI Codex assistance.",
+  "open_questions": [
+    {
+      "question": "Can bounded sampler bias fit a source-bound inverse caller?",
+      "why_it_matters": "Could keep a bounded-time stochastic approximation route open.",
+      "first_step": "Prove reached residues and propagate their exact bias through the caller suffix.",
+      "blocked_by": "No actual caller reachability or error budget is supplied."
+    },
+    {
+      "question": "Can an exact variable-time sampler meet the caller tape and cleanup contract?",
+      "why_it_matters": "Expected two draws do not supply a deterministic complete tariff.",
+      "first_step": "Implement the comparison loop modulo thirteen with an explicit stopping record.",
+      "blocked_by": "No physical random-tape host or reversible variable-time cleanup."
+    }
+  ]
+}
diff --git a/research/odd-denominator-rounding-budget/VERIFY.json b/research/odd-denominator-rounding-budget/VERIFY.json
new file mode 100644
index 0000000000..7a01f7ce2f
--- /dev/null
+++ b/research/odd-denominator-rounding-budget/VERIFY.json
@@ -0,0 +1,33 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/p104-stochastic-prefix/PROOF.md",
+    "research/physical-inverse-pair/README.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exhaustive bounded fair-bit success counts, conditional abort triples, exact stopping trees and literal tapes, cap/retry congruence and rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Same exact checks with assertions disabled."
+    }
+  ]
+}
diff --git a/research/odd-denominator-rounding-budget/verify.py b/research/odd-denominator-rounding-budget/verify.py
new file mode 100644
index 0000000000..f8ead06c49
--- /dev/null
+++ b/research/odd-denominator-rounding-budget/verify.py
@@ -0,0 +1,139 @@
+"""Exact fair-bit budget tradeoffs for rational stochastic rounding. Apache-2.0."""
+from fractions import Fraction as Q
+from itertools import product
+from math import gcd
+from pathlib import Path
+import hashlib
+import json
+
+HERE=Path(__file__).resolve().parent
+ROOT=HERE.parents[1]
+
+
+def need(ok,msg):
+    if not ok:raise ValueError(msg)
+
+
+def bounds(a,b,r):
+    need(type(a) is int and type(b) is int and 0<a<b and b%2==1 and gcd(a,b)==1,'reduced odd-denominator interior probability')
+    need(type(r) is int and 0<=r<=16,'finite verification budget')
+    n=1<<r;res=(a*n)%b
+    return Q(min(res,b-res),b*n),Q(n%b,n)
+
+
+def tree(a,b,depth):
+    # Enumerate every fair-bit prefix, retaining all unresolved strings.
+    # Uniform binary comparison to a/b; exact integer residue recursion.
+    unresolved={():a};ones=zeros=0
+    for t in range(1,depth+1):
+        nxt={};ones*=2;zeros*=2
+        for prefix,rem in unresolved.items():
+            bit,newrem=divmod(2*rem,b)
+            need(newrem!=0,'nondyadic comparison remainder')
+            for coin in (0,1):
+                if coin<bit:ones+=1
+                elif coin>bit:zeros+=1
+                else:nxt[prefix+(coin,)]=newrem
+        unresolved=nxt
+        need(len(unresolved)==1,'exact one unresolved fair prefix')
+        need(ones+zeros+1==1<<t,'full stopping-tree mass')
+        need(Q(ones,1<<t)<Q(a,b)<Q(ones+1,1<<t),'exact unfinished success interval')
+    return ones,zeros,len(unresolved)
+
+
+def sample(a,b,bits):
+    rem=a
+    for i,coin in enumerate(bits):
+        need(coin in (0,1),'fair-bit value')
+        digit,rem=divmod(2*rem,b)
+        if coin<digit:return 1,i+1
+        if coin>digit:return 0,i+1
+    return None,len(bits)
+
+
+def rejected(fn):
+    try:fn()
+    except ValueError:return
+    raise ValueError('negative control accepted')
+
+
+def main():
+    pins=json.loads((HERE/'SOURCES.json').read_text())
+    for row in pins['files']:
+        if row['usage']=='input':
+            need(hashlib.sha256((ROOT/row['path']).read_bytes()).hexdigest()==row['sha256'],'source bytes')
+    lattice=0
+    for b in range(3,32,2):
+        for a in range(1,b):
+            if gcd(a,b)!=1:continue
+            for r in range(0,11):
+                n=1<<r;bias,abort=bounds(a,b,r)
+                # Independent exhaustive integer output-count oracle.
+                best=min(abs(k*b-a*n) for k in range(n+1))
+                need(bias==Q(best,b*n) and bias>0,'sharp bounded sampler bias')
+                need(abort==Q(n-b*(n//b),n) and abort>0,'sharp exact conditional abort')
+                lattice+=1
+    triples=0
+    for b in (3,5,7,9,11,13,15):
+        for a in range(1,b):
+            if gcd(a,b)!=1:continue
+            for r in range(0,6):
+                n=1<<r;accepted=0
+                for one in range(n+1):
+                    for zero in range(n-one+1):
+                        total=one+zero
+                        if total and b*one==a*total:
+                            need(total%b==0,'exact conditional count divisor')
+                            accepted=max(accepted,total)
+                        triples+=1
+                need(accepted==b*(n//b),'optimal accepted fair strings')
+    trees=0;literal=0
+    for b in range(3,20,2):
+        for a in range(1,b):
+            if gcd(a,b)!=1:continue
+            tree(a,b,16);trees+=1
+            one=zero=unresolved=0
+            for bits in product((0,1),repeat=8):
+                out,used=sample(a,b,bits)
+                if out==1:one+=1
+                elif out==0:zero+=1
+                else:unresolved+=1
+                need(1<=used<=8,'stopping length');literal+=1
+            want=tree(a,b,8)
+            need((one,zero,unresolved)==want,'literal full binary-tape oracle')
+    # Capping and retrying preserves the law only at the correct congruence.
+    for b in range(3,20,2):
+        for a in range(1,b):
+            if gcd(a,b)!=1:continue
+            for r in range(1,11):
+                one,zero,left=tree(a,b,r)
+                need((Q(one,one+zero)==Q(a,b))==(((1<<r)-1)%b==0),
+                     'exact capped-retry congruence')
+    one,zero,left=tree(1,13,4)
+    need((one,zero,left)==(1,14,1) and Q(one,one+zero)==Q(1,15),
+         'four-bit retry changes 1/13 to 1/15')
+    # Geometric stopping: E min(T,k)=2-2^(1-k), P(T>k)=2^-k.
+    for k in range(1,65):
+        need(sum((Q(1,1<<j) for j in range(k)),Q(0))==2-Q(1,1<<(k-1)),'exact truncated mean')
+    table={}
+    for r in (4,8,12,16):
+        bias,abort=bounds(1,13,r)
+        table[r]={'bias':str(bias),'abort':str(abort)}
+    need(table[4]=={'bias':'3/208','abort':'3/16'},'denominator-13 four-bit fixture')
+    need(table[12]=={'bias':'1/53248','abort':'1/4096'},'denominator-13 twelve-bit fixture')
+    for r in range(0,17):
+        worst=max(bounds(a,13,r)[0] for a in range(1,13))
+        need(worst==Q(6,13*(1<<r)),'uniform residue worst bias')
+    rejected(lambda:need(bounds(1,13,12)[0]==0,'false bounded exact sampler'))
+    rejected(lambda:need(bounds(1,13,4)[1]<Q(3,16),'understated abort'))
+    rejected(lambda:bounds(2,6,4))
+    rejected(lambda:bounds(0,13,4))
+    rejected(lambda:bounds(1,13,17))
+    # A finite expected count cannot be used as a hard completion guarantee.
+    need(tree(1,13,16)[2]==1,'positive mass remains at every fixed depth')
+    print(json.dumps(dict(status='PASS_ODD_DENOMINATOR_ROUNDING_BUDGET',lattice_cases=lattice,
+                         conditional_count_triples=triples,comparison_trees=trees,literal_tapes=literal,
+                         denominator13=table,scope='sharp standalone sampler and capped-retry tradeoff; no inverse implementation or new kappa'),sort_keys=True))
+
+
+if __name__=='__main__':main()