diff --git a/research/acyclic-border-error/PROOF.md b/research/acyclic-border-error/PROOF.md
new file mode 100644
index 0000000000..8152b84a6f
--- /dev/null
+++ b/research/acyclic-border-error/PROOF.md
@@ -0,0 +1,129 @@
+# Bounded acyclic selectors retain their rank rows
+
+This is a scoped proof over the real or complex numbers. The rational program
+corroborates finite instances. No predecessor scientific executable is run.
+
+## 1. Sharp envelope
+
+Fix n>=2 and L>=1. Define
+
+    f(e) = e sum_{k=0}^{n-1} (1+L-e)^k.
+
+There is a unique a=a_n(L) in (0,1/n) with f(a)=1. For every complex
+n by n matrix A satisfying, in a single coordinate order,
+
+    |A_ii - 1| <= e,
+    |A_ij| <= L       if i<j,
+    |A_ij| <= e       if i>j,
+
+e<a implies rank A=n. The cutoff is sharp for this envelope. At e=a,
+the real matrix with diagonal 1-a, every upper entry -L and every lower
+entry -a has rank exactly n-1. For n=1 the cutoff is exactly one.
+
+On [0,1/n], put q=1+L-e>=1. Each summand in the derivative
+
+    f'(e) = sum_{k=0}^{n-1} q^k - e sum_{k=1}^{n-1} k q^{k-1}
+
+is positive, since q-ek>0. Also f(0)=0 and f(1/n)>1. On (1/n,1],
+f(e)>=ne>1. This proves existence and uniqueness in the stated interval.
+
+Let B have entry L above the diagonal and e on or below it. Set
+w_i=q^{n-1-i}, with indices starting at zero. Direct row subtraction gives
+
+    (I-B)w = (1-f(e)) 1.
+
+Thus w>0 and Bw<w when e<a. If Az=0 for nonzero z, choose i maximizing
+|z_i|/w_i=t>0. The hypotheses give
+
+    |z_i| = |((I-A)z)_i| <= t(Bw)_i < t w_i = |z_i|,
+
+a contradiction. Absolute values make this valid for complex entries.
+
+At e=a the displayed real matrix is I-B and has kernel vector w. Replace
+row i by old row i minus old row i+1 for i=0,...,n-2, leaving the last row
+unchanged. This determinant-one row transformation gives the independent
+first n-1 equations z_i-q z_{i+1}=0. The last becomes
+(1-f(e))z_{n-1}=0. Therefore det(I-B)=1-f(e), and its boundary rank
+is exactly n-1. This proves sharpness over the full directed triangular
+envelope. It does not assert that a symmetric P112 mask attains it.
+
+## 2. Rational attainment and growth
+
+For rational q>=2 and n>=2 set
+
+    S=sum_{k=0}^{n-1} q^k,   e=1/S,   L=q-1+e.
+
+All entries of I-B and its kernel vector are rational, L>=1, and f(e)=1.
+For n=8,q=2 this gives e=1/255, L=256/255 and rank seven. These are
+boundary fixtures, not P112 decoder constructions.
+
+At the cutoff q=1+L-a>1, the geometric-sum identity gives
+
+    a(1+L-a)^n=L,
+    L/(1+L)^n < a <= L^{-(n-1)},
+    a L^{n-1} -> 1 as L -> infinity, for fixed n.
+
+The bounds follow from L<=q<1+L; the limit follows from q/L->1.
+The exponent n-1 is therefore sharp. A simpler necessary condition for
+a singular matrix is e>=a>1/(2^n L^{n-1}). If e<=2^-p and L<=2^b,
+singularity requires p<n+(n-1)b. This is a magnitude constraint, not a
+physical precision or tape-cost theorem. The asymptotic assertion fixes n.
+
+## 3. Transfer to an approximate AGLB row
+
+DreamingOfClouds's PR5559, PROOF.md section 5, uses an acyclic generalized
+Lemma B, abbreviated AGLB. Retain its exact support, price and certificate
+statements as predecessors. We extend one rank row; we do not re-establish
+its enumerations, LP bounds or COPY64 claims.
+
+Let B0 be a zero-one mask with unit diagonal. Let J be a zero-one selector
+which is one on B0 and nonzero outside B0 only on directed acyclic arcs.
+Let the subtotal to which the row is applied be
+
+    M_paid=sum_{k=1}^m p_k q_k^T.
+
+Assume |(M_paid)_ij-delta_ij|<=e on B0 and |(M_paid)_ij|<=L on the
+extra selected arcs, with L>=1. A topological order puts those arcs above
+the diagonal. C=J Hadamard M_paid satisfies section 1, since e<a<=1<=L.
+Consequently, for e<a,
+
+    n = rank C
+      <= sum_k rank( diag(p_k) J diag(q_k) )
+       = sum_k rank J[supp p_k, supp q_k].
+
+These ranks are over the coefficient field, not F2. Exact supports justify
+the final equality, including empty supports. The same reasoning applies
+to each principal-subset row at its own dimension. A cost certificate using
+only these rows and inequalities valid independently of the exact decoder
+equations transfers when every rank row meets these hypotheses. Exact-only
+off-diagonal cover and coefficient-ratio clauses do not automatically
+transfer. This is a conditional rule, not a replay of any cost certificate.
+
+If zero-price terms are omitted in the exact argument, M_paid MUST be the
+subtotal after that omission. A final-total bound does not suffice. In the
+n=2 rational family above, adding L E_01, a free term for the directed
+diagonal-and-lower mask, cancels the large upper entry and leaves a bounded
+invertible lower triangular total. The paid subtotal is still singular and
+has magnitude L. This is a directed-mask example, not a P112 realization.
+
+If m is fixed and every factor entry has magnitude at most H, subtotal
+entries have magnitude at most m H^2. Take L=max(1,m H^2). A deficient
+AGLB row at error tending to zero forces unbounded factor magnitude.
+Once m H^2>=1 it requires
+
+    H > [1/(2^n e m^{n-1})]^{1/(2(n-1))}.
+
+No unrestricted border-cost floor, physical cost for these coefficients,
+native realization or new kappa follows.
+
+## 4. Prior mathematical methods
+
+Absolute-value comparison and scaled diagonal dominance are classical
+interval-matrix methods. See Jiri Rohn, *Forty necessary and sufficient
+conditions for regularity of interval matrices: a survey*, Electronic
+Journal of Linear Algebra 18 (2009), 500-512, especially Theorem 4.1(ii):
+https://journals.uwyo.edu/index.php/ela/article/view/655 . That theory retains
+credit. No general literature-priority claim is made for interval regularity.
+The contribution is this explicit envelope, its rational attainment and
+growth law, and the paid-subtotal transfer to decoder rank rows left outside
+PR5559's exact-only argument.
diff --git a/research/acyclic-border-error/README.md b/research/acyclic-border-error/README.md
new file mode 100644
index 0000000000..b43cea2b8f
--- /dev/null
+++ b/research/acyclic-border-error/README.md
@@ -0,0 +1,119 @@
+# A sharp error cutoff for bounded acyclic decoder rows
+
+Scoped proof with exact finite corroboration. No new kappa.
+
+For n>=2 and L>=1, define a_n(L) as the first positive root of
+
+    e sum_{k=0}^{n-1} (1+L-e)^k = 1.
+
+An n by n complex matrix whose diagonal error and lower entries have
+magnitude at most e, and whose upper entries have magnitude at most L,
+is nonsingular whenever e<a_n(L). An explicit real boundary matrix has
+rank n-1, so the envelope is sharp. Rational boundary examples exist for
+every n. The cutoff satisfies a_n(L) L^{n-1}->1 for fixed n as L grows.
+
+This extends the acyclic generalized Lemma B rank rows used in
+[DreamingOfClouds's PR5559](https://github.com/CrocSwap/integer-mult-bounds/pull/5559)
+to approximate masked decoders under a bound on the paid subtotal's selected
+unmasked entries. That package explicitly excludes border cost. Its exact
+decoder floors and computations are cited predecessors, not replay targets.
+
+For eight rows and L=1, the cutoff lies strictly between 1/256 and 1/250.
+A separate exact boundary has e=1/255, L=256/255 and rank seven.
+For a deficient row with error at most 2^-p and L<=2^b, necessarily
+p<n+(n-1)b. Unbounded coefficient growth can escape this obstruction.
+
+[PROOF.md](PROOF.md) gives the all-dimension argument, rational attaining
+family, factor-magnitude consequence and transfer contract. Sharpness is
+over directed triangular envelopes, not an asserted P112 decoder optimum.
+Bounds on the final decoder total cannot replace bounds on the paid
+subtotal. An exact example demonstrates cancellation by an omitted free term.
+
+## Reproduction
+
+From the repository root, with the Python 3.12 standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/acyclic-border-error/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/acyclic-border-error/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/acyclic-border-error
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/acyclic-border-error --check-source-history
+```
+
+Substitute another CPython 3.12 path elsewhere. Expected markers are
+`PASS_ACYCLIC_BORDER_ERROR`, `PASS_REGISTERED_RESEARCH_PACKAGE` and
+`PASS_RESEARCH_COMMIT_BYTES`. The standalone verifier has no network, Git,
+solver or dependency requirement. It writes only a generated JSON receipt
+and marker to stdout. The receipt hashes all seven package files.
+
+Finite evidence consists of 75 literal determinant identities, all 1,056
+real sign vertices of four two/three-dimensional boxes, 60 independently
+eliminated rational boundary matrices through dimension sixteen, 60 rejected
+wrap omissions and 15 named domain or semantic controls.
+These finite checks corroborate the written proof; they do not exhaust the
+complex matrix domain or constitute proof-kernel verification.
+
+## Scope and implementation bounds
+
+The actual selected record at base
+`7c49fe32c55de02c2c873655c804b16e4c3fef0a` reports conditional kappa
+0.003125804. The source-binding baseline passed; no selected scientific
+replay was run. TASK.json changes the `complex-rank-shape-decoder` card to
+this quantitative side result. SOURCES.json pins the original card,
+selected record and PR5559 proof as historical provenance. No predecessor
+scientific program is imported and no live external input is needed.
+
+The mathematical theorem allows arbitrary finite n and real L>=1. The
+certificate API limits n to 32, parameter numerator/denominator height to
+4096 bits, and bisection to 128 rounds. The fixed verifier uses n<=16,
+permutation determinants only through n=5, and sign enumeration only
+through n=3. Functions are below 60 lines; all loops have fixed or
+input-bounded domains. API domain violations raise ValueError. Exact
+internal assertions are corroborated by explicit checks that survive -O.
+
+Power of Ten rule 3 has a managed-runtime deviation in both Python files.
+Fraction and Python container allocations are dynamic. Input dimensions,
+heights, iteration limits and seven receipt inputs of at most 1 MiB bound
+live state. The largest sign box has 512 vertices, processed one at a time;
+matrices have at most 1024 entries. No child processes, callbacks, dynamic
+evaluation, global mutable state or persistent file writes occur.
+Normal/optimized warning-strict replay supplies interpreted-code diagnostics.
+No separate static analyzer is configured for this isolated package. A
+fixed-capacity implementation is a follow-up if these domains are expanded.
+
+No unrestricted border-cost floor, COPY64 theorem, P112 attaining decoder,
+complete paid invoice, native coefficient implementation, precision or tape
+cost, stock, restoration or supplier admission is claimed. The five selected
+framework assumptions remain. Independent human and formal proof-kernel
+review are unclaimed.
+
+## Open next questions
+
+1. Derive the sharper threshold for one actual P112 selector with its exact
+   zero cells. Start from its comparison matrix and a positive-weight
+   certificate. An actual paid-subtotal magnitude contract is still needed.
+2. Price a complete approximate decoder after the required factor growth.
+   Start with one native paid word and include coefficient delivery, rounding
+   and restoration. These physical obligations remain open.
+
+The structured questions and their relevance are in TASK.json.
+
+## Credit and overlap
+
+This contribution was produced by Nick Petalas. Credit DreamingOfClouds
+for PR5559's exact acyclic rank rows and explicit border-cost caveat, Cinna
+Davis for the P112 dictionary/decoder setting, and all predecessors retained
+there. Classical interval-matrix comparison and scaled diagonal dominance
+retain their credit; [Jiri Rohn's survey](https://journals.uwyo.edu/index.php/ela/article/view/655)
+records the general regularity framework. The explicit envelope and decoder
+transfer are the contribution here. No global literature-priority claim is
+made. Predecessor files and attribution are unchanged. Apache-2.0.
+
+Overlap checks covered live PR metadata and Discussion claims, local batch
+reservations, the card's cached overlap report, and distinctive Git searches
+over main's complete README inventory. The cache's sparse local-note coverage
+was incomplete; unpublished work and arbitrary historical code diffs remain
+outside the search. The
+[advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19440631)
+states the scope. No other checked result supplied this bounded approximate
+transfer. This observation is limited to the inspected coverage.
diff --git a/research/acyclic-border-error/SOURCES.json b/research/acyclic-border-error/SOURCES.json
new file mode 100644
index 0000000000..dbb7869082
--- /dev/null
+++ b/research/acyclic-border-error/SOURCES.json
@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "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/p112-decoder-wall-partial/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "92e1d713d9b8d83d801ddfa58598ca4308883e89",
+      "sha256": "6ad98192f34e68af9e07d6c405ffdcfa13924c24d23d131d104214a740bb39d4"
+    }
+  ]
+}
diff --git a/research/acyclic-border-error/TASK.json b/research/acyclic-border-error/TASK.json
new file mode 100644
index 0000000000..330922a3fd
--- /dev/null
+++ b/research/acyclic-border-error/TASK.json
@@ -0,0 +1,81 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-rank-shape-decoder",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "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": "A sharp universal triangular-envelope error cutoff, rational rank-deficient boundary family, coefficient-growth law, and conditional transfer of acyclic decoder rank rows to approximate paid subtotals.",
+  "scope_change_reason": "This side result addresses the exact-versus-border caveat of PR5559 rather than constructing a complete changed supplier or signed invoice.",
+  "bottleneck_link": "An approximate decoder cannot evade an AGLB rank row with bounded paid-subtotal magnitudes; escaping through growing coefficients creates a quantitative precision obligation.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first proved sharp envelope and its exact corroboration; do not extend to P112 synthesis or a broader search.",
+  "outcome": "completed",
+  "evidence": "PROOF.md and warning-strict normal/optimized standalone exact checks; generated stdout receipt binds all seven files.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "What sharper cutoff follows for one actual P112 acyclic selector, retaining all its zero cells?",
+      "why_it_matters": "The universal triangular envelope may overestimate the permitted free arcs and errors.",
+      "first_step": "Take one exact selector as an input and derive its nonnegative comparison matrix and a positive-weight certificate.",
+      "blocked_by": "The actual selector, paid-subtotal magnitude contract and physical coefficient bill must be supplied; no source floor is replayed here."
+    },
+    {
+      "question": "Can a complete approximate decoder profit after the necessary coefficient growth is priced?",
+      "why_it_matters": "A growing coefficient family alone is neither a free approximation nor a multiplication improvement.",
+      "first_step": "Construct one paid word and bound its actual subtotal, factor magnitudes, rounding and restoration costs.",
+      "blocked_by": "No native realization, compiler, precision, ownership or outer supplier admission is provided."
+    }
+  ]
+}
diff --git a/research/acyclic-border-error/VERIFY.json b/research/acyclic-border-error/VERIFY.json
new file mode 100644
index 0000000000..9fe9d3bf95
--- /dev/null
+++ b/research/acyclic-border-error/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": 120,
+      "checks": "Exact determinant/positive-weight identities, sign vertices, rank-deficient boundaries, corruptions and domain controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Repeat every finite mathematical and rejection check with assertions disabled."
+    }
+  ]
+}
diff --git a/research/acyclic-border-error/bounds.py b/research/acyclic-border-error/bounds.py
new file mode 100644
index 0000000000..f7feacac73
--- /dev/null
+++ b/research/acyclic-border-error/bounds.py
@@ -0,0 +1,70 @@
+"""Exact certificates for the bounded acyclic-selector error threshold."""
+
+from fractions import Fraction
+
+MAX_DIMENSION = 32
+MAX_BITS = 4096
+
+
+def validate(n: int, limit: Fraction, error: Fraction) -> None:
+    """Bound the public arithmetic domain before constructing certificates."""
+    if type(n) is not int or not 1 <= n <= MAX_DIMENSION:
+        raise ValueError("dimension must be an integer in 1..32")
+    for value in (limit, error):
+        if not isinstance(value, Fraction):
+            raise ValueError("parameters must be exact Fractions")
+        height = max(abs(value.numerator).bit_length(), value.denominator.bit_length())
+        if height > MAX_BITS:
+            raise ValueError("parameter height exceeds 4096 bits")
+    if limit < 1 or not 0 <= error <= 1:
+        raise ValueError("require limit >= 1 and error in [0,1]")
+
+
+def comparison(n: int, limit: Fraction, error: Fraction) -> list[list[Fraction]]:
+    """Return I-B, where B has limit above and error on/below the diagonal."""
+    validate(n, limit, error)
+    return [[Fraction(i == j) - (limit if i < j else error)
+             for j in range(n)] for i in range(n)]
+
+
+def certificate(n: int, limit: Fraction, error: Fraction) -> tuple[tuple[Fraction, ...], Fraction]:
+    """Return positive weights and their common comparison residual."""
+    validate(n, limit, error)
+    ratio = 1 + limit - error
+    weights = tuple(ratio ** (n - 1 - i) for i in range(n))
+    residual = 1 - error * sum(weights)
+    return weights, residual
+
+
+def cutoff(n: int, limit: Fraction, bits: int = 80) -> tuple[Fraction, Fraction]:
+    """Enclose the first root in an exact rational interval of width <= 2^-bits."""
+    validate(n, limit, Fraction(0))
+    if type(bits) is not int or not 1 <= bits <= 128:
+        raise ValueError("precision must be an integer in 1..128")
+    if n == 1:
+        return Fraction(1), Fraction(1)
+    low, high = Fraction(0), Fraction(1, n)
+    for _ in range(bits):
+        middle = (low + high) / 2
+        _, margin = certificate(n, limit, middle)
+        if margin > 0:
+            low = middle
+        else:
+            high = middle
+    assert high - low <= Fraction(1, 2 ** bits)
+    assert certificate(n, limit, low)[1] > 0
+    assert certificate(n, limit, high)[1] <= 0
+    return low, high
+
+
+def rational_boundary(n: int, ratio: Fraction) -> tuple[Fraction, Fraction, tuple[Fraction, ...]]:
+    """A rational rank-(n-1) boundary family, parameterized by ratio >= 2."""
+    validate(n, ratio, Fraction(0))
+    if ratio < 2:
+        raise ValueError("boundary ratio must be >= 2")
+    error = 1 / sum(ratio ** k for k in range(n))
+    limit = ratio - 1 + error
+    validate(n, limit, error)
+    weights, margin = certificate(n, limit, error)
+    assert margin == 0
+    return limit, error, weights
diff --git a/research/acyclic-border-error/verify.py b/research/acyclic-border-error/verify.py
new file mode 100644
index 0000000000..f9f47b6678
--- /dev/null
+++ b/research/acyclic-border-error/verify.py
@@ -0,0 +1,163 @@
+"""Standalone exact finite corroboration; writes only a generated stdout receipt."""
+
+from fractions import Fraction as F
+from hashlib import sha256
+from itertools import permutations, product
+import json
+from pathlib import Path
+import sys
+
+from bounds import certificate, comparison, cutoff, rational_boundary
+
+
+def require(condition: bool, message: str) -> None:
+    if not condition:
+        raise ValueError(message)
+
+
+def determinant(matrix: list[list[F]]) -> F:
+    """Literal signed permutation oracle, deliberately independent of the law."""
+    n = len(matrix)
+    require(1 <= n <= 5 and all(len(row) == n for row in matrix), "oracle dimensions")
+    total = F(0)
+    for order in permutations(range(n)):
+        inversions = sum(order[i] > order[j] for i in range(n) for j in range(i + 1, n))
+        term = F((-1) ** inversions)
+        for i in range(n):
+            term *= matrix[i][order[i]]
+        total += term
+    return total
+
+
+def rank(matrix: list[list[F]]) -> int:
+    """Independent rational elimination for the larger attaining witnesses."""
+    n = len(matrix)
+    require(1 <= n <= 32 and all(len(row) == n for row in matrix), "rank dimensions")
+    rows = [row[:] for row in matrix]
+    pivots = 0
+    for col in range(n):
+        candidates = [i for i in range(pivots, n) if rows[i][col]]
+        if not candidates:
+            continue
+        pivot = candidates[0]
+        rows[pivots], rows[pivot] = rows[pivot], rows[pivots]
+        divisor = rows[pivots][col]
+        rows[pivots] = [value / divisor for value in rows[pivots]]
+        for i in range(pivots + 1, n):
+            multiplier = rows[i][col]
+            rows[i] = [a - multiplier * b for a, b in zip(rows[i], rows[pivots])]
+        pivots += 1
+    return pivots
+
+
+def check_identities() -> int:
+    count = 0
+    for n, limit, error in product(range(1, 6), (F(1), F(3, 2), F(4)),
+                                    (F(0), F(1, 256), F(1, 250), F(1, 7), F(1))):
+        matrix = comparison(n, limit, error)
+        weights, margin = certificate(n, limit, error)
+        residual = [sum(a * b for a, b in zip(row, weights)) for row in matrix]
+        require(residual == [margin] * n, "weighted identity")
+        require(determinant(matrix) == margin, "literal determinant disagrees")
+        count += 1
+    return count
+
+
+def check_vertices() -> int:
+    """Every real sign vertex in the stated n=2,3 parameter boxes."""
+    count = 0
+    for n, limit in product((2, 3), (F(1), F(2))):
+        error = cutoff(n, limit, 16)[0] / 2
+        weights, margin = certificate(n, limit, error)
+        require(margin > 0 and all(w > 0 for w in weights), "invalid positive certificate")
+        for signs in product((-1, 1), repeat=n * n):
+            matrix = [[F(i == j) + signs[i*n+j] * (limit if i < j else error)
+                       for j in range(n)] for i in range(n)]
+            require(determinant(matrix) != 0, "singular sign vertex below cutoff")
+            count += 1
+    return count
+
+
+def check_boundaries() -> tuple[int, int]:
+    count, broken = 0, 0
+    for n, ratio in product(range(2, 17), (F(2), F(3), F(7, 2), F(16))):
+        limit, error, weights = rational_boundary(n, ratio)
+        matrix = comparison(n, limit, error)
+        require(rank(matrix) == n - 1, "boundary rank")
+        require(all(sum(a*b for a, b in zip(row, weights)) == 0 for row in matrix), "kernel")
+        require(error * (1 + limit - error) ** n == limit, "boundary polynomial")
+        require(limit / (1 + limit) ** n < error <= 1 / limit ** (n - 1), "growth sandwich")
+        low, high = cutoff(n, limit, 40)
+        require(low <= error <= high, "boundary outside cutoff interval")
+        changed = [row[:] for row in matrix]
+        changed[-1][0] += error
+        require(rank(changed) == n, "missing wrap term was not detected")
+        count += 1
+        broken += 1
+    return count, broken
+
+
+def check_controls() -> list[str]:
+    invalid = ((0, F(1), F(0)), (33, F(1), F(0)), (True, F(1), F(0)),
+               (2, F(1, 2), F(0)), (2, F(1), F(-1)), (2, F(1), F(2)),
+               (2, 1, F(0)), (2, F(1 << 4097), F(0)))
+    for n, limit, error in invalid:
+        try:
+            certificate(n, limit, error)
+        except ValueError:
+            continue
+        raise ValueError("invalid domain accepted")
+    for bits in (0, 129, True):
+        try:
+            cutoff(2, F(1), bits)
+        except ValueError:
+            continue
+        raise ValueError("invalid precision accepted")
+    require(rank([[F(1), F(1)], [F(1), F(1)]]) == 1, "cyclic zero-error counterexample")
+    limit, error, _ = rational_boundary(2, F(256))
+    paid = comparison(2, limit, error)
+    total = [row[:] for row in paid]
+    total[0][1] += limit  # An off-mask summand can conceal paid-subtotal growth.
+    require(rank(paid) == 1 and rank(total) == 2, "paid-subtotal control")
+    require(max(abs(x) for row in total for x in row) < 1, "bounded final total")
+    require(limit > 255, "large paid subtotal")
+    require(certificate(8, F(1), F(1, 256))[1] > 0, "eight-line safe cutoff")
+    require(certificate(8, F(1), F(1, 250))[1] < 0, "eight-line upper bracket")
+    require(certificate(1, F(1), F(1))[1] == 0, "diagonal-error boundary")
+    return ([f"invalid-domain-{i}" for i in range(len(invalid))]
+            + [f"invalid-precision-{i}" for i in range(3)]
+            + ["cyclic-zero-error", "paid-subtotal-vs-final-total",
+               "eight-line-bracket", "diagonal-error-boundary"])
+
+
+def receipt_files() -> dict[str, str]:
+    root = Path(__file__).resolve().parent
+    names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "bounds.py", "verify.py")
+    result = {}
+    for name in names:
+        path = root / name
+        require(path.stat().st_size <= 1024 * 1024, "receipt input too large")
+        data = path.read_bytes()
+        result[name] = sha256(data).hexdigest()
+    return result
+
+
+def main() -> None:
+    require(len(sys.argv) == 1, "no CLI arguments are accepted")
+    identities = check_identities()
+    vertices = check_vertices()
+    boundaries, omissions = check_boundaries()
+    controls = check_controls()
+    low, high = cutoff(8, F(1))
+    result = {"claim_type": "scoped proof with exact finite corroboration", "new_kappa": False,
+              "determinant_identities": identities, "sign_vertices": vertices,
+              "rank_n_minus_one_witnesses": boundaries, "wrap_omissions_rejected": omissions,
+              "controls": controls, "control_count": len(controls),
+              "n8_L1_cutoff": [str(low), str(high)],
+              "files_sha256": receipt_files()}
+    print(json.dumps(result, sort_keys=True, separators=(",", ":")))
+    print("PASS_ACYCLIC_BORDER_ERROR")
+
+
+if __name__ == "__main__":
+    main()