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))
:
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.
Instances For
Dependency graph
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))
:
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.
Instances For
Dependency graph
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.
Instances For
Dependency graph
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.
Instances For
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.readLvE_gate_setFlag
{L : FirstOrder.Language}
{dt : Data L}
{A : Type}
[LinearOrder A]
[Finite A]
[Nonempty A]
[L.IsRelational]
[L.Structure A]
{zero one : A}
{b : Fin dt.ko ⊕ Fin dt.ki}
{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}
(r : Fin (dt.domNr t))
(bb : Bool)
(q : dt.CtlIx → A)
(g : dt.SlotIx → A)
:
A domain leaf-read store preserves the wide loop element.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.readLvE_gate_init
{L : FirstOrder.Language}
{dt : Data L}
{A : Type}
[LinearOrder A]
[Finite A]
[Nonempty A]
[L.IsRelational]
[L.Structure A]
{zero one : A}
{b : Fin dt.ko ⊕ Fin dt.ki}
{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}
(q : dt.CtlIx → A)
(g : dt.SlotIx → A)
:
The branch's domain loop starts at the least wide tuple.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.readLvE_gate_adv
{L : FirstOrder.Language}
{dt : Data L}
{A : Type}
[LinearOrder A]
[Finite A]
[Nonempty A]
[L.IsRelational]
[L.Structure A]
{zero one : A}
{b : Fin dt.ko ⊕ Fin dt.ki}
{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}
(q : dt.CtlIx → A)
(g : dt.SlotIx → A)
:
A domain round's fold-and-advance steps the wide tuple.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.readLvE_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))
:
The loop element is the round's wide tuple, at every stage of a gate's family.
Dependency graph
The witness chain: read-back and decode #
theorem
DescriptiveComplexity.Draw.Data.ctlBit_gateTagFam_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}
{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}
(hzo : zero ≠ one)
(f₀ : dt.CtlIx → A)
(t' : dt.X.Tag)
:
dt.ctlBit one (dt.gateTagFam RF zero one b st hc hn hrd vAdr f₀ (Fin.last (Fintype.card dt.X.Tag)))
(dt.gateTagC hc t') ↔ st.mir (dt.gateTagCell zero one b ((Fintype.equivFin dt.X.Tag) t'))
The witness flags read back: after the chain, the flag of tag t'
holds the digit of t''s witness cell in the gated block.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.ctlBit_gateTagFam_wit
{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}
(hzo : zero ≠ one)
(f₀ : dt.CtlIx → A)
(t' : dt.X.Tag)
:
The witness flags after the chain read the block value: the flag of
tag t' holds exactly when t''s witness tuple belongs to the gated
block.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.dspTagsAre_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}
{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}
(hzo : zero ≠ one)
(f₀ : dt.CtlIx → A)
:
dt.DspTagsAre one hc (dt.dspTagOf zero one (wmBlk st.mir (Tag.arg (toLex b))))
(dt.gateTagFam RF zero one b st hc hn hrd vAdr f₀ (Fin.last (Fintype.card dt.X.Tag)))
The chain's decoding always dispatches: at a block value with a one-hot witness the flags decode its tag, and at any other the default branch fires – the totality of the branch checkpoint on every block value the sweep produces.
Dependency graph
The domain payload at a generated state, and the leaf guards #
theorem
DescriptiveComplexity.Draw.Data.domPay_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))
(r : Fin (dt.domNr t))
:
dt.domPay zero t r ⋯ (dt.gateFam RF zero one b st t hc hn hrd vAdr f₀ a j) = pad zero fun (q : Fin (dt.X.B.arity (domLeafData t r).fst)) => ofLex a (Fin.castLE ⋯ ((domLeafData t r).snd q))
The payload a domain leaf spells at a generated state is the round's tuple's.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.domMatch_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}
(hzo : zero ≠ one)
(hlin : IsLinOrd WMLe)
(f₀ : dt.CtlIx → A)
(a : Lex (Fin dt.eDim → A))
(j : Fin (dt.domNr t + 1))
(r : Fin (dt.domNr t))
:
A domain leaf read's guard holds at its cell.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.domMatch_gateFam_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}
{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}
(hzo : zero ≠ one)
(hlin : IsLinOrd WMLe)
(f₀ : dt.CtlIx → A)
(a : Lex (Fin dt.eDim → A))
(j : Fin (dt.domNr t + 1))
(r : Fin (dt.domNr t))
{y : Univ A R P dt.KIx dt.dd → Prop}
(hM :
dt.domMatch zero one b t r ⋯ (dt.gateFam RF zero one b st t hc hn hrd vAdr f₀ a j) (dt.back RF.cell zero one ⋯ st y))
:
A domain leaf read's guard identifies its cell.
Dependency graph
The gate's machine run #
theorem
DescriptiveComplexity.Draw.Data.gate_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))
[Nonempty A]
[L.IsRelational]
[L.Structure 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}
{emb : TagPh (Fintype.card dt.X.Tag) dt.X.Tag dt.domNr → P}
{exitPh : P}
{rEmb : (i : TagSite (Fintype.card dt.X.Tag) dt.X.Tag dt.domNr) → TagSh (Fintype.card dt.X.Tag) dt.X.Tag dt.domNr i → R}
[Finite dt.KIx]
(hrules :
∀ (i : TagSite (Fintype.card dt.X.Tag) dt.X.Tag dt.domNr) (ρ : TagSh (Fintype.card dt.X.Tag) dt.X.Tag dt.domNr i),
PR.rules (rEmb i ρ) = tagRule PR.one Slot.wk Slot.reg emb (dt.gateArgs PR.zero PR.one b hc hn hrd).rdTrackT
(dt.gateArgs PR.zero PR.one b hc hn hrd).MatchT (dt.gateArgs PR.zero PR.one b hc hn hrd).setTagFlag
(dt.gateArgs PR.zero PR.one b hc hn hrd).TagsAre (dt.gateArgs PR.zero PR.one b hc hn hrd).rdTrackE
(dt.gateArgs PR.zero PR.one b hc hn hrd).MatchE (dt.gateArgs PR.zero PR.one b hc hn hrd).setFlagE
(dt.gateArgs PR.zero PR.one b hc hn hrd).initEl (dt.gateArgs PR.zero PR.one b hc hn hrd).advEl
(dt.gateArgs PR.zero PR.one b hc hn hrd).exitSt (dt.gateArgs PR.zero PR.one b hc 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₀)
(htag : dt.dspTagOf PR.zero PR.one (wmBlk st.mir (Tag.arg (toLex b))) = t)
(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.gateArgs PR.zero PR.one b hc hn hrd).exitSt t
(dt.gateFam RF PR.zero PR.one b st t hc hn hrd v
(dt.gateTagFam RF PR.zero PR.one b st hc hn hrd v f₀ (Fin.last (Fintype.card dt.X.Tag))) (toLex topTup)
(Fin.last (dt.domNr t)))
(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 gate's machine run: from the machinery's first phase at the marker – the witness chain reading the block value, the dispatch onto the decoded tag's branch (or the default tag's, where the witness is not one-hot), and the branch's domain loop over the wide tuples – to the exit phase one cell to the marker's right.
Dependency graph
The sub-fold: the sac invariant and the conjoining exit #
noncomputable def
DescriptiveComplexity.Draw.Data.gateLeafP
{L : FirstOrder.Language}
(dt : Data L)
{A R P : Type}
[LinearOrder A]
[L.IsRelational]
[L.Structure A]
(b : Fin dt.ko ⊕ Fin dt.ki)
(st : TapeStD dt A R P)
(t : dt.X.Tag)
(hnt : (dt.domPk t).n ≤ dt.eDim)
(zero one : A)
(v : Fin dt.eDim → A)
:
A gate's leaf, over the wide valuation: the tag's domain sentence at the decoded assignment of the raw block value – no encoding assumed.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.ctlBit_rdf_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}
(hzo : zero ≠ one)
(f₀ : dt.CtlIx → A)
(a : Lex (Fin dt.eDim → A))
(r : Fin (dt.domNr t))
:
The domain leaf-read flags read back at a round's end.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.domLeafVal_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}
(hzo : zero ≠ one)
(f₀ : dt.CtlIx → A)
(a : Lex (Fin dt.eDim → A))
:
The leaf flag's value at a round's end is the gate's leaf: the domain sentence's matrix at the decoded assignment, read at the round's tuple.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.readSac_gateIter
{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}
(hzo : zero ≠ one)
(f₀ : dt.CtlIx → A)
(a : Lex (Fin dt.eDim → A))
(j : ℕ)
(hj : j < dt.eDim)
:
dt.readSac one
(elemIter ((dt.gateArgs zero one b hc hn hrd).setFlagE t) ((dt.gateArgs zero one b hc hn hrd).initEl t)
((dt.gateArgs zero one b hc hn hrd).advEl t) (dt.back RF.cell zero one ⋯ st) vAdr
(fun (x : Fin (dt.domNr t)) => st.mir) (dt.gateECell zero one b t ⋯) f₀ a)
j ↔ accCVal (dt.domPk t).pol (dt.gateLeafP b st t ⋯ zero one) (fun (x1 x2 : A) => x1 ≤ x2) j (ofLex a)
A gate's accumulators fold the strict prefix: at every round's
entry, the sac slots hold the contributions of the domain sentence's
prefix at the round's tuple.
Dependency graph
The gates' flag rides, and the conjoining exit #
theorem
DescriptiveComplexity.Draw.Data.ctlBit_chainSt_of
{L : FirstOrder.Language}
{dt : Data L}
{A : Type}
{one : A}
(q : dt.CtlIx)
{nr : ℕ}
(bit : Fin nr → Prop)
(upd : Fin nr → Bool → (dt.CtlIx → A) → dt.CtlIx → A)
(hupd : ∀ (i : Fin nr) (bb : Bool) (f : dt.CtlIx → A), dt.ctlBit one (upd i bb f) q ↔ dt.ctlBit one f q)
(base : dt.CtlIx → A)
(n : ℕ)
:
A fixed control bit rides along a chain that never writes it.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.ctlBit_tgf_gate_adv
{L : FirstOrder.Language}
{dt : Data L}
{A : Type}
[LinearOrder A]
[Finite A]
[Nonempty A]
[L.IsRelational]
[L.Structure A]
{zero one : A}
{b : Fin dt.ko ⊕ Fin dt.ki}
{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}
(t₂ : dt.X.Tag)
(q : dt.CtlIx → A)
(g : dt.SlotIx → A)
:
A witness flag rides along one branch round.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.ctlBit_tgf_gate_init
{L : FirstOrder.Language}
{dt : Data L}
{A : Type}
[LinearOrder A]
[Finite A]
[Nonempty A]
[L.IsRelational]
[L.Structure A]
{zero one : A}
{b : Fin dt.ko ⊕ Fin dt.ki}
{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}
(t₂ : dt.X.Tag)
(q : dt.CtlIx → A)
(g : dt.SlotIx → A)
:
A witness flag rides along a branch loop's start.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.ctlBit_tgf_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}
(t₂ : dt.X.Tag)
(f₀ : dt.CtlIx → A)
(a : Lex (Fin dt.eDim → A))
(j : Fin (dt.domNr t + 1))
:
The witness flags survive a branch's domain loop: neither the leaf reads nor the fold write them, so the conjoining exit still reads the chain's decoding.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.ctlBit_gateFlagC_gate_adv
{L : FirstOrder.Language}
{dt : Data L}
{A : Type}
[LinearOrder A]
[Finite A]
[Nonempty A]
[L.IsRelational]
[L.Structure A]
{zero one : A}
{b : Fin dt.ko ⊕ Fin dt.ki}
{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}
(q : dt.CtlIx → A)
(g : dt.SlotIx → A)
:
The gates' flag rides along one branch round.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.ctlBit_gateFlagC_gate_init
{L : FirstOrder.Language}
{dt : Data L}
{A : Type}
[LinearOrder A]
[Finite A]
[Nonempty A]
[L.IsRelational]
[L.Structure A]
{zero one : A}
{b : Fin dt.ko ⊕ Fin dt.ki}
{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}
(q : dt.CtlIx → A)
(g : dt.SlotIx → A)
:
The gates' flag rides along a branch loop's start.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.ctlBit_gateFlagC_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))
:
The gates' flag survives one gate's machinery: neither the witness chain nor the branch's domain loop writes it.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.ctlBit_gateFlagC_gate_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]
(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}
(hzo : zero ≠ one)
(f₀ : dt.CtlIx → A)
:
dt.ctlBit one
((dt.gateArgs zero one b hc hn hrd).exitSt t
(dt.gateFam RF zero one b st t hc hn hrd vAdr
(dt.gateTagFam RF zero one b st hc hn hrd vAdr f₀ (Fin.last (Fintype.card dt.X.Tag))) (toLex topTup)
(Fin.last (dt.domNr t)))
(dt.back RF.cell zero one ⋯ st vAdr))
dt.gateFlagC ↔ dt.ctlBit one f₀ dt.gateFlagC ∧ (∀ (t' : dt.X.Tag), wmBlk st.mir (Tag.arg (toLex b)) (encTagTup dt.ly zero one t') ↔ t' = t) ∧ foldFrom (dt.domPk t).pol (dt.gateLeafP b st t ⋯ zero one) (fun (x1 x2 : A) => x1 ≤ x2) 0 topTup
The verdict the conjoining exit carries: the gates' flag holds after one gate exactly when it held before – every earlier block passed – and the block value's witness is one-hot at the dispatched tag – so the default branch always clears – and the fold of this block's domain sentence over the whole wide enumeration holds, i.e., the tag's domain condition at the decoded assignment.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.ctlBit_gateFlagC_gate_domHolds
{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}
(hzo : zero ≠ one)
(f₀ : dt.CtlIx → A)
:
dt.ctlBit one
((dt.gateArgs zero one b hc hn hrd).exitSt t
(dt.gateFam RF zero one b st t hc hn hrd vAdr
(dt.gateTagFam RF zero one b st hc hn hrd vAdr f₀ (Fin.last (Fintype.card dt.X.Tag))) (toLex topTup)
(Fin.last (dt.domNr t)))
(dt.back RF.cell zero one ⋯ st vAdr))
dt.gateFlagC ↔ dt.ctlBit one f₀ dt.gateFlagC ∧ (∀ (t' : dt.X.Tag), wmBlk st.mir (Tag.arg (toLex b)) (encTagTup dt.ly zero one t') ↔ t' = t) ∧ ExpExpansion.DomHolds (t, decRho dt.ly zero one (wmBlk st.mir (Tag.arg (toLex b))))
The gate's verdict is the gate: after one gate the flag holds exactly when it held before – every earlier block passed – and the block value's witness is one-hot at the dispatched tag and the decoded assignment satisfies that tag's domain sentence.