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

theorem DescriptiveComplexity.Draw.Data.encTup_pdd {L : FirstOrder.Language} (dt : Data L) {A : Type} {zero one : A} (d : PtCode dt.X) (pay : Fin (blockArityBound dt.X.B) → A) {j : Fin dt.dd} (hj : dt.dd0 ≤ ↑j) : encTup dt.ly zero one d pay j = zero

An encoded tuple is canonically padded: the layout inhabits the first dd₀ coordinates, so everything above them is the designated zero.

theorem DescriptiveComplexity.Draw.Data.eq_encTup_of_marks {L : FirstOrder.Language} (dt : Data L) {A : Type} {zero one : A} {u2 : Fin dt.dd → A} {d : PtCode dt.X} {pay : Fin (blockArityBound dt.X.B) → A} (hpdd : ∀ (j : Fin dt.dd), dt.dd0 ≤ ↑j → u2 j = zero) (hname : ∀ (j : Fin dt.dd0), u2 (Fin.castLE ⋯ j) = encTup dt.ly zero one d pay (Fin.castLE ⋯ j)) : u2 = encTup dt.ly zero one d pay

A padded tuple whose name coordinates spell an encoded tuple is that tuple: the coordinates above dd₀ agree because both sides are zero there.

The per-cell questions, read

theorem DescriptiveComplexity.Draw.Data.shape_marks_iff {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)] (RF : RegFile (Univ A R P dt.KIx dt.dd)) {zero one : A} (hzo : zero ≠ one) (hlin : IsLinOrd WMLe) (st : TapeStD dt A R P) (u : Univ A R P dt.KIx dt.dd) : dt.back RF.cell zero one ⋯ st (RF.cell u) Slot.pdd = one ∧ ((∃ (t : dt.X.Tag), ∀ (j : Fin dt.dd0), dt.back RF.cell zero one ⋯ st (RF.cell u) (Slot.name 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), dt.back RF.cell zero one ⋯ st (RF.cell u) (Slot.name j) = encAsgTup dt.ly zero one i w (Fin.castLE ⋯ j)) ↔ (∃ (t : dt.X.Tag), u.2 = encTagTup dt.ly zero one t) ∨ ∃ (i : dt.X.B.ι) (w : Fin (dt.X.B.arity i) → A), u.2 = encAsgTup dt.ly zero one i w

The shape clause of the marks is the shape of the cell's tuple: the padding mark together with a name-coordinate match is full equality with the encoded tuple.

theorem DescriptiveComplexity.Draw.Data.wellShapedG_back_iff {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)] (RF : RegFile (Univ A R P dt.KIx dt.dd)) {zero one : A} (hzo : zero ≠ one) (hlin : IsLinOrd WMLe) (st : TapeStD dt A R P) (b' : Fin dt.ko ⊕ Fin dt.ki) (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.1 = Tag.arg (toLex b') → st.mir u → (∃ (t : dt.X.Tag), u.2 = encTagTup dt.ly zero one t) ∨ ∃ (i : dt.X.B.ι) (w : Fin (dt.X.B.arity i) → A), u.2 = encAsgTup dt.ly zero one i w

The outer file test's question, read off the marks: if the cell is of the gated block and belongs to MIRROR, its tuple is a witness or a member shape.

theorem DescriptiveComplexity.Draw.Data.igTest_iff {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)] (RF : RegFile (Univ A R P dt.KIx dt.dd)) {zero one : A} (hzo : zero ≠ one) (hlin : IsLinOrd WMLe) (stV : TapeStD dt A R P) (b' : Fin dt.ko ⊕ Fin dt.ki) (u : Univ A R P dt.KIx dt.dd) : dt.igTest RF zero one stV b' u ↔ u.1 = Tag.arg (toLex b') → stV.val u → (∃ (t : dt.X.Tag), u.2 = encTagTup dt.ly zero one t) ∨ ∃ (i : dt.X.B.ι) (w : Fin (dt.X.B.arity i) → A), u.2 = encAsgTup dt.ly zero one i w

The inner file test's question, read off the marks: the same at the VAL register.

The shape clause of a block value

theorem DescriptiveComplexity.Draw.Data.forall_shape_iff_of_cells {L : FirstOrder.Language} (dt : Data L) {A R P : Type} {zero one : A} {m : Univ A R P dt.KIx dt.dd → Prop} {b' : Fin dt.ko ⊕ Fin dt.ki} (hcell : ∀ (u : Univ A R P dt.KIx dt.dd), u.1 = Tag.arg (toLex b') → m u → (∃ (t : dt.X.Tag), u.2 = encTagTup dt.ly zero one t) ∨ ∃ (i : dt.X.B.ι) (w : Fin (dt.X.B.arity i) → A), u.2 = encAsgTup dt.ly zero one i w) (w : Fin dt.dd → A) : wmBlk m (Tag.arg (toLex b')) w → (∃ (t : dt.X.Tag), w = encTagTup dt.ly zero one t) ∨ ∃ (i : dt.X.B.ι) (w' : Fin (dt.X.B.arity i) → A), w = encAsgTup dt.ly zero one i w'

The per-cell questions of a block answer for its value: every cell of block b' in the register is well-shaped exactly when every member of the block value is a witness or a member shape.

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

theorem DescriptiveComplexity.Draw.Data.testOf_of_encMap {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)] (RF : RegFile (Univ A R P dt.KIx dt.dd)) [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} {p : dt.X.Map A} (hS : wmBlk st.mir (Tag.arg (toLex b')) = encMap dt.ly zero one p) (u : Univ A R P dt.KIx dt.dd) : dt.wellShapedG zero one b' (dt.back RF.cell zero one ⋯ st (RF.cell u))

At an encoding every cell passes the outer file test.

theorem DescriptiveComplexity.Draw.Data.wit_of_encMap {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [L.Structure A] {zero one : A} (hzo : zero ≠ one) {m : Univ A R P dt.KIx dt.dd → Prop} {b' : Fin dt.ko ⊕ Fin dt.ki} {p : dt.X.Map A} (hS : wmBlk m (Tag.arg (toLex b')) = encMap dt.ly zero one p) (t' : dt.X.Tag) : wmBlk m (Tag.arg (toLex b')) (encTagTup dt.ly zero one t') ↔ t' = (↑p).1

At an encoding the witness is one-hot at the point's tag.

theorem DescriptiveComplexity.Draw.Data.dspTagOf_encMap {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [Finite A] [Nonempty A] [L.Structure A] {zero one : A} (hzo : zero ≠ one) {m : Univ A R P dt.KIx dt.dd → Prop} {b' : Fin dt.ko ⊕ Fin dt.ki} {p : dt.X.Map A} (hS : wmBlk m (Tag.arg (toLex b')) = encMap dt.ly zero one p) : dt.dspTagOf zero one (wmBlk m (Tag.arg (toLex b'))) = (↑p).1

At an encoding the dispatch is the point's tag.

theorem DescriptiveComplexity.Draw.Data.domHolds_of_encMap {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [LinearOrder A] [L.Structure A] {zero one : A} (hzo : zero ≠ one) {m : Univ A R P dt.KIx dt.dd → Prop} {b' : Fin dt.ko ⊕ Fin dt.ki} {p : dt.X.Map A} (hS : wmBlk m (Tag.arg (toLex b')) = encMap dt.ly zero one p) : ExpExpansion.DomHolds ((↑p).1, decRho dt.ly zero one (wmBlk m (Tag.arg (toLex b'))))

At an encoding the domain condition holds of the decoded assignment – the point carries it.

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.igTest_of_encMap {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)] (RF : RegFile (Univ A R P dt.KIx dt.dd)) [L.Structure A] {zero one : A} (hzo : zero ≠ one) (hlin : IsLinOrd WMLe) {stV : TapeStD dt A R P} {b' : Fin dt.ko ⊕ Fin dt.ki} {p : dt.X.Map A} (hS : wmBlk stV.val (Tag.arg (toLex b')) = encMap dt.ly zero one p) (u : Univ A R P dt.KIx dt.dd) : dt.igTest RF zero one stV b' u

Every cell of an encoded VAL block passes the inner file test.

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.