What a parameter pack owes, and one atom kind's machinery

The machineries above the combinators take their parameters in a pack (DescriptiveComplexity.Draw.StageArgs, TagArgs, ElemArgs), so what they owe the interpretation is stated pack by pack. A pack's fields split in two: the static ones – which slot a trip walks, which block it names, where the coordinate loop lives – must not depend on the instance at all (DescriptiveComplexity.Draw.UConst), since they are what the emitted formula is built from; the dynamic ones are guards and control updates, and owe the usual three obligations.

With the three pack statements, an atom kind's machinery (DescriptiveComplexity.Draw.Data.kindRule) is definable one constructor at a time: the stage atom's by DescriptiveComplexity.Draw.Data.uRulesDefinable_stageRule, an expansion atom's by the tag-branched statement, an equality's and an order atom's by the element loop's.

def DescriptiveComplexity.Draw.UConst {L : FirstOrder.Language} {α : Type} (F : Env L → α) : Prop

A field that does not depend on the instance: what a static parameter of a pack owes, the emitted formula being built from it.

Equations

• DescriptiveComplexity.Draw.UConst F = ∃ (a : α), ∀ (e : DescriptiveComplexity.Draw.Env L), F e = a

An element loop's pack

structure DescriptiveComplexity.Draw.UElemArgsDef {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] {nr : ℕ} (args : (e : Env L) → ElemArgs e.α Q W nr) : Prop

What an element loop's pack owes.

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

  The tracks it walks are the same at every instance.

• MatchOf (j : Fin nr) : UGDefinable fun (e : Env L) => (args e).MatchOf j

  Each leaf's name guard is definable.

• setFlag (j : Fin nr) (b : Bool) : UStDefinable fun (e : Env L) => (args e).setFlag j b

  And so is each leaf's filing.

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

  The three folds are definable.

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

  Advancing and folding.

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

  The final fold.

• IsMaxEl : UGDefinable fun (e : Env L) (f : Q → e.α) (x : W → e.α) => (args e).IsMaxEl f

  And the exhaustion test.

theorem DescriptiveComplexity.Draw.uRulesDefinable_elemArgs {L : FirstOrder.Language} {Q W P : Type} [Fintype Q] [Fintype W] {nr : ℕ} {wk rg : W} {emb : ElemPh nr → P} {exitPh : P} {args : (e : Env L) → ElemArgs e.α Q W nr} (h : UElemArgsDef args) : URulesDefinable fun (e : Env L) => elemRule e.one wk rg emb (args e).rdTrack (args e).MatchOf (args e).setFlag (args e).initEl (args e).advEl (args e).exitSt (args e).IsMaxEl exitPh

A tag-branched machinery's pack

structure DescriptiveComplexity.Draw.UTagArgsDef {L : FirstOrder.Language} {Q W : Type} [Fintype Q] [Fintype W] {m : ℕ} {T : Type} {nrOf : T → ℕ} (args : (e : Env L) → TagArgs e.α Q W m T nrOf) : Prop

What a tag-branched machinery's pack owes.

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

  The witness tracks are the same at every instance.

• MatchT (i : Fin m) : UGDefinable fun (e : Env L) => (args e).MatchT i

  Each witness read's name guard is definable.

• setTagFlag (i : Fin m) (b : Bool) : UStDefinable fun (e : Env L) => (args e).setTagFlag i b

  And so is its filing.

• TagsAre (τ : T) : UGDefinable fun (e : Env L) (f : Q → e.α) (x : W → e.α) => (args e).TagsAre τ f

  The branch's decoding is definable.

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

  The leaf tracks are the same at every instance.

• MatchE (τ : T) (j : Fin (nrOf τ)) : UGDefinable fun (e : Env L) => (args e).MatchE τ j

  Each leaf's name guard is definable.

• setFlagE (τ : T) (j : Fin (nrOf τ)) (b : Bool) : UStDefinable fun (e : Env L) => (args e).setFlagE τ j b

  And so is its filing.

• initEl (τ : T) : UStDefinable fun (e : Env L) => (args e).initEl τ

  The three folds are definable, per branch.

• advEl (τ : T) : UStDefinable fun (e : Env L) => (args e).advEl τ

  Advancing and folding.

• exitSt (τ : T) : UStDefinable fun (e : Env L) => (args e).exitSt τ

  The final fold.

• IsMaxEl (τ : T) : UGDefinable fun (e : Env L) (f : Q → e.α) (x : W → e.α) => (args e).IsMaxEl τ f

  And the exhaustion test.

theorem DescriptiveComplexity.Draw.uRulesDefinable_tagArgs {L : FirstOrder.Language} {Q W P : Type} [Fintype Q] [Fintype W] {m : ℕ} {T : Type} {nrOf : T → ℕ} {wk rg : W} {emb : TagPh m T nrOf → P} {exitPh : P} {args : (e : Env L) → TagArgs e.α Q W m T nrOf} (h : UTagArgsDef args) : URulesDefinable fun (e : Env L) => tagRule e.one wk rg emb (args e).rdTrackT (args e).MatchT (args e).setTagFlag (args e).TagsAre (args e).rdTrackE (args e).MatchE (args e).setFlagE (args e).initEl (args e).advEl (args e).exitSt (args e).IsMaxEl exitPh

A stage atom's pack, and an atom kind's machinery

structure DescriptiveComplexity.Draw.Data.UStageArgsDef {L : FirstOrder.Language} {Q : Type} [Fintype Q] {dt : Data L} [Fintype dt.SlotIx] {k : ℕ} (args : (e : Env L) → StageArgs e.α Q dt.SlotIx (Fin dt.ko ⊕ Fin dt.ki) dt.dd0 k) : Prop

What a stage atom's pack owes.

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

  The source tracks are the same at every instance.

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

  And so are the two block families.

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

  The target's among them.

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

  And the coordinate loop's control location.

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

  and the stage track read under the head.

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

  The copied bit is definable.

• setBit (b : Bool) : UStDefinable fun (e : Env L) => (args e).setBit b

  And so is its filing.

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

  The coordinate loop's two updates are definable.

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

  The advance among them.

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

  With its exhaustion test.

• setAv (b : Bool) : UStDefinable fun (e : Env L) => (args e).setAv b

  and the verdict's filing.

theorem DescriptiveComplexity.Draw.Data.uRulesDefinable_stageArgs {L : FirstOrder.Language} {Q P : Type} [Fintype Q] {dt : Data L} [Fintype dt.SlotIx] {k : ℕ} {emb : StagePh k → P} {exitPh : P} {args : (e : Env L) → StageArgs e.α Q dt.SlotIx (Fin dt.ko ⊕ Fin dt.ki) dt.dd0 k} (h : UStageArgsDef args) : URulesDefinable fun (e : Env L) => dt.stageRule e.zero e.one emb (args e).srcTrack (args e).srcBlk (args e).dstBlk (args e).coord (args e).bitFlag (args e).setBit (args e).initLv (args e).advLv (args e).IsMaxLv (args e).oldSlot (args e).setAv exitPh

noncomputable def DescriptiveComplexity.Draw.Data.UKindArgsDef {L : FirstOrder.Language} {Q : Type} [Fintype Q] {dt : Data L} [Fintype dt.SlotIx] {n : ℕ} (κ : MatAtom dt.X dt.d.B n) : ((e : Env L) → dt.KindArgs κ) → Prop

What an atom kind's pack owes, one constructor at a time.

Equations

• DescriptiveComplexity.Draw.Data.UKindArgsDef (DescriptiveComplexity.Draw.MatAtom.stage i a) args = DescriptiveComplexity.Draw.Data.UStageArgsDef args
• DescriptiveComplexity.Draw.Data.UKindArgsDef (DescriptiveComplexity.Draw.MatAtom.exp a a_1) args = DescriptiveComplexity.Draw.UTagArgsDef args
• DescriptiveComplexity.Draw.Data.UKindArgsDef (DescriptiveComplexity.Draw.MatAtom.eq a a_1) args = DescriptiveComplexity.Draw.UElemArgsDef args
• DescriptiveComplexity.Draw.Data.UKindArgsDef (DescriptiveComplexity.Draw.MatAtom.ord a a_1) args = DescriptiveComplexity.Draw.UElemArgsDef args

theorem DescriptiveComplexity.Draw.Data.uRulesDefinable_kindRule {L : FirstOrder.Language} {Q P : Type} [Fintype Q] {dt : Data L} [Fintype dt.SlotIx] {n : ℕ} (κ : MatAtom dt.X dt.d.B n) {args : (e : Env L) → dt.KindArgs κ} {emb : dt.KindPh κ → P} {exitPh : P} (h : UKindArgsDef κ args) : URulesDefinable fun (e : Env L) => dt.kindRule e.zero e.one κ (args e) emb exitPh

An atom kind's machinery is definable, given its pack: the stage atom's by its own statement, an expansion atom's by the tag-branched one, an equality's and an order atom's by the element loop's.