diff --git a/research/native-lazy-tensor-boundary/PROOF.md b/research/native-lazy-tensor-boundary/PROOF.md
new file mode 100644
index 0000000000..e31582a469
--- /dev/null
+++ b/research/native-lazy-tensor-boundary/PROOF.md
@@ -0,0 +1,163 @@
+# Uniform lazy tensor routing at the actual lender333 boundary
+
+JoyboyBrian, with substantial OpenAI Codex assistance. Apache-2.0.
+
+## Source contract and quantified statement
+
+The frozen predecessor PROOF and BOUNDARY are inputs, not newly certified native
+recipes. They identify PR3945 `warps[4]=(1081,333,G,U,E)`, the three consumers
+B1081/1082/1083 with signs -,-,+, and the next lender333 transition at B1097.
+Its signed affine monomial M has translation458 and global phase i^3. The next
+native transition is L C0 R. The predecessor establishes these literal local
+interfaces and absence of intervening observations of333. We retain that premise.
+
+For every integer f>=1 let N=512^f, and tensor **each individual operator**.
+On arbitrary independent complex arrays v,d1,d2,d3, the required boundary is
+
+    d_j -> d_j + sign_j M_f v;
+    v -> L_f (C0)^tensor f R_f M_f v.
+
+Set F=RM. The lazy schedule computes the three destination updates directly at
+M's permuted addresses, leaves v unmaterialized, then applies F_f, the unchanged
+paid child and L_f. Functoriality `(RM)^tensor f=R_f M_f` proves equality at every
+width. This is not tensorization of a sum. The translation is applied separately
+to every column; phases add modulo4, so the global i^3 becomes i^(3f).
+
+All four array outputs agree before the common suffix. Therefore an identical
+deterministic rounded suffix would also agree, but this does not establish that
+suffix's accuracy or cost. Earlier consumers of destination arrays see exactly
+the same values. The source owner's no-intervening-observation premise is vital.
+
+## Uniform address algorithm without an N-entry table
+
+Decode each fixed base monomial into p(x),q(x) on512 symbols. Exact cycle census
+gives orders d_M=12,d_R=24,d_F=28,d_L=252. A tensor permutation applies p separately
+to the f base512 digits. Its order divides d for every f, even with mixed digit
+cycle lengths. Phases do not alter the permutation order and are never discarded.
+
+For a monomial of order d, retain d fixed tables
+
+    table_k[a] = (p^k(a), q(p^k(a))), 0<=k<d.
+
+These contain512d pairs, independent of f. For a packed address x, maintain d
+packed addresses p_f^k(x) and d phase sums sum_j q(p^k(x_j)) modulo4. Initialize
+at x=0 in df digit steps. When digit j changes a->b, replace its contribution
+using `(p^k(a) XOR p^k(b)) << 9j` and update the phase by subtracting the old and
+adding the new table phase. Both shifts are explicit ABI operations. Every
+address fits9f bits; table indices and shift counts fit an additional fixed
+constant number of such words. No multiplication or unbounded array operation
+is an instruction.
+
+At x, scan all d addresses for their minimum. If x is that minimum, its orbit
+appears exactly once. Find its length ell by the first return to x, then rotate
+its source values in place: hold the old value at x, load the next old value
+before overwrite, store the appropriately rotated held pair, and advance. The
+phase attached to each original position is already in the maintained lane.
+Fixed coordinates with nonzero phase must still execute. Fixed phase-zero
+coordinates may be skipped only for a plain monomial, never when their consumers
+need that value. This implementation uses two complex held values, destination
+working pairs and sign selection; eight owned real scratch words suffice as in
+the predecessor. No full clean array and no borrowed dirty array is assumed.
+
+The lazy consumer scan uses one lane `(p(a),q(a))`, without a leader search.
+Packed addresses/phase registers and the f-digit odometer are control workspace,
+not productive data. They are initialized and cleared. At most252 packed address
+and252 phase registers, f digit words and constant loop words suffice when the
+common L pass is included. The fixed tables use at most252*512 pairs per pass,
+plus retained base tables. These metadata are owned and retained for the word,
+then cleared or retained under an explicitly persistent owner contract. They
+are not free storage. A word needs9f+O(1) address bits and the independent scalar
+precision width; ordinary bounded RAM permits both within a fixed number of
+words when f and precision are O(log n). No fixed-tape translation is asserted.
+
+## Complete bounded routing invoice and comparison
+
+Let U_f=sum_{j=0}^{f-1} floor((N-1)/512^j). Exactly U_f odometer digits change in
+one full scan; U_f<512N/511. Each lane-digit replacement uses two fixed-table
+pair reads, one digit XOR, one shift, one packed XOR, two phase add/subtractions
+and one mask. Initializing a lane uses f table/shift/phase steps. These are
+specified bounded-word primitives, not a unit-cost whole-array permutation.
+
+The strong materialized comparator combines M with its three consumers, sharing
+source loads and prepared signs, then applies R. The lazy word scans consumers
+using M and applies F. The common child and L suffix are identical and retain
+all their actual costs; they are not removed from the complete invoice.
+
+| Noncommon category | Materialized | Lazy |
+|---|---:|---:|
+| orbit/consumer lanes |12+24=36|1+28=29|
+| initial lane-digit steps |36f|29f|
+| lane-digit replacements |36U_f|29U_f|
+| leader comparisons |(11+23)N=34N|27N|
+| source real reads |4N|4N|
+| source real writes |4N|2N|
+| consumer real reads and writes |6N each|6N each|
+| consumer ADD and prepared NEG |6N and2N|6N and2N|
+| second pass phase NEG |N|N|
+
+M,R,F have no base fixed coordinates, hence none at any positive tensor width.
+R and F each have128 entries of every phase. Convolution of their phase counts
+is uniform at every width; quarter-turns need0,1,2,1 real negations, whose mean
+is1. Thus their second-pass NEG counts both equal N. Consumer signs are prepared
+once and shared with M's materialization in the strong comparator. The comparison
+does not claim avoidable read or negation savings.
+
+Loop and orbit discovery are also charged. Both schedules have two full scans,
+2U_f digit carries,2N iterations, and2N visited source/consumer positions. Their
+per-cycle length searches cost at most N comparisons per monomial; the exact
+count is N minus the number of full-order cycles. The baseline's two searches
+cost at least(2-1/12-1/24)N, while the lazy search costs at most N. Thus no unpaid
+extra length-search penalty hides in the lazy bound. Cycle-start/exit work is
+bounded by a fixed number of instructions per processed coordinate. No data-
+dependent branching or lookup on caller values is used. Resetting owned control
+registers is linear in lane count plus f and does not reverse the inequality
+when both comparators reserve the same maximum-sized workspace.
+
+Preparation is not zero: all base recipe decoding, cycle census, orbit tables,
+F composition, allocation, initialization and final clearing must be paid. F
+composition takes1024 base table reads,512 writes and512 mod4 additions. The
+noncommon expanded table totals are36*512 versus29*512 pairs. We do **not** infer
+net machine time from these categories. A conservative complete ordinary-RAM
+invoice is
+
+    setup K + c_route U_f + c_leader N + c_data N
+      + identical_paid_child(f,precision) + identical_L(f,precision),
+
+with the displayed exact route/data coefficients and all register/loop costs
+included by their stated per-coordinate bounds. K is a fixed constructively
+finite setup bill for the chosen literal implementation and tariff, independent
+of f. A crossover may be stated only after this actual K and primitive tariffs
+are fixed. This paper proves a uniform traffic saving2N and reduced principal
+routing work, not a measured total-time speedup, optimal tariff, or native-cost
+admission. The O(N) address theorem closes the predecessor's exponential-table
+risk without silently giving preparation or control a zero price.
+
+## Scalar magnitude and remaining interface
+
+Before the common child, all monomials preserve complex coordinate magnitude;
+if incoming magnitudes are <=B, destinations are <=2B. Sign selection and ADD
+require the corresponding guard capacity. The unchanged tensor child has exact
+infinity norm2^(f/2); after it the source is at most2^(f/2)B. Its internal rounding,
+word growth and accelerated recursive execution are separate contracts. Our
+algorithm touches neither recursive rank nor owner width. Native allocation,
+whole supplier compilation, fixed tapes, precision recovery and the selected
+frontier are not established by this RAM construction.
+
+## Verification and scope
+
+The proof above supplies the all-f quantifier. The independent out-of-place
+oracle checks all four dense actual arrays at f=1 and distinguishes wrong global
+phase, translation and reversed composition. Small permutations with mixed cycle
+lengths/fixed phases exhaust addresses through four tensor factors; exact lane
+counts are checked against the formula. Eight actual f=2 columns cross digit
+carries and verify source composition. Full actual f=2 arrays, common native
+child/supplier replays, formal kernels and machine timing are not claimed.
+
+## Executable-reference versus RAM tariff
+
+Python is a semantic and route-counter reference, not an instruction-for-instruction
+implementation of the scalar tariff. In particular `rotate` eagerly constructs
+phase alternatives in Python, while the stated RAM schedule selects/reuses the
+required signed operands. The exact NEG categories are for that declared schedule,
+not measured Python unary operations or CPU instructions. Only explicitly
+instrumented route/store counts are reported as executable counters.
diff --git a/research/native-lazy-tensor-boundary/README.md b/research/native-lazy-tensor-boundary/README.md
new file mode 100644
index 0000000000..b4bf8f5703
--- /dev/null
+++ b/research/native-lazy-tensor-boundary/README.md
@@ -0,0 +1,49 @@
+# Uniform lazy signed-affine routing for lender333
+
+The actual finite boundary in `staged544-paid-native-fusion` has a uniform
+all-width realization with O(N) bounded-word address work and no N-entry routing
+table, where N=512^f. It preserves all four arbitrary caller arrays and saves
+exactly2N real writes against the strong materialized comparator. Its principal
+routing counts also fall from36 to29 odometer lanes and34N to27N leader
+comparisons. No recursive child, owner-width or κ improvement is claimed.
+
+[PROOF.md](PROOF.md) gives the quantified algorithm, exact traffic/route categories,
+owned metadata, setup and clearing obligations, and remaining tariff boundary.
+Setup is fixed but nonzero; no total-time crossover is asserted without fixing
+its actual primitive tariffs. The common native child and L suffix remain paid.
+
+```
+python3 -I -W error -B research/native-lazy-tensor-boundary/verify.py
+python3 -I -W error -O -B research/native-lazy-tensor-boundary/verify.py
+python3 -B scripts/research_package.py --package research/native-lazy-tensor-boundary
+```
+
+The verifier authenticates the retained exact source boundary/proof, reconstructs
+all512 base mappings, checks the actual dirty four-array boundary, uses a separate
+out-of-place oracle, exercises tensor cycles and phases on small exhaustive
+fixtures, and rejects altered phases/translation/composition. RESULT is regenerated
+and compared. Finite probes support the uniform proof; they do not prove it by
+extrapolation. Runtime code uses standard-library Python as executable evidence,
+not cycle-accurate RAM timing. The source f=1 native certificate is a retained
+premise rather than freshly repeated here.
+
+Source base32890bc5de034ab8fc93ac88ead7279a6a416d04, priority7; selected5413 remains
+unchanged. [Discussion5474](https://github.com/CrocSwap/integer-mult-bounds/discussions/5474)
+is the canonical investigation. Full open-PR and Discussion overlap was coordinated
+by root before assignment; this is the explicit all-f handoff of the predecessor,
+not a new phase-tag normalization or native recipe census.
+
+## Open next questions
+
+- Fix the ordinary RAM primitive tariff and execute the complete setup/runtime
+  instruction trace to determine its crossover against a stronger downstream
+  fused comparator. The categories here do not determine actual machine time.
+- Bind the lazy ownership representation into one current complete native caller,
+  with its precision, fixed-tape and clearing obligations. The historical PR3945
+  cut alone does not imply admission into selected5413.
+
+Prepared by JoyboyBrian with substantial OpenAI Codex assistance; Apache-2.0.
+Credit Chris R/Clear1nsight for the actual paid-native-fusion boundary and fair
+comparator, ToikY PR4002 for phase tags, Chris R PR3987 for signed recipes,
+Dugongue PR3945 for native words, and all source-native/compiler lineage retained
+in source/PROOF.md. New uniform routing proof and controls are this contribution.
diff --git a/research/native-lazy-tensor-boundary/RESULT.json b/research/native-lazy-tensor-boundary/RESULT.json
new file mode 100644
index 0000000000..c29da8147f
--- /dev/null
+++ b/research/native-lazy-tensor-boundary/RESULT.json
@@ -0,0 +1,123 @@
+{
+  "status": "PASS_NATIVE_LAZY_TENSOR_BOUNDARY",
+  "orders": [
+    12,
+    24,
+    28,
+    252
+  ],
+  "small_tensor_columns": 710,
+  "controls": 6,
+  "actual_dense_width": 1,
+  "actual_width2_columns": 8,
+  "invoice": [
+    {
+      "width": 1,
+      "N": 512,
+      "digit_increments_per_scan": 511,
+      "materialized_route_lanes": 36,
+      "lazy_route_lanes": 29,
+      "materialized_initial_lane_digits": 36,
+      "lazy_initial_lane_digits": 29,
+      "materialized_lane_digit_updates": 18396,
+      "lazy_lane_digit_updates": 14819,
+      "materialized_leader_comparisons": 17408,
+      "lazy_leader_comparisons": 13824,
+      "materialized_source_real_reads": 2048,
+      "lazy_source_real_reads": 2048,
+      "materialized_source_real_writes": 2048,
+      "lazy_source_real_writes": 1024,
+      "common_consumer_real_reads": 3072,
+      "common_consumer_real_writes": 3072,
+      "common_consumer_adds": 3072,
+      "common_consumer_negations": 1024,
+      "common_second_pass_negations": 512,
+      "setup_orbit_table_entries_materialized": 18432,
+      "setup_orbit_table_entries_lazy": 14848,
+      "extra_composition_table_reads": 1024,
+      "extra_composition_table_writes": 512,
+      "extra_composition_phase_adds": 512
+    },
+    {
+      "width": 2,
+      "N": 262144,
+      "digit_increments_per_scan": 262654,
+      "materialized_route_lanes": 36,
+      "lazy_route_lanes": 29,
+      "materialized_initial_lane_digits": 72,
+      "lazy_initial_lane_digits": 58,
+      "materialized_lane_digit_updates": 9455544,
+      "lazy_lane_digit_updates": 7616966,
+      "materialized_leader_comparisons": 8912896,
+      "lazy_leader_comparisons": 7077888,
+      "materialized_source_real_reads": 1048576,
+      "lazy_source_real_reads": 1048576,
+      "materialized_source_real_writes": 1048576,
+      "lazy_source_real_writes": 524288,
+      "common_consumer_real_reads": 1572864,
+      "common_consumer_real_writes": 1572864,
+      "common_consumer_adds": 1572864,
+      "common_consumer_negations": 524288,
+      "common_second_pass_negations": 262144,
+      "setup_orbit_table_entries_materialized": 18432,
+      "setup_orbit_table_entries_lazy": 14848,
+      "extra_composition_table_reads": 1024,
+      "extra_composition_table_writes": 512,
+      "extra_composition_phase_adds": 512
+    },
+    {
+      "width": 3,
+      "N": 134217728,
+      "digit_increments_per_scan": 134480381,
+      "materialized_route_lanes": 36,
+      "lazy_route_lanes": 29,
+      "materialized_initial_lane_digits": 108,
+      "lazy_initial_lane_digits": 87,
+      "materialized_lane_digit_updates": 4841293716,
+      "lazy_lane_digit_updates": 3899931049,
+      "materialized_leader_comparisons": 4563402752,
+      "lazy_leader_comparisons": 3623878656,
+      "materialized_source_real_reads": 536870912,
+      "lazy_source_real_reads": 536870912,
+      "materialized_source_real_writes": 536870912,
+      "lazy_source_real_writes": 268435456,
+      "common_consumer_real_reads": 805306368,
+      "common_consumer_real_writes": 805306368,
+      "common_consumer_adds": 805306368,
+      "common_consumer_negations": 268435456,
+      "common_second_pass_negations": 134217728,
+      "setup_orbit_table_entries_materialized": 18432,
+      "setup_orbit_table_entries_lazy": 14848,
+      "extra_composition_table_reads": 1024,
+      "extra_composition_table_writes": 512,
+      "extra_composition_phase_adds": 512
+    },
+    {
+      "width": 16,
+      "N": 22300745198530623141535718272648361505980416,
+      "digit_increments_per_scan": 22344386578566886591910543553025364170375664,
+      "materialized_route_lanes": 36,
+      "lazy_route_lanes": 29,
+      "materialized_initial_lane_digits": 576,
+      "lazy_initial_lane_digits": 464,
+      "materialized_lane_digit_updates": 804397916828407917308779567908913110133523904,
+      "lazy_lane_digit_updates": 647987210778439711165405763037735560940894256,
+      "materialized_leader_comparisons": 758225336750041186812214421270044291203334144,
+      "lazy_leader_comparisons": 602120120360326824821464393361505760661471232,
+      "materialized_source_real_reads": 89202980794122492566142873090593446023921664,
+      "lazy_source_real_reads": 89202980794122492566142873090593446023921664,
+      "materialized_source_real_writes": 89202980794122492566142873090593446023921664,
+      "lazy_source_real_writes": 44601490397061246283071436545296723011960832,
+      "common_consumer_real_reads": 133804471191183738849214309635890169035882496,
+      "common_consumer_real_writes": 133804471191183738849214309635890169035882496,
+      "common_consumer_adds": 133804471191183738849214309635890169035882496,
+      "common_consumer_negations": 44601490397061246283071436545296723011960832,
+      "common_second_pass_negations": 22300745198530623141535718272648361505980416,
+      "setup_orbit_table_entries_materialized": 18432,
+      "setup_orbit_table_entries_lazy": 14848,
+      "extra_composition_table_reads": 1024,
+      "extra_composition_table_writes": 512,
+      "extra_composition_phase_adds": 512
+    }
+  ]
+}
diff --git a/research/native-lazy-tensor-boundary/SOURCES.json b/research/native-lazy-tensor-boundary/SOURCES.json
new file mode 100644
index 0000000000..0865837b9c
--- /dev/null
+++ b/research/native-lazy-tensor-boundary/SOURCES.json
@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446",
+      "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/staged544-paid-native-fusion/BOUNDARY.json",
+      "usage": "provenance",
+      "git_blob": "f7d80157073847c7b57cb33f1f0cc2454173cc4f",
+      "sha256": "e46236d640768950d24cf26dc5a5650fa79052b19f66245e51a23f0daf0dc5c3"
+    },
+    {
+      "path": "research/staged544-paid-native-fusion/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "e5007f51f5798a13a0873aa8b2ca41fbc42c1d0d",
+      "sha256": "6c3cbb6d49a91c53d3fb3bdeea26967b5439e2dd9cbb662d12b4811bf3730820"
+    }
+  ]
+}
diff --git a/research/native-lazy-tensor-boundary/TASK.json b/research/native-lazy-tensor-boundary/TASK.json
new file mode 100644
index 0000000000..fc2ca78d13
--- /dev/null
+++ b/research/native-lazy-tensor-boundary/TASK.json
@@ -0,0 +1,106 @@
+{
+  "schema_version": 1,
+  "task_id": "independent-moment",
+  "priority_revision": 7,
+  "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04",
+  "original_card": {
+    "id": "independent-moment",
+    "question": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/staged544-mixed-fourth-entry/README.md",
+      "research/staged-fourth-mixture-ceiling/README.md",
+      "research/r437-two-window-carrier/README.md"
+    ],
+    "methods": [
+      "Independently reconstruct one changed paid ledger or pooled dual with exact source and model binding.",
+      "Check a genuinely uncovered moment implication with a different enclosure method and semantic controls."
+    ],
+    "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Choose one uncovered implication in #4088 literal mixed fill, #4091 pooled dual/model binding or #4067 changed frame/host bill. #4091 pins an earlier #4088 head: validate word, capacity and stock equivalence before applying that ceiling to the later fill.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Independently reconstruct one changed ledger or pooled certificate with a positive case and a semantic failure control. Compare exact sources and name what existing checks miss. Keep this separate from supplier-boundary-audit (ordinary/outer dispatch) and uniform-transfer-audit (all-size proof). Stop after the chosen implication; more digits of an unchanged root are not additional mechanism coverage.",
+    "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.",
+    "allowed_variations": [
+      "Reconstruct either a source ledger or a numeric enclosure with a different method."
+    ],
+    "scope_change_triggers": [
+      "Importing the primary function and calling its output independent verification.",
+      "Calling an aggregate histogram or source archive an independently accepted physical supplier."
+    ],
+    "overlap_terms": [
+      "independent moment",
+      "rank histogram",
+      "exact enclosure",
+      "2979",
+      "rank7 joint endframes",
+      "paired extraction",
+      "joint lowering",
+      "4088",
+      "4091",
+      "4067",
+      "staged544-mixed-fourth-entry",
+      "staged-fourth-mixture-ceiling",
+      "r437-two-window-carrier"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.",
+        "evidence": "research/staged544-mixed-fourth-entry/README.md",
+        "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.",
+        "status": "author-checked",
+        "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.",
+        "evidence": "research/staged-fourth-mixture-ceiling/README.md",
+        "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.",
+        "status": "author-checked",
+        "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.",
+        "evidence": "research/r437-two-window-carrier/README.md",
+        "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.",
+        "status": "author-checked",
+        "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Uniform tensor implementation and complete scoped route/traffic ledger for actual lazy lender333 boundary.",
+  "scope_change_reason": "Explicit released all-f implementation handoff after the finite source boundary; this is not another moment computation.",
+  "bottleneck_link": "Removes exponential metadata risk at a real native boundary and exposes remaining tariff/admission obligations.",
+  "budget_minutes": 60,
+  "stop_rule": "One actual all-f routing theorem and bounded source checks; no supplier expansion or kappa claim.",
+  "outcome": "completed",
+  "evidence": "PROOF.md; independently regenerated RESULT.json; actual dense width1, small exhaustive tensor cycles and actual width2 columns.",
+  "author": "JoyboyBrian",
+  "ai_assistance": "Substantial OpenAI Codex assistance in proof, implementation and checks; no independent human or proof-kernel review.",
+  "open_questions": [
+    {
+      "question": "What is the priced full setup/runtime crossover?",
+      "why_it_matters": "Write savings alone do not establish machine-time gain.",
+      "first_step": "Fix primitive RAM tariffs and count the literal preparation and all loops.",
+      "blocked_by": "No native tariff or timing implementation is fixed."
+    },
+    {
+      "question": "Can the lazy state be installed in a current complete native caller?",
+      "why_it_matters": "Historical local equality does not imply selected supplier admission.",
+      "first_step": "Bind one current owner transition and its rounded suffix.",
+      "blocked_by": "Current owner/native/precision/tape contracts are not instantiated."
+    }
+  ]
+}
diff --git a/research/native-lazy-tensor-boundary/VALIDATION.md b/research/native-lazy-tensor-boundary/VALIDATION.md
new file mode 100644
index 0000000000..328edbbd7f
--- /dev/null
+++ b/research/native-lazy-tensor-boundary/VALIDATION.md
@@ -0,0 +1,19 @@
+# Validation scope
+
+Canonical base32890bc5de034ab8fc93ac88ead7279a6a416d04; Darwin, standard-library
+Python3.12 registered replay. The registered normal and optimized scientific
+checks and optimized Git-free subprocess mutation controls passed. Each mutation
+changes an actual copied file: authenticated source bytes, the scientific receipt,
+and the implementation's central phase/rounding rule. Positive replay precedes
+mutations. No network or Git executable is available in these copied-package runs.
+Source-history and committed-byte preflight plus official export/cold replay are
+reported in the publication handoff after the final commit, separately from this
+working-science evidence. Transport hashes do not authenticate mathematical truth.
+
+The initial generic python3 registered command was rejected because this host's
+python3 is3.14 and the manifest requires3.12; the corrected python3.12 command
+passed. Direct scientific execution also passed on3.14 before registration.
+No Lean, Docker, hosted CI, selected-frontier or unrelated historical suite ran.
+
+A separate OpenAI Codex peer reviewed the mathematical/implementation interface.
+This is additional AI review, not independent human or formal-kernel acceptance.
diff --git a/research/native-lazy-tensor-boundary/VERIFY.json b/research/native-lazy-tensor-boundary/VERIFY.json
new file mode 100644
index 0000000000..6783299b73
--- /dev/null
+++ b/research/native-lazy-tensor-boundary/VERIFY.json
@@ -0,0 +1,46 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Source-bound uniform tensor-routing controls, dirty endpoint, exact cost categories and rejected phase/translation mutations."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Source-bound uniform tensor-routing controls, dirty endpoint, exact cost categories and rejected phase/translation mutations."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/test_package.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Optimized Git-free positive replay, then actual damaged source, receipt and scientific code rejection controls."
+    }
+  ]
+}
diff --git a/research/native-lazy-tensor-boundary/routing.py b/research/native-lazy-tensor-boundary/routing.py
new file mode 100644
index 0000000000..470df1b6e1
--- /dev/null
+++ b/research/native-lazy-tensor-boundary/routing.py
@@ -0,0 +1,126 @@
+"""Uniform tensor routing. JoyboyBrian, OpenAI Codex assistance; Apache-2.0."""
+from math import lcm
+
+
+def need(ok, why):
+    if not ok: raise ValueError(why)
+
+
+def decode(rec):
+    rows, q, a = rec['matrix_rows'], rec['quadratic_rows'], rec['linear_Z4']
+    n=len(rows); out=[]; phases=[]
+    for x in range(1<<n):
+        out.append(rec['offset'] ^ sum(((x&r).bit_count()%2)<<i for i,r in enumerate(rows)))
+        phases.append((rec['phase']+sum(a[i] for i in range(n) if x>>i&1)+
+            2*sum((q[i]>>j)&1 for i in range(n) for j in range(i+1,n) if x>>i&1 and x>>j&1))%4)
+    need(sorted(out)==list(range(1<<n)), 'source bijection')
+    return tuple(out),tuple(phases)
+
+
+def compose(a,b):
+    p,q=a; r,s=b
+    return tuple(p[x] for x in r),tuple((s[i]+q[r[i]])%4 for i in range(len(r)))
+
+
+def order(p):
+    seen=set(); lengths=[]
+    for x in range(len(p)):
+        if x in seen: continue
+        y=x; length=0
+        while y not in seen: seen.add(y); y=p[y]; length+=1
+        need(y==x,'permutation orbit'); lengths.append(length)
+    return lcm(*lengths)
+
+
+def tables(m):
+    p,q=m; cur=list(range(len(p))); out=[]
+    for k in range(order(p)):
+        out.append(tuple((x,q[x]) for x in cur))
+        cur=[p[x] for x in cur]
+    return out
+
+
+def odometer(lanes,f,bits,bill):
+    """Yield packed lane values and phase sums; working lists reused after yield."""
+    need(type(f) is int and f>=1 and bits>=1,'positive width')
+    base=1<<bits; mask=base-1; N=1<<(bits*f); d=len(lanes)
+    need(d>0 and all(len(t)==base for t in lanes),'table dimensions')
+    digits=[0]*f; positions=[0]*d; phases=[0]*d
+    for k,t in enumerate(lanes):
+        for j in range(f):
+            positions[k] |= t[0][0]<<(bits*j); phases[k]=(phases[k]+t[0][1])&3
+            bill['initial_lane_digits']=bill.get('initial_lane_digits',0)+1
+    for x in range(N):
+        yield x,positions,phases
+        if x==N-1: break
+        j=0
+        while True:
+            old=digits[j]; new=(old+1)&mask; digits[j]=new
+            for k,t in enumerate(lanes):
+                u,a=t[old]; v,b=t[new]
+                positions[k] ^= (u^v)<<(bits*j)
+                phases[k]=(phases[k]-a+b)&3
+                bill['lane_digit_updates']=bill.get('lane_digit_updates',0)+1
+            bill['digit_increments']=bill.get('digit_increments',0)+1
+            if new: break
+            j+=1
+
+
+def rotate(z,q):
+    a,b=z
+    return ((a,b),(-b,a),(-a,-b),(b,-a))[q]
+
+
+def cycle_apply(v,m,f,bits,bill,targets=None):
+    lanes=tables(m); d=len(lanes)
+    for x,pos,phase in odometer(lanes,f,bits,bill):
+        bill['leader_comparisons']=bill.get('leader_comparisons',0)+d-1
+        if min(pos)!=x: continue
+        length=next((j for j in range(1,d) if pos[j]==x),d)
+        if targets is None and length==1 and phase[0]==0: continue
+        saved=v[x]
+        for k in range(length):
+            y=pos[(k+1)%length]; following=v[y] if k+1<length else None
+            z=rotate(saved,phase[k]); v[y]=z
+            bill['complex_stores']=bill.get('complex_stores',0)+1
+            if targets is not None:
+                for target,sign in zip(targets,(-1,-1,1)):
+                    a,b=target[y]; target[y]=(a+sign*z[0],b+sign*z[1])
+            saved=following
+
+
+def consumers(v,targets,m,f,bits,bill):
+    lane=[tuple(zip(*m))]
+    for x,pos,phase in odometer(lane,f,bits,bill):
+        y=pos[0]; z=rotate(v[x],phase[0])
+        for target,sign in zip(targets,(-1,-1,1)):
+            a,b=target[y]; target[y]=(a+sign*z[0],b+sign*z[1])
+
+
+def boundary(arrays,M,R,f,bits,lazy):
+    v,*targets=[list(x) for x in arrays]; bill={}
+    if lazy:
+        consumers(v,targets,M,f,bits,bill)
+        cycle_apply(v,compose(R,M),f,bits,bill)
+    else:
+        cycle_apply(v,M,f,bits,bill,targets)
+        cycle_apply(v,R,f,bits,bill)
+    return [v,*targets],bill
+
+
+def invoice(f):
+    need(type(f) is int and f>=1,'positive width')
+    N=512**f; U=sum((N-1)//512**j for j in range(f))
+    return dict(width=f,N=N,digit_increments_per_scan=U,
+        materialized_route_lanes=36,lazy_route_lanes=29,
+        materialized_initial_lane_digits=36*f,lazy_initial_lane_digits=29*f,
+        materialized_lane_digit_updates=36*U,lazy_lane_digit_updates=29*U,
+        materialized_leader_comparisons=34*N,lazy_leader_comparisons=27*N,
+        materialized_source_real_reads=4*N,lazy_source_real_reads=4*N,
+        materialized_source_real_writes=4*N,lazy_source_real_writes=2*N,
+        common_consumer_real_reads=6*N,common_consumer_real_writes=6*N,
+        common_consumer_adds=6*N,common_consumer_negations=2*N,
+        common_second_pass_negations=N,
+        setup_orbit_table_entries_materialized=36*512,setup_orbit_table_entries_lazy=29*512,
+        extra_composition_table_reads=1024,extra_composition_table_writes=512,
+        extra_composition_phase_adds=512)
diff --git a/research/native-lazy-tensor-boundary/source/BOUNDARY.json b/research/native-lazy-tensor-boundary/source/BOUNDARY.json
new file mode 100644
index 0000000000..f7d8015707
--- /dev/null
+++ b/research/native-lazy-tensor-boundary/source/BOUNDARY.json
@@ -0,0 +1,158 @@
+{
+  "warp_index_zero_based": 4,
+  "register": 333,
+  "pre_b_index": 1081,
+  "consumers": [
+    1081,
+    1082,
+    1083
+  ],
+  "next_b_index": 1097,
+  "entrance": [
+    266,
+    138,
+    74,
+    30,
+    1
+  ],
+  "exit": [
+    426,
+    96,
+    24,
+    6,
+    1
+  ],
+  "next_frame": [
+    392,
+    66,
+    34,
+    24,
+    6,
+    1
+  ],
+  "G_columns": [
+    1,
+    2,
+    8,
+    32,
+    44,
+    128,
+    59,
+    66,
+    489
+  ],
+  "warp": {
+    "matrix_rows": [
+      1,
+      67,
+      16,
+      468,
+      65,
+      217,
+      128,
+      417,
+      385
+    ],
+    "offset": 458,
+    "quadratic_rows": [
+      251,
+      65,
+      464,
+      209,
+      269,
+      385,
+      335,
+      301,
+      244
+    ],
+    "linear_Z4": [
+      1,
+      2,
+      2,
+      0,
+      2,
+      2,
+      3,
+      2,
+      2
+    ],
+    "phase": 3
+  },
+  "child": {
+    "rank": 1,
+    "left": {
+      "matrix_rows": [
+        2,
+        4,
+        8,
+        17,
+        32,
+        65,
+        129,
+        257,
+        1
+      ],
+      "offset": 0,
+      "quadratic_rows": [
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "linear_Z4": [
+        2,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0,
+        0
+      ],
+      "phase": 0
+    },
+    "right": {
+      "matrix_rows": [
+        424,
+        1,
+        34,
+        4,
+        264,
+        16,
+        256,
+        320,
+        384
+      ],
+      "offset": 133,
+      "quadratic_rows": [
+        0,
+        32,
+        0,
+        168,
+        0,
+        170,
+        0,
+        168,
+        0
+      ],
+      "linear_Z4": [
+        0,
+        2,
+        0,
+        3,
+        0,
+        3,
+        0,
+        3,
+        2
+      ],
+      "phase": 3
+    }
+  }
+}
diff --git a/research/native-lazy-tensor-boundary/source/PROOF.md b/research/native-lazy-tensor-boundary/source/PROOF.md
new file mode 100644
index 0000000000..e5007f51f5
--- /dev/null
+++ b/research/native-lazy-tensor-boundary/source/PROOF.md
@@ -0,0 +1,54 @@
+# A paid finite interface: one avoided materialization
+
+This is a finite `f=1` construction, not a native supplier admission or a lower bound on all implementations. At the actual fifth PR3945 native event, retaining an unmaterialized lender through its three immediate consumers and composing its next right monomial saves **1024 caller-real writes** against a stronger materialized implementation that already shares source loads and phase negations. Reads, negations, additions and exact halves are equal. Address/control cost, cycle preparation and the native tariff remain unresolved. A weaker, stage-separated implementation is reported only for comparison.
+
+## Literal boundary and exact operators
+
+Both pinned providers have `warps[4]=(1081,333,G,U,E)`. Immediately afterward, B1081/B1082/B1083 add lender333 to registers656/657/658 with coefficients −1,−1,+1 in frame E. No intervening scalar or native event touches333 before B1097, whose incoming lender frame V has rank6. We replace only these immediate output updates and the lender's pending frame transition; intervening instructions receive exactly the same destination values, and the lender cannot be observed until its next transition.
+
+Let M=T_E K_G T_U†. The retained PR3987 signed recipe gives a monomial with affine translation458 and global phase i³, not a homogeneous permutation. Let A=T_V T_E†=L C₀ R, with the exact rank-one child. BOUNDARY.json contains all matrix rows, offsets, quadratic phase coefficients and global phases. The sparse credited evaluator independently checks both identities on all512 input columns. The new dense evaluator uses full signed512-entry tables, including translations and global phases; it does not import the lowering compiler.
+
+For input arrays v,d₁,d₂,d₃, the materialized circuit returns
+
+- d₁−Mv, d₂−Mv, d₃+Mv;
+- source L C₀ R Mv.
+
+The lazy circuit updates each destination at p_M(x) with i^q_M(x)v[x], and then applies the signed composition F=R∘M followed by C₀ and L. The four outputs therefore coincide. The verifier checks all2048 complex basis columns (all four arrays), not only the source column. All three implementations are complex-linear, so these columns establish equality for arbitrary complex caller contents. Two additional dense nonzero dirty-input challenges verify inverse return of all four arrays. Inverse integer ×4 alignment merely compares common-denominator representations; inverse operation counts are not used in the forward bill.
+
+## PR4002 phase compensation, on these actual frames
+
+Write D|x⟩=i^wt(x)|x⟩ and J_B=D P_B D†. The source kernel is K_B=J_B Z_t, with
+`t_j=(q_B(2^j)−wt(B2^j)+1)/2 mod2`.
+The verifier checks the full512-point identity, rather than guessing a phase-free matrix. For a canonical frame with r coordinate factors,
+
+T_U=J_B (Z_t C_[r] Z_t) J_B†.
+
+A flipped axis satisfies Z C_j Z=i C_j†. Consequently the adjointed factors require their central global i. The actual completed bases give tags7,14,31 for U,E,V, flipped axes [0,1,2], [1,2,3], [0,1,2,3,4], and global powers3,3,1. All512 columns of each compensated actual frame are checked. Dropping central compensation or its global phase is rejected. The PR4002 K-only composition law is not extrapolated to affine M: F is composed from the full signed tables directly.
+
+## Strong materialized comparator
+
+A fair comparator can combine materializing M with its consumers. During each permutation cycle, save the original source pair, preserve the following original pair, prepare both negatives once, and select the M-store and consumer operands from those four signed components. This shares the extra source load and phase negations that a stage-separated implementation wastes. `materialized_consumers()` implements precisely that comparator. It then applies R,C₀,L.
+
+The lazy implementation's sole caller-data advantage over this comparator is deletion of M's512 complex stores. All actual M,R,F coordinates are active; L has511 active coordinates. The final counts are in RESULT.json. This is not a globally optimal compiler claim: further downstream fusion could change both implementations. It is an exact comparison of three declared loop schedules at one genuine source boundary.
+
+## Scalar and storage microcontract
+
+A caller-real read/write accesses one real component. ADD performs a real sum; NEG a sign change; HALVE denotes an exact dyadic division. A phase quarter-turn uses swaps via operand selection plus the explicitly counted negations. The consumer kernel prepares −a,−b once per original source pair for both implementations. The child computes four sums/differences then four output combinations:8ADD,4NEG,4HALVE per pair. Dyadic values are exact; no rounding is modeled. If all caller components initially have absolute value at most B, consumer outputs are bounded by2B, and child integer numerators by4B. This needs two guard bits and one fractional bit; word size is a declared finite contract, not a general-f precision proof.
+
+Eight private real words are a constructive schedule upper bound, **not measured Python storage**. The witness harness `scratch_schedule.py` checks the following overwrite plans and explicit zero return from arbitrary private initial data:
+
+- Cycles with materialized consumers: slots0–1 saved,2–3 following,4–5 negatives,6–7 current destination. The signed routing selects aliases of slots0,1,4,5; update slots6–7, store, and reuse them for the next destination. Preserve slots2–3 until the cycle advances.
+- Lazy consumers need only saved, negatives, destination (six words); monomial cycles fit within the same eight-word allocation.
+- Child: slots0–3 hold a,b,c,d; slots4–7 receive a+c,b+d,a−c,b−d; overwrite0–3 with the four output numerators; store those slots with the exact half interpretation.
+
+The whole forward program reserves eight private words, clears them at entry and return (16 CLEAR operations), and reuses them throughout. It does not borrow or restore an extra dirty caller array. Python's lists are proof representations, not a claim about interpreter memory. Caller arrays are genuinely arbitrary and their prescribed transformed outputs, not their original contents, are preserved by the forward circuit; the inverse returns their inputs.
+
+## Routing setup is not free
+
+Each implementation retains three signed tables of512 entries×(9 destination bits+2 phase bits)=16896 bits. The lazy consumers still need M's full tags; they cannot erase them. The lazy set is M,F,L; materialized is M,R,L. Cycle-leader storage is792 versus252 bits; runtime leader reads are88 versus28. Each runtime reads1536 routing entries. These are explicit metadata categories, not a conversion to real arithmetic cost.
+
+Constructing F adds1024 table-entry reads,512 writes and512 mod4 additions; its temporary table is5632 bits. Cycle decomposition additionally visits512 points and uses512 visited bits plus leader records. The certificate lists this preparation separately and does not price its control/address arithmetic, allocation, cache behavior or hardware latency. The runtime write saving is therefore **not a net total physical-cost or amortization claim**. A native tariff with these terms, a general-f lift, and a fresh whole-supplier replay remain required before any asymptotic inference. Recursive child count and owner width remain unchanged.
+
+## Rejection and independence boundaries
+
+Eight semantic controls reject omitted affine translation, all phases, global i³, the adjoint warp, reversed R/M composition, missing central frame compensation, missing compensated global i and a changed source-bound recipe. Checks use explicit exceptions and also run with Python optimization enabled. The independent sparse evaluator was authored in PR3987 with substantial OpenAI assistance and is retained byte-for-byte; the lowering compiler is used only by optional generate.py. The new dense implementation is a different evaluator, not a fresh human review or proof-kernel certificate. Frozen native author receipts are not promoted to a full fresh supplier replay.
diff --git a/research/native-lazy-tensor-boundary/source/pins.json b/research/native-lazy-tensor-boundary/source/pins.json
new file mode 100644
index 0000000000..7e53a9bc90
--- /dev/null
+++ b/research/native-lazy-tensor-boundary/source/pins.json
@@ -0,0 +1,4 @@
+{
+  "BOUNDARY.json": "e46236d640768950d24cf26dc5a5650fa79052b19f66245e51a23f0daf0dc5c3",
+  "PROOF.md": "6c3cbb6d49a91c53d3fb3bdeea26967b5439e2dd9cbb662d12b4811bf3730820"
+}
diff --git a/research/native-lazy-tensor-boundary/test_package.py b/research/native-lazy-tensor-boundary/test_package.py
new file mode 100644
index 0000000000..568c8e54b3
--- /dev/null
+++ b/research/native-lazy-tensor-boundary/test_package.py
@@ -0,0 +1,21 @@
+"""Optimized Git-free replay and actual on-disk rejection controls."""
+import json,os,shutil,subprocess,sys,tempfile
+from pathlib import Path
+P=Path(__file__).resolve().parent
+
+def run(p,accept):
+    env=dict(os.environ,PATH='',PYTHONDONTWRITEBYTECODE='1')
+    out=subprocess.run([sys.executable,'-I','-O','-B',str(p/'verify.py')],cwd=p.parent,env=env,capture_output=True,text=True,timeout=30)
+    if (out.returncode==0)!=accept:raise ValueError(out.stdout+out.stderr)
+
+def main():
+    with tempfile.TemporaryDirectory() as temp:
+        q=Path(temp)/'package';shutil.copytree(P,q,ignore=shutil.ignore_patterns('__pycache__'))
+        run(q,True)
+        path=q/'source'/'BOUNDARY.json';raw=path.read_bytes();path.write_bytes(raw+b'\n');run(q,False);path.write_bytes(raw)
+        path=q/'RESULT.json';raw=path.read_bytes();record=json.loads(raw);record['status']=False;path.write_text(json.dumps(record));run(q,False);path.write_bytes(raw)
+        path=q/'routing.py';raw=path.read_text()
+        if raw.count('phases[k]=(phases[k]-a+b)&3')!=1:raise ValueError('science mutation anchor')
+        path.write_text(raw.replace('phases[k]=(phases[k]-a+b)&3','phases[k]=(phases[k]+a+b)&3'));run(q,False)
+    print('PASS_PACKAGE_GITFREE_MUTATIONS controls=3 optimized_git_free=true')
+if __name__=='__main__':main()
diff --git a/research/native-lazy-tensor-boundary/verify.py b/research/native-lazy-tensor-boundary/verify.py
new file mode 100644
index 0000000000..2a3c3e1ce8
--- /dev/null
+++ b/research/native-lazy-tensor-boundary/verify.py
@@ -0,0 +1,86 @@
+"""Independent finite controls for the written uniform proof; no predecessor imports."""
+import hashlib,json,sys
+from pathlib import Path
+P=Path(__file__).resolve().parent
+sys.path.insert(0,str(P))
+import routing as r
+
+
+def direct(m,x,f,bits):
+    p,q=m; y=phase=0
+    for j in range(f):
+        a=(x>>(bits*j))&((1<<bits)-1)
+        y |= p[a]<<(bits*j); phase+=q[a]
+    return y,phase%4
+
+
+def oracle(v,m,f,bits):
+    out=[None]*len(v)
+    for x,z in enumerate(v):
+        y,q=direct(m,x,f,bits); out[y]=r.rotate(z,q)
+    return out
+
+
+def check_lanes(m,f,bits):
+    lanes=r.tables(m); bill={}; count=0
+    for x,pos,ph in r.odometer(lanes,f,bits,bill):
+        a=x
+        for k in range(len(lanes)):
+            _,q=direct(m,a,f,bits)
+            r.need(pos[k]==a and ph[k]==q,'odometer versus independent tensor routing')
+            a,_=direct(m,a,f,bits)
+        count+=1
+    N=1<<(bits*f); U=sum((N-1)//(1<<bits)**j for j in range(f))
+    r.need(bill['lane_digit_updates']==len(lanes)*U,'exact odometer bill')
+    return count
+
+
+def verify():
+    pins=json.loads((P/'source/pins.json').read_text())
+    for name,h in pins.items(): r.need(hashlib.sha256((P/'source'/name).read_bytes()).hexdigest()==h,'source hash '+name)
+    b=json.loads((P/'source/BOUNDARY.json').read_text())
+    r.need((b['register'],b['pre_b_index'],b['next_b_index'])==(333,1081,1097),'actual lender boundary')
+    M=r.decode(b['warp']); R=r.decode(b['child']['right']); L=r.decode(b['child']['left']); F=r.compose(R,M)
+    r.need([r.order(m[0]) for m in (M,R,F,L)]==[12,24,28,252],'base orders')
+    for m in (M,R,F): r.need(all(x!=y for x,y in enumerate(m[0])),'no fixed coordinates')
+    for m in (R,F): r.need([m[1].count(j) for j in range(4)]==[128]*4,'uniform phase distribution')
+    arrays=[[(17*x-3*k,5*x+11*k) for x in range(512)] for k in range(4)]
+    strong,bs=r.boundary(arrays,M,R,1,9,False); lazy,bl=r.boundary(arrays,M,R,1,9,True)
+    r.need(strong==lazy,'four arbitrary dirty arrays before common suffix')
+    mv=oracle(arrays[0],M,1,9); rv=oracle(mv,R,1,9)
+    want=[rv]+[[(a+sg*c,b+sg*d) for (a,b),(c,d) in zip(t,mv)] for t,sg in zip(arrays[1:],(-1,-1,1))]
+    r.need(strong==want,'separate out-of-place oracle')
+    r.need(bs['complex_stores']-bl['complex_stores']==512,'source store delta')
+    for bill,lanes,comparisons in ((bs,36,34),(bl,29,27)):
+        r.need(bill['lane_digit_updates']==lanes*511 and bill['leader_comparisons']==comparisons*512,'actual counted routing invoice')
+    # Small alphabets exercise tensor cycles, nontrivial fixed phases and mixed periods.
+    fixtures=[((1,0),(0,3)),((1,2,3,0),(0,1,2,3)),((0,2,1,3),(2,0,3,1))]
+    columns=0
+    for m in fixtures:
+        bits=(len(m[0])-1).bit_length()
+        for f in range(1,5):
+            columns+=check_lanes(m,f,bits)
+            data=[(i+7,3-i) for i in range(len(m[0])**f)]; got=list(data)
+            r.cycle_apply(got,m,f,bits,{})
+            r.need(got==oracle(data,m,f,bits),'tensor cycle exactness')
+    # Real width-two columns include carries and affine/global phases; no full array allocated.
+    for x in [0,1,511,512,513,65535,131072,262143]:
+        y,a=direct(M,x,2,9); z,c=direct(R,y,2,9)
+        r.need(direct(F,x,2,9)==(z,(a+c)%4),'actual width-two composition')
+    controls=0
+    for wrong in [(M[0],tuple((q-3)%4 for q in M[1])),(tuple(y^458 for y in M[0]),M[1])]:
+        r.need(oracle(arrays[0],wrong,1,9)!=mv,'phase/translation mutation'); controls+=1
+    r.need(r.compose(M,R)!=F,'reversed composition mutation');controls+=1
+    for bad in (0,-1,True):
+        try:r.invoice(bad)
+        except ValueError:controls+=1
+        else:raise ValueError('invalid width accepted')
+    for f in range(1,33):
+        z=r.invoice(f);r.need(z['materialized_source_real_writes']-z['lazy_source_real_writes']==2*z['N'],'uniform invoice')
+    return dict(status='PASS_NATIVE_LAZY_TENSOR_BOUNDARY',orders=[12,24,28,252],small_tensor_columns=columns,controls=controls,actual_dense_width=1,actual_width2_columns=8,invoice=[r.invoice(f) for f in (1,2,3,16)])
+
+if __name__=='__main__':
+    result=verify()
+    if '--write' in sys.argv: (P/'RESULT.json').write_text(json.dumps(result,indent=2)+'\n')
+    else:r.need(json.dumps(result,sort_keys=True)==json.dumps(json.loads((P/'RESULT.json').read_text()),sort_keys=True),'receipt mismatch')
+    print(result['status'])