The gate, decomposed the way the machine checks it

DescriptiveComplexity.Draw.IsEnc – a block value encodes a point of the expanded universe – is an existential over points, which is not a shape a machine can test. This file decomposes it into the three questions the program's gate subroutine actually asks:

• exactly one tag's witness is present – one membership question per tag, finitely many, and the answers are the control's tag flags;
• every member is well-shaped – a witness tuple or a member tuple: one file test, the per-cell question read off the name marks, and tag-free, which is why the code of a member carries no tag (DescriptiveComplexity.Draw.PtCode);
• the domain sentence holds of the decoded assignment – where DescriptiveComplexity.Draw.decRho reads the assignment back one membership question per bit, which is the element-loop sub-evaluation.

DescriptiveComplexity.Draw.isEnc_iff_parts is the equivalence. Uniqueness of the witness is a clause and not an afterthought – with tag-free members it is the only thing tying the block value to one tag – and it costs nothing: the machine reads every tag's witness cell anyway, so the condition is a one-hotness test on the flags it has just filled.

def DescriptiveComplexity.Draw.decRho {L : FirstOrder.Language} {X : ExpExpansion L} {dd : ℕ} (ly : EncLayout (PtCode X) (blockArityBound X.B) dd) {A : Type} (zero one : A) (S : (Fin dd → A) → Prop) : X.B.Assignment A

The assignment a block value decodes to at a tag: one membership question per bit. On a value that is an encoding this is the encoded assignment; elsewhere it is read only under the gate's other clauses.

Equations

• DescriptiveComplexity.Draw.decRho ly zero one S i w = S (DescriptiveComplexity.Draw.encAsgTup ly zero one i w)

theorem DescriptiveComplexity.Draw.decRho_encPt {L : FirstOrder.Language} {X : ExpExpansion L} {dd : ℕ} (ly : EncLayout (PtCode X) (blockArityBound X.B) dd) {A : Type} {zero one : A} (hne : zero ≠ one) (p : X.Point A) : decRho ly zero one (encPt ly zero one p) = p.2

On an encoding, the decoded assignment is the encoded one.

theorem DescriptiveComplexity.Draw.isEnc_iff_parts {L : FirstOrder.Language} {X : ExpExpansion L} {dd : ℕ} (ly : EncLayout (PtCode X) (blockArityBound X.B) dd) {A : Type} {zero one : A} [L.Structure A] [LinearOrder A] (hne : zero ≠ one) (S : (Fin dd → A) → Prop) : IsEnc ly zero one S ↔ ∃ (t : X.Tag), S (encTagTup ly zero one t) ∧ (∀ (t' : X.Tag), S (encTagTup ly zero one t') → t' = t) ∧ (∀ (v : Fin dd → A), S v → (∃ (t' : X.Tag), v = encTagTup ly zero one t') ∨ ∃ (i : X.B.ι) (w : Fin (X.B.arity i) → A), v = encAsgTup ly zero one i w) ∧ ExpExpansion.DomHolds (t, decRho ly zero one S)

The gate, decomposed: a block value is an encoding exactly when some tag's witness belongs to it, every member is well-shaped for that tag, and the domain sentence holds of the decoded assignment. These are the three questions the machine's gate subroutine asks, in the order it asks them.