Unambiguous transcript cells and quadratic-potential unique-sink representations

Every straight-line threshold program in strict unit-margin normal form (StrictMarginProgram), where each gate i has score Q_i(x, z) = ∑ a, a_{i, a} x_a + ∑ j < i, b_{i, j} z_j - θ_i with |Q_i(x, z)| ≥ 1 on all Boolean assignments and outputs true iff 0 < Q_i(x, z), admits two exact characterizations of its gate transcript (StrictMarginProgram.eval):

1. Unambiguous cells, coordinatewise dominance, and unique-extension ILP (Section 10 of [ThresholdCircuitRepresentations2026]): For a putative transcript z : Fin g → Bool with sign σ_i = boolSign (z i) ∈ {-1, 1}, the consistency cell predicate ∀ i, 1 ≤ σ_i * Q_i(x, z) holds if and only if z = P.eval x (inTranscriptCell_iff_eq_eval). The cells therefore partition the input cube (∃! z, P.inTranscriptCell x z, existsUnique_inTranscriptCell). Across any input split U, cell membership is equivalent to coordinatewise dominance rightDemand ≤ leftSupply in dimension g (inTranscriptCell_iff_dominance), and given upper bounds |Q_i(x, z)| ≤ M_i, to the linear inequalities 1 - (M_i + 1)(1 - z_i) ≤ Q_i(x, z) ≤ -1 + (M_i + 1) z_i (ilpValid_iff_eq_eval).

2. Quadratic Boolean potential and unique sinks on cube faces (Section 11, Theorem 11.1 of [ThresholdCircuitRepresentations2026]): Defining positive priorities backwards by λ_i = 1 + ∑_{j > i} λ_j |b_{j, i}| (priority) and the quadratic Boolean energy E_x(z) = - ∑_i λ_i z_i Q_i(x, z) (energy), flipping coordinate i from false to true changes E_x by -λ_i Q_i(x, z) - ∑_{j > i} λ_j b_{j, i} z_j (energy_update_true_sub_false). Because the later-gate sum has magnitude at most λ_i - 1 while |λ_i Q_i(x, z)| ≥ λ_i, the energy-decreasing direction of every cube edge at coordinate i agrees strictly (by at least 1) with gate i's local threshold rule (energy_le_update_not_iff). Consequently, on every subcube face (fixed, val), there is a unique sink under single-coordinate flips, equal to the face-restricted topological evaluation (isSinkOnFace_iff_eq_faceEval, existsUnique_isSinkOnFace), and a topological sweep reaches it in g coordinate steps (sweep_eq_faceEval).

Main definitions

• Cslib.Circuits.Boolean.WeightedThreshold.boolSign: {false, true} → {-1, 1} ⊂ ℝ.
• Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram: straight-line threshold program with strictly lower-triangular gate weights and unit score margin |Q_i(x, z)| ≥ 1.
• Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.score, .sweep, .faceEval, .eval: gate scores, topological coordinate sweep, face evaluation, and full evaluation.
• Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.inTranscriptCell, .leftSupply, .rightDemand, .ilpValid: transcript cell, split-dominance vectors, and ILP inequalities.
• Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.priority, .energy, .IsSinkOnFace: backwards positive priorities, quadratic Boolean energy, and cube-face sinks.

Main results

• Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.inTranscriptCell_iff_eq_eval, .existsUnique_inTranscriptCell: unambiguous transcript cell characterization and partition.
• Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.inTranscriptCell_iff_dominance, .ilpValid_iff_eq_eval: coordinatewise dominance and unique-extension ILP characterizations.
• Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.energy_update_true_sub_false: exact coordinate-flip energy difference (equation (27)).
• Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.isSinkOnFace_iff_eq_faceEval, .existsUnique_isSinkOnFace, .isSink_iff_eq_eval: unique sink on every cube face and on the whole cube (Theorem 11.1).
• Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.sweep_eq_faceEval, .energy_sweep_le: topological coordinate sweep reaches the unique sink in g steps with nonincreasing energy when started on the face.
• Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.priority_le_pow: exponential upper bound λ_i ≤ (W + 1) ^ (g - 1 - i) under weight bound |b_{j, i}| ≤ W.

References

• [Threshold Circuits as Decision Trees and Finite-State Programs, Sections 10 and 11] [26]

def Cslib.Circuits.Boolean.WeightedThreshold.boolSign (b : Bool) : ℝ

Sign 2 z - 1 ∈ {-1, 1} of a Boolean bit z.

@[simp]

theorem Cslib.Circuits.Boolean.WeightedThreshold.boolSign_true : boolSign true = 1

@[simp]

theorem Cslib.Circuits.Boolean.WeightedThreshold.boolSign_false : boolSign false = -1

theorem Cslib.Circuits.Boolean.WeightedThreshold.boolSign_eq_two_mul_toNat_sub_one (b : Bool) : boolSign b = 2 * ↑b.toNat - 1

@[simp]

theorem Cslib.Circuits.Boolean.WeightedThreshold.abs_boolSign (b : Bool) : |boolSign b| = 1

structure Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram (n g : ℕ) : Type

A straight-line threshold program on n Boolean inputs with g gates in strict unit-margin normal form (Sections 10–11 of [ThresholdCircuitRepresentations2026]): gate i has score Q_i(x, z) = ∑ a, inputWeight i a * x_a + ∑ j, gateWeight i j * z_j - threshold i with gateWeight i j = 0 for i ≤ j and |Q_i(x, z)| ≥ 1 on every Boolean (x, z).

• inputWeight : Fin g → Fin n → ℝ

  Direct input weights a_i for gate i.

• gateWeight : Fin g → Fin g → ℝ

  Strictly lower-triangular internal gate weights b_{i, j} (0 for i ≤ j).

• threshold : Fin g → ℝ

  Threshold θ_i for gate i.

• gateWeight_eq_zero_of_le (i j : Fin g) : i ≤ j → self.gateWeight i j = 0

  Strict lower triangularity of gateWeight.

• one_le_abs_score (x : Fin n → Bool) (z : Fin g → Bool) (i : Fin g) : 1 ≤ |∑ a : Fin n, self.inputWeight i a * ↑(x a).toNat + ∑ j : Fin g, self.gateWeight i j * ↑(z j).toNat - self.threshold i|

  Unit margin |Q_i(x, z)| ≥ 1 on all Boolean inputs and transcripts.

def Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.inputSum {n g : ℕ} (P : StrictMarginProgram n g) (i : Fin g) (x : Fin n → Bool) : ℝ

Direct input contribution ∑ a, a_{i, a} x_a at gate i.

def Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.internalSum {n g : ℕ} (P : StrictMarginProgram n g) (i : Fin g) (z : Fin g → Bool) : ℝ

Internal gate contribution ∑ j, b_{i, j} z_j at gate i.

def Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.score {n g : ℕ} (P : StrictMarginProgram n g) (x : Fin n → Bool) (z : Fin g → Bool) (i : Fin g) : ℝ

Score Q_i(x, z) = inputSum i x + internalSum i z - threshold i at gate i.

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.one_le_abs_score' {n g : ℕ} (P : StrictMarginProgram n g) (x : Fin n → Bool) (z : Fin g → Bool) (i : Fin g) : 1 ≤ |P.score x z i|

Every gate score has absolute value at least 1.

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.score_le_neg_one_or_one_le {n g : ℕ} (P : StrictMarginProgram n g) (x : Fin n → Bool) (z : Fin g → Bool) (i : Fin g) : P.score x z i ≤ -1 ∨ 1 ≤ P.score x z i

Every gate score is either at most -1 or at least 1.

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.score_ne_zero {n g : ℕ} (P : StrictMarginProgram n g) (x : Fin n → Bool) (z : Fin g → Bool) (i : Fin g) : P.score x z i ≠ 0

No gate score vanishes.

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.pos_score_iff_one_le {n g : ℕ} (P : StrictMarginProgram n g) (x : Fin n → Bool) (z : Fin g → Bool) (i : Fin g) : 0 < P.score x z i ↔ 1 ≤ P.score x z i

By the unit margin, 0 < Q_i(x, z) is equivalent to 1 ≤ Q_i(x, z).

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.pos_score_iff_nonneg {n g : ℕ} (P : StrictMarginProgram n g) (x : Fin n → Bool) (z : Fin g → Bool) (i : Fin g) : 0 < P.score x z i ↔ 0 ≤ P.score x z i

By the unit margin, 0 < Q_i(x, z) is equivalent to 0 ≤ Q_i(x, z).

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.internalSum_congr_lt {n g : ℕ} (P : StrictMarginProgram n g) {z₁ z₂ : Fin g → Bool} {i : Fin g} (h : ∀ j < i, z₁ j = z₂ j) : P.internalSum i z₁ = P.internalSum i z₂

Gate i's internal sum depends only on earlier coordinates j < i.

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.score_congr_lt {n g : ℕ} (P : StrictMarginProgram n g) (x : Fin n → Bool) {z₁ z₂ : Fin g → Bool} {i : Fin g} (h : ∀ j < i, z₁ j = z₂ j) : P.score x z₁ i = P.score x z₂ i

Gate i's score depends only on earlier coordinates j < i.

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.score_update_of_le {n g : ℕ} (P : StrictMarginProgram n g) (x : Fin n → Bool) (z : Fin g → Bool) {i j : Fin g} (hij : i ≤ j) (b : Bool) : P.score x (Function.update z j b) i = P.score x z i

Updating coordinate j ≥ i leaves gate i's score unchanged.

Topological coordinate sweep and face evaluation

noncomputable def Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.faceStep {n g : ℕ} (P : StrictMarginProgram n g) (fixed : Finset (Fin g)) (val : Fin g → Bool) (x : Fin n → Bool) (z : Fin g → Bool) (i : Fin g) : Fin g → Bool

Single-coordinate update at gate i on the subcube face (fixed, val): assign val i if i ∈ fixed, and the local threshold rule decide (0 < P.score x z i) otherwise.

noncomputable def Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.sweep {n g : ℕ} (P : StrictMarginProgram n g) (fixed : Finset (Fin g)) (val : Fin g → Bool) (x : Fin n → Bool) (z : Fin g → Bool) : ℕ → Fin g → Bool

Topological sweep of the first k coordinates on the subcube face (fixed, val), starting from z.

@[simp]

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.sweep_zero {n g : ℕ} (P : StrictMarginProgram n g) (fixed : Finset (Fin g)) (val : Fin g → Bool) (x : Fin n → Bool) (z : Fin g → Bool) : P.sweep fixed val x z 0 = z

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.sweep_succ {n g : ℕ} (P : StrictMarginProgram n g) (fixed : Finset (Fin g)) (val : Fin g → Bool) (x : Fin n → Bool) (z : Fin g → Bool) (k : ℕ) : P.sweep fixed val x z (k + 1) = if hk : k < g then P.faceStep fixed val x (P.sweep fixed val x z k) ⟨k, hk⟩ else P.sweep fixed val x z k

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.sweep_eq_of_lt {n g : ℕ} (P : StrictMarginProgram n g) (fixed : Finset (Fin g)) (val : Fin g → Bool) (x : Fin n → Bool) (z : Fin g → Bool) {i : Fin g} {k : ℕ} (hik : ↑i < k) : P.sweep fixed val x z k i = P.sweep fixed val x z (↑i + 1) i

Once coordinate i has been swept at step i + 1, later sweep steps leave it unchanged.

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.sweep_succ_self {n g : ℕ} (P : StrictMarginProgram n g) (fixed : Finset (Fin g)) (val : Fin g → Bool) (x : Fin n → Bool) (z : Fin g → Bool) (i : Fin g) : P.sweep fixed val x z (↑i + 1) i = if i ∈ fixed then val i else decide (0 < P.score x (P.sweep fixed val x z ↑i) i)

At step i + 1, coordinate i is set according to the face rule on the state after i steps.

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.sweep_apply {n g : ℕ} (P : StrictMarginProgram n g) (fixed : Finset (Fin g)) (val : Fin g → Bool) (x : Fin n → Bool) (z : Fin g → Bool) (i : Fin g) : P.sweep fixed val x z g i = if i ∈ fixed then val i else decide (0 < P.score x (P.sweep fixed val x z g) i)

After g sweep steps from any initial assignment z, every coordinate i satisfies the face-restricted gate equation.

noncomputable def Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.faceEval {n g : ℕ} (P : StrictMarginProgram n g) (fixed : Finset (Fin g)) (val : Fin g → Bool) (x : Fin n → Bool) : Fin g → Bool

Face-restricted topological evaluation on (fixed, val), fixing z_i = val i for i ∈ fixed and evaluating free gates in topological order.

noncomputable def Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.eval {n g : ℕ} (P : StrictMarginProgram n g) (x : Fin n → Bool) : Fin g → Bool

Full topological gate evaluation P.eval x : Fin g → Bool (the face with fixed = ∅).

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.faceEval_apply {n g : ℕ} (P : StrictMarginProgram n g) (fixed : Finset (Fin g)) (val : Fin g → Bool) (x : Fin n → Bool) (i : Fin g) : P.faceEval fixed val x i = if i ∈ fixed then val i else decide (0 < P.score x (P.faceEval fixed val x) i)

@[simp]

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.faceEval_of_mem {n g : ℕ} (P : StrictMarginProgram n g) {fixed : Finset (Fin g)} {val : Fin g → Bool} {x : Fin n → Bool} {i : Fin g} (hi : i ∈ fixed) : P.faceEval fixed val x i = val i

@[simp]

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.faceEval_of_notMem {n g : ℕ} (P : StrictMarginProgram n g) {fixed : Finset (Fin g)} {val : Fin g → Bool} {x : Fin n → Bool} {i : Fin g} (hi : i ∉ fixed) : P.faceEval fixed val x i = decide (0 < P.score x (P.faceEval fixed val x) i)

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.eval_eq {n g : ℕ} (P : StrictMarginProgram n g) (x : Fin n → Bool) (i : Fin g) : P.eval x i = decide (0 < P.score x (P.eval x) i)

Every gate of P.eval x equals decide (0 < P.score x (P.eval x) i).

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.eq_faceEval_iff {n g : ℕ} (P : StrictMarginProgram n g) (fixed : Finset (Fin g)) (val : Fin g → Bool) (x : Fin n → Bool) (z : Fin g → Bool) : z = P.faceEval fixed val x ↔ (∀ i ∈ fixed, z i = val i) ∧ ∀ i ∉ fixed, z i = decide (0 < P.score x z i)

P.faceEval fixed val x is the unique assignment agreeing with val on fixed and satisfying every free gate's threshold rule.

@[simp]

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.sweep_eq_faceEval {n g : ℕ} (P : StrictMarginProgram n g) (fixed : Finset (Fin g)) (val : Fin g → Bool) (x : Fin n → Bool) (z : Fin g → Bool) : P.sweep fixed val x z g = P.faceEval fixed val x

A full g-step topological sweep from any starting assignment z reaches P.faceEval fixed val x.

@[simp]

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.faceEval_empty_eq_eval {n g : ℕ} (P : StrictMarginProgram n g) (val : Fin g → Bool) (x : Fin n → Bool) : P.faceEval ∅ val x = P.eval x

With no fixed coordinates, P.faceEval ∅ val x equals P.eval x.

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.sweep_empty_eq_eval {n g : ℕ} (P : StrictMarginProgram n g) (val : Fin g → Bool) (x : Fin n → Bool) (z : Fin g → Bool) : P.sweep ∅ val x z g = P.eval x

A full g-step topological sweep with no fixed coordinates reaches P.eval x.

def Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.ofProgram {n g : ℕ} (p : Program signature n g) (hmargin : ∀ (x : Fin n → Bool) (z : Fin g → Bool) (i : Fin g), 1 ≤ |∑ a : Fin n, WeightedThreshold.inputWeight p i a * ↑(x a).toNat + ∑ j : Fin g, WeightedThreshold.gateWeight p i j * ↑(z j).toNat - (p.lines i).op.threshold|) : StrictMarginProgram n g

Construct a StrictMarginProgram from a Program signature n g whose gates satisfy the unit margin condition.

@[simp]

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.eval_ofProgram {n g : ℕ} (p : Program signature n g) (hmargin : ∀ (x : Fin n → Bool) (z : Fin g → Bool) (i : Fin g), 1 ≤ |∑ a : Fin n, WeightedThreshold.inputWeight p i a * ↑(x a).toNat + ∑ j : Fin g, WeightedThreshold.gateWeight p i j * ↑(z j).toNat - (p.lines i).op.threshold|) (x : Fin n → Bool) : (ofProgram p hmargin).eval x = p.eval interpretation x

Evaluation of ofProgram p hmargin agrees with p.eval interpretation.

Section 10: Unambiguous cells, coordinatewise dominance, and unique-extension ILP

def Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.inTranscriptCell {n g : ℕ} (P : StrictMarginProgram n g) (x : Fin n → Bool) (z : Fin g → Bool) : Prop

Consistency cell predicate x ∈ P_z (equation (23)): (2 z_i - 1) Q_i(x, z) ≥ 1 for every gate i.

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.one_le_boolSign_mul_score_iff {n g : ℕ} (P : StrictMarginProgram n g) {x : Fin n → Bool} {z : Fin g → Bool} {i : Fin g} : 1 ≤ boolSign (z i) * P.score x z i ↔ z i = decide (0 < P.score x z i)

By the unit margin, 1 ≤ boolSign (z i) * P.score x z i holds iff z i agrees with gate i's threshold decision.

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.inTranscriptCell_iff_eq_eval {n g : ℕ} (P : StrictMarginProgram n g) (x : Fin n → Bool) (z : Fin g → Bool) : P.inTranscriptCell x z ↔ z = P.eval x

Unambiguous cell theorem: x belongs to the consistency cell of z if and only if z is the unique circuit transcript P.eval x.

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.existsUnique_inTranscriptCell {n g : ℕ} (P : StrictMarginProgram n g) (x : Fin n → Bool) : ∃! z : Fin g → Bool, P.inTranscriptCell x z

The consistency cells {P_z}_{z : Fin g → Bool} partition the input cube: every input x belongs to the cell of a unique transcript z.

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.sum_inTranscriptCell_ite {n g : ℕ} (P : StrictMarginProgram n g) (x : Fin n → Bool) [DecidablePred (P.inTranscriptCell x)] (out : Fin g) : (∑ z : Fin g → Bool, if P.inTranscriptCell x z ∧ z out = true then 1 else 0) = (P.eval x out).toNat

Disjoint-support indicator expansion (equation (24)): summing the cell indicators over all transcripts with z out = true recovers the output bit (P.eval x out).toNat.

def Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.leftSupply {n g : ℕ} (P : StrictMarginProgram n g) (U : Finset (Fin n)) (z : Fin g → Bool) (x : Fin n → Bool) (i : Fin g) : ℝ

Left-half supply vector α_z(u)_i = σ_i ∑_{a ∈ U} a_{i, a} x_a for an input split U.

def Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.rightDemand {n g : ℕ} (P : StrictMarginProgram n g) (U : Finset (Fin n)) (z : Fin g → Bool) (x : Fin n → Bool) (i : Fin g) : ℝ

Right-half demand vector β_z(v)_i = 1 - σ_i (∑_{a ∈ Uᶜ} a_{i, a} x_a + internalSum i z - θ_i) for an input split U.

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.inTranscriptCell_iff_dominance {n g : ℕ} (P : StrictMarginProgram n g) (U : Finset (Fin n)) (x : Fin n → Bool) (z : Fin g → Bool) : P.inTranscriptCell x z ↔ ∀ (i : Fin g), P.rightDemand U z x i ≤ P.leftSupply U z x i

Coordinatewise dominance characterization: across any input split U, x belongs to the consistency cell of z iff rightDemand U z x i ≤ leftSupply U z x i for every gate i.

def Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.ilpValid {n g : ℕ} (P : StrictMarginProgram n g) (M : Fin g → ℝ) (x : Fin n → Bool) (z : Fin g → Bool) : Prop

Linear inequalities of the unique-extension integer linear program (equation (25)) with score upper bounds M : Fin g → ℝ.

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.ilpValid_gate_iff {n g : ℕ} (P : StrictMarginProgram n g) {M : Fin g → ℝ} {x : Fin n → Bool} {z : Fin g → Bool} {i : Fin g} (hM : |P.score x z i| ≤ M i) : 1 - (M i + 1) * (1 - ↑(z i).toNat) ≤ P.score x z i ∧ P.score x z i ≤ -1 + (M i + 1) * ↑(z i).toNat ↔ 1 ≤ boolSign (z i) * P.score x z i

Given score bounds |P.score x z i| ≤ M i, the ILP inequalities at gate i are equivalent to 1 ≤ boolSign (z i) * P.score x z i.

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.ilpValid_iff_eq_eval {n g : ℕ} (P : StrictMarginProgram n g) {M : Fin g → ℝ} {x : Fin n → Bool} {z : Fin g → Bool} (hM : ∀ (i : Fin g), |P.score x z i| ≤ M i) : P.ilpValid M x z ↔ z = P.eval x

Unique-extension ILP theorem (equation (25)): when |P.score x z i| ≤ M i for every gate i, P.ilpValid M x z holds if and only if z = P.eval x.

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.existsUnique_ilpValid {n g : ℕ} (P : StrictMarginProgram n g) {M : Fin g → ℝ} {x : Fin n → Bool} (hM : ∀ (z : Fin g → Bool) (i : Fin g), |P.score x z i| ≤ M i) : ∃! z : Fin g → Bool, P.ilpValid M x z

Every input x has a unique transcript z satisfying P.ilpValid M x z.

Section 11: Backwards priorities, quadratic Boolean energy, and unique sinks

@[irreducible]

def Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.priority {n g : ℕ} (P : StrictMarginProgram n g) (i : Fin g) : ℝ

Backwards positive priority λ_i = 1 + ∑_{j > i} λ_j |b_{j, i}|.

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.priority_eq {n g : ℕ} (P : StrictMarginProgram n g) (i : Fin g) : P.priority i = 1 + ∑ j : Fin g, if i < j then P.priority j * |P.gateWeight j i| else 0

Unfolding equation for the backwards priority P.priority i.

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.one_le_priority {n g : ℕ} (P : StrictMarginProgram n g) (i : Fin g) : 1 ≤ P.priority i

Every gate priority is at least 1.

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.priority_pos {n g : ℕ} (P : StrictMarginProgram n g) (i : Fin g) : 0 < P.priority i

Every gate priority is strictly positive.

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.abs_sum_later_le_priority_sub_one {n g : ℕ} (P : StrictMarginProgram n g) (z : Fin g → Bool) (i : Fin g) : |∑ j : Fin g, if i < j then P.priority j * P.gateWeight j i * ↑(z j).toNat else 0| ≤ P.priority i - 1

The total contribution of later gates j > i to coordinate i's flip difference has magnitude at most P.priority i - 1.

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.priority_le_pow {n g : ℕ} (P : StrictMarginProgram n g) {W : ℝ} (hW0 : 0 ≤ W) (hW : ∀ (j i : Fin g), i < j → |P.gateWeight j i| ≤ W) (i : Fin g) : P.priority i ≤ (W + 1) ^ (g - 1 - ↑i)

If |b_{j, i}| ≤ W for all i < j, then P.priority i ≤ (W + 1) ^ (g - 1 - i).

def Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.energy {n g : ℕ} (P : StrictMarginProgram n g) (x : Fin n → Bool) (z : Fin g → Bool) : ℝ

Quadratic Boolean energy E_x(z) = - ∑ i, λ_i z_i Q_i(x, z) (equation (26)).

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.energy_update_true_sub_false {n g : ℕ} (P : StrictMarginProgram n g) (x : Fin n → Bool) (z : Fin g → Bool) (i : Fin g) : P.energy x (Function.update z i true) - P.energy x (Function.update z i false) = -P.priority i * P.score x z i - ∑ j : Fin g, if i < j then P.priority j * P.gateWeight j i * ↑(z j).toNat else 0

Coordinate-flip energy identity (equation (27)): changing z_i from false to true changes P.energy x by -λ_i Q_i(x, z) - ∑_{j > i} λ_j b_{j, i} z_j.

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.energy_update_true_add_one_le_false {n g : ℕ} (P : StrictMarginProgram n g) {x : Fin n → Bool} {z : Fin g → Bool} {i : Fin g} (h : 0 < P.score x z i) : P.energy x (Function.update z i true) + 1 ≤ P.energy x (Function.update z i false)

When 0 < P.score x z i, setting z_i = true decreases the energy by at least 1 relative to z_i = false.

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.energy_update_false_add_one_le_true {n g : ℕ} (P : StrictMarginProgram n g) {x : Fin n → Bool} {z : Fin g → Bool} {i : Fin g} (h : ¬0 < P.score x z i) : P.energy x (Function.update z i false) + 1 ≤ P.energy x (Function.update z i true)

When ¬ (0 < P.score x z i), setting z_i = false decreases the energy by at least 1 relative to z_i = true.

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.energy_le_update_not_iff {n g : ℕ} (P : StrictMarginProgram n g) (x : Fin n → Bool) (z : Fin g → Bool) (i : Fin g) : P.energy x z ≤ P.energy x (Function.update z i !z i) ↔ z i = decide (0 < P.score x z i)

Flipping coordinate i does not decrease P.energy x if and only if z i already satisfies gate i's local threshold rule.

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.energy_update_not_lt_iff {n g : ℕ} (P : StrictMarginProgram n g) (x : Fin n → Bool) (z : Fin g → Bool) (i : Fin g) : P.energy x (Function.update z i !z i) < P.energy x z ↔ z i ≠ decide (0 < P.score x z i)

Flipping coordinate i strictly decreases P.energy x if and only if z i violates gate i's local threshold rule.

def Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.IsSinkOnFace {n g : ℕ} (P : StrictMarginProgram n g) (fixed : Finset (Fin g)) (val : Fin g → Bool) (x : Fin n → Bool) (z : Fin g → Bool) : Prop

z is a sink on the cube face (fixed, val) if z agrees with val on fixed and no single free-coordinate flip strictly decreases P.energy x.

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.isSinkOnFace_iff_eq_faceEval {n g : ℕ} (P : StrictMarginProgram n g) (fixed : Finset (Fin g)) (val : Fin g → Bool) (x : Fin n → Bool) (z : Fin g → Bool) : P.IsSinkOnFace fixed val x z ↔ z = P.faceEval fixed val x

Theorem 11.1 (Unique sink on every cube face): z is a sink on the subcube face (fixed, val) if and only if z = P.faceEval fixed val x.

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.existsUnique_isSinkOnFace {n g : ℕ} (P : StrictMarginProgram n g) (fixed : Finset (Fin g)) (val : Fin g → Bool) (x : Fin n → Bool) : ∃! z : Fin g → Bool, P.IsSinkOnFace fixed val x z

Every subcube face (fixed, val) has a unique sink under P.energy x.

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.isSink_iff_eq_eval {n g : ℕ} (P : StrictMarginProgram n g) (x : Fin n → Bool) (z : Fin g → Bool) : P.IsSinkOnFace ∅ (fun (x : Fin g) => false) x z ↔ z = P.eval x

Unique sink on the whole cube: on the unrestricted cube (fixed = ∅), z is a sink under P.energy x if and only if z is the circuit transcript P.eval x.

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.energy_faceStep_le {n g : ℕ} (P : StrictMarginProgram n g) {fixed : Finset (Fin g)} {val : Fin g → Bool} {x : Fin n → Bool} {z : Fin g → Bool} {i : Fin g} (hfix : i ∈ fixed → z i = val i) : P.energy x (P.faceStep fixed val x z i) ≤ P.energy x z

Updating coordinate i via P.faceStep fixed val x does not increase P.energy x whenever z already agrees with val at i if i ∈ fixed.

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.sweep_mem_fixed {n g : ℕ} (P : StrictMarginProgram n g) {fixed : Finset (Fin g)} {val : Fin g → Bool} {x : Fin n → Bool} {z : Fin g → Bool} (hfix : ∀ i ∈ fixed, z i = val i) (k : ℕ) {i : Fin g} (hi : i ∈ fixed) : P.sweep fixed val x z k i = val i

Sweeping preserves agreement with val on fixed.

theorem Cslib.Circuits.Boolean.WeightedThreshold.StrictMarginProgram.energy_sweep_le {n g : ℕ} (P : StrictMarginProgram n g) {fixed : Finset (Fin g)} {val : Fin g → Bool} {x : Fin n → Bool} {z : Fin g → Bool} (hfix : ∀ i ∈ fixed, z i = val i) (k : ℕ) : P.energy x (P.sweep fixed val x z k) ≤ P.energy x z

Starting from any assignment z on the face (fixed, val), the topological coordinate sweep monotonically decreases (or preserves) P.energy x at every step.