The gates' facts, from the marks

What the gate machinery asks – the file tests' per-cell questions, the witness one-hotness, the domain conditions – read off DescriptiveComplexity.Draw.Data.back's marks and answered by the encoding. The marks of a register cell spell the cell's own coordinates (name), its padding (pdd) and its tag's block (blk), so a file test's question is a statement about the cell, and a block value's answers are statements about the value:

• wellShapedG_back_iff / igTest_iff – the per-cell question is «if the cell is of the gated block and in the register, its tuple is a witness or a member shape», at MIRROR and at VAL;
• testOf_of_encMap, wit_of_encMap, domHolds_of_encMap, dspTagOf_encMap – at a block value that is an encoding, every gated hypothesis of DescriptiveComplexity.Draw.Data.varMachine_run holds, and the dispatch is the point's tag;
• gate_trichotomy – every block value is an encoding, has an ill-shaped register cell, or is all-shaped with the one-hot-and-domain conjunct failing at the dispatched tag: the three legs DescriptiveComplexity.Draw.Data.varLeg_run / varLegFail_run / varLegUngated_run are exhaustive;
• igPassP_iff_isEnc – the inner loop's per-level verdict is DescriptiveComplexity.Draw.IsEnc of the level's block value, the marks-to-shapes bridge the two-flag characterization was stated against.

Encoded tuples against the marks

The per-cell questions, read

The shape clause of a block value

The gated facts: at a block value that is an encoding

The trichotomy: the three legs are exhaustive

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

Every block value makes one of three landings: it is an encoding (the gated leg), some register cell of its block is ill-shaped (the shape-failing leg), or every cell is well-shaped and the one-hot-and-domain conjunct fails at the dispatched tag (the ungated leg).

The inner loop's bridge: the per-level verdict is the gate

theorem DescriptiveComplexity.Draw.Data.igPassP_iff_isEnc {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] (RF : RegFile (Univ A R P dt.KIx dt.dd)) [Nonempty A] [L.Structure A] (zero one : A) (hzo : zero ≠ one) (hlin : IsLinOrd WMLe) (vi : dt.VarIx) (stV : TapeStD dt A R P) (ℓ : Fin (dt.nIn vi)) : dt.igPassP RF zero one vi stV ℓ ↔ IsEnc dt.ly zero one (wmBlk stV.val (Tag.arg (toLex (dt.igBlk vi ℓ))))

The inner loop's per-level verdict is the gate: a level passes – its file test, the one-hot witness at the dispatched tag and the domain condition there – exactly when its block value is an encoding. The marks-to-shapes bridge of the two-flag characterization.