The whole assembly is definable, given its semantic packs

The last floor: one variable's machinery (DescriptiveComplexity.Draw.Data.varRuleF), the evaluation's machineries (smRule), its spine (evalRuleF) and the program's assembly (progAsm) are definable as soon as the semantic packs are – which is what DescriptiveComplexity.Draw.Data.UVarArgsDef says, field by field: the four control locations a variable's machinery names must be the same at every instance, and every guard and control update it carries must be definable.

Nothing above this file reads a rule any more: what is left of the discharge is DescriptiveComplexity.Draw.Data.varArgsOf meeting UVarArgsDef, which is a statement about DescriptiveComplexity.Problems.Wide.DrawArgs alone.

structure DescriptiveComplexity.Draw.Data.UVarArgsDef {L : FirstOrder.Language} {dt : Data L} {Q : Type} [Fintype Q] [Fintype dt.SlotIx] (v : dt.VarIx) (args : (e : Env L) → dt.VarArgs v) : Prop

What one variable's semantic pack owes.

• argsA (a : Fin (dt.natOf v)) : UKindArgsDef (dt.kindOf v a) fun (e : Env L) => (args e).argsA a

  Each classified atom's pack.

• enterAtomSt (a : Fin (dt.natOf v)) : UStDefinable fun (e : Env L) => (args e).enterAtomSt a

  The update entering each atom.

• argsG (b : Fin (dt.arOf v)) : UTagArgsDef fun (e : Env L) => (args e).argsG b

  Each argument block's pack.

• wellGOf (b : Fin (dt.arOf v)) : UGDefinable fun (e : Env L) (x : Q → e.α) (g : dt.SlotIx → e.α) => (args e).wellGOf b g

  Each argument block's well-shapedness question.

• setFail : UStDefinable fun (e : Env L) => (args e).setFail

  Clearing the gates' verdict flag.

• enterBlockSt (b : Fin (dt.arOf v)) : UStDefinable fun (e : Env L) => (args e).enterBlockSt b

  The update entering each argument block.

• argsIG (b : Fin (dt.nIn v)) : UTagArgsDef fun (e : Env L) => (args e).argsIG b

  Each quantified level's pack.

• wellIGOf (b : Fin (dt.nIn v)) : UGDefinable fun (e : Env L) (x : Q → e.α) (g : dt.SlotIx → e.α) => (args e).wellIGOf b g

  Each quantified level's well-shapedness question.

• setFailIGOf (b : Fin (dt.nIn v)) : UStDefinable fun (e : Env L) => (args e).setFailIGOf b

  Clearing each level's polarity flag.

• enterIGSt (b : Fin (dt.nIn v)) : UStDefinable fun (e : Env L) => (args e).enterIGSt b

  The update entering each level's block.

• existFlag : UConst fun (e : Env L) => (args e).existFlag

  The ∃-levels' flag is the same at every instance.

• allFlag : UConst fun (e : Env L) => (args e).allFlag

  And so is the ∀-levels'.

• newSlot : UConst fun (e : Env L) => (args e).newSlot

  And so is the stage slot the variable writes.

• gateFlag : UConst fun (e : Env L) => (args e).gateFlag

  And so is the gates' verdict flag.

• accBit : UGDefinable fun (e : Env L) (f : Q → e.α) (x : dt.SlotIx → e.α) => (args e).accBit f

  The verdict the exit checkpoint writes is definable.

• enterSt : UStDefinable fun (e : Env L) => (args e).enterSt

  And so are the four folds.

• initSt : UStDefinable fun (e : Env L) => (args e).initSt

  The folds at the empty valuation.

• postFold : UStDefinable fun (e : Env L) => (args e).postFold

  The folds after a matrix pass.

• storeCarry (b : dt.CarryB) : UStDefinable fun (e : Env L) => (args e).storeCarry b

  And the folds at an increment's carry block.

theorem DescriptiveComplexity.Draw.Data.uRulesDefinable_varRuleF {L : FirstOrder.Language} {dt : Data L} {Q P : Type} [Fintype Q] [Fintype dt.SlotIx] {v : dt.VarIx} {args : (e : Env L) → dt.VarArgs v} {emb : dt.VarPhF v → P} {exitPh : P} (h : UVarArgsDef v args) : URulesDefinable fun (e : Env L) => dt.varRuleF e.zero e.one v (args e) emb exitPh

One variable's machinery is definable: the gates, the round – inner gates and matrix behind the branch checkpoint – and the variable's own checkpoints.

theorem DescriptiveComplexity.Draw.Data.uRulesDefinable_smRule {L : FirstOrder.Language} {dt : Data L} {Q : Type} [Fintype Q] [Fintype dt.SlotIx] {args : (e : Env L) → (v : dt.VarIx) → dt.VarArgs v} (h : ∀ (v : dt.VarIx), UVarArgsDef v fun (e : Env L) => args e v) : URulesDefinable fun (e : Env L) => dt.smRule e.zero e.one (args e)

The evaluation's machineries are definable: one copy of the variable machinery per spine position, and the output's.

theorem DescriptiveComplexity.Draw.Data.uRulesDefinable_evalRuleF {L : FirstOrder.Language} {dt : Data L} {Q : Type} [Fintype Q] [Fintype dt.SlotIx] {args : (e : Env L) → (v : dt.VarIx) → dt.VarArgs v} (h : ∀ (v : dt.VarIx), UVarArgsDef v fun (e : Env L) => args e v) : URulesDefinable fun (e : Env L) => dt.evalRuleF e.zero e.one (args e)

The evaluation is definable: its spine over the machineries.

theorem DescriptiveComplexity.Draw.Data.uRulesDefinable_progAsm {L : FirstOrder.Language} {dt : Data L} {Q : Type} [Fintype Q] [Fintype dt.SlotIx] {args : (e : Env L) → (v : dt.VarIx) → dt.VarArgs v} (h : ∀ (v : dt.VarIx), UVarArgsDef v fun (e : Env L) => args e v) : URulesDefinable fun (e : Env L) => dt.outerRule e.zero e.one (dt.evalRuleF e.zero e.one (args e)) (EvalPh.chk 0) (EvalPh.sub dt.smEntryOut)

The whole program's rule set is definable: the outer loop around the evaluation. This is DescriptiveComplexity.Draw.Data.progAsm's rule field, so an interpretation may be written down from here.