The inner gates, instantiated #
The mirror of DescriptiveComplexity.Problems.Wide.DrawInstGate at the
VAL register: one gate block per quantified level of a variable's
pack, read off the round's register content instead of the mirror, its
verdict conjoined into the level's polarity flag – one of the round's
two – instead of the gates' single flag. The witness cells are the same
(gateTagCell/gateECell are register-free), the control families are
the same operations at the igateArgs pack, and the run is the same
tag_run_iter with the read registers pointed at VAL.
The flag-riding lemmas are stated at a flag constrained to the round's
two (hflag : flag = existGateC ∨ flag = allGateC), which is what makes
every disequality against the machinery's written slots decidable.
noncomputable def
DescriptiveComplexity.Draw.Data.igateTagFam
{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)
(flag : dt.CtlIx)
(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.igateFam
{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)
(flag : dt.CtlIx)
(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.igateTagFam_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}
{b : Fin dt.ko ⊕ Fin dt.ki}
{st : TapeStD dt A R P}
{flag : dt.CtlIx}
{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}
{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 (Fintype.card dt.X.Tag + 1))
:
dt.igateTagFam RF zero one b st flag hc hn hrd vAdr f₀ i = dt.igateTagFam RF zero one b st' flag hc hn hrd vAdr f₀ i
A gate's witness chain is blind to the two scratch registers: it reads the VAL register and its background at the working cell.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.igateFam_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}
{b : Fin dt.ko ⊕ Fin dt.ki}
{st : TapeStD dt A R P}
{t : dt.X.Tag}
{flag : dt.CtlIx}
{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}
{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.domNr t + 1))
:
A gate's domain loop is blind to them too.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.readLvE_igate_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}
{flag : dt.CtlIx}
{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_igate_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}
{flag : dt.CtlIx}
{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_igate_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}
{flag : dt.CtlIx}
{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_igateFam
{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}
{flag : dt.CtlIx}
{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_igateTagFam_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}
{flag : dt.CtlIx}
{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.igateTagFam RF zero one b st flag hc hn hrd vAdr f₀ (Fin.last (Fintype.card dt.X.Tag)))
(dt.gateTagC hc t') ↔ st.val (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_igateTagFam_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}
{flag : dt.CtlIx}
{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.igTagsAre_igateFam
{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}
{flag : dt.CtlIx}
{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.val (Tag.arg (toLex b))))
(dt.igateTagFam RF zero one b st flag 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 VAL enumeration produces.
Dependency graph
The domain payload at a generated state, and the leaf guards #
theorem
DescriptiveComplexity.Draw.Data.domPay_igateFam
{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}
{flag : dt.CtlIx}
{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.igateFam RF zero one b st t flag 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_igateFam
{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}
{flag : dt.CtlIx}
{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_igateFam_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}
{flag : dt.CtlIx}
{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.igateFam RF zero one b st t flag 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.igate_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}
{flag : dt.CtlIx}
{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.igateArgs PR.zero PR.one b flag hc hn hrd).rdTrackT
(dt.igateArgs PR.zero PR.one b flag hc hn hrd).MatchT (dt.igateArgs PR.zero PR.one b flag hc hn hrd).setTagFlag
(dt.igateArgs PR.zero PR.one b flag hc hn hrd).TagsAre (dt.igateArgs PR.zero PR.one b flag hc hn hrd).rdTrackE
(dt.igateArgs PR.zero PR.one b flag hc hn hrd).MatchE (dt.igateArgs PR.zero PR.one b flag hc hn hrd).setFlagE
(dt.igateArgs PR.zero PR.one b flag hc hn hrd).initEl (dt.igateArgs PR.zero PR.one b flag hc hn hrd).advEl
(dt.igateArgs PR.zero PR.one b flag hc hn hrd).exitSt (dt.igateArgs PR.zero PR.one b flag 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.val (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.igateArgs PR.zero PR.one b flag hc hn hrd).exitSt t
(dt.igateFam RF PR.zero PR.one b st t flag hc hn hrd v
(dt.igateTagFam RF PR.zero PR.one b st flag 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.igateLeafP
{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_igateFam
{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}
{flag : dt.CtlIx}
{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_igateFam
{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}
{flag : dt.CtlIx}
{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))
:
dt.domLeafVal one t ⋯ ⋯ (dt.igateFam RF zero one b st t flag hc hn hrd vAdr f₀ a (Fin.last (dt.domNr t))) ↔ dt.igateLeafP b st t ⋯ zero one (ofLex 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_igateIter
{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}
{flag : dt.CtlIx}
{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.igateArgs zero one b flag hc hn hrd).setFlagE t) ((dt.igateArgs zero one b flag hc hn hrd).initEl t)
((dt.igateArgs zero one b flag hc hn hrd).advEl t) (dt.back RF.cell zero one ⋯ st) vAdr
(fun (x : Fin (dt.domNr t)) => st.val) (dt.gateECell zero one b t ⋯) f₀ a)
j ↔ accCVal (dt.domPk t).pol (dt.igateLeafP 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_tgf_igate_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}
{flag : dt.CtlIx}
{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_igate_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}
{flag : dt.CtlIx}
{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_igateFam
{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}
{flag : dt.CtlIx}
{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_flag_igate_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}
{flag : dt.CtlIx}
{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}
(hflag : flag = dt.existGateC ∨ flag = dt.allGateC)
(q : dt.CtlIx → A)
(g : dt.SlotIx → A)
:
The gates' flag rides along one branch round.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.ctlBit_flag_igate_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}
{flag : dt.CtlIx}
{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}
(hflag : flag = dt.existGateC ∨ flag = dt.allGateC)
(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_roundFlag_igate_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}
{flag : dt.CtlIx}
{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}
(hq : q = dt.existGateC ∨ q = dt.allGateC)
(qc : dt.CtlIx → A)
(g : dt.SlotIx → A)
:
Either round flag rides along one branch round – the other polarity's included, whatever the pack's own flag.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.ctlBit_roundFlag_igate_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}
{flag : dt.CtlIx}
{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}
(hq : q = dt.existGateC ∨ q = dt.allGateC)
(qc : dt.CtlIx → A)
(g : dt.SlotIx → A)
:
Either round flag rides along a branch loop's start.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.ctlBit_roundFlag_igateFam
{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}
{flag : dt.CtlIx}
{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}
{q : dt.CtlIx}
(hq : q = dt.existGateC ∨ q = dt.allGateC)
(f₀ : dt.CtlIx → A)
(a : Lex (Fin dt.eDim → A))
(j : Fin (dt.domNr t + 1))
:
dt.ctlBit one
(dt.igateFam RF zero one b st t flag hc hn hrd vAdr
(dt.igateTagFam RF zero one b st flag hc hn hrd vAdr f₀ (Fin.last (Fintype.card dt.X.Tag))) a j)
q ↔ dt.ctlBit one f₀ q
Either round flag survives one gate's machinery – the other polarity's included: neither the witness chain nor the branch's domain loop writes any flag at all.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.ctlBit_flag_igateFam
{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}
{flag : dt.CtlIx}
{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}
(hflag : flag = dt.existGateC ∨ flag = dt.allGateC)
(f₀ : dt.CtlIx → A)
(a : Lex (Fin dt.eDim → A))
(j : Fin (dt.domNr t + 1))
:
dt.ctlBit one
(dt.igateFam RF zero one b st t flag hc hn hrd vAdr
(dt.igateTagFam RF zero one b st flag hc hn hrd vAdr f₀ (Fin.last (Fintype.card dt.X.Tag))) a j)
flag ↔ dt.ctlBit one f₀ flag
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_flag_igate_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}
{flag : dt.CtlIx}
{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}
(hflag : flag = dt.existGateC ∨ flag = dt.allGateC)
(hzo : zero ≠ one)
(f₀ : dt.CtlIx → A)
:
dt.ctlBit one
((dt.igateArgs zero one b flag hc hn hrd).exitSt t
(dt.igateFam RF zero one b st t flag hc hn hrd vAdr
(dt.igateTagFam RF zero one b st flag 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))
flag ↔ dt.ctlBit one f₀ flag ∧ (∀ (t' : dt.X.Tag), wmBlk st.val (Tag.arg (toLex b)) (encTagTup dt.ly zero one t') ↔ t' = t) ∧ foldFrom (dt.domPk t).pol (dt.igateLeafP 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_flag_igate_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}
{flag : dt.CtlIx}
{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}
(hflag : flag = dt.existGateC ∨ flag = dt.allGateC)
(hzo : zero ≠ one)
(f₀ : dt.CtlIx → A)
:
dt.ctlBit one
((dt.igateArgs zero one b flag hc hn hrd).exitSt t
(dt.igateFam RF zero one b st t flag hc hn hrd vAdr
(dt.igateTagFam RF zero one b st flag 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))
flag ↔ dt.ctlBit one f₀ flag ∧ (∀ (t' : dt.X.Tag), wmBlk st.val (Tag.arg (toLex b)) (encTagTup dt.ly zero one t') ↔ t' = t) ∧ ExpExpansion.DomHolds (t, decRho dt.ly zero one (wmBlk st.val (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.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.igVerdict_iff_isEnc
{L : FirstOrder.Language}
{dt : Data L}
{A : Type}
[LinearOrder A]
[Finite A]
[Nonempty A]
[L.Structure A]
{zero one : A}
(hzo : zero ≠ one)
{S : (Fin dt.dd → A) → Prop}
(hshape :
∀ (w : Fin dt.dd → A),
S w →
(∃ (t' : dt.X.Tag), w = encTagTup dt.ly zero one t') ∨ ∃ (i : dt.X.B.ι) (w' : Fin (dt.X.B.arity i) → A), w = encAsgTup dt.ly zero one i w')
:
The machine's per-level verdict is the gate: at a block value all of
whose members are encoding-shaped – the file test's question – the
dispatch's one-hotness together with the domain condition at the dispatched
tag is exactly DescriptiveComplexity.Draw.IsEnc.