The inner gates at an arbitrary file #
The mirror of DescriptiveComplexity.Problems.Wide.DrawIxGate 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. The registers the trips go to are the gates' own
(DescriptiveComplexity.Draw.Data.ixGateTagCell/ixGateECell), so only the
families, the guards and the run are restated here.
noncomputable def
DescriptiveComplexity.Draw.Data.ixIGateLeafP
{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)
:
An inner gate's leaf at the file, over the wide valuation: the tag's domain sentence at the decoded assignment of the block value the VAL marks' address holds.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dependency graph
noncomputable def
DescriptiveComplexity.Draw.Data.ixIGateTagFam
{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)
(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.ixIGateFam
{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)
(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.ixIGateTagFam_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]
{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}
{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' : TapeSt dt A R P I}
(h : dt.ScratchEq st st')
(hreg : ¬∃ (u : I), vAdr = F.cell u)
(f₀ : dt.CtlIx → A)
(i : Fin (Fintype.card dt.X.Tag + 1))
:
dt.ixIGateTagFam F hhas one b st flag hc hn hrd vAdr f₀ i = dt.ixIGateTagFam F hhas 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.ixIGateFam_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]
{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}
{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' : TapeSt dt A R P I}
(h : dt.ScratchEq st st')
(hreg : ¬∃ (u : I), vAdr = F.cell u)
(f₀ : dt.CtlIx → A)
(a : Lex (Fin dt.eDim → A))
(j : Fin (dt.domNr t + 1))
:
dt.ixIGateFam F hhas one b st t flag hc hn hrd vAdr f₀ a j = dt.ixIGateFam F hhas one b st' t flag hc hn hrd vAdr f₀ a j
A gate's domain loop is blind to them too.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.readLvE_ixIGateFam
{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}
{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_ixIGateTagFam_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]
{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}
{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.ixIGateTagFam F hhas one b st flag hc hn hrd vAdr f₀ (Fin.last (Fintype.card dt.X.Tag)))
(dt.gateTagC hc t') ↔ st.val (dt.ixGateTagCell F hhas 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_ixIGateTagFam_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]
{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}
{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}
{elt : I → Univ A R P dt.KIx dt.dd}
(hinj : Function.Injective elt)
(helt : ∀ (b' : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhas b' c) = dt.blkElt b' (pad zero c))
(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_ixIGateFam
{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}
{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}
{elt : I → Univ A R P dt.KIx dt.dd}
(hinj : Function.Injective elt)
(helt : ∀ (b' : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhas b' c) = dt.blkElt b' (pad zero c))
(hzo : zero ≠ one)
(f₀ : dt.CtlIx → A)
:
dt.DspTagsAre one hc (dt.dspTagOf zero one (wmBlk (ixAddr elt st.val) (Tag.arg (toLex b))))
(dt.ixIGateTagFam F hhas 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_ixIGateFam
{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}
{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.ixIGateFam F hhas 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.ixDomMatch_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]
{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}
{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)
(hix : IsLinOrd F.le)
(hsepP : F.toLayout.NameSep zero ⋯)
(f₀ : dt.CtlIx → A)
(a : Lex (Fin dt.eDim → A))
(j : Fin (dt.domNr t + 1))
(r : Fin (dt.domNr t))
:
dt.domMatch zero one b t r ⋯ (dt.ixIGateFam F hhas one b st t flag hc hn hrd vAdr f₀ a j)
(dt.ixBack F.toLayout zero one ⋯ st (F.cell (dt.ixGateECell F hhas one b t ⋯ a r)))
A domain leaf read's guard holds at its cell.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.ixDomMatch_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]
{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}
{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)
(hix : IsLinOrd F.le)
(hsepP : F.toLayout.NameSep zero ⋯)
(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.ixIGateFam F hhas one b st t flag hc hn hrd vAdr f₀ a j)
(dt.ixBack F.toLayout zero one ⋯ st y))
:
A domain leaf read's guard identifies its cell.
Dependency graph
The gate's machine run #
theorem
DescriptiveComplexity.Draw.Data.ixIGate_reachesIn
{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}
{I : Type}
{F : LaidFile dt A R P I}
[Nonempty A]
[L.IsRelational]
[L.Structure A]
{b : Fin dt.ko ⊕ Fin dt.ki}
{st : TapeSt dt A R P I}
{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}
(hhasP : F.toLayout.HasName PR.zero)
(hsepR : F.toLayout.NameSep PR.zero ⋯)
(hixR : IsLinOrd F.le)
{eltR : I → Univ A R P dt.KIx dt.dd}
(hinjR : Function.Injective eltR)
(heltR :
∀ (b' : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), eltR (F.toLayout.reg hhasP b' c) = dt.blkElt b' (pad PR.zero c))
{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 : I}
(hbot : ∀ (y : I), F.le gbot y)
{v v' : Univ A R P dt.KIx dt.dd → Prop}
(hv : WMSetLt WMLe v (F.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₀ : I → Prop}
(hm₀ :
∀ (r : Univ A R P dt.KIx dt.dd → Prop),
dt.ixBack F.toLayout PR.zero PR.one ⋯ st r t₀ = bitVal PR.zero PR.one (bitAtOf F.cell m₀ r))
(hwkt₀ : Slot.wk ≠ t₀)
(hrgt₀ : Slot.reg ≠ t₀)
(htag : dt.dspTagOf PR.zero PR.one (wmBlk (ixAddr eltR st.val) (Tag.arg (toLex b))) = t)
(f₀ : dt.CtlIx → A)
(w : ℕ)
(hcostT :
∀ (c : Fin (Fintype.card dt.X.Tag)),
2 * (wideRank (F.cell (dt.ixGateTagCell F hhasP PR.one b c)) - wideRank v) + 2 ≤ w)
(hcostE :
∀ (a : Lex (Fin dt.eDim → A)) (r : Fin (dt.domNr t)),
2 * (wideRank (F.cell (dt.ixGateECell F hhasP PR.one b t ⋯ a r)) - wideRank v) + 2 ≤ w)
:
(wideData (Univ A R P dt.KIx dt.dd)).ReachesIn
((w + 2) * Fintype.card dt.X.Tag + 2 + ((2 + (w + 2) * dt.domNr t) * (Nat.card (Lex (Fin dt.eDim → A)) + 1) + 1))
{ state := Sum.inr (PR.stElt (tagFirstRd emb) f₀), head := Sum.inl v,
tape := wideTape (PR.trackTapeAt F.cell t₀ (dt.ixBack F.toLayout 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.ixIGateFam F hhasP PR.one b st t flag hc hn hrd v
(dt.ixIGateTagFam F hhasP 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.ixBack F.toLayout PR.zero PR.one ⋯ st v))),
head := Sum.inl v',
tape := wideTape (PR.trackTapeAt F.cell t₀ (dt.ixBack F.toLayout 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 #
theorem
DescriptiveComplexity.Draw.Data.ctlBit_rdf_ixIGateFam
{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}
{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))
:
dt.ctlBit one (dt.ixIGateFam F hhas one b st t flag hc hn hrd vAdr f₀ a (Fin.last (dt.domNr t)))
(dt.rdfC (Fin.castLE ⋯ r)) ↔ st.val (dt.ixGateECell F hhas one b t ⋯ a r)
The domain leaf-read flags read back at a round's end.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.domLeafVal_ixIGateFam
{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}
{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}
{elt : I → Univ A R P dt.KIx dt.dd}
(hinj : Function.Injective elt)
(helt : ∀ (b' : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhas b' c) = dt.blkElt b' (pad zero c))
(hzo : zero ≠ one)
(f₀ : dt.CtlIx → A)
(a : Lex (Fin dt.eDim → A))
:
dt.domLeafVal one t ⋯ ⋯ (dt.ixIGateFam F hhas one b st t flag hc hn hrd vAdr f₀ a (Fin.last (dt.domNr t))) ↔ dt.ixIGateLeafP 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_ixIGateIter
{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}
{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}
{elt : I → Univ A R P dt.KIx dt.dd}
(hinj : Function.Injective elt)
(helt : ∀ (b' : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhas b' c) = dt.blkElt b' (pad zero c))
(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.ixBack F.toLayout zero one ⋯ st) vAdr
(fun (x : Fin (dt.domNr t)) => st.val) (dt.ixGateECell F hhas one b t ⋯) f₀ a)
j ↔ accCVal (dt.domPk t).pol (dt.ixIGateLeafP 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_ixIGateFam
{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}
{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_roundFlag_ixIGateFam
{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}
{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.ixIGateFam F hhas one b st t flag hc hn hrd vAdr
(dt.ixIGateTagFam F hhas 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_ixIGateFam
{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}
{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.ixIGateFam F hhas one b st t flag hc hn hrd vAdr
(dt.ixIGateTagFam F hhas 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_ixIGate_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]
{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}
{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}
{elt : I → Univ A R P dt.KIx dt.dd}
(hinj : Function.Injective elt)
(helt : ∀ (b' : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhas b' c) = dt.blkElt b' (pad zero c))
(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.ixIGateFam F hhas one b st t flag hc hn hrd vAdr
(dt.ixIGateTagFam F hhas one b st flag hc hn hrd vAdr f₀ (Fin.last (Fintype.card dt.X.Tag))) (toLex topTup)
(Fin.last (dt.domNr t)))
(dt.ixBack F.toLayout zero one ⋯ st vAdr))
flag ↔ dt.ctlBit one f₀ flag ∧ (∀ (t' : dt.X.Tag), wmBlk (ixAddr elt st.val) (Tag.arg (toLex b)) (encTagTup dt.ly zero one t') ↔ t' = t) ∧ foldFrom (dt.domPk t).pol (dt.ixIGateLeafP 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_ixIGate_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]
{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}
{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}
{elt : I → Univ A R P dt.KIx dt.dd}
(hinj : Function.Injective elt)
(helt : ∀ (b' : Fin dt.ko ⊕ Fin dt.ki) (c : Fin dt.dd0 → A), elt (F.toLayout.reg hhas b' c) = dt.blkElt b' (pad zero c))
(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.ixIGateFam F hhas one b st t flag hc hn hrd vAdr
(dt.ixIGateTagFam F hhas one b st flag hc hn hrd vAdr f₀ (Fin.last (Fintype.card dt.X.Tag))) (toLex topTup)
(Fin.last (dt.domNr t)))
(dt.ixBack F.toLayout zero one ⋯ st vAdr))
flag ↔ dt.ctlBit one f₀ flag ∧ (∀ (t' : dt.X.Tag), wmBlk (ixAddr elt st.val) (Tag.arg (toLex b)) (encTagTup dt.ly zero one t') ↔ t' = t) ∧ ExpExpansion.DomHolds (t, decRho dt.ly zero one (wmBlk (ixAddr elt 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.