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

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_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.

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.

The payload at a generated state, and the leaf cells

The leaf guards, at the generated states

The expansion atom's machine run

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