diff --git a/Complexity.lean b/Complexity.lean
index e546790ca0..cf7aea2ad6 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -112,6 +112,8 @@ public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.Ada
 public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.Admission
 public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.Copy
 public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.Core
+public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.DyadicCost
+public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.DyadicExecution
 public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.Exec
 public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.Flat
 public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.Header
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/DyadicCost.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/DyadicCost.lean
new file mode 100644
index 0000000000..51cc127efe
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/DyadicCost.lean
@@ -0,0 +1,266 @@
+/-
+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.CallableFixedPrime.SourceBounds
+public import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.TimeBound
+public import Complexity.Algorithms.WordRAM.ExactTriangle.DyadicCost.Asymptotics
+public import Complexity.Algorithms.WordRAM.ExactTriangle.DyadicParameters.Exec
+import Mathlib.Analysis.SpecialFunctions.Log.Base
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
+
+/-!
+# A content-independent natural allowance for callable dyadic solving
+
+The natural function depends only on original dimension n and original weight bound F. A
+selected-prime logarithmic estimate and the actual wrapper charges bound the real parameter,
+selector and callable ledger, including header/halt reserve. This is a mathematical time bound;
+the program does not compute it or receive a time certificate. Small-branch execution and
+actual program assembly remain separate.
+
+## Main definitions
+
+* `dyadicTime`: natural allowance for the complete fast ledger, independent of input contents,
+  reference memory, layout and physical width.
+
+## Main results
+
+* `timeBound_le_dyadicTime`: the actual charged fast ledger is bounded at every selected prime.
+* `exists_dyadicTime_subcubic_bound`: uniform strict-subcubic growth for polynomial original F.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime
+
+open Filter Cslib.WordRAM Cslib.Matrix Cslib.Algorithms.ExactTriangle
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+open ParameterChoice
+
+private noncomputable def weightExponent (n F : ℕ) : ℝ :=
+  1 + Real.logb n (F + 1)
+
+private def setupLog (n F : ℕ) : ℕ :=
+  Nat.clog 2 (4 * n + 3 * (n * n) * (2 * F + 1) + 4)
+
+private noncomputable def upperTime (n F : ℕ) : ℝ :=
+  3 * DyadicCost.costCoefficient (weightExponent n F) n * ((n : ℝ) ^ 3 / groups n) +
+    24 * (n : ℝ) ^ 2 + 24669 * (setupLog n F : ℝ) + 497
+
+/-- Natural fast-ledger allowance from original n and F only. The ceiling is descriptive
+metadata, not an executed instruction or an oracle supplied to the native solver. The final
+sixteen reserve the assembled initialized header and halt. -/
+noncomputable def dyadicTime (n F : ℕ) : ℕ := ⌈upperTime n F⌉₊ + 16
+
+private theorem one_le_weightExponent {n : ℕ} (hn : 2 ≤ n) (F : ℕ) :
+    1 ≤ weightExponent n F := by
+  have hlog : 0 < Real.log (n : ℝ) := Real.log_pos (by exact_mod_cast hn)
+  have hF : 0 ≤ Real.log (F + 1 : ℝ) :=
+    Real.log_nonneg (by exact_mod_cast (by omega : 1 ≤ F + 1))
+  have hdiv := div_nonneg hF hlog.le
+  unfold weightExponent Real.logb
+  linarith only [hdiv]
+
+private theorem bound_le_rpow_weightExponent {n : ℕ} (hn : 2 ≤ n) (F : ℕ) :
+    (F : ℝ) ≤ (n : ℝ) ^ weightExponent n F := by
+  have hn0 : (0 : ℝ) < n := by exact_mod_cast (by omega : 0 < n)
+  have hn1 : (n : ℝ) ≠ 1 := by exact_mod_cast (by omega : n ≠ 1)
+  rw [weightExponent, Real.rpow_add hn0, Real.rpow_one,
+    Real.rpow_logb hn0 hn1 (by positivity)]
+  have hnR : (1 : ℝ) ≤ n := by exact_mod_cast (by omega : 1 ≤ n)
+  nlinarith
+
+private theorem original_weights {n F : ℕ} (values : List ℤ)
+    (hlen : values.length = 3 * (n * n)) (hv : ∀ z ∈ values, z.natAbs ≤ F) :
+    WeightsBoundedBy
+      (fun u v : Fin n => values.getD (pairIndex (u, v)) 0)
+      (fun u v => values.getD (n * n + pairIndex (u, v)) 0)
+      (fun u v => values.getD (2 * (n * n) + pairIndex (u, v)) 0) (F : ℝ) := by
+  have hlookup (q : ℕ) : (values.getD q 0).natAbs ≤ F := by
+    by_cases hq : q < 3 * (n * n)
+    · exact RecordWitness.original_magnitude values hlen hv hq
+    · rw [List.getD_eq_default values 0 (by omega : values.length ≤ q), Int.natAbs_zero]
+      exact Nat.zero_le F
+  have hw (q : ℕ) : ((|values.getD q 0| : ℤ) : ℝ) ≤ F := by
+    rw [← Int.natCast_natAbs, Int.cast_natCast]
+    exact_mod_cast hlookup q
+  exact ⟨fun _ _ => hw _, fun _ _ => hw _, fun _ _ => hw _⟩
+
+private theorem scalar_bounds {n p : ℕ} (hn : 0 < n)
+    (hp : p ∈ Nat.sqrtPrimeWindow (window n)) :
+    window n ≤ n ∧ groups n ≤ n ∧ p ≤ n := by
+  have hd := window_le hn
+  have hsq := (Nat.mem_sqrtPrimeWindow_iff_sq.mp hp).2.2
+  exact ⟨hd, (groups_le_window n).trans hd,
+    (Nat.le_self_pow (by decide : 2 ≠ 0) p).trans (hsq.le.trans hd)⟩
+
+/-- Bound the actual fast initialized ledger, including all copies, setup, dispatch/restore,
+header and halt. All original matrices bounded by F share this same natural function. The
+prime is actually selected; no layout, execution or time law is a premise. -/
+theorem timeBound_le_dyadicTime {n F p : ℕ} (hf : 0 < blocks n) (values : List ℤ)
+    (hlen : values.length = 3 * (n * n)) (hv : ∀ z ∈ values, z.natAbs ≤ F)
+    (hp : IsSelectedPrime
+      (fun u v : Fin n => values.getD (pairIndex (u, v)) 0)
+      (fun u v => values.getD (n * n + pairIndex (u, v)) 0)
+      (fun u v => values.getD (2 * (n * n) + pairIndex (u, v)) 0) (window n) p)
+    (mem : ℕ → ℕ) :
+    DyadicParameters.timeBound n + PrimeSelection.timeBound n (window n) +
+        timeBound (m := level n) (pos_of_blocks_pos hf) (groups n) p values mem + 42 ≤
+      dyadicTime n F := by
+  have hn := pos_of_blocks_pos hf
+  obtain ⟨hd, hg, hpN⟩ := scalar_bounds hn hp.1
+  have hn2 : 2 ≤ n := by have h := (window_ge_sixteen hf).trans hd; omega
+  have hexp := bound_le_rpow_weightExponent hn2 F
+  obtain ⟨hab, hbc, hac⟩ := original_weights values hlen hv
+  have hv' : WeightsBoundedBy
+      (fun u v : Fin n => values.getD (pairIndex (u, v)) 0)
+      (fun u v => values.getD (n * n + pairIndex (u, v)) 0)
+      (fun u v => values.getD (2 * (n * n) + pairIndex (u, v)) 0)
+      ((n : ℝ) ^ weightExponent n F) :=
+    ⟨fun _ _ => (hab _ _).trans hexp, fun _ _ => (hbc _ _).trans hexp,
+      fun _ _ => (hac _ _).trans hexp⟩
+  have hc := DyadicCost.components_timeBound_le hf (one_le_weightExponent hn2 F) values mem hv' hp
+  change (_ : ℝ) ≤ DyadicCost.costCoefficient (weightExponent n F) n *
+    ((n : ℝ) ^ 3 / groups n) at hc
+  have hraw := rawTotal_le values hlen hv
+  have hlog : Nat.clog 2 (n + window n + groups n + p + rawTotal n values + 4) ≤ setupLog n F :=
+    Nat.clog_mono_right 2 (by omega)
+  have hparam := DyadicParameters.timeBound_le n
+  have hnat : DyadicParameters.timeBound n + PrimeSelection.timeBound n (window n) +
+      timeBound (m := level n) hn (groups n) p values mem + 42 ≤
+    3 * (12 * Nat.log 2 n + 36 + (PrimeSelection.timeBound n (window n) + 16) +
+      FixedPrime.timeBound (m := level n) hn (groups n) p values mem) +
+        24 * (n * n) + 24669 * setupLog n F + 497 + 16 := by
+    unfold timeBound
+    dsimp only [D, window] at *
+    nlinarith only [hlog, hparam]
+  have hreal := (Nat.cast_le (α := ℝ)).mpr hnat
+  have hceil : upperTime n F ≤ (⌈upperTime n F⌉₊ : ℝ) := Nat.le_ceil _
+  apply (Nat.cast_le (α := ℝ)).mp
+  unfold dyadicTime
+  push_cast at hreal hc ⊢
+  unfold upperTime at hceil ⊢
+  nlinarith only [hreal, hc, hceil]
+
+private theorem setupLog_le_log {n F κ : ℕ} (hF : F ≤ (n + 2) ^ κ) :
+    setupLog n F ≤ (κ + 7) * Nat.clog 2 (n + 2) := by
+  let B := n + 2
+  have hb : 2 ≤ B := by dsimp only [B]; omega
+  have hb1 : 1 ≤ B := by omega
+  have hnB : n ≤ B := by dsimp only [B]; omega
+  have hn2 : n * n ≤ B ^ 2 := (Nat.mul_le_mul hnB hnB).trans_eq (by ring)
+  have hunit : 1 ≤ B ^ κ := Nat.one_le_pow _ _ hb1
+  have hcoef : 2 * F + 1 ≤ 3 * B ^ κ := by
+    have : F ≤ B ^ κ := hF
+    omega
+  have hterm : 3 * (n * n) * (2 * F + 1) ≤ 9 * B ^ (κ + 2) := by
+    calc
+      _ ≤ (3 * B ^ 2) * (3 * B ^ κ) :=
+        Nat.mul_le_mul (Nat.mul_le_mul_left 3 hn2) hcoef
+      _ = _ := by rw [pow_add]; ring
+  have hB : B ≤ B ^ (κ + 2) := Nat.le_self_pow (by omega) _
+  have hlinear : 4 * n + 4 ≤ 8 * B ^ (κ + 2) := by nlinarith only [hnB, hb1, hB]
+  have hsum : 4 * n + 3 * (n * n) * (2 * F + 1) + 4 ≤ 17 * B ^ (κ + 2) := by
+    omega
+  have h17 : 17 ≤ B ^ 5 := (by decide : 17 ≤ (2 : ℕ) ^ 5).trans
+    (Nat.pow_le_pow_left hb 5)
+  have hpoly : 4 * n + 3 * (n * n) * (2 * F + 1) + 4 ≤ B ^ (κ + 7) := by
+    calc
+      _ ≤ 17 * B ^ (κ + 2) := hsum
+      _ ≤ B ^ 5 * B ^ (κ + 2) := Nat.mul_le_mul_right _ h17
+      _ = _ := by rw [← pow_add]; congr 1; omega
+  have h := hpoly.trans (Nat.pow_le_pow_left
+    (Nat.le_pow_clog (by decide : 1 < (2 : ℕ)) B) (κ + 7))
+  rw [← pow_mul, Nat.mul_comm (Nat.clog 2 B) (κ + 7)] at h
+  exact Nat.clog_le_of_le_pow h
+
+private theorem weightExponent_le {n F κ : ℕ} (hn : 2 ≤ n) (hF : F ≤ (n + 2) ^ κ) :
+    weightExponent n F ≤ (2 * κ + 2 : ℕ) := by
+  have hpow : F ≤ n ^ (2 * κ) :=
+    hF.trans ((Nat.pow_le_pow_left (by nlinarith : n + 2 ≤ n ^ 2) κ).trans_eq
+      (by rw [← pow_mul]))
+  have hunit : 1 ≤ n ^ (2 * κ) := Nat.one_le_pow _ _ (by omega)
+  have hF1 : F + 1 ≤ n ^ (2 * κ + 1) := by
+    rw [pow_succ]
+    nlinarith only [hpow, hunit, hn]
+  have hF1R : (F + 1 : ℝ) ≤ (n : ℝ) ^ ((2 * κ + 1 : ℕ) : ℝ) := by
+    rw [Real.rpow_natCast]
+    exact_mod_cast hF1
+  have hnR : (1 : ℝ) < n := by exact_mod_cast hn
+  have hlog := (Real.logb_le_iff_le_rpow hnR (by positivity : (0 : ℝ) < F + 1)).mpr hF1R
+  unfold weightExponent
+  push_cast at hlog ⊢
+  linarith only [hlog]
+
+private theorem upperTime_nonneg {n : ℕ} (hn : 2 ≤ n) (F : ℕ) : 0 ≤ upperTime n F := by
+  have hC : 0 ≤ falsePositiveConst := (by norm_num : (0 : ℝ) ≤ 1).trans one_le_falsePositiveConst
+  have hlog : 0 ≤ Real.log (n : ℝ) := Real.log_nonneg (by exact_mod_cast (by omega : 1 ≤ n))
+  have hexp : 0 ≤ weightExponent n F := (by norm_num : (0 : ℝ) ≤ 1).trans
+    (one_le_weightExponent hn F)
+  unfold upperTime DyadicCost.costCoefficient
+  positivity
+
+-- Only the original fixed fast-threshold numeral is normalized during filter transport.
+set_option exponentiation.threshold 1296 in
+/-- One positive coefficient and threshold per weight exponent control the natural time
+function uniformly over all original bounds F≤(n+2)^κ. This is an estimate of the bound
+function itself, usable by the actual Callee contract. No contents/layout/width occurs in it. -/
+theorem exists_dyadicTime_subcubic_bound {κ : ℕ} (hκ : 1 ≤ κ) :
+    ∃ C : ℝ, 0 < C ∧ ∃ N : ℕ, 2 ^ 1296 ≤ N ∧
+      ∀ n ≥ N, ∀ F ≤ (n + 2) ^ κ,
+        (dyadicTime n F : ℝ) ≤ C * (n : ℝ) ^ (3 - 1 / 1296 : ℝ) := by
+  let C : ℝ := (49338 * (κ + 7) + 550 : ℕ)
+  have hcκ : (1 : ℝ) ≤ (2 * κ + 2 : ℕ) := by exact_mod_cast (by omega : 1 ≤ 2 * κ + 2)
+  have hevent := DyadicCost.costCoefficient_eventually_le_rpow hcκ
+    (by norm_num : (0 : ℝ) < 1 / 1296)
+  have hfinal : ∀ᶠ n : ℕ in atTop, ∀ F ≤ (n + 2) ^ κ,
+      (dyadicTime n F : ℝ) ≤ C * (n : ℝ) ^ (3 - 1 / 1296 : ℝ) := by
+    filter_upwards [hevent, eventually_ge_atTop (16 : ℕ)] with n hc hn
+    intro F hF
+    have hn2 : 2 ≤ n := by omega
+    have hn1 : 1 ≤ n := by omega
+    have hcoeff := (DyadicCost.costCoefficient_mono hn1 (weightExponent_le hn2 hF)).trans hc
+    have hmain : 3 * DyadicCost.costCoefficient (weightExponent n F) n *
+        ((n : ℝ) ^ 3 / groups n) ≤ 12 * (n : ℝ) ^ (3 - 1 / 1296 : ℝ) := by
+      calc
+        _ ≤ 3 * (n : ℝ) ^ (1 / 1296 : ℝ) * ((n : ℝ) ^ 3 / groups n) := by gcongr
+        _ ≤ 3 * (n : ℝ) ^ (1 / 1296 : ℝ) *
+            (4 * (n : ℝ) ^ (3 - 1 / 648 : ℝ)) := by
+          exact mul_le_mul_of_nonneg_left (cubic_div_groups_le (by omega)) (by positivity)
+        _ = _ := by
+          rw [mul_assoc, mul_left_comm ((n : ℝ) ^ (1 / 1296 : ℝ)) 4,
+            ← mul_assoc, ← Real.rpow_add (by exact_mod_cast (by omega : 0 < n))]
+          norm_num
+    have hlog := setupLog_le_log hF
+    have hclog : Nat.clog 2 (n + 2) ≤ n + 2 :=
+      Nat.clog_le_of_le_pow (show n + 2 ≤ 2 ^ (n + 2) from Nat.lt_two_pow_self.le)
+    have hn2' : n + 2 ≤ 2 * (n * n) := by nlinarith
+    have hsetup := hlog.trans (Nat.mul_le_mul_left (κ + 7) (hclog.trans hn2'))
+    have hsmallNat : 24 * (n * n) + 24669 * setupLog n F + 514 ≤
+        (49338 * (κ + 7) + 538) * (n * n) := by
+      have hunit : 1 ≤ n * n := by nlinarith
+      nlinarith only [hsetup, hunit]
+    have hsmallR := (Nat.cast_le (α := ℝ)).mpr hsmallNat
+    have hpow : (n : ℝ) ^ 2 ≤ (n : ℝ) ^ (3 - 1 / 1296 : ℝ) := by
+      rw [← Real.rpow_natCast]
+      exact Real.rpow_le_rpow_of_exponent_le (by exact_mod_cast hn1) (by norm_num)
+    have hscaled := mul_le_mul_of_nonneg_left hpow
+      (show (0 : ℝ) ≤ (49338 * (κ + 7) + 538 : ℕ) by positivity)
+    have hceil := (Nat.ceil_lt_add_one (upperTime_nonneg hn2 F)).le
+    unfold dyadicTime C
+    push_cast at hsmallR hscaled ⊢
+    unfold upperTime at hceil ⊢
+    nlinarith only [hmain, hsmallR, hscaled, hceil]
+  obtain ⟨N, hN⟩ := eventually_atTop.mp hfinal
+  refine ⟨C, by dsimp only [C]; positivity, max N (2 ^ 1296), le_max_right _ _, ?_⟩
+  intro n hn
+  exact hN n ((le_max_left _ _).trans hn)
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/DyadicExecution.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/DyadicExecution.lean
new file mode 100644
index 0000000000..262c944209
--- /dev/null
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/CallableFixedPrime/DyadicExecution.lean
@@ -0,0 +1,93 @@
+/-
+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.CallableFixedPrime.DyadicCost
+
+/-!
+# Selected-prime initialized executions with a strict-subcubic charge
+
+The existing real callable program supplies original signed verdicts and witnesses. Its actual
+initialized prefix and halt are bounded by the natural dyadic time function, which is uniformly
+strict-subcubic for polynomial original weights. The sufficient physical width is derived from
+the original inputs. Runtime p is still a selected prime supplied in the input; parameter/prime
+execution and final 3SUM composition remain separate.
+
+## Main results
+
+* `exists_dyadic_runs_threshold`: a shared coefficient and threshold per weight exponent, with
+  actual same-state prefix/halt, natural time allowance, exact verdict/witness and input frame.
+-/
+
+public section
+
+namespace Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime
+
+open Cslib.WordRAM Cslib.Matrix Cslib.Algorithms.ExactTriangle
+open Cslib.Algorithms.MatrixMultiplication.Schonhage
+open ParameterChoice
+
+-- Only the existing fixed fast-threshold numeral is normalized during proof transport.
+set_option exponentiation.threshold 1296 in
+/-- Actual initialized computation, not a supplied run law. The positive coefficient and
+threshold are chosen before every original input, prime and width. Selected-prime membership
+is a performance hypothesis on runtime p; no layout, clock or execution certificate is supplied.
+The allowance conservatively includes parameter/selector work not executed by this subroutine. -/
+theorem exists_dyadic_runs_threshold {κ : ℕ} (hκ : 1 ≤ κ) :
+    ∃ C : ℝ, 0 < C ∧ ∃ N : ℕ, 2 ^ 1296 ≤ N ∧
+      ∀ n ≥ N, ∀ (F : ℕ) (values : List ℤ) (p W : ℕ),
+        values.length = 3 * (n * n) → (∀ z ∈ values, z.natAbs ≤ F) → F ≤ (n + 2) ^ κ →
+        IsSelectedPrime
+          (fun u v : Fin n => values.getD (pairIndex (u, v)) 0)
+          (fun u v => values.getD (n * n + pairIndex (u, v)) 0)
+          (fun u v => values.getD (2 * (n * n) + pairIndex (u, v)) 0) (window n) p →
+        (24664 * (κ + 9) + 19) * Nat.clog 2 (n + 2) ≤ W →
+        InputFits W (PreparationInput.input n (window n) (groups n) p values) ∧
+          ∃ y t,
+            Runs W (entryProgram.program Reg.found)
+              (State.init (PreparationInput.input n (window n) (groups n) p values))
+              ⟨entryProgram.size, y⟩ t ∧
+            Executes W (entryProgram.program Reg.found)
+              (State.init (PreparationInput.input n (window n) (groups n) p values))
+              (y.regs Reg.found) (t + 1) ∧
+            t + 1 ≤ dyadicTime n F ∧
+            (dyadicTime n F : ℝ) ≤ C * (n : ℝ) ^ (3 - 1 / 1296 : ℝ) ∧
+            y.Bounded W ∧ (y.regs Reg.found = 0 ∨ y.regs Reg.found = 1) ∧
+            (y.regs Reg.found = 1 ↔ HasZeroTriangle
+              (fun u v : Fin n => values.getD (pairIndex (u, v)) 0)
+              (fun u v => values.getD (n * n + pairIndex (u, v)) 0)
+              (fun u v => values.getD (2 * (n * n) + pairIndex (u, v)) 0)) ∧
+            (y.regs Reg.found = 1 → ∃ u v c : Fin n,
+              y.regs Reg.witnessA = u.val ∧ y.regs Reg.witnessB = v.val ∧
+              y.regs Reg.witnessC = c.val ∧
+              weightSum (fun a b => values.getD (pairIndex (a, b)) 0)
+                (fun a b => values.getD (n * n + pairIndex (a, b)) 0)
+                (fun a b => values.getD (2 * (n * n) + pairIndex (a, b)) 0) u v c = 0) ∧
+            ∀ q < workspaceBase n, y.mem q =
+              (Data.init (PreparationInput.input n (window n) (groups n) p values) :
+                Data 640).mem q := by
+  obtain ⟨C, hC, N, hN, hc⟩ := exists_dyadicTime_subcubic_bound hκ
+  refine ⟨C, hC, N, hN, ?_⟩
+  intro n hnN F values p W hlen hv hF hp hW
+  have hn : 0 < n := (Nat.two_pow_pos 1296).trans_le (hN.trans hnN)
+  have hf := (blocks_pos_iff n).mpr (hN.trans hnN)
+  have hd := window_le hn
+  have hg := (groups_le_window n).trans hd
+  have hpN : p ≤ n := (Nat.le_self_pow (by decide : 2 ≠ 0) p).trans
+    ((Nat.mem_sqrtPrimeWindow_iff_sq.mp hp.1).2.2.le.trans hd)
+  have hw : inputWidth n (window n) (groups n) p values ≤ W :=
+    (inputWidth_le_log values hlen hv hd hg hpN hF).trans hW
+  obtain ⟨hi, a, hout, y, t, ht, hr, he, hbound, hflag, hscan, hiff, hwitness, hframe, hregs⟩ :=
+    runs_input (m := level n) values hlen (window_ge_sixteen hf)
+      (one_le_groups n) hp.1 (geometry hn) hw
+  have hb := timeBound_le_dyadicTime hf values hlen hv hp a.mem
+  have ht' : t + 1 ≤ dyadicTime n F := by omega
+  exact ⟨hi, y, t, hr, he, ht', hc n hnN F hF, hbound, hflag, hiff, hwitness,
+    fun q hq => hframe q (Or.inl hq)⟩
+
+end Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime
diff --git a/Complexity/Algorithms/WordRAM/ExactTriangle/DyadicCost/Asymptotics.lean b/Complexity/Algorithms/WordRAM/ExactTriangle/DyadicCost/Asymptotics.lean
index e1a0a05b7f..2b990cc5fe 100644
--- a/Complexity/Algorithms/WordRAM/ExactTriangle/DyadicCost/Asymptotics.lean
+++ b/Complexity/Algorithms/WordRAM/ExactTriangle/DyadicCost/Asymptotics.lean
@@ -27,6 +27,9 @@ the source's tuned 3SUM exponent.
 
 ## Main results
 
+* `costCoefficient_mono`: monotonicity in the original-weight exponent.
+* `costCoefficient_eventually_le_rpow`: reusable coefficient absorption for concrete native callers.
+
 * `exists_components_subcubic_threshold`: beyond one threshold, the actual component allowance
   is at most `4*n^(3-1/1296)`, uniformly over original weights bounded by `n^κ`.
 -/
@@ -38,10 +41,22 @@ namespace Cslib.Algorithms.WordRAM.ExactTriangle.DyadicCost
 open Filter Cslib.Matrix Cslib.Algorithms.ExactTriangle
 open ParameterChoice
 
-private noncomputable def coefficient (κ : ℝ) (n : ℕ) : ℝ :=
+/-- The explicit coefficient in the proved dyadic component allowance. This is a numerical
+upper estimate, not an execution contract supplied to an algorithm. -/
+@[expose] noncomputable def costCoefficient (κ : ℝ) (n : ℕ) : ℝ :=
   238169 + 12 * (Nat.log 2 n : ℝ) + 138412032 * ((19 * level n + 1 : ℕ) : ℝ) +
     (140 * falsePositiveConst + 140) * κ * Real.log n
 
+/-- The component coefficient is monotone in its weight exponent for positive dimensions. -/
+theorem costCoefficient_mono {n : ℕ} (hn : 1 ≤ n) {a b : ℝ} (h : a ≤ b) :
+    costCoefficient a n ≤ costCoefficient b n := by
+  have hC : 0 ≤ falsePositiveConst := (by norm_num : (0 : ℝ) ≤ 1).trans one_le_falsePositiveConst
+  have hlog : 0 ≤ Real.log (n : ℝ) := Real.log_nonneg (by exact_mod_cast hn)
+  have hm := mul_le_mul_of_nonneg_left h
+    (show 0 ≤ (140 * falsePositiveConst + 140) * Real.log (n : ℝ) by positivity)
+  unfold costCoefficient
+  nlinarith only [hm]
+
 private noncomputable def logCoefficient (κ : ℝ) : ℝ :=
   238169 + 138412032 + (12 + 19 * 138412032) / Real.log 2 +
     (140 * falsePositiveConst + 140) * κ
@@ -54,7 +69,7 @@ private theorem logCoefficient_pos {κ : ℝ} (hκ : 1 ≤ κ) : 0 < logCoeffici
   positivity
 
 private theorem coefficient_le_log {n : ℕ} {κ : ℝ} (hn : 16 ≤ n) :
-    coefficient κ n ≤ logCoefficient κ * Real.log n := by
+    costCoefficient κ n ≤ logCoefficient κ * Real.log n := by
   have hnR : (16 : ℝ) ≤ n := by exact_mod_cast hn
   have hlog1 : 1 ≤ Real.log n :=
     (Real.le_log_iff_exp_le (by linarith)).mpr
@@ -62,7 +77,7 @@ private theorem coefficient_le_log {n : ℕ} {κ : ℝ} (hn : 16 ≤ n) :
   have hl : (level n : ℝ) ≤ Nat.log 2 n := by exact_mod_cast level_le_log n
   have hb : (Nat.log 2 n : ℝ) ≤ Real.log n / Real.log 2 := by
     simpa only [Real.logb, Nat.cast_ofNat] using Real.natLog_le_logb n 2
-  unfold coefficient logCoefficient
+  unfold costCoefficient logCoefficient
   push_cast
   have hlevel := mul_le_mul_of_nonneg_left hl (by norm_num : (0 : ℝ) ≤ 19 * 138412032)
   have hconstant := mul_le_mul_of_nonneg_left hlog1
@@ -81,8 +96,10 @@ private theorem coefficient_le_log {n : ℕ} {κ : ℝ} (hn : 16 ≤ n) :
         simpa only [mul_one] using hconstant
     _ = _ := by ring
 
-private theorem coefficient_eventually_le_rpow {κ ε : ℝ} (hκ : 1 ≤ κ) (hε : 0 < ε) :
-    ∀ᶠ n : ℕ in atTop, coefficient κ n ≤ (n : ℝ) ^ ε := by
+/-- The complete component coefficient, including all logarithmic terms, is eventually at
+most any fixed positive real power. Its threshold is chosen before original matrix data. -/
+theorem costCoefficient_eventually_le_rpow {κ ε : ℝ} (hκ : 1 ≤ κ) (hε : 0 < ε) :
+    ∀ᶠ n : ℕ in atTop, costCoefficient κ n ≤ (n : ℝ) ^ ε := by
   have hc := logCoefficient_pos hκ
   have hlog : (fun n : ℕ => Real.log (n : ℝ)) =o[atTop] (fun n => (n : ℝ) ^ ε) :=
     (isLittleO_log_rpow_atTop hε).comp_tendsto tendsto_natCast_atTop_atTop
@@ -111,14 +128,14 @@ private theorem components_eventually_le {κ ε : ℝ} (hκ : 1 ≤ κ) (hε : 0
       ((12 * Nat.log 2 n + 36 + (PrimeSelection.timeBound n (window n) + 16) +
           FixedPrime.timeBound (m := level n) hn (groups n) p values mem : ℕ) : ℝ) ≤
         4 * (n : ℝ) ^ (3 - 1 / 648 + ε : ℝ) := by
-  filter_upwards [coefficient_eventually_le_rpow hκ hε,
+  filter_upwards [costCoefficient_eventually_le_rpow hκ hε,
     eventually_ge_atTop (2 ^ 1296 : ℕ)] with n hc hfast
   intro hn values mem p hv hp
   have hf := (blocks_pos_iff n).mpr hfast
   have hb := components_timeBound_le hf hκ values mem hv hp
-  change (_ : ℝ) ≤ coefficient κ n * ((n : ℝ) ^ 3 / groups n) at hb
+  change (_ : ℝ) ≤ costCoefficient κ n * ((n : ℝ) ^ 3 / groups n) at hb
   calc
-    _ ≤ coefficient κ n * ((n : ℝ) ^ 3 / groups n) := hb
+    _ ≤ costCoefficient κ n * ((n : ℝ) ^ 3 / groups n) := hb
     _ ≤ (n : ℝ) ^ ε * ((n : ℝ) ^ 3 / groups n) :=
       mul_le_mul_of_nonneg_right hc (by positivity)
     _ ≤ (n : ℝ) ^ ε * (4 * (n : ℝ) ^ (3 - 1 / 648 : ℝ)) :=
diff --git a/ComplexityTests/WordRAMCallableDyadicExecution.lean b/ComplexityTests/WordRAMCallableDyadicExecution.lean
new file mode 100644
index 0000000000..2bf22a6fe4
--- /dev/null
+++ b/ComplexityTests/WordRAMCallableDyadicExecution.lean
@@ -0,0 +1,105 @@
+/-
+Copyright (c) 2026 Erik Demaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine
+-/
+
+-- upstream: local-only (tests)
+
+import Complexity.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime.DyadicExecution
+import Mathlib.Data.List.GetD
+
+/-!
+# Actual selected-prime runs at the natural subcubic allowance
+
+The original zero, positive and negative constant inputs discharge all premises and run the
+existing real program from State.init. Prefix, charged halt, literal verdict, natural time and
+original-input frame use the same final state. These are kernel clients on large admitted
+geometry, not enormous interpreter fixtures or supplied executions.
+-/
+
+namespace ComplexityTests.WordRAMCallableDyadicExecution
+
+open Cslib.WordRAM Cslib.Matrix Cslib.Algorithms.ExactTriangle
+open Cslib.Algorithms.WordRAM.ExactTriangle
+open Cslib.Algorithms.WordRAM.ExactTriangle.CallableFixedPrime
+open ParameterChoice
+
+private def data (n : ℕ) (z : ℤ) : List ℤ := List.replicate (3 * (n * n)) z
+private def width (n : ℕ) : ℕ := 246659 * Nat.clog 2 (n + 2)
+private def words (n p : ℕ) (z : ℤ) : List ℕ :=
+  PreparationInput.input n (window n) (groups n) p (data n z)
+
+private theorem pair_lt {n : ℕ} (a b : Fin n) : pairIndex (a, b) < n * n := by
+  simpa [pairIndex, Nat.mul_comm, Nat.add_comm] using (finProdFinEquiv (a, b)).isLt
+
+private theorem triangle_iff {n : ℕ} (hn : 0 < n) (z : ℤ) :
+    HasZeroTriangle (fun _ _ : Fin n => z) (fun _ _ => z) (fun _ _ => z) ↔ z = 0 := by
+  constructor
+  · rintro ⟨a, b, c, h⟩
+    dsimp only [weightSum] at h
+    omega
+  · intro hz
+    exact ⟨⟨0, hn⟩, ⟨0, hn⟩, ⟨0, hn⟩, by simp [hz]⟩
+
+private def TimedConstant (z : ℤ) (answer : ℕ) : Prop :=
+  ∃ C : ℝ, 0 < C ∧ ∃ N : ℕ, 2 ^ 1296 ≤ N ∧ ∀ n ≥ N,
+    ∃ p y t,
+      IsSelectedPrime (fun _ _ : Fin n => z) (fun _ _ => z) (fun _ _ => z) (window n) p ∧
+      InputFits (width n) (words n p z) ∧
+      Runs (width n) (entryProgram.program Reg.found) (State.init (words n p z))
+        ⟨entryProgram.size, y⟩ t ∧
+      Executes (width n) (entryProgram.program Reg.found) (State.init (words n p z))
+        answer (t + 1) ∧
+      t + 1 ≤ dyadicTime n 1 ∧ (dyadicTime n 1 : ℝ) ≤ C * (n : ℝ) ^ (3 - 1 / 1296 : ℝ) ∧
+      y.regs Reg.found = answer ∧
+      ∀ q < workspaceBase n, y.mem q = (Data.init (words n p z) : Data 640).mem q
+
+-- Permit the existing concrete fast-threshold numeral during this original-input client.
+set_option exponentiation.threshold 1296 in
+private theorem timed_constant (z : ℤ) (hz : z.natAbs ≤ 1) :
+    TimedConstant z (if z = 0 then 1 else 0) := by
+  obtain ⟨C, hC, N, hN, hrun⟩ := exists_dyadic_runs_threshold (by decide : 1 ≤ (1 : ℕ))
+  refine ⟨C, hC, N, hN, ?_⟩
+  intro n hnN
+  have hn : 0 < n := (Nat.two_pow_pos 1296).trans_le (hN.trans hnN)
+  have hf := (blocks_pos_iff n).mpr (hN.trans hnN)
+  obtain ⟨p, hp⟩ := exists_isSelectedPrime (fun _ _ : Fin n => z)
+    (fun _ _ => z) (fun _ _ => z) (window n) (window_ge_sixteen hf)
+  have hab (a b : Fin n) : (data n z).getD (pairIndex (a, b)) 0 = z :=
+    List.getD_replicate z (by have h := pair_lt a b; omega)
+  have hbc (a b : Fin n) : (data n z).getD (n * n + pairIndex (a, b)) 0 = z :=
+    List.getD_replicate z (by have h := pair_lt a b; omega)
+  have hac (a b : Fin n) : (data n z).getD (2 * (n * n) + pairIndex (a, b)) 0 = z :=
+    List.getD_replicate z (by have h := pair_lt a b; omega)
+  have hp' : IsSelectedPrime
+      (fun a b : Fin n => (data n z).getD (pairIndex (a, b)) 0)
+      (fun a b => (data n z).getD (n * n + pairIndex (a, b)) 0)
+      (fun a b => (data n z).getD (2 * (n * n) + pairIndex (a, b)) 0) (window n) p := by
+    simpa only [hab, hbc, hac] using hp
+  have hlen : (data n z).length = 3 * (n * n) := by simp only [data, List.length_replicate]
+  have hv : ∀ v ∈ data n z, v.natAbs ≤ 1 := by
+    intro v hv
+    have heq : v = z := (List.mem_replicate.mp hv).2
+    simpa only [heq] using hz
+  obtain ⟨hi, y, t, hr, he, ht, htime, hbounded, hflag, hiff, hwitness, hframe⟩ :=
+    hrun n hnN 1 (data n z) p (width n) hlen hv (by simp) hp' (by exact le_rfl)
+  have hiff' : y.regs Reg.found = 1 ↔ z = 0 := by
+    have ht : HasZeroTriangle
+        (fun a b : Fin n => (data n z).getD (pairIndex (a, b)) 0)
+        (fun a b => (data n z).getD (n * n + pairIndex (a, b)) 0)
+        (fun a b => (data n z).getD (2 * (n * n) + pairIndex (a, b)) 0) ↔ z = 0 := by
+      simpa only [hab, hbc, hac] using triangle_iff hn z
+    exact hiff.trans ht
+  have hanswer : y.regs Reg.found = (if z = 0 then 1 else 0) := by
+    split_ifs with hz0
+    · exact hiff'.mpr hz0
+    · exact hflag.resolve_right (fun h => hz0 (hiff'.mp h))
+  exact ⟨p, y, t, hp, hi, hr, by simpa only [words, hanswer] using he,
+    ht, htime, hanswer, hframe⟩
+
+example : TimedConstant 0 1 := by simpa using timed_constant 0 (by decide)
+example : TimedConstant 1 0 := by simpa using timed_constant 1 (by decide)
+example : TimedConstant (-1) 0 := by simpa using timed_constant (-1) (by decide)
+
+end ComplexityTests.WordRAMCallableDyadicExecution