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.ixBack_blk_cell_eq {L : FirstOrder.Language} {dt : Data L} {A R' P' I : Type} {lay : Layout dt A R' P' I} {zero one : A} (hinj : Function.Injective lay.cell) (st : TapeSt dt A R' P' I) (u : I) (b : Option (Fin dt.ko ⊕ Fin dt.ki)) : dt.ixBack lay zero one ⋯ st (lay.cell u) (Slot.blk b) = bitVal zero one (lay.blk u = b)

A coarse background's block one-hot, at a register: the register's own block, which by hblkP is the block of the element it stands for.

theorem DescriptiveComplexity.Draw.Data.ixBack_mir_cell_eq {L : FirstOrder.Language} {dt : Data L} {A R' P' I : Type} {lay : Layout dt A R' P' I} {zero one : A} (hinj : Function.Injective lay.cell) (st : TapeSt dt A R' P' I) (u : I) : dt.ixBack lay zero one ⋯ st (lay.cell u) Slot.mir = bitVal zero one (st.mir u)

A coarse background's mirror bit, at a register: the mirror at that register.

theorem DescriptiveComplexity.Draw.Data.ixBack_pdd_cell_eq {L : FirstOrder.Language} {dt : Data L} {A R' P' I : Type} {lay : Layout dt A R' P' I} {zero one : A} (hinj : Function.Injective lay.cell) (st : TapeSt dt A R' P' I) (u : I) : dt.ixBack lay zero one ⋯ st (lay.cell u) Slot.pdd = bitVal zero one (∀ (j : Fin dt.dd), dt.dd0 ≤ ↑j → lay.arg u j = zero)

A coarse background's padding flag, at a register: the register's tuple is zero above dd₀.

theorem DescriptiveComplexity.Draw.Data.ixBack_name_cell_eq {L : FirstOrder.Language} {dt : Data L} {A R' P' I : Type} {lay : Layout dt A R' P' I} {zero one : A} (hinj : Function.Injective lay.cell) (st : TapeSt dt A R' P' I) (u : I) (j : Fin dt.dd0) : dt.ixBack lay zero one ⋯ st (lay.cell u) (Slot.name j) = lay.arg u (Fin.castLE ⋯ j)

A coarse background's name slots, at a register: the register's own tuple.

theorem DescriptiveComplexity.Draw.Data.ixBack_val_cell_eq {L : FirstOrder.Language} {dt : Data L} {A R' P' I : Type} {lay : Layout dt A R' P' I} {zero one : A} (hinj : Function.Injective lay.cell) (st : TapeSt dt A R' P' I) (u : I) : dt.ixBack lay zero one ⋯ st (lay.cell u) Slot.val = bitVal zero one (st.val u)

A coarse background's VAL bit, at a register: VAL at that register.

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.

theorem DescriptiveComplexity.Draw.Data.wellShapedIG_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.wellShapedIG zero one b (dt.ixBack lay zero one ⋯ st (lay.cell u)) ↔ tagBlk (elt u).1 = some b → ixAddr elt st.val (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))

An inner gate's shape test is the elementwise one too: the same four slots, with VAL where the outer gate reads the mirror.

theorem DescriptiveComplexity.Draw.Data.ix_gate_trichotomy {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] [Nonempty A] [L.Structure A] {I : Type} {lay : Layout dt A R' P' I} {elt : I → Univ A R' P' dt.KIx dt.dd} {zero one : A} (RF : RegFile (Univ A R' P' dt.KIx dt.dd)) (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) (hlin : IsLinOrd WMLe) (st : TapeSt dt A R' P' I) (b' : Fin dt.ko ⊕ Fin dt.ki) : IsEnc dt.ly zero one (wmBlk (ixAddr elt st.mir) (Tag.arg (toLex b'))) ∨ (∃ (u₀ : I), ¬dt.wellShapedG zero one b' (dt.ixBack lay zero one ⋯ st (lay.cell u₀))) ∨ (∀ (u : I), dt.wellShapedG zero one b' (dt.ixBack lay zero one ⋯ st (lay.cell u))) ∧ ¬((∀ (t' : dt.X.Tag), wmBlk (ixAddr elt st.mir) (Tag.arg (toLex b')) (encTagTup dt.ly zero one t') ↔ t' = dt.dspTagOf zero one (wmBlk (ixAddr elt st.mir) (Tag.arg (toLex b')))) ∧ ExpExpansion.DomHolds (dt.dspTagOf zero one (wmBlk (ixAddr elt st.mir) (Tag.arg (toLex b'))), decRho dt.ly zero one (wmBlk (ixAddr elt st.mir) (Tag.arg (toLex b')))))

The gates' trichotomy at a coarse file: either the block of the mirror's address is an encoding, or some register fails the shape test, or every register passes it and the tag half fails. This is DescriptiveComplexity.Draw.Data.gate_trichotomy read at a file whose registers are not the elements: the shape test is the same question (wellShapedG_ixBack_iff), and what carries the failing witness across costs nothing: an element that fails the shape test is one the address holds, so it is a register's element already, and no file has to have a register for every element of a block.