Finite average-case circuit bounds

theorem Complexity.Frontier.agreement_le_layout {σ : Cslib.Circuits.Signature} {n : ℕ} (I : Cslib.Circuits.Interpretation σ Bool) (c : Cslib.Circuits.Circuit σ n 1) {f : (Fin n → Bool) → Bool} {K : ℕ} {β : ℝ} (hf : RectangleBias f K β) (hK : 1 < K) (hβ : 0 ≤ β) (hfan : c.FanInAtMost 2) (π : Layout (Compiler.Vertex c.program c.outputs)) {w : ℕ} (hw : ∀ (t : ℕ), ((constraintNetwork I {true} c).frontier π t).ncard ≤ w) : (agreement f fun (x : Fin n → Bool) => c.eval I x 0) ≤ (1 + β) / 2 + ↑((K - 1) ^ 2 * (Nat.card (Compiler.Vertex c.program c.outputs) * 2 ^ (w + 4) + 2 ^ (constraintNetwork I {true} c).readᶜ.ncard)) / 2 ^ n

Bias on the two output classes is bounded by the size of any frontier layout.

theorem Complexity.Frontier.agreement_le_unused {σ : Cslib.Circuits.Signature} {n : ℕ} (I : Cslib.Circuits.Interpretation σ Bool) (c : Cslib.Circuits.Circuit σ n 1) {f : (Fin n → Bool) → Bool} {K : ℕ} {β : ℝ} (hf : RectangleBias f K β) (hK : 1 < K) (hβ : 0 ≤ β) (hu : K ≤ 2 ^ (constraintNetwork I {true} c).readᶜ.ncard) : (agreement f fun (x : Fin n → Bool) => c.eval I x 0) ≤ (1 + β) / 2 + 2 * ↑K ^ 2 / 2 ^ n

A circuit with many unread inputs has negligible advantage beyond the rectangle bias.