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.
Instances For
Dependency graph
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.
Instances For
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.elt_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)
{elt : I → Univ A R P dt.KIx dt.dd}
(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))
(c : Fin (Fintype.card dt.X.Tag))
:
The witness register holds the witness cell.
Dependency graph
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.
Instances For
Dependency graph
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.
Instances For
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.readLvE_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))
:
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_ixGateTagFam_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}
{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.ixGateTagFam F hhas one b st hc hn hrd vAdr f₀ (Fin.last (Fintype.card dt.X.Tag)))
(dt.gateTagC hc t') ↔ st.mir (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_ixGateTagFam_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}
{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))
{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.ixDspTagsAre_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]
{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}
{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))
{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 (ixAddr elt st.mir) (Tag.arg (toLex b))))
(dt.ixGateTagFam F hhas 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_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))
(r : Fin (dt.domNr t))
:
dt.domPay zero t r ⋯ (dt.ixGateFam F hhas 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.ixDomMatch_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]
{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}
(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))
:
A domain leaf read's guard holds at its cell.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.ixDomMatch_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]
{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}
(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.ixGateFam F hhas one b st t 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
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)
:
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.
Instances For
Dependency graph
The gate's machine run #
theorem
DescriptiveComplexity.Draw.Data.ixGate_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}
{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.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 : 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.mir) (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.gateArgs PR.zero PR.one b hc hn hrd).exitSt t
(dt.ixGateFam F hhasP PR.one b st t hc hn hrd v
(dt.ixGateTagFam F hhasP PR.one b st 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_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}
(hzo : zero ≠ one)
(f₀ : dt.CtlIx → A)
(a : Lex (Fin dt.eDim → A))
(r : Fin (dt.domNr t))
:
dt.ctlBit one (dt.ixGateFam F hhas one b st t hc hn hrd vAdr f₀ a (Fin.last (dt.domNr t))) (dt.rdfC (Fin.castLE ⋯ r)) ↔ st.mir (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_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}
{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))
{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.ixGateFam F hhas one b st t hc hn hrd vAdr f₀ a (Fin.last (dt.domNr t))) ↔ dt.ixGateLeafP 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_ixGateIter
{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}
{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))
{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.ixBack F.toLayout zero one ⋯ st) vAdr
(fun (x : Fin (dt.domNr t)) => st.mir) (dt.ixGateECell F hhas one b t ⋯) f₀ a)
j ↔ accCVal (dt.domPk t).pol (dt.ixGateLeafP 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_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}
(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_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))
:
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_ixGate_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}
{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))
{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.ixGateFam F hhas one b st t hc hn hrd vAdr
(dt.ixGateTagFam F hhas one b st 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))
dt.gateFlagC ↔ dt.ctlBit one f₀ dt.gateFlagC ∧ (∀ (t' : dt.X.Tag), wmBlk (ixAddr elt st.mir) (Tag.arg (toLex b)) (encTagTup dt.ly zero one t') ↔ t' = t) ∧ foldFrom (dt.domPk t).pol (dt.ixGateLeafP 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_ixGate_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}
{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))
{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.ixGateFam F hhas one b st t hc hn hrd vAdr
(dt.ixGateTagFam F hhas one b st 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))
dt.gateFlagC ↔ dt.ctlBit one f₀ dt.gateFlagC ∧ (∀ (t' : dt.X.Tag), wmBlk (ixAddr elt st.mir) (Tag.arg (toLex b)) (encTagTup dt.ly zero one t') ↔ t' = t) ∧ ExpExpansion.DomHolds (t, decRho dt.ly zero one (wmBlk (ixAddr elt 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.