diff --git a/research/pascal-lane-depth/PROOF.md b/research/pascal-lane-depth/PROOF.md
new file mode 100644
index 0000000000..a6e4b3a99a
--- /dev/null
+++ b/research/pascal-lane-depth/PROOF.md
@@ -0,0 +1,166 @@
+# The optimal boundary fraction under bare Pascal iteration
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+Claim type: scoped mathematical proof with an exact finite numerical certificate.
+Independent human and formal proof-kernel review are unclaimed.
+
+## 1. Declared model and predecessor boundary
+
+Yiyang / Lyy-iiis's PR #5037, retained in
+`research/bounded-lane-border-core/core/PROOF.md`, Section 7, gives the formal
+population recurrence
+
+```text
+d'_h = d_h + d_(h-1),   0 <= h <= H,   d_(-1) = 0.
+```
+
+The term above grade H is omitted. The source already observes eventual
+top-grade domination. We take that recurrence and its published local invoice
+as premises. We do not establish a native implementation of the recurrence or
+recount the source word. The new result optimizes the boundary fraction over
+every starting population and certifies an exact failure depth.
+
+Let d be any nonzero vector in R_(>=0)^(H+1), let K=I+S where S shifts grades
+up by one and truncates above H, and put d^(e)=K^e d for an integer e>=0.
+Let D_e be the sum of its entries and z_e its grade-H entry.
+
+We declare the homogeneous local-ledger extension explicitly. Each unit of
+population receives the same complete local target and paid profiles T and P;
+each top-grade unit loses 112 rank-17 productive targets. At exponent t the
+signed surplus is therefore
+
+```text
+A(t) = sum_k T_k k^t - sum_r P_r r^t,
+B(t) = 112 * 17^t,
+M_e(d) = A(t) D_e - B(t) z_e.
+```
+
+This is a scalar accounting relaxation of a potential recursive caller.
+The source does not prove that actual graded main/helper inventories realize
+this homogeneous extension. The theorem below concerns this declared ledger,
+not arbitrary implementations of the border core. Extra costs can only worsen
+this ledger when its productive contract is held fixed. Changed profiles,
+new productive outputs or paid grade-reset mechanisms require a new analysis.
+
+## 2. Sharp population theorem
+
+Use binom(e,k)=0 for k>e. For every H,e>=0 and every permitted d,
+
+```text
+z_e / D_e >= q_H(e),
+q_H(e) = binom(e,H) / sum_(k=0)^H binom(e,k).
+```
+
+Equality is attained simultaneously at every depth by d=(1,0,...,0).
+If e>=H>=1, equality holds exactly when all initial grades above zero vanish.
+For fixed H>=1, q_H(e) is zero for e<H, strictly increases for e>=H,
+and tends to one as e tends to infinity.
+
+**Proof.** Since S^(H+1)=0, the binomial theorem gives
+
+```text
+d^(e)_h = sum_(j=0)^h binom(e,h-j) d_j.
+```
+
+Write a_l=binom(e,l) and s_l=sum_(k=0)^l a_k. The contribution of initial
+grade j to z_e is a_(H-j) d_j and its contribution to D_e is s_(H-j) d_j.
+Consequently z_e/D_e is a weighted average of the ratios a_l/s_l, with
+nonnegative weights s_(H-j)d_j.
+
+If e<H, the claimed lower bound is zero and the pure lowest grade attains it.
+Suppose e>=H. For 0<=l<=e,
+
+```text
+s_l/a_l = sum_(j=0)^l product_(a=0)^(j-1) (l-a)/(e-l+1+a).
+```
+
+For l<e, replacing l by l+1 increases every nonempty product already present and
+adds one positive term. Thus s_l/a_l strictly increases with l, so a_l/s_l
+strictly decreases. The weighted average is minimized at l=H, which
+corresponds to initial grade zero. Strictness gives the equality case.
+
+For e>=H, the same expression with l=H shows that 1/q_H(e) strictly
+decreases with e when H>=1: every nonempty product decreases. These products
+tend to zero, so q_H(e) tends to one. The transition from e=H-1 to e=H
+is from zero to a positive fraction. This proves every assertion. For H=0,
+q_0(e)=1 and the population ratio is identically one. QED.
+
+## 3. Exact local-ledger depth limit
+
+Suppose B>0. The largest possible surplus per unit final population is exactly
+
+```text
+max_(d != 0, d >= 0) M_e(d)/D_e = A - B q_H(e).
+```
+
+The pure lowest-grade vector attains it. Thus a positive local surplus is
+possible exactly when q_H(e)<A/B. In particular, if 0<A/B<1, every fixed
+height eventually fails, even after optimizing the initial populations.
+This sharpens the source's qualitative domination observation to an exact
+decision criterion at each depth.
+
+For the cited PR5037 invoice, take
+
+```text
+T = {4:56, 7:14, 8:94, 9:652, 17:224},
+P = {1:4656, 2:920, 3:1386},
+t = 4983/5000,   H = 65.
+```
+
+The integer-only certificate in `verify.py` proves
+
+```text
+0.015196119 < A/B < 0.015196120,
+q_65(110) < A/B < q_65(111).
+```
+
+Therefore the first impossible depth is **111 bare Pascal steps**. Through
+depth 110 the algebraic ledger has an attainer with strictly positive
+surplus; this is not an attained native construction. At every depth at
+least 111, every nonzero nonnegative initial population fails strictly.
+Depth here counts applications of K to the initial population, not actual
+recursive calls or the logarithmic depth of a multiplication algorithm.
+
+For the source's equal-population start d=(1,...,1) with 66 entries, the
+initial population has D_0=66 and z_0=1. Its first successor is
+(1,2,...,2), with D_1=131 and z_1=2. Exact enclosures give
+
+```text
+  5.551472 < 66 A - B     <   5.551475,
+-17.553092 < 131 A - 2 B < -17.553089.
+```
+
+Thus the equal-population one-shot bill already fails on the first bare
+reuse. Enlarging the initial populations can delay failure, but cannot
+pass depth 111 in this height-65 ledger. This says nothing against a
+changed matching, replenishment, filtration height or local invoice.
+
+## 4. Exact numerical certificate and finite checks
+
+No floating-point transcendental value is trusted. Rank one is exact. For
+each of the other seven distinct ranks in T and P, the checker bounds
+r^(4983/5000) between L/s and U/s, where s=10^12. It finds adjacent integers
+L,U by at most 48 bisections and directly verifies
+
+```text
+L^5000 <= r^4983 * s^5000 <= U^5000.
+```
+
+Monotonicity of the positive 5000th power proves the enclosure. Signed
+interval addition gives bounds on A and B. Exact rational comparisons with
+the binomial fractions certify the two depth signs and the equal-start
+failure. The printed intervals are rounded outward to denominator 10^9.
+
+The separate finite population engine applies the recurrence literally and
+compares it with the binomial formula, its optimal ratio and equality case
+for all nonzero vectors in {0,1,2}^(H+1), H=0,...,4, e=0,...,12.
+Pure-grade attainers and monotonicity through depth 256 are also checked.
+Invalid inputs and four false extrapolations have explicit rejection
+controls. These finite checks corroborate the proof; the universal
+quantifiers come from Sections 2 and 3.
+
+Every run prints a generated JSON receipt binding all six package files
+and the two cited inputs by SHA256. The receipt is stdout, so replay writes
+nothing into the checkout. The source numerical/operator verifiers are
+never imported or executed. Their mathematical premises retain Yiyang's
+and the underlying native/compiler contributors' credit.
diff --git a/research/pascal-lane-depth/README.md b/research/pascal-lane-depth/README.md
new file mode 100644
index 0000000000..59cfdf90ba
--- /dev/null
+++ b/research/pascal-lane-depth/README.md
@@ -0,0 +1,134 @@
+# Sharp depth limit for bare Pascal lane iteration
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+Claim type: scoped proof with an exact finite numerical certificate.
+Independent human and formal proof-kernel review are unclaimed.
+
+At height 65, **no starting population passes the declared C=.0034 local
+ledger after 111 bare Pascal steps**. The bound is sharp: a pure lowest-grade
+start passes through step 110 in this algebraic relaxation. The original
+66-grade equal-population start already fails after its first bare reuse,
+with signed surplus in `[-17.553090674, -17.553090235]`.
+
+Yiyang / Lyy-iiis's [PR5037](https://github.com/CrocSwap/integer-mult-bounds/pull/5037)
+gives the reduced-domain border core, its one-shot local invoice and the
+recurrence `d'_h=d_h+d_(h-1)`. It already observes eventual top-grade
+domination. The new theorem optimizes every nonnegative starting population
+and gives an exact first-failure depth. The source operator and native counts
+are cited premises, not newly audited results.
+
+For every fixed height H and integer depth e, the sharp minimum top-grade
+fraction is
+
+```text
+q_H(e) = binom(e,H) / sum_(k=0)^H binom(e,k).
+```
+
+The surplus per unit final population is at most `A-B q_H(e)`, where A is
+the cited base target-minus-paid moment and B is its top-grade target debit.
+The pure lowest-grade vector attains this upper bound at every depth. For
+e>=H>=1 it is the unique attaining direction. See [PROOF.md](PROOF.md) for
+the weighted-average argument, equality cases and strict monotonicity.
+
+## Scope and relevance
+
+This is a partial answer to PR5037's whole-job matching question. It rules
+out keeping a favorable homogeneous local bill through unchanged fixed-height
+Pascal iteration by choosing better initial populations alone. The next
+construction needs changed matching, a priced reset or a changed per-grade
+invoice. It gives no new kappa or selected-frontier change.
+
+The accounting extension is an explicit hypothesis: each population unit
+has the same T/P ledger and each top-grade unit loses 112 rank-17 targets.
+PR5037 does not establish that actual graded main/helper inventories realize
+this extension. The theorem concerns that scalar relaxation. Depth counts
+applications of the population recurrence, not actual multiplication recursion.
+It excludes no different graded caller, replenishment or increasing height.
+Native shears, all-size source/exit/complement matching, ownership, routing,
+precision, stock, BIT transfer and outer admission remain open or inherited.
+No complete multiplication theorem or formal-kernel proof is claimed.
+
+## Evidence and reproduction
+
+CPython 3.12 and its standard library suffice. Local replay used CPython
+3.12.15 on macOS 27.0.1 arm64. From the repository root:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/pascal-lane-depth/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/pascal-lane-depth/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/pascal-lane-depth
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/pascal-lane-depth --check-source-history
+```
+
+A portable Python 3.12 interpreter can replace the absolute path. Both direct
+modes print `PASS_PASCAL_LANE_DEPTH` in a generated JSON receipt binding all
+six package files and both cited inputs by SHA256. Direct replay needs only
+these relative paths, without Git or network access. It writes nothing;
+redirect stdout outside the checkout to retain a receipt. There is no
+handwritten or frozen result receipt.
+
+The certificate uses integer powers to bound all eight rank powers. It proves
+strict signs at depths 110 and 111 and for the equal-start first reuse.
+Literal iteration and the binomial formula agree in 4,654 population/depth
+cases. The checks also cover 65 pure-grade attainers, 3,360 equality-case
+fixtures, optimal-fraction monotonicity through depth 256, eight invalid
+inputs and four false extrapolation controls. Finite checks corroborate the
+written universal proof. Predecessor scientific verifiers are never executed.
+
+## Sources and overlap
+
+Canonical base is `721c03822c421b7f7fcbb2598993b947c4d88419`, priority
+revision 8. [TASK.json](TASK.json) records the changed scope from
+`complex-rank-shape-decoder`; [SOURCES.json](SOURCES.json) pins the exact
+predecessor README and proof. The card's current first command,
+`research_selected_baseline.py`, passes source bindings only. The selected
+conditional frontier is unchanged.
+
+The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19247035)
+records this question. The initial overlap cache included 407 open PR bodies and
+5,828 Discussion records with complete reported remote pagination. Sparse
+local overlap covered 78 of 8,348 tracked note paths; separate Git searches
+covered main's README corpus and merged/all-state PR searches covered Pascal,
+border, lane and grade terms. This is bounded overlap evidence, not proof of
+novelty or coverage of unpublished work. PR5117's root-only sign extraction
+is a different question and is not extended here.
+
+Credit Yiyang / Lyy-iiis for PR5037 and its bounded-lane core/recurrence/invoice;
+Cao Yifan for the round-three native source; Dillon for border recovery;
+Jacob Alan Sussman and the finite-precompiler contributors; and the retained
+native, Clifford, helper, precision and outer lineage. The binomial theorem
+and weighted-average method are classical. The new contribution is the sharp
+population optimization and its source-specific exact depth consequence.
+Predecessor files and their credit lines are unchanged.
+
+## Implementation bounds
+
+The checker uses direct calls, no recursion, subprocesses, external imports
+or network access. Population entry points enforce height <=65, depth <=256,
+and initial entries below 2^256. The exhaustive small domain has height <=4
+and depth <=12. Each rank-power root uses at most 48 iterations, with integers
+below 2^220000. Inputs and package files are each bounded below 1 MiB; the
+source manifest has exactly four declarations and two fixed input paths.
+All functions fit within sixty physical lines. Invariants use explicit
+exceptions and remain active with optimization. Both registered modes enable
+warning errors; no external static analyzer is claimed.
+
+Power of Ten rule 3 deviation: CPython allocates arithmetic objects and bounded
+collections dynamically. This one-shot exact checker cannot prohibit those
+runtime allocations. Enforced inputs bound live data, and only one small
+population or rank-power bisection is live at a time. Normal and optimized
+replay exercise the maximum height/depth and invalid-input limits. A future
+steady-operation native implementation would need fixed-capacity arithmetic
+storage before removing this deviation.
+
+## Open next questions
+
+1. Can a paid grade-reset or replenishment operation keep the complete bill
+   favorable? Start with one explicit reset, retained independent inputs,
+   restored helpers and its full signed invoice. Legal native transport,
+   ownership and reset costs are blockers. A reset is not free in this result.
+2. Can a literal whole-job caller use nonhomogeneous per-grade profiles to
+   escape the scalar ledger? Export one matched parent/child slice with
+   source, exit and complement identities, then compute its full per-grade
+   T/P profiles. Actual native shears and constructed graded adapters remain
+   prerequisites. The present theorem does not supply that caller.
diff --git a/research/pascal-lane-depth/SOURCES.json b/research/pascal-lane-depth/SOURCES.json
new file mode 100644
index 0000000000..c33ff37ad8
--- /dev/null
+++ b/research/pascal-lane-depth/SOURCES.json
@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "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/bounded-lane-border-core/README.md",
+      "usage": "input",
+      "git_blob": "30449eb1e9f70bbce76ee4db3046d79ea8e593c7",
+      "sha256": "78b85269d7f931e080e3ca263584761859656ea76d8ba509023101d3b04340d7"
+    },
+    {
+      "path": "research/bounded-lane-border-core/core/PROOF.md",
+      "usage": "input",
+      "git_blob": "87d0d64ac5e51da40b87aacb906200aea187faa3",
+      "sha256": "fcbc93f44eed41dd79aedd089f874a784fc0dac255a104a3cd39f08f2fcc5b38"
+    }
+  ]
+}
diff --git a/research/pascal-lane-depth/TASK.json b/research/pascal-lane-depth/TASK.json
new file mode 100644
index 0000000000..5cce6ad1ed
--- /dev/null
+++ b/research/pascal-lane-depth/TASK.json
@@ -0,0 +1,84 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-rank-shape-decoder",
+  "priority_revision": 8,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "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": "Sharp top-grade population fraction for every nonnegative initial vector under bare fixed-height Pascal iteration, and the exact C=.0034 failure depth for the declared homogeneous PR5037 ledger.",
+  "scope_change_reason": "Partial answer to PR5037 open next question 2. The source gives only qualitative top-grade domination; the changed question optimizes every initial population and certifies the first impossible depth. It does not audit the source operator or native counts.",
+  "bottleneck_link": "The proposed two-full border can target the admitted BIT budget only if its complete graded ledger stays favorable. This obstruction rejects unchanged bare grade iteration, including its first equal-population reuse, and directs work toward changed matching or a priced reset.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first sharp fixed-model obstruction with a written proof and bounded exact certificate; do not extend to a reset construction or supplier admission.",
+  "outcome": "negative-result",
+  "evidence": "PROOF.md; normal and optimized verify.py stdout receipts; registered metadata/source replay and committed-byte/source-history preflight.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can a paid grade-reset or replenishment mechanism preserve a favorable complete local ledger?",
+      "why_it_matters": "Changing initial populations alone cannot evade the depth-111 bound at height 65.",
+      "first_step": "Specify one reset operation with its retained independent inputs, restored helpers, productive outputs and full signed invoice.",
+      "blocked_by": "Actual coherent native shears, legal grade transport, ownership and the reset cost."
+    },
+    {
+      "question": "Does a literal whole-job caller have nonhomogeneous grade profiles that escape this scalar ledger?",
+      "why_it_matters": "The source recurrence does not establish a uniform native main/helper inventory at every grade.",
+      "first_step": "Export one matched parent/child source-exit-complement slice and compute its per-grade paid and productive profiles.",
+      "blocked_by": "A constructed native caller and source-bound graded adapters."
+    }
+  ],
+  "result_summary": "At height 65 every starting population fails the declared C=.0034 homogeneous local ledger after 111 bare Pascal steps; the bound is sharp and the equal-population start fails after one step.",
+  "claim_type": "Scoped proof with an exact finite numerical certificate.",
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19247035"
+}
diff --git a/research/pascal-lane-depth/VERIFY.json b/research/pascal-lane-depth/VERIFY.json
new file mode 100644
index 0000000000..4386cafbcd
--- /dev/null
+++ b/research/pascal-lane-depth/VERIFY.json
@@ -0,0 +1,37 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/bounded-lane-border-core/README.md",
+    "research/bounded-lane-border-core/core/PROOF.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Integer-only rank-power enclosures; sharp depth-110/111 signs; equal-start failure; literal versus binomial recurrence, optimality/equality cases and rejection controls; generated source-bound receipt."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "The same complete exact certificate and rejection controls under optimization; every invariant uses an explicit exception."
+    }
+  ]
+}
diff --git a/research/pascal-lane-depth/verify.py b/research/pascal-lane-depth/verify.py
new file mode 100644
index 0000000000..857066297f
--- /dev/null
+++ b/research/pascal-lane-depth/verify.py
@@ -0,0 +1,225 @@
+#!/usr/bin/env python3
+"""Exact certificates for the bare Pascal population and local-ledger model."""
+
+import hashlib
+import itertools
+import json
+import math
+from fractions import Fraction as Q
+from pathlib import Path
+
+
+PACKAGE = Path(__file__).resolve().parent
+ROOT = PACKAGE.parents[1]
+MAX_HEIGHT = 65
+MAX_DEPTH = 256
+SCALE = 10**12
+
+
+def require(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def parameters(height, depth):
+    require(type(height) is int and 0 <= height <= MAX_HEIGHT, "height range")
+    require(type(depth) is int and 0 <= depth <= MAX_DEPTH, "depth range")
+
+
+def validate_population(start, depth):
+    parameters(len(start) - 1, depth)
+    require(all(type(x) is int and 0 <= x < 2**256 for x in start),
+            "population entries")
+    require(any(start), "empty productive population")
+
+
+def choose(n, k):
+    return math.comb(n, k) if k <= n else 0
+
+
+def closed_population(start, depth):
+    validate_population(start, depth)
+    return tuple(sum(choose(depth, h - j) * start[j] for j in range(h + 1))
+                 for h in range(len(start)))
+
+
+def literal_population(start, depth):
+    validate_population(start, depth)
+    current = tuple(start)
+    for _ in range(depth):
+        current = (current[0],) + tuple(current[h] + current[h - 1]
+                                       for h in range(1, len(current)))
+    return current
+
+
+def optimum(height, depth):
+    parameters(height, depth)
+    return Q(choose(depth, height),
+             sum(choose(depth, k) for k in range(height + 1)))
+
+
+def power_bounds(rank):
+    require(type(rank) is int and 1 <= rank <= 17, "power rank range")
+    if rank == 1:
+        return Q(1), Q(1)
+    # Integer-only certificate: (r^(4983/5000) * SCALE)^5000 is target.
+    target = rank**4983 * SCALE**5000
+    lower, upper = SCALE, rank * SCALE
+    for _ in range(48):
+        if upper - lower == 1:
+            break
+        middle = (lower + upper) // 2
+        if middle**5000 <= target:
+            lower = middle
+        else:
+            upper = middle
+    require(upper - lower == 1, "integer root bisection exhausted")
+    require(lower**5000 <= target <= upper**5000, "integer power certificate")
+    return Q(lower, SCALE), Q(upper, SCALE)
+
+
+def ledger_bounds():
+    # Cited PR5037 local invoice, used as a premise, not recounted from a word.
+    target = {4: 56, 7: 14, 8: 94, 9: 652, 17: 224}
+    paid = {1: 4656, 2: 920, 3: 1386}
+    bounds = {r: power_bounds(r) for r in sorted(target.keys() | paid.keys())}
+    lower = sum(n * bounds[r][0] for r, n in target.items())
+    lower -= sum(n * bounds[r][1] for r, n in paid.items())
+    upper = sum(n * bounds[r][1] for r, n in target.items())
+    upper -= sum(n * bounds[r][0] for r, n in paid.items())
+    omitted = (112 * bounds[17][0], 112 * bounds[17][1])
+    require(Q(0) < lower < upper and Q(0) < omitted[0] <= omitted[1],
+            "positive local coefficients")
+    return (lower, upper), omitted
+
+
+def enclosure(bounds):
+    lower, upper = bounds
+    require(lower <= upper, "ordered interval")
+    scale = 10**9
+    lo = lower.numerator * scale // lower.denominator
+    hi = -((-upper.numerator * scale) // upper.denominator)
+    return [str(Q(lo, scale)), str(Q(hi, scale))]
+
+
+def check_small_populations():
+    checked, sharp, unique = 0, 0, 0
+    for height in range(5):
+        for start in itertools.product(range(3), repeat=height + 1):
+            if not any(start):
+                continue
+            for depth in range(13):
+                closed = closed_population(start, depth)
+                require(closed == literal_population(start, depth), "binomial identity")
+                actual = Q(closed[-1], sum(closed))
+                best = optimum(height, depth)
+                require(actual >= best, "optimal fraction")
+                checked += 1
+                if depth >= height >= 1:
+                    require((actual == best) == (not any(start[1:])), "unique optimum")
+                    unique += 1
+        pure = (1,) + (0,) * height
+        for depth in range(13):
+            population = literal_population(pure, depth)
+            require(Q(population[-1], sum(population)) == optimum(height, depth),
+                    "pure lowest grade attains")
+            sharp += 1
+    return {"population_depth_cases": checked, "pure_grade_attainers": sharp,
+            "uniqueness_cases": unique}
+
+
+def check_depth_certificate(a, b):
+    previous = Q(0)
+    for depth in range(MAX_DEPTH + 1):
+        fraction = optimum(65, depth)
+        require(fraction >= previous, "nondecreasing optimal loss")
+        if depth > 65:
+            require(fraction > previous, "strict optimal loss growth")
+        previous = fraction
+    q110, q111 = optimum(65, 110), optimum(65, 111)
+    require(a[0] - b[1] * q110 > 0, "depth 110 strict pass")
+    require(a[1] - b[0] * q111 < 0, "depth 111 strict failure")
+    start = (1,) * 66
+    first = literal_population(start, 1)
+    require(sum(first) == 131 and first[-1] == 2, "equal population first step")
+    initial = (66 * a[0] - b[1], 66 * a[1] - b[0])
+    after = (131 * a[0] - 2 * b[1], 131 * a[1] - 2 * b[0])
+    require(initial[0] > 0 and after[1] < 0, "equal population loses on reuse")
+    return {"first_impossible_depth": 111, "last_possible_depth": 110,
+            "optimal_fraction_at_110": str(q110),
+            "optimal_fraction_at_111": str(q111),
+            "normalized_margin_at_110": enclosure((a[0] - b[1] * q110,
+                                                    a[1] - b[0] * q110)),
+            "normalized_margin_at_111": enclosure((a[0] - b[1] * q111,
+                                                    a[1] - b[0] * q111)),
+            "equal_start_initial_margin": enclosure(initial),
+            "equal_start_after_one_margin": enclosure(after),
+            "monotonicity_depth_cases": MAX_DEPTH + 1}
+
+
+def rejection_controls():
+    invalid = [((), 0), ((0,), 0), ((-1,), 0), ((True,), 0),
+               ((2**256,), 0), ((1,) * 67, 0), ((1,), -1), ((1,), 257)]
+    for start, depth in invalid:
+        try:
+            closed_population(start, depth)
+        except ValueError:
+            continue
+        raise ValueError("invalid population accepted")
+    # These false extrapolations give different exact answers on new fixtures.
+    require(Q(1, 66) != Q(2, 131), "constant boundary fraction control")
+    require(optimum(2, 3) != Q(choose(3, 2), 2**3), "untruncated total control")
+    require(closed_population((1, 0, 0), 2) != (1, 0, 0), "no shift control")
+    require(optimum(2, 3) != optimum(2, 4), "depth independent optimum control")
+    largest = (2**256 - 1,) + (0,) * MAX_HEIGHT
+    boundary = closed_population(largest, MAX_DEPTH)
+    require(boundary == literal_population(largest, MAX_DEPTH), "maximum valid limits")
+    require(Q(boundary[-1], sum(boundary)) == optimum(MAX_HEIGHT, MAX_DEPTH),
+            "maximum valid attainer")
+    return {"invalid_inputs_rejected": len(invalid), "false_shortcuts_rejected": 4,
+            "maximum_valid_population_cases": 1}
+
+
+def source_hashes():
+    source_path = PACKAGE / "SOURCES.json"
+    require(source_path.stat().st_size < 1024**2, "source manifest size bound")
+    manifest = json.loads(source_path.read_text())
+    require(len(manifest["files"]) == 4, "four source declarations")
+    inputs = [row for row in manifest["files"] if row["usage"] == "input"]
+    expected = {"research/bounded-lane-border-core/README.md",
+                "research/bounded-lane-border-core/core/PROOF.md"}
+    require(len(inputs) == 2 and {row["path"] for row in inputs} == expected,
+            "exact two cited source inputs")
+    hashes = {}
+    for row in inputs:
+        path = ROOT / row["path"]
+        require(path.stat().st_size < 1024**2, "source size bound")
+        digest = hashlib.sha256(path.read_bytes()).hexdigest()
+        require(digest == row["sha256"], "cited input drift: " + row["path"])
+        hashes[row["path"]] = digest
+    names = ("README.md", "PROOF.md", "verify.py", "TASK.json", "SOURCES.json",
+             "VERIFY.json")
+    for name in names:
+        path = PACKAGE / name
+        require(path.stat().st_size < 1024**2, "package size bound")
+        hashes[str(path.relative_to(ROOT))] = hashlib.sha256(path.read_bytes()).hexdigest()
+    return hashes
+
+
+def main():
+    hashes = source_hashes()
+    a, b = ledger_bounds()
+    scientific = check_depth_certificate(a, b)
+    scientific.update(check_small_populations())
+    scientific.update(rejection_controls())
+    scientific["base_margin"] = enclosure(a)
+    scientific["top_grade_debit"] = enclosure(b)
+    scientific["passing_fraction_threshold"] = enclosure((a[0] / b[1], a[1] / b[0]))
+    print(json.dumps({"schema": "pascal-lane-depth/v1",
+                      "status": "PASS_PASCAL_LANE_DEPTH",
+                      "scientific": scientific, "sha256": hashes},
+                     sort_keys=True, indent=2))
+
+
+if __name__ == "__main__":
+    main()