What a coarse file's gate test is, elementwise

The gates' shape test reads four slots of the background – the block one-hot, the mirror bit, the padding flag and the name coordinates – and none of the address-side ones. Each of the four is a fact about the register's own index, and at a file whose registers stand for elements each is the same fact about the element: the block is the element's tag's (hblkP), the tuple is the element's (hargP), and the mirror bit at the register is the mirror's address at the element (ixAddr_elt).

So a coarse file's shape test at a register is the elementwise test at the element it stands for, which is the step the two bridges hpassEnc and hgateEnc need: DescriptiveComplexity.Draw.Data.gate_trichotomy is stated elementwise and reaches a coarse file through this file.

theorem DescriptiveComplexity.Draw.Data.wellShapedG_ixBack_iff {L : FirstOrder.Language} {dt : Data L} {A R' P' I : Type} {lay : Layout dt A R' P' I} {elt : I → Univ A R' P' dt.KIx dt.dd} {zero one : A} (hinj : Function.Injective lay.cell) (heltInj : Function.Injective elt) (hblkP : ∀ (u : I), lay.blk u = tagBlk (elt u).1) (hargP : ∀ (u : I), lay.arg u = (elt u).2) (hzo : zero ≠ one) (st : TapeSt dt A R' P' I) (b : Fin dt.ko ⊕ Fin dt.ki) (u : I) : dt.wellShapedG zero one b (dt.ixBack lay zero one ⋯ st (lay.cell u)) ↔ tagBlk (elt u).1 = some b → ixAddr elt st.mir (elt u) → (∀ (j : Fin dt.dd), dt.dd0 ≤ ↑j → (elt u).2 j = zero) ∧ ((∃ (t : dt.X.Tag), ∀ (j : Fin dt.dd0), (elt u).2 (Fin.castLE ⋯ j) = encTagTup dt.ly zero one t (Fin.castLE ⋯ j)) ∨ ∃ (i : dt.X.B.ι) (w : Fin (dt.X.B.arity i) → A), ∀ (j : Fin dt.dd0), (elt u).2 (Fin.castLE ⋯ j) = encAsgTup dt.ly zero one i w (Fin.castLE ⋯ j))

A coarse file's shape test is the elementwise one: the gate's four slots are the register's block, mirror bit, padding and tuple, and each of them is the same fact about the element the register stands for. So a program whose registers are not the elements asks exactly the question DescriptiveComplexity.Draw.Data.gate_trichotomy answers.