Relative lower bounds from necessary source values

SourceSupport says that a selected subset of a supplied family determines the target. sourceSupportSize minimizes the number of selected sources, independently of a circuit basis. Weighted frontier counting then bounds this semantic minimum by the number of outputs plus the circuit cost.

def Algebraic.SourceSupport {X : Sort u_1} {m : ℕ} {U : Sort u_2} {n : ℕ} (target : X → Fin m → U) (sources : X → Fin n → U) (selected : Finset (Fin n)) : Prop

Agreement on selected supplied values forces agreement of the target.

Equations

• Algebraic.SourceSupport target sources selected = ∀ (x y : X), (∀ i ∈ selected, sources x i = sources y i) → target x = target y

noncomputable def Algebraic.sourceSupportSize {X : Sort u_1} {m : ℕ} {U : Sort u_2} {n : ℕ} (target : X → Fin m → U) (sources : X → Fin n → U) : ℕ∞

Fewest source coordinates determining the target, or infinity if even the whole supplied family does not determine it.

Equations

• Algebraic.sourceSupportSize target sources = ⨅ (selected : Finset (Fin n)), ⨅ (_ : Algebraic.SourceSupport target sources selected), ↑selected.card

theorem Algebraic.sourceSupportSize_le {X : Sort u_1} {m : ℕ} {U : Sort u_2} {n : ℕ} {target : X → Fin m → U} {sources : X → Fin n → U} {selected : Finset (Fin n)} (determines : SourceSupport target sources selected) : sourceSupportSize target sources ≤ ↑selected.card

Any determining set bounds the minimum number of required source values.

theorem Algebraic.le_sourceSupportSize {X : Sort u_1} {m : ℕ} {U : Sort u_2} {n : ℕ} {target : X → Fin m → U} {sources : X → Fin n → U} (lower : ℕ∞) (bounded : ∀ (selected : Finset (Fin n)), SourceSupport target sources selected → lower ≤ ↑selected.card) : lower ≤ sourceSupportSize target sources

A uniform bound on determining sets bounds the semantic minimum.

theorem Algebraic.sourceSupportSize_le_iff {X : Sort u_1} {m : ℕ} {U : Sort u_2} {n : ℕ} (target : X → Fin m → U) (sources : X → Fin n → U) (budget : ℕ) : sourceSupportSize target sources ≤ ↑budget ↔ ∃ (selected : Finset (Fin n)), SourceSupport target sources selected ∧ selected.card ≤ budget

A finite source budget is witnessed by a determining set.

theorem Cslib.Circuits.Circuit.ComputesFrom.sourceSupport {σ : Signature} {n m : ℕ} {U : Type u_2} {X : Sort u_3} {circuit : Circuit σ n m} {interpretation : Interpretation σ U} {target : X → Fin m → U} {sources : X → Fin n → U} (computes : circuit.ComputesFrom interpretation target sources) : Algebraic.SourceSupport target sources circuit.inputSupport

Every relative implementation uses a source subset determining its target.

theorem Cslib.Circuits.Circuit.card_inputSupport_le_cost {σ : Signature} {n m : ℕ} (circuit : Circuit σ n m) (weight : Algebraic.OperationCost σ) (bounded : ∀ (op : σ.Op), σ.Arity op ≤ weight op + 1) : circuit.inputSupport.card ≤ m + circuit.cost weight

The weighted frontier bound specialized to all designated output wires.

theorem Cslib.Circuits.Circuit.sourceSupportSize_le_relativeCostComplexity {σ : Signature} {U : Type u_2} {X : Sort u_3} {m n : ℕ} (interpretation : Interpretation σ U) (weight : Algebraic.OperationCost σ) (bounded : ∀ (op : σ.Op), σ.Arity op ≤ weight op + 1) (target : X → Fin m → U) (sources : X → Fin n → U) : Algebraic.sourceSupportSize target sources ≤ ↑m + relativeCostComplexity interpretation weight target sources

Necessary supplied values lower-bound weighted relative complexity.

theorem Cslib.Circuits.Circuit.sourceSupportSize_le_size {σ : Signature} {n m : ℕ} {U : Type u_2} {X : Sort u_3} {b : ℕ} {circuit : Circuit σ n m} {interpretation : Interpretation σ U} {target : X → Fin m → U} {sources : X → Fin n → U} (computes : circuit.ComputesFrom interpretation target sources) (bounded : circuit.FanInAtMost b) : Algebraic.sourceSupportSize target sources ≤ ↑(m + (b - 1) * circuit.size)

A bounded-fan-in implementation must touch enough supplied values.

theorem Cslib.Circuits.Circuit.sourceSupportSize_le_relativeGateComplexity {σ : Signature} {U : Type u_2} {X : Sort u_3} {m n : ℕ} (interpretation : Interpretation σ U) (b : ℕ) (positive : 2 ≤ b) (bounded : ∀ (op : σ.Op), σ.Arity op ≤ b) (target : X → Fin m → U) (sources : X → Fin n → U) : Algebraic.sourceSupportSize target sources ≤ ↑m + ↑(b - 1) * relativeGateComplexity interpretation target sources

The semantic source count bounds minimum gate complexity for any basis of fan-in at most b, with b ≥ 2 so infinite complexities cause no 0 * ∞.