The emitter loop driver

emitLoopTM body ctr fuel runs body once per mark of the fuel register, incrementing the counter register ctr after each run. Its Hoare rule (emitLoop_hoareTime) is the single lemma behind every runtime loop of the reduction emitter: the t-loops over tableau rows and the position loops over tape cells. The per-iteration emission is an arbitrary word family E : ℕ → List Bool, so nested loops instantiate E with inner loop outputs, and leaf bodies instantiate it with CNF.encode images.

Also here: the arithmetic cap lemma flatCaps (one bound 4·A·B·C·D ≤ M discharges every LitDesc.Spec obligation) and the encode/flatMap distribution lemma.

theorem Complexity.SAT.flatMap_range_succ {α : Type u_1} (E : ℕ → List α) (i : ℕ) : List.flatMap E (List.range (i + 1)) = List.flatMap E (List.range i) ++ E i

Peel the last iteration off a flatMap over List.range: (range (i+1)).flatMap E = (range i).flatMap E ++ E i.

theorem Complexity.SAT.CNF.encode_flatMap {α : Type u_1} (l : List α) (F : α → CNF) : encode (List.flatMap F l) = List.flatMap (fun (a : α) => (F a).encode) l

CNF.encode distributes over flatMap.

theorem Complexity.SAT.flatCaps {A B C D M tag a b c d : ℕ} (htag : tag ≤ 3) (ha : a < A) (hb : b < B) (hc : c < C) (hd : d < D) (hM : 4 * A * B * C * D ≤ M) : tag ≤ M ∧ tag * A + a ≤ M ∧ (tag * A + a) * B + b ≤ M ∧ ((tag * A + a) * B + b) * C + c ≤ M ∧ (((tag * A + a) * B + b) * C + c) * D + d ≤ M

One cap rules them all: digits below their radices and 4·A·B·C·D ≤ M bound every intermediate mixed-radix value.

theorem Complexity.SAT.radix_caps {A B C D M : ℕ} (hA1 : 1 ≤ A) (hB1 : 1 ≤ B) (hC1 : 1 ≤ C) (hD1 : 1 ≤ D) (hM : 4 * A * B * C * D ≤ M) : A ≤ M ∧ B ≤ M ∧ C ≤ M ∧ D ≤ M

The radices themselves sit below the master cap.

def Complexity.SAT.emitLoopTM {n : ℕ} (body : TM n) (ctr fuel : Fin n) : TM n

The emitter loop: run body once per mark of fuel, incrementing ctr after each run.

Equations

• Complexity.SAT.emitLoopTM body ctr fuel = (body.seqTM (Complexity.TM.incRegTM ctr)).forRegTM fuel

def Complexity.SAT.loopBudget (M inner : ℕ) : ℕ

Uniform budget of an emitter loop with at most M iterations whose body runs within inner.

Equations

• Complexity.SAT.loopBudget M inner = M * (inner + 1 + Complexity.TM.opBudget M + 2) + (M + 2)

theorem Complexity.SAT.loopBudget_mono {M inner inner' : ℕ} (h : inner ≤ inner') : loopBudget M inner ≤ loopBudget M inner'

loopBudget M is monotone in the inner budget.

theorem Complexity.SAT.loop_le_loopBudget {v M inner : ℕ} (hv : v ≤ M) : v * (inner + 1 + TM.opBudget M + 2) + (v + 2) ≤ loopBudget M inner

The raw loop bound rounds up to loopBudget.

theorem Complexity.SAT.clauseBudget_mono {L L' M : ℕ} (h : L ≤ L') : clauseBudget L M ≤ clauseBudget L' M

clauseBudget · M is monotone in the literal count.

theorem Complexity.SAT.cnfBudget_mono {K K' L L' M : ℕ} (hK : K ≤ K') (hL : L ≤ L') : cnfBudget K L M ≤ cnfBudget K' L' M

cnfBudget · · M is monotone in both the clause count and the literal count.

theorem Complexity.SAT.emitLoop_hoareTime {n : ℕ} (body : TM n) (ctr fuel : Fin n) (hcf : ctr ≠ fuel) (v M b_body : ℕ) (hv : v ≤ M) (E : ℕ → List Bool) (inp₀ : Tape) (W : Fin n → Tape) (ys₀ : List Bool) (hinp₀ : TM.Parked inp₀) (hW : ∀ (i : Fin n), TM.Parked (W i)) (hfuel : W fuel = TM.regTape v) (hctr : W ctr = TM.regTape 0) (hbody : ∀ i < v, body.HoareTime (TM.EmitPred inp₀ (Function.update (Function.update W ctr (TM.regTape i)) fuel { head := i + 2, cells := TM.regCells v }) (ys₀ ++ List.flatMap E (List.range i))) (TM.EmitPred inp₀ (Function.update (Function.update W ctr (TM.regTape i)) fuel { head := i + 2, cells := TM.regCells v }) (ys₀ ++ List.flatMap E (List.range (i + 1)))) b_body) : (emitLoopTM body ctr fuel).HoareTime (TM.EmitPred inp₀ W ys₀) (TM.EmitPred inp₀ (Function.update W ctr (TM.regTape v)) (ys₀ ++ List.flatMap E (List.range v))) (v * (b_body + 1 + TM.opBudget M + 2) + (v + 2))

emitLoopTM Hoare rule. From fuel = v and ctr = 0, run the body at every i < v; the body sees ctr = i (fuel tape parked mid-loop), emits E i, and restores the work tapes. Afterwards ctr = v and the output extends by (range v).flatMap E.

theorem Complexity.SAT.emitLoopFrom_hoareTime {n : ℕ} (body : TM n) (ctr fuel : Fin n) (hcf : ctr ≠ fuel) (s v M b_body : ℕ) (hsv : s + v ≤ M) (E : ℕ → List Bool) (inp₀ : Tape) (W : Fin n → Tape) (ys₀ : List Bool) (hinp₀ : TM.Parked inp₀) (hW : ∀ (i : Fin n), TM.Parked (W i)) (hfuel : W fuel = TM.regTape v) (hctr : W ctr = TM.regTape s) (hbody : ∀ i < v, body.HoareTime (TM.EmitPred inp₀ (Function.update (Function.update W ctr (TM.regTape (s + i))) fuel { head := i + 2, cells := TM.regCells v }) (ys₀ ++ List.flatMap E (List.range i))) (TM.EmitPred inp₀ (Function.update (Function.update W ctr (TM.regTape (s + i))) fuel { head := i + 2, cells := TM.regCells v }) (ys₀ ++ List.flatMap E (List.range (i + 1)))) b_body) : (emitLoopTM body ctr fuel).HoareTime (TM.EmitPred inp₀ W ys₀) (TM.EmitPred inp₀ (Function.update W ctr (TM.regTape (s + v))) (ys₀ ++ List.flatMap E (List.range v))) (v * (b_body + 1 + TM.opBudget M + 2) + (v + 2))

emitLoopTM Hoare rule, offset form: the counter starts at s and ends at s + v; the body at iteration i < v sees ctr = s + i. Used by the pairwise at-most-one families, whose inner position loops start just past the outer position.

theorem Complexity.SAT.emitLoopGen_hoareTime {n : ℕ} (body : TM n) (ctr fuel : Fin n) (hcf : ctr ≠ fuel) (v M b_body : ℕ) (ctrVal : ℕ → ℕ) (hctrM : ∀ i < v, ctrVal i ≤ M) (E : ℕ → List Bool) (inp₀ : Tape) (u : ℕ → Fin n → Tape) (ys₀ : List Bool) (hinp₀ : TM.Parked inp₀) (hu : ∀ (i : ℕ) (j : Fin n), TM.Parked (u i j)) (hufuel : ∀ (i : ℕ), u i fuel = TM.regTape v) (huctr : ∀ (i : ℕ), u (i + 1) ctr = TM.regTape (ctrVal i + 1)) (hbody : ∀ i < v, body.HoareTime (TM.EmitPred inp₀ (Function.update (u i) fuel { head := i + 2, cells := TM.regCells v }) (ys₀ ++ List.flatMap E (List.range i))) (TM.EmitPred inp₀ (Function.update (Function.update (u (i + 1)) ctr (TM.regTape (ctrVal i))) fuel { head := i + 2, cells := TM.regCells v }) (ys₀ ++ List.flatMap E (List.range (i + 1)))) b_body) : (emitLoopTM body ctr fuel).HoareTime (TM.EmitPred inp₀ (u 0) ys₀) (TM.EmitPred inp₀ (u v) (ys₀ ++ List.flatMap E (List.range v))) (v * (b_body + 1 + TM.opBudget M + 2) + (v + 2))

emitLoopTM Hoare rule, general form: the per-iteration work states are an arbitrary ghost family u (so bodies may drift registers across iterations — shrinking inner fuels, mirrored counters), and the counter value is an arbitrary ghost ctrVal. The body at iteration i carries u i to u (i + 1)-with-the-counter-still-old; the loop's own increment finishes the move.