Tag-branched element loops: the expansion atoms and the domain gates

An expansion atom's defining sentence – and a block's domain sentence – depends on the tags of its argument points. The machine reads them first: one named-bit read per argument position and candidate tag, at the canonical tag-witness cell, the verdicts stored one-hot in the control. A branch checkpoint then dispatches on the decoded tag tuple – one dispatch rule per tuple, their guards made exclusive by the decoding – into that tuple's own element loop (DescriptiveComplexity.Problems.Wide.DrawElem), which evaluates the sentence's prefix with one leaf read per block atom of its matrix.

The expansion atoms instantiate this at their arity, the domain gates at one argument. As everywhere, the shapes and separation are fixed here; the decodings and folds are parameters.

The shapes

inductive DescriptiveComplexity.Draw.BrRule (T : Type) : Type

The rules of a branch checkpoint: the walk back, and one dispatch per tag tuple.

• stay {T : Type} : BrRule T

  Walk left back to the marker.

• dsp {T : Type} : T → BrRule T

  Dispatch into the tuple's loop.

inductive DescriptiveComplexity.Draw.TagPh (m : ℕ) (T : Type) (nrOf : T → ℕ) : Type

The phases of a tag-branched machinery: the witness reads, the branch checkpoint, and one element loop per tag tuple.

• tagRdP {m : ℕ} {T : Type} {nrOf : T → ℕ} : Fin m → ReadPh → TagPh m T nrOf

  The i-th witness read.

• brP {m : ℕ} {T : Type} {nrOf : T → ℕ} : TagPh m T nrOf

  The branch checkpoint.

• loopP {m : ℕ} {T : Type} {nrOf : T → ℕ} (τ : T) : ElemPh (nrOf τ) → TagPh m T nrOf

  A phase of the tuple's element loop.

inductive DescriptiveComplexity.Draw.TagSite (m : ℕ) (T : Type) (nrOf : T → ℕ) : Type

The sites of a tag-branched machinery.

• tagRd {m : ℕ} {T : Type} {nrOf : T → ℕ} : Fin m → TagSite m T nrOf

  A witness read.

• br {m : ℕ} {T : Type} {nrOf : T → ℕ} : TagSite m T nrOf

  The branch checkpoint.

• loop {m : ℕ} {T : Type} {nrOf : T → ℕ} (τ : T) : ElemSite (nrOf τ) → TagSite m T nrOf

  A site of the tuple's element loop.

def DescriptiveComplexity.Draw.TagSh (m : ℕ) (T : Type) (nrOf : T → ℕ) : TagSite m T nrOf → Type

The rule shape of each site.

Equations

• DescriptiveComplexity.Draw.TagSh m T nrOf (DescriptiveComplexity.Draw.TagSite.tagRd a) = (DescriptiveComplexity.Draw.ReadRule ⊕ Bool)
• DescriptiveComplexity.Draw.TagSh m T nrOf DescriptiveComplexity.Draw.TagSite.br = DescriptiveComplexity.Draw.BrRule T
• DescriptiveComplexity.Draw.TagSh m T nrOf (DescriptiveComplexity.Draw.TagSite.loop τ s) = DescriptiveComplexity.Draw.ElemSh (nrOf τ) s

def DescriptiveComplexity.Draw.tagOwn {m : ℕ} {T : Type} {nrOf : T → ℕ} : TagPh m T nrOf → TagSite m T nrOf

The owner of each phase of a tag-branched machinery.

Equations

• DescriptiveComplexity.Draw.tagOwn (DescriptiveComplexity.Draw.TagPh.tagRdP i a) = DescriptiveComplexity.Draw.TagSite.tagRd i
• DescriptiveComplexity.Draw.tagOwn DescriptiveComplexity.Draw.TagPh.brP = DescriptiveComplexity.Draw.TagSite.br
• DescriptiveComplexity.Draw.tagOwn (DescriptiveComplexity.Draw.TagPh.loopP τ p) = DescriptiveComplexity.Draw.TagSite.loop τ (DescriptiveComplexity.Draw.elemOwn p)

def DescriptiveComplexity.Draw.tagFirstRd {P T : Type} {m : ℕ} {nrOf : T → ℕ} (emb : TagPh m T nrOf → P) : P

The first witness read's entry, or the branch checkpoint when there is none.

Equations

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

def DescriptiveComplexity.Draw.tagNextRd {P T : Type} {m : ℕ} {nrOf : T → ℕ} (emb : TagPh m T nrOf → P) (i : Fin m) : P

The phase after the i-th witness read.

Equations

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

def DescriptiveComplexity.Draw.tagRule {A Q W P T : Type} {m : ℕ} {nrOf : T → ℕ} (one : A) (wk rg : W) (emb : TagPh m T nrOf → P) (rdTrackT : Fin m → W) (MatchT : Fin m → (Q → A) → (W → A) → Prop) (setTagFlag : Fin m → Bool → (Q → A) → (W → A) → Q → A) (TagsAre : T → (Q → A) → Prop) (rdTrackE : (τ : T) → Fin (nrOf τ) → W) (MatchE : (τ : T) → Fin (nrOf τ) → (Q → A) → (W → A) → Prop) (setFlagE : (τ : T) → Fin (nrOf τ) → Bool → (Q → A) → (W → A) → Q → A) (initEl advEl exitSt : T → (Q → A) → (W → A) → Q → A) (IsMaxEl : T → (Q → A) → Prop) (exitPh : P) (i : TagSite m T nrOf) : TagSh m T nrOf i → Rule A Q W P

The rules of a tag-branched machinery.

Equations

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

theorem DescriptiveComplexity.Draw.tagRule_dstPh {A Q W P T : Type} {m : ℕ} {nrOf : T → ℕ} (one : A) (wk rg : W) {emb : TagPh m T nrOf → P} (rdTrackT : Fin m → W) (MatchT : Fin m → (Q → A) → (W → A) → Prop) (setTagFlag : Fin m → Bool → (Q → A) → (W → A) → Q → A) (TagsAre : T → (Q → A) → Prop) (rdTrackE : (τ : T) → Fin (nrOf τ) → W) (MatchE : (τ : T) → Fin (nrOf τ) → (Q → A) → (W → A) → Prop) (setFlagE : (τ : T) → Fin (nrOf τ) → Bool → (Q → A) → (W → A) → Q → A) (initEl advEl exitSt : T → (Q → A) → (W → A) → Q → A) (IsMaxEl : T → (Q → A) → Prop) (exitPh : P) (i : TagSite m T nrOf) (ρ : TagSh m T nrOf i) : (∃ (p : TagPh m T nrOf), (tagRule one wk rg emb rdTrackT MatchT setTagFlag TagsAre rdTrackE MatchE setFlagE initEl advEl exitSt IsMaxEl exitPh i ρ).dstPh = emb p) ∨ (tagRule one wk rg emb rdTrackT MatchT setTagFlag TagsAre rdTrackE MatchE setFlagE initEl advEl exitSt IsMaxEl exitPh i ρ).dstPh = exitPh

A tag-branched machinery leaves only into its own phases or its exit: the witness reads' trips stay inside it, the branch lands in the decoded tag's loop, and only the loop's last dispatch leaves.

theorem DescriptiveComplexity.Draw.tagRule_dstIn {A Q W P T : Type} {m : ℕ} {nrOf : T → ℕ} (one : A) (wk rg : W) {emb : TagPh m T nrOf → P} (rdTrackT : Fin m → W) (MatchT : Fin m → (Q → A) → (W → A) → Prop) (setTagFlag : Fin m → Bool → (Q → A) → (W → A) → Q → A) (TagsAre : T → (Q → A) → Prop) (rdTrackE : (τ : T) → Fin (nrOf τ) → W) (MatchE : (τ : T) → Fin (nrOf τ) → (Q → A) → (W → A) → Prop) (setFlagE : (τ : T) → Fin (nrOf τ) → Bool → (Q → A) → (W → A) → Q → A) (initEl advEl exitSt : T → (Q → A) → (W → A) → Q → A) (IsMaxEl : T → (Q → A) → Prop) (exitPh : P) {S : P → Prop} (hemb : ∀ (p : TagPh m T nrOf), S (emb p)) (hexit : S exitPh) (i : TagSite m T nrOf) (ρ : TagSh m T nrOf i) : S (tagRule one wk rg emb rdTrackT MatchT setTagFlag TagsAre rdTrackE MatchE setFlagE initEl advEl exitSt IsMaxEl exitPh i ρ).dstPh

A property of the machinery's phases and its exit holds of every phase it can move to.

theorem DescriptiveComplexity.Draw.tagHosrc {A Q W P T : Type} {m : ℕ} {nrOf : T → ℕ} (one : A) (wk rg : W) {emb : TagPh m T nrOf → P} (rdTrackT : Fin m → W) (MatchT : Fin m → (Q → A) → (W → A) → Prop) (setTagFlag : Fin m → Bool → (Q → A) → (W → A) → Q → A) (TagsAre : T → (Q → A) → Prop) (rdTrackE : (τ : T) → Fin (nrOf τ) → W) (MatchE : (τ : T) → Fin (nrOf τ) → (Q → A) → (W → A) → Prop) (setFlagE : (τ : T) → Fin (nrOf τ) → Bool → (Q → A) → (W → A) → Q → A) (initEl advEl exitSt : T → (Q → A) → (W → A) → Q → A) (IsMaxEl : T → (Q → A) → Prop) (exitPh : P) (i : TagSite m T nrOf) (ρ : TagSh m T nrOf i) : ∃ (p : TagPh m T nrOf), (tagRule one wk rg emb rdTrackT MatchT setTagFlag TagsAre rdTrackE MatchE setFlagE initEl advEl exitSt IsMaxEl exitPh i ρ).srcPh = emb p ∧ tagOwn p = i

Every rule of a tag-branched machinery fires from a phase its site owns; the loops' obligation is the element loop's.

theorem DescriptiveComplexity.Draw.tagSep {A Q W P T : Type} {m : ℕ} {nrOf : T → ℕ} (one : A) (wk rg : W) {emb : TagPh m T nrOf → P} (rdTrackT : Fin m → W) (MatchT : Fin m → (Q → A) → (W → A) → Prop) (setTagFlag : Fin m → Bool → (Q → A) → (W → A) → Q → A) (TagsAre : T → (Q → A) → Prop) (rdTrackE : (τ : T) → Fin (nrOf τ) → W) (MatchE : (τ : T) → Fin (nrOf τ) → (Q → A) → (W → A) → Prop) (setFlagE : (τ : T) → Fin (nrOf τ) → Bool → (Q → A) → (W → A) → Q → A) (initEl advEl exitSt : T → (Q → A) → (W → A) → Q → A) (IsMaxEl : T → (Q → A) → Prop) (exitPh : P) (hemb : Function.Injective emb) (hTags : ∀ (τ τ' : T) (f : Q → A), TagsAre τ f → TagsAre τ' f → τ = τ') (i : TagSite m T nrOf) (ρ ρ' : TagSh m T nrOf i) (f : Q → A) (g : W → A) : (tagRule one wk rg emb rdTrackT MatchT setTagFlag TagsAre rdTrackE MatchE setFlagE initEl advEl exitSt IsMaxEl exitPh i ρ).guard f g → (tagRule one wk rg emb rdTrackT MatchT setTagFlag TagsAre rdTrackE MatchE setFlagE initEl advEl exitSt IsMaxEl exitPh i ρ').guard f g → (tagRule one wk rg emb rdTrackT MatchT setTagFlag TagsAre rdTrackE MatchE setFlagE initEl advEl exitSt IsMaxEl exitPh i ρ).srcPh = (tagRule one wk rg emb rdTrackT MatchT setTagFlag TagsAre rdTrackE MatchE setFlagE initEl advEl exitSt IsMaxEl exitPh i ρ').srcPh → ρ = ρ'

A tag-branched machinery separates in-shape: the reads by their kit, the branch's dispatches by the exclusive decoding, the loops by their own separation.