Partial assignments and subcubes

A consistent partial assignment is modelled as a function V → Option Bool: none means the coordinate is free, some b means it is fixed to b. (Consistency is automatic in this encoding.)

Main definitions, following Section 1.3 of bs_lambda.txt:

• PartialAssign.Sat P x / PartialAssign.cube P — the subcube C(P);
• PartialAssign.proj P x — the nearest-point projection π_C(x);
• PartialAssign.Conflict P Q v — P and Q fix v to opposite values;
• PartialAssign.fixedSet P — the coordinates fixed by P;
• PartialAssign.codim P — its cardinality;
• PartialAssign.violSet P x — the fixed literals of P violated by x;
• PartialAssign.dist P x — dist(x, C(P)), the number of violated literals;
• PartialAssign.indUnion P — the indicator of the union of a family of subcubes.

The two directions relating a point to its projection are PartialAssign.isLeast_dist (the projection realises the distance) and PartialAssign.eq_flipSet_proj_violSet (the point is recovered from the projection by flipping the violated literals).

Adapted for Lean Pool from Timeroot/BS_Lam at commit 7bd39a8d41ee7910d3296d0477ad18f8fff9d870; ported to Lean Pool with proof and dependency cleanup.

@[reducible, inline]

abbrev BSLambda.PartialAssign (V : Type u_1) : Type u_1

A consistent partial assignment on the coordinate set V: none = free, some b = fixed to b.

Equations

• BSLambda.PartialAssign V = (V → Option Bool)

Satisfaction, projection and conflicts

def BSLambda.PartialAssign.Sat {V : Type u_1} (P : PartialAssign V) (x : Input V) : Prop

x satisfies every literal of P.

Equations

• P.Sat x = ∀ (v : V) (b : Bool), P v = some b → x v = b

theorem BSLambda.PartialAssign.Sat.eq_of_fixed {V : Type u_1} {P : PartialAssign V} {x : Input V} (hx : P.Sat x) {v : V} {b : Bool} (hv : P v = some b) : x v = b

def BSLambda.PartialAssign.proj {V : Type u_1} (P : PartialAssign V) (x : Input V) : Input V

The nearest-point projection of x onto C(P): reset every violated fixed coordinate, leave the free coordinates alone.

Equations

• P.proj x v = (P v).getD (x v)

@[simp]

theorem BSLambda.PartialAssign.proj_apply {V : Type u_1} (P : PartialAssign V) (x : Input V) (v : V) : P.proj x v = (P v).getD (x v)

The projection keeps the value P fixes, falling back on the value of x.

@[simp]

theorem BSLambda.PartialAssign.proj_sat {V : Type u_1} (P : PartialAssign V) (x : Input V) : P.Sat (P.proj x)

theorem BSLambda.PartialAssign.proj_eq_self_of_sat {V : Type u_1} {P : PartialAssign V} {x : Input V} (hx : P.Sat x) : P.proj x = x

def BSLambda.PartialAssign.Conflict {V : Type u_1} (P Q : PartialAssign V) (v : V) : Prop

Two partial assignments conflict at v if they fix v to opposite values.

Equations

• P.Conflict Q v = ∃ (b : Bool), P v = some b ∧ Q v = some !b

@[instance_reducible]

instance BSLambda.PartialAssign.instDecidableConflict {V : Type u_1} (P Q : PartialAssign V) (v : V) : Decidable (P.Conflict Q v)

Conflict is an existential over Bool, hence decidable; providing the instance keeps the Finset statements of Section 4 free of Classical.dec.

Equations

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

theorem BSLambda.PartialAssign.Conflict.symm {V : Type u_1} {P Q : PartialAssign V} {v : V} (h : P.Conflict Q v) : Q.Conflict P v

theorem BSLambda.PartialAssign.Conflict.ne {V : Type u_1} {P Q : PartialAssign V} {v : V} (h : P.Conflict Q v) {x y : Input V} (hx : P.Sat x) (hy : Q.Sat y) : x v ≠ y v

Points of two conflicting subcubes disagree at the conflict coordinate.

theorem BSLambda.PartialAssign.sat_unique_of_conflict {V : Type u_1} {ι : Type u_2} {P : ι → PartialAssign V} (h : Pairwise fun (i j : ι) => ∃ (v : V), (P i).Conflict (P j) v) {i j : ι} {x : Input V} (hi : (P i).Sat x) (hj : (P j).Sat x) : i = j

A point of the cube lies in at most one member of a pairwise conflicting family.

theorem BSLambda.PartialAssign.exists_sat_and_sat_of_forall_not_conflict {V : Type u_1} {P Q : PartialAssign V} (h : ∀ (v : V), ¬P.Conflict Q v) : ∃ (x : Input V), P.Sat x ∧ Q.Sat x

Two partial assignments that conflict nowhere have a common point: merge them, taking the value of P where P fixes a coordinate and the value of Q elsewhere.

theorem BSLambda.PartialAssign.exists_conflict_of_forall_not_sat {V : Type u_1} {P Q : PartialAssign V} (h : ∀ (x : Input V), P.Sat x → ¬Q.Sat x) : ∃ (v : V), P.Conflict Q v

Converse of Conflict.disjoint_cube: disjoint subcubes come from a conflicting pair of literals.

@[instance_reducible]

instance BSLambda.PartialAssign.instDecidableSat {V : Type u_1} [Fintype V] (P : PartialAssign V) (x : Input V) : Decidable (P.Sat x)

Equations

• P.instDecidableSat x = { decide := decide (∀ a ∈ Finset.univ, (fun (v : V) => ∀ (b : Bool), P v = some b → x v = b) a), reflects_decide := ⋯ }

The fixed coordinates and the codimension

def BSLambda.PartialAssign.fixedSet {V : Type u_1} [Fintype V] (P : PartialAssign V) : Finset V

The set of coordinates fixed by P.

Equations

• P.fixedSet = {v : V | (P v).isSome = true}

@[simp]

theorem BSLambda.PartialAssign.mem_fixedSet {V : Type u_1} [Fintype V] {P : PartialAssign V} {v : V} : v ∈ P.fixedSet ↔ (P v).isSome = true

theorem BSLambda.PartialAssign.mem_fixedSet_iff_ne_none {V : Type u_1} [Fintype V] {P : PartialAssign V} {v : V} : v ∈ P.fixedSet ↔ P v ≠ none

theorem BSLambda.PartialAssign.mem_fixedSet_iff_exists {V : Type u_1} [Fintype V] {P : PartialAssign V} {v : V} : v ∈ P.fixedSet ↔ ∃ (b : Bool), P v = some b

A fixed coordinate carries an actual value.

def BSLambda.PartialAssign.codim {V : Type u_1} [Fintype V] (P : PartialAssign V) : ℕ

The codimension of the subcube C(P): the number of coordinates that P fixes.

Equations

• P.codim = P.fixedSet.card

theorem BSLambda.PartialAssign.codim_eq_card_fixedSet {V : Type u_1} [Fintype V] (P : PartialAssign V) : P.codim = P.fixedSet.card

The defining equation for codim, so that call sites need not unfold the def.

theorem BSLambda.PartialAssign.notMem_fixedSet_of_apply_ne {V : Type u_1} [Fintype V] {P : PartialAssign V} {x y : Input V} (hx : P.Sat x) (hy : P.Sat y) {v : V} (hne : x v ≠ y v) : v ∉ P.fixedSet

Two points of the same subcube can only differ at a coordinate the subcube leaves free.

theorem BSLambda.PartialAssign.proj_eq_of_sat_of_eq_off_fixedSet {V : Type u_1} [Fintype V] {P : PartialAssign V} {x y : Input V} (hx : P.Sat x) (h : ∀ v ∉ P.fixedSet, y v = x v) : P.proj y = x

A point that agrees with a point of C(P) off the coordinates fixed by P projects onto it.

The violated literals and the distance to the subcube

def BSLambda.PartialAssign.violSet {V : Type u_1} [Fintype V] (P : PartialAssign V) (x : Input V) : Finset V

The fixed literals of P that x violates.

Equations

• P.violSet x = {v : V | P v ≠ none ∧ P v ≠ some (x v)}

@[simp]

theorem BSLambda.PartialAssign.mem_violSet {V : Type u_1} [Fintype V] {P : PartialAssign V} {x : Input V} {v : V} : v ∈ P.violSet x ↔ P v ≠ none ∧ P v ≠ some (x v)

theorem BSLambda.PartialAssign.mem_violSet_iff_exists_ne {V : Type u_1} [Fintype V] {P : PartialAssign V} {x : Input V} {v : V} : v ∈ P.violSet x ↔ ∃ (b : Bool), P v = some b ∧ x v ≠ b

v is violated by x exactly when P fixes v to a value other than x v.

theorem BSLambda.PartialAssign.violSet_subset_fixedSet {V : Type u_1} [Fintype V] (P : PartialAssign V) (x : Input V) : P.violSet x ⊆ P.fixedSet

theorem BSLambda.PartialAssign.violSet_subset_of_sat_of_eq_off {V : Type u_1} [Fintype V] {P : PartialAssign V} {x y : Input V} {A : Finset V} (hx : P.Sat x) (h : ∀ v ∉ A, y v = x v) : P.violSet y ⊆ A

A point that agrees outside A with some point of C(P) violates no literal of P outside A.

def BSLambda.PartialAssign.dist {V : Type u_1} [Fintype V] (P : PartialAssign V) (x : Input V) : ℕ

dist(x, C(P)): the number of fixed literals of P violated by x.

Equations

• P.dist x = (P.violSet x).card

theorem BSLambda.PartialAssign.dist_eq_card_violSet {V : Type u_1} [Fintype V] (P : PartialAssign V) (x : Input V) : P.dist x = (P.violSet x).card

The defining equation for dist, so that call sites need not unfold the def.

theorem BSLambda.PartialAssign.dist_le_codim {V : Type u_1} [Fintype V] (P : PartialAssign V) (x : Input V) : P.dist x ≤ P.codim

@[simp]

theorem BSLambda.PartialAssign.dist_eq_zero_iff {V : Type u_1} [Fintype V] {P : PartialAssign V} {x : Input V} : P.dist x = 0 ↔ P.Sat x

theorem BSLambda.PartialAssign.hammingDist_proj {V : Type u_1} [Fintype V] (P : PartialAssign V) (x : Input V) : hammingDist x (P.proj x) = P.dist x

The distance to C(P) is realised by the projection.

theorem BSLambda.PartialAssign.dist_le_hammingDist {V : Type u_1} [Fintype V] {P : PartialAssign V} {x y : Input V} (hy : P.Sat y) : P.dist x ≤ hammingDist x y

No point of C(P) is closer to x than dist(x, C(P)).

theorem BSLambda.PartialAssign.Conflict.mem_violSet {V : Type u_1} [Fintype V] {P Q : PartialAssign V} {v : V} (h : P.Conflict Q v) {x : Input V} (hx : P.Sat x) : v ∈ Q.violSet x

A coordinate at which P and Q conflict is a literal of Q violated by every point of the subcube of P.

theorem BSLambda.PartialAssign.conflict_of_mem_fixedSet {V : Type u_1} [Fintype V] {P Q : PartialAssign V} {x y : Input V} (hx : P.Sat x) (hy : Q.Sat y) {v : V} (hP : v ∈ P.fixedSet) (hQ : v ∈ Q.fixedSet) (hne : x v ≠ y v) : P.Conflict Q v

Converse of Conflict.ne: a coordinate fixed by both P and Q at which two satisfying points differ is a conflict coordinate.

The indicator of a union of subcubes

def BSLambda.PartialAssign.indUnion {V : Type u_1} [Fintype V] {ι : Type u_2} [Fintype ι] (P : ι → PartialAssign V) : Input V → Bool

The indicator of the union ⋃ i, C(P i) of a family of subcubes.

Equations

• BSLambda.PartialAssign.indUnion P x = decide (∃ (i : ι), (P i).Sat x)

@[simp]

theorem BSLambda.PartialAssign.indUnion_eq_true_iff {V : Type u_1} [Fintype V] {ι : Type u_2} [Fintype ι] {P : ι → PartialAssign V} {x : Input V} : indUnion P x = true ↔ ∃ (i : ι), (P i).Sat x

@[simp]

theorem BSLambda.PartialAssign.indUnion_eq_false_iff {V : Type u_1} [Fintype V] {ι : Type u_2} [Fintype ι] {P : ι → PartialAssign V} {x : Input V} : indUnion P x = false ↔ ∀ (i : ι), ¬(P i).Sat x

theorem BSLambda.PartialAssign.indUnion_eq_true_of_sat {V : Type u_1} [Fintype V] {ι : Type u_2} [Fintype ι] {P : ι → PartialAssign V} {x : Input V} {i : ι} (h : (P i).Sat x) : indUnion P x = true

Every point of a member subcube is positive.

The subcube as a Finset

def BSLambda.PartialAssign.cube {V : Type u_1} [Fintype V] [DecidableEq V] (P : PartialAssign V) : Finset (Input V)

The subcube C(P) cut out by the partial assignment P.

Equations

• P.cube = {x : BSLambda.Input V | P.Sat x}

@[simp]

theorem BSLambda.PartialAssign.mem_cube {V : Type u_1} [Fintype V] [DecidableEq V] {P : PartialAssign V} {x : Input V} : x ∈ P.cube ↔ P.Sat x

theorem BSLambda.PartialAssign.proj_mem_cube {V : Type u_1} [Fintype V] [DecidableEq V] (P : PartialAssign V) (x : Input V) : P.proj x ∈ P.cube

theorem BSLambda.PartialAssign.isLeast_dist {V : Type u_1} [Fintype V] [DecidableEq V] (P : PartialAssign V) (x : Input V) : IsLeast (hammingDist x '' ↑P.cube) (P.dist x)

dist(x, C(P)) really is the minimum Hamming distance to the subcube.

theorem BSLambda.PartialAssign.Conflict.disjoint_cube {V : Type u_1} [Fintype V] [DecidableEq V] {P Q : PartialAssign V} {v : V} (h : P.Conflict Q v) : Disjoint P.cube Q.cube

If P and Q conflict somewhere then their subcubes are disjoint.

Points, projections and flips

theorem BSLambda.PartialAssign.Sat.flipSet_singleton {V : Type u_1} [Fintype V] [DecidableEq V] {P : PartialAssign V} {x : Input V} (hx : P.Sat x) {v : V} (hv : v ∉ P.fixedSet) : P.Sat (flipSet x {v})

Flipping a coordinate that P leaves free keeps the point inside C(P).

theorem BSLambda.PartialAssign.eq_flipSet_proj_violSet {V : Type u_1} [Fintype V] [DecidableEq V] (P : PartialAssign V) (x : Input V) : x = flipSet (P.proj x) (P.violSet x)

Every point is recovered from its projection onto C(P) by flipping exactly the literals of P that it violates.

theorem BSLambda.PartialAssign.eq_flipSet_proj_of_dist_eq_one {V : Type u_1} [Fintype V] [DecidableEq V] {P : PartialAssign V} {x : Input V} (hd : P.dist x = 1) : ∃ (v : V), P.violSet x = {v} ∧ x = flipSet (P.proj x) {v}

A point at distance one from C(P) is a single flip of its projection, at the unique violated coordinate.

Two conflicting subcubes joined by a two-coordinate flip

theorem BSLambda.PartialAssign.violSet_eq_singleton_of_conflict {V : Type u_1} [Fintype V] [DecidableEq V] {P Q : PartialAssign V} {x : Input V} {p q : V} (hx : P.Sat x) (hy : Q.Sat (flipSet x {p, q})) (hc : P.Conflict Q q) (hp : p ∉ Q.fixedSet) : Q.violSet x = {q}

If x ∈ C(P), its {p, q}-flip lies in C(Q), P and Q conflict at q and Q leaves p free, then q is the only literal of Q that x violates.

theorem BSLambda.PartialAssign.violSet_eq_pair_of_conflict {V : Type u_1} [Fintype V] [DecidableEq V] {P Q : PartialAssign V} {x : Input V} {p q : V} (hx : P.Sat x) (hy : Q.Sat (flipSet x {p, q})) (hc : P.Conflict Q q) (hp : p ∈ P.fixedSet) : P.violSet (flipSet x {p, q}) = {p, q}

In the situation of violSet_eq_singleton_of_conflict, if instead P does fix p, then the flipped point violates exactly the two literals p and q of P.