One variable's verdict is one step of the iteration

The capstone DescriptiveComplexity.Draw.Data.accVerdict_varFM_qfValue reads the machinery's exit bit as the alternating prefix over an abstract leaf Ps; DescriptiveComplexity.Draw.Data.altQuantFrom_leafP reads that prefix, at the concrete leaf, as DescriptiveComplexity.StepDef.next. This file joins them, discharging every abstract input of the capstone from the two facts a reduction's tape maintains:

• the working address's outer blocks encode the argument tuple (hmb);
• each stage track holds the stage dictionary (hdict).

Two statements: accVerdict_leafP, at any variable, whose right-hand side is the prefix over DescriptiveComplexity.Draw.Data.leafP at the address's blocks – the form the output sentence's leg also needs – and accVerdict_next, its specialization at a fixed-point variable, whose right-hand side is d.next itself.

The semantic pack is a hypothesis in the form the capstone consumes (hsem, pinning it to DescriptiveComplexity.Draw.Data.passSem) rather than a fixed choice, because the spine's per-position family (DescriptiveComplexity.Draw.Data.evalSpine_run's semOfJ) is chosen by the caller and only has to agree with the pass's pack.

noncomputable def DescriptiveComplexity.Draw.Data.mirBlk {L : FirstOrder.Language} (dt : Data L) {A R P : Type} (st : TapeStD dt A R P) : Fin dt.ko → (Fin dt.dd → A) → Prop

The working address's outer blocks, as the valuation the free levels of a pack read: the mirror's block at each outer index.

Equations

• dt.mirBlk st k = DescriptiveComplexity.wmBlk st.mir (DescriptiveComplexity.Draw.Tag.arg (toLex (Sum.inl k)))

theorem DescriptiveComplexity.Draw.Data.mirBlk_of_mir {L : FirstOrder.Language} {dt : Data L} {A R P : Type} {st st' : TapeStD dt A R P} (h : st.mir = st'.mir) : dt.mirBlk st = dt.mirBlk st'

The address's blocks depend on the mirror alone.

theorem DescriptiveComplexity.Draw.Data.accVerdict_leafP {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] [L.IsRelational] [L.Structure A] [LinearOrder (dt.X.Map A)] (vi : dt.VarIx) (st : TapeStD dt A R P) {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] [Finite ιV] (mV : ιV → Univ A R P dt.KIx dt.dd → Prop) (semOf : (a : ιV) → (∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF PR.zero PR.one vi (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf vi)) → dt.KindSem PR.zero PR.one vi (dt.roundSt st (mV a)) (dt.kindOf vi b)) (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {a₀ aT : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (hmV0 : mV a₀ = fun (x : Univ A R P dt.KIx dt.dd) => False) (hIncr : ∀ (a a' : ιV), a < a' → (∀ (b : ιV), ¬(a < b ∧ b < a')) → WMIncr WMLe (mV a) (mV a')) (hKin : ∀ (a : ιV) (t : Tag R P dt.KIx) (w : Fin dt.dd → A), mV a (t, w) → ∃ (j : Fin dt.ki), t = argIn dt.ko j) (hTop : ∀ (u : Univ A R P dt.KIx dt.dd), dt.InnerFull (fun (u : Univ A R P dt.KIx dt.dd) => tagBlk u.1) (mV aT) u) (σ : dt.d.B.Assignment (dt.X.Map A)) (mbW : Fin (dt.arOf vi) → dt.X.Map A) (hmb : ∀ (ℓ : Fin (dt.arOf vi)), dt.mirBlk st (Fin.castLE ⋯ ℓ) = encMap dt.ly PR.zero PR.one (mbW ℓ)) {Below : (Univ A R P dt.KIx dt.dd → Prop) → Prop} (hdict : ∀ (iv : dt.d.B.ι) (s : Univ A R P dt.KIx dt.dd → Prop), Below s → (st.old iv s ↔ trackOf dt.ly PR.zero PR.one ⋯ σ s)) (hbelow : ∀ (a : ιV) (iv : dt.d.B.ι) (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf vi)), Below (dt.stageTgtD PR.zero vi iv ts (dt.roundSt st (mV a)) v (dt.d.B.arity iv))) (hordP : ∀ (p q : dt.X.Map A), p ≤ q ↔ p ≤ q) (hsem : ∀ (a : ιV) (hp : ∀ (ℓ : Fin (dt.nIn vi)), dt.igPassP RF PR.zero PR.one vi (dt.roundSt st (mV a)) ℓ) (b : Fin (dt.natOf vi)), semOf a hp b = dt.passSem RF ⋯ hlin vi (dt.roundSt st (mV a)) hp mbW ⋯ b) (fG : dt.CtlIx → A) : dt.accVerdict PR.one (dt.polOf vi) ((dt.varArgsOf PR.zero PR.one vi).postFold (roundFX RF hord vi st v mV semOf (varFM RF hord vi st v mV semOf fG aT) aT) (dt.back RF.cell PR.zero PR.one ⋯ (dt.roundSt st (mV aT)) v)) ↔ altQuantFrom (dt.polOf vi) (dt.leafP PR.zero PR.one vi σ (dt.mirBlk st)) 0 (ixBlk (argIn dt.ko) (mV aT))

The machinery's verdict is the prefix over the leaf: every abstract input of DescriptiveComplexity.Draw.Data.accVerdict_varFM_qfValue discharged – the flags by DescriptiveComplexity.Draw.Data.ctlBit_roundFX_pass_iff, the pass by DescriptiveComplexity.Draw.Data.roundPass_of_polarities, the valuation and its pack by DescriptiveComplexity.Draw.Data.passW, the stage reads by DescriptiveComplexity.Draw.Data.old_trackOf_stageTgtD, and the two leaf readings by DescriptiveComplexity.Draw.Data.leafP_pass_iff / DescriptiveComplexity.Draw.Data.leafP_fail_iff.

theorem DescriptiveComplexity.Draw.Data.accVerdict_next {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] [L.IsRelational] [L.Structure A] [LinearOrder (dt.X.Map A)] (st : TapeStD dt A R P) {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] [Finite ιV] (mV : ιV → Univ A R P dt.KIx dt.dd → Prop) (i : dt.d.B.ι) (semOf : (a : ιV) → (∀ (ℓ : Fin (dt.nIn (some i))), dt.igPassP RF PR.zero PR.one (some i) (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf (some i))) → dt.KindSem PR.zero PR.one (some i) (dt.roundSt st (mV a)) (dt.kindOf (some i) b)) (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {a₀ aT : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (hmV0 : mV a₀ = fun (x : Univ A R P dt.KIx dt.dd) => False) (hIncr : ∀ (a a' : ιV), a < a' → (∀ (b : ιV), ¬(a < b ∧ b < a')) → WMIncr WMLe (mV a) (mV a')) (hKin : ∀ (a : ιV) (t : Tag R P dt.KIx) (w : Fin dt.dd → A), mV a (t, w) → ∃ (j : Fin dt.ki), t = argIn dt.ko j) (hTop : ∀ (u : Univ A R P dt.KIx dt.dd), dt.InnerFull (fun (u : Univ A R P dt.KIx dt.dd) => tagBlk u.1) (mV aT) u) (σ : dt.d.B.Assignment (dt.X.Map A)) (mbW : Fin (dt.arOf (some i)) → dt.X.Map A) (hmb : ∀ (ℓ : Fin (dt.arOf (some i))), dt.mirBlk st (Fin.castLE ⋯ ℓ) = encMap dt.ly PR.zero PR.one (mbW ℓ)) {Below : (Univ A R P dt.KIx dt.dd → Prop) → Prop} (hdict : ∀ (iv : dt.d.B.ι) (s : Univ A R P dt.KIx dt.dd → Prop), Below s → (st.old iv s ↔ trackOf dt.ly PR.zero PR.one ⋯ σ s)) (hbelow : ∀ (a : ιV) (iv : dt.d.B.ι) (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf (some i))), Below (dt.stageTgtD PR.zero (some i) iv ts (dt.roundSt st (mV a)) v (dt.d.B.arity iv))) (hordP : ∀ (p q : dt.X.Map A), p ≤ q ↔ p ≤ q) (hsem : ∀ (a : ιV) (hp : ∀ (ℓ : Fin (dt.nIn (some i))), dt.igPassP RF PR.zero PR.one (some i) (dt.roundSt st (mV a)) ℓ) (b : Fin (dt.natOf (some i))), semOf a hp b = dt.passSem RF ⋯ hlin (some i) (dt.roundSt st (mV a)) hp mbW ⋯ b) (fG : dt.CtlIx → A) : dt.accVerdict PR.one (dt.polOf (some i)) ((dt.varArgsOf PR.zero PR.one (some i)).postFold (roundFX RF hord (some i) st v mV semOf (varFM RF hord (some i) st v mV semOf fG aT) aT) (dt.back RF.cell PR.zero PR.one ⋯ (dt.roundSt st (mV aT)) v)) ↔ dt.d.next σ i mbW

The machinery's verdict at a fixed-point variable is one step of the iteration at the points the working address's outer blocks encode: the prefix of DescriptiveComplexity.Draw.Data.accVerdict_leafP read through DescriptiveComplexity.Draw.Data.altQuantFrom_leafP.

theorem DescriptiveComplexity.Draw.Data.accVerdict_out {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] [L.IsRelational] [L.Structure A] [LinearOrder (dt.X.Map A)] (st : TapeStD dt A R P) {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} [LinearOrder ιV] [Finite ιV] (mV : ιV → Univ A R P dt.KIx dt.dd → Prop) (semOf : (a : ιV) → (∀ (ℓ : Fin (dt.nIn none)), dt.igPassP RF PR.zero PR.one none (dt.roundSt st (mV a)) ℓ) → (b : Fin (dt.natOf none)) → dt.KindSem PR.zero PR.one none (dt.roundSt st (mV a)) (dt.kindOf none b)) (hlin : IsLinOrd WMLe) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) {a₀ aT : ιV} (hbotV : ∀ (a : ιV), a₀ ≤ a) (hmV0 : mV a₀ = fun (x : Univ A R P dt.KIx dt.dd) => False) (hIncr : ∀ (a a' : ιV), a < a' → (∀ (b : ιV), ¬(a < b ∧ b < a')) → WMIncr WMLe (mV a) (mV a')) (hKin : ∀ (a : ιV) (t : Tag R P dt.KIx) (w : Fin dt.dd → A), mV a (t, w) → ∃ (j : Fin dt.ki), t = argIn dt.ko j) (hTop : ∀ (u : Univ A R P dt.KIx dt.dd), dt.InnerFull (fun (u : Univ A R P dt.KIx dt.dd) => tagBlk u.1) (mV aT) u) (σ : dt.d.B.Assignment (dt.X.Map A)) {Below : (Univ A R P dt.KIx dt.dd → Prop) → Prop} (hdict : ∀ (iv : dt.d.B.ι) (s : Univ A R P dt.KIx dt.dd → Prop), Below s → (st.old iv s ↔ trackOf dt.ly PR.zero PR.one ⋯ σ s)) (hbelow : ∀ (a : ιV) (iv : dt.d.B.ι) (ts : Fin (dt.d.B.arity iv) → Fin (dt.nOf none)), Below (dt.stageTgtD PR.zero none iv ts (dt.roundSt st (mV a)) v (dt.d.B.arity iv))) (hordP : ∀ (p q : dt.X.Map A), p ≤ q ↔ p ≤ q) (hsem : ∀ (a : ιV) (hp : ∀ (ℓ : Fin (dt.nIn none)), dt.igPassP RF PR.zero PR.one none (dt.roundSt st (mV a)) ℓ) (b : Fin (dt.natOf none)), semOf a hp b = dt.passSem RF ⋯ hlin none (dt.roundSt st (mV a)) hp (fun (ℓ : Fin (dt.arOf none)) => ℓ.elim0) ⋯ b) (fG : dt.CtlIx → A) : dt.accVerdict PR.one (dt.polOf none) ((dt.varArgsOf PR.zero PR.one none).postFold (roundFX RF hord none st v mV semOf (varFM RF hord none st v mV semOf fG aT) aT) (dt.back RF.cell PR.zero PR.one ⋯ (dt.roundSt st (mV aT)) v)) ↔ dt.X.Map A ⊨ dt.d.out

The machinery's verdict at the output variable is the output sentence at the stage the tracks hold: the prefix of DescriptiveComplexity.Draw.Data.accVerdict_leafP read through DescriptiveComplexity.Draw.Data.altQuantFrom_leafP_out. The output variable is nullary, so the working address's outer blocks encode the empty tuple and there is nothing to ask of them – which is why this is the one verdict a reduction can take at the empty address.