The gates at an arbitrary file

A gate asks of one block of the working address that it encode a point: the witness chain reads every tag's witness cell, the branch dispatches on the one-hot decoding, and the branch's element loop evaluates the tag's domain sentence at the decoded assignment. Every read goes to the cell of an encoded tuple in the gated block, so this is DescriptiveComplexity.Problems.Wide.DrawInstGate read at a coarse file exactly as DescriptiveComplexity.Problems.Wide.DrawIxExp reads the expansion atoms: the cells become the registers the layout names (DescriptiveComplexity.Draw.Data.ixEncG_iff), the marks become marks on registers, and the block value the gate reads is the one the address the marks stand for holds (DescriptiveComplexity.ixAddr).

Only the declarations that mention the file are restated here; everything the elementwise file says about the control alone is imported.

noncomputable def DescriptiveComplexity.Draw.Data.ixGateTagCell {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)] {I : Type} (F : LaidFile dt A R P I) {zero : A} (hhas : F.toLayout.HasName zero) (one : A) (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin (Fintype.card dt.X.Tag)) : I

The register of one tag's witness read: the one the layout names by the tag's witness tuple in the gated block.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.ixGateECell {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)] {I : Type} (F : LaidFile dt A R P I) [L.IsRelational] {zero : A} (hhas : F.toLayout.HasName zero) (one : A) (b : Fin dt.ko ⊕ Fin dt.ki) (t : dt.X.Tag) (hnt : (dt.domPk t).n ≤ dt.eDim) (a : Lex (Fin dt.eDim → A)) (r : Fin (dt.domNr t)) : I

The register of the r-th domain leaf read at round a: the one the layout names by the member tuple the block atom spells.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.ixGateTagFam {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] {I : Type} (F : LaidFile dt A R P I) [Nonempty A] [L.IsRelational] [L.Structure A] {zero : A} (hhas : F.toLayout.HasName zero) (one : A) (b : Fin dt.ko ⊕ Fin dt.ki) (st : TapeSt dt A R P I) (hc : Fintype.card dt.X.Tag ≤ dt.ntgDim) (hn : ∀ (t' : dt.X.Tag), (dt.domPk t').n ≤ dt.eDim) (hrd : ∀ (t' : dt.X.Tag), dt.domNr t' ≤ dt.nfDim) (vAdr : Univ A R P dt.KIx dt.dd → Prop) (f₀ : dt.CtlIx → A) (i : Fin (Fintype.card dt.X.Tag + 1)) : dt.CtlIx → A

The generated witness chain of a gate, at the pack.

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.ixGateFam {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] {I : Type} (F : LaidFile dt A R P I) [Nonempty A] [L.IsRelational] [L.Structure A] {zero : A} (hhas : F.toLayout.HasName zero) (one : A) (b : Fin dt.ko ⊕ Fin dt.ki) (st : TapeSt dt A R P I) (t : dt.X.Tag) (hc : Fintype.card dt.X.Tag ≤ dt.ntgDim) (hn : ∀ (t' : dt.X.Tag), (dt.domPk t').n ≤ dt.eDim) (hrd : ∀ (t' : dt.X.Tag), dt.domNr t' ≤ 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.domNr t + 1)) : dt.CtlIx → A

The generated family of branch t's domain loop, at the pack.

Equations

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

The witness chain: read-back and decode

The domain payload at a generated state, and the leaf guards

noncomputable def DescriptiveComplexity.Draw.Data.ixGateLeafP {L : FirstOrder.Language} {A R P : Type} [LinearOrder A] [L.IsRelational] [L.Structure A] (dt : Data L) {I : Type} (b : Fin dt.ko ⊕ Fin dt.ki) (st : TapeSt dt A R P I) (t : dt.X.Tag) (hnt : (dt.domPk t).n ≤ dt.eDim) {elt : I → Univ A R P dt.KIx dt.dd} (zero one : A) (v : Fin dt.eDim → A) : Prop

A gate's leaf at the file, over the wide valuation: the tag's domain sentence at the decoded assignment of the block value the marks' address holds.

Equations

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

The gate's machine run

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

The gates' flag rides, and the conjoining exit