Threshold programs as block decompositions

• Program.evalFrom_eq_eval: overriding gates by their true values and feeding the other gates their true weighted input sums recovers the ordinary evaluation.
• Program.piecesAtMost_evalFrom_internal (Lemma 2): if every unfixed gate j receives the input contribution slope j * t, the gate values have at most 2 ^ r pieces as functions of t, where r counts the unfixed gates with slope j ≠ 0. Induction over the gates: on each piece of the earlier gates, the next gate is [slope * t + c ≥ 0] for one constant c, which is monotone in t and splits the piece into at most two intervals; a gate with zero slope or a fixed gate is constant on each piece.
• Program.DirectionRuns.toBlockDecomposition: a split of the gates into runs along single directions gives a block decomposition whose i-th block changes at most 2 ^ rᵢ - 1 times, rᵢ being the number of input-reading gates of the run.

theorem Algebraic.Threshold.Program.evalFrom_eq {n s : ℕ} (C : Program n s) (fixed : Finset (Fin s)) (η : Fin s → Bool) (z : Fin s → ℝ) (j : Fin s) : C.evalFrom fixed η z j = if j ∈ fixed then η j else decide (0 ≤ (z j + ∑ k : Fin s, if k < j then C.gateWeight j k * ↑(C.evalFrom fixed η z k).toNat else 0) + C.bias j)

theorem Algebraic.Threshold.Program.eval_eq_internal {n s : ℕ} (C : Program n s) (x : Fin n → Bool) (j : Fin s) : C.eval x j = decide (0 ≤ (weightedSum (C.inputWeight j) x + ∑ k : Fin s, if k < j then C.gateWeight j k * ↑(C.eval x k).toNat else 0) + C.bias j)

theorem Algebraic.Threshold.Program.evalFrom_eq_eval {n s : ℕ} (C : Program n s) {fixed : Finset (Fin s)} {η : Fin s → Bool} {z : Fin s → ℝ} {x : Fin n → Bool} (j : Fin s) (hfix : ∀ k ≤ j, k ∈ fixed → η k = C.eval x k) (hz : ∀ k ≤ j, k ∉ fixed → z k = weightedSum (C.inputWeight k) x) : C.evalFrom fixed η z j = C.eval x j

Overriding gates by their true values and feeding the other gates their true weighted input sums recovers the ordinary evaluation, gate by gate.

noncomputable def Algebraic.Threshold.Program.prefixValues {n s : ℕ} (C : Program n s) (fixed : Finset (Fin s)) (η : Fin s → Bool) (slope : Fin s → ℝ) (d : ℕ) (t : ℝ) : Fin s → Bool

The values of the first d gates, as functions of the parameter t.

Equations

• C.prefixValues fixed η slope d t j = if ↑j < d then C.evalFrom fixed η (fun (k : Fin s) => slope k * t) j else false

noncomputable def Algebraic.Threshold.Program.activeCount {s : ℕ} (fixed : Finset (Fin s)) (slope : Fin s → ℝ) (d : ℕ) : ℕ

The number of unfixed gates with a nonzero slope among the first d gates.

Equations

• Algebraic.Threshold.Program.activeCount fixed slope d = {j : Fin s | ↑j < d ∧ j ∉ fixed ∧ slope j ≠ 0}.card

theorem Algebraic.Threshold.Program.piecesAtMost_evalFrom_internal {n s : ℕ} (C : Program n s) (fixed : Finset (Fin s)) (η : Fin s → Bool) (slope : Fin s → ℝ) : PiecesAtMost (fun (t : ℝ) => C.evalFrom fixed η fun (j : Fin s) => slope j * t) (2 ^ {j : Fin s | j ∉ fixed ∧ slope j ≠ 0}.card)

Lemma 2 (pieces of a run). If every gate outside fixed receives the input contribution slope j * t, the gate values have at most 2 ^ r pieces as functions of t, where r counts the gates outside fixed with a nonzero slope.

noncomputable def Algebraic.Threshold.Program.DirectionRuns.slope {n s : ℕ} {C : Program n s} {B : ℕ} (R : C.DirectionRuns B) (i : ℕ) (j : Fin s) : ℝ

The slope of a gate of run i along the direction of the run, and zero elsewhere.

Equations

• R.slope i j = if R.run j = i ∧ C.inputWeight j ≠ 0 then ⋯.choose else 0

theorem Algebraic.Threshold.Program.weightedSum_smul {n : ℕ} (c : ℝ) (w : Fin n → ℝ) (x : Fin n → Bool) : weightedSum (c • w) x = c * weightedSum w x

theorem Algebraic.Threshold.Program.weightedSum_zero {n : ℕ} (x : Fin n → Bool) : weightedSum 0 x = 0

theorem Algebraic.Threshold.Program.DirectionRuns.weightedSum_eq {n s : ℕ} {C : Program n s} {B : ℕ} (R : C.DirectionRuns B) {i : ℕ} {j : Fin s} (hj : R.run j = i) (x : Fin n → Bool) : weightedSum (C.inputWeight j) x = R.slope i j * weightedSum (R.dir i) x

noncomputable def Algebraic.Threshold.Program.DirectionRuns.toBlockDecomposition {n s : ℕ} {C : Program n s} {B : ℕ} {f : Cslib.BooleanFunction n} (R : C.DirectionRuns B) (hC : C.Computes f) : BlockDecomposition f (Fin s → Bool)

The block decomposition of a program along a split into direction runs: the history after i blocks holds the values of the gates of the first i runs.

Equations

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

theorem Algebraic.Threshold.Program.DirectionRuns.toBlockDecomposition_cost {n s : ℕ} {C : Program n s} {B : ℕ} {f : Cslib.BooleanFunction n} (R : C.DirectionRuns B) (hC : C.Computes f) : (R.toBlockDecomposition hC).cost = ∏ i ∈ Finset.range B, (BlockKind.oneDim (2 ^ R.size i - 1)).cost