diff --git a/Complexity.lean b/Complexity.lean
index 3942e2e28b..81a55cc6d2 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -1513,6 +1513,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Arit
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Bounds
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Constructible
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.FunProp
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Lists
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.NatPolynomial
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Option
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/FunProp.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/FunProp.lean
new file mode 100644
index 0000000000..571b4c5bd5
--- /dev/null
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/FunProp.lean
@@ -0,0 +1,77 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Quantitative
+public import Complexity.Computability.Machines.Turing.MultiTape.Internal.OCombinators
+
+/-!
+# `fun_prop` rules for bounds up to constants
+
+`fun_prop` proves `Turing.MultiTapeTM.ComputableInO f encIn encOut T S` from rules in
+compositional form. The bounds of each rule's conclusion are a function of the bounds of its
+premises, so in a goal whose bounds `T` and `S` are metavariables, `fun_prop` assembles them from
+the parts of `f`. The usual pattern compares the assembled bounds with the intended ones in a
+single step:
+
+```
+refine .mono (by fun_prop) k (fun a => ?_) fun a => ?_
+```
+
+The rules cover constants, the identity, composition, pairs and their projections, case
+distinction on a computed Boolean, and `Option.isSome` and `Option.getD`. Other certificates
+become rules in the same compositional form, for example `fun x => F (g x)` from
+`Turing.MultiTapeTM.ComputableInO.comp'`.
+
+## Main results
+
+* `Turing.MultiTapeTM.ComputableInO.id'`, `.comp'`: the identity and composition, in the form
+  required by `fun_prop`.
+* `Turing.MultiTapeTM.ComputableInO.optionIsSome`, `.optionGetD`: option tests and defaults, with
+  the bounds of the option.
+-/
+
+@[expose] public section
+
+namespace Turing.MultiTapeTM.ComputableInO
+
+variable {α β γ : Type} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool}
+  {encOut : γ ↪ List Bool} {T S : α → ℕ}
+
+attribute [fun_prop] ComputableInO
+attribute [fun_prop] const prod fst' snd' ite
+
+/-- Copy an encoded value, within linear time and space. -/
+@[fun_prop]
+theorem id' : ComputableInO (fun b : β => b) encMid encMid (fun b => (encMid b).length)
+    fun b => (encMid b).length :=
+  of_eq fun _ => rfl
+
+/-- `Turing.MultiTapeTM.ComputableInO.comp` in the form required by `fun_prop`. -/
+@[fun_prop]
+theorem comp' {f : β → γ} {g : α → β} {T₁ S₁ : α → ℕ} {T₂ S₂ : β → ℕ}
+    (hf : ComputableInO f encMid encOut T₂ S₂) (hg : ComputableInO g encIn encMid T₁ S₁) :
+    ComputableInO (fun a => f (g a)) encIn encOut (fun a => T₁ a + T₂ (g a))
+      fun a => S₁ a + S₂ (g a) :=
+  hf.comp hg
+
+/-- Whether a computed option holds a value, within the bounds of the option. -/
+@[fun_prop]
+theorem optionIsSome {enc : β ↪ List Bool} {o : α → Option β}
+    (h : ComputableInO o encIn (encOption enc) T S) :
+    ComputableInO (fun a => (o a).isSome) encIn encBool T S :=
+  (ComputableInDegree.isSome enc).inO_one.comp_linear h
+
+/-- The value of a computed option, or a fixed default, within the bounds of the option. -/
+@[fun_prop]
+theorem optionGetD {enc : β ↪ List Bool} {o : α → Option β} (d : β)
+    (h : ComputableInO o encIn (encOption enc) T S) :
+    ComputableInO (fun a => (o a).getD d) encIn enc T S :=
+  (ComputableInDegree.optionGetD enc d).inO_one.comp_linear h
+
+end Turing.MultiTapeTM.ComputableInO
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/Pi.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/Pi.lean
index 351ae911aa..3c7e3ba90c 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/Pi.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/Pi.lean
@@ -8,7 +8,7 @@ module
 -- upstream: candidate
 
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Pi
-public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Quantitative
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.FunProp
 
 /-!
 # Parameterized resource bounds for finite tuples
@@ -35,8 +35,6 @@ cslib `crypto` branch at `5ff69ca93402e7c947208dc56396d6d86203ccd8`.
 
 @[expose] public section
 
-attribute [fun_prop] Turing.MultiTapeTM.ComputableInO
-
 namespace Turing.MultiTapeTM.ComputableInO
 
 variable {α Index Value : Type} {input : α ↪ List Bool} {enc : Value ↪ List Bool}
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/Sum.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/Sum.lean
index 5e817ee36c..df7f900a03 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/Sum.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/Sum.lean
@@ -8,7 +8,7 @@ module
 -- upstream: candidate
 
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Sum
-public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Quantitative
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.FunProp
 
 /-!
 # Linear resource bounds for tagged sum constructors
@@ -30,8 +30,6 @@ Uses Christian Reitwiessner's native degree/resource calculus (`ComputableInO.ap
 
 @[expose] public section
 
-attribute [fun_prop] Turing.MultiTapeTM.ComputableInO
-
 namespace Turing.MultiTapeTM.ComputableInO
 
 variable {α β : Type}
diff --git a/ComplexityTests/ComputableInOFunProp.lean b/ComplexityTests/ComputableInOFunProp.lean
new file mode 100644
index 0000000000..4ff2471eb6
--- /dev/null
+++ b/ComplexityTests/ComputableInOFunProp.lean
@@ -0,0 +1,75 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.FunProp
+
+/-!
+# `fun_prop` for bounds up to constants
+
+`fun_prop` assembles `Turing.MultiTapeTM.ComputableInO` certificates with composite bounds: the
+projections of nested pairs, a case distinction on `Option.isSome`, and `Option.getD`. One `mono`
+step then compares the assembled bounds with the intended ones.
+-/
+
+@[expose] public section
+
+open Turing.MultiTapeTM
+
+namespace ComplexityTests.ComputableInOFunProp
+
+variable {enc : ℕ ↪ List Bool}
+
+/-- The encoding of the test inputs. -/
+abbrev eIn : (ℕ × Option ℕ) × ℕ ↪ List Bool := encPair (encPair enc (encOption enc)) enc
+
+-- Projections of nested pairs keep the bounds of the projected pair.
+example : ComputableInO (fun p : (ℕ × Option ℕ) × ℕ => (p.2, p.1.1)) (eIn (enc := enc))
+    (encPair enc enc) (fun p => (eIn (enc := enc) p).length + (eIn (enc := enc) p).length)
+    fun p => (eIn (enc := enc) p).length + (eIn (enc := enc) p).length := by
+  fun_prop
+
+-- A default for a projected option keeps the bounds of the projection.
+example (d : ℕ) : ComputableInO (fun p : (ℕ × Option ℕ) × ℕ => p.1.2.getD d) (eIn (enc := enc))
+    enc (fun p => (eIn (enc := enc) p).length) fun p => (eIn (enc := enc) p).length := by
+  fun_prop
+
+-- A case distinction adds the bounds of the test and of the branch taken.
+example (d : ℕ) : ComputableInO
+    (fun p : (ℕ × Option ℕ) × ℕ => if p.1.2.isSome then (p.1.2.getD d, p.2) else (p.2, d))
+    (eIn (enc := enc)) (encPair enc enc)
+    (fun p => (eIn (enc := enc) p).length + if p.1.2.isSome then
+      (eIn (enc := enc) p).length + (eIn (enc := enc) p).length
+      else (eIn (enc := enc) p).length + (eIn (enc := enc) p).length)
+    fun p => (eIn (enc := enc) p).length + if p.1.2.isSome then
+      (eIn (enc := enc) p).length + (eIn (enc := enc) p).length
+      else (eIn (enc := enc) p).length + (eIn (enc := enc) p).length := by
+  fun_prop
+
+-- With unknown bounds, `fun_prop` assembles them, and one `mono` step reaches linear bounds.
+example (d : ℕ) : ComputableInO
+    (fun p : (ℕ × Option ℕ) × ℕ => if p.1.2.isSome then (p.1.2.getD d, p.2) else (p.2, d))
+    (eIn (enc := enc)) (encPair enc enc) (fun p => (eIn (enc := enc) p).length)
+    fun p => (eIn (enc := enc) p).length := by
+  refine .mono (by fun_prop) 3 (fun p => ?_) fun p => ?_ <;> split_ifs <;> omega
+
+/-- A certificate with a nonlinear bound, used through composition. -/
+theorem square_inO {g : ℕ → ℕ} (h : ComputableInO g enc enc
+    (fun n => (enc n).length * (enc n).length) fun n => (enc n).length) :
+    ComputableInO (fun p : (ℕ × Option ℕ) × ℕ => (g p.1.1, p.2)) (eIn (enc := enc))
+      (encPair enc enc) (fun p => ((eIn (enc := enc) p).length + 1) ^ 2)
+      fun p => (eIn (enc := enc) p).length := by
+  refine .mono (by fun_prop) 4 (fun p => ?_) fun p => ?_
+  all_goals
+    have h₁ : (enc p.1.1).length ≤ (eIn (enc := enc) p).length := by
+      simp only [eIn, length_encPair]; omega
+  · have := Nat.mul_le_mul h₁ h₁
+    nlinarith
+  · omega
+
+end ComplexityTests.ComputableInOFunProp