From 91246e5131152ccb1f64a969c36706360861f821 Mon Sep 17 00:00:00 2001
From: Jerry Jiaheng Chen <80299683+CubeJerry@users.noreply.github.com>
Date: Wed, 11 Nov 2026 21:31:19 +0800
Subject: [PATCH] Construct exact Pascal occurrence and owner addresses without
 materializing compiler classes

---
 research/pascal-occurrence-codec/NOTICE.md    |  17 +
 research/pascal-occurrence-codec/PR.md        |  63 +++
 research/pascal-occurrence-codec/PROOF.md     | 221 ++++++++++
 research/pascal-occurrence-codec/README.md    | 135 +++++++
 research/pascal-occurrence-codec/REVIEW.md    |  52 +++
 research/pascal-occurrence-codec/SOURCES.json |  52 +++
 research/pascal-occurrence-codec/TASK.json    |  22 +
 .../pascal-occurrence-codec/VALIDATION.json   |  48 +++
 research/pascal-occurrence-codec/codec.py     | 222 ++++++++++
 .../independent_check.py                      |  94 +++++
 .../inputs/finite_dag_audit.py                | 379 ++++++++++++++++++
 research/pascal-occurrence-codec/verify.py    | 170 ++++++++
 12 files changed, 1475 insertions(+)
 create mode 100644 research/pascal-occurrence-codec/NOTICE.md
 create mode 100644 research/pascal-occurrence-codec/PR.md
 create mode 100644 research/pascal-occurrence-codec/PROOF.md
 create mode 100644 research/pascal-occurrence-codec/README.md
 create mode 100644 research/pascal-occurrence-codec/REVIEW.md
 create mode 100644 research/pascal-occurrence-codec/SOURCES.json
 create mode 100644 research/pascal-occurrence-codec/TASK.json
 create mode 100644 research/pascal-occurrence-codec/VALIDATION.json
 create mode 100644 research/pascal-occurrence-codec/codec.py
 create mode 100644 research/pascal-occurrence-codec/independent_check.py
 create mode 100644 research/pascal-occurrence-codec/inputs/finite_dag_audit.py
 create mode 100644 research/pascal-occurrence-codec/verify.py

diff --git a/research/pascal-occurrence-codec/NOTICE.md b/research/pascal-occurrence-codec/NOTICE.md
new file mode 100644
index 0000000000..33f0adc8ca
--- /dev/null
+++ b/research/pascal-occurrence-codec/NOTICE.md
@@ -0,0 +1,17 @@
+# Notice
+
+New Pascal interval codec, proof and scoped verifier: prepared for Jerry Chen
+(@CubeJerry), with substantial OpenAI assistance, 2026. Apache-2.0.
+
+`inputs/finite_dag_audit.py` is a byte-identical retained source from
+`research/kappa-rebuild/transfer-audit/finite_dag_audit.py` at canonical commit
+`e54523517d0f03e58352e647c403a5af3e525a57`. Its Apache-2.0 and OpenAI-assistance
+header is preserved. The compiler/audit work is credited to zxv and its
+retained predecessor lineage. Jacob Alan Sussman supplies the underlying
+Theorem 1G integer lockstep/Pascal construction; this package does not claim
+that flow or its original independence proof as new work.
+
+Mark / Matarener's live-role and completion/lifetime work and Jerry Chen's
+occurrence-layout work supply cited predecessor contracts. Their source
+packages remain unchanged. A separate AI review, if supplied, is not human
+peer review or proof-kernel acceptance.
diff --git a/research/pascal-occurrence-codec/PR.md b/research/pascal-occurrence-codec/PR.md
new file mode 100644
index 0000000000..fe82e035b9
--- /dev/null
+++ b/research/pascal-occurrence-codec/PR.md
@@ -0,0 +1,63 @@
+## Change and mathematical scope
+
+The finite mixed-target compiler currently obtains its owner matching by
+materializing per-rank occurrence buckets. This adds an exact arithmetic
+codec for that same ordered Pascal bijection and a direct physical-owner
+lookup using at most G+1 ancestry decisions. It supplies one concrete part
+of #6878's outstanding final-occurrence-emitter obligation.
+
+The proof covers arbitrary separated finite rules, every valid integer top
+rank, actual ambient caps above the largest target, arbitrary native role
+order, owned fields and distinct invocation/replica namespaces. It includes
+descriptor size and a separately charged offline big-integer work bound.
+This is an enabling compiler lemma: **no new kappa or assumption discharge**.
+The selected conditional bound remains 0.00363005817.
+
+## Novelty relative to predecessors
+
+#4359's precompilation and literal audit already establish the Pascal count,
+rank descent and denominator clearing. #4691 already establishes the general
+live-role induction, and #6878 supplies charged occurrence geometry. The new
+step is an explicit inverse of the actual ordered bucket pairing, followed
+by a terminating owner-address algorithm requiring no occurrence table.
+The package preserves and authenticates its unchanged predecessor oracle.
+
+## Verification
+
+```sh
+python3 -I -W error -B research/pascal-occurrence-codec/verify.py
+python3 -I -W error -O -B research/pascal-occurrence-codec/verify.py
+```
+
+Both modes pass 242 complete small flows, 1,665 ordered class streams, 9,934
+role-owner comparisons, 4,998 exact matched edges and 2,132 terminal owners.
+There are ten input-validation and semantic controls, including invalid ranks, missing letters,
+duplicate identities, wrong offsets and cap/replica errors. A 128-level query
+addresses a 2^128 occurrence population without enumerating it. The extended
+ambient fixtures override only the oracle's declared ambient property; that
+test adapter and the source-aware comparison are explicitly disclosed.
+
+Exact base: `e54523517d0f03e58352e647c403a5af3e525a57`.
+Source Git blobs and SHA256 values are in SOURCES.json. The written all-size
+proof, finite evidence, arithmetic costs and unexecuted obligations are separate.
+
+## Limits and next obligations
+
+The complete selected product/owner manifest, contiguous source rank/unrank,
+all source complements and recursive substitutions, native endpoints,
+physical row/tape lowering and precision/recovery remain open or inherited.
+The algorithm is offline logical addressing; a name does not provide free
+random access. No actual winning-rank word, practical speedup, supplier
+admission, human review or proof-kernel acceptance is claimed.
+
+## Credit
+
+Prepared for Jerry Chen / **@CubeJerry** with substantial OpenAI assistance.
+Jacob Alan Sussman supplies the lockstep/Pascal flow; zxv supplies the retained
+finite compiler/audit; Mark / Matarener supplies the live-role/completion work;
+@CubeJerry and the retained native/geometry contributors supply #6878's
+predecessor interface. Original oracle bytes and notices are preserved.
+
+## Additional independent review
+
+[independent review](https://github.com/CubeJerry/integer-mult-bounds/blob/research/pascal-occurrence-codec-20261111-1313/research/pascal-occurrence-codec/REVIEW.md) records a separate proof review, byte-identical remote oracle check, and 1,092 literal-word plus 171 owner-graph checks. Reproduce with `python3 -I -W error -B research/pascal-occurrence-codec/independent_check.py`. This AI review is not human or formal-kernel verification.
diff --git a/research/pascal-occurrence-codec/PROOF.md b/research/pascal-occurrence-codec/PROOF.md
new file mode 100644
index 0000000000..d0905fdac4
--- /dev/null
+++ b/research/pascal-occurrence-codec/PROOF.md
@@ -0,0 +1,221 @@
+# A direct Pascal codec for complete lockstep occurrences
+
+## 1. Contract and distinction from the inherited flow
+
+Fix an ordered finite list of productive roles `t=0,...,W-1`, each with
+integer target rank `k(t)>=2`, and an ordered finite list of paid occurrences
+`j=0,...,P-1`. Occurrence j has positive rank r(j) and acts on exactly one
+productive role or one separately named owned bank. All names are distinct,
+and owned banks are disjoint from productive roles. Require
+
+`r_max < k_min <= k_max <= A`,
+
+where A is the actual ambient cap. It need not occur as a target rank.
+For a positive integer N>=A, set `G=max{g:A*k_min^g<=N}`.
+
+The native endpoint, arbitrary-input contract, spectator correctness,
+whole-job adapters, allowed initialization/erasure and costs are retained
+premises. This result only constructs the logical field-address and matching
+layer of the finite compiler. It supplies neither those primitives nor a
+fixed-tape execution bound.
+
+The inherited `finite_dag_audit.py` materializes each class, gathers matching
+target slots in a dictionary indexed by their augmented multiindex, and pairs
+incoming jobs to that list in order. Its class-unit order is lexicographic
+multiindex, then increasing unit ordinal; role order is the supplied native
+role list. We give exactly that bijection as arithmetic on one occurrence
+descriptor, and then resolve its physical owner without a stored class or
+owner table. The original Pascal and live-role arguments retain their credit.
+
+## 2. The interval bijection
+
+Let the distinct target ranks be `k_0<...<k_(d-1)` and let `W_i` be the
+number of roles of rank k_i. For a nonnegative multiindex alpha put
+
+`c(alpha)=product_i k_i^alpha_i`,
+
+`u(alpha)=|alpha|! / product_i alpha_i! * product_i W_i^alpha_i`.
+
+For `|alpha|>0`, the weighted Pascal identity is
+
+`u(alpha)=sum_(i:alpha_i>0) W_i u(alpha-e_i)`.
+
+For each present i define
+
+`b_i=sum_(h<i, alpha_h>0) W_h u(alpha-e_h)`.
+
+The half-open intervals
+
+`[b_i,b_i+W_i u(alpha-e_i))`
+
+partition `[0,u(alpha))`. Therefore every ordinal a in this interval has the
+unique representation
+
+`a=b_i+W_i*v+l`,  with `0<=v<u(alpha-e_i)` and `0<=l<W_i`.
+
+The decoded child is its unit at point `alpha-e_i`, ordinal v, and the l-th
+native role of rank k_i. Conversely those data recover a by the displayed
+formula. All operations are on integers; no rounded population or fractional
+array occurs.
+
+**Order correspondence.** At fixed alpha, the child points `alpha-e_i`
+appear in increasing i order in the predecessor's lexicographic lattice.
+Within one child point its unit ordinal increases first and the matching
+roles retain native order. Hence its target-slot list consists precisely of
+the blocks above. The parent supply bucket uses increasing ordinal a at
+point alpha. Encode/decode consequently reproduce its exact ordered pairing,
+not just a rank histogram or an arbitrary equinumerous matching. This holds
+even when the native role list is not grouped by target rank.
+
+## 3. Capacity, sources and exact matched ranks
+
+A class has a paid-occurrence path `p=(j_1,...,j_h)` and dilation
+`rho(p)=product r(j_l)`. Its unit descriptors are
+
+`(p,alpha,a)`, where `|alpha|=G-h`, `0<=a<u(alpha)`,
+and `A rho(p)c(alpha)<=N`.
+
+A child slot `(p,beta,v,t)` with nonempty path has potential parent
+
+`p'=p without its last occurrence`,
+`alpha=beta+e_i`, where `k(t)=k_i`,
+`a=b_i+W_i*v+l(t)`.
+
+If `A rho(p')c(alpha)<=N`, that parent exists and issues the slot's job at
+the last paid occurrence j of p. The requested and delivered ranks agree:
+
+`r(j)rho(p')c(alpha)=k_i rho(p)c(beta)`.
+
+If the potential parent is absent, this is a fresh source. Root-class slots
+are fresh sources by definition. This criterion is exact: for a present parent
+of point alpha, every Pascal child group is present because
+
+`A rho(p') r(j)c(alpha-e_i)
+ = A rho(p')c(alpha) r(j)/k_i <=N`.
+
+The strict separation assumption makes the ratio less than one. Thus the
+entire interval bijection is available whenever its parent bucket exists;
+otherwise its incoming bucket is empty. There is no partially funded prefix
+to hide. Extending this codec unchanged to overlapping paid/target ranks is
+not justified and its public constructor rejects that input.
+
+Every fresh source rank s is in `(N/A,N]`. Its upper bound follows from
+`k_i<=A` and the child's fit inequality. At a nonroot source, parent absence
+gives `A rho(p')c(alpha)>N`, and thus
+`s=r(j)rho(p')c(alpha)>r(j)N/A>=N/A`.
+At a root source, `A c(alpha)k_i>N` follows from the definition of G:
+otherwise the degree-G+1 multiindex `alpha+e_i` would fit.
+
+Every terminal paid exit has `e=r(j)rho(p)c(0)<N`, since its unit fits and
+`r(j)<A`. A source complement N-s is either zero or smaller than N. These
+facts recover the inherited strict-descent domain with the actual ambient
+cap A, including the selected construction's case with no rank-A target.
+They are compatibility checks, not new asymptotic leaf estimates.
+
+## 4. Direct physical-owner identifiers
+
+Supply an external namespace identifying this particular flow invocation
+and a nonnegative replica number. They remain part of every identifier.
+Define
+
+`Source(namespace,replica,p,alpha,a,t)` and
+`Owned(namespace,replica,p,alpha,a,b)`
+
+for a source slot t and an owned bank b of one unit. Tags are different even
+if their payload values happen to agree. The identifier is a mathematical
+field name, not permission to read that field in constant machine time.
+
+To resolve the physical field of a productive slot, compute its potential
+parent by Section 3. If absent, return its Source identifier. If present,
+inspect the last paid occurrence's actual owner. When that owner is an owned
+bank, return its Owned identifier on the parent unit. Otherwise replace the
+current slot by that productive parent slot and repeat. Each iteration removes
+one paid occurrence, so at most `|p|+1<=G+1` such decisions terminate the lookup.
+The algorithm never enumerates the other unit occurrences.
+
+**Owner equivalence.** Induct on |p|. A root slot is exactly the predecessor's
+fresh input. A later unmatched slot is exactly its fresh input by the capacity
+criterion. A matched slot receives exactly the field on which the issuing
+parent's paid occurrence acts, by the ordered bijection. That field is either
+the explicitly named parent owned bank or the parent's productive field,
+already identified by induction. Thus the returned name equals the literal
+compiler's physical field after replacing its sequential numeric source/owned
+labels by these canonical occurrence labels. It need not equal the literal
+compiler's arbitrary numeric uid.
+
+**Distinct live fields.** Within one class, the parent supplies one job per
+unit at the same paid position. The interval bijection uses each such job
+exactly once. Assuming the parent class's fields are distinct, these matched
+fields are distinct. New source tags are distinct and cannot coincide with
+an ancestor's tag; owned tags are separate per unit. Induction therefore gives
+injective productive/owned field identities within each class. Reuse along
+a chain of suspended ancestors is intended and is not a new productive input.
+The inherited lockstep schedule completes a child class before resuming its
+parent. This codec specifies the identical owner on that schedule; it does
+not replace the separate lifetime proof.
+
+Paid paths record occurrence numbers, not just their ranks or product.
+Two paid positions of equal rank can act on different owners and require
+different source fields. Replica and invocation namespaces similarly cannot
+be discarded. Source, owned and replica labels receive no productive credit
+beyond the source count already present in the original flow.
+
+## 5. Representation and separately paid arithmetic
+
+Let S be the bit size of the read-only finite role/paid-owner specification,
+using integer role indices, and write `ell(x)=ceil(log2(x+1))`. The live
+query descriptor and answer require
+
+`O(S + log N + d ell(G) + G ell(W+P))` bits.
+
+The point has d entries at most G. The path has at most G paid indices.
+An occurrence ordinal has at most `G log2 W+1` bits because the total number
+of weighted words of length G is `W^G`, and u(alpha) is one of its groups.
+Valid capacities/columns and the one-step absent-parent comparison have
+`O(log N+log A)` bits. Intermediate weighted multinomial computations can be
+done by exact small-factor binomial recurrences; they need no factorial-sized
+table. A returned symbolic identifier and its constituent fields are counted
+in the bound. No occurrence dictionary, GL cover or generated instruction
+list is counted as implicit free storage.
+
+This is **offline arithmetic**, not unit-cost execution on a Turing machine.
+For a conservative implementation let
+
+`B=S+ell(N)+(G+1)ell(W+P+A+G+2)`.
+
+One u(alpha) uses O(G+d) exact integer multiply/divide operations, with
+O(Sd) additional scans if target weights are recomputed from the fixed input.
+Encode tests at most d blocks and the owner query has at most G+1 levels.
+Including validation, path products and linear role lookup gives the loose
+bound
+
+`O((S+1)(d+1)^2(G+1)^2 B^2)` bit operations
+
+using schoolbook multiplication and division. This upper bound is deliberately
+conservative; no practical speedup or constant-time random access is asserted.
+The code's Python tuples/dictionaries are verification conveniences, not a
+fixed-tape lowering. The all-size claim is the algorithm and the foregoing
+integer argument, not extrapolation from measured Python timings.
+
+`iter_units` streams the predecessor's ordered class descriptors with ordinary
+lexicographic counters. Its total time must include every emitted item;
+the per-query bound does not turn a huge complete output into a short output.
+Ranking all fresh Source names into a contiguous physical row interval,
+integrating source complements and smaller-rank invocations, and generating
+all actual native segments remain subsequent tasks.
+
+## 6. What this contributes to the selected compiler assumption
+
+The selected #7000 proof uses a separated completed unit, actual ambient
+`A=153^1920` and finite compiler rank `N=2^H_C`. The codec theorem permits
+that domain abstractly whenever the full finite role/paid-owner specification
+is supplied. It does not materialize A, N, the product's role list, all source
+arrays or its emitted word. Merely supplying the number A or an invoice does
+not supply the role/owner specification.
+
+The reduction is precise: the compiler's previously implicit per-bucket
+Pascal matching and physical-owner lookup can be replaced by the explicit,
+terminating local algorithm above. The remaining emitter must supply the
+finite product/completion/splitting role manifest, contiguous source indexing,
+owned initialization/erasure, complete coordinate routes and physical tariff.
+The selected five assumptions and the accepted kappa remain unchanged.
diff --git a/research/pascal-occurrence-codec/README.md b/research/pascal-occurrence-codec/README.md
new file mode 100644
index 0000000000..747e58ad34
--- /dev/null
+++ b/research/pascal-occurrence-codec/README.md
@@ -0,0 +1,135 @@
+# Construct exact Pascal occurrence and owner addresses without materializing compiler classes
+
+**Scoped constructive compiler lemma; no new kappa.** The finite mixed-target
+compiler can resolve its exact chronological matching and the physical field
+behind any productive occurrence by arithmetic on one descriptor. A query
+uses at most G+1 ancestor decisions and does not build its class, matching
+bucket or owner table. The construction covers every positive integer top
+rank in the separated-flow domain, with the actual ambient cap A allowed to
+exceed every target rank.
+
+This answers one part of [#6878](https://github.com/CrocSwap/integer-mult-bounds/pull/6878)'s
+request for an explicit occurrence emitter: the previously implicit ordered
+Pascal matching and owner-address lookup now have a concrete, terminating
+codec. The selected conditional value stays **0.00363005817**. All five
+selected assumptions remain; this package does not claim a complete dispatcher.
+
+## Exact result
+
+For target multiplicities W_i and multiindex alpha, let
+
+`u(alpha)=multinomial(|alpha|;alpha)*product W_i^alpha_i`.
+
+The parent occurrence interval `[0,u(alpha))` partitions into blocks of
+length `W_i*u(alpha-e_i)`. In the block for i, quotient and remainder by W_i
+give the child occurrence and the exact native role. The inverse reconstructs
+the parent ordinal. This is the ordering used by the retained literal compiler,
+including native role lists whose equal-rank roles are not adjacent.
+
+At a child occurrence, the actual ambient inequality decides whether that
+parent exists. Otherwise the slot is a new source. If it exists, following
+the paid occurrence's actual productive or owned owner removes one path
+letter. Repeating reaches the canonical source or owned-bank identifier.
+Paths distinguish paid *positions*, not merely equal ranks, and retain the
+invocation namespace and replica number.
+
+[PROOF.md](PROOF.md) establishes the bijection, exact source classification,
+matched-rank equality, owner identity, injectivity within every live class,
+termination and descriptor bounds. It separately charges integer arithmetic:
+the offline lookup has an explicit polynomial bit-work bound. A symbolic
+field name does not grant constant-time access to that field on tapes.
+
+## Evidence and reproduction
+
+From the repository root, after placing this directory at
+`research/pascal-occurrence-codec/`:
+
+```sh
+python3 -I -W error -B research/pascal-occurrence-codec/verify.py
+python3 -I -W error -O -B research/pascal-occurrence-codec/verify.py
+```
+
+Standard-library Python 3.12 suffices. Both commands print
+`PASS_PASCAL_OCCURRENCE_CODEC` in their JSON result. Local runs agree exactly.
+
+| Executed coverage | Count |
+|---|---:|
+| Complete small flow instances | 242 |
+| Instances with A greater than every target rank | 130 |
+| Ordered class streams | 1,665 |
+| Native unit occurrences | 3,310 |
+| Productive role owner comparisons | 9,934 |
+| Exact matched-edge comparisons | 4,998 |
+| Fresh source identifiers | 4,936 |
+| Terminal paid owner comparisons | 2,132 |
+| Negative controls | 10 |
+
+The oracle is the byte-identical retained `finite_dag_audit.py`, pinned by
+Git blob and SHA256 in [SOURCES.json](SOURCES.json). For the 130 ambient-cap
+fixtures, an explicit test adapter overrides only its `Rule.dimension`
+property. Every matching, class, source, exit and field computation remains
+the retained oracle's code. This parameter adapter is disclosed rather than
+described as unchanged-source coverage of the larger ambient domain.
+
+Separate tests resolve a 128-generation chain into the last of `2^128`
+root occurrences without enumerating that population. Controls reject zero
+ranks, overlapping paid/target ranks, duplicate productive labels, a missing
+Pascal letter, an invalid ordinal, a wrong interval offset, repeated occurrence
+identities, an absent unit at the cap boundary and omitted replica identity.
+These checks corroborate the written universal proof; they do not establish
+it by extrapolation. The oracle is independently authored predecessor work,
+but this codec's author read that source, so this is not a blind comparison.
+
+## Novelty and limits
+
+Jacob Alan Sussman's weighted Pascal flow and zxv's finite precompilation
+already supply the counting identity, chronological schedule, denominator
+clearing and rank descent. [#4691](https://github.com/CrocSwap/integer-mult-bounds/pull/4691)
+already proves the general live-role induction and tests an event-level
+executor. [#6878](https://github.com/CrocSwap/integer-mult-bounds/pull/6878)
+already constructs charged complete-coordinate occurrence routes. Those
+results are not claimed again as new theorems.
+
+The addition is a direct arithmetic inverse to the actual ordered bucket
+matching and a terminating, table-free owner-address algorithm, with source
+equivalence and explicit descriptor/arithmetic costs. Its input is a complete
+finite native role/paid-owner specification, not a rank histogram. The selected
+1920-fold product and its winning uniform rank are not materialized here.
+The codec has not been installed into a full native, numerical or tape caller.
+No total-time speedup, smaller threshold, supplier admission, human peer review
+or proof-kernel acceptance is claimed.
+
+Bounded overlap inspection covered the pinned compiler, live-role,
+completion, source-law and occurrence-layout packages; research-directory
+metadata; and GitHub searches for Pascal/codec, lazy/compiler and
+occurrence/matching. #7136/#7137 concern a different V02 compiler-input/custody
+workstream. Absence of another matching search result is not proof of novelty.
+
+## Open next questions
+
+1. **Rank fresh source names into contiguous row intervals without a table.**
+   Start by deriving subtree source counts for the existing paid-path order.
+   This would connect the codec to integer batching and actual row ownership;
+   count-level source conservation alone does not supply this rank/unrank map.
+2. **Bind one complete selected occurrence stream.** Start with the actual
+   chronological product at power two and its complete paid-owner manifest,
+   then compose the codec with #6878's routes. The enormous final product
+   manifest and all native segments remain explicit missing inputs.
+3. **Lower the resulting metadata service with its complete physical bill.**
+   Choose a descriptor representation and charge scans, big-integer work,
+   source access, restoration and nested bank lifetime. The present offline
+   algorithm is not a fixed-tape tariff and cannot remove precision_tape.
+
+## Provenance and credit
+
+Canonical base: `e54523517d0f03e58352e647c403a5af3e525a57`.
+Prepared for **Jerry Chen / @CubeJerry** with substantial OpenAI assistance.
+Credit Jacob Alan Sussman for the lockstep/Pascal construction; zxv for
+`FINITE-PRECOMPILATION.md` and its literal audit; Mark / Matarener for #4691
+and the completion/lifetime executor; and @CubeJerry and predecessor authors
+for #6878's occurrence-layout theorem. The source oracle retains its original
+header and is not modified. Apache-2.0. See [NOTICE.md](NOTICE.md).
+
+## Additional independent review
+
+[REVIEW.md](REVIEW.md) records a separate proof review, byte-identical remote oracle check, and 1,092 literal-word plus 171 owner-graph checks. Reproduce with `python3 -I -W error -B research/pascal-occurrence-codec/independent_check.py`. This AI review is not human or formal-kernel verification.
diff --git a/research/pascal-occurrence-codec/REVIEW.md b/research/pascal-occurrence-codec/REVIEW.md
new file mode 100644
index 0000000000..67dfcb1a7c
--- /dev/null
+++ b/research/pascal-occurrence-codec/REVIEW.md
@@ -0,0 +1,52 @@
+# Independent orchestration review
+
+Reviewed at canonical base `e54523517d0f03e58352e647c403a5af3e525a57`.
+This is a separate AI reasoning/checking pass, not human peer review or a
+formal-kernel proof. The reviewer read the proposed claim and implementation.
+
+## Mathematical checks
+
+The interval partition follows exactly from weighted Pascal, with lower-type
+intervals preceding higher types because `alpha-e_i` is lexicographically
+increasing in i. Within an interval, quotient and remainder preserve the
+predecessor's unit-first, native-role-second order. Strict separation ensures
+that every predecessor child block fits whenever its parent fits; no partially
+funded bucket is silently treated as complete.
+
+At a missing parent, the cap inequality gives the stated strict source band;
+at the root, degree G+1 implies a product at least `k_min^(G+1)>N/A`.
+Every owner lookup removes a paid-path position. Distinct matched fields follow
+from the bijection and the parent's distinct live fields, while fresh source,
+owned-bank, invocation and replica tags preserve the intended identities.
+The proof separates descriptor arithmetic from physical source access.
+
+## Independent executable check
+
+`independent_check.py` enumerates literal words over productive role names,
+then constructs a materialized parent-owner graph. It uses neither the
+predecessor audit nor the interval formula to generate expected answers.
+
+```sh
+python3 -I -W error -B research/pascal-occurrence-codec/independent_check.py
+```
+
+Executed result: `PASS_INDEPENDENT_PASCAL_REVIEW`, 1,092 word codec cases and
+171 owner comparisons, including owned-bank stops and full-class injectivity.
+The checked codec SHA256 is
+`cec2c8b5e153a264127e8301ed59591fe97c9a46078ff2343b3784d177c6984d`.
+
+The normal and optimized main verifier were also rerun in separate fresh
+bytecode namespaces. Both reproduce the recorded 242-flow result. The vendored
+oracle was fetched independently by its canonical Git blob and compared byte
+for byte with `inputs/finite_dag_audit.py`; all 19,149 bytes agree.
+Input-validation and semantic fault controls are distinguished from universal
+proof. The finite checks corroborate the arguments above.
+
+## Decision and boundaries
+
+Approved for publication as a scoped logical compiler lemma. The complete
+selected manifest, contiguous source numbering, payload realization, tape
+costs and the five registered assumptions remain open or inherited. There is
+no new kappa, complete multiplier, human review or formal-kernel acceptance.
+
+Prepared for Jerry Chen / @CubeJerry with substantial OpenAI assistance.
diff --git a/research/pascal-occurrence-codec/SOURCES.json b/research/pascal-occurrence-codec/SOURCES.json
new file mode 100644
index 0000000000..624086c3f1
--- /dev/null
+++ b/research/pascal-occurrence-codec/SOURCES.json
@@ -0,0 +1,52 @@
+{
+  "repository": "CrocSwap/integer-mult-bounds",
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "source_files": [
+    {
+      "path": "research/kappa-rebuild/architecture/FINITE-PRECOMPILATION.md",
+      "pin": "e54523517d0f03e58352e647c403a5af3e525a57",
+      "git_blob": "4badb40f0919c515823cb07e44c6470d4d6469ca",
+      "sha256": "4cb32f6b8e388ecf6ed41b5bbdeeb4539cb40c8424f194974afea58f7e0921e8",
+      "usage": "provenance"
+    },
+    {
+      "path": "research/kappa-rebuild/transfer-audit/finite_dag_audit.py",
+      "pin": "e54523517d0f03e58352e647c403a5af3e525a57",
+      "git_blob": "c1798bfa9c1d47a40313a276a8ce639c232143e5",
+      "sha256": "f842f0e07ca40a181782a565a381b0ee20c6a4b08b8c2b8a4d5d630381bd1e8e",
+      "usage": "vendored_oracle"
+    },
+    {
+      "path": "research/lockstep-live-role-audit/README.md",
+      "pin": "e54523517d0f03e58352e647c403a5af3e525a57",
+      "git_blob": "158858c0a330465589c6b584926ec8b050191490",
+      "sha256": "0f3de4ae60ec52ad8096f5979db88e9949d8a54b50364b902ffb66a9b39eb075",
+      "usage": "provenance"
+    },
+    {
+      "path": "research/selected-compiler-occurrence-layout/README.md",
+      "pin": "e54523517d0f03e58352e647c403a5af3e525a57",
+      "git_blob": "54a8eb481cc46c583421fc022574964394305160",
+      "sha256": "ed613492d83b15af49f1c60bf5b788229df89d56db92733d1671f305c4370bca",
+      "usage": "provenance"
+    },
+    {
+      "path": "research/selected-compiler-occurrence-layout/PROOF.md",
+      "pin": "e54523517d0f03e58352e647c403a5af3e525a57",
+      "git_blob": "152fcd41486dc8d078ae2a77cb3e6a26c37e8e10",
+      "sha256": "dbc8af6f9f6bef61b7c9a4b19a20a2233e7e2551b9979c852bebba27028a9a49",
+      "usage": "provenance"
+    },
+    {
+      "path": "research/lockstep-completion-pass/README.md",
+      "pin": "e54523517d0f03e58352e647c403a5af3e525a57",
+      "git_blob": "373c6b79ccee78fb32d759c62f7aaf04418f68c8",
+      "sha256": "a5bc9b00044e3b252b821bdedc47787cbd405cca3ac0edb7875042fea96eaf1d",
+      "usage": "provenance"
+    }
+  ],
+  "vendored_oracle": "inputs/finite_dag_audit.py",
+  "selected_kappa": "0.00363005817",
+  "claimed_new_kappa": null,
+  "oracle_modification": "Source byte-identical; test adapter overrides only Rule.dimension to declared ambient for 130 fixtures."
+}
diff --git a/research/pascal-occurrence-codec/TASK.json b/research/pascal-occurrence-codec/TASK.json
new file mode 100644
index 0000000000..9376ceded9
--- /dev/null
+++ b/research/pascal-occurrence-codec/TASK.json
@@ -0,0 +1,22 @@
+{
+  "task": "user-assigned foundational compiler implication",
+  "base": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "track": [
+    50,
+    75
+  ],
+  "scope": "exact ordered Pascal interval codec and direct logical owner lookup",
+  "excluded": [
+    "rank exponent optimization",
+    "new kappa",
+    "physical fixed-tape tariff",
+    "complete selected word"
+  ],
+  "outcome": "scoped constructive all-size lemma with bounded exact source comparison",
+  "research_package_hook": "standalone verifier; no automatic replay hook registered",
+  "open_next_questions": [
+    "contiguous fresh source rank/unrank",
+    "selected finite product-owner manifest binding",
+    "physical metadata lowering and complete costs"
+  ]
+}
diff --git a/research/pascal-occurrence-codec/VALIDATION.json b/research/pascal-occurrence-codec/VALIDATION.json
new file mode 100644
index 0000000000..9e428a4928
--- /dev/null
+++ b/research/pascal-occurrence-codec/VALIDATION.json
@@ -0,0 +1,48 @@
+{
+  "python": "3.12.14",
+  "platform": "Linux-6.18.57-x86_64-with-glibc2.41",
+  "normal_exit": 0,
+  "optimized_exit": 0,
+  "outputs_equal": true,
+  "result": {
+    "ambient_exceeds_target_cases": 130,
+    "cases": 242,
+    "long_ancestry_depth": 128,
+    "negative_controls": [
+      "zero target rank",
+      "zero paid rank",
+      "nonseparated rank",
+      "duplicate productive label",
+      "missing Pascal letter",
+      "out-of-range occurrence",
+      "wrong offset",
+      "duplicated occurrence",
+      "absent cap-boundary unit",
+      "dropped replica"
+    ],
+    "oracle_sha256": "f842f0e07ca40a181782a565a381b0ee20c6a4b08b8c2b8a4d5d630381bd1e8e",
+    "scope": "logical identity, no tape tariff or kappa",
+    "status": "PASS_PASCAL_OCCURRENCE_CODEC",
+    "totals": {
+      "classes": 1665,
+      "exits": 2132,
+      "matched": 4998,
+      "roles": 9934,
+      "sources": 4936,
+      "units": 3310
+    },
+    "unmaterialized_root_occurrences": "2^128"
+  },
+  "human_review": false,
+  "formal_kernel": false,
+  "cold_selected_replay": false,
+  "complete_selected_emitter": false,
+  "orchestrator_review": {
+    "proof": "REVIEW.md",
+    "command": "python3 -I -W error -B research/pascal-occurrence-codec/independent_check.py",
+    "word_cases": 1092,
+    "owner_cases": 171,
+    "remote_oracle_bytes_equal": true,
+    "canonical_main_rechecked": "e54523517d0f03e58352e647c403a5af3e525a57"
+  }
+}
diff --git a/research/pascal-occurrence-codec/codec.py b/research/pascal-occurrence-codec/codec.py
new file mode 100644
index 0000000000..2fb4426cc8
--- /dev/null
+++ b/research/pascal-occurrence-codec/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/pascal-occurrence-codec/independent_check.py b/research/pascal-occurrence-codec/independent_check.py
new file mode 100644
index 0000000000..9b87fc1fa7
--- /dev/null
+++ b/research/pascal-occurrence-codec/independent_check.py
@@ -0,0 +1,94 @@
+#!/usr/bin/env python3
+"""Root review by literal words and a separately materialized owner graph.
+
+Written without using the predecessor oracle or the codec's interval formula.
+Apache-2.0; prepared for CubeJerry with substantial OpenAI assistance.
+"""
+import hashlib
+import itertools
+import json
+from pathlib import Path
+import sys
+import types
+
+HERE = Path(__file__).resolve().parent
+raw = (HERE / 'codec.py').read_bytes()
+C = types.ModuleType('root_review_codec')
+sys.modules[C.__name__] = C
+exec(compile(raw, str(HERE / 'codec.py'), 'exec'), C.__dict__)
+
+
+def need(ok, message):
+    if not ok:
+        raise ValueError(message)
+
+
+def main():
+    rule = C.Rule((('a', 3), ('b', 3), ('c', 5)),
+                  ((1, 'a'), (2, 'bank'), (2, 'b')))
+    names = tuple(name for name, _ in rule.roles)
+    types_ = (3, 5)
+    type_index = {'a': 0, 'b': 0, 'c': 1}
+    role_index = {'a': 0, 'b': 1, 'c': 0}
+
+    def order(word):
+        if not word:
+            return ()
+        return (type_index[word[-1]], order(word[:-1]), role_index[word[-1]])
+
+    def words(point):
+        return sorted((word for word in itertools.product(names, repeat=sum(point))
+                       if tuple(sum(type_index[x] == i for x in word)
+                                for i in range(2)) == point), key=order)
+
+    word_cases = 0
+    for degree in range(1, 7):
+        for first in range(degree + 1):
+            point = (first, degree-first)
+            literal = words(point)
+            need(len(literal) == C.multiplicity(rule, point), 'literal word count')
+            for index, word in enumerate(literal):
+                child, ordinal, role = C.decode(rule, point, index)
+                need(words(child)[ordinal] + (role,) == word, 'literal decode')
+                need(C.encode(rule, point, ordinal, role) == index, 'literal encode')
+                word_cases += 1
+
+    owner_cases = 0
+    for rank in (5, 15, 24, 45, 80):
+        flow, owners = C.FlowCodec(rule, rank), {}
+        for depth in range(flow.height + 1):
+            for path in itertools.product(range(3), repeat=depth):
+                dilation = 1
+                for site in path:
+                    dilation *= rule.rounds[site][0]
+                degree = flow.height-depth
+                class_fields = []
+                for first in range(degree + 1):
+                    point = (first, degree-first)
+                    if 5*dilation*3**point[0]*5**point[1] > rank:
+                        continue
+                    for ordinal, word in enumerate(words(point)):
+                        unit = C.Unit(path, point, ordinal)
+                        for role in names:
+                            parent = tuple(point[i] + (i == type_index[role]) for i in range(2))
+                            parent_scale = dilation//rule.rounds[path[-1]][0] if path else None
+                            if not path or 5*parent_scale*3**parent[0]*5**parent[1] > rank:
+                                expected = ('flow', 0, 'source', path, point, ordinal, role)
+                            else:
+                                parent_ordinal = words(parent).index(word + (role,))
+                                owner = rule.rounds[path[-1]][1]
+                                expected = (('flow', 0, 'owned', path[:-1], parent,
+                                             parent_ordinal, owner) if owner == 'bank' else
+                                            owners[(path[:-1], parent, parent_ordinal, owner)])
+                            need(flow.owner(unit, role) == expected, 'literal owner graph')
+                            owners[(path, point, ordinal, role)] = expected
+                            class_fields.append(expected)
+                            owner_cases += 1
+                need(len(class_fields) == len(set(class_fields)), 'class owner alias')
+    print(json.dumps({'status': 'PASS_INDEPENDENT_PASCAL_REVIEW',
+                      'word_cases': word_cases, 'owner_cases': owner_cases,
+                      'codec_sha256': hashlib.sha256(raw).hexdigest()}, sort_keys=True))
+
+
+if __name__ == '__main__':
+    main()
diff --git a/research/pascal-occurrence-codec/inputs/finite_dag_audit.py b/research/pascal-occurrence-codec/inputs/finite_dag_audit.py
new file mode 100644
index 0000000000..c1798bfa9c
--- /dev/null
+++ b/research/pascal-occurrence-codec/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/pascal-occurrence-codec/verify.py b/research/pascal-occurrence-codec/verify.py
new file mode 100644
index 0000000000..ff485bb505
--- /dev/null
+++ b/research/pascal-occurrence-codec/verify.py
@@ -0,0 +1,170 @@
+#!/usr/bin/env python3
+"""Bounded, exact checks of the logical Pascal owner codec (stdlib only)."""
+import hashlib
+import importlib.util
+import itertools
+import json
+from pathlib import Path
+import sys
+from collections import Counter
+
+HERE = Path(__file__).resolve().parent
+ORACLE_SHA256 = "f842f0e07ca40a181782a565a381b0ee20c6a4b08b8c2b8a4d5d630381bd1e8e"
+
+
+def need(ok, message):
+    if not ok:
+        raise ValueError(message)
+
+
+def load(name, path):
+    spec = importlib.util.spec_from_file_location(name, path)
+    module = importlib.util.module_from_spec(spec)
+    sys.modules[name] = module
+    spec.loader.exec_module(module)
+    return module
+
+
+raw = (HERE / "inputs/finite_dag_audit.py").read_bytes()
+need(hashlib.sha256(raw).hexdigest() == ORACLE_SHA256, "predecessor source hash")
+C = load("pascal_codec", HERE / "codec.py")
+O = load("pascal_predecessor_oracle", HERE / "inputs/finite_dag_audit.py")
+
+
+class AmbientOracleRule(O.Rule):
+    @property
+    def dimension(self):
+        return self._ambient
+
+
+def compare(rule, n):
+    oracle_rule = AmbientOracleRule(rule.roles, rule.rounds, rule.owned)
+    object.__setattr__(oracle_rule, "_ambient", rule.ambient)
+    tree = O.IntegerTree(oracle_rule, n)
+    codec = C.FlowCodec(rule, n)
+    need(codec.height == tree.depth, "height")
+    ordinal = Counter()
+    names, translated = {}, {}
+    for unit in tree.units:
+        key = (unit["path"], unit["point"])
+        names[unit["uid"]] = C.Unit(*key, ordinal[key])
+        ordinal[key] += 1
+    for source in tree.sources:
+        unit = names[source["unit"]]
+        translated[source["field"]] = ("flow", 0, "source", unit.path,
+                unit.point, unit.ordinal, source["role"])
+    for unit in tree.units:
+        u = names[unit["uid"]]
+        for name, field in unit["owned"].items():
+            translated[field] = ("flow", 0, "owned", u.path, u.point, u.ordinal, name)
+    roles, inverse, exits = 0, 0, 0
+    for unit in tree.units:
+        u = names[unit["uid"]]
+        for role, field in unit["fields"].items():
+            need(codec.owner(u, role) == translated[field], "literal physical owner")
+            parent = codec.parent(u, role)
+            if parent is not None:
+                decoded = C.decode(rule, parent.point, parent.ordinal)
+                need(decoded == (u.point, u.ordinal, role), "Pascal inverse")
+                r = rule.rounds[u.path[-1]][0]
+                k = dict(rule.roles)[role]
+                left = r * codec.dilation(parent.path) * C.column(rule, parent.point)
+                right = k * codec.dilation(u.path) * C.column(rule, u.point)
+                need(left == right, "whole-job rank equality")
+                inverse += 1
+            roles += 1
+    for path, ids in tree.classes:
+        expected = [names[uid] for uid in ids]
+        need(list(codec.iter_units(path)) == expected, "complete ordered class stream")
+        fields = [codec.owner(u, role) for u in expected for role, _ in rule.roles]
+        need(len(fields) == len(set(fields)), "simultaneous source/owner alias")
+    for group in tree.exits:
+        for job in group:
+            u = names[job["uid"]]
+            need(codec.paid_owner(u, job["round"]) == translated[job["field"]],
+                 "literal exit owner")
+            exits += 1
+    return {"units": len(tree.units), "roles": roles, "matched": inverse,
+            "sources": len(tree.sources), "exits": exits, "classes": len(tree.classes)}
+
+
+def rejection(action, label):
+    try:
+        action()
+    except (ValueError, AssertionError):
+        return label
+    raise ValueError("negative control accepted: " + label)
+
+
+def distinct(ids):
+    need(len(ids) == len(set(ids)), "duplicate occurrence identity")
+
+
+def controls():
+    r = C.Rule((("a", 2), ("b", 2), ("c", 3)), ((1, "b"), (1, "bank")))
+    checks = [rejection(lambda: C.Rule((("a", 0),), ((1, "a"),)), "zero target rank"),
+              rejection(lambda: C.Rule((("a", 2),), ((0, "a"),)), "zero paid rank"),
+              rejection(lambda: C.Rule((("a", 2),), ((2, "a"),)), "nonseparated rank"),
+              rejection(lambda: C.Rule((("a", 2), ("a", 3)), ((1, "a"),)),
+                        "duplicate productive label"),
+              rejection(lambda: C.encode(r, (2, 0), 0, "c"), "missing Pascal letter"),
+              rejection(lambda: C.decode(r, (1, 1), 4), "out-of-range occurrence")]
+    correct = C.encode(r, (1, 1), 0, "c")
+    wrong = 0  # omit the lower-type interval offset
+    checks.append(rejection(lambda: need(C.decode(r, (1, 1), wrong) ==
+                  C.decode(r, (1, 1), correct), "wrong offset"), "wrong offset"))
+    f = C.FlowCodec(r, 12)
+    u = next(f.iter_units(()))
+    ids = [f.owner(u, x) for x, _ in r.roles]
+    checks.append(rejection(lambda: distinct([ids[0], ids[0], ids[2]]),
+                            "duplicated occurrence"))
+    checks.append(rejection(lambda: C.FlowCodec(r, 11).validate_unit(
+                    C.Unit((), (2, 0), 0)), "absent cap-boundary unit"))
+    edge = C.FlowCodec(r, 12)
+    edge.validate_unit(C.Unit((), (2, 0), 0))
+    checks.append(rejection(lambda: need(edge.owner(u, "a", replica=0) ==
+                  edge.owner(u, "a", replica=1), "replica identity"), "dropped replica"))
+    return checks
+
+
+def main():
+    totals, cases, ambient_cases = Counter(), 0, 0
+    for ranks in ((2, 3), (2, 4), (3, 4), (4, 6)):
+        for duplicate in (False, True):
+            roles = (("a", ranks[0]), ("c", ranks[1]))
+            if duplicate:
+                roles = (roles[0], ("b", ranks[0]), roles[1])
+            for owned_call in (False, True):
+                rounds = ((1, "a"), (min(ranks)-1, "bank" if owned_call else "c"))
+                for extra in (0, 1):
+                    rule = C.Rule(roles, rounds, ambient=max(ranks)+extra)
+                    m, k = rule.ambient, min(ranks)
+                    for n in sorted(set((m, m*k-1, m*k, m*k*k-1, m*k*k,
+                                         m*k*k*k, m*k*k*k+1))):
+                        totals.update(compare(rule, n))
+                        cases += 1
+                        ambient_cases += bool(extra)
+    # Three target types and native role orders that do not group equal ranks.
+    roles = (("z", 5), ("a", 2), ("b", 3), ("c", 2), ("d", 5))
+    for ordering in (roles, tuple(reversed(roles)), roles[2:]+roles[:2]):
+        rule = C.Rule(ordering, ((1, "c"), (1, "bank"), (1, "a")), ambient=7)
+        for n in (7, 14, 27, 28, 55, 56):
+            totals.update(compare(rule, n))
+            cases += 1
+            ambient_cases += 1
+    # A 128-level descriptor addresses 2^128 root occurrences without enumeration.
+    rule = C.Rule((("a", 2), ("b", 2)), ((1, "b"),))
+    flow = C.FlowCodec(rule, 2**129)
+    owner = flow.owner(C.Unit((0,)*128, (0,), 0), "b")
+    need(owner == ("flow", 0, "source", (), (128,), 2**128-1, "b"),
+         "long ancestry exact binary address")
+    result = {"status": "PASS_PASCAL_OCCURRENCE_CODEC", "cases": cases,
+              "ambient_exceeds_target_cases": ambient_cases,
+              "totals": dict(sorted(totals.items())), "negative_controls": controls(),
+              "long_ancestry_depth": 128, "unmaterialized_root_occurrences": "2^128",
+              "oracle_sha256": ORACLE_SHA256, "scope": "logical identity, no tape tariff or kappa"}
+    print(json.dumps(result, indent=2, sort_keys=True))
+
+
+if __name__ == "__main__":
+    main()