diff --git a/research/current-serial-pass-lower-bound/CHECKPOINT.json b/research/current-serial-pass-lower-bound/CHECKPOINT.json
new file mode 100644
index 0000000000..1585a8fedb
--- /dev/null
+++ b/research/current-serial-pass-lower-bound/CHECKPOINT.json
@@ -0,0 +1,14 @@
+{
+  "base": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "branch": "research/current-serial-pass-lower-bound-20261109",
+  "wave": 9,
+  "track": "10/50/75",
+  "status": "verified proof and registered controls; lead literal-source review found no blocker",
+  "next": "Committed-byte/export checks and lead publication decision; no new speculative work.",
+  "blocked_global": "No full supplier producer admission or global d/V mapping; bounded leaf wrappers not contradicted.",
+  "sources": [
+    "2ec95e06c2a16e73f9da9a8fe41912710135daaf",
+    "e573186e695f85cb5dbb32ee13ba20ca3159d62a",
+    "a61652557fa88cd0b24c1b28445cf519f6b1213e"
+  ]
+}
diff --git a/research/current-serial-pass-lower-bound/DEPENDENCIES.json b/research/current-serial-pass-lower-bound/DEPENDENCIES.json
new file mode 100644
index 0000000000..d012270880
--- /dev/null
+++ b/research/current-serial-pass-lower-bound/DEPENDENCIES.json
@@ -0,0 +1,106 @@
+{
+  "schema_version": 1,
+  "files": [
+    {
+      "path": "source/column_view.py",
+      "repository": "CubeJerry/integer-mult-bounds",
+      "commit": "2ec95e06c2a16e73f9da9a8fe41912710135daaf",
+      "original_path": "research/current-serial-monomial-leaf/column_view.py",
+      "sha256": "fb19f59af7c8ef8f502c99cc4837d55a4e35f42b6334a3589cb37795b7627117",
+      "git_blob": "f547ed7a72d89fdfd23f6c54a9983b522e16076d",
+      "bytes": 6733
+    },
+    {
+      "path": "source/serial-proof.md",
+      "repository": "CubeJerry/integer-mult-bounds",
+      "commit": "2ec95e06c2a16e73f9da9a8fe41912710135daaf",
+      "original_path": "research/current-serial-monomial-leaf/PROOF.md",
+      "sha256": "9d9887da91617030174d1c7eb5e76492ac05974c78bb06e77412e5a6e34463a0",
+      "git_blob": "f6097b18553ede9b6ec3d4168cac79448d82eb4b",
+      "bytes": 9185
+    },
+    {
+      "path": "source/phase_adapter.py",
+      "repository": "CubeJerry/integer-mult-bounds",
+      "commit": "2ec95e06c2a16e73f9da9a8fe41912710135daaf",
+      "original_path": "research/current-serial-monomial-leaf/vendor/monomial/phase_adapter.py",
+      "sha256": "42687d9cd5f8f4a964e2ddd79aa404432ff26f9ebb55e9c069bbba30f0c3044f",
+      "git_blob": "02f0fdc3ba178f13c27c97c36260107d2c0bba82",
+      "bytes": 9463
+    },
+    {
+      "path": "source/machine.py",
+      "repository": "CubeJerry/integer-mult-bounds",
+      "commit": "2ec95e06c2a16e73f9da9a8fe41912710135daaf",
+      "original_path": "research/current-serial-monomial-leaf/vendor/monomial/vendor/binding/vendor/lifecycle/machine.py",
+      "sha256": "ec597bce13275003ff30e4be481c936401826c1d4af642b55eec0c410774d1df",
+      "git_blob": "acf475e4fccaff2fb64bd5b0b3f3fc0d246dc592",
+      "bytes": 14932
+    },
+    {
+      "path": "source/header_provider.py",
+      "repository": "CubeJerry/integer-mult-bounds",
+      "commit": "2ec95e06c2a16e73f9da9a8fe41912710135daaf",
+      "original_path": "research/current-serial-monomial-leaf/vendor/monomial/vendor/binding/provider.py",
+      "sha256": "3b7bb4f7940ffa9fafd34d25bbb1a9225e1b671924ed194ad012cb26251d7460",
+      "git_blob": "481013b988e5ae8189a0dddfcbb2f521e3142cab",
+      "bytes": 10325
+    },
+    {
+      "path": "source/selected_service.py",
+      "repository": "CubeJerry/integer-mult-bounds",
+      "commit": "2ec95e06c2a16e73f9da9a8fe41912710135daaf",
+      "original_path": "research/current-serial-monomial-leaf/vendor/monomial/selected_service.py",
+      "sha256": "afd4ba2ae8f833e8a47456a8c2dc502fb3e12158601aba999b0d0994085bf4b0",
+      "git_blob": "fc3cbdc16be69eeab39e887e1d3a33ea21a80cb7",
+      "bytes": 3608
+    },
+    {
+      "path": "source/clifford_exact.py",
+      "repository": "CubeJerry/integer-mult-bounds",
+      "commit": "2ec95e06c2a16e73f9da9a8fe41912710135daaf",
+      "original_path": "research/current-serial-monomial-leaf/vendor/monomial/vendor/selected/clifford_exact.py",
+      "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962",
+      "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2",
+      "bytes": 6824
+    },
+    {
+      "path": "source/WORD.json.gz",
+      "repository": "CubeJerry/integer-mult-bounds",
+      "commit": "2ec95e06c2a16e73f9da9a8fe41912710135daaf",
+      "original_path": "research/current-serial-monomial-leaf/vendor/monomial/vendor/selected/WORD.json.gz",
+      "sha256": "7834725d9e34ee846a9ccc615221ea81e0201613938afa185d2eda0c9a6c232f",
+      "git_blob": "22f9ab02d1b73ea0aa4b07ce445a14cc2602c760",
+      "bytes": 119880
+    },
+    {
+      "path": "source/phase-proof.md",
+      "repository": "CubeJerry/integer-mult-bounds",
+      "commit": "2ec95e06c2a16e73f9da9a8fe41912710135daaf",
+      "original_path": "research/current-serial-monomial-leaf/vendor/monomial/PROOF.md",
+      "sha256": "5bd00e9764cb628cbd92a113419c2cd79c77ba81b1e15b04519026c26ff3091f",
+      "git_blob": "5bd585e03ce948261ef979b748a1c6df8cbc2fb4",
+      "bytes": 24018
+    },
+    {
+      "path": "source/rounded-move-proof.md",
+      "repository": "CubeJerry/integer-mult-bounds",
+      "commit": "e573186e695f85cb5dbb32ee13ba20ca3159d62a",
+      "original_path": "research/current-rounded-source-move/PROOF.md",
+      "sha256": "d29639a20f57a6a0d16e0c3a7d6634e94ee2ae505ea265ae3be6b9282f2aeab8",
+      "git_blob": "4d6b48527632d9ae8764024684d2af0d1d59eb3e",
+      "bytes": 22332,
+      "usage": "reference cutoff domain"
+    },
+    {
+      "path": "source/direct-move-proof.md",
+      "repository": "CubeJerry/integer-mult-bounds",
+      "commit": "a61652557fa88cd0b24c1b28445cf519f6b1213e",
+      "original_path": "research/current-direct-source-move/PROOF.md",
+      "sha256": "fc53d095a69816c67febf7a613ff6a7d71ac17bec8e76338651c66ce33d20a00",
+      "git_blob": "6ec8326a8ffa9325a3af7385d2375b8f0e29362e",
+      "bytes": 13482,
+      "usage": "reference cutoff domain"
+    }
+  ]
+}
diff --git a/research/current-serial-pass-lower-bound/FINAL-CHECKS.json b/research/current-serial-pass-lower-bound/FINAL-CHECKS.json
new file mode 100644
index 0000000000..20eaf48995
--- /dev/null
+++ b/research/current-serial-pass-lower-bound/FINAL-CHECKS.json
@@ -0,0 +1,30 @@
+{
+  "status": "author-verified; separate lead source/proof review found no blocker; requested metric distinction applied",
+  "metadata": "PASS_PACKAGE_METADATA_AND_PINS",
+  "registered": "PASS_REGISTERED_RESEARCH_PACKAGE",
+  "commands": 2,
+  "modes": [
+    "normal",
+    "optimized"
+  ],
+  "retained_files": 11,
+  "family_members": 516,
+  "negative_controls": 9,
+  "numerical_native_execution": false,
+  "full_supplier_family_proved": false,
+  "fixed_leaf_budget_refuted": false,
+  "python": "3.12.14 (main, Aug 25 2026, 14:00:49) [Clang 22.1.3 ]",
+  "scientific_sha256": {
+    "PROOF.md": "e33d1c8632935ee91ea819254bdd25ab0e6c06dfd478e051865c3ec812916c82",
+    "verify.py": "ce72c8e3ae1185c3fd51140c24abfa6084364c18979ec99da29311d84ddc2c30",
+    "DEPENDENCIES.json": "7ce856d526691d0d62ef9217995b87bae5fbbe1d45e71d17c8e53ce0d3115aa8"
+  },
+  "supplemental_lead_descriptor_regression": {
+    "f": 146,
+    "stored_cutoff": 145,
+    "physical_actions": 8458911,
+    "materialized_private_cells": 7707,
+    "numerical_field_allocated": false,
+    "registered_dependency": false
+  }
+}
diff --git a/research/current-serial-pass-lower-bound/LEAD-REVIEW.md b/research/current-serial-pass-lower-bound/LEAD-REVIEW.md
new file mode 100644
index 0000000000..1e5b80e338
--- /dev/null
+++ b/research/current-serial-pass-lower-bound/LEAD-REVIEW.md
@@ -0,0 +1,32 @@
+# Separate model-assisted lead review
+
+The lead independently read the literal import/export and guide-return
+bodies, all consumed `prepare` guards, and the explicit 23-field family.
+It found no blocking issue in the vector or family. It requested that the
+rate ratio define T as literal unit moves or raw actions, with a separate
+fixed-P conversion for simultaneous multitape steps. PROOF.md section4
+now states this explicitly. Its review is shared-source, model-assisted
+mathematical/code review, not human or proof-kernel verification.
+
+The lead additionally ran the unchanged predecessor `check_descriptor.case`
+on the new family at f=146, stored cutoff145 and rank9. The retained JSON
+receipt is in `review/serial-lower-descriptor-review.json`. All146 real
+encoded ColumnView states completed, using 8,458,911 literal physical
+actions and 7,707 retained materialized private cells; the parent/ancestor
+prefixes and heads were restored and current private bodies erased.
+The input and maximum view each had 3,783 binary bits.
+
+This is supplemental regression of a new boundary case through the real
+predecessor descriptor machinery, not an independent universal proof.
+No numerical field was allocated and no numerical monomial ran. The
+materialized storage number is not a maximum visited-space certificate.
+This external predecessor trace is not a registered replay dependency;
+the package's source proof and local static/primitive controls are complete
+without it. Reproduction requires the public serial package at
+`2ec95e06c2a16e73f9da9a8fe41912710135daaf`, then
+`check_descriptor.case(9, values)` with PROOF.md section3's23 descriptor
+values at f146 (h is the separate numerical width and is not a header key).
+
+Prepared for @CubeJerry with substantial OpenAI assistance. The lead and
+native-physical agent are distinct research-agent executions sharing
+immutable source; no claim of separate human or proof-kernel independence.
diff --git a/research/current-serial-pass-lower-bound/PR-DESCRIPTION.md b/research/current-serial-pass-lower-bound/PR-DESCRIPTION.md
new file mode 100644
index 0000000000..bae848f472
--- /dev/null
+++ b/research/current-serial-pass-lower-bound/PR-DESCRIPTION.md
@@ -0,0 +1,59 @@
+## Why this matters
+
+The completed serial monomial removes ordinary numerical calls on its
+direct route, but retains a repeated full-field invoice. An upper invoice
+alone does not prove a lower rate obstruction. This package identifies
+mandatory literal work and the exact dimension, volume and cutoff
+conditions for a source-specific lower consequence.
+
+## Exact result
+
+Every successful serial invocation incurs on its public field alone at
+least **4fV physical unit moves, (4/3)fV reads and fV writes**. V is the
+complete coded body. Each column unconditionally imports, rewinds,
+exports and rewinds the entire field; all other work adds cost.
+
+For the actual selected #6030 event9896 right monomial, an explicit
+infinite admitted local zero-input family has d=9f, V=(9/2)Vraw and the
+long-record condition. It excludes C V d^epsilon for epsilon<1 for this
+implementation only if the full supplier admits such unbounded f and
+comparable complete-field volume. Fixed-cutoff MOVE leaf wrappers admit
+bounded f and are not contradicted. Literal actions and simultaneous
+multitape steps are separated, with any required fixed conversion explicit.
+
+## Provenance and novelty
+
+Canonical base: `7c49fe32c55de02c2c873655c804b16e4c3fef0a`.
+Serial source: `CubeJerry/integer-mult-bounds@2ec95e06c2a16e73f9da9a8fe41912710135daaf`.
+Current monomial: `7d1ff23714e6f9182c1d0ff9214f65def2f30e04`.
+The serial predecessor proves an implementation and upper invoice; its
+Compact-binding warning expressly excludes an algorithmic lower inference.
+This adds mandatory traversals, an admitted family and the cutoff boundary.
+Eleven retained files authenticate the sources and predecessor domains.
+
+Credit remains with the original work including
+CrocSwap/integer-mult-bounds#3087, CrocSwap/integer-mult-bounds#4172,
+the selected #6030 source and the published current adapters. Prepared
+for @CubeJerry with substantial OpenAI assistance. Separate lead review
+shares sources and is model-assisted, not human or proof-kernel verification.
+
+## Verification
+
+```sh
+python -I -B scripts/research_package.py --package research/current-serial-pass-lower-bound
+```
+
+Both normal and optimized registered gates passed: source authentication,
+actual nontrivial recipe reconstruction, literal traversal structure and
+coded primitive counters, 516 descriptor members, induction premises and
+nine reservation/rewind/volume/cutoff controls. Expected status:
+`PASS_SERIAL_MANDATORY_FIELD_PASSES`. The universal theorem is proved by
+control flow and induction, not finite extrapolation. No numerical
+monomial, whole MOVE or complete caller is run.
+
+## Limits and next obligation
+
+Actual full supplier/exporter admission, d/V mapping, global cost
+conversion and all five foundational assumptions remain separate. Bind
+one exact nonleaf caller domain or construct a different batching route.
+This is not a general monomial or multiplication lower bound. **No new kappa.**
diff --git a/research/current-serial-pass-lower-bound/PROOF.md b/research/current-serial-pass-lower-bound/PROOF.md
new file mode 100644
index 0000000000..d9f82fb9b4
--- /dev/null
+++ b/research/current-serial-pass-lower-bound/PROOF.md
@@ -0,0 +1,217 @@
+# Mandatory complete-field passes in the current serial monomial
+
+Prepared for @CubeJerry with substantial OpenAI assistance. Apache-2.0.
+This is a scoped implementation lower bound. **No new kappa, supplier
+admission, general algorithm lower bound or multiplication lower bound.**
+
+## 1. Claim and exact source
+
+Fix the actual `SerialProvider` at public CubeJerry commit
+`2ec95e06c2a16e73f9da9a8fe41912710135daaf`, with its unchanged current
+monomial adapter and literal `CodedPort` implementation. The retained
+sources and public paths are in `DEPENDENCIES.json`. The canonical base
+is `7c49fe32c55de02c2c873655c804b16e4c3fef0a`.
+
+Let f>0 be the parent column count and V the length in PHYSICAL BITS of
+the complete coded public numerical field, excluding its left marker and
+blank frontier. For any successful admitted serial invocation on the
+unchanged complete format, its public field alone incurs at least
+
+```text
+4 f V        physical unit moves,
+(4/3) f V    physical reads,
+f V          physical writes.
+```
+
+V is a multiple of three. These are simultaneous coordinatewise lower
+bounds obtained by selecting disjoint mandatory instructions. Additional
+work is nonnegative. No operation-time measurement or earlier upper bound
+is used to derive them.
+
+This applies in particular to the fixed, nontrivial, actual selected
+#6030 MOVE event9896 entrance/right monomial, from raw record
+`("MOVE",236,3,7,False)`. Its matrix rank is nine and constant phase is1.
+The selected raw MOVE's positive child rank1 is a DIFFERENT parameter;
+the source right/left monomials each act on nine chart coordinates.
+The verifier regenerates this literal recipe from the exact retained
+selected word and canonical Clifford constructor. This does not port or
+replace the proposed #6936 catalogue.
+
+## 2. Four complete traversals, independently of numerical input
+
+The literal serial loop first prepares its private header iterator, then
+calls `self.native.run(self.field,self.view.context)`, advances the
+iterator and repeats until `finished`. The unchanged PREPARE saves f,
+sets column=0 and emits the first one-column view. NEXT increments the
+encoded column, returns `ready` while column<f and `finished` at equality.
+Thus successful return includes exactly f completed monomial invocations.
+There is no all-zero-field shortcut, caller-dependent batch skip or
+replacement of the native object between columns.
+
+Every one-column adapter call unconditionally executes `import_field`,
+the retained engine, and `export_field`, in that order. Let S=V/3 be the
+number of virtual numeric symbols, including component delimiters.
+`import_field` consumes every signed data bit and both component
+delimiters of every record until the physical field frontier. It calls
+`field.move(1)` once per symbol and appends one guide marker per symbol.
+Its `rewind_field` consumes all S guide markers and calls `field.move(-1)`
+once per marker. This is a full advance followed by a full return.
+
+On successful exact-format return, `export_field` writes and advances
+over every returned data bit and every original delimiter. It checks the
+same complete frontier, then invokes `rewind_field` on the same S guide
+markers before clearing the guide. This is another full advance and
+return. The source geometry/tensor map preserves the number and width
+of records; success explicitly checks the matching complete frontier.
+The numerical values, including a zero payload, do not alter these loops.
+
+Each successful ordinary `CodedPort.move` makes one physical read and
+exactly three physical unit moves. A right move from a blank cell may
+materialize additional code, but in these four field traversals every
+step begins on a complete existing body symbol, or is a valid return
+from the frontier. The backward direction also has one read and three
+moves. None crosses the local LEFT marker. Four S-step traversals hence
+give at least 4S reads and 12S moves, namely `(4/3)V` and 4V per column.
+
+Every virtual symbol in the successful export receives one `field.write`,
+including each delimiter. The literal write has three physical writes,
+so this contributes 3S=V physical writes per column. Reads, moves and
+writes internal to `read`/`write`, native codecs, raw bridge copies,
+phase computation, permutations, private header creation, counters,
+engine setup, source construction and retirement are omitted positively.
+Historical backing cannot provide a negative credit. Summing f calls
+proves the three inequalities for arbitrary successful admitted inputs.
+
+This is a statement about the actual fixed implementation, not about
+the mathematical monomial's intrinsic complexity. Identity and zero data
+can have cheaper alternative algorithms; this code still scans them.
+
+## 3. An admitted infinite local descriptor family
+
+The following is a family at the ACTUAL SERIAL MONOMIAL ABI, not a claim
+that a global compiler currently produces it. For each integer f>=128,
+fix the same actual rank-nine right recipe and choose
+
+```text
+outer=rows=stock=1,  h=2,  one complex coefficient per record,
+d=selected_axes=p=D=9f,  remainder=0,
+K=G=1, rho=0, H=f,
+active_start=u=2f, entry_start=2f,
+back_start=z=11f, within_bits=a=12f,
+record_bits=6(h+1)=18, row_bits=18*2^(12f),
+q0=qF=qB=0, cutoff=145.
+```
+
+The 23 descriptor fields use the canonical encoding; h is the public
+component width, not an additional header field. Unused fields are stated
+explicitly; they are not asserted to satisfy unconsumed global producer
+identities. Supply the entire field of `2^(12f)` records, both h-bit signed
+components zero, valid local markers and exact blank frontier. Supply
+the fixed actual provider's full disjoint, blank private inventory; retain
+and price its historical backing as required by the predecessor.
+
+The consumed guards hold:
+`(f-1)G=f-1<=H`, `2H=u`, `u+9fK=z`, `z+H=a`,
+`rho<K`, `9f+remainder=selected_axes<=d`, and `0<=remainder<9`.
+The row equality and `record_bits=6r(h+1)` hold with r=1; h>=2 and
+all required positive quantities are positive. Therefore the exact
+parent monomial geometry is admitted. Its one-column views have
+`f'=1,K'=f,rho'=j,selected_axes'=9` for 0<=j<f and still act at
+`u+if+j`. All19 other fields, complete record extents and spectators
+remain unchanged. The per-call back suffix becomes f bits, accounted
+as additional coefficients; it is not dropped from V.
+
+Every intermediate signed permutation/quarter-phase maps zero to zero.
+Zero is strictly between -2^(h-1) and 2^(h-1), so all signed phase
+guards succeed. No exact-half/grid promise is needed by this monomial.
+The frozen provider's completed format, permutation and lifecycle
+contracts remain inherited premises; the arithmetic family checks do
+not create a new physical simulator proof. No huge field is allocated
+or run in this package.
+
+Here the physical field length is `V=18*2^(12f)` and its delimiter-free
+signed payload length is `Vraw=4*2^(12f)`. Thus `V=(9/2)Vraw`; changing
+between those two COMPLETE-field conventions loses only a fixed factor.
+The native header dimension really is `d=9f`; it is neither the number
+of records `2^a` nor the positive child rank1. No extra f is hidden by
+renaming an already f-multiplied comparison volume.
+
+The family even meets the previous long-record upper simplification:
+its one-column R1=2hr*2^(a-z)=2^(f+2), M1=2^z and
+`A1=2+z+ceil(log2(R1+1))=12f+5`. At f=128,
+`2^(f+2)>=(12f+5)^6`. The ratio on increasing f is
+`2/(1+12/(12f+5))^6>1`: for f>=128, the parenthesized term is at most
+`1+12/1541<129/128`, and `(129/128)^6<2` by exact integer arithmetic.
+This proves the long-record inequality for all f>=128, not just tested
+members. The canonical descriptor length E is O(f): the largest field,
+row_bits, has 12f+5 bits and all other fields have O(log(f+1)) bits.
+Hence `(E+1)^4+Q=O(V)` for the fixed finite inventory Q. The lower bound
+does not rely on these upper absorption conditions, but is not defeated
+by their absence on this example.
+
+## 4. Conditional supplier consequence and cutoff boundary
+
+Here T denotes the literal physical unit-move count, or the raw
+read/write/unit-move action count which dominates it. For this local
+implementation and family, no fixed C and epsilon<1 can satisfy
+`T<=C V d^epsilon` on every f: the mandatory move count gives
+
+```text
+T / (V d^epsilon) >= 4 f / (9f)^epsilon
+                    = 4*9^(-epsilon)*f^(1-epsilon) -> infinity.
+```
+
+Canonical simultaneous multitape steps are a different metric. If a step
+can perform at most P of these physical unit moves, with fixed P, the
+corresponding implication is `T_TM>=4fV/P`, not automatically `4fV`.
+The exact conversion/simulation contract must be supplied; its fixed
+factor does not change the divergent power of f.
+
+The same asymptotic conclusion holds with Vraw or any comparison volume
+uniformly Theta(V), and with any fixed conversion factor between literal
+physical unit moves and the proposed cost metric. If the comparison volume has
+already been multiplied by f, or d is exponentially larger than f, this
+argument does not establish that displayed rate obstruction. Those
+parameter mappings must not be silently changed.
+
+**This does not refute the current direct-leaf wrappers' contract.**
+SerialProvider and its monomial adapter never consume `cutoff`; the
+family stores the fixed value145 without using it. The later protected
+direct/rounded MOVE wrappers separately require parent f<=cutoff (an
+older direct route also required r*f<=cutoff). With a fixed global
+cutoff t, these wrappers only admit bounded f, and their O(fV) work
+can be absorbed in an O_t(V) leaf constant. The above infinite family
+is not thereby an admitted full-MOVE/nonleaf family.
+
+The useful exclusion is precise: reusing THIS serial implementation as
+a full supplier uniformly over a producer-admitted unbounded regime
+f=Theta(d), with comparable complete-field volume, cannot establish a
+sublinear power of d by changing only fixed tariffs or constants.
+Actual producer admission, its volume and dimension identities and the
+global cost conversion remain separate obligations. No global
+assumption, selected exponent or accepted certificate is changed.
+
+## 5. Novelty, evidence and open next questions
+
+The public serial predecessor proves the positive implementation and
+an upper invoice, explicitly retaining repeated setup and O(fV) cost.
+Its cited current Compact binding warning is expressly an upper-bound
+implication limit, not an algorithmic lower bound. This package adds the
+mandatory four-traversal lower theorem, an explicit unbounded admitted
+local family, and the fixed-cutoff limitation. Original monomial work
+including CrocSwap/integer-mult-bounds#3087 and #4172 and the public
+current monomial/serial adapters retain full credit.
+
+The checker authenticates source bytes, regenerates the one actual
+selected recipe, checks the four-traversal call structure and literal
+coded primitive costs, verifies bounded family arithmetic, and rejects
+missing rewind, invalid reservations, false volume and false cutoff
+scope controls. It does not execute a numerical monomial or prove the
+universal theorem by finite sampling. The traversal and induction
+arguments above carry that quantification.
+
+**Open next questions:** bind f,d,V and cutoff to one actual full
+supplier/exporter domain, or devise a different implementation that
+avoids per-column complete-field import/export. A source-bound batching
+construction must still pay its actual phases, routing and cleanup;
+the lower theorem does not rule out such a construction.
diff --git a/research/current-serial-pass-lower-bound/README.md b/research/current-serial-pass-lower-bound/README.md
new file mode 100644
index 0000000000..08ee04df81
--- /dev/null
+++ b/research/current-serial-pass-lower-bound/README.md
@@ -0,0 +1,43 @@
+# Mandatory full-field passes in the current serial monomial
+
+For every successful invocation of the public serial monomial provider,
+the public field alone pays at least **4fV physical unit moves**,
+**(4/3)fV reads** and **fV writes**, where V is its complete coded body.
+The proof follows four unconditional traversals for each of f columns;
+it does not infer a lower bound from the predecessor's upper invoice.
+
+An explicit zero-input family for the actual selected #6030 event9896
+right recipe has d=9f and satisfies all consumed format/geometry/signed
+guards, including the optional long-record condition for f>=128.
+This only excludes a sublinear-in-d full-supplier tariff for this
+implementation **if the actual supplier admits such unbounded f and a
+comparable full-field volume**. Fixed-cutoff direct MOVE wrappers admit
+bounded f and are not contradicted. All global assumptions and the
+accepted multiplication bound remain unchanged. **No new kappa.**
+
+Read [PROOF.md](PROOF.md) for the exact quantifiers, cutoff distinction,
+source pins, full-field conventions and inherited runtime premises.
+
+```sh
+python -I -B research/current-serial-pass-lower-bound/verify.py
+python -I -O -B research/current-serial-pass-lower-bound/verify.py
+```
+
+Expected: `PASS_SERIAL_MANDATORY_FIELD_PASSES`. The check authenticates
+eleven retained files, reconstructs the actual nontrivial recipe and checks
+literal paths, primitive counts, parameter arithmetic and negative
+controls. It does not run a huge field or a numerical whole MOVE.
+
+## Open next questions
+
+The structured question in TASK.json asks whether the actual global
+supplier/exporter admits an unbounded f=Theta(d) family with the same
+complete-field volume. First bind one exact nonleaf occurrence's
+dimension, cutoff and volume; this is blocked by caller/exporter and
+tariff domain obligations. A different batching implementation is not
+excluded by this source-specific theorem.
+
+Prepared for @CubeJerry with substantial OpenAI assistance. The frozen
+serial provider at `2ec95e06c2a16e73f9da9a8fe41912710135daaf`, current
+monomial at `7d1ff23714e6f9182c1d0ff9214f65def2f30e04`, and originating
+CrocSwap/integer-mult-bounds#3087/#4172 retain credit. Apache-2.0.
diff --git a/research/current-serial-pass-lower-bound/SOURCES.json b/research/current-serial-pass-lower-bound/SOURCES.json
new file mode 100644
index 0000000000..75ea7c3d55
--- /dev/null
+++ b/research/current-serial-pass-lower-bound/SOURCES.json
@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    }
+  ]
+}
diff --git a/research/current-serial-pass-lower-bound/TASK.json b/research/current-serial-pass-lower-bound/TASK.json
new file mode 100644
index 0000000000..35862d128c
--- /dev/null
+++ b/research/current-serial-pass-lower-bound/TASK.json
@@ -0,0 +1,87 @@
+{
+  "actual_scope": "Source-specific mandatory full-public-field traversals for the exact serial monomial implementation; admitted infinite local descriptor family and conditional growing-d rate obstruction. Explicit fixed-leaf cutoff limitation.",
+  "ai_assistance": "Substantial OpenAI assistance in proofs, implementation, experiments and documentation; separate AI checks share source context and are not human or proof-kernel admission.",
+  "author": "@CubeJerry",
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "bottleneck_link": "native_all_columns: distinguishes current serial leaf execution from any claimed sublinear-in-d full supplier rate.",
+  "evidence": "Literal serial/codec control-flow proof, source-selected nontrivial recipe, exact family guard arithmetic, static mutation and coded primitive controls; no full native numerical run.",
+  "freshness": {
+    "canonical_main": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+    "serial_public": "2ec95e06c2a16e73f9da9a8fe41912710135daaf",
+    "overlap": "Prior serial proof gives an upper invoice only; prior compiled-binding proof explicitly excludes a lower inference. Lead owns current queue/claims refresh."
+  },
+  "open_questions": [
+    {
+      "question": "Does the actual full supplier/exporter admit an unbounded family with f=Theta(d) and the same full-field volume?",
+      "why_it_matters": "Only that premise turns the local implementation lower bound into a supplier-tariff obstruction. Fixed global leaf cutoffs do not.",
+      "first_step": "Bind the producer dimension, cutoff and volume identities at one actual nonleaf occurrence.",
+      "blocked_by": "Enclosing caller/exporter and global tariff domain, outside this package."
+    }
+  ],
+  "original_card": {
+    "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "existing_checks": [
+      {
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.",
+        "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "status": "author-checked"
+      },
+      {
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "status": "reviewed"
+      }
+    ],
+    "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "id": "uniform-transfer-audit",
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "overlap_terms": [
+      "native_all_columns",
+      "owned_erasure",
+      "compiler",
+      "precision_tape",
+      "analytic_recovery"
+    ],
+    "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?",
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md"
+    ]
+  },
+  "outcome": "completed",
+  "schema_version": 1,
+  "scope_change_reason": "Lead wave9 asks for an actual lower bound, distinct from the prior repeated upper invoice, and the exact condition under which it has supplier-rate consequences.",
+  "scope_status": "refined",
+  "stop_rule": "Complete bounded proof/preflight by22:26UTC; no new numerical full-field execution or broad supplier/global claims.",
+  "task_id": "uniform-transfer-audit",
+  "time_budget_minutes": 15
+}
diff --git a/research/current-serial-pass-lower-bound/VERIFY.json b/research/current-serial-pass-lower-bound/VERIFY.json
new file mode 100644
index 0000000000..346c83a927
--- /dev/null
+++ b/research/current-serial-pass-lower-bound/VERIFY.json
@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "research/current-serial-pass-lower-bound/verify.py"
+      ],
+      "timeout_seconds": 30,
+      "checks": "Exact source pins, selected nontrivial recipe, literal four-traversal structure, ordinary coded move/write costs, descriptor-family guards, long-record inequalities and scope/mutation controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-B",
+        "research/current-serial-pass-lower-bound/verify.py"
+      ],
+      "timeout_seconds": 30,
+      "checks": "Exact source pins, selected nontrivial recipe, literal four-traversal structure, ordinary coded move/write costs, descriptor-family guards, long-record inequalities and scope/mutation controls."
+    }
+  ]
+}
diff --git a/research/current-serial-pass-lower-bound/review/LEAD-REVIEW.md b/research/current-serial-pass-lower-bound/review/LEAD-REVIEW.md
new file mode 100644
index 0000000000..d6aee6b250
--- /dev/null
+++ b/research/current-serial-pass-lower-bound/review/LEAD-REVIEW.md
@@ -0,0 +1,42 @@
+# Separate lead proof review
+
+Verdict: pass after the explicit clock-metric correction. Prepared for
+@CubeJerry with OpenAI assistance; shared immutable sources, no claim of
+human or proof-kernel review.
+
+The lead read the literal phase adapter and checked that each successful
+import and export advances once per complete numerical symbol, records
+exactly one guide marker, and returns once per marker. There are four
+disjoint full traversals. Each coded move contributes exactly three raw
+unit moves and at least one read; each exported symbol contributes three
+writes. The serial iterator completes exactly f calls, so the stated
+coordinatewise bounds follow without using its earlier upper invoice.
+
+The lead separately checked every consumed prepare guard and the complete
+23-field descriptor family, including the distinction between public h
+and encoded fields, all spectators, suffix coefficient folding, and
+V=(9/2)Vraw. Zero lies in the strict signed domain for every phase.
+The long-record base2^130>=1541^6 and ratio(129/128)^6<2 establish the
+unbounded induction; finite arithmetic checks are supplementary.
+
+The root review required two scope distinctions now present in the proof:
+1. Header d and physical V are not automatically global supplier parameters.
+2. Four f V raw moves imply only4fV/P simultaneous multitape steps when
+   at most P fixed heads move per step. Fixed-cutoff whole MOVE families
+   have bounded f and are not refuted by this all-f local counterfamily.
+
+The retained supplemental receipt records an actual encoded ColumnView
+run for f146 with stored cutoff145. All146 views,3783-bit headers, parent
+preservation, ancestors and cleanup passed; no numerical field or monomial
+was run. This reused the predecessor descriptor checker on a new family,
+so it is regression evidence, not an independent universal proof. Reproduce
+with the published2ec95e06 source package's check_descriptor.case(9,v),
+using exactly the f146 instantiation in PROOF section3.
+
+Final scientific hashes reviewed:
+
+- PROOF.md: `e33d1c8632935ee91ea819254bdd25ab0e6c06dfd478e051865c3ec812916c82`
+- verify.py: `ce72c8e3ae1185c3fd51140c24abfa6084364c18979ec99da29311d84ddc2c30`
+- source/phase_adapter.py: `42687d9cd5f8f4a964e2ddd79aa404432ff26f9ebb55e9c069bbba30f0c3044f`
+- source/column_view.py: `fb19f59af7c8ef8f502c99cc4837d55a4e35f42b6334a3589cb37795b7627117`
+- source/machine.py: `ec597bce13275003ff30e4be481c936401826c1d4af642b55eec0c410774d1df`
diff --git a/research/current-serial-pass-lower-bound/review/serial-lower-descriptor-review.json b/research/current-serial-pass-lower-bound/review/serial-lower-descriptor-review.json
new file mode 100644
index 0000000000..2725413d22
--- /dev/null
+++ b/research/current-serial-pass-lower-bound/review/serial-lower-descriptor-review.json
@@ -0,0 +1,18 @@
+{
+  "status": "pass",
+  "method": "actual retained encoded ColumnView on the new f146 descriptor family; separate source traversal/guard proof reviewed",
+  "descriptor": {
+    "rank": 9,
+    "f": 146,
+    "input_bits": 3783,
+    "maximum_view_bits": 3783,
+    "columns": 146,
+    "physical_actions": 8458911,
+    "retained_materialized_cells": 7707
+  },
+  "stored_cutoff": 145,
+  "parent_f": 146,
+  "numerical_field_allocated": false,
+  "numerical_monomial_executed": false,
+  "scope": "Standalone monomial descriptor only; not full MOVE admission or global supplier mapping."
+}
diff --git a/research/current-serial-pass-lower-bound/source/WORD.json.gz b/research/current-serial-pass-lower-bound/source/WORD.json.gz
new file mode 100644
index 0000000000..22f9ab02d1
Binary files /dev/null and b/research/current-serial-pass-lower-bound/source/WORD.json.gz differ
diff --git a/research/current-serial-pass-lower-bound/source/clifford_exact.py b/research/current-serial-pass-lower-bound/source/clifford_exact.py
new file mode 100644
index 0000000000..166841a037
--- /dev/null
+++ b/research/current-serial-pass-lower-bound/source/clifford_exact.py
@@ -0,0 +1,149 @@
+"""Small exact Gaussian-dyadic Clifford compiler, independent of gx internals.
+Paulis use i^p X^x Z^z. State vectors use integer Gaussian numerators / 2^d.
+The tableau is supplemented by a literal circuit, so global phases are kept.
+"""
+from dataclasses import dataclass
+
+def parity(x):return x.bit_count()&1
+def rank(rows):
+ p={}
+ for x in rows:
+  while x:
+   b=x.bit_length()-1
+   if b not in p:p[b]=x;break
+   x^=p[b]
+ return len(p)
+def transpose(rows,n):return tuple(sum(((rows[j]>>i)&1)<<j for j in range(n)) for i in range(n))
+def mv(rows,x):return sum(parity(r&x)<<i for i,r in enumerate(rows))
+def inv(rows,n):
+ a=[r|(1<<(n+i)) for i,r in enumerate(rows)]
+ for j in range(n):
+  k=next(i for i in range(j,n) if a[i]>>j&1);a[j],a[k]=a[k],a[j]
+  for i in range(n):
+   if i!=j and a[i]>>j&1:a[i]^=a[j]
+ assert [r&((1<<n)-1) for r in a]==[1<<i for i in range(n)]
+ return tuple(r>>n for r in a)
+def basis_extend(cols,n):
+ out=[]
+ for x in list(cols)+[1<<i for i in range(n)]:
+  if rank(out+[x])>len(out):out.append(x)
+ assert len(out)==n
+ return tuple(out)
+def nullspace(rows,n):
+ a=list(rows);p=[];k=0
+ for j in range(n):
+  t=next((i for i in range(k,len(a)) if a[i]>>j&1),None)
+  if t is None:continue
+  a[t],a[k]=a[k],a[t]
+  for i in range(len(a)):
+   if i!=k and a[i]>>j&1:a[i]^=a[k]
+  p.append(j);k+=1
+ return tuple((1<<j)|sum(((a[i]>>j)&1)<<v for i,v in enumerate(p)) for j in range(n) if j not in p)
+def pmul(a,b):
+ x,z,p=a;y,w,q=b
+ return x^y,z^w,(p+q+2*parity(z&y))%4
+def identity(n):return tuple([(1<<i,0,0) for i in range(n)]+[(0,1<<i,0) for i in range(n)])
+def apply(T,p):
+ n=len(T)//2;x,z,ph=p;out=(0,0,ph)
+ for i in range(n):
+  if x>>i&1:out=pmul(out,T[i])
+ for i in range(n):
+  if z>>i&1:out=pmul(out,T[n+i])
+ return out
+def compose(A,B):return tuple(apply(A,p) for p in B)
+def inverse(T):
+ n=len(T)//2;cols=[x|(z<<n) for x,z,p in T];rows=transpose(cols,2*n);cols_inv=transpose(inv(rows,2*n),2*n);out=[]
+ for j,w in enumerate(cols_inv):
+  x=w&((1<<n)-1);z=w>>n;u,v,p=apply(T,(x,z,0));assert (u,v)==identity(n)[j][:2];out.append((x,z,(-p)%4))
+ return tuple(out)
+def qvalue(Q,alpha,x,n):
+ return (sum(alpha[i] for i in range(n) if x>>i&1)+2*sum(parity((Q[i]>>(i+1))&(x>>(i+1))) for i in range(n) if x>>i&1))%4
+def mul_i(a,p):
+ x,y=a;p%=4
+ return [(x,y),(-y,x),(-x,-y),(y,-x)][p]
+@dataclass
+class Op:
+ n:int
+ tab:tuple
+ circuit:list
+ def then(self,b):
+  assert self.n==b.n
+  return Op(self.n,compose(b.tab,self.tab),self.circuit+b.circuit)
+ def adjoint(self):
+  circ=[]
+  for e in reversed(self.circuit):
+   if e[0]=='P':circ.append(('P',inv(e[1],self.n)))
+   elif e[0]=='D':circ.append(('D',e[1],tuple((-x)%4 for x in e[2])))
+   elif e[0]=='C':circ.append(('C',e[1],-e[2]))
+   elif e[0]=='phase':circ.append(('phase',(-e[1])%4))
+   else:circ.append(e)
+  return Op(self.n,inverse(self.tab),circ)
+ def zero_state(self,basis=0):
+  N=1<<self.n;vec=[(0,0)]*N;vec[basis]=(1,0);den=0
+  for e in self.circuit:
+   if e[0]=='P':
+    v=[(0,0)]*N
+    for x,a in enumerate(vec):v[mv(e[1],x)]=a
+    vec=v
+   elif e[0]=='X':vec=[vec[x^e[1]] for x in range(N)]
+   elif e[0]=='D':vec=[mul_i(a,qvalue(e[1],e[2],x,self.n)) for x,a in enumerate(vec)]
+   elif e[0]=='phase':vec=[mul_i(a,e[1]) for a in vec]
+   elif e[0]=='C':
+    q,sgn=e[1:];v=[]
+    for x,(a,b) in enumerate(vec):
+     c,d=vec[x^q]
+     # C=(1+i)I/2+(1-i)X/2; inverse conjugates both coefficients.
+     v.append((a-sgn*b+c+sgn*d,b+sgn*a+d-sgn*c))
+    vec=v;den+=1
+   else:raise AssertionError(e)
+   while den and all((a&1)==(b&1)==0 for a,b in vec):vec=[(a//2,b//2) for a,b in vec];den-=1
+  return vec,den
+def ident(n):return Op(n,identity(n),[])
+def perm(n,G):
+ cols=transpose(G,n);gi=inv(G,n)
+ return Op(n,tuple([(a,0,0) for a in cols]+[(0,a,0) for a in gi]),[('P',tuple(G))])
+def diag(n,Q,alpha=None):
+ Q=tuple(Q);assert transpose(Q,n)==Q
+ alpha=tuple(alpha) if alpha is not None else tuple((Q[i]>>i)&1 for i in range(n))
+ assert all(alpha[i]%2==(Q[i]>>i)&1 for i in range(n))
+ return Op(n,tuple([(1<<i,Q[i],alpha[i]) for i in range(n)]+[(0,1<<i,0) for i in range(n)]),[('D',Q,alpha)])
+def cgate(n,q,sgn=1):
+ return Op(n,tuple([(1<<i,0,0) for i in range(n)]+[(q if q>>i&1 else 0,1<<i,(3*sgn)%4 if q>>i&1 else 0) for i in range(n)]),[('C',q,sgn)])
+def xgate(n,b):return Op(n,tuple([(1<<i,0,0) for i in range(n)]+[(0,1<<i,2*((b>>i)&1)) for i in range(n)]),[('X',b)])
+def fourier(n,axes=None):
+ out=ident(n)
+ for i in range(n) if axes is None else axes:out=out.then(cgate(n,1<<i))
+ return out
+def hadamard(n,axes):
+ axes=list(axes);Q=tuple(1<<i if i in axes else 0 for i in range(n));S=diag(n,Q)
+ return S.then(fourier(n,axes)).then(S)
+def canonical_frame(n,U):
+ r=len(U)
+ if r==0:return ident(n)
+ if r==n:return fourier(n)
+ G=transpose(basis_extend(U,n),n);gi=inv(G,n);Q=tuple((1<<i)^sum(parity(gi_i&gi_j)<<j for j,gi_j in enumerate(transpose(gi,n))) for i,gi_i in enumerate(transpose(gi,n)))
+ K=perm(n,G).then(diag(n,Q))
+ return K.adjoint().then(fourier(n,range(r))).then(K)
+def monomial(op):
+ n=op.n;T=op.tab;assert all(x==0 and p%2==0 for x,z,p in T[n:]);G=transpose([x for x,z,p in T[:n]],n);b=mv(G,sum((p//2)<<i for i,(x,z,p) in enumerate(T[n:])))
+ gt=transpose(G,n);cols=[mv(gt,z) for x,z,p in T[:n]];Q=transpose(cols,n);alpha=[(p-2*parity(b&z))%4 for x,z,p in T[:n]]
+ out=diag(n,Q,alpha).then(perm(n,G)).then(xgate(n,b));assert out.tab==T
+ vec,den=op.zero_state();assert den==0 and all(a==(0,0) for i,a in enumerate(vec) if i!=b);phase=[(1,0),(0,1),(-1,0),(0,-1)].index(vec[b]);out=out.then(Op(n,identity(n),[('phase',phase)]));assert out.zero_state()==op.zero_state()
+ return out,dict(matrix_rows=G,offset=b,quadratic_rows=Q,linear_Z4=alpha,phase=phase)
+def lower_child(op):
+ n=op.n;Bcols=[x for x,z,p in op.tab[n:]];r=rank(Bcols)
+ if not r:
+  mon,rec=monomial(op);return dict(rank=0,left=rec,right=None),mon
+ G=transpose(basis_extend(Bcols,n),n);A=inv(G,n);PA=perm(n,A);part=op.then(PA);Bcols=[x for x,z,p in part.tab[n:]];Dcols=[z for x,z,p in part.tab[n:]]
+ picks=[];selected=[]
+ for j,x in enumerate(Bcols):
+  if rank(selected+[x])>len(selected):picks.append(j);selected.append(x)
+ assert len(picks)==r and all(x>>r==0 for x in Bcols)
+ Br=transpose(selected,r);Bi=inv(Br,r);Dr=transpose([Dcols[j]&((1<<r)-1) for j in picks],r)
+ Qsmall=tuple(sum(parity(row&col)<<j for j,col in enumerate(transpose(Bi,r))) for row in Dr);Q=Qsmall+(0,)*(n-r);DQ=diag(n,Q)
+ V=part.then(DQ).then(hadamard(n,range(r)));assert all(x==0 for x,z,p in V.tab[n:]);Vmon,Vrec=monomial(V)
+ S=diag(n,tuple(1<<i if i<r else 0 for i in range(n)))
+ left=S.adjoint().then(DQ.adjoint()).then(PA.adjoint());right=Vmon.then(S.adjoint()).then(xgate(n,(1<<r)-1))
+ lmon,lrec=monomial(left);rmon,rrec=monomial(right);compiled=rmon.then(fourier(n,range(r))).then(lmon)
+ assert compiled.tab==op.tab and compiled.zero_state()==op.zero_state()
+ return dict(rank=r,left=lrec,right=rrec),compiled
diff --git a/research/current-serial-pass-lower-bound/source/column_view.py b/research/current-serial-pass-lower-bound/source/column_view.py
new file mode 100644
index 0000000000..f547ed7a72
--- /dev/null
+++ b/research/current-serial-pass-lower-bound/source/column_view.py
@@ -0,0 +1,200 @@
+"""Physically encoded serialization into genuine one-column monomial calls.
+
+Runtime integers remain on fixed raw binary tapes. Construction depends only
+on the finite recipe rank. Prepared for @CubeJerry with substantial OpenAI
+assistance. Apache-2.0.
+"""
+from serial_sources import activate, need
+
+S = activate()
+R = S.rows
+ROLES = dict(R.SCHEMA)
+PARENT, VIEW = R.HEADER, R.CHILD_HEADER
+FBOUND, OLD_K, COLUMN, ACC, SUM, M = range(40, 46)
+PORTS = 46
+PRIVATE = tuple(i for i in range(PORTS) if i != PARENT)
+FIELDS = tuple(port for _, port in R.SCHEMA)
+
+
+def literal(b, tape, value):
+    """Only a fixed compile-time integer is supplied here."""
+    need(type(value) is int and value >= 0, "fixed nonnegative literal")
+    b.empty(tape)
+    for digit in bin(value)[2:][::-1]:
+        b.write(tape, digit)
+        b.move(tape, 1)
+    b.rewind(tape)
+
+
+def compile_prepare(rank):
+    need(type(rank) is int and 1 <= rank <= 73, "fixed compiled monomial rank")
+    b = R.Builder()
+    for port in (PARENT, *PRIVATE):
+        b.boundary(port)
+    for port in PRIVATE:
+        b.empty(port)
+    b.decode(PARENT, FIELDS)
+    b.canonical(ROLES["f"], positive=True)
+    b.canonical(ROLES["K"], positive=True)
+    b.copy(ROLES["f"], FBOUND)
+    b.copy(ROLES["K"], OLD_K)
+    literal(b, COLUMN, 0)
+    literal(b, ACC, 0)
+    loop, more, end = (b.fresh("product") for _ in range(3))
+    b.mark(loop)
+    b.compare(COLUMN, FBOUND, more, end, "reject")
+    b.mark(more)
+    b.add(ACC, OLD_K, SUM)
+    b.clear(ACC)
+    b.copy(SUM, ACC)
+    b.clear(SUM)
+    b.increment(COLUMN)
+    b.go(loop)
+    b.mark(end)
+    b.clear(ROLES["K"])
+    b.copy(ACC, ROLES["K"])
+    b.clear(ACC)
+    b.clear(ROLES["f"])
+    literal(b, ROLES["f"], 1)
+    b.clear(ROLES["selected_axes"])
+    literal(b, M, rank)
+    b.add(M, ROLES["remainder"], ROLES["selected_axes"])
+    b.clear(M)
+    b.clear(COLUMN)
+    literal(b, COLUMN, 0)
+    b.encode(FIELDS, VIEW)
+    b.code.append(("result", "ready"))
+    return b.close()
+
+
+def compile_next():
+    b = R.Builder()
+    b.clear(VIEW)
+    b.increment(COLUMN)
+    more, end = (b.fresh("column") for _ in range(2))
+    b.compare(COLUMN, FBOUND, more, end, "reject")
+    b.mark(more)
+    b.add(ROLES["rho"], OLD_K, SUM)
+    b.clear(ROLES["rho"])
+    b.copy(SUM, ROLES["rho"])
+    b.clear(SUM)
+    b.encode(FIELDS, VIEW)
+    b.code.append(("result", "ready"))
+    b.mark(end)
+    b.code.append(("result", "finished"))
+    return b.close()
+
+
+def compile_release():
+    b = R.Builder()
+    for port in PRIVATE:
+        b.clear(port)
+    b.rewind(PARENT)
+    return b.close()
+
+
+NEXT, RELEASE = compile_next(), compile_release()
+
+
+def validate(table):
+    for row in table:
+        need(row[0] in ("read", "write", "move", "goto", "done", "result", "reject", "quarantine"),
+             "literal local instruction vocabulary")
+        if row[0] in ("read", "write", "move"):
+            need(type(row[1]) is int and 0 <= row[1] < PORTS, "fixed role")
+        if row[0] == "write":
+            need(row[1] != PARENT and row[2] in (R.ZERO, R.ONE, R.BLANK),
+                 "parent and markers are read-only")
+        if row[0] == "move":
+            need(row[2] in (-1, 1), "unit movement")
+        if row[0] == "result":
+            need(row[1] in ("ready", "finished"), "finite decision alphabet")
+    return len(table)
+
+
+class ColumnView:
+    port_count = len(PRIVATE)
+
+    def __init__(self, rank):
+        self.prepare_table = compile_prepare(rank)
+        for table in (self.prepare_table, NEXT, RELEASE):
+            validate(table)
+        self.ports = self.parent = self.work = None
+        self.active = False
+
+    def bind(self, work, context):
+        need(not self.active and len(work) == self.port_count,
+             "complete fixed descriptor bank before execution")
+        need(len(set(map(id, work))) == len(work)
+             and all(port is not context.tape for port in work),
+             "distinct descriptor segments; actual disjointness is a caller premise")
+        self.parent, self.work = context, tuple(work)
+        self.ports = {PARENT: R.PhysicalPort(context.tape)}
+        self.ports.update((role, R.PhysicalPort(port)) for role, port in zip(PRIVATE, work))
+
+    @property
+    def context(self):
+        need(self.ports is not None, "bound descriptor bank")
+        return S.abi.BinaryContextPort(self.ports[VIEW].tape)
+
+    def prepare(self):
+        need(self.ports is not None and not self.active, "single active descriptor iteration")
+        self.active = True
+        try:
+            result, _steps = R.run_choice(self.prepare_table, self.ports)
+            need(result == "ready", "first column available")
+        except Exception:
+            self.release()
+            raise
+
+    def advance(self):
+        need(self.active, "active descriptor iteration")
+        result, _steps = R.run_choice(NEXT, self.ports)
+        need(result in ("ready", "finished"), "finite column decision")
+        return result
+
+    def release(self):
+        need(self.active, "active descriptor iteration to retire")
+        try:
+            R.run(RELEASE, self.ports)
+        finally:
+            self.active = False
+
+
+class SerialProvider:
+    """Actual unchanged monomial, with physically priced descriptor iteration.
+
+Partial column updates can precede a later named arithmetic rejection. A
+protected whole-field wrapper is required for whole-job public atomicity.
+No provider is reset, recreated, or given decoded shape values between calls.
+"""
+    def __init__(self, literal_recipe, native_factory, inverse=False):
+        self.native = S.adapter.Provider(literal_recipe, native_factory, inverse=inverse)
+        self.view = ColumnView(self.native.rank)
+        self.field = self.work = None
+
+    @property
+    def port_count(self):
+        return self.view.port_count + self.native.port_count
+
+    def bind(self, work, field, context):
+        need(len(work) == self.port_count and len(set(map(id, work))) == len(work),
+             "fixed distinct complete inventory")
+        need(field.tape is not context.tape
+             and all(field.tape is not p and context.tape is not p for p in work),
+             "field, parent descriptor and work are disjoint")
+        self.work, self.field = tuple(work), field
+        self.view.bind(work[:self.view.port_count], context)
+        self.native.bind(work[self.view.port_count:])
+
+    def run(self):
+        need(self.work is not None, "bound serial monomial")
+        try:
+            self.view.prepare()
+            while True:
+                self.native.run(self.field, self.view.context)
+                if self.view.advance() == "finished":
+                    break
+        finally:
+            if self.view.active:
+                self.view.release()
diff --git a/research/current-serial-pass-lower-bound/source/direct-move-proof.md b/research/current-serial-pass-lower-bound/source/direct-move-proof.md
new file mode 100644
index 0000000000..6ec8326a8f
--- /dev/null
+++ b/research/current-serial-pass-lower-bound/source/direct-move-proof.md
@@ -0,0 +1,262 @@
+# Protected selected direct MOVEs without ordinary numerical runtime
+
+Prepared for @CubeJerry with substantial OpenAI assistance. Apache-2.0.
+No new kappa. The five global selected assumptions remain.
+
+## 1. Exact source statement and removed premise
+
+Canonical base: `7c49fe32c55de02c2c873655c804b16e4c3fef0a`.
+Immediate public pins are the source-complete positive child
+`12e58dfdad9371a26f9978c814779da344fd80b4` and the serial monomial
+`2ec95e06c2a16e73f9da9a8fe41912710135daaf`. Their full trees were checked
+against the frozen tested trees before reuse. The protected whole-field
+coordinator and factor sources are retained transitively at their exact
+public pins, including `41b67c290c1533de25bfba19d4dec27e1aaf0970`.
+
+Fix any actual raw MOVE in the selected finite source family: 3453
+occurrences and 2886 distinct directed chart pairs. Its genuine current-local
+events are a right-monomial SERVICE, positive rank-r PAID, and left-monomial
+SERVICE, with 1<=r<=8. The unchanged typed binder checks the entire raw source
+record, owner, rank and chronological triple. Nested remap/product tokens
+are not stripped or substituted. A source MOVE's boolean is a private-owner
+lifetime flag, not a Fourier inverse flag.
+
+On the domain below, `DirectMove` implements this complete raw MOVE using
+the actual right monomial serialized into genuine one-column calls, the
+rank-scaled positive C child, and the actual left monomial serialized in the
+same way. It invokes no ordinary numerical runtime entry. The original
+complete field is protected until all factors return and then committed.
+
+This removes the monomial ordinary **runtime numerical/rate contract** from
+this direct route. It retains finite closed ordinary constructors and all
+their allocated ports, physical permutation/phase/codec primitives, supplied
+source placement, complete costs and source-to-machine premises. No nonleaf
+tariff, global cutoff admission or full compiler/multiplication theorem is
+deduced from this construction.
+
+## 2. Quantified parent geometry and numerical domain
+
+The original canonical current descriptor has positive f,K,G,H,outer,rows,
+0<=rho<K, source monomial rank nine, and remainder e with 0<=e<9. Write
+u=active_start, z=back_start, a=within_bits. Retain
+
+    (f-1)G<=H,  2H<=u,  u+9fK<=z,  z+H<=a,
+    selected_axes=9f+e<=d.
+
+Each complete row has 2^a records, each with c>=1 complex coefficients and
+h>=2 signed bits per real/imaginary component on one common quantum. The
+current format has a delimiter after each component and three physical bits
+per virtual symbol, so
+
+    b=record_bits=6c(h+1),  row_bits=2^a b,
+    C=outer*rows,  V=C*2^a b.
+
+Every original field/header/owned segment is genuinely disjoint with its
+supplied LEFT marker and origin head. The whole protected stage and all
+private bodies begin physically blank; old erased backing stays allocated.
+Object-identity checks do not establish disjointness for arbitrary custom
+physical port objects. These are normalized local source positions, not a
+proof that an enclosing caller produced them.
+
+The actual direct-leaf stopping condition is **r*f<=original cutoff**.
+Cutoff is unchanged by every view. All intermediate serialized signed phases
+must be representable; every actual C-stage Gaussian halving must be exact
+on the common grid, and every C-stage output component must fit the signed
+range. The final answer fitting alone does not establish this domain.
+
+A useful sufficient uniform domain is: every input integer component is
+divisible by 2^(r*f) and has absolute value strictly less than
+2^(h-r*f-1). Each monomial address permutation/quarter rotation preserves
+divisibility and absolute component magnitude. Each positive C stage spends
+one divisibility bit and multiplies the maximum component magnitude by at
+most two. Induction over r*f stages gives exact halves and strict symmetric
+headroom throughout, including every exit column's signed phase. The
+inherited fused arithmetic kernel's intermediate representation is retained.
+
+The exact prefix-admitted domain is larger than this sufficient envelope.
+The nonzero Gaussian-character h=2 finite fixture belongs to that larger
+domain: its actual halves are exact and all components stay in {-1,0,1}.
+It does not satisfy input divisibility by two and is not described as a
+test of the stronger sufficient envelope.
+
+The serial success domain is genuinely narrower than the original batched
+monomial's domain. A cancelling batch phase can accept the most-negative
+signed value while an intermediate serial negation cannot. The serial
+predecessor proves and executes that obstruction. No equality of the two
+acceptance domains is used here.
+
+## 3. Three exact consumer views and complete operator identity
+
+The parent's source positions are
+
+    p_(i,j)=u+(if+j)K+rho,  0<=i<9, 0<=j<f.
+
+Each serial monomial uses its own 45-port physically encoded descriptor
+iterator. At column j it supplies only its actual monomial consumer with
+
+    f'=1, K'=fK, rho'=jK+rho, selected_axes'=9+e,
+
+leaving the other 19 fields unchanged. Then
+u+iK'+rho'=p_(i,j), and 0<=rho'<K'. The compact width becomes zero, the
+before/after intervals stay valid, and folding the entire suffix into extra
+coefficient fields preserves every one of the original V physical bits.
+The view is never passed to an ordinary provider or to the positive child.
+It need not satisfy unused global producer relations.
+
+The actual unchanged monomial engine computes n=f'-1=0 and selects its
+`single_column_rows` branch at every affine gate. That branch and its signed
+phase/format/cleanup work invoke no ordinary runtime call. Both serial
+providers are constructed and bound once, then reused across all f columns;
+no reset, fresh inventory or data-dependent host loop bound is introduced.
+The literal iterator's ready/finished results drive the loop physically.
+
+The middle positive child uses its separate 39-port leaf-only view
+
+    f_child=r*f,
+
+preserving the original cutoff and other 22 values. Its selected axes
+u+kK+rho, 0<=k<r*f, are exactly p_(i,j) for i<r and j<f. This view is not a
+general native descriptor and never reaches either monomial. The positive
+kernel is exactly
+
+    C_1 = 1/2 [[1+i,1-i],[1-i,1+i]].
+
+It applies C_1 on each selected axis and identity on every complete spectator,
+row and coefficient. Parent geometry gives u+r*f*K<=a, and the physical leaf
+checks the actual r*f cutoff.
+
+For each column, the fixed-source certificate proves
+
+    U = M_left (C_1^(tensor r) tensor I_(9-r)) M_right
+
+including absolute phase. Different columns act on disjoint tensor factors,
+so the two serialized monomials and the multi-axis positive child compose
+to U^(tensor f), tensored with identity on every other coordinate and label.
+Each monomial's constant phase occurs once per column; no i^(f*c) is replaced
+by i^c. The public all-source package independently checked all 2886 finite
+chart identities using 18 Pauli conjugations and all 512 entries of one
+normalized separating column. Its commutant lemma fixes the entire matrix.
+We reuse that exact finite certificate, not a new general compiler theorem.
+The arbitrary-f assertion follows from this separate tensor/view argument.
+
+## 4. Whole-field protection and named returned failures
+
+The coordinator first copies all V physical body bits to one blank private
+stage. Entrance, child and exit receive that stage; the public original is
+unchanged. Their numeric adapters preserve the complete coded format, size,
+component quantum and row/spectator order. The parent header is read-only.
+
+On success all three complete factors return, then the unchanged published
+`AtomicMove.commit` copies the complete result to the public field. Finally
+the stage is erased and returned to origin. Each serial descriptor bank,
+native bank and child/view cohort has already been closed and retired.
+
+A serial factor may have completed earlier columns before a later named
+signed rejection. This changes only the private stage. The serial source
+returns its descriptor, all working heads and a valid complete field extent
+at the source boundary. The positive leaf has its corresponding valid
+parity/headroom/cutoff return contract. Therefore a named valid returned
+failure skips commit and retires the complete stage, preserving the original
+public field and parent header. Child-local rollback alone would not establish
+this property; the paid whole-field stage is essential.
+
+This is not a guarantee for physical interruption, malformed streams,
+unexpected corrupt successful output or a provider violating its inherited
+return contract. In particular, the protected copy precedes the try/finally
+just as in its predecessor and requires the stated valid blank-stage domain.
+
+The raw-bit loops have unchanged exact action counts:
+
+    transfer = 8V+14,  commit = 9V+14,  retire = 5V+7.
+
+Thus administrative overhead is 22V+35 on success and 13V+21 on a named
+valid returned failure. Both invoices add every executed provider action,
+descriptor operation, failed scan, return and retirement; no earlier column
+or partially attempted factor becomes free.
+
+## 5. Optimistic and actual complete budgets
+
+Let F_template include fixed source authentication/binding, finite recipe
+compilation and table construction, real closed ordinary constructors, fixed
+bank reservation and template storage. Let P_R,j and P_L,j be the complete
+unchanged one-column monomial costs, including their codec, full-field copies,
+phase/permutation work, encoded controls and cleanup. Let H_R,H_L be the two
+literal descriptor-loop costs, and let T_C be the complete positive-leaf bill.
+The successful composed invoice is
+
+    F_template + H_R+H_L + sum_(j=0)^(f-1)(P_R,j+P_L,j)
+               + T_C(V,h,r*f,E_child) + H_child + 22V+35.
+
+The serial predecessor proves H_R+H_L=O_9(f(E+1)); the positive view has
+E_child<=E+6 and H_child<=1000E+10000. These descriptors are constructed,
+iterated, restored and erased physically. They are not free rebinding of
+host parameters.
+
+For comparison with the explicit inherited one-column ceiling, write
+
+    R1=2hc*2^(a-z),  M1=C*2^z,  Vraw=M1*R1,
+    A1=2+z+ceil(log2(R1+1)),
+
+and let g_R,g_L count the finite affine gates in the two actual recipes.
+The complete upper bound retains
+
+    F_template
+      + O_9(f*((g_R+g_L+2)*(Vraw+M1*A1^6)
+                   + V+(E+1)^4+Q_R+Q_L)
+             + r*f*V+(E+1)^4+388) + 22V+35.
+
+No ordinary numerical tariff is subtracted from an unrelated bound. Under
+the additional explicit long-record condition R1>=A1^6 and control absorption
+`(E+1)^4+Q_total=O(V)`, fixed source ranks/gates give
+`F_template+O(fV)`. If either condition fails, the larger displayed bound
+remains. The finite complete-MOVE fixture uses the latter regime and does
+not demonstrate long-record absorption. Neither regime implies the faster
+nonleaf native tariff or a larger complete multiplication kappa.
+
+If Q_R,Q_L are the actual finite monomial cohort sizes, the total inventory is
+
+    Q_total = 1+(45+Q_R)+388+(45+Q_L) = 479+Q_R+Q_L.
+
+For the documented real q2/capacity64 closed constructors, Q_R=Q_L=1878 and
+Q_total=4235. Larger constructors change that number and remain charged.
+An ordinary object being unused at runtime does not remove its tapes or
+initialization from the inventory.
+
+## 6. Complete historical backing
+
+The protected stage retains its supplied origin prefix and at most
+1+max V body/frontier cells across all calls. Each positive-header role
+retains at most 2*max E+1 body/frontier cells, as proved by its predecessor.
+Each of the two serial banks has 45 roles with O_9(max E+1) retained
+body/frontier bounds from the literal iterator proof. Their sum, not the
+largest active header, is charged.
+
+Add the complete inherited retained backing of both monomial native cohorts,
+the 349-role positive numeric cohort, original public fields/parent headers,
+all parked caller ancestors and fixed template/source storage. For each
+physical role take its maximum over the entire call and column history before
+summing roles. Completed blank cohorts remain allocated, and different roles
+may attain their maxima on different columns or calls. Nothing is reset or
+deallocated between the f monomial calls.
+
+The array-tape trace reports materialized role extents, which can differ from
+visited blank addresses. A conservative visited bound adds initially supplied
+regions and origins to the literal action count, since a unit move exposes
+at most one new address. Those observations do not replace the source space
+proof or establish a global caller stock bound.
+
+## 7. Exact limits and open next questions
+
+This is a source-level fixed-inventory construction for actual raw direct
+MOVEs. It reuses unchanged factors and source certificates; it does not
+materialize an enclosing source_ir.product/remap fragment, prove the global
+descriptor producer, or flatten all numeric control into lifecycle tables.
+The elementary r*f cutoff and precision/stock prerequisites still need to
+be established at an actual complete multiplication caller.
+
+The next useful obligations are a verified produced parent/placement and
+typed enclosing occurrence; literal lifecycle export of this complete numeric
+service; and a global argument admitting cutoff, common grid, headroom and
+long-record/control costs in the selected recurrence. These are distinct
+from the removed ordinary numerical runtime premise. All five foundational
+assumptions remain; no new kappa or unconditional theorem is claimed.
diff --git a/research/current-serial-pass-lower-bound/source/header_provider.py b/research/current-serial-pass-lower-bound/source/header_provider.py
new file mode 100644
index 0000000000..481013b988
--- /dev/null
+++ b/research/current-serial-pass-lower-bound/source/header_provider.py
@@ -0,0 +1,189 @@
+"""Current descriptor to retained Compact: a structured finite-control service.
+
+This is an executable source-level refinement, not an emitted A transition
+table. It accepts precisely A's numeric/context port views and fixed blank
+work ports. Runtime numerical values remain in Count tapes throughout.
+Prepared for @CubeJerry with substantial OpenAI assistance. Apache-2.0.
+"""
+from contextlib import ExitStack
+from binding_sources import need
+from codec import S,A,Cohort,collect_tapes,execution
+from cardinal_counts import Count,positive
+from compact_counts import power_two,copy_bits,append_bits
+from compact_layout import Layout
+from compact_streams import digit_permutation
+from encoded import compare,subtract
+from records import Tape
+from stream import Counter
+from session import OuterScope,borrowed_count,borrowed_tape,erase_marker,sealed_constructors
+from scratch_pool import ScratchPool
+
+SCHEMA=('outer','rows','stock','row_bits','within_bits','record_bits','p','d','K','G','H',
+        'q0','qF','qB','D','f','rho','active_start','back_start','selected_axes',
+        'entry_start','remainder','cutoff')
+NAMES=('u','u_rest','t','t_rest','before','x','middle','y','after','b')
+
+def scale(value,constant):
+    need(type(constant) is int and constant>=0,'compiled nonnegative multiplier')
+    if constant==0:return Count.literal(0)
+    out=Count(value)
+    if constant>1:out.multiply_small(constant)
+    return out
+
+class Provider:
+    def __init__(self,rank,source_block,target_block,native_factory):
+        need(type(rank) is int and rank>=2,'fixed compiled rank')
+        need(0<=source_block<rank and 0<=target_block<rank and source_block!=target_block,
+             'fixed distinct selected-block pair')
+        self.rank=rank;self.source_block=source_block;self.target_block=target_block
+        self.late=source_block>target_block
+        # native_factory constructs a fixed precompiled Ordinary supplier.
+        # It receives no runtime parameter or payload and is never called again.
+        with collect_tapes() as tapes:
+            native=native_factory()
+            need(type(native) is S.ordinary.Ordinary and native.observe is None
+                 and native.runtime.observe is None,'unchanged ordinary engine without payload callbacks')
+            self.engine=S.engine.CompactEngine(NAMES,'y' if self.late else 'x',
+                                              'x' if self.late else 'y',self.late,native)
+            self.pool=ScratchPool(160);self.scope=OuterScope(self.pool)
+            self.bridge,self.field_guide,self.header_guide,self.length_guide=(Tape() for _ in range(4))
+        self.cohort=Cohort(tapes,native)
+        self.observed_calls=0
+
+    @property
+    def port_count(self):return self.cohort.port_count
+
+    def bind(self,work):self.cohort.bind(work)
+
+    def read_header(self,context):
+        result={}
+        def advance():
+            self.header_guide.append(1);context.move(1)
+        for name in SCHEMA:
+            self.length_guide.rewind()
+            while context.read()==1:
+                self.length_guide.append(1);advance()
+            need(context.read()==0,'self-delimiting current header length');advance()
+            self.length_guide.rewind()
+            value=object.__new__(Count);value.tape=self.pool.acquire()
+            any_digit=multiple=False;last=0
+            while self.length_guide.read()!=4:
+                need(self.length_guide.read()==1,'unary current header length')
+                bit=context.read();need(bit in (0,1),'binary current header digit')
+                multiple=multiple or any_digit;any_digit=True;last=bit
+                value.tape.append(bit);advance();self.length_guide.step(1)
+            need(any_digit and (last==1 or not multiple),'canonical LSF current header value')
+            value.tape.append(3);value.rewind();result[name]=value
+            self.length_guide.clear()
+        need(context.read()==6,'exact current header frontier')
+        self.header_guide.rewind()
+        while self.header_guide.read()!=4:
+            context.move(-1);self.header_guide.step(1)
+        self.header_guide.clear()
+        return result
+
+    def prepare(self,header,cleanup):
+        def own(x):cleanup.callback(x.close);return x
+        for key in ('outer','rows','row_bits','record_bits','f','K','G','H'):
+            positive(header[key])
+        one=own(Count.literal(1));twoH=own(scale(header['H'],2))
+        need(compare(header['rho'],header['K'])<0,'selected offset inside one chunk')
+        n=own(subtract(header['f'],one))
+        compact=own(Count.product(n,header['G']))
+        rest=own(subtract(header['H'],compact))
+        chunk=own(Count.product(header['f'],header['K']))
+        left=own(scale(chunk,min(self.source_block,self.target_block)))
+        right=own(scale(chunk,max(self.source_block,self.target_block)))
+        left.add(header['active_start']);right.add(header['active_start'])
+        before=own(subtract(left,twoH))
+        difference=own(subtract(right,left));middle=own(subtract(difference,chunk))
+        right_end=own(Count(right));right_end.add(chunk)
+        after=own(subtract(header['back_start'],right_end))
+        tail=own(subtract(header['within_bits'],header['back_start']))
+        suffix=own(subtract(tail,compact))
+        # The full reserved back field exists, including its unused suffix.
+        need(compare(tail,header['H'])>=0,'complete root back reservation')
+        reduced=own(subtract(header['K'],one));rho=own(subtract(reduced,header['rho']))
+        fibre=own(power_two(suffix));record=own(Count.product(fibre,header['record_bits']))
+        rows=own(Count.product(header['outer'],header['rows']))
+        full=own(power_two(header['within_bits']));expected=own(Count.product(full,header['record_bits']))
+        need(compare(expected,header['row_bits'])==0,'exact complete physical row length')
+        active=own(scale(header['f'],self.rank));active.add(header['remainder'])
+        need(compare(active,header['selected_axes'])==0,'current f/remainder geometry')
+        rank=own(Count.literal(self.rank))
+        need(compare(header['remainder'],rank)<0,'ordinary remainder below fixed rank')
+        need(compare(header['selected_axes'],header['d'])<=0,'ordinary width within root budget')
+        active_end=own(scale(chunk,self.rank));active_end.add(header['active_start'])
+        need(compare(active_end,header['back_start'])<=0,'complete active block list precedes back field')
+        widths=(compact,rest,compact,rest,before,chunk,middle,chunk,after,compact)
+        return widths,n,rho,record,rows
+
+    def import_field(self,field):
+        while (symbol:=field.read())!=4:
+            need(symbol in (0,1,2),'complete canonical numerical field')
+            for shift in (2,1,0):self.bridge.append((symbol>>shift)&1)
+            self.field_guide.append(1);field.move(1)
+        self.bridge.rewind();self.field_guide.rewind()
+        while self.field_guide.read()!=4:
+            field.move(-1);self.field_guide.step(1)
+        self.field_guide.rewind()
+
+    def export_field(self,field,output):
+        output.rewind();self.field_guide.rewind()
+        while self.field_guide.read()!=4:
+            value=0
+            for _ in range(3):
+                bit=output.read();need(bit in (0,1),'complete returned physical codeword')
+                value=2*value+bit;output.step(1)
+            need(value in (0,1,2),'returned complete numerical record format')
+            need(field.read() in (0,1,2),'returned field has original exact extent')
+            field.write(value);field.move(1);self.field_guide.step(1)
+        need(output.read()==4 and field.read()==4,'exact full-field return frontier')
+        self.field_guide.rewind()
+        while self.field_guide.read()!=4:
+            field.move(-1);self.field_guide.step(1)
+        self.field_guide.clear();output.rewind()
+
+    def single(self,widths,rho,record,rows):
+        """f=1: the actual retained four-bucket bit gate, with no n>0 guard."""
+        e=self.engine;e.rearm();source=borrowed_tape(self.bridge)
+        with sealed_constructors(),e.scope.installed(),ExitStack() as cleanup:
+            plan=Layout(NAMES,widths,record);cleanup.callback(plan.close)
+            remaining=Counter(rows);cleanup.callback(remaining.close)
+            source_bit=plan.bit_position(e.source,rho);cleanup.callback(source_bit.close)
+            target_bit=plan.bit_position(e.target,rho);cleanup.callback(target_bit.close)
+            early=compare(source_bit,target_bit)<0
+            first,second=(source_bit,target_bit) if early else (target_bit,source_bit)
+            mapping=(0,1,3,2) if early else (0,3,2,1)
+            while not remaining.finished:
+                current=e.pool.acquire()
+                copy_bits(source,current,plan.row_bits);current.rewind()
+                following=digit_permutation(current,plan,first,second,mapping,e.pool.acquire)
+                append_bits(following,e.output);following.clear();remaining.decrement()
+                e.calls['rows']+=1
+            need(source.read()==4,'complete f=1 outer-row packet');source.rewind()
+        e.pool.empty()
+        for tape in e.pool.tapes:erase_marker(tape)
+        e.output.rewind();e.closed=True
+        return e.output
+
+    def run(self,field,context):
+        """field=A.CodedPort, context=A.BinaryContextPort; both start at origin.
+
+        The successful-input theorem leaves only field's exact output, context
+        unchanged, and every work port physically blank at its current origin.
+        No interrupted-service rollback contract is claimed.
+        """
+        self.cohort.start()
+        with execution(),self.scope.installed(),ExitStack() as cleanup:
+            header=self.read_header(context)
+            for value in header.values():cleanup.callback(value.close)
+            widths,n,rho,record,rows=self.prepare(header,cleanup)
+            self.import_field(field)
+            with self.scope.suspended():
+                returned=(self.single(widths,rho,record,rows) if n.zero() else
+                          self.engine.run(self.bridge,widths,n,header['K'],header['G'],rho,record,rows))
+            self.export_field(field,returned)
+            returned.clear();erase_marker(returned);self.bridge.clear()
+        self.pool.empty()
+        self.cohort.finish();self.observed_calls+=1
diff --git a/research/current-serial-pass-lower-bound/source/machine.py b/research/current-serial-pass-lower-bound/source/machine.py
new file mode 100644
index 0000000000..acf475e4fc
--- /dev/null
+++ b/research/current-serial-pass-lower-bound/source/machine.py
@@ -0,0 +1,406 @@
+"""Literal lifecycle control on fixed sequential tapes.
+
+Prepared for @CubeJerry with substantial OpenAI assistance. Apache-2.0.
+Stack is the authenticated #5356 implementation supplied by the loader.
+Algorithms never read tape addresses, extents, hardware arrays or a host stack.
+Instruction and primitive tables are fixed before runtime inputs vary.
+"""
+from dataclasses import dataclass
+
+ZERO, ONE, LEFT, SEP, END, BASE, BLANK = range(7)
+COMPONENT = 2
+
+
+def need(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def emit(tape, symbol):
+    tape.write(symbol)
+    tape.move(1)
+
+
+def origin(tape, marker=LEFT):
+    tape.move(-1)
+    while tape.read() != marker:
+        tape.move(-1)
+    tape.move(1)
+
+
+def retire(tape, marker=LEFT):
+    """Erase all coded bytes, including encoded logical blanks."""
+    origin(tape, marker)
+    while (symbol := tape.read()) != BLANK:
+        need(symbol in (ZERO, ONE), "contiguous binary body")
+        emit(tape, BLANK)
+    origin(tape, marker)
+
+
+def transfer(source, target, source_marker=LEFT, target_marker=LEFT):
+    """Administrative actual-byte copy; never an arithmetic COPY."""
+    origin(source, source_marker)
+    origin(target, target_marker)
+    need(target.read() == BLANK, "administrative transfer needs empty target")
+    while (symbol := source.read()) != BLANK:
+        need(symbol in (ZERO, ONE), "binary transfer")
+        emit(target, symbol)
+        source.move(1)
+    origin(source, source_marker)
+    origin(target, target_marker)
+
+
+class CodedPort:
+    """Seven virtual symbols encoded as three nonblank physical bits.
+
+    The physical LEFT before the current body is never exposed as data.
+    A left step at its local origin rejects. Two-sided routines first use
+    the standard translation to two one-sided ports.
+    """
+    __slots__ = ("tape",)
+
+    def __init__(self, tape):
+        self.tape = tape
+
+    def read(self):
+        t = self.tape
+        if t.read() == BLANK:
+            return 4
+        value = 0
+        for _ in range(3):
+            bit = t.read()
+            need(bit in (ZERO, ONE), "whole virtual codeword")
+            value = 2 * value + bit
+            t.move(1)
+        for _ in range(3):
+            t.move(-1)
+        need(value < 7, "unused virtual codeword")
+        return value
+
+    def write(self, value):
+        need(type(value) is int and 0 <= value < 7, "virtual alphabet")
+        for shift in (2, 1, 0):
+            emit(self.tape, (value >> shift) & 1)
+        for _ in range(3):
+            self.tape.move(-1)
+
+    def move(self, direction):
+        need(direction in (-1, 1), "virtual unit move")
+        t = self.tape
+        if direction == 1:
+            if t.read() == BLANK:
+                self.write(4)
+            for _ in range(3):
+                t.move(1)
+        else:
+            t.move(-1)
+            if t.read() == LEFT:
+                t.move(1)
+                raise ValueError("native routine crossed its local origin")
+            t.move(-1)
+            t.move(-1)
+
+
+class BinaryContextPort:
+    """Read-only raw binary descriptor, with its own physical alphabet.
+
+    Unlike CodedPort, read returns physical BLANK=6 at the frontier. A table
+    may inspect that frontier but cannot pass it or the current LEFT marker.
+    This supplies runtime e/f/K/rho data through counted local operations.
+    """
+    __slots__ = ("tape",)
+
+    def __init__(self, tape):
+        self.tape = tape
+
+    def read(self):
+        symbol = self.tape.read()
+        need(symbol in (ZERO, ONE, BLANK), "binary context alphabet")
+        return symbol
+
+    def write(self, value):
+        raise ValueError("native context is read-only")
+
+    def move(self, direction):
+        need(direction in (-1, 1), "binary context unit move")
+        t = self.tape
+        if direction == 1:
+            need(t.read() in (ZERO, ONE), "context frontier cannot be crossed")
+            t.move(1)
+        else:
+            t.move(-1)
+            if t.read() == LEFT:
+                t.move(1)
+                raise ValueError("native context crossed its local origin")
+
+
+def read_code(tape):
+    """Consume a numeric-format code; physical frontier returns None."""
+    if tape.read() == BLANK:
+        return None
+    value = 0
+    for _ in range(3):
+        bit = tape.read()
+        need(bit in (ZERO, ONE), "numeric codeword")
+        value = 2 * value + bit
+        tape.move(1)
+    need(value < 7, "unused numeric codeword")
+    return value
+
+
+def write_code(tape, value):
+    for shift in (2, 1, 0):
+        emit(tape, (value >> shift) & 1)
+
+
+def initialize(target, shape):
+    """Dispose of arbitrary old bytes, then zero the complete common format."""
+    need(target is not shape, "private initialization cannot destroy its guide")
+    retire(target)
+    origin(shape)
+    in_component = False
+    while (symbol := read_code(shape)) is not None:
+        need(symbol in (ZERO, ONE, COMPONENT), "canonical signed components")
+        if symbol == COMPONENT:
+            need(in_component, "positive component width")
+            write_code(target, COMPONENT)
+            in_component = False
+        else:
+            write_code(target, ZERO)
+            in_component = True
+    need(not in_component, "component terminator")
+    origin(shape)
+    origin(target)
+
+
+def copy_as_add(target, source):
+    """Signed addition into the actual destination, including any residue.
+
+    Components are little-endian two's complement followed by COMPONENT.
+    Carries reset at delimiters; equal-sign signed overflow rejects.
+    No ideal-zero test or exact-value overwrite substitutes for addition.
+    """
+    need(target is not source, "distinct COPY/ADD ports")
+    origin(source)
+    origin(target)
+    carry = 0
+    last_a = last_b = last_out = 0
+    in_component = False
+    while True:
+        a = read_code(source)
+        b = read_code(target)
+        need((a is None) == (b is None), "same complete numerical extent")
+        if a is None:
+            need(not in_component, "complete signed component")
+            break
+        need(a in (ZERO, ONE, COMPONENT) and b in (ZERO, ONE, COMPONENT),
+             "canonical signed addition operands")
+        need((a == COMPONENT) == (b == COMPONENT), "same component boundaries")
+        if a == COMPONENT:
+            need(in_component, "positive signed component width")
+            need(last_a != last_b or last_out == last_a, "signed addition overflow")
+            carry = 0
+            in_component = False
+            continue
+        value = a + b + carry
+        last_a, last_b, last_out = a, b, value & 1
+        carry = value >> 1
+        for _ in range(3):
+            target.move(-1)
+        write_code(target, last_out)
+        in_component = True
+    origin(source)
+    origin(target)
+
+
+def execute_table(table, ports, readonly_context=()):
+    """Run a supplied finite native table with every port confined.
+
+    These tables retain explicit semantics/time/space premises. Fixture
+    tables are not advertised as Gaussian implementations.
+    """
+    views = (tuple(CodedPort(t) for t in ports)
+             + tuple(BinaryContextPort(t) for t in readonly_context))
+    pc = 0
+    while True:
+        row = table[pc]
+        op = row[0]
+        if op == "halt":
+            break
+        if op == "reject":
+            raise ValueError(row[1])
+        if op == "goto":
+            pc = row[1]
+            continue
+        view = views[row[1]]
+        if op == "branch":
+            pc = dict(row[2]).get(view.read(), row[3])
+            continue
+        if op == "write":
+            view.write(row[2])
+        elif op == "move":
+            view.move(row[2])
+        else:
+            raise ValueError("native table opcode")
+        pc += 1
+    for tape in tuple(ports)+tuple(readonly_context):
+        origin(tape)
+
+
+@dataclass(frozen=True)
+class Instruction:
+    op: str
+    ports: tuple = ()
+    token: tuple = ()
+
+
+class Controller:
+    """Fixed finite controller of a fixed flat compiled template.
+
+    rows implements the separately priced row/shape interface; all its
+    dynamic state belongs on the supplied tapes. services contains fixed
+    finite transition tables. Payload ports include metadata and all scratch.
+    The only runtime continuation is the physical Stack.
+    """
+    def __init__(self, program, public_count, payloads, control, descriptor,
+                 bridge, child_header, rows, services, stack_class, protected_ports=(),
+                 primitive_work=(), primitive_context=()):
+        self.program = tuple(program)
+        self.public_count = public_count
+        self.payloads = tuple(payloads)
+        self.control = control
+        self.descriptor = descriptor
+        self.bridge = bridge
+        self.child_header = child_header
+        self.rows = rows
+        self.services = services
+        need(len({id(t) for t in self.payloads+(control,descriptor,bridge,child_header)})
+             == len(self.payloads)+4, "all physical ports distinct")
+        self.stack = stack_class(self.payloads, control, descriptor)
+        self.protected_ports = tuple(protected_ports)
+        owned = {e.ports[0] for e in self.program if e.op == "INIT"}
+        need(all(public_count <= i < len(self.payloads) for i in owned), "INIT only private physical slots")
+        need(owned.isdisjoint(self.protected_ports), "owned fields cannot be borrowed descriptors")
+        self.root_cleanup = tuple(i for i in range(public_count,len(self.payloads))
+                                  if i not in self.protected_ports)
+        self.primitive_work = tuple(primitive_work)
+        self.primitive_context = tuple(primitive_context)
+        data_ports = {i for e in self.program for i in e.ports}
+        need(all(0 <= i < len(self.payloads) for i in data_ports), "compiled port range")
+        need(all(i >= public_count and i < len(self.payloads) and i not in data_ports
+                 and i not in self.protected_ports for i in self.primitive_work), "separate primitive scratch")
+        need(len(set(self.primitive_work)) == len(self.primitive_work), "distinct primitive work ports")
+        need(len(set(self.primitive_context)) == len(self.primitive_context)
+             and all(i in self.protected_ports and 0 <= i < len(self.payloads)
+                     and i not in data_ports for i in self.primitive_context), "borrowed binary context ports")
+        self.pc_bits = max(1, (len(self.program) - 1).bit_length())
+        self.pc_words = tuple(tuple((pc >> j) & 1 for j in range(self.pc_bits))
+                              for pc in range(len(self.program)))
+        need(self.program and self.program[-1].op == "RET", "finite completed program")
+
+    def save_pc(self, pc):
+        need(self.descriptor.read() == BLANK, "empty active PC descriptor")
+        for bit in self.pc_words[pc]:
+            emit(self.descriptor, bit)
+        origin(self.descriptor, BASE)
+
+    def consume_pc(self):
+        pc = 0
+        for shift in range(self.pc_bits):
+            bit = self.descriptor.read()
+            need(bit in (ZERO, ONE), "binary return PC")
+            pc |= bit << shift
+            emit(self.descriptor, BLANK)
+        need(self.descriptor.read() == BLANK, "exact fixed return PC width")
+        origin(self.descriptor, BASE)
+        need(pc < len(self.program) and pc > 0 and self.program[pc-1].op == "PAID",
+             "return PC designates a paid continuation")
+        return pc
+
+    def has_parent(self):
+        self.control.move(-1)
+        symbol = self.control.read()
+        self.control.move(1)
+        need(symbol in (BASE, END), "complete continuation top")
+        return symbol == END
+
+    def descend(self, pc):
+        event = self.program[pc]
+        source = self.payloads[event.ports[0]]
+        transfer(source, self.bridge, target_marker=BASE)
+        self.rows.prepare(event.token, self.child_header)
+        self.save_pc(pc + 1)
+        self.stack.push((True,) * len(self.payloads))
+        self.rows.install(self.bridge, self.child_header,
+                          self.payloads[:self.public_count])
+        retire(self.bridge, BASE)
+        retire(self.child_header, BASE)
+
+    def primitive(self, token, fields):
+        for i in self.primitive_work:
+            retire(self.payloads[i])
+        execute_table(self.services[token],
+                      tuple(self.payloads[i] for i in fields+self.primitive_work),
+                      tuple(self.payloads[i] for i in self.primitive_context))
+        for i in self.primitive_work:
+            retire(self.payloads[i])
+
+    def ascend(self):
+        self.rows.collect(self.payloads[:self.public_count], self.bridge)
+        for tape in self.payloads:
+            retire(tape)
+        self.stack.pop()                   # ignore observer sizes and heads
+        pc = self.consume_pc()
+        target = self.payloads[self.program[pc-1].ports[0]]
+        retire(target)
+        transfer(self.bridge, target, source_marker=BASE)
+        retire(self.bridge, BASE)
+        return pc
+
+    def run(self, observe=None):
+        pc = 0
+        while True:
+            event = self.program[pc]
+            if observe is not None:
+                observe("before", pc, event)  # checker only; ignores return value
+            if event.op == "INIT":
+                initialize(self.payloads[event.ports[0]], self.payloads[0])
+                pc += 1
+            elif event.op == "CLEAR":
+                retire(self.payloads[event.ports[0]])
+                pc += 1
+            elif event.op == "COPY":
+                copy_as_add(self.payloads[event.ports[0]], self.payloads[event.ports[1]])
+                pc += 1
+            elif event.op == "SERVICE":
+                self.primitive(event.token,event.ports)
+                pc += 1
+            elif event.op == "PAID":
+                if self.rows.is_leaf(event.token):
+                    self.primitive(("leaf",)+event.token,event.ports)
+                    pc += 1
+                else:
+                    self.descend(pc)
+                    pc = 0
+            elif event.op == "RET":
+                if not self.has_parent():
+                    for i in self.root_cleanup:
+                        retire(self.payloads[i])
+                    break
+                pc = self.ascend()
+            else:
+                raise ValueError("compiled opcode")
+            if observe is not None:
+                observe("after", pc, event)
+
+
+def boundary_actions(q, b, parent_total, child_total, input_length,
+                     output_length, staged_header_length):
+    """Exact descend+ascend actions, excluding the three row-service calls.
+
+    Also excludes caller leaf/top tests. All heads are at local origins.
+    Includes PC, all retirement, occupied-target replacement and both relays.
+    """
+    return (4 * parent_total + 5 * child_total + 18 * input_length
+            + 13 * output_length + 5 * staged_header_length
+            + 38 * q + 27 * b + 103)
diff --git a/research/current-serial-pass-lower-bound/source/phase-proof.md b/research/current-serial-pass-lower-bound/source/phase-proof.md
new file mode 100644
index 0000000000..5bd585e03c
--- /dev/null
+++ b/research/current-serial-pass-lower-bound/source/phase-proof.md
@@ -0,0 +1,449 @@
+# Current coded Gaussian monomial with complete coefficient fibres
+
+Prepared for **@CubeJerry**, with substantial OpenAI assistance in source
+analysis, implementation, mathematical argument, and adversarial verification.
+Apache-2.0; predecessor notices and exact computational sources are retained.
+
+## 1. Claim and non-overlap
+
+This package supplies the missing format and context join between the physical
+Gaussian monomial of [#3087](https://github.com/CrocSwap/integer-mult-bounds/pull/3087)
+and the current three-bit `CodedPort` numeric field and twenty-three-field
+descriptor. It produces the old layout and signed coefficients through counted
+physical operations, executes the unchanged monomial, and returns the complete
+current format in place. It preserves the descriptor and all caller ancestors,
+and erases every owned current segment, including encoded logical blanks.
+
+The theorem below is a **structured finite-control, fixed-inventory source
+refinement**, relative to the stated completed ordinary supplier and current
+port contracts. It is not an emitted flat transition table for the lifecycle
+controller. It does not close a universal selected assumption or change kappa.
+
+The inherited phase formula, affine compiler, signed-pair theorem, Compact
+algorithm, and their cost are not new results. Jose Manuel (`jmbarrancoml`), with
+OpenAI assistance, already implemented those in #3087, building on #2250,
+#2378, #2422, and #3055. [#6293](https://github.com/CrocSwap/integer-mult-bounds/pull/6293)
+already treats the all-width phase convention, including the repeated constant.
+[#6930](https://github.com/CrocSwap/integer-mult-bounds/pull/6930), pinned at
+`c726399fbdb6d80dd13bed760b56572fb4ea1022`, already audits the primary phase
+integer of the selected MOVE used here. We inherit those results.
+
+Chris R (`Clear1nsight`), with OpenAI assistance, supplied the older prepared
+QQ16 common-grid conversion and signed packet join in
+[#4129](https://github.com/CrocSwap/integer-mult-bounds/pull/4129). Its raw/tagged
+packet and caller contracts differ from this current descriptor, current
+`CodedPort`, selected source token, and suffix layout. We neither repeat its
+quantum conversion nor identify its old component ABI with the current one.
+
+The separately credited [current Compact binding](https://github.com/CubeJerry/integer-mult-bounds/tree/5629e7772d1720d6727465e328a45694f8620538/research/compiled-compact-native-binding) supplies the
+shared current symbol codec, exact header parser, guarded old-tape refinement,
+and complete current-segment retirement. We reuse those exact bytes. Its opaque
+record permutation by itself does not establish arithmetic on the three-bit
+encoding: the new delimiter stripping, signed-field grouping, and exact return
+in this package are necessary for that step.
+
+## 2. Quantified current interface
+
+Compile a literal invertible binary monomial of fixed rank `1<=m<=73`, with
+matrix `L`, offset `v`, constant `c` modulo four, linear coefficients `l_i`
+modulo four, and strict-upper quadratic coefficients `q_ik` in `{0,1}`.
+Compile its direction and one completed ordinary supplier before numerical
+input. The supplier has the unchanged native interface and the contract used
+by #3087; its fixture elementary branch is not an admission of its faster rate.
+
+`Provider(literal,native_factory,inverse=False).bind(work)` fixes a finite set of
+physical work ports. `run(field,context)` receives a current `CodedPort` field
+and a read-only `BinaryContextPort` descriptor, both at their local origins.
+The caller supplies genuinely disjoint physical segments for field, context,
+and all work roles. The object-identity guards reject obvious aliasing but do
+not prove disjointness of distinct wrappers over the same physical segment.
+All current work segments are initially physically blank. Caller ancestors
+precede protected local origin markers and are outside the writable segments.
+
+The exact descriptor order is
+
+```
+outer, rows, stock, row_bits, within_bits, record_bits, p, d, K, G, H,
+q0, qF, qB, D, f, rho, active_start, back_start, selected_axes,
+entry_start, remainder, cutoff.
+```
+
+Each nonnegative integer is represented by a positive unary digit length,
+a zero separator, and that many canonical least-significant-first binary
+digits. The exact physical frontier follows field 23. All fields are scanned
+and returned unchanged; unused large metadata is not free. In particular,
+the address reservation `H` is not the signed component width below.
+
+Write `a=within_bits`, `b=record_bits`, `u=active_start`, `z=back_start`,
+`C=outer*rows`, and let `h>=2` be the uniform signed component width. Each
+original numeric record contains `r>=1` complex coefficient fields. Each field
+has `h` real bits then a component delimiter, and `h` imaginary bits then a
+component delimiter. The bits are little-endian two's-complement integers on
+one fixed common grid supplied by the caller. Each virtual bit or delimiter
+is encoded by the current three-bit code, so
+
+```
+b=6*r*(h+1),  row_bits=2^a*b,  V=C*2^a*b.
+```
+
+The delimiter is virtual symbol 2, physically `010`. A numeric zero component
+therefore retains its delimiter; it is not an unformatted run of physical zeros.
+Virtual blank 4 is the stream frontier, while physical blank is symbol 6.
+No internal physical blank is admitted inside a canonical complete field.
+
+The required geometry is
+
+```
+outer,rows,f,K,G,H > 0,    0<=rho<K,
+n=f-1,  t=n*G<=H,
+2H<=u,  u+m*f*K<=z,  z+H<=a,
+selected_axes=m*f+remainder<=d,  0<=remainder<m.
+```
+
+All positions are already within-row coordinates measured from the left.
+This service does not subtract a global prefix again, and does not change
+within-row geometry when `rows` or `stock` changes. Row counts may be arbitrary
+positive integers. The remaining current producer premises, such as `H=dG`,
+the correct occurrence placement and the global common-grid choice, are
+retained when this service is used by that producer.
+
+For each original address `x`, let `x_j` be the rank-m column at positions
+`u+(i*f+j)*K+rho`, `0<=i<m`, `0<=j<f`. The endpoint is exactly the inherited
+monomial
+
+```
+P(x)=f*c+sum_j(sum_i l_i*x_(j,i)
+                  +2*sum_(i<k) q_(i,k)*x_(j,i)*x_(j,k))  (mod 4).
+```
+
+It applies `x_j -> L*x_j+v` in each column, and applies `i^P(x)` to every one
+of the `r` original complex coefficients. All other address coordinates,
+outer-row labels, coefficient ordering, common quantum, and descriptor values
+are preserved. The inverse recovers the original address first and applies
+`i^-P(x)` there. No precision conversion or rounding occurs.
+
+## 3. Encoded geometry and the suffix-fibre identity
+
+Set `s=a-z-t>=0`. The last `s` unselected address bits are a complete consecutive
+suffix fibre. Interpret its `2^s` original records as additional coefficient
+fields of a single old-format record:
+
+```
+r'=2^s*r,  R=2*h*r',  a'=a-s=z+t,
+M0=2^a',  M=C*M0,  v0=M0*R,  Vraw=C*v0=C*2^a*2*h*r.
+```
+
+For `h>=2`, `Vraw/V=h/(3(h+1))` lies between `2/9` and `1/3`, so raw
+and current physical payload volumes differ by a bounded constant factor.
+
+The old field schema is fixed at construction:
+
+| Field | Width | Current interval |
+|---|---:|---|
+| `u` | `t` | first front prefix |
+| `u_rest` | `H-t` | remainder of first front field |
+| `t` | `t` | second front prefix |
+| `t_rest` | `H-t` | remainder of second front field |
+| `before` | `u-2H` | all positions before the vector blocks |
+| `v_i`, each `0<=i<m` | `fK` | current vector block i |
+| `after` | `z-u-mfK` | all positions before the back field |
+| `b` | `t` | back prefix |
+
+The field widths sum to `a'`. Every displayed width is nonnegative by the
+interface. The two front prefixes precede all vectors, and the back prefix
+follows them. All residual helper fields may contain arbitrary dirty address
+bits. No helper is initialized to zero or discarded.
+
+This is an equality of consecutive physical stream intervals after delimiter
+stripping, not an uncharged permutation. The old record traverses first the
+suffix address and then the original coefficient index, exactly their current
+stream order. Since no selected bit is in that suffix, every coefficient in
+the fibre has the same `P` and affine destination. The unchanged #3087 scan
+processes all `r'` coefficients. Thus grouping the suffix preserves each
+original coefficient's endpoint. Leaving the suffix among enumerated address
+bits would also be algebraically possible, but would lose the long-record
+accounting used below; the implementation performs this explicit grouping.
+
+Old native selected positions are counted from the least-significant end of
+each vector field. Set
+
+```
+rho_native=K-1-rho.
+```
+
+The old selected position `rho_native+jK` equals the current position with
+column ordinal `f-1-j`. The same reversal occurs in every vector block. Since
+the identical affine map acts independently on each column and the phase is
+the sum over all columns, this reversal changes neither endpoint. Merely
+passing current `rho` to the old API would generally select other bits.
+
+`prepare` constructs these integers with encoded Counts. It reads `h` by
+counting the first component's format symbols; it does not decode a signed
+value. It divides `b` by `6(h+1)` and checks positive quotient and zero
+remainder. It checks the exact complete row length and all intervals above.
+Its varying row counts, widths, shifts, and coefficient count remain on tapes.
+
+## 4. Signed conversion and the complete return
+
+`import_field` visits the current stream in order. For each complex pair it
+copies exactly `h` bits, checks and skips delimiter 2, then repeats for the
+imaginary component. It uses an encoded ripple counter for those widths and
+a lockstep guide for the current symbols. It checks each later component has
+the same width and delimiter. It preserves the complete `h`-bit representation,
+including leading zeros and redundant sign bits; components are never
+normalized as unsigned Counts. The old input has precisely the complete raw
+format of #3087. The inherited engine verifies its total extent against
+`C*2^a'*R`, so a whole-pair-aligned but incorrectly sized field is not silently
+accepted. The guide restores the current public head without decoding a
+payload length or consulting its allocated array length.
+
+The monomial runs on that separate borrowed raw copy while the parent scope
+is suspended. Its protected result is consumed before engine reuse. Only after
+the entire monomial has returned does `export_field` modify the public field.
+It copies every returned signed bit and reinserts each component delimiter at
+its existing position. It requires exact agreement of raw output, current
+field and guide frontiers. It restores the public origin and clears the
+protected return, marker, bridge and guide. Consequently the returned current
+body has exactly `V` physical bits in the same canonical format and on the
+same numerical grid.
+
+The only numerical admission is inherited signed representability. For phase
+0 no component is negated; phase 1 requires the imaginary component to exceed
+`-2^(h-1)`; phase 2 requires both; phase 3 requires the real component. These
+conditions are required separately for every coefficient in every folded
+fibre. The unchanged #3087 implementation checks both components before
+emitting that pair, and raises `SignedHeadroomError` when needed.
+
+On this named error for otherwise admitted shape and format, the inherited
+engine erases partial output, closes its counters and current packet, and
+returns to a reusable closed state. The wrapper has not written the public
+field, closes its setup Counts, and retires all coded work. Thus field and
+context remain unchanged and a subsequent valid input may use the same
+inventory. This statement does not promise rollback for arbitrary malformed
+streams, internal errors or interrupted execution.
+
+## 5. Physical refinement, ownership, and retained backing
+
+The source bootstrap loads the authenticated computational bodies of #3087
+unchanged. Its archive-discovery module is replaced only by a shim selecting
+the already authenticated shared Compact, Count, Tape and ordinary modules
+from `compiled-compact-native-binding`. Runtime identity checks require one
+actual Count/Tape vocabulary. `DEPENDENCIES.json` records Git blob and SHA256
+for all copied source files, together with original repository, commit or
+archive/member provenance. No numerical computation is delegated to a fixture
+callback or to a host array.
+
+That binding represents each old symbol by four current virtual bits, hence
+twelve physical bits. Logical blanks are coded nonblank physical strings.
+The old runtime `read`, `write`, `step`, origin guards and parking-table steps
+are refined by local physical operations. Runtime indexing of old `cells`
+is blocked; host head positions are not exposed to the algorithm. Fixed
+template data, fixed role identities, alphabet symbols and finite phase states
+may be in control. Varying coordinates and shapes use the encoded primitives.
+
+Construction, including the literal affine word and native inventory, occurs
+before input and has a positive fixed cost `F_template`. The wrapper adds
+192 setup scratch roles and four persistent buffers to the inherited finite
+engine inventory. The wrapper has 23 borrowed-header copies and a fixed
+number of setup temporaries: 24 `prepare` results and the component-width Count,
+with fewer than 32 additional arithmetic/counter roles at any source site.
+Thus fewer than 80 wrapper roles are simultaneously live. Its parent scope is suspended across the child,
+so these roles are not silently shared with active child leases. There is no
+physical tape allocation per row, coefficient, column, gate, or recursion depth.
+
+On completion, raw current retirement scans through coded logical blank tails
+to the first fresh physical blank and restores the local origin. It does not
+stop at an internal old logical blank. Therefore every owned current extent
+is physically blank, and ancestor prefixes are untouched. The normal and
+optimized executions below inspect all historical backing cells to test this
+claim; the mathematical invariant is the contiguous coded frontier and local
+origin, not the inspected array representation.
+
+Previously allocated backing remains allocated. For role i let `o_i(k)` be
+its current physical origin and `z_i(k)` its reached old-symbol extent in call
+k, including coded blank extension. An honest retained envelope includes
+
+```
+sum_i max_(k<=current) [o_i(k)+12*z_i(k)+O(1)],
+```
+
+as well as borrowed field/context backing and the caller's continuation bank.
+Smaller calls do not shrink this envelope. They also do not rescan a prior
+larger extent: a successful preceding retirement leaves it physically blank,
+and a new contiguous call stops at its own frontier.
+
+## 6. Complete cost and the favorable domain
+
+Let `E` be the physical header length, `Q` the fixed work-port count, and
+`A=2+a'+ceil(log2(R+1))`. Let `g_E` be the literal word's early XOR/toggle
+count, `g_L` its late XOR count, `g=g_E+g_L`, and `S=4g_E+12g_L`.
+For `f>1` set
+
+```
+delta=min(1,(f-1)*(2*2^(-G)+8*2^(G-K))).
+```
+
+The completed binary ordinary bill `T_B(v,beta)` includes real padding and
+restriction, its native work, borrowed preservation, return consumption and
+cleanup. #3087 and #3055 give the unchanged old-symbol invoice
+
+```
+T_old <= S*sum_(j=1)^C T_B(v0,(f-1)G)
+         + O_(m)((g+1)*(Vraw+M*A^6)
+                  +g*delta*M*A*(R+A)).                         (1)
+```
+
+There are actually `S*C` ordinary calls. At `f=1` there are no ordinary calls
+or exceptional term; retain `O_m((g+1)*Vraw+M*A^6)`. The phase-only recipe has
+`g=0` and still pays its complete coefficient scan and setup. No fixture timing
+is used to derive (1).
+
+The new wrapper incurs no per-payload-bit long length scan. Ripple counter
+initialization and decrements for an h-bit component cost `O(h)` in aggregate,
+and each current symbol is visited a bounded number of times by the bridge
+and guide. Hence signed format conversion costs `O(V)`. The first component
+width scan costs `O(h)` and is included in this bound. Since a valid header's
+`row_bits` value has at least `a+log2(b)` digits, and `h<=b`, all one-time
+geometry arithmetic has operand lengths `O_m(E+1)`. Repeated doublings build
+`2^a` and `2^s` in polynomial time in E. A conservative envelope for the fixed
+number of products, divisions, comparisons and such loops is `O_m((E+1)^4)`.
+
+Let `Z=sum_i z_i` denote **this call's** sum of reached old-symbol extents over
+all work, setup, bridge and parking roles. A complete current-physical bill is
+
+```
+T_current <= F_template + C_codec*T_old
+             + C_m*(V+(E+1)^4+Q) + 64*(Z+Q).                  (2)
+```
+
+The fixed `C_codec` covers the whole guarded source-control refinement,
+including local head and parking checks; it is not inferred solely from the
+constant for one read/write/move. The explicit last term pays current raw
+retirement, including encoded blanks and origin work. Every reached symbol
+costs a unit move or initialization in this call, so
+`Z=O(T_old+V+(E+1)^4+Q)`. Substitution gives the shape of (1), with a fixed
+codec factor and the displayed new setup/conversion bill. In contrast to
+#3087's specialized f=1 unused-G observation, this adapter reads the complete
+current descriptor and charges its E even when a field is unused.
+
+For occupied workspace, keep the inherited conservative monomial allowance
+
+```
+6*Vraw+2*delta*M*a'+M+O_m(A+log(C+1))
+    +W_B(v0,(f-1)G)+F_native,
+```
+
+with ordinary and exceptional terms omitted at f=1. Add the borrowed current
+field V, header E, setup/header guides `O(E+A)`, and the current field guide
+`O(V)`, multiply old-symbol owned extents by twelve, and include the fixed
+parking roles. For fresh backing also retain each inherited parent role's
+maximum `O(Vraw+A+log(C+1))`, each Compact role's maximum
+`O(v0+delta*M0*a'+A+log(C+1))`, protected output, and the actual ordinary
+supplier's per-role allowance. Fixed role capacities are genuine constants.
+For reuse use the historical maxima in Section 5 rather than fresh size alone.
+
+A favorable production specialization must state its hypotheses. If `H=dG`,
+`m>=2`, and `mf+remainder<=d`, then `f<=d/2` and
+
+```
+s>=H-(f-1)G>=dG/2,
+R=2*h*r*2^s >= 2*h*r*2^(dG/2).
+```
+
+For m=1 this automatic inequality is unavailable; long-record growth remains
+an explicit extra domain premise. In a root regime with `d->infinity`,
+`G=4ceil(log2 p)+6`, `A=O(p)`, and `E=O_m(p+log(C+1))`, R exceeds every fixed
+power of p. The selected schedule's `K=128G` satisfies the sufficient retained
+guard inequality `K>=G+4ceil(log2 p)+10`, giving `delta=O(p^-3)` for `f<=p`.
+Then `M*A^6/Vraw=A^6/R` and
+`delta*M*A*(R+A)/Vraw=delta*A*(1+A/R)` are bounded by the claimed lower order
+terms. The E-polynomial is absorbed using superpolynomial R and
+`log(C+1)^k=O_k(C)` for each fixed k. These are additional stated domain
+conditions, not consequences of an arbitrary valid finite header.
+
+If the admitted ordinary supplier has `T_B(v,beta)<=K_q*v*(1+beta^tau_B)`,
+the favorable specialization is
+`O_(q,m)(V*(1+((f-1)G)^tau_B))`. The retained historical exponent is
+`tau_B=99830289/100000000`. It does not imply the smaller current selected
+node exponent. Equations (1) and (2), the source supplier premises, and the
+backing envelopes remain the complete all-size statement; no new kappa is
+claimed.
+
+## 7. One actual selected source boundary
+
+`selected_service.py` authenticates the current selected word and canonical
+Clifford source. It locates raw event 9896,
+`["MOVE",236,3,7,false]`, through the current lifecycle `current_local` lowering.
+The exact service token is `("move-in","local",9896,raw_record)` on owner
+236, with the matching `move-out` cut. This raw four-field token is the
+established source boundary. The guard also accepts a syntactically flat prefix
+before that tuple, but this optional flat-prefix ABI is **not** the nested
+token emitted by `source_ir.remap`. The actual `caller-local` token contains
+the old token as its last tuple member, and is not accepted by this binder.
+An enclosing caller therefore still needs a separate typed token adapter;
+no complete nested caller-occurrence binding is claimed. The physical owner is
+bound explicitly through the event's field list; it is not an implicit global
+array reference.
+
+The event token alone does not normalize the enclosing occurrence's header.
+At this boundary the caller must expose the nine current vector blocks and
+their span with `selected_axes=9*f+remainder`, in the coordinates admitted in
+Section 2. A larger compiler occurrence needs its existing paid placement and
+descriptor service to establish this premise, in addition to the token adapter
+above. Matching a raw token or flat suffix is not a proof of that geometry.
+
+The literal comes from the authenticated canonical frame transition 3 to 7.
+The existing #6930 audit supplies the width-one phase interpretation. Its
+right monomial has constant 1 and the exact rows
+
+```
+matrix=(21,17,2,20,8,32,64,128,256), offset=1,
+linear=(3,0,3,0,2,0,0,0,0), quadratic=(5,0,5,0,0,0,0,0,0).
+```
+
+The resulting record hash and complete left literal are in `SELECTED-MOVE.json`.
+`Service` compiles the right monomial at `move-in`, and the left at `move-out`.
+The intermediate rank-one Fourier child is outside this contribution. This
+is not a new primary-phase audit, and not a numerical proof of the full MOVE.
+
+Four selected physical phase-control calls use the actual 23-field descriptor,
+native recipe, and codec with f=2,3,4. The zero-column f=2 case produces phase2,
+not a copied one-column phase1. A wrong residue and wrong frame token are
+discriminating negative controls. These execute the actual selected control
+interface but do not materialize its complete rank-nine packet. The all-size
+endpoint follows from Sections 2-5 and inherited monomial correctness; the
+finite evidence cannot replace those arguments.
+
+## 8. Evidence, limits, and remaining work
+
+The author fixture uses a separately coded signed/address endpoint oracle and
+complete current physical packets. It covers f=1 with nontrivial K/rho
+orientation, f=2 forward and inverse with real Compact/ordinary calls, all
+coefficient fields, multiple outer/inner rows, dirty spectators, folded suffix
+fibres, nonzero translated origins, later-field signed-headroom rejection and
+valid retry, and historical backing reuse. Both normal and optimized Python
+must reproduce the same exact action and endpoint receipts. It uses the actual
+ordinary elementary branch, never an oracle supplied to the numerical engine.
+Independent review is registered separately when its receipt is frozen.
+
+The selected rank-nine complete packet is not executed. These tests admit
+neither the retained faster ordinary rate nor the selected native exponent.
+The current placement/row service, actual complete numerical caller, flat-table
+export, global width/headroom allocation, full selected recurrence budget,
+coefficient arithmetic and analytic recovery remain outside this scoped join.
+All five selected framework assumptions remain listed in the receipt.
+
+## Open next questions
+
+1. Export the bounded current adapter control into the lifecycle controller's
+   literal transition-table syntax. First preserve this exact complete-format
+   endpoint and signed-error boundary on one occurrence; the existing semantic
+   service token alone is not a machine table.
+2. Supply a completed binary ordinary service at the current required rate,
+   or a different full invoice. Its source preservation, private cleanup and
+   output consumption must accompany the rate; this adapter cannot upgrade
+   the historical exponent.
+3. Join the current numerical caller's width/common-grid allocation to these
+   phase-specific headroom conditions and to the paid rank-one child between
+   the two MOVE monomials. The first useful check is a complete small actual
+   caller occurrence with its live descriptor and suspended private bank.
diff --git a/research/current-serial-pass-lower-bound/source/phase_adapter.py b/research/current-serial-pass-lower-bound/source/phase_adapter.py
new file mode 100644
index 0000000000..02f0fdc3ba
--- /dev/null
+++ b/research/current-serial-pass-lower-bound/source/phase_adapter.py
@@ -0,0 +1,213 @@
+"""Paid current signed-format and 23-field context join to unchanged #3087.
+
+Runtime shapes stay on encoded Count tapes. The complete untouched back suffix
+is folded into additional coefficient fields, so every one receives its phase.
+Prepared for @CubeJerry with substantial OpenAI assistance. Apache-2.0.
+"""
+from contextlib import ExitStack
+from phase_binding import activate, need
+
+S = activate()
+from cardinal_counts import Count, positive
+from compact_counts import power_two
+from encoded import compare, divide, subtract
+from records import Tape
+from scratch_pool import ScratchPool
+from session import OuterScope, erase_marker
+from stream import Counter
+from codec import Cohort, collect_tapes, execution
+
+SCHEMA = S.provider.SCHEMA
+
+
+def scale(value, multiplier):
+    need(type(multiplier) is int and multiplier >= 0, "fixed template multiplier")
+    if multiplier == 0:
+        return Count.literal(0)
+    out = Count(value)
+    if multiplier != 1:
+        out.multiply_small(multiplier)
+    return out
+
+
+class Provider:
+    def __init__(self, literal, native_factory, inverse=False):
+        need(type(inverse) is bool, "compiled monomial direction")
+        self.rank = len(literal["matrix_rows"])
+        need(1 <= self.rank <= 73, "fixed source monomial rank")
+        self.inverse = inverse
+        self.vectors = tuple("v" + str(i) for i in range(self.rank))
+        self.names = ("u", "u_rest", "t", "t_rest", "before", *self.vectors, "after", "b")
+        with collect_tapes() as tapes:
+            native = native_factory()
+            need(type(native) is S.source.ordinary.Ordinary and native.observe is None
+                 and native.runtime.observe is None, "same closed ordinary supplier without payload callback")
+            self.engine = S.engine.MonomialEngine(self.names, self.vectors, literal, native)
+            self.pool = ScratchPool(192)
+            self.scope = OuterScope(self.pool)
+            self.bridge, self.field_guide, self.header_guide, self.length_guide = (Tape() for _ in range(4))
+        self.cohort = Cohort(tapes, native)
+        self.calls = 0
+
+    @property
+    def port_count(self):
+        return self.cohort.port_count
+
+    def bind(self, work):
+        self.cohort.bind(work)
+
+    def read_header(self, context):
+        return S.provider.Provider.read_header(self, context)
+
+    def component_width(self, field):
+        """Read only the first component's format length, never its integer."""
+        width = Count.literal(0)
+        while field.read() in (0, 1):
+            width.increment()
+            field.move(1)
+        need(field.read() == 2, "first canonical signed component terminator")
+        remaining = Counter(width)
+        try:
+            while not remaining.finished:
+                field.move(-1)
+                remaining.decrement()
+        finally:
+            remaining.close()
+        return width
+
+    def prepare(self, header, h, cleanup):
+        def own(value):
+            cleanup.callback(value.close)
+            return value
+        for name in ("outer", "rows", "row_bits", "record_bits", "f", "K", "G", "H"):
+            positive(header[name])
+        one, two = own(Count.literal(1)), own(Count.literal(2))
+        need(compare(h, two) >= 0 and compare(header["rho"], header["K"]) < 0,
+             "signed width and selected current residue")
+        n = own(subtract(header["f"], one))
+        compact = own(Count.product(n, header["G"]))
+        rest = own(subtract(header["H"], compact))
+        twice_H = own(scale(header["H"], 2))
+        before = own(subtract(header["active_start"], twice_H))
+        chunk = own(Count.product(header["f"], header["K"]))
+        active_end = own(scale(chunk, self.rank))
+        active_end.add(header["active_start"])
+        after = own(subtract(header["back_start"], active_end))
+        tail = own(subtract(header["within_bits"], header["back_start"]))
+        need(compare(tail, header["H"]) >= 0, "entire current back reservation")
+        suffix = own(subtract(tail, compact))
+        fibre = own(power_two(suffix))
+        top = own(subtract(header["K"], one))
+        rho = own(subtract(top, header["rho"]))
+        selected = own(scale(header["f"], self.rank))
+        selected.add(header["remainder"])
+        rank = own(Count.literal(self.rank))
+        need(compare(selected, header["selected_axes"]) == 0
+             and compare(header["remainder"], rank) < 0
+             and compare(header["selected_axes"], header["d"]) <= 0,
+             "current active width, fixed rank and untouched ordinary remainder")
+        complete = own(power_two(header["within_bits"]))
+        expected = own(Count.product(complete, header["record_bits"]))
+        need(compare(expected, header["row_bits"]) == 0, "exact complete current physical row")
+        pair_codes = own(Count(h))
+        pair_codes.increment()
+        pair_codes.multiply_small(6)
+        base_coefficients, remainder = divide(header["record_bits"], pair_codes)
+        own(base_coefficients); own(remainder)
+        need(remainder.zero(), "record_bits equals 6 r (h+1)")
+        positive(base_coefficients)
+        coefficients = own(Count.product(base_coefficients, fibre))
+        rows = own(Count.product(header["outer"], header["rows"]))
+        widths = (compact, rest, compact, rest, before,
+                  *(chunk for _ in self.vectors), after, compact)
+        return widths, rho, coefficients, rows
+
+    def rewind_field(self, field):
+        self.field_guide.rewind()
+        while self.field_guide.read() != 4:
+            need(self.field_guide.read() == 1, "complete current field guide")
+            field.move(-1)
+            self.field_guide.step(1)
+        self.field_guide.rewind()
+
+    def import_field(self, field, h):
+        """Strip actual component delimiters, preserving every signed bit."""
+        while field.read() != 4:
+            for _ in (0, 1):
+                remaining = Counter(h)
+                try:
+                    while not remaining.finished:
+                        value = field.read()
+                        need(value in (0, 1), "uniform complete signed component")
+                        self.bridge.append(value)
+                        self.field_guide.append(1)
+                        field.move(1)
+                        remaining.decrement()
+                finally:
+                    remaining.close()
+                need(field.read() == 2, "exact signed component delimiter")
+                self.field_guide.append(1)
+                field.move(1)
+        self.bridge.rewind()
+        self.rewind_field(field)
+
+    def export_field(self, field, returned, h):
+        """Reinsert the exact complete format at the unchanged common grid."""
+        returned.rewind()
+        self.field_guide.rewind()
+        while returned.read() != 4:
+            for _ in (0, 1):
+                remaining = Counter(h)
+                try:
+                    while not remaining.finished:
+                        value = returned.read()
+                        need(value in (0, 1) and field.read() in (0, 1)
+                             and self.field_guide.read() == 1, "exact returned signed component")
+                        field.write(value)
+                        field.move(1)
+                        returned.step(1)
+                        self.field_guide.step(1)
+                        remaining.decrement()
+                finally:
+                    remaining.close()
+                need(field.read() == 2 and self.field_guide.read() == 1,
+                     "same complete signed component boundary")
+                field.write(2)
+                field.move(1)
+                self.field_guide.step(1)
+        need(field.read() == self.field_guide.read() == 4, "exact full-format return frontier")
+        self.rewind_field(field)
+        self.field_guide.clear()
+        returned.rewind()
+
+    def run(self, field, context):
+        """Current CodedPort field and BinaryContextPort at their local origins.
+
+        SignedHeadroomError preserves field and context and allows a valid
+        retry. The all-size theorem concerns valid format and descriptors;
+        arbitrary malformed/interrupted execution has no rollback claim.
+        """
+        need(self.cohort.ports is not None and field.tape is not context.tape
+             and all(field.tape is not port and context.tape is not port for port in self.cohort.ports),
+             "distinct public/current-context and private physical segments")
+        self.cohort.start()
+        try:
+            with execution(), self.scope.installed(), ExitStack() as cleanup:
+                header = self.read_header(context)
+                for value in header.values():
+                    cleanup.callback(value.close)
+                h = self.component_width(field)
+                cleanup.callback(h.close)
+                widths, rho, coefficients, rows = self.prepare(header, h, cleanup)
+                self.import_field(field, h)
+                with self.scope.suspended():
+                    returned = self.engine.run(self.bridge, widths, header["f"], header["K"],
+                        header["G"], rho, h, coefficients, rows, self.inverse)
+                self.export_field(field, returned, h)
+                returned.clear()
+                erase_marker(returned)
+                self.bridge.clear()
+            self.pool.empty()
+            self.calls += 1
+        finally:
+            self.cohort.finish()
diff --git a/research/current-serial-pass-lower-bound/source/rounded-move-proof.md b/research/current-serial-pass-lower-bound/source/rounded-move-proof.md
new file mode 100644
index 0000000000..4d6b485276
--- /dev/null
+++ b/research/current-serial-pass-lower-bound/source/rounded-move-proof.md
@@ -0,0 +1,408 @@
+# Once-rounded complete raw MOVE for the selected #6030 source
+
+**Source scope matters.** This theorem binds the selected **#6030** catalogue
+retained by the all-source leaf: 22,803 source events, 3,453 raw MOVE
+occurrences and 2,886 directed chart pairs. It does not bind the proposed
+#6936 arithmetic word (71,144 events and 6,323 MOVEs). Sharing an abstract
+operator or ABI does not establish a source/recipe/caller correspondence
+between those words. There is no new κ or global assumption discharge.
+
+Canonical base is `7c49fe32c55de02c2c873655c804b16e4c3fef0a`.
+Runtime dependencies are the rounded positive wrapper at public
+`3a6b01655f9f0893cef52563a63d79b3295bc67d`, the exact direct-MOVE coordinator
+at `a61652557fa88cd0b24c1b28445cf519f6b1213e`, and their retained exact
+source/serial/cutoff packages. In particular the positive child is deliberately
+replaced by public cutoff transport
+`785000b8f400609943cd9ff04843317af4ae67a4`. The existing coordinator's
+computational bytes are unchanged; its old f-only child is not secretly
+claimed equivalent on a larger domain. This new supplier substitution is
+part of the theorem below. DEPENDENCIES.json authenticates all retained
+files; SHARED-SOURCE-JOIN.json checks the 109 reused serial-source identities.
+
+## 1. Precise domain and result
+
+Fix one exact typed raw selected #6030 entrance/PAID/exit triple admitted by
+the unchanged catalogue. Its positive rank is r in {1,...,8}; both monomial
+recipes have nine vectors. Fix positive parent column width f and retain
+the direct-branch premise **f<=t**, where t is the original cutoff. This
+claim does not cover f>t through an invented cutoff change.
+
+Write H,G,K,u,z,a for the parent's reserved H, spacing G, chunk K,
+active_start, back_start and within_bits. Retain the complete source geometry:
+
+    H,G,K >= 1; 0 <= rho < K; 0 <= e < 9;
+    (f-1)G <= H; 2H <= u;
+    u+9fK <= z; z+H <= a;
+    selected_axes = 9f+e <= d.
+
+The original header is canonical, all positive extents are positive, and
+every complete row has exactly 2^a records. There are c>=1 complex
+coefficients per record, each real/imaginary component encoded in h>=2
+two's-complement bits followed by delimiter 2. Virtual symbols retain the
+current three-bit physical code. Thus, with B=outer*rows,
+
+    b=6c(h+1), row_bits=2^a b, V=B 2^a b.
+
+All supplied work roles are initially blank at their current local origins;
+the public field, descriptor, every owned role and protected caller ancestor
+are genuinely disjoint as required by the predecessors. Fixed ordinary
+constructors satisfy the retained type, closed-state and no-observer
+contracts. They are actually constructed and charged even though no
+ordinary numerical invocation occurs on this serialized direct route.
+Every source/physical return premise of the retained exact providers remains
+explicit. The new orchestration is a source-level finite-control refinement,
+not a new flattened compiler theorem.
+
+Let U be the exact original source Clifford map, including its absolute
+phase, on all 9f native coordinates and every spectator, row and coefficient.
+Let Delta=2^-F be the original common component grid; F is a scale annotation,
+not an absent header field. Input numerators are arbitrary signed h-bit
+integers. Put g=rf and
+
+    sigma=ceil((g+1)/2)+1,  w=h+g+sigma.
+
+The completed provider returns exactly the componentwise function
+
+    R_Delta(Ux)=Delta * floor(Ux/Delta+1/2)
+
+if all rounded components fit the original h-bit range. It raises the
+explicit final `RoundedOverflow`, preserving the entire public input, if
+any one does not fit. For the stated valid geometry/physical provider domain,
+there is no extra divisibility or intermediate signed-headroom admission.
+
+For totality with an error bound, use a complete containing X-fibre which
+contains **all 9f native axes**, not merely the g Gaussian axes. If its
+actual input norm is at most R and
+
+    R+Delta/2 < 2^(h-1) Delta,
+
+then the final output fits and the primitive is total, with
+
+    ||R_Delta(Ux)-Ux||_X <= 2^((X-1)/2) Delta = eta_X.
+
+No ideal-input, input correlation, empty-helper or intermediate zero-error
+premise is used. This is a local raw-MOVE contract; caller placement,
+recursive/nonleaf admission, global precision and analytic recovery remain
+unproved here.
+
+## 2. Exact source, shared objects and the four descriptors
+
+The inherited source certificate identifies
+
+    U = L (C on g selected axes) R,
+    C = (1/2) [[1+i,1-i],[1-i,1+i]].
+
+Here the physically executed entrance is the recorded right monomial R and
+the exit is the recorded left monomial L. The selected catalogue binds the
+actual owner, raw token, rank and chronology. It does not erase nested
+remaps, replace expanded caller fragments, or accept a different #6936
+triple merely because it has the same spelling.
+
+`rounded_move_sources.py` first activates the frozen rounded-leaf closure.
+The authenticated serial discovery shim points to exactly those monomial,
+row, Count, Tape, codec and ABI objects. The unchanged direct coordinator
+then receives that serial provider, the same catalogue and ABI, and the
+explicit private-cutoff positive child. No duplicate Count/Tape classes,
+alternate tape alphabet or numerical callback is installed. These objects
+are fixed before input binding and remain fixed throughout the call.
+
+The descriptor lifetimes and permissions are:
+
+| Descriptor | Numerical width and physical sizes | Geometry/control changes | Consumer |
+|---|---|---|---|
+| Original P | h; b and row_bits | none | outer lift/setup and final return |
+| Widened P_w | w; b'=6c(w+1), row_bits'=2^a b' | other 21 fields unchanged, including f,t | direct coordinator, both serial view builders, positive view builder |
+| Serial column j | w and the same full b',row_bits' | f'=1,K'=fK,rho'=rho+jK, selected_axes'=9+e | one actual monomial call |
+| Positive view | w and the same full b',row_bits' | f'=rf,cutoff'=rt only | exact positive numeric leaf |
+
+The previous rounded-leaf package restricted P_w to its leaf use. The next
+section is a **new permission proof** for the serial monomial consumers;
+it does not edit or silently broaden that predecessor's documentation. The
+f/t-scaled positive descriptor remains strictly LEAF-private and is never
+passed to a monomial or a global row/cutoff consumer.
+
+The outer wrapper computes g from the original f. P_w retains that f;
+only the positive view scales it. Thus rank is never applied twice. No
+global cutoff is recomputed from the larger physical precision.
+
+## 3. Every serial consumer accepts the widened physical parent
+
+First, widening changes no logical address coordinate. The literal serial
+builder reads the same f,K,rho,e and emits the same column geometry. Its
+arithmetic fK and rho+jK, loop bounds, finite rank9 constant and cleanup
+are unchanged. The two enlarged physical length values are canonically
+copied into every column view, including the last one.
+
+The unchanged signed monomial `prepare` scans the actual first component,
+so it now obtains w. Its only h-dependent record equation is
+`record_bits=6c(h+1)`. With the physical b' it recovers exactly c. It checks
+`row_bits=2^a record_bits`, which holds with row_bits'. Every other geometric
+test is independent of numerical component length and is the old serial
+identity: f'=1 gives n'=0, used compact extent zero and full reserved H
+still present; all nine vector slots have width fK; the source offsets
+select exactly `u+(if+j)K+rho`; before/after intervals and the untouched
+ordinary remainder stay the same.
+
+The complete suffix after z is folded into coefficients. For the one-column
+call, its number is `c*2^(a-z)`, exactly as before widening; its physical
+record width is now `2w*c*2^(a-z)` old numerical symbols. The number of
+enumerated prefix records remains `B*2^z`. Their product is the complete
+stripped numerical field `2w c B 2^a`. No reserved suffix or coefficient is
+discarded to make the view fit. The current coded field is correspondingly
+`V'=6c(w+1)B2^a` physical bits.
+
+The engine's subsequent width consumers use this actual w in the signed
+phase scan, record layout, complete copying, digit permutations and export.
+Its only component-width lower guard is w>=2. The numerical monomial
+operations are coefficient permutations and multiplications by ±1 or ±i;
+they do not create a new hidden denominator. The n'=0 branch uses literal
+one-column digit gates, not ordinary or Compact numerical invocations.
+The complete normalization/format and private-return contracts are the same
+retained ones. The metadata checker actually executes both serial tables
+and both monomial `prepare` methods, for every tested column, at ranks1,2,8
+and f1/2 with multiplicities; it does not substitute a Python header oracle
+for those consumers.
+
+The positive child's own exact record and row checks recover c and the
+same complete rows at w. It receives g=rf, the original K and rho, and
+selects the first r native blocks across all f columns. The parent
+inequality u+9fK<=z<=a implies u+rfK<=a. Its unchanged guard compares
+rf<=rt, equivalent to the original positive f<=t. Thus all three factors
+consume physically correct widened words under their actual local guards.
+
+## 4. All exact numerical prefixes fit
+
+The paid outer codec emits g low zeros, the original h bits and sigma sign
+copies for every component, preserving every delimiter and the complete
+field. It represents `2^g m` on grid Delta/2^g, not an unpriced reinterpretation.
+
+The entrance monomial and all its serialized intermediate phase/permutation
+steps preserve the absolute value of each real/imaginary component, up to
+swapping components. Their magnitude is at most `2^(h+g-1)`, strictly below
+the widened signed boundary because sigma>=2. Consequently an entrance
+negation can never encounter the widened most-negative word. This closes
+the serial predecessor's narrower signed-domain issue, including temporary
+sign changes which could cancel only after later columns.
+
+After entrance, every component is still divisible by 2^g. Each positive
+Gaussian stage divides a signed integer linear combination by two, so after
+j stages every component is divisible by `2^(g-j)`. All g halves are exact.
+For the stored-output bound, any complete g-axis fibre after entrance has
+2^(g+1) real components bounded by `2^(h+g-1)`. Every Gaussian prefix is
+unitary, giving
+
+    |stored component| <= 2^(h+g+(g-1)/2) <= 2^(w-2).
+
+This internal bound uses only the g mixing axes. It is valid even though
+the full operator/error fibre must contain all 9f axes: entrance can
+permute values between different g-fibres, but each entry still satisfies
+the same component bound. The argument does not assume that entrance
+preserves a particular smaller g-fibre norm.
+
+The inherited fused Gaussian arithmetic uses bounded carry rather than
+storing a potentially larger four-term numerator in w bits; the bound
+above is exactly its stored-output obligation. The exit monomial again
+only permutes components and applies unit phases. Its every serialized
+intermediate has magnitude at most `2^(w-2)`, so it too cannot hit the
+widened most-negative word. All source prefixes therefore meet the larger
+**exact-prefix** domain of the direct-MOVE theorem. We do not claim they
+satisfy that predecessor's stronger sufficient L1/divisibility envelope.
+
+The complete exact coordinator returns precisely `2^g U(m)` in the widened
+field, with original absolute phase. Its positive child is exact; there is
+no intermediate rounding. Only after its exit and protected inner commit
+does the inherited dynamic-g drop run. The previous codec proof establishes
+`floor(z/2^g+1/2)` for every signed z, negative ties included, and checks
+the entire signed extension. Hence the outer final result is exactly
+R_Delta(Ux), and its only numerical rejection on the valid source/shape
+domain is true final h-bit output overflow.
+
+## 5. Final rounding, error domain and source counterexamples
+
+All 9f axes participate in the full monomial/C/monomial map. On a complete
+X-fibre containing them, U is unitary. For an actual input radius R, every
+ideal output component has magnitude at most R. One final componentwise
+round contributes at most Delta/2. The stated strict radius condition
+therefore guarantees signed fit and totality. There are 2^(X+1) real
+components, so the squared residual is at most `2^(X-1) Delta^2`, proving
+eta_X. This uses the actual input to the completed call, including errors
+from any earlier computation, without identifying it with an ideal vector.
+
+Upward rounding does not commute with a negative unit phase. We retain an
+exact selected #6030 discriminator rather than relying only on a generic
+example. At raw event9896, owner236, rank1, logical basis0 input (1,0),
+the original source's output21 is `(1/2,-1/2)`. Rounding after the complete
+exit gives `(1,0)`; rounding immediately after the positive child and then
+performing the exit gives `(0,-1)`. All512 logical outputs are compared
+using the predecessor's independent original-circuit integer evaluator,
+not the production tape kernels.
+
+A second bounded witness for the same source shows premature overflow.
+Prepare the right-monomial preimage of a vector supported on middle
+addresses1 and0 with values `(1,0)` and `(1,1)`. Every original input fits
+h=2. The positive child's early rounded pair at address1 is `(2,1)`, which
+does not fit; nevertheless every once-rounded complete original-source
+output fits h=2. The checker finds this at the third of at most16 specified
+candidates and verifies the complete source factorization. It does not
+claim the stricter radius sufficient condition for this witness. Both
+counterexamples are exact finite source algebra, not physical whole-MOVE
+executions or general impossibility theorems.
+
+## 6. Ownership, call order and full inventory
+
+The exact direct coordinator retains its own protected widened stage. The
+outer protection is not used to silently delete that stage or its invoice.
+The life order is: outer lift and header construction; complete exact
+entrance, positive child and exit; inner commit/retirement; sole final grid
+drop into the original-width stage; final public commit; retirement.
+
+The source activation and port attachment are completed before numerical
+inputs are inspected. `ExactMoveChild` accepts only the same prebound field
+and context. The outer Count/codec scopes are suspended while the exact
+coordinator and its providers run; the shared global codec is never nested.
+Live outer Count leases occupy distinct fixed roles throughout. On return
+the outer scope resumes for rounding and its own cleanup.
+
+| Fixed cohort | Ports |
+|---|---:|
+| Outer expanded field, rounded output, widened descriptor | 3 |
+| Outer metadata and two parser guides | 130 |
+| Inner protected complete widened stage | 1 |
+| Two serial descriptor banks | 90 |
+| Positive cutoff and exact numeric child | 388 |
+| Two complete monomial cohorts | Q_R+Q_L |
+| **Total** | **612+Q_R+Q_L** |
+
+The actual q2/capacity64 constructors give Q_R=Q_L=1878, hence4368 roles.
+Different admitted fixed factories retain their actual sizes and costs.
+No unused ordinary object or its marker/backing inventory is deleted.
+
+Before final commit, the original field is untouched. A named valid returned
+factor rejection first retires the inner stage, then unwinds the outer live
+counts and its stages. A true late final overflow occurs only after the
+exact inner job has returned; it similarly retires the partial rounded
+stage without a public write. Borrowed header bytes and caller ancestors
+remain intact, and every owned role returns blank at its current origin.
+These claims inherit the providers' valid-return/cleanup contracts. They
+exclude interruption, malformed input or late output, hidden overlap and
+providers violating their stated return obligations.
+
+## 7. Complete expanded invoice and historical backing
+
+Let E be the original binary descriptor length, Ew the widened parent length
+and V'=V(w+1)/(h+1). From the unchanged outer codec proof,
+
+    Ew <= E+4 ceil(log2((w+1)/(h+1))) = O(E+1).
+
+The positive view adds at most12 more physical bits. The two serial view
+loops cost H_R+H_L=O_9(f(Ew+1)); their current descriptor lengths are O(Ew+1).
+Their columns are genuinely repeated complete calls, not one free batch.
+Let P_R,j and P_L,j include every actual one-column codec, source access,
+phase/permutation, copy, encoded control, restoration and cleanup action.
+Let T_C be the full widened positive numeric bill and H_C the literal
+cutoff-view bill (`H_C<=2000Ew+20000`). The exact inner invoice is
+
+    F_inner + H_R+H_L + sum_j(P_R,j+P_L,j)
+            + H_C + T_C(g,V',w,Echild) + 22V'+35.
+
+The unchanged administrative coefficients are transfer8V'+14,
+commit9V'+14 and retire5V'+7. On a named valid returned inner failure the
+administrative subtotal is13V'+21, plus every actually attempted provider
+and descriptor operation. The outer invoice additionally charges its
+complete lift, drop, encoded setup, original-width commit9V+14, both outer
+numeric stages, widened descriptor, count markers and erasure.
+
+For the explicit unabsorbed one-column ceiling, write
+
+    R1'=2wc*2^(a-z),  M1=B*2^z,  Vraw'=M1*R1',
+    A1'=2+z+ceil(log2(R1'+1)).
+
+Vraw' is stripped old numerical length; it is not confused with the current
+coded V'. Let d_R,d_L count the fixed affine gates in the exact recipes.
+The complete upper envelope retains
+
+    F_template
+      + O_9(f*((d_R+d_L+2)*(Vraw'+M1*(A1')^6)
+                         + V'+(Ew+1)^4+Q_R+Q_L)
+             + gV'+(Ew+13)^4+Q_total+V')
+      + 22V'+35 + 9V+14.
+
+F_template includes all exact source authentication/delivery, fixed recipe
+and table compilation, the real closed ordinary constructors, complete
+fixed inventories and program storage. Outer codec/source/header passes
+are O(V'+(E+1)^4+130) with their explicit retained physical-code factors;
+the positive leaf is charged at expanded V', not the original field size.
+Every newly reached body/frontier cell and owned cleanup is paid. No factor,
+restoration, retained stage, recursive helper assumption or failed work is
+assigned zero cost.
+
+Only with the additional **expanded** long-record hypothesis
+`R1'>=(A1')^6` and control absorption `(Ew+13)^4+Q_total=O(V')` does the
+fixed source/gate/rank regime simplify to `F_template+O(fV')`.
+The old h-width hypothesis is not silently substituted for this w-width
+condition. Separately, `g<=h` implies `V'<=3V`; without such an expansion
+bound the ratio is unbounded. Neither simplification is a faster nonleaf
+tariff or a complete multiplication exponent improvement.
+
+The precision56bc938 formula `W=p+h_guard+2D+3+g_small` gives only the
+conditional arithmetic implication: if a separately established source and
+parameter correspondence identifies this h with W and places all9f native
+axes inside X<=D, then g=rf<=9f<=D<W=h. It does not establish that binding
+for this selected #6030 source, nor transfer the proposed #6936 global
+precision theorem or its S1--S5 premises.
+
+For backing, retain both full expanded stages, the original-width rounded
+stage, all descriptors and every monomial/positive/outer cohort. Add each
+predecessor's full per-role backing envelope at the widened arguments; no
+long-record or occupied-content simplification removes visited storage.
+Across completed calls, charge `sum_i max_k(origin_i(k)+B_i(k))`, including
+previous history and borrowed ancestor storage. The maxima of distinct roles
+can occur on distinct calls. Outer counts remain live while inner roles are
+active, and blank completed cohorts retain their historical maxima.
+
+## 8. Evidence and execution boundary
+
+The geometry proves `a>=3H+9fK>=12`. Thus every admitted full MOVE has at
+least4096 records and V>=73,728 bits; even the minimal lifted width has
+w>=5 and V'>=147,456 bits. The earlier exact direct-MOVE fixture at this
+minimum took815.504 seconds before widening. A finite census of all3453
+source occurrences also found that its event13096 ties event13222 for the
+minimum combined affine-gate count4. This is a gate metric, not a proof of
+minimum host runtime across all inputs/recipes.
+
+No new complete numerical whole-MOVE run was attempted. Under the explicit
+120-second/no-repeat budget, there is no smaller admitted packet to use.
+The recorded larger **structural-only** codec/admin attempt lost its session
+during parent interruption and produced no receipt; no observed exit status,
+timeout status or success is invented. It is not repeated.
+
+Six metadata cases execute actual literal serial/cutoff tables and actual
+monomial/positive preparation consumers. They do not materialize the complete
+declared numeric fields. The tiny call-order and failure controls explicitly
+replace all three numerical factor methods, use a shape **outside** the
+nine-block domain, and are labelled structural instrumentation. They execute
+the actual outer lift/drop and both protected coordinators, checking success,
+named rejection, late overflow and all4368-role retirement. They are not
+numerical MOVE evidence. The source counterexamples are exact algebraic
+checks, separately labelled. The universal result is the stated reviewed
+composition of authenticated provider contracts, not an extrapolation of
+these controls.
+
+## Open next questions
+
+1. Obtain a complete physical once-rounded selected #6030 MOVE trace under
+   an honestly enlarged budget or a separately verified faster implementation;
+   do not weaken mandatory geometry to manufacture a small witness.
+2. Bind this raw source provider at an actual typed enclosing caller and
+   prove its grid/radius, source placement, ownership and complete expanded
+   invoice. The #6030/#6936 correspondence, if desired, needs explicit proof.
+3. Establish the required expanded long-record/control or alternative full
+   cost bounds at the caller. Local component correctness does not improve κ.
+4. Close remaining nonleaf, compiler, owned-erasure and analytic recovery
+   obligations. All five global selected assumptions remain at their full
+   scopes.
+
+Prepared for @CubeJerry with substantial OpenAI assistance. Predecessor
+proofs, implementations and exact source notices remain credited and frozen.
+Independent checker logic and separate model-assisted lead review are not
+claims of independent human or proof-kernel admission.
diff --git a/research/current-serial-pass-lower-bound/source/selected_service.py b/research/current-serial-pass-lower-bound/source/selected_service.py
new file mode 100644
index 0000000000..fc3cbdc16b
--- /dev/null
+++ b/research/current-serial-pass-lower-bound/source/selected_service.py
@@ -0,0 +1,76 @@
+"""One current #6030 MOVE boundary, with its actual source monomial.
+
+The width-one phase record and its tensor convention are inherited from #6293
+and #6930. This file binds the actual source token and owner to the current
+signed-format service; it does not re-audit the primary native recorder.
+Prepared for @CubeJerry with substantial OpenAI assistance. Apache-2.0.
+"""
+import gzip
+from hashlib import sha256
+import json
+from phase_binding import HERE, authenticate, load, need
+from phase_adapter import Provider
+
+_selected = None
+EVENT = 9896
+RAW = ("MOVE", 236, 3, 7, False)
+
+
+def source_boundary():
+    global _selected
+    if _selected is not None:
+        return _selected
+    authenticate()
+    root = HERE / "vendor/selected"
+    word = json.loads(gzip.decompress((root / "WORD.json.gz").read_bytes()))
+    need(tuple(word["program"][EVENT]) == RAW, "actual selected MOVE source record")
+    ir = load("selected_phase_current_ir", HERE / "vendor/binding/vendor/lifecycle/source_ir.py")
+    events, stats = ir.current_local(word)
+    entry = next(e for e in events if e.op == "SERVICE" and e.token == ("move-in", "local", EVENT, RAW))
+    leave = next(e for e in events if e.op == "SERVICE" and e.token == ("move-out", "local", EVENT, RAW))
+    need(entry.fields == leave.fields == (236,), "actual selected field owner at both monomial cuts")
+    clifford = load("selected_phase_clifford", root / "clifford_exact.py")
+    start = clifford.canonical_frame(9, tuple(word["frames"][3]))
+    stop = clifford.canonical_frame(9, tuple(word["frames"][7]))
+    record, _compiled = clifford.lower_child(start.adjoint().then(stop))
+    need(record["rank"] == 1 and record["right"]["phase"] == 1
+         and record["left"]["phase"] == 0, "inherited #6930 actual chart record")
+    raw = json.dumps(record, sort_keys=True, separators=(",", ":")).encode()
+    report = dict(event=EVENT, raw=RAW, owner=236, rank=record["rank"],
+                  right=record["right"], left=record["left"], source_token=entry.token,
+                  record_sha256=sha256(raw).hexdigest(),
+                  source_phase_audit="unpaidmoon/integer-mult-bounds@c726399fbdb6d80dd13bed760b56572fb4ea1022",
+                  phase_algebra_inherited_from=[3087, 6293, 6930],
+                  current_source_events=stats["events"], selected_frontier_changed=False)
+    _selected = entry, leave, record, report
+    return _selected
+
+
+class Service:
+    def __init__(self, event, native_factory):
+        entry, leave, record, self.report = source_boundary()
+        need(event.op == "SERVICE" and len(event.fields) == 1 and len(event.token) >= 4,
+             "actual single-owner current MOVE service")
+        tail = event.token[-4:]
+        need(tail in (entry.token, leave.token), "fixed current source chart and occurrence token")
+        self.token, self.owner = event.token, event.fields[0]
+        self.side = "right" if tail == entry.token else "left"
+        self.provider = Provider(record[self.side], native_factory)
+        self.field = self.context = None
+
+    @property
+    def port_count(self):
+        return self.provider.port_count
+
+    def bind(self, work, fields, context):
+        need(self.owner in fields, "actual current MOVE owner has its physical field")
+        self.field, self.context = fields[self.owner], context
+        self.provider.bind(work)
+
+    def run(self):
+        need(self.field is not None, "fixed current source/field/context binding before input")
+        self.provider.run(self.field, self.context)
+
+
+if __name__ == "__main__":
+    print(json.dumps(source_boundary()[3], sort_keys=True))
diff --git a/research/current-serial-pass-lower-bound/source/serial-proof.md b/research/current-serial-pass-lower-bound/source/serial-proof.md
new file mode 100644
index 0000000000..f6097b1855
--- /dev/null
+++ b/research/current-serial-pass-lower-bound/source/serial-proof.md
@@ -0,0 +1,160 @@
+# Direct current monomials without ordinary runtime calls
+
+**Conditional enabling lemma; executed gates and complementary review passed. No new kappa.**
+Prepared for @CubeJerry with substantial OpenAI assistance. Apache-2.0.
+
+Canonical base: `7c49fe32c55de02c2c873655c804b16e4c3fef0a`.
+Exact unchanged monomial dependency:
+`CubeJerry/integer-mult-bounds@7d1ff23714e6f9182c1d0ff9214f65def2f30e04`,
+`research/current-coded-gaussian-monomial`. Every reused byte is separately
+authenticated by DEPENDENCIES.json. No retained monomial, Compact, Count,
+Tape, or ordinary constructor source is changed.
+
+## Claim, useful domain and predecessor distinction
+
+The retained monomial already has a genuine one-column branch with no ordinary
+runtime invocation. That fact and source history/action analysis are prior
+results, including [#3087](https://github.com/CrocSwap/integer-mult-bounds/pull/3087)
+and [#4172](https://github.com/CrocSwap/integer-mult-bounds/pull/4172). Current
+descriptor adaptation is the public monomial package above. Literal local
+header views are also supplied by public commit
+`772198276518065c6ae42ef4bafc77df9c3c73b3`. These mechanisms are not claimed new.
+The new implication serializes a complete valid current multi-column monomial
+through actual one-column calls, with an exact private descriptor identity,
+absolute tensor phases, a physically encoded iterator, and its repeated bill.
+
+**Conditional theorem.** On valid current geometry and the domain where every
+serialized intermediate signed phase fits, SerialProvider executes exactly
+the parent tensor monomial, including its absolute phase, without any ordinary
+runtime call. A sufficient uniform domain has every real and imaginary signed
+component strictly between -2^(h-1) and 2^(h-1). This is narrower than the
+original batched provider's success domain; see the counterexample in section4.
+
+This is a direct leaf alternative, with all costs below. It does not establish
+the faster nonleaf ordinary tariff or an accepted recursive recurrence. It
+removes a completed ordinary runtime numerical/rate premise from this route,
+while retaining its finite constructor/inventory and all digit-permutation,
+signed-phase, physical-tape, ownership and format contracts.
+
+## 1. Exact geometry and operator identity
+
+Retain the monomial provider's complete coded-field contract: uniform signed
+component width h>=2, its exact record delimiters and common quantum, supplied
+local LEFT markers and aligned origins, and actually disjoint public, context
+and private segments. Current private prefixes start physically blank; previous
+erased backing remains allocated. These are caller premises, not inferred
+from object identity or a short fixture.
+
+Let a valid parent monomial descriptor have fixed recipe rank m, positive f,K,
+0<=rho<K, active start u, back start z, address width a, positive H,G, and
+remainder e with 0<=e<m. Its selected axes are mf+e<=d. It obeys
+
+    (f-1)G <= H,  2H <= u,  u+mfK <= z,  z+H <= a.
+
+The complete row satisfies row_bits=record_bits*2^a, with unchanged outer
+count, row count, signed component width and common grid. The parent recipe
+acts on bit positions u+(if+j)K+rho, for i=0,...,m-1 and j=0,...,f-1.
+
+For column j construct a private descriptor with exactly four changed fields:
+
+    f'=1,  K'=fK,  rho'=jK+rho,  selected_axes'=m+e.
+
+All nineteen other fields remain unchanged, including e,p,d,H,G,u,z,a,
+entry_start, row_bits, record_bits, grids and cutoff. This private monomial
+view is never supplied to an ordinary provider. It need not preserve unused
+global producer relationships involving p or entry_start. Only the exact
+retained monomial consumer and its stated guards receive it.
+
+We have 0<=rho'<K' and m+e<=mf+e<=d. The used compact reservation t' is zero;
+before=u-2H and after=z-u-mfK are unchanged. Used widths become
+(0,H,0,H,before,fK,...,fK,after,0). The coefficient suffix grows to a-z,
+exactly offsetting the smaller enumerated address extent z, so no complete
+field bit is dropped. The chosen position is exactly
+u+iK'+rho'=u+(if+j)K+rho. Each actual one-column call therefore applies the
+recipe on column j, preserving every other coordinate, coefficient and row.
+
+Different columns use disjoint coordinate factors. Their complete linear maps
+commute and their product is the parent tensor monomial. The constant Gaussian
+phase occurs once per column, giving i^(f*c), not i^c. Inverse one-column maps
+likewise multiply to the inverse parent map. Equality includes absolute phase.
+
+The unchanged engine computes n=f'-1=0 and uses single_column_rows for every
+affine gate. Its flip_digit/digit_permutation route never calls compact_gate
+or the ordinary engine. Signed phases, full-field conversion/copying and
+cleanup still execute. Exact numerical success requires the stated additional
+intermediate representability condition.
+
+## 2. Physically encoded descriptor iteration
+
+column_view.py emits finite PREPARE, NEXT and RELEASE tables from the unchanged
+Builder. Runtime instructions are local symbol reads/writes, unit moves,
+jumps and two fixed terminal labels. Forty-five fixed private raw binary ports
+hold decoded fields, saved f and K, a counter, sum and private child view.
+No runtime shape is decoded into a Python integer or used to allocate work.
+
+PREPARE decodes 23 canonical fields, checks positive f,K and computes fK by
+physically encoded repeated addition of K, comparing an encoded counter to f.
+It writes f'=1 and m+e, resets j=0 and emits the first view. NEXT destroys the
+private view, increments j and compares it with f. For j<f it adds old K to
+rho' and encodes another complete view; at equality it returns `finished`.
+RELEASE clears all current private prefixes and restores origins. The wrapper
+invokes one real unchanged monomial provider between `ready` and NEXT.
+
+The provider is constructed/bound once and never reset or recreated between
+columns; its closed ordinary object remains allocated. Parent bytes and all
+ancestor prefixes are read-only. Valid parent geometry is an input premise,
+not a consequence of checking canonical encoding and positive f,K.
+
+Let E be the original descriptor length. bitlength(fK)<=bitlength(f)+bitlength(K)
+and bitlength(jK+rho)<=bitlength(fK), so child and working lengths are O(E+1).
+PREPARE costs O(f(E+1)), each NEXT O(E+1), and RELEASE O(E+1). Thus metadata
+cost is O(f(E+1)), with O(E+1) current backing per fixed role. Historical
+backing remains counted. Later small calls scan their current prefixes and
+receive no free allocator/history reset.
+
+## 3. Full optimistic invoice and useful asymptotic domain
+
+Write C=outer*rows, R1=2hr*2^(a-z), M1=C*2^z, Vraw=M1*R1,
+and A1=2+z+ceil(log2(R1+1)). Let g count the finite affine gates and V be the
+complete coded field length. Each one-column call pays its entire inherited
+bill, codec, encoded setup and retirement, hence
+
+    F_template + O_m(f*((g+1)*(Vraw+M1*A1^6) + V + (E+1)^4 + Q)).
+
+Q includes the complete fixed work inventory, including unused ordinary
+tapes. Setup is paid f times; provider/ancestor historical maxima remain in
+the space bill. No ordinary cost is subtracted from an unrelated upper bound.
+Under explicit R1>=A1^6 and (E+1)^4+Q=O(V), this is F_template+O_m(fV).
+The larger displayed bill remains if either absorption condition fails.
+
+This can match a direct PAID-leaf budget when a separate global cutoff admits
+the complete source construction, including rf<=cutoff for a rank-r leaf.
+No such cutoff, compiled stock/precision substitution, new supplier rate or
+assembled kappa is established here.
+
+## 4. Strict numerical-domain distinction and rejection
+
+Phases act as signed permutations of the real/imaginary components. Strict
+symmetric component headroom is invariant under every such phase and address
+permutation, proving all intermediate representability in the sufficient
+domain. The unchanged common grid needs no extra arithmetic rounding.
+
+The original combined-phase admission does not suffice. For a constant-phase-2
+monomial with f=2, the tensor phase is +1, so a most-negative h-bit component
+can pass the batched phase. The first serialized column multiplies it by -1,
+which cannot fit. Thus the two acceptance domains are provably different.
+For the actual selected right recipe, whose constant is1, f=4 and an input
+supported on the all-zero selected bits similarly has combined phase +1;
+serial quarter rotations can expose an unrepresentable intermediate negation.
+This caveat was found by the separate native worker's adversarial review.
+
+Each retained one-column call preserves its input on its named arithmetic
+rejection. Earlier completed columns can nevertheless have changed the serial
+field. SerialProvider therefore has no whole-job rollback guarantee. A full
+protected stage, such as the separately published atomic MOVE wrapper, must
+pay transfer/commit/retirement to obtain that property. No interruption or
+malformed-success rollback is claimed.
+
+Global native source correctness, the full compiler placement, ownership,
+precision and analytic multiplication assumptions remain. Finite witnesses
+do not discharge those universal premises, and no accepted certificate changes.
diff --git a/research/current-serial-pass-lower-bound/verify.py b/research/current-serial-pass-lower-bound/verify.py
new file mode 100644
index 0000000000..40344f07d9
--- /dev/null
+++ b/research/current-serial-pass-lower-bound/verify.py
@@ -0,0 +1,194 @@
+"""Source-only replay of mandatory serial full-field passes. No native run.
+Prepared for @CubeJerry with substantial OpenAI assistance. Apache-2.0.
+"""
+import ast
+import copy
+import gzip
+import hashlib
+import importlib.util
+import json
+from pathlib import Path
+import sys
+
+HERE = Path(__file__).resolve().parent
+
+
+def need(ok, message):
+    if not ok:
+        raise ValueError(message)
+
+
+def authenticate():
+    manifest = json.loads((HERE/'DEPENDENCIES.json').read_text())
+    for row in manifest['files']:
+        raw = (HERE/row['path']).read_bytes()
+        need(len(raw) == row['bytes'] and hashlib.sha256(raw).hexdigest() == row['sha256']
+             and hashlib.sha1(b'blob '+str(len(raw)).encode()+b'\0'+raw).hexdigest() == row['git_blob'],
+             'immutable source '+row['path'])
+    return len(manifest['files'])
+
+
+def method(tree, cls, name):
+    c = next(n for n in tree.body if isinstance(n, ast.ClassDef) and n.name == cls)
+    return next(n for n in c.body if isinstance(n, ast.FunctionDef) and n.name == name)
+
+
+def calls(node, name):
+    return sorted((n for n in ast.walk(node) if isinstance(n, ast.Call)
+                   and ast.unparse(n.func) == name), key=lambda n: n.lineno)
+
+
+def four_traversals(tree):
+    importer = method(tree, 'Provider', 'import_field')
+    exporter = method(tree, 'Provider', 'export_field')
+    rewind = method(tree, 'Provider', 'rewind_field')
+    run = method(tree, 'Provider', 'run')
+    for part in (importer, exporter):
+        need(len(calls(part, 'self.rewind_field')) == 1, 'one complete return per codec direction')
+        need(any(isinstance(n, ast.Expr) and isinstance(n.value, ast.Call)
+                 and ast.unparse(n.value.func) == 'self.rewind_field' for n in part.body),
+             'return outside the data loop')
+        advance = calls(part, 'field.move')
+        need(len(advance) == 2 and all(ast.literal_eval(n.args[0]) == 1 for n in advance),
+             'data and delimiter forward movement')
+    back = calls(rewind, 'field.move')
+    need(len(back) == 1 and ast.literal_eval(back[0].args[0]) == -1,
+         'per-guide-marker backward movement')
+    keys = ('self.import_field', 'self.engine.run', 'self.export_field')
+    ordered = [calls(run, key) for key in keys]
+    need(all(len(v) == 1 for v in ordered)
+         and [v[0].lineno for v in ordered] == sorted(v[0].lineno for v in ordered),
+         'import, actual engine, export in fixed order')
+    return True
+
+
+def literal_coded_costs():
+    tree = ast.parse((HERE/'source/machine.py').read_bytes())
+    nodes = [n for n in tree.body if isinstance(n, (ast.FunctionDef, ast.ClassDef))
+             and n.name in ('need', 'emit', 'CodedPort')]
+    env = {'ZERO': 0, 'ONE': 1, 'LEFT': 2, 'BLANK': 6}
+    exec(compile(ast.Module(body=nodes, type_ignores=[]), '<pinned literal CodedPort>', 'exec'), env)
+
+    class Meter:
+        def __init__(self):
+            self.cells = [2]+[0]*15
+            self.head = 4
+            self.count = [0, 0, 0]
+        def read(self):
+            self.count[0] += 1
+            return self.cells[self.head]
+        def write(self, value):
+            self.count[1] += 1
+            self.cells[self.head] = value
+        def move(self, direction):
+            need(direction in (-1, 1), 'unit primitive')
+            self.count[2] += 1
+            self.head += direction
+
+    result = {}
+    for label, op in [('forward', lambda p: p.move(1)),
+                      ('backward', lambda p: p.move(-1)),
+                      ('write', lambda p: p.write(2)),
+                      ('read', lambda p: p.read())]:
+        t = Meter();op(env['CodedPort'](t));result[label] = t.count
+    need(result == dict(forward=[1,0,3], backward=[1,0,3], write=[0,3,6], read=[4,0,6]),
+         'literal coded primitive costs')
+    return result
+
+
+def source_recipe():
+    word = json.loads(gzip.decompress((HERE/'source/WORD.json.gz').read_bytes()))
+    raw = ['MOVE', 236, 3, 7, False]
+    need(word['program'][9896] == raw and type(word['program'][9896][-1]) is bool,
+         'exact selected raw occurrence')
+    spec = importlib.util.spec_from_file_location('serial_lower_retained_clifford', HERE/'source/clifford_exact.py')
+    C = importlib.util.module_from_spec(spec);sys.modules[spec.name] = C;spec.loader.exec_module(C)
+    a = C.canonical_frame(9, tuple(word['frames'][3]))
+    b = C.canonical_frame(9, tuple(word['frames'][7]))
+    rec, _ = C.lower_child(a.adjoint().then(b))
+    recipe = rec['right']
+    need(len(recipe['matrix_rows']) == 9 and recipe['phase'] == 1 and rec['rank'] == 1,
+         'nontrivial actual right recipe; child rank differs from monomial rank')
+    return dict(event=9896, raw=raw, monomial_rank=9, positive_child_rank=rec['rank'],
+                right=recipe, recipe_sha256=hashlib.sha256(json.dumps(recipe, sort_keys=True,
+                separators=(',', ':')).encode()).hexdigest())
+
+
+def family(f):
+    return dict(outer=1, rows=1, stock=1, h=2, d=9*f, selected_axes=9*f, p=9*f,
+                D=9*f, remainder=0, K=1, G=1, rho=0, H=f,
+                active_start=2*f, entry_start=2*f, back_start=11*f,
+                within_bits=12*f, record_bits=18, row_bits=18 << (12*f),
+                q0=0, qF=0, qB=0, cutoff=145, f=f)
+
+
+def admitted(v):
+    m = 9
+    need(all(type(x) is int and x >= 0 for x in v.values()), 'nonnegative canonical integers')
+    need(all(v[k] > 0 for k in ('outer','rows','row_bits','record_bits','f','K','G','H')),
+         'positive consumed parameters')
+    need(v['h'] >= 2 and v['rho'] < v['K'], 'signed width and residue')
+    need((v['f']-1)*v['G'] <= v['H'] and 2*v['H'] <= v['active_start'], 'front reservations')
+    need(v['active_start']+m*v['f']*v['K'] <= v['back_start'], 'active axis extent')
+    need(v['back_start']+v['H'] <= v['within_bits'], 'entire back reservation')
+    need(m*v['f']+v['remainder'] == v['selected_axes'] <= v['d']
+         and v['remainder'] < m, 'selected dimensions')
+    need(v['row_bits'] == v['record_bits'] << v['within_bits'], 'complete row')
+    need(v['record_bits'] % (6*(v['h']+1)) == 0, 'whole positive coefficient records')
+    return True
+
+
+def main():
+    retained = authenticate()
+    phase = ast.parse((HERE/'source/phase_adapter.py').read_bytes())
+    four_traversals(phase)
+    serial = ast.parse((HERE/'source/column_view.py').read_bytes())
+    run = method(serial, 'SerialProvider', 'run')
+    need(len(calls(run, 'self.native.run')) == len(calls(run, 'self.view.advance')) == 1,
+         'one native invocation per encoded iterator cycle')
+    need(not any(isinstance(n, ast.Constant) and n.value == 'cutoff' for n in ast.walk(phase)),
+         'monomial adapter does not consume cutoff')
+    mutant = copy.deepcopy(phase)
+    ex = method(mutant, 'Provider', 'export_field')
+    ex.body = [n for n in ex.body if not (isinstance(n, ast.Expr) and isinstance(n.value, ast.Call)
+               and ast.unparse(n.value.func) == 'self.rewind_field')]
+    controls = []
+    try: four_traversals(mutant)
+    except ValueError: controls.append('missing_export_rewind')
+    else: raise ValueError('missing rewind escaped structure control')
+    count = 0
+    for f in list(range(128, 641))+[1024,2048,4096]:
+        v=family(f);admitted(v)
+        V=v['row_bits'];Vraw=4 << (12*f)
+        need(2*V == 9*Vraw and v['d'] == 9*f, 'actual volume and dimension identities')
+        need((1 << (f+2)) >= (12*f+5)**6, 'long-record member')
+        for j in (0, f//2, f-1):
+            child=dict(v,f=1,K=f,rho=j,selected_axes=9)
+            admitted(child)
+            need(all(child['active_start']+i*child['K']+child['rho']
+                     == v['active_start']+(i*f+j)*v['K'] for i in range(9)), 'all9 coordinate positions')
+        count += 1
+    need(129**6 < 2*128**6 and (1 << 130) >= 1541**6,
+         'exact induction base and uniform ratio premise')
+    for key, bad in [('H',126),('active_start',255),('back_start',1407),
+                     ('row_bits',18),('d',1151),('rho',1)]:
+        v=family(128);v[key]=bad
+        try: admitted(v)
+        except ValueError: controls.append('invalid_'+key)
+        else: raise ValueError(('invalid family escaped',key))
+    v=family(146);admitted(v)
+    need(v['f'] > v['cutoff'], 'local family does not imply fixed-cutoff MOVE admission')
+    controls.append('fixed_cutoff_scope')
+    need(family(128)['row_bits']//128 != family(128)['row_bits'], 'f-divided field is not complete volume')
+    controls.append('false_f_divided_volume')
+    result=dict(status='PASS_SERIAL_MANDATORY_FIELD_PASSES',retained_files=retained,
+                source=source_recipe(),primitive_costs=literal_coded_costs(),
+                family_members=count,controls=controls,
+                lower_per_fV=dict(physical_moves='4',physical_reads='4/3',physical_writes='1'),
+                numerical_native_execution=False,full_supplier_family_proved=False,
+                fixed_leaf_budget_refuted=False,new_kappa=False)
+    print(json.dumps(result,sort_keys=True))
+
+
+if __name__ == '__main__':
+    main()