A gated position's semantic pack, at an arbitrary file and phase

What a leg of the evaluation is run with is a pack per position and VAL content: the points the position's argument blocks encode. This file builds them – it does not assume them – from the two bridges a coarse file needs (hpassEnc, hgateEnc) and nothing else, so the space-bounded program and the clocked one get their packs from the same place.

The construction is one step: a gated position's blocks are encodings (ixIsEnc_of_gatedAt, the bridge read forwards), and ixPassSem turns encodings into a pack. ixGatedSem is that pack at the state the matrix's atoms run at, ixGatedSem₀ at the round's own, and ixGatedSem_eq_semCastT says the first is the second transported – which is what the VAL loop's bridge asks of a threaded family. The transport lemmas under them (ixPassW_congr, ixKindSemCast_passSem, and the one-pack family) say the same thing once: a pack sees the state through the mirror and VAL alone.

What a gated position knows

The branch DescriptiveComplexity.Draw.Data.ixGatedAt takes is not merely the one where the machine runs the machinery: it is the one where the argument blocks are encodings, which is what a semantic pack needs to exist at all. DescriptiveComplexity.Draw.Data.gate_trichotomy says the three legs are exhaustive; read in the other direction it says a gated position's blocks encode points.

theorem DescriptiveComplexity.Draw.Data.ixIsEnc_of_gatedAt {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.Structure A] (hgateEnc : ∀ (j : Fin dt.nv) (st : TapeSt dt A R P I), dt.ixGatedAt F j st ↔ ∀ (ℓ : Fin (dt.arOf (dt.varAt j))), IsEnc dt.ly PR.zero PR.one (wmBlk (ixAddr elt st.mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))))) (j : Fin dt.nv) (st : TapeSt dt A R P I) (hg : dt.ixGatedAt F j st) (ℓ : Fin (dt.arOf (dt.varAt j))) : IsEnc dt.ly PR.zero PR.one (wmBlk (ixAddr elt st.mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))))

A gated position's argument blocks are encodings – the converse of testOf_of_encMap/wit_of_encMap/domHolds_of_encMap, off the trichotomy. This is what makes a position's semantic pack constructible rather than assumed: at a junk position no pack exists, and at a gated one the points are the blocks' own.

noncomputable def DescriptiveComplexity.Draw.Data.ixGatedSem {L : FirstOrder.Language} (dt : Data L) {A R P : Type} [Fintype dt.SlotIx] [LinearOrder A] [LinearOrder R] [LinearOrder P] [FirstOrder.Language.wide.Structure (Univ A R P dt.KIx dt.dd)] [Finite A] {PR : Prog A R P dt.CtlIx dt.SlotIx dt.KIx dt.dd} {I : Type} (F : LaidFile dt A R P I) {elt : I → Univ A R P dt.KIx dt.dd} [Nonempty A] [L.Structure A] (hpassEnc : ∀ (vi : dt.VarIx) (stV : TapeSt dt A R P I) (ℓ : Fin (dt.nIn vi)), dt.ixIGPassP F PR.zero PR.one vi stV ℓ ↔ IsEnc dt.ly PR.zero PR.one (wmBlk (ixAddr elt stV.val) (Tag.arg (toLex (dt.igBlk vi ℓ))))) (hgateEnc : ∀ (j : Fin dt.nv) (st : TapeSt dt A R P I), dt.ixGatedAt F j st ↔ ∀ (ℓ : Fin (dt.arOf (dt.varAt j))), IsEnc dt.ly PR.zero PR.one (wmBlk (ixAddr elt st.mir) (Tag.arg (toLex (Sum.inl (Fin.castLE ⋯ ℓ)))))) (_hzo : PR.zero ≠ PR.one) (_hlin : IsLinOrd WMLe) {v : Univ A R P dt.KIx dt.dd → Prop} {ιV : Type} (mV : ιV → I → Prop) (j : Fin dt.nv) (st : TapeSt dt A R P I) (hg : dt.ixGatedAt F j st) (p : dt.IxScratch A R P I) (a : ιV) (hp : ∀ (ℓ : Fin (dt.nIn (dt.varAt j))), dt.ixIGPassP F PR.zero PR.one (dt.varAt j) (ixVarRdSt st p (mV a)) ℓ) (b : Fin (dt.natOf (dt.varAt j))) : dt.IxKindSem PR.zero PR.one (dt.varAt j) (dt.ixMatSt (dt.varAt j) (ixVarRdSt st p (mV a)) v ↑b) elt (dt.kindOf (dt.varAt j) b)

A gated position's semantic pack, built – not assumed. The blocks are encodings (ixIsEnc_of_gatedAt), so their points are the valuation the pass decodes, and ixPassSem builds the pack there; ixKindSemCast carries it to the state the matrix's atoms run at, which differs from it in the two scratch registers alone. This is what a branched leg's semT is.

Equations

• One or more equations did not get rendered due to their size.

The gates' bridge, proved

hgateEnc is a hypothesis of the layers above because an arbitrary file need not have a register for every element it is asked about. Where it does – any file laid by blocks and tuples – the bridge is the elementwise one (gate_trichotomy and testOf_of_encMap) read through DescriptiveComplexity.Draw.Data.wellShapedG_ixBack_iff.