The gates, instantiated: the domain evaluation of one block

The fourth semantic instantiation: a gate's machinery at the pack DescriptiveComplexity.Draw.Data.gateArgs. The gate asks of one block of the working address – held in MIRROR – 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 DescriptiveComplexity.Draw.decRho – the raw block value, no encoding assumed, which is what lets the gate be the check rather than presuppose it.

The layer mirrors DescriptiveComplexity.Problems.Wide.DrawInstExp with two differences: every read walks the MIRROR track, and the exit conjoins into the gates' flag, so one failing block fails the address.

noncomputable def DescriptiveComplexity.Draw.Data.gateTagCell {L : FirstOrder.Language} (dt : Data L) {A R P : Type} (zero one : A) (b : Fin dt.ko ⊕ Fin dt.ki) (c : Fin (Fintype.card dt.X.Tag)) : Univ A R P dt.KIx dt.dd

The cell of one tag's witness read: 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.gateECell {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [L.IsRelational] (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)) : Univ A R P dt.KIx dt.dd

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

Equations

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

noncomputable def DescriptiveComplexity.Draw.Data.gateTagFam {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) (b : Fin dt.ko ⊕ Fin dt.ki) (st : TapeStD dt A R P) (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.gateFam {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) (b : Fin dt.ko ⊕ Fin dt.ki) (st : TapeStD dt A R P) (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

The gate's machine run

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

The gates' flag rides, and the conjoining exit