What a gate's branch dispatches on

A gate block's branch checkpoint dispatches on the tag its witness flags decode. The decoding itself (DescriptiveComplexity.Draw.Data.GateTagsAre) is one-hotness of finitely many control flags, so it is definable outright. The total dispatch (DspTagsAre) adds a default branch for the block values no point encodes, and that branch names a tag – which the interpretation may only do if the tag is the same at every instance.

DescriptiveComplexity.Draw.Data.defTag is chosen from a nonemptiness of the tags rather than from a point, exactly so that it is – by proof irrelevance, the structure that witnessed the tags inhabited does not survive into the value – and DescriptiveComplexity.Draw.Data.uConst_defTag is that fact: one environment is all it takes, and every other names the same tag.

theorem DescriptiveComplexity.Draw.Data.uGDefinable_gateTagsAre {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] (hc : Fintype.card dt.X.Tag ≤ dt.ntgDim) (t : dt.X.Tag) : UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => dt.GateTagsAre e.one hc t f

A gate's decoding is definable: one-hotness of the witness flags.

theorem DescriptiveComplexity.Draw.Data.uConst_defTag {L : FirstOrder.Language} {dt : Data L} (e₀ : Env L) : UConst fun (e : Env L) => dt.defTag

The default tag is the same at every instance: it is Classical's choice at a Prop, so which structure witnessed the tags inhabited does not survive into it. One environment is all it takes to name it.

theorem DescriptiveComplexity.Draw.Data.uGDefinable_dspTagsAre {L : FirstOrder.Language} {dt : Data L} [Fintype dt.SlotIx] (hc : Fintype.card dt.X.Tag ≤ dt.ntgDim) (e₀ : Env L) (t : dt.X.Tag) : UGDefinable fun (e : Env L) (f : dt.CtlIx → e.α) (x : dt.SlotIx → e.α) => dt.DspTagsAre e.one hc t f

The total dispatch is definable: its genuine branch is the decoding, and its default branch names a tag no instance can move.