Mister-Meeseeks · Oct 16, 2026 · Oct 15, 2026 · Oct 15, 2026
diff --git a/research/multitape-proof-toolkit/API.md b/research/multitape-proof-toolkit/API.md
@@ -0,0 +1,121 @@
+# Public theorem guide
+
+All names below are under `MultitapeToolkit`. Import the aggregator
+`MultitapeToolkit` or the narrow module matching your construction.
+
+| Need | Interface | Evidence required from the caller |
+|---|---|---|
+| Literal locality | `Locality.step_locality` | One actual successful physical step |
+| Fixed finite decision table | `Locality.decisionTable_lookup`, `Locality.decisionTable_card_le` | A fixed finite machine |
+| Exact relative/absolute transfer | `Absolute.runs_simulation`, `Absolute.halts_iff` | Actual relative run or halt |
+| Concatenate machines | `compose_runs`, `compose_computesWithin` | Actual first run/halt and second run on exactly the returned tapes |
+| Protect far cells | `Absolute.Trace.runs_reach_and_frame` | Actual run and distance from its initial heads |
+| Preserve a whole parked tape | `Absolute.Trace.IdleOn`, `Absolute.Trace.runs_idle_tape` | A checked predicate on the literal transition table |
+| Replay with arbitrary outside dirt | `Absolute.FrameRule.runs_finite_frame_simulation` | An actual run; the theorem constructs its finite footprint |
+| Preserve completed runtime and halt | `Absolute.FrameRule.completed_runs_finite_frame` | Actual run and actual terminal halt |
+| Compose footprints | `Absolute.FrameRule.FootprintedRuns.compose`, `Absolute.FrameRule.charged_handoff_frame` | Actual runs for every middle/handoff stage, not just endpoint equalities |
+| Compile homogeneous source macros | `TM2Compiler.compile_run`, `TM2Compiler.encode_halts`, `TM2Compiler.read_output` | Fixed finite program and exact source run |
+| Compile dependent alphabets | `TM2HeterogeneousCompiler.compile_run`, `decode_output` | Fixed finite heterogeneous program and exact source run |
+| Keep typed-stack invariants | `TM2HeterogeneousCompiler.WellTagged` and flattening lemmas | The actual mapped configuration; inspect the module for exact binders |
+| Compile completed time contracts | `Transport.compiled_computesInTime`, `Transport.compiled_computesInTime_depth` | Actual source executions, halt, output, and optional fixed depth bound |
+| Transfer arbitrary asymptotic targets | `Transport.fixed_overhead_isBigO`, `Transport.compiled_and_adapter_isBigO` | Pointwise physical cost bound and established source/adapter Big-O |
+| Compile a fixed stage sequence | `Absolute.Subroutines.scheduler_assembly` | Literal runs, halts, and tape/head boundary equalities for all stages |
+| Invoice stage volumes | `Absolute.Subroutines.scheduler_affine_volume_bound` | Charged time bound for each supplied stage volume |
+| Use the full sufficient compiler/frame result | `VerifiedPipeline.compile_completed_frame` | One fixed source program, depth bound, exact completed source execution |
+| Start from a concrete program | `Examples.literal_copy_correct`, `Examples.completed_copy_frame` | Arbitrary initial tape functions and heads; no algorithm premise |
+
+## Routine recipe
+
+For a source TM2 subroutine, prove the source `step` iterate, its `l = none`
+terminal condition, and the exact returned lists. Supply the finite type
+instances and fixed depth bound, then use `compile_completed_frame`. It gives
+the actual absolute-coordinate run and a finite observed set. The output is
+the realization of `encode M d`, so `decode_output` recovers each source stack.
+
+For native tape routines, prove `Runs` directly and use `completed_runs_finite_frame`.
+The returned `MatchesOn` condition requires equal initial control and head
+positions as well as observed symbols. It deliberately permits every other
+cell to differ, including arbitrarily long pre-existing parked payloads.
+
+For sequential callers, prove physical entry/exit agreement before invoking
+the scheduler. A run of one component ending at the next component's desired
+mathematical value is insufficient unless the actual tape bank and heads also
+meet that boundary. Every handoff is charged explicitly.
+
+## Uniformity checklist
+
+- Fix tape types, alphabets, control, program, and entry states before varying
+  operand lengths or values.
+- Bound syntactic statement depth or retain its explicit overhead in the cost.
+- A tape can be write-idle while its scanned symbols still influence control.
+  Use the observation footprint when runtime independence is needed.
+- Include terminal scanned positions when transferring a halt condition.
+- Count physical parsing, padding, reversal, relocation, and trimming adapters
+  before changing input/output conventions.
+- Treat the finite reference fixtures as implementation controls, and the
+  complete `replay.py` run as the kernel/axiom evidence.
+
+
+## Concrete reusable construction extension
+
+| Need | Interface | Actual conclusion |
+|---|---|---|
+| Tag distinct finite controls | `Absolute.ControlEmbedding.lift_runs`, `lift_halts` | Same physical execution and cost |
+| Marked-stream local representation | `Absolute.MarkedStreams.cellView`, `Physical`, `bank2_step` | Literal write/unit-move semantics, arbitrary past |
+| Transfer and real child | `Absolute.MarkedStreams.move_runs`, `flip_runs` | Exact2n+2 transitions and head-restored output |
+| Push/pop | `Absolute.ParkStack.push_correct`, `pop_correct` | Exact2n+2 /3n+5 and full literal banks |
+| Initialize/remove markers | `Absolute.MarkerLifecycle.marker_run`, `install_remove_cells` | Real two-step operations; full-cell restoration under blank marker sites |
+| Reusable caller | `Absolute.ParkingController.wrapper_correct` | Actual changing-length child gives cost2|x|+2|z|+5|y|+16+t and true halt |
+| Closed finite controller | `Absolute.ParkingController.boundary_machine_correct` | Real bit-flip child, every length, exact6|x|+5|y|+18, full endpoint |
+| Copy/flip observed regions | `Absolute.MarkedStreams.move_footprints`, `flip_footprints` | Actual bounded FootprintedRuns and spectator footprints |
+| Parking observed regions | `Absolute.ParkFootprints.pop_completed_footprint`, `push_completed_footprint` | Actual finite footprints, marker floors, old-prefix preservation |
+| Canonical output | `OutputNormalization.compiled_normalize`, `compiled_output`, `compiled_fixedWidth` | Actual compiled source empty/output and physical bound10(input.length+1) |
+
+Names are taken from actual defining modules; inspect exact binders before use.
+The controller assumes marked word banks; the output converter assumes the
+compiler's stack representation and a real MSB-first input list. Neither hides
+a buffer placement or reversal cost.
+
+
+## Larger banks and physical output ABI
+
+| Need | Interface | Actual conclusion |
+|---|---|---|
+| Add finite tapes | `Absolute.TapeEmbedding.lift_step`, `lift_runs`, `lift_halts`, `preserves_extra` | Identical transition count and whole dirty extra preservation |
+| Child work bank | `Absolute.GenericParkingController.wrapper_correct` | Actual child may return changed extra heads/cells; full caller invoice and halt |
+| Unmarked lifecycle | `Absolute.CleanBoundary.machine_correct`, `Absolute.GenericParkingController.clean_machine_correct` | Exact `6|x|+5|y|+24`; fully blank IO/temp; arbitrary bank spectators |
+| Compiler anchors | `TM2Compiler.Anchored.anchored_compile_run`, `anchored_halts` | Actual final head `anchor-length(stack)`, exact realized cells and bounded physical run |
+| Stack-origin output | `Absolute.StackOriginSerializer.serialize_correct` | Exact `3m+4`; padded reversed word at origin zero, source erased and both heads restored |
+| Arithmetic example | `BinaryMultiplicationOriginABI.quadratic_origin_product`, `quadratic_origin_product_uniform` | Fixed six-tape actual quadratic product at origin, with charged serializer and handoff |
+| Empty arithmetic | `BinaryMultiplicationOriginABI.zero_correct`, `output_zero_bank` | Genuine width-zero run/halt and all-zero heads/full blank cells |
+
+The serializer requires distinct source/destination roles, a real LSB compiler
+stack, a fully blank destination headed at zero, and arbitrary spectators.
+The arithmetic input is two separate LSB compiler stacks, not a single serialized
+input word. Its output is fixed-width padded MSB, not trimmed canonical bits.
+Its remaining arithmetic workspace is described explicitly. The arbitrary-bank
+caller uses marked Symbol IO and needs its actual child entry/return contract;
+the arithmetic example is not silently identified with that convention.
+
+
+## Clean multiplication and eight applications (2026-10-15)
+
+Names below are under `MultitapeToolkit`.
+
+| Application | Interface | Sufficient checked conclusion |
+|---|---|---|
+| Clean multiplication | `IntegerMultiplicationEngine.clean_product` | Actual run, genuine halt, five globally blank non-output tapes; bound 280n²+322n+122 |
+| Bounded dirty windows | `Absolute.BoundedWindows.completed_window` | Agreement in radius-budget closed windows gives same exact completed execution and unchanged exterior |
+| Relocated multiplication | `IntegerMultiplicationEngine.Windows.dirty_relocated_product`, `product_word_in_window`, `input_window_centers` | Same multiplication table, independent supplied tape origins, literal output inside windows, arbitrary exterior retained |
+| Exact setup / tighter clean bound | `IntegerMultiplicationCompilerApplications.setup_charged`, `setup_physical`, `clean_product_tight` | Exact40n+30 setup; complete actual clean bound280n²+278n+68 |
+| Fixed alphabet | `IntegerMultiplicationCompilerApplications.Alphabet.compile_step`, `compile_runs`, `compile_halts`, `encoded_clean_product` | Injective static alphabet compilation; exact time and halt on encoded configurations |
+| Least input width | `IntegerMultiplicationProductApplications.commonWidth_spec`, `fixedBits_eq_bits_padding`, `minimalInput_literal_operands`, `minimal_width_product` | Least common Nat.size width, literal initial zero padding, actual clean run for every natural pair |
+| Residue labels | `IntegerMultiplicationProductApplications.zmod_product`, `signed_residue_label`, `signed_residue_product` | Exact double-width output, correct ring and signed Euclidean-residue labels; no physical truncation/parser |
+| Designated tape endpoints | `Absolute.EndpointAdapters.fixes_designated`, `lift_iterate`, `completed` | Fixed permutations preserve fixed tape endpoints; Semiconj iterate transport preserves actual time |
+| Accumulator output | `IntegerMultiplicationPhysicalApplications.unchanged_input`, `accumulator_product`, `accumulator_output_contract`, `accumulator_output_heads` | Static table swap fixes input ABI; product on accumulator with genuine halt and real terminal heads |
+
+`ExecutionCertificates` also supplies exact eval/run equivalence, splitting,
+uniqueness, prefix and halt certificates. `Relocation` supplies exact same-table
+head/full-cell conjugacy. The dirty-window output contract is local; it does not
+claim that arbitrary exterior dirt becomes globally blank. Minimal-width,
+residue and accumulator statements retain the conservative clean bound.
diff --git a/research/multitape-proof-toolkit/FRONTIER.json b/research/multitape-proof-toolkit/FRONTIER.json
@@ -0,0 +1,92 @@
+{
+  "schema_version": 2,
+  "repository": "CrocSwap/integer-mult-bounds",
+  "refresh": {
+    "main": "8e22a9d9f621c72ab5b299061c2be4c7f638fd3c",
+    "retrieved": "2026-10-15T20:59:08.669Z",
+    "cutoff": "2026-10-14T00:00:00Z",
+    "pages": 19,
+    "complete": true,
+    "prs": 1898,
+    "hits": 1744,
+    "latest": 2767,
+    "scope": "All updated metadata since cutoff; actual source review recorded separately. No novelty completeness claim."
+  },
+  "scope": "All updated metadata retrieved; only the selected actual sources in reviews were compared. Not exhaustive semantic coverage, complete diffs, historical work or Discussions.",
+  "reviewed_prs": [
+    {
+      "number": 2411,
+      "title": "[Lean] Link an end-to-end proof of multiplication below n log n",
+      "head": "c284cdf993353b61e9582607e9322ec65746c50f",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2411"
+    },
+    {
+      "number": 2235,
+      "title": "Add verified multitape foundations, compilers, dirty-frame callers and quadratic multiplication output",
+      "head": "e5a5d0651003e8774e98121250203b35c236b02b",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2235"
+    },
+    {
+      "number": 2636,
+      "title": "Implement linear aggregate padding on fixed bit tapes",
+      "head": "c1e173b7af38603bc7660a8829e75006e93645d3",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2636"
+    },
+    {
+      "number": 2635,
+      "title": "Implement finite two-tape control for nested parking frames",
+      "head": "1662dda699d9ea57b3fb13a23873b087d765149f",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2635"
+    },
+    {
+      "number": 2531,
+      "title": "Decode HPE Lean recipe literals as UTF-8 on Windows",
+      "head": "2dfb25cd3c762a2b24ba732a28bb21e4d331687a",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2531"
+    },
+    {
+      "number": 2439,
+      "title": "[Lean] Execute paid exponent widening and half-source addition",
+      "head": "4bbcd5ec320eff1deb0240fcc8a12e5919564741",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2439"
+    },
+    {
+      "number": 2438,
+      "title": "[Lean] Return reusable dyadic output with paid copy and sign split",
+      "head": "3e4399b276d663f8716b17c7758b597f96503675",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2438"
+    },
+    {
+      "number": 2425,
+      "title": "[Lean] Decode compact bytes and recover the L450 source operator",
+      "head": "8ac792828e70a90beda501749608d31ef7d9250a",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2425"
+    },
+    {
+      "number": 2418,
+      "title": "[Lean] Pay positioned paired-track acquisition and global return",
+      "head": "ddaf7234581133ec0c15496f4dfc65570aef401c",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2418"
+    },
+    {
+      "number": 2410,
+      "title": "[Lean] Check original PR1942 chart witnesses and strict envelope",
+      "head": "4c07034bcda475ba4063d3a137c0815291a7480c",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2410"
+    },
+    {
+      "number": 2404,
+      "title": "Formalize normal-class rank and complete count/price bounds in Lean",
+      "head": "d7db77c9e3f19fd1196393c045e597539fdcfc8a",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2404"
+    },
+    {
+      "number": 2371,
+      "title": "[Lean] Bind exact L450 fragment bytes to checked chart payload",
+      "head": "5bbe542064308dbc10f50582c05116ebd0925223",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2371"
+    }
+  ],
+  "novelty_claim": false,
+  "discussion_scope": "Public first-page index, start-here1163 and handoff1166 read; not all comments or historical discussions."
+}
diff --git a/research/multitape-proof-toolkit/FRONTIER.md b/research/multitape-proof-toolkit/FRONTIER.md
@@ -0,0 +1,26 @@
+# Refreshed upstream and actual-source overlap
+
+Main was refreshed to `8e22a9d9f621c72ab5b299061c2be4c7f638fd3c`.
+The2026-10-15T20:59:08.669Z checkpoint fetched all1,898 PRs updated since
+2026-10-14T00:00:00Z over19 paginated API pages, through PR2767. These are
+metadata retrieval counts, not a claim that every proof or diff was reviewed.
+The current README, selected-result record, autoresearch, bottleneck/family guide,
+contribution-review index, PR ledger and contribution rules were read. Public
+Discussion index/start-here1163/handoff1166 were inspected with bounded comment
+coverage. No claim/discussion message or PR was posted by this local deliverable.
+
+`reviews/compiler.md`, `reviews/product.md`, `reviews/physical.md` compare actual
+pinned relevant sources. PR2235 is direct multiplication/toolkit reuse; PR1641,
+PR1379 and rfu08's PR64 remain the credited parking/compiler predecessor chain.
+PR2411's referenced external development already has alphabet simulation and
+finite-TM2 multiplication results. PR2418/2438/2439 supply real paid returns,
+output adapters and widening. PR2635/2636 supply finite parking and physical
+padding. These are substantial overlap, not merely similar titles.
+
+The clean endpoint, exact six-phase invoice and concrete specializations are the
+scope of this release. Generic alphabet transport, binary multiplication,
+semiconjugacy, padding and output adaptation are not claimed as inventions.
+No exhaustive-library, unpublished-work or first-application claim is established.
+The external sources were inspected, not all independently rebuilt. Their stronger
+or different statements are not imported assumptions in the portable proof.
+The selected conditional record and its own all-size obligations remain unchanged.