diff --git a/formal/LambdaVM.lean b/formal/LambdaVM.lean
index 298ab5036..64923b6c8 100644
--- a/formal/LambdaVM.lean
+++ b/formal/LambdaVM.lean
@@ -13,3 +13,6 @@ public import LambdaVM.Tables.Eq
 public import LambdaVM.Tables.Shift
 public import LambdaVM.Ensembles.EqLookup
 public import LambdaVM.Channels.Counted
+public import LambdaVM.Tables.MinToy
+public import LambdaVM.Ensembles.LtStaged
+public import LambdaVM.Ensembles.CountedSameBus
diff --git a/formal/LambdaVM/Buses/Alu.lean b/formal/LambdaVM/Buses/Alu.lean
index 9f06b1123..96f96bb33 100644
--- a/formal/LambdaVM/Buses/Alu.lean
+++ b/formal/LambdaVM/Buses/Alu.lean
@@ -65,6 +65,10 @@ def shiftResult (word signed direction x s : ℕ) : ℕ :=
   else if signed = 0 then x >>> k
   else sra64 x k
 
+/-- `opsel` of MIN: a toy operation for the counted-pulls PoC, not an RV64IM op. It has the shape of
+DIVREM: its chip pulls LT on this bus and pushes its own result on the same bus. -/
+def opselMIN : ℕ := 7
+
 /-- What a puller learns. The caller must have range-checked both words of both operands
 (the chips' `IS_WORD` assumptions). One clause per `opsel`, selected by the flag byte read
 as a natural. -/
@@ -83,7 +87,11 @@ def Guarantees (m : Msg (F p)) : Prop :=
     (∀ w s d : ℕ, w < 2 → s < 2 → d < 2 →
       m.flags.val = opselSHIFT + w + 32 * s + 64 * d →
       m.outLo.val < 2^32 ∧ m.outHi.val < 2^32 ∧
-      dword m.outLo m.outHi = shiftResult w s d (dword m.in1Lo m.in1Hi) (m.in2Lo.val % 256))
+      dword m.outLo m.outHi = shiftResult w s d (dword m.in1Lo m.in1Hi) (m.in2Lo.val % 256)) ∧
+    -- MIN (toy, see `opselMIN`): flags = opsel(MIN), out = the unsigned minimum
+    (m.flags.val = opselMIN →
+      m.outLo.val < 2^32 ∧ m.outHi.val < 2^32 ∧
+      dword m.outLo m.outHi = min (dword m.in1Lo m.in1Hi) (dword m.in2Lo m.in2Hi))
 
 def channel : Channel (F p) Msg where
   name := "ALU"
diff --git a/formal/LambdaVM/Channels/Counted.lean b/formal/LambdaVM/Channels/Counted.lean
index 85a826a16..f0640db5b 100644
--- a/formal/LambdaVM/Channels/Counted.lean
+++ b/formal/LambdaVM/Channels/Counted.lean
@@ -19,7 +19,9 @@ The price is in the balance premise. `exists_push_of_pull` needs `N · length <
 `BalancedInteractions` only matches pulls of multiplicity `1`, and counts a pull of any other
 nonzero multiplicity as a push; `not_consistent` shows the gap is real: for `N ≥ 2` the counted
 channel is not `Consistent`, so it cannot be finished in a `SoundEnsemble` until that premise
-carries the bound. With `N = 1` everything coincides (`counted 1 channel` is `Normal`).
+carries the bound. With `N = 1` everything coincides (`counted 1 channel` is `Normal`). With the
+bounded balance `BalancedUpTo N` of the modified Clean (`counted-pulls`), `consistentUpTo` closes
+the gap.
 -/
 
 namespace LambdaVM.Counted
@@ -275,6 +277,33 @@ theorem not_consistent (N : ℕ) (hN : 2 ≤ N) (hN' : N ≤ 255)
   convert h
   simp [ProvableType.fromElements_toElements]
 
+/-- With the bounded balance of the modified Clean (`BalancedUpTo N`, the premise `not_consistent`
+asks for), the counted channel is consistent: a pull of `1, …, N` is matched by an interaction
+that is not such a pull, and that interaction's requirement is the guarantee. -/
+instance consistentUpTo (N : ℕ) (channel : Channel (F p) Message) :
+    (counted N channel).ConsistentUpTo N where
+  consistent interactions data balanced reqs a a_mem := by
+    obtain ⟨ a_channel, - ⟩ := reqs a a_mem
+    by_cases a_pull : a.PullUpTo N
+    case neg =>
+      rcases a with ⟨ _, a_direction, a_mult, a_msg, a_size ⟩
+      subst a_channel
+      simp only [Interaction.Guarantees, counted]
+      exact fun h_direction h_count => absurd ⟨ h_direction, h_count ⟩ a_pull
+    obtain ⟨ b, b_mem, b_msg, b_ne_zero, b_not_pull ⟩ := balanced.matchedUpTo a a_mem a_pull
+    obtain ⟨ b_channel, b_reqs ⟩ := reqs b b_mem
+    rcases a with ⟨ _, a_direction, a_mult, a_msg, a_size ⟩
+    rcases b with ⟨ _, b_direction, b_mult, b_msg', b_size ⟩
+    subst a_channel b_channel
+    simp only at b_msg
+    subst b_msg
+    simp only [Interaction.Guarantees, Interaction.Requirements, Interaction.msgVector,
+      counted] at b_reqs ⊢
+    intro _ _
+    cases b_direction with
+    | push => exact b_reqs b_ne_zero
+    | pull => exact b_reqs b_ne_zero (b_not_pull rfl)
+
 end LambdaVM.Counted
 
 /-! ## A deduplicated row
diff --git a/formal/LambdaVM/Ensembles/CountedSameBus.lean b/formal/LambdaVM/Ensembles/CountedSameBus.lean
new file mode 100644
index 000000000..de7d05c51
--- /dev/null
+++ b/formal/LambdaVM/Ensembles/CountedSameBus.lean
@@ -0,0 +1,280 @@
+module
+
+public import LambdaVM.Ensembles.LtStaged
+
+@[expose] public section
+
+/-!
+# Counted pulls and a response on the same bus (PoC)
+
+The shape of DVRM with everything at once. The ALU bus is a counted channel. One table, CMIN,
+answers `μ ≤ 255` identical MIN requests per row: it pulls an LT result on the ALU bus with
+multiplicity `μ`, bounded by its own pull of `ARE_BYTES[μ, 0]`, and pushes the MIN result `μ`
+times on the same bus. The LT answers come from a provider that stands for the LT table.
+
+Stages, oldest first: `ARE_BYTES`, the ALU messages that are not MIN, the MIN messages. CMIN's
+requirement on its counted pull (`μ = 0 ∨ 1 ≤ μ ≤ 255`) uses its guarantee on `ARE_BYTES`; its
+requirement on the MIN push uses its guarantee on the LT pull, in the earlier ALU class.
+-/
+
+namespace LambdaVM.CountedMin
+open LambdaVM.LT (muMax)
+
+/-- The ALU bus with pulls of multiplicity up to `muMax`. -/
+abbrev AluC : RawChannel (F p) := Alu.channel.counted muMax
+
+def main (r : Var MinToy.Row (F p)) : Circuit (F p) Unit := do
+  -- μ : Byte: ARE_BYTES[μ, 0]
+  Bitwise.AreBytes.pull (r.mu, 0)
+  -- ALU[a, b, opsel(LT)] -> [lt, 0], μ times
+  Alu.channel.pullUpTo muMax r.mu ⟨r.a0, r.a1, r.b0, r.b1, 4, r.lt, 0⟩
+  -- out = lt ? a : b
+  assertZero (r.out0 - (r.lt * r.a0 + (1 - r.lt) * r.b0))
+  assertZero (r.out1 - (r.lt * r.a1 + (1 - r.lt) * r.b1))
+  -- ALU[a, b, opsel(MIN)] -> out, μ times
+  Alu.channel.emitUpTo muMax r.mu ⟨r.a0, r.a1, r.b0, r.b1, 7, r.out0, r.out1⟩
+
+/-- The honest prover's row: `μ` a byte, `lt` the comparison and `out` the selected operand. -/
+def Honest (r : MinToy.Row (F p)) : Prop :=
+  r.mu.val < 2^8 ∧ r.lt = ((Alu.ltBit 0 0 (dword r.a0 r.a1) (dword r.b0 r.b1) : ℕ) : F p) ∧
+  r.out0 = r.lt * r.a0 + (1 - r.lt) * r.b0 ∧ r.out1 = r.lt * r.a1 + (1 - r.lt) * r.b1
+
+def circuit : GeneralFormalCircuit (F p) MinToy.Row unit where
+  name := "CMIN"
+  main
+  Spec _ _ _ := True
+  channelsWithRequirements := [AluC]
+  requirementsChannelsLawful input_var i₀ := by
+    obtain ⟨a0, a1, b0, b1, lt, out0, out1, mu⟩ := input_var
+    simp only [circuit_norm, main, AluC, Bitwise.AreBytes]
+    intro channel h
+    tauto
+  soundness := by
+    circuit_proof_start [main, Alu.channel, Alu.Guarantees, Bitwise.areBytesTable]
+    obtain ⟨⟨h_mu, -⟩, h_pull, h_o0, h_o1⟩ := h_holds
+    -- with μ = 0 nothing is owed
+    by_cases h0 : input_mu = 0
+    · simp [h0]
+    -- otherwise ARE_BYTES[μ, 0] makes μ a count of at most 255
+    have hcount : Channel.CountUpTo muMax input_mu :=
+      Channel.countUpTo_of_val h0 (by simp only [muMax]; omega)
+    refine ⟨.inr hcount, fun _ ha0 ha1 hb0 hb1 => ?_⟩
+    have h4 : (4 : F p).val = 4 := by simpa using MinToy.val_lit 4 (by norm_num)
+    have h7 : (7 : F p).val = 7 := by simpa using MinToy.val_lit 7 (by norm_num)
+    -- the pulled LT result
+    obtain ⟨hLT, -⟩ := h_pull hcount ha0 ha1 hb0 hb1
+    have hlt := hLT 0 0 (by norm_num) (by norm_num) (by rw [h4]; simp [opselLT])
+    have hL : dword input_a0 input_a1 < 2^64 := by unfold dword; omega
+    have hR : dword input_b0 input_b1 < 2^64 := by unfold dword; omega
+    rw [h7]
+    refine ⟨fun s i hs hi h => by simp only [opselLT] at h; omega,
+      fun i hi h => by simp only [opselEQ] at h; omega,
+      fun w s d hw hs hd h => by simp only [opselSHIFT] at h; omega, fun _ => ?_⟩
+    by_cases hLR : dword input_a0 input_a1 < dword input_b0 input_b1
+    · have h1 : input_lt = 1 := by
+        rw [hlt]; simp [Alu.ltBit, Alu.ltRaw, Alu.ult_ofNat_iff hL hR, hLR]
+      have e0 : input_out0 = input_a0 := by rw [h1] at h_o0; linear_combination h_o0
+      have e1 : input_out1 = input_a1 := by rw [h1] at h_o1; linear_combination h_o1
+      rw [e0, e1, min_eq_left hLR.le]
+      exact ⟨ha0, ha1, rfl⟩
+    · have h1 : input_lt = 0 := by
+        rw [hlt]; simp [Alu.ltBit, Alu.ltRaw, Alu.ult_ofNat_iff hL hR, hLR]
+      have e0 : input_out0 = input_b0 := by rw [h1] at h_o0; linear_combination h_o0
+      have e1 : input_out1 = input_b1 := by rw [h1] at h_o1; linear_combination h_o1
+      rw [e0, e1, min_eq_right (not_lt.mp hLR)]
+      exact ⟨hb0, hb1, rfl⟩
+
+  ProverAssumptions r _ _ := Honest r
+  completeness := by
+    circuit_proof_start [main, Alu.channel, Alu.Guarantees, Bitwise.areBytesTable, Honest]
+    obtain ⟨hmu, hlt, ho0, ho1⟩ := h_assumptions
+    have h4 : (4 : F p).val = 4 := by simpa using MinToy.val_lit 4 (by norm_num)
+    refine ⟨⟨hmu, by simp⟩, ?_, by rw [ho0]; ring, by rw [ho1]; ring⟩
+    intro _ _ _ _ _
+    rw [h4]
+    refine ⟨fun s i hs hi h => ?_, fun i hi h => by simp only [opselEQ] at h; omega,
+      fun w s d hw hs hd h => by simp only [opselSHIFT] at h; omega,
+      fun h => by simp only [Alu.opselMIN] at h; omega⟩
+    simp only [opselLT] at h
+    obtain ⟨rfl, rfl⟩ : s = 0 ∧ i = 0 := by omega
+    exact hlt
+
+/-! ## The ensemble: ARE_BYTES, the LT answers, CMIN -/
+
+open Air.Flat
+open Ensembles.LtStaged (providerComponent countedProviderComponent demandOn isMinMsg
+  isMinMsg_toElements msg_eval mu_count providerComponent_guarantees
+  providerComponent_requirements countedProviderComponent_guarantees
+  countedProviderComponent_requirements)
+
+def cminComponent : Component (F p) where
+  circuit := circuit
+  generation := demandOn Alu.channel _
+
+@[circuit_norm] lemma cminComponent_guarantees :
+    cminComponent.circuit.channelsWithGuarantees = [Bitwise.AreBytes.toRaw, AluC] := rfl
+@[circuit_norm] lemma cminComponent_requirements :
+    cminComponent.circuit.channelsWithRequirements = [AluC] := rfl
+
+/-- Stages, newest first: the MIN messages, the other ALU messages, ARE_BYTES. -/
+def stages : List (Stage (F p)) :=
+  [{ channel := AluC, cls := isMinMsg }, { channel := AluC, cls := fun m => !isMinMsg m },
+   { channel := Bitwise.AreBytes.toRaw }]
+
+/-- The LT answers stand for the LT table: a provider of ALU messages on the counted bus. -/
+def ensemble : Ensemble (F p) unit where
+  tables := [providerComponent Bitwise.AreBytes, countedProviderComponent muMax Alu.channel,
+    cminComponent]
+  unique_names := by
+    simp [providerComponent, countedProviderComponent, cminComponent, Ensembles.LtStaged.provider,
+      Ensembles.LtStaged.countedProvider, circuit, Alu.channel, Bitwise.AreBytes,
+      Bitwise.areBytesTable, StaticLookupChannel.toChannel]
+  channels := [AluC, Bitwise.AreBytes.toRaw]
+  unique_channel_names := by
+    simp [AluC, circuit_norm, Alu.channel, Bitwise.AreBytes, Bitwise.areBytesTable]
+  tables_channels := by
+    intro table h
+    simp only [List.mem_cons, List.not_mem_nil, or_false] at h
+    rcases h with rfl | rfl | rfl <;>
+      simp only [GeneralFormalCircuit.channels, providerComponent_guarantees,
+        providerComponent_requirements, countedProviderComponent_guarantees,
+        countedProviderComponent_requirements, cminComponent_guarantees,
+        cminComponent_requirements] <;>
+      simp [AluC]
+  verifier_channels := by simp [circuit_norm]
+
+/-- `msg_eval`, in the form `simp` leaves an evaluated message in. -/
+lemma msg_eval_array {M : TypeMap} [ProvableType M] (env : Environment (F p))
+    (x : M (Expression (F p))) :
+    Array.map (Expression.eval env) (toElements x).toArray = (toElements (eval env x)).toArray := by
+  rw [← Vector.toArray_map]
+  exact msg_eval env x
+
+lemma isMinMsg_eval (env : Environment (F p)) (m : Alu.Msg (Expression (F p))) :
+    isMinMsg (Array.map (fun x => Expression.eval env x) (toElements m).toArray) =
+      decide ((eval env m).flags = 7) := by
+  rw [show (fun x => Expression.eval env x) = Expression.eval env from rfl, msg_eval_array,
+    isMinMsg_toElements]
+
+lemma areBytesTable_guarantees (x y : F p) :
+    Bitwise.areBytesTable.Guarantees (x, y) ↔ x.val < 2^8 ∧ y.val < 2^8 := Iff.rfl
+
+lemma bytes_ne_alu : Bitwise.AreBytes.toRaw ≠ Channel.counted muMax Alu.channel := by
+  intro h
+  have := congrArg RawChannel.name h
+  simp [circuit_norm, Alu.channel, Bitwise.AreBytes, Bitwise.areBytesTable, StaticLookupChannel.toChannel,
+    Channel.counted, Channel.toRaw] at this
+
+/-- Each row of CMIN has two interactions on the ALU bus: the LT pull, which is not a MIN message,
+and the MIN push. -/
+lemma cmin_alu_shape {table : Table (F p)} (h_comp : table.component = cminComponent)
+    {i : Interaction (F p)} (h_i : i ∈ table.interactionsWith AluC) :
+    (i.direction = .pull ∧ isMinMsg i.msg = false) ∨
+      (i.direction = .push ∧ isMinMsg i.msg = true) := by
+  cases table
+  simp only at h_comp
+  subst h_comp
+  simp [Table.interactionsWith, List.mem_flatMap, Operations.interactionValuesWith_eq_map,
+    Component.interactionsWith_eq, Component.rowOperations, cminComponent, circuit, main, AluC,
+    circuit_norm] at h_i
+  obtain ⟨row, -, a, ha, rfl⟩ := h_i
+  split_ifs at ha with h_eq
+  · exfalso
+    have := congrArg RawChannel.name h_eq
+    simp [Bitwise.areBytesTable, Channel.counted, Alu.channel, circuit_norm] at this
+  simp only [List.mem_cons, List.not_mem_nil, or_false] at ha
+  rcases ha with rfl | rfl
+  · left
+    simp only [AbstractInteraction.eval, Channel.pulledUpTo]
+    erw [msg_eval, isMinMsg_toElements]
+    simp (config := { decide := true }) [circuit_norm]
+  · right
+    simp only [AbstractInteraction.eval, Channel.emittedUpTo]
+    erw [msg_eval, isMinMsg_toElements]
+    simp (config := { decide := true }) [circuit_norm]
+
+/-- CMIN's counted pull owes `μ = 0 ∨ 1 ≤ μ ≤ 255`, which its guarantee on ARE_BYTES gives. -/
+lemma cmin_pull_requirement {table : Table (F p)} (h_comp : table.component = cminComponent)
+    (g_bytes : ∀ i ∈ table.interactionsWith Bitwise.AreBytes.toRaw, i.Guarantees table.data)
+    {i : Interaction (F p)} (h_i : i ∈ table.interactionsWith AluC)
+    (h_pull : i.direction = .pull) : i.Requirements table.data := by
+  cases table
+  simp only at h_comp
+  subst h_comp
+  simp [Table.interactionsWith, List.mem_flatMap, Operations.interactionValuesWith_eq_map,
+    Component.interactionsWith_eq, Component.rowOperations, cminComponent, circuit, main, AluC,
+    circuit_norm, forall_exists_index, and_imp] at h_i g_bytes
+  obtain ⟨row, hrow, a, ha, rfl⟩ := h_i
+  split_ifs at ha with h_eq
+  · exfalso
+    have := congrArg RawChannel.name h_eq
+    simp [Bitwise.areBytesTable, Channel.counted, Alu.channel, circuit_norm] at this
+  simp only [List.mem_cons, List.not_mem_nil, or_false] at ha
+  rcases ha with rfl | rfl
+  · have g := g_bytes _ row hrow (Or.inl rfl)
+    simp only [AbstractInteraction.eval, ChannelInteraction.toRaw, pulled, Interaction.Guarantees,
+      Channel.toRaw, Interaction.msgVector] at g
+    have g1 := g trivial (by simp [circuit_norm])
+    simp only [Vector.mk_toArray, ProvableType.fromElements_eval_toElements] at g1
+    simp only [circuit_norm, explicit_provable_type, areBytesTable_guarantees] at g1
+    simp only [AbstractInteraction.eval, Channel.pulledUpTo, Interaction.Requirements,
+      Channel.counted]
+    exact mu_count g1.1
+  · simp [AbstractInteraction.eval, Channel.emittedUpTo] at h_pull
+
+theorem tableSoundness : ensemble.TableSoundness (Balance.logUpUpTo muMax) := by
+  apply Ensemble.tableSoundness_of_stagedOn stages rfl
+  · intro s hs
+    simp only [stages, List.mem_cons, List.not_mem_nil, or_false] at hs
+    rcases hs with rfl | rfl | rfl <;> simp [ensemble]
+  · intro component h c hc msg
+    simp only [ensemble, List.mem_cons, List.not_mem_nil, or_false] at h
+    rcases h with rfl | rfl | rfl
+    iterate 2 simp [providerComponent_guarantees, countedProviderComponent_guarantees] at hc
+    · rw [cminComponent_guarantees] at hc
+      simp only [List.mem_cons, List.not_mem_nil, or_false] at hc
+      rcases hc with rfl | rfl
+      · exact ⟨{ channel := Bitwise.AreBytes.toRaw }, by simp [stages], rfl, rfl⟩
+      · cases h : isMinMsg msg
+        · exact ⟨{ channel := AluC, cls := fun m => !isMinMsg m }, by simp [stages], rfl,
+            by simp [h]⟩
+        · exact ⟨{ channel := AluC, cls := isMinMsg }, by simp [stages], rfl, h⟩
+  · intro s hs
+    show s.channel.ConsistentUpTo muMax
+    simp only [stages, List.mem_cons, List.not_mem_nil, or_false] at hs
+    rcases hs with rfl | rfl | rfl <;> infer_instance
+  · intro component h
+    simp only [ensemble, List.mem_cons, List.not_mem_nil, or_false] at h
+    rcases h with rfl | rfl | rfl
+    -- the providers pull nothing
+    iterate 2
+      refine ⟨?_, ?_, ?_, trivial⟩ <;>
+        exact Component.requirementsAfterOn_of_guarantees_subset (by
+          simp [providerComponent_guarantees, countedProviderComponent_guarantees])
+    refine ⟨?_, ?_, ?_, trivial⟩
+    -- MIN messages: after the LT pull's class and ARE_BYTES
+    · apply Component.requirementsAfterOn_of_covered
+      intro table h_comp c hc i h_i h_pull
+      rw [cminComponent_guarantees] at hc
+      simp only [List.mem_cons, List.not_mem_nil, or_false] at hc
+      rcases hc with rfl | rfl
+      · exact ⟨{ channel := Bitwise.AreBytes.toRaw }, by simp, rfl, rfl⟩
+      · rcases cmin_alu_shape h_comp h_i with ⟨-, h_cls⟩ | ⟨h_push, -⟩
+        · exact ⟨{ channel := AluC, cls := fun m => !isMinMsg m }, by simp, rfl, by simp [h_cls]⟩
+        · simp [h_push] at h_pull
+    -- the other ALU messages: only the counted pull, bounded through ARE_BYTES
+    · rintro table h_comp - - guarantees i h_i h_cls
+      rcases cmin_alu_shape h_comp h_i with ⟨h_pull, -⟩ | ⟨-, h_min⟩
+      · exact cmin_pull_requirement h_comp
+          (fun j hj => guarantees { channel := Bitwise.AreBytes.toRaw } (by simp) j hj rfl)
+          h_i h_pull
+      · simp [h_min] at h_cls
+    -- nothing owed on ARE_BYTES
+    · apply Component.requirementsAfterOn_of_not_mem
+      rw [cminComponent_requirements, List.mem_singleton]
+      intro h
+      have := congrArg RawChannel.name h
+      simp [circuit_norm, AluC, Alu.channel, Bitwise.AreBytes, Bitwise.areBytesTable,
+        StaticLookupChannel.toChannel, Channel.counted, Channel.toRaw] at this
+
+end LambdaVM.CountedMin
diff --git a/formal/LambdaVM/Ensembles/LtStaged.lean b/formal/LambdaVM/Ensembles/LtStaged.lean
new file mode 100644
index 000000000..fb60cccb6
--- /dev/null
+++ b/formal/LambdaVM/Ensembles/LtStaged.lean
@@ -0,0 +1,395 @@
+module
+
+public import LambdaVM.Tables.Lt
+public import LambdaVM.Tables.MinToy
+public import Clean.Air.StagedChannels
+
+@[expose] public section
+
+/-!
+# LT with counted pulls (PoC)
+
+`ARE_BYTES`, `IS_HALF` and `MSB16` providers and the LT chip, with `μ` a byte as in `lt.rs`.
+LT pulls `IS_HALF` and `MSB16` with multiplicity `μ`, so they are counted channels, and the bound
+`μ ≤ 255` comes from LT's own pull of `ARE_BYTES[μ, 0]`. Clean's `OrderedChannel` cannot express
+that (LT pulls from and owes requirements on `IS_HALF`); soundness by channel finishing order can:
+
+  ARE_BYTES → IS_HALF (counted) → MSB16 (counted) → ALU
+
+LT's requirements on `IS_HALF` and `MSB16` (`μ = 0 ∨ 1 ≤ μ ≤ 255`) follow from its guarantee on
+`ARE_BYTES`, which is finished before them.
+-/
+
+namespace LambdaVM.Ensembles.LtStaged
+open Air.Flat LambdaVM.LT
+
+variable {Message : TypeMap} [ProvableType Message]
+
+/-- A provider row: pushes `value` `multiplicity` times, assuming `value` satisfies the channel's
+guarantee. Stands for the BITWISE table, whose rows are fixed. -/
+def provider (channel : Channel (F p) Message) :
+    GeneralFormalCircuit (F p) (ProvablePair Message field) unit where
+  name := channel.name
+  main | (value, multiplicity) => channel.emit multiplicity value
+  channelsWithRequirements := [channel.toRaw]
+  Assumptions input data := channel.Guarantees input.1 data
+  Spec _ _ _ := True
+  soundness := by
+    circuit_proof_start
+    rcases input with ⟨value, multiplicity⟩
+    simp_all
+  completeness := by circuit_proof_start
+
+/-- The same, on `channel.counted N`. -/
+def countedProvider (N : ℕ) (channel : Channel (F p) Message) :
+    GeneralFormalCircuit (F p) (ProvablePair Message field) unit where
+  name := channel.name
+  main | (value, multiplicity) => channel.emitUpTo N multiplicity value
+  channelsWithRequirements := [channel.counted N]
+  Assumptions input data := channel.Guarantees input.1 data
+  Spec _ _ _ := True
+  soundness := by
+    circuit_proof_start
+    rcases input with ⟨value, multiplicity⟩
+    simp_all
+  completeness := by circuit_proof_start
+
+@[circuit_norm] lemma provider_channelsWithGuarantees (channel : Channel (F p) Message) :
+    (provider channel).channelsWithGuarantees = [] := rfl
+@[circuit_norm] lemma countedProvider_channelsWithGuarantees (N : ℕ) (channel : Channel (F p) Message) :
+    (countedProvider N channel).channelsWithGuarantees = [] := rfl
+@[circuit_norm] lemma provider_channelsWithRequirements (channel : Channel (F p) Message) :
+    (provider channel).channelsWithRequirements = [channel.toRaw] := rfl
+@[circuit_norm] lemma countedProvider_channelsWithRequirements (N : ℕ)
+    (channel : Channel (F p) Message) :
+    (countedProvider N channel).channelsWithRequirements = [channel.counted N] := rfl
+@[circuit_norm] lemma lt_channelsWithRequirements :
+    LT.circuit.channelsWithRequirements = [Alu.channel.toRaw, IsHalfC, Msb16C] := rfl
+@[circuit_norm] lemma lt_channelsWithGuarantees :
+    LT.circuit.channelsWithGuarantees = [Bitwise.AreBytes.toRaw, IsHalfC, IsHalfC, Msb16C, Msb16C,
+      IsHalfC, IsHalfC, IsHalfC, IsHalfC] := rfl
+
+/-- Witness generation is not part of this PoC: every component answers demand on its channel. -/
+def demandOn (channel : Channel (F p) Message) (Input : TypeMap) [ProvableType Input] :
+    WitnessGeneration.Generation (F p) Input :=
+  .demand {
+    channel
+    trigger := .pull
+    input _ := pure (fromElements (Vector.replicate (size Input) .multiplicity)) }
+
+def providerComponent (channel : Channel (F p) Message) : Component (F p) where
+  circuit := provider channel
+  generation := demandOn channel _
+  Assumptions input data := channel.Guarantees input.1 data
+  circuit_assumptions_of_assumptions := by intro _ _ _ _ _ h; exact h
+
+def countedProviderComponent (N : ℕ) (channel : Channel (F p) Message) : Component (F p) where
+  circuit := countedProvider N channel
+  generation := demandOn channel _
+  Assumptions input data := channel.Guarantees input.1 data
+  circuit_assumptions_of_assumptions := by intro _ _ _ _ _ h; exact h
+
+def ltComponent : Component (F p) where
+  circuit := LT.circuit
+  generation := demandOn Alu.channel _
+
+@[circuit_norm] lemma providerComponent_guarantees (channel : Channel (F p) Message) :
+    (providerComponent channel).circuit.channelsWithGuarantees = [] := rfl
+@[circuit_norm] lemma providerComponent_requirements (channel : Channel (F p) Message) :
+    (providerComponent channel).circuit.channelsWithRequirements = [channel.toRaw] := rfl
+@[circuit_norm] lemma countedProviderComponent_guarantees (N : ℕ) (channel : Channel (F p) Message) :
+    (countedProviderComponent N channel).circuit.channelsWithGuarantees = [] := rfl
+@[circuit_norm] lemma countedProviderComponent_requirements (N : ℕ)
+    (channel : Channel (F p) Message) :
+    (countedProviderComponent N channel).circuit.channelsWithRequirements =
+      [channel.counted N] := rfl
+@[circuit_norm] lemma ltComponent_guarantees :
+    ltComponent.circuit.channelsWithGuarantees = [Bitwise.AreBytes.toRaw, IsHalfC, IsHalfC, Msb16C,
+      Msb16C, IsHalfC, IsHalfC, IsHalfC, IsHalfC] := rfl
+@[circuit_norm] lemma ltComponent_requirements :
+    ltComponent.circuit.channelsWithRequirements = [Alu.channel.toRaw, IsHalfC, Msb16C] := rfl
+
+/-- Finishing order, newest first. -/
+def finished : List (RawChannel (F p)) :=
+  [Alu.channel.toRaw, Msb16C, IsHalfC, Bitwise.AreBytes.toRaw]
+
+def ensemble : Ensemble (F p) unit where
+  tables := [providerComponent Bitwise.AreBytes, countedProviderComponent muMax Bitwise.IsHalf,
+    countedProviderComponent muMax Bitwise.Msb16, ltComponent]
+  unique_names := by
+    simp [providerComponent, countedProviderComponent, ltComponent, provider, countedProvider,
+      LT.circuit, Bitwise.AreBytes, Bitwise.IsHalf, Bitwise.Msb16, Bitwise.areBytesTable,
+      Bitwise.isHalfTable, Bitwise.msb16Table, StaticLookupChannel.toChannel]
+  channels := finished
+  unique_channel_names := by
+    simp [finished, circuit_norm, Alu.channel, Bitwise.AreBytes, Bitwise.IsHalf, Bitwise.Msb16,
+      Bitwise.areBytesTable, Bitwise.isHalfTable, Bitwise.msb16Table]
+  tables_channels := by
+    intro table h
+    simp only [List.mem_cons, List.not_mem_nil, or_false] at h
+    rcases h with rfl | rfl | rfl | rfl <;>
+      simp only [GeneralFormalCircuit.channels, providerComponent_guarantees, providerComponent_requirements, countedProviderComponent_guarantees, countedProviderComponent_requirements, ltComponent_guarantees, ltComponent_requirements] <;>
+      simp [finished, IsHalfC, Msb16C]
+  verifier_channels := by simp [circuit_norm]
+
+/-- `μ` from `ARE_BYTES[μ, 0]` is an inactive or counted pull. -/
+lemma mu_count {x : F p} (h : x.val < 256) : x = 0 ∨ Channel.CountUpTo muMax x := by
+  by_cases h0 : x = 0
+  · exact .inl h0
+  · exact .inr (Channel.countUpTo_of_val h0 (by simp only [muMax]; omega))
+
+/-- LT's requirements on its counted pulls follow from its guarantee on `ARE_BYTES`. -/
+theorem lt_requirementsAfter_counted {c : RawChannel (F p)} (hc : c = IsHalfC ∨ c = Msb16C)
+    {earlier : List (RawChannel (F p))} (h_earlier : Bitwise.AreBytes.toRaw ∈ earlier) :
+    ltComponent.RequirementsAfter c earlier := by
+  rintro table h_comp - constraints guarantees row hrow
+  have g := guarantees _ h_earlier row hrow
+  cases table
+  simp only at h_comp
+  subst h_comp
+  simp only [Component.channelGuarantees_iff, Component.channelRequirements_iff] at g ⊢
+  simp (config := { decide := true }) [circuit_norm, Component.rowOperations, ltComponent,
+    LT.circuit, LT.main, isBit, sub, add, Add.carry0, Add.carry1, IsHalfC, Msb16C, Alu.channel,
+    Bitwise.AreBytes, Bitwise.IsHalf, Bitwise.Msb16, Bitwise.areBytesTable, Bitwise.isHalfTable,
+    Bitwise.msb16Table, StaticLookupChannel.toChannel] at g ⊢
+  have hm := mu_count g.1
+  rcases hc with rfl | rfl <;>
+    simp (config := { decide := true }) [hm, IsHalfC, Msb16C, Bitwise.IsHalf, Bitwise.Msb16,
+      Bitwise.isHalfTable, Bitwise.msb16Table, StaticLookupChannel.toChannel]
+  -- the ALU push is on another channel
+  all_goals
+    intro h
+    have := congrArg RawChannel.name h
+    simp [Channel.counted, Channel.toRaw] at this
+
+theorem tableSoundness : ensemble.TableSoundness (Balance.logUpUpTo muMax) := by
+  apply Ensemble.tableSoundness_of_staged finished rfl (List.Subset.refl _)
+  · intro component h
+    simp only [ensemble, List.mem_cons, List.not_mem_nil, or_false] at h
+    rcases h with rfl | rfl | rfl | rfl <;>
+      simp only [providerComponent_guarantees, countedProviderComponent_guarantees,
+        ltComponent_guarantees] <;>
+      simp [finished, IsHalfC, Msb16C]
+  · intro c hc
+    show c.ConsistentUpTo muMax
+    simp only [finished, List.mem_cons, List.not_mem_nil, or_false] at hc
+    rcases hc with rfl | rfl | rfl | rfl <;> infer_instance
+  · intro component h
+    simp only [ensemble, List.mem_cons, List.not_mem_nil, or_false] at h
+    rcases h with rfl | rfl | rfl | rfl
+    -- the providers pull nothing
+    iterate 3
+      exact Component.stagedRequirements_of_forall fun _ _ _ =>
+        Component.requirementsAfter_of_guarantees_subset (by
+          simp only [providerComponent_guarantees, countedProviderComponent_guarantees,
+            List.nil_subset])
+    -- LT: ALU after its pulls, the counted pulls after ARE_BYTES, nothing owed on ARE_BYTES
+    refine ⟨?_, lt_requirementsAfter_counted (.inr rfl) (by simp),
+      lt_requirementsAfter_counted (.inl rfl) (by simp), ?_, trivial⟩
+    · apply Component.requirementsAfter_of_guarantees_subset
+      simp only [ltComponent_guarantees]
+      simp [IsHalfC, Msb16C]
+    · apply Component.requirementsAfter_of_not_mem
+      simp only [ltComponent_requirements, List.mem_cons, List.not_mem_nil, or_false, not_or]
+      refine ⟨fun h => ?_, fun h => ?_, fun h => ?_⟩ <;> have := congrArg RawChannel.name h <;>
+        simp [circuit_norm, IsHalfC, Msb16C, Alu.channel, Bitwise.AreBytes, Bitwise.IsHalf,
+          Bitwise.Msb16, Bitwise.areBytesTable, Bitwise.isHalfTable, Bitwise.msb16Table,
+          StaticLookupChannel.toChannel] at this
+
+end LambdaVM.Ensembles.LtStaged
+
+/-!
+## Adding MIN: one table pulls and pushes on the same bus
+
+MIN pulls an LT result from the ALU bus and pushes its own result on the same bus. Ordering by
+whole channels can't place it: ALU would have to be finished before MIN (for its pull) and after
+it (for its push). Ordering by stages can: the ALU messages that are not MIN are finished first,
+then the MIN messages. MIN is one table; only the bus is read in two classes.
+-/
+
+namespace LambdaVM.Ensembles.LtStaged
+open Air.Flat LambdaVM.LT
+
+def minComponent : Component (F p) where
+  circuit := MinToy.circuit
+  generation := demandOn Alu.channel _
+
+@[circuit_norm] lemma minComponent_guarantees :
+    minComponent.circuit.channelsWithGuarantees = [Alu.channel.toRaw] := rfl
+@[circuit_norm] lemma minComponent_requirements :
+    minComponent.circuit.channelsWithRequirements = [Alu.channel.toRaw] := rfl
+
+/-- The ALU messages of MIN: read as an ALU message, the flag field is `opsel(MIN)`. -/
+def isMinMsg (msg : Array (F p)) : Bool :=
+  if h : msg.size = size Alu.Msg then
+    decide ((fromElements (⟨msg, h⟩ : Vector (F p) (size Alu.Msg)) : Alu.Msg (F p)).flags = 7)
+  else false
+
+lemma isMinMsg_toElements (m : Alu.Msg (F p)) :
+    isMinMsg (toElements m).toArray = decide (m.flags = 7) := by
+  simp [isMinMsg, ProvableType.fromElements_toElements]
+
+/-- The message of an evaluated interaction, as the evaluated typed message. -/
+lemma msg_eval {M : TypeMap} [ProvableType M] (env : Environment (F p)) (x : M (Expression (F p))) :
+    ((toElements x).map (Expression.eval env)).toArray = (toElements (eval env x)).toArray := by
+  rw [← ProvableType.fromElements_eval_toElements (env := env) x,
+    ProvableType.toElements_fromElements, Vector.toArray_map]
+
+/-- Each row of MIN has two interactions on ALU: the LT pull, which is not a MIN message, and
+the MIN push. -/
+lemma min_alu_shape {table : Table (F p)} (h_comp : table.component = minComponent)
+    {i : Interaction (F p)} (h_i : i ∈ table.interactionsWith Alu.channel.toRaw) :
+    (i.direction = .pull ∧ isMinMsg i.msg = false) ∨
+      (i.direction = .push ∧ isMinMsg i.msg = true) := by
+  cases table
+  simp only at h_comp
+  subst h_comp
+  simp [Table.interactionsWith, List.mem_flatMap, Operations.interactionValuesWith_eq_map,
+    Component.interactionsWith_eq, Component.rowOperations, minComponent, MinToy.circuit,
+    MinToy.main, isBit, circuit_norm] at h_i
+  obtain ⟨row, -, rfl | rfl⟩ := h_i
+  · left
+    simp only [AbstractInteraction.eval, ChannelInteraction.toRaw, pulled, msg_eval,
+      isMinMsg_toElements]
+    simp (config := { decide := true }) [circuit_norm]
+  · right
+    simp only [AbstractInteraction.eval, ChannelInteraction.toRaw, pushedIf, msg_eval,
+      isMinMsg_toElements]
+    simp (config := { decide := true }) [circuit_norm]
+
+/-- MIN's pull, of multiplicity `1`, owes nothing beyond its multiplicity. -/
+lemma min_pull_requirements {table : Table (F p)} (h_comp : table.component = minComponent)
+    (constraints : table.Constraints) {i : Interaction (F p)}
+    (h_i : i ∈ table.interactionsWith Alu.channel.toRaw) (h_pull : i.direction = .pull) :
+    i.Requirements table.data := by
+  cases table
+  simp only at h_comp
+  subst h_comp
+  simp [Table.interactionsWith, List.mem_flatMap, Operations.interactionValuesWith_eq_map,
+    Component.interactionsWith_eq, Component.rowOperations, minComponent, MinToy.circuit,
+    MinToy.main, isBit, circuit_norm] at h_i
+  obtain ⟨row, -, rfl | rfl⟩ := h_i
+  · simp [AbstractInteraction.eval, ChannelInteraction.toRaw, pulled, Interaction.Requirements,
+      Channel.toRaw]
+    exact .inr (by simp [circuit_norm])
+  · simp [AbstractInteraction.eval, ChannelInteraction.toRaw, pushedIf] at h_pull
+
+/-- Stages, newest first. The ALU bus is finished in two classes: first every message that is
+not MIN, then the MIN messages. -/
+def stages : List (Stage (F p)) :=
+  [{ channel := Alu.channel.toRaw, cls := isMinMsg },
+   { channel := Alu.channel.toRaw, cls := fun m => !isMinMsg m },
+   { channel := Msb16C }, { channel := IsHalfC }, { channel := Bitwise.AreBytes.toRaw }]
+
+def ensembleMin : Ensemble (F p) unit where
+  tables := [providerComponent Bitwise.AreBytes, countedProviderComponent muMax Bitwise.IsHalf,
+    countedProviderComponent muMax Bitwise.Msb16, ltComponent, minComponent]
+  unique_names := by
+    simp [providerComponent, countedProviderComponent, ltComponent, minComponent, provider,
+      countedProvider, LT.circuit, MinToy.circuit, Bitwise.AreBytes, Bitwise.IsHalf, Bitwise.Msb16,
+      Bitwise.areBytesTable, Bitwise.isHalfTable, Bitwise.msb16Table, StaticLookupChannel.toChannel]
+  channels := finished
+  unique_channel_names := ensemble.unique_channel_names
+  tables_channels := by
+    intro table h
+    simp only [List.mem_cons, List.not_mem_nil, or_false] at h
+    rcases h with rfl | rfl | rfl | rfl | rfl <;>
+      simp only [GeneralFormalCircuit.channels, providerComponent_guarantees,
+        providerComponent_requirements, countedProviderComponent_guarantees,
+        countedProviderComponent_requirements, ltComponent_guarantees, ltComponent_requirements,
+        minComponent_guarantees, minComponent_requirements] <;>
+      simp [finished, IsHalfC, Msb16C]
+  verifier_channels := by simp [circuit_norm]
+
+/-- A channel other than ALU, by name. -/
+lemma ne_alu {c : RawChannel (F p)}
+    (hc : c = IsHalfC ∨ c = Msb16C ∨ c = Bitwise.AreBytes.toRaw) : c ∉ [Alu.channel.toRaw] := by
+  rw [List.mem_singleton]
+  intro h
+  have := congrArg RawChannel.name h
+  rcases hc with rfl | rfl | rfl <;>
+    simp [circuit_norm, IsHalfC, Msb16C, Alu.channel, Bitwise.AreBytes, Bitwise.IsHalf,
+      Bitwise.Msb16, Bitwise.areBytesTable, Bitwise.isHalfTable, Bitwise.msb16Table,
+      StaticLookupChannel.toChannel, Channel.counted, Channel.toRaw] at this
+
+theorem tableSoundness_withMin : ensembleMin.TableSoundness (Balance.logUpUpTo muMax) := by
+  apply Ensemble.tableSoundness_of_stagedOn stages rfl
+  · intro s hs
+    simp only [stages, List.mem_cons, List.not_mem_nil, or_false] at hs
+    rcases hs with rfl | rfl | rfl | rfl | rfl <;> simp [ensembleMin, finished]
+  · intro component h c hc msg
+    simp only [ensembleMin, List.mem_cons, List.not_mem_nil, or_false] at h
+    rcases h with rfl | rfl | rfl | rfl | rfl
+    iterate 3 simp [providerComponent_guarantees, countedProviderComponent_guarantees] at hc
+    · rw [ltComponent_guarantees] at hc
+      simp only [List.mem_cons, List.not_mem_nil, or_false] at hc
+      rcases hc with rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> simp [stages]
+    · rw [minComponent_guarantees, List.mem_singleton] at hc
+      subst hc
+      cases h : isMinMsg msg
+      · exact ⟨{ channel := Alu.channel.toRaw, cls := fun m => !isMinMsg m }, by simp [stages],
+          rfl, by simp [h]⟩
+      · exact ⟨{ channel := Alu.channel.toRaw, cls := isMinMsg }, by simp [stages], rfl, h⟩
+  · intro s hs
+    show s.channel.ConsistentUpTo muMax
+    simp only [stages, List.mem_cons, List.not_mem_nil, or_false] at hs
+    rcases hs with rfl | rfl | rfl | rfl | rfl <;> infer_instance
+  · intro component h
+    simp only [ensembleMin, List.mem_cons, List.not_mem_nil, or_false] at h
+    rcases h with rfl | rfl | rfl | rfl | rfl
+    -- the providers pull nothing
+    iterate 3
+      refine ⟨?_, ?_, ?_, ?_, ?_, trivial⟩ <;>
+        exact Component.requirementsAfterOn_of_guarantees_subset (by
+          simp [providerComponent_guarantees, countedProviderComponent_guarantees])
+    -- LT: both ALU classes after its pulls, the counted pulls after ARE_BYTES
+    · refine ⟨?_, ?_, ?_, ?_, ?_, trivial⟩
+      iterate 2
+        apply Component.requirementsAfterOn_of_guarantees_subset
+        rw [ltComponent_guarantees]
+        intro c hc msg
+        simp only [List.mem_cons, List.not_mem_nil, or_false] at hc
+        rcases hc with rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> simp
+      · exact Component.requirementsAfterOn_of_requirementsAfter
+          (lt_requirementsAfter_counted (earlier := [IsHalfC, Bitwise.AreBytes.toRaw]) (.inr rfl)
+            (by simp))
+          (by
+            intro c hc
+            simp only [List.mem_cons, List.not_mem_nil, or_false] at hc
+            rcases hc with rfl | rfl
+            · exact ⟨{ channel := IsHalfC }, by simp, rfl, fun _ => rfl⟩
+            · exact ⟨{ channel := Bitwise.AreBytes.toRaw }, by simp, rfl, fun _ => rfl⟩)
+      · exact Component.requirementsAfterOn_of_requirementsAfter
+          (lt_requirementsAfter_counted (earlier := [Bitwise.AreBytes.toRaw]) (.inl rfl) (by simp))
+          (by
+            intro c hc
+            rw [List.mem_singleton] at hc
+            subst hc
+            exact ⟨{ channel := Bitwise.AreBytes.toRaw }, by simp, rfl, fun _ => rfl⟩)
+      · apply Component.requirementsAfterOn_of_not_mem
+        simp only [ltComponent_requirements, List.mem_cons, List.not_mem_nil, or_false, not_or]
+        refine ⟨fun h => ?_, fun h => ?_, fun h => ?_⟩ <;> have := congrArg RawChannel.name h <;>
+          simp [circuit_norm, IsHalfC, Msb16C, Alu.channel, Bitwise.AreBytes, Bitwise.IsHalf,
+            Bitwise.Msb16, Bitwise.areBytesTable, Bitwise.isHalfTable, Bitwise.msb16Table,
+            StaticLookupChannel.toChannel] at this
+    -- MIN: the MIN class after the other ALU class, which holds its LT pull
+    · refine ⟨?_, ?_, ?_, ?_, ?_, trivial⟩
+      · apply Component.requirementsAfterOn_of_covered
+        intro table h_comp c hc i h_i h_pull
+        rw [minComponent_guarantees, List.mem_singleton] at hc
+        subst hc
+        rcases min_alu_shape h_comp h_i with ⟨-, h_cls⟩ | ⟨h_push, -⟩
+        · exact ⟨{ channel := Alu.channel.toRaw, cls := fun m => !isMinMsg m }, by simp,
+            rfl, by simp [h_cls]⟩
+        · simp [h_push] at h_pull
+      · -- on the other class MIN owes only its pull's multiplicity, from its constraints
+        rintro table h_comp - constraints - i h_i h_cls
+        rcases min_alu_shape h_comp h_i with ⟨h_pull, -⟩ | ⟨-, h_min⟩
+        · exact min_pull_requirements h_comp constraints h_i h_pull
+        · simp [h_min] at h_cls
+      all_goals
+        apply Component.requirementsAfterOn_of_not_mem
+        rw [minComponent_requirements]
+        exact ne_alu (by simp)
+
+end LambdaVM.Ensembles.LtStaged
diff --git a/formal/LambdaVM/Tables/Eq.lean b/formal/LambdaVM/Tables/Eq.lean
index 3fcee4831..380b14e0f 100644
--- a/formal/LambdaVM/Tables/Eq.lean
+++ b/formal/LambdaVM/Tables/Eq.lean
@@ -165,7 +165,7 @@ def circuit : GeneralFormalCircuit (F p) Row unit where
     -- the flag byte, read as a natural
     have hflagsV : (3 + 64 * input_invert : F p).val = 3 + 64 * input_invert.val :=
       val_eq_of_eq_natCast (by push_cast; simp only [ZMod.natCast_zmod_val]) (by omega)
-    refine ⟨?_, ?_, ?_⟩
+    refine ⟨?_, ?_, ?_, ?_⟩
     · -- the LT clause does not apply: opsel(EQ) + 64·i ≠ opsel(LT) + 32·s + 64·i'
       intro s i hs hi hflags
       exfalso; rw [hflagsV] at hflags; simp only [opselLT] at hflags; omega
@@ -173,6 +173,10 @@ def circuit : GeneralFormalCircuit (F p) Row unit where
     · -- nor the SHIFT clause
       intro w s d hw hs hd hflags
       exfalso; rw [hflagsV] at hflags; simp only [opselSHIFT] at hflags; omega
+    swap
+    · -- nor the MIN clause
+      intro hflags
+      exfalso; rw [hflagsV] at hflags; simp only [Alu.opselMIN] at hflags; omega
     intro i hi hflags
     rw [hflagsV] at hflags; simp only [opselEQ] at hflags
     rw [key ha0 ha1 hb0 hb1, show input_invert.val = i by omega]
diff --git a/formal/LambdaVM/Tables/Lt.lean b/formal/LambdaVM/Tables/Lt.lean
index 89de939f8..badb095b6 100644
--- a/formal/LambdaVM/Tables/Lt.lean
+++ b/formal/LambdaVM/Tables/Lt.lean
@@ -1,6 +1,7 @@
 module
 
 public import LambdaVM.Tables.Bitwise
+public import Clean.Air.CountedChannel
 public import LambdaVM.Buses.Alu
 public import LambdaVM.Templates.IsBit
 public import LambdaVM.Templates.Add
@@ -70,17 +71,24 @@ theorem core
   rw [Alu.slt_ofNat_iff (by omega) (by omega)]
   split_ifs <;> omega
 
+/-- The largest multiplicity of an LT row: `MU_MAX` in `prover/src/tables/types.rs`. -/
+abbrev muMax : ℕ := 255
+
+/-- `IS_HALF` and `MSB16` with pulls of multiplicity up to `muMax`. -/
+abbrev IsHalfC : RawChannel (F p) := Bitwise.IsHalf.counted muMax
+abbrev Msb16C : RawChannel (F p) := Bitwise.Msb16.counted muMax
+
 def main (r : Var Row (F p)) : Circuit (F p) Unit := do
-  -- μ : Bit here; the spec and lt.rs range-check it as a byte (see README).
-  isBit r.mu
+  -- μ : Byte, as in the spec and lt.rs: ARE_BYTES[μ, 0]
+  Bitwise.AreBytes.pull (r.mu, 0)
   -- range: IS_HALF[lhs[1]], IS_HALF[rhs[1]], IS_BIT<signed>, IS_BIT<invert>
-  Bitwise.IsHalf.pullIf r.mu r.lhs1
-  Bitwise.IsHalf.pullIf r.mu r.rhs1
+  Bitwise.IsHalf.pullUpTo muMax r.mu r.lhs1
+  Bitwise.IsHalf.pullUpTo muMax r.mu r.rhs1
   isBit r.signed
   isBit r.invert
   -- defs: MSB16[lhs[2]] -> lhs_msb, MSB16[rhs[2]] -> rhs_msb
-  Bitwise.Msb16.pullIf r.mu (r.lhs2, r.lhsMsb)
-  Bitwise.Msb16.pullIf r.mu (r.rhs2, r.rhsMsb)
+  Bitwise.Msb16.pullUpTo muMax r.mu (r.lhs2, r.lhsMsb)
+  Bitwise.Msb16.pullUpTo muMax r.mu (r.rhs2, r.rhsMsb)
   let lhsHi := r.lhs1 + 65536 * r.lhs2
   let rhsHi := r.rhs1 + 65536 * r.rhs2
   let subLo := r.lhsSubRhs0 + 65536 * r.lhsSubRhs1
@@ -94,11 +102,11 @@ def main (r : Var Row (F p)) : Circuit (F p) Unit := do
   assertZero (r.res + 2 * r.lt * r.invert - r.lt - r.invert)
   -- sub: IS_BIT<carry[i]>, IS_HALF[lhs_sub_rhs[i]]
   sub ⟨r.lhs0, lhsHi⟩ ⟨r.rhs0, rhsHi⟩ ⟨subLo, subHi⟩
-  Bitwise.IsHalf.pullIf r.mu r.lhsSubRhs0
-  Bitwise.IsHalf.pullIf r.mu r.lhsSubRhs1
-  Bitwise.IsHalf.pullIf r.mu r.lhsSubRhs2
-  Bitwise.IsHalf.pullIf r.mu r.lhsSubRhs3
-  -- output: ALU[lhs, rhs, opsel(LT) + 32·signed + 64·invert] -> [res, 0]
+  Bitwise.IsHalf.pullUpTo muMax r.mu r.lhsSubRhs0
+  Bitwise.IsHalf.pullUpTo muMax r.mu r.lhsSubRhs1
+  Bitwise.IsHalf.pullUpTo muMax r.mu r.lhsSubRhs2
+  Bitwise.IsHalf.pullUpTo muMax r.mu r.lhsSubRhs3
+  -- output: ALU[lhs, rhs, opsel(LT) + 32·signed + 64·invert] -> [res, 0], μ times
   Alu.channel.pushIf r.mu
     ⟨r.lhs0, lhsHi, r.rhs0, rhsHi, 4 + 32 * r.signed + 64 * r.invert, r.res, 0⟩
 
@@ -147,7 +155,7 @@ lemma res_constraint {lt invert res : F p} {ltv iv : ℕ}
 
 /-- The honest prover's row, as `generate_lt_trace` fills it. -/
 def Honest (r : Row (F p)) : Prop :=
-  IsBool r.mu ∧ IsBool r.signed ∧ IsBool r.invert ∧
+  r.mu.val < 2^8 ∧ IsBool r.signed ∧ IsBool r.invert ∧
   r.lhs0.val < 2^32 ∧ r.lhs1.val < 2^16 ∧ r.lhs2.val < 2^16 ∧
   r.rhs0.val < 2^32 ∧ r.rhs1.val < 2^16 ∧ r.rhs2.val < 2^16 ∧
   r.lhsSubRhs0.val < 2^16 ∧ r.lhsSubRhs1.val < 2^16 ∧ r.lhsSubRhs2.val < 2^16 ∧ r.lhsSubRhs3.val < 2^16 ∧
@@ -160,46 +168,46 @@ def Honest (r : Row (F p)) : Prop :=
 
 /-- What an active row establishes: with range-checked low words, `res` is the comparison bit. -/
 def RowSpec (r : Row (F p)) : Prop :=
-  r.mu = 1 → r.lhs0.val < 2^32 → r.rhs0.val < 2^32 →
+  r.mu ≠ 0 → r.lhs0.val < 2^32 → r.rhs0.val < 2^32 →
     r.res = ((ltBit r.signed.val r.invert.val r.lhsVal r.rhsVal : ℕ) : F p)
 
 def circuit : GeneralFormalCircuit (F p) Row unit where
+  name := "LT"
   main
   Spec r _ _ := RowSpec r
-  channelsWithRequirements := [Alu.channel.toRaw]
+  channelsWithRequirements := [Alu.channel.toRaw, IsHalfC, Msb16C]
   requirementsChannelsLawful input_var i₀ := by
-    obtain ⟨lhs0, lhs1, lhs2, rhs0, rhs1, rhs2, signed, lt, lhsSubRhs0, lhsSubRhs1, lhsSubRhs2, lhsSubRhs3,
-      lhsMsb, rhsMsb, invert, res, mu⟩ := input_var
-    simp only [circuit_norm, main, isBit, sub, add, Add.carry0, Add.carry1, Alu.channel,
-      Bitwise.isHalfTable, Bitwise.msb16Table]
-    constructor
-    · intro channel h; tauto
-    · intro env h
-      -- each pull owes a multiplicity of 0 or 1: μ is a bit
-      exact mul_one_sub_eq_zero_iff.mp h.1
+    obtain ⟨lhs0, lhs1, lhs2, rhs0, rhs1, rhs2, signed, lt, lhsSubRhs0, lhsSubRhs1, lhsSubRhs2,
+      lhsSubRhs3, lhsMsb, rhsMsb, invert, res, mu⟩ := input_var
+    simp only [circuit_norm, main, isBit, sub, add, Add.carry0, Add.carry1, IsHalfC, Msb16C,
+      Bitwise.IsHalf, Bitwise.Msb16, Bitwise.AreBytes]
+    intro channel h
+    tauto
 
   soundness := by
     circuit_proof_start [main, isBit, sub, add, Add.carry0, Add.carry1, RowSpec, Row.lhsVal, Row.rhsVal,
-      dword, Alu.channel, Alu.Guarantees, Bitwise.isHalfTable, Bitwise.msb16Table]
-    obtain ⟨h_mu, h_l1, h_r1, h_s, h_i, h_lm, h_rm, h_lt, h_res, h_c0, h_c1, h_s0, h_s1, h_s2, h_s3⟩ :=
-      h_holds
-    -- μ ∈ {0, 1}; with μ = 0 every requirement is vacuous
-    rcases mul_one_sub_eq_zero_iff.mp h_mu with h0 | h1
-    · subst h0; simp
-    subst h1
+      dword, Alu.channel, Alu.Guarantees, Bitwise.isHalfTable, Bitwise.msb16Table, Bitwise.areBytesTable]
+    obtain ⟨⟨h_mu, -⟩, h_l1, h_r1, h_s, h_i, h_lm, h_rm, h_lt, h_res, h_c0, h_c1, h_s0, h_s1, h_s2,
+      h_s3⟩ := h_holds
+    -- with μ = 0 every requirement is vacuous
+    by_cases h0 : input_mu = 0
+    · simp [h0]
+    -- otherwise ARE_BYTES[μ, 0] makes μ a count of at most 255, so the pulls get their guarantees
+    have hcount : Channel.CountUpTo muMax input_mu :=
+      Channel.countUpTo_of_val h0 (by simp only [muMax]; omega)
     have hsb : IsBool input_signed := mul_one_sub_eq_zero_iff.mp h_s
     have hib : IsBool input_invert := mul_one_sub_eq_zero_iff.mp h_i
     have hs_2 := IsBool.val_lt_two hsb
     have hi_2 := IsBool.val_lt_two hib
     -- the pulled guarantees are now unconditional
-    have hl1 := h_l1 rfl
-    have hr1 := h_r1 rfl
-    obtain ⟨hl2, hlm⟩ := h_lm rfl
-    obtain ⟨hr2, hrm⟩ := h_rm rfl
-    have hs0 := h_s0 rfl
-    have hs1 := h_s1 rfl
-    have hs2 := h_s2 rfl
-    have hs3 := h_s3 rfl
+    have hl1 := h_l1 hcount
+    have hr1 := h_r1 hcount
+    obtain ⟨hl2, hlm⟩ := h_lm hcount
+    obtain ⟨hr2, hrm⟩ := h_rm hcount
+    have hs0 := h_s0 hcount
+    have hs1 := h_s1 hcount
+    have hs2 := h_s2 hcount
+    have hs3 := h_s3 hcount
     -- values of the composite limbs
     have hval_lhsHi : (input_lhs1 + 65536 * input_lhs2).val = input_lhs1.val + 65536 * input_lhs2.val :=
       val_eq_of_eq_natCast (by push_cast; simp only [ZMod.natCast_zmod_val]) (by omega)
@@ -255,14 +263,14 @@ def circuit : GeneralFormalCircuit (F p) Row unit where
       first
       | (exfalso; omega)
       | (subst hlt'; norm_num at hres'; simp [hAv, hBv, hC, hres'])
-    refine ⟨fun _ hl0 hr0 => key _ _ rfl rfl hl0 hr0, by simp, by simp, by simp, by simp, by simp,
-      by simp, by simp, by simp, ?_⟩
+    refine ⟨fun _ hl0 hr0 => key _ _ rfl rfl hl0 hr0, .inr hcount, .inr hcount, .inr hcount,
+      .inr hcount, .inr hcount, .inr hcount, .inr hcount, .inr hcount, ?_⟩
     intro _ hl0 hlhi hr0 hrhi
     -- the flag byte, read as a natural
     have hflagsV : (4 + 32 * input_signed + 64 * input_invert : F p).val
         = 4 + 32 * input_signed.val + 64 * input_invert.val :=
       val_eq_of_eq_natCast (by push_cast; simp only [ZMod.natCast_zmod_val]) (by omega)
-    refine ⟨?_, ?_, ?_⟩
+    refine ⟨?_, ?_, ?_, ?_⟩
     · intro s i hs hi hflags
       rw [hflagsV] at hflags; simp only [opselLT] at hflags
       rw [key s i (by omega) (by omega) hl0 hr0, hval_lhsHi, hval_rhsHi]
@@ -272,13 +280,16 @@ def circuit : GeneralFormalCircuit (F p) Row unit where
     · -- nor the SHIFT clause: opsel(SHIFT) + w + 32·s + 64·d ≡ 5 or 6 (mod 32)
       intro w s d hw hs hd hflags
       exfalso; rw [hflagsV] at hflags; simp only [opselSHIFT] at hflags; omega
+    · -- nor the MIN clause
+      intro hflags
+      exfalso; rw [hflagsV] at hflags; simp only [Alu.opselMIN] at hflags; omega
 
 
   ProverAssumptions r _ _ := Honest r
 
   completeness := by
     circuit_proof_start [main, isBit, sub, add, Add.carry0, Add.carry1, Alu.channel, Alu.Guarantees,
-      Bitwise.isHalfTable, Bitwise.msb16Table, Honest, Row.lhsVal, Row.rhsVal]
+      Bitwise.isHalfTable, Bitwise.msb16Table, Bitwise.areBytesTable, Honest, Row.lhsVal, Row.rhsVal]
     obtain ⟨hmu, hsb, hib, hl0, hl1, hl2, hr0, hr1, hr2, hs0, hs1, hs2, hs3, hsum, hlm, hrm, hlt, hres⟩ :=
       h_assumptions
     set L := input_lhs0.val + 2^32 * (input_lhs1.val + 65536 * input_lhs2.val) with hL
@@ -314,7 +325,7 @@ def circuit : GeneralFormalCircuit (F p) Row unit where
     have hres_cast : input_res = ((ltRaw input_signed.val L R + input_invert.val
         - 2 * ltRaw input_signed.val L R * input_invert.val : ℕ) : F p) := by
       rw [← ltBit_eq (IsBool.val_lt_two hib), ← hres, ZMod.natCast_zmod_val]
-    refine ⟨mul_one_sub_eq_zero_iff.mpr hmu, fun _ => by omega, fun _ => by omega,
+    refine ⟨⟨hmu, by simp⟩, fun _ => by omega, fun _ => by omega,
       mul_one_sub_eq_zero_iff.mpr hsb, mul_one_sub_eq_zero_iff.mpr hib,
       fun _ => ⟨by omega, hlm⟩, fun _ => ⟨by omega, hrm⟩, ?_, ?_, ?_, ?_,
       fun _ => by omega, fun _ => by omega, fun _ => by omega, fun _ => by omega⟩
@@ -326,5 +337,4 @@ def circuit : GeneralFormalCircuit (F p) Row unit where
     · rw [hc0k]; rcases (by omega : k0 = 0 ∨ k0 = 1) with rfl | rfl <;> simp
     · rw [hc1k]; rcases (by omega : k1 = 0 ∨ k1 = 1) with rfl | rfl <;> simp
 
-
 end LambdaVM.LT
diff --git a/formal/LambdaVM/Tables/MinToy.lean b/formal/LambdaVM/Tables/MinToy.lean
new file mode 100644
index 000000000..b86dee773
--- /dev/null
+++ b/formal/LambdaVM/Tables/MinToy.lean
@@ -0,0 +1,98 @@
+module
+
+public import LambdaVM.Buses.Alu
+public import LambdaVM.Templates.IsBit
+
+@[expose] public section
+
+/-!
+# MIN (toy, for the counted-pulls PoC)
+
+A chip with the shape of DVRM: it pulls an LT result on the ALU bus and pushes its own result on
+the same bus. `out = lt ? a : b` limb by limb, where `lt = (a < b)` comes from the pulled LT
+message. One table, one bus, no cycle: it receives `flags = opsel(LT)` and owes
+`flags = opsel(MIN)`.
+-/
+
+namespace LambdaVM.MinToy
+
+structure Row (F : Type) where
+  a0 : F
+  a1 : F
+  b0 : F
+  b1 : F
+  lt : F
+  out0 : F
+  out1 : F
+  mu : F
+deriving ProvableStruct
+
+def main (r : Var Row (F p)) : Circuit (F p) Unit := do
+  isBit r.mu
+  -- ALU[a, b, opsel(LT)] -> [lt, 0]: unsigned, no invert. Pulled on every row, padding included.
+  Alu.channel.pull ⟨r.a0, r.a1, r.b0, r.b1, 4, r.lt, 0⟩
+  -- out = lt ? a : b
+  assertZero (r.out0 - (r.lt * r.a0 + (1 - r.lt) * r.b0))
+  assertZero (r.out1 - (r.lt * r.a1 + (1 - r.lt) * r.b1))
+  -- ALU[a, b, opsel(MIN)] -> out
+  Alu.channel.pushIf r.mu ⟨r.a0, r.a1, r.b0, r.b1, 7, r.out0, r.out1⟩
+
+lemma val_lit (n : ℕ) (h : n < 2^40) : ((n : F p)).val = n :=
+  ZMod.val_natCast_of_lt (lt_p_of_lt_two_pow_40 h)
+
+/-- The honest prover's row: `lt` is the comparison and `out` the selected operand. -/
+def Honest (r : Row (F p)) : Prop :=
+  IsBool r.mu ∧ r.lt = ((Alu.ltBit 0 0 (dword r.a0 r.a1) (dword r.b0 r.b1) : ℕ) : F p) ∧
+  r.out0 = r.lt * r.a0 + (1 - r.lt) * r.b0 ∧ r.out1 = r.lt * r.a1 + (1 - r.lt) * r.b1
+
+def circuit : GeneralFormalCircuit (F p) Row unit where
+  name := "MIN"
+  main
+  Spec _ _ _ := True
+  channelsWithRequirements := [Alu.channel.toRaw]
+  soundness := by
+    circuit_proof_start [main, isBit, Alu.channel, Alu.Guarantees]
+    obtain ⟨-, h_pull, h_o0, h_o1⟩ := h_holds
+    intro _ ha0 ha1 hb0 hb1
+    have h4 : (4 : F p).val = 4 := by simpa using val_lit 4 (by norm_num)
+    have h7 : (7 : F p).val = 7 := by simpa using val_lit 7 (by norm_num)
+    -- the pulled LT result, with μ = 1
+    obtain ⟨hLT, -⟩ := h_pull ha0 ha1 hb0 hb1
+    have hlt := hLT 0 0 (by norm_num) (by norm_num) (by rw [h4]; simp [opselLT])
+    have hL : dword input_a0 input_a1 < 2^64 := by unfold dword; omega
+    have hR : dword input_b0 input_b1 < 2^64 := by unfold dword; omega
+    rw [h7]
+    -- only the MIN clause applies to flags = 7
+    refine ⟨fun s i hs hi h => by simp only [opselLT] at h; omega,
+      fun i hi h => by simp only [opselEQ] at h; omega,
+      fun w s d hw hs hd h => by simp only [opselSHIFT] at h; omega, fun _ => ?_⟩
+    by_cases hLR : dword input_a0 input_a1 < dword input_b0 input_b1
+    · have h1 : input_lt = 1 := by
+        rw [hlt]; simp [Alu.ltBit, Alu.ltRaw, Alu.ult_ofNat_iff hL hR, hLR]
+      have e0 : input_out0 = input_a0 := by rw [h1] at h_o0; linear_combination h_o0
+      have e1 : input_out1 = input_a1 := by rw [h1] at h_o1; linear_combination h_o1
+      rw [e0, e1, min_eq_left hLR.le]
+      exact ⟨ha0, ha1, rfl⟩
+    · have h1 : input_lt = 0 := by
+        rw [hlt]; simp [Alu.ltBit, Alu.ltRaw, Alu.ult_ofNat_iff hL hR, hLR]
+      have e0 : input_out0 = input_b0 := by rw [h1] at h_o0; linear_combination h_o0
+      have e1 : input_out1 = input_b1 := by rw [h1] at h_o1; linear_combination h_o1
+      rw [e0, e1, min_eq_right (not_lt.mp hLR)]
+      exact ⟨hb0, hb1, rfl⟩
+
+  ProverAssumptions r _ _ := Honest r
+  completeness := by
+    circuit_proof_start [main, isBit, Alu.channel, Alu.Guarantees, Honest]
+    obtain ⟨hmu, hlt, ho0, ho1⟩ := h_assumptions
+    have h4 : (4 : F p).val = 4 := by simpa using val_lit 4 (by norm_num)
+    refine ⟨mul_one_sub_eq_zero_iff.mpr hmu, ?_, by rw [ho0]; ring, by rw [ho1]; ring⟩
+    intro _ _ _ _
+    rw [h4]
+    refine ⟨fun s i hs hi h => ?_, fun i hi h => by simp only [opselEQ] at h; omega,
+      fun w s d hw hs hd h => by simp only [opselSHIFT] at h; omega,
+      fun h => by simp only [Alu.opselMIN] at h; omega⟩
+    simp only [opselLT] at h
+    obtain ⟨rfl, rfl⟩ : s = 0 ∧ i = 0 := by omega
+    exact hlt
+
+end LambdaVM.MinToy
diff --git a/formal/LambdaVM/Tables/Shift.lean b/formal/LambdaVM/Tables/Shift.lean
index 3b9afedbf..9016373f6 100644
--- a/formal/LambdaVM/Tables/Shift.lean
+++ b/formal/LambdaVM/Tables/Shift.lean
@@ -508,13 +508,17 @@ theorem soundness :
     have hflagsV : (5 + input_wordInstr + 32 * input_signed + 64 * input_direction : F p).val
         = 5 + input_wordInstr.val + 32 * input_signed.val + 64 * input_direction.val :=
       val_eq_of_eq_natCast (by push_cast; simp only [ZMod.natCast_zmod_val]) (by omega)
-    refine ⟨?_, ?_, ?_⟩
+    refine ⟨?_, ?_, ?_, ?_⟩
     · -- not LT: 5 + w + 32 s + 64 d ≠ 4 + 32 s' + 64 i (mod 32)
       intro s i hs hi hflags
       exfalso; rw [hflagsV] at hflags; simp only [opselLT] at hflags; omega
     · -- not EQ
       intro i hi hflags
       exfalso; rw [hflagsV] at hflags; simp only [opselEQ] at hflags; omega
+    swap
+    · -- not MIN
+      intro hflags
+      exfalso; rw [hflagsV] at hflags; simp only [Alu.opselMIN] at hflags; omega
     · intro w s d hw hs hd hflags
       rw [hflagsV] at hflags; simp only [opselSHIFT] at hflags
       obtain ⟨rfl, rfl, rfl⟩ : input_wordInstr.val = w ∧ input_signed.val = s ∧
diff --git a/formal/README.md b/formal/README.md
index b7f834d01..f9ca91344 100644
--- a/formal/README.md
+++ b/formal/README.md
@@ -25,8 +25,9 @@ FRI / WHIR prover, the LogUp argument itself, the executor, GPU code.
 - `LambdaVM/Buses/` — the buses that are not static tables. `Alu.lean` is the
   unified ALU bus: message layout as in `BusId::Alu`, the caller's `IS_WORD`
   assumptions on both operands as hypotheses, and one `Guarantees` clause per
-  `opsel` (LT, EQ and SHIFT). The flag byte is read as a natural, so a chip
-  pushing with one `opsel` discharges the other clauses by `omega`.
+  `opsel` (LT, EQ, SHIFT and the toy MIN of the counted-pulls PoC). The flag
+  byte is read as a natural, so a chip pushing with one `opsel` discharges the
+  other clauses by `omega`.
 - `LambdaVM/Tables/` — one file per chip. `Bitwise.lean` transcribes the
   precomputed row function of `prover/src/tables/bitwise.rs` and defines each bus
   the table serves as a `StaticLookupChannel` (read through `toChannel`), with
@@ -49,7 +50,8 @@ FRI / WHIR prover, the LogUp argument itself, the executor, GPU code.
   first global theorem: for any witness whose constraints hold and whose
   channels balance, every EQ row with `μ = 1` and range-checked operands
   carries the equality bit. The lookup argument is what turns the pulled range
-  checks into facts.
+  checks into facts. `LtStaged.lean` and `CountedSameBus.lean` are the
+  counted-pulls ensembles (see below).
 - `LambdaVM/Tables/ShiftCore.lean` and `Shift.lean` — the SHIFT chip. `ShiftCore`
   is the two-phase shift argument of `spec/shift.typ` on naturals (HWSL
   per limb, then whole limbs, left and right, logical and arithmetic), ending in
@@ -58,6 +60,10 @@ FRI / WHIR prover, the LogUp argument itself, the executor, GPU code.
   overrides) and concludes `shiftResult`. `Shift.lean` mirrors the 22 constraints
   and 17 interactions of `shift.rs` and proves soundness and completeness, the
   latter for both the honest active row and the padding row.
+- `LambdaVM/Tables/MinToy.lean` — MIN, a toy ALU operation with the shape of
+  DVRM: it pulls an LT result on the ALU bus and pushes its own result on the
+  same bus. Not an RV64IM operation; it stands in for DVRM until DVRM is
+  modelled.
 
 ## Lessons for big chips (from SHIFT)
 
@@ -99,8 +105,8 @@ Result on `main` after that merge, 2026-10-28:
 
 - EQ: 5 constraints and 6 interactions, exact match.
 - SHIFT: 22 constraints and 17 interactions, exact match.
-- LT: exact match except the two documented deltas: `μ·(1 − μ) = 0` exists
-  only in Lean, `ARE_BYTES[μ, 0]` exists only in Rust.
+- LT: 6 constraints and 10 interactions, exact match, with `μ` a byte as in
+  `lt.rs`.
 
 The check compares polynomials, not zero sets: it caught `μ·(μ − 1)` versus
 `μ·(1 − μ)` in EQ, which is why the Lean bit constraints use the spec's form.
@@ -139,26 +145,42 @@ multiplicity is a requirement the row cannot meet.
   `channelsWithRequirements`: an out-of-range `μ` is only ruled out by the byte
   guarantee, which lawfulness does not see but soundness does.
 
-What upstream Clean needs for an end-to-end LT theorem with byte `μ`:
+An end-to-end LT theorem with byte `μ` needs two things Clean main lacks:
 
 1. A `Balance` for counted pulls: `BalancedInteractions` matching a pull of
    `1, …, N`, and a `fits` that bounds `N * count` rather than `count` by the
    characteristic.
-2. Either a dependency-aware `OrderedChannel` (a table may hold guarantees and
+2. A dependency-aware finishing order: a table may hold guarantees and
    requirements on the same channel when the requirements depend only on
-   channels finished earlier), or the range check of `μ` as a static `lookup`,
-   which is a local constraint and makes the requirement vacuous at lawfulness.
-
-Until then LT keeps `μ ∈ {0, 1}` (see below).
+   channels finished earlier.
+
+The model takes both from the `counted-pulls` branch of
+[yetanotherco/clean](https://github.com/yetanotherco/clean/tree/counted-pulls),
+Clean main `f3abad7c` plus three commits: `Balance.logUpUpTo N` with
+`RawChannel.ConsistentUpTo N`, the typed `Channel.counted N`, and
+`Ensemble.tableSoundness_of_staged` / `_stagedOn` (soundness by finishing
+order of channels, and of message classes within a channel). On top of it:
+
+- `Tables/Lt.lean` pulls `IS_HALF` and `MSB16` with multiplicity `μ` through
+  `Channel.counted 255`, bounded by its own pull of `ARE_BYTES[μ, 0]`, exactly
+  as `lt.rs`.
+- `Ensembles/LtStaged.lean` proves the LT ensemble sound under
+  `Balance.logUpUpTo 255`, finishing `ARE_BYTES` before the counted `IS_HALF`
+  and `MSB16` and those before ALU. Its second half adds MIN, which pulls LT
+  and pushes MIN on the ALU bus: ALU is finished in two stages, the non-MIN
+  messages first and the MIN messages after.
+- `Ensembles/CountedSameBus.lean` (CMIN) does the same with the ALU bus itself
+  counted: a row answers `μ` identical MIN requests, the full shape of DVRM.
+
+`Channels/Counted.lean` above predates the fork. Its `not_consistent` is the
+reason the fork's balance carries the `N * count` bound; its `consistentUpTo`
+shows the counted channel is consistent under the fork's `BalancedUpTo N`.
+Nothing else uses it.
 
 ## Known differences from the Rust prover
 
-- `LT` constrains `μ·(1 − μ) = 0`. The spec types `μ` as `Byte` with
-  `IS_BYTE[μ]` and `lt.rs` sends `ARE_BYTES[μ, 0]`, because LT deduplicates
-  rows and `μ` is a count. Clean only grants a channel guarantee to a pull with
-  multiplicity exactly 1, so until the counted pulls above land upstream the
-  model keeps `μ` a bit. Every chip whose `μ` the spec types as `Byte` (MUL,
-  DVRM, BRANCH, BYTEWISE) will need the same treatment.
+- Every chip whose `μ` the spec types as `Byte` (MUL, DVRM, BRANCH, BYTEWISE)
+  needs the counted treatment LT got above; none of them is modelled yet.
 - The `spec/` copy in this repository lags the `spec/main` branch; the spec the
   models follow is the branch (EQ's `μ` is `Bit` with `IS_BIT[μ]` there).
 
diff --git a/formal/export/lt.json b/formal/export/lt.json
index 800c9d42d..5caa8e178 100644
--- a/formal/export/lt.json
+++ b/formal/export/lt.json
@@ -1,14 +1,9 @@
 {"operations":
- [{"assert":
-   {"type": "mul",
-    "rhs":
-    {"type": "add",
-     "rhs":
-     {"type": "mul",
-      "rhs": {"type": "var", "index": 16},
-      "lhs": {"value": 18446744069414584320, "type": "const"}},
-     "lhs": {"value": 1, "type": "const"}},
-    "lhs": {"type": "var", "index": 16}}},
+ [{"interact":
+   {"multiplicity": {"value": 1, "type": "const"},
+    "message": [{"type": "var", "index": 16}, {"value": 0, "type": "const"}],
+    "direction": "pull",
+    "channel": "ARE_BYTES"}},
   {"interact":
    {"multiplicity": {"type": "var", "index": 16},
     "message": [{"type": "var", "index": 1}],
diff --git a/formal/lake-manifest.json b/formal/lake-manifest.json
index ca5842997..0fd1d9f57 100644
--- a/formal/lake-manifest.json
+++ b/formal/lake-manifest.json
@@ -1,14 +1,14 @@
 {"version": "1.3.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/Verified-zkEVM/clean",
+ [{"url": "https://github.com/yetanotherco/clean",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "f3abad7c099e49f847836c1883dd9e7c539f06f9",
+   "rev": "1cf67e24816808b880aa6af8592047cf42546efc",
    "name": "Clean",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "f3abad7c099e49f847836c1883dd9e7c539f06f9",
+   "inputRev": "1cf67e24816808b880aa6af8592047cf42546efc",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/Verified-zkEVM/CompPoly.git",
diff --git a/formal/lakefile.toml b/formal/lakefile.toml
index 8c801fdea..0f85231ad 100644
--- a/formal/lakefile.toml
+++ b/formal/lakefile.toml
@@ -5,11 +5,13 @@ defaultTargets = ["LambdaVM", "LambdaVMExport"]
 autoImplicit = false
 relaxedAutoImplicit = false
 
-# Clean pinned to a revision; Mathlib and CompPoly come in through Clean's manifest.
+# Clean from the counted-pulls branch of the yetanotherco fork (on Clean main f3abad7c): pulls of
+# multiplicity up to N and soundness by finishing order. Mathlib and CompPoly come in through
+# Clean's manifest.
 [[require]]
 name = "Clean"
-git = "https://github.com/Verified-zkEVM/clean"
-rev = "f3abad7c099e49f847836c1883dd9e7c539f06f9"
+git = "https://github.com/yetanotherco/clean"
+rev = "1cf67e24816808b880aa6af8592047cf42546efc"
 
 [[lean_lib]]
 name = "LambdaVM"
diff --git a/prover/src/tests/lean_diff.rs b/prover/src/tests/lean_diff.rs
index cdabf95e8..0f9521321 100644
--- a/prover/src/tests/lean_diff.rs
+++ b/prover/src/tests/lean_diff.rs
@@ -361,12 +361,11 @@ fn lean_diff_lt() {
         cols::NUM_COLUMNS,
         &rows_of(&trace, cols::NUM_COLUMNS),
     );
-    // Known deltas: the Lean model keeps `μ·(1 − μ) = 0` (assert 0), the Rust chip bounds
-    // `μ` with the `ARE_BYTES[μ, 0]` send instead.
-    assert_eq!(
-        report.lean_asserts_unmatched,
-        vec![0],
-        "[LT] only the μ bit constraint should be Lean-only"
+    // The Lean model bounds `μ` with the `ARE_BYTES[μ, 0]` pull, as the Rust chip does, so the
+    // two agree exactly.
+    assert!(
+        report.lean_asserts_unmatched.is_empty(),
+        "[LT] Lean-only constraints"
     );
     assert!(
         report.rust_constraints_unmatched.is_empty(),
@@ -376,10 +375,9 @@ fn lean_diff_lt() {
         report.lean_interacts_unmatched.is_empty(),
         "[LT] Lean-only interactions"
     );
-    assert_eq!(
-        report.rust_interacts_unmatched,
-        vec![0],
-        "[LT] only ARE_BYTES[μ, 0] should be Rust-only"
+    assert!(
+        report.rust_interacts_unmatched.is_empty(),
+        "[LT] Rust-only interactions"
     );
 }