From ddaf7234581133ec0c15496f4dfc65570aef401c Mon Sep 17 00:00:00 2001
From: dot <dot@localhost>
Date: Thu, 15 Oct 2026 01:33:30 -0700
Subject: [PATCH] [Lean] Pay positioned paired-track acquisition and global
 return

Publish accepted three-tape paired-store acquisition and global return with entrance-volume bounds.
---
 .../ACCEPTANCE.json                           | 413 ++++++++++++++++
 .../PUBLIC_SOURCE_MANIFEST.json               | 463 ++++++++++++++++++
 .../README.md                                 |  44 ++
 .../REPRODUCTION.md                           |  67 +++
 .../sources/PackedMetadataSlots.lean          | 284 +++++++++++
 .../PaidPairedAcquisitionResources.lean       | 121 +++++
 .../sources/PaidPairedTrackAcquisition.lean   | 210 ++++++++
 .../sources/PairedTrackExtraction.lean        | 260 ++++++++++
 .../sources/PairedTrackExtractionFraming.lean | 157 ++++++
 .../sources/PositionalMetadataAccess.lean     | 312 ++++++++++++
 .../sources/PositionalMetadataReturn.lean     | 317 ++++++++++++
 11 files changed, 2648 insertions(+)
 create mode 100644 research/lean-paid-positioned-acquisition/ACCEPTANCE.json
 create mode 100644 research/lean-paid-positioned-acquisition/PUBLIC_SOURCE_MANIFEST.json
 create mode 100644 research/lean-paid-positioned-acquisition/README.md
 create mode 100644 research/lean-paid-positioned-acquisition/REPRODUCTION.md
 create mode 100644 research/lean-paid-positioned-acquisition/sources/PackedMetadataSlots.lean
 create mode 100644 research/lean-paid-positioned-acquisition/sources/PaidPairedAcquisitionResources.lean
 create mode 100644 research/lean-paid-positioned-acquisition/sources/PaidPairedTrackAcquisition.lean
 create mode 100644 research/lean-paid-positioned-acquisition/sources/PairedTrackExtraction.lean
 create mode 100644 research/lean-paid-positioned-acquisition/sources/PairedTrackExtractionFraming.lean
 create mode 100644 research/lean-paid-positioned-acquisition/sources/PositionalMetadataAccess.lean
 create mode 100644 research/lean-paid-positioned-acquisition/sources/PositionalMetadataReturn.lean

diff --git a/research/lean-paid-positioned-acquisition/ACCEPTANCE.json b/research/lean-paid-positioned-acquisition/ACCEPTANCE.json
new file mode 100644
index 0000000000..2ea8486aa7
--- /dev/null
+++ b/research/lean-paid-positioned-acquisition/ACCEPTANCE.json
@@ -0,0 +1,413 @@
+{
+  "schema": "public-source-bound-acceptance-v1",
+  "lean_version": "4.21.0",
+  "mathlib_commit": "308445d7985027f538e281e18df29ca16ede2ba3",
+  "summary": "Seven unchanged independently accepted roots; complete standard-only axiom probes and printed theorem types.",
+  "modules": [
+    {
+      "module": "PairedTrackExtraction",
+      "source_sha256": "37a4b7c94d721a69994e23f4297e16d31d0b71d7ca3c0c3ae8e01a91d6ef7c68",
+      "source_bytes": 12842,
+      "independent_reviewer": "prove_main_analytic_assembly",
+      "result": "PASS",
+      "probes": [
+        {
+          "declaration": "CurrentMain.PairedTrackExtraction.model_step",
+          "axioms": [
+            "propext"
+          ]
+        },
+        {
+          "declaration": "CurrentMain.PairedTrackExtraction.model_run",
+          "axioms": [
+            "propext"
+          ]
+        },
+        {
+          "declaration": "CurrentMain.PairedTrackExtraction.extraction_result",
+          "axioms": [
+            "propext",
+            "Quot.sound"
+          ]
+        },
+        {
+          "declaration": "CurrentMain.PairedTrackExtraction.extraction_storage",
+          "axioms": [
+            "propext",
+            "Classical.choice",
+            "Quot.sound"
+          ]
+        },
+        {
+          "declaration": "CurrentMain.PairedTrackExtraction.output_value",
+          "axioms": [
+            "propext",
+            "Quot.sound"
+          ]
+        }
+      ],
+      "printed_full_types": "CurrentMain.PairedTrackExtraction.extraction_result : ∀ (second : Bool) (rows : List CurrentMain.PairedBitXorScan.Pair)\n  (r : SequentialBitAddition.Registers),\n  CurrentMain.PairedTrackExtraction.run second (6 * rows.length + 16)\n        (CurrentMain.PairedTrackExtraction.initial rows r) =\n      CurrentMain.PairedTrackExtraction.final second rows ∧\n    (CurrentMain.PairedTrackExtraction.final second rows).phase = CurrentMain.PairedTrackExtraction.Phase.halt ∧\n      ∀ k < 6 * rows.length + 16,\n        (CurrentMain.PairedTrackExtraction.run second k (CurrentMain.PairedTrackExtraction.initial rows r)).phase ≠\n          CurrentMain.PairedTrackExtraction.Phase.halt\nCurrentMain.PairedTrackExtraction.output_value : ∀ (second : Bool) (rows : List CurrentMain.PairedBitXorScan.Pair)\n  (r : SequentialBitAddition.Registers),\n  (CurrentMain.PairedTrackExtraction.run second (6 * rows.length + 16)\n          (CurrentMain.PairedTrackExtraction.initial rows r)).source =\n      { left := [], right := CurrentMain.MarkedBitXorScan.marked rows } ∧\n    (CurrentMain.PairedTrackExtraction.run second (6 * rows.length + 16)\n          (CurrentMain.PairedTrackExtraction.initial rows r)).output =\n      MarkedZeroPadding.marked\n        (MarkedZeroPadding.bits (List.map (CurrentMain.PairedTrackExtraction.chosen second) rows))\n",
+      "printed_type_count": 2,
+      "warnings": [],
+      "errors": []
+    },
+    {
+      "module": "PairedTrackExtractionFraming",
+      "source_sha256": "1281ce4b355eaac7944485406de2bfb48e9f9ddf0bb30b2d990702ed23c3dc29",
+      "source_bytes": 8836,
+      "independent_reviewer": "prove_main_analytic_assembly",
+      "result": "PASS",
+      "probes": [
+        {
+          "declaration": "CurrentMain.PairedTrackExtractionFraming.confined_step",
+          "axioms": [
+            "propext"
+          ]
+        },
+        {
+          "declaration": "CurrentMain.PairedTrackExtractionFraming.step_embed",
+          "axioms": [
+            "propext",
+            "Quot.sound"
+          ]
+        },
+        {
+          "declaration": "CurrentMain.PairedTrackExtractionFraming.run_embed",
+          "axioms": [
+            "propext",
+            "Quot.sound"
+          ]
+        },
+        {
+          "declaration": "CurrentMain.PairedTrackExtractionFraming.cells_embed",
+          "axioms": [
+            "propext",
+            "Quot.sound"
+          ]
+        },
+        {
+          "declaration": "CurrentMain.PairedTrackExtractionFraming.framed_result",
+          "axioms": [
+            "propext",
+            "Quot.sound"
+          ]
+        },
+        {
+          "declaration": "CurrentMain.PairedTrackExtractionFraming.framed_storage",
+          "axioms": [
+            "propext",
+            "Classical.choice",
+            "Quot.sound"
+          ]
+        }
+      ],
+      "printed_full_types": "CurrentMain.PairedTrackExtractionFraming.framed_result : ∀ (second : Bool)\n  (left right : List CurrentMain.PairedTrackExtraction.Symbol) (rows : List CurrentMain.PairedBitXorScan.Pair)\n  (r : SequentialBitAddition.Registers),\n  CurrentMain.PairedTrackExtraction.run second (6 * rows.length + 16)\n        (CurrentMain.PairedTrackExtractionFraming.embed left right (CurrentMain.PairedTrackExtraction.initial rows r)) =\n      CurrentMain.PairedTrackExtractionFraming.embed left right (CurrentMain.PairedTrackExtraction.final second rows) ∧\n    ∀ k < 6 * rows.length + 16,\n      (CurrentMain.PairedTrackExtraction.run second k\n            (CurrentMain.PairedTrackExtractionFraming.embed left right\n              (CurrentMain.PairedTrackExtraction.initial rows r))).phase ≠\n        CurrentMain.PairedTrackExtraction.Phase.halt\nCurrentMain.PairedTrackExtractionFraming.framed_storage : ∀ (second : Bool)\n  (left right : List CurrentMain.PairedTrackExtraction.Symbol) (rows : List CurrentMain.PairedBitXorScan.Pair)\n  (r : SequentialBitAddition.Registers) (k : ℕ),\n  CurrentMain.PairedTrackExtraction.cells\n      (CurrentMain.PairedTrackExtraction.run second k\n        (CurrentMain.PairedTrackExtractionFraming.embed left right\n          (CurrentMain.PairedTrackExtraction.initial rows r))) ≤\n    left.length + (2 * rows.length + 4) + right.length\n",
+      "printed_type_count": 2,
+      "warnings": [],
+      "errors": []
+    },
+    {
+      "module": "PackedMetadataSlots",
+      "source_sha256": "50bd27baab6a2ded29a72f4af963b55fbaef3da6fc9895b663cad3c34b9d23ca",
+      "source_bytes": 13400,
+      "independent_reviewer": "integration",
+      "result": "PASS",
+      "probes": [
+        {
+          "declaration": "CurrentMain.PackedMetadataSlots.locate_spec",
+          "axioms": [
+            "propext"
+          ]
+        },
+        {
+          "declaration": "CurrentMain.PackedMetadataSlots.locate_none",
+          "axioms": [
+            "propext",
+            "Quot.sound"
+          ]
+        },
+        {
+          "declaration": "CurrentMain.PackedMetadataSlots.locate_unique",
+          "axioms": [
+            "propext",
+            "Quot.sound"
+          ]
+        },
+        {
+          "declaration": "CurrentMain.PackedMetadataSlots.pack_capacity",
+          "axioms": [
+            "propext",
+            "Quot.sound"
+          ]
+        },
+        {
+          "declaration": "CurrentMain.PackedMetadataSlots.uniform_capacity",
+          "axioms": [
+            "propext",
+            "Quot.sound"
+          ]
+        },
+        {
+          "declaration": "CurrentMain.PackedMetadataSlots.focus_pack",
+          "axioms": [
+            "propext"
+          ]
+        },
+        {
+          "declaration": "CurrentMain.PackedMetadataSlots.run_focused",
+          "axioms": [
+            "propext",
+            "Quot.sound"
+          ]
+        },
+        {
+          "declaration": "CurrentMain.PackedMetadataSlots.run_repacked",
+          "axioms": [
+            "propext",
+            "Quot.sound"
+          ]
+        },
+        {
+          "declaration": "CurrentMain.PackedMetadataSlots.located_storage",
+          "axioms": [
+            "propext",
+            "Quot.sound"
+          ]
+        },
+        {
+          "declaration": "CurrentMain.PackedMetadataSlots.metadata_avoids",
+          "axioms": [
+            "propext"
+          ]
+        },
+        {
+          "declaration": "CurrentMain.PackedMetadataSlots.located_toggle",
+          "axioms": [
+            "propext",
+            "Classical.choice",
+            "Quot.sound"
+          ]
+        },
+        {
+          "declaration": "CurrentMain.PackedMetadataSlots.located_clear",
+          "axioms": [
+            "propext",
+            "Classical.choice",
+            "Quot.sound"
+          ]
+        }
+      ],
+      "printed_full_types": "CurrentMain.PackedMetadataSlots.located_toggle : ∀ (ambient : ℕ → ℕ) (key : ℕ)\n  (blocks : List CurrentMain.PackedMetadataSlots.Block) (f : CurrentMain.PackedMetadataSlots.Focus),\n  CurrentMain.PackedMetadataSlots.locate key blocks = some f →\n    CurrentMain.PackedMetadataSlots.toggleAt key blocks = some (CurrentMain.PackedMetadataSlots.replaced f) ∧\n      CurrentMain.PackedMetadataSlots.keys (CurrentMain.PackedMetadataSlots.replaced f) =\n          CurrentMain.PackedMetadataSlots.keys blocks ∧\n        CurrentMain.PackedMetadataSlots.metadata ambient (CurrentMain.PackedMetadataSlots.replaced f) =\n          Function.update (CurrentMain.PackedMetadataSlots.metadata ambient blocks) key\n            (CurrentMain.PackedMetadataSlots.metadata ambient blocks key ^^^\n              CurrentMain.PackedMetadataSlots.sourceValue f.selected)\nCurrentMain.PackedMetadataSlots.located_storage : ∀ (key : ℕ) (blocks : List CurrentMain.PackedMetadataSlots.Block)\n  (f : CurrentMain.PackedMetadataSlots.Focus),\n  CurrentMain.PackedMetadataSlots.locate key blocks = some f →\n    ∀ (k : ℕ),\n      CurrentMain.MarkedBitXorScan.cells\n          (CurrentMain.MarkedBitXorScan.run k (CurrentMain.PackedMetadataSlots.focusState f)) =\n        CurrentMain.PackedMetadataSlots.capacity blocks\n",
+      "printed_type_count": 2,
+      "warnings": [
+        "PackedMetadataSlots.lean:146:108: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice",
+        "note: this linter can be disabled with `set_option linter.unnecessarySeqFocus false`",
+        "PackedMetadataSlots.lean:197:70: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice",
+        "note: this linter can be disabled with `set_option linter.unnecessarySeqFocus false`"
+      ],
+      "errors": []
+    },
+    {
+      "module": "PositionalMetadataAccess",
+      "source_sha256": "1854ed8040ebbe2a00ef54ddefa84f82bd8dc26eb5aff3418dab68cb8a31ce60",
+      "source_bytes": 15608,
+      "independent_reviewer": "integration",
+      "result": "PASS",
+      "probes": [
+        {
+          "declaration": "CurrentMain.PositionalMetadataAccess.access_exact",
+          "axioms": [
+            "propext",
+            "Quot.sound"
+          ]
+        },
+        {
+          "declaration": "CurrentMain.PositionalMetadataAccess.access_result",
+          "axioms": [
+            "propext",
+            "Quot.sound"
+          ]
+        },
+        {
+          "declaration": "CurrentMain.PositionalMetadataAccess.access_first_halt",
+          "axioms": [
+            "propext",
+            "Quot.sound"
+          ]
+        },
+        {
+          "declaration": "CurrentMain.PositionalMetadataAccess.access_storage",
+          "axioms": [
+            "propext",
+            "Quot.sound"
+          ]
+        },
+        {
+          "declaration": "CurrentMain.PositionalMetadataAccess.access_from_locate",
+          "axioms": [
+            "propext",
+            "Quot.sound"
+          ]
+        }
+      ],
+      "printed_full_types": "CurrentMain.PositionalMetadataAccess.access_from_locate : ∀ (key : ℕ)\n  (blocks : List CurrentMain.PackedMetadataSlots.Block) (f : CurrentMain.PackedMetadataSlots.Focus),\n  CurrentMain.PackedMetadataSlots.locate key blocks = some f →\n    ∀ (scratch : Bool),\n      let out :=\n        CurrentMain.PositionalMetadataAccess.run\n          (CurrentMain.PackedMetadataSlots.capacity f.before + 2 * f.before.length + 4)\n          (CurrentMain.PositionalMetadataAccess.initial f.before.length blocks scratch);\n      out.dataTape = (CurrentMain.PackedMetadataSlots.focusState f).tape ∧\n        out.controlTape = CurrentMain.PositionalMetadataAccess.unary f.before.length ∧\n          out.scratch = scratch ∧ out.phase = CurrentMain.PositionalMetadataAccess.Phase.halt\nCurrentMain.PositionalMetadataAccess.access_storage : ∀ (pre : List CurrentMain.PackedMetadataSlots.Block)\n  (selected : CurrentMain.PackedMetadataSlots.Block) (post : List CurrentMain.PackedMetadataSlots.Block)\n  (scratch : Bool) (k : ℕ),\n  CurrentMain.PositionalMetadataAccess.cells\n      (CurrentMain.PositionalMetadataAccess.run k\n        (CurrentMain.PositionalMetadataAccess.initial pre.length (pre ++ selected :: post) scratch)) =\n    CurrentMain.PackedMetadataSlots.capacity (pre ++ selected :: post) + (pre.length + 2)\n",
+      "printed_type_count": 2,
+      "warnings": [],
+      "errors": []
+    },
+    {
+      "module": "PositionalMetadataReturn",
+      "source_sha256": "e1721065fb10b9576fd0d7e9539f25567981d09fdb4796bd9d32fa8dded799a6",
+      "source_bytes": 15425,
+      "independent_reviewer": "integration",
+      "result": "PASS",
+      "probes": [
+        {
+          "declaration": "CurrentMain.PositionalMetadataReturn.return_exact",
+          "axioms": [
+            "propext",
+            "Quot.sound"
+          ]
+        },
+        {
+          "declaration": "CurrentMain.PositionalMetadataReturn.return_result",
+          "axioms": [
+            "propext",
+            "Quot.sound"
+          ]
+        },
+        {
+          "declaration": "CurrentMain.PositionalMetadataReturn.return_first_halt",
+          "axioms": [
+            "propext",
+            "Quot.sound"
+          ]
+        },
+        {
+          "declaration": "CurrentMain.PositionalMetadataReturn.return_storage",
+          "axioms": [
+            "propext",
+            "Quot.sound"
+          ]
+        }
+      ],
+      "printed_full_types": "CurrentMain.PositionalMetadataReturn.return_result : ∀ (pre : List CurrentMain.PackedMetadataSlots.Block)\n  (selected : CurrentMain.PackedMetadataSlots.Block) (post : List CurrentMain.PackedMetadataSlots.Block)\n  (scratch : Bool),\n  CurrentMain.PositionalMetadataReturn.run (CurrentMain.PackedMetadataSlots.capacity pre + 2 * pre.length + 4)\n      (CurrentMain.PositionalMetadataReturn.initial pre selected post scratch) =\n    CurrentMain.PositionalMetadataReturn.final pre.length (pre ++ selected :: post) scratch\n",
+      "printed_type_count": 1,
+      "warnings": [],
+      "errors": []
+    },
+    {
+      "module": "PaidPairedTrackAcquisition",
+      "source_sha256": "8ecf7909570e003a9d1e03c0dd920c024457aed2ee1e427dde89c2ed228b1507",
+      "source_bytes": 12843,
+      "independent_reviewer": "prove_main_analytic_assembly",
+      "result": "PASS",
+      "probes": [
+        {
+          "declaration": "CurrentMain.PaidPairedTrackAcquisition.enter_extraction",
+          "axioms": [
+            "propext",
+            "Quot.sound"
+          ]
+        },
+        {
+          "declaration": "CurrentMain.PaidPairedTrackAcquisition.home_handoff",
+          "axioms": []
+        },
+        {
+          "declaration": "CurrentMain.PaidPairedTrackAcquisition.machine_result",
+          "axioms": [
+            "propext",
+            "Quot.sound"
+          ]
+        },
+        {
+          "declaration": "CurrentMain.PaidPairedTrackAcquisition.time_eq",
+          "axioms": [
+            "propext",
+            "Quot.sound"
+          ]
+        },
+        {
+          "declaration": "CurrentMain.PaidPairedTrackAcquisition.initial_cells",
+          "axioms": [
+            "propext",
+            "Quot.sound"
+          ]
+        },
+        {
+          "declaration": "CurrentMain.PaidPairedTrackAcquisition.acquisition_from_locate",
+          "axioms": [
+            "propext",
+            "Quot.sound"
+          ]
+        }
+      ],
+      "printed_full_types": "CurrentMain.PaidPairedTrackAcquisition.machine_result : ∀ (second : Bool)\n  (pre : List CurrentMain.PackedMetadataSlots.Block) (selected : CurrentMain.PackedMetadataSlots.Block)\n  (post : List CurrentMain.PackedMetadataSlots.Block) (scratch : Bool) (r : SequentialBitAddition.Registers),\n  CurrentMain.PaidPairedTrackAcquisition.run second (CurrentMain.PaidPairedTrackAcquisition.totalTime pre selected)\n        (CurrentMain.PaidPairedTrackAcquisition.initial pre.length (pre ++ selected :: post) scratch r) =\n      CurrentMain.PaidPairedTrackAcquisition.final second pre selected post scratch ∧\n    CurrentMain.PaidPairedTrackAcquisition.Halted\n        (CurrentMain.PaidPairedTrackAcquisition.final second pre selected post scratch) ∧\n      ∀ k < CurrentMain.PaidPairedTrackAcquisition.totalTime pre selected,\n        ¬CurrentMain.PaidPairedTrackAcquisition.Halted\n            (CurrentMain.PaidPairedTrackAcquisition.run second k\n              (CurrentMain.PaidPairedTrackAcquisition.initial pre.length (pre ++ selected :: post) scratch r))\nCurrentMain.PaidPairedTrackAcquisition.acquisition_from_locate : ∀ (second : Bool) (key : ℕ)\n  (blocks : List CurrentMain.PackedMetadataSlots.Block) (f : CurrentMain.PackedMetadataSlots.Focus),\n  CurrentMain.PackedMetadataSlots.locate key blocks = some f →\n    ∀ (scratch : Bool) (r : SequentialBitAddition.Registers),\n      CurrentMain.PaidPairedTrackAcquisition.run second\n            (CurrentMain.PaidPairedTrackAcquisition.totalTime f.before f.selected)\n            (CurrentMain.PaidPairedTrackAcquisition.initial f.before.length blocks scratch r) =\n          CurrentMain.PaidPairedTrackAcquisition.final second f.before f.selected f.after scratch ∧\n        CurrentMain.PaidPairedTrackAcquisition.Halted\n            (CurrentMain.PaidPairedTrackAcquisition.final second f.before f.selected f.after scratch) ∧\n          ∀ k < CurrentMain.PaidPairedTrackAcquisition.totalTime f.before f.selected,\n            ¬CurrentMain.PaidPairedTrackAcquisition.Halted\n                (CurrentMain.PaidPairedTrackAcquisition.run second k\n                  (CurrentMain.PaidPairedTrackAcquisition.initial f.before.length blocks scratch r))\n",
+      "printed_type_count": 2,
+      "warnings": [],
+      "errors": []
+    },
+    {
+      "module": "PaidPairedAcquisitionResources",
+      "source_sha256": "066b1222dcf1dea05453dcb7f39e1024191c347a639ebc9a2aae360ee1696e89",
+      "source_bytes": 6756,
+      "independent_reviewer": "prove_main_analytic_assembly",
+      "result": "PASS",
+      "probes": [
+        {
+          "declaration": "CurrentMain.PaidPairedAcquisitionResources.access_prefix_cells",
+          "axioms": [
+            "propext",
+            "Quot.sound"
+          ]
+        },
+        {
+          "declaration": "CurrentMain.PaidPairedAcquisitionResources.extraction_prefix_cells",
+          "axioms": [
+            "propext",
+            "Classical.choice",
+            "Quot.sound"
+          ]
+        },
+        {
+          "declaration": "CurrentMain.PaidPairedAcquisitionResources.home_suffix_cells",
+          "axioms": [
+            "propext",
+            "Quot.sound"
+          ]
+        },
+        {
+          "declaration": "CurrentMain.PaidPairedAcquisitionResources.machine_storage",
+          "axioms": [
+            "propext",
+            "Classical.choice",
+            "Quot.sound"
+          ]
+        },
+        {
+          "declaration": "CurrentMain.PaidPairedAcquisitionResources.entrance_resources",
+          "axioms": [
+            "propext",
+            "Classical.choice",
+            "Quot.sound"
+          ]
+        }
+      ],
+      "printed_full_types": "CurrentMain.PaidPairedAcquisitionResources.entrance_resources : ∀ (second : Bool)\n  (pre : List CurrentMain.PackedMetadataSlots.Block) (selected : CurrentMain.PackedMetadataSlots.Block)\n  (post : List CurrentMain.PackedMetadataSlots.Block) (scratch : Bool) (r : SequentialBitAddition.Registers),\n  let s := CurrentMain.PaidPairedTrackAcquisition.initial pre.length (pre ++ selected :: post) scratch r;\n  CurrentMain.PaidPairedTrackAcquisition.totalTime pre selected ≤ 7 * CurrentMain.PaidPairedTrackAcquisition.cells s ∧\n    CurrentMain.PaidPairedTrackAcquisition.run second (CurrentMain.PaidPairedTrackAcquisition.totalTime pre selected)\n          s =\n        CurrentMain.PaidPairedTrackAcquisition.final second pre selected post scratch ∧\n      CurrentMain.PaidPairedTrackAcquisition.Halted\n          (CurrentMain.PaidPairedTrackAcquisition.final second pre selected post scratch) ∧\n        (∀ k < CurrentMain.PaidPairedTrackAcquisition.totalTime pre selected,\n            ¬CurrentMain.PaidPairedTrackAcquisition.Halted (CurrentMain.PaidPairedTrackAcquisition.run second k s)) ∧\n          ∀ (k : ℕ),\n            CurrentMain.PaidPairedTrackAcquisition.cells (CurrentMain.PaidPairedTrackAcquisition.run second k s) ≤\n              2 * CurrentMain.PaidPairedTrackAcquisition.cells s\n",
+      "printed_type_count": 1,
+      "warnings": [],
+      "errors": []
+    }
+  ],
+  "probe_count": 43,
+  "printed_full_type_count": 12,
+  "acceptance_note": "The source hashes bind completed independent acceptance. Historical preparation comments remain byte-exact; later successful source-bound acceptance supplies current status. Two unnecessarySeqFocus lints in PackedMetadataSlots are retained. Other shipped roots have no diagnostics.",
+  "limits": [
+    "The initial complete marked packed store, supplied marked unary position, separate empty output tape and fixed track selector remain explicit.",
+    "Logical Nat keys are not encoded in the tape alphabet. Successful locate is a structural selection premise; key search, key-to-position compilation and unary preparation are not charged by this endpoint.",
+    "The source tracks, other blocks, control tape and carried Boolean scratch are preserved. The seven extraction registers are cleared, not restored to arbitrary prior values.",
+    "The 7V time and 2V tape-cell bounds apply to this actual three-tape run and its original represented entrance volume. Finite control/register fields are separate; no selected global recursion or full multiplication cost is inferred.",
+    "Physical encoding, store construction, initial allocation, arithmetic operation implementation and output writeback remain separate caller obligations."
+  ]
+}
diff --git a/research/lean-paid-positioned-acquisition/PUBLIC_SOURCE_MANIFEST.json b/research/lean-paid-positioned-acquisition/PUBLIC_SOURCE_MANIFEST.json
new file mode 100644
index 0000000000..558fd361c9
--- /dev/null
+++ b/research/lean-paid-positioned-acquisition/PUBLIC_SOURCE_MANIFEST.json
@@ -0,0 +1,463 @@
+{
+  "schema": "public-paid-positioned-acquisition-v1",
+  "status": "KERNEL_CHECKED_SOURCE_SET",
+  "author_checked_context": {
+    "kappa": "836330098538459/500000000000000000",
+    "decimal": "0.001672660197076918",
+    "author_checked": true,
+    "source_context_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea",
+    "meaning": "Unchanged selected PR1094 context only; the supplied-store finite-symbol acquisition bounds do not establish the selected multiplication runtime.",
+    "observed_critical_continuity_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2"
+  },
+  "shipped_modules": [
+    {
+      "module": "PairedTrackExtraction",
+      "path": "sources/PairedTrackExtraction.lean",
+      "bytes": 12842,
+      "sha256": "37a4b7c94d721a69994e23f4297e16d31d0b71d7ca3c0c3ae8e01a91d6ef7c68",
+      "git_blob": "19b2d96531936d71d33af0869ec36cbb0bc2924a",
+      "imports": [
+        "MarkedBitDifference",
+        "MarkedBitXorScan"
+      ]
+    },
+    {
+      "module": "PairedTrackExtractionFraming",
+      "path": "sources/PairedTrackExtractionFraming.lean",
+      "bytes": 8836,
+      "sha256": "1281ce4b355eaac7944485406de2bfb48e9f9ddf0bb30b2d990702ed23c3dc29",
+      "git_blob": "928d391b3b73c3c30d09af6a67a42d298c2074be",
+      "imports": [
+        "PairedTrackExtraction"
+      ]
+    },
+    {
+      "module": "PackedMetadataSlots",
+      "path": "sources/PackedMetadataSlots.lean",
+      "bytes": 13400,
+      "sha256": "50bd27baab6a2ded29a72f4af963b55fbaef3da6fc9895b663cad3c34b9d23ca",
+      "git_blob": "54e3705e2798aa09e94f74229a780231994208f9",
+      "imports": [
+        "FramedExponentMetadata"
+      ]
+    },
+    {
+      "module": "PositionalMetadataAccess",
+      "path": "sources/PositionalMetadataAccess.lean",
+      "bytes": 15608,
+      "sha256": "1854ed8040ebbe2a00ef54ddefa84f82bd8dc26eb5aff3418dab68cb8a31ce60",
+      "git_blob": "0ff88575285125032e7ae558719b3e68a0b381ec",
+      "imports": [
+        "PackedMetadataSlots"
+      ]
+    },
+    {
+      "module": "PositionalMetadataReturn",
+      "path": "sources/PositionalMetadataReturn.lean",
+      "bytes": 15425,
+      "sha256": "e1721065fb10b9576fd0d7e9539f25567981d09fdb4796bd9d32fa8dded799a6",
+      "git_blob": "558e63f32e7404dfefddab8fae905fe6658c6f95",
+      "imports": [
+        "PositionalMetadataAccess"
+      ]
+    },
+    {
+      "module": "PaidPairedTrackAcquisition",
+      "path": "sources/PaidPairedTrackAcquisition.lean",
+      "bytes": 12843,
+      "sha256": "8ecf7909570e003a9d1e03c0dd920c024457aed2ee1e427dde89c2ed228b1507",
+      "git_blob": "2f0e19c13bab7fa1bedace6d36fe354c250bd26e",
+      "imports": [
+        "PairedTrackExtractionFraming",
+        "PositionalMetadataReturn"
+      ]
+    },
+    {
+      "module": "PaidPairedAcquisitionResources",
+      "path": "sources/PaidPairedAcquisitionResources.lean",
+      "bytes": 6756,
+      "sha256": "066b1222dcf1dea05453dcb7f39e1024191c347a639ebc9a2aae360ee1696e89",
+      "git_blob": "f927f1128e91b365ac5f60cd62aa007f7aeac838",
+      "imports": [
+        "PaidPairedTrackAcquisition"
+      ]
+    }
+  ],
+  "public_prerequisites": [
+    {
+      "module": "PairedBitXorScan",
+      "repository": "CrocSwap/integer-mult-bounds",
+      "commit": "3f1b0641d5866f9d0b6cdd8e46db416fed6c5645",
+      "path": "research/lean-paired-bit-xor-machines/PairedBitXorScan.lean",
+      "bytes": 8418,
+      "sha256": "33a93351132f90fbb21f3dc06aa959c2a92d5202498540490df67149719279ed",
+      "git_blob": "eed92f0e224fefc0ad27eeb35015c968274a1ec3",
+      "pull_request": 1840
+    },
+    {
+      "module": "SequentialBitAddition",
+      "path": "research/lean-counted-bit-addition-padding/SequentialBitAddition.lean",
+      "repository": "CrocSwap/integer-mult-bounds",
+      "commit": "65ab016b4a464e3f5e2dd26c1bb0ae477e1ebce8",
+      "bytes": 20019,
+      "sha256": "7729e218143ac20dac17ca3c5ecd68b784d1d1c0b70fd2f0e4d13b8961e26c92",
+      "git_blob": "e44df99d7828d81e9504c5a0476da1dc098c9a6d"
+    },
+    {
+      "module": "PairedDifferenceArithmetic",
+      "path": "research/lean-binary-difference-unary/PairedDifferenceArithmetic.lean",
+      "sha256": "4ac5d39ef7912e852e2c62553e28f2d322214a0601119529eb6068108b6208e4",
+      "bytes": 6319,
+      "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/1947",
+      "repository": "CrocSwap/integer-mult-bounds",
+      "commit": "57278dcffa83a70a033eb2eef296f713b4025ff9",
+      "git_blob": "d23c9719d436fc716ea7bdc57db27cdf820b5f10"
+    },
+    {
+      "module": "MarkedBitXorScan",
+      "repository": "CrocSwap/integer-mult-bounds",
+      "commit": "3f1b0641d5866f9d0b6cdd8e46db416fed6c5645",
+      "path": "research/lean-paired-bit-xor-machines/MarkedBitXorScan.lean",
+      "bytes": 10945,
+      "sha256": "f28dbd4d53da61436b82cdd83cd3c7b49ec637fd0c4b40b527476e3976a50bb3",
+      "git_blob": "63c8f6a94cb7cccd04be435c55e7592c04555cac",
+      "pull_request": 1840
+    },
+    {
+      "module": "MarkedBitAddition",
+      "path": "research/lean-padded-signed-addition/MarkedBitAddition.lean",
+      "repository": "CrocSwap/integer-mult-bounds",
+      "commit": "6282571be5a5654cfb82568d8d70987bc4596add",
+      "bytes": 16174,
+      "sha256": "ae494a2841876ecbf4cb9ccae3cc12f11c66297660e2d63d534b4da051d4630d",
+      "git_blob": "7073b3f4762dc5012ab3c6777081c5872520f49b"
+    },
+    {
+      "module": "MarkedZeroPadding",
+      "path": "research/lean-counted-bit-addition-padding/MarkedZeroPadding.lean",
+      "repository": "CrocSwap/integer-mult-bounds",
+      "commit": "65ab016b4a464e3f5e2dd26c1bb0ae477e1ebce8",
+      "bytes": 25017,
+      "sha256": "bd289c3ec5857e8dfd74a6e1138e8493c49f37bdbb83c4d6912ac902a879f302",
+      "git_blob": "c4ca01e88cb9611f8d2a0c81ea8ce613a727f821"
+    },
+    {
+      "module": "MarkedBitDifference",
+      "path": "research/lean-binary-difference-unary/MarkedBitDifference.lean",
+      "sha256": "7dc3752deed02c88bc1b90884c61cf62414dd8b0c0fe635af5ebea2018a23049",
+      "bytes": 32454,
+      "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/1947",
+      "repository": "CrocSwap/integer-mult-bounds",
+      "commit": "57278dcffa83a70a033eb2eef296f713b4025ff9",
+      "git_blob": "ab7e26db39f97cd533e6ff9fffa691304de1123e"
+    },
+    {
+      "module": "MarkedXorFraming",
+      "path": "research/lean-prepared-pair-xor/MarkedXorFraming.lean",
+      "sha256": "fa08ca77d29ab24a7166951cc83602776c8d322df88b30217ea21c923134f3e6",
+      "bytes": 9416,
+      "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/1921",
+      "repository": "CrocSwap/integer-mult-bounds",
+      "commit": "69fefa9c2b2d3e5aa9bc11537537fd25ed3ea72c",
+      "git_blob": "3fdd8b861312be68ddfedb2588ecab7a6599be62"
+    },
+    {
+      "module": "FreshScalarSupportStream",
+      "repository": "CrocSwap/integer-mult-bounds",
+      "commit": "299eb8effe080183313757ac36e76c1b98ed9fae",
+      "path": "research/e8-lemma-g-lean/LemmaG/Stream.lean",
+      "bytes": 15263,
+      "sha256": "7138f4b859d0574a803e99401f05ef5e0ec9eeac0eb480775cd9b86595c365f8",
+      "git_blob": "e89897190307a6f3fcfb858f8de00cc5a7f49b3e",
+      "local_module_filename": "FreshScalarSupportStream.lean",
+      "transformation": "Filename only; source bytes unchanged."
+    },
+    {
+      "module": "FreshScalarSupportRealize",
+      "repository": "DreamingOfClouds/integer-mult-bounds",
+      "commit": "1c6b6ff9366a94e1f86a6c5d661a7df75c6ff814",
+      "path": "research/e8-lemma-a-lean/LemmaA/Realize.lean",
+      "upstream_bytes": 8108,
+      "upstream_sha256": "3aa9afd36035afd94296ef410c647d5a8c6fb282f64062542c7070bb1d99a14f",
+      "upstream_git_blob": "8917c5b7f7d86352fd0b505141a9047a4a676279",
+      "replacement": {
+        "before": "import LemmaG.Stream\n",
+        "after": "import FreshScalarSupportStream\n",
+        "count": 1
+      },
+      "derived_bytes": 8119,
+      "derived_sha256": "733c728e11394ed545d473b42f57206c256b3f01dc85455514176297d8c47a50",
+      "local_module_filename": "FreshScalarSupportRealize.lean",
+      "attribution": "PR509/516 LemmaG/LemmaA work by DreamingOfClouds with Claude assistance; exact source header and proof bodies retained."
+    },
+    {
+      "module": "Current1094PrivateCentreHosting",
+      "repository": "CrocSwap/integer-mult-bounds",
+      "commit": "7e50f40f73e355f4c53dcfc35516c868493a7069",
+      "path": "research/lean-current1094-private-centre-hosting/Current1094PrivateCentreHosting.lean",
+      "bytes": 4110,
+      "sha256": "f4ddb193fc07a44f56ed53cb903f80d0776474d06e890984f9a3e29b9fac0589",
+      "pull_request": 1802,
+      "git_blob": "96076bb973472756eb114a7ecaba99c35ad33730"
+    },
+    {
+      "module": "IndependentEntryUpdates",
+      "path": "research/lean-reference-component-store/sources/IndependentEntryUpdates.lean",
+      "sha256": "c6a68560a44d2386fcffddd506e386ed3898e78e732ba3652b8462a0c312453a",
+      "bytes": 2433,
+      "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/1985",
+      "repository": "CrocSwap/integer-mult-bounds",
+      "commit": "c2166eeef9cb36ad46c77c001b854d06e9f1b3cc",
+      "git_blob": "800edeeb2498460efb963c1f507d4644cc532fd8"
+    },
+    {
+      "module": "FreshScalarPrefixNorm",
+      "repository": "bitplane/integer-mult-bounds",
+      "commit": "5bde684f9189b59d1388c089ec5475fb5cf59565",
+      "path": "research/lean-unitary-prefix-norm/PrefixNorm.lean",
+      "upstream_bytes": 9110,
+      "upstream_sha256": "d1889e7402bc4ff4d2f78cd84034b51fd91d3020c17d65ddc3cb2c53b87621b1",
+      "upstream_git_blob": "4b4e9251bb6a451f54e17b6da3d8d17133f47fdb",
+      "replacement": {
+        "before": "import LemmaG.Stream\n",
+        "after": "import FreshScalarSupportStream\n",
+        "count": 1
+      },
+      "derived_bytes": 9121,
+      "derived_sha256": "2929a6e200d5e49cccc3dfffd3647c70fd003bbb43bf6c4fabb253864298cdfe",
+      "local_module_filename": "FreshScalarPrefixNorm.lean",
+      "attribution": "Gareth Davidson (@bitplane), with substantial OpenAI Codex assistance; unchanged proof/definition bodies and header, Apache-2.0."
+    },
+    {
+      "module": "FreshComponentStoreFoldRefinement",
+      "path": "research/lean-reference-component-store/sources/FreshComponentStoreFoldRefinement.lean",
+      "sha256": "b3c4673d9d1eafb1bd487cd6b404adb9ef288c44b7d22ac1cc55cc2b13eb80d0",
+      "bytes": 7316,
+      "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/1985",
+      "repository": "CrocSwap/integer-mult-bounds",
+      "commit": "c2166eeef9cb36ad46c77c001b854d06e9f1b3cc",
+      "git_blob": "2937033176e25e2c18022b24697e0b48045185ea"
+    },
+    {
+      "module": "FreshReferenceMinusHalfStore",
+      "path": "research/lean-reference-component-store/sources/FreshReferenceMinusHalfStore.lean",
+      "sha256": "d020b36c945e3782afa90c90c7fcade89e45a42661dfac102cb6282ba54ea0de",
+      "bytes": 4834,
+      "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/1985",
+      "repository": "CrocSwap/integer-mult-bounds",
+      "commit": "c2166eeef9cb36ad46c77c001b854d06e9f1b3cc",
+      "git_blob": "23f5df4530084018a80226843fd55200051f10a0"
+    },
+    {
+      "module": "Current1094Row1ScalarRealization",
+      "path": "research/lean-reference-dyadic-arithmetic/sources/Current1094Row1ScalarRealization.lean",
+      "sha256": "a76dc436d0e2eb70e535f117579d1b1019c415ecedec2ff6b6b1744dd9f62d24",
+      "bytes": 5313,
+      "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/2025",
+      "repository": "CrocSwap/integer-mult-bounds",
+      "commit": "c8005ae112094a33c3158e87baf257da8999568d",
+      "git_blob": "3ccd398e02d7f3380f746519e6e62e033cd28807"
+    },
+    {
+      "module": "Current1094Row1FlatReference",
+      "path": "research/lean-reference-dyadic-arithmetic/sources/Current1094Row1FlatReference.lean",
+      "sha256": "b4e1dcccfaace9e6b237a5e2598f87c3e7567b602fedcb7249f093ce4037329d",
+      "bytes": 8943,
+      "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/2025",
+      "repository": "CrocSwap/integer-mult-bounds",
+      "commit": "c8005ae112094a33c3158e87baf257da8999568d",
+      "git_blob": "545481860ebd2a11bd867a247742e245a14d5e59"
+    },
+    {
+      "module": "Current1094Row1DyadicReference",
+      "path": "research/lean-reference-dyadic-arithmetic/sources/Current1094Row1DyadicReference.lean",
+      "sha256": "50718d7225ba5b3da8c174d2c6e5aeb7d9bba16cd265dfc5f0965555573eb6bb",
+      "bytes": 8592,
+      "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/2025",
+      "repository": "CrocSwap/integer-mult-bounds",
+      "commit": "c8005ae112094a33c3158e87baf257da8999568d",
+      "git_blob": "732761a6f75453993bebe866a83cb3e6dc80689e"
+    },
+    {
+      "module": "DyadicCellAddition",
+      "path": "research/lean-reference-dyadic-arithmetic/sources/DyadicCellAddition.lean",
+      "sha256": "f5affbdc38bc3f65539dd390a4d7ef982b71aac65be018dc87cfe13f6c3809d6",
+      "bytes": 5769,
+      "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/2025",
+      "repository": "CrocSwap/integer-mult-bounds",
+      "commit": "c8005ae112094a33c3158e87baf257da8999568d",
+      "git_blob": "e0c1325b3b420c99c4b46de2a842e6ffc44fbf05"
+    },
+    {
+      "module": "DyadicAddSavedExponent",
+      "path": "research/lean-ambient-exponent-metadata/sources/DyadicAddSavedExponent.lean",
+      "sha256": "c3ff3e4f581f76cc45dcdfdb444b36f080452b3721e62127499080fbbee4ae6d",
+      "bytes": 3591,
+      "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/2403",
+      "repository": "CrocSwap/integer-mult-bounds",
+      "commit": "df580dfc3009a6c6c2a8a895949acf74230c388f",
+      "git_blob": "6c9e256ba517e89fb98813b429034b95df60ef38"
+    },
+    {
+      "module": "Current1094Row1FamilyBlocks",
+      "path": "research/lean-aligned-add-trace-budget/sources/Current1094Row1FamilyBlocks.lean",
+      "sha256": "1fbb6f833afbd74e7d9b9025b12d1f3f1e26c69a936c49b7891554f362031a4f",
+      "bytes": 4439,
+      "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/2370",
+      "repository": "CrocSwap/integer-mult-bounds",
+      "commit": "9db8170ed82cd0d96b696d3fb7ba4c839daef884",
+      "git_blob": "70cf29fd525686c8915bacd0dc0dda7f7b655409"
+    },
+    {
+      "module": "Current1094CallSequenceRouting",
+      "repository": "CrocSwap/integer-mult-bounds",
+      "commit": "457c6c315598ba1a05692fed55e3f47d99dbb184",
+      "path": "research/lean-current1094-all144-helper-owners/sources/Current1094CallSequenceRouting.lean",
+      "bytes": 6870,
+      "sha256": "96938c28866deff3db15d8f5e6df1c75dace1583721b36ca7c9eac73f7f862ca",
+      "git_blob": "ad3ec500ef14011ee415e5c29533e02210e85b86",
+      "pull_request": 1807
+    },
+    {
+      "module": "Current1094Row2AddReference",
+      "path": "research/lean-aligned-add-trace-budget/sources/Current1094Row2AddReference.lean",
+      "sha256": "97a148bbe6dd45d27aba25ac24cf9a93b8dc123ec7bc8e4f587610707aea5748",
+      "bytes": 17241,
+      "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/2370",
+      "repository": "CrocSwap/integer-mult-bounds",
+      "commit": "9db8170ed82cd0d96b696d3fb7ba4c839daef884",
+      "git_blob": "9782bd18903fa013ec8c05c85275848a471cc0f5"
+    },
+    {
+      "module": "Current1094Row2DyadicReference",
+      "path": "research/lean-aligned-add-trace-budget/sources/Current1094Row2DyadicReference.lean",
+      "sha256": "018583f2356f3914e3f321d244c8a1ba314438a970dccc0bf21f56539b33b75b",
+      "bytes": 11330,
+      "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/2370",
+      "repository": "CrocSwap/integer-mult-bounds",
+      "commit": "9db8170ed82cd0d96b696d3fb7ba4c839daef884",
+      "git_blob": "1399d1fc2f60557f6ffd6764501ed026bb4752a8"
+    },
+    {
+      "module": "DyadicAddExponentCleanup",
+      "path": "research/lean-ambient-exponent-metadata/sources/DyadicAddExponentCleanup.lean",
+      "sha256": "72ef894c1bc7db91f15af4c4e51923ea3e80db958acd36c83af5c3da1460ea5a",
+      "bytes": 6967,
+      "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/2403",
+      "repository": "CrocSwap/integer-mult-bounds",
+      "commit": "df580dfc3009a6c6c2a8a895949acf74230c388f",
+      "git_blob": "04bec60a13040afb9640b70fe51337b7e0c91632"
+    },
+    {
+      "module": "ExponentMetadataBitAdapter",
+      "path": "research/lean-ambient-exponent-metadata/sources/ExponentMetadataBitAdapter.lean",
+      "sha256": "7d499f3cbcc4ca40edbf7fdd1ab95585b57e8c9300e68b4edbfed95581cc1bc6",
+      "bytes": 7390,
+      "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/2403",
+      "repository": "CrocSwap/integer-mult-bounds",
+      "commit": "df580dfc3009a6c6c2a8a895949acf74230c388f",
+      "git_blob": "1b2040de2478ee2bc78405a0eb82ba3bf3379b6d"
+    },
+    {
+      "module": "FramedExponentMetadata",
+      "path": "research/lean-ambient-exponent-metadata/sources/FramedExponentMetadata.lean",
+      "sha256": "695fe1b4dd438022a4e159b0c791783e9c35e08534be50f21ecb4bd371bf2841",
+      "bytes": 3126,
+      "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/2403",
+      "repository": "CrocSwap/integer-mult-bounds",
+      "commit": "df580dfc3009a6c6c2a8a895949acf74230c388f",
+      "git_blob": "5afb7e5530624cf0e8d962e7e98a332f04d81174"
+    }
+  ],
+  "compile_order": [
+    "PairedBitXorScan",
+    "SequentialBitAddition",
+    "PairedDifferenceArithmetic",
+    "MarkedBitXorScan",
+    "MarkedBitAddition",
+    "MarkedZeroPadding",
+    "MarkedBitDifference",
+    "PairedTrackExtraction",
+    "PairedTrackExtractionFraming",
+    "MarkedXorFraming",
+    "FreshScalarSupportStream",
+    "FreshScalarSupportRealize",
+    "Current1094PrivateCentreHosting",
+    "IndependentEntryUpdates",
+    "FreshScalarPrefixNorm",
+    "FreshComponentStoreFoldRefinement",
+    "FreshReferenceMinusHalfStore",
+    "Current1094Row1ScalarRealization",
+    "Current1094Row1FlatReference",
+    "Current1094Row1DyadicReference",
+    "DyadicCellAddition",
+    "DyadicAddSavedExponent",
+    "Current1094Row1FamilyBlocks",
+    "Current1094CallSequenceRouting",
+    "Current1094Row2AddReference",
+    "Current1094Row2DyadicReference",
+    "DyadicAddExponentCleanup",
+    "ExponentMetadataBitAdapter",
+    "FramedExponentMetadata",
+    "PackedMetadataSlots",
+    "PositionalMetadataAccess",
+    "PositionalMetadataReturn",
+    "PaidPairedTrackAcquisition",
+    "PaidPairedAcquisitionResources"
+  ],
+  "runtime": {
+    "lean": "4.21.0",
+    "mathlib_commit": "308445d7985027f538e281e18df29ca16ede2ba3",
+    "official_package_commits": [
+      {
+        "name": "plausible",
+        "commit": "c4aa78186d388e50a436e8362b947bae125a2933"
+      },
+      {
+        "name": "LeanSearchClient",
+        "commit": "6c62474116f525d2814f0157bb468bf3a4f9f120"
+      },
+      {
+        "name": "importGraph",
+        "commit": "d07bd64f1910f1cc5e4cc87b6b9c590080e7a457"
+      },
+      {
+        "name": "proofwidgets",
+        "commit": "6980f6ca164de593cb77cd03d8eac549cc444156"
+      },
+      {
+        "name": "aesop",
+        "commit": "8ff27701d003456fd59f13a9212431239d902aef"
+      },
+      {
+        "name": "Qq",
+        "commit": "e9c65db4823976353cd0bb03199a172719efbeb7"
+      },
+      {
+        "name": "batteries",
+        "commit": "8d2067bf518731a70a255d4a61b5c103922c772e"
+      },
+      {
+        "name": "Cli",
+        "commit": "7c6aef5f75a43ebbba763b44d535175a1b04c9e0"
+      }
+    ],
+    "preparation": "Use an already prepared official installation and cached matching dependencies. This package performs no installation."
+  },
+  "source_counts": {
+    "shipped_modules": 7,
+    "shipped_lean_bytes": 85710,
+    "reused_modules": 27,
+    "reused_lean_bytes": 269529,
+    "complete_research_modules": 34,
+    "complete_research_source_bytes": 355239
+  },
+  "namespace_rule": "Reconstruct the one FreshScalarSupportStream closure. Do not simultaneously import original LemmaG.Stream/LemmaA.Realize/PrefixNorm or competing aliases with the same namespaces.",
+  "limits": [
+    "The initial complete marked packed store, supplied marked unary position, separate empty output tape and fixed track selector remain explicit.",
+    "Logical Nat keys are not encoded in the tape alphabet. Successful locate is a structural selection premise; key search, key-to-position compilation and unary preparation are not charged by this endpoint.",
+    "The source tracks, other blocks, control tape and carried Boolean scratch are preserved. The seven extraction registers are cleared, not restored to arbitrary prior values.",
+    "The 7V time and 2V tape-cell bounds apply to this actual three-tape run and its original represented entrance volume. Finite control/register fields are separate; no selected global recursion or full multiplication cost is inferred.",
+    "Physical encoding, store construction, initial allocation, arithmetic operation implementation and output writeback remain separate caller obligations."
+  ]
+}
diff --git a/research/lean-paid-positioned-acquisition/README.md b/research/lean-paid-positioned-acquisition/README.md
new file mode 100644
index 0000000000..5853178a80
--- /dev/null
+++ b/research/lean-paid-positioned-acquisition/README.md
@@ -0,0 +1,44 @@
+# Paid positioned track acquisition and return
+
+Seven unchanged accepted Lean modules compose an actual three-tape read of one selected paired track from a supplied finite packed store, returning its data and control heads to home. The chosen bits are copied to a separately supplied empty tape. The complete store and both original paired tracks survive.
+
+## Author-checked context
+
+κ = 836330098538459/500000000000000000 = 0.001672660197076918 is the unchanged selected PR1094 context, author-checked by James Chang with OpenAI assistance. The original source context is 0b1cccf86e2f5132ed286a26ef0a681a495740ea; the five selected critical source blobs remain identical at observed main 0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2. These finite supplied-store results do not improve κ or establish the full selected multiplication theorem.
+
+## Checked endpoint
+
+Let `pre`, `selected`, `post` describe the ordered store, `p = pre.length`, and `w = selected.rows.length`. The actual controller performs positional access, one charged handoff, source-preserving track extraction, one charged handoff, and physical return to global home. Its first halt is exactly
+
+`2 * capacity(pre) + 4*p + 6*w + 26` transitions.
+
+The original represented entrance volume is `V = capacity(pre ++ selected :: post) + p + 2`, including every packed delimiter and the marked unary control. The output is initially empty. `entrance_resources` derives actual endpoint and first halt with time at most `7*V` and, for every run prefix including terminal stuttering, at most `2*V` represented tape cells. The copied output includes its paid left/right markers. Zero-width blocks and position zero are covered.
+
+The complete data store, both selected source tracks, all other blocks, the unary control tape and the carried Boolean scratch are preserved. The seven extraction registers finish clear; arbitrary old register values are not restored. The track selector is a fixed Boolean program parameter. Tape-cell volume counts represented zipper cells; finite control and register fields remain separate fixed fields.
+
+## Module roles
+
+- `PairedTrackExtraction` specializes the accepted marked-difference extraction phase to a chosen Boolean track of the existing paired alphabet. It derives `6*w+16` transitions, first halt, exact output and `2*w+4` prefix cells from actual steps.
+- `PairedTrackExtractionFraming` derives confinement and step/run compatibility with arbitrary surrounding source lists, then exact framed output and full-context storage. The left list is stored in reverse zipper order. Output remains a distinct empty-at-entry tape.
+- `PackedMetadataSlots` supplies ordered structural lookup with explicit before/selected/after focus, missing-key failure, unique-key ownership, complete packing/capacity, and the existing metadata XOR/update refinement. Keys are logical labels, absent from the physical alphabet. Semantic first-match update and unique physical ownership are distinct facts.
+- `PositionalMetadataAccess` traverses actual L/data/R symbols using one supplied unary tick per preceding block. Exact first halt is `capacity(pre)+2*p+4`; the control head rewinds while the data head reaches the selected left marker. All symbols and arbitrary carried scratch survive.
+- `PositionalMetadataReturn` traverses those blocks in reverse physical order, returning data and unary heads home at the same exact cost. It reads finite symbols without a numeric seek or hidden boundary sensor.
+- `PaidPairedTrackAcquisition` composes the three actual machines with two charged transitions, and binds executable `locate` success to the reached focus and copied word.
+- `PaidPairedAcquisitionResources` derives the complete prefix bound and original-entrance `7V` time / `2V` space invoice without adding an execution premise.
+
+`ACCEPTANCE.json` binds 43 complete axiom probes and 12 full printed types to exact source hashes. All use only standard Lean axioms. Two harmless `unnecessarySeqFocus` style warnings in `PackedMetadataSlots` are retained verbatim; the other six roots have no diagnostics. The historical “Uncompiled candidate” label in `PositionalMetadataReturn` is preserved. Its exact source subsequently passed and has an independent accepted terminal, as the source-bound summary records.
+
+## Explicit caller obligations
+
+The initial marked packed store, unary positional tape, distinct empty output tape, fixed track choice and valid ordered layout are supplied. Structural key lookup is not a paid runtime key search. Key-to-position binding, unary preparation, physical field encoding, initial store construction/allocation, source refresh and subsequent output writeback remain separate obligations. A malformed entrance gets no success theorem merely because transitions are total. No uniform recursive bit-cost, selected precision, arbitrary dirty-register recovery or full multiplier theorem is claimed.
+
+## Reuse and attribution
+
+James Chang with OpenAI assistance, Apache-2.0; preserve all source headers and prerequisite attribution. The actual extractor reuses public PR1947 marked-difference extraction and PR1840/1869/1899 marked tape and arithmetic foundations. Packed metadata reuses PR2403 ambient exponent metadata, PR1921 XOR framing, and the exact reference arithmetic/store/routing chain. Import-renamed public LemmaG/LemmaA and PrefixNorm retain DreamingOfClouds and Gareth Davidson (@bitplane) credits and unchanged proof bodies.
+
+PR2235 provides substantial generic finite-head machine, framing, charged-caller and serializer infrastructure. Its inspected serializer consumes a compiler-stack input into a blank-origin output. This package's endpoint is a source-preserving selected track of an occupied paired store, with actual positional access and return. The model/ABI distinction is explicit; no priority or generic framing novelty claim is made.
+
+
+The later [PR2411 framework](https://github.com/CrocSwap/integer-mult-bounds/pull/2411), at immutable provider commit `7415d773d14212c68b523979aaac6db9dc0ba542`, also supplies general components that overlap this work: [GuardedMapCopy.copy_hoare](https://github.com/platypii/integer-mult-bounds-lean/blob/7415d773d14212c68b523979aaac6db9dc0ba542/IntegerMultBounds/Machine/GuardedMapCopy.lean#L52) preserves an occupied source and the destination outside the written interval while applying a fixed symbol map in exactly the word length; [CountedSeek](https://github.com/platypii/integer-mult-bounds-lean/blob/7415d773d14212c68b523979aaac6db9dc0ba542/IntegerMultBounds/Machine/CountedSeek.lean#L212) supplies payload-preserving forward/backward movement with an immutable binary descriptor and clean local clock, bounded by `5*distance + 7*descriptor.length + 16`; [MarkedReturn.return_hoare](https://github.com/platypii/integer-mult-bounds-lean/blob/7415d773d14212c68b523979aaac6db9dc0ba542/IntegerMultBounds/Machine/MarkedReturn.lean#L104) restores a marked word's origin in `length+2` transitions. Those are reusable generic suppliers, not missing primitives. The present accepted endpoint remains specific to the existing paired-symbol/zipper model, a unary count of variable-width blocks, its two charged handoffs, exact home/output states and original represented-volume `7V/2V` theorem. The bounded comparison found no exact combined endpoint substitution; reuse in the other finite-alphabet absolute-tape model still needs an explicit representation/position/interface bridge. No generic copy/seek/return novelty or global absence claim is made.
+
+Seven shipped sources total 85,710 bytes. Twenty-seven immutable public or deterministic import-derived prerequisites give a complete 34-module research closure of 355,239 bytes. No public prerequisite is recopied. `PUBLIC_SOURCE_MANIFEST.json` records exact identities and topological order. Use `REPRODUCTION.md` with an already prepared Lean 4.21.0 / Mathlib installation, and avoid loading conflicting original and alias namespaces together.
diff --git a/research/lean-paid-positioned-acquisition/REPRODUCTION.md b/research/lean-paid-positioned-acquisition/REPRODUCTION.md
new file mode 100644
index 0000000000..a6c04d9229
--- /dev/null
+++ b/research/lean-paid-positioned-acquisition/REPRODUCTION.md
@@ -0,0 +1,67 @@
+# Reproduce the exact paid acquisition source closure
+
+Use an already prepared official Lean 4.21.0 installation and Mathlib checkout/caches at the manifest commit, with its eight pinned package checkouts. Set LEAN_HOME, MATHLIB_HOME and a shared LEAN_REPLAY_LOCK. Git, Python3, timeout and flock are required. The recipe never invokes elan or installs/rebuilds dependencies. Run from this package directory.
+
+```sh
+set -eu
+: "$LEAN_HOME" "$MATHLIB_HOME" "$LEAN_REPLAY_LOCK"
+test -x "$LEAN_HOME/bin/lean"
+unset LEAN_OPTS LEAN_PATH
+"$LEAN_HOME/bin/lean" --version | grep -Eq '^Lean \(version 4\.21\.0([,)]| )'
+[ "$(git -C "$MATHLIB_HOME" rev-parse HEAD)" = 308445d7985027f538e281e18df29ca16ede2ba3 ]
+[ -z "$(git -C "$MATHLIB_HOME" status --porcelain --untracked-files=no)" ]
+export MATHLIB_HOME
+python3 - <<'PY_CHECK'
+import json,os,pathlib,subprocess
+m=json.load(open('PUBLIC_SOURCE_MANIFEST.json'));root=pathlib.Path(os.environ['MATHLIB_HOME'])
+for x in m['runtime']['official_package_commits']:
+    p=root/'.lake/packages'/x['name']
+    assert subprocess.check_output(['git','-C',str(p),'rev-parse','HEAD'],text=True).strip()==x['commit']
+    assert not subprocess.check_output(['git','-C',str(p),'status','--porcelain','--untracked-files=no'],text=True).strip()
+PY_CHECK
+exec 9>"$LEAN_REPLAY_LOCK"
+flock 9
+work=$(mktemp -d)
+export work
+python3 - <<'PY_SOURCES'
+import pathlib,hashlib,json,os,subprocess
+w=pathlib.Path(os.environ['work']);m=json.load(open('PUBLIC_SOURCE_MANIFEST.json'))
+for d in ['sources','objects','logs','upstream']:(w/d).mkdir()
+def run(*a):return subprocess.check_output(list(a))
+run('git','init','-q',str(w/'upstream'));fetched=set()
+for x in m['public_prerequisites']:
+    key=(x['repository'],x['commit'])
+    if key not in fetched:
+        run('git','-C',str(w/'upstream'),'fetch','--no-tags','--depth=1','https://github.com/'+x['repository']+'.git',x['commit']);fetched.add(key)
+    b=run('git','-C',str(w/'upstream'),'show',x['commit']+':'+x['path'])
+    if 'replacement' in x:
+        assert len(b)==x['upstream_bytes'] and hashlib.sha256(b).hexdigest()==x['upstream_sha256']
+        r=x['replacement'];a=r['before'].encode();c=r['after'].encode();assert b.count(a)==r['count']==1
+        b=b.replace(a,c,1)
+    size=x.get('derived_bytes',x.get('bytes'));sha=x.get('derived_sha256',x.get('sha256'))
+    assert len(b)==size and hashlib.sha256(b).hexdigest()==sha
+    (w/'sources'/(x['module']+'.lean')).write_bytes(b)
+for x in m['shipped_modules']:
+    b=pathlib.Path(x['path']).read_bytes()
+    assert len(b)==x['bytes'] and hashlib.sha256(b).hexdigest()==x['sha256']
+    (w/'sources'/(x['module']+'.lean')).write_bytes(b)
+(w/'order').write_text('\n'.join(m['compile_order'])+'\n')
+PY_SOURCES
+libpath="$work/objects:$MATHLIB_HOME/.lake/build/lib/lean"
+for p in plausible LeanSearchClient importGraph proofwidgets aesop Qq batteries Cli; do
+  libpath="$libpath:$MATHLIB_HOME/.lake/packages/$p/.lake/build/lib/lean"
+done
+while IFS= read -r module; do
+  available_kib=$(df -Pk "$work" | awk 'NR==2 {print $4}')
+  [ "$available_kib" -ge 8388608 ] || { echo 'Need at least 8 GiB free'; exit 1; }
+  set +e
+  (ulimit -v 4194304; LEAN_PATH="$libpath" timeout --signal=KILL 60s "$LEAN_HOME/bin/lean" -j1 -o "$work/objects/$module.olean" "$work/sources/$module.lean") >"$work/logs/$module.stdout" 2>"$work/logs/$module.stderr"
+  result=$?
+  set -e
+  printf '%s\n' "$result" >"$work/logs/$module.exit-code"
+  [ "$result" -eq 0 ] || { echo "Stopped; complete logs retained in $work/logs"; exit "$result"; }
+done < "$work/order"
+printf 'Sources, objects and logs retained in %s\n' "$work"
+```
+
+This is a reproduction recipe, not a claim of another publication-candidate replay. Stop if the prepared prerequisites are unavailable. The seven shipped modules retain two PackedMetadataSlots style warnings; all other shipped diagnostics were empty. Preserve every warning from reused prerequisites as well.
diff --git a/research/lean-paid-positioned-acquisition/sources/PackedMetadataSlots.lean b/research/lean-paid-positioned-acquisition/sources/PackedMetadataSlots.lean
new file mode 100644
index 0000000000..54e3705e27
--- /dev/null
+++ b/research/lean-paid-positioned-acquisition/sources/PackedMetadataSlots.lean
@@ -0,0 +1,284 @@
+import FramedExponentMetadata
+
+/-!
+Finite keyed storage bridge for the accepted marked paired-bit XOR segment.
+The executable structural locate returns the actual before/block/after split;
+its result constructs a head positioned at that block. Accepted ambient framing
+then changes only that block's target bits and preserves the remaining packed
+symbols. A derived total semantic view refines Function.update at the located
+Nat key, with an explicit ambient fallback for keys absent from the layout.
+
+All supplied blocks, markers and payload cells are charged, not just the active
+block. Keys are logical labels here: their bit encoding/storage, sequential key
+comparison cost, head travel to the constructed focus, width choice, pairing,
+allocation/initialization and source-track refresh are not supplied or free.
+Other BoundaryState fields and compound arithmetic workspace stay separate.
+James Chang with OpenAI assistance; Apache-2.0. Reuses accepted machine paired
+XOR and metadata interpretation plus signed ambient framing without replay.
+Pinned conditional context: kappa=836330098538459/500000000000000000.
+Uncompiled candidate.
+-/
+set_option Elab.async false
+set_option autoImplicit false
+namespace CurrentMain.PackedMetadataSlots
+open PairedBitXorScan (Pair value xorPair)
+open MarkedBitXorScan
+
+structure Block where
+  key : Nat
+  rows : List Pair
+
+structure Focus where
+  before : List Block
+  selected : Block
+  after : List Block
+
+/-- An executable sequential search, not unit-cost random access. -/
+def locate (key : Nat) : List Block → Option Focus
+  | [] => none
+  | block :: rest =>
+      if block.key = key then some ⟨[], block, rest⟩
+      else (locate key rest).map (fun f => ⟨block :: f.before, f.selected, f.after⟩)
+
+def Unique : List Block → Prop
+  | [] => True
+  | block :: rest => (∀ b, b ∈ rest → b.key ≠ block.key) ∧ Unique rest
+
+def pack : List Block → List Symbol
+  | [] => []
+  | block :: rest => marked block.rows ++ pack rest
+
+def capacity : List Block → Nat
+  | [] => 0
+  | block :: rest => block.rows.length + 2 + capacity rest
+
+def keys (blocks : List Block) : List Nat := blocks.map Block.key
+
+def targetValue (b : Block) : Nat := value (b.rows.map Prod.fst)
+def sourceValue (b : Block) : Nat := value (b.rows.map Prod.snd)
+
+/-- Total semantic observation of a supplied finite store. The ambient function
+is retained off-layout; this definition does not implement a memory lookup. -/
+def metadata (ambient : Nat → Nat) : List Block → Nat → Nat
+  | [] => ambient
+  | block :: rest => Function.update (metadata ambient rest) block.key (targetValue block)
+
+def toggleBlock (b : Block) : Block := ⟨b.key, b.rows.map xorPair⟩
+def replaced (f : Focus) : List Block := f.before ++ toggleBlock f.selected :: f.after
+
+def toggleAt (key : Nat) (blocks : List Block) : Option (List Block) :=
+  (locate key blocks).map replaced
+
+/-- Exact successful search decomposition and absence of earlier matches. -/
+theorem locate_spec (key : Nat) (blocks : List Block) : ∀ f,
+    locate key blocks = some f →
+      blocks = f.before ++ f.selected :: f.after ∧ f.selected.key = key ∧
+      (∀ b, b ∈ f.before → b.key ≠ key) := by
+  induction blocks with
+  | nil => intro f h; simp [locate] at h
+  | cons block rest ih =>
+      intro f h
+      by_cases hk : block.key = key
+      · simp only [locate, hk, ↓reduceIte, Option.some.injEq] at h
+        cases h
+        exact ⟨rfl, hk, by intro b hb; cases hb⟩
+      · simp only [locate, hk, ↓reduceIte] at h
+        cases he : locate key rest with
+        | none => simp [he] at h
+        | some tail =>
+            rcases tail with ⟨pre, selected, post⟩
+            simp only [he, Option.map_some, Option.some.injEq] at h
+            cases h
+            obtain ⟨hr, hs, hp⟩ := ih ⟨pre, selected, post⟩ he
+            refine ⟨by simpa only [List.cons_append] using congrArg (block :: ·) hr, hs, ?_⟩
+            intro b hb
+            rcases List.mem_cons.mp hb with h | h
+            · subst b; exact hk
+            · exact hp b h
+
+theorem locate_none (key : Nat) (blocks : List Block) :
+    locate key blocks = none ↔ ∀ b, b ∈ blocks → b.key ≠ key := by
+  induction blocks with
+  | nil => simp [locate]
+  | cons block rest ih =>
+      by_cases hk : block.key = key
+      · simp [locate, hk]
+      · simp only [locate, hk, ↓reduceIte, Option.map_eq_none_iff, ih, List.mem_cons]
+        constructor
+        · intro h b hb
+          rcases hb with rfl | hb
+          · exact hk
+          · exact h b hb
+        · intro h b hb
+          exact h b (Or.inr hb)
+
+private theorem unique_middle (pre post : List Block) (selected : Block)
+    (h : Unique (pre ++ selected :: post)) :
+    ∀ b, b ∈ pre ++ post → b.key ≠ selected.key := by
+  induction pre with
+  | nil => exact h.1
+  | cons block pre ih =>
+      have hne : block.key ≠ selected.key :=
+        Ne.symm (h.1 selected (by simp))
+      have ht := ih h.2
+      intro b hb
+      rcases List.mem_cons.mp hb with rfl | hb
+      · exact hne
+      · exact ht b hb
+
+/-- Unique-key input ensures the selected key occurs in no spectator block. -/
+theorem locate_unique (key : Nat) (blocks : List Block) (f : Focus)
+    (hu : Unique blocks) (h : locate key blocks = some f) :
+    ∀ b, b ∈ f.before ++ f.after → b.key ≠ key := by
+  obtain ⟨he, hk, _⟩ := locate_spec key blocks f h
+  rw [he] at hu
+  simpa only [hk] using unique_middle f.before f.after f.selected hu
+
+private theorem pack_append (xs ys : List Block) : pack (xs ++ ys) = pack xs ++ pack ys := by
+  induction xs with
+  | nil => rfl
+  | cons block rest ih => simp only [List.cons_append, pack, ih, List.append_assoc]
+
+/-- Entire supplied tape capacity, including a marker pair for every block. -/
+theorem pack_capacity (blocks : List Block) : (pack blocks).length = capacity blocks := by
+  induction blocks with
+  | nil => rfl
+  | cons block rest ih => simp [pack, capacity, marked, ih, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] <;> omega
+
+theorem uniform_capacity (blocks : List Block) (width : Nat)
+    (h : ∀ b, b ∈ blocks → b.rows.length = width) :
+    capacity blocks = blocks.length * (width + 2) := by
+  induction blocks with
+  | nil => simp [capacity]
+  | cons block rest ih =>
+      have hb := h block (by simp)
+      have ht := ih (fun b hb => h b (by simp [hb]))
+      simp only [capacity, List.length_cons, hb, ht, Nat.succ_mul]
+      omega
+
+/-- Focus construction uses the real located prefix in stored reverse order.
+Moving a physical head from a different position to this focus is unpriced. -/
+def focusState (f : Focus) : State :=
+  MarkedXorFraming.embed (pack f.before).reverse (pack f.after) (initial f.selected.rows)
+
+def tapeWord (s : State) : List Symbol := s.tape.left.reverse ++ s.tape.right
+
+/-- The constructed entrance contains exactly all supplied blocks in order. -/
+theorem focus_pack (key : Nat) (blocks : List Block) (f : Focus)
+    (h : locate key blocks = some f) : tapeWord (focusState f) = pack blocks := by
+  obtain ⟨he, _, _⟩ := locate_spec key blocks f h
+  rw [he, pack_append]
+  simp only [tapeWord, focusState, MarkedXorFraming.embed, initial, pack,
+    List.nil_append, List.reverse_reverse, List.append_assoc]
+
+/-- Actual framed execution changes only the focused payload; both complete
+spectator lists remain byte-for-symbol identical, with the returned marker head. -/
+theorem run_focused (f : Focus) :
+    run (5 * f.selected.rows.length + 4) (focusState f) =
+      ⟨⟨(pack f.before).reverse,
+        marked (f.selected.rows.map xorPair) ++ pack f.after⟩, false, .halt⟩ := by
+  exact MarkedXorFraming.framed_scan_result (pack f.before).reverse (pack f.after) f.selected.rows
+
+theorem run_repacked (f : Focus) :
+    tapeWord (run (5 * f.selected.rows.length + 4) (focusState f)) = pack (replaced f) := by
+  rw [run_focused]
+  simp only [tapeWord, replaced, pack_append, pack, toggleBlock, List.reverse_reverse, List.append_assoc]
+
+/-- Every prefix charges the whole packed store, not merely the active block. -/
+theorem located_storage (key : Nat) (blocks : List Block) (f : Focus)
+    (h : locate key blocks = some f) (k : Nat) :
+    cells (run k (focusState f)) = capacity blocks := by
+  have hs := MarkedXorFraming.framed_scan_storage (pack f.before).reverse (pack f.after) f.selected.rows k
+  change cells (run k (focusState f)) = _ at hs
+  rw [List.length_reverse] at hs
+  rw [hs, ← pack_capacity]
+  obtain ⟨he, _, _⟩ := locate_spec key blocks f h
+  rw [he, pack_append]
+  simp [pack, marked, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] <;> omega
+
+/-- Absent keys retain the supplied ambient metadata, including dirty values. -/
+theorem metadata_avoids (ambient : Nat → Nat) (blocks : List Block) (key : Nat)
+    (h : ∀ b, b ∈ blocks → b.key ≠ key) : metadata ambient blocks key = ambient key := by
+  induction blocks with
+  | nil => rfl
+  | cons block rest ih =>
+      have hb : key ≠ block.key := Ne.symm (h block (by simp))
+      rw [metadata, Function.update_of_ne hb]
+      exact ih (fun b hb => h b (by simp [hb]))
+
+private theorem metadata_skip (ambient : Nat → Nat) (pre rest : List Block) (key : Nat)
+    (h : ∀ b, b ∈ pre → b.key ≠ key) :
+    metadata ambient (pre ++ rest) key = metadata ambient rest key := by
+  induction pre with
+  | nil => rfl
+  | cons block pre ih =>
+      rw [List.cons_append, metadata, Function.update_of_ne (Ne.symm (h block (by simp)))]
+      exact ih (fun b hb => h b (by simp [hb]))
+
+private theorem metadata_replace (ambient : Nat → Nat) (pre post : List Block)
+    (selected : Block) (rows : List Pair)
+    (h : ∀ b, b ∈ pre → b.key ≠ selected.key) :
+    metadata ambient (pre ++ { selected with rows := rows } :: post) =
+      Function.update (metadata ambient (pre ++ selected :: post)) selected.key (value (rows.map Prod.fst)) := by
+  induction pre with
+  | nil => simp only [List.nil_append, metadata, targetValue, Function.update_idem]
+  | cons block pre ih =>
+      have hb := h block (by simp)
+      have ht := ih (fun b hb => h b (by simp [hb]))
+      simp only [List.cons_append, metadata]
+      rw [ht]
+      exact Function.update_comm (Ne.symm hb) _ _ _
+
+/-- Executable replacement and exact decoded Nat update. The original target
+value is derived from search, and the increment is the retained source track. -/
+theorem located_toggle (ambient : Nat → Nat) (key : Nat) (blocks : List Block) (f : Focus)
+    (h : locate key blocks = some f) :
+    toggleAt key blocks = some (replaced f) ∧
+    keys (replaced f) = keys blocks ∧
+    metadata ambient (replaced f) =
+      Function.update (metadata ambient blocks) key
+        (metadata ambient blocks key ^^^ sourceValue f.selected) := by
+  obtain ⟨he, hk, hp⟩ := locate_spec key blocks f h
+  have hv : metadata ambient blocks key = targetValue f.selected := by
+    rw [he, metadata_skip ambient f.before (f.selected :: f.after) key hp, metadata, hk, Function.update_self]
+  refine ⟨by simp only [toggleAt, h, Option.map_some], ?_, ?_⟩
+  · rw [he]
+    simp only [keys, replaced, List.map_append, List.map_cons, toggleBlock]
+  · have hu := metadata_replace ambient f.before f.after f.selected (f.selected.rows.map xorPair)
+      (by simpa only [hk] using hp)
+    change metadata ambient (replaced f) = _ at hu
+    rw [PairedBitXorScan.value_xor, ← he, hk] at hu
+    change metadata ambient (replaced f) = Function.update (metadata ambient blocks) key
+      (targetValue f.selected ^^^ sourceValue f.selected) at hu
+    rw [← hv] at hu
+    exact hu
+
+/-- Numeric restored-exponent equality gives literal cleared target bits; no
+canonical-width assumption or free clearing instruction is introduced. -/
+theorem located_clear (ambient : Nat → Nat) (key : Nat) (blocks : List Block) (f : Focus)
+    (h : locate key blocks = some f)
+    (hequal : metadata ambient blocks key = sourceValue f.selected) :
+    (toggleBlock f.selected).rows.map Prod.fst = List.replicate f.selected.rows.length false ∧
+    metadata ambient (replaced f) = Function.update (metadata ambient blocks) key 0 := by
+  obtain ⟨he, hk, hp⟩ := locate_spec key blocks f h
+  have hv : metadata ambient blocks key = targetValue f.selected := by
+    rw [he, metadata_skip ambient f.before (f.selected :: f.after) key hp, metadata, hk, Function.update_self]
+  constructor
+  · exact ExponentMetadataBitAdapter.xor_targets_clear f.selected.rows (hv.symm.trans hequal)
+  · rw [(located_toggle ambient key blocks f h).2.2, hequal, Nat.xor_self]
+
+end CurrentMain.PackedMetadataSlots
+#print axioms CurrentMain.PackedMetadataSlots.locate_spec
+#print axioms CurrentMain.PackedMetadataSlots.locate_none
+#print axioms CurrentMain.PackedMetadataSlots.locate_unique
+#print axioms CurrentMain.PackedMetadataSlots.pack_capacity
+#print axioms CurrentMain.PackedMetadataSlots.uniform_capacity
+#print axioms CurrentMain.PackedMetadataSlots.focus_pack
+#print axioms CurrentMain.PackedMetadataSlots.run_focused
+#print axioms CurrentMain.PackedMetadataSlots.run_repacked
+#print axioms CurrentMain.PackedMetadataSlots.located_storage
+#print axioms CurrentMain.PackedMetadataSlots.metadata_avoids
+#print axioms CurrentMain.PackedMetadataSlots.located_toggle
+#print axioms CurrentMain.PackedMetadataSlots.located_clear
+#check @CurrentMain.PackedMetadataSlots.located_toggle
+#check @CurrentMain.PackedMetadataSlots.located_storage
diff --git a/research/lean-paid-positioned-acquisition/sources/PaidPairedAcquisitionResources.lean b/research/lean-paid-positioned-acquisition/sources/PaidPairedAcquisitionResources.lean
new file mode 100644
index 0000000000..f927f1128e
--- /dev/null
+++ b/research/lean-paid-positioned-acquisition/sources/PaidPairedAcquisitionResources.lean
@@ -0,0 +1,121 @@
+import PaidPairedTrackAcquisition
+
+/-!
+Copyright (c) 2026 James Chang. Apache-2.0. OpenAI-assisted.
+Whole-prefix storage and original-entrance volume for the unchanged three-tape
+acquisition controller. Actual access, both charged switches, framed copying,
+and home return are all covered, including terminal stuttering. The two symbols
+of every stored delimiter are counted. No new transition or execution premise.
+The input volume includes the complete supplied store and unary control; the
+new output is initially empty and its allocation is charged. This is a finite
+marked multitape model bound, with physical input construction still explicit.
+Author-checked context kappa=836330098538459/500000000000000000.
+-/
+set_option Elab.async false
+set_option autoImplicit false
+namespace CurrentMain.PaidPairedAcquisitionResources
+open PairedBitXorScan (Tape)
+open PackedMetadataSlots (Block pack capacity)
+open SequentialBitAddition (Registers)
+open PaidPairedTrackAcquisition
+
+private theorem capacity_append (pre post : List Block) :
+    capacity (pre++post)=capacity pre+capacity post := by
+  induction pre with
+  | nil => simp only [List.nil_append,capacity,Nat.zero_add]
+  | cons b pre ih => simp [capacity,ih,Nat.add_assoc]
+private theorem unary_cells (n : Nat) : tapeCells (PositionalMetadataAccess.unary n)=n+2 := by
+  simp [tapeCells,PositionalMetadataAccess.unary,Nat.add_assoc,Nat.add_comm,Nat.add_left_comm]
+private theorem output_cells (second : Bool) (selected : Block) :
+    tapeCells (PairedTrackExtraction.final second selected.rows).output=selected.rows.length+2 := by
+  simp [tapeCells,PairedTrackExtraction.final,MarkedZeroPadding.marked,MarkedZeroPadding.bits,
+    Nat.add_assoc,Nat.add_comm,Nat.add_left_comm]
+
+/-- The access phase preserves the whole store and supplied control exactly. -/
+theorem access_prefix_cells (second : Bool) (pre : List Block) (selected : Block) (post : List Block)
+    (scratch : Bool) (r : Registers) (k : Nat) (hk : k≤travel pre) :
+    cells (run second k (initial pre.length (pre++selected::post) scratch r))=
+      capacity (pre++selected::post)+(pre.length+2) := by
+  rw [access_prefix second pre selected post scratch r k hk]
+  change 0+PositionalMetadataAccess.cells (PositionalMetadataAccess.run k
+    (PositionalMetadataAccess.initial pre.length (pre++selected::post) scratch))=_
+  rw [Nat.zero_add,PositionalMetadataAccess.access_storage]
+
+/-- This includes the post-entry state and the terminal copy state; both source
+contexts and the separately carried positional control are counted. -/
+theorem extraction_prefix_cells (second : Bool) (pre : List Block) (selected : Block) (post : List Block)
+    (scratch : Bool) (r : Registers) (j : Nat) (hj : j≤copyTime selected) :
+    cells (run second (travel pre+1+j) (initial pre.length (pre++selected::post) scratch r))≤
+      capacity (pre++selected::post)+pre.length+selected.rows.length+4 := by
+  rw [extraction_prefix second pre selected post scratch r j hj]
+  change tapeCells (PositionalMetadataAccess.unary pre.length)+
+    PairedTrackExtraction.cells (PairedTrackExtraction.run second j (focusedInitial pre selected post r))≤_
+  rw [unary_cells]
+  have h:=PairedTrackExtractionFraming.framed_storage second (pack pre).reverse (pack post) selected.rows r j
+  change PairedTrackExtraction.cells (PairedTrackExtraction.run second j (focusedInitial pre selected post r))≤_ at h
+  simp only [List.length_reverse,PackedMetadataSlots.pack_capacity] at h
+  rw [capacity_append]
+  simp only [capacity]
+  omega
+
+/-- Actual return and arbitrary later halt stuttering preserve full allocated
+storage, including the completed output and the unary control. -/
+theorem home_suffix_cells (second : Bool) (pre : List Block) (selected : Block) (post : List Block)
+    (scratch : Bool) (r : Registers) (j : Nat) :
+    cells (run second (travel pre+1+copyTime selected+1+j)
+      (initial pre.length (pre++selected::post) scratch r))=
+      capacity (pre++selected::post)+pre.length+selected.rows.length+4 := by
+  rw [home_suffix]
+  change tapeCells (PairedTrackExtraction.final second selected.rows).output+
+    PositionalMetadataReturn.cells (PositionalMetadataReturn.run j
+      (PositionalMetadataReturn.initial pre selected post scratch))=_
+  rw [output_cells,PositionalMetadataReturn.return_storage]
+  omega
+
+/-- The split includes both charged handoffs; no prefix is omitted. -/
+theorem machine_storage (second : Bool) (pre : List Block) (selected : Block) (post : List Block)
+    (scratch : Bool) (r : Registers) (k : Nat) :
+    cells (run second k (initial pre.length (pre++selected::post) scratch r))≤
+      capacity (pre++selected::post)+pre.length+selected.rows.length+4 := by
+  by_cases ha:k≤travel pre
+  · rw [access_prefix_cells second pre selected post scratch r k ha]
+    omega
+  · by_cases he:k≤travel pre+1+copyTime selected
+    · have hs:k=travel pre+1+(k-(travel pre+1)):=by omega
+      rw [hs]
+      exact extraction_prefix_cells second pre selected post scratch r _ (by omega)
+    · have hs:k=travel pre+1+copyTime selected+1+(k-(travel pre+1+copyTime selected+1)):=by omega
+      rw [hs,home_suffix_cells]
+
+/-- Constant bounds in the complete original represented entrance volume.
+The initially empty output is not silently preallocated. -/
+theorem entrance_resources (second : Bool) (pre : List Block) (selected : Block) (post : List Block)
+    (scratch : Bool) (r : Registers) :
+    let s:=initial pre.length (pre++selected::post) scratch r
+    totalTime pre selected≤7*cells s ∧
+    run second (totalTime pre selected) s=final second pre selected post scratch ∧
+    Halted (final second pre selected post scratch) ∧
+    (∀ k<totalTime pre selected,¬Halted (run second k s)) ∧
+    (∀ k,cells (run second k s)≤2*cells s) := by
+  dsimp only
+  have hi:=initial_cells pre.length (pre++selected::post) scratch r
+  have hc:capacity (pre++selected::post)=capacity pre+selected.rows.length+2+capacity post := by
+    rw [capacity_append]
+    simp only [capacity]
+    omega
+  obtain ⟨hr,hh,hl⟩:=machine_result second pre selected post scratch r
+  refine ⟨?_,hr,hh,hl,?_⟩
+  · rw [time_eq,hi]
+    omega
+  · intro k
+    have h:=machine_storage second pre selected post scratch r k
+    rw [hi]
+    omega
+
+end CurrentMain.PaidPairedAcquisitionResources
+#print axioms CurrentMain.PaidPairedAcquisitionResources.access_prefix_cells
+#print axioms CurrentMain.PaidPairedAcquisitionResources.extraction_prefix_cells
+#print axioms CurrentMain.PaidPairedAcquisitionResources.home_suffix_cells
+#print axioms CurrentMain.PaidPairedAcquisitionResources.machine_storage
+#print axioms CurrentMain.PaidPairedAcquisitionResources.entrance_resources
+#check @CurrentMain.PaidPairedAcquisitionResources.entrance_resources
diff --git a/research/lean-paid-positioned-acquisition/sources/PaidPairedTrackAcquisition.lean b/research/lean-paid-positioned-acquisition/sources/PaidPairedTrackAcquisition.lean
new file mode 100644
index 0000000000..2f0e19c13b
--- /dev/null
+++ b/research/lean-paid-positioned-acquisition/sources/PaidPairedTrackAcquisition.lean
@@ -0,0 +1,210 @@
+import PairedTrackExtractionFraming
+import PositionalMetadataReturn
+
+/-!
+Copyright (c) 2026 James Chang. Apache-2.0. OpenAI-assisted.
+Three-tape paid acquisition from an existing packed store: actual positional
+access, one charged handoff, unchanged chosen-track extraction, one charged
+handoff and actual return to global home. Both pair tracks and all other packed
+blocks are preserved, as is the supplied unary control and Boolean scratch.
+The fresh output starts empty; the copy machine writes its markers and bits.
+Its seven registers are cleared, rather than restoring their old dirty values.
+
+All input symbols and the ordered layout are supplied. A logical locate result
+only selects that layout; no runtime key search, free tape relayout or Nat-to-bit
+conversion occurs. The track selector is a fixed Boolean program parameter.
+Author-checked conditional context kappa=836330098538459/500000000000000000.
+-/
+set_option Elab.async false
+set_option autoImplicit false
+namespace CurrentMain.PaidPairedTrackAcquisition
+open PairedBitXorScan (Tape Pair)
+open PackedMetadataSlots (Block Focus pack capacity locate)
+open PositionalMetadataAccess (ControlSymbol)
+open SequentialBitAddition (Registers)
+abbrev OutputTape := Tape MarkedZeroPadding.Symbol
+
+inductive State where
+  | access (output : OutputTape) (registers : Registers) (s : PositionalMetadataAccess.State)
+  | extracting (control : Tape ControlSymbol) (scratch : Bool) (s : PairedTrackExtraction.State)
+  | home (output : OutputTape) (registers : Registers) (s : PositionalMetadataReturn.State)
+
+def step (second : Bool) : State → State
+  | .access output registers s =>
+      if s.phase=.halt then
+        .extracting s.controlTape s.scratch ⟨s.dataTape,output,registers,.writeOutputLeft⟩
+      else .access output registers (PositionalMetadataAccess.step s)
+  | .extracting control scratch s =>
+      if s.phase=.halt then
+        .home s.output s.registers ⟨s.source,control,scratch,.enterControl⟩
+      else .extracting control scratch (PairedTrackExtraction.step second s)
+  | .home output registers s => .home output registers (PositionalMetadataReturn.step s)
+
+def run (second : Bool) : Nat → State → State
+  | 0,s => s
+  | k+1,s => run second k (step second s)
+def Halted : State → Prop
+  | .home _ _ s => s.phase=.halt
+  | _ => False
+
+def tapeCells {α : Type} (s : Tape α) : Nat := s.left.length+s.right.length
+def cells : State → Nat
+  | .access out _ s => tapeCells out+PositionalMetadataAccess.cells s
+  | .extracting control _ s => tapeCells control+PairedTrackExtraction.cells s
+  | .home out _ s => tapeCells out+PositionalMetadataReturn.cells s
+
+def initial (position : Nat) (blocks : List Block) (scratch : Bool) (r : Registers) : State :=
+  .access ⟨[],[]⟩ r (PositionalMetadataAccess.initial position blocks scratch)
+def focusedInitial (pre : List Block) (selected : Block) (post : List Block) (r : Registers) : PairedTrackExtraction.State :=
+  PairedTrackExtractionFraming.embed (pack pre).reverse (pack post) (PairedTrackExtraction.initial selected.rows r)
+def focusedFinal (second : Bool) (pre : List Block) (selected : Block) (post : List Block) : PairedTrackExtraction.State :=
+  PairedTrackExtractionFraming.embed (pack pre).reverse (pack post) (PairedTrackExtraction.final second selected.rows)
+def final (second : Bool) (pre : List Block) (selected : Block) (post : List Block) (scratch : Bool) : State :=
+  .home (PairedTrackExtraction.final second selected.rows).output SequentialBitAddition.clearRegisters
+    (PositionalMetadataReturn.final pre.length (pre++selected::post) scratch)
+def travel (pre : List Block) : Nat := capacity pre+2*pre.length+4
+def copyTime (selected : Block) : Nat := 6*selected.rows.length+16
+def totalTime (pre : List Block) (selected : Block) : Nat := travel pre+1+copyTime selected+1+travel pre
+
+private theorem run_add (second : Bool) (m n : Nat) (s : State) :
+    run second (m+n) s=run second n (run second m s) := by
+  induction m generalizing s with
+  | zero => simp only [Nat.zero_add,run]
+  | succ m ih => simpa only [Nat.succ_add,run] using ih (step second s)
+private theorem run_succ (second : Bool) (k : Nat) (s : State) :
+    run second (k+1) s=step second (run second k s) := by
+  induction k generalizing s with
+  | zero => rfl
+  | succ k ih => exact ih (step second s)
+private theorem access_succ (k : Nat) (s : PositionalMetadataAccess.State) :
+    PositionalMetadataAccess.run (k+1) s=PositionalMetadataAccess.step (PositionalMetadataAccess.run k s) := by
+  induction k generalizing s with
+  | zero => rfl
+  | succ k ih => exact ih (PositionalMetadataAccess.step s)
+private theorem extracting_succ (second : Bool) (k : Nat) (s : PairedTrackExtraction.State) :
+    PairedTrackExtraction.run second (k+1) s=PairedTrackExtraction.step second (PairedTrackExtraction.run second k s) := by
+  induction k generalizing s with
+  | zero => rfl
+  | succ k ih => exact ih (PairedTrackExtraction.step second s)
+private theorem access_upto (second : Bool) (out : OutputTape) (r : Registers) (s : PositionalMetadataAccess.State) (k : Nat)
+    (h : ∀ j<k,(PositionalMetadataAccess.run j s).phase≠.halt) :
+    run second k (.access out r s)=.access out r (PositionalMetadataAccess.run k s) := by
+  induction k with
+  | zero => rfl
+  | succ k ih =>
+      rw [run_succ,ih (fun j hj=>h j (by omega)),access_succ]
+      simp only [step,if_neg (h k (by omega))]
+private theorem extracting_upto (second : Bool) (control : Tape ControlSymbol) (scratch : Bool)
+    (s : PairedTrackExtraction.State) (k : Nat)
+    (h : ∀ j<k,(PairedTrackExtraction.run second j s).phase≠.halt) :
+    run second k (.extracting control scratch s)=.extracting control scratch (PairedTrackExtraction.run second k s) := by
+  induction k with
+  | zero => rfl
+  | succ k ih =>
+      rw [run_succ,ih (fun j hj=>h j (by omega)),extracting_succ]
+      simp only [step,if_neg (h k (by omega))]
+private theorem home_run (second : Bool) (out : OutputTape) (r : Registers) (s : PositionalMetadataReturn.State) (k : Nat) :
+    run second k (.home out r s)=.home out r (PositionalMetadataReturn.run k s) := by
+  induction k generalizing s with
+  | zero => rfl
+  | succ k ih => exact ih (PositionalMetadataReturn.step s)
+
+theorem access_prefix (second : Bool) (pre : List Block) (selected : Block) (post : List Block)
+    (scratch : Bool) (r : Registers) (k : Nat) (hk : k≤travel pre) :
+    run second k (initial pre.length (pre++selected::post) scratch r)=
+      .access ⟨[],[]⟩ r (PositionalMetadataAccess.run k (PositionalMetadataAccess.initial pre.length (pre++selected::post) scratch)) := by
+  apply access_upto
+  intro j hj
+  exact (PositionalMetadataAccess.access_first_halt pre selected post scratch).2 j
+    (by simpa only [travel] using Nat.lt_of_lt_of_le hj hk)
+
+/-- This charged switch passes the reached head and existing output allocation. -/
+theorem enter_extraction (second : Bool) (pre : List Block) (selected : Block) (post : List Block)
+    (scratch : Bool) (r : Registers) :
+    run second (travel pre+1) (initial pre.length (pre++selected::post) scratch r)=
+      .extracting (PositionalMetadataAccess.unary pre.length) scratch (focusedInitial pre selected post r) := by
+  rw [run_succ,access_prefix second pre selected post scratch r _ (Nat.le_refl _)]
+  rw [show travel pre=capacity pre+2*pre.length+4 from rfl,PositionalMetadataAccess.access_result]
+  rfl
+
+theorem extraction_prefix (second : Bool) (pre : List Block) (selected : Block) (post : List Block)
+    (scratch : Bool) (r : Registers) (j : Nat) (hj : j≤copyTime selected) :
+    run second (travel pre+1+j) (initial pre.length (pre++selected::post) scratch r)=
+      .extracting (PositionalMetadataAccess.unary pre.length) scratch
+        (PairedTrackExtraction.run second j (focusedInitial pre selected post r)) := by
+  rw [run_add,enter_extraction]
+  apply extracting_upto
+  intro k hk
+  exact (PairedTrackExtractionFraming.framed_result second (pack pre).reverse (pack post) selected.rows r).2 k
+    (by simpa only [copyTime] using Nat.lt_of_lt_of_le hk hj)
+
+/-- The actual source is passed back to the return controller, without repacking. -/
+theorem home_handoff (second : Bool) (pre : List Block) (selected : Block) (post : List Block) (scratch : Bool) :
+    step second (.extracting (PositionalMetadataAccess.unary pre.length) scratch (focusedFinal second pre selected post))=
+      .home (PairedTrackExtraction.final second selected.rows).output SequentialBitAddition.clearRegisters
+        (PositionalMetadataReturn.initial pre selected post scratch) := rfl
+
+theorem home_suffix (second : Bool) (pre : List Block) (selected : Block) (post : List Block)
+    (scratch : Bool) (r : Registers) (j : Nat) :
+    run second (travel pre+1+copyTime selected+1+j) (initial pre.length (pre++selected::post) scratch r)=
+      .home (PairedTrackExtraction.final second selected.rows).output SequentialBitAddition.clearRegisters
+        (PositionalMetadataReturn.run j (PositionalMetadataReturn.initial pre selected post scratch)) := by
+  have hr := (PairedTrackExtractionFraming.framed_result second (pack pre).reverse (pack post) selected.rows r).1
+  change PairedTrackExtraction.run second (copyTime selected) (focusedInitial pre selected post r)=focusedFinal second pre selected post at hr
+  rw [run_add,run_succ,extraction_prefix second pre selected post scratch r _ (Nat.le_refl _),hr,home_handoff,home_run]
+
+/-- Exact first halt, all original packed symbols and the control restored at
+home, with a newly written chosen-track word. Both handoffs are charged. -/
+theorem machine_result (second : Bool) (pre : List Block) (selected : Block) (post : List Block)
+    (scratch : Bool) (r : Registers) :
+    run second (totalTime pre selected) (initial pre.length (pre++selected::post) scratch r)=final second pre selected post scratch ∧
+    Halted (final second pre selected post scratch) ∧
+    ∀ k<totalTime pre selected,¬Halted (run second k (initial pre.length (pre++selected::post) scratch r)) := by
+  refine ⟨?_,rfl,?_⟩
+  · unfold totalTime
+    rw [home_suffix,show travel pre=capacity pre+2*pre.length+4 from rfl,PositionalMetadataReturn.return_result]
+    rfl
+  · intro k hk
+    by_cases ha:k≤travel pre
+    · rw [access_prefix second pre selected post scratch r k ha]
+      exact fun h=>h
+    · by_cases he:k≤travel pre+1+copyTime selected
+      · have hs:k=travel pre+1+(k-(travel pre+1)):=by omega
+        rw [hs,extraction_prefix second pre selected post scratch r _ (by omega)]
+        exact fun h=>h
+      · have hs:k=travel pre+1+copyTime selected+1+(k-(travel pre+1+copyTime selected+1)):=by omega
+        rw [hs,home_suffix]
+        apply (PositionalMetadataReturn.return_first_halt pre selected post scratch).2
+        simpa only [travel] using (show k-(travel pre+1+copyTime selected+1)<travel pre by unfold totalTime at hk;omega)
+
+theorem time_eq (pre : List Block) (selected : Block) :
+    totalTime pre selected=2*capacity pre+4*pre.length+6*selected.rows.length+26 := by
+  unfold totalTime travel copyTime
+  omega
+
+theorem initial_cells (position : Nat) (blocks : List Block) (scratch : Bool) (r : Registers) :
+    cells (initial position blocks scratch r)=capacity blocks+(position+2) := by
+  simp only [initial,cells,tapeCells,PositionalMetadataAccess.initial,PositionalMetadataAccess.cells,
+    PositionalMetadataAccess.tapeCells,PositionalMetadataAccess.unary,List.length_nil,List.length_cons,
+    List.length_append,List.length_replicate,PackedMetadataSlots.pack_capacity]
+  omega
+
+/-- Logical first-match evidence supplies only the existing split and position. -/
+theorem acquisition_from_locate (second : Bool) (key : Nat) (blocks : List Block) (f : Focus)
+    (located : locate key blocks=some f) (scratch : Bool) (r : Registers) :
+    run second (totalTime f.before f.selected) (initial f.before.length blocks scratch r)=final second f.before f.selected f.after scratch ∧
+    Halted (final second f.before f.selected f.after scratch) ∧
+    ∀ k<totalTime f.before f.selected,¬Halted (run second k (initial f.before.length blocks scratch r)) := by
+  obtain ⟨he,_,_⟩:=PackedMetadataSlots.locate_spec key blocks f located
+  rw [he]
+  exact machine_result second f.before f.selected f.after scratch r
+
+end CurrentMain.PaidPairedTrackAcquisition
+#print axioms CurrentMain.PaidPairedTrackAcquisition.enter_extraction
+#print axioms CurrentMain.PaidPairedTrackAcquisition.home_handoff
+#print axioms CurrentMain.PaidPairedTrackAcquisition.machine_result
+#print axioms CurrentMain.PaidPairedTrackAcquisition.time_eq
+#print axioms CurrentMain.PaidPairedTrackAcquisition.initial_cells
+#print axioms CurrentMain.PaidPairedTrackAcquisition.acquisition_from_locate
+#check @CurrentMain.PaidPairedTrackAcquisition.machine_result
+#check @CurrentMain.PaidPairedTrackAcquisition.acquisition_from_locate
diff --git a/research/lean-paid-positioned-acquisition/sources/PairedTrackExtraction.lean b/research/lean-paid-positioned-acquisition/sources/PairedTrackExtraction.lean
new file mode 100644
index 0000000000..19b2d96531
--- /dev/null
+++ b/research/lean-paid-positioned-acquisition/sources/PairedTrackExtraction.lean
@@ -0,0 +1,260 @@
+import MarkedBitDifference
+import MarkedBitXorScan
+
+/-!
+Copyright (c) 2026 James Chang. Apache-2.0. OpenAI-assisted.
+Finite-alphabet specialization of the accepted MarkedBitDifference copy phase.
+The actual source is the existing two-track packed-store alphabet; each read
+selects one Boolean at the current cell. The program parameter second chooses
+the track. Source writes and whole-tape maps never occur in the transition.
+
+A proof-only embedding places each pair p in the row (p,chosen p), allowing
+reuse of the accepted extraction trace, marker handling, return and seven
+register clears. Both original pair bits and the source head are preserved.
+The output is a separately supplied blank tape; its markers and bits are paid.
+Ambient source framing and access/home composition are subsequent obligations.
+Old registers are cleared rather than restored. The 6w+16 transition count is
+for the declared finite multitape model, not an unbounded-arithmetic invoice.
+Author-checked context kappa=836330098538459/500000000000000000.
+-/
+set_option Elab.async false
+set_option autoImplicit false
+namespace CurrentMain.PairedTrackExtraction
+open PairedBitXorScan (Tape Pair)
+open SequentialBitAddition (Registers ClearSlot)
+abbrev Symbol := MarkedBitXorScan.Symbol
+abbrev BitSymbol := MarkedZeroPadding.Symbol
+
+def chosen (second:Bool) (p:Pair) : Bool := if second then p.2 else p.1
+inductive Phase where
+  | writeOutputLeft | enterOutput | enterInput | copyTest | copyWrite
+  | advanceInput | advanceOutput | writeOutputRight | rewindOutput | rewindInput
+  | clear (slot:ClearSlot) | halt
+  deriving DecidableEq
+structure State where
+  source : Tape Symbol
+  output : Tape BitSymbol
+  registers : Registers
+  phase : Phase
+  deriving DecidableEq
+
+def afterClear : ClearSlot → Phase
+  | .x => .clear .y
+  | .y => .clear .carry
+  | .carry => .clear .xorXY
+  | .xorXY => .clear .sum
+  | .sum => .clear .andXY
+  | .andXY => .clear .andTC
+  | .andTC => .halt
+
+/-- A finite current-symbol transition, with one chosen-bit read, output
+write or head move in each corresponding inherited phase. -/
+def step (second:Bool) (s:State) : State :=
+  match s.phase with
+  | .halt => s
+  | .writeOutputLeft => {s with output:=s.output.writeHead .leftMarker,phase:=.enterOutput}
+  | .enterOutput => {s with output:=s.output.moveRight .blank,phase:=.enterInput}
+  | .enterInput => {s with source:=s.source.moveRight .blank,phase:=.copyTest}
+  | .copyTest => match s.source.readHead .blank with
+    | .data a b => {s with registers:={s.registers with sum:=chosen second (a,b)},phase:=.copyWrite}
+    | .rightMarker => {s with phase:=.writeOutputRight}
+    | _ => {s with phase:=.halt}
+  | .copyWrite => {s with output:=s.output.writeHead (.data s.registers.sum),phase:=.advanceInput}
+  | .advanceInput => {s with source:=s.source.moveRight .blank,phase:=.advanceOutput}
+  | .advanceOutput => {s with output:=s.output.moveRight .blank,phase:=.copyTest}
+  | .writeOutputRight => {s with output:=s.output.writeHead .rightMarker,phase:=.rewindOutput}
+  | .rewindOutput => if s.output.readHead .blank=.leftMarker then {s with phase:=.rewindInput}
+      else {s with output:=s.output.moveLeft .blank}
+  | .rewindInput => if s.source.readHead .blank=.leftMarker then {s with phase:=.clear .x}
+      else {s with source:=s.source.moveLeft .blank}
+  | .clear slot => {s with registers:=SequentialBitAddition.clearSlot slot s.registers,phase:=afterClear slot}
+
+def run (second:Bool) : Nat → State → State
+  | 0,s => s
+  | k+1,s => run second k (step second s)
+
+/-- Proof-only alphabet map; absent from the executed step. -/
+def rowOf (second:Bool) (p:Pair) : SequentialBitAddition.Row := (p,chosen second p)
+def symbolOf (second:Bool) : Symbol → MarkedBitAddition.Symbol
+  | .blank => .blank
+  | .leftMarker => .leftMarker
+  | .rightMarker => .rightMarker
+  | .data a b => .data (rowOf second (a,b))
+def tapeOf (second:Bool) (t:Tape Symbol) : Tape MarkedBitAddition.Symbol :=
+  ⟨t.left.map (symbolOf second),t.right.map (symbolOf second)⟩
+def phaseOf : Phase → MarkedBitDifference.Phase
+  | .writeOutputLeft => .writeOutputLeft
+  | .enterOutput => .enterOutput
+  | .enterInput => .enterInput
+  | .copyTest => .copyTest
+  | .copyWrite => .copyWrite
+  | .advanceInput => .copyAdvanceInput
+  | .advanceOutput => .copyAdvanceOutput
+  | .writeOutputRight => .writeOutputRight
+  | .rewindOutput => .rewindOutput
+  | .rewindInput => .rewindInput
+  | .clear slot => .clear slot
+  | .halt => .halt
+def model (second:Bool) (s:State) : MarkedBitDifference.State :=
+  ⟨tapeOf second s.source,s.output,s.registers,false,phaseOf s.phase⟩
+
+private theorem tapeOf_read (second:Bool) (t:Tape Symbol) :
+    (tapeOf second t).readHead .blank=symbolOf second (t.readHead .blank) := by
+  rcases t with ⟨ls,rs⟩
+  cases rs <;> rfl
+private theorem tapeOf_right (second:Bool) (t:Tape Symbol) :
+    tapeOf second (t.moveRight .blank)=(tapeOf second t).moveRight .blank := by
+  rcases t with ⟨ls,rs⟩
+  cases rs <;> rfl
+private theorem tapeOf_left (second:Bool) (t:Tape Symbol) :
+    tapeOf second (t.moveLeft .blank)=(tapeOf second t).moveLeft .blank := by
+  rcases t with ⟨ls,rs⟩
+  cases ls <;> rfl
+private theorem symbolOf_left (second:Bool) (s:Symbol) :
+    (symbolOf second s=MarkedBitAddition.Symbol.leftMarker)↔s=.leftMarker := by
+  cases s <;> simp [symbolOf]
+
+/-- Every real transition refines the existing extraction phase. -/
+theorem model_step (second:Bool) (s:State) :
+    model second (step second s)=MarkedBitDifference.step (model second s) := by
+  rcases s with ⟨src,out,r,p⟩
+  cases p with
+  | copyTest =>
+      cases h:src.readHead .blank <;>
+        simp [step,model,phaseOf,tapeOf_read,h,symbolOf,MarkedBitDifference.step,rowOf]
+  | rewindOutput =>
+      by_cases h:out.readHead .blank=.leftMarker <;>
+        simp [step,model,phaseOf,MarkedBitDifference.step,h]
+  | rewindInput =>
+      by_cases h:src.readHead .blank=.leftMarker <;>
+        simp [step,model,phaseOf,MarkedBitDifference.step,tapeOf_read,symbolOf_left,h,tapeOf_left]
+  | clear slot =>
+      cases slot <;> rfl
+  | _ => simp [step,model,phaseOf,MarkedBitDifference.step,tapeOf_right]
+
+theorem model_run (second:Bool) (s:State) (k:Nat) :
+    model second (run second k s)=MarkedBitDifference.run k (model second s) := by
+  induction k generalizing s with
+  | zero => rfl
+  | succ k ih => rw [run,ih,model_step,MarkedBitDifference.run]
+
+private def symbolBack : MarkedBitAddition.Symbol → Symbol
+  | .blank => .blank
+  | .leftMarker => .leftMarker
+  | .rightMarker => .rightMarker
+  | .data p => .data p.1.1 p.1.2
+private def phaseBack : MarkedBitDifference.Phase → Phase
+  | .writeOutputLeft => .writeOutputLeft
+  | .enterOutput => .enterOutput
+  | .enterInput => .enterInput
+  | .copyTest => .copyTest
+  | .copyWrite => .copyWrite
+  | .copyAdvanceInput => .advanceInput
+  | .copyAdvanceOutput => .advanceOutput
+  | .writeOutputRight => .writeOutputRight
+  | .rewindOutput => .rewindOutput
+  | .rewindInput => .rewindInput
+  | .clear slot => .clear slot
+  | _ => .halt
+private def back (s:MarkedBitDifference.State) : State :=
+  ⟨⟨s.tape.left.map symbolBack,s.tape.right.map symbolBack⟩,s.output,s.registers,phaseBack s.phase⟩
+private theorem symbol_back (second:Bool) (s:Symbol) : symbolBack (symbolOf second s)=s := by
+  cases s <;> rfl
+private theorem back_model (second:Bool) (s:State) : back (model second s)=s := by
+  rcases s with ⟨⟨ls,rs⟩,out,r,p⟩
+  cases p <;> simp [back,model,tapeOf,phaseOf,phaseBack,List.map_map,Function.comp_def,symbol_back]
+private theorem model_injective (second:Bool) : Function.Injective (model second) := by
+  intro s t h
+  have hb:=congrArg back h
+  simpa only [back_model] using hb
+private theorem model_halt (second:Bool) (s:State) :
+    (model second s).phase=.halt ↔ s.phase=.halt := by
+  cases hp:s.phase <;> simp [model,phaseOf,hp]
+
+def initial (rows:List Pair) (r:Registers) : State :=
+  ⟨⟨[],MarkedBitXorScan.marked rows⟩,⟨[],[]⟩,r,.writeOutputLeft⟩
+def final (second:Bool) (rows:List Pair) : State :=
+  ⟨⟨[],MarkedBitXorScan.marked rows⟩,
+    MarkedZeroPadding.marked (MarkedZeroPadding.bits (rows.map (chosen second))),
+    SequentialBitAddition.clearRegisters,.halt⟩
+private theorem model_initial (second:Bool) (rows:List Pair) (r:Registers) :
+    model second (initial rows r)=
+      (⟨MarkedBitAddition.marked (rows.map (rowOf second)),⟨[],[]⟩,r,false,.writeOutputLeft⟩:MarkedBitDifference.State) := by
+  simp [model,initial,tapeOf,MarkedBitXorScan.marked,MarkedBitAddition.marked,
+    List.map_map,Function.comp_def,symbolOf,MarkedBitXorScan.dataSymbol,phaseOf]
+private theorem model_final (second:Bool) (rows:List Pair) :
+    model second (final second rows)=MarkedBitDifference.copyFinal (rows.map (rowOf second)) false := by
+  simp [model,final,tapeOf,MarkedBitXorScan.marked,MarkedBitAddition.marked,
+    MarkedBitDifference.copyFinal,List.map_map,Function.comp_def,symbolOf,rowOf,phaseOf,MarkedBitXorScan.dataSymbol]
+
+-- Generic observations of the imported trace are repeated only because
+-- those helpers are private; the extraction algorithm/trace is reused.
+private theorem trace_sound {k:Nat} {s t:MarkedBitDifference.State}
+    (h:MarkedBitDifference.Trace k s t) : MarkedBitDifference.run k s=t := by
+  induction h with
+  | nil => rfl
+  | next _ _ ih => exact ih
+private theorem trace_live {n:Nat} {s t:MarkedBitDifference.State}
+    (h:MarkedBitDifference.Trace n s t) (k:Nat) (hk:k<n) : (MarkedBitDifference.run k s).phase≠.halt := by
+  induction h generalizing k with
+  | nil => omega
+  | next live tail ih => cases k with
+    | zero => exact live
+    | succ k => exact ih k (by omega)
+
+/-- Literal returned source, paid chosen-bit output, first halt and cleared
+registers are inherited from the actual refined extraction trace. -/
+theorem extraction_result (second:Bool) (rows:List Pair) (r:Registers) :
+    run second (6*rows.length+16) (initial rows r)=final second rows ∧
+    (final second rows).phase=.halt ∧
+    ∀ k<6*rows.length+16,(run second k (initial rows r)).phase≠.halt := by
+  have ht:=MarkedBitDifference.extraction_exact (rows.map (rowOf second)) r false
+  simp only [List.length_map] at ht
+  have hr:=trace_sound ht
+  rw [← model_initial,← model_final,← model_run] at hr
+  refine ⟨model_injective second hr,rfl,?_⟩
+  intro k hk hh
+  have hl:=trace_live ht k hk
+  rw [← model_initial,← model_run] at hl
+  exact hl ((model_halt second _).mpr hh)
+
+def cells (s:State) : Nat :=
+  s.source.left.length+s.source.right.length+s.output.left.length+s.output.right.length
+private theorem model_cells (second:Bool) (s:State) : MarkedBitDifference.cells (model second s)=cells s := by
+  simp [model,tapeOf,cells,MarkedBitDifference.cells,MarkedBitDifference.tapeCells,Nat.add_assoc]
+private theorem halt_run (s:MarkedBitDifference.State) (h:s.phase=.halt) (k:Nat) : MarkedBitDifference.run k s=s := by
+  induction k with
+  | zero => rfl
+  | succ k ih => simpa [MarkedBitDifference.run,MarkedBitDifference.step,h] using ih
+private theorem trace_storage {n:Nat} {s t:MarkedBitDifference.State}
+    (h:MarkedBitDifference.Trace n s t) (ht:t.phase=.halt) (k:Nat) :
+    MarkedBitDifference.cells (MarkedBitDifference.run k s)≤MarkedBitDifference.cells t := by
+  induction h generalizing k with
+  | nil s => rw [halt_run s ht]
+  | @next n s t live tail ih => cases k with
+    | zero => exact (MarkedBitDifference.step_cells s).trans (ih ht 0)
+    | succ k => exact ih ht k
+
+theorem extraction_storage (second:Bool) (rows:List Pair) (r:Registers) (k:Nat) :
+    cells (run second k (initial rows r))≤2*rows.length+4 := by
+  have ht:=MarkedBitDifference.extraction_exact (rows.map (rowOf second)) r false
+  have hs:=trace_storage ht rfl k
+  rw [← model_initial,← model_final,← model_run,model_cells,model_cells] at hs
+  simpa [cells,final,MarkedBitXorScan.marked,MarkedZeroPadding.marked,MarkedZeroPadding.bits,
+    Nat.two_mul,Nat.add_assoc,Nat.add_comm,Nat.add_left_comm] using hs
+
+theorem output_value (second:Bool) (rows:List Pair) (r:Registers) :
+    (run second (6*rows.length+16) (initial rows r)).source=⟨[],MarkedBitXorScan.marked rows⟩ ∧
+    (run second (6*rows.length+16) (initial rows r)).output=
+      MarkedZeroPadding.marked (MarkedZeroPadding.bits (rows.map (chosen second))) := by
+  rw [(extraction_result second rows r).1]
+  exact ⟨rfl,rfl⟩
+
+end CurrentMain.PairedTrackExtraction
+#print axioms CurrentMain.PairedTrackExtraction.model_step
+#print axioms CurrentMain.PairedTrackExtraction.model_run
+#print axioms CurrentMain.PairedTrackExtraction.extraction_result
+#print axioms CurrentMain.PairedTrackExtraction.extraction_storage
+#print axioms CurrentMain.PairedTrackExtraction.output_value
+#check @CurrentMain.PairedTrackExtraction.extraction_result
+#check @CurrentMain.PairedTrackExtraction.output_value
diff --git a/research/lean-paid-positioned-acquisition/sources/PairedTrackExtractionFraming.lean b/research/lean-paid-positioned-acquisition/sources/PairedTrackExtractionFraming.lean
new file mode 100644
index 0000000000..928d391b3b
--- /dev/null
+++ b/research/lean-paid-positioned-acquisition/sources/PairedTrackExtractionFraming.lean
@@ -0,0 +1,157 @@
+import PairedTrackExtraction
+
+/-!
+Copyright (c) 2026 James Chang. Apache-2.0. OpenAI-assisted.
+Ambient source confinement for the unchanged paired-track extractor. Literal
+markers stop every source scan and rewind. Arbitrary left/right packed-store
+spectators survive every actual prefix, even if they contain markers. The
+fresh output remains a distinct tape, whose allocation is counted.
+This reuses the accepted marked-XOR/writeback framing proof pattern; no copy
+algorithm, assumed endpoint or unpriced tape relayout is introduced.
+Actual access from global home and return are the subsequent charged join.
+Author-checked context kappa=836330098538459/500000000000000000.
+-/
+set_option Elab.async false
+set_option autoImplicit false
+namespace CurrentMain.PairedTrackExtractionFraming
+open PairedBitXorScan (Tape Pair)
+open MarkedBitXorScan (marked dataSymbol)
+open PairedTrackExtraction
+open SequentialBitAddition (Registers)
+
+def embed (left right:List Symbol) (s:State) : State :=
+  {s with source:=⟨s.source.left++left,s.source.right++right⟩}
+
+/-- Only phases whose next source move cannot cross R may inhabit R. -/
+def RightSafe : Phase → Prop
+  | .copyTest | .advanceOutput | .writeOutputRight | .rewindOutput | .rewindInput | .clear _ | .halt => True
+  | _ => False
+inductive Confined : State → Prop where
+  | home (rows:List Pair) (out:Tape BitSymbol) (r:Registers) (p:Phase) :
+      Confined ⟨⟨[],marked rows⟩,out,r,p⟩
+  | body (ls:List Pair) (a b:Bool) (rs:List Pair) (out:Tape BitSymbol) (r:Registers) (p:Phase) :
+      Confined ⟨⟨ls.map dataSymbol++[.leftMarker],.data a b::(rs.map dataSymbol++[.rightMarker])⟩,out,r,p⟩
+  | rightEnd (ls:List Pair) (out:Tape BitSymbol) (r:Registers) (p:Phase) (safe:RightSafe p) :
+      Confined ⟨⟨ls.map dataSymbol++[.leftMarker],[.rightMarker]⟩,out,r,p⟩
+private theorem inside (ls rs:List Pair) (out:Tape BitSymbol) (r:Registers) (p:Phase) (safe:RightSafe p) :
+    Confined ⟨⟨ls.map dataSymbol++[.leftMarker],rs.map dataSymbol++[.rightMarker]⟩,out,r,p⟩ := by
+  cases rs with
+  | nil => exact Confined.rightEnd ls out r p safe
+  | cons row rs => rcases row with ⟨a,b⟩;exact Confined.body ls a b rs out r p
+
+/-- Confinement is derived from the actual finite transition table. -/
+theorem confined_step (second:Bool) {s:State} (h:Confined s) : Confined (step second s) := by
+  cases h with
+  | home rows out r p =>
+      cases p with
+      | enterInput =>
+          simpa [step,marked,Tape.moveRight] using inside [] rows out r .copyTest (by trivial)
+      | advanceInput =>
+          simpa [step,marked,Tape.moveRight] using inside [] rows out r .advanceOutput (by trivial)
+      | copyTest => simpa [step,marked,Tape.readHead] using Confined.home rows out r .halt
+      | rewindInput => simpa [step,marked,Tape.readHead] using Confined.home rows out r (.clear .x)
+      | rewindOutput =>
+          by_cases hh:out.readHead .blank=.leftMarker <;> simp only [step,hh,if_true,if_false]
+          all_goals exact Confined.home _ _ _ _
+      | writeOutputLeft => exact Confined.home _ _ _ _
+      | enterOutput => exact Confined.home _ _ _ _
+      | copyWrite => exact Confined.home _ _ _ _
+      | advanceOutput => exact Confined.home _ _ _ _
+      | writeOutputRight => exact Confined.home _ _ _ _
+      | clear slot => exact Confined.home _ _ _ _
+      | halt => exact Confined.home _ _ _ _
+  | body ls a b rs out r p =>
+      cases p with
+      | enterInput =>
+          simpa [step,Tape.moveRight,dataSymbol] using inside ((a,b)::ls) rs out r .copyTest (by trivial)
+      | advanceInput =>
+          simpa [step,Tape.moveRight,dataSymbol] using inside ((a,b)::ls) rs out r .advanceOutput (by trivial)
+      | copyTest => simpa [step,Tape.readHead] using Confined.body ls a b rs out {r with sum:=chosen second (a,b)} .copyWrite
+      | rewindInput =>
+          cases ls with
+          | nil => simpa [step,Tape.readHead,Tape.moveLeft,marked,dataSymbol] using Confined.home ((a,b)::rs) out r .rewindInput
+          | cons row ls =>
+              rcases row with ⟨x,y⟩
+              simpa [step,Tape.readHead,Tape.moveLeft,dataSymbol] using Confined.body ls x y ((a,b)::rs) out r .rewindInput
+      | rewindOutput =>
+          by_cases hh:out.readHead .blank=.leftMarker <;> simp only [step,hh,if_true,if_false]
+          all_goals exact Confined.body _ _ _ _ _ _ _
+      | writeOutputLeft => exact Confined.body _ _ _ _ _ _ _
+      | enterOutput => exact Confined.body _ _ _ _ _ _ _
+      | copyWrite => exact Confined.body _ _ _ _ _ _ _
+      | advanceOutput => exact Confined.body _ _ _ _ _ _ _
+      | writeOutputRight => exact Confined.body _ _ _ _ _ _ _
+      | clear slot => exact Confined.body _ _ _ _ _ _ _
+      | halt => exact Confined.body _ _ _ _ _ _ _
+  | rightEnd ls out r p safe =>
+      cases p with
+      | writeOutputLeft | enterOutput | enterInput | copyWrite | advanceInput => exact False.elim safe
+      | copyTest => simpa [step,Tape.readHead] using Confined.rightEnd ls out r .writeOutputRight (by trivial)
+      | advanceOutput => exact Confined.rightEnd _ _ _ _ (by trivial)
+      | writeOutputRight => exact Confined.rightEnd _ _ _ _ (by trivial)
+      | rewindOutput =>
+          by_cases hh:out.readHead .blank=.leftMarker <;> simp only [step,hh,if_true,if_false]
+          all_goals exact Confined.rightEnd _ _ _ _ (by trivial)
+      | rewindInput =>
+          cases ls with
+          | nil => simpa [step,Tape.readHead,Tape.moveLeft,marked] using Confined.home [] out r .rewindInput
+          | cons row ls =>
+              rcases row with ⟨x,y⟩
+              simpa [step,Tape.readHead,Tape.moveLeft,dataSymbol] using Confined.body ls x y [] out r .rewindInput
+      | clear slot => cases slot <;> exact Confined.rightEnd _ _ _ _ (by trivial)
+      | halt => exact Confined.rightEnd _ _ _ _ (by trivial)
+
+theorem step_embed (second:Bool) (left right:List Symbol) {s:State} (h:Confined s) :
+    step second (embed left right s)=embed left right (step second s) := by
+  cases h with
+  | home rows out r p =>
+      by_cases hh:out.readHead .blank=.leftMarker <;> cases p <;>
+        simp_all [embed,step,marked,Tape.readHead,Tape.moveRight,Tape.moveLeft,List.append_assoc]
+  | body ls a b rs out r p =>
+      by_cases hh:out.readHead .blank=.leftMarker <;> cases p <;> cases ls <;>
+        simp_all [embed,step,Tape.readHead,Tape.moveRight,Tape.moveLeft,dataSymbol,List.append_assoc]
+  | rightEnd ls out r p safe =>
+      by_cases hh:out.readHead .blank=.leftMarker <;> cases p <;> cases ls <;>
+        simp_all [RightSafe,embed,step,Tape.readHead,Tape.moveRight,Tape.moveLeft,dataSymbol,List.append_assoc]
+
+theorem run_embed (second:Bool) (left right:List Symbol) (s:State) (h:Confined s) (k:Nat) :
+    run second k (embed left right s)=embed left right (run second k s) := by
+  induction k generalizing s with
+  | zero => rfl
+  | succ k ih =>
+      simp only [run]
+      rw [step_embed second left right h]
+      exact ih (step second s) (confined_step second h)
+
+theorem cells_embed (left right:List Symbol) (s:State) :
+    cells (embed left right s)=left.length+cells s+right.length := by
+  simp [embed,cells]
+  omega
+
+/-- The source block and both spectators survive; the fresh output contains
+exactly the selected track. Every marker/return/clear transition is charged. -/
+theorem framed_result (second:Bool) (left right:List Symbol) (rows:List Pair) (r:Registers) :
+    run second (6*rows.length+16) (embed left right (initial rows r))=
+      embed left right (final second rows) ∧
+    ∀ k<6*rows.length+16,(run second k (embed left right (initial rows r))).phase≠.halt := by
+  constructor
+  · rw [run_embed second left right (initial rows r) (Confined.home rows _ r _), (extraction_result second rows r).1]
+  · intro k hk
+    rw [run_embed second left right (initial rows r) (Confined.home rows _ r _)]
+    exact (extraction_result second rows r).2.2 k hk
+
+theorem framed_storage (second:Bool) (left right:List Symbol) (rows:List Pair) (r:Registers) (k:Nat) :
+    cells (run second k (embed left right (initial rows r)))≤left.length+(2*rows.length+4)+right.length := by
+  rw [run_embed second left right (initial rows r) (Confined.home rows _ r _),cells_embed]
+  have h:=extraction_storage second rows r k
+  omega
+
+end CurrentMain.PairedTrackExtractionFraming
+#print axioms CurrentMain.PairedTrackExtractionFraming.confined_step
+#print axioms CurrentMain.PairedTrackExtractionFraming.step_embed
+#print axioms CurrentMain.PairedTrackExtractionFraming.run_embed
+#print axioms CurrentMain.PairedTrackExtractionFraming.cells_embed
+#print axioms CurrentMain.PairedTrackExtractionFraming.framed_result
+#print axioms CurrentMain.PairedTrackExtractionFraming.framed_storage
+#check @CurrentMain.PairedTrackExtractionFraming.framed_result
+#check @CurrentMain.PairedTrackExtractionFraming.framed_storage
diff --git a/research/lean-paid-positioned-acquisition/sources/PositionalMetadataAccess.lean b/research/lean-paid-positioned-acquisition/sources/PositionalMetadataAccess.lean
new file mode 100644
index 0000000000..0ff8857528
--- /dev/null
+++ b/research/lean-paid-positioned-acquisition/sources/PositionalMetadataAccess.lean
@@ -0,0 +1,312 @@
+import PackedMetadataSlots
+
+/-!
+Paid positional access to a supplied finite packed metadata store. A marked
+unary control supplies one tick per preceding block. The actual finite-symbol
+controller reads only current symbols, traverses every preceding L/data/R cell,
+and rewinds the unary-control head. The data head remains at the selected L.
+No Nat decrement, key comparison, list-length test, or hidden boundary sensor
+occurs in step. External run fuel and input constructors are observations.
+
+Successful access consumes the exact valid packed/control entrance, and the
+locate corollary binds its unary length to the executable lookup's before list.
+Missing/malformed inputs do not acquire a successful-lookup theorem from the
+total fallback transitions. All supplied packed and unary cells are counted.
+Arbitrary carried Boolean scratch and the complete packed/control words are
+returned unchanged at the proved endpoint. Global data-head return, computing
+key-to-position, key encoding, unary preparation, allocation, source refresh
+and handoff into another controller remain separate costs.
+
+James Chang with OpenAI assistance; Apache-2.0. Reuses accepted Tape head/move
+operations, packed-slot decomposition and ambient XOR interface. The accepted
+marked-padding machine motivates the supplied unary-control convention; its
+padding-specific execution is not relabelled as this new seek controller.
+Pinned conditional context: kappa=836330098538459/500000000000000000.
+Uncompiled candidate.
+-/
+set_option Elab.async false
+set_option autoImplicit false
+namespace CurrentMain.PositionalMetadataAccess
+open PairedBitXorScan (Tape Pair)
+open MarkedBitXorScan (Symbol marked dataSymbol)
+open PackedMetadataSlots (Block Focus pack capacity)
+
+inductive ControlSymbol where
+  | blank | leftMarker | rightMarker | tick
+  deriving DecidableEq
+
+inductive Phase where
+  | enterControl | choose | scan | advanceControl | rewindControl | halt
+  deriving DecidableEq
+
+structure State where
+  dataTape : Tape Symbol
+  controlTape : Tape ControlSymbol
+  scratch : Bool
+  phase : Phase
+
+def step (s : State) : State :=
+  match s.phase with
+  | .halt => s
+  | .enterControl =>
+      match s.controlTape.readHead .blank with
+      | .leftMarker => { s with controlTape := s.controlTape.moveRight .blank, phase := .choose }
+      | _ => { s with phase := .halt }
+  | .choose =>
+      match s.controlTape.readHead .blank, s.dataTape.readHead .blank with
+      | .tick, .leftMarker => { s with dataTape := s.dataTape.moveRight .blank, phase := .scan }
+      | .rightMarker, .leftMarker => { s with phase := .rewindControl }
+      | _, _ => { s with phase := .halt }
+  | .scan =>
+      match s.dataTape.readHead .blank with
+      | .data _ _ => { s with dataTape := s.dataTape.moveRight .blank }
+      | .rightMarker => { s with dataTape := s.dataTape.moveRight .blank, phase := .advanceControl }
+      | _ => { s with phase := .halt }
+  | .advanceControl => { s with controlTape := s.controlTape.moveRight .blank, phase := .choose }
+  | .rewindControl =>
+      match s.controlTape.readHead .blank with
+      | .leftMarker => { s with phase := .halt }
+      | _ => { s with controlTape := s.controlTape.moveLeft .blank }
+
+def run : Nat → State → State
+  | 0, s => s
+  | k+1, s => run k (step s)
+
+def tapeCells {α : Type} (t : Tape α) : Nat := t.left.length + t.right.length
+
+def cells (s : State) : Nat := tapeCells s.dataTape + tapeCells s.controlTape
+
+/-- Actual live transitions, each with its proved no-allocation equation. -/
+inductive Trace : Nat → State → State → Prop where
+  | nil (s : State) : Trace 0 s s
+  | next {n : Nat} {s t : State} (live : s.phase ≠ .halt)
+      (size : cells (step s) = cells s) (tail : Trace n (step s) t) : Trace (n+1) s t
+
+private theorem trace_one (s : State) (h : s.phase ≠ .halt)
+    (hs : cells (step s) = cells s) : Trace 1 s (step s) :=
+  Trace.next h hs (Trace.nil _)
+
+private theorem trace_trans {m n : Nat} {s u t : State}
+    (h : Trace m s u) (g : Trace n u t) : Trace (m+n) s t := by
+  induction h with
+  | nil => simpa only [Nat.zero_add] using g
+  | next live size tail ih => simpa only [Nat.succ_add] using Trace.next live size (ih g)
+
+private theorem trace_sound {n : Nat} {s t : State} (h : Trace n s t) : run n s = t := by
+  induction h with
+  | nil => rfl
+  | next _ _ _ ih => exact ih
+
+private theorem trace_live {n : Nat} {s t : State} (h : Trace n s t)
+    (k : Nat) (hk : k < n) : (run k s).phase ≠ .halt := by
+  induction h generalizing k with
+  | nil => omega
+  | next live _ _ ih =>
+      cases k with
+      | zero => exact live
+      | succ k => exact ih k (by omega)
+
+private theorem halt_run (s : State) (h : s.phase = .halt) (k : Nat) : run k s = s := by
+  induction k with
+  | zero => rfl
+  | succ k ih => simpa only [run, step, h] using ih
+
+private theorem trace_storage {n : Nat} {s t : State} (h : Trace n s t)
+    (ht : t.phase = .halt) (k : Nat) : cells (run k s) = cells s := by
+  induction h generalizing k with
+  | nil => rw [halt_run _ ht]
+  | next _ size _ ih =>
+      cases k with
+      | zero => rfl
+      | succ k => exact (ih ht k).trans size
+
+def snapshot (dl dr : List Symbol) (cl cr : List ControlSymbol)
+    (scratch : Bool) (phase : Phase) : State :=
+  ⟨⟨dl,dr⟩,⟨cl,cr⟩,scratch,phase⟩
+
+/-- Cross every real payload cell and its R marker, never inspecting a list
+length in the transition function. Left/right remaining data are spectators. -/
+private theorem scan_data (rows : List Pair) (dl dr : List Symbol)
+    (cl cr : List ControlSymbol) (scratch : Bool) :
+    Trace (rows.length+1)
+      (snapshot dl (rows.map dataSymbol ++ .rightMarker :: dr) cl cr scratch .scan)
+      (snapshot (.rightMarker :: (rows.reverse.map dataSymbol ++ dl)) dr cl cr scratch .advanceControl) := by
+  induction rows generalizing dl with
+  | nil =>
+      apply Trace.next (by intro h; cases h)
+      · simp [snapshot, cells, tapeCells, step, Tape.readHead, Tape.moveRight]
+        omega
+      · exact Trace.nil _
+  | cons row rows ih =>
+      apply Trace.next (by intro h; cases h)
+      · simp [snapshot, cells, tapeCells, step, Tape.readHead, Tape.moveRight, dataSymbol]
+        omega
+      · simpa [snapshot, step, Tape.readHead, Tape.moveRight, dataSymbol,
+          List.reverse_cons, List.map_append, List.append_assoc] using ih (dataSymbol row :: dl)
+
+/-- One skip consumes one control tick and moves across one complete block. -/
+private theorem skip_block (rows : List Pair) (dl dr : List Symbol)
+    (cl cr : List ControlSymbol) (scratch : Bool) :
+    Trace (rows.length+3)
+      (snapshot dl (marked rows ++ dr) cl (.tick :: cr) scratch .choose)
+      (snapshot ((marked rows).reverse ++ dl) dr (.tick :: cl) cr scratch .choose) := by
+  have hs := scan_data rows (.leftMarker :: dl) dr cl (.tick :: cr) scratch
+  let middle := snapshot (.rightMarker :: (rows.reverse.map dataSymbol ++ (.leftMarker :: dl)))
+    dr cl (.tick :: cr) scratch .advanceControl
+  have ha : Trace 1 middle (step middle) := trace_one middle (by intro h; cases h) (by
+    simp [middle, snapshot, step, cells, tapeCells, Tape.moveRight]
+    omega)
+  have ht := trace_trans hs ha
+  have hsum : rows.length + 1 + 1 + 1 = rows.length + 3 := by omega
+  rw [← hsum]
+  apply Trace.next (by intro h; cases h)
+  · simp [snapshot, marked, cells, tapeCells, step, Tape.readHead, Tape.moveRight]
+    omega
+  · simpa [snapshot, marked, middle, step, Tape.readHead, Tape.moveRight,
+      List.reverse_append, List.map_reverse, List.append_assoc] using ht
+
+private theorem ticks_cons (n : Nat) (tail : List ControlSymbol) :
+    List.replicate n .tick ++ .tick :: tail = .tick :: (List.replicate n .tick ++ tail) := by
+  induction n with
+  | zero => rfl
+  | succ n ih => simpa only [List.replicate_succ, List.cons_append] using congrArg (ControlSymbol.tick :: ·) ih
+
+private theorem skip_blocks (pre : List Block) (selected : Block) (post : List Block)
+    (dl : List Symbol) (cl : List ControlSymbol) (scratch : Bool) :
+    Trace (capacity pre + pre.length)
+      (snapshot dl (pack (pre ++ selected :: post)) cl
+        (List.replicate pre.length .tick ++ [.rightMarker]) scratch .choose)
+      (snapshot ((pack pre).reverse ++ dl) (pack (selected :: post))
+        (List.replicate pre.length .tick ++ cl) [.rightMarker] scratch .choose) := by
+  induction pre generalizing dl cl with
+  | nil => simpa [capacity, pack, snapshot] using
+      Trace.nil (snapshot dl (pack (selected :: post)) cl [.rightMarker] scratch .choose)
+  | cons block pre ih =>
+      have hb := skip_block block.rows dl (pack (pre ++ selected :: post)) cl
+        (List.replicate pre.length .tick ++ [.rightMarker]) scratch
+      have ht := ih ((marked block.rows).reverse ++ dl) (.tick :: cl)
+      have h := trace_trans hb ht
+      have hc : block.rows.length + 3 + (capacity pre + pre.length) =
+          capacity (block :: pre) + (block :: pre).length := by
+        simp only [capacity, List.length_cons]
+        omega
+      rw [hc] at h
+      simpa only [List.cons_append, pack, List.length_cons, List.replicate_succ,
+        List.cons_append, List.reverse_append, List.append_assoc,
+        ticks_cons] using h
+
+/-- Rewind only supplied unary ticks. The actual control head returns to L;
+the reached packed-data focus and arbitrary carried scratch stay fixed. -/
+private theorem rewind_ticks (n : Nat) (data : Tape Symbol) (rs : List ControlSymbol)
+    (scratch : Bool) (hr : (⟨[],rs⟩ : Tape ControlSymbol).readHead .blank ≠ .leftMarker) :
+    Trace (n+2)
+      ⟨data,⟨List.replicate n .tick ++ [.leftMarker],rs⟩,scratch,.rewindControl⟩
+      ⟨data,⟨[],.leftMarker :: (List.replicate n .tick ++ rs)⟩,scratch,.halt⟩ := by
+  induction n generalizing rs with
+  | zero =>
+      apply Trace.next (by intro h; cases h)
+      · cases hrs : rs with
+        | nil => simp [cells, tapeCells, step, Tape.readHead, Tape.moveLeft]
+        | cons x xs =>
+            cases x <;> simp_all [cells, tapeCells, step, Tape.readHead, Tape.moveLeft]
+            all_goals omega
+      · have hx : step (⟨data,⟨List.replicate 0 .tick ++ [.leftMarker],rs⟩,scratch,.rewindControl⟩ : State) =
+          ⟨data,⟨[],.leftMarker :: rs⟩,scratch,.rewindControl⟩ := by
+          cases rs with
+          | nil => rfl
+          | cons x xs => cases x <;> simp_all [step, Tape.readHead, Tape.moveLeft]
+        rw [hx]
+        apply Trace.next (by intro h; cases h)
+        · rfl
+        · exact Trace.nil _
+  | succ n ih =>
+      have hx : step (⟨data,⟨List.replicate (n+1) .tick ++ [.leftMarker],rs⟩,scratch,.rewindControl⟩ : State) =
+          ⟨data,⟨List.replicate n .tick ++ [.leftMarker],.tick :: rs⟩,scratch,.rewindControl⟩ := by
+        cases rs with
+        | nil => simp [step, Tape.readHead, Tape.moveLeft, List.replicate_succ]
+        | cons x xs => cases x <;> simp_all [step, Tape.readHead, Tape.moveLeft, List.replicate_succ]
+      apply Trace.next (by intro h; cases h)
+      · rw [hx]
+        simp [cells, tapeCells, List.replicate_succ]
+        omega
+      · rw [hx]
+        have h := ih (.tick :: rs) (by intro h; cases h)
+        simpa only [List.replicate_succ, List.cons_append, ticks_cons] using h
+
+def unary (n : Nat) : Tape ControlSymbol :=
+  ⟨[],.leftMarker :: (List.replicate n .tick ++ [.rightMarker])⟩
+
+def initial (n : Nat) (blocks : List Block) (scratch : Bool) : State :=
+  ⟨⟨[],pack blocks⟩,unary n,scratch,.enterControl⟩
+
+def final (pre : List Block) (selected : Block) (post : List Block) (scratch : Bool) : State :=
+  ⟨⟨(pack pre).reverse,pack (selected :: post)⟩,unary pre.length,scratch,.halt⟩
+
+/-- Count derived from the actual transitions: skip cost is capacity(pre)+n;
+entry, endpoint detection and control rewind add another n+4. -/
+theorem access_exact (pre : List Block) (selected : Block) (post : List Block) (scratch : Bool) :
+    Trace (capacity pre + 2*pre.length + 4)
+      (initial pre.length (pre ++ selected :: post) scratch)
+      (final pre selected post scratch) := by
+  have hs := skip_blocks pre selected post [] [.leftMarker] scratch
+  simp only [List.append_nil] at hs
+  have hr := rewind_ticks pre.length
+    (⟨(pack pre).reverse,pack (selected :: post)⟩ : Tape Symbol) [.rightMarker] scratch
+    (by intro h; cases h)
+  have hc : Trace (pre.length+3)
+      (snapshot (pack pre).reverse (pack (selected :: post))
+        (List.replicate pre.length .tick ++ [.leftMarker]) [.rightMarker] scratch .choose)
+      (final pre selected post scratch) := by
+    apply Trace.next (by intro h; cases h)
+    · rfl
+    · simpa [snapshot, step, pack, marked, Tape.readHead, final, unary] using hr
+  have ht := trace_trans hs hc
+  have hn : capacity pre + pre.length + (pre.length+3) + 1 = capacity pre + 2*pre.length + 4 := by omega
+  rw [← hn]
+  apply Trace.next (by intro h; cases h)
+  · simp [initial, unary, cells, tapeCells, step, Tape.readHead, Tape.moveRight]
+    omega
+  · simpa [initial, unary, snapshot, step, Tape.readHead, Tape.moveRight] using ht
+
+theorem access_result (pre : List Block) (selected : Block) (post : List Block) (scratch : Bool) :
+    run (capacity pre + 2*pre.length + 4)
+      (initial pre.length (pre ++ selected :: post) scratch) = final pre selected post scratch :=
+  trace_sound (access_exact pre selected post scratch)
+
+theorem access_first_halt (pre : List Block) (selected : Block) (post : List Block) (scratch : Bool) :
+    (run (capacity pre + 2*pre.length + 4)
+      (initial pre.length (pre ++ selected :: post) scratch)).phase = .halt ∧
+    ∀ k, k < capacity pre + 2*pre.length + 4 →
+      (run k (initial pre.length (pre ++ selected :: post) scratch)).phase ≠ .halt :=
+  ⟨by rw [access_result]; rfl, trace_live (access_exact pre selected post scratch)⟩
+
+/-- Both full packed storage and the entire supplied unary tape are charged;
+the one carried Boolean scratch and finite control are separate fixed fields. -/
+theorem access_storage (pre : List Block) (selected : Block) (post : List Block)
+    (scratch : Bool) (k : Nat) :
+    cells (run k (initial pre.length (pre ++ selected :: post) scratch)) =
+      capacity (pre ++ selected :: post) + (pre.length + 2) := by
+  rw [trace_storage (access_exact pre selected post scratch) rfl k]
+  simp [initial, unary, cells, tapeCells, PackedMetadataSlots.pack_capacity, Nat.add_assoc]
+
+/-- Locate success supplies the valid slot and positional index. The paid
+controller, rather than a chosen zipper endpoint, then reaches that exact focus.
+The logical key-to-index search and unary construction are still not priced. -/
+theorem access_from_locate (key : Nat) (blocks : List Block) (f : Focus)
+    (h : PackedMetadataSlots.locate key blocks = some f) (scratch : Bool) :
+    let out := run (capacity f.before + 2*f.before.length + 4)
+      (initial f.before.length blocks scratch)
+    out.dataTape = (PackedMetadataSlots.focusState f).tape ∧
+      out.controlTape = unary f.before.length ∧ out.scratch = scratch ∧ out.phase = .halt := by
+  obtain ⟨he, _, _⟩ := PackedMetadataSlots.locate_spec key blocks f h
+  rw [he, access_result]
+  exact ⟨rfl,rfl,rfl,rfl⟩
+
+end CurrentMain.PositionalMetadataAccess
+#print axioms CurrentMain.PositionalMetadataAccess.access_exact
+#print axioms CurrentMain.PositionalMetadataAccess.access_result
+#print axioms CurrentMain.PositionalMetadataAccess.access_first_halt
+#print axioms CurrentMain.PositionalMetadataAccess.access_storage
+#print axioms CurrentMain.PositionalMetadataAccess.access_from_locate
+#check @CurrentMain.PositionalMetadataAccess.access_from_locate
+#check @CurrentMain.PositionalMetadataAccess.access_storage
diff --git a/research/lean-paid-positioned-acquisition/sources/PositionalMetadataReturn.lean b/research/lean-paid-positioned-acquisition/sources/PositionalMetadataReturn.lean
new file mode 100644
index 0000000000..558e63f32e
--- /dev/null
+++ b/research/lean-paid-positioned-acquisition/sources/PositionalMetadataReturn.lean
@@ -0,0 +1,317 @@
+import PositionalMetadataAccess
+
+/-!
+Actual reverse block traversal from a supplied marked-block focus to global
+packed home, using the same finite unary positional control. Each tick crosses
+one preceding block in reverse physical order. The transition reads finite
+L/data/R and control symbols only; it never inspects zipper emptiness or a Nat
+position. It rewinds the unary head and preserves all symbols and arbitrary
+Boolean scratch. The count is derived from the transition trace.
+
+Reuses the accepted tape operations and unary convention. The unary rewind
+proof follows PositionalMetadataAccess with the identical rewind transition;
+the reverse data traversal is new. James Chang with OpenAI assistance,
+Apache-2.0. Pinned conditional context:
+kappa=836330098538459/500000000000000000. Uncompiled candidate.
+Key-to-position, unary preparation, allocation and source refresh stay external.
+-/
+set_option Elab.async false
+set_option autoImplicit false
+namespace CurrentMain.PositionalMetadataReturn
+open PairedBitXorScan (Tape Pair)
+open MarkedBitXorScan (Symbol marked dataSymbol)
+open PackedMetadataSlots (Block Focus pack capacity)
+open PositionalMetadataAccess (ControlSymbol)
+
+inductive Phase where
+  | enterControl | choose | scan | rewindControl | halt
+  deriving DecidableEq
+
+structure State where
+  dataTape : Tape Symbol
+  controlTape : Tape ControlSymbol
+  scratch : Bool
+  phase : Phase
+
+def step (s : State) : State :=
+  match s.phase with
+  | .halt => s
+  | .enterControl =>
+      match s.controlTape.readHead .blank with
+      | .leftMarker => { s with controlTape := s.controlTape.moveRight .blank, phase := .choose }
+      | _ => { s with phase := .halt }
+  | .choose =>
+      match s.controlTape.readHead .blank, s.dataTape.readHead .blank with
+      | .tick, .leftMarker => { s with dataTape := s.dataTape.moveLeft .blank, phase := .scan }
+      | .rightMarker, .leftMarker => { s with phase := .rewindControl }
+      | _, _ => { s with phase := .halt }
+  | .scan =>
+      match s.dataTape.readHead .blank with
+      | .data _ _ => { s with dataTape := s.dataTape.moveLeft .blank }
+      | .rightMarker => { s with dataTape := s.dataTape.moveLeft .blank }
+      | .leftMarker => { s with controlTape := s.controlTape.moveRight .blank, phase := .choose }
+      | .blank => { s with phase := .halt }
+  | .rewindControl =>
+      match s.controlTape.readHead .blank with
+      | .leftMarker => { s with phase := .halt }
+      | _ => { s with controlTape := s.controlTape.moveLeft .blank }
+
+def run : Nat → State → State
+  | 0, s => s
+  | k+1, s => run k (step s)
+
+def tapeCells {α : Type} (t : Tape α) : Nat := t.left.length + t.right.length
+
+def cells (s : State) : Nat := tapeCells s.dataTape + tapeCells s.controlTape
+
+/-- Actual live transitions, each with its proved no-allocation equation. -/
+inductive Trace : Nat → State → State → Prop where
+  | nil (s : State) : Trace 0 s s
+  | next {n : Nat} {s t : State} (live : s.phase ≠ .halt)
+      (size : cells (step s) = cells s) (tail : Trace n (step s) t) : Trace (n+1) s t
+
+private theorem trace_one (s : State) (h : s.phase ≠ .halt)
+    (hs : cells (step s) = cells s) : Trace 1 s (step s) :=
+  Trace.next h hs (Trace.nil _)
+
+private theorem trace_trans {m n : Nat} {s u t : State}
+    (h : Trace m s u) (g : Trace n u t) : Trace (m+n) s t := by
+  induction h with
+  | nil => simpa only [Nat.zero_add] using g
+  | next live size tail ih => simpa only [Nat.succ_add] using Trace.next live size (ih g)
+
+private theorem trace_sound {n : Nat} {s t : State} (h : Trace n s t) : run n s = t := by
+  induction h with
+  | nil => rfl
+  | next _ _ _ ih => exact ih
+
+private theorem trace_live {n : Nat} {s t : State} (h : Trace n s t)
+    (k : Nat) (hk : k < n) : (run k s).phase ≠ .halt := by
+  induction h generalizing k with
+  | nil => omega
+  | next live _ _ ih =>
+      cases k with
+      | zero => exact live
+      | succ k => exact ih k (by omega)
+
+private theorem halt_run (s : State) (h : s.phase = .halt) (k : Nat) : run k s = s := by
+  induction k with
+  | zero => rfl
+  | succ k ih => simpa only [run, step, h] using ih
+
+private theorem trace_storage {n : Nat} {s t : State} (h : Trace n s t)
+    (ht : t.phase = .halt) (k : Nat) : cells (run k s) = cells s := by
+  induction h generalizing k with
+  | nil => rw [halt_run _ ht]
+  | next _ size _ ih =>
+      cases k with
+      | zero => rfl
+      | succ k => exact (ih ht k).trans size
+
+def snapshot (dl dr : List Symbol) (cl cr : List ControlSymbol)
+    (scratch : Bool) (phase : Phase) : State :=
+  ⟨⟨dl,dr⟩,⟨cl,cr⟩,scratch,phase⟩
+
+private theorem scan_move (dl dr : List Symbol) (cl cr : List ControlSymbol) (scratch : Bool)
+    (hl : (⟨[],dr⟩ : Tape Symbol).readHead .blank ≠ .leftMarker)
+    (hb : (⟨[],dr⟩ : Tape Symbol).readHead .blank ≠ .blank) :
+    step (snapshot dl dr cl cr scratch .scan) =
+      ⟨(⟨dl,dr⟩ : Tape Symbol).moveLeft .blank,⟨cl,cr⟩,scratch,.scan⟩ := by
+  cases hh : (⟨[],dr⟩ : Tape Symbol).readHead .blank <;>
+    simp_all [snapshot, step, Tape.readHead]
+
+/-- Rewind the remaining reversed payload and its L, then advance one control
+ tick. The right-hand word, including the already updated selected block, is
+ carried verbatim through each real move. -/
+private theorem rewind_data (ls : List Pair) (dl dr : List Symbol)
+    (cl cr : List ControlSymbol) (scratch : Bool)
+    (hl : (⟨[],dr⟩ : Tape Symbol).readHead .blank ≠ .leftMarker)
+    (hb : (⟨[],dr⟩ : Tape Symbol).readHead .blank ≠ .blank) :
+    Trace (ls.length+2)
+      (snapshot (ls.map dataSymbol ++ .leftMarker :: dl) dr cl (.tick :: cr) scratch .scan)
+      (snapshot dl (.leftMarker :: (ls.reverse.map dataSymbol ++ dr)) (.tick :: cl) cr scratch .choose) := by
+  induction ls generalizing dr with
+  | nil =>
+      simp only [List.map_nil, List.nil_append, List.reverse_nil]
+      have hm := scan_move (.leftMarker :: dl) dr cl (.tick :: cr) scratch hl hb
+      apply Trace.next (by intro h; cases h)
+      · rw [hm]
+        simp [snapshot, cells, tapeCells, Tape.moveLeft]
+        omega
+      · rw [hm]
+        apply Trace.next (by intro h; cases h)
+        · simp [snapshot, cells, tapeCells, step, Tape.readHead, Tape.moveLeft, Tape.moveRight]
+          omega
+        · exact Trace.nil _
+  | cons row ls ih =>
+      have hm := scan_move ((row :: ls).map dataSymbol ++ .leftMarker :: dl) dr cl (.tick :: cr) scratch hl hb
+      apply Trace.next (by intro h; cases h)
+      · rw [hm]
+        simp [snapshot, cells, tapeCells, Tape.moveLeft]
+        omega
+      · rw [hm]
+        have ht := ih (dataSymbol row :: dr) (by simp [Tape.readHead, dataSymbol])
+          (by simp [Tape.readHead, dataSymbol])
+        simpa [snapshot, Tape.moveLeft, List.reverse_cons, List.map_append, List.append_assoc] using ht
+
+private theorem skip_block (rows : List Pair) (dl dr : List Symbol)
+    (cl cr : List ControlSymbol) (scratch : Bool)
+    (hh : (⟨[],dr⟩ : Tape Symbol).readHead .blank = .leftMarker) :
+    Trace (rows.length+3)
+      (snapshot ((marked rows).reverse ++ dl) dr cl (.tick :: cr) scratch .choose)
+      (snapshot dl (marked rows ++ dr) (.tick :: cl) cr scratch .choose) := by
+  simp only [Tape.readHead] at hh
+  have hd := rewind_data rows.reverse dl (.rightMarker :: dr) cl cr scratch
+    (by intro h; cases h) (by intro h; cases h)
+  have hn : rows.reverse.length + 2 + 1 = rows.length + 3 := by simp
+  rw [← hn]
+  apply Trace.next (by intro h; cases h)
+  · simp [snapshot, cells, tapeCells, step, Tape.readHead, hh, marked,
+      List.reverse_append, List.map_reverse, Tape.moveLeft]
+    omega
+  · simpa [snapshot, step, Tape.readHead, hh, marked, List.reverse_append,
+      List.map_reverse, Tape.moveLeft, List.append_assoc] using hd
+
+private theorem ticks_cons (n : Nat) (tail : List ControlSymbol) :
+    List.replicate n .tick ++ .tick :: tail = .tick :: (List.replicate n .tick ++ tail) := by
+  induction n with
+  | zero => rfl
+  | succ n ih => simpa only [List.replicate_succ, List.cons_append] using congrArg (ControlSymbol.tick :: ·) ih
+
+private theorem pack_append (xs ys : List Block) : pack (xs ++ ys) = pack xs ++ pack ys := by
+  induction xs with
+  | nil => rfl
+  | cons b xs ih => simp only [List.cons_append, pack, ih, List.append_assoc]
+
+private theorem pack_head (pre : List Block) (dr : List Symbol)
+    (hh : (⟨[],dr⟩ : Tape Symbol).readHead .blank = .leftMarker) :
+    (⟨[],pack pre ++ dr⟩ : Tape Symbol).readHead .blank = .leftMarker := by
+  cases pre with
+  | nil => exact hh
+  | cons b pre => rfl
+
+/-- Normal list induction executes the tail first, which is the actual reverse
+order stored in the left zipper. No right-suffix symbols are overwritten. -/
+private theorem skip_blocks (pre : List Block) (dl dr : List Symbol)
+    (cl cr : List ControlSymbol) (scratch : Bool)
+    (hh : (⟨[],dr⟩ : Tape Symbol).readHead .blank = .leftMarker) :
+    Trace (capacity pre + pre.length)
+      (snapshot ((pack pre).reverse ++ dl) dr cl
+        (List.replicate pre.length .tick ++ cr) scratch .choose)
+      (snapshot dl (pack pre ++ dr)
+        (List.replicate pre.length .tick ++ cl) cr scratch .choose) := by
+  induction pre generalizing dl cl cr with
+  | nil => simpa [capacity, pack, snapshot] using Trace.nil (snapshot dl dr cl cr scratch .choose)
+  | cons block pre ih =>
+      have ht := ih ((marked block.rows).reverse ++ dl) cl (.tick :: cr)
+      have hb := skip_block block.rows dl (pack pre ++ dr)
+        (List.replicate pre.length .tick ++ cl) cr scratch (pack_head pre dr hh)
+      have h := trace_trans ht hb
+      have hn : (capacity pre + pre.length) + (block.rows.length + 3) =
+          capacity (block :: pre) + (block :: pre).length := by
+        simp only [capacity, List.length_cons]
+        omega
+      rw [hn] at h
+      simpa only [pack, List.length_cons, List.replicate_succ, List.cons_append,
+        List.reverse_append, List.append_assoc, ticks_cons] using h
+
+/-- Rewind only supplied unary ticks. The actual control head returns to L;
+the reached packed-data focus and arbitrary carried scratch stay fixed. -/
+private theorem rewind_ticks (n : Nat) (data : Tape Symbol) (rs : List ControlSymbol)
+    (scratch : Bool) (hr : (⟨[],rs⟩ : Tape ControlSymbol).readHead .blank ≠ .leftMarker) :
+    Trace (n+2)
+      ⟨data,⟨List.replicate n .tick ++ [.leftMarker],rs⟩,scratch,.rewindControl⟩
+      ⟨data,⟨[],.leftMarker :: (List.replicate n .tick ++ rs)⟩,scratch,.halt⟩ := by
+  induction n generalizing rs with
+  | zero =>
+      apply Trace.next (by intro h; cases h)
+      · cases hrs : rs with
+        | nil => simp [cells, tapeCells, step, Tape.readHead, Tape.moveLeft]
+        | cons x xs =>
+            cases x <;> simp_all [cells, tapeCells, step, Tape.readHead, Tape.moveLeft]
+            all_goals omega
+      · have hx : step (⟨data,⟨List.replicate 0 .tick ++ [.leftMarker],rs⟩,scratch,.rewindControl⟩ : State) =
+          ⟨data,⟨[],.leftMarker :: rs⟩,scratch,.rewindControl⟩ := by
+          cases rs with
+          | nil => rfl
+          | cons x xs => cases x <;> simp_all [step, Tape.readHead, Tape.moveLeft]
+        rw [hx]
+        apply Trace.next (by intro h; cases h)
+        · rfl
+        · exact Trace.nil _
+  | succ n ih =>
+      have hx : step (⟨data,⟨List.replicate (n+1) .tick ++ [.leftMarker],rs⟩,scratch,.rewindControl⟩ : State) =
+          ⟨data,⟨List.replicate n .tick ++ [.leftMarker],.tick :: rs⟩,scratch,.rewindControl⟩ := by
+        cases rs with
+        | nil => simp [step, Tape.readHead, Tape.moveLeft, List.replicate_succ]
+        | cons x xs => cases x <;> simp_all [step, Tape.readHead, Tape.moveLeft, List.replicate_succ]
+      apply Trace.next (by intro h; cases h)
+      · rw [hx]
+        simp [cells, tapeCells, List.replicate_succ]
+        omega
+      · rw [hx]
+        have h := ih (.tick :: rs) (by intro h; cases h)
+        simpa only [List.replicate_succ, List.cons_append, ticks_cons] using h
+
+abbrev unary := PositionalMetadataAccess.unary
+
+def initial (pre : List Block) (selected : Block) (post : List Block) (scratch : Bool) : State :=
+  ⟨⟨(pack pre).reverse,pack (selected :: post)⟩,unary pre.length,scratch,.enterControl⟩
+
+def final (n : Nat) (blocks : List Block) (scratch : Bool) : State :=
+  ⟨⟨[],pack blocks⟩,unary n,scratch,.halt⟩
+
+theorem return_exact (pre : List Block) (selected : Block) (post : List Block) (scratch : Bool) :
+    Trace (capacity pre + 2*pre.length + 4)
+      (initial pre selected post scratch)
+      (final pre.length (pre ++ selected :: post) scratch) := by
+  have hs := skip_blocks pre [] (pack (selected :: post)) [.leftMarker] [.rightMarker] scratch rfl
+  simp only [List.append_nil] at hs
+  have hr := rewind_ticks pre.length
+    (⟨[],pack pre ++ pack (selected :: post)⟩ : Tape Symbol) [.rightMarker] scratch
+    (by intro h; cases h)
+  have hh := pack_head pre (pack (selected :: post)) rfl
+  simp only [Tape.readHead] at hh
+  have hc : Trace (pre.length+3)
+      (snapshot [] (pack pre ++ pack (selected :: post))
+        (List.replicate pre.length .tick ++ [.leftMarker]) [.rightMarker] scratch .choose)
+      (final pre.length (pre ++ selected :: post) scratch) := by
+    apply Trace.next (by intro h; cases h)
+    · simp [snapshot, step, Tape.readHead, hh, cells]
+    · simpa [snapshot, step, hh,
+        Tape.readHead, final, unary, PositionalMetadataAccess.unary, pack_append] using hr
+  have ht := trace_trans hs hc
+  have hn : capacity pre + pre.length + (pre.length+3) + 1 = capacity pre + 2*pre.length + 4 := by omega
+  rw [← hn]
+  apply Trace.next (by intro h; cases h)
+  · simp [initial, unary, PositionalMetadataAccess.unary, cells, tapeCells, step, Tape.readHead, Tape.moveRight]
+    omega
+  · simpa [initial, unary, PositionalMetadataAccess.unary, snapshot, step, Tape.readHead, Tape.moveRight] using ht
+
+theorem return_result (pre : List Block) (selected : Block) (post : List Block) (scratch : Bool) :
+    run (capacity pre + 2*pre.length + 4) (initial pre selected post scratch) =
+      final pre.length (pre ++ selected :: post) scratch :=
+  trace_sound (return_exact pre selected post scratch)
+
+theorem return_first_halt (pre : List Block) (selected : Block) (post : List Block) (scratch : Bool) :
+    (run (capacity pre + 2*pre.length + 4) (initial pre selected post scratch)).phase = .halt ∧
+    ∀ k, k < capacity pre + 2*pre.length + 4 →
+      (run k (initial pre selected post scratch)).phase ≠ .halt :=
+  ⟨by rw [return_result]; rfl, trace_live (return_exact pre selected post scratch)⟩
+
+theorem return_storage (pre : List Block) (selected : Block) (post : List Block)
+    (scratch : Bool) (k : Nat) :
+    cells (run k (initial pre selected post scratch)) =
+      capacity (pre ++ selected :: post) + (pre.length+2) := by
+  rw [trace_storage (return_exact pre selected post scratch) rfl k]
+  have hp := PackedMetadataSlots.pack_capacity (pre ++ selected :: post)
+  rw [pack_append, List.length_append] at hp
+  simp [initial, unary, PositionalMetadataAccess.unary, cells, tapeCells]
+  omega
+
+end CurrentMain.PositionalMetadataReturn
+#print axioms CurrentMain.PositionalMetadataReturn.return_exact
+#print axioms CurrentMain.PositionalMetadataReturn.return_result
+#print axioms CurrentMain.PositionalMetadataReturn.return_first_halt
+#print axioms CurrentMain.PositionalMetadataReturn.return_storage
+#check @CurrentMain.PositionalMetadataReturn.return_result