The drawn circuit, gate by gate

What the interpretation of DescriptiveComplexity.Problems.Cvp.Hardness.Interp marks and wires, read back as statements about named points – bdPt, hdPt … – rather than about raw tagged tuples. Two kinds of lemma are needed downstream and both are proved here once:

• the marks: which points are gates of which kind, and which point is the output;
• the wires: for each gate, an iff naming its left and right inputs, so that a derivation can be built (the mpr direction, used to evaluate the circuit) and inverted (the mp direction, used to prove that nothing else evaluates to 1).

Everything is stated relative to a minimum m and a maximum M of the universe, which a finite nonempty linear order supplies; the coordinates a tag does not use are pinned to m.

The points

The marks

The wires

Each gate names its left and its right input. The mpr direction builds a derivation, the mp direction inverts one; the constants have no input at all.