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.

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.

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)

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)

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.

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.

The witness chain's read-back and the branch dispatch

The leaf guards, at the generated states

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.

The sub-fold: the sac invariant and the exit verdict