karnseth · Oct 29, 2026 · Oct 28, 2026 · Oct 28, 2026 · Oct 28, 2026 · Oct 28, 2026
diff --git a/Complexity.lean b/Complexity.lean
@@ -102,6 +102,23 @@ public import Complexity.Algorithms.WordRAM.ExactTriangle.PreparationInput
 public import Complexity.Algorithms.WordRAM.ExactTriangle.PreparationSpec
 public import Complexity.Algorithms.WordRAM.ExactTriangle.QueryScan
 public import Complexity.Algorithms.WordRAM.ExactTriangle.QuerySpec
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.Bounds
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.Copy
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.Decode
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.Entry
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.Exec
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.First
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.Flat
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.Header
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.InputSpec
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.Kernel
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.Prepare
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.Producer
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.ProducerQueries
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.Program
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.RawInput
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.SourceBounds
 public import Complexity.Algorithms.WordRAM.ExactTriangle.ResidueClasses
 public import Complexity.Algorithms.WordRAM.ExactTriangle.WriteMatrices
 public import Complexity.Algorithms.WordRAM.FusionTree.Binary

diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/PreparationInput.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/PreparationInput.lean
@@ -29,6 +29,7 @@ pre-halt state and the final halt charged.
 
 ## Main results
 
+* `PreparationInput.exec_input`: structured execution for composition, without the final halt.
 * `PreparationInput.runs_input`: initialized execution, exact readback, fits and charged halt.
 * `PreparationInput.bounded_reachable`: input-derived word and address bounds at every prefix.
 * `PreparationInput.width_le_log`, `PreparationInput.wordBound_le_pow`: logarithmic physical
@@ -213,18 +214,17 @@ private theorem input_fits {n D g p A : ℕ} (values : List ℤ)
       have hs := hmag.of_natAbs_le ((hv z hz).trans (by omega : A ≤ A + p + 1))
       exact (Signed.encode_fits hs).mono (by dsimp only [width]; omega)
 
-/-- Complete initialized execution at every admitted physical width. The prefix witness and
-the output predicate use the same actual pre-halt memory, and the bound includes the halt. -/
-theorem runs_input {n D g p A W : ℕ} (values : List ℤ)
+/-- Structured initialized execution for real native caller composition. The budget excludes
+only the final halt; all existing original-input, width and exact readback hypotheses remain.
+This does not accept an execution, layout or intermediate-fit certificate. -/
+theorem exec_input {n D g p A W : ℕ} (values : List ℤ)
     (hlen : values.length = 3 * (n * n))
     (hD : 1 ≤ D) (hDn : D ≤ n) (hg : 1 ≤ g) (hp : 0 < p)
     (hv : ∀ z ∈ values, z.natAbs ≤ A) (hw : width n D g p A ≤ W) :
     let C := fun rho => Nat.count (fun q => (values.getD q 0 % (p : ℤ)).toNat = rho) (n * n)
     let K := ChunkCatalogue.before C (queryCap n D) p
-    ∃ y t, t ≤ Instances.timeBound n D p K (numPieces n D g) ∧
-      Runs W flatProgram (State.init (input n D g p values)) ⟨Instances.program.size, y⟩
-        (t - 1) ∧
-      Executes W flatProgram (State.init (input n D g p values)) (y.regs Instances.output) t ∧
+    ∃ y, ExecWithin W Instances.program (.init (input n D g p values)) y
+        (Instances.timeBound n D p K (numPieces n D g) - 1) ∧
       Instances.Output n D g p (fun q => values.getD q 0)
         (.init (input n D g p values)) y ∧
       InputFits W (input n D g p values) ∧ y.Bounded W := by
@@ -244,6 +244,24 @@ theorem runs_input {n D g p A W : ℕ} (values : List ℤ)
   have hew := ExecWithin.mono_width Instances.program_fixed.2 hy hw
   have hi := (input_fits values hlen hv).mono hw
   have hybounded := hew.bounded (Data.Bounded.init hi)
+  exact ⟨y, hew, hout, hi, hybounded⟩
+
+/-- Complete initialized execution at every admitted physical width. The prefix witness and
+the output predicate use the same actual pre-halt memory, and the bound includes the halt. -/
+theorem runs_input {n D g p A W : ℕ} (values : List ℤ)
+    (hlen : values.length = 3 * (n * n))
+    (hD : 1 ≤ D) (hDn : D ≤ n) (hg : 1 ≤ g) (hp : 0 < p)
+    (hv : ∀ z ∈ values, z.natAbs ≤ A) (hw : width n D g p A ≤ W) :
+    let C := fun rho => Nat.count (fun q => (values.getD q 0 % (p : ℤ)).toNat = rho) (n * n)
+    let K := ChunkCatalogue.before C (queryCap n D) p
+    ∃ y t, t ≤ Instances.timeBound n D p K (numPieces n D g) ∧
+      Runs W flatProgram (State.init (input n D g p values)) ⟨Instances.program.size, y⟩
+        (t - 1) ∧
+      Executes W flatProgram (State.init (input n D g p values)) (y.regs Instances.output) t ∧
+      Instances.Output n D g p (fun q => values.getD q 0)
+        (.init (input n D g p values)) y ∧
+      InputFits W (input n D g p values) ∧ y.Bounded W := by
+  obtain ⟨y, hew, hout, hi, hybounded⟩ := exec_input values hlen hD hDn hg hp hv hw
   obtain ⟨t, ht, he⟩ := hew
   have hr := he.runs (pc := 0) (p := flatProgram) (Program.Contains.self _).append_left
   refine ⟨y, t + 1, ?_, ?_, ?_, hout, hi, hybounded⟩

diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct.lean
@@ -0,0 +1,65 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.SourceBounds
+
+/-!
+# Native ExactTriangle record-to-product adapter
+
+## Main definitions
+
+* `RecordProduct.program`: fixed 320-register consumer of any occupied producer record ordinal.
+* `RecordProduct.entryProgram`: actual original-input producer followed by ordinal-zero selection
+  and that consumer; original geometry proves the first record exists.
+* `RecordProduct.leftMatrix`, `RecordProduct.rightMatrix`: the unchanged native writer's actual
+  raw zero/one matrices, read in their respective row-major orders.
+* `RecordProduct.admissionWidth`, `RecordProduct.wordBound`: original-header/weight bounds for
+  every sufficiently wide physical execution and its complete prefix words/address support.
+
+## Main results
+
+* `RecordProduct.exec_of_output`: actual producer readback derives all six record words, every
+  matrix/query pointer and separation, the coordinate occurrences and their sparsity; the actual
+  callee returns all requested product values and preserves the producer catalogue and registers.
+* `RecordProduct.runs_input`: complete native `State.init`, same-data prefix `Runs`, returned
+  pointer, charged halt, exact product words, caller frame and occurrence sparsity. This fixed
+  initialized client selects the first record, rather than solving all prepared instances.
+* `RecordProduct.timeBound_le`: actual callee work plus `O(nD+Q)` descriptor/log/header/copy/
+  invocation overhead. There is no whole-window/catalogue initialization or snapshot.
+* `RecordProduct.thin_timeBound_sparse`: under `D=4^m`, `L=19m`, `D^18≤n` and `Q·2^m≤n²`, the
+  per-record bound including halt is `34603008·(19m+1)·n²/D^(1/18)`. The actual chunk derives
+  its occurrence bound; a mere distinct-set bound instead retains the additive occurrence term.
+* `RecordProduct.admissionWidth_le_log`: original polynomial header/weight envelopes give the
+  positive logarithmic threshold `(257κ+5906)·clog₂(n+2)` as a sufficient upper envelope.
+* `RecordProduct.bounded_reachable_original`, `RecordProduct.wordBound_le_pow`: all wider native
+  prefixes have polynomial words/support independent of the chosen physical width.
+
+The native code computes the record stride/address, reads every descriptor word, recovers `m`
+with the existing binary-logarithm program and division by two, writes original local headers,
+and copies raw X/Y and all interleaved coordinate occurrences above the actual producer heap.
+The entire 163-register callable bank is renamed together. Memory rebasing is performed by its
+actual compiler; register renaming alone is not a memory relocation. Raw matrix entries remain
+zero/one during adapter copying: the actual callee already charges their canonical-signed doubling.
+
+`PreparationInput.exec_input` exposes the existing structured initialized producer execution,
+and `PreparationInput.runs_input` reuses it without changing its statement or cost. Stage lemmas
+in the submodules are internal implementation interfaces. No intermediate fits, layouts, routing
+tables, run/time/solver or sparse-bound certificate is an original input hypothesis.
+
+This is per-record composition, not an aggregate subcubic ExactTriangle solver. Global parameter
+and prime selection, the outer instance loop, backend/witness reconstruction, the full ordinary
+distinct-position 3SUM composition and the improved 1.9992 endpoint remain open under #1394.
+
+## References
+
+The existing matrix writer and queried-product mathematics retain their pinned
+[AlmanWilliams2026] / Anthropic source mapping. This adapter, register framing, initialized
+composition and charged native proofs are original work; they do not transfer source Light
+semantics or instruction constants. The value-only matrix wrappers reuse `WriteMatrices.entry`.
+-/
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Bounds.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/RecordProduct/Bounds.lean
@@ -0,0 +1,154 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.WordRAM.ExactTriangle.RecordProduct.Producer
+public import Complexity.Algorithms.WordRAM.ExactTriangle.PreparationInput
+
+/-!
+# Input-derived admission and charged adapter overhead
+
+The actual producer supplies a polynomial bound for every pre-adapter word and address.
+Its existing `wordBound` determines a sufficient positive logarithmic physical width for the
+selected product's computed window. Adaptation is linear in `nD+Q`; this per-record statement
+does not sum an ExactTriangle solver or establish its aggregate subcubic bound.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct
+
+open Cslib.WordRAM Cslib.Algorithms.ExactTriangle
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+open Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage
+
+/-- Original-input physical width covering the actual producer, every dirty producer word
+before normalization, and all relocated product addresses. -/
+@[expose] def admissionWidth (n D g p A : ℕ) : ℕ :=
+  PreparationInput.width n D g p A +
+    256 * Nat.clog 2 (2 * PreparationInput.wordBound n D g p A + n + n ^ 2 + 5)
+
+/-- Physical admission is positive, including parameter boundary cases. -/
+theorem admissionWidth_pos (n D g p A : ℕ) : 0 < admissionWidth n D g p A := by
+  unfold admissionWidth PreparationInput.width
+  omega
+
+/-- Actual producer word/address bounds and the computed chunk size discharge the physical
+fit numerically; neither a window nor an intermediate arithmetic certificate is an input. -/
+theorem physical_fits {W n D g p A b Q : ℕ}
+    (hb : b ≤ PreparationInput.wordBound n D g p A) (hQ : Q ≤ n ^ 2)
+    (hW : admissionWidth n D g p A ≤ W) :
+    Fits W (2 * b + 4 * CallableProduct.windowSize n Q + 1024) := by
+  have hw : 256 * Nat.clog 2 (2 * PreparationInput.wordBound n D g p A + n + n ^ 2 + 5) ≤ W :=
+    by unfold admissionWidth at hW; omega
+  have hfit := CallableProduct.physical_fits hw
+  have hM : CallableProduct.windowSize n Q ≤ CallableProduct.windowSize n (n ^ 2) := by
+    apply Nat.pow_le_pow_right (by decide)
+    exact Nat.mul_le_mul_left 128 (Nat.clog_mono_right 2 (by omega))
+  exact hfit.of_le (by omega)
+
+/-- The final threshold is logarithmic in the original outer dimension under the producer's
+standard polynomial original-header/weight hypotheses. The constant is positive for every κ. -/
+theorem admissionWidth_le_log {n D g p A κ : ℕ} (hn : 1 ≤ n)
+    (hD : D ≤ n) (hg : g ≤ n) (hp : p ≤ n) (hA : A ≤ (n + 2) ^ κ) :
+    admissionWidth n D g p A ≤ (257 * κ + 5906) * Nat.clog 2 (n + 2) := by
+  let b := n + 2
+  have hb : 2 ≤ b := by dsimp only [b]; omega
+  have hP := PreparationInput.wordBound_le_pow hn hD hg hp hA
+  change PreparationInput.wordBound n D g p A ≤ b ^ (κ + 19) at hP
+  have hunit : 1 ≤ b ^ (κ + 19) := Nat.one_le_pow _ _ (by omega)
+  have hnpow : n ≤ b ^ (κ + 19) := (show n ≤ b by dsimp only [b]; omega).trans
+    (Nat.le_self_pow (by omega) b)
+  have hn2 : n ^ 2 ≤ b ^ (κ + 19) :=
+    (Nat.pow_le_pow_left (by dsimp only [b]; omega : n ≤ b) 2).trans
+      (Nat.pow_le_pow_right (by omega : 1 ≤ b) (by omega : 2 ≤ κ + 19))
+  have harg : 2 * PreparationInput.wordBound n D g p A + n + n ^ 2 + 5 ≤ b ^ (κ + 23) := by
+    have hsum : 2 * PreparationInput.wordBound n D g p A + n + n ^ 2 + 5 ≤
+        9 * b ^ (κ + 19) := by omega
+    have hc : 9 ≤ b ^ 4 := (show 9 ≤ 2 ^ 4 by decide).trans (Nat.pow_le_pow_left hb 4)
+    calc
+      _ ≤ 9 * b ^ (κ + 19) := hsum
+      _ ≤ b ^ 4 * b ^ (κ + 19) := Nat.mul_le_mul_right _ hc
+      _ = b ^ (κ + 23) := by rw [← Nat.pow_add]; congr 1; omega
+  have hbase := Nat.le_pow_clog (by decide : 1 < (2 : ℕ)) b
+  have hlogBound := harg.trans (Nat.pow_le_pow_left hbase (κ + 23))
+  rw [← Nat.pow_mul] at hlogBound
+  have hlog := Nat.clog_le_of_le_pow hlogBound
+  have hprep := PreparationInput.width_le_log hn hD hg hp hA
+  change Nat.clog 2 (2 * PreparationInput.wordBound n D g p A + n + n ^ 2 + 5) ≤
+    Nat.clog 2 b * (κ + 23) at hlog
+  unfold admissionWidth
+  dsimp only [b] at hlog
+  nlinarith only [hlog, hprep]
+
+/-- All real descriptor/log/header/copy/invocation work is linear in original matrices and
+occurrences. This includes standalone halt, but not another execution of the producer. -/
+theorem timeBound_le {m n : ℕ} (qs : List (Fin n × Fin n)) (hN : D m ^ 18 ≤ n) :
+    timeBound (m := m) qs + 1 ≤
+      3 * (QueriedProduct.timeBound (show m ≤ 19 * m by omega) qs + 1) +
+        4096 * (n * D m + qs.length + 1) := by
+  have hn : 1 ≤ n := Nat.pow_pos (Nat.pow_pos (by decide : 0 < (4 : ℕ))) |>.trans_le hN
+  have hm : m ≤ D m := by
+    have hlog := Nat.log_le_self 2 (4 ^ m)
+    rw [log_two_four_pow] at hlog
+    change m ≤ 4 ^ m
+    omega
+  have hND : D m ≤ n * D m := Nat.le_mul_of_pos_left _ hn
+  have ht := CallableProduct.timeBound_le (m := m) qs
+  unfold timeBound
+  omega
+
+/-- The actual callee envelope already dominates a second copy of this linear adaptation.
+This comparison reuses its established sparse bounds without a separate polylog oracle. -/
+theorem timeBound_le_twice_callable {m n : ℕ} (qs : List (Fin n × Fin n))
+    (hN : D m ^ 18 ≤ n) :
+    timeBound (m := m) qs + 1 ≤ 2 * (CallableProduct.timeBound (m := m) qs + 3) := by
+  have hn : 1 ≤ n := Nat.pow_pos (Nat.pow_pos (by decide : 0 < (4 : ℕ))) |>.trans_le hN
+  have hm : m ≤ n * D m := by
+    have hlog := Nat.log_le_self 2 (4 ^ m)
+    rw [log_two_four_pow] at hlog
+    have hmul : D m ≤ n * D m := Nat.le_mul_of_pos_left _ hn
+    change 4 ^ m ≤ n * D m at hmul
+    omega
+  unfold timeBound CallableProduct.timeBound CallableProduct.coreTime QueriedProduct.timeBound
+    QueriedProduct.inputEnd
+  omega
+
+/-- Distinct-set sparsity retains the actual list-occurrence charge. -/
+theorem thin_timeBound {m n : ℕ} (qs : List (Fin n × Fin n)) (hN : D m ^ 18 ≤ n)
+    (hQ : qs.toFinset.card * 2 ^ m ≤ n ^ 2) :
+    ((timeBound (m := m) qs + 1 : ℕ) : ℝ) ≤
+      524288 * ((19 * m + 1 : ℕ) : ℝ) *
+        (65 * ((D m : ℝ) ^ (-(1 / 18 : ℝ)) * (n : ℝ) ^ 2) + qs.length) := by
+  have ht : ((timeBound (m := m) qs + 1 : ℕ) : ℝ) ≤
+      2 * ((CallableProduct.timeBound (m := m) qs + 3 : ℕ) : ℝ) := by
+    exact_mod_cast timeBound_le_twice_callable qs hN
+  have h := CallableProduct.thin_timeBound qs hN hQ
+  calc
+    _ ≤ 2 * ((CallableProduct.timeBound (m := m) qs + 3 : ℕ) : ℝ) := ht
+    _ ≤ 2 * (262144 * ((19 * m + 1 : ℕ) : ℝ) *
+        (65 * ((D m : ℝ) ^ (-(1 / 18 : ℝ)) * (n : ℝ) ^ 2) + qs.length)) := by linarith
+    _ = _ := by ring
+
+/-- Occurrence sparsity, which actual producer chunks supply, absorbs every occurrence charge.
+The bound includes the adapter's standalone halt; producer execution is charged separately. -/
+theorem thin_timeBound_sparse {m n : ℕ} (qs : List (Fin n × Fin n))
+    (hN : D m ^ 18 ≤ n) (hQ : qs.length * 2 ^ m ≤ n ^ 2) :
+    ((timeBound (m := m) qs + 1 : ℕ) : ℝ) ≤
+      34603008 * ((19 * m + 1 : ℕ) : ℝ) * (n : ℝ) ^ 2 / (D m : ℝ) ^ (1 / 18 : ℝ) := by
+  have ht : ((timeBound (m := m) qs + 1 : ℕ) : ℝ) ≤
+      2 * ((CallableProduct.timeBound (m := m) qs + 3 : ℕ) : ℝ) := by
+    exact_mod_cast timeBound_le_twice_callable qs hN
+  have h := CallableProduct.thin_timeBound_sparse qs hN hQ
+  calc
+    _ ≤ 2 * ((CallableProduct.timeBound (m := m) qs + 3 : ℕ) : ℝ) := ht
+    _ ≤ 2 * (17301504 * ((19 * m + 1 : ℕ) : ℝ) * (n : ℝ) ^ 2 /
+        (D m : ℝ) ^ (1 / 18 : ℝ)) := by linarith
+    _ = _ := by ring
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct