From 6a455d0b66f61fedbdeb160f95164b3908d042c8 Mon Sep 17 00:00:00 2001
From: Devon Tuma <dtumad@gmail.com>
Date: Wed, 5 Aug 2026 09:29:37 -0500
Subject: [PATCH 1/3] chore: update mathlib/cslib dependency

---
 lake-manifest.json | 4 ++--
 lakefile.toml      | 6 +++---
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/lake-manifest.json b/lake-manifest.json
index c7800442..140d6850 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "197a7be621263b84c67ca4f803f69205b36d06df",
+   "rev": "93aa05752a62ad3498e734d5b75fcbff965891ce",
    "name": "cslib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.32.0",
+   "inputRev": "v4.32.2",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4",
diff --git a/lakefile.toml b/lakefile.toml
index c4df044f..f5596e8e 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -28,16 +28,16 @@ weak.linter.allScriptsDocumented = false
 linter.mathlibStandardSet = true
 linter.style.longFile = 1500
 
-# Pinned to Lean v4.32.0 (matches `lean-toolchain`).
+# Pinned to Lean v4.32.2 (matches `lean-toolchain`).
 [[require]]
 name = "mathlib"
 scope = "leanprover-community"
-rev = "v4.32.0"
+rev = "v4.32.2"
 
 [[require]]
 name = "cslib"
 scope = "leanprover"
-rev = "v4.32.0"
+rev = "v4.32.2"
 
 [[lean_lib]]
 name = "PolyFun"

From 7f3235672f8a88a19df551ebb7f43af205e3ae95 Mon Sep 17 00:00:00 2001
From: Devon Tuma <dtumad@gmail.com>
Date: Wed, 5 Aug 2026 12:30:46 -0500
Subject: [PATCH 2/3] feat(dynamical): upstream flat-machine helpers from the
 VCVio polytime draft
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Adds the pieces VCVio's polytime draft (Verified-zkEVM/VCVio#500) carries
locally with `-- upstream candidate for DynComputation` comments, plus one
`FreeM` bound lemma they will need.

`DynComputation`:
* `ofStep` — build a returning computation from a raw one-step transition plus
  an initialization. Reducible, so `view` reads the supplied data back
  transparently; this is the primary constructor for a hand-built machine.
* `setInit` — replace the initialization while keeping the dynamics. Reducible,
  so computations sharing `toMachine` share every derived step map
  definitionally.

`DynComputation/Bounded`:
* `unroll_setInit`, `unroll_mapResult`, `unroll_wrap` and their `run_*`
  corollaries. The `setInit` case needs a fuel induction rather than `rfl`,
  because `view` does not unify automatically across the input-type change.

`PFunctor.Bound`:
* `isTotalRollBound_mapLens` — a lens relabels positions and reindexes
  directions, leaving the number of rolls along each branch untouched.

All additions; no existing declaration changes behaviour.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---
 PolyFun/PFunctor/Bound.lean                   | 16 +++-
 .../PFunctor/Dynamical/DynComputation.lean    | 56 ++++++++++++
 .../Dynamical/DynComputation/Bounded.lean     | 89 ++++++++++++++++++-
 3 files changed, 159 insertions(+), 2 deletions(-)

diff --git a/PolyFun/PFunctor/Bound.lean b/PolyFun/PFunctor/Bound.lean
index 2c5db7f9..0fd5c12a 100644
--- a/PolyFun/PFunctor/Bound.lean
+++ b/PolyFun/PFunctor/Bound.lean
@@ -31,7 +31,7 @@ witnesses the equivalence by `Iff.rfl`.
 
 @[expose] public section
 
-universe v w uA uB
+universe v w uA uB uA₂ uB₂
 
 namespace PFunctor.FreeM
 
@@ -240,4 +240,18 @@ lemma isTotalRollBound_seq {og : FreeM P (α → β)} {oa : FreeM P α}
     IsTotalRollBound (og <*> oa) (n₁ + n₂) := by
   refine isRollBound_seq (fun a b => a + b) ?_ ?_ h₁ h₂ <;> grind
 
+/-- Interface transport along a lens preserves total roll bounds. A lens relabels
+positions and reindexes directions, leaving the branching structure — and hence the
+number of rolls along each branch — untouched. -/
+lemma isTotalRollBound_mapLens {Q : PFunctor.{uA₂, uB₂}} (l : Lens P Q)
+    (oa : FreeM P α) {n : ℕ} (h : oa.IsTotalRollBound n) :
+    (oa.mapLens l).IsTotalRollBound n := by
+  induction oa generalizing n with
+  | pure x => simp
+  | lift_bind a cont ih =>
+      rw [isTotalRollBound_lift_bind_iff] at h
+      rw [FreeM.mapLens_lift_bind, FreeM.liftBind_eq,
+        isTotalRollBound_lift_bind_iff]
+      exact ⟨h.1, fun d => ih _ (h.2 _)⟩
+
 end PFunctor.FreeM
diff --git a/PolyFun/PFunctor/Dynamical/DynComputation.lean b/PolyFun/PFunctor/Dynamical/DynComputation.lean
index 1b9b515a..d558c102 100644
--- a/PolyFun/PFunctor/Dynamical/DynComputation.lean
+++ b/PolyFun/PFunctor/Dynamical/DynComputation.lean
@@ -170,6 +170,32 @@ def contramapInput {γ : Type uγ} (M : DynComputation.{u} p α β) (f : γ →
     (M : DynComputation.{u} p α β) (input : γ) :
     (M.contramapInput f).denote input = M.denote (f input) := rfl
 
+/-- Replace a returning computation's initialization map, possibly changing the
+input type, while keeping its dynamics untouched. Reducible so that the state
+type, one-step views, and behaviors of `M.setInit g` reduce to those of `M`:
+computations sharing `toMachine` share every derived step map definitionally. -/
+@[reducible] def setInit {γ : Type uγ} (M : DynComputation.{u} p α β)
+    (g : γ → M.State) : DynComputation.{u} p γ β :=
+  ⟨M.toMachine, g⟩
+
+@[simp] theorem setInit_State {γ : Type uγ} (M : DynComputation.{u} p α β)
+    (g : γ → M.State) : (M.setInit g).State = M.State := rfl
+
+@[simp] theorem setInit_init {γ : Type uγ} (M : DynComputation.{u} p α β)
+    (g : γ → M.State) (input : γ) : (M.setInit g).init input = g input := rfl
+
+@[simp] theorem setInit_view {γ : Type uγ} (M : DynComputation.{u} p α β)
+    (g : γ → M.State) (state : M.State) :
+    (M.setInit g).view state = M.view state := rfl
+
+@[simp] theorem setInit_denote {γ : Type uγ} (M : DynComputation.{u} p α β)
+    (g : γ → M.State) (input : γ) :
+    (M.setInit g).denote input = M.toDynSystem.behavior (g input) := rfl
+
+/-- Reindexing inputs is exactly precomposing the initialization map. -/
+theorem contramapInput_eq_setInit {γ : Type uγ} (M : DynComputation.{u} p α β)
+    (f : γ → α) : M.contramapInput f = M.setInit (M.init ∘ f) := rfl
+
 private def mapResultLift {γ : Type uγ} (f : β → γ) :
     Lens.{max uβ uA, uB, max uγ uA, uB}
       (C.{uβ, uB} β + p) (C.{uγ, uB} γ + p) :=
@@ -660,6 +686,36 @@ theorem seqComp_ofFn_obsEq {γ : Type uγ} (M : DynComputation.{u} p α β)
   funext value
   exact denote_ofFn f value
 
+/-! ## Realizations from a raw step function -/
+
+/-- Realize a returning computation from a one-step transition — returning either
+a value or a visible query with an explicit state-valued continuation — together
+with an initialization.
+
+This is the primary constructor for a hand-built machine: the supplied step
+function is exactly what `view` reads back, so no repackaging is visible to the
+caller. Reducible, so the state type and one-step views of a computation built
+this way are transparently those of the supplied data. -/
+@[reducible] def ofStep {S : Type u} (stepFn : S → β ⊕ p.Obj S) (init : α → S) :
+    DynComputation.{u} p α β where
+  State := S
+  toDynSystem :=
+    (fun state => (Resumption.pack (β := β) (stepFn state)).1) ⇆
+      fun state => (Resumption.pack (β := β) (stepFn state)).2
+  init := init
+
+@[simp] theorem ofStep_State {S : Type u} (stepFn : S → β ⊕ p.Obj S)
+    (init : α → S) : (ofStep (p := p) stepFn init).State = S := rfl
+
+@[simp] theorem ofStep_init {S : Type u} (stepFn : S → β ⊕ p.Obj S)
+    (init : α → S) (input : α) :
+    (ofStep (p := p) stepFn init).init input = init input := rfl
+
+@[simp] theorem view_ofStep {S : Type u} (stepFn : S → β ⊕ p.Obj S)
+    (init : α → S) (state : S) :
+    (ofStep (p := p) stepFn init).view state = stepFn state :=
+  Resumption.unpack_pack (stepFn state)
+
 /-! ## Resumption realizations -/
 
 /-- Realize a family of resumptions directly, using the resumption itself as
diff --git a/PolyFun/PFunctor/Dynamical/DynComputation/Bounded.lean b/PolyFun/PFunctor/Dynamical/DynComputation/Bounded.lean
index 5a3e1abf..5f05c81e 100644
--- a/PolyFun/PFunctor/Dynamical/DynComputation/Bounded.lean
+++ b/PolyFun/PFunctor/Dynamical/DynComputation/Bounded.lean
@@ -29,7 +29,7 @@ bridges inherit their existing `Classical.choice` footprint.
 
 @[expose] public section
 
-universe u v uA uB uα uβ uγ
+universe u v uA uB uA₂ uB₂ uα uβ uγ
 
 namespace PFunctor
 
@@ -127,6 +127,93 @@ theorem isTotalRollBound_unroll (M : DynComputation.{u} p α β)
   rw [unroll_eq_truncate]
   exact Resumption.isTotalRollBound_truncate k (M.toDynSystem.behavior state)
 
+/-! ## Transport of bounded unrolling
+
+Bounded unrolling commutes with each of the three reindexings of a returning
+computation: replacing the initialization leaves it untouched, mapping the
+returned value maps the optional result, and interface transport along a lens
+transports the resulting syntax along the same lens.
+
+Each proof is a fuel induction rather than a definitional equality, because
+`unroll` is defined by cases on the computation's one-step view and so does not
+reduce until that view is exposed.
+-/
+
+/-- Replacing the initialization map leaves bounded unrolling from a hidden state
+unchanged: the two computations share `toMachine`, hence share their views. -/
+theorem unroll_setInit {γ : Type uγ} (M : DynComputation.{u} p α β)
+    (g : γ → M.State) (k : ℕ) (state : M.State) :
+    (M.setInit g).unroll k state = M.unroll k state := by
+  induction k generalizing state with
+  | zero =>
+      rw [unroll_zero (M.setInit g) state, unroll_zero M state, setInit_view]
+      cases hview : M.view state with
+      | inl value => rfl
+      | inr query => rfl
+  | succ k ih =>
+      rw [unroll_succ (M.setInit g) k state, unroll_succ M k state, setInit_view]
+      cases hview : M.view state with
+      | inl value => rfl
+      | inr query =>
+          rcases query with ⟨position, next⟩
+          exact congrArg (FreeM.liftBind position)
+            (funext fun direction => ih (next direction))
+
+theorem run_setInit {γ : Type uγ} (M : DynComputation.{u} p α β)
+    (g : γ → M.State) (k : ℕ) (input : γ) :
+    (M.setInit g).run k input = M.unroll k (g input) :=
+  M.unroll_setInit g k (g input)
+
+/-- Mapping returned values maps the optional result of a bounded unrolling. -/
+@[simp] theorem unroll_mapResult {γ : Type uγ} (M : DynComputation.{u} p α β)
+    (f : β → γ) (k : ℕ) (state : M.State) :
+    (M.mapResult f).unroll k state =
+      FreeM.map (Option.map f) (M.unroll k state) := by
+  induction k generalizing state with
+  | zero =>
+      rw [unroll_zero (M.mapResult f) state, unroll_zero M state, mapResult_view]
+      cases hview : M.view state with
+      | inl value => rfl
+      | inr query => rfl
+  | succ k ih =>
+      rw [unroll_succ (M.mapResult f) k state, unroll_succ M k state, mapResult_view]
+      cases hview : M.view state with
+      | inl value => rfl
+      | inr query =>
+          rcases query with ⟨position, next⟩
+          exact congrArg (FreeM.liftBind position)
+            (funext fun direction => ih (next direction))
+
+@[simp] theorem run_mapResult {γ : Type uγ} (M : DynComputation.{u} p α β)
+    (f : β → γ) (k : ℕ) (input : α) :
+    (M.mapResult f).run k input = FreeM.map (Option.map f) (M.run k input) :=
+  M.unroll_mapResult f k (M.init input)
+
+/-- Interface transport along a lens transports bounded unrolling along the same
+lens. -/
+@[simp] theorem unroll_wrap {q : PFunctor.{uA₂, uB₂}} (M : DynComputation.{u} p α β)
+    (lens : Lens p q) (k : ℕ) (state : M.State) :
+    (M.wrap lens).unroll k state = (M.unroll k state).mapLens lens := by
+  induction k generalizing state with
+  | zero =>
+      rw [unroll_zero (M.wrap lens) state, unroll_zero M state, wrap_view]
+      cases hview : M.view state with
+      | inl value => rfl
+      | inr query => rfl
+  | succ k ih =>
+      rw [unroll_succ (M.wrap lens) k state, unroll_succ M k state, wrap_view]
+      cases hview : M.view state with
+      | inl value => rfl
+      | inr query =>
+          rcases query with ⟨position, next⟩
+          exact congrArg (FreeM.liftBind (lens.toFunA position))
+            (funext fun direction => ih (next (lens.toFunB position direction)))
+
+@[simp] theorem run_wrap {q : PFunctor.{uA₂, uB₂}} (M : DynComputation.{u} p α β)
+    (lens : Lens p q) (k : ℕ) (input : α) :
+    (M.wrap lens).run k input = (M.run k input).mapLens lens :=
+  M.unroll_wrap lens k (M.init input)
+
 /-! ## Resolution within a uniform query budget -/
 
 /-- Every answer branch from `state` returns within `k` visible queries. -/

From 0696ba77c749ad7567cc0607bcecb97e0810f15a Mon Sep 17 00:00:00 2001
From: Devon Tuma <dtumad@gmail.com>
Date: Wed, 5 Aug 2026 12:31:04 -0500
Subject: [PATCH 3/3] feat(realizability): machine realizability over a
 distributive step class
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

New `PolyFun/Realizability/` subtree. Answers "can this `FreeM` program be run
by a machine whose transition functions satisfy a given predicate?", generically
in the predicate.

`StepClass` is a wide subcategory of `Type u` presented pointwise: a
representation structure `Str` on types plus an admissibility predicate `Hom` on
functions, closed under identities and composition. With the `HasProd`, `HasSum`
and `IsDistributive` mixins it is exactly a distributive category (Cockett 1993;
Carboni–Lack–Walters 1993) presented concretely over `Type`. `HasOption` records
that the flattened transition is partial.

`Machine.lean` re-presents `DynComputation`'s dynamics as first-order maps a
predicate on functions can constrain: `head` (definitionally the position map of
the machine's lens) and the partial `update?`. `updateFlat`, `output`, `expose`
and `stepD` are derived, for a machine-facing cost model.
`ofStep_step_eq_of_flat_eq` shows the presentation is faithful.

`Basic.lean` defines `Boundary`, `Realization`, `IsRealizableBy` and
`IsRealizableWithin`. `Closure.lean` proves closure under `ofFn`, input
precomposition, result postcomposition, `seqComp` (i.e. `FreeM.bind`, with
budgets adding), interface transport along an admissible lens, and refinement of
the ambient class.

`Instances.lean` gives four classes: unconstrained (with a non-vacuity theorem),
finite (finite-state realizability), computable (Mathlib `Primcodable` /
`Computable`), and `WordClass` — the bridge from a monomorphic class of word
functions, which is how external complexity libraries present themselves.

Design note: `update?` is partial rather than total because the total convention
does not compose across a state coproduct with a handoff. On a mismatched answer
tag the composite stays in the left summand while the second phase alone would
stay at its own initial state, and reconciling those junk values would require
the class to contain a decidable equality test on interface positions — not
derivable from products, coproducts and distributivity. With `none` both agree
and `update?_seqComp_inl` holds unconditionally in the answer index.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---
 AGENTS.md                               |  12 +
 PolyFun.lean                            |   5 +
 PolyFun/Realizability/Basic.lean        | 313 ++++++++++++++
 PolyFun/Realizability/Closure.lean      | 378 +++++++++++++++++
 PolyFun/Realizability/Instances.lean    | 512 +++++++++++++++++++++++
 PolyFun/Realizability/Machine.lean      | 535 ++++++++++++++++++++++++
 PolyFun/Realizability/StepClass.lean    | 355 ++++++++++++++++
 PolyFunTest/Realizability/Examples.lean | 237 +++++++++++
 REFERENCES.md                           | 236 ++++++++++-
 docs/wiki/README.md                     |   4 +
 docs/wiki/realizability.md              | 298 +++++++++++++
 docs/wiki/repo-map.md                   |  10 +
 12 files changed, 2892 insertions(+), 3 deletions(-)
 create mode 100644 PolyFun/Realizability/Basic.lean
 create mode 100644 PolyFun/Realizability/Closure.lean
 create mode 100644 PolyFun/Realizability/Instances.lean
 create mode 100644 PolyFun/Realizability/Machine.lean
 create mode 100644 PolyFun/Realizability/StepClass.lean
 create mode 100644 PolyFunTest/Realizability/Examples.lean
 create mode 100644 docs/wiki/realizability.md

diff --git a/AGENTS.md b/AGENTS.md
index fd4b2b3b..5b2a195d 100644
--- a/AGENTS.md
+++ b/AGENTS.md
@@ -76,6 +76,16 @@ and depend on this library.
     (interfaces, par, wire, plug), corruption models, environment
     actions, leakage. *Generic only* — security-flavored UC layers
     (computational equivalence, asymptotic security) live in VCVio.
+- `PolyFun/Realizability/`: step classes (`StepClass` — a wide subcategory of
+  `Type u` presented by a representation structure on types and an
+  admissibility predicate on functions; with products, sums and distributivity
+  it is exactly a distributive category) and realizability of `FreeM` program
+  families by `DynComputation` machines whose first-order step maps are
+  admissible. Closed under `ofFn`, input precomposition, result
+  postcomposition, `bind`, interface transport, and class refinement.
+  Instances: unconstrained, finite-state, Mathlib-`Computable`, and a bridge
+  from any class of word functions. *Generic only* — cost measures and
+  concrete complexity classes live downstream.
 - `PolyFun/Control/`: monad and comonad infrastructure transitively
   required by the above (coalgebra, comonad, free / freecont monad
   algebra, monad iter / hom, lawful re-exports).
@@ -228,6 +238,8 @@ too specific or too changeable to keep at the repo root.
 - [`docs/wiki/itree.md`](docs/wiki/itree.md): interaction trees layer.
 - [`docs/wiki/interaction.md`](docs/wiki/interaction.md): generic interaction
   framework (`TypeTree`, two-party, multiparty, concurrent, UC).
+- [`docs/wiki/realizability.md`](docs/wiki/realizability.md): step classes and
+  realizability of free programs by admissible state machines.
 - [`docs/wiki/notation.md`](docs/wiki/notation.md): notation reference (UC
   composition operators).
 - [`docs/wiki/gotchas.md`](docs/wiki/gotchas.md): recurring traps and
diff --git a/PolyFun.lean b/PolyFun.lean
index 55153ac0..21000fc8 100644
--- a/PolyFun.lean
+++ b/PolyFun.lean
@@ -223,3 +223,8 @@ public import PolyFun.PFunctor.SubstMonoid.Extension
 public import PolyFun.PFunctor.Trace
 public import PolyFun.PFunctor.Wiring
 public import PolyFun.PFunctor.Wiring.Parallel
+public import PolyFun.Realizability.Basic
+public import PolyFun.Realizability.Closure
+public import PolyFun.Realizability.Instances
+public import PolyFun.Realizability.Machine
+public import PolyFun.Realizability.StepClass
diff --git a/PolyFun/Realizability/Basic.lean b/PolyFun/Realizability/Basic.lean
new file mode 100644
index 00000000..6324ed95
--- /dev/null
+++ b/PolyFun/Realizability/Basic.lean
@@ -0,0 +1,313 @@
+/-
+Copyright (c) 2026 PolyFun Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Devon Tuma
+-/
+module
+
+public import PolyFun.Realizability.Machine
+public import PolyFun.Realizability.StepClass
+
+/-!
+# Realizability of free programs by admissible state machines
+
+A well-founded program family `program : α → FreeM p β` says *what* interaction
+to perform. A `DynComputation p α β` says *how* a machine performs it, and
+`DynComputation.Implements` says the two agree. This module adds the missing
+third ingredient: a constraint on the machine's transition functions.
+
+`IsRealizableBy C bd program` holds when some `C`-admissible machine implements
+`program`, where `C` is a `StepClass` and admissibility is asserted of the three
+first-order step maps `init`, `head`, and `update?` from
+`PolyFun.Realizability.Machine`. `IsRealizableWithin C bd program k` additionally
+demands that every branch resolve within `k` visible queries.
+
+Instantiating `C` recovers a spectrum of concrete notions from one definition:
+the trivial class gives back plain implementability, a finiteness class gives
+finite-state realizability, a computability class gives machines with computable
+transitions, and a resource-bounded class gives the polynomial-time
+adversary model used in cryptography.
+
+## The boundary is a parameter, never an existential
+
+`Boundary` collects the representations of the input type, the result type, and
+the interface. It is always a *parameter* of a realizability statement. A
+statement of the form `∃ bd, IsRealizableBy C bd program` is vacuous, because a
+representation is only required to be admissible, not canonical: an adversarially
+chosen encoding can precompute across the boundary. Only the machine's own state
+representation is chosen by the realization, and that choice is harmless — it is
+exactly the freedom to pick a state layout.
+
+## Universe discipline
+
+`StepClass.Str` speaks about types in a single universe, so this layer is stated
+at `p : PFunctor.{u, u}` with `α β : Type u` and hence `State : Type u`. Then
+`p.A`, `p.Idx`, `β ⊕ p.A`, and `State × p.Idx` all live in `Type u`. The
+underlying `DynComputation` API remains fully universe-polymorphic; only the
+realizability predicates are pinned.
+
+## Provenance
+
+This is a `C`-relative *realization* condition in the sense of classical
+(co)algebraic realization theory (Arbib–Manes 1974; Adámek–Milius–Moss–Sousa
+2013) and of finite-state realizability in reactive synthesis (Pnueli–Rosner
+1989), transported to the free-monad-over-a-polynomial-functor setting of
+Libkind–Spivak 2025 and Aberlé 2026, with the resource bound imposed as an
+admissibility predicate on the structure maps rather than as a Blum-style
+measure on runs (Blum 1967).
+
+Two identifications make the shape of the definition inevitable. A `p`-coalgebra
+on `S` *is* a way of running every `FreeM p` program in `S` (Uustalu 2015:
+stateful runners are comodels, hence coalgebras), so a realization has nowhere
+else to live. And the known special case at the class "given by a finite `FreeM`
+term" is the alternating `νX.μY.` representation of stream processors
+(Ghani–Hancock–Pattinson 2009).
+
+The word *realization* rather than *implementation* is deliberate: Aberlé uses
+"implementation" for the free-monad Kleisli morphism, that is, for the program
+side. See `REFERENCES.md`.
+-/
+
+@[expose] public section
+
+universe u v v₂
+
+namespace PFunctor
+
+namespace DynSystem.DynComputation
+
+variable {p : PFunctor.{u, u}} {α β : Type u}
+
+/-! ## The boundary of a realizability statement -/
+
+/-- The pinned representations at the boundary of a realizability statement: the
+input type, the returned-value type, and the interface's query positions and
+index space.
+
+The positions and the index space are supplied independently — nothing derives
+one from the other, since a class need not represent dependent sums. -/
+structure Boundary (C : StepClass.{u, v}) (p : PFunctor.{u, u}) (α β : Type u) :
+    Type v where
+  /-- Representation of the input type. -/
+  input : C.Str α
+  /-- Representation of the returned-value type. -/
+  out : C.Str β
+  /-- Representation of the interface's query positions. -/
+  pos : C.Str p.A
+  /-- Representation of the interface's index space `Idx p = Σ a, p.B a`. -/
+  idx : C.Str p.Idx
+
+namespace Boundary
+
+variable {C : StepClass.{u, v}}
+
+/-- The representation of a machine's one-step readout `β ⊕ p.A`, assembled from
+the result and position representations. -/
+def head [S : C.HasSum] (bd : Boundary C p α β) : C.Str (β ⊕ p.A) :=
+  S.sum bd.out bd.pos
+
+/-- The representation of the flattened transition's domain: a machine state
+paired with the interface's index space. -/
+def stateIdx [P : C.HasProd] (bd : Boundary C p α β) {S : Type u}
+    (state : C.Str S) : C.Str (S × p.Idx) :=
+  P.prod state bd.idx
+
+/-- Replace the input representation of a boundary, keeping the result and
+interface representations. -/
+def withInput {γ : Type u} (bd : Boundary C p α β) (inputRep : C.Str γ) :
+    Boundary C p γ β :=
+  ⟨inputRep, bd.out, bd.pos, bd.idx⟩
+
+/-- Replace the result representation of a boundary, keeping the input and
+interface representations. -/
+def withOut {γ : Type u} (bd : Boundary C p α β) (outRep : C.Str γ) :
+    Boundary C p α γ :=
+  ⟨bd.input, outRep, bd.pos, bd.idx⟩
+
+@[simp] theorem withInput_input {γ : Type u} (bd : Boundary C p α β)
+    (inputRep : C.Str γ) : (bd.withInput inputRep).input = inputRep := rfl
+
+@[simp] theorem withOut_out {γ : Type u} (bd : Boundary C p α β)
+    (outRep : C.Str γ) : (bd.withOut outRep).out = outRep := rfl
+
+@[simp] theorem withInput_head [C.HasSum] {γ : Type u} (bd : Boundary C p α β)
+    (inputRep : C.Str γ) : (bd.withInput inputRep).head = bd.head := rfl
+
+@[simp] theorem withOut_input {γ : Type u} (bd : Boundary C p α β)
+    (outRep : C.Str γ) : (bd.withOut outRep).input = bd.input := rfl
+
+/-- The middle boundary of a sequential composition: the second phase reads the
+first's results and shares its interface.
+
+Derived rather than constrained. Representations are *data*, so a `Prop`-valued
+equality between two boundaries would force `subst` transport at every use site;
+deriving the middle boundary makes every compatibility fact hold by `rfl`. The
+composite boundary of a sequential composition is then simply
+`bd.withOut outRep`. -/
+def mid {γ : Type u} (bd : Boundary C p α β) (outRep : C.Str γ) :
+    Boundary C p β γ :=
+  (bd.withOut outRep).withInput bd.out
+
+@[simp] theorem mid_input {γ : Type u} (bd : Boundary C p α β)
+    (outRep : C.Str γ) : (bd.mid outRep).input = bd.out := rfl
+
+@[simp] theorem mid_out {γ : Type u} (bd : Boundary C p α β)
+    (outRep : C.Str γ) : (bd.mid outRep).out = outRep := rfl
+
+@[simp] theorem mid_pos {γ : Type u} (bd : Boundary C p α β)
+    (outRep : C.Str γ) : (bd.mid outRep).pos = bd.pos := rfl
+
+@[simp] theorem mid_idx {γ : Type u} (bd : Boundary C p α β)
+    (outRep : C.Str γ) : (bd.mid outRep).idx = bd.idx := rfl
+
+/-- Two boundaries compose when the second reads the first's results and both
+describe the same interface. A convenience wrapper over `mid`, for use sites that
+already have both boundaries in hand. -/
+structure Composable {γ : Type u} (bd₁ : Boundary C p α β)
+    (bd₂ : Boundary C p β γ) : Prop where
+  /-- The second phase reads the first's results. -/
+  input_eq : bd₂.input = bd₁.out
+  /-- Both phases describe the same query positions. -/
+  pos_eq : bd₂.pos = bd₁.pos
+  /-- Both phases describe the same index space. -/
+  idx_eq : bd₂.idx = bd₁.idx
+
+theorem eq_mid_of_composable {γ : Type u} {bd₁ : Boundary C p α β}
+    {bd₂ : Boundary C p β γ} (h : bd₁.Composable bd₂) :
+    bd₂ = bd₁.mid bd₂.out := by
+  obtain ⟨input, out, pos, idx⟩ := bd₂
+  obtain ⟨hinput, hpos, hidx⟩ := h
+  subst hinput
+  subst hpos
+  subst hidx
+  rfl
+
+/-- Replace the interface representations of a boundary, keeping the input and
+result representations. This is the target boundary of an interface transport. -/
+def withInterface (bd : Boundary C p α β) {q : PFunctor.{u, u}}
+    (posRep : C.Str q.A) (idxRep : C.Str q.Idx) : Boundary C q α β :=
+  ⟨bd.input, bd.out, posRep, idxRep⟩
+
+@[simp] theorem withInterface_input (bd : Boundary C p α β)
+    {q : PFunctor.{u, u}} (posRep : C.Str q.A) (idxRep : C.Str q.Idx) :
+    (bd.withInterface posRep idxRep).input = bd.input := rfl
+
+@[simp] theorem withInterface_out (bd : Boundary C p α β)
+    {q : PFunctor.{u, u}} (posRep : C.Str q.A) (idxRep : C.Str q.Idx) :
+    (bd.withInterface posRep idxRep).out = bd.out := rfl
+
+@[simp] theorem withInterface_pos (bd : Boundary C p α β)
+    {q : PFunctor.{u, u}} (posRep : C.Str q.A) (idxRep : C.Str q.Idx) :
+    (bd.withInterface posRep idxRep).pos = posRep := rfl
+
+@[simp] theorem withInterface_idx (bd : Boundary C p α β)
+    {q : PFunctor.{u, u}} (posRep : C.Str q.A) (idxRep : C.Str q.Idx) :
+    (bd.withInterface posRep idxRep).idx = idxRep := rfl
+
+/-- Translate a boundary along a refinement of step classes. -/
+def mapRefines {D : StepClass.{u, v₂}} [C.HasProd] [C.HasSum] [C.HasOption]
+    [D.HasProd] [D.HasSum] [D.HasOption] (Ref : C.Refines D)
+    (bd : Boundary C p α β) : Boundary D p α β :=
+  ⟨Ref.str bd.input, Ref.str bd.out, Ref.str bd.pos, Ref.str bd.idx⟩
+
+end Boundary
+
+/-! ## Admissible realizations -/
+
+/-- A `C`-admissible realization of an interface-`p` computation with inputs `α`
+and results `β`.
+
+The data is a returning dynamical computation together with a representation of
+its hidden state — chosen freely by the realization — and proofs that its three
+first-order step maps are `C`-morphisms:
+
+* `init : α → State` starts the machine. Constraining it is what forbids
+  smuggling precomputed advice into the initial state.
+* `head : State → β ⊕ p.A` reads off a returned value or an exposed query.
+* `update? : State × p.Idx → Option State` consumes a tagged answer, partially.
+
+By `ofStep_step_eq_of_flat_eq` those three maps determine the machine, so this is
+a constraint on the machine itself rather than on a lossy projection of it.
+
+Nothing here constrains the machine's *behaviour*: a realization is admissible
+machinery, and agreement with a program is the separate `Implements` predicate.
+The two are combined by `IsRealizableBy`. -/
+structure Realization (C : StepClass.{u, v}) [C.HasProd] [C.HasSum] [C.HasOption]
+    [DecidableEq p.A] (bd : Boundary C p α β) where
+  /-- The underlying machine. -/
+  machine : DynComputation.{u} p α β
+  /-- The chosen representation of the machine's hidden state. -/
+  state : C.Str machine.State
+  /-- Initialization is admissible. -/
+  init_mem : C.Hom bd.input state machine.init
+  /-- The one-step readout is admissible. -/
+  head_mem : C.Hom state bd.head machine.head
+  /-- The partial flattened transition is admissible. -/
+  update_mem : C.Hom (bd.stateIdx state) (StepClass.HasOption.option state)
+    machine.update?
+
+/-! ## The realizability predicates -/
+
+/-- `program` is `C`-realizable: some `C`-admissible machine implements it.
+
+Resource bounds are deliberately not part of this predicate; see
+`IsRealizableWithin` for the bounded form. -/
+def IsRealizableBy (C : StepClass.{u, v}) [C.HasProd] [C.HasSum] [C.HasOption]
+    [DecidableEq p.A] (bd : Boundary C p α β) (program : α → FreeM p β) : Prop :=
+  ∃ R : Realization C bd, R.machine.Implements program
+
+/-- `program` is `C`-realizable within the uniform query budget `k`: some
+`C`-admissible machine implements it and resolves every answer branch within `k`
+visible queries. -/
+def IsRealizableWithin (C : StepClass.{u, v}) [C.HasProd] [C.HasSum] [C.HasOption]
+    [DecidableEq p.A] (bd : Boundary C p α β) (program : α → FreeM p β)
+    (k : ℕ) : Prop :=
+  ∃ R : Realization C bd, R.machine.ImplementsWithin program k
+
+section Basic
+
+variable {C : StepClass.{u, v}} [C.HasProd] [C.HasSum] [C.HasOption]
+  [DecidableEq p.A] {bd : Boundary C p α β} {program : α → FreeM p β}
+
+/-- A bounded realization is in particular a realization. -/
+theorem IsRealizableWithin.isRealizableBy {k : ℕ}
+    (h : IsRealizableWithin C bd program k) : IsRealizableBy C bd program := by
+  obtain ⟨R, hR⟩ := h
+  exact ⟨R, ((implementsWithin_iff_implements_and_bound R.machine program k).mp hR).1⟩
+
+/-- A bounded realization certifies that the program itself fits the budget: the
+resource bound is a property of the syntax, extracted from the machine. -/
+theorem IsRealizableWithin.isTotalRollBound {k : ℕ}
+    (h : IsRealizableWithin C bd program k) (input : α) :
+    (program input).IsTotalRollBound k := by
+  obtain ⟨R, hR⟩ := h
+  exact ((implementsWithin_iff_implements_and_bound R.machine program k).mp hR).2 input
+
+/-- Bounded realizability is monotone in the query budget. -/
+theorem IsRealizableWithin.mono {j k : ℕ}
+    (h : IsRealizableWithin C bd program j) (hjk : j ≤ k) :
+    IsRealizableWithin C bd program k := by
+  obtain ⟨R, hR⟩ := h
+  exact ⟨R, hR.mono hjk⟩
+
+/-- Realizability only depends on the program family through its values. -/
+theorem IsRealizableBy.congr {program' : α → FreeM p β}
+    (h : IsRealizableBy C bd program) (hprog : ∀ input, program input = program' input) :
+    IsRealizableBy C bd program' := by
+  obtain ⟨R, hR⟩ := h
+  exact ⟨R, fun input => (hprog input) ▸ hR input⟩
+
+/-- Bounded realizability only depends on the program family through its
+values. -/
+theorem IsRealizableWithin.congr {program' : α → FreeM p β} {k : ℕ}
+    (h : IsRealizableWithin C bd program k)
+    (hprog : ∀ input, program input = program' input) :
+    IsRealizableWithin C bd program' k := by
+  obtain ⟨R, hR⟩ := h
+  exact ⟨R, fun input => (hprog input) ▸ hR input⟩
+
+end Basic
+
+end DynSystem.DynComputation
+
+end PFunctor
diff --git a/PolyFun/Realizability/Closure.lean b/PolyFun/Realizability/Closure.lean
new file mode 100644
index 00000000..1b7b09f9
--- /dev/null
+++ b/PolyFun/Realizability/Closure.lean
@@ -0,0 +1,378 @@
+/-
+Copyright (c) 2026 PolyFun Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Devon Tuma
+-/
+module
+
+public import PolyFun.Realizability.Basic
+
+/-!
+# Closure properties of admissible realizability
+
+Realizability is closed under the operations that leave a machine's dynamics
+intact or reindex them by an admissible map, and it transports along refinements
+of the ambient step class. Each theorem asks of the class exactly the structure
+its construction consumes:
+
+* `isRealizableBy_ofFn` — an immediately returning program, realized by the
+  one-step machine whose states are its own results. Needs the returning map to
+  be admissible.
+* `IsRealizableBy.precomp` / `IsRealizableWithin.precomp` — input
+  precomposition, realized by `setInit`. The machine, its state representation,
+  and both of its remaining step maps are untouched, so only the initialization
+  obligation changes.
+* `IsRealizableBy.mapResult` / `IsRealizableWithin.mapResult` — postcomposition
+  on results, realized by `mapResult`. The readout gains a `Sum.map` and the
+  transition is unchanged.
+* `IsRealizableBy.seqComp` / `IsRealizableWithin.seqComp` — **closure under
+  `FreeM.bind`**, realized by `seqComp`. The state is the coproduct of the two
+  phases' states, and budgets add. Needs `IsDistributive`.
+* `IsRealizableBy.wrap` / `IsRealizableWithin.wrap` — interface transport along a
+  lens, realized by `wrap`. Needs the lens to be `Lens.IsAdmissible`.
+* `IsRealizableBy.mono` / `IsRealizableWithin.mono'` — transport along a
+  `StepClass.Refines`.
+
+Budget monotonicity and the bridge from the bounded to the unbounded predicate
+live in `PolyFun.Realizability.Basic`.
+
+## Where the structure is spent
+
+Distributivity is consumed in exactly one place, and only twice: the composite
+`update?` of a sequential composition splits on the state summand, and then on the
+first phase's readout, each time retaining the answer index. The *readout* side of
+the same composition needs no products at all — only `comp_mem`, `elim_mem`, and
+`inr_mem`.
+
+None of this needs a decidable-equality test on interface positions, and that is a
+consequence of `update?` being partial: each phase's own transition already returns
+`none` on an answer it is not waiting for, so the composite inherits the tag test
+rather than performing it. With the total `updateFlat` no uniform equation holds and
+an equality-test axiom would be forced; see `PolyFun.Realizability.Machine`.
+
+Interface transport is the one place a tag test does surface, because pulling an
+answer back along a lens must compare it against the position the lens exposes.
+That is why `wrap` takes a `Lens.IsAdmissible` hypothesis while `seqComp` takes
+none.
+-/
+
+@[expose] public section
+
+universe u v v₂
+
+namespace PFunctor
+
+namespace DynSystem.DynComputation
+
+variable {p : PFunctor.{u, u}} {α β : Type u}
+  {C : StepClass.{u, v}} [P : C.HasProd] [S : C.HasSum] [O : C.HasOption]
+  [DecidableEq p.A] {bd : Boundary C p α β} {program : α → FreeM p β}
+
+/-! ## Immediately returning programs -/
+
+/-- An immediately returning program is realizable exactly when its returning map
+is admissible. The realizing machine takes the result type itself as its state:
+`head` is the left injection and the flattened transition is the first
+projection. -/
+theorem isRealizableBy_ofFn {f : α → β} (hf : C.Hom bd.input bd.out f) :
+    IsRealizableBy C bd (fun input => FreeM.pure (f input)) := by
+  refine ⟨⟨ofFn (p := p) f, bd.out, hf, StepClass.HasSum.inl_mem bd.out bd.pos, ?_⟩,
+    ?_⟩
+  · refine (StepClass.HasOption.none_mem (bd.stateIdx bd.out) bd.out).congr ?_
+    intro step
+    exact (update?_of_view_return (ofFn (p := p) f) (view_ofFn f step.1) step.2).symm
+  · intro input
+    rw [denote_ofFn]
+    simp
+
+/-- A constant program is realizable whenever the constant is: the special case
+of `isRealizableBy_ofFn` at a constant returning map. -/
+theorem isRealizableBy_pure {value : β}
+    (hvalue : C.Hom bd.input bd.out fun _ : α => value) :
+    IsRealizableBy C bd fun _ : α => (FreeM.pure value : FreeM p β) :=
+  isRealizableBy_ofFn hvalue
+
+/-! ## Input precomposition -/
+
+/-- Input precomposition along an admissible map. The realizing machine is the
+original one with a new initialization, so its readout and transition maps — and
+hence their admissibility proofs — are shared definitionally. -/
+theorem IsRealizableBy.precomp {γ : Type u} {inputRep : C.Str γ} {f : γ → α}
+    (h : IsRealizableBy C bd program) (hf : C.Hom inputRep bd.input f) :
+    IsRealizableBy C (bd.withInput inputRep) fun input => program (f input) := by
+  obtain ⟨R, hR⟩ := h
+  refine ⟨⟨R.machine.contramapInput f, R.state, ?_, R.head_mem, R.update_mem⟩,
+    hR.contramapInput f⟩
+  change C.Hom inputRep R.state (R.machine.init ∘ f)
+  exact C.comp_mem hf R.init_mem
+
+/-- Input precomposition preserves the query budget: reindexing inputs performs
+no queries of its own. -/
+theorem IsRealizableWithin.precomp {γ : Type u} {inputRep : C.Str γ} {f : γ → α}
+    {k : ℕ} (h : IsRealizableWithin C bd program k)
+    (hf : C.Hom inputRep bd.input f) :
+    IsRealizableWithin C (bd.withInput inputRep) (fun input => program (f input)) k := by
+  obtain ⟨R, hR⟩ := h
+  rw [implementsWithin_iff_implements_and_bound] at hR
+  refine ⟨⟨R.machine.contramapInput f, R.state, ?_, R.head_mem, R.update_mem⟩, ?_⟩
+  · change C.Hom inputRep R.state (R.machine.init ∘ f)
+    exact C.comp_mem hf R.init_mem
+  · rw [implementsWithin_iff_implements_and_bound]
+    exact ⟨hR.1.contramapInput f, fun input => hR.2 (f input)⟩
+
+/-! ## Result postcomposition -/
+
+/-- Postcomposition on results along an admissible map. The realizing machine is
+the original one with its readout postcomposed, which acts on the one-step
+readout `β ⊕ p.A` by `Sum.map` and leaves the flattened transition alone. -/
+theorem IsRealizableBy.mapResult {γ : Type u} {outRep : C.Str γ} {g : β → γ}
+    (h : IsRealizableBy C bd program) (hg : C.Hom bd.out outRep g) :
+    IsRealizableBy C (bd.withOut outRep)
+      fun input => FreeM.map g (program input) := by
+  obtain ⟨R, hR⟩ := h
+  refine ⟨⟨R.machine.mapResult g, R.state, R.init_mem, ?_, ?_⟩, hR.mapResult g⟩
+  · refine (C.comp_mem R.head_mem
+      (StepClass.HasSum.map_mem hg (C.id_mem bd.pos))).congr ?_
+    intro state
+    exact (head_mapResult R.machine g state).symm
+  · refine R.update_mem.congr ?_
+    intro step
+    exact (update?_mapResult R.machine g step).symm
+
+/-- Postcomposition on results preserves the query budget: mapping a returned
+value performs no queries of its own. -/
+theorem IsRealizableWithin.mapResult {γ : Type u} {outRep : C.Str γ} {g : β → γ}
+    {k : ℕ} (h : IsRealizableWithin C bd program k)
+    (hg : C.Hom bd.out outRep g) :
+    IsRealizableWithin C (bd.withOut outRep)
+      (fun input => FreeM.map g (program input)) k := by
+  obtain ⟨R, hR⟩ := h
+  rw [implementsWithin_iff_implements_and_bound] at hR
+  refine ⟨⟨R.machine.mapResult g, R.state, R.init_mem, ?_, ?_⟩, ?_⟩
+  · refine (C.comp_mem R.head_mem
+      (StepClass.HasSum.map_mem hg (C.id_mem bd.pos))).congr ?_
+    intro state
+    exact (head_mapResult R.machine g state).symm
+  · refine R.update_mem.congr ?_
+    intro step
+    exact (update?_mapResult R.machine g step).symm
+  · rw [implementsWithin_iff_implements_and_bound]
+    refine ⟨hR.1.mapResult g, fun input => ?_⟩
+    exact (FreeM.isRollBound_map_iff (program input) g k _ _).mpr (hR.2 input)
+
+/-! ## Sequential composition -/
+
+section SeqComp
+
+variable [D : C.IsDistributive] {γ : Type u} {outRep : C.Str γ}
+  {program₁ : α → FreeM p β} {program₂ : β → FreeM p γ}
+
+/-- The admissible realization of a sequential composition.
+
+The state is the coproduct of the two phases' states. The readout needs only
+`comp_mem`, `elim_mem`, and `inr_mem` — no products at all. The partial transition
+is where distributivity enters, twice: once to split on the state summand, once to
+split on the first phase's readout while retaining the answer index. -/
+private def seqCompRealization (R₁ : Realization C bd)
+    (R₂ : Realization C (bd.mid outRep)) :
+    Realization C (bd.withOut outRep) where
+  machine := R₁.machine.seqComp R₂.machine
+  state := S.sum R₁.state R₂.state
+  init_mem := by
+    refine (C.comp_mem R₁.init_mem (S.inl_mem R₁.state R₂.state)).congr ?_
+    intro input
+    rfl
+  head_mem := by
+    refine (S.elim_mem
+      (C.comp_mem R₁.head_mem
+        (S.elim_mem (C.comp_mem R₂.init_mem R₂.head_mem)
+          (S.inr_mem outRep bd.pos)))
+      R₂.head_mem).congr ?_
+    intro state
+    cases state with
+    | inl state₁ => exact (head_seqComp_inl R₁.machine R₂.machine state₁).symm
+    | inr state₂ => exact (head_seqComp_inr R₁.machine R₂.machine state₂).symm
+  update_mem := by
+    -- The right summand: advance the second phase and re-tag the result.
+    have hRight : C.Hom (P.prod R₂.state bd.idx)
+        (StepClass.HasOption.option (S.sum R₁.state R₂.state))
+        (fun x => Option.map Sum.inr (R₂.machine.update? x)) :=
+      C.comp_mem R₂.update_mem
+        (StepClass.HasOption.omap_mem (S.inr_mem R₁.state R₂.state))
+    -- The left summand, first phase still exposing a query.
+    have hQuery : C.Hom (P.prod bd.pos (P.prod R₁.state bd.idx))
+        (StepClass.HasOption.option (S.sum R₁.state R₂.state))
+        (fun y => Option.map Sum.inl (R₁.machine.update? y.2)) :=
+      C.comp_mem (P.snd_mem bd.pos (P.prod R₁.state bd.idx))
+        (C.comp_mem R₁.update_mem
+          (StepClass.HasOption.omap_mem (S.inl_mem R₁.state R₂.state)))
+    -- The left summand, first phase already returned: hand over to the second.
+    have hHandoff : C.Hom (P.prod bd.out (P.prod R₁.state bd.idx))
+        (StepClass.HasOption.option (S.sum R₁.state R₂.state))
+        (fun y => Option.map Sum.inr
+          (R₂.machine.update? (R₂.machine.init y.1, y.2.2))) :=
+      C.comp_mem
+        (P.pair_mem
+          (C.comp_mem (P.fst_mem bd.out (P.prod R₁.state bd.idx)) R₂.init_mem)
+          (C.comp_mem (P.snd_mem bd.out (P.prod R₁.state bd.idx))
+            (P.snd_mem R₁.state bd.idx)))
+        hRight
+    -- Splitting on the first phase's readout, retaining the state and the index.
+    have hLeft : C.Hom (P.prod R₁.state bd.idx)
+        (StepClass.HasOption.option (S.sum R₁.state R₂.state))
+        (fun x => Sum.elim
+          (fun value => Option.map Sum.inr
+            (R₂.machine.update? (R₂.machine.init value, x.2)))
+          (fun _ : p.A => Option.map Sum.inl (R₁.machine.update? x))
+          (R₁.machine.head x.1)) :=
+      C.comp_mem
+        (P.withInput_mem (C.comp_mem (P.fst_mem R₁.state bd.idx) R₁.head_mem))
+        (StepClass.IsDistributive.elimCtx_mem hHandoff hQuery)
+    -- Splitting on the state summand.
+    refine (StepClass.IsDistributive.elimCtx_mem hLeft hRight).congr ?_
+    intro x
+    obtain ⟨state, index⟩ := x
+    cases state with
+    | inl state₁ =>
+        exact (update?_seqComp_inl R₁.machine R₂.machine state₁ index).symm
+    | inr state₂ =>
+        exact (update?_seqComp_inr R₁.machine R₂.machine state₂ index).symm
+
+/-- **Closure under `bind`.** A realization of the first phase and a realization of
+the second compose into a realization of their sequential composition.
+
+The middle boundary is `bd.mid outRep`: the second phase reads the first's results
+and shares its interface. Distributivity is what the composite transition needs,
+and only there — the readout side needs no products at all. -/
+theorem IsRealizableBy.seqComp (h₁ : IsRealizableBy C bd program₁)
+    (h₂ : IsRealizableBy C (bd.mid outRep) program₂) :
+    IsRealizableBy C (bd.withOut outRep)
+      fun input => FreeM.bind (program₁ input) program₂ := by
+  obtain ⟨R₁, hR₁⟩ := h₁
+  obtain ⟨R₂, hR₂⟩ := h₂
+  exact ⟨seqCompRealization R₁ R₂, hR₁.seqComp hR₂⟩
+
+/-- Sequential composition of bounded realizations, with additive budgets. The
+query budget is exactly the one the underlying `ImplementsWithin.seqComp`
+supplies. -/
+theorem IsRealizableWithin.seqComp {k₁ k₂ : ℕ}
+    (h₁ : IsRealizableWithin C bd program₁ k₁)
+    (h₂ : IsRealizableWithin C (bd.mid outRep) program₂ k₂) :
+    IsRealizableWithin C (bd.withOut outRep)
+      (fun input => FreeM.bind (program₁ input) program₂) (k₁ + k₂) := by
+  obtain ⟨R₁, hR₁⟩ := h₁
+  obtain ⟨R₂, hR₂⟩ := h₂
+  exact ⟨seqCompRealization R₁ R₂, hR₁.seqComp hR₂⟩
+
+end SeqComp
+
+/-! ## Interface transport -/
+
+section Wrap
+
+variable {q : PFunctor.{u, u}} [DecidableEq q.A]
+
+variable (posRep : C.Str q.A) (idxRep : C.Str q.Idx)
+
+/-- A lens is `C`-admissible, relative to a boundary for its source interface and
+representations for its target interface, when its position map and its flattened
+index pullback are `C`-morphisms.
+
+Two fields rather than one existential: the pullback is uniquely determined by the
+lens, so it is `Lens.pullHeadIdx` and only its admissibility is a hypothesis.
+
+Unlike `Lens.IsCartesian` this has no `.id` and no `.comp`, and that is not an
+oversight. `pullHeadIdx` compares the incoming answer's tag against the position
+the lens exposes, so even the *identity* lens's pullback performs a decidable
+equality test on positions — which is exactly the operation the rest of this layer
+is designed not to require of a step class. Admissibility of a lens is therefore a
+genuine hypothesis about the class, satisfiable by every realistic one but not
+derivable from the mixins. That is also why `seqComp` needs no such hypothesis:
+each phase's own `update?` performs its own tag test internally. -/
+structure _root_.PFunctor.Lens.IsAdmissible (C : StepClass.{u, v}) [C.HasProd]
+    [C.HasSum] [C.HasOption] {p q : PFunctor.{u, u}} [DecidableEq q.A]
+    {α β : Type u} (bd : Boundary C p α β) (posRep : C.Str q.A)
+    (idxRep : C.Str q.Idx) (lens : Lens p q) : Prop where
+  /-- The position map is admissible. -/
+  onPos : C.Hom bd.pos posRep lens.toFunA
+  /-- The flattened index pullback is admissible. -/
+  onPull : C.Hom (StepClass.HasProd.prod bd.head idxRep)
+    (StepClass.HasOption.option bd.idx) (lens.pullHeadIdx β)
+
+/-- Interface transport along an admissible lens. The readout is post-composed
+with the lens's position map; the transition pulls an answer back along the lens
+before feeding it to the underlying computation.
+
+The resolved case needs no constant-map axiom: `pullHeadIdx` returns `none` at a
+resolved readout, and the underlying `update?` is `none` there anyway. -/
+theorem IsRealizableBy.wrap {lens : Lens p q}
+    (hlens : lens.IsAdmissible C bd posRep idxRep)
+    (h : IsRealizableBy C bd program) :
+    IsRealizableBy C (bd.withInterface posRep idxRep)
+      fun input => (program input).mapLens lens := by
+  obtain ⟨R, hR⟩ := h
+  refine ⟨⟨R.machine.wrap lens, R.state, R.init_mem, ?_, ?_⟩, hR.wrap lens⟩
+  · refine (C.comp_mem R.head_mem
+      (S.map_mem (C.id_mem bd.out) hlens.onPos)).congr ?_
+    intro state
+    rfl
+  · refine (C.comp_mem
+      (P.withInput_mem (C.comp_mem (P.pairRight_mem R.head_mem) hlens.onPull))
+      (StepClass.HasOption.obindCtx_mem
+        (C.comp_mem
+          (P.pair_mem
+            (C.comp_mem (P.snd_mem bd.idx (P.prod R.state idxRep))
+              (P.fst_mem R.state idxRep))
+            (P.fst_mem bd.idx (P.prod R.state idxRep)))
+          R.update_mem))).congr ?_
+    intro x
+    obtain ⟨state, index⟩ := x
+    obtain ⟨iposition, idirection⟩ := index
+    exact (update?_wrap R.machine lens state iposition idirection).symm
+
+/-- Interface transport preserves the query budget: a lens relabels positions and
+reindexes directions, leaving the branching structure alone. -/
+theorem IsRealizableWithin.wrap {lens : Lens p q} {k : ℕ}
+    (hlens : lens.IsAdmissible C bd posRep idxRep)
+    (h : IsRealizableWithin C bd program k) :
+    IsRealizableWithin C (bd.withInterface posRep idxRep)
+      (fun input => (program input).mapLens lens) k := by
+  obtain ⟨R, hR⟩ := h
+  rw [implementsWithin_iff_implements_and_bound] at hR
+  obtain ⟨R', hR'⟩ :=
+    IsRealizableBy.wrap (program := program) posRep idxRep hlens ⟨R, hR.1⟩
+  refine ⟨R', ?_⟩
+  rw [implementsWithin_iff_implements_and_bound]
+  exact ⟨hR', fun input => FreeM.isTotalRollBound_mapLens lens _ (hR.2 input)⟩
+
+end Wrap
+
+/-! ## Enlarging the step class -/
+
+variable {D : StepClass.{u, v₂}} [D.HasProd] [D.HasSum] [D.HasOption]
+
+/-- Realizability transports along a refinement of step classes: a realization by
+an admissible machine for a small class is one for every larger class. -/
+theorem IsRealizableBy.mono (Ref : C.Refines D) (h : IsRealizableBy C bd program) :
+    IsRealizableBy D (bd.mapRefines Ref) program := by
+  obtain ⟨R, hR⟩ := h
+  refine ⟨⟨R.machine, Ref.str R.state, Ref.hom R.init_mem, ?_, ?_⟩, hR⟩
+  · rw [Boundary.head, Boundary.mapRefines, ← Ref.str_sum]
+    exact Ref.hom R.head_mem
+  · rw [Boundary.stateIdx, Boundary.mapRefines, ← Ref.str_prod, ← Ref.str_option]
+    exact Ref.hom R.update_mem
+
+/-- Bounded realizability transports along a refinement of step classes. -/
+theorem IsRealizableWithin.mono' {k : ℕ} (Ref : C.Refines D)
+    (h : IsRealizableWithin C bd program k) :
+    IsRealizableWithin D (bd.mapRefines Ref) program k := by
+  obtain ⟨R, hR⟩ := h
+  refine ⟨⟨R.machine, Ref.str R.state, Ref.hom R.init_mem, ?_, ?_⟩, hR⟩
+  · rw [Boundary.head, Boundary.mapRefines, ← Ref.str_sum]
+    exact Ref.hom R.head_mem
+  · rw [Boundary.stateIdx, Boundary.mapRefines, ← Ref.str_prod, ← Ref.str_option]
+    exact Ref.hom R.update_mem
+
+end DynSystem.DynComputation
+
+end PFunctor
diff --git a/PolyFun/Realizability/Instances.lean b/PolyFun/Realizability/Instances.lean
new file mode 100644
index 00000000..bb414537
--- /dev/null
+++ b/PolyFun/Realizability/Instances.lean
@@ -0,0 +1,512 @@
+/-
+Copyright (c) 2026 PolyFun Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Devon Tuma
+-/
+module
+
+public import PolyFun.Realizability.Basic
+public import Mathlib.Computability.Partrec
+public import Mathlib.Data.Fintype.Prod
+public import Mathlib.Data.Fintype.Sum
+
+/-!
+# Concrete step classes
+
+Four instantiations of `PFunctor.StepClass`, in increasing order of content.
+
+* `StepClass.unconstrained` — every type is representable and every function
+  admissible. Realizability collapses to plain implementability, which
+  `isRealizableBy_unconstrained` confirms is never a real restriction. This is the
+  non-vacuity check for the whole layer.
+* `StepClass.finite` — a type is representable when it is finite. Realizability in
+  this class is *finite-state realizability*, the notion Church's synthesis
+  problem asks about and which Pnueli and Rosner (1989) made precise; see
+  `REFERENCES.md`.
+* `StepClass.computable` — Mathlib's `Primcodable` representations and
+  `Computable` functions: machines whose transition functions are computable.
+* `StepClass.ofWordClass` — the bridge from an externally defined class of *word*
+  functions `W → W`. Complexity classes in the wild are almost always presented
+  this way, on one concrete function type such as `List Bool → List Bool`, with no
+  encoding-generic predicate.
+
+Each class carries all four mixins: `HasProd`, `HasSum`, `HasOption`, and
+`IsDistributive`. For `unconstrained` and `finite` every obligation is trivial.
+For `computable` they are short, because Mathlib's `Computable.sumCasesOn` and
+`Computable.option_map` are already stated in *contextual* form — branches
+`α → β → σ` with `α` the ambient context — which is exactly distributivity.
+
+## What a word class has to supply
+
+None of the four mixins is automatic for a monomorphic word class. Bundle the
+required data as a `WordClass`: identity and composition closure, a `WordPairing`
+codec, a `WordTagging` scheme with a distinguished word, and a `WordDistrib`
+rearrangement moving a tag past a pairing. `WordClass.toStepClass` then carries all
+four mixins as instances, so a client never names them.
+
+`WordDistrib` is forced by the mathematics rather than by this presentation:
+`WordTagging.elim` hands each branch only the untagged payload, so its branches
+cannot see the surrounding context and a tag cannot be moved past a pairing using
+`elim` alone.
+
+What this costs a real client: `Complexity.FP` (complexitylib) and
+`Cslib.Turing.PolyTimeComputable` (cslib) both supply the identity and composition
+closure, and complexitylib has the pairing ingredients (`Complexity.pair`,
+`unpair?`, `delimit`) — but neither exposes them as class-level closure results,
+and cslib has no pairing or projection machines at all. cslib's
+`PolyTimeComputable` is additionally `Type`-valued with a `Monotone` side condition
+on `comp` whose removal is still a `TODO` upstream, so `Mem f :=
+Nonempty (PolyTimeComputable f)` needs a monotonisation lemma that does not exist
+yet.
+-/
+
+@[expose] public section
+
+universe u v
+
+namespace PFunctor
+
+namespace StepClass
+
+/-! ## The unconstrained class -/
+
+/-- The step class that constrains nothing: every type is representable, by no
+data, and every function is admissible. -/
+def unconstrained : StepClass.{u, v} where
+  Str _ := PUnit.{v + 1}
+  Hom _ _ _ := True
+  id_mem _ := True.intro
+  comp_mem _ _ := True.intro
+
+instance : (unconstrained.{u, v}).HasProd where
+  prod _ _ := PUnit.unit
+  fst_mem _ _ := True.intro
+  snd_mem _ _ := True.intro
+  pair_mem _ _ := True.intro
+
+instance : (unconstrained.{u, v}).HasSum where
+  sum _ _ := PUnit.unit
+  inl_mem _ _ := True.intro
+  inr_mem _ _ := True.intro
+  elim_mem _ _ := True.intro
+
+instance : (unconstrained.{u, v}).HasOption where
+  option _ := PUnit.unit
+  omap_mem _ := True.intro
+  none_mem _ _ := True.intro
+  obindCtx_mem _ := True.intro
+
+instance : (unconstrained.{u, v}).IsDistributive where
+  distrib_mem _ _ _ := True.intro
+
+/-! ## The finite class -/
+
+/-- The step class of finite representations: a type is representable exactly when
+it is finite, and every function between finite types is admissible. -/
+def finite : StepClass.{u, u} where
+  Str := Fintype
+  Hom _ _ _ := True
+  id_mem _ := True.intro
+  comp_mem _ _ := True.intro
+
+instance : (finite.{u}).HasProd where
+  prod {A B} a b := @instFintypeProd A B a b
+  fst_mem _ _ := True.intro
+  snd_mem _ _ := True.intro
+  pair_mem _ _ := True.intro
+
+instance : (finite.{u}).HasSum where
+  sum {A B} a b := @instFintypeSum A B a b
+  inl_mem _ _ := True.intro
+  inr_mem _ _ := True.intro
+  elim_mem _ _ := True.intro
+
+instance : (finite.{u}).HasOption where
+  option {A} a := by
+    letI : Fintype A := a
+    exact (inferInstance : Fintype (Option A))
+  omap_mem _ := True.intro
+  none_mem _ _ := True.intro
+  obindCtx_mem _ := True.intro
+
+instance : (finite.{u}).IsDistributive where
+  distrib_mem _ _ _ := True.intro
+
+/-! ## The computable class -/
+
+/-- The step class of computable functions between `Primcodable` types.
+
+The representation carried by a type is its `Primcodable` structure, which is
+genuine data: `Computable f` is a statement about the encodings, so the class
+cannot be phrased without them. -/
+def computable : StepClass.{u, u} where
+  Str := Primcodable
+  Hom {A B} a b f := @Computable A B a b f
+  id_mem {A} a := by
+    letI : Primcodable A := a
+    exact Computable.id
+  comp_mem {A B D} {a b d} {f g} hf hg := by
+    letI : Primcodable A := a
+    letI : Primcodable B := b
+    letI : Primcodable D := d
+    have hf' : Computable f := hf
+    have hg' : Computable g := hg
+    exact hg'.comp hf'
+
+instance : (computable.{u}).HasProd where
+  prod {A B} a b := @Primcodable.prod A B a b
+  fst_mem {A B} a b := by
+    letI : Primcodable A := a
+    letI : Primcodable B := b
+    exact Computable.fst
+  snd_mem {A B} a b := by
+    letI : Primcodable A := a
+    letI : Primcodable B := b
+    exact Computable.snd
+  pair_mem {A B D} {a b d} {f g} hf hg := by
+    letI : Primcodable A := a
+    letI : Primcodable B := b
+    letI : Primcodable D := d
+    have hf' : Computable f := hf
+    have hg' : Computable g := hg
+    exact hf'.pair hg'
+
+instance : (computable.{u}).HasSum where
+  sum {A B} a b := @Primcodable.sum A B a b
+  inl_mem {A B} a b := by
+    letI : Primcodable A := a
+    letI : Primcodable B := b
+    exact Primrec.sumInl.to_comp
+  inr_mem {A B} a b := by
+    letI : Primcodable A := a
+    letI : Primcodable B := b
+    exact Primrec.sumInr.to_comp
+  elim_mem {A B D} {a b d} {f g} hf hg := by
+    letI : Primcodable A := a
+    letI : Primcodable B := b
+    letI : Primcodable D := d
+    have hf' : Computable f := hf
+    have hg' : Computable g := hg
+    refine Computable.of_eq (Computable.sumCasesOn Computable.id
+      (hf'.comp Computable.snd).to₂ (hg'.comp Computable.snd).to₂) ?_
+    intro x
+    cases x <;> rfl
+
+instance : (computable.{u}).HasOption where
+  option {A} a := @Primcodable.option A a
+  omap_mem {A B} {a b} {f} hf := by
+    letI : Primcodable A := a
+    letI : Primcodable B := b
+    have hf' : Computable f := hf
+    refine Computable.of_eq
+      (Computable.option_map Computable.id (hf'.comp Computable.snd).to₂) ?_
+    intro x
+    cases x <;> rfl
+  none_mem {A B} a b := by
+    letI : Primcodable A := a
+    letI : Primcodable B := b
+    exact Computable.const none
+  obindCtx_mem {A B E} {a b e} {k} hk := by
+    letI : Primcodable A := a
+    letI : Primcodable B := b
+    letI : Primcodable E := e
+    have hk' : Computable k := hk
+    refine Computable.of_eq
+      (Computable.option_bind Computable.fst
+        (hk'.comp (Computable.pair Computable.snd
+          (Computable.snd.comp Computable.fst))).to₂) ?_
+    intro y
+    cases y.1 <;> rfl
+
+/-- Mathlib's sum eliminator is already stated in *contextual* form — its branches
+are `α → β → σ` with `α` the ambient context — which is exactly distributivity. -/
+instance : (computable.{u}).IsDistributive where
+  distrib_mem {A B I} a b i := by
+    letI : Primcodable A := a
+    letI : Primcodable B := b
+    letI : Primcodable I := i
+    refine Computable.of_eq (Computable.sumCasesOn Computable.fst
+      (Primrec.sumInl.to_comp.comp (Computable.pair Computable.snd
+        (Computable.snd.comp Computable.fst))).to₂
+      (Primrec.sumInr.to_comp.comp (Computable.pair Computable.snd
+        (Computable.snd.comp Computable.fst))).to₂) ?_
+    rintro ⟨x | x, j⟩ <;> rfl
+
+/-! ## The bridge from a class of word functions -/
+
+/-- A pairing codec on `W` whose operations the word class `Q` admits. This is the
+data a monomorphic word class needs in order to represent binary products. -/
+structure WordPairing {W : Type u} (Q : (W → W) → Prop) where
+  /-- Pair two words. -/
+  pair : W → W → W
+  /-- Pairing is injective in both arguments jointly. -/
+  pair_inj : ∀ w₁ w₂ w₁' w₂', pair w₁ w₂ = pair w₁' w₂' → w₁ = w₁' ∧ w₂ = w₂'
+  /-- Recover the first component. -/
+  fst : W → W
+  /-- Recover the second component. -/
+  snd : W → W
+  /-- The first projection is admissible. -/
+  fst_mem : Q fst
+  /-- The second projection is admissible. -/
+  snd_mem : Q snd
+  /-- `fst` is a left inverse of pairing. -/
+  fst_pair : ∀ w₁ w₂, fst (pair w₁ w₂) = w₁
+  /-- `snd` is a right inverse of pairing. -/
+  snd_pair : ∀ w₁ w₂, snd (pair w₁ w₂) = w₂
+  /-- Admissible functions can be paired. -/
+  pair_mem : ∀ {f g : W → W}, Q f → Q g → Q fun w => pair (f w) (g w)
+
+/-- A tagging scheme on `W` whose operations the word class `Q` admits. This is the
+data a monomorphic word class needs in order to represent binary sums. -/
+structure WordTagging {W : Type u} (Q : (W → W) → Prop) where
+  /-- Tag a word as coming from the left summand. -/
+  inl : W → W
+  /-- Tag a word as coming from the right summand. -/
+  inr : W → W
+  /-- Left tagging is admissible. -/
+  inl_mem : Q inl
+  /-- Right tagging is admissible. -/
+  inr_mem : Q inr
+  /-- Left tagging is injective. -/
+  inl_inj : Function.Injective inl
+  /-- Right tagging is injective. -/
+  inr_inj : Function.Injective inr
+  /-- The two tags are distinguishable. -/
+  inl_ne_inr : ∀ w₁ w₂, inl w₁ ≠ inr w₂
+  /-- Dispatch on the tag. -/
+  elim : (W → W) → (W → W) → W → W
+  /-- Dispatch on admissible branches is admissible. -/
+  elim_mem : ∀ {f g : W → W}, Q f → Q g → Q (elim f g)
+  /-- Dispatch takes the left branch on a left tag. -/
+  elim_inl : ∀ (f g : W → W) (w : W), elim f g (inl w) = f w
+  /-- Dispatch takes the right branch on a right tag. -/
+  elim_inr : ∀ (f g : W → W) (w : W), elim f g (inr w) = g w
+  /-- A distinguished word, used as the payload of the absent optional value. -/
+  pt : W
+  /-- The constant map at the distinguished word is admissible. -/
+  const_mem : Q fun _ => pt
+
+/-- Moving a tag past a pairing: the word-level content of distributivity.
+
+This datum is forced by the mathematics rather than by the presentation.
+`WordTagging.elim` hands each branch only the *untagged* payload, so its branches
+cannot see the surrounding context, and a tag therefore cannot be moved past a
+pairing using `elim` alone. -/
+structure WordDistrib {W : Type u} (Q : (W → W) → Prop) (P : WordPairing Q)
+    (T : WordTagging Q) where
+  /-- Move the tag of a paired word's first component outwards. -/
+  distrib : W → W
+  /-- The rearrangement is admissible. -/
+  distrib_mem : Q distrib
+  /-- On a left tag. -/
+  distrib_inl : ∀ w v, distrib (P.pair (T.inl w) v) = T.inl (P.pair w v)
+  /-- On a right tag. -/
+  distrib_inr : ∀ w v, distrib (P.pair (T.inr w) v) = T.inr (P.pair w v)
+
+/-- The step class built from a class `Q` of word functions on `W` that contains
+the identity and is closed under composition.
+
+A type is representable by an injective encoding into `W` — injectivity is the
+only semantic demand, exactly as for a raw bit encoding — and a function is
+admissible when some `Q`-function intertwines the encodings. -/
+def ofWordClass (W : Type u) (Q : (W → W) → Prop) (hid : Q id)
+    (hcomp : ∀ {f g : W → W}, Q f → Q g → Q (g ∘ f)) : StepClass.{u, u} where
+  Str A := { encode : A → W // Function.Injective encode }
+  Hom eA eB f := ∃ q : W → W, Q q ∧ ∀ x, q (eA.1 x) = eB.1 (f x)
+  id_mem _ := ⟨id, hid, fun _ => rfl⟩
+  comp_mem := by
+    rintro A B D a b d f g ⟨qf, hqf, hfEq⟩ ⟨qg, hqg, hgEq⟩
+    refine ⟨qg ∘ qf, hcomp hqf hqg, fun x => ?_⟩
+    simp only [Function.comp_apply, hfEq, hgEq]
+
+/-- All the word-level data a monomorphic class needs in order to be a
+distributive step class: identity and composition closure, a pairing codec, a
+tagging scheme, and the tag-past-pairing rearrangement.
+
+Supplying one of these is what an external complexity library has to do. The four
+`StepClass` mixins are then instances on `toStepClass`, so a client never has to
+name them. -/
+structure WordClass (W : Type u) where
+  /-- Which word functions the class admits. -/
+  Mem : (W → W) → Prop
+  /-- The identity is admissible. -/
+  id_mem : Mem id
+  /-- Admissible word functions compose. -/
+  comp_mem : ∀ {f g : W → W}, Mem f → Mem g → Mem (g ∘ f)
+  /-- A pairing codec. -/
+  pairing : WordPairing Mem
+  /-- A tagging scheme. -/
+  tagging : WordTagging Mem
+  /-- The tag-past-pairing rearrangement. -/
+  distributor : WordDistrib Mem pairing tagging
+
+/-- The step class presented by a bundle of word-level data. -/
+@[reducible] def WordClass.toStepClass {W : Type u} (V : WordClass W) :
+    StepClass.{u, u} :=
+  ofWordClass W V.Mem V.id_mem V.comp_mem
+
+/-- Products for a word class, from a pairing codec. -/
+@[reducible] def ofWordClass.hasProd {W : Type u} {Q : (W → W) → Prop} {hid : Q id}
+    {hcomp : ∀ {f g : W → W}, Q f → Q g → Q (g ∘ f)}
+    (P : WordPairing Q) : (ofWordClass W Q hid hcomp).HasProd where
+  prod a b :=
+    ⟨fun x => P.pair (a.1 x.1) (b.1 x.2), by
+      rintro ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ h
+      obtain ⟨h₁, h₂⟩ := P.pair_inj _ _ _ _ h
+      exact Prod.ext (a.2 h₁) (b.2 h₂)⟩
+  fst_mem _ _ := ⟨P.fst, P.fst_mem, fun _ => P.fst_pair _ _⟩
+  snd_mem _ _ := ⟨P.snd, P.snd_mem, fun _ => P.snd_pair _ _⟩
+  pair_mem := by
+    rintro A B D a b d f g ⟨qf, hqf, hfEq⟩ ⟨qg, hqg, hgEq⟩
+    refine ⟨fun w => P.pair (qf w) (qg w), P.pair_mem hqf hqg, fun x => ?_⟩
+    change P.pair (qf (a.1 x)) (qg (a.1 x)) = P.pair (b.1 (f x)) (d.1 (g x))
+    rw [hfEq, hgEq]
+
+/-- Sums for a word class, from a tagging scheme. -/
+@[reducible] def ofWordClass.hasSum {W : Type u} {Q : (W → W) → Prop} {hid : Q id}
+    {hcomp : ∀ {f g : W → W}, Q f → Q g → Q (g ∘ f)}
+    (T : WordTagging Q) : (ofWordClass W Q hid hcomp).HasSum where
+  sum a b :=
+    ⟨Sum.elim (fun x => T.inl (a.1 x)) fun y => T.inr (b.1 y), by
+      rintro (x | x) (y | y) h
+      · exact congrArg Sum.inl (a.2 (T.inl_inj h))
+      · exact absurd h (T.inl_ne_inr _ _)
+      · exact absurd h.symm (T.inl_ne_inr _ _)
+      · exact congrArg Sum.inr (b.2 (T.inr_inj h))⟩
+  inl_mem _ _ := ⟨T.inl, T.inl_mem, fun _ => rfl⟩
+  inr_mem _ _ := ⟨T.inr, T.inr_mem, fun _ => rfl⟩
+  elim_mem := by
+    rintro A B D a b d f g ⟨qf, hqf, hfEq⟩ ⟨qg, hqg, hgEq⟩
+    refine ⟨T.elim qf qg, T.elim_mem hqf hqg, fun x => ?_⟩
+    cases x with
+    | inl x =>
+        change T.elim qf qg (T.inl (a.1 x)) = d.1 (f x)
+        rw [T.elim_inl, hfEq]
+    | inr y =>
+        change T.elim qf qg (T.inr (b.1 y)) = d.1 (g y)
+        rw [T.elim_inr, hgEq]
+
+section WordClassInstances
+
+variable {W : Type u} (V : WordClass W)
+
+instance WordClass.instHasProd : V.toStepClass.HasProd :=
+  ofWordClass.hasProd V.pairing
+
+instance WordClass.instHasSum : V.toStepClass.HasSum :=
+  ofWordClass.hasSum V.tagging
+
+/-- Optional values for a word class: the absent value is the right tag carrying
+the distinguished word.
+
+`obindCtx_mem` needs the tag-past-pairing rearrangement, because sequencing must
+inspect the tag of the first component while retaining the second. -/
+instance WordClass.instHasOption : V.toStepClass.HasOption where
+  option a :=
+    ⟨fun o => o.elim (V.tagging.inr V.tagging.pt) fun x => V.tagging.inl (a.1 x), by
+      rintro (_ | x) (_ | y) h
+      · rfl
+      · exact absurd h.symm (V.tagging.inl_ne_inr _ _)
+      · exact absurd h (V.tagging.inl_ne_inr _ _)
+      · exact congrArg some (a.2 (V.tagging.inl_inj h))⟩
+  omap_mem := by
+    rintro A B a b f ⟨qf, hqf, hfEq⟩
+    refine ⟨V.tagging.elim (fun w => V.tagging.inl (qf w)) V.tagging.inr,
+      V.tagging.elim_mem (V.comp_mem hqf V.tagging.inl_mem) V.tagging.inr_mem, fun o => ?_⟩
+    cases o with
+    | none =>
+        change V.tagging.elim _ _ (V.tagging.inr V.tagging.pt) = V.tagging.inr V.tagging.pt
+        rw [V.tagging.elim_inr]
+    | some x =>
+        change V.tagging.elim _ _ (V.tagging.inl (a.1 x)) = V.tagging.inl (b.1 (f x))
+        rw [V.tagging.elim_inl, hfEq]
+  none_mem a b :=
+    ⟨fun _ => V.tagging.inr V.tagging.pt,
+      V.comp_mem V.tagging.const_mem V.tagging.inr_mem, fun _ => rfl⟩
+  obindCtx_mem := by
+    rintro A B E a b e k ⟨qk, hqk, hkEq⟩
+    refine ⟨V.tagging.elim qk (fun _ => V.tagging.inr V.tagging.pt) ∘
+        V.distributor.distrib,
+      V.comp_mem V.distributor.distrib_mem
+        (V.tagging.elim_mem hqk (V.comp_mem V.tagging.const_mem V.tagging.inr_mem)),
+      fun y => ?_⟩
+    obtain ⟨o, v⟩ := y
+    cases o with
+    | none =>
+        change V.tagging.elim _ _
+          (V.distributor.distrib (V.pairing.pair (V.tagging.inr V.tagging.pt)
+            (e.1 v))) = V.tagging.inr V.tagging.pt
+        rw [V.distributor.distrib_inr, V.tagging.elim_inr]
+    | some j =>
+        change V.tagging.elim _ _
+          (V.distributor.distrib (V.pairing.pair (V.tagging.inl (a.1 j))
+            (e.1 v))) = _
+        rw [V.distributor.distrib_inl, V.tagging.elim_inl]
+        exact hkEq (j, v)
+
+/-- Distributivity for a word class: exactly the tag-past-pairing
+rearrangement. -/
+instance WordClass.instIsDistributive : V.toStepClass.IsDistributive where
+  distrib_mem a b i := by
+    refine ⟨V.distributor.distrib, V.distributor.distrib_mem, fun x => ?_⟩
+    obtain ⟨s, v⟩ := x
+    cases s with
+    | inl l =>
+        change V.distributor.distrib
+            (V.pairing.pair (V.tagging.inl (a.1 l)) (i.1 v)) =
+          V.tagging.inl (V.pairing.pair (a.1 l) (i.1 v))
+        rw [V.distributor.distrib_inl]
+    | inr r =>
+        change V.distributor.distrib
+            (V.pairing.pair (V.tagging.inr (b.1 r)) (i.1 v)) =
+          V.tagging.inr (V.pairing.pair (b.1 r) (i.1 v))
+        rw [V.distributor.distrib_inr]
+
+end WordClassInstances
+
+end StepClass
+
+namespace DynSystem.DynComputation
+
+variable {p : PFunctor.{u, u}} {α β : Type u}
+
+/-! ## Non-vacuity -/
+
+/-- The boundary carrying no information, over the unconstrained class. -/
+def Boundary.unconstrained (p : PFunctor.{u, u}) (α β : Type u) :
+    Boundary StepClass.unconstrained.{u, v} p α β :=
+  ⟨PUnit.unit, PUnit.unit, PUnit.unit, PUnit.unit⟩
+
+/-- Non-vacuity of the whole layer: with no constraint on the step maps,
+realizability is exactly plain implementability, and every well-founded program
+family is realized — by the canonical machine whose states are the residual
+programs.
+
+Any *failure* of realizability is therefore attributable to the step class, never
+to the shape of the definition. -/
+theorem isRealizableBy_unconstrained [DecidableEq p.A] (program : α → FreeM p β) :
+    IsRealizableBy StepClass.unconstrained.{u, v}
+      (Boundary.unconstrained p α β) program :=
+  ⟨⟨ofFreeM program, PUnit.unit, True.intro, True.intro, True.intro⟩,
+    implements_ofFreeM program⟩
+
+/-! ## Finite-state realizability -/
+
+/-- Finite-state realizability: the program family is implemented by a machine
+with a finite state set. This is the notion Church's synthesis problem asks about,
+and the specialization of `IsRealizableBy` at `StepClass.finite`. -/
+abbrev IsFiniteStateRealizable [DecidableEq p.A]
+    (bd : Boundary StepClass.finite.{u} p α β) (program : α → FreeM p β) : Prop :=
+  IsRealizableBy StepClass.finite bd program
+
+/-- Finite-state realizability within a budget bounds the program's query depth.
+The machine's finiteness plays no part: the bound is carried by the budget. -/
+theorem IsFiniteStateRealizable.isTotalRollBound [DecidableEq p.A]
+    {bd : Boundary StepClass.finite.{u} p α β} {program : α → FreeM p β} {k : ℕ}
+    (h : IsRealizableWithin StepClass.finite bd program k) (input : α) :
+    (program input).IsTotalRollBound k :=
+  h.isTotalRollBound input
+
+end DynSystem.DynComputation
+
+end PFunctor
diff --git a/PolyFun/Realizability/Machine.lean b/PolyFun/Realizability/Machine.lean
new file mode 100644
index 00000000..86e0cd9a
--- /dev/null
+++ b/PolyFun/Realizability/Machine.lean
@@ -0,0 +1,535 @@
+/-
+Copyright (c) 2026 PolyFun Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Devon Tuma
+-/
+module
+
+public import PolyFun.PFunctor.Dynamical.DynComputation.Bounded
+
+/-!
+# First-order step maps of a returning dynamical computation
+
+A `DynComputation`'s dynamics are carried by `view`, whose codomain
+`β ⊕ p.Obj State` stores a *function-valued* continuation and whose second
+component is dependent on the exposed position. Neither shape can be constrained
+by a predicate on plain functions. This module presents the same dynamics as
+first-order maps between plain types:
+
+* `head : State → β ⊕ p.A` — the one-step readout: the value returned at a
+  resolved state, or the query position exposed at an unresolved one. This is
+  *definitionally* the position map of the computation's underlying lens.
+* `update? : State × p.Idx → Option State` — the continuation, flattened onto the
+  whole index space `p.Idx = Σ a, p.B a`. `none` means the pair is not a step the
+  computation can take: the state has already returned, or the answer is tagged
+  with a position the computation is not exposing.
+
+**Partiality is load-bearing.** The total variant `updateFlat`, which collapses
+`none` to the unchanged state, does not compose across a state coproduct with a
+handoff: at a left state whose intermediate value has been handed to the second
+phase, a mismatched tag leaves the composite in the *left* summand while the
+second phase alone would stay at its own initial state. Reconciling those junk
+values would require the ambient class to contain a decidable-equality test on
+interface positions. With `none` they agree, and `update?_seqComp_inl` becomes an
+equation unconditional in the answer index.
+
+Nothing constrains where `none` occurs beyond what the semantics forces, and the
+run semantics never feeds a direction at a position other than the exposed one, so
+the flattening carries no coherence side conditions — the only cost is
+`DecidableEq p.A`.
+
+`updateFlat`, `output`, `expose`, and `stepD` are the derived accessors a
+machine-facing cost model consumes: a total state-to-state transition, an optional
+readout, a total query selector, and the deterministic one-step transition against
+a fixed pure handler.
+
+`ofStep_step_eq_of_flat_eq` records that the presentation is faithful: a step
+function is determined by the `head` and `update?` it induces, so constraining
+those two maps (plus `init`) is a constraint on the machine itself and not on an
+arbitrary projection of it.
+
+Every map here is spelled with `Sum` and `Option` combinators rather than with
+`match`. An auto-generated matcher abstracts the computation and blocks
+unification across distinct input types, whereas combinator applications reduce
+by congruence over the shared `view`; that is exactly why the `setInit`
+transport lemmas below hold by `rfl`.
+-/
+
+@[expose] public section
+
+universe u v w uA uB uA₂ uB₂ uα uβ uγ
+
+namespace PFunctor
+
+namespace DynSystem.DynComputation
+
+variable {p : PFunctor.{uA, uB}} {α : Type uα} {β : Type uβ}
+
+/-! ## The one-step readout -/
+
+/-- The one-step readout of a returning computation: the value returned at a
+resolved state, or the query position exposed at an unresolved one.
+
+This is exactly the position map of the computation's underlying lens, so
+computations sharing `toMachine` share it definitionally, and interface or
+result transport act on it by plain post-composition. -/
+def head (M : DynComputation.{u} p α β) : M.State → β ⊕ p.A :=
+  M.toDynSystem.expose
+
+theorem head_def (M : DynComputation.{u} p α β) (state : M.State) :
+    M.head state = M.toDynSystem.expose state := rfl
+
+private theorem sumMap_fst_unpack {X : Type w}
+    (step : (C.{uβ, uB} β + p).Obj X) :
+    Sum.map id Sigma.fst (Resumption.unpack (β := β) step) = step.1 := by
+  rcases step with ⟨position, next⟩
+  cases position <;> rfl
+
+/-- The readout is the position component of the one-step view: it forgets the
+continuation and keeps the returned value or the exposed position. -/
+theorem head_eq_sumMap_view (M : DynComputation.{u} p α β) (state : M.State) :
+    M.head state = Sum.map id Sigma.fst (M.view state) :=
+  (sumMap_fst_unpack (M.toDynSystem.out state)).symm
+
+theorem head_eq_inl_of_view (M : DynComputation.{u} p α β)
+    {state : M.State} {value : β} (hview : M.view state = Sum.inl value) :
+    M.head state = Sum.inl value := by
+  rw [head_eq_sumMap_view, hview]; rfl
+
+theorem head_eq_inr_of_view (M : DynComputation.{u} p α β)
+    {state : M.State} {query : p.Obj M.State}
+    (hview : M.view state = Sum.inr query) :
+    M.head state = Sum.inr query.1 := by
+  rw [head_eq_sumMap_view, hview]; rfl
+
+/-! ## The flattened transition -/
+
+/-- The continuation of a returning computation, flattened onto the whole index
+space as a *partial* function.
+
+`none` means the pair is not a step the computation can take: the state has
+already returned, or the answer is tagged with a position the computation is not
+exposing. `some state'` means the answer is one the computation is waiting for and
+`state'` is where it goes.
+
+Partiality is what makes the flattening compositional. The total variant
+`updateFlat` collapses `none` to the unchanged state, which suits a cost model
+that wants a plain state-to-state map, but does not compose across a state
+coproduct with a handoff: at a left state whose intermediate value has been handed
+over, the composite stays in the left summand on a mismatched tag while the second
+phase alone would stay at its own initial state. With `none` both are `none`. -/
+def update? [DecidableEq p.A] (M : DynComputation.{u} p α β) :
+    M.State × p.Idx → Option M.State := fun step =>
+  (M.view step.1).elim (fun _ => none)
+    (fun query =>
+      if h : step.2.1 = query.1 then some (query.2 (h ▸ step.2.2)) else none)
+
+theorem update?_of_view_return [DecidableEq p.A] (M : DynComputation.{u} p α β)
+    {state : M.State} {value : β} (hview : M.view state = Sum.inl value)
+    (index : p.Idx) : M.update? (state, index) = none := by
+  unfold update?; rw [hview]; rfl
+
+theorem update?_of_view_query [DecidableEq p.A] (M : DynComputation.{u} p α β)
+    {state : M.State} {position : p.A} {next : p.B position → M.State}
+    (hview : M.view state = Sum.inr ⟨position, next⟩)
+    (direction : p.B position) :
+    M.update? (state, ⟨position, direction⟩) = some (next direction) := by
+  unfold update?; rw [hview]
+  simp only [Sum.elim_inr, dif_pos]
+
+theorem update?_of_view_query_of_ne [DecidableEq p.A]
+    (M : DynComputation.{u} p α β) {state : M.State} {query : p.Obj M.State}
+    (hview : M.view state = Sum.inr query) {index : p.Idx}
+    (hne : index.1 ≠ query.1) : M.update? (state, index) = none := by
+  unfold update?; rw [hview]
+  simp only [Sum.elim_inr, dif_neg hne]
+
+/-- The total variant of the flattened transition: a mismatched tag or an already
+returned state leaves the state unchanged.
+
+This is the shape a machine-facing cost model wants, since it is a plain
+state-to-state map. It is derived from `update?`, so the two never disagree about
+which answers are steps. -/
+def updateFlat [DecidableEq p.A] (M : DynComputation.{u} p α β)
+    (step : M.State × p.Idx) : M.State :=
+  (M.update? step).getD step.1
+
+theorem updateFlat_eq_getD [DecidableEq p.A] (M : DynComputation.{u} p α β)
+    (step : M.State × p.Idx) :
+    M.updateFlat step = (M.update? step).getD step.1 := rfl
+
+theorem updateFlat_of_view_return [DecidableEq p.A] (M : DynComputation.{u} p α β)
+    {state : M.State} {value : β} (hview : M.view state = Sum.inl value)
+    (index : p.Idx) : M.updateFlat (state, index) = state := by
+  unfold updateFlat; rw [M.update?_of_view_return hview index]; rfl
+
+theorem updateFlat_of_view_query [DecidableEq p.A] (M : DynComputation.{u} p α β)
+    {state : M.State} {position : p.A} {next : p.B position → M.State}
+    (hview : M.view state = Sum.inr ⟨position, next⟩)
+    (direction : p.B position) :
+    M.updateFlat (state, ⟨position, direction⟩) = next direction := by
+  unfold updateFlat; rw [M.update?_of_view_query hview direction]; rfl
+
+theorem updateFlat_of_view_query_of_ne [DecidableEq p.A]
+    (M : DynComputation.{u} p α β) {state : M.State} {query : p.Obj M.State}
+    (hview : M.view state = Sum.inr query) {index : p.Idx}
+    (hne : index.1 ≠ query.1) : M.updateFlat (state, index) = state := by
+  unfold updateFlat; rw [M.update?_of_view_query_of_ne hview hne]; rfl
+
+/-! ## Derived machine-facing accessors -/
+
+/-- The optional readout of a returning computation: the returned value at a
+resolved state and `none` at an unresolved one. -/
+def output (M : DynComputation.{u} p α β) (state : M.State) : Option β :=
+  (M.head state).getLeft?
+
+/-- The query a computation selects at a state. At a resolved state, where no
+query is exposed, this is the interface's default position; the run semantics
+never consults that value. -/
+def expose [Inhabited p.A] (M : DynComputation.{u} p α β) (state : M.State) : p.A :=
+  (M.head state).elim (fun _ => default) id
+
+/-- The deterministic one-step transition of a computation against a fixed pure
+handler. A resolved state is absorbing. -/
+def stepD (M : DynComputation.{u} p α β) (handler : (a : p.A) → p.B a)
+    (state : M.State) : M.State :=
+  (M.view state).elim (fun _ => state) (fun query => query.2 (handler query.1))
+
+@[simp] theorem output_eq_some_iff (M : DynComputation.{u} p α β)
+    (state : M.State) (value : β) :
+    M.output state = some value ↔ M.head state = Sum.inl value := by
+  unfold output
+  cases M.head state <;> simp
+
+@[simp] theorem stepD_of_view_return (M : DynComputation.{u} p α β)
+    (handler : (a : p.A) → p.B a) {state : M.State} {value : β}
+    (hview : M.view state = Sum.inl value) : M.stepD handler state = state := by
+  unfold stepD; rw [hview]; rfl
+
+@[simp] theorem stepD_of_view_query (M : DynComputation.{u} p α β)
+    (handler : (a : p.A) → p.B a) {state : M.State} {query : p.Obj M.State}
+    (hview : M.view state = Sum.inr query) :
+    M.stepD handler state = query.2 (handler query.1) := by
+  unfold stepD; rw [hview]; rfl
+
+/-! ## Transport along replacement of the initialization
+
+Every step map is shared definitionally by computations that share `toMachine`.
+-/
+
+@[simp] theorem head_setInit {γ : Type uγ} (M : DynComputation.{u} p α β)
+    (g : γ → M.State) (state : M.State) :
+    (M.setInit g).head state = M.head state := rfl
+
+@[simp] theorem update?_setInit [DecidableEq p.A] {γ : Type uγ}
+    (M : DynComputation.{u} p α β) (g : γ → M.State) (step : M.State × p.Idx) :
+    (M.setInit g).update? step = M.update? step := rfl
+
+@[simp] theorem updateFlat_setInit [DecidableEq p.A] {γ : Type uγ}
+    (M : DynComputation.{u} p α β) (g : γ → M.State) (step : M.State × p.Idx) :
+    (M.setInit g).updateFlat step = M.updateFlat step := rfl
+
+@[simp] theorem output_setInit {γ : Type uγ} (M : DynComputation.{u} p α β)
+    (g : γ → M.State) (state : M.State) :
+    (M.setInit g).output state = M.output state := rfl
+
+@[simp] theorem expose_setInit [Inhabited p.A] {γ : Type uγ}
+    (M : DynComputation.{u} p α β) (g : γ → M.State) (state : M.State) :
+    (M.setInit g).expose state = M.expose state := rfl
+
+@[simp] theorem stepD_setInit {γ : Type uγ} (M : DynComputation.{u} p α β)
+    (g : γ → M.State) (handler : (a : p.A) → p.B a) (state : M.State) :
+    (M.setInit g).stepD handler state = M.stepD handler state := rfl
+
+/-! ## Transport along result mapping -/
+
+@[simp] theorem head_mapResult {γ : Type uγ} (M : DynComputation.{u} p α β)
+    (f : β → γ) (state : M.State) :
+    (M.mapResult f).head state = Sum.map f id (M.head state) := rfl
+
+@[simp] theorem update?_mapResult [DecidableEq p.A] {γ : Type uγ}
+    (M : DynComputation.{u} p α β) (f : β → γ) (step : M.State × p.Idx) :
+    (M.mapResult f).update? step = M.update? step := by
+  unfold update?
+  rw [mapResult_view]
+  cases hview : M.view step.1 with
+  | inl value => rfl
+  | inr query => rfl
+
+@[simp] theorem updateFlat_mapResult [DecidableEq p.A] {γ : Type uγ}
+    (M : DynComputation.{u} p α β) (f : β → γ) (step : M.State × p.Idx) :
+    (M.mapResult f).updateFlat step = M.updateFlat step := by
+  unfold updateFlat
+  rw [M.update?_mapResult f step]
+  rfl
+
+/-! ## Transport along interface transport -/
+
+@[simp] theorem head_wrap {q : PFunctor.{uA₂, uB₂}} (M : DynComputation.{u} p α β)
+    (lens : Lens p q) (state : M.State) :
+    (M.wrap lens).head state = Sum.map id lens.toFunA (M.head state) := rfl
+
+/-- The flattened index pullback of a lens, absorbing the resolved case: an answer
+at the position the lens exposes for `a` is pulled back to an answer at `a`, while
+a resolved readout or a mismatched tag has no preimage.
+
+The domain carries the machine's whole readout `β ⊕ p.A` rather than just a
+position. Absorbing the resolved case here is what lets interface transport avoid
+`expose` and hence avoid needing an admissible constant `default`. -/
+def _root_.PFunctor.Lens.pullHeadIdx {q : PFunctor.{uA₂, uB₂}} [DecidableEq q.A]
+    (lens : Lens p q) (β : Type uβ) : (β ⊕ p.A) × q.Idx → Option p.Idx := fun x =>
+  x.1.elim (fun _ => none)
+    (fun a =>
+      if h : x.2.1 = lens.toFunA a then
+        some ⟨a, lens.toFunB a (h ▸ x.2.2)⟩
+      else none)
+
+/-- Interface transport pulls an answer back along the lens before feeding it to
+the underlying computation. The resolved case needs no special handling: the
+underlying `update?` is already `none` there. -/
+theorem update?_wrap {q : PFunctor.{uA₂, uB₂}} [DecidableEq p.A] [DecidableEq q.A]
+    (M : DynComputation.{u} p α β) (lens : Lens p q) (state : M.State)
+    (iposition : q.A) (idirection : q.B iposition) :
+    (M.wrap lens).update? (state, ⟨iposition, idirection⟩) =
+      (lens.pullHeadIdx β (M.head state, ⟨iposition, idirection⟩)).bind
+        fun index => M.update? (state, index) := by
+  cases hview : M.view state with
+  | inl value =>
+      rw [update?_of_view_return (M.wrap lens)
+          (show (M.wrap lens).view state = Sum.inl value by rw [wrap_view, hview])
+          ⟨iposition, idirection⟩,
+        head_eq_inl_of_view M hview]
+      rfl
+  | inr query =>
+      rcases query with ⟨position, next⟩
+      have hcomp : (M.wrap lens).view state =
+          Sum.inr ⟨lens.toFunA position,
+            fun direction => next (lens.toFunB position direction)⟩ := by
+        rw [wrap_view, hview]
+      rw [head_eq_inr_of_view M hview]
+      by_cases h : iposition = lens.toFunA position
+      · subst h
+        rw [update?_of_view_query (M.wrap lens) hcomp idirection]
+        change _ = Option.bind (dite _ _ _) _
+        rw [dif_pos rfl, Option.bind_some, update?_of_view_query M hview]
+        rfl
+      · rw [update?_of_view_query_of_ne (M.wrap lens) hcomp h]
+        change none = Option.bind (dite _ _ _) _
+        rw [dif_neg h]
+        rfl
+
+/-! ## The step maps of a sequential composition -/
+
+section SeqComp
+
+variable {γ : Type uγ}
+
+theorem seqComp_view_inl_of_return (M₁ : DynComputation.{u} p α β)
+    (M₂ : DynComputation.{v} p β γ) {state₁ : M₁.State} {value : β}
+    (hview : M₁.view state₁ = Sum.inl value) :
+    (M₁.seqComp M₂).view (Sum.inl state₁) =
+      Sum.map (fun result : γ => result)
+        (p.map (Sum.inr : M₂.State → M₁.State ⊕ M₂.State))
+        (M₂.view (M₂.init value)) := by
+  rw [seqComp_view_inl, hview]
+  rfl
+
+theorem seqComp_view_inl_of_query (M₁ : DynComputation.{u} p α β)
+    (M₂ : DynComputation.{v} p β γ) {state₁ : M₁.State}
+    {position : p.A} {next : p.B position → M₁.State}
+    (hview : M₁.view state₁ = Sum.inr ⟨position, next⟩) :
+    (M₁.seqComp M₂).view (Sum.inl state₁) =
+      Sum.inr ⟨position, fun direction => Sum.inl (next direction)⟩ := by
+  rw [seqComp_view_inl, hview]
+  rfl
+
+@[simp] theorem head_seqComp_inr (M₁ : DynComputation.{u} p α β)
+    (M₂ : DynComputation.{v} p β γ) (state₂ : M₂.State) :
+    (M₁.seqComp M₂).head (Sum.inr state₂) = M₂.head state₂ := by
+  rw [head_eq_sumMap_view (M₁.seqComp M₂) (Sum.inr state₂), seqComp_view_inr,
+    head_eq_sumMap_view M₂ state₂]
+  cases M₂.view state₂ <;> rfl
+
+/-- At a left state the composite reads off `M₁`; a returned intermediate value
+is handed over to `M₂`'s initial readout in the same observation. -/
+@[simp] theorem head_seqComp_inl (M₁ : DynComputation.{u} p α β)
+    (M₂ : DynComputation.{v} p β γ) (state₁ : M₁.State) :
+    (M₁.seqComp M₂).head (Sum.inl state₁) =
+      Sum.elim (fun value => M₂.head (M₂.init value)) Sum.inr (M₁.head state₁) := by
+  rw [head_eq_sumMap_view (M₁.seqComp M₂) (Sum.inl state₁)]
+  cases hview : M₁.view state₁ with
+  | inl value =>
+      rw [seqComp_view_inl_of_return M₁ M₂ hview, head_eq_inl_of_view M₁ hview,
+        Sum.elim_inl, head_eq_sumMap_view M₂ (M₂.init value)]
+      cases M₂.view (M₂.init value) <;> rfl
+  | inr query =>
+      rcases query with ⟨position, next⟩
+      rw [seqComp_view_inl_of_query M₁ M₂ hview, head_eq_inr_of_view M₁ hview]
+      rfl
+
+@[simp] theorem update?_seqComp_inr [DecidableEq p.A]
+    (M₁ : DynComputation.{u} p α β) (M₂ : DynComputation.{v} p β γ)
+    (state₂ : M₂.State) (index : p.Idx) :
+    (M₁.seqComp M₂).update? (Sum.inr state₂, index) =
+      Option.map Sum.inr (M₂.update? (state₂, index)) := by
+  obtain ⟨position, direction⟩ := index
+  cases hview : M₂.view state₂ with
+  | inl value =>
+      rw [update?_of_view_return (M₁.seqComp M₂)
+          (show (M₁.seqComp M₂).view (Sum.inr state₂) = Sum.inl value by
+            rw [seqComp_view_inr, hview]; rfl),
+        update?_of_view_return M₂ hview]
+      rfl
+  | inr query =>
+      rcases query with ⟨position₂, next₂⟩
+      have hcomp : (M₁.seqComp M₂).view (Sum.inr state₂) =
+          Sum.inr ⟨position₂, fun direction => Sum.inr (next₂ direction)⟩ := by
+        rw [seqComp_view_inr, hview]; rfl
+      by_cases h : position = position₂
+      · subst h
+        rw [update?_of_view_query (M₁.seqComp M₂) hcomp direction,
+          update?_of_view_query M₂ hview direction]
+        rfl
+      · rw [update?_of_view_query_of_ne (M₁.seqComp M₂) hcomp h,
+          update?_of_view_query_of_ne M₂ hview h]
+        rfl
+
+/-- At a left state the composite advances `M₁`, unless `M₁` has already returned
+an intermediate value, in which case control has been handed to `M₂` initialized
+at that value.
+
+This equation is **unconditional in the answer index**, which is exactly what
+partiality buys. With the total `updateFlat` no such equation holds: on a
+mismatched tag the composite stays at `Sum.inl state₁` while `M₂` alone would stay
+at `M₂.init value`. With `none` both agree, and the case where `M₂` also returns
+immediately is subsumed for the same reason.
+
+So this single lemma covers what the total variant needed three conditional ones
+for — a matching-tag case, a mismatched-tag case, and a both-phases-returned case.
+Only the two uniform total-variant lemmas are kept below;
+`updateFlat_eq_getD` recovers the rest. -/
+@[simp] theorem update?_seqComp_inl [DecidableEq p.A]
+    (M₁ : DynComputation.{u} p α β) (M₂ : DynComputation.{v} p β γ)
+    (state₁ : M₁.State) (index : p.Idx) :
+    (M₁.seqComp M₂).update? (Sum.inl state₁, index) =
+      Sum.elim (fun value => Option.map Sum.inr (M₂.update? (M₂.init value, index)))
+        (fun _ : p.A => Option.map Sum.inl (M₁.update? (state₁, index)))
+        (M₁.head state₁) := by
+  obtain ⟨position, direction⟩ := index
+  cases hview : M₁.view state₁ with
+  | inr query =>
+      rcases query with ⟨position₁, next₁⟩
+      rw [head_eq_inr_of_view M₁ hview, Sum.elim_inr]
+      have hcomp := seqComp_view_inl_of_query M₁ M₂ hview
+      by_cases h : position = position₁
+      · subst h
+        rw [update?_of_view_query (M₁.seqComp M₂) hcomp direction,
+          update?_of_view_query M₁ hview direction]
+        rfl
+      · rw [update?_of_view_query_of_ne (M₁.seqComp M₂) hcomp h,
+          update?_of_view_query_of_ne M₁ hview h]
+        rfl
+  | inl value =>
+      rw [head_eq_inl_of_view M₁ hview, Sum.elim_inl]
+      cases hview₂ : M₂.view (M₂.init value) with
+      | inl result =>
+          rw [update?_of_view_return (M₁.seqComp M₂) (value := result)
+              (by rw [seqComp_view_inl_of_return M₁ M₂ hview, hview₂]; rfl),
+            update?_of_view_return M₂ hview₂]
+          rfl
+      | inr query₂ =>
+          rcases query₂ with ⟨position₂, next₂⟩
+          have hcomp : (M₁.seqComp M₂).view (Sum.inl state₁) =
+              Sum.inr ⟨position₂, fun d => Sum.inr (next₂ d)⟩ := by
+            rw [seqComp_view_inl_of_return M₁ M₂ hview, hview₂]; rfl
+          by_cases h : position = position₂
+          · subst h
+            rw [update?_of_view_query (M₁.seqComp M₂) hcomp direction,
+              update?_of_view_query M₂ hview₂ direction]
+            rfl
+          · rw [update?_of_view_query_of_ne (M₁.seqComp M₂) hcomp h,
+              update?_of_view_query_of_ne M₂ hview₂ h]
+            rfl
+
+@[simp] theorem updateFlat_seqComp_inr [DecidableEq p.A]
+    (M₁ : DynComputation.{u} p α β) (M₂ : DynComputation.{v} p β γ)
+    (state₂ : M₂.State) (index : p.Idx) :
+    (M₁.seqComp M₂).updateFlat (Sum.inr state₂, index) =
+      Sum.inr (M₂.updateFlat (state₂, index)) := by
+  unfold updateFlat
+  rw [update?_seqComp_inr]
+  cases M₂.update? (state₂, index) <;> rfl
+
+/-- At a left state exposing a query, the composite advances `M₁` inside the left
+summand. -/
+theorem updateFlat_seqComp_inl_of_query [DecidableEq p.A]
+    (M₁ : DynComputation.{u} p α β) (M₂ : DynComputation.{v} p β γ)
+    {state₁ : M₁.State} {position₁ : p.A} {next₁ : p.B position₁ → M₁.State}
+    (hview : M₁.view state₁ = Sum.inr ⟨position₁, next₁⟩) (index : p.Idx) :
+    (M₁.seqComp M₂).updateFlat (Sum.inl state₁, index) =
+      Sum.inl (M₁.updateFlat (state₁, index)) := by
+  unfold updateFlat
+  rw [update?_seqComp_inl, head_eq_inr_of_view M₁ hview, Sum.elim_inr]
+  cases M₁.update? (state₁, index) <;> rfl
+
+end SeqComp
+
+/-! ## Faithfulness of the flat presentation
+
+The flat step maps lose nothing: a step function is determined by the readout and
+the partial transition it induces. So presenting a computation by
+`(State, init, head, update?)` is a genuine presentation rather than a lossy
+projection — which is why constraining those three maps is the right notion of an
+admissible machine.
+-/
+
+/-- A step function is determined by the readout and the partial transition it
+induces. -/
+theorem ofStep_step_eq_of_flat_eq [DecidableEq p.A] {S : Type u}
+    (step₁ step₂ : S → β ⊕ p.Obj S) (init : α → S)
+    (hhead : ∀ state, (ofStep (p := p) step₁ init).head state =
+      (ofStep (p := p) step₂ init).head state)
+    (hupdate : ∀ pair, (ofStep (p := p) step₁ init).update? pair =
+      (ofStep (p := p) step₂ init).update? pair) :
+    step₁ = step₂ := by
+  funext state
+  have hview₁ : (ofStep (p := p) step₁ init).view state = step₁ state :=
+    view_ofStep step₁ init state
+  have hview₂ : (ofStep (p := p) step₂ init).view state = step₂ state :=
+    view_ofStep step₂ init state
+  have hpos := hhead state
+  rw [head_eq_sumMap_view, head_eq_sumMap_view, hview₁, hview₂] at hpos
+  cases h₁ : step₁ state with
+  | inl value₁ =>
+      cases h₂ : step₂ state with
+      | inl value₂ =>
+          rw [h₁, h₂] at hpos
+          change Sum.inl value₁ = Sum.inl value₂ at hpos
+          rw [Sum.inl.inj hpos]
+      | inr query₂ =>
+          rw [h₁, h₂] at hpos
+          change Sum.inl value₁ = Sum.inr query₂.1 at hpos
+          exact absurd hpos (by simp)
+  | inr query₁ =>
+      cases h₂ : step₂ state with
+      | inl value₂ =>
+          rw [h₁, h₂] at hpos
+          change Sum.inr query₁.1 = Sum.inl value₂ at hpos
+          exact absurd hpos (by simp)
+      | inr query₂ =>
+          rcases query₁ with ⟨position₁, next₁⟩
+          rcases query₂ with ⟨position₂, next₂⟩
+          have hposEq : position₁ = position₂ := by
+            rw [h₁, h₂] at hpos
+            change Sum.inr position₁ = Sum.inr position₂ at hpos
+            exact Sum.inr.inj hpos
+          subst hposEq
+          refine congrArg Sum.inr (Sigma.ext rfl (heq_of_eq (funext fun d => ?_)))
+          have := hupdate (state, ⟨position₁, d⟩)
+          rw [update?_of_view_query _ (hview₁.trans h₁) d,
+            update?_of_view_query _ (hview₂.trans h₂) d] at this
+          exact Option.some.inj this
+
+end DynSystem.DynComputation
+
+end PFunctor
diff --git a/PolyFun/Realizability/StepClass.lean b/PolyFun/Realizability/StepClass.lean
new file mode 100644
index 00000000..618c1832
--- /dev/null
+++ b/PolyFun/Realizability/StepClass.lean
@@ -0,0 +1,355 @@
+/-
+Copyright (c) 2026 PolyFun Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Devon Tuma
+-/
+module
+
+public import PolyFun.PFunctor.Basic
+
+/-!
+# Classes of admissible functions
+
+A `PFunctor.StepClass` is a class of allowed data representations and functions
+between them — a wide subcategory of `Type u`, presented pointwise by
+
+* `Str A`, the structure a type must carry to be representable (a bit encoding,
+  a finiteness witness, a `Primcodable` instance, …), and
+* `Hom a b f`, the proposition that `f : A → B` is admissible between chosen
+  representations,
+
+closed under identities and composition.
+
+`Str` is *data* rather than a proposition because a resource bound only makes
+sense relative to a chosen representation: "`f` runs in polynomial time" is a
+statement about encoded inputs, not about the bare function. `Hom` is a
+proposition because the realizability layer only ever asks *whether* a step map
+is admissible; a cost-bearing refinement, in which witnesses carry running-time
+and description-size measures, would replace it by a `Type`-valued field.
+
+The mixin classes `StepClass.HasProd` and `StepClass.HasSum` record that a class
+represents binary products and sums with admissible projections, injections,
+pairing, and case analysis. They are kept separate from `StepClass` so that each
+downstream definition requires exactly the structure it consumes.
+
+`StepClass.Refines C D` translates `C`-representations into `D`-representations
+compatibly with admissibility, so a statement proved for a small class
+specializes to every larger one.
+
+This file is deliberately free of polynomial-functor content beyond its
+namespace: the interface between a step class and the machine layer lives in
+`PolyFun.Realizability.Basic`.
+
+Taking the resource bound as a predicate on the implementation, rather than as a
+measure on runs, follows Petcher and Morrisett's Foundational Cryptography
+Framework (2015), where security definitions are parameterized by an
+*admissibility predicate* naming the class of allowed adversaries; the
+`admissible` / `_mem` vocabulary here is theirs. See `REFERENCES.md`.
+-/
+
+@[expose] public section
+
+universe u v v₂ v₃
+
+namespace PFunctor
+
+set_option linter.checkUnivs false in
+/-- A class of admissible data representations and functions between them: a wide
+subcategory of `Type u` presented by a structure on objects and a predicate on
+morphisms.
+
+`Str A` is the representation structure carried by an admissible type, and
+`Hom a b f` says that `f` is admissible from representation `a` to
+representation `b`. The two closure fields make the admissible functions a
+category containing every identity. -/
+-- The representation universe `v` is independent of the represented universe `u`:
+-- a `Type`-valued encoding structure must be usable on types in any universe.
+structure StepClass where
+  /-- The representation structure an admissible type must carry. -/
+  Str : Type u → Type v
+  /-- Admissibility of a function between represented types. -/
+  Hom : {A B : Type u} → Str A → Str B → (A → B) → Prop
+  /-- Identities are admissible. -/
+  id_mem : ∀ {A : Type u} (a : Str A), Hom a a id
+  /-- Admissible functions compose. -/
+  comp_mem : ∀ {A B D : Type u} {a : Str A} {b : Str B} {d : Str D}
+    {f : A → B} {g : B → D}, Hom a b f → Hom b d g → Hom a d (g ∘ f)
+
+namespace StepClass
+
+variable {C : StepClass.{u, v}}
+
+/-- Admissibility depends on a function only through its values: a class
+constrains functions, not their syntactic presentation.
+
+This is the workhorse of the realizability closure theory, where a step map of a
+composite machine is almost never *syntactically* the admissible combination one
+builds by hand. -/
+theorem Hom.congr {A B : Type u} {a : C.Str A} {b : C.Str B} {f g : A → B}
+    (h : C.Hom a b f) (hfg : ∀ x, f x = g x) : C.Hom a b g := by
+  rwa [← funext hfg]
+
+/-! ## Products -/
+
+/-- A step class with admissible binary products.
+
+The realizability layer requires this of every class it uses: the flattened
+transition map of a machine is a function out of the product of the state with
+the interface's index space. -/
+class HasProd (C : StepClass.{u, v}) where
+  /-- The representation of a binary product. -/
+  prod : {A B : Type u} → C.Str A → C.Str B → C.Str (A × B)
+  /-- The first projection is admissible. -/
+  fst_mem : ∀ {A B : Type u} (a : C.Str A) (b : C.Str B), C.Hom (prod a b) a Prod.fst
+  /-- The second projection is admissible. -/
+  snd_mem : ∀ {A B : Type u} (a : C.Str A) (b : C.Str B), C.Hom (prod a b) b Prod.snd
+  /-- Admissible functions out of a common source pair. -/
+  pair_mem : ∀ {A B D : Type u} {a : C.Str A} {b : C.Str B} {d : C.Str D}
+    {f : A → B} {g : A → D}, C.Hom a b f → C.Hom a d g →
+      C.Hom a (prod b d) fun x => (f x, g x)
+
+/-- Admissible functions act on products componentwise. -/
+theorem HasProd.map_mem [P : C.HasProd] {A B A' B' : Type u} {a : C.Str A}
+    {b : C.Str B} {a' : C.Str A'} {b' : C.Str B'} {f : A → A'} {g : B → B'}
+    (hf : C.Hom a a' f) (hg : C.Hom b b' g) :
+    C.Hom (P.prod a b) (P.prod a' b') (Prod.map f g) := by
+  refine (P.pair_mem (C.comp_mem (P.fst_mem a b) hf)
+    (C.comp_mem (P.snd_mem a b) hg)).congr ?_
+  intro x
+  cases x
+  rfl
+
+/-- Pairing an admissible function with a fixed second component. -/
+theorem HasProd.pairRight_mem [P : C.HasProd] {A B D : Type u} {a : C.Str A}
+    {b : C.Str B} {d : C.Str D} {f : A → B} (hf : C.Hom a b f) :
+    C.Hom (P.prod a d) (P.prod b d) fun x => (f x.1, x.2) :=
+  P.pair_mem (C.comp_mem (P.fst_mem a d) hf) (P.snd_mem a d)
+
+/-- Pairing an admissible function with a fixed first component. -/
+theorem HasProd.pairLeft_mem [P : C.HasProd] {A B D : Type u} {a : C.Str A}
+    {b : C.Str B} {d : C.Str D} {f : A → B} (hf : C.Hom a b f) :
+    C.Hom (P.prod d a) (P.prod d b) fun x => (x.1, f x.2) :=
+  P.pair_mem (P.fst_mem d a) (C.comp_mem (P.snd_mem d a) hf)
+
+/-- Duplicating a value is admissible. This is what lets a closure proof retain
+an input while dispatching on some function of it. -/
+theorem HasProd.diag_mem [P : C.HasProd] {A : Type u} (a : C.Str A) :
+    C.Hom a (P.prod a a) fun x => (x, x) :=
+  P.pair_mem (C.id_mem a) (C.id_mem a)
+
+/-- Retaining an input alongside an admissible readout of it. -/
+theorem HasProd.withInput_mem [P : C.HasProd] {A B : Type u} {a : C.Str A}
+    {b : C.Str B} {f : A → B} (hf : C.Hom a b f) :
+    C.Hom a (P.prod b a) fun x => (f x, x) :=
+  P.pair_mem hf (C.id_mem a)
+
+/-- Swapping the components of a product is admissible. -/
+theorem HasProd.swap_mem [P : C.HasProd] {A B : Type u} (a : C.Str A)
+    (b : C.Str B) : C.Hom (P.prod a b) (P.prod b a) Prod.swap := by
+  refine (P.pair_mem (P.snd_mem a b) (P.fst_mem a b)).congr ?_
+  intro x
+  cases x
+  rfl
+
+/-- Reassociating a product is admissible. -/
+theorem HasProd.assoc_mem [P : C.HasProd] {A B D : Type u} (a : C.Str A)
+    (b : C.Str B) (d : C.Str D) :
+    C.Hom (P.prod (P.prod a b) d) (P.prod a (P.prod b d))
+      fun x => (x.1.1, (x.1.2, x.2)) :=
+  P.pair_mem (C.comp_mem (P.fst_mem (P.prod a b) d) (P.fst_mem a b))
+    (P.pair_mem (C.comp_mem (P.fst_mem (P.prod a b) d) (P.snd_mem a b))
+      (P.snd_mem (P.prod a b) d))
+
+/-! ## Sums -/
+
+/-- A step class with admissible binary sums.
+
+The realizability layer requires this of every class it uses: a machine's
+one-step readout lands in `β ⊕ p.A`, a returned value or an exposed query
+position. -/
+class HasSum (C : StepClass.{u, v}) where
+  /-- The representation of a binary sum. -/
+  sum : {A B : Type u} → C.Str A → C.Str B → C.Str (A ⊕ B)
+  /-- The left injection is admissible. -/
+  inl_mem : ∀ {A B : Type u} (a : C.Str A) (b : C.Str B), C.Hom a (sum a b) Sum.inl
+  /-- The right injection is admissible. -/
+  inr_mem : ∀ {A B : Type u} (a : C.Str A) (b : C.Str B), C.Hom b (sum a b) Sum.inr
+  /-- Case analysis on admissible branches is admissible. -/
+  elim_mem : ∀ {A B D : Type u} {a : C.Str A} {b : C.Str B} {d : C.Str D}
+    {f : A → D} {g : B → D}, C.Hom a d f → C.Hom b d g →
+      C.Hom (sum a b) d (Sum.elim f g)
+
+/-- Admissible functions act on sums summandwise. -/
+theorem HasSum.map_mem [S : C.HasSum] {A B A' B' : Type u} {a : C.Str A}
+    {b : C.Str B} {a' : C.Str A'} {b' : C.Str B'} {f : A → A'} {g : B → B'}
+    (hf : C.Hom a a' f) (hg : C.Hom b b' g) :
+    C.Hom (S.sum a b) (S.sum a' b') (Sum.map f g) := by
+  refine (S.elim_mem (C.comp_mem hf (S.inl_mem a' b'))
+    (C.comp_mem hg (S.inr_mem a' b'))).congr ?_
+  intro x
+  cases x <;> rfl
+
+/-! ## Optional values -/
+
+/-- A step class with admissible optional values.
+
+The realizability layer requires this of every class it uses: a machine's
+flattened transition is *partial*, and `none` records that an answer is not one
+the machine is waiting for. Partiality is what makes the flattening
+compositional — see `PolyFun.Realizability.Machine`.
+
+Up to the equivalence `Option A ≃ A ⊕ PUnit` this is `HasSum` together with a
+terminal representation, but it is taken as primitive: factoring it would force
+a terminal representation on every instance, and nothing else needs one. For the
+same reason `omap_mem` and `obindCtx_mem` are both primitive — each is derivable
+from the other only through a unit representation. -/
+class HasOption (C : StepClass.{u, v}) [P : C.HasProd] where
+  /-- The representation of an optional value. -/
+  option : {A : Type u} → C.Str A → C.Str (Option A)
+  /-- Admissible functions act on optional values. -/
+  omap_mem : ∀ {A B : Type u} {a : C.Str A} {b : C.Str B} {f : A → B},
+    C.Hom a b f → C.Hom (option a) (option b) (Option.map f)
+  /-- The absent value is admissible as a constant. This is the one constant map
+  the layer assumes: a machine that has already returned takes no step, so its
+  transition is constantly `none`. -/
+  none_mem : ∀ {A B : Type u} (a : C.Str A) (b : C.Str B),
+    C.Hom a (option b) fun _ => none
+  /-- Sequencing a partial value against an admissible continuation that also
+  reads a retained context. Needed to transport a realization along a lens,
+  where the pulled-back answer index is partial and the continuation still needs
+  the machine's state. -/
+  obindCtx_mem : ∀ {A B E : Type u} {a : C.Str A} {b : C.Str B} {e : C.Str E}
+    {k : A × E → Option B}, C.Hom (P.prod a e) (option b) k →
+      C.Hom (P.prod (option a) e) (option b) fun y => y.1.bind fun j => k (j, y.2)
+
+/-! ## Distributivity -/
+
+/-- A step class whose product and sum representations distribute.
+
+Equivalently — and this is the form the closure theory actually uses, available as
+`IsDistributive.elimCtx_mem` — *case analysis in a context* is admissible.
+
+The field is the **inverse** of the map a category theorist calls canonical: the
+canonical (cogap) direction is `codistrib_mem` below, which needs no axiom at all.
+Both directions being admissible is exactly "the canonical map is an isomorphism
+in the subcategory", so this is Cockett's distributivity verbatim rather than a
+one-sided weakening. Only the binary case is required; no terminal or initial
+representation is assumed, so this is weaker than
+`CategoryTheory.IsCartesianDistributive`.
+
+Note that distributivity genuinely does not come for free: every bicartesian
+*closed* category is automatically distributive because `X × (-)` is a left
+adjoint, but the motivating classes here have no exponentials. -/
+class IsDistributive (C : StepClass.{u, v}) [P : C.HasProd] [S : C.HasSum] :
+    Prop where
+  distrib_mem : ∀ {A B I : Type u} (a : C.Str A) (b : C.Str B) (i : C.Str I),
+    C.Hom (P.prod (S.sum a b) i) (S.sum (P.prod a i) (P.prod b i))
+      fun x => Sum.elim (fun l => Sum.inl (l, x.2)) (fun r => Sum.inr (r, x.2)) x.1
+
+/-- The canonical direction of the distributivity map, which needs only products
+and sums. Together with `IsDistributive.distrib_mem` it exhibits the canonical map
+as an isomorphism in the subcategory. -/
+theorem codistrib_mem [P : C.HasProd] [S : C.HasSum] {A B I : Type u}
+    (a : C.Str A) (b : C.Str B) (i : C.Str I) :
+    C.Hom (S.sum (P.prod a i) (P.prod b i)) (P.prod (S.sum a b) i)
+      (Sum.elim (Prod.map Sum.inl id) (Prod.map Sum.inr id)) :=
+  S.elim_mem (P.map_mem (S.inl_mem a b) (C.id_mem i))
+    (P.map_mem (S.inr_mem a b) (C.id_mem i))
+
+/-- Case analysis in a context: dispatching on a sum-valued component while
+retaining the rest of the input.
+
+This is the workhorse of the closure theory. Distributivity is equivalent to it;
+in the presence of `HasProd.diag_mem` it even implies the unparameterized
+`HasSum.elim_mem`, by taking the context to be the sum itself — so the axioms are
+not independent. `elim_mem` is nonetheless kept primitive, since deriving it would
+churn every instance for no gain. -/
+theorem IsDistributive.elimCtx_mem [P : C.HasProd] [S : C.HasSum]
+    [D : C.IsDistributive] {A B E Z : Type u} {a : C.Str A} {b : C.Str B}
+    {e : C.Str E} {z : C.Str Z} {f : A × E → Z} {g : B × E → Z}
+    (hf : C.Hom (P.prod a e) z f) (hg : C.Hom (P.prod b e) z g) :
+    C.Hom (P.prod (S.sum a b) e) z
+      fun x => Sum.elim (fun l => f (l, x.2)) (fun r => g (r, x.2)) x.1 := by
+  refine (C.comp_mem (D.distrib_mem a b e) (S.elim_mem hf hg)).congr ?_
+  intro x
+  cases x with
+  | mk s v => cases s <;> rfl
+
+/-- A distributive step class: a distributive category (Cockett 1993) presented
+concretely over `Type u`, together with admissible optional values.
+
+This bundles the structure the closure theory consumes. It is a convenience only;
+each individual theorem asks for exactly the mixins it uses. -/
+class Distributive (C : StepClass.{u, v}) where
+  /-- The class has admissible binary products. -/
+  [toHasProd : C.HasProd]
+  /-- The class has admissible binary sums. -/
+  [toHasSum : C.HasSum]
+  /-- The class has admissible optional values. -/
+  [toHasOption : C.HasOption]
+  /-- The class's products and sums distribute. -/
+  [toIsDistributive : C.IsDistributive]
+
+attribute [implicit_reducible, instance] Distributive.toHasProd
+  Distributive.toHasSum Distributive.toHasOption
+
+attribute [instance] Distributive.toIsDistributive
+
+/-! ## Refinement between classes -/
+
+set_option linter.checkUnivs false in
+/-- A refinement of step classes: a translation of representations carrying
+`C`-admissibility to `D`-admissibility, compatibly with the product and sum
+representations. Realizability transports forward along a refinement, so a
+realization in a small class is a realization in every larger one.
+
+Compatibility with products and sums is not automatic and is not implied by
+`hom`, but it is needed for the transport: the realizability layer's derived
+representations are built from the boundary with `HasProd.prod` and
+`HasSum.sum`, and a refinement that translated those to unrelated
+representations would not carry a realization anywhere. -/
+-- The two representation universes are independent of each other and of the
+-- represented universe: refining a `Type`-valued encoding into a `Prop`-valued
+-- one is a typical use.
+structure Refines (C : StepClass.{u, v}) (D : StepClass.{u, v₂})
+    [C.HasProd] [C.HasSum] [C.HasOption] [D.HasProd] [D.HasSum] [D.HasOption] where
+  /-- Translate a `C`-representation into a `D`-representation. -/
+  str : {A : Type u} → C.Str A → D.Str A
+  /-- Every `C`-admissible function is `D`-admissible between the translations. -/
+  hom : ∀ {A B : Type u} {a : C.Str A} {b : C.Str B} {f : A → B},
+    C.Hom a b f → D.Hom (str a) (str b) f
+  /-- The translation preserves product representations. -/
+  str_prod : ∀ {A B : Type u} (a : C.Str A) (b : C.Str B),
+    str (HasProd.prod a b) = HasProd.prod (str a) (str b)
+  /-- The translation preserves sum representations. -/
+  str_sum : ∀ {A B : Type u} (a : C.Str A) (b : C.Str B),
+    str (HasSum.sum a b) = HasSum.sum (str a) (str b)
+  /-- The translation preserves optional representations. -/
+  str_option : ∀ {A : Type u} (a : C.Str A),
+    str (HasOption.option a) = HasOption.option (str a)
+
+/-- Refinement is reflexive. -/
+def Refines.refl (C : StepClass.{u, v}) [C.HasProd] [C.HasSum] [C.HasOption] :
+    C.Refines C where
+  str a := a
+  hom h := h
+  str_prod _ _ := rfl
+  str_sum _ _ := rfl
+  str_option _ := rfl
+
+set_option linter.checkUnivs false in
+/-- Refinements compose. -/
+-- Three independent representation universes, for the same reason as `Refines`.
+def Refines.trans {C : StepClass.{u, v}} {D : StepClass.{u, v₂}}
+    {E : StepClass.{u, v₃}} [C.HasProd] [C.HasSum] [C.HasOption] [D.HasProd]
+    [D.HasSum] [D.HasOption] [E.HasProd] [E.HasSum] [E.HasOption]
+    (R : C.Refines D) (S : D.Refines E) : C.Refines E where
+  str a := S.str (R.str a)
+  hom h := S.hom (R.hom h)
+  str_prod a b := by rw [R.str_prod, S.str_prod]
+  str_sum a b := by rw [R.str_sum, S.str_sum]
+  str_option a := by rw [R.str_option, S.str_option]
+
+end StepClass
+
+end PFunctor
diff --git a/PolyFunTest/Realizability/Examples.lean b/PolyFunTest/Realizability/Examples.lean
new file mode 100644
index 00000000..a5befff0
--- /dev/null
+++ b/PolyFunTest/Realizability/Examples.lean
@@ -0,0 +1,237 @@
+/-
+Copyright (c) 2026 PolyFun Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Devon Tuma
+-/
+module
+
+public import PolyFun.Realizability.Closure
+public import PolyFun.Realizability.Instances
+
+/-!
+# Worked examples of admissible realizability
+
+A hand-built two-state machine realizing a one-query program, checked against the
+finite step class, plus smoke tests pinning the definitional behaviour the
+closure theory relies on:
+
+* the flat step maps of `ofStep` read back exactly the supplied step function;
+* replacing the initialization leaves every step map alone *by `rfl`*, which is
+  what makes `IsRealizableBy.precomp` free;
+* two one-query programs compose under `bind`, with budgets adding, and the
+  composite transition satisfies an equation unconditional in the answer index;
+* `StepClass.computable.Hom` really is Mathlib's `Computable`;
+* a realization transports from the computable class to the unconstrained one
+  along a `StepClass.Refines`.
+-/
+
+@[expose] public section
+
+namespace PFunctor.RealizabilityExamples
+
+open PFunctor
+open PFunctor.DynSystem
+open PFunctor.DynSystem.DynComputation
+
+/-! ## A one-query interface and program -/
+
+/-- A single-query interface: one query, answered by a bit. -/
+def coin : PFunctor.{0, 0} :=
+  { A := Unit, B := fun _ => Bool }
+
+instance : DecidableEq coin.A := inferInstanceAs (DecidableEq Unit)
+
+/-- Ask the single query once and return its answer. -/
+def program : Unit → FreeM coin Bool :=
+  fun _ => FreeM.lift ()
+
+/-- The realizing machine: `none` before the query, `some answer` after. Two
+states suffice, and the whole machine is given by one step function. -/
+def machine : DynComputation.{0} coin Unit Bool :=
+  DynComputation.ofStep
+    (fun state => match state with
+      | none => Sum.inr ⟨(), fun answer => some answer⟩
+      | some answer => Sum.inl answer)
+    fun _ => none
+
+example : machine.State = Option Bool := rfl
+
+/-! ## The flat step maps read back the supplied step function -/
+
+example : machine.head none = Sum.inr () := rfl
+
+example (answer : Bool) : machine.head (some answer) = Sum.inl answer := rfl
+
+example (answer : Bool) :
+    machine.update? (none, ⟨(), answer⟩) = some (some answer) :=
+  machine.update?_of_view_query rfl answer
+
+/-- A resolved state takes no step, and neither does a mismatched answer — with a
+one-position interface only the former can occur. -/
+example (answer : Bool) : ∀ given : Bool,
+    machine.update? (some answer, ⟨(), given⟩) = none :=
+  fun _ => machine.update?_of_view_return rfl _
+
+/-- The total variant collapses `none` to the unchanged state. -/
+example (answer : Bool) : ∀ given : Bool,
+    machine.updateFlat (some answer, ⟨(), given⟩) = some answer :=
+  fun _ => machine.updateFlat_of_view_return rfl _
+
+example : machine.output none = none := rfl
+
+example (answer : Bool) : machine.output (some answer) = some answer := rfl
+
+/-! ## Finite-state realizability -/
+
+/-- The boundary: every type at the boundary of this statement is finite. -/
+def finiteBoundary : Boundary StepClass.finite.{0} coin Unit Bool where
+  input := inferInstanceAs (Fintype Unit)
+  out := inferInstanceAs (Fintype Bool)
+  pos := inferInstanceAs (Fintype Unit)
+  idx := inferInstanceAs (Fintype (Σ _ : Unit, Bool))
+
+/-- The machine implements the program within one query. Both sides are the same
+`FreeM` term, so the check is definitional. -/
+example : machine.ImplementsWithin program 1 := fun _ => rfl
+
+/-- `program` is realizable by a finite-state machine within one query. -/
+theorem isRealizableWithin_finite :
+    IsRealizableWithin StepClass.finite finiteBoundary program 1 :=
+  ⟨{ machine := machine
+     state := inferInstanceAs (Fintype (Option Bool))
+     init_mem := True.intro
+     head_mem := True.intro
+     update_mem := True.intro }, fun _ => rfl⟩
+
+/-- The bounded predicate implies the unbounded one. -/
+example : IsFiniteStateRealizable finiteBoundary program :=
+  isRealizableWithin_finite.isRealizableBy
+
+/-- A bounded realization certifies the program's own query depth. -/
+example (input : Unit) : (program input).IsTotalRollBound 1 :=
+  isRealizableWithin_finite.isTotalRollBound input
+
+/-- Budget monotonicity. -/
+example : IsRealizableWithin StepClass.finite finiteBoundary program 3 :=
+  isRealizableWithin_finite.mono (by omega)
+
+/-- Result postcomposition in action: negating the returned bit stays realizable
+at the same budget, because mapping a result performs no queries. -/
+example :
+    IsRealizableWithin StepClass.finite
+      (finiteBoundary.withOut (inferInstanceAs (Fintype Bool)))
+      (fun input => FreeM.map not (program input)) 1 :=
+  isRealizableWithin_finite.mapResult True.intro
+
+/-- Input precomposition in action. -/
+example :
+    IsRealizableWithin StepClass.finite
+      (finiteBoundary.withInput (inferInstanceAs (Fintype Bool)))
+      (fun _ : Bool => program ()) 1 :=
+  isRealizableWithin_finite.precomp (f := fun _ : Bool => ()) True.intro
+
+/-! ## Closure under `bind`
+
+Two one-query programs compose into a two-query one, and the realizations compose
+with them. The budgets add, and the composite machine's state is the coproduct of
+the two phases' states.
+-/
+
+/-- The second phase: the same machine, reindexed to consume the first phase's
+result as its input. -/
+def machine₂ : DynComputation.{0} coin Bool Bool :=
+  machine.contramapInput fun _ : Bool => ()
+
+/-- Ask the query once, then ask it again — realizable by a finite-state machine
+within `1 + 1` queries. -/
+example : IsRealizableWithin StepClass.finite
+    (finiteBoundary.withOut (inferInstanceAs (Fintype Bool)))
+    (fun input => FreeM.bind (program input) fun _ => program ()) (1 + 1) :=
+  isRealizableWithin_finite.seqComp
+    (isRealizableWithin_finite.precomp (f := fun _ : Bool => ()) True.intro)
+
+/-- The composite machine's state really is the coproduct. -/
+example :
+    (machine.seqComp machine₂).State = (Option Bool ⊕ Option Bool) := rfl
+
+/-- The composite readout hands a returned intermediate value straight to the
+second phase, in the same observation. -/
+example (answer : Bool) :
+    (machine.seqComp machine₂).head (Sum.inl (some answer)) = Sum.inr () := rfl
+
+/-- And the composite transition is unconditional in the answer index — the
+equation that partiality buys. -/
+example (answer given : Bool) :
+    (machine.seqComp machine₂).update? (Sum.inl (some answer), ⟨(), given⟩) =
+      Option.map Sum.inr (machine₂.update? (machine₂.init answer, ⟨(), given⟩)) :=
+  machine.update?_seqComp_inl machine₂ (some answer) ⟨(), given⟩
+
+/-! ## Non-vacuity of the unconstrained class -/
+
+example :
+    IsRealizableBy StepClass.unconstrained.{0, 0}
+      (Boundary.unconstrained coin Unit Bool) program :=
+  isRealizableBy_unconstrained program
+
+/-! ## Replacing the initialization is definitionally transparent
+
+These are the `rfl` checks that make `precomp` free: a machine and its
+reinitialization share every step map on the nose. If a `match` ever creeps into
+one of the step-map definitions, these break.
+-/
+
+section SetInit
+
+variable (M : DynComputation.{0} coin Unit Bool) (g : Bool → M.State)
+
+example : (M.setInit g).head = M.head := rfl
+
+example : (M.setInit g).output = M.output := rfl
+
+example (step : M.State × coin.Idx) :
+    (M.setInit g).update? step = M.update? step := rfl
+
+example (step : M.State × coin.Idx) :
+    (M.setInit g).updateFlat step = M.updateFlat step := rfl
+
+example (handler : (a : coin.A) → coin.B a) :
+    (M.setInit g).stepD handler = M.stepD handler := rfl
+
+end SetInit
+
+/-! ## The computable class is Mathlib's `Computable` -/
+
+example : StepClass.computable.{0}.Hom (A := ℕ) (B := ℕ)
+    (inferInstanceAs (Primcodable ℕ)) (inferInstanceAs (Primcodable ℕ)) id :=
+  Computable.id
+
+example : StepClass.computable.{0}.Hom (A := ℕ × ℕ) (B := ℕ)
+    (inferInstanceAs (Primcodable (ℕ × ℕ))) (inferInstanceAs (Primcodable ℕ))
+    Prod.fst :=
+  Computable.fst
+
+example : StepClass.computable.{0}.Hom (A := ℕ) (B := ℕ ⊕ ℕ)
+    (inferInstanceAs (Primcodable ℕ)) (inferInstanceAs (Primcodable (ℕ ⊕ ℕ)))
+    Sum.inl :=
+  Primrec.sumInl.to_comp
+
+/-! ## Transport along a refinement of step classes
+
+Every computable machine is in particular an unconstrained one. -/
+
+/-- The computable class refines the unconstrained one. -/
+def computableRefinesUnconstrained :
+    StepClass.computable.{0}.Refines StepClass.unconstrained.{0, 0} where
+  str _ := PUnit.unit
+  hom _ := True.intro
+  str_prod _ _ := rfl
+  str_sum _ _ := rfl
+  str_option _ := rfl
+
+example (bd : Boundary StepClass.computable.{0} coin Unit Bool)
+    (h : IsRealizableBy StepClass.computable bd program) :
+    IsRealizableBy StepClass.unconstrained.{0, 0}
+      (bd.mapRefines computableRefinesUnconstrained) program :=
+  h.mono computableRefinesUnconstrained
+
+end PFunctor.RealizabilityExamples
diff --git a/REFERENCES.md b/REFERENCES.md
index ca5120c0..c72d023a 100644
--- a/REFERENCES.md
+++ b/REFERENCES.md
@@ -70,8 +70,9 @@ free-monad-as-module-over-cofree-comonad structure made explicit (a module
 action, not an adjunction).
 
 Used in: `PolyFun/PFunctor/SubstMonoid.lean`,
-`PolyFun/PFunctor/Free/Path.lean`, and
-`PolyFun/PFunctor/PatternRunsOnMatter/`.
+`PolyFun/PFunctor/Free/Path.lean`,
+`PolyFun/PFunctor/PatternRunsOnMatter/`, and
+`PolyFun/Realizability/Basic.lean`.
 
 ### XZHHMPZ20 — Xia, Zakowski, He, Hur, Malecha, Pierce, Zdancewic, *Interaction Trees*
 
@@ -135,7 +136,8 @@ arXiv:2604.01303, 2026.
 Dependent polynomials over a base polynomial, their free displayed extension,
 displayed handlers, and compositional verification applications.
 
-Used in: `PolyFun/PFunctor/Display/`.
+Used in: `PolyFun/PFunctor/Display/`,
+`PolyFun/Realizability/Basic.lean`.
 
 ### Spi12 — Spivak, *Functorial data migration*
 
@@ -162,3 +164,231 @@ lens layer in `PolyFun/PFunctor/Lens/` makes dependent.
 
 Used in: `PolyFun/PFunctor/Lens/State.lean`,
 `PolyFun/PFunctor/Lens/Basic.lean`.
+
+## Realizability citations
+
+The realizability layer in `PolyFun/Realizability/` recombines pieces owned by
+four separate communities; these are the canonical sources for each. No single
+source states the combination — a machine realization whose *structure maps* are
+constrained by an abstract predicate — so the layer's docstrings cite the
+ingredients rather than claiming a name for the whole.
+
+### AM74 — Arbib and Manes, *Machines in a category*
+
+Michael A. Arbib and Ernest G. Manes.
+*Machines in a Category: An Expository Introduction*.
+*SIAM Review* 16(2):163–192, 1974.
+DOI: <https://doi.org/10.1137/1016026>
+
+A machine in an arbitrary category as an initialization / transition / readout
+triple, and its induced behaviour. The `expose` / `update` / readout triple of a
+`DynComputation` is an Arbib–Manes machine for the one-step polynomial functor;
+what the realizability layer adds is that the structure maps must lie in a
+distinguished class. Companion sources for "realization is universal": Goguen
+1972/73 and Naudé, *Universal realization*, JCSS 19(3), 1979.
+
+Used in: `PolyFun/Realizability/Basic.lean`.
+
+### AMMS13 — Adámek, Milius, Moss, Sousa, *Well-pointed coalgebras*
+
+Jiří Adámek, Stefan Milius, Lawrence S. Moss, and Lurdes Sousa.
+*Well-Pointed Coalgebras*.
+*Logical Methods in Computer Science* 9(3), 2013.
+arXiv:1305.0576
+
+The coalgebraic use of the word *realization*: a pointed coalgebra realizes the
+corresponding element of the terminal coalgebra, and the well-pointed coalgebras
+are exactly the minimal realizations. This is the realizability predicate of
+`PolyFun/Realizability/` with the admissibility constraint removed.
+
+Used in: `PolyFun/Realizability/Basic.lean`.
+
+### PR89 — Pnueli and Rosner, *On the synthesis of a reactive module*
+
+Amir Pnueli and Roni Rosner.
+*On the Synthesis of a Reactive Module*.
+In *Principles of Programming Languages* (POPL), 1989.
+DOI: <https://doi.org/10.1145/75277.75293>
+
+*Realizability* as the existence of a finite-state machine meeting a
+specification — the reading recovered by `StepClass.finite`, for which
+`IsFiniteStateRealizable` is provided as the community's name. Ancestor: Church,
+*Applications of recursive arithmetic to the problem of circuit synthesis*, 1963.
+
+Used in: `PolyFun/Realizability/Instances.lean`.
+
+### Uus15 — Uustalu, *Stateful runners of effectful computations*
+
+Tarmo Uustalu.
+*Stateful Runners of Effectful Computations*.
+*Mathematical Foundations of Programming Semantics* XXXI,
+*Electronic Notes in Theoretical Computer Science* 319:403–421, 2015.
+DOI: <https://doi.org/10.1016/j.entcs.2015.12.024>
+
+A stateful runner of `T`-computations is exactly a comodel, i.e. a coalgebra of
+the corresponding comonad. This is why a `p`-coalgebra with state `S` *is* a way
+of running every `FreeM p` program in `S`, and hence why realizability is a
+statement about coalgebras. See also Katsumata, Rivas, and Uustalu,
+*Interaction laws of monads and comonads*, LICS 2020 (arXiv:1912.13477).
+
+Used in: `PolyFun/Realizability/Basic.lean`.
+
+### PM15 — Petcher and Morrisett, *The Foundational Cryptography Framework*
+
+Adam Petcher and Greg Morrisett.
+*The Foundational Cryptography Framework*.
+In *Principles of Security and Trust* (POST/ESOP), LNCS 9036, 2015.
+arXiv:1410.3735
+
+Security definitions parameterized by an *admissibility predicate* naming the
+class of allowed adversaries, over a free-monad-shaped computation type. This is
+the design precedent for taking the resource bound as a predicate on the
+implementation rather than as a measure on runs, and the source of the
+`admissible` / `_mem` vocabulary used throughout the layer.
+
+Used in: `PolyFun/Realizability/StepClass.lean`.
+
+### Blum67 — Blum, *A machine-independent theory of complexity*
+
+Manuel Blum.
+*A Machine-Independent Theory of the Complexity of Recursive Functions*.
+*Journal of the ACM* 14(2):322–336, 1967.
+DOI: <https://doi.org/10.1145/321386.321395>
+
+Complexity measures axiomatized rather than fixed, with a complexity class as
+"there exists a program from an enumeration satisfying a resource predicate" —
+the same existential shape as `IsRealizableBy`, but quantifying over a Gödel
+numbering of programs rather than over machines with constrained structure maps.
+
+Used in: `PolyFun/Realizability/Basic.lean`.
+
+### GHP09 — Ghani, Hancock, Pattinson, *Representations of stream processors*
+
+Neil Ghani, Peter Hancock, and Dirk Pattinson.
+*Representations of Stream Processors Using Nested Fixed Points*.
+*Logical Methods in Computer Science* 5(3:9), 2009.
+arXiv:0905.4813
+
+Continuous and computable functions on final coalgebras represented by an
+alternating `νX.μY.` fixpoint — a machine whose individual steps are finite
+well-founded programs. This is the known special case of admissible
+realizability at the class "given by a finite `FreeM` term".
+
+Used in: `PolyFun/Realizability/Basic.lean`.
+
+## Distributive-category citations
+
+The closure structure a step class needs — finite products, finite coproducts, and
+distributivity — is exactly a distributive category. These are the canonical
+sources for the concept and for the complexity-theory vocabulary it replaces.
+
+### Coc93 — Cockett, *Introduction to distributive categories*
+
+J. Robin B. Cockett.
+*Introduction to Distributive Categories*.
+*Mathematical Structures in Computer Science* 3(3):277–307, 1993.
+DOI: <https://doi.org/10.1017/S0960129500000232>
+
+The definition: a category with finite products and binary coproducts in which the
+canonical map has an inverse. Also the distributive / recognizable / extensive /
+familial hierarchy, and the theorem that the distributive completion of a
+cartesian category is its coproduct completion.
+
+`PFunctor.StepClass.IsDistributive` axiomatizes the inverse direction; the
+canonical (cogap) direction is derivable from products and sums alone and ships as
+`StepClass.codistrib_mem`, so the two together give Cockett's axiom verbatim. Only
+the binary case is required here. Compare
+`Mathlib.CategoryTheory.IsCartesianDistributive`, which states the axiom in the
+cogap orientation.
+
+Used in: `PolyFun/Realizability/StepClass.lean`.
+
+### CLW93 — Carboni, Lack, Walters, *Extensive and distributive categories*
+
+Aurelio Carboni, Stephen Lack, and R. F. C. Walters.
+*Introduction to Extensive and Distributive Categories*.
+*Journal of Pure and Applied Algebra* 84(2):145–158, 1993.
+DOI: <https://doi.org/10.1016/0022-4049(93)90035-R>
+
+Disentangles distributivity from extensivity, which had been conflated. Includes
+the nullary clause `0 ≅ A × 0` that full finite distributivity also demands and
+that this layer deliberately omits, extensivity being a statement about pullbacks
+that a class of resource-bounded functions has no business claiming.
+
+Textbook companion: R. F. C. Walters, *Categories and Computer Science*,
+Cambridge Computer Science Texts 28, CUP, 1991 — the treatment that made
+distributive categories the CS-facing default.
+
+Used in: `PolyFun/Realizability/StepClass.lean`.
+
+### CF92 — Cockett and Fukushima, *About Charity*
+
+J. Robin B. Cockett and Tom Fukushima.
+*About Charity*.
+Yellow Series Report 92/480/18, Department of Computer Science,
+University of Calgary, 1992.
+
+The internal language of distributive categories, as a programming language, and
+the source of the reading this layer uses: distributivity is what makes *proof by
+case analysis* available. `IsDistributive.elimCtx_mem` — case analysis in a
+context — is that reading made into the working lemma. Companion:
+Cockett and Spencer, *Strong categorical datatypes II: A term logic for
+categorical programming*, TCS 139(1–2):69–113, 1995.
+
+Used in: `PolyFun/Realizability/StepClass.lean`.
+
+### CDGH12 — Cockett, Díaz-Boïls, Gallagher, Hrubeš, *Timed sets*
+
+J. Robin B. Cockett, Joaquín Díaz-Boïls, Jonathan Gallagher, and Pavel Hrubeš.
+*Timed Sets, Functional Complexity, and Computability*.
+*Electronic Notes in Theoretical Computer Science* 286:117–137, 2012 (MFPS XXVIII).
+DOI: <https://doi.org/10.1016/j.entcs.2012.08.009>
+
+Categories of timed sets modulo a complexity order form distributive restriction
+categories, with PTIME and LOGSPACE as worked examples. The closest existing
+statement that a complexity class *is* a distributive category, and hence the
+nearest prior art for treating a resource-bounded function class as one.
+
+Used in: `docs/wiki/realizability.md`.
+
+### CH08 — Cockett and Hofstra, *Introduction to Turing categories*
+
+J. Robin B. Cockett and Pieter J. W. Hofstra.
+*Introduction to Turing Categories*.
+*Annals of Pure and Applied Logic* 156(2–3):183–209, 2008.
+DOI: <https://doi.org/10.1016/j.apal.2008.04.005>
+
+Axioms for when a class of total maps is the total-map subcategory of a Turing
+category, instantiated at LINTIME, PTIME, and EXPTIME. This is the precedent for
+presenting a complexity class as a cartesian category with a faithful functor to
+`Set` — and, by omission, evidence that the coproduct and distributivity
+requirements here are not inherited from that tradition: the Turing-category
+axioms mention neither, using two disjoint points of a universal object as a
+hand-rolled stand-in for `1 ⊕ 1`.
+
+Companion: Cockett, Hofstra, and Hrubeš, *Total maps of Turing categories*,
+ENTCS 308:129–146, 2014.
+
+Used in: `docs/wiki/realizability.md`.
+
+### Clo99 — Clote, *Computation models and function algebras*
+
+Peter Clote.
+*Computation Models and Function Algebras*.
+In *Handbook of Computability Theory* (E. R. Griffor, ed.),
+Studies in Logic and the Foundations of Mathematics 140,
+Elsevier, 1999, pp. 589–681.
+DOI: <https://doi.org/10.1016/S0049-237X(99)80033-0>
+
+The complexity-native vocabulary for a class of functions closed under
+composition: a *function algebra*. Foundational instances: Cobham, *The intrinsic
+computational difficulty of functions*, 1965 (FP by bounded recursion on
+notation), and Bellantoni and Cook, *A new recursion-theoretic characterization of
+the polytime functions*, Computational Complexity 2:97–110, 1992.
+
+Function algebras are single-sorted, so branching enters as a *base function*
+(`caseBit`, Bellantoni–Cook's `C`) and distributivity is invisible in that
+tradition. Making the axiom visible is a consequence of this layer being
+multi-sorted and representation-indexed.
+
+Used in: `docs/wiki/realizability.md`.
diff --git a/docs/wiki/README.md b/docs/wiki/README.md
index b327be58..67a3268b 100644
--- a/docs/wiki/README.md
+++ b/docs/wiki/README.md
@@ -46,6 +46,9 @@ See the *Wiki Maintenance Contract* section in
 - [`interaction.md`](interaction.md): the generic interaction framework
   (sequential `TypeTree`, two-party, multiparty local views, concurrent
   processes, UC open systems).
+- [`realizability.md`](realizability.md): realizability of free programs by
+  state machines whose transition functions satisfy a given predicate
+  (`StepClass`, `Realization`, `IsRealizableBy`).
 
 ## Cross-Cutting Notes
 
@@ -69,6 +72,7 @@ See the *Wiki Maintenance Contract* section in
   - `ipfunctor.md` for the state-indexed `IPFunctor` / `FreeM` / `FreeM₂` substrate.
   - `itree.md` for interaction trees, bisimulation, and handlers.
   - `interaction.md` for the interaction framework above `FreeM`.
+  - `realizability.md` for step classes and machine realizability.
   - `notation.md` for notation cross-references.
   - `gotchas.md` for recurring traps.
 - Add new pages when a recurring topic no longer fits cleanly in an existing
diff --git a/docs/wiki/realizability.md b/docs/wiki/realizability.md
new file mode 100644
index 00000000..54e0fe32
--- /dev/null
+++ b/docs/wiki/realizability.md
@@ -0,0 +1,298 @@
+# Realizability By Admissible State Machines
+
+`PolyFun/Realizability/` answers the question "can this program be run by a
+machine whose transition functions satisfy a given predicate?" — generically in
+the predicate. It is the missing third ingredient above the existing machine
+layer:
+
+| Question | Where it is answered |
+| --- | --- |
+| *What* interaction does the program perform? | `PFunctor.FreeM p β` |
+| *How* does a machine perform it? | `PFunctor.DynSystem.DynComputation p α β` |
+| Do the two agree (and within what budget)? | `Implements` / `ImplementsWithin` |
+| Is the machine's *machinery* allowed? | **this subtree** |
+
+Instantiating the predicate recovers a spectrum of notions from one definition:
+finite-state realizability, machines with computable transitions, and — the
+motivating case downstream — the polynomial-time adversary model used in
+cryptography.
+
+## The Four Modules
+
+```text
+PolyFun/Realizability/
+  StepClass.lean    PFunctor.StepClass; HasProd / HasSum / HasOption /
+                    IsDistributive mixins; the Distributive bundle; Refines
+  Machine.lean      the first-order step maps: head, update?, updateFlat,
+                    output, expose, stepD, their transport lemmas, and
+                    faithfulness of the flat presentation
+  Basic.lean        Boundary, Realization, IsRealizableBy, IsRealizableWithin
+  Closure.lean      closure under ofFn, precomp, mapResult, seqComp (bind),
+                    wrap (interface transport), and class refinement
+  Instances.lean    unconstrained, finite, computable, WordClass
+```
+
+`Machine.lean` and `StepClass.lean` are independent; `Basic.lean` joins them.
+
+## `StepClass`: A Class Of Admissible Functions
+
+```lean
+structure PFunctor.StepClass where
+  Str : Type u → Type v
+  Hom : {A B : Type u} → Str A → Str B → (A → B) → Prop
+  id_mem : ∀ {A} (a : Str A), Hom a a id
+  comp_mem : Hom a b f → Hom b d g → Hom a d (g ∘ f)
+```
+
+A wide subcategory of `Type u`, presented pointwise. Two deliberate choices:
+
+- **`Str` is data, not a proposition.** A resource bound only makes sense
+  relative to a chosen representation: "`f` runs in polynomial time" is a
+  statement about encoded inputs, not about the bare function.
+- **`Hom` is a proposition.** The realizability layer only ever asks *whether* a
+  step map is admissible. A cost-bearing refinement — witnesses carrying
+  running-time and description-size measures — would replace it by a
+  `Type`-valued field. That refinement is deliberately not in this subtree.
+
+`StepClass.Hom.congr` transports admissibility along pointwise equality of
+functions. It is the workhorse of the closure theory: a step map of a derived
+machine is almost never *syntactically* the admissible combination one builds by
+hand.
+
+## Four mixins, and what each one buys
+
+| Mixin | Required by | Content |
+| --- | --- | --- |
+| `HasProd` | the core | the flattened transition has a product domain |
+| `HasSum` | the core | the one-step readout lands in a sum |
+| `HasOption` | the core | the flattened transition is *partial* |
+| `IsDistributive` | `seqComp` only | case analysis in a context |
+
+They are kept out of `StepClass` so that a cost-bearing successor can require
+different structure, and split so that each theorem asks for exactly what it
+consumes.
+
+### It really is a distributive category
+
+A class with `HasProd`, `HasSum`, and `IsDistributive` is exactly a **distributive
+category** in the sense of Cockett (MSCS 1993) and Carboni–Lack–Walters (JPAA
+1993), presented concretely — i.e. with a faithful functor to `Type` preserving
+finite products and coproducts. Two points worth knowing:
+
+* **This is not a one-sided weakening.** The *other* direction of the canonical
+  map, the cogap `(A × I) ⊕ (B × I) → (A ⊕ B) × I`, is derivable from `HasProd`
+  and `HasSum` alone and ships as `StepClass.codistrib_mem`. Both directions
+  being admissible is literally "the canonical map is an isomorphism in the
+  subcategory", which is Cockett's axiom verbatim.
+* **Mathlib's canonical orientation is the opposite one.** Mathlib does have this
+  concept — `CategoryTheory.IsCartesianDistributive`, citing the same two papers —
+  and states the axiom in the cogap direction. Our `distrib_mem` field is the
+  *inverse*. Do not read the arrow as a mistake.
+
+We deliberately do **not** import Mathlib's version. `MorphismProperty (Type u)`
+cannot type our `Hom`, which is indexed by *representations* and not just by
+types; the `BundledHom` framework that matched this pattern exactly was
+deprecated to nothing in February 2026; and `IsCartesianDistributive` has zero
+consumers in Mathlib, so adopting it would cost a full monoidal/limit-cone layer
+for no new theorem. Only the binary case is axiomatized here — no terminal or
+initial representation is required, and none is needed — so
+`StepClass.Distributive` is deliberately weaker than `IsCartesianDistributive`.
+
+Distributivity is a real axiom, not a theorem: every bicartesian *closed* category
+is automatically distributive because `X × (−)` is a left adjoint, but the
+motivating classes have no exponentials.
+
+### A note on the complexity-theory tradition
+
+The complexity-native presentation of a class of functions is a **function
+algebra** (Cobham 1965; Bellantoni–Cook 1992; Clote's handbook survey). Those are
+*single-sorted*, so branching enters as a *base function* (`caseBit`,
+Bellantoni–Cook's `C`) and distributivity is invisible. Making the axiom visible
+is a consequence of being multi-sorted and representation-indexed. The closest
+existing statement that a complexity class *is* a distributive category is
+Cockett–Díaz-Boïls–Gallagher–Hrubeš (ENTCS 286, 2012), which exhibits PTIME and
+LOGSPACE that way.
+
+## The First-Order Step Maps
+
+`DynComputation`'s dynamics live in `view : State → β ⊕ p.Obj State`, whose
+second component stores a *function-valued* continuation and is *dependent* on
+the exposed position. Neither shape can be constrained by a predicate on plain
+functions, so `Machine.lean` re-presents the same dynamics first-order:
+
+```lean
+def head (M : DynComputation p α β) : M.State → β ⊕ p.A :=
+  M.toDynSystem.expose
+
+def update? [DecidableEq p.A] (M : DynComputation p α β) :
+    M.State × p.Idx → Option M.State
+```
+
+`head` is not a new definition — it is *definitionally* the position map of the
+machine's underlying lens. That is why it transports so well:
+
+| Operation | Effect on `head` | Holds by |
+| --- | --- | --- |
+| `setInit g` | unchanged | `rfl` |
+| `mapResult f` | `Sum.map f id ∘ head` | `rfl` |
+| `wrap lens` | `Sum.map id lens.toFunA ∘ head` | `rfl` |
+
+**`head`, not an `output` / `expose` pair.** Splitting the readout into
+`output : State → Option β` and `expose : State → p.A` forces a `default`
+convention at resolved states, and that convention breaks compositionality:
+`(M.wrap lens).expose` is *not* `lens.toFunA ∘ M.expose`, because the two
+disagree exactly at resolved states. `head` has no such wart. `output`, `expose`,
+and `stepD` are still provided, as the derived accessors a machine-facing cost
+model consumes.
+
+**`update?` is partial, and that is load-bearing.** `none` means the pair is not a
+step the machine can take: the state has already returned, or the answer is tagged
+with a position the machine is not exposing. The total variant `updateFlat`
+(retained, derived as `(update? step).getD step.1`, because that is the shape a
+machine-facing cost model wants) does **not** compose across a state coproduct with
+a handoff:
+
+| answer tag | composite `updateFlat` | `Sum.inr (M₂.updateFlat (M₂.init v, i))` |
+| --- | --- | --- |
+| matches `M₂`'s exposed position | `Sum.inr (next₂ d)` | `Sum.inr (next₂ d)` ✓ |
+| does not match | `Sum.inl s₁` | `Sum.inr (M₂.init v)` ✗ |
+
+Reconciling those junk values would require the class to contain a decidable
+equality test on interface positions — provably not derivable from products,
+coproducts, and distributivity, since in the free distributive category on one
+object `Hom(X × X, 1 ⊕ 1)` contains only the two constants, and `StepClass` has no
+terminal object. With `none` both rows agree, the both-resolved case is subsumed
+(`M₂.update?` is `none` at a resolved state), and `update?_seqComp_inl` becomes an
+equation *unconditional in the answer index*. That is the whole reason for the
+partiality; the only cost is `DecidableEq p.A`.
+
+**The presentation is faithful.** `ofStep_step_eq_of_flat_eq`: a step function is
+determined by the `head` and `update?` it induces. So constraining those two maps
+plus `init` constrains the machine, not a lossy projection of it.
+
+**Spell the step maps with combinators, never `match`.** `Sum.elim`,
+`Option.getLeft?`, `Sigma.fst`, and `dite` all reduce by congruence over the
+shared `view`. An auto-generated matcher instead abstracts the computation and
+blocks unification across distinct input types, which would cost the `rfl`
+transport above. `PolyFunTest/Realizability/Examples.lean` pins those `rfl`s so a
+regression fails the test build.
+
+## The Boundary Is A Parameter, Never An Existential
+
+```lean
+structure Boundary (C : StepClass) (p : PFunctor) (α β : Type u) where
+  input : C.Str α
+  out : C.Str β
+  pos : C.Str p.A
+  idx : C.Str p.Idx
+```
+
+A `Boundary` is always a *parameter* of a realizability statement. A statement
+of the form `∃ bd, IsRealizableBy C bd program` is **vacuous**: a representation
+is only required to be admissible, not canonical, so an adversarially chosen
+encoding can precompute across the boundary. Only the machine's own state
+representation is chosen by the realization — and that choice is harmless, being
+exactly the freedom to pick a state layout.
+
+`pos` and `idx` are supplied independently. Nothing derives one from the other,
+since a step class is not assumed to represent dependent sums.
+
+## The Predicates
+
+```lean
+def IsRealizableBy (C) (bd) (program : α → FreeM p β) : Prop :=
+  ∃ R : Realization C bd, R.machine.Implements program
+
+def IsRealizableWithin (C) (bd) (program : α → FreeM p β) (k : ℕ) : Prop :=
+  ∃ R : Realization C bd, R.machine.ImplementsWithin program k
+```
+
+A `Realization` bundles a machine, a representation of its hidden state, and
+three admissibility proofs — for `init`, `head`, and `updateFlat`. Constraining
+`init` is what forbids smuggling precomputed advice into the initial state.
+
+`IsRealizableWithin.isTotalRollBound` extracts a bound on the *program*'s query
+depth from the machine, and `IsRealizableWithin.isRealizableBy` drops the budget.
+
+## Universe Discipline
+
+`StepClass.Str` speaks about types in a single universe, so the realizability
+predicates are stated at `p : PFunctor.{u, u}` with `α β : Type u`, hence
+`State : Type u`. Then `p.A`, `p.Idx`, `β ⊕ p.A`, and `State × p.Idx` all live in
+`Type u`. The underlying `DynComputation` API stays fully universe-polymorphic;
+only this layer is pinned. Every intended instantiation target is monomorphic
+anyway.
+
+## Instantiating With An External Complexity Class
+
+Complexity classes in the wild are presented on one concrete function type —
+`Complexity.FP : Set (List Bool → List Bool)` in complexitylib,
+`Cslib.Turing.PolyTimeComputable` on `List Symbol → List Symbol` in cslib — with
+no encoding-generic predicate. `StepClass.ofWordClass` is the bridge:
+
+```lean
+def ofWordClass (W : Type u) (Q : (W → W) → Prop) (hid : Q id)
+    (hcomp : ∀ {f g}, Q f → Q g → Q (g ∘ f)) : StepClass.{u, u} where
+  Str A := { encode : A → W // Function.Injective encode }
+  Hom eA eB f := ∃ q, Q q ∧ ∀ x, q (eA.1 x) = eB.1 (f x)
+```
+
+Injectivity of the encoding is the only semantic demand, exactly as for a raw bit
+encoding.
+
+Products and sums are *not* automatic. They need a pairing codec and a tagging
+scheme whose operations the word class admits, supplied as `WordPairing` and
+`WordTagging` and consumed by `ofWordClass.hasProd` / `ofWordClass.hasSum`. As of
+this writing complexitylib has the ingredients (`Complexity.pair`, `unpair?`,
+`delimit`) but has not exposed them as a class-level closure result, and cslib's
+`PolyTimeComputable` has `id` and `comp` but no pairing or projection machines at
+all. So a cslib instantiation is blocked upstream, not here.
+
+`StepClass.computable` — Mathlib's `Primcodable` representations and `Computable`
+functions — is the in-repo instance that works today and exercises every mixin.
+
+## Known Gaps
+
+- **No cost-bearing layer.** `Hom` is `Prop`-valued, so nothing here measures
+  running time or description size. The successor layer needs `Hom` replaced by a
+  `Type`-valued witness field carrying measures in an ordered semiring, with
+  `size` additive under composition and `time` composing by substitution.
+- **`ImplementsWithin` is pinned to a uniform `ℕ` budget.** `FreeM.IsRollBound`
+  is already generic in the budget type; `ImplementsWithin` is not.
+- **No terminal or initial representation**, hence only binary distributivity and
+  no unparameterized equality test. Nothing needs them; adding them would tax
+  every instance.
+- **Constant maps are not assumed admissible**, with one exception: `HasOption`
+  asserts `none_mem`, because a machine that has returned takes no step and so has
+  a constantly-`none` transition. Everything else — `isRealizableBy_pure`, for
+  instance — takes constant-admissibility as a per-theorem hypothesis.
+- **`Lens.IsAdmissible` has no `.id` and no `.comp`.** This is not an oversight:
+  `pullHeadIdx` compares the incoming answer's tag against the position the lens
+  exposes, so even the identity lens's pullback performs an equality test on
+  positions. Admissibility of a lens is a genuine hypothesis about the class,
+  satisfiable by every realistic one but not derivable from the mixins. It is also
+  why `wrap` needs the hypothesis and `seqComp` does not.
+- **No internal-language presentation.** An inductive syntax for the free
+  distributive category over the class's own maps, with one induction discharging
+  all plumbing, is real prior art on paper (Cockett–Fukushima's Charity; Vigna,
+  *Distributive computability*, 2003) and appears to be unformalized in any proof
+  assistant. It would replace the hand-assembled combinator chains in
+  `Closure.lean` with "exhibit a term". Worth doing if the combinator lemmas start
+  multiplying; over-engineering for the five closure theorems here.
+
+## References
+
+See [`REFERENCES.md`](../../REFERENCES.md) — `AM74`, `AMMS13`, `PR89`, `Uus15`,
+`PM15`, `Blum67`, `GHP09` for the realizability notion, and `Coc93`, `CLW93`,
+`Wal91`, `CF92`, `CDGH12`, `CH08`, `Clo99` for the distributive-category and
+function-algebra vocabulary; plus `SN24`, `LS25`, and `Abe26`.
+
+Terminology follows classical (co)algebraic *realization* theory rather than the
+word "implementation", which Aberlé (2026) uses for the free-monad Kleisli
+morphism — that is, for the program side.
+
+One clash worth flagging: in computable analysis *admissible representation* is a
+fixed technical term (Weihrauch 1985), where "admissible" qualifies the
+representation rather than the function class. This layer uses "admissible" in the
+sense of Petcher–Morrisett's FCF admissibility predicate — a property of a
+function, relative to chosen representations.
diff --git a/docs/wiki/repo-map.md b/docs/wiki/repo-map.md
index 0be98feb..61ab20a8 100644
--- a/docs/wiki/repo-map.md
+++ b/docs/wiki/repo-map.md
@@ -22,6 +22,8 @@ PolyFun/
     Multiparty/      per-party local view modes, observation kernels
     Concurrent/      structural and dynamic concurrent semantics
     UC/              open-process / open-theory layer (no security content)
+  Realizability/     step classes and realizability of free programs by
+                     machines whose transition functions are admissible
   Control/           monad/comonad and LTS infrastructure (Coalgebra,
                      Comonad, Lawful, Free, Iter, Bisimulation, LTS/Trace)
   Logic/             small logic helpers (HEq)
@@ -183,6 +185,14 @@ Interaction/{Concurrent, Basic} -> Interaction/UC/{Interface,
                                    Emulates, MachineId, EnvAction,
                                    EnvOpenProcess, CorruptionModel,
                                    MomentaryCorruption, Leakage}
+
+PFunctor/Basic -> Realizability/StepClass
+PFunctor/Dynamical/DynComputation/Bounded -> Realizability/Machine
+Realizability/{StepClass, Machine} -> Realizability/Basic
+  -> Realizability/Closure
+  -> Realizability/Instances
+  (Instances additionally draws on Mathlib's Computability and Fintype layers;
+   nothing under PFunctor/, ITree/, or Interaction/ depends on Realizability/)
 ```
 
 `PolyFun.lean` is a generated umbrella import file, not a hand-maintained