Certificate families

A CertFamily V ι packages exactly the hypotheses of the Spectral Lemma of Section 11: a family P : ι → PartialAssign V of partial assignments such that

• every C_i = C(P i) has codimension c;
• every pair C_i, C_j (i ≠ j) has exactly one conflicting fixed literal;
• every point of the union has at most A other certificates at distance 1;
• every point of the union has at most B other certificates at distance at most 2.

F.ind is the indicator of the union, F.owner x is the unique index i with x ∈ C_i, and F.conflictCoord is the unique conflict coordinate of two distinct certificates.

The Spectral Lemma itself (lam F.ind ^ 2 ≤ c + 2 √((c-1) A B)) is proved in BSLambda/Spectral/CertUnion.lean.

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

structure BSLambda.CertFamily (V : Type u_3) (ι : Type u_4) [Fintype V] [DecidableEq V] [Fintype ι] [DecidableEq ι] : Type (max u_3 u_4)

The hypotheses of the Spectral Lemma of Section 11 of bs_lambda.txt: a family of pairwise-conflicting certificate subcubes of common codimension c with local certificate-list bounds A (at distance one) and B (at distance at most two).

• P : ι → PartialAssign V

  The partial assignment cutting out the i-th certificate subcube.

• c : ℕ

  The common codimension of the certificates.

• A : ℕ

  The radius-one certificate-list bound (A = 3 for the construction).

• B : ℕ

  The radius-two certificate-list bound (B = 7 for the construction).

• codim_eq (i : ι) : (self.P i).codim = self.c

  Every certificate has codimension c.

• uniqueConflict (i j : ι) : i ≠ j → ∃! v : V, (self.P i).Conflict (self.P j) v

  Distinct certificates have exactly one conflicting fixed literal.

• listOne (i : ι) (x : Input V) : (self.P i).Sat x → {j : ι | j ≠ i ∧ (self.P j).dist x = 1}.card ≤ self.A

  Property (L1) of Section 6.

• listTwo (i : ι) (x : Input V) : (self.P i).Sat x → {j : ι | j ≠ i ∧ (self.P j).dist x ≤ 2}.card ≤ self.B

  Property (L2) of Section 6.

noncomputable def BSLambda.CertFamily.conflictCoord {V : Type u_1} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) {i j : ι} (h : i ≠ j) : V

The unique conflict coordinate q_{ij} of two distinct certificates (Section 4).

Equations

• F.conflictCoord h = Exists.choose ⋯

theorem BSLambda.CertFamily.conflict_conflictCoord {V : Type u_1} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) {i j : ι} (h : i ≠ j) : (F.P i).Conflict (F.P j) (F.conflictCoord h)

The conflict coordinate does conflict.

theorem BSLambda.CertFamily.eq_conflictCoord {V : Type u_1} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) {i j : ι} (h : i ≠ j) {v : V} (hv : (F.P i).Conflict (F.P j) v) : v = F.conflictCoord h

The conflict coordinate is the only coordinate that conflicts.

The indicator of the union

ind is a distinct head symbol from PartialAssign.indUnion, so the simp lemmas of the latter do not fire on it; the first three lemmas below restate them for ind.

def BSLambda.CertFamily.ind {V : Type u_1} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) : Input V → Bool

The indicator f of the union of the certificate subcubes (Section 3.3).

Equations

• F.ind = BSLambda.PartialAssign.indUnion F.P

@[simp]

theorem BSLambda.CertFamily.ind_eq_true_iff {V : Type u_1} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) {x : Input V} : F.ind x = true ↔ ∃ (i : ι), (F.P i).Sat x

A point is positive exactly when some certificate subcube contains it.

@[simp]

theorem BSLambda.CertFamily.ind_eq_false_iff {V : Type u_1} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) {x : Input V} : F.ind x = false ↔ ∀ (i : ι), ¬(F.P i).Sat x

A point is negative exactly when no certificate subcube contains it.

theorem BSLambda.CertFamily.ind_eq_true_of_sat {V : Type u_1} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) {i : ι} {x : Input V} (h : (F.P i).Sat x) : F.ind x = true

Every point of a certificate subcube is positive.

theorem BSLambda.CertFamily.ind_flipSet_singleton_eq_true {V : Type u_1} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) {i : ι} {x : Input V} (hx : (F.P i).Sat x) {p : V} (hp : p ∉ (F.P i).fixedSet) : F.ind (flipSet x {p}) = true

Flipping a coordinate that a certificate leaves free keeps the point inside it, hence positive (Section 11.2). This is the source of every "one midpoint is positive" argument in BSLambda/Spectral/GramClass.lean.

theorem BSLambda.CertFamily.mem_fixedSet_of_ind_flipSet_singleton_eq_false {V : Type u_1} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) {i : ι} {x : Input V} (hx : (F.P i).Sat x) {p : V} (hp : F.ind (flipSet x {p}) = false) : p ∈ (F.P i).fixedSet

Contrapositive of ind_flipSet_singleton_eq_true: a negative single flip of a positive input can only happen at a coordinate that the input's own certificate fixes (Section 11.2).

theorem BSLambda.CertFamily.sat_unique {V : Type u_1} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) {i j : ι} {x : Input V} (hi : (F.P i).Sat x) (hj : (F.P j).Sat x) : i = j

Distinct certificates are disjoint, so a point lies in at most one of them (Section 4).

noncomputable def BSLambda.CertFamily.owner {V : Type u_1} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) (x : Ones F.ind) : ι

The owner of a positive input: the unique index whose certificate contains it (Section 4).

Equations

• F.owner x = ⋯.choose

theorem BSLambda.CertFamily.owner_sat {V : Type u_1} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) (x : Ones F.ind) : (F.P (F.owner x)).Sat ↑x

The owner's certificate does contain the point.

theorem BSLambda.CertFamily.owner_eq {V : Type u_1} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) {x : Ones F.ind} {i : ι} (h : (F.P i).Sat ↑x) : F.owner x = i

The owner is the only index whose certificate contains the point.

theorem BSLambda.CertFamily.sensAt_le_c {V : Type u_1} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) {i : ι} {x : Input V} (hx : (F.P i).Sat x) : sensAt F.ind x ≤ F.c

Only the c coordinates fixed by a containing certificate can be sensitive, so every positive input has sensitivity at most c (Section 11.1).

theorem BSLambda.CertFamily.gram_diag_le {V : Type u_1} {ι : Type u_2} [Fintype V] [DecidableEq V] [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) (x : Ones F.ind) : gram F.ind x x ≤ ↑F.c

The diagonal of the positive-side Gram matrix is bounded by c (Section 11.1).