The last four layers, and the program's own kits

One round, one variable's machinery, the evaluation's spine and the outer loop are the four remaining combinators, and each is checkpoints over machineries that are already discharged. What is new here is small and concrete: the program's own kits (DescriptiveComplexity.Draw.Data.compareKit, copyKit, seekKit, advKit, clearMirKit, tgtTopKit) and the two questions they are written from – every stage track agrees with its next (DescriptiveComplexity.Draw.Data.cmpG), and the working cell is at an argument-tagged block. Each is a conjunction, a disjunction or an equivalence of the three atoms, indexed by a finite type.

One round

theorem DescriptiveComplexity.Draw.Data.uRulesDefinable_roundRule {L : FirstOrder.Language} {dt : Data L} {Q P : Type} [Fintype Q] [Fintype dt.SlotIx] {PG PX SG SX : Type} {ShG : SG → Type} {ShX : SX → Type} {emb : RoundPh PG PX → P} {ruleG : (e : Env L) → (s : SG) → ShG s → Rule e.α Q dt.SlotIx P} {ruleX : (e : Env L) → (s : SX) → ShX s → Rule e.α Q dt.SlotIx P} {pxEntry exitPh : P} {existFlag allFlag : Q} (hG : URulesDefinable ruleG) (hX : URulesDefinable ruleX) : URulesDefinable fun (e : Env L) => dt.roundRule e.one emb (ruleG e) (ruleX e) pxEntry exitPh existFlag allFlag

One round's rules are definable: the branch checkpoint's dispatches read the two gate flags, which are control slots.

One variable's machinery

theorem DescriptiveComplexity.Draw.Data.uRulesDefinable_varRule {L : FirstOrder.Language} {dt : Data L} {Q P : Type} [Fintype Q] [Fintype dt.SlotIx] {PG PX SG SX : Type} {ShG : SG → Type} {ShX : SX → Type} {emb : VarPh dt.CarryB PG PX → P} {ruleG : (e : Env L) → (s : SG) → ShG s → Rule e.α Q dt.SlotIx P} {ruleX : (e : Env L) → (s : SX) → ShX s → Rule e.α Q dt.SlotIx P} {pgEntry pxEntry exitPh : P} {newSlot : dt.SlotIx} {gateFlag : Q} {accBit : (e : Env L) → (Q → e.α) → Prop} {enterSt initSt postFold : (e : Env L) → (Q → e.α) → (dt.SlotIx → e.α) → Q → e.α} {storeCarry : (e : Env L) → dt.CarryB → (Q → e.α) → (dt.SlotIx → e.α) → Q → e.α} (hG : URulesDefinable ruleG) (hX : URulesDefinable ruleX) (hacc : UGDefinable fun (e : Env L) (f : Q → e.α) (x : dt.SlotIx → e.α) => accBit e f) (henter : UStDefinable enterSt) (hinit : UStDefinable initSt) (hpost : UStDefinable postFold) (hcarry : ∀ (b : dt.CarryB), UStDefinable fun (e : Env L) => storeCarry e b) : URulesDefinable fun (e : Env L) => dt.varRule e.zero e.one emb (ruleG e) (ruleX e) pgEntry pxEntry exitPh newSlot gateFlag (accBit e) (enterSt e) (initSt e) (postFold e) (storeCarry e)

One variable's machinery is definable: five checkpoints, the VAL clear, the exhaustion test and the block-indexed increment, with the folds as the caller's control updates and the two stage writes as single-slot updates.

The evaluation's spine

theorem DescriptiveComplexity.Draw.Data.uRulesDefinable_evalRule {L : FirstOrder.Language} {dt : Data L} {Q : Type} [Fintype Q] [Fintype dt.SlotIx] {PM SM : Type} {nv : ℕ} {ShM : SM → Type} {ruleM : (e : Env L) → (s : SM) → ShM s → Rule e.α Q dt.SlotIx (OuterPh (EvalPh nv PM))} {subEntry : Fin nv → PM} (hM : URulesDefinable ruleM) : URulesDefinable fun (e : Env L) => dt.evalRule e.zero e.one (ruleM e) subEntry

The evaluation's spine is definable: one checkpoint per variable position, the last one erasing the marker towards the sweep's advance or the post-sweep reset.

The program's own questions and rewrite

theorem DescriptiveComplexity.Draw.Data.uGDefinable_cmpG {L : FirstOrder.Language} {dt : Data L} {Q : Type} [Fintype Q] [Fintype dt.SlotIx] : UGDefinable fun (e : Env L) (x : Q → e.α) (g : dt.SlotIx → e.α) => dt.cmpG e.one g

The convergence test's question is definable: one equivalence per fixed-point variable.

theorem DescriptiveComplexity.Draw.Data.uTrDefinable_copyKit_wrG {L : FirstOrder.Language} {dt : Data L} {Q P : Type} [Fintype Q] [Fintype dt.SlotIx] {ph : P} : UTrDefinable fun (e : Env L) (x : Q → e.α) (g : dt.SlotIx → e.α) => (dt.copyKit ph).wrG g

The copy-back's rewrite is definable: every stage track takes its next's digit, and every other slot rides along – a decision made slot by slot.

The outer loop

theorem DescriptiveComplexity.Draw.Data.uRulesDefinable_outerRule {L : FirstOrder.Language} {dt : Data L} {Q : Type} [Fintype Q] [Fintype dt.SlotIx] {PE SE : Type} {ShE : SE → Type} {ruleE : (e : Env L) → (s : SE) → ShE s → Rule e.α Q dt.SlotIx (OuterPh PE)} {evalEntry evalEntryOut : PE} (hE : URulesDefinable ruleE) : URulesDefinable fun (e : Env L) => dt.outerRule e.zero e.one (ruleE e) evalEntry evalEntryOut

The outer program's rules are definable: thirteen kits with their exit rules, the initial step, and the evaluation's rules as the parameter.