What the drawn circuit computes

The intended value of each gate of DescriptiveComplexity.Problems.Cvp.Hardness.Interp, and the two halves of the statement that the circuit computes it.

The building half (this file's first section) walks the chains: each gate's value follows from its inputs', by induction along the order for the two chains and by strong induction on the rank of the stage for the propagation, whose gates at stage s read the propagation gates one stage below. The inverting half is the converse, and it is one induction on the derivation DescriptiveComplexity.GateVal: whatever the circuit derives, it derives for the intended reason, because the wiring lemmas leave a gate no other input to have derived it from.

Only the true rail carries information; the false rail is where the constant 0 and the unfired chains sit, and nothing downstream reads it, so the inverting half states nothing about it.

The intended values

def DescriptiveComplexity.CvpVal.BdVal {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (c y s : A) : Prop

The value of a conjunction-chain gate: every negative literal of c up to y is forced within orank s rounds.

Equations

• DescriptiveComplexity.CvpVal.BdVal c y s = ∀ y' ≤ y, DescriptiveComplexity.SatOcc.NegIn c y' → DescriptiveComplexity.ForcedIn (DescriptiveComplexity.orank s) y'

def DescriptiveComplexity.CvpVal.HdVal {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (x c s : A) : Prop

The value of a propagation-chain gate: some clause up to c forces x in one round from the stage orank s.

Equations

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

def DescriptiveComplexity.CvpVal.BdTopVal {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (c y : A) : Prop

The value of a top-stage conjunction-chain gate: every negative literal of c up to y is forced at all.

Equations

• DescriptiveComplexity.CvpVal.BdTopVal c y = ∀ y' ≤ y, DescriptiveComplexity.SatOcc.NegIn c y' → DescriptiveComplexity.Forced y'

def DescriptiveComplexity.CvpVal.GlVal {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (c : A) : Prop

The value of a goal-chain gate: the instance is not Horn, or some clause up to c is a goal clause whose negative literals are all forced.

Equations

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

Reading the values off the stages

theorem DescriptiveComplexity.CvpVal.hdVal_top {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {M : A} (hM : ∀ (a : A), a ≤ M) (x s : A) : HdVal x M s ↔ ForcedIn (orank s + 1) x

At the top of the clause walk, a propagation gate is one round of unit propagation.

theorem DescriptiveComplexity.CvpVal.bdVal_top {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {M : A} (hM : ∀ (a : A), a ≤ M) (c s : A) : BdVal c M s ↔ ∀ (y : A), SatOcc.NegIn c y → ForcedIn (orank s) y

At the top of the literal walk, a conjunction gate is the body condition.

theorem DescriptiveComplexity.CvpVal.forced_iff_top {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {M : A} (hM : ∀ (a : A), a ≤ M) (x : A) : Forced x ↔ ForcedIn (orank M + 1) x

The last stage is the fixed point: Nat.card A rounds of propagation force everything that is forced at all.

Building a derivation

Each gate evaluates to 1 as soon as its intended value holds.

theorem DescriptiveComplexity.CvpVal.gateVal_tt {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] {m : A} (hm : ∀ (a : A), m ≤ a) : GateVal true (CvpDraw.ttPt m)

The constant 1 gate derives 1.

theorem DescriptiveComplexity.CvpVal.gateVal_stage {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] {m M : A} (hm : ∀ (a : A), m ≤ a) (hM : ∀ (a : A), a ≤ M) (n : ℕ) (s : A) : orank s = n → (∀ (c y : A), BdVal c y s → GateVal true (CvpDraw.bdPt c y s)) ∧ ∀ (x c : A), HdVal x c s → GateVal true (CvpDraw.hdPt x c s)

The two chains of one stage, by strong induction on the rank of the stage: the conjunction chains of a stage read the propagation gates of the stage below, and the propagation chain of a stage reads the conjunction chains of its own.

theorem DescriptiveComplexity.CvpVal.gateVal_bdTop {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {m M : A} (hm : ∀ (a : A), m ≤ a) (hM : ∀ (a : A), a ≤ M) (c y : A) (hval : BdTopVal c y) : GateVal true (CvpDraw.bdTopPt m c y)

A conjunction gate of the top stage evaluates to 1 when its value holds.

theorem DescriptiveComplexity.CvpVal.gateVal_gl {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {m M : A} (hm : ∀ (a : A), m ≤ a) (hM : ∀ (a : A), a ≤ M) (c : A) (hval : GlVal c) : GateVal true (CvpDraw.glPt m c)

A goal-chain gate evaluates to 1 when its value holds.

Inverting a derivation

Whatever the circuit derives on the true rail, it derives for the intended reason: the wiring leaves a gate no other input to have derived it from.

def DescriptiveComplexity.CvpVal.Val {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (p : cvpInterp.Map A) : Prop

The intended value of a point, by tag. The constant 1 carries no information and the constant 0 is never derived, which is what makes the induction go through.

Equations

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

theorem DescriptiveComplexity.CvpVal.val_of_gateVal {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {m M : A} (hm : ∀ (a : A), m ≤ a) (hM : ∀ (a : A), a ≤ M) {b : Bool} {p : cvpInterp.Map A} : GateVal b p → b = true → Val p

Nothing else evaluates to 1. By induction on the derivation: every rule that can fire at a gate of the drawn circuit fires for the intended reason. The false rail carries no information and is not tracked.