Every digit-definable function reduces to the number written by a circuit

DescriptiveComplexity.DigitLFPDef.orderedParsimonious: a function whose binary digits are relations of a least fixed point (DescriptiveComplexity.DigitDefinable) reduces to DescriptiveComplexity.CircuitNumber by an ordered parsimonious reduction, the circuit being the one drawn from the rules (DescriptiveComplexity.CircNum.drawInterp).

• The circuit evaluates the fixed point (DescriptiveComplexity.CircNum.gateVal_atom_iff): the gate of an atom derives 1 exactly when the rules derive the atom. One direction rebuilds a derivation of the rules as a derivation of the gates, link by link along a conjunction chain (DescriptiveComplexity.CircNum.gateVal_of_derives); the other inverts a derivation of the gates, every rule that can fire at a gate of the drawn circuit firing for the intended reason (DescriptiveComplexity.CircNum.val_of_gateVal).
• The outputs are the digits: the output gates are the canonically padded atoms of the relations holding the digits, and padding preserves the lexicographic order (DescriptiveComplexity.CircNum.tupLeLex_pad), so the outputs are compared as their positions are (DescriptiveComplexity.CircNum.below_bitPt), and the number is read off the positions (DescriptiveComplexity.finsum_digits_eq).

Padding and the lexicographic order

theorem DescriptiveComplexity.CircNum.tupLeLex_pad {A : Type} {D m : ℕ} [LinearOrder A] (a₀ : A) (h : m ≤ D) (y x : Fin m → A) : tupLeLex (pad a₀ y) (pad a₀ x) ↔ tupLeLex y x

Padding preserves the lexicographic order.

What the gates derive

def DescriptiveComplexity.CircNum.Val {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {prog : HornProgram (L.sum FirstOrder.Language.order) B k} {c : ℕ} {bit : Fin c → B.ι} (p : (drawInterp prog bit).Map A) : Prop

What a gate deriving 1 means: an atom is canonically padded and derived by the rules; a link of a conjunction chain has every body atom from its position on derived.

Equations

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

theorem DescriptiveComplexity.CircNum.val_of_gateVal {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {prog : HornProgram (L.sum FirstOrder.Language.order) B k} {c : ℕ} {bit : Fin c → B.ι} {b : Bool} {p : (drawInterp prog bit).Map A} : GateVal b p → b = true → Val p

Nothing else evaluates to 1. By induction on the derivation of the gates: 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.

theorem DescriptiveComplexity.CircNum.gateVal_of_derives {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {prog : HornProgram (L.sum FirstOrder.Language.order) B k} {c : ℕ} {bit : Fin c → B.ι} {a₀ : A} (h₀ : IsBot a₀) (q : (i : B.ι) × (Fin (B.arity i) → A)) : Derives prog q → GateVal true (atomTag q.fst, pad a₀ q.snd)

Every atom the rules derive has its gate deriving 1: a derivation of the rules is rebuilt as a derivation of the gates, the conjunction chain of each rule instance being climbed from its end.

theorem DescriptiveComplexity.CircNum.gateVal_atom_iff {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {prog : HornProgram (L.sum FirstOrder.Language.order) B k} {c : ℕ} {bit : Fin c → B.ι} {a₀ : A} (h₀ : IsBot a₀) (i : B.ι) (w : Fin (clauseDim B k) → A) : GateVal true (atomTag i, w) ↔ Canon (B.arity i) w ∧ Derives prog ⟨i, pref ⋯ w⟩

The circuit evaluates the fixed point: the gate of an atom derives 1 exactly when it is canonically padded and the rules derive the atom.

The outputs are the digits

theorem DescriptiveComplexity.CircNum.tupLeLex_iff_le {A : Type} [LinearOrder A] {m : ℕ} (y x : Fin m → A) : tupLeLex y x ↔ toLex y ≤ toLex x

noncomputable def DescriptiveComplexity.CircNum.bitPt {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} (prog : HornProgram (L.sum FirstOrder.Language.order) B k) {c : ℕ} (bit : Fin c → B.ι) {ℓ : ℕ} (hℓ : ∀ (τ : Fin c), B.arity (bit τ) = ℓ) (a₀ : A) (q : Lex (Fin c × Lex (Fin ℓ → A))) : (drawInterp prog bit).Map A

The output gate of a position: the atom of its tuple in the relation variable of its group, canonically padded.

Equations

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

theorem DescriptiveComplexity.CircNum.bitPt_injective {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} {prog : HornProgram (L.sum FirstOrder.Language.order) B k} {c : ℕ} {bit : Fin c → B.ι} {ℓ : ℕ} (hinj : Function.Injective bit) (hℓ : ∀ (τ : Fin c), B.arity (bit τ) = ℓ) (a₀ : A) : Function.Injective (bitPt prog bit hℓ a₀)

theorem DescriptiveComplexity.CircNum.below_bitPt {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {prog : HornProgram (L.sum FirstOrder.Language.order) B k} {c : ℕ} {bit : Fin c → B.ι} {a₀ : A} {ℓ : ℕ} (hinj : Function.Injective bit) (hℓ : ∀ (τ : Fin c), B.arity (bit τ) = ℓ) (q' q : Lex (Fin c × Lex (Fin ℓ → A))) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.ncBelow ![bitPt prog bit hℓ a₀ q', bitPt prog bit hℓ a₀ q] ↔ q' ≤ q

The gates of the positions are compared as the positions are.

theorem DescriptiveComplexity.CircNum.circuitNumber_drawInterp {L : FirstOrder.Language} {B : SOBlock} {k : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {prog : HornProgram (L.sum FirstOrder.Language.order) B k} {c : ℕ} {bit : Fin c → B.ι} {a₀ : A} {ℓ : ℕ} (hinj : Function.Injective bit) (hℓ : ∀ (τ : Fin c), B.arity (bit τ) = ℓ) [Finite A] (h₀ : IsBot a₀) : circuitNumber ((drawInterp prog bit).Map A) = ∑ᶠ (q : Lex (Fin c × Lex (Fin ℓ → A))), if lfpAssign prog (bit (ofLex q).1) fun (k : Fin (B.arity (bit (ofLex q).1))) => ofLex (ofLex q).2 (Fin.cast ⋯ k) then 2 ^ orank q else 0

The drawn circuit writes the number whose digits are the relations bit τ of the least fixed point.

The reduction

noncomputable def DescriptiveComplexity.DigitLFPDef.orderedParsimonious {L : FirstOrder.Language} [L.IsRelational] {C : CountingProblem L} (d : DigitLFPDef L) (h : ∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A] [Finite A] [Nonempty A], C.Count A = d.value A) : OrderedParsimoniousReduction C CircuitNumber

A function whose binary digits are relations of a least fixed point reduces to the number written by a circuit, by drawing the circuit of the rules inside the instance.

Equations

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

theorem DescriptiveComplexity.DigitDefinable.nonempty_orderedParsimonious {L : FirstOrder.Language} [L.IsRelational] {C : CountingProblem L} (h : DigitDefinable C) : Nonempty (OrderedParsimoniousReduction C CircuitNumber)

Every digit-definable problem parsimoniously reduces to the number written by a circuit.