Soundness of the inductive-counting machine

Every accepting run of DescriptiveComplexity.InductiveCounting.CfgStep proves what it claims: no target is reachable from a source. The proof is a phase-indexed invariant, DescriptiveComplexity.InductiveCounting.Inv, preserved by every transition.

The delicate part is the inner loop, where the machine guesses which nodes belong to the current layer. A guess is certified, so the guessed set is always a subset of the layer; what rules out a guess that is too small is the count: the invariant records that the counter is at most the number of layer nodes already scanned, and that it is strictly below that number as soon as a node that would have mattered – a target, or a node putting the outer node into the next layer – has been skipped (DescriptiveComplexity.InductiveCounting.InnerInv, last clause). At the end of the scan the counter is checked against |Rset d|, which leaves no room for a skipped node.

Reading a configuration

@[simp]

theorem DescriptiveComplexity.InductiveCounting.eW_coe_coe {V : Type} {E : V → V → Prop} {p q : V} : EW E ↑p ↑q ↔ E p q

@[simp]

theorem DescriptiveComplexity.InductiveCounting.pW_coe {V : Type} {S : V → Prop} {p : V} : PW S ↑p ↔ S p

The invariant

Two steps of the inner loop

Preservation, phase by phase

Soundness