The expansion atoms at an arbitrary file #
An expansion atom reads a witness cell per position and tag, dispatches on the
decoded tags, and runs the branch's wide element loop, one leaf trip per block
atom. Every one of those trips goes to the cell of an encoded tuple
(DescriptiveComplexity.Draw.encTup) in an argument block. At the elementwise
file that cell is an element of the universe
(DescriptiveComplexity.Draw.Data.expTagCell/expECell); at a coarser one it
is a register, the one the layout names by the tuple's coordinates
(DescriptiveComplexity.Draw.Data.ixEncG_iff), and the encoding's canonical
padding is what makes the two the same cell
(DescriptiveComplexity.Draw.Data.elt_reg_encCoord).
This file is that reading: the named registers, the generated families over
them, the guards' arrival and uniqueness, and the atom's run
(DescriptiveComplexity.Draw.Data.ixExp_reachesIn). As in
DescriptiveComplexity.Draw.Data.ixStageAtom_reachesIn the file is carried by
one coherence hypothesis – the element a register holds the bit of is the
element its name spells – and everything the semantics says of an elementwise
run then says of this one.
The registers an expansion atom's trips go to #
noncomputable def
DescriptiveComplexity.Draw.Data.ixExpTagCell
{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)
(vi : dt.VarIx)
{k : ℕ}
(ts : Fin k → Fin (dt.nOf vi))
(i : Fin (k * Fintype.card dt.X.Tag))
:
I
The register of the i-th witness read: the one the layout names by
the tag's witness tuple in the copy's block.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dependency graph
noncomputable def
DescriptiveComplexity.Draw.Data.ixExpECell
{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)
(vi : dt.VarIx)
{k : ℕ}
(ts : Fin k → Fin (dt.nOf vi))
(e : dt.X.E.Relations k)
(τ : Fin k → dt.X.Tag)
(hnτ : (dt.relPk e τ).n ≤ dt.eDim)
(a : Lex (Fin dt.eDim → A))
(r : Fin (dt.relNr e τ))
:
I
The register of the r-th 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_ixExpTagCell
{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)
(vi : dt.VarIx)
{k : ℕ}
(ts : Fin k → Fin (dt.nOf vi))
{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))
(i : Fin (k * Fintype.card dt.X.Tag))
:
The witness register holds the witness cell: its address is the cell an elementwise atom reads.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.elt_ixExpECell
{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)
(vi : dt.VarIx)
{k : ℕ}
(ts : Fin k → Fin (dt.nOf vi))
(e : dt.X.E.Relations k)
(τ : Fin k → dt.X.Tag)
(hnτ : (dt.relPk e τ).n ≤ dt.eDim)
{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))
(a : Lex (Fin dt.eDim → A))
(r : Fin (dt.relNr e τ))
:
The leaf register holds the leaf cell.
Dependency graph
The generated families, over the file's registers #
noncomputable def
DescriptiveComplexity.Draw.Data.ixExpTagSet
{L : FirstOrder.Language}
(dt : Data L)
{A R P I : Type}
(vi : dt.VarIx)
{k : ℕ}
(ts : Fin k → Fin (dt.nOf vi))
(st : TapeSt dt A R P I)
(i : Fin (k * Fintype.card dt.X.Tag))
:
I → Prop
The register behind the i-th witness read, at the file: the copy's
level's register set.
Equations
- dt.ixExpTagSet vi ts st i = dt.lvSet st vi (ts (dt.wIx i).1)
Instances For
Dependency graph
noncomputable def
DescriptiveComplexity.Draw.Data.ixExpESet
{L : FirstOrder.Language}
(dt : Data L)
{A R P I : Type}
[L.IsRelational]
(vi : dt.VarIx)
{k : ℕ}
(ts : Fin k → Fin (dt.nOf vi))
(e : dt.X.E.Relations k)
(st : TapeSt dt A R P I)
(τ : Fin k → dt.X.Tag)
(r : Fin (dt.relNr e τ))
:
I → Prop
The register behind the r-th leaf read of branch τ, at the file.
Equations
- dt.ixExpESet vi ts e st τ r = dt.lvSet st vi (ts (DescriptiveComplexity.Draw.Data.relLeafData e τ r).fst.1)
Instances For
Dependency graph
noncomputable def
DescriptiveComplexity.Draw.Data.ixExpFam
{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)
(vi : dt.VarIx)
{k : ℕ}
(ts : Fin k → Fin (dt.nOf vi))
(e : dt.X.E.Relations k)
(av : Fin dt.natMax)
(st : TapeSt dt A R P I)
(τ : Fin k → dt.X.Tag)
(hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim)
(hn : ∀ (τ' : Fin k → dt.X.Tag), (dt.relPk e τ').n ≤ dt.eDim)
(hrd : ∀ (τ' : Fin k → dt.X.Tag), dt.relNr e τ' ≤ 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.relNr e τ + 1))
:
dt.CtlIx → A
The generated family of branch τ's element loop, at the file.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dependency graph
noncomputable def
DescriptiveComplexity.Draw.Data.ixExpTagFam
{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)
(vi : dt.VarIx)
{k : ℕ}
(ts : Fin k → Fin (dt.nOf vi))
(e : dt.X.E.Relations k)
(av : Fin dt.natMax)
(st : TapeSt dt A R P I)
(hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim)
(hn : ∀ (τ' : Fin k → dt.X.Tag), (dt.relPk e τ').n ≤ dt.eDim)
(hrd : ∀ (τ' : Fin k → dt.X.Tag), dt.relNr e τ' ≤ dt.nfDim)
(vAdr : Univ A R P dt.KIx dt.dd → Prop)
(f₀ : dt.CtlIx → A)
(i : Fin (k * Fintype.card dt.X.Tag + 1))
:
dt.CtlIx → A
The generated witness chain of an expansion atom, at the file.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.readLvE_ixExpFam
{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}
{vi : dt.VarIx}
{k : ℕ}
{ts : Fin k → Fin (dt.nOf vi)}
{e : dt.X.E.Relations k}
{av : Fin dt.natMax}
{st : TapeSt dt A R P I}
{τ : Fin k → dt.X.Tag}
{hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim}
{hn : ∀ (τ' : Fin k → dt.X.Tag), (dt.relPk e τ').n ≤ dt.eDim}
{hrd : ∀ (τ' : Fin k → dt.X.Tag), dt.relNr e τ' ≤ 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.relNr e τ + 1))
:
The loop element is the round's wide tuple, at every stage of the family: the same reading as at the elementwise file, the reads now going to the registers the layout names.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.ixExpFam_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}
{vi : dt.VarIx}
{k : ℕ}
{ts : Fin k → Fin (dt.nOf vi)}
{e : dt.X.E.Relations k}
{av : Fin dt.natMax}
{st : TapeSt dt A R P I}
{τ : Fin k → dt.X.Tag}
{hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim}
{hn : ∀ (τ' : Fin k → dt.X.Tag), (dt.relPk e τ').n ≤ dt.eDim}
{hrd : ∀ (τ' : Fin k → dt.X.Tag), dt.relNr e τ' ≤ 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.relNr e τ + 1))
:
An expansion atom's element loop is blind to the two scratch registers, at an arbitrary file: it reads the levels' register sets – the mirror and VAL – and its background at the working cell alone.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.ixExpTagFam_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}
{vi : dt.VarIx}
{k : ℕ}
{ts : Fin k → Fin (dt.nOf vi)}
{e : dt.X.E.Relations k}
{av : Fin dt.natMax}
{st : TapeSt dt A R P I}
{hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim}
{hn : ∀ (τ' : Fin k → dt.X.Tag), (dt.relPk e τ').n ≤ dt.eDim}
{hrd : ∀ (τ' : Fin k → dt.X.Tag), dt.relNr e τ' ≤ 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 (k * Fintype.card dt.X.Tag + 1))
:
dt.ixExpTagFam F hhas one vi ts e av st hk hn hrd vAdr f₀ i = dt.ixExpTagFam F hhas one vi ts e av st' hk hn hrd vAdr f₀ i
The witness chain is blind to the two scratch registers too.
Dependency graph
The witness chain's read-back and the branch dispatch #
theorem
DescriptiveComplexity.Draw.Data.ctlBit_ixExpTagFam_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}
{vi : dt.VarIx}
{k : ℕ}
{ts : Fin k → Fin (dt.nOf vi)}
{e : dt.X.E.Relations k}
{av : Fin dt.natMax}
{st : TapeSt dt A R P I}
{hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim}
{hn : ∀ (τ' : Fin k → dt.X.Tag), (dt.relPk e τ').n ≤ dt.eDim}
{hrd : ∀ (τ' : Fin k → dt.X.Tag), dt.relNr e τ' ≤ dt.nfDim}
{vAdr : Univ A R P dt.KIx dt.dd → Prop}
(hzo : zero ≠ one)
(f₀ : dt.CtlIx → A)
(ℓ : Fin k)
(t : dt.X.Tag)
:
dt.ctlBit one (dt.ixExpTagFam F hhas one vi ts e av st hk hn hrd vAdr f₀ (Fin.last (k * Fintype.card dt.X.Tag)))
(dt.tagIx hk ℓ t) ↔ dt.ixExpTagSet vi ts st (tagIxOf ℓ t) (dt.ixExpTagCell F hhas one vi ts (tagIxOf ℓ t))
The witness flags read back: after the chain, the flag of position ℓ
and tag t holds the digit of the register the witness cell of (ℓ, t) is.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.tagsAre_ixExpTagFam
{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]
[Finite R]
[Finite P]
{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}
{vi : dt.VarIx}
{k : ℕ}
{ts : Fin k → Fin (dt.nOf vi)}
{e : dt.X.E.Relations k}
{av : Fin dt.natMax}
{st : TapeSt dt A R P I}
{hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim}
{hn : ∀ (τ' : Fin k → dt.X.Tag), (dt.relPk e τ').n ≤ dt.eDim}
{hrd : ∀ (τ' : Fin k → dt.X.Tag), dt.relNr e τ' ≤ dt.nfDim}
{vAdr : Univ A R P dt.KIx dt.dd → Prop}
{elt : I → Univ A R P dt.KIx dt.dd}
(hzo : zero ≠ one)
(hlin : IsLinOrd WMLe)
(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))
(pts : Fin k → dt.X.Map A)
(hENC :
∀ (ℓ : Fin k),
wmBlk (ixAddr elt (dt.lvSet st vi (ts ℓ))) (Tag.arg (toLex (dt.lvBlk vi (ts ℓ)))) = encMap dt.ly zero one (pts ℓ))
(f₀ : dt.CtlIx → A)
:
(dt.expArgs zero one vi ts e av hk hn hrd).TagsAre (fun (ℓ : Fin k) => (↑(pts ℓ)).1)
(dt.ixExpTagFam F hhas one vi ts e av st hk hn hrd vAdr f₀ (Fin.last (k * Fintype.card dt.X.Tag)))
The chain decodes the argument points' tags, at the file: if the addresses the levels' registers stand for hold the encodings of the points, the flags are one-hot at the points' tag tuple, which is the branch dispatch's guard.
Dependency graph
The leaf guards, at the generated states #
theorem
DescriptiveComplexity.Draw.Data.expPay_ixExpFam
{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}
{vi : dt.VarIx}
{k : ℕ}
{ts : Fin k → Fin (dt.nOf vi)}
{e : dt.X.E.Relations k}
{av : Fin dt.natMax}
{st : TapeSt dt A R P I}
{τ : Fin k → dt.X.Tag}
{hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim}
{hn : ∀ (τ' : Fin k → dt.X.Tag), (dt.relPk e τ').n ≤ dt.eDim}
{hrd : ∀ (τ' : Fin k → dt.X.Tag), dt.relNr e τ' ≤ 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.relNr e τ + 1))
(r : Fin (dt.relNr e τ))
:
The payload a leaf read spells at a generated state is the round's tuple's, so the guard's computed coordinates name the round's register.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.ixExpMatch_ixExpFam
{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}
{vi : dt.VarIx}
{k : ℕ}
{ts : Fin k → Fin (dt.nOf vi)}
{e : dt.X.E.Relations k}
{av : Fin dt.natMax}
{st : TapeSt dt A R P I}
{τ : Fin k → dt.X.Tag}
{hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim}
{hn : ∀ (τ' : Fin k → dt.X.Tag), (dt.relPk e τ').n ≤ dt.eDim}
{hrd : ∀ (τ' : Fin k → dt.X.Tag), dt.relNr e τ' ≤ dt.nfDim}
{vAdr : Univ A R P dt.KIx dt.dd → Prop}
(hzo : zero ≠ one)
(hix : IsLinOrd F.le)
(hsep : F.toLayout.NameSep zero ⋯)
(f₀ : dt.CtlIx → A)
(a : Lex (Fin dt.eDim → A))
(j : Fin (dt.relNr e τ + 1))
(r : Fin (dt.relNr e τ))
:
A leaf read's guard holds at its register: the computed coordinates are the round's payload, so the trip stops at the register the layout names by the member tuple.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.ixExpMatch_ixExpFam_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}
{vi : dt.VarIx}
{k : ℕ}
{ts : Fin k → Fin (dt.nOf vi)}
{e : dt.X.E.Relations k}
{av : Fin dt.natMax}
{st : TapeSt dt A R P I}
{τ : Fin k → dt.X.Tag}
{hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim}
{hn : ∀ (τ' : Fin k → dt.X.Tag), (dt.relPk e τ').n ≤ dt.eDim}
{hrd : ∀ (τ' : Fin k → dt.X.Tag), dt.relNr e τ' ≤ dt.nfDim}
{vAdr : Univ A R P dt.KIx dt.dd → Prop}
(hzo : zero ≠ one)
(hix : IsLinOrd F.le)
(hsep : F.toLayout.NameSep zero ⋯)
(f₀ : dt.CtlIx → A)
(a : Lex (Fin dt.eDim → A))
(j : Fin (dt.relNr e τ + 1))
(r : Fin (dt.relNr e τ))
{y : Univ A R P dt.KIx dt.dd → Prop}
(hM :
dt.expMatch zero one vi ts e τ r ⋯ (dt.ixExpFam F hhas one vi ts e av st τ hk hn hrd vAdr f₀ a j)
(dt.ixBack F.toLayout zero one ⋯ st y))
:
A leaf read's guard identifies its register.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.ixExpESet_ixExpECell_iff
{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]
[Finite R]
[Finite P]
{I : Type}
{F : LaidFile dt A R P I}
[L.IsRelational]
[L.Structure A]
{zero : A}
{hhas : F.toLayout.HasName zero}
{one : A}
{vi : dt.VarIx}
{k : ℕ}
{ts : Fin k → Fin (dt.nOf vi)}
{e : dt.X.E.Relations k}
{st : TapeSt dt A R P I}
{τ : Fin k → dt.X.Tag}
{hn : ∀ (τ' : Fin k → dt.X.Tag), (dt.relPk e τ').n ≤ dt.eDim}
{elt : I → Univ A R P dt.KIx dt.dd}
(hzo : zero ≠ one)
(hlin : IsLinOrd WMLe)
(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))
(pts : Fin k → dt.X.Map A)
(hENC :
∀ (ℓ : Fin k),
wmBlk (ixAddr elt (dt.lvSet st vi (ts ℓ))) (Tag.arg (toLex (dt.lvBlk vi (ts ℓ)))) = encMap dt.ly zero one (pts ℓ))
(a : Lex (Fin dt.eDim → A))
(r : Fin (dt.relNr e τ))
{f : dt.CtlIx → A}
(hf : dt.readLvE f = ofLex a)
:
dt.ixExpESet vi ts e st τ r (dt.ixExpECell F hhas one vi ts e τ ⋯ a r) ↔ BlkAtom.holds (dt.X.B.replicateAssign fun (ℓ : Fin k) => (↑(pts ℓ)).2)
(fun (j : Fin (dt.relPk e τ).n) => f (dt.lvE (Fin.castLE ⋯ j)))
(BlkAtom.blkA (relLeafData e τ r).fst (relLeafData e τ r).snd)
What a leaf trip's digit means, at the file: at a round's register, the bit is the block atom's value at the points the addresses encode, read at the valuation the round's tuple spells.
Dependency graph
The expansion atom's machine run #
theorem
DescriptiveComplexity.Draw.Data.ixExp_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]
(hhasP : F.toLayout.HasName PR.zero)
(hsepP : F.toLayout.NameSep PR.zero ⋯)
(hix : IsLinOrd F.le)
(vi : dt.VarIx)
{k : ℕ}
(ts : Fin k → Fin (dt.nOf vi))
(e : dt.X.E.Relations k)
(av : Fin dt.natMax)
(st : TapeSt dt A R P I)
(hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim)
(hn : ∀ (τ' : Fin k → dt.X.Tag), (dt.relPk e τ').n ≤ dt.eDim)
(hrd : ∀ (τ' : Fin k → dt.X.Tag), dt.relNr e τ' ≤ dt.nfDim)
{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 hhasP b c) = dt.blkElt b (pad PR.zero c))
{emb : TagPh (k * Fintype.card dt.X.Tag) (Fin k → dt.X.Tag) (dt.relNr e) → P}
{exitPh : P}
{rEmb :
(i : TagSite (k * Fintype.card dt.X.Tag) (Fin k → dt.X.Tag) (dt.relNr e)) →
TagSh (k * Fintype.card dt.X.Tag) (Fin k → dt.X.Tag) (dt.relNr e) i → R}
[Finite dt.KIx]
(hrules :
∀ (i : TagSite (k * Fintype.card dt.X.Tag) (Fin k → dt.X.Tag) (dt.relNr e))
(ρ : TagSh (k * Fintype.card dt.X.Tag) (Fin k → dt.X.Tag) (dt.relNr e) i),
PR.rules (rEmb i ρ) = tagRule PR.one Slot.wk Slot.reg emb (dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).rdTrackT
(dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).MatchT
(dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).setTagFlag
(dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).TagsAre
(dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).rdTrackE
(dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).MatchE
(dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).setFlagE
(dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).initEl (dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).advEl
(dt.expArgs PR.zero PR.one vi ts e av hk hn hrd).exitSt (dt.expArgs PR.zero PR.one vi ts e av hk 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₀)
(pts : Fin k → dt.X.Map A)
(hENC :
∀ (ℓ : Fin k),
wmBlk (ixAddr elt (dt.lvSet st vi (ts ℓ))) (Tag.arg (toLex (dt.lvBlk vi (ts ℓ)))) = encMap dt.ly PR.zero PR.one (pts ℓ))
(f₀ : dt.CtlIx → A)
(w : ℕ)
(hcostT :
∀ (i : Fin (k * Fintype.card dt.X.Tag)),
2 * (wideRank (F.cell (dt.ixExpTagCell F hhasP PR.one vi ts i)) - wideRank v) + 2 ≤ w)
(hcostE :
∀ (a : Lex (Fin dt.eDim → A)) (r : Fin (dt.relNr e fun (ℓ : Fin k) => (↑(pts ℓ)).1)),
2 * (wideRank (F.cell (dt.ixExpECell F hhasP PR.one vi ts e (fun (ℓ : Fin k) => (↑(pts ℓ)).1) ⋯ a r)) - wideRank v) + 2 ≤ w)
:
(wideData (Univ A R P dt.KIx dt.dd)).ReachesIn
((w + 2) * (k * Fintype.card dt.X.Tag) + 2 + ((2 + (w + 2) * dt.relNr e fun (ℓ : Fin k) => (↑(pts ℓ)).1) * (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.expArgs PR.zero PR.one vi ts e av hk hn hrd).exitSt (fun (ℓ : Fin k) => (↑(pts ℓ)).1)
(dt.ixExpFam F hhasP PR.one vi ts e av st (fun (ℓ : Fin k) => (↑(pts ℓ)).1) hk hn hrd v
(dt.ixExpTagFam F hhasP PR.one vi ts e av st hk hn hrd v f₀ (Fin.last (k * Fintype.card dt.X.Tag)))
(toLex topTup) (Fin.last (dt.relNr e fun (ℓ : Fin k) => (↑(pts ℓ)).1)))
(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 expansion atom's machine run at an arbitrary file, on a clock: from the machinery's first phase at the marker – the witness chain decoding the argument points' tags, the dispatch onto their branch, and that branch's wide element loop, one leaf trip per block atom – to the exit phase one cell to the marker's right. Every trip goes to a register the layout names, and the cost is the chain's reads and the branch's whole loop.
Dependency graph
The sub-fold: the sac invariant and the exit verdict #
noncomputable def
DescriptiveComplexity.Draw.Data.ixExpLeafP
{L : FirstOrder.Language}
(dt : Data L)
{A : Type}
[LinearOrder A]
[L.IsRelational]
[L.Structure A]
{k : ℕ}
(e : dt.X.E.Relations k)
(τ : Fin k → dt.X.Tag)
(hnτ : (dt.relPk e τ).n ≤ dt.eDim)
(pts : Fin k → dt.X.Map A)
(v : Fin dt.eDim → A)
:
The branch's leaf, over the wide valuation: the defining sentence's
matrix at the points' assignments, its levels read off the first n
coordinates of the wide tuple.
Equations
- dt.ixExpLeafP e τ hnτ pts v = dt.expLeaf e τ (fun (ℓ : Fin k) => (↑(pts ℓ)).2) fun (j : Fin (dt.relPk e τ).n) => v (Fin.castLE hnτ j)
Instances For
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.ctlBit_rdf_ixExpFam
{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)
(vi : dt.VarIx)
{k : ℕ}
(ts : Fin k → Fin (dt.nOf vi))
(e : dt.X.E.Relations k)
(av : Fin dt.natMax)
(st : TapeSt dt A R P I)
(τ : Fin k → dt.X.Tag)
(hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim)
(hn : ∀ (τ' : Fin k → dt.X.Tag), (dt.relPk e τ').n ≤ dt.eDim)
(hrd : ∀ (τ' : Fin k → dt.X.Tag), dt.relNr e τ' ≤ 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.relNr e τ))
:
dt.ctlBit one (dt.ixExpFam F hhas one vi ts e av st τ hk hn hrd vAdr f₀ a (Fin.last (dt.relNr e τ)))
(dt.rdfC (Fin.castLE ⋯ r)) ↔ dt.ixExpESet vi ts e st τ r (dt.ixExpECell F hhas one vi ts e τ ⋯ a r)
The leaf-read flags read back: at a round's end, the flag of the
r-th block atom holds the digit of the round's cell.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.expLeafVal_ixExpFam
{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]
[Finite R]
[Finite P]
{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)
(vi : dt.VarIx)
{k : ℕ}
(ts : Fin k → Fin (dt.nOf vi))
(e : dt.X.E.Relations k)
(av : Fin dt.natMax)
(st : TapeSt dt A R P I)
(τ : Fin k → dt.X.Tag)
(hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim)
(hn : ∀ (τ' : Fin k → dt.X.Tag), (dt.relPk e τ').n ≤ dt.eDim)
(hrd : ∀ (τ' : Fin k → dt.X.Tag), dt.relNr e τ' ≤ 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)
(hlin : IsLinOrd WMLe)
(pts : Fin k → dt.X.Map A)
(hENC :
∀ (ℓ : Fin k),
wmBlk (ixAddr elt (dt.lvSet st vi (ts ℓ))) (Tag.arg (toLex (dt.lvBlk vi (ts ℓ)))) = encMap dt.ly zero one (pts ℓ))
(f₀ : dt.CtlIx → A)
(a : Lex (Fin dt.eDim → A))
:
dt.expLeafVal one e τ ⋯ ⋯ (dt.ixExpFam F hhas one vi ts e av st τ hk hn hrd vAdr f₀ a (Fin.last (dt.relNr e τ))) ↔ dt.ixExpLeafP e τ ⋯ pts (ofLex a)
The leaf flag's value at a round's end is the branch's leaf: with the flags holding the block atoms' bits and the loop element the round's tuple, the Boolean function the control computes is the leaf predicate at that tuple.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.readSac_ixExpIter
{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]
[Finite R]
[Finite P]
{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)
(vi : dt.VarIx)
{k : ℕ}
(ts : Fin k → Fin (dt.nOf vi))
(e : dt.X.E.Relations k)
(av : Fin dt.natMax)
(st : TapeSt dt A R P I)
(τ : Fin k → dt.X.Tag)
(hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim)
(hn : ∀ (τ' : Fin k → dt.X.Tag), (dt.relPk e τ').n ≤ dt.eDim)
(hrd : ∀ (τ' : Fin k → dt.X.Tag), dt.relNr e τ' ≤ 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)
(hlin : IsLinOrd WMLe)
(pts : Fin k → dt.X.Map A)
(hENC :
∀ (ℓ : Fin k),
wmBlk (ixAddr elt (dt.lvSet st vi (ts ℓ))) (Tag.arg (toLex (dt.lvBlk vi (ts ℓ)))) = encMap dt.ly zero one (pts ℓ))
(f₀ : dt.CtlIx → A)
(a : Lex (Fin dt.eDim → A))
(j : ℕ)
(hj : j < dt.eDim)
:
dt.readSac one
(elemIter ((dt.expArgs zero one vi ts e av hk hn hrd).setFlagE τ)
((dt.expArgs zero one vi ts e av hk hn hrd).initEl τ) ((dt.expArgs zero one vi ts e av hk hn hrd).advEl τ)
(dt.ixBack F.toLayout zero one ⋯ st) vAdr (dt.ixExpESet vi ts e st τ) (dt.ixExpECell F hhas one vi ts e τ ⋯) f₀ a)
j ↔ accCVal (dt.relPk e τ).pol (dt.ixExpLeafP e τ ⋯ pts) (fun (x1 x2 : A) => x1 ≤ x2) j (ofLex a)
The sub-fold's accumulators fold the strict prefix: at every round's
entry, the sac slots hold the completed-subtree contributions of the
branch's prefix at the round's tuple.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.ctlBit_avC_ixExp_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]
[Finite R]
[Finite P]
{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)
(vi : dt.VarIx)
{k : ℕ}
(ts : Fin k → Fin (dt.nOf vi))
(e : dt.X.E.Relations k)
(av : Fin dt.natMax)
(st : TapeSt dt A R P I)
(τ : Fin k → dt.X.Tag)
(hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim)
(hn : ∀ (τ' : Fin k → dt.X.Tag), (dt.relPk e τ').n ≤ dt.eDim)
(hrd : ∀ (τ' : Fin k → dt.X.Tag), dt.relNr e τ' ≤ 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)
(hlin : IsLinOrd WMLe)
(pts : Fin k → dt.X.Map A)
(hENC :
∀ (ℓ : Fin k),
wmBlk (ixAddr elt (dt.lvSet st vi (ts ℓ))) (Tag.arg (toLex (dt.lvBlk vi (ts ℓ)))) = encMap dt.ly zero one (pts ℓ))
(f₀ : dt.CtlIx → A)
:
dt.ctlBit one
((dt.expArgs zero one vi ts e av hk hn hrd).exitSt τ
(dt.ixExpFam F hhas one vi ts e av st τ hk hn hrd vAdr f₀ (toLex topTup) (Fin.last (dt.relNr e τ)))
(dt.ixBack F.toLayout zero one ⋯ st vAdr))
(dt.avC av) ↔ foldFrom (dt.relPk e τ).pol (dt.ixExpLeafP e τ ⋯ pts) (fun (x1 x2 : A) => x1 ≤ x2) 0 topTup
The verdict the exit control carries: the atom's slot holds the fold
of the branch's whole prefix at the points' assignments – the value
DescriptiveComplexity.Draw.Data.expLeaf's prefix takes over every wide
tuple, which DescriptiveComplexity.Problems.Wide.DrawExp reads as the
expansion atom's truth.
Dependency graph
theorem
DescriptiveComplexity.Draw.Data.ctlBit_avC_ixExp_relMap
{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]
[Finite R]
[Finite P]
{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)
(vi : dt.VarIx)
{k : ℕ}
(ts : Fin k → Fin (dt.nOf vi))
(e : dt.X.E.Relations k)
(av : Fin dt.natMax)
(st : TapeSt dt A R P I)
(hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim)
(hn : ∀ (τ' : Fin k → dt.X.Tag), (dt.relPk e τ').n ≤ dt.eDim)
(hrd : ∀ (τ' : Fin k → dt.X.Tag), dt.relNr e τ' ≤ 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)
(hlin : IsLinOrd WMLe)
(pts : Fin k → dt.X.Map A)
(hENC :
∀ (ℓ : Fin k),
wmBlk (ixAddr elt (dt.lvSet st vi (ts ℓ))) (Tag.arg (toLex (dt.lvBlk vi (ts ℓ)))) = encMap dt.ly zero one (pts ℓ))
(f₀ : dt.CtlIx → A)
:
dt.ctlBit one
((dt.expArgs zero one vi ts e av hk hn hrd).exitSt (fun (ℓ : Fin k) => (↑(pts ℓ)).1)
(dt.ixExpFam F hhas one vi ts e av st (fun (ℓ : Fin k) => (↑(pts ℓ)).1) hk hn hrd vAdr f₀ (toLex topTup)
(Fin.last (dt.relNr e fun (ℓ : Fin k) => (↑(pts ℓ)).1)))
(dt.ixBack F.toLayout zero one ⋯ st vAdr))
(dt.avC av) ↔ FirstOrder.Language.Structure.RelMap e pts
The expansion atom's verdict is its truth: at the argument points
the registers encode, the bit the exit control files in the atom's slot is
RelMap of the expansion – the machine has evaluated the defining
sentence.