diff --git a/.github/workflows/formal.yml b/.github/workflows/formal.yml
index 9b1424fa8..1d49c73d0 100644
--- a/.github/workflows/formal.yml
+++ b/.github/workflows/formal.yml
@@ -48,6 +48,40 @@ jobs:
       - name: Build
         run: lake build
 
+      # `LambdaVM/Axioms.lean` is a list of `#print axioms` lines, one per modelled circuit and
+      # per ensemble theorem. It is not part of the library, so `lake build` does not see it.
+      - name: No sorry, no axioms beyond the standard three
+        run: |
+          set -euo pipefail
+          report="${RUNNER_TEMP:-/tmp}/axioms.txt"
+          lake env lean LambdaVM/Axioms.lean | tee "$report"
+
+          # One report per `#print axioms` line: a renamed or deleted declaration fails here
+          # instead of quietly dropping out of the check.
+          expected=$(grep -c '^#print axioms ' LambdaVM/Axioms.lean || true)
+          got=$(grep -c 'depends on axioms\|does not depend on any axioms' "$report" || true)
+          if [ "$expected" -ne "$got" ]; then
+            echo "::error::expected $expected axiom reports, got $got"
+            exit 1
+          fi
+
+          if grep -q 'sorryAx' "$report"; then
+            echo "::error::a modelled circuit or ensemble theorem depends on sorry"
+            exit 1
+          fi
+
+          unexpected=$(
+            sed -n 's/.*depends on axioms: \[\(.*\)\]/\1/p' "$report" \
+              | tr ',' '\n' | sed 's/[[:space:]]//g; /^$/d' | sort -u \
+              | grep -vxF -e propext -e Classical.choice -e Quot.sound || true
+          )
+          if [ -n "$unexpected" ]; then
+            echo "::error::axioms outside propext, Classical.choice, Quot.sound: $(echo $unexpected)"
+            exit 1
+          fi
+
+          echo "$expected declarations checked, no sorry, no extra axioms"
+
       - name: Export is up to date
         run: |
           lake env lean --run LambdaVM/Export.lean
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/Axioms.lean b/formal/LambdaVM/Axioms.lean
new file mode 100644
index 000000000..84265e51b
--- /dev/null
+++ b/formal/LambdaVM/Axioms.lean
@@ -0,0 +1,30 @@
+module
+
+public import LambdaVM
+
+/-!
+# Axiom check
+
+Every modelled circuit and every ensemble theorem must rest on nothing beyond Lean's three
+standard axioms: `propext`, `Classical.choice`, `Quot.sound`. In particular none of them may
+depend on `sorryAx`.
+
+`.github/workflows/formal.yml` runs this file with `lake env lean` and fails if any report
+names `sorryAx` or an axiom outside those three. It also counts the `#print axioms` lines
+here and requires one report for each, so a declaration that stops existing fails the build
+rather than silently dropping out of the check. Add a line for every new circuit, ensemble
+soundness theorem or global row theorem.
+-/
+
+-- The modelled chips. Each `circuit` bundles its own soundness and completeness proofs.
+#print axioms LambdaVM.LT.circuit
+#print axioms LambdaVM.EQ.circuit
+#print axioms LambdaVM.SHIFT.circuit
+#print axioms LambdaVM.MinToy.circuit
+#print axioms LambdaVM.CountedMin.circuit
+
+-- The ensembles.
+#print axioms LambdaVM.Ensembles.eq_rows_correct
+#print axioms LambdaVM.Ensembles.LtStaged.tableSoundness
+#print axioms LambdaVM.Ensembles.LtStaged.tableSoundness_withMin
+#print axioms LambdaVM.CountedMin.tableSoundness
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..29ddf96f8 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)
 
@@ -89,18 +95,18 @@ For each table the test evaluates the Lean asserts and the Rust `ConstraintSet`
 on 64 random rows and matches them as multisets of functions, does the same for
 the interactions (bus id, signed multiplicity, message elements), and checks
 that every Lean constraint vanishes on honest traces from `generate_*_trace`,
-padding rows included; the Lean-only constraints of the documented deltas are
-skipped there. The sign of an interaction comes from its direction: a Rust
-sender is Clean's pull and counts `−m`, a receiver is Clean's push and counts
-`+m`.
+padding rows included. Each test asserts that all four unmatched lists are
+empty: no table has a Lean-only or a Rust-only constraint or interaction left.
+The sign of an interaction comes from its direction: a Rust sender is Clean's
+pull and counts `−m`, a receiver is Clean's push and counts `+m`.
 
 The models follow the multiplicity constraints of PR #1016, merged 2026-10-23.
 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,67 @@ 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 `μ`:
+Counted pulls in the LT model need 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 `tableSoundness`, that is
+  `Ensemble.TableSoundness (Balance.logUpUpTo 255)` for the LT ensemble,
+  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.
+
+That is not an end-to-end LT theorem. `TableSoundness` is one premise of a
+sound ensemble, not the conclusion: it reads `witness.Assumptions →
+witness.Constraints → witness.InteractionsFit balance → witness.Balanced
+balance → witness.Spec`, and leaves `witness.Assumptions` for the caller to
+discharge. In `LtStaged` that premise is not free, because the `ARE_BYTES`,
+`IS_HALF` and `MSB16` providers are not tables. `provider` and
+`countedProvider` are rows that push whatever value they are handed, under
+`Assumptions input data := channel.Guarantees input.1 data`, and
+`providerComponent` and `countedProviderComponent` carry the same assumption
+into the ensemble. Each provider assumes its own answers are correct; nothing
+in the file derives that from a row of BITWISE. `CountedSameBus` reuses those
+two components, so the LT answers it feeds to CMIN are assumed in the same way.
+
+`EqLookup`, in this same PR, is the contrast. Its `pushStatic` emits the
+entries of a real `StaticLookupChannel` and proves the guarantee from
+membership in the table, so `eq_rows_correct` discharges `witness.Assumptions`
+outright — "no component assumes anything" — and states a conclusion about
+rows: every EQ row with `μ = 1` and range-checked operands carries the
+equality bit. There is no `lt_rows_correct`. Writing one needs `pushStatic`,
+or a counted analogue of it, behind LT's three range checks, and this branch
+has neither. What `LtStaged` and `CountedSameBus` do establish is that the
+staged finishing order admits counted pulls, which is what they were written
+for.
+
+`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..a041db1eb 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": "73309694ae33279094597f7f3f819fb8a3439620",
    "name": "Clean",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "f3abad7c099e49f847836c1883dd9e7c539f06f9",
+   "inputRev": "73309694ae33279094597f7f3f819fb8a3439620",
    "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..444ff0a57 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, plus the four review fixes that answer
+# the audit of that branch. 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 = "73309694ae33279094597f7f3f819fb8a3439620"
 
 [[lean_lib]]
 name = "LambdaVM"
diff --git a/prover/src/tests/lean_diff.rs b/prover/src/tests/lean_diff.rs
index cdabf95e8..adb13f3e0 100644
--- a/prover/src/tests/lean_diff.rs
+++ b/prover/src/tests/lean_diff.rs
@@ -261,9 +261,10 @@ fn compare<CS: ConstraintSet<Gl, Gl3>>(
         .collect();
     let rust_interacts_unmatched = ri.iter().map(|&j| interactions[j].bus_id).collect();
 
-    // Every Lean constraint with a Rust counterpart vanishes on the honest trace. The
-    // Lean-only ones are the documented deltas (LT's `μ·(1 − μ)` does not hold on a
-    // deduplicated Rust row with `μ > 1`).
+    // Every Lean constraint with a Rust counterpart vanishes on the honest trace. There are no
+    // Lean-only constraints left: LT's `μ·(1 − μ)` became a pull of `ARE_BYTES[μ, 0]`, as in
+    // `lt.rs`, and every test below asserts that both unmatched lists are empty. The skip is kept
+    // for the next table added here, which may land before its Rust side does.
     for (r, row) in honest_rows.iter().enumerate() {
         for (i, e) in lean.asserts.iter().enumerate() {
             if lean_asserts_unmatched.contains(&i) {
@@ -361,12 +362,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 +376,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"
     );
 }