The expansion atoms, instantiated: the tag-branched wide loop

The third semantic instantiation: an expansion atom's machinery at the pack DescriptiveComplexity.Draw.Data.expArgs. The witness chain reads each argument point's tag off its witness cell, the branch dispatches on the one-hot decoding, and the branch's element loop enumerates the wide tuples – the whole prefix of the defining sentence – one leaf-read trip per block atom, the sub-fold riding in the sac slots.

This file builds the generated families and their invariants:

• DescriptiveComplexity.Draw.Data.expTagCell/expECell – the cells the trips go to: the tag-witness tuples and the member tuples of the copies' points, at the payload the round's wide tuple spells;
• DescriptiveComplexity.Draw.Data.readLvE_expFam – the loop element is the round's wide tuple at every stage of the family;
• the chain read-backs: the witness flags decode the points' tags, the leaf-read flags hold the block atoms' bits.

The wide loop element through the machinery's operations

theorem DescriptiveComplexity.Draw.Data.readLvE_setCtl {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} {q : dt.CtlIx} (hq : ∀ (j : Fin dt.eDim), dt.lvE j ≠ q) (b : Prop) (f : dt.CtlIx → A) : dt.readLvE (dt.setCtl zero one q b f) = dt.readLvE f

The wide loop element rides along a control-bit store off it.

theorem DescriptiveComplexity.Draw.Data.readLvE_putSac {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} (f : dt.CtlIx → A) (b : Fin dt.eDim → Prop) : dt.readLvE (dt.putSac zero one f b) = dt.readLvE f

The wide loop element rides along a sub-fold accumulator write.

theorem DescriptiveComplexity.Draw.Data.readLvE_advLvE {L : FirstOrder.Language} {dt : Data L} {A : Type} [LinearOrder A] (f : dt.CtlIx → A) : dt.readLvE (dt.advLvE f) = tupNext (dt.readLvE f)

The wide loop element after an advance is the next tuple.

theorem DescriptiveComplexity.Draw.Data.readLvE_chainSt {L : FirstOrder.Language} {dt : Data L} {A : Type} {nr : ℕ} (bit : Fin nr → Prop) (upd : Fin nr → Bool → (dt.CtlIx → A) → dt.CtlIx → A) (hupd : ∀ (i : Fin nr) (b : Bool) (f : dt.CtlIx → A), dt.readLvE (upd i b f) = dt.readLvE f) (base : dt.CtlIx → A) (n : ℕ) : dt.readLvE (chainSt bit upd base n) = dt.readLvE base

A within-round chain preserving the loop element preserves it end to end – the generic riding lemma every stored-read chain uses.

The cells and registers of an expansion atom

noncomputable def DescriptiveComplexity.Draw.Data.expTagSet {L : FirstOrder.Language} (dt : Data L) {A R P : Type} (vi : dt.VarIx) {k : ℕ} (ts : Fin k → Fin (dt.nOf vi)) (st : TapeStD dt A R P) (i : Fin (k * Fintype.card dt.X.Tag)) : Univ A R P dt.KIx dt.dd → Prop

The register behind the i-th witness read: the copy's level's register.

Equations

• dt.expTagSet vi ts st i = dt.lvSet st vi (ts (dt.wIx i).1)

noncomputable def DescriptiveComplexity.Draw.Data.expTagCell {L : FirstOrder.Language} (dt : Data L) {A R P : Type} (zero one : A) (vi : dt.VarIx) {k : ℕ} (ts : Fin k → Fin (dt.nOf vi)) (i : Fin (k * Fintype.card dt.X.Tag)) : Univ A R P dt.KIx dt.dd

The cell of the i-th witness read: the tag's witness tuple in the copy's block.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.expESet {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [L.IsRelational] (vi : dt.VarIx) {k : ℕ} (ts : Fin k → Fin (dt.nOf vi)) (e : dt.X.E.Relations k) (st : TapeStD dt A R P) (τ : Fin k → dt.X.Tag) (r : Fin (dt.relNr e τ)) : Univ A R P dt.KIx dt.dd → Prop

The register behind the r-th leaf read of branch τ.

Equations

• dt.expESet vi ts e st τ r = dt.lvSet st vi (ts (DescriptiveComplexity.Draw.Data.relLeafData e τ r).fst.1)

noncomputable def DescriptiveComplexity.Draw.Data.expPayTup {L : FirstOrder.Language} (dt : Data L) {A : Type} [L.IsRelational] (zero : A) {k : ℕ} (e : dt.X.E.Relations k) (τ : Fin k → dt.X.Tag) (hnτ : (dt.relPk e τ).n ≤ dt.eDim) (a : Lex (Fin dt.eDim → A)) (r : Fin (dt.relNr e τ)) : Fin (blockArityBound dt.X.B) → A

The payload the r-th leaf spells at round a: the block atom's levels read out of the round's wide tuple.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.expECell {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [L.IsRelational] (zero one : A) (vi : dt.VarIx) {k : ℕ} (ts : Fin k → Fin (dt.nOf vi)) (e : dt.X.E.Relations k) (τ : Fin k → dt.X.Tag) (hnτ : (dt.relPk e τ).n ≤ dt.eDim) (a : Lex (Fin dt.eDim → A)) (r : Fin (dt.relNr e τ)) : Univ A R P dt.KIx dt.dd

The cell of the r-th leaf read at round a: the member tuple the block atom names, in the copy's block.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.expFam {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] [L.IsRelational] [L.Structure A] (zero one : A) (vi : dt.VarIx) {k : ℕ} (ts : Fin k → Fin (dt.nOf vi)) (e : dt.X.E.Relations k) (av : Fin dt.natMax) (st : TapeStD dt A R P) (τ : Fin k → dt.X.Tag) (hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim) (hn : ∀ (τ' : Fin k → dt.X.Tag), (dt.relPk e τ').n ≤ dt.eDim) (hrd : ∀ (τ' : Fin k → dt.X.Tag), dt.relNr e τ' ≤ dt.nfDim) (vAdr : Univ A R P dt.KIx dt.dd → Prop) (f₀ : dt.CtlIx → A) (a : Lex (Fin dt.eDim → A)) (j : Fin (dt.relNr e τ + 1)) : dt.CtlIx → A

The generated family of branch τ's element loop, at the pack.

Equations

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

theorem DescriptiveComplexity.Draw.Data.readLvE_exp_setFlag {L : FirstOrder.Language} {dt : Data L} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} {vi : dt.VarIx} {k : ℕ} {ts : Fin k → Fin (dt.nOf vi)} {e : dt.X.E.Relations k} {av : Fin dt.natMax} {τ : Fin k → dt.X.Tag} {hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim} {hn : ∀ (τ' : Fin k → dt.X.Tag), (dt.relPk e τ').n ≤ dt.eDim} {hrd : ∀ (τ' : Fin k → dt.X.Tag), dt.relNr e τ' ≤ dt.nfDim} (r : Fin (dt.relNr e τ)) (bb : Bool) (q : dt.CtlIx → A) (g : dt.SlotIx → A) : dt.readLvE ((dt.expArgs zero one vi ts e av hk hn hrd).setFlagE τ r bb q g) = dt.readLvE q

A leaf-read store preserves the wide loop element.

theorem DescriptiveComplexity.Draw.Data.readLvE_exp_init {L : FirstOrder.Language} {dt : Data L} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} {vi : dt.VarIx} {k : ℕ} {ts : Fin k → Fin (dt.nOf vi)} {e : dt.X.E.Relations k} {av : Fin dt.natMax} {τ : Fin k → dt.X.Tag} {hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim} {hn : ∀ (τ' : Fin k → dt.X.Tag), (dt.relPk e τ').n ≤ dt.eDim} {hrd : ∀ (τ' : Fin k → dt.X.Tag), dt.relNr e τ' ≤ dt.nfDim} (q : dt.CtlIx → A) (g : dt.SlotIx → A) : dt.readLvE ((dt.expArgs zero one vi ts e av hk hn hrd).initEl τ q g) = botTup

The branch's loop starts at the least wide tuple.

theorem DescriptiveComplexity.Draw.Data.readLvE_exp_adv {L : FirstOrder.Language} {dt : Data L} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} {vi : dt.VarIx} {k : ℕ} {ts : Fin k → Fin (dt.nOf vi)} {e : dt.X.E.Relations k} {av : Fin dt.natMax} {τ : Fin k → dt.X.Tag} {hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim} {hn : ∀ (τ' : Fin k → dt.X.Tag), (dt.relPk e τ').n ≤ dt.eDim} {hrd : ∀ (τ' : Fin k → dt.X.Tag), dt.relNr e τ' ≤ dt.nfDim} (q : dt.CtlIx → A) (g : dt.SlotIx → A) : dt.readLvE ((dt.expArgs zero one vi ts e av hk hn hrd).advEl τ q g) = tupNext (dt.readLvE q)

A round's fold-and-advance steps the wide tuple.

theorem DescriptiveComplexity.Draw.Data.readLvE_expFam {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} {vi : dt.VarIx} {k : ℕ} {ts : Fin k → Fin (dt.nOf vi)} {e : dt.X.E.Relations k} {av : Fin dt.natMax} {st : TapeStD dt A R P} {τ : Fin k → dt.X.Tag} {hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim} {hn : ∀ (τ' : Fin k → dt.X.Tag), (dt.relPk e τ').n ≤ dt.eDim} {hrd : ∀ (τ' : Fin k → dt.X.Tag), dt.relNr e τ' ≤ dt.nfDim} {vAdr : Univ A R P dt.KIx dt.dd → Prop} (f₀ : dt.CtlIx → A) (a : Lex (Fin dt.eDim → A)) (j : Fin (dt.relNr e τ + 1)) : dt.readLvE (dt.expFam RF zero one vi ts e av st τ hk hn hrd vAdr f₀ a j) = ofLex a

The loop element is the round's wide tuple, at every stage of the family.

theorem DescriptiveComplexity.Draw.Data.expFam_congr_scratch {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} {vi : dt.VarIx} {k : ℕ} {ts : Fin k → Fin (dt.nOf vi)} {e : dt.X.E.Relations k} {av : Fin dt.natMax} {st : TapeStD dt A R P} {τ : Fin k → dt.X.Tag} {hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim} {hn : ∀ (τ' : Fin k → dt.X.Tag), (dt.relPk e τ').n ≤ dt.eDim} {hrd : ∀ (τ' : Fin k → dt.X.Tag), dt.relNr e τ' ≤ dt.nfDim} {vAdr : Univ A R P dt.KIx dt.dd → Prop} {st' : TapeStD dt A R P} (h : dt.ScratchEq st st') (hreg : ¬∃ (u : Univ A R P dt.KIx dt.dd), vAdr = RF.cell u) (f₀ : dt.CtlIx → A) (a : Lex (Fin dt.eDim → A)) (j : Fin (dt.relNr e τ + 1)) : dt.expFam RF zero one vi ts e av st τ hk hn hrd vAdr f₀ a j = dt.expFam RF zero one vi ts e av st' τ hk hn hrd vAdr f₀ a j

An expansion atom's element loop is blind to the two scratch registers: it reads the levels' register sets – the mirror and VAL – and its background at the working cell alone.

The witness chain: its family, read-backs and decode

noncomputable def DescriptiveComplexity.Draw.Data.expTagFam {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] [L.IsRelational] [L.Structure A] (zero one : A) (vi : dt.VarIx) {k : ℕ} (ts : Fin k → Fin (dt.nOf vi)) (e : dt.X.E.Relations k) (av : Fin dt.natMax) (st : TapeStD dt A R P) (hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim) (hn : ∀ (τ' : Fin k → dt.X.Tag), (dt.relPk e τ').n ≤ dt.eDim) (hrd : ∀ (τ' : Fin k → dt.X.Tag), dt.relNr e τ' ≤ dt.nfDim) (vAdr : Univ A R P dt.KIx dt.dd → Prop) (f₀ : dt.CtlIx → A) (i : Fin (k * Fintype.card dt.X.Tag + 1)) : dt.CtlIx → A

The generated witness chain of an expansion atom, at the pack.

Equations

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

theorem DescriptiveComplexity.Draw.Data.expTagFam_congr_scratch {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} {vi : dt.VarIx} {k : ℕ} {ts : Fin k → Fin (dt.nOf vi)} {e : dt.X.E.Relations k} {av : Fin dt.natMax} {st : TapeStD dt A R P} {hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim} {hn : ∀ (τ' : Fin k → dt.X.Tag), (dt.relPk e τ').n ≤ dt.eDim} {hrd : ∀ (τ' : Fin k → dt.X.Tag), dt.relNr e τ' ≤ dt.nfDim} {vAdr : Univ A R P dt.KIx dt.dd → Prop} {st' : TapeStD dt A R P} (h : dt.ScratchEq st st') (hreg : ¬∃ (u : Univ A R P dt.KIx dt.dd), vAdr = RF.cell u) (f₀ : dt.CtlIx → A) (i : Fin (k * Fintype.card dt.X.Tag + 1)) : expTagFam RF zero one vi ts e av st hk hn hrd vAdr f₀ i = expTagFam RF zero one vi ts e av st' hk hn hrd vAdr f₀ i

The witness chain is blind to the two scratch registers too.

theorem DescriptiveComplexity.Draw.Data.wIx_injective {L : FirstOrder.Language} {dt : Data L} {k : ℕ} {i i' : Fin (k * Fintype.card dt.X.Tag)} (h : dt.wIx i = dt.wIx i') : i = i'

The witness numbering is injective.

noncomputable def DescriptiveComplexity.Draw.Data.tagIxOf {L : FirstOrder.Language} {dt : Data L} {k : ℕ} (ℓ : Fin k) (t : dt.X.Tag) : Fin (k * Fintype.card dt.X.Tag)

The index of one witness read, by position and tag.

Equations

• DescriptiveComplexity.Draw.Data.tagIxOf ℓ t = finProdFinEquiv (ℓ, (Fintype.equivFin dt.X.Tag) t)

theorem DescriptiveComplexity.Draw.Data.wIx_tagIxOf {L : FirstOrder.Language} {dt : Data L} {k : ℕ} (ℓ : Fin k) (t : dt.X.Tag) : dt.wIx (tagIxOf ℓ t) = (ℓ, t)

The numbering decodes the index.

theorem DescriptiveComplexity.Draw.Data.ctlBit_expTagFam_last {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} {vi : dt.VarIx} {k : ℕ} {ts : Fin k → Fin (dt.nOf vi)} {e : dt.X.E.Relations k} {av : Fin dt.natMax} {st : TapeStD dt A R P} {hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim} {hn : ∀ (τ' : Fin k → dt.X.Tag), (dt.relPk e τ').n ≤ dt.eDim} {hrd : ∀ (τ' : Fin k → dt.X.Tag), dt.relNr e τ' ≤ dt.nfDim} {vAdr : Univ A R P dt.KIx dt.dd → Prop} (hzo : zero ≠ one) (f₀ : dt.CtlIx → A) (ℓ : Fin k) (t : dt.X.Tag) : dt.ctlBit one (expTagFam RF zero one vi ts e av st hk hn hrd vAdr f₀ (Fin.last (k * Fintype.card dt.X.Tag))) (dt.tagIx hk ℓ t) ↔ dt.expTagSet vi ts st (tagIxOf ℓ t) (dt.expTagCell zero one vi ts (tagIxOf ℓ t))

The witness flags read back: after the chain, the flag of position ℓ and tag t holds the digit of the witness cell of (ℓ, t).

theorem DescriptiveComplexity.Draw.Data.tagsAre_expTagFam {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} {vi : dt.VarIx} {k : ℕ} {ts : Fin k → Fin (dt.nOf vi)} {e : dt.X.E.Relations k} {av : Fin dt.natMax} {st : TapeStD dt A R P} {hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim} {hn : ∀ (τ' : Fin k → dt.X.Tag), (dt.relPk e τ').n ≤ dt.eDim} {hrd : ∀ (τ' : Fin k → dt.X.Tag), dt.relNr e τ' ≤ dt.nfDim} {vAdr : Univ A R P dt.KIx dt.dd → Prop} (hzo : zero ≠ one) (hlin : IsLinOrd WMLe) (pts : Fin k → dt.X.Map A) (hENC : ∀ (ℓ : Fin k), wmBlk (dt.lvSet st vi (ts ℓ)) (Tag.arg (toLex (dt.lvBlk vi (ts ℓ)))) = encMap dt.ly zero one (pts ℓ)) (f₀ : dt.CtlIx → A) : (dt.expArgs zero one vi ts e av hk hn hrd).TagsAre (fun (ℓ : Fin k) => (↑(pts ℓ)).1) (expTagFam RF zero one vi ts e av st hk hn hrd vAdr f₀ (Fin.last (k * Fintype.card dt.X.Tag)))

The chain decodes the argument points' tags: if the levels' registers hold the encodings of the points, the flags are one-hot at the points' tag tuple, which is the branch dispatch's guard.

The payload at a generated state, and the leaf cells

theorem DescriptiveComplexity.Draw.Data.expPay_expFam {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} {vi : dt.VarIx} {k : ℕ} {ts : Fin k → Fin (dt.nOf vi)} {e : dt.X.E.Relations k} {av : Fin dt.natMax} {st : TapeStD dt A R P} {τ : Fin k → dt.X.Tag} {hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim} {hn : ∀ (τ' : Fin k → dt.X.Tag), (dt.relPk e τ').n ≤ dt.eDim} {hrd : ∀ (τ' : Fin k → dt.X.Tag), dt.relNr e τ' ≤ dt.nfDim} {vAdr : Univ A R P dt.KIx dt.dd → Prop} (f₀ : dt.CtlIx → A) (a : Lex (Fin dt.eDim → A)) (j : Fin (dt.relNr e τ + 1)) (r : Fin (dt.relNr e τ)) : dt.expPay zero e τ r ⋯ (dt.expFam RF zero one vi ts e av st τ hk hn hrd vAdr f₀ a j) = dt.expPayTup zero e τ ⋯ a r

The payload a leaf read spells at a generated state is the round's tuple's: the guard's computed coordinates are the cell of DescriptiveComplexity.Draw.Data.expECell.

The leaf guards, at the generated states

theorem DescriptiveComplexity.Draw.Data.expMatch_expFam {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} {vi : dt.VarIx} {k : ℕ} {ts : Fin k → Fin (dt.nOf vi)} {e : dt.X.E.Relations k} {av : Fin dt.natMax} {st : TapeStD dt A R P} {τ : Fin k → dt.X.Tag} {hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim} {hn : ∀ (τ' : Fin k → dt.X.Tag), (dt.relPk e τ').n ≤ dt.eDim} {hrd : ∀ (τ' : Fin k → dt.X.Tag), dt.relNr e τ' ≤ dt.nfDim} {vAdr : Univ A R P dt.KIx dt.dd → Prop} (hzo : zero ≠ one) (hlin : IsLinOrd WMLe) (f₀ : dt.CtlIx → A) (a : Lex (Fin dt.eDim → A)) (j : Fin (dt.relNr e τ + 1)) (r : Fin (dt.relNr e τ)) : dt.expMatch zero one vi ts e τ r ⋯ (dt.expFam RF zero one vi ts e av st τ hk hn hrd vAdr f₀ a j) (dt.back RF.cell zero one ⋯ st (RF.cell (dt.expECell zero one vi ts e τ ⋯ a r)))

A leaf read's guard holds at its cell: the computed coordinates are the round's payload, so the trip stops at the member tuple's cell.

theorem DescriptiveComplexity.Draw.Data.expMatch_expFam_uniq {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} {vi : dt.VarIx} {k : ℕ} {ts : Fin k → Fin (dt.nOf vi)} {e : dt.X.E.Relations k} {av : Fin dt.natMax} {st : TapeStD dt A R P} {τ : Fin k → dt.X.Tag} {hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim} {hn : ∀ (τ' : Fin k → dt.X.Tag), (dt.relPk e τ').n ≤ dt.eDim} {hrd : ∀ (τ' : Fin k → dt.X.Tag), dt.relNr e τ' ≤ dt.nfDim} {vAdr : Univ A R P dt.KIx dt.dd → Prop} (hzo : zero ≠ one) (hlin : IsLinOrd WMLe) (f₀ : dt.CtlIx → A) (a : Lex (Fin dt.eDim → A)) (j : Fin (dt.relNr e τ + 1)) (r : Fin (dt.relNr e τ)) {y : Univ A R P dt.KIx dt.dd → Prop} (hM : dt.expMatch zero one vi ts e τ r ⋯ (dt.expFam RF zero one vi ts e av st τ hk hn hrd vAdr f₀ a j) (dt.back RF.cell zero one ⋯ st y)) : y = RF.cell (dt.expECell zero one vi ts e τ ⋯ a r)

A leaf read's guard identifies its cell.

theorem DescriptiveComplexity.Draw.Data.expESet_expECell_iff {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [LinearOrder A] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] [L.IsRelational] [L.Structure A] {zero one : A} {vi : dt.VarIx} {k : ℕ} {ts : Fin k → Fin (dt.nOf vi)} {e : dt.X.E.Relations k} {st : TapeStD dt A R P} {τ : Fin k → dt.X.Tag} {hn : ∀ (τ' : Fin k → dt.X.Tag), (dt.relPk e τ').n ≤ dt.eDim} (hzo : zero ≠ one) (hlin : IsLinOrd WMLe) (pts : Fin k → dt.X.Map A) (hENC : ∀ (ℓ : Fin k), wmBlk (dt.lvSet st vi (ts ℓ)) (Tag.arg (toLex (dt.lvBlk vi (ts ℓ)))) = encMap dt.ly zero one (pts ℓ)) (a : Lex (Fin dt.eDim → A)) (r : Fin (dt.relNr e τ)) {f : dt.CtlIx → A} (hf : dt.readLvE f = ofLex a) : dt.expESet vi ts e st τ r (dt.expECell zero one vi ts e τ ⋯ a r) ↔ BlkAtom.holds (dt.X.B.replicateAssign fun (ℓ : Fin k) => (↑(pts ℓ)).2) (fun (j : Fin (dt.relPk e τ).n) => f (dt.lvE (Fin.castLE ⋯ j))) (BlkAtom.blkA (relLeafData e τ r).fst (relLeafData e τ r).snd)

What a leaf trip's digit means: at a round's cell, the register's bit is the block atom's value at the points the registers encode, read at the valuation the round's tuple spells. This is the hav input of DescriptiveComplexity.Draw.Data.expLeafVal_iff, hence of the exit verdict.

The expansion atom's machine run

theorem DescriptiveComplexity.Draw.Data.exp_run {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} (RF : RegFile (Univ A R P dt.KIx dt.dd)) (hord : ∀ (x y : Univ A R P dt.KIx dt.dd), WMLe x y ↔ tagTupleLe x y) [Nonempty A] [L.IsRelational] [L.Structure A] {vi : dt.VarIx} {k : ℕ} {ts : Fin k → Fin (dt.nOf vi)} {e : dt.X.E.Relations k} {av : Fin dt.natMax} {st : TapeStD dt A R P} {hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim} {hn : ∀ (τ' : Fin k → dt.X.Tag), (dt.relPk e τ').n ≤ dt.eDim} {hrd : ∀ (τ' : Fin k → dt.X.Tag), dt.relNr e τ' ≤ dt.nfDim} {emb : TagPh (k * Fintype.card dt.X.Tag) (Fin k → dt.X.Tag) (dt.relNr e) → P} {exitPh : P} {rEmb : (i : TagSite (k * Fintype.card dt.X.Tag) (Fin k → dt.X.Tag) (dt.relNr e)) → TagSh (k * Fintype.card dt.X.Tag) (Fin k → dt.X.Tag) (dt.relNr e) i → R} [Finite dt.KIx] (hrules : ∀ (i : TagSite (k * Fintype.card dt.X.Tag) (Fin k → dt.X.Tag) (dt.relNr e)) (ρ : TagSh (k * Fintype.card dt.X.Tag) (Fin k → dt.X.Tag) (dt.relNr e) i), PR.rules (rEmb i ρ) = tagRule PR.one Slot.wk Slot.reg emb (dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).rdTrackT (dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).MatchT (dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).setTagFlag (dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).TagsAre (dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).rdTrackE (dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).MatchE (dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).setFlagE (dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).initEl (dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).advEl (dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).exitSt (dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).IsMaxEl exitPh i ρ) (hR : PR.table.Reads) (hlin : IsLinOrd WMLe) {gbot : Univ A R P dt.KIx dt.dd} (hbot : ∀ (y : Univ A R P dt.KIx dt.dd), WMLe gbot y) {v v' : Univ A R P dt.KIx dt.dd → Prop} (hv : WMSetLt WMLe v (RF.cell gbot)) (hvi : WMIncr WMLe v v') (hwkSt : st.wk = fun (r : Univ A R P dt.KIx dt.dd → Prop) => r = v) {t₀ : dt.SlotIx} {m₀ : Univ A R P dt.KIx dt.dd → Prop} (hm₀ : ∀ (r : Univ A R P dt.KIx dt.dd → Prop), dt.back RF.cell PR.zero PR.one ⋯ st r t₀ = bitVal PR.zero PR.one (bitAtOf RF.cell m₀ r)) (hwkt₀ : Slot.wk ≠ t₀) (hrgt₀ : Slot.reg ≠ t₀) (pts : Fin k → dt.X.Map A) (hENC : ∀ (ℓ : Fin k), wmBlk (dt.lvSet st vi (ts ℓ)) (Tag.arg (toLex (dt.lvBlk vi (ts ℓ)))) = encMap dt.ly PR.zero PR.one (pts ℓ)) (f₀ : dt.CtlIx → A) : Relation.ReflTransGen (wideData (Univ A R P dt.KIx dt.dd)).Step { state := Sum.inr (PR.stElt (tagFirstRd emb) f₀), head := Sum.inl v, tape := wideTape (PR.trackTapeAt RF.cell t₀ (dt.back RF.cell PR.zero PR.one ⋯ st) m₀) (PR.syElt PR.blank) } { state := Sum.inr (PR.stElt exitPh ((dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).exitSt (fun (ℓ : Fin k) => (↑(pts ℓ)).1) (dt.expFam RF PR.zero PR.one vi ts e av st (fun (ℓ : Fin k) => (↑(pts ℓ)).1) hk hn hrd v (expTagFam RF PR.zero PR.one vi ts e av st hk hn hrd v f₀ (Fin.last (k * Fintype.card dt.X.Tag))) (toLex topTup) (Fin.last (dt.relNr e fun (ℓ : Fin k) => (↑(pts ℓ)).1))) (dt.back RF.cell PR.zero PR.one ⋯ st v))), head := Sum.inl v', tape := wideTape (PR.trackTapeAt RF.cell t₀ (dt.back RF.cell PR.zero PR.one ⋯ st) m₀) (PR.syElt PR.blank) }

The expansion atom's machine run: from the machinery's first phase at the marker – the witness chain decoding the argument points' tags, the dispatch onto their branch, and that branch's wide element loop, one leaf trip per block atom – to the exit phase one cell to the marker's right.

The sub-fold: the sac invariant and the exit verdict

noncomputable def DescriptiveComplexity.Draw.Data.expLeafP {L : FirstOrder.Language} (dt : Data L) {A : Type} [LinearOrder A] [L.IsRelational] [L.Structure A] {k : ℕ} (e : dt.X.E.Relations k) (τ : Fin k → dt.X.Tag) (hnτ : (dt.relPk e τ).n ≤ dt.eDim) (pts : Fin k → dt.X.Map A) (v : Fin dt.eDim → A) : Prop

The branch's leaf, over the wide valuation: the defining sentence's matrix at the points' assignments, its levels read off the first n coordinates of the wide tuple.

Equations

• dt.expLeafP e τ hnτ pts v = dt.expLeaf e τ (fun (ℓ : Fin k) => (↑(pts ℓ)).2) fun (j : Fin (dt.relPk e τ).n) => v (Fin.castLE hnτ j)

theorem DescriptiveComplexity.Draw.Data.readSac_setCtl {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} {q : dt.CtlIx} (hq : ∀ (j : Fin dt.eDim), dt.sacC j ≠ q) (b : Prop) (f : dt.CtlIx → A) (j : ℕ) : dt.readSac one (dt.setCtl zero one q b f) j ↔ dt.readSac one f j

A sub-fold accumulator rides along a control-bit store off it.

theorem DescriptiveComplexity.Draw.Data.readSac_advLvE {L : FirstOrder.Language} {dt : Data L} {A : Type} [LinearOrder A] {one : A} (f : dt.CtlIx → A) (j : ℕ) : dt.readSac one (dt.advLvE f) j ↔ dt.readSac one f j

A sub-fold accumulator rides along a wide-tuple advance.

theorem DescriptiveComplexity.Draw.Data.readSac_chainSt {L : FirstOrder.Language} {dt : Data L} {A : Type} {one : A} {nr : ℕ} (bit : Fin nr → Prop) (upd : Fin nr → Bool → (dt.CtlIx → A) → dt.CtlIx → A) (hupd : ∀ (i : Fin nr) (b : Bool) (f : dt.CtlIx → A) (j : ℕ), dt.readSac one (upd i b f) j ↔ dt.readSac one f j) (base : dt.CtlIx → A) (n j : ℕ) : dt.readSac one (chainSt bit upd base n) j ↔ dt.readSac one base j

A within-round chain preserving the accumulators preserves them end to end.

theorem DescriptiveComplexity.Draw.Data.readSac_exp_setFlag {L : FirstOrder.Language} {dt : Data L} {A : Type} [LinearOrder A] [Finite A] [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} {vi : dt.VarIx} {k : ℕ} {ts : Fin k → Fin (dt.nOf vi)} {e : dt.X.E.Relations k} {av : Fin dt.natMax} {τ : Fin k → dt.X.Tag} {hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim} {hn : ∀ (τ' : Fin k → dt.X.Tag), (dt.relPk e τ').n ≤ dt.eDim} {hrd : ∀ (τ' : Fin k → dt.X.Tag), dt.relNr e τ' ≤ dt.nfDim} (r : Fin (dt.relNr e τ)) (bb : Bool) (q : dt.CtlIx → A) (g : dt.SlotIx → A) (j : ℕ) : dt.readSac one ((dt.expArgs zero one vi ts e av hk hn hrd).setFlagE τ r bb q g) j ↔ dt.readSac one q j

A leaf-read store preserves the accumulators.

theorem DescriptiveComplexity.Draw.Data.ctlBit_rdf_expFam {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} {vi : dt.VarIx} {k : ℕ} {ts : Fin k → Fin (dt.nOf vi)} {e : dt.X.E.Relations k} {av : Fin dt.natMax} {st : TapeStD dt A R P} {τ : Fin k → dt.X.Tag} {hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim} {hn : ∀ (τ' : Fin k → dt.X.Tag), (dt.relPk e τ').n ≤ dt.eDim} {hrd : ∀ (τ' : Fin k → dt.X.Tag), dt.relNr e τ' ≤ dt.nfDim} {vAdr : Univ A R P dt.KIx dt.dd → Prop} (hzo : zero ≠ one) (f₀ : dt.CtlIx → A) (a : Lex (Fin dt.eDim → A)) (r : Fin (dt.relNr e τ)) : dt.ctlBit one (dt.expFam RF zero one vi ts e av st τ hk hn hrd vAdr f₀ a (Fin.last (dt.relNr e τ))) (dt.rdfC (Fin.castLE ⋯ r)) ↔ dt.expESet vi ts e st τ r (dt.expECell zero one vi ts e τ ⋯ a r)

The leaf-read flags read back: at a round's end, the flag of the r-th block atom holds the digit of the round's cell.

theorem DescriptiveComplexity.Draw.Data.expLeafVal_expFam {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} {vi : dt.VarIx} {k : ℕ} {ts : Fin k → Fin (dt.nOf vi)} {e : dt.X.E.Relations k} {av : Fin dt.natMax} {st : TapeStD dt A R P} {τ : Fin k → dt.X.Tag} {hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim} {hn : ∀ (τ' : Fin k → dt.X.Tag), (dt.relPk e τ').n ≤ dt.eDim} {hrd : ∀ (τ' : Fin k → dt.X.Tag), dt.relNr e τ' ≤ dt.nfDim} {vAdr : Univ A R P dt.KIx dt.dd → Prop} (hzo : zero ≠ one) (hlin : IsLinOrd WMLe) (pts : Fin k → dt.X.Map A) (hENC : ∀ (ℓ : Fin k), wmBlk (dt.lvSet st vi (ts ℓ)) (Tag.arg (toLex (dt.lvBlk vi (ts ℓ)))) = encMap dt.ly zero one (pts ℓ)) (f₀ : dt.CtlIx → A) (a : Lex (Fin dt.eDim → A)) : dt.expLeafVal one e τ ⋯ ⋯ (dt.expFam RF zero one vi ts e av st τ hk hn hrd vAdr f₀ a (Fin.last (dt.relNr e τ))) ↔ dt.expLeafP e τ ⋯ pts (ofLex a)

The leaf flag's value at a round's end is the branch's leaf: with the flags holding the block atoms' bits and the loop element the round's tuple, the Boolean function the control computes is the leaf predicate at that tuple.

theorem DescriptiveComplexity.Draw.Data.readSac_expIter {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} {vi : dt.VarIx} {k : ℕ} {ts : Fin k → Fin (dt.nOf vi)} {e : dt.X.E.Relations k} {av : Fin dt.natMax} {st : TapeStD dt A R P} {τ : Fin k → dt.X.Tag} {hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim} {hn : ∀ (τ' : Fin k → dt.X.Tag), (dt.relPk e τ').n ≤ dt.eDim} {hrd : ∀ (τ' : Fin k → dt.X.Tag), dt.relNr e τ' ≤ dt.nfDim} {vAdr : Univ A R P dt.KIx dt.dd → Prop} (hzo : zero ≠ one) (hlin : IsLinOrd WMLe) (pts : Fin k → dt.X.Map A) (hENC : ∀ (ℓ : Fin k), wmBlk (dt.lvSet st vi (ts ℓ)) (Tag.arg (toLex (dt.lvBlk vi (ts ℓ)))) = encMap dt.ly zero one (pts ℓ)) (f₀ : dt.CtlIx → A) (a : Lex (Fin dt.eDim → A)) (j : ℕ) (hj : j < dt.eDim) : dt.readSac one (elemIter ((dt.expArgs zero one vi ts e av hk hn hrd).setFlagE τ) ((dt.expArgs zero one vi ts e av hk hn hrd).initEl τ) ((dt.expArgs zero one vi ts e av hk hn hrd).advEl τ) (dt.back RF.cell zero one ⋯ st) vAdr (dt.expESet vi ts e st τ) (dt.expECell zero one vi ts e τ ⋯) f₀ a) j ↔ accCVal (dt.relPk e τ).pol (dt.expLeafP e τ ⋯ pts) (fun (x1 x2 : A) => x1 ≤ x2) j (ofLex a)

The sub-fold's accumulators fold the strict prefix: at every round's entry, the sac slots hold the completed-subtree contributions of the branch's prefix at the round's tuple.

theorem DescriptiveComplexity.Draw.Data.ctlBit_avC_exp_exit {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} {vi : dt.VarIx} {k : ℕ} {ts : Fin k → Fin (dt.nOf vi)} {e : dt.X.E.Relations k} {av : Fin dt.natMax} {st : TapeStD dt A R P} {τ : Fin k → dt.X.Tag} {hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim} {hn : ∀ (τ' : Fin k → dt.X.Tag), (dt.relPk e τ').n ≤ dt.eDim} {hrd : ∀ (τ' : Fin k → dt.X.Tag), dt.relNr e τ' ≤ dt.nfDim} {vAdr : Univ A R P dt.KIx dt.dd → Prop} (hzo : zero ≠ one) (hlin : IsLinOrd WMLe) (pts : Fin k → dt.X.Map A) (hENC : ∀ (ℓ : Fin k), wmBlk (dt.lvSet st vi (ts ℓ)) (Tag.arg (toLex (dt.lvBlk vi (ts ℓ)))) = encMap dt.ly zero one (pts ℓ)) (f₀ : dt.CtlIx → A) : dt.ctlBit one ((dt.expArgs zero one vi ts e av hk hn hrd).exitSt τ (dt.expFam RF zero one vi ts e av st τ hk hn hrd vAdr f₀ (toLex topTup) (Fin.last (dt.relNr e τ))) (dt.back RF.cell zero one ⋯ st vAdr)) (dt.avC av) ↔ foldFrom (dt.relPk e τ).pol (dt.expLeafP e τ ⋯ pts) (fun (x1 x2 : A) => x1 ≤ x2) 0 topTup

The verdict the exit control carries: the atom's slot holds the fold of the branch's whole prefix at the points' assignments – the value DescriptiveComplexity.Draw.Data.expLeaf's prefix takes over every wide tuple, which DescriptiveComplexity.Problems.Wide.DrawExp reads as the expansion atom's truth.

theorem DescriptiveComplexity.Draw.Data.ctlBit_avC_exp_relMap {L : FirstOrder.Language} {dt : Data L} {A R P : Type} [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] [Finite R] [Finite P] (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] [L.IsRelational] [L.Structure A] {zero one : A} {vi : dt.VarIx} {k : ℕ} {ts : Fin k → Fin (dt.nOf vi)} {e : dt.X.E.Relations k} {av : Fin dt.natMax} {st : TapeStD dt A R P} {hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim} {hn : ∀ (τ' : Fin k → dt.X.Tag), (dt.relPk e τ').n ≤ dt.eDim} {hrd : ∀ (τ' : Fin k → dt.X.Tag), dt.relNr e τ' ≤ dt.nfDim} {vAdr : Univ A R P dt.KIx dt.dd → Prop} (hzo : zero ≠ one) (hlin : IsLinOrd WMLe) (pts : Fin k → dt.X.Map A) (hENC : ∀ (ℓ : Fin k), wmBlk (dt.lvSet st vi (ts ℓ)) (Tag.arg (toLex (dt.lvBlk vi (ts ℓ)))) = encMap dt.ly zero one (pts ℓ)) (f₀ : dt.CtlIx → A) : dt.ctlBit one ((dt.expArgs zero one vi ts e av hk hn hrd).exitSt (fun (ℓ : Fin k) => (↑(pts ℓ)).1) (dt.expFam RF zero one vi ts e av st (fun (ℓ : Fin k) => (↑(pts ℓ)).1) hk hn hrd vAdr f₀ (toLex topTup) (Fin.last (dt.relNr e fun (ℓ : Fin k) => (↑(pts ℓ)).1))) (dt.back RF.cell zero one ⋯ st vAdr)) (dt.avC av) ↔ FirstOrder.Language.Structure.RelMap e pts

The expansion atom's verdict is its truth: at the argument points the registers encode, the bit the exit control files in the atom's slot is RelMap of the expansion – the machine has evaluated the defining sentence.