The rules of an atom's machinery, dispatched by its kind

One atom of a step matrix gets the machinery its kind names: a stage atom the random access of DescriptiveComplexity.Problems.Wide.DrawStageAtom, an expansion atom the tag-branched loops of DescriptiveComplexity.Problems.Wide.DrawTagged, a comparison the coordinate loop of DescriptiveComplexity.Problems.Wide.DrawElem. This file is the dispatch: per kind a parameter pack (DescriptiveComplexity.Draw.StageArgs and friends) mirroring the machinery's semantic parameters – the matches, the control updates, the loop operations, and for the tag branch its exclusivity proof – then DescriptiveComplexity.Draw.Data.kindRule/kindSep/kindEntry: the rules, their separation, and the machinery's entry phase.

The packs keep the semantic content where it belongs – it is fixed with the runs – while the shapes and their separation are closed here: kindSep needs nothing beyond the packs and the embedding's injectivity.

The parameter packs

structure DescriptiveComplexity.Draw.StageArgs (A Q W KB : Type) (dd0 k : ℕ) : Type

The parameters of a stage atom's machinery (see DescriptiveComplexity.Draw.Data.stageRule).

• srcTrack : Fin k → W

  The source track of each argument position.

• srcBlk : Fin k → KB

  The source block of each argument position.

• dstBlk : Fin k → KB

  The target block of each argument position.

• coord : Fin dd0 → Q

  The control location of the coordinate loop.

• bitFlag : (Q → A) → Prop

  The copied bit, read back from the control.

• setBit : Bool → (Q → A) → (W → A) → Q → A

  Storing the read bit.

• initLv : (Q → A) → (W → A) → Q → A

  Initializing the coordinate loop.

• advLv : (Q → A) → (W → A) → Q → A

  Advancing the coordinate loop.

• IsMaxLv : (Q → A) → Prop

  The coordinate loop is exhausted.

• oldSlot : W

  The stage track read under the head.

• setAv : Bool → (Q → A) → (W → A) → Q → A

  Storing the atom's verdict.

structure DescriptiveComplexity.Draw.TagArgs (A Q W : Type) (m : ℕ) (T : Type) (nrOf : T → ℕ) : Type

The parameters of a tag-branched machinery (see DescriptiveComplexity.Draw.tagRule), with the branch's exclusivity proof.

• rdTrackT : Fin m → W

  The track of each witness read.

• MatchT : Fin m → (Q → A) → (W → A) → Prop

  The name guard of each witness read.

• setTagFlag : Fin m → Bool → (Q → A) → (W → A) → Q → A

  Storing a witness bit.

• TagsAre : T → (Q → A) → Prop

  The branch's decoding.

• hTags (τ τ' : T) (f : Q → A) : self.TagsAre τ f → self.TagsAre τ' f → τ = τ'

  The decoding is exclusive.

• rdTrackE (τ : T) : Fin (nrOf τ) → W

  The track of each leaf read, per branch.

• MatchE (τ : T) : Fin (nrOf τ) → (Q → A) → (W → A) → Prop

  The name guard of each leaf read, per branch.

• setFlagE (τ : T) : Fin (nrOf τ) → Bool → (Q → A) → (W → A) → Q → A

  Storing a leaf bit.

• initEl : T → (Q → A) → (W → A) → Q → A

  Initializing the loop and accumulators.

• advEl : T → (Q → A) → (W → A) → Q → A

  Advancing and folding.

• exitSt : T → (Q → A) → (W → A) → Q → A

  The final fold.

• IsMaxEl : T → (Q → A) → Prop

  The loop is exhausted.

structure DescriptiveComplexity.Draw.ElemArgs (A Q W : Type) (nr : ℕ) : Type

The parameters of a plain element loop (see DescriptiveComplexity.Draw.elemRule).

• rdTrack : Fin nr → W

  The track of each leaf read.

• MatchOf : Fin nr → (Q → A) → (W → A) → Prop

  The name guard of each leaf read.

• setFlag : Fin nr → Bool → (Q → A) → (W → A) → Q → A

  Storing a leaf bit.

• initEl : (Q → A) → (W → A) → Q → A

  Initializing the loop and accumulators.

• advEl : (Q → A) → (W → A) → Q → A

  Advancing and folding.

• exitSt : (Q → A) → (W → A) → Q → A

  The final fold.

• IsMaxEl : (Q → A) → Prop

  The loop is exhausted.

noncomputable def DescriptiveComplexity.Draw.Data.KindArgs {L : FirstOrder.Language} (dt : Data L) {A Q : Type} {n : ℕ} : MatAtom dt.X dt.d.B n → Type

The parameter pack of an atom kind's machinery.

Equations

• dt.KindArgs (DescriptiveComplexity.Draw.MatAtom.stage i a) = DescriptiveComplexity.Draw.StageArgs A Q dt.SlotIx (Fin dt.ko ⊕ Fin dt.ki) dt.dd0 (dt.d.B.arity i)
• dt.KindArgs (DescriptiveComplexity.Draw.MatAtom.exp e a) = DescriptiveComplexity.Draw.TagArgs A Q dt.SlotIx (k * Fintype.card dt.X.Tag) (Fin k → dt.X.Tag) (dt.relNr e)
• dt.KindArgs (DescriptiveComplexity.Draw.MatAtom.eq a a_1) = DescriptiveComplexity.Draw.ElemArgs A Q dt.SlotIx 2
• dt.KindArgs (DescriptiveComplexity.Draw.MatAtom.ord a a_1) = DescriptiveComplexity.Draw.ElemArgs A Q dt.SlotIx 2

noncomputable def DescriptiveComplexity.Draw.Data.kindEntry {L : FirstOrder.Language} (dt : Data L) {n : ℕ} (κ : MatAtom dt.X dt.d.B n) : dt.KindPh κ

The entry phase of an atom kind's machinery: the machinery's own first phase – for an expansion atom the first witness read, so the tag chain is entered, not skipped (the branch checkpoint only when there is no read at all).

Equations

• One or more equations did not get rendered due to their size.
• dt.kindEntry (DescriptiveComplexity.Draw.MatAtom.stage i a) = DescriptiveComplexity.Draw.StagePh.savP DescriptiveComplexity.Draw.TrackPh.up
• dt.kindEntry (DescriptiveComplexity.Draw.MatAtom.eq a a_1) = DescriptiveComplexity.Draw.ElemPh.e0
• dt.kindEntry (DescriptiveComplexity.Draw.MatAtom.ord a a_1) = DescriptiveComplexity.Draw.ElemPh.e0

noncomputable def DescriptiveComplexity.Draw.Data.kindRule {L : FirstOrder.Language} (dt : Data L) {A Q P : Type} (zero one : A) {n : ℕ} (κ : MatAtom dt.X dt.d.B n) (_args : dt.KindArgs κ) (_emb : dt.KindPh κ → P) (_exitPh : P) (s : dt.KindSite κ) : dt.KindSh κ s → Rule A Q dt.SlotIx P

The rules of an atom kind's machinery, at its parameter pack.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.Draw.Data.kindDstIn {L : FirstOrder.Language} {dt : Data L} {A Q P : Type} (zero one : A) {S : P → Prop} {n : ℕ} (κ : MatAtom dt.X dt.d.B n) (args : dt.KindArgs κ) {emb : dt.KindPh κ → P} (exitPh : P) (hemb : ∀ (p : dt.KindPh κ), S (emb p)) (hexit : S exitPh) (s : dt.KindSite κ) (ρ : dt.KindSh κ s) : S (dt.kindRule zero one κ args emb exitPh s ρ).dstPh

A property of an atom kind's phases and its exit holds of every phase it can move to: whichever kind it is, its machinery stays inside its own phases and only its verdict leaves. This is what a determinism-after-the-guess argument asks of an atom (DescriptiveComplexity.Draw.Data.nexProg_uniqueFrom).

theorem DescriptiveComplexity.Draw.Data.kindHosrc {L : FirstOrder.Language} {dt : Data L} {A Q P : Type} (zero one : A) {n : ℕ} (κ : MatAtom dt.X dt.d.B n) (args : dt.KindArgs κ) {emb : dt.KindPh κ → P} (exitPh : P) (s : dt.KindSite κ) (ρ : dt.KindSh κ s) : ∃ (p : dt.KindPh κ), (dt.kindRule zero one κ args emb exitPh s ρ).srcPh = emb p ∧ dt.kindOwn κ p = s

Every rule of an atom kind's machinery fires from a phase its site owns.

theorem DescriptiveComplexity.Draw.Data.kindSep {L : FirstOrder.Language} {dt : Data L} {A Q P : Type} (zero one : A) (hzo : zero ≠ one) {n : ℕ} (κ : MatAtom dt.X dt.d.B n) (args : dt.KindArgs κ) {emb : dt.KindPh κ → P} (hemb : Function.Injective emb) (exitPh : P) (s : dt.KindSite κ) (ρ ρ' : dt.KindSh κ s) (f : Q → A) (g : dt.SlotIx → A) : (dt.kindRule zero one κ args emb exitPh s ρ).guard f g → (dt.kindRule zero one κ args emb exitPh s ρ').guard f g → (dt.kindRule zero one κ args emb exitPh s ρ).srcPh = (dt.kindRule zero one κ args emb exitPh s ρ').srcPh → ρ = ρ'

An atom kind's machinery separates in-shape.