The semantic parameters, filled in: the comparison atoms

The rule shapes of the program were closed before a single semantic choice was made, the content riding in parameter packs (DescriptiveComplexity.Draw.StageArgs and friends). This file begins filling them, at the kind whose loop is simplest: a comparison – an equality or an order atom between two levels of the prefix.

What the machine does there, and what the packs say (the anchor is DescriptiveComplexity.Problems.Wide.DrawCmp): walk the canonically padded cells of the two argument blocks in the lexicographic order of their dd₀ coordinates, reading one bit from each block per cell – which is why these are element loops and not file tests – and keep three bits of bookkeeping: whether every cell so far agreed, whether a difference has been seen, and, at the first difference, whether it was the second block that held the cell. An equality atom's verdict is the first bit; an order atom's is «agreed throughout, or the first difference went the right way».

Where a level's point lives is fixed here too (DescriptiveComplexity.Draw.Data.lvBlk / lvTrack), in the dictionary of DescriptiveComplexity.Problems.Wide.DrawLeaf: the free levels in the outer blocks of the MIRROR register – the working address – and the quantified ones in the inner blocks of VAL.

Where a level's point lives

noncomputable def DescriptiveComplexity.Draw.Data.lvBlk {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) (j : Fin (dt.nOf v)) : Fin dt.ko ⊕ Fin dt.ki

The argument block a level's point occupies: an outer block – of the working address – below the variable's arity, an inner one – of the VAL register – above it.

Equations

• dt.lvBlk v j = if h : ↑j < dt.arOf v then Sum.inl ⟨↑j, ⋯⟩ else Sum.inr ⟨↑j, ⋯⟩

noncomputable def DescriptiveComplexity.Draw.Data.lvTrack {L : FirstOrder.Language} (dt : Data L) (v : dt.VarIx) (j : Fin (dt.nOf v)) : dt.SlotIx

The register a level's point is read from: MIRROR for a free level, VAL for a quantified one.

Equations

• dt.lvTrack v j = if ↑j < dt.arOf v then DescriptiveComplexity.Draw.Slot.mir else DescriptiveComplexity.Draw.Slot.val

The comparison loops' bookkeeping

noncomputable def DescriptiveComplexity.Draw.Data.cmpAccC {L : FirstOrder.Language} (dt : Data L) : dt.CtlIx

Every cell so far agreed.

Equations

• dt.cmpAccC = dt.scratchC 1

noncomputable def DescriptiveComplexity.Draw.Data.cmpDecC {L : FirstOrder.Language} (dt : Data L) : dt.CtlIx

A difference has been seen.

Equations

• dt.cmpDecC = dt.scratchC 2

noncomputable def DescriptiveComplexity.Draw.Data.cmpValC {L : FirstOrder.Language} (dt : Data L) : dt.CtlIx

At the first difference, the second block held the cell.

Equations

• dt.cmpValC = dt.scratchC 3

noncomputable def DescriptiveComplexity.Draw.Data.cmpRdC {L : FirstOrder.Language} (dt : Data L) (hnf : 2 ≤ dt.nfDim) (k : Fin 2) : dt.CtlIx

The two paired reads of a comparison's round.

Equations

• dt.cmpRdC hnf k = dt.rdfC (Fin.castLE hnf k)

theorem DescriptiveComplexity.Draw.Data.cmpAccC_ne_cmpDecC {L : FirstOrder.Language} {dt : Data L} : dt.cmpAccC ≠ dt.cmpDecC

theorem DescriptiveComplexity.Draw.Data.cmpAccC_ne_cmpValC {L : FirstOrder.Language} {dt : Data L} : dt.cmpAccC ≠ dt.cmpValC

theorem DescriptiveComplexity.Draw.Data.cmpDecC_ne_cmpValC {L : FirstOrder.Language} {dt : Data L} : dt.cmpDecC ≠ dt.cmpValC

theorem DescriptiveComplexity.Draw.Data.cmpDecC_ne_cmpAccC {L : FirstOrder.Language} {dt : Data L} : dt.cmpDecC ≠ dt.cmpAccC

theorem DescriptiveComplexity.Draw.Data.cmpValC_ne_cmpAccC {L : FirstOrder.Language} {dt : Data L} : dt.cmpValC ≠ dt.cmpAccC

theorem DescriptiveComplexity.Draw.Data.cmpValC_ne_cmpDecC {L : FirstOrder.Language} {dt : Data L} : dt.cmpValC ≠ dt.cmpDecC

theorem DescriptiveComplexity.Draw.Data.lvC_ne_cmpAccC {L : FirstOrder.Language} {dt : Data L} (j : Fin dt.dd0) : dt.lvC j ≠ dt.cmpAccC

theorem DescriptiveComplexity.Draw.Data.lvC_ne_cmpDecC {L : FirstOrder.Language} {dt : Data L} (j : Fin dt.dd0) : dt.lvC j ≠ dt.cmpDecC

theorem DescriptiveComplexity.Draw.Data.lvC_ne_cmpValC {L : FirstOrder.Language} {dt : Data L} (j : Fin dt.dd0) : dt.lvC j ≠ dt.cmpValC

theorem DescriptiveComplexity.Draw.Data.cmpRdC_ne_cmpAccC {L : FirstOrder.Language} {dt : Data L} (hnf : 2 ≤ dt.nfDim) (k : Fin 2) : dt.cmpRdC hnf k ≠ dt.cmpAccC

theorem DescriptiveComplexity.Draw.Data.cmpRdC_ne_cmpDecC {L : FirstOrder.Language} {dt : Data L} (hnf : 2 ≤ dt.nfDim) (k : Fin 2) : dt.cmpRdC hnf k ≠ dt.cmpDecC

theorem DescriptiveComplexity.Draw.Data.cmpRdC_ne_cmpValC {L : FirstOrder.Language} {dt : Data L} (hnf : 2 ≤ dt.nfDim) (k : Fin 2) : dt.cmpRdC hnf k ≠ dt.cmpValC

One round of a comparison

noncomputable def DescriptiveComplexity.Draw.Data.cmpFold {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) (hnf : 2 ≤ dt.nfDim) (f : dt.CtlIx → A) : dt.CtlIx → A

The bookkeeping of one round: the pair of bits just read is folded into the three flags – agreement so far, a difference has been seen, and the verdict at the first difference, which is why the last is written only while none has been seen.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.Draw.Data.cmpVerdict {L : FirstOrder.Language} (dt : Data L) {A : Type} (one : A) (isEq : Bool) (f : dt.CtlIx → A) : Prop

What a comparison concludes: an equality atom holds when every cell agreed; an order atom when they did, or when the first difference was the second block's.

Equations

• dt.cmpVerdict one isEq f = if isEq = true then dt.ctlBit one f dt.cmpAccC else dt.ctlBit one f dt.cmpAccC ∨ dt.ctlBit one f dt.cmpValC

noncomputable def DescriptiveComplexity.Draw.Data.cmpInit {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) (f : dt.CtlIx → A) : dt.CtlIx → A

The loop's first round starts from agreement: nothing differs yet, no difference has been seen, and the tuple is the least.

Equations

• dt.cmpInit zero one f = dt.setCtl zero one dt.cmpAccC True (dt.setCtl zero one dt.cmpDecC False (dt.setCtl zero one dt.cmpValC False f))

The read-backs a run cites

theorem DescriptiveComplexity.Draw.Data.ctlBit_cmpAccC_cmpFold {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} (hzo : zero ≠ one) (hnf : 2 ≤ dt.nfDim) (f : dt.CtlIx → A) : dt.ctlBit one (dt.cmpFold zero one hnf f) dt.cmpAccC ↔ dt.ctlBit one f dt.cmpAccC ∧ (dt.ctlBit one f (dt.cmpRdC hnf 0) ↔ dt.ctlBit one f (dt.cmpRdC hnf 1))

theorem DescriptiveComplexity.Draw.Data.ctlBit_cmpDecC_cmpFold {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} (hzo : zero ≠ one) (hnf : 2 ≤ dt.nfDim) (f : dt.CtlIx → A) : dt.ctlBit one (dt.cmpFold zero one hnf f) dt.cmpDecC ↔ dt.ctlBit one f dt.cmpDecC ∨ ¬(dt.ctlBit one f (dt.cmpRdC hnf 0) ↔ dt.ctlBit one f (dt.cmpRdC hnf 1))

theorem DescriptiveComplexity.Draw.Data.ctlBit_cmpValC_cmpFold {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} (hzo : zero ≠ one) (hnf : 2 ≤ dt.nfDim) (f : dt.CtlIx → A) : dt.ctlBit one (dt.cmpFold zero one hnf f) dt.cmpValC ↔ dt.ctlBit one f dt.cmpDecC ∧ dt.ctlBit one f dt.cmpValC ∨ ¬dt.ctlBit one f dt.cmpDecC ∧ ¬dt.ctlBit one f (dt.cmpRdC hnf 0) ∧ dt.ctlBit one f (dt.cmpRdC hnf 1)

theorem DescriptiveComplexity.Draw.Data.readLv_cmpFold {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} (hnf : 2 ≤ dt.nfDim) (f : dt.CtlIx → A) : dt.readLv (dt.cmpFold zero one hnf f) = dt.readLv f

The loop element rides along the bookkeeping, so a round may fold and advance in one step.

theorem DescriptiveComplexity.Draw.Data.ctlBit_cmpAccC_cmpInit {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} (hzo : zero ≠ one) (f : dt.CtlIx → A) : dt.ctlBit one (dt.cmpInit zero one f) dt.cmpAccC

theorem DescriptiveComplexity.Draw.Data.ctlBit_cmpDecC_cmpInit {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} (hzo : zero ≠ one) (f : dt.CtlIx → A) : ¬dt.ctlBit one (dt.cmpInit zero one f) dt.cmpDecC

theorem DescriptiveComplexity.Draw.Data.ctlBit_cmpValC_cmpInit {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} (hzo : zero ≠ one) (f : dt.CtlIx → A) : ¬dt.ctlBit one (dt.cmpInit zero one f) dt.cmpValC

The pack

noncomputable def DescriptiveComplexity.Draw.Data.cmpArgs {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) [LinearOrder A] [Finite A] [Nonempty A] (v : dt.VarIx) (a : Fin dt.natMax) (hnf : 2 ≤ dt.nfDim) (isEq : Bool) (j₁ j₂ : Fin (dt.nOf v)) : ElemArgs A dt.CtlIx dt.SlotIx 2

The parameters of a comparison atom's loop: the two paired reads – one in each level's block, at the padded cell of the control's narrow tuple – the three bookkeeping flags, and the narrow tuple enumeration. The verdict lands in the atom's own slot.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.Draw.Data.cmpArgs_exitSt_congr {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) [LinearOrder A] [Finite A] [Nonempty A] (v : dt.VarIx) (a : Fin dt.natMax) (hnf : 2 ≤ dt.nfDim) (isEq : Bool) (j₁ j₂ : Fin (dt.nOf v)) (f : dt.CtlIx → A) (g g' : dt.SlotIx → A) : (dt.cmpArgs zero one v a hnf isEq j₁ j₂).exitSt f g = (dt.cmpArgs zero one v a hnf isEq j₁ j₂).exitSt f g'

A comparison's exit reads the control alone: the atom's verdict is folded out of the flags, not off the tape.

The tag witnesses of an expansion atom

An expansion atom must know the tags of its argument points before it can pick the defining sentence to run: it reads, for each argument position and each tag, whether that tag's witness cell belongs to the position's block (DescriptiveComplexity.Draw.Data.blk_encTagTup_iff – the read is the point's tag test), and files the answer in a flag. The branch checkpoint then dispatches on the whole tuple, which the flags decode one-hot: that is what makes its dispatches exclusive, and it is the only hypothesis DescriptiveComplexity.Draw.tagSep asks for.

@[instance_reducible]

noncomputable instance DescriptiveComplexity.Draw.Data.instFintypeTagX {L : FirstOrder.Language} (dt : Data L) : Fintype dt.X.Tag

The tag inventory as a Fintype, so that positions and tags can be numbered together.

Equations

• dt.instFintypeTagX = Fintype.ofFinite dt.X.Tag

noncomputable def DescriptiveComplexity.Draw.Data.tagIx {L : FirstOrder.Language} (dt : Data L) {k : ℕ} (hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim) (ℓ : Fin k) (t : dt.X.Tag) : dt.CtlIx

The flag of one witness read: argument position ℓ, tag t.

Equations

• dt.tagIx hk ℓ t = dt.tgfC (Fin.castLE hk (finProdFinEquiv (ℓ, (Fintype.equivFin dt.X.Tag) t)))

theorem DescriptiveComplexity.Draw.Data.tagIx_injective {L : FirstOrder.Language} {dt : Data L} {k : ℕ} (hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim) {ℓ ℓ' : Fin k} {t t' : dt.X.Tag} (h : dt.tagIx hk ℓ t = dt.tagIx hk ℓ' t') : ℓ = ℓ' ∧ t = t'

def DescriptiveComplexity.Draw.Data.TagsAre {L : FirstOrder.Language} (dt : Data L) {A : Type} (one : A) {k : ℕ} (hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim) (τ : Fin k → dt.X.Tag) (f : dt.CtlIx → A) : Prop

What the flags say: the tuple of tags they decode, read as a one-hot family – position by position, exactly the tag of that position is flagged.

Equations

• dt.TagsAre one hk τ f = ∀ (ℓ : Fin k) (t : dt.X.Tag), dt.ctlBit one f (dt.tagIx hk ℓ t) ↔ t = τ ℓ

noncomputable def DescriptiveComplexity.Draw.Data.tagMatch {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) (v : dt.VarIx) {k : ℕ} (ts : Fin k → Fin (dt.nOf v)) (ℓ : Fin k) (t : dt.X.Tag) : (dt.CtlIx → A) → (dt.SlotIx → A) → Prop

The witness read's guard: the tag witness cell of the tag t in the block of the level the position reads. Its digit is the point's tag test.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.Draw.Data.tagsAre_unique {L : FirstOrder.Language} {dt : Data L} {A : Type} {one : A} {k : ℕ} (hk : k * Fintype.card dt.X.Tag ≤ dt.ntgDim) (τ τ' : Fin k → dt.X.Tag) (f : dt.CtlIx → A) (h : dt.TagsAre one hk τ f) (h' : dt.TagsAre one hk τ' f) : τ = τ'

The decoding is exclusive: a one-hot family determines its tuple, so the branch checkpoint's dispatches never co-fire. This is the hypothesis DescriptiveComplexity.Draw.tagSep carries.

The read leaves of an expansion atom

A round of an expansion atom's element loop makes one trip per block atom of the defining sentence's matrix: the atom names a copy – which argument point – a relation variable of that point's block, and the levels its payload reads. The trip goes to the cell of that member tuple, in the block the copy's level occupies, and its digit is the assignment bit (DescriptiveComplexity.Draw.Data.blk_encAsgTup_iff).

noncomputable def DescriptiveComplexity.Draw.Data.relLeafData {L : FirstOrder.Language} {dt : Data L} [L.IsRelational] {k : ℕ} (e : dt.X.E.Relations k) (τ : Fin k → dt.X.Tag) (r : Fin (dt.relNr e τ)) : (i : (dt.X.B.replicate k).ι) × (Fin ((dt.X.B.replicate k).arity i) → Fin (dt.relPk e τ).n)

The data of the r-th read leaf: the block atom's variable – a copy of the block, so an argument position paired with one of the point's relation variables – and the levels its payload reads.

Equations

• DescriptiveComplexity.Draw.Data.relLeafData e τ r = ⟨⋯.choose, ⋯.choose⟩

theorem DescriptiveComplexity.Draw.Data.blkAtom?_relLeafData {L : FirstOrder.Language} {dt : Data L} [L.IsRelational] {k : ℕ} (e : dt.X.E.Relations k) (τ : Fin k → dt.X.Tag) (r : Fin (dt.relNr e τ)) : blkAtom? ((blkAtoms (dt.relPk e τ).mat).get r) = some (BlkAtom.blkA (relLeafData e τ r).fst (relLeafData e τ r).snd)

The leaf is that block atom: what the trip's digit has to mean.

noncomputable def DescriptiveComplexity.Draw.Data.expPay {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero : A) [L.IsRelational] {k : ℕ} (e : dt.X.E.Relations k) (τ : Fin k → dt.X.Tag) (r : Fin (dt.relNr e τ)) (hn : (dt.relPk e τ).n ≤ dt.eDim) (f : dt.CtlIx → A) : Fin (blockArityBound dt.X.B) → A

The payload a read leaf spells: the block atom's levels, read out of the loop's wide tuple and padded to the block's arity bound – which is exactly the payload of the member tuple DescriptiveComplexity.Draw.encAsgTup.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.Draw.Data.expRdTrack {L : FirstOrder.Language} (dt : Data L) [L.IsRelational] {k : ℕ} (v : dt.VarIx) (ts : Fin k → Fin (dt.nOf v)) (e : dt.X.E.Relations k) (τ : Fin k → dt.X.Tag) (r : Fin (dt.relNr e τ)) : dt.SlotIx

The track a read leaf reads: the register the copy's level lives in.

Equations

• dt.expRdTrack v ts e τ r = dt.lvTrack v (ts (DescriptiveComplexity.Draw.Data.relLeafData e τ r).fst.1)

noncomputable def DescriptiveComplexity.Draw.Data.expMatch {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) [L.IsRelational] {k : ℕ} (v : dt.VarIx) (ts : Fin k → Fin (dt.nOf v)) (e : dt.X.E.Relations k) (τ : Fin k → dt.X.Tag) (r : Fin (dt.relNr e τ)) (hn : (dt.relPk e τ).n ≤ dt.eDim) : (dt.CtlIx → A) → (dt.SlotIx → A) → Prop

The cell a read leaf goes to: the member tuple of the copy's point, in the block that point occupies.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.Draw.Data.expSetFlag {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) {k : ℕ} (e : dt.X.E.Relations k) (τ : Fin k → dt.X.Tag) (r : Fin (dt.relNr e τ)) (hrd : dt.relNr e τ ≤ dt.nfDim) (b : Bool) (f : dt.CtlIx → A) (_g : dt.SlotIx → A) : dt.CtlIx → A

Where a read leaf files its bit: the leaf-read flag of its index.

Equations

• dt.expSetFlag zero one e τ r hrd b f _g = dt.setCtl zero one (dt.rdfC (Fin.castLE hrd r)) (b = true) f

The leaf of a branch, as the control computes it

noncomputable def DescriptiveComplexity.Draw.Data.expLeafVal {L : FirstOrder.Language} (dt : Data L) {A : Type} (one : A) [L.IsRelational] [LinearOrder A] [L.Structure A] {k : ℕ} (e : dt.X.E.Relations k) (τ : Fin k → dt.X.Tag) (hn : (dt.relPk e τ).n ≤ dt.eDim) (hrd : dt.relNr e τ ≤ dt.nfDim) (f : dt.CtlIx → A) : Prop

The value of a branch's matrix, from the control alone: its block atoms are the leaf-read flags the round has just filed, its base atoms are guards – equalities, base relations and order comparisons on the loop's own tuple, which the transition table evaluates where they stand.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.Draw.Data.expLeafVal_iff {L : FirstOrder.Language} (dt : Data L) {A : Type} (one : A) [L.IsRelational] [LinearOrder A] [L.Structure A] {k : ℕ} (e : dt.X.E.Relations k) (τ : Fin k → dt.X.Tag) (hn : (dt.relPk e τ).n ≤ dt.eDim) (hrd : dt.relNr e τ ≤ dt.nfDim) (ρs : Fin k → dt.X.B.Assignment A) (f : dt.CtlIx → A) (hav : ∀ (r : Fin (dt.relNr e τ)), dt.ctlBit one f (dt.rdfC (Fin.castLE hrd r)) ↔ BlkAtom.holds (dt.X.B.replicateAssign ρs) (fun (j : Fin (dt.relPk e τ).n) => f (dt.lvE (Fin.castLE hn j))) (BlkAtom.blkA (relLeafData e τ r).fst (relLeafData e τ r).snd)) : dt.expLeafVal one e τ hn hrd f ↔ dt.expLeaf e τ ρs fun (j : Fin (dt.relPk e τ).n) => f (dt.lvE (Fin.castLE hn j))

What the control computes is the branch's leaf. Given that every leaf-read flag holds its block atom's value – which DescriptiveComplexity.Draw.Data.regBit_expMatch is what the trip delivers – the Boolean function of the flags and the guards is the leaf predicate DescriptiveComplexity.Draw.Data.expLeaf of DescriptiveComplexity.Problems.Wide.DrawExp.

A branch's loop, wired

noncomputable def DescriptiveComplexity.Draw.Data.expInit {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) [LinearOrder A] [Finite A] [Nonempty A] {k : ℕ} (e : dt.X.E.Relations k) (τ : Fin k → dt.X.Tag) (f : dt.CtlIx → A) : dt.CtlIx → A

A branch's loop, started: the wide tuple at the least, the sub-fold's accumulators at the polarity's units.

Equations

• dt.expInit zero one e τ f = dt.initSac zero one (dt.relPk e τ).pol (dt.initLvE f)

noncomputable def DescriptiveComplexity.Draw.Data.expAdv {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) [L.IsRelational] [LinearOrder A] [L.Structure A] {k : ℕ} (e : dt.X.E.Relations k) (τ : Fin k → dt.X.Tag) (hn : (dt.relPk e τ).n ≤ dt.eDim) (hrd : dt.relNr e τ ≤ dt.nfDim) (f : dt.CtlIx → A) : dt.CtlIx → A

A branch's round, folded and advanced: the leaf the round just computed is filed, the accumulators fold at the coordinate the tuple carries (DescriptiveComplexity.Draw.tupCarry), and the tuple steps.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.Draw.Data.expExit {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) [L.IsRelational] [LinearOrder A] [L.Structure A] {k : ℕ} (e : dt.X.E.Relations k) (τ : Fin k → dt.X.Tag) (hn : (dt.relPk e τ).n ≤ dt.eDim) (hrd : dt.relNr e τ ≤ dt.nfDim) (a : Fin dt.natMax) (f : dt.CtlIx → A) : dt.CtlIx → A

A branch's last round: the final leaf is filed and the sub-fold's verdict lands in the atom's slot.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.Draw.Data.wIx {L : FirstOrder.Language} (dt : Data L) {k : ℕ} (i : Fin (k * Fintype.card dt.X.Tag)) : Fin k × dt.X.Tag

The witness reads of an expansion atom, numbered: one per argument position and tag.

Equations

• dt.wIx i = ((finProdFinEquiv.symm i).1, (Fintype.equivFin dt.X.Tag).symm (finProdFinEquiv.symm i).2)

noncomputable def DescriptiveComplexity.Draw.Data.expArgs {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) [L.IsRelational] [LinearOrder A] [L.Structure A] [Finite A] [Nonempty A] {k : ℕ} (v : dt.VarIx) (ts : Fin k → Fin (dt.nOf v)) (e : dt.X.E.Relations k) (a : Fin dt.natMax) (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) : TagArgs A dt.CtlIx dt.SlotIx (k * Fintype.card dt.X.Tag) (Fin k → dt.X.Tag) (dt.relNr e)

The parameter pack of an expansion atom's machinery: the tag witnesses and their one-hot decoding, then, per branch, the read leaves of the defining sentence and the sub-fold over its prefix.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.Draw.Data.expArgs_exitSt_congr {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) [L.IsRelational] [LinearOrder A] [L.Structure A] [Finite A] [Nonempty A] {k : ℕ} (v : dt.VarIx) (ts : Fin k → Fin (dt.nOf v)) (e : dt.X.E.Relations k) (a : Fin dt.natMax) (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) (τ : Fin k → dt.X.Tag) (f : dt.CtlIx → A) (g g' : dt.SlotIx → A) : (dt.expArgs zero one v ts e a hk hn hrd).exitSt τ f g = (dt.expArgs zero one v ts e a hk hn hrd).exitSt τ f g'

An expansion atom's exit reads the control alone.

The gates

A gate asks of one outer block of the working address – held in MIRROR – that it encode a point: which tag its witness carries, that every member is well-shaped for that tag, and that the tag's domain sentence hold of the decoded assignment (DescriptiveComplexity.Draw.isEnc_iff_parts). The last is the element loop again, at the domain pack, and all of its read leaves go to the same block – the domain sentence is over the un-replicated block, so every block atom is about the gated point itself.

noncomputable def DescriptiveComplexity.Draw.Data.tagWitnessMatch {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) (b : Fin dt.ko ⊕ Fin dt.ki) (t : dt.X.Tag) : (dt.CtlIx → A) → (dt.SlotIx → A) → Prop

The tag-witness guard of a block: the cell of the tag's witness tuple.

Equations

• dt.tagWitnessMatch zero one b t = dt.nameGF one b (dt.encCoord zero one (Sum.inl t) fun (x : dt.CtlIx → A) (x_1 : Fin (DescriptiveComplexity.blockArityBound dt.X.B)) => zero)

noncomputable def DescriptiveComplexity.Draw.Data.gateTagC {L : FirstOrder.Language} (dt : Data L) (hc : Fintype.card dt.X.Tag ≤ dt.ntgDim) (t : dt.X.Tag) : dt.CtlIx

A gate's tag flag: one per tag of the block it gates.

Equations

• dt.gateTagC hc t = dt.tgfC (Fin.castLE hc ((Fintype.equivFin dt.X.Tag) t))

def DescriptiveComplexity.Draw.Data.GateTagsAre {L : FirstOrder.Language} (dt : Data L) {A : Type} (one : A) (hc : Fintype.card dt.X.Tag ≤ dt.ntgDim) (t : dt.X.Tag) (f : dt.CtlIx → A) : Prop

What a gate's flags say: the tag they decode, one-hot.

Equations

• dt.GateTagsAre one hc t f = ∀ (t' : dt.X.Tag), dt.ctlBit one f (dt.gateTagC hc t') ↔ t' = t

theorem DescriptiveComplexity.Draw.Data.gateTagsAre_unique {L : FirstOrder.Language} {dt : Data L} {A : Type} {one : A} (hc : Fintype.card dt.X.Tag ≤ dt.ntgDim) (t t' : dt.X.Tag) (f : dt.CtlIx → A) (h : dt.GateTagsAre one hc t f) (h' : dt.GateTagsAre one hc t' f) : t = t'

A gate's decoding is exclusive, so its branch never co-fires.

noncomputable def DescriptiveComplexity.Draw.Data.domLeafData {L : FirstOrder.Language} {dt : Data L} [L.IsRelational] (t : dt.X.Tag) (r : Fin (dt.domNr t)) : (i : dt.X.B.ι) × (Fin (dt.X.B.arity i) → Fin (dt.domPk t).n)

The data of the r-th read leaf of a domain sentence: the point's relation variable and the levels its payload reads – all at the gated block, since the sentence is over the block itself.

Equations

• DescriptiveComplexity.Draw.Data.domLeafData t r = ⟨⋯.choose, ⋯.choose⟩

theorem DescriptiveComplexity.Draw.Data.blkAtom?_domLeafData {L : FirstOrder.Language} {dt : Data L} [L.IsRelational] (t : dt.X.Tag) (r : Fin (dt.domNr t)) : blkAtom? ((blkAtoms (dt.domPk t).mat).get r) = some (BlkAtom.blkA (domLeafData t r).fst (domLeafData t r).snd)

The leaf is that block atom.

noncomputable def DescriptiveComplexity.Draw.Data.domPay {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero : A) [L.IsRelational] (t : dt.X.Tag) (r : Fin (dt.domNr t)) (hn : (dt.domPk t).n ≤ dt.eDim) (f : dt.CtlIx → A) : Fin (blockArityBound dt.X.B) → A

The payload a domain read leaf spells.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.Draw.Data.domMatch {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) [L.IsRelational] (b : Fin dt.ko ⊕ Fin dt.ki) (t : dt.X.Tag) (r : Fin (dt.domNr t)) (hn : (dt.domPk t).n ≤ dt.eDim) : (dt.CtlIx → A) → (dt.SlotIx → A) → Prop

The cell a domain read leaf goes to: the member tuple of the gated point, in the block being gated.

Equations

• dt.domMatch zero one b t r hn = dt.nameGF one b (dt.encCoord zero one (Sum.inr (DescriptiveComplexity.Draw.Data.domLeafData t r).fst) (dt.domPay zero t r hn))

noncomputable def DescriptiveComplexity.Draw.Data.domSetFlag {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) (t : dt.X.Tag) (r : Fin (dt.domNr t)) (hrd : dt.domNr t ≤ dt.nfDim) (b : Bool) (f : dt.CtlIx → A) (_g : dt.SlotIx → A) : dt.CtlIx → A

Where a domain read leaf files its bit.

Equations

• dt.domSetFlag zero one t r hrd b f _g = dt.setCtl zero one (dt.rdfC (Fin.castLE hrd r)) (b = true) f

noncomputable def DescriptiveComplexity.Draw.Data.domLeafVal {L : FirstOrder.Language} (dt : Data L) {A : Type} (one : A) [L.IsRelational] [LinearOrder A] [L.Structure A] (t : dt.X.Tag) (hn : (dt.domPk t).n ≤ dt.eDim) (hrd : dt.domNr t ≤ dt.nfDim) (f : dt.CtlIx → A) : Prop

The value of a domain sentence's matrix, from the control alone.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.Draw.Data.domLeafVal_iff {L : FirstOrder.Language} {dt : Data L} {A : Type} {one : A} [L.IsRelational] [LinearOrder A] [L.Structure A] (t : dt.X.Tag) (hn : (dt.domPk t).n ≤ dt.eDim) (hrd : dt.domNr t ≤ dt.nfDim) (ρ : dt.X.B.Assignment A) (f : dt.CtlIx → A) (hav : ∀ (r : Fin (dt.domNr t)), dt.ctlBit one f (dt.rdfC (Fin.castLE hrd r)) ↔ BlkAtom.holds ρ (fun (j : Fin (dt.domPk t).n) => f (dt.lvE (Fin.castLE hn j))) (BlkAtom.blkA (domLeafData t r).fst (domLeafData t r).snd)) : dt.domLeafVal one t hn hrd f ↔ dt.domLeaf t ρ fun (j : Fin (dt.domPk t).n) => f (dt.lvE (Fin.castLE hn j))

What the control computes is the domain sentence's leaf, given that every leaf-read flag holds its block atom's bit.

noncomputable def DescriptiveComplexity.Draw.Data.gateInit {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) [LinearOrder A] [Finite A] [Nonempty A] (t : dt.X.Tag) (f : dt.CtlIx → A) : dt.CtlIx → A

A gate's domain loop, started.

Equations

• dt.gateInit zero one t f = dt.initSac zero one (dt.domPk t).pol (dt.initLvE f)

noncomputable def DescriptiveComplexity.Draw.Data.gateAdv {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) [L.IsRelational] [LinearOrder A] [L.Structure A] (t : dt.X.Tag) (hn : (dt.domPk t).n ≤ dt.eDim) (hrd : dt.domNr t ≤ dt.nfDim) (f : dt.CtlIx → A) : dt.CtlIx → A

A gate's domain round, folded and advanced.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.Draw.Data.defTag {L : FirstOrder.Language} (dt : Data L) {A : Type} [LinearOrder A] [L.Structure A] [Finite A] [Nonempty A] : dt.X.Tag

The dispatch's default tag. A gate's branch checkpoint dispatches on the decoded tag of its block value; where the witness flags are not one-hot – block values the sweeps and the VAL enumeration produce and no point encodes – the checkpoint fires into this tag's branch instead, and the branch's conjoining exit reads the non-one-hotness off the surviving witness flags and clears the flag. Any tag serves.

That last sentence is what permits the choice, and is why the tag is chosen from a nonemptiness of the tags rather than from a point: an interpretation names this tag in a formula, so it must be the same tag at every instance, and by proof irrelevance a Classical.ofNonempty at a Prop is (the structure only witnesses that the tags are inhabited, and which structure witnessed it does not survive into the value). Choosing a point instead would give a different tag at a different instance, and no formula could name it.

Equations

• dt.defTag = Classical.ofNonempty

def DescriptiveComplexity.Draw.Data.DspTagsAre {L : FirstOrder.Language} (dt : Data L) {A : Type} (one : A) [LinearOrder A] [L.Structure A] [Finite A] [Nonempty A] (hc : Fintype.card dt.X.Tag ≤ dt.ntgDim) (t : dt.X.Tag) (f : dt.CtlIx → A) : Prop

What a gate's branch checkpoint dispatches on: the decoded tag where the witness flags are one-hot, the default tag where they are not – so some dispatch always fires, on every block value. The exit's one-hotness conjunct makes the default branch clear the flag, so totality costs no wrong verdict. Shared by the outer gates (at MIRROR) and the inner ones (at VAL).

Equations

• dt.DspTagsAre one hc t f = (dt.GateTagsAre one hc t f ∨ t = dt.defTag ∧ ∀ (t' : dt.X.Tag), ¬dt.GateTagsAre one hc t' f)

theorem DescriptiveComplexity.Draw.Data.dspTagsAre_unique {L : FirstOrder.Language} {dt : Data L} {A : Type} {one : A} [LinearOrder A] [L.Structure A] [Finite A] [Nonempty A] (hc : Fintype.card dt.X.Tag ≤ dt.ntgDim) (t t' : dt.X.Tag) (f : dt.CtlIx → A) (h : dt.DspTagsAre one hc t f) (h' : dt.DspTagsAre one hc t' f) : t = t'

The total dispatch is still exclusive, so the branch never co-fires.

noncomputable def DescriptiveComplexity.Draw.Data.dspTagOf {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) [LinearOrder A] [L.Structure A] [Finite A] [Nonempty A] (S : (Fin dt.dd → A) → Prop) : dt.X.Tag

The tag a gate dispatches to: the unique tag whose witness the block value holds, where there is one; the default tag otherwise.

Equations

• dt.dspTagOf zero one S = if h : ∃ (t : dt.X.Tag), ∀ (t' : dt.X.Tag), S (DescriptiveComplexity.Draw.encTagTup dt.ly zero one t') ↔ t' = t then h.choose else dt.defTag

theorem DescriptiveComplexity.Draw.Data.dspTagOf_eq_of_onehot {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [LinearOrder A] [L.Structure A] [Finite A] [Nonempty A] {S : (Fin dt.dd → A) → Prop} {t : dt.X.Tag} (hone : ∀ (t' : dt.X.Tag), S (encTagTup dt.ly zero one t') ↔ t' = t) : dt.dspTagOf zero one S = t

At a one-hot block value the dispatch is the decoded tag – how a gated address's per-block tag data pins the dispatch.

noncomputable def DescriptiveComplexity.Draw.Data.gateExit {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) [L.IsRelational] [LinearOrder A] [L.Structure A] (t : dt.X.Tag) (hc : Fintype.card dt.X.Tag ≤ dt.ntgDim) (hn : (dt.domPk t).n ≤ dt.eDim) (hrd : dt.domNr t ≤ dt.nfDim) (f : dt.CtlIx → A) : dt.CtlIx → A

A gate's conjoining exit: the flag keeps its value only if the block's witness flags are one-hot at the dispatched tag – so the default branch always clears – and the sub-fold of the tag's domain sentence holds.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.Draw.Data.gateArgs {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) [L.IsRelational] [LinearOrder A] [L.Structure A] [Finite A] [Nonempty A] (b : Fin dt.ko ⊕ Fin dt.ki) (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) : TagArgs A dt.CtlIx dt.SlotIx (Fintype.card dt.X.Tag) dt.X.Tag dt.domNr

The parameter pack of one gate block's domain evaluation: the tag witnesses of the block, their one-hot decoding, and per tag the read leaves of its domain sentence with the sub-fold over its prefix.

Equations

• One or more equations did not get rendered due to their size.

The stage atoms

A stage atom is the random access: the argument points' blocks are copied into the outer blocks of TARGET – one coordinate loop per position, a read trip and a write trip per padded cell – the working cell is sought to that address, and the stage track is read under the head. Everything the pack names is already fixed: where a level's point lives, the narrow tuple enumeration, and the copied bit's flag.

noncomputable def DescriptiveComplexity.Draw.Data.stageArgs {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) [LinearOrder A] [Finite A] [Nonempty A] (v : dt.VarIx) (i : dt.d.B.ι) (ts : Fin (dt.d.B.arity i) → Fin (dt.nOf v)) (a : Fin dt.natMax) : StageArgs A dt.CtlIx dt.SlotIx (Fin dt.ko ⊕ Fin dt.ki) dt.dd0 (dt.d.B.arity i)

The parameter pack of a stage atom's machinery: the source track and block of each argument position, the outer block of TARGET it is copied to, the coordinate loop and its copied bit, the stage track read under the head, and the atom's verdict slot.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.Draw.Data.stageArgs_setAv_congr {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) [LinearOrder A] [Finite A] [Nonempty A] (v : dt.VarIx) (i : dt.d.B.ι) (ts : Fin (dt.d.B.arity i) → Fin (dt.nOf v)) (a : Fin dt.natMax) (b : Bool) (f : dt.CtlIx → A) (g g' : dt.SlotIx → A) : (dt.stageArgs zero one v i ts a).setAv b f g = (dt.stageArgs zero one v i ts a).setAv b f g'

A stage atom's verdict store reads the control alone: what it files is the bit the random access came back with, and that bit is a hypothesis of the store, not a read of it.

The dispatch: one pack per atom

noncomputable def DescriptiveComplexity.Draw.Data.kindArgsOf {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) [L.IsRelational] [LinearOrder A] [L.Structure A] [Finite A] [Nonempty A] (v : dt.VarIx) (a : Fin dt.natMax) (κ : MatAtom dt.X dt.d.B (dt.nOf v)) : dt.kindArgs κ * Fintype.card dt.X.Tag ≤ dt.ntgDim → dt.kindDepth κ ≤ dt.eDim → dt.kindReads κ ≤ dt.nfDim → dt.KindArgs κ

The pack of an atom, by its kind, with the budgets it needs as hypotheses about that kind – so the match is on the kind itself and the stuck DescriptiveComplexity.Draw.Data.kindOf never has to be unfolded.

Equations

• dt.kindArgsOf zero one v a (DescriptiveComplexity.Draw.MatAtom.eq j₁ j₂) x_4 x_5 hrd = dt.cmpArgs zero one v a hrd true j₁ j₂
• dt.kindArgsOf zero one v a (DescriptiveComplexity.Draw.MatAtom.ord j₁ j₂) x_4 x_5 hrd = dt.cmpArgs zero one v a hrd false j₁ j₂
• dt.kindArgsOf zero one v a (DescriptiveComplexity.Draw.MatAtom.stage i ts) x_4 x_5 x_6 = dt.stageArgs zero one v i ts a
• dt.kindArgsOf zero one v a (DescriptiveComplexity.Draw.MatAtom.exp e ts) hk hn hrd = dt.expArgs zero one v ts e a hk ⋯ ⋯

noncomputable def DescriptiveComplexity.Draw.Data.atomArgs {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) [L.IsRelational] [LinearOrder A] [L.Structure A] [Finite A] [Nonempty A] (v : dt.VarIx) (a : Fin (dt.natOf v)) : dt.KindArgs (dt.kindOf v a)

The pack of the a-th atom of a variable's matrix.

Equations

• dt.atomArgs zero one v a = dt.kindArgsOf zero one v (Fin.castLE ⋯ a) (dt.kindOf v a) ⋯ ⋯ ⋯

The whole pack of a variable

noncomputable def DescriptiveComplexity.Draw.Data.wellShapedG {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) (b : Fin dt.ko ⊕ Fin dt.ki) (g : dt.SlotIx → A) : Prop

The well-shapedness question of a gate, per cell: a cell of the gated block whose digit is set must carry a canonically padded element whose name slots spell an encoded tuple – the witness of some tag, or a member of some relation variable. With the tag out of the members (DescriptiveComplexity.Draw.PtCode) this is a question about the cell and nothing else, which is what a file test can ask.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.Draw.Data.wellShapedIG {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) (b : Fin dt.ko ⊕ Fin dt.ki) (g : dt.SlotIx → A) : Prop

The well-shapedness question of an inner gate, per cell: the same question as DescriptiveComplexity.Draw.Data.wellShapedG with the digit read off the VAL register instead of the mirror.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.Draw.Data.igateExit {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) [L.IsRelational] [LinearOrder A] [L.Structure A] (flag : dt.CtlIx) (t : dt.X.Tag) (hc : Fintype.card dt.X.Tag ≤ dt.ntgDim) (hn : (dt.domPk t).n ≤ dt.eDim) (hrd : dt.domNr t ≤ dt.nfDim) (f : dt.CtlIx → A) : dt.CtlIx → A

An inner gate's conjoining exit: as DescriptiveComplexity.Draw.Data.gateExit, into the given flag – the level's polarity chooses which of the round's two flags – with one conjunct more: the witness flags must be one-hot at the dispatched tag. On the genuine branch the conjunct is what the dispatch already knew; on the default branch it is false, so the flag is cleared – which is the right verdict, a block value with no one-hot witness encoding no point.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.Draw.Data.igateArgs {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) [L.IsRelational] [LinearOrder A] [L.Structure A] [Finite A] [Nonempty A] (b : Fin dt.ko ⊕ Fin dt.ki) (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) : TagArgs A dt.CtlIx dt.SlotIx (Fintype.card dt.X.Tag) dt.X.Tag dt.domNr

The parameter pack of one inner gate block: the outer gates' pack with the read tracks on VAL and the verdict conjoined into the level's polarity flag.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.Draw.Data.varArgsOf {L : FirstOrder.Language} (dt : Data L) {A : Type} (zero one : A) [L.IsRelational] [LinearOrder A] [L.Structure A] [Finite A] [Nonempty A] (v : dt.VarIx) : dt.VarArgs v

The semantic pack of one variable's machinery, assembled: the atoms' packs by kind, the gates' per block, the fold updates in the control, and the stage slot the variable writes – the output's being the marker itself, which a true verdict rewrites with the value already there and a false one erases just as the machine halts.

Equations

• One or more equations did not get rendered due to their size.

What a read leaf finds

theorem DescriptiveComplexity.Draw.Data.regBit_expMatch {L : FirstOrder.Language} {dt : Data L} {A : Type} {zero one : A} [L.IsRelational] [LinearOrder A] [L.Structure A] [Finite A] {R' P' : Type} [Finite R'] [Finite P'] [Finite dt.KIx] [FirstOrder.Language.wide.Structure (Univ A R' P' dt.KIx dt.dd)] (hzo : zero ≠ one) (hlin : IsLinOrd WMLe) {k : ℕ} {v : dt.VarIx} (ts : Fin k → Fin (dt.nOf v)) (e : dt.X.E.Relations k) (τ : Fin k → dt.X.Tag) (r : Fin (dt.relNr e τ)) (hn : (dt.relPk e τ).n ≤ dt.eDim) (points : Fin k → dt.X.Map A) {m : Univ A R' P' dt.KIx dt.dd → Prop} (hp : wmBlk m (Tag.arg (toLex (dt.lvBlk v (ts (relLeafData e τ r).fst.1)))) = encMap dt.ly zero one (points (relLeafData e τ r).fst.1)) (f : dt.CtlIx → A) : regBit m (wmSeg (dt.blkElt (dt.lvBlk v (ts (relLeafData e τ r).fst.1)) (encTup dt.ly zero one (Sum.inr (relLeafData e τ r).fst.2) (dt.expPay zero e τ r hn f)))) ↔ BlkAtom.holds (dt.X.B.replicateAssign fun (ℓ : Fin k) => (↑(points ℓ)).2) (fun (j : Fin (dt.relPk e τ).n) => f (dt.lvE (Fin.castLE hn j))) (BlkAtom.blkA (relLeafData e τ r).fst (relLeafData e τ r).snd)

A read leaf's digit is the block atom's value. At a block holding the encoding of the copy's point, the bit the trip finds at the member tuple is exactly what DescriptiveComplexity.Draw.BlkAtom.holds says of the atom, at the valuation the loop's wide tuple spells. This is the join between DescriptiveComplexity.Problems.Wide.DrawExp's leaf predicate and the machine.