diff --git a/research/lockstep-source-row-index/COST-MODEL-REVIEW.md b/research/lockstep-source-row-index/COST-MODEL-REVIEW.md
new file mode 100644
index 0000000000..e352ed2bea
--- /dev/null
+++ b/research/lockstep-source-row-index/COST-MODEL-REVIEW.md
@@ -0,0 +1,141 @@
+# Independent computational-model review of the source index
+
+Reviewer: `/root/tape_dispatch`, with OpenAI assistance for @CubeJerry's
+research run. Date: 2026-11-11. Scientific base:
+`e54523517d0f03e58352e647c403a5af3e525a57`.
+
+## Scope and snapshot
+
+This is a source-reading and mathematical cost review of section 5, not a
+runtime replay or a replacement for checking the indexing identities. The
+author's files were not modified. Reviewed SHA256 pins, relative to
+`work/compiler_source_index/package/`:
+
+| File | SHA256 |
+| --- | --- |
+| `PROOF.md` | `5571b0e6329f620c4bf58e90fb03ce4dfefae95708435739f8fac5e78aa52c9b` |
+| `source_index.py` | `b45f671eeac3d5dead19285cf5f455b705596e9f3679a2eddbdd225e4fbf3718` |
+| `inputs/pascal_codec.py` | `cec2c8b5e153a264127e8301ed59591fe97c9a46078ff2343b3784d177c6984d` |
+
+**Outcome: a repairable computational-model gap.** The current Python already
+replaces growing state dictionaries/sets with `sorted_unique` and
+`SortedStateTable`. That resolves the earlier hash-table objection for these
+tables. Binary-search accesses and indexed value writes nevertheless have not
+been lowered to a tape algorithm with paid seeks and returns. Calling the
+displayed time formula bit work, or saying it is not unit-cost RAM, does not
+alone establish those costs.
+
+This does not refute the state aggregation or rank/unrank theorem. It also
+does not show that no other implementation attains the sharper formula. A
+specific memory-access argument is missing; the following conservative one
+preserves the claimed polynomiality.
+
+## Deterministic sequential alternative
+
+Keep the author's definitions
+
+\[
+R=1+q\binom{G+q-1}{q},\quad M=\binom{G+d}{d},
+\]
+
+\[
+B=S+\ell(N)+(G+1)\ell(A+W+P+G+2)+1,
+\quad \ell(x)=\lceil\log_2(x+1)\rceil,
+\quad L=(S+R+dM)B.
+\]
+
+Serialize input, profiles, state keys and local/total counts as delimited
+binary records on a constant number of tapes. Scalar fields need O(B) bits;
+a profile needs O(dB) bits. Padded count fields avoid variable-size shifts.
+Group state records by depth and profiles in their specified lexicographic
+order. The query path/output also fits O(L), since M is at least G+1 when
+d is positive and individual indices fit O(B).
+
+Generate one candidate next state from one current state and one distinct
+paid rank. Scan the next-depth records to test membership; append only if
+absent. There are at most qR candidate operations, and candidates are never
+materialized simultaneously. Profile generation uses explicit bounded
+counters/stack, with O(dB) work storage. Bottom-up recurrence evaluation and
+rank/unrank find every count by a complete table scan. Role and paid-position
+lookup uses the same convention. Return every work head to a marked origin
+after each operation, or store and restore an explicit binary cursor. Charge
+both choices.
+
+A conservative O(L^2) moves per record/arithmetic operation suffices: there
+are O(L) stored symbols and at most O(L) key comparisons per scan; charging
+O(L) for each comparison and all candidate-key rewinds is already quadratic.
+Origin returns, insertion, updates, explicit copies and output emission fit
+that bound as well. Schoolbook O(B^2) scalar arithmetic is bounded by O(L^2).
+The representation and a fixed number of scratch records occupy O(L) cells,
+including historical blank backing. No paid-path tree or source list is
+materialized.
+
+Let the scalar/record-operation envelopes be
+
+\[
+K_{\rm setup}=(S+1)^2
+[M(G+d+1)+R(M(d+1)+q+1)],
+\]
+
+\[
+K_{\rm query}=(S+1)^2
+[M(d+1)+GP+G+d+1].
+\]
+
+The profile loops, qR streamed candidate operations, state/profile recurrence
+loops and chronological query loops fit these envelopes. Consequently an
+explicit deterministic sequential alternative satisfies
+
+\[
+T_{\rm setup}=O(K_{\rm setup}L^2),\qquad
+T_{\rm query}=O(K_{\rm query}L^2),\qquad
+S_{\rm work}=O(L).
+\]
+
+This is an existence proof for the described sequential realization, not a
+transition-count certification of the Python runtime. It is polynomial in
+G and log N for each fixed native rule because q and d are fixed. A tighter
+scan protocol could improve the deliberately loose exponent; no such claim
+is necessary for this logical indexing advance.
+
+## Suggested author change and retained limitations
+
+Either use the conservative deterministic bounds above, labelling Python as
+the reference mathematical implementation, or specify another deterministic
+bit model and prove access, deduplication and cursor costs before retaining
+the sharper formula. If both are shown, name their different models.
+
+No native row lookup, gather, copy, erase, owner transfer, or payload
+permutation follows. The actual selected role/owner manifest and native
+routing tariffs remain obligations. The five selected assumptions remain.
+**No new kappa; no unconditional multiplication theorem.**
+
+## Resolution after the author's revision
+
+
+The author revised section 5 and the table implementation while this review
+was in progress. The reviewed repair snapshot is:
+
+| File | SHA256 |
+| --- | --- |
+| `PROOF.md` | `1631e28072e1ad39c3833ec83ff7d59e35c4d8fd1ad45ebce6b777aed4125bdb` |
+| `source_index.py` | `e978025591b06770026b9879f1e5b10827424f410794fb2b1e1f10a720f49176` |
+
+The final proof pin adds a numeric-hash source reference and CPython wording
+to the initially reviewed repair; the serialized-table argument was re-read
+and is unchanged. The revised proof explicitly separates indexed metadata arithmetic/comparison
+work from a deterministic serialized-table realization. It uses
+L=(S+R+dM+1)B and the conservative O(K_setup L^2), O(K_query L^2), O(L)
+time/space bounds, with candidate insertion, key access, copying, cursor
+return, arithmetic and retirement charged. Its O(L) extra spare representation
+keeps workspace within O(L). Streaming at most qR candidates prevents storing
+qR states simultaneously. Valid query lengths and oversized malformed queries
+are distinguished.
+
+The revised code deduplicates current dilations before generating children;
+at fixed paid rank the next-state map is injective. This also makes the total
+sorted candidate count at most R, supporting the stated O(R log(R+1)) key
+comparison tally. This reviewer accepts the computational-model repair for
+this snapshot. The earlier finding is retained above as review history. The
+separate collision-family audit and its asymptotic lower bound are outside
+this review's assigned scope and were not independently verified here.
diff --git a/research/lockstep-source-row-index/INDEPENDENT-RESULT.json b/research/lockstep-source-row-index/INDEPENDENT-RESULT.json
new file mode 100644
index 0000000000..eaac37926d
--- /dev/null
+++ b/research/lockstep-source-row-index/INDEPENDENT-RESULT.json
@@ -0,0 +1,168 @@
+{
+  "bounded_cases": [
+    {
+      "height": 0,
+      "paid_alphabet": 4,
+      "replicas": 5,
+      "sources": 3,
+      "states": 1,
+      "target_alphabet": 2
+    },
+    {
+      "height": 0,
+      "paid_alphabet": 4,
+      "replicas": 5,
+      "sources": 3,
+      "states": 1,
+      "target_alphabet": 2
+    },
+    {
+      "height": 1,
+      "paid_alphabet": 4,
+      "replicas": 5,
+      "sources": 10,
+      "states": 5,
+      "target_alphabet": 2
+    },
+    {
+      "height": 1,
+      "paid_alphabet": 4,
+      "replicas": 5,
+      "sources": 10,
+      "states": 5,
+      "target_alphabet": 2
+    },
+    {
+      "height": 2,
+      "paid_alphabet": 4,
+      "replicas": 5,
+      "sources": 33,
+      "states": 21,
+      "target_alphabet": 2
+    },
+    {
+      "height": 2,
+      "paid_alphabet": 4,
+      "replicas": 5,
+      "sources": 33,
+      "states": 21,
+      "target_alphabet": 2
+    },
+    {
+      "height": 3,
+      "paid_alphabet": 4,
+      "replicas": 5,
+      "sources": 107,
+      "states": 57,
+      "target_alphabet": 2
+    },
+    {
+      "height": 3,
+      "paid_alphabet": 4,
+      "replicas": 5,
+      "sources": 107,
+      "states": 57,
+      "target_alphabet": 2
+    },
+    {
+      "height": 0,
+      "paid_alphabet": 3,
+      "replicas": 5,
+      "sources": 1,
+      "states": 1,
+      "target_alphabet": 1
+    },
+    {
+      "height": 0,
+      "paid_alphabet": 3,
+      "replicas": 5,
+      "sources": 1,
+      "states": 1,
+      "target_alphabet": 1
+    },
+    {
+      "height": 1,
+      "paid_alphabet": 3,
+      "replicas": 5,
+      "sources": 1,
+      "states": 4,
+      "target_alphabet": 1
+    },
+    {
+      "height": 1,
+      "paid_alphabet": 3,
+      "replicas": 5,
+      "sources": 1,
+      "states": 4,
+      "target_alphabet": 1
+    },
+    {
+      "height": 2,
+      "paid_alphabet": 3,
+      "replicas": 5,
+      "sources": 1,
+      "states": 13,
+      "target_alphabet": 1
+    },
+    {
+      "height": 2,
+      "paid_alphabet": 3,
+      "replicas": 5,
+      "sources": 1,
+      "states": 13,
+      "target_alphabet": 1
+    },
+    {
+      "height": 3,
+      "paid_alphabet": 3,
+      "replicas": 5,
+      "sources": 1,
+      "states": 28,
+      "target_alphabet": 1
+    },
+    {
+      "height": 3,
+      "paid_alphabet": 3,
+      "replicas": 5,
+      "sources": 1,
+      "states": 28,
+      "target_alphabet": 1
+    }
+  ],
+  "collision_witness": {
+    "cases": [
+      {
+        "distinct_hashes": 1,
+        "height": 1,
+        "layer_states": 5,
+        "sources": 1
+      },
+      {
+        "distinct_hashes": 1,
+        "height": 2,
+        "layer_states": 25,
+        "sources": 1
+      },
+      {
+        "distinct_hashes": 1,
+        "height": 3,
+        "layer_states": 75,
+        "sources": 1
+      },
+      {
+        "distinct_hashes": 1,
+        "height": 4,
+        "layer_states": 175,
+        "sources": 1
+      }
+    ],
+    "integer_hash_modulus": 2305843009213693951
+  },
+  "package_hashes": {
+    "PROOF.md": "1631e28072e1ad39c3833ec83ff7d59e35c4d8fd1ad45ebce6b777aed4125bdb",
+    "source_index.py": "e978025591b06770026b9879f1e5b10827424f410794fb2b1e1f10a720f49176",
+    "verify.py": "fb89cad83c3ed69bffaf2a95347b21d26dde4da1dc9c52b4304e7d94d836f623"
+  },
+  "sources_checked": 314,
+  "status": "PASS_SOURCE_INDEX_PEER_FUNCTIONAL_CHECKS"
+}
diff --git a/research/lockstep-source-row-index/INITIAL-REVIEW-RESULT.json b/research/lockstep-source-row-index/INITIAL-REVIEW-RESULT.json
new file mode 100644
index 0000000000..4921b25dc8
--- /dev/null
+++ b/research/lockstep-source-row-index/INITIAL-REVIEW-RESULT.json
@@ -0,0 +1,168 @@
+{
+  "bounded_cases": [
+    {
+      "height": 0,
+      "paid_alphabet": 4,
+      "replicas": 5,
+      "sources": 3,
+      "states": 1,
+      "target_alphabet": 2
+    },
+    {
+      "height": 0,
+      "paid_alphabet": 4,
+      "replicas": 5,
+      "sources": 3,
+      "states": 1,
+      "target_alphabet": 2
+    },
+    {
+      "height": 1,
+      "paid_alphabet": 4,
+      "replicas": 5,
+      "sources": 10,
+      "states": 5,
+      "target_alphabet": 2
+    },
+    {
+      "height": 1,
+      "paid_alphabet": 4,
+      "replicas": 5,
+      "sources": 10,
+      "states": 5,
+      "target_alphabet": 2
+    },
+    {
+      "height": 2,
+      "paid_alphabet": 4,
+      "replicas": 5,
+      "sources": 33,
+      "states": 21,
+      "target_alphabet": 2
+    },
+    {
+      "height": 2,
+      "paid_alphabet": 4,
+      "replicas": 5,
+      "sources": 33,
+      "states": 21,
+      "target_alphabet": 2
+    },
+    {
+      "height": 3,
+      "paid_alphabet": 4,
+      "replicas": 5,
+      "sources": 107,
+      "states": 57,
+      "target_alphabet": 2
+    },
+    {
+      "height": 3,
+      "paid_alphabet": 4,
+      "replicas": 5,
+      "sources": 107,
+      "states": 57,
+      "target_alphabet": 2
+    },
+    {
+      "height": 0,
+      "paid_alphabet": 3,
+      "replicas": 5,
+      "sources": 1,
+      "states": 1,
+      "target_alphabet": 1
+    },
+    {
+      "height": 0,
+      "paid_alphabet": 3,
+      "replicas": 5,
+      "sources": 1,
+      "states": 1,
+      "target_alphabet": 1
+    },
+    {
+      "height": 1,
+      "paid_alphabet": 3,
+      "replicas": 5,
+      "sources": 1,
+      "states": 4,
+      "target_alphabet": 1
+    },
+    {
+      "height": 1,
+      "paid_alphabet": 3,
+      "replicas": 5,
+      "sources": 1,
+      "states": 4,
+      "target_alphabet": 1
+    },
+    {
+      "height": 2,
+      "paid_alphabet": 3,
+      "replicas": 5,
+      "sources": 1,
+      "states": 13,
+      "target_alphabet": 1
+    },
+    {
+      "height": 2,
+      "paid_alphabet": 3,
+      "replicas": 5,
+      "sources": 1,
+      "states": 13,
+      "target_alphabet": 1
+    },
+    {
+      "height": 3,
+      "paid_alphabet": 3,
+      "replicas": 5,
+      "sources": 1,
+      "states": 28,
+      "target_alphabet": 1
+    },
+    {
+      "height": 3,
+      "paid_alphabet": 3,
+      "replicas": 5,
+      "sources": 1,
+      "states": 28,
+      "target_alphabet": 1
+    }
+  ],
+  "collision_witness": {
+    "cases": [
+      {
+        "distinct_hashes": 1,
+        "height": 1,
+        "layer_states": 5,
+        "sources": 1
+      },
+      {
+        "distinct_hashes": 1,
+        "height": 2,
+        "layer_states": 25,
+        "sources": 1
+      },
+      {
+        "distinct_hashes": 1,
+        "height": 3,
+        "layer_states": 75,
+        "sources": 1
+      },
+      {
+        "distinct_hashes": 1,
+        "height": 4,
+        "layer_states": 175,
+        "sources": 1
+      }
+    ],
+    "integer_hash_modulus": 2305843009213693951
+  },
+  "package_hashes": {
+    "PROOF.md": "5571b0e6329f620c4bf58e90fb03ce4dfefae95708435739f8fac5e78aa52c9b",
+    "source_index.py": "589876e684b98bc8441e88079263b64724d64e17f734955362e54d55bfba6e64",
+    "verify.py": "b753fa3954085ba9eac1837b2e2f1ac64b623c403160ae6fb221ad2dbcf9dbac"
+  },
+  "sources_checked": 314,
+  "status": "PASS_SOURCE_INDEX_PEER_FUNCTIONAL_CHECKS"
+}
diff --git a/research/lockstep-source-row-index/NOTICE.md b/research/lockstep-source-row-index/NOTICE.md
new file mode 100644
index 0000000000..e31ef217a0
--- /dev/null
+++ b/research/lockstep-source-row-index/NOTICE.md
@@ -0,0 +1,24 @@
+# Notice
+
+New source-subtree counting, contiguous indexing, proof and checks: prepared
+for Jerry Chen (@CubeJerry), 2026, with substantial OpenAI assistance.
+Apache-2.0.
+
+`inputs/pascal_codec.py` is unchanged from CubeJerry/integer-mult-bounds
+commit `91246e5131152ccb1f64a969c36706360861f821`, path
+`research/pascal-occurrence-codec/codec.py`. Its header and attribution remain.
+
+`inputs/finite_dag_audit.py` is unchanged from CrocSwap/integer-mult-bounds
+commit `e54523517d0f03e58352e647c403a5af3e525a57`, path
+`research/kappa-rebuild/transfer-audit/finite_dag_audit.py`. Its Apache-2.0
+and substantial OpenAI-assistance header remains. Credit zxv and the source's
+retained predecessors, especially Jacob Alan Sussman's Theorem 1G flow.
+
+Mark / Matarener's #4691 live-role work and the #6878 occurrence-layout work
+are cited predecessor contracts. This contribution does not claim their
+Pascal flow, native semantics or physical tariffs as new results.
+
+Independent AI peer review identified the initial data-dependent hash-table
+complexity defect and the need to price metadata access separately. The
+repaired sorted-table implementation, adversarial collision family and
+serialized-table bound retain that audit's substance in PROOF.md.
diff --git a/research/lockstep-source-row-index/PR.md b/research/lockstep-source-row-index/PR.md
new file mode 100644
index 0000000000..e8834ab8f1
--- /dev/null
+++ b/research/lockstep-source-row-index/PR.md
@@ -0,0 +1,79 @@
+## Change and mathematical scope
+
+The published [Pascal occurrence codec](https://github.com/CubeJerry/integer-mult-bounds/tree/91246e5131152ccb1f64a969c36706360861f821/research/pascal-occurrence-codec)
+left contiguous source indexing open. This adds exact rank/unrank between
+fresh source occurrences and every integer in `[0,S_N)`, extending to all
+replicated productive rows `[0,a*S_N)`. Owned banks receive no productive
+source credit.
+
+The subtree count depends only on depth, paid-rank product and last paid
+rank. With q distinct paid ranks and d target ranks, at most
+`1+q*binom(G+q-1,q)` states and `binom(G+d,d)` target multiindices suffice.
+This avoids enumerating the chronological class tree or each multinomial
+occurrence. The proof includes exact ordering, state/count bit sizes and
+separately charged deterministic setup/query work. Sorted level lists and
+binary-search count tables remove hash-dispersion assumptions. A separate
+serialized-table construction charges metadata access on fixed tapes.
+
+**No new kappa and no complete assumption discharge.** The selected
+conditional value remains 0.00363005817.
+
+## Why it matters and what is new
+
+This supplies actual integer row names for the preceding symbolic owner
+codec, resolving its first open question and advancing #6878's occurrence
+emitter obligation. The inherited Pascal flow, live-role correctness and
+rank descent are not new claims. Distinct paid positions retain separate
+physical intervals even when their subtree statistics are identical.
+
+## Verification
+
+```sh
+python3 -I -W error -B research/lockstep-source-row-index/verify.py
+python3 -I -W error -O -B research/lockstep-source-row-index/verify.py
+```
+
+Both modes agree on 102 complete literal small flows and all 1,431 fresh
+source ranks/inverses, including replicated row intervals, plus fourteen
+rejecting controls. A height-64 fixture needs 4,161 states despite a class
+tree exceeding 5*10^30 nodes. A different ordered-word-product counter
+corroborates all 4,161 state totals using incoming-unit subtraction.
+The exact source-count and interval samples are recorded in VALIDATION.json.
+
+Independent review found and corrected a worst-case complexity defect in
+the initial hash-table implementation. A fixed five-paid-rank rule makes
+every same-depth state hash identically; the repaired checker verifies its
+3,961 states at height 8. PROOF.md preserves the obstruction and explicitly
+separates indexed arithmetic/comparison work from paid serialized scans.
+
+The unchanged predecessor codec and literal oracle are source-hashed.
+The ambient-property test adapter and source-aware comparison are disclosed.
+Canonical base: `e54523517d0f03e58352e647c403a5af3e525a57`.
+Codec dependency: `91246e5131152ccb1f64a969c36706360861f821`.
+
+Separate functional and cost-model reviewers passed the repaired snapshot.
+The independent checker uses literal ordered role words instead of the
+author's source-count recurrence and covers 16 cases, 314 sources and all
+1,570 replicated rows; four exact collision families also pass. From this
+package directory run `python3 -I -W error -B independent_check.py .`.
+REVIEW.md and COST-MODEL-REVIEW.md preserve both the original objection and
+the accepted correction; INDEPENDENT-RESULT.json pins the executed snapshot.
+
+## Limitations and next obligations
+
+The selected finite product's complete role/paid-owner manifest remains
+required. This does not execute source-complement grouping, smaller-rank
+substitution, owned allocation, payload access or the physical tape caller.
+Its canonical row numbering need not equal incidental numeric IDs in an
+older interpreter. Any layout conversion retains its actual movement bill.
+All selected native, compiler, precision/tape and analytic conditions remain.
+No practical winning-rank materialization, supplier admission, human proof
+or formal-kernel acceptance is asserted.
+
+## Credit
+
+Prepared for Jerry Chen / **@CubeJerry** with substantial OpenAI assistance.
+Credit the preceding occurrence-codec publication and separate root AI review,
+Jacob Alan Sussman's lockstep/Pascal construction, zxv's compiler and literal
+audit, Mark / Matarener's #4691 executor, and the #6878 geometry lineage.
+Original dependency files and notices are unchanged. Apache-2.0.
diff --git a/research/lockstep-source-row-index/PROOF.md b/research/lockstep-source-row-index/PROOF.md
new file mode 100644
index 0000000000..0016c418cb
--- /dev/null
+++ b/research/lockstep-source-row-index/PROOF.md
@@ -0,0 +1,306 @@
+# Contiguous source indices from aggregated chronological subtrees
+
+## 1. Domain and declared order
+
+Use the separated finite rule and the exact occurrence/owner codec at
+CubeJerry commit `91246e5131152ccb1f64a969c36706360861f821`,
+`research/pascal-occurrence-codec/`. Its fixed role list has W productive
+roles of ranks `k_i>=2`, with d distinct target ranks and multiplicities W_i.
+There are P ordered paid occurrences with positive ranks strictly below
+`k_min`; their q distinct ranks have multiplicities P_r. The actual ambient
+cap A satisfies `A>=k_max`. For integer N>=A set
+
+`G=max{g:A*k_min^g<=N}`.
+
+A unit `(p,alpha,v)` has `|p|+|alpha|=G`, column
+`rho(p)c(alpha)`, fit `A rho(p)c(alpha)<=N`, and
+`0<=v<u(alpha)`, with c and u as in the predecessor. Each paid position,
+productive role and owned bank retains its separate identity.
+
+Number fresh sources in this fixed order:
+
+1. Visit classes in depth-first preorder, with children in actual paid-position
+   order. The class's own fresh inputs precede its child classes.
+2. Within one class, visit unit multiindices lexicographically, unit ordinals
+   increasingly, then roles in the native role-list order; keep only fresh slots.
+
+This is a declared canonical row numbering, compatible with the direct
+per-unit source order in the #4691 executor. It need not equal the incidental
+numeric source IDs allocated by `finite_dag_audit.py`'s dictionary of augmented
+points. No job, native instruction or paid occurrence is reordered. The new
+numbers specify which independent input array occupies each existing source
+slot; changing an already stored external layout still requires the caller's
+charged row permutation.
+
+## 2. Exact source counts at one class
+
+For a class at depth h let rho be its paid-rank product. If h>0, let r be
+the rank of its last paid occurrence. At the root use state `(0,1,0)`.
+The state for counting is therefore `(h,rho,r)`; it is not a physical owner ID.
+
+For any fitting multiindex alpha of degree G-h define the number of fresh
+roles per unit by
+
+`F(h,rho,r;alpha)
+ = sum_i W_i * 1[h=0 or A*(rho/r)*c(alpha)*k_i>N]`.
+
+At h=0 the predicate is defined to be true without dividing by zero. The
+local source count is
+
+`C(h,rho,r)
+ = sum_(|alpha|=G-h, A*rho*c(alpha)<=N) u(alpha)*F(h,rho,r;alpha)`.
+
+This is the predecessor's exact absence-of-parent test. For a present
+parent the complete Pascal interval is available, because `r<k_min`.
+Consequently there is no partially supplied bucket and the formula counts
+all and only fresh inputs. The count depends on h, rho and r, rather than
+the whole paid path or its owner values.
+
+The last rank is necessary. For targets `{3:1,5:1}`, ambient A=5,
+paid ranks 1 and 2, and N=45, G=2. At depth 2 and rho=2,
+
+`C(2,2,1)=1`, while `C(2,2,2)=0`.
+
+The two paths have identical dilation but different parent capacities. A
+cache keyed only by depth and dilation would be incorrect.
+
+As a separate count identity, let U(h,rho) be the number of units in that
+class. Then
+
+`C(0,1,0)=W*U(0,1)`,
+`C(h,rho,r)=W*U(h,rho)-U(h-1,rho/r)` for h>0.
+
+Every parent unit supplies exactly one target slot at that paid position;
+the inherited bijection supplies all of them. This identity provides an
+alternative way to verify the local source counts. It does not merge the
+physical fields of distinct classes.
+
+## 3. Subtree aggregation and polynomial state count
+
+Let T(h,rho,r) be the total fresh sources in the complete subtree beginning
+at that class. At h=G, put T=C. For h<G use
+
+`T(h,rho,r)=C(h,rho,r)+sum_s P_s*T(h+1,rho*s,s)`.
+
+All states refer to positive finite integers. Induction on G-h proves the
+recurrence: first count this class, then each actual paid occurrence's child
+subtree. Equal paid ranks have identical *counts*, so their multiplicity
+P_s may multiply one cached value. They still occupy separate consecutive
+intervals in actual paid-position order. In particular, they must not be
+collapsed into one physical source interval.
+
+There is a fitting unit at every class path of depth h<=G: its minimum
+possible column is at most `r_max^h*k_min^(G-h)<=k_min^G<=N/A`.
+The recurrence therefore describes the same full depth-G class tree as the
+separated predecessor. Empty source blocks and subtrees are permitted;
+they have count zero and are skipped in indexing.
+
+At a positive depth h, fix the last rank s. The preceding h-1 paid ranks
+are described, for their product, by a multiplicity vector on q values.
+There are `binom(h+q-2,q-1)` such vectors. Multiplicative coincidences can
+only reduce the number of distinct products. Summing over last ranks and
+depths bounds the total number of cached states by
+
+`R = 1 + q*binom(G+q-1,q)`.
+
+Use `binom(q-1,q)=0` when G=0; the bound is then one. At q=1 the formula
+is G+1. No factorization of paid ranks or enumeration of paid paths is needed.
+Keep each level sorted by `(rho,r)`. First remove adjacent repeated rho
+values, then form `(rho*s,s)` for each remaining rho and distinct paid rank s.
+These candidates are already distinct: equality forces the same s and then
+the same rho. Comparison sorting and adjacent deduplication produce the next
+sorted level. Thus the temporary candidate list has exactly the next level's
+state count; it is not q times a list containing duplicate dilations.
+
+All target multiindices needed at degrees 0 through G number exactly
+
+`M = sum_(g=0..G) binom(g+d-1,d-1) = binom(G+d,d)`.
+
+They may be enumerated once with c(alpha) and u(alpha), then scanned by the
+capacity predicate. This enumerates neither the u(alpha) individual unit
+occurrences nor the P^G paid paths. R and M are polynomial in G for fixed
+finite rank alphabets q,d. No polynomial bound with a degree independent
+of varying q,d is asserted.
+
+## 4. Rank and unrank are inverse
+
+Set `S_N=T(0,1,0)>0`. To rank a fresh source with path p, start at the root
+with offset zero. For every selected paid position j on its path, add the
+current class's C and the T values of all preceding paid positions; then
+descend to j. This gives the number of sources before the destination class.
+
+Within that class, for every fitting multiindex beta preceding alpha add
+`u(beta)*F(beta)`. For alpha add
+
+`v*F(alpha) + #{fresh native roles preceding the given role}`.
+
+Reject a role whose parent is present. This yields an integer in `[0,S_N)`.
+
+To unrank `x in [0,S_N)`, compare x to the current class's local C. If x<C,
+scan its nonzero multiindex blocks in order. In the unique block containing
+x, division by F gives its unit ordinal v and remainder indexing the fresh
+native roles. If x>=C, subtract C and skip complete child intervals in actual
+paid-position order until reaching the one containing x; descend and repeat.
+At each descent h increases, so there are at most G descents. Zero-size
+intervals are simply skipped. The half-open intervals partition the current
+state's total, so a valid x cannot fall outside them.
+
+Induction over this finite interval decomposition proves both inverse
+identities. Consequently fresh source occurrences are in bijection with
+every integer in `[0,S_N)`, not merely with a sparse set of large labels.
+The distinction between source roles at the same target rank and between
+equal-rank paid occurrences is preserved.
+
+For a positive integer replica count a, the full finite compiler has the
+source width `B_N=a*S_N`. Encode a source in replica b as
+
+`row = b*S_N + rank(source)`,  for `0<=b<a`.
+
+Euclidean division by S_N recovers b and the local source index. The namespace
+identifies the particular invocation's row arena. Owned-bank identifiers are
+rejected: they are not independent productive sources and receive no row credit
+from this bijection. A productive role first resolved by the predecessor codec
+can now be assigned its concrete row integer when its ultimate owner is a source.
+Owned ultimate owners retain their separately reserved bank identity.
+
+## 5. Bit sizes, setup, and query work
+
+Counting a subtree does not require storing a source for every occurrence.
+At depth h there are at most `P^h*W^(G-h)` units. Therefore
+
+`S_N <= W*sum_(h=0..G) P^h W^(G-h)
+     <= (G+1)*W*max(W,P)^G`.
+
+Every source or subtree count thus has
+`O(log(G+1)+log W+G log(max(W,P)))` bits. Point products have at most
+`O(G log A)` bits even when a point is later discarded by the capacity test.
+The number of classes can be exponential while their exact counts have only
+linear-in-G bit length.
+
+Let S be the bit size of the finite input specification, including its role
+and paid-position lists, namespace and replica count a. Put
+
+`B=S+ell(N)+(G+1)*ell(A+W+P+G+2)+1`,
+
+where `ell(x)=ceil(log2(x+1))`. All relevant arithmetic fits O(B) bits.
+Use the following logical operation envelopes:
+
+`K_setup=(S+1)^2 * [M(G+d+1)+R(M(d+1)+q+1)]`,
+
+`K_query=(S+1)^2 * [M(d+1)+G*P+G+d+1]`.
+
+There are two distinct access models below. Neither grants free physical
+payload access.
+
+### Deterministic indexed metadata algorithm
+
+The supplied implementation uses a list of point profiles, sorted level
+lists, and two value arrays sharing one immutable sorted vector of all
+state keys. `SortedStateTable` locates a key by binary search and verifies
+exact equality. No expanding state set or dictionary occurs. The only
+remaining hash collections are over the fixed input specification (the
+paid-rank Counter and predecessor rule validation/type lists). Even total
+collision there costs at most a quadratic factor in S, already included.
+
+For the arithmetic/comparison count, an indexed metadata record can be
+retrieved/copied into arithmetic workspace with its bit length charged;
+physical travel to that record is a separate model below. A state key
+comparison costs O(B), and a lookup makes O(log(R+1)) comparisons. Since
+`R<=sum_(h=0..G) P^h`, `log(R+1)=O(B)`. Hence each lookup costs O(B^2)
+in this indexed model, including index arithmetic and record bits.
+Sorting all state levels costs O(R log(R+1)) key comparisons; forming
+their candidates and all child count queries fits O(qR) operations.
+These costs are included in `K_setup*B^2`.
+
+Exact small-factor binomial arithmetic and schoolbook multiplication/
+division therefore give these intentionally loose bounds:
+
+* Setup indexed arithmetic/comparison work: `O(K_setup*B^2)`.
+* Stored input, state counts and target profiles: `O((S+R+dM)*B)` bits.
+* A valid rank or unrank query after setup: `O(K_query*B^2)` indexed
+  arithmetic/comparison work.
+
+The bounds include capacity tests, repeated role lookup, all count
+comparisons and lookups, multiplication/division, interval subtraction and
+replica encoding. A malformed query's reading/rejection cost also depends
+on its supplied length; no bounded-length claim is made for arbitrary
+oversized invalid input. These are deterministic bounds, with no average
+hash dispersion premise and no unit-cost big-integer arithmetic premise.
+They are not by themselves fixed-tape time bounds.
+
+### Conservative serialized-table simulation
+
+A separate implementation removes indexed metadata access. Set
+
+`L=(S+R+dM+1)*B`.
+
+Serialize the input, profiles, state keys and counts on a fixed number of
+binary work tapes using delimiters, with total length O(L). Keep only
+O(B)-bit scalar arithmetic registers and one current d-component point;
+enumerate the lexicographic profiles with counters rather than retaining a
+recursive stack of tuple copies. Their storage is included in O(L).
+
+Generate each state candidate and insert it into a sorted serialized level
+by one scan and copy to a spare tape, discarding equality matches. There
+are at most qR candidates; the unique stored keys remain bounded by R.
+For each logical count lookup or update, scan the serialized key table,
+compare with the current key, and copy/update its value. This linear scan
+replaces the implementation's binary search; it does not simulate a random
+access instruction for free. An O(L)-bit scan with binary position/extent
+counters, key comparisons, copying and head return takes at most O(LB)
+local operations. Shifting an encoded record, retiring the spare copy,
+and restoring cursors fit the same conservative O(L^2) allowance.
+Schoolbook O(B^2) arithmetic also fits because B<=L.
+
+Charge O(L^2) to each logical operation counted in K_setup or K_query,
+including each candidate insertion. This gives the standalone offline
+metadata bounds
+
+* Setup: `O(K_setup*L^2)` fixed-tape time and O(L) workspace.
+* A valid query after setup: `O(K_query*L^2)` fixed-tape time and O(L)
+  workspace, including retained metadata.
+
+An optional final erasure of this bounded private workspace costs O(L)
+and fits these bounds. This is a conservative simulation construction,
+not a claim that the Python interpreter is that tape machine or a binary
+lowering of the selected multiplier. Both models remain polynomial in G
+and log N for a fixed native rule.
+
+### Collision audit and correction
+
+An independent peer review rejected the earlier unqualified hash-table
+work claim. Let H be Python's positive integer hash modulus; the
+[Python 3.12 numeric-hash specification](https://docs.python.org/3.12/library/stdtypes.html#hashing-of-numeric-types)
+gives hash(x)=x mod H for nonnegative integers. Fix one role
+of rank 8H, ambient A=8H, and five paid ranks H,2H,3H,5H,7H. Take
+`N=A*(8H)^G`. At positive depth h there are exactly
+`5*binom(h+3,4)` distinct states, but hash(rho)=hash(last)=0 for every one;
+all same-depth CPython tuple hashes therefore coincide. Building the old hash
+sets incurs quadratic probing work per level, totaling Omega(G^9), while
+the former displayed fixed-rule estimate was only O(G^8 log^2 G).
+The indexing bijection was unaffected; its data structure did not satisfy
+that claimed worst-case tariff. Sorted comparison tables remove this
+premise. The verifier includes the same fixed-rule collision family at
+G=8, checks all 3,961 state counts and the one source row, and rejects
+absent, unordered, duplicate or uninitialized table entries. These checks
+are structural controls, not timing evidence for the universal bound.
+
+The emitted row identifier needs O(log a + log S_N) bits. Issuing its actual
+array access still requires the caller's movement, restoration and routing
+bill. This theorem does not make a lookup, gather, COPY, erase or whole-row
+permutation free.
+
+## 6. Relation to the unfinished selected compiler
+
+The predecessor codec left contiguous fresh-source rank/unrank open. This
+theorem closes that logical indexing obligation and supplies exact integer
+row names compatible with replication `B_N=a*S_N`. Together the two codecs
+specify a productive occurrence's ultimate source row without materializing
+the class tree or source array list.
+
+The selected finite product's actual role/paid-owner manifest is still a
+required input. Neither its 1920-fold expansion nor its winning N is emitted.
+Integer batching factors, source complements, nested smaller-rank programs,
+owned-bank allocation and the native/tape endpoints remain separate contracts.
+The selected five assumptions and kappa are unchanged. No complete multiplier,
+physical source access tariff or unconditional theorem follows.
diff --git a/research/lockstep-source-row-index/README.md b/research/lockstep-source-row-index/README.md
new file mode 100644
index 0000000000..9d8b199ac6
--- /dev/null
+++ b/research/lockstep-source-row-index/README.md
@@ -0,0 +1,147 @@
+# Index every replicated compiler source row using polynomially many chronological states
+
+**Scoped constructive compiler result; no new kappa.** Every fresh source
+of a separated finite mixed-target flow now has an exact contiguous row
+index, with an inverse that recovers its occurrence. Counting shares only
+subtree statistics; distinct chronological occurrences and physical rows
+retain their identities.
+
+The [preceding occurrence codec](https://github.com/CubeJerry/integer-mult-bounds/tree/91246e5131152ccb1f64a969c36706360861f821/research/pascal-occurrence-codec)
+resolved a productive field to a symbolic source or owned-bank name. Its
+first open question was to rank fresh source names into physical row intervals.
+This package closes that logical indexing question and connects its source
+names to integers `0,...,a*S_N-1` for the actual replication count a. Owned
+banks are excluded from productive row credit.
+
+## Exact theorem
+
+Let G be the finite flow height, d the number of distinct target ranks,
+and q the number of distinct paid ranks. A class's source-subtree count
+depends only on depth, paid-rank product and the **last paid rank**. The
+number of such states is at most
+
+`R=1+q*binom(G+q-1,q)`.
+
+The required target multiindices number `M=binom(G+d,d)`. Both are
+polynomial in G for fixed finite rank alphabets. The algorithm enumerates
+neither every paid path nor all unit occurrences of a multiindex. Its
+rank/unrank query follows one chronological path and skips whole intervals.
+
+[PROOF.md](PROOF.md) gives the exact source-count recurrence, inverse proof,
+bit sizes, deterministic sorted-table setup/query costs, and a separately
+charged conservative serialized-table simulation. The declared
+source order is depth-first class preorder, lexicographic unit multiindex,
+unit ordinal and native role order. This canonical numbering can differ
+from the literal audit's incidental numeric IDs; it leaves job chronology
+and owner identity unchanged.
+
+Two details are essential:
+
+* Equal paid ranks may share cached counts, but their actual occurrence
+  multiplicities and positions remain in every source interval.
+* The last rank cannot be dropped from the state: at one exact fixture,
+  equal depth and dilation have local source counts 1 and 0 depending on
+  that last rank.
+
+## Evidence and reproduction
+
+After placing this directory at `research/lockstep-source-row-index/`, run:
+
+```sh
+python3 -I -W error -B research/lockstep-source-row-index/verify.py
+python3 -I -W error -O -B research/lockstep-source-row-index/verify.py
+```
+
+Both standard-library Python 3.12 commands print
+`PASS_CONTIGUOUS_SOURCE_INDEX`; the local outputs agree exactly.
+
+The literal predecessor oracle supplies 102 complete small flows, with
+555 classes, 1,005 native units and 1,431 fresh sources. Every fresh source
+is checked against its exact sorted literal rank and inverse, including
+replica 0 and replica 2 in a three-replica row interval. Fourteen controls reject
+lost paid multiplicities, out-of-range indices, a wrong namespace, owned
+bank credit, a matched role masquerading as a source, omitted last-rank
+state, invalid occurrence ordinals and physical merging of equal-statistic
+sibling classes, as well as absent, unordered, duplicate and uninitialized
+state-table entries.
+
+A separate height-64 fixture indexes
+
+`20,857,390,061,882,631,902,013,162,838,873,341,952` source rows
+
+using **4,161** states and **2,145** target multiindices. Its complete class
+tree has more than `5*10^30` classes and is not enumerated. Five interval
+positions round-trip. A different counting method independently corroborates
+every one of those 4,161 state totals: it counts ordered target words by their
+product, then obtains fresh inputs by subtracting incoming parent-unit counts.
+This alternative uses the same inherited flow theorem, rather than an
+independent proof kernel.
+
+An independent peer review found that the original hash-based state tables
+did not support their advertised worst-case work bound. The repaired
+algorithm uses sorted/deduplicated level lists, one shared sorted key vector
+and binary-search count tables; target profiles use a list. The verifier
+includes a fixed rule with paid ranks proportional to Python's integer hash
+modulus: at height 8 its **3,961** states collide within every depth, yet all
+counts and its source-row inverse pass. The proof retains the explicit
+counterexample and correction rather than treating hash behavior as an
+average-case premise.
+
+The retained literal oracle and the preceding codec are copied byte-for-byte
+under `inputs/` and authenticated before use. Their source commits, Git blobs
+and SHA256 values are in [SOURCES.json](SOURCES.json). An explicit adapter
+sets the literal oracle's ambient cap; its matching and source computation
+remain unchanged. Verification is source-aware, not a blind experiment.
+
+## Significance and limits
+
+The result supplies concrete integers for the productive source inputs of
+the finite compiler, which previously had only symbolic occurrence names.
+For fixed native rank alphabets, the metadata construction has polynomial
+arithmetic/comparison work in the flow height and input bit sizes. A separate
+serialized-table construction also has an explicit conservative polynomial
+fixed-tape bound, including metadata scans and head return. This does not imply a
+practical construction at the selected astronomical compiler parameters.
+
+The selected conditional value remains **0.00363005817**, and all five
+selected assumptions remain. A row integer does not provide constant-time
+payload access. The full selected product/paid-owner manifest, grouped source
+complements, smaller-rank substitutions, owned-bank allocation and all actual
+native, precision and fixed-tape costs remain separate obligations. No
+complete multiplier, new supplier, human review or formal-kernel acceptance
+is claimed.
+
+This is a source-indexing successor to the published codec, with independent
+base `e54523517d0f03e58352e647c403a5af3e525a57`. The source proof/code,
+#4691 live-role executor, and #6878 occurrence-layout work were checked for
+overlap. Targeted all-state PR searches for source rank/unrank/compiler,
+source indexing and subtree/Pascal did not locate this construction; those
+bounded searches do not establish universal priority.
+
+## Open next questions
+
+1. **Integrate source rank groups with complement batches.** Supply exact
+   index/rank maps for one source-rank bucket and its complementary program.
+   The present numbering covers all sources in chronological order; it does
+   not execute grouping or the associated physical permutation.
+2. **Bind the real selected product manifest.** Emit the actual role and
+   paid-owner lists for a smaller complete product, then use both codecs on
+   that source. The final 1920-fold template is still unmaterialized.
+3. **Price one actual row dispatcher.** Lower the integer indices to a
+   declared tape representation and account for access, head return,
+   preservation, copies and erasure. Offline indexing supplies no zero-cost
+   field lookup or native endpoint.
+
+## Credit
+
+Prepared for **Jerry Chen / @CubeJerry**, with substantial OpenAI assistance.
+The preceding codec and its root's separate AI review retain their exact
+publication and evidence. Jacob Alan Sussman supplies the integer Pascal/
+lockstep flow; zxv supplies the finite compiler and literal audit; Mark /
+Matarener supplies the live-role executor; @CubeJerry and retained geometry
+contributors supply #6878's occurrence routes. The reused files retain their
+original headers. Apache-2.0; see [NOTICE.md](NOTICE.md).
+
+## Separate independent reviews
+
+[REVIEW.md](REVIEW.md) preserves the initial collision finding and its repaired disposition. A different worker reviewed metadata access and serialized-tape costs in [COST-MODEL-REVIEW.md](COST-MODEL-REVIEW.md). Run `python3 -I -W error -B independent_check.py .` from this directory for the separate ordered-word oracle: 16 cases, 314 sources, all 1,570 replicated rows and four collision-family controls. Its final receipt is [INDEPENDENT-RESULT.json](INDEPENDENT-RESULT.json).
diff --git a/research/lockstep-source-row-index/REVIEW.md b/research/lockstep-source-row-index/REVIEW.md
new file mode 100644
index 0000000000..ae74bd7b7b
--- /dev/null
+++ b/research/lockstep-source-row-index/REVIEW.md
@@ -0,0 +1,194 @@
+# Independent review of the contiguous compiler source-row index
+
+Reviewer: separate analytic-recovery research agent, prepared for CubeJerry
+with substantial OpenAI assistance. This is independent AI reasoning and
+bounded execution, not independent human review or formal-kernel acceptance.
+No author source file was edited by this reviewer.
+
+**Final disposition: PASS after deterministic-table repair.** The initial findings below are historical; accepted final hashes and model-specific bounds appear in the repaired-version section.
+
+## Initial reviewed version and disposition
+
+Initial `source_index.py` SHA256:
+`589876e684b98bc8441e88079263b64724d64e17f734955362e54d55bfba6e64`.
+The exact proof, verifier and executable hashes inspected by each replay
+are recorded in INITIAL-REVIEW-RESULT.json and INDEPENDENT-RESULT.json. The initial logical indexing theorem passes
+this review. Its advertised universal implementation bit-work bound has
+a material hash-map qualification requiring repair before publication.
+The root and author were notified and a deterministic-table repair is in
+progress. A later addendum must record the repaired hashes and disposition.
+
+## Mathematical checks
+
+The local count depends exactly on depth h, paid-rank product rho, and last
+paid rank r. At child multiindex alpha, a productive type k_i is fresh iff
+the issuing parent point alpha+e_i at dilation rho/r is absent. The parent's
+fit is `A*(rho/r)*c(alpha)*k_i <= N`. The strict separated-rank hypothesis
+r<k_min ensures a fitting parent supplies a fully fitting Pascal bucket;
+there is no partial bucket hidden in this test. Summing native roles with
+the same rank by W_i is appropriate for counts, while row enumeration keeps
+their distinct native-list identities.
+
+The last rank cannot be dropped. At A=5, targets 3 and 5, N=45, G=2,
+the state (h,rho)=(2,2) has one fresh role when r=1 (the rank-five parent
+would need capacity 50), and zero when r=2 (parent requirements 15 and 25).
+The dependence on owner labels disappears only in the count; it does not
+merge physical owner identities.
+
+The subtree recurrence multiplies each equal-rank child count by its number
+of actual paid positions. Its state cap
+`1+q*binom(G+q-1,q)` follows by fixing the last rank and counting multisets
+of h-1 earlier ranks. Multiplicative coincidences only decrease this cap.
+Every chronological class exists because a repeated minimum-target word
+fits at every h<=G under r_max<k_min. The total target-profile count
+`binom(G+d,d)` includes degree zero. These formulas handle G=0 and q=1.
+
+The declared order is depth-first class preorder followed by lexicographic
+multiindex, ordinal and actual native role order. Lexicographic finite
+path tuples have exactly this preorder, including empty paths and prefixes.
+The rank algorithm skips disjoint half-open child/source intervals; unrank
+chooses the unique containing interval. Local zero blocks and zero subtrees
+are safely skipped. Equal paid ranks still have separate consecutive child
+intervals. Replica offsets b*S_N and Euclidean division give the claimed
+contiguous product interval, and `kind == source` excludes all owned banks.
+
+Source-count bits fit the stated bound since there are at most
+P^h W^(G-h) units at depth h and at most W fresh roles per unit. Products
+and binomial intermediates have O(B) bits with the supplied B. The missing
+cost item in the initial version is data-structure access, not the counts
+or the size of those integer operands.
+
+## Exact collision family against the original setup tariff
+
+On the tested CPython 3.12 interpreter let
+
+    H = sys.hash_info.modulus = 2305843009213693951.
+
+Use one productive target rank 8H, ambient A=8H, and five paid positions
+of ranks H*(1,2,3,5,7), all owned by that productive role. Set
+N=A*(8H)^G. This is a fixed separated finite rule with d=1,q=P=5,W=1.
+
+At every positive depth, rho and the last paid rank are multiples of H,
+so their integer hashes are zero. Consequently every tuple (rho,last)
+in that level has the same hash. The four independent prime exponents
+2,3,5,7 show that the exact number of distinct states at depth h is
+`5*binom(h+3,4)`. The bounded check confirms 5,25,75,175 distinct states
+at h=1,2,3,4 respectively, each level with exactly one hash. The correct
+source count is one; the indexing semantics are unaffected.
+
+Python's hash-based deduplication and state dictionaries cannot be priced
+as uniformly bounded or logarithmic lookup operations on this family.
+Identical-hash open-address insertion has quadratic collision work in the
+number of distinct level keys. Summing the level lower bounds gives
+Omega(sum h^8)=Omega(G^9) equality/probe work. For this fixed rule the
+initial displayed setup expression is O(G^8 log^2 G). Thus its use as a
+universal tariff for the supplied hash-map implementation is unsound.
+The finite witness establishes the actual collision pattern; the polynomial
+exponents follow from the all-size family, not timing extrapolation.
+
+A deterministic repair is to sort candidate level pairs and deduplicate
+adjacent equal entries, then use sorted state keys with binary-search values
+and list-indexed degree profiles. `log R=O(B)` follows from the class-tree
+count, so comparison-based metadata lookup can be charged explicitly.
+An actual sequential tape/bit-machine statement additionally needs to pay
+metadata movement; a conservative serialized-table full scan is sufficient
+to retain polynomial work for fixed alphabets, even if it is much looser.
+No constant-time payload access follows from any metadata representation.
+
+## Independent executable evidence
+
+From the workspace root:
+
+```sh
+python3 -I -W error -B independent_check.py .
+```
+
+Expected initial result:
+
+```text
+PASS_SOURCE_INDEX_PEER_FUNCTIONAL_CHECKS cases=16 sources=314 hash_collision_cases=4
+```
+
+The oracle enumerates ordered native-role words, actual paid-position paths
+and physical role identities before sorting the resulting fresh sources.
+It does not use the author's multiplicity, parent, local-count, block or
+subtree implementations to build expected intervals. The 16 cases include
+four distinct paid ranks, multiplicative coincidences such as 2*3=6,
+duplicate paid positions and target ranks, one-target families, empty child
+source blocks, G=0..3 and all five replicas. Every one of 314 independent
+source rows is ranked and unranked, and all 1,570 replicated rows checked.
+Out-of-range rows and owned-bank source credit reject.
+
+These checks and the written argument support the logical theorem at its
+stated inherited-flow boundary. The real selected product manifest, full
+compiler emission, physical source access, owned allocation, compiler
+assumption and multiplication bound remain unproved by this package.
+
+
+# Repaired-version disposition: pass at the declared scope
+
+The deterministic-table repair resolves the setup-tariff objection in
+REVIEW.md. Reviewed SHA256 values:
+
+- source_index.py: `e978025591b06770026b9879f1e5b10827424f410794fb2b1e1f10a720f49176`
+- PROOF.md: `1631e28072e1ad39c3833ec83ff7d59e35c4d8fd1ad45ebce6b777aed4125bdb`
+- verify.py: `fb89cad83c3ed69bffaf2a95347b21d26dde4da1dc9c52b4304e7d94d836f623`
+
+The author now generates states in sorted lists, deduplicates prior dilations
+before multiplying by each next distinct paid rank, and stores both count
+tables under one immutable sorted key vector with binary-search values.
+Degree profiles are list-indexed. Growing state-table access no longer relies
+on hash dispersion. Remaining hash collections are over the fixed input rule;
+their worst-case quadratic work fits the specification-size factor.
+
+The dilation deduplication preserves the storage bound. Prior `(rho,last)`
+pairs are sorted, so equal rho values are adjacent. At fixed next rank r,
+multiplication is injective in positive rho. Different next ranks give
+different last-rank fields. Thus the generated candidate count is exactly
+the next level's state count, with no q-times duplicated buffer hidden
+under the O(R) state envelope.
+
+The revised proof separates two access models. In the indexed metadata model,
+a key comparison costs O(B), binary search uses O(log(R+1)) comparisons, and
+log(R+1)=O(B) follows from the chronological class-tree bound. Comparison
+sorting and lookup fit the displayed arithmetic bound. Travel to a metadata
+record is explicitly excluded from that bound.
+
+The separate sequential simulation serializes metadata of length
+L=(S+R+dM+1)B and charges O(L^2) per logical operation, including candidate
+insertion, metadata scans, copying, shifting, arithmetic and head returns.
+O(L) stored representation plus a spare copy and O(B)-bit scalar registers
+supports this conservative simulation. This is a described offline
+simulation construction, not a claim that Python is that tape machine or
+that selected multiplier code was emitted. Both costs remain polynomial
+for fixed target and paid-rank alphabets. No free payload access follows.
+
+The independent ordered-word oracle was rerun and again passed 16 cases,
+314 source rows and all 1,570 replicated rows. The same four adversarial
+families retain their proven hash collisions and correct source count;
+the repaired implementation does not use those hashes for state access.
+Exact final results and tested hashes are in INDEPENDENT-RESULT.json. The original defect and witness remain documented above and in PROOF.md.
+
+Reproduction from this package directory:
+
+```sh
+python3 -I -W error -B independent_check.py .
+```
+
+Expected output:
+
+```text
+PASS_SOURCE_INDEX_PEER_FUNCTIONAL_CHECKS cases=16 sources=314 hash_collision_cases=4
+```
+
+Disposition: no remaining objection to the stated logical bijection,
+state-count/storage bounds or revised model-separated costs. The inherited
+flow, selected-manifest, actual row-access and full compiler limitations
+remain. This is independent AI review and bounded execution, not human
+or formal-kernel acceptance.
+
+## Root integration review
+
+The orchestrator read the complete proof, repaired implementation, hash-collision witness and both independent reviews. The mathematical state recurrence, last-rank distinction, complete source interval bijection and conservative serialized-table model passed review. Only packaging and the independent checker's paths were adapted. Reviewed scientific bytes remain frozen. The final self-contained author and independent checks are recorded below through their executable receipts; no complete selected-certificate replay or assumption discharge is claimed.
+
+The root also inspected the primary CPython v3.12.14 sources: [tupleobject.c](https://github.com/python/cpython/blob/v3.12.14/Objects/tupleobject.c), function `tuplehash`, combines only the fixed tuple length and element hashes; [setobject.c](https://github.com/python/cpython/blob/v3.12.14/Objects/setobject.c), functions `set_add_entry` and `set_insert_clean`, use the same deterministic probe sequence for equal hashes. Distinct equal-hash tuples consequently occupy successive positions of that shared probe sequence; insertion of n such keys incurs quadratic probing work. This supports the explicitly CPython-scoped collision witness independently of timing measurements.
diff --git a/research/lockstep-source-row-index/SOURCES.json b/research/lockstep-source-row-index/SOURCES.json
new file mode 100644
index 0000000000..cda1e872c0
--- /dev/null
+++ b/research/lockstep-source-row-index/SOURCES.json
@@ -0,0 +1,25 @@
+{
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "inputs": [
+    {
+      "local_path": "inputs/pascal_codec.py",
+      "source_path": "research/pascal-occurrence-codec/codec.py",
+      "repository": "CubeJerry/integer-mult-bounds",
+      "commit": "91246e5131152ccb1f64a969c36706360861f821",
+      "git_blob": "2fb4426cc821a7e029e5c697787e235c79b4e756",
+      "sha256": "cec2c8b5e153a264127e8301ed59591fe97c9a46078ff2343b3784d177c6984d",
+      "usage": "unchanged vendored executable input"
+    },
+    {
+      "local_path": "inputs/finite_dag_audit.py",
+      "source_path": "research/kappa-rebuild/transfer-audit/finite_dag_audit.py",
+      "repository": "CrocSwap/integer-mult-bounds",
+      "commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+      "git_blob": "c1798bfa9c1d47a40313a276a8ce639c232143e5",
+      "sha256": "f842f0e07ca40a181782a565a381b0ee20c6a4b08b8c2b8a4d5d630381bd1e8e",
+      "usage": "unchanged vendored executable input"
+    }
+  ],
+  "selected_kappa": "0.00363005817",
+  "new_kappa": null
+}
diff --git a/research/lockstep-source-row-index/TASK.json b/research/lockstep-source-row-index/TASK.json
new file mode 100644
index 0000000000..e557175af6
--- /dev/null
+++ b/research/lockstep-source-row-index/TASK.json
@@ -0,0 +1,26 @@
+{
+  "task": "user-assigned second-wave compiler source indexing",
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "predecessor_commit": "91246e5131152ccb1f64a969c36706360861f821",
+  "scope": "contiguous source rank/unrank from polynomially many counting states for fixed rank alphabets",
+  "track": [
+    50,
+    75
+  ],
+  "outcome": "constructive theorem with bounded source comparison",
+  "external_publication": "Verified package prepared by root; no upstream pull request submitted",
+  "registered_hook": false,
+  "overlap_queries": [
+    "repo:CrocSwap/integer-mult-bounds is:pr source rank/unrank compiler",
+    "repo:CrocSwap/integer-mult-bounds is:pr source indexing",
+    "repo:CrocSwap/integer-mult-bounds is:pr subtree Pascal"
+  ],
+  "open_next_questions": [
+    "source-rank grouping and complement batches",
+    "actual selected product owner manifest",
+    "paid fixed-tape row access"
+  ],
+  "repair_gate": "Passed independent functional and cost-model reviews after deterministic-table repair; accepted hashes are recorded in both review files.",
+  "frozen_for_review": true,
+  "root_reproduction": "Strict normal and optimized author verifiers and independent checker passed from final self-contained package"
+}
diff --git a/research/lockstep-source-row-index/VALIDATION.json b/research/lockstep-source-row-index/VALIDATION.json
new file mode 100644
index 0000000000..7af9a9c351
--- /dev/null
+++ b/research/lockstep-source-row-index/VALIDATION.json
@@ -0,0 +1,69 @@
+{
+  "python": "3.12.14",
+  "platform": "Linux-6.18.57-x86_64-with-glibc2.41",
+  "normal_exit": 0,
+  "optimized_exit": 0,
+  "mode_outputs_equal": true,
+  "result": {
+    "collision_family": {
+      "hash_modulus": "2305843009213693951",
+      "height": 8,
+      "lookup": "sorted keys and deterministic binary search",
+      "source_count": 1,
+      "state_hashes_per_positive_depth": 1,
+      "states": 3961,
+      "states_per_positive_depth": [
+        5,
+        25,
+        75,
+        175,
+        350,
+        630,
+        1050,
+        1650
+      ]
+    },
+    "large_case": {
+      "height": 64,
+      "independent_word_product_states": 4161,
+      "literal_classes_not_enumerated": "5150525730438768726986773633921",
+      "round_trip_samples": 5,
+      "source_count": "20857390061882631902013162838873341952",
+      "states": 4161,
+      "target_multiindices": 2145
+    },
+    "negative_controls": [
+      "dropped repeated paid occurrence",
+      "source upper endpoint",
+      "negative source index",
+      "replicated row upper endpoint",
+      "wrong namespace",
+      "owned bank credited as source",
+      "matched role passed as fresh source",
+      "dropped last paid rank",
+      "out-of-range native occurrence",
+      "physical occurrence merge",
+      "absent sorted-table state",
+      "unsorted table keys",
+      "duplicate table keys",
+      "uninitialized table count"
+    ],
+    "scope": "offline logical row indexing; no payload tape tariff or kappa",
+    "status": "PASS_CONTIGUOUS_SOURCE_INDEX",
+    "totals": {
+      "cases": 102,
+      "literal_classes": 555,
+      "native_units": 1005,
+      "sources": 1431,
+      "states": 362
+    }
+  },
+  "human_review": false,
+  "formal_kernel": false,
+  "complete_selected_emitter": false,
+  "physical_payload_execution": false,
+  "repair": "deterministic sorted state tables and separately charged metadata access",
+  "source_index_sha256": "e978025591b06770026b9879f1e5b10827424f410794fb2b1e1f10a720f49176",
+  "proof_sha256": "1631e28072e1ad39c3833ec83ff7d59e35c4d8fd1ad45ebce6b777aed4125bdb",
+  "verify_sha256": "fb89cad83c3ed69bffaf2a95347b21d26dde4da1dc9c52b4304e7d94d836f623"
+}
diff --git a/research/lockstep-source-row-index/independent_check.py b/research/lockstep-source-row-index/independent_check.py
new file mode 100644
index 0000000000..357c8cb104
--- /dev/null
+++ b/research/lockstep-source-row-index/independent_check.py
@@ -0,0 +1,129 @@
+"""Independent finite word enumeration and adversarial state-hash witness.
+
+Author code is never edited. The expected source list does not use its
+multiplicity, parent, local-count or block implementation.
+"""
+from collections import Counter
+from hashlib import sha256
+from itertools import product
+from math import comb, prod
+from pathlib import Path
+from types import ModuleType
+import json
+import sys
+
+HERE = Path(__file__).resolve().parent
+PACKAGE = Path(sys.argv[1]).resolve() if len(sys.argv)>1 else HERE
+
+
+def need(ok, message):
+    if not ok:
+        raise ValueError(message)
+
+
+def load_source():
+    path = PACKAGE/'source_index.py'
+    module = ModuleType('peer_source_index')
+    module.__file__ = str(path)
+    sys.modules[module.__name__] = module
+    exec(compile(path.read_bytes(), str(path), 'exec'), module.__dict__)
+    return module
+
+
+def word_sources(index):
+    rule, height = index.rule, index.height
+    types = tuple(sorted(set(k for _, k in rule.roles)))
+    expected = []
+    for depth in range(height+1):
+        for path in product(range(len(rule.rounds)), repeat=depth):
+            dilation = prod(rule.rounds[j][0] for j in path)
+            groups = Counter()
+            for word in product(range(len(rule.roles)), repeat=height-depth):
+                ranks = tuple(rule.roles[j][1] for j in word)
+                if rule.ambient*dilation*prod(ranks) <= index.rank:
+                    groups[tuple(ranks.count(k) for k in types)] += 1
+            for point, count in groups.items():
+                column = prod(k**a for k, a in zip(types, point))
+                parent_dilation = prod(rule.rounds[j][0] for j in path[:-1])
+                for ordinal in range(count):
+                    for role_index, (role, target) in enumerate(rule.roles):
+                        if not path or rule.ambient*parent_dilation*column*target > index.rank:
+                            expected.append((path, point, ordinal, role_index, role))
+    expected.sort()
+    return expected
+
+
+def check_case(module, rule, rank):
+    index = module.SourceIndex(rule, rank, replicas=5, namespace='peer')
+    expected = word_sources(index)
+    need(index.size == len(expected), 'ordered-word source total')
+    for row, (path, point, ordinal, _, role) in enumerate(expected):
+        unit = module.C.Unit(path, point, ordinal)
+        need(index.rank_source(unit, role) == row, 'declared source order')
+        need(index.unrank_source(row) == (unit, role), 'source inverse')
+        for replica in range(5):
+            owner = ('peer', replica, 'source', path, point, ordinal, role)
+            physical = replica*index.size+row
+            need(index.row(owner) == physical and index.owner(physical) == owner,
+                 'replicated source interval')
+    for illegal in (-1, 5*index.size):
+        try:
+            index.owner(illegal)
+        except ValueError:
+            pass
+        else:
+            raise ValueError('row boundary accepted')
+    sample = index.owner(0)
+    try:
+        index.row(sample[:2]+('owned',)+sample[3:])
+    except ValueError:
+        pass
+    else:
+        raise ValueError('owned role received source credit')
+    q, d, height = len(index.paid), len(rule.types), index.height
+    need(len(index.total) <= 1+q*comb(height+q-1, q), 'state-count envelope')
+    profiles = index.point_data.values() if isinstance(index.point_data, dict) else index.point_data
+    need(sum(map(len, profiles)) == comb(height+d, d), 'target-profile count')
+    return {'height':height, 'paid_alphabet':q, 'target_alphabet':d,
+            'sources':len(expected), 'replicas':5, 'states':len(index.total)}
+
+
+def collision_family(module):
+    hmod = sys.hash_info.modulus
+    rule = module.C.Rule((('single',8*hmod),),
+                        tuple((hmod*p,'single') for p in (1,2,3,5,7)))
+    result = []
+    for height in (1,2,3,4):
+        index = module.SourceIndex(rule, rule.ambient*(8*hmod)**height)
+        states = [(rho,last) for h,rho,last in index.total if h == height]
+        count = 5*comb(height+3,4)
+        need(len(states) == count, 'collision family exact cardinality')
+        need(len(set(map(hash,states))) == 1, 'all states share hash')
+        need(index.size == 1, 'collision-family source total')
+        result.append({'height':height, 'layer_states':count,
+                       'distinct_hashes':1, 'sources':index.size})
+    return {'integer_hash_modulus':hmod, 'cases':result}
+
+
+def main():
+    module = load_source()
+    rule1 = module.C.Rule((('seven_a',7),('eleven',11),('seven_b',7)),
+                         ((1,'seven_a'),(2,'seven_b'),(3,'bank'),(6,'eleven')),
+                         ambient=13)
+    rule2 = module.C.Rule((('one',5),),
+                         ((1,'one'),(2,'bank'),(2,'one'),(4,'one')),ambient=8)
+    cases = [check_case(module,rule,rule.ambient*min(rule.types)**height+delta)
+             for rule in (rule1,rule2) for height in (0,1,2,3)
+             for delta in (0,min(rule.types)-1)]
+    result = {'status':'PASS_SOURCE_INDEX_PEER_FUNCTIONAL_CHECKS',
+              'package_hashes':{name:sha256((PACKAGE/name).read_bytes()).hexdigest()
+                                for name in ('source_index.py','PROOF.md','verify.py')},
+              'bounded_cases':cases, 'sources_checked':sum(x['sources'] for x in cases),
+              'collision_witness':collision_family(module)}
+    (HERE/'INDEPENDENT-RESULT.json').write_text(json.dumps(result,indent=2,sort_keys=True)+'\n')
+    print(result['status'], 'cases='+str(len(cases)),
+          'sources='+str(result['sources_checked']), 'hash_collision_cases=4')
+
+
+if __name__ == '__main__':
+    main()
diff --git a/research/lockstep-source-row-index/inputs/finite_dag_audit.py b/research/lockstep-source-row-index/inputs/finite_dag_audit.py
new file mode 100644
index 0000000000..c1798bfa9c
--- /dev/null
+++ b/research/lockstep-source-row-index/inputs/finite_dag_audit.py
@@ -0,0 +1,379 @@
+#!/usr/bin/env python3
+"""Independent integer and field-identity audit of finite mixed-job compilation.
+
+Apache-2.0. Substantial OpenAI assistance. The mathematical lockstep flow is
+Jacob Alan Sussman's Theorem 1G; attribution and limits are in AUDIT.md.
+No implementation from its tree_flow.py or explicit_sim.py is imported.
+This checks scheduling and exact finite batching under a mixed-unit contract;
+it does not manufacture that operator contract from a rank histogram.
+"""
+from collections import Counter, defaultdict, deque
+from dataclasses import dataclass
+from fractions import Fraction
+from functools import lru_cache
+from hashlib import sha256
+from math import factorial, gcd, lcm, prod
+from pathlib import Path
+import argparse
+import gzip
+import json
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parents[2]
+
+
+def need(test, message):
+    if not test:
+        raise AssertionError(message)
+
+
+def read(path):
+    raw = Path(path).read_bytes()
+    return json.loads(gzip.decompress(raw) if str(path).endswith('.gz') else raw)
+
+
+def digest(path):
+    return sha256(Path(path).read_bytes()).hexdigest()
+
+
+def rational(value):
+    value = Fraction(value)
+    return f'{value.numerator}/{value.denominator}'
+
+
+@dataclass(frozen=True)
+class Rule:
+    # Productive target roles have fixed names and positive ranks.
+    roles: tuple
+    # A paid round is (rank, exact productive or owned role name).
+    rounds: tuple
+    owned: tuple = ('owned-C0',)
+
+    def __post_init__(self):
+        names = [name for name, rank in self.roles]
+        need(len(set(names)) == len(names), 'Distinct productive roles')
+        need(set(names).isdisjoint(self.owned), 'Owned roles uncredited')
+        need(all(rank > 0 for name, rank in self.roles), 'Positive target ranks')
+        need(all(rank > 0 and name in set(names) | set(self.owned)
+                 for rank, name in self.rounds), 'Every paid call has a real role')
+        need(max(rank for rank, name in self.rounds) < min(rank for name, rank in self.roles),
+             'Strict mixed hierarchy')
+
+    @property
+    def targets(self):
+        return Counter(rank for name, rank in self.roles)
+
+    @property
+    def dimension(self):
+        return max(self.targets)
+
+
+class IntegerTree:
+    """Literal classes, units, field names, and dependency edges at one rank."""
+
+    def __init__(self, rule, rank):
+        self.rule, self.rank = rule, rank
+        self.types = tuple(sorted(rule.targets))
+        self.weights = tuple(rule.targets[k] for k in self.types)
+        self.points = self.lattice(1)
+        need(bool(self.points), 'At least one mixed unit fits')
+        self.depth = max(map(sum, self.points))
+        self.units = []
+        self.classes = []
+        self.sources = []
+        self.exits = []
+        self.edges = set()
+        self.nodes = set()
+        self.source_counter = Counter()
+        self._class((), 1, [])
+        self.validate_fields()
+        need(self.topological_size() == len(self.nodes), 'Native-order dependency DAG')
+
+    def lattice(self, dilation):
+        bound = self.rank // (self.rule.dimension * dilation)
+        out = []
+
+        def visit(index, powers, value):
+            if index == len(self.types):
+                out.append(tuple(powers))
+                return
+            exponent = 0
+            while value <= bound:
+                visit(index+1, powers+[exponent], value)
+                exponent += 1
+                value *= self.types[index]
+
+        if bound:
+            visit(0, [], 1)
+        return out
+
+    def column(self, point):
+        return prod(k**a for k, a in zip(self.types, point))
+
+    def multiplicity(self, point):
+        return factorial(sum(point)) // prod(factorial(a) for a in point) * prod(
+            w**a for w, a in zip(self.weights, point))
+
+    def edge(self, before, after):
+        self.nodes.update((before, after))
+        self.edges.add((before, after))
+
+    def after(self, uid, round_index):
+        return ('issue', uid, round_index+1) if round_index+1 < len(self.rule.rounds) else ('finish', uid)
+
+    def _class(self, path, dilation, incoming):
+        depth = len(path)
+        class_units = []
+        demands = defaultdict(list)
+        for point in self.lattice(dilation):
+            if sum(point) != self.depth-depth:
+                continue
+            column = dilation*self.column(point)
+            need(self.rule.dimension*column <= self.rank, 'All ambient axes fit')
+            for repetition in range(self.multiplicity(point)):
+                uid = len(self.units)
+                unit = {'uid': uid, 'path': path, 'point': point, 'column': column,
+                        'fields': {}, 'owned': {name: ('owned', uid, name) for name in self.rule.owned}}
+                self.units.append(unit)
+                class_units.append(unit)
+                for name, target in self.rule.roles:
+                    index = self.types.index(target)
+                    point_next = tuple(a+int(i == index) for i, a in enumerate(point))
+                    demands[point_next].append((unit, name, target*column))
+                self.edge(('start', uid), ('issue', uid, 0))
+                for j in range(len(self.rule.rounds)):
+                    self.edge(('issue', uid, j), self.after(uid, j))
+        self.classes.append((path, tuple(u['uid'] for u in class_units)))
+        supply = defaultdict(list)
+        for job in incoming:
+            supply[job['point']].append(job)
+        need(set(supply) <= set(demands), 'No paid output is abandoned')
+        for point, slots in demands.items():
+            jobs = supply.get(point, [])
+            need(len(jobs) <= len(slots), 'No target is double funded')
+            for index, (unit, name, target) in enumerate(slots):
+                if index < len(jobs):
+                    job = jobs[index]
+                    need(job['rank'] == target, 'Exact target rank equality')
+                    unit['fields'][name] = job['field']
+                    self.edge(('issue', job['uid'], job['round']), ('start', unit['uid']))
+                    self.edge(('finish', unit['uid']), self.after(job['uid'], job['round']))
+                else:
+                    field = ('source', len(self.sources))
+                    unit['fields'][name] = field
+                    self.sources.append({'field': field, 'rank': target, 'unit': unit['uid'], 'role': name})
+                    self.source_counter[target] += 1
+                    need(self.rank < self.rule.dimension*target <= self.rule.dimension*self.rank,
+                         'Whole source lies in the proved source band')
+        all_fields = [field for unit in class_units for field in unit['fields'].values()]
+        need(len(all_fields) == len(set(all_fields)), 'Simultaneous units have disjoint arbitrary inputs')
+        need(all(len(unit['fields']) == len(self.rule.roles) for unit in class_units), 'Every input slot filled')
+        for j, (paid_rank, paid_role) in enumerate(self.rule.rounds):
+            outgoing = []
+            for unit in class_units:
+                field = unit['fields'].get(paid_role, unit['owned'].get(paid_role))
+                need(field is not None, 'Paid call remains on its physical owner')
+                outgoing.append({'field': field, 'rank': paid_rank*unit['column'],
+                                 'point': unit['point'], 'uid': unit['uid'], 'round': j})
+            need(len({job['field'] for job in outgoing}) == len(outgoing), 'Ordered round has no field alias')
+            if depth < self.depth:
+                self._class(path+(j,), dilation*paid_rank, outgoing)
+            else:
+                need(all(sum(job['point']) == 0 for job in outgoing), 'Only zero-generation exits')
+                need(len({job['rank'] for job in outgoing}) == 1, 'One rank per ordered exit batch')
+                for job in outgoing:
+                    need(job['rank'] < self.rank, 'Every recursive exit strictly smaller')
+                    complete = ('exit', len(self.exits), job['uid'])
+                    self.edge(('issue', job['uid'], j), complete)
+                    self.edge(complete, self.after(job['uid'], j))
+                self.exits.append(outgoing)
+
+    def topological_size(self, extra_edges=()):
+        successors = defaultdict(list)
+        indegrees = {node: 0 for node in self.nodes}
+        for before, after in self.edges | set(extra_edges):
+            successors[before].append(after)
+            indegrees[after] += 1
+        ready = deque(node for node in self.nodes if not indegrees[node])
+        count = 0
+        while ready:
+            before = ready.popleft()
+            count += 1
+            for after in successors[before]:
+                indegrees[after] -= 1
+                if not indegrees[after]:
+                    ready.append(after)
+        return count
+
+    def validate_fields(self):
+        need(len({row['field'] for row in self.sources}) == len(self.sources),
+             'Every source is a distinct arbitrary field')
+        for path, unit_ids in self.classes:
+            fields = [field for uid in unit_ids for field in self.units[uid]['fields'].values()]
+            need(len(fields) == len(set(fields)), 'No duplicated independent input in a class')
+
+    def summary(self):
+        return {'rank': self.rank, 'generations': self.depth, 'classes': len(self.classes),
+                'units': len(self.units), 'source_fields': len(self.sources),
+                'source_ranks': dict(sorted(self.source_counter.items())),
+                'exit_ranks': dict(sorted(Counter(job['rank'] for group in self.exits for job in group).items())),
+                'ordered_exit_batches': len(self.exits), 'event_nodes': len(self.nodes),
+                'dependency_edges': len(self.edges), 'acyclic': True,
+                'every_paid_call_real_owner': True, 'class_input_disjointness': True,
+                'owned_fields_uncredited_conservative_allocation': len(self.units)*len(self.rule.owned)}
+
+
+class Compiler:
+    def __init__(self, rule):
+        self.rule = rule
+        self.trees = {}
+
+    @lru_cache(None)
+    def compile(self, rank):
+        if rank < self.rule.dimension:
+            return {'rank': rank, 'width': 1, 'leaves': rank, 'units': 0, 'per_array': Fraction(rank),
+                    'all_productive_fields_full_rank': True}
+        tree = IntegerTree(self.rule, rank)
+        self.trees[rank] = tree
+        multiplier = 1
+        requirements = []
+        for jobs in tree.exits:
+            smaller = self.compile(jobs[0]['rank'])
+            required = smaller['width']//gcd(smaller['width'], len(jobs))
+            multiplier = lcm(multiplier, required)
+            requirements.append(('ordered_exit', jobs[0]['rank'], len(jobs), smaller['width']))
+        for source_rank, count in tree.source_counter.items():
+            smaller = self.compile(rank-source_rank)
+            required = smaller['width']//gcd(smaller['width'], count)
+            multiplier = lcm(multiplier, required)
+            requirements.append(('source_complement', rank-source_rank, count, smaller['width']))
+        need(all(multiplier*count % width == 0 for kind, size, count, width in requirements),
+             'Each ordered batch is independently integral')
+        width = multiplier*len(tree.sources)
+        normalized_leaves = sum((Fraction(len(jobs))*self.compile(jobs[0]['rank'])['per_array']
+                                for jobs in tree.exits), Fraction(0))
+        normalized_leaves += sum((count*self.compile(rank-source_rank)['per_array']
+                                 for source_rank, count in tree.source_counter.items()), Fraction(0))
+        leaves = multiplier*normalized_leaves
+        need(leaves.denominator == 1, 'Integral actual leaf count')
+        unit_count = Fraction(len(tree.units))
+        for kind, size, count, child_width in requirements:
+            child = self.compile(size)
+            unit_count += Fraction(count*child['units'], child_width)
+        unit_count *= multiplier
+        need(unit_count.denominator == 1, 'Integral conservative owned allocation')
+        for source in tree.sources:
+            source_axes = set(range(source['rank']))
+            complement = set(range(source['rank'], rank))
+            need(source_axes.isdisjoint(complement) and source_axes | complement == set(range(rank)),
+                 'Each independent source receives the full rank-N job exactly once')
+        return {'rank': rank, 'width': width, 'leaves': leaves.numerator, 'units': unit_count.numerator,
+                'per_array': leaves/width, 'replication': multiplier, 'ordered_requirements': requirements,
+                'all_productive_fields_full_rank': True,
+                'owned_fields_uncredited': unit_count.numerator*len(self.rule.owned),
+                'strict_uniform_child_rank': 1, 'native_halving_guard': rank*rank > 2}
+
+
+def actual_rule():
+    """Extract every paid owner in chronology from the source-bound p2 word."""
+    controller_path = ROOT/'research/kappa-rebuild/controller/GLOBAL-IDENTITY-COVER.json.gz'
+    controller = read(controller_path)
+    case = controller['all_three']
+    roles = [(f'{side}{pair}:{port}', 41) for pair in range(2) for side in ('X', 'Y') for port in range(112)]
+    roles += [(row['owner'], row['target_rank']) for row in case['fresh_outputs']]
+    native_path = ROOT/'research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz'
+    native = read(native_path)
+    rounds = []
+    stages = ((0, 'forward'), (0, 'backward'), (0, 'forward'), (1, 'backward'), (1, 'forward'))
+    for stage, (pair, direction) in enumerate(stages):
+        helper = {row['role']: row['owner'] for row in case['helper_bindings'] if row['stage'] == stage}
+        for event in native[direction]:
+            if event[0] == 'climb':
+                _, part, role, old, new, rank = event
+                owner = f'X{pair}:{role}' if role < 112 else f'Y{pair}:{role-112}' if role < 224 else helper[role]
+                rounds.append((rank, owner))
+            elif event[0] == 'center':
+                rounds.append((event[-1], 'owned-C0'))
+        for residual in case['paid_residuals']:
+            if residual['after_stage'] == stage:
+                rounds.append((residual['rank'], residual['owner']))
+    need(Counter(rank for rank, name in rounds) == Counter({int(k): v for k, v in case['paid'].items()}),
+         'Literal native paid-call extraction agrees with complete bill')
+    rule = Rule(tuple(roles), tuple(rounds))
+    need(rule.targets == Counter({6:146, 9:803, 41:448}), 'Actual independent output jobs')
+    return rule, {str(path.relative_to(ROOT)): digest(path) for path in (controller_path, native_path)}
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument('--output', type=Path, default=HERE/'FINITE-DAG-AUDIT.json')
+    args = parser.parse_args()
+    # This synthetic contract tests only the generic compiler; no native circuit
+    # is claimed for its deliberately repeated/owned paid-role sequence.
+    toy = Rule((('a', 3), ('b', 3), ('c', 4)),
+               ((1, 'a'), (1, 'owned-C0'), (1, 'b'), (1, 'a'), (2, 'c'), (2, 'owned-C0')))
+    compiler = Compiler(toy)
+    toy_results = []
+    for rank in (4, 7, 12, 16, 28, 40):
+        compiled = compiler.compile(rank)
+        row = {k: rational(v) if isinstance(v, Fraction) else v for k, v in compiled.items()
+               if k != 'ordered_requirements'}
+        row['tree'] = compiler.trees[rank].summary()
+        toy_results.append(row)
+    tree = compiler.trees[16]
+    child = next(unit for unit in tree.units if unit['path'] == (0,))
+    parent = next(unit for unit in tree.units if unit['path'] == ())
+    cyclic = tree.topological_size([(('issue', parent['uid'], 1), ('start', child['uid']))]) < len(tree.nodes)
+    need(cyclic, 'Later-round dependency negative control creates a cycle')
+    fields = tree.units[0]['fields']
+    first, second = tuple(fields)[:2]
+    old = fields[second]
+    fields[second] = fields[first]
+    illegal_alias = False
+    try:
+        tree.validate_fields()
+    except AssertionError:
+        illegal_alias = True
+    finally:
+        fields[second] = old
+    need(illegal_alias, 'Independent fields cannot share a source token')
+    cleared = compiler.compile(16)
+    bad_multiplier = cleared['replication']-1
+    uncleared_rejected = any(bad_multiplier*count % width
+                            for kind, size, count, width in cleared['ordered_requirements'])
+    need(uncleared_rejected, 'One fewer replica fails a real ordered batch divisibility requirement')
+    uniform = compiler.compile(40)
+    need(uniform['leaves']**10 < uniform['width']**10 * 40**9,
+         'Exact finite toy supplier beats exponent 9/10, including all complements')
+    actual, pins = actual_rule()
+    actual_compiler = Compiler(actual)
+    finite = actual_compiler.compile(41)
+    actual_row = {k: rational(v) if isinstance(v, Fraction) else v for k, v in finite.items()
+                  if k != 'ordered_requirements'}
+    actual_row['tree'] = actual_compiler.trees[41].summary()
+    need(finite['width'] == 1397 and finite['leaves'] == 57149,
+         'Independent full-rank completion bill including every complementary axis')
+    need(41*1397-finite['leaves'] == 128, 'No credit from partial fields or owned center')
+    output = {'schema':'independent-finite-mixed-job-compilation-audit/1',
+              'status':'PASS_FINITE_DAG_FIELD_OWNERS_BATCH_CLEARING_AND_FULL_RANK_COMPLETION',
+              'source_sha256':digest(__file__), 'pinned_native_inputs':pins,
+              'synthetic_rule_tests':toy_results, 'actual_p2_rank41':actual_row,
+              'negative_controls':{'future_round_deadlock_rejected':cyclic,
+                                   'aliased_independent_source_rejected':illegal_alias,
+                                   'uncleared_ordered_batch_rejected':uncleared_rejected,
+                                   'partial_source_not_full': set(range(6)) != set(range(41)),
+                                   'owned_center_not_counted': len(actual.roles) == 1397},
+              'toy_strict_uniform_moment':{'rank':40,'exponent':'9/10',
+                                           'integer_power_comparison':True},
+              'scope':['Independent finite flow and owner identities, not a proof of an abstract unit from its histogram.',
+                       'Actual p2 paid calls extracted in native order with original owners.',
+                       'Full F_N completion is a compositional proof under the pinned native endpoint contract.',
+                       'No winning near-threshold large-N supplier was materialized; the existence theorem is separate.',
+                       'No dynamic RAM transfer or new kappa is claimed.']}
+    args.output.write_text(json.dumps(output, indent=2, sort_keys=True)+'\n')
+    print(json.dumps({'status':output['status'], 'toy_ranks':[row['rank'] for row in toy_results],
+                      'actual_full_rank':41, 'actual_width':finite['width'], 'actual_paid_rank1':finite['leaves']}))
+
+
+if __name__ == '__main__':
+    main()
diff --git a/research/lockstep-source-row-index/inputs/pascal_codec.py b/research/lockstep-source-row-index/inputs/pascal_codec.py
new file mode 100644
index 0000000000..2fb4426cc8
--- /dev/null
+++ b/research/lockstep-source-row-index/inputs/pascal_codec.py
@@ -0,0 +1,222 @@
+"""Exact Pascal interval codec for a separated lockstep flow.
+
+Apache-2.0. Prepared for CubeJerry with substantial OpenAI assistance.
+This is an offline logical occurrence codec, not a fixed-tape dispatcher.
+"""
+from dataclasses import dataclass
+
+
+def require(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def natural(value, message):
+    require(type(value) is int and value >= 0, message)
+
+
+@dataclass(frozen=True)
+class Rule:
+    roles: tuple
+    rounds: tuple
+    owned: tuple = ("bank",)
+    ambient: int | None = None
+
+    def __post_init__(self):
+        require(bool(self.roles) and bool(self.rounds), "nonempty rule")
+        names = tuple(name for name, _ in self.roles)
+        require(len(set(names)) == len(names), "duplicate productive role")
+        require(len(set(self.owned)) == len(self.owned), "duplicate owned role")
+        require(not set(names) & set(self.owned), "owned/productive alias")
+        require(all(type(k) is int and k >= 2 for _, k in self.roles),
+                "target ranks are integers at least two")
+        require(all(type(r) is int and 1 <= r < min(k for _, k in self.roles)
+                    and owner in names + self.owned for r, owner in self.rounds),
+                "positive separated paid rank and real owner")
+        if self.ambient is None:
+            object.__setattr__(self, "ambient", max(k for _, k in self.roles))
+        require(type(self.ambient) is int and
+                self.ambient >= max(k for _, k in self.roles), "ambient cap")
+
+    @property
+    def types(self):
+        return tuple(sorted(set(k for _, k in self.roles)))
+
+    @property
+    def weights(self):
+        return tuple(sum(k == rank for _, k in self.roles) for rank in self.types)
+
+    def type_of(self, role):
+        names = tuple(name for name, _ in self.roles)
+        require(role in names, "unknown productive role")
+        rank = self.roles[names.index(role)][1]
+        return self.types.index(rank)
+
+    def same_type_roles(self, i):
+        return tuple(name for name, k in self.roles if k == self.types[i])
+
+
+@dataclass(frozen=True)
+class Unit:
+    path: tuple
+    point: tuple
+    ordinal: int
+
+
+def validate_point(rule, point):
+    require(len(point) == len(rule.types), "point dimension")
+    for a in point:
+        natural(a, "nonnegative integer point")
+
+
+def column(rule, point):
+    validate_point(rule, point)
+    out = 1
+    for k, a in zip(rule.types, point):
+        for _ in range(a):
+            out *= k
+    return out
+
+
+def multiplicity(rule, point):
+    """Multinomial times weights, using exact small-factor arithmetic."""
+    validate_point(rule, point)
+    remaining, out = sum(point), 1
+    for a, weight in zip(point, rule.weights):
+        choose = 1
+        for j in range(1, a + 1):
+            choose = choose * (remaining - j + 1) // j
+        out *= choose
+        for _ in range(a):
+            out *= weight
+        remaining -= a
+    return out
+
+
+def remove_letter(point, i):
+    require(0 <= i < len(point) and point[i] > 0, "missing target letter")
+    return tuple(a - int(j == i) for j, a in enumerate(point))
+
+
+def encode(rule, parent_point, child_ordinal, role):
+    """Exact ordinal in the parent's Pascal bucket."""
+    validate_point(rule, parent_point)
+    i = rule.type_of(role)
+    child_point = remove_letter(parent_point, i)
+    natural(child_ordinal, "child ordinal")
+    require(child_ordinal < multiplicity(rule, child_point), "child ordinal range")
+    offset = 0
+    for j in range(i):
+        if parent_point[j]:
+            offset += rule.weights[j] * multiplicity(rule, remove_letter(parent_point, j))
+    same = rule.same_type_roles(i)
+    return offset + len(same) * child_ordinal + same.index(role)
+
+
+def decode(rule, parent_point, parent_ordinal):
+    """Inverse: (child point, child ordinal, productive role)."""
+    validate_point(rule, parent_point)
+    require(sum(parent_point) > 0, "no Pascal split of an empty word")
+    natural(parent_ordinal, "parent ordinal")
+    require(parent_ordinal < multiplicity(rule, parent_point), "parent ordinal range")
+    residual = parent_ordinal
+    for i, a in enumerate(parent_point):
+        if not a:
+            continue
+        child = remove_letter(parent_point, i)
+        names = rule.same_type_roles(i)
+        size = len(names) * multiplicity(rule, child)
+        if residual < size:
+            ordinal, role_index = divmod(residual, len(names))
+            return child, ordinal, names[role_index]
+        residual -= size
+    raise ValueError("Pascal identity failed")
+
+
+class FlowCodec:
+    def __init__(self, rule, rank):
+        natural(rank, "ambient rank")
+        require(rank >= rule.ambient, "at least one unit fits")
+        self.rule, self.rank = rule, rank
+        capacity, self.height = rank // rule.ambient, 0
+        power, smallest = 1, min(rule.types)
+        while power <= capacity // smallest:
+            power *= smallest
+            self.height += 1
+
+    def dilation(self, path):
+        value = 1
+        for j in path:
+            natural(j, "paid occurrence")
+            require(j < len(self.rule.rounds), "paid occurrence range")
+            value *= self.rule.rounds[j][0]
+        return value
+
+    def validate_unit(self, unit):
+        validate_point(self.rule, unit.point)
+        require(len(unit.path) + sum(unit.point) == self.height, "class degree")
+        natural(unit.ordinal, "unit ordinal")
+        require(unit.ordinal < multiplicity(self.rule, unit.point), "unit ordinal range")
+        require(self.rule.ambient * self.dilation(unit.path) *
+                column(self.rule, unit.point) <= self.rank, "absent unit")
+
+    def parent(self, unit, role):
+        """None means a fresh source, otherwise the exact issuing parent."""
+        self.validate_unit(unit)
+        i = self.rule.type_of(role)
+        if not unit.path:
+            return None
+        point = tuple(a + int(j == i) for j, a in enumerate(unit.point))
+        path = unit.path[:-1]
+        if self.rule.ambient * self.dilation(path) * column(self.rule, point) > self.rank:
+            return None
+        return Unit(path, point, encode(self.rule, point, unit.ordinal, role))
+
+    def owner(self, unit, role, namespace="flow", replica=0):
+        """Resolve a canonical field identity without any occurrence table."""
+        natural(replica, "replica")
+        self.validate_unit(unit)
+        self.rule.type_of(role)
+        while True:
+            parent = self.parent(unit, role)
+            if parent is None:
+                return (namespace, replica, "source", unit.path, unit.point, unit.ordinal, role)
+            parent_owner = self.rule.rounds[unit.path[-1]][1]
+            if parent_owner in self.rule.owned:
+                return (namespace, replica, "owned", parent.path, parent.point,
+                        parent.ordinal, parent_owner)
+            unit, role = parent, parent_owner
+
+    def paid_owner(self, unit, j, namespace="flow", replica=0):
+        self.validate_unit(unit)
+        natural(j, "paid occurrence")
+        require(j < len(self.rule.rounds), "paid occurrence range")
+        owner = self.rule.rounds[j][1]
+        if owner in self.rule.owned:
+            return (namespace, replica, "owned", unit.path, unit.point, unit.ordinal, owner)
+        return self.owner(unit, owner, namespace, replica)
+
+    def iter_points(self, path):
+        """Stream the predecessor's lexicographic lattice order."""
+        degree = self.height - len(path)
+        require(degree >= 0, "path too deep")
+        limit = self.rank // (self.rule.ambient * self.dilation(path))
+        types = self.rule.types
+
+        def visit(i, left, value, prefix):
+            if i == len(types):
+                if left == 0:
+                    yield tuple(prefix)
+                return
+            for a in range(left + 1):
+                if value > limit:
+                    break
+                yield from visit(i + 1, left - a, value, prefix + [a])
+                value *= types[i]
+
+        yield from visit(0, degree, 1, [])
+
+    def iter_units(self, path):
+        for point in self.iter_points(path):
+            for ordinal in range(multiplicity(self.rule, point)):
+                yield Unit(path, point, ordinal)
diff --git a/research/lockstep-source-row-index/source_index.py b/research/lockstep-source-row-index/source_index.py
new file mode 100644
index 0000000000..4e3cb2a53f
--- /dev/null
+++ b/research/lockstep-source-row-index/source_index.py
@@ -0,0 +1,205 @@
+"""Contiguous source rows by aggregated lockstep-subtree counting.
+
+Apache-2.0. Prepared for CubeJerry with substantial OpenAI assistance.
+This is offline indexing, not a fixed-tape payload implementation.
+"""
+from collections import Counter
+from bisect import bisect_left
+import hashlib
+import importlib.util
+from pathlib import Path
+import sys
+
+HERE = Path(__file__).resolve().parent
+CODEC_HASH = "cec2c8b5e153a264127e8301ed59591fe97c9a46078ff2343b3784d177c6984d"
+CODEC_PATH = HERE / "inputs/pascal_codec.py"
+if hashlib.sha256(CODEC_PATH.read_bytes()).hexdigest() != CODEC_HASH:
+    raise ValueError("frozen occurrence codec hash")
+spec = importlib.util.spec_from_file_location("source_index_codec", CODEC_PATH)
+C = importlib.util.module_from_spec(spec)
+sys.modules[spec.name] = C
+spec.loader.exec_module(C)
+
+
+def points(degree, dimensions):
+    """Lexicographic nonnegative multiindices of one exact degree."""
+    if dimensions == 1:
+        yield (degree,)
+        return
+    for first in range(degree + 1):
+        for rest in points(degree - first, dimensions - 1):
+            yield (first,) + rest
+
+
+def sorted_unique(items):
+    """Deterministic comparison sort and adjacent deduplication; no hashing."""
+    ordered = sorted(items)
+    unique = []
+    for item in ordered:
+        if not unique or item != unique[-1]:
+            unique.append(item)
+    return unique
+
+
+class SortedStateTable:
+    """Fixed sorted integer keys, binary-search lookup and indexed values.
+
+    The two count tables share one immutable key tuple. No growing state
+    set/dictionary and no expected hash-table time enters the theorem.
+    """
+    def __init__(self, keys):
+        C.require(all(a < b for a, b in zip(keys, keys[1:])),
+                  "strictly sorted distinct state keys")
+        self._keys = keys
+        self._values = [None] * len(keys)
+
+    def position(self, key):
+        at = bisect_left(self._keys, key)
+        C.require(at < len(self._keys) and self._keys[at] == key,
+                  "state key absent from fixed table")
+        return at
+
+    def __getitem__(self, key):
+        value = self._values[self.position(key)]
+        C.require(value is not None, "state count not initialized")
+        return value
+
+    def __setitem__(self, key, value):
+        self._values[self.position(key)] = value
+
+    def __len__(self):
+        return len(self._keys)
+
+    def __iter__(self):
+        return iter(self._keys)
+
+    def keys(self):
+        return iter(self._keys)
+
+    def values(self):
+        return iter(self._values)
+
+    def items(self):
+        return zip(self._keys, self._values)
+
+
+class SourceIndex:
+    def __init__(self, rule, rank, replicas=1, namespace="flow"):
+        C.natural(replicas, "replica count")
+        C.require(replicas > 0, "positive replica count")
+        self.flow = C.FlowCodec(rule, rank)
+        self.rule, self.rank = rule, rank
+        self.replicas, self.namespace = replicas, namespace
+        self.height = self.flow.height
+        self.types, self.weights = rule.types, rule.weights
+        self.paid = Counter(r for r, _ in rule.rounds)
+        # Counter is confined to the fixed input list; its worst-case
+        # collision cost is covered by the specification-size factor.
+        self.point_data = []
+        for g in range(self.height + 1):
+            self.point_data.append(tuple((a, C.column(rule, a), C.multiplicity(rule, a))
+                                         for a in points(g, len(self.types))))
+        levels = [[(1, 0)]]
+        for _ in range(self.height):
+            # Adjacent equal dilations differ only in their last rank.
+            # Deduplicate them before generating children: (rho*r,r) is
+            # injective in rho at fixed r, and distinct r give distinct keys.
+            dilations = []
+            for rho, _ in levels[-1]:
+                if not dilations or rho != dilations[-1]:
+                    dilations.append(rho)
+            levels.append(sorted_unique((rho*r, r) for rho in dilations
+                                        for r in self.paid))
+        keys = tuple((h, rho, previous) for h, level in enumerate(levels)
+                     for rho, previous in level)
+        self.local, self.total = SortedStateTable(keys), SortedStateTable(keys)
+        for h in range(self.height, -1, -1):
+            for rho, previous in levels[h]:
+                state = (h, rho, previous)
+                local = sum(u*count for _, _, u, count in self.blocks(state))
+                total = local
+                if h < self.height:
+                    total += sum(mult*self.total[h+1, rho*r, r]
+                                 for r, mult in self.paid.items())
+                self.local[state], self.total[state] = local, total
+        self.size = self.total[0, 1, 0]
+        C.require(self.size > 0, "nonempty source interval")
+
+    def fresh_type(self, state, column, i):
+        h, rho, previous = state
+        return h == 0 or self.rule.ambient * (rho // previous) * column * self.types[i] > self.rank
+
+    def blocks(self, state):
+        h, rho, _ = state
+        for point, column, units in self.point_data[self.height-h]:
+            if self.rule.ambient * rho * column <= self.rank:
+                count = sum(w for i, w in enumerate(self.weights)
+                            if self.fresh_type(state, column, i))
+                if count:
+                    yield point, column, units, count
+
+    def fresh_roles(self, state, column):
+        return tuple(name for name, k in self.rule.roles
+                     if self.fresh_type(state, column, self.types.index(k)))
+
+    def rank_source(self, unit, role):
+        self.flow.validate_unit(unit)
+        self.rule.type_of(role)
+        state, offset = (0, 1, 0), 0
+        for chosen in unit.path:
+            h, rho, _ = state
+            offset += self.local[state]
+            for r, _ in self.rule.rounds[:chosen]:
+                offset += self.total[h+1, rho*r, r]
+            r = self.rule.rounds[chosen][0]
+            state = (h+1, rho*r, r)
+        for point, column, units, count in self.blocks(state):
+            if point < unit.point:
+                offset += units*count
+                continue
+            if point == unit.point:
+                roles = self.fresh_roles(state, column)
+                C.require(role in roles, "slot is matched, not a fresh source")
+                return offset + unit.ordinal*count + roles.index(role)
+            break
+        raise ValueError("slot is matched, not a fresh source")
+
+    def unrank_source(self, index):
+        C.natural(index, "source index")
+        C.require(index < self.size, "source index range")
+        state, path = (0, 1, 0), ()
+        while True:
+            if index < self.local[state]:
+                for point, column, units, count in self.blocks(state):
+                    if index < units*count:
+                        ordinal, role = divmod(index, count)
+                        return C.Unit(path, point, ordinal), self.fresh_roles(state, column)[role]
+                    index -= units*count
+                raise ValueError("local count/index disagreement")
+            index -= self.local[state]
+            h, rho, _ = state
+            C.require(h < self.height, "no child beyond the last class")
+            for j, (r, _) in enumerate(self.rule.rounds):
+                child = (h+1, rho*r, r)
+                if index < self.total[child]:
+                    state, path = child, path + (j,)
+                    break
+                index -= self.total[child]
+            else:
+                raise ValueError("subtree count/index disagreement")
+
+    def row(self, owner):
+        C.require(type(owner) is tuple and len(owner) == 7, "complete field identifier")
+        namespace, replica, kind, path, point, ordinal, role = owner
+        C.require(namespace == self.namespace, "invocation namespace")
+        C.natural(replica, "replica")
+        C.require(replica < self.replicas, "replica range")
+        C.require(kind == "source", "owned bank has no productive source row")
+        return replica*self.size + self.rank_source(C.Unit(path, point, ordinal), role)
+
+    def owner(self, row):
+        C.natural(row, "physical row index")
+        C.require(row < self.replicas*self.size, "physical row index range")
+        replica, index = divmod(row, self.size)
+        unit, role = self.unrank_source(index)
+        return (self.namespace, replica, "source", unit.path, unit.point, unit.ordinal, role)
diff --git a/research/lockstep-source-row-index/verify.py b/research/lockstep-source-row-index/verify.py
new file mode 100644
index 0000000000..ac9e1b57b3
--- /dev/null
+++ b/research/lockstep-source-row-index/verify.py
@@ -0,0 +1,234 @@
+#!/usr/bin/env python3
+"""Exact bounded literal-source comparisons for contiguous row indexing."""
+from collections import Counter
+import hashlib
+import importlib.util
+import json
+from math import comb
+from functools import lru_cache
+from pathlib import Path
+import sys
+
+HERE = Path(__file__).resolve().parent
+
+
+def need(ok, message):
+    if not ok:
+        raise ValueError(message)
+
+
+def load(name, path):
+    spec = importlib.util.spec_from_file_location(name, path)
+    obj = importlib.util.module_from_spec(spec)
+    sys.modules[name] = obj
+    spec.loader.exec_module(obj)
+    return obj
+
+
+I = load("source_index", HERE / "source_index.py")
+C = I.C
+oracle = HERE / "inputs/finite_dag_audit.py"
+need(hashlib.sha256(oracle.read_bytes()).hexdigest() ==
+     "f842f0e07ca40a181782a565a381b0ee20c6a4b08b8c2b8a4d5d630381bd1e8e",
+     "literal oracle hash")
+O = load("source_index_literal_oracle", oracle)
+
+
+class AmbientRule(O.Rule):
+    @property
+    def dimension(self):
+        return self._ambient
+
+
+def literal(rule, n):
+    old = AmbientRule(rule.roles, rule.rounds, rule.owned)
+    object.__setattr__(old, "_ambient", rule.ambient)
+    tree = O.IntegerTree(old, n)
+    occurrence, units = Counter(), {}
+    for unit in tree.units:
+        key = (unit["path"], unit["point"])
+        units[unit["uid"]] = C.Unit(*key, occurrence[key])
+        occurrence[key] += 1
+    order = {role: j for j, (role, _) in enumerate(rule.roles)}
+    sources = [(units[s["unit"]], s["role"]) for s in tree.sources]
+    sources.sort(key=lambda x: (x[0].path, x[0].point, x[0].ordinal, order[x[1]]))
+    return sources, tree
+
+
+def check(rule, n):
+    expected, tree = literal(rule, n)
+    index = I.SourceIndex(rule, n, replicas=3)
+    need(index.size == len(expected), "full literal source count")
+    for rank, (unit, role) in enumerate(expected):
+        need(index.rank_source(unit, role) == rank, "literal source rank")
+        need(index.unrank_source(rank) == (unit, role), "literal source unrank")
+        for replica in (0, 2):
+            owner = ("flow", replica, "source", unit.path, unit.point, unit.ordinal, role)
+            physical = replica*index.size + rank
+            need(index.row(owner) == physical and index.owner(physical) == owner,
+                 "complete replicated physical row bijection")
+    q, G, d = len(index.paid), index.height, len(rule.types)
+    bound = 1 + q*comb(G+q-1, q) if G else 1
+    need(len(index.total) <= bound, "aggregated-state bound")
+    need(sum(map(len, index.point_data)) == comb(G+d, d), "point count")
+    return Counter(cases=1, sources=len(expected), states=len(index.total),
+                   literal_classes=len(tree.classes), native_units=len(tree.units))
+
+
+def rejected(action, label):
+    try:
+        action()
+    except (ValueError, AssertionError):
+        return label
+    raise ValueError("negative control accepted: " + label)
+
+
+def independent_counts(index):
+    """Count ordered target words by product, then subtract incoming units."""
+    targets = Counter(k for _, k in index.rule.roles)
+    words = [Counter({1: 1})]
+    for _ in range(index.height):
+        layer = Counter()
+        for product, count in words[-1].items():
+            for rank, weight in targets.items():
+                layer[product*rank] += count*weight
+        words.append(layer)
+    paid = tuple(r for r, _ in index.rule.rounds)
+    W = len(index.rule.roles)
+
+    @lru_cache(None)
+    def units(h, rho):
+        cap = index.rank // (index.rule.ambient*rho)
+        return sum(count for product, count in words[index.height-h].items()
+                   if product <= cap)
+
+    @lru_cache(None)
+    def subtree(h, rho, previous):
+        local = W*units(h, rho) - (units(h-1, rho//previous) if h else 0)
+        need(local == index.local[h, rho, previous], "independent local incoming subtraction")
+        total = local
+        if h < index.height:
+            total += sum(subtree(h+1, rho*r, r) for r in paid)
+        need(total == index.total[h, rho, previous], "independent subtree count")
+        return total
+
+    need(subtree(0, 1, 0) == index.size, "independent source total")
+    return subtree.cache_info().currsize
+
+
+def collision_family():
+    """Fixed rule whose same-depth states all hash alike; no timing claim."""
+    H, G = sys.hash_info.modulus, 8
+    rank = 8*H
+    rule = C.Rule((("single", rank),),
+                  tuple((H*s, "single") for s in (1, 2, 3, 5, 7)),
+                  ambient=rank)
+    index = I.SourceIndex(rule, rank**(G+1))
+    need(type(index.local) is I.SortedStateTable and
+         type(index.total) is I.SortedStateTable and
+         type(index.point_data) is list, "deterministic expanding metadata")
+    need(index.local._keys is index.total._keys, "shared fixed sorted key vector")
+    level_counts = []
+    for h in range(1, G+1):
+        layer = [state for state in index.total if state[0] == h]
+        need(len(layer) == 5*comb(h+3, 4), "exact colliding state family")
+        need(all(hash(rho) == hash(last) == 0 for _, rho, last in layer),
+             "integer hash collision witness")
+        need(all(hash(state) == hash(layer[0]) for state in layer),
+             "one state hash per positive depth")
+        need(all(index.local[state] == index.total[state] == 0 for state in layer),
+             "single target has no nonroot fresh source")
+        level_counts.append(len(layer))
+    need(index.size == 1 and len(index.total) == 1+5*comb(G+4, 5),
+         "collision-family exact count")
+    unit, role = index.unrank_source(0)
+    need(index.rank_source(unit, role) == 0 and unit.path == () and
+         unit.point == (G,) and role == "single", "collision-family row inverse")
+    return {"height": G, "hash_modulus": str(H), "states": len(index.total),
+            "states_per_positive_depth": level_counts,
+            "state_hashes_per_positive_depth": 1, "source_count": 1,
+            "lookup": "sorted keys and deterministic binary search"}
+
+
+def controls():
+    r = C.Rule((("small", 2), ("large", 5)), ((1, "small"), (1, "bank")))
+    index = I.SourceIndex(r, 10, replicas=2)
+    need(index.size == 4, "literal repeated-rank source fixture")
+    child = index.total[1, 1, 1]
+    bad_total = index.local[0, 1, 0] + child
+    out = [rejected(lambda: need(bad_total == index.size, "lost occurrence multiplicity"),
+                    "dropped repeated paid occurrence"),
+           rejected(lambda: index.unrank_source(index.size), "source upper endpoint"),
+           rejected(lambda: index.unrank_source(-1), "negative source index"),
+           rejected(lambda: index.owner(2*index.size), "replicated row upper endpoint")]
+    owner = index.owner(0)
+    out.append(rejected(lambda: index.row(("wrong",)+owner[1:]), "wrong namespace"))
+    out.append(rejected(lambda: index.row(owner[:2]+("owned",)+owner[3:]),
+                        "owned bank credited as source"))
+    matched = C.Unit((0,), (0, 0), 0)
+    out.append(rejected(lambda: index.rank_source(matched, "small"),
+                        "matched role passed as fresh source"))
+    other = I.SourceIndex(C.Rule((("a", 3), ("b", 5)),
+                           ((1, "a"), (2, "bank"))), 45)
+    need(other.local[2, 2, 1] == 1 and other.local[2, 2, 2] == 0,
+         "last-paid-rank distinction fixture")
+    out.append(rejected(lambda: need(other.local[2, 2, 1] == other.local[2, 2, 2],
+                                     "last rank omitted"), "dropped last paid rank"))
+    unit, role = index.unrank_source(0)
+    wrong_ordinal = C.Unit(unit.path, unit.point, C.multiplicity(r, unit.point))
+    out.append(rejected(lambda: index.rank_source(wrong_ordinal, role),
+                        "out-of-range native occurrence"))
+    child_sources = [index.unrank_source(rank) for rank in range(index.size)
+                     if index.unrank_source(rank)[0].path]
+    need(len(child_sources) == 2, "two equal-statistic sibling sources")
+    left, right = child_sources
+    out.append(rejected(lambda: need(index.rank_source(*left) == index.rank_source(*right),
+                                     "sibling path merged"), "physical occurrence merge"))
+    out.append(rejected(lambda: index.total[100, 1, 1], "absent sorted-table state"))
+    out.append(rejected(lambda: I.SortedStateTable(((1, 1, 1), (0, 1, 0))),
+                        "unsorted table keys"))
+    out.append(rejected(lambda: I.SortedStateTable(((0, 1, 0), (0, 1, 0))),
+                        "duplicate table keys"))
+    empty = I.SortedStateTable(((0, 1, 0),))
+    out.append(rejected(lambda: empty[0, 1, 0], "uninitialized table count"))
+    return out
+
+
+def main():
+    totals = Counter()
+    for ranks in ((2, 3), (2, 5), (3, 5), (4, 6)):
+        for duplicate in (False, True):
+            roles = (("large", ranks[1]), ("small", ranks[0]))
+            if duplicate:
+                roles += (("extra", ranks[0]),)
+            for owned in (False, True):
+                rule = C.Rule(roles, ((1, "small"), (min(ranks)-1,
+                               "bank" if owned else "large")), ambient=max(ranks)+1)
+                A, k = rule.ambient, min(ranks)
+                for n in (A, A*k-1, A*k, A*k*k-1, A*k*k, A*k*k*k):
+                    totals.update(check(rule, n))
+    rule = C.Rule((("c", 5), ("a", 3), ("b", 4), ("d", 3)),
+                  ((1, "a"), (1, "bank"), (2, "c")), ambient=7)
+    for n in (7, 21, 62, 63, 188, 189):
+        totals.update(check(rule, n))
+    large = I.SourceIndex(C.Rule((("a", 3), ("b", 3), ("c", 5), ("d", 5)),
+                         ((1, "a"), (1, "bank"), (2, "c")), ambient=7), 7*3**64)
+    samples = (0, 1, large.size//2, large.size-2, large.size-1)
+    for k in samples:
+        need(large.rank_source(*large.unrank_source(k)) == k, "large interval inverse")
+    need(len(large.total) <= 1+2*comb(65, 2), "large polynomial state bound")
+    independently_counted = independent_counts(large)
+    result = {"status": "PASS_CONTIGUOUS_SOURCE_INDEX", "totals": dict(totals),
+              "negative_controls": controls(), "collision_family": collision_family(),
+              "large_case": {
+                  "height": 64, "states": len(large.total),
+                  "target_multiindices": sum(map(len, large.point_data)),
+                  "independent_word_product_states": independently_counted,
+                  "literal_classes_not_enumerated": str((3**65-1)//2),
+                  "source_count": str(large.size), "round_trip_samples": len(samples)},
+              "scope": "offline logical row indexing; no payload tape tariff or kappa"}
+    print(json.dumps(result, indent=2, sort_keys=True))
+
+
+if __name__ == "__main__":
+    main()