Off-diagonal Gram entries

Sections 11.2 and 11.3 of bs_lambda.txt.

Let F : CertFamily V ι and let x ≠ y be two positive inputs of F.ind, with owners i = owner x and j = owner y. Write G = gram F.ind, so that G x y counts the common negative Hamming neighbours of x and y.

Two pure cube-geometry lemmas come first: a common neighbour of x ≠ y forces y = x^{p,q} for two distinct coordinates p ≠ q, and then the only possible common neighbours are the two midpoints x^p and x^q.

The classification itself is exists_flip_pair_of_gram_ne_zero: for a nonzero off-diagonal entry the owners differ, one of the two flipped coordinates is the (unique) conflict coordinate q of C_i and C_j, and the other one, p, is fixed by exactly one of the two certificates. Everything else in the file is a consequence:

• gram_eq_zero_of_owner_eq — if i = j then G x y = 0;
• gram_le_one — for x ≠ y always G x y ≤ 1;
• dist_eq_one_or_dist_eq_one — if G x y ≠ 0 then dist(x, C_j) = 1 or dist(y, C_i) = 1;
• exists_flip_pair_of_dist_eq_one — in the first case the ambiguity in p is resolved: C_i fixes p and C_j does not;
• dist_eq_two_of_dist_eq_one — in the first case dist(y, C_i) = 2 (so in particular the two alternatives above are exclusive) and x = π_{C_i}(y), the column bound of Section 11.3;
• exists_flip_proj — in the first case y = (π_{C_j} x)^p with p fixed by C_i (the row bound of Section 11.3);
• exists_flip_proj_self — and x = (π_{C_j} x)^q is another such flip, which is what produces the c - 1 rather than c in the row bound.

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

Cube geometry

The two facts about the Boolean cube that drive the whole classification: a pair of points with a common neighbour is a two-coordinate flip, and such a pair has only the two obvious common neighbours.

theorem BSLambda.exists_pair_of_common_nbr {V : Type u_1} [Fintype V] [DecidableEq V] {x y z : Input V} (hxy : x ≠ y) (hxz : hammingDist x z = 1) (hyz : hammingDist y z = 1) : ∃ (p : V) (q : V), p ≠ q ∧ y = flipSet x {p, q}

Two distinct inputs with a common Hamming neighbour differ in exactly two coordinates (Section 11.2).

theorem BSLambda.eq_flipSet_singleton_of_common_nbr {V : Type u_1} [Fintype V] [DecidableEq V] {x z : Input V} {p q : V} (hpq : p ≠ q) (hxz : hammingDist x z = 1) (hyz : hammingDist (flipSet x {p, q}) z = 1) : z = flipSet x {p} ∨ z = flipSet x {q}

The only common Hamming neighbours of x and its two-coordinate flip x^{p,q} are the two midpoints x^p and x^q: a third one would sit at distance three from x^{p,q} (Section 11.2).

theorem BSLambda.CertFamily.gram_eq_zero_of_owner_eq {V : Type u_1} [Fintype V] [DecidableEq V] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) {x y : Ones F.ind} (hxy : x ≠ y) (h : F.owner x = F.owner y) : gram F.ind x y = 0

Two distinct positive inputs with the same owner have no common negative neighbour: both flipped coordinates are free for the common owner, so both midpoints stay inside its certificate and are therefore positive (Section 11.2, case i = j).

theorem BSLambda.CertFamily.owner_ne_of_gram_ne_zero {V : Type u_1} [Fintype V] [DecidableEq V] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) {x y : Ones F.ind} (hxy : x ≠ y) (hne : gram F.ind x y ≠ 0) : F.owner x ≠ F.owner y

A nonzero off-diagonal Gram entry forces distinct owners (Section 11.2).

theorem BSLambda.CertFamily.ne_of_dist_eq_one {V : Type u_1} [Fintype V] [DecidableEq V] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) {x y : Ones F.ind} (hd : (F.P (F.owner y)).dist ↑x = 1) : x ≠ y

A point at distance one from another point's certificate is not that point, since every point satisfies its own certificate. This is why the oriented lemmas below take no separate x ≠ y hypothesis (Section 11.2).

theorem BSLambda.CertFamily.exists_flip_pair_of_gram_ne_zero {V : Type u_1} [Fintype V] [DecidableEq V] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) {x y : Ones F.ind} (hxy : x ≠ y) (hne : gram F.ind x y ≠ 0) : ∃ (p : V) (q : V), p ≠ q ∧ (F.P (F.owner x)).Conflict (F.P (F.owner y)) q ∧ ↑y = flipSet ↑x {p, q} ∧ (p ∈ (F.P (F.owner x)).fixedSet ∧ p ∉ (F.P (F.owner y)).fixedSet ∨ p ∈ (F.P (F.owner y)).fixedSet ∧ p ∉ (F.P (F.owner x)).fixedSet)

Classification of a nonzero off-diagonal Gram entry (Section 11.2). The two inputs differ in exactly two coordinates p ≠ q; the coordinate q is the unique conflict of the two owners' certificates, and the other coordinate p is fixed by exactly one of them.

theorem BSLambda.CertFamily.ind_flipSet_singleton_eq_true_or {V : Type u_1} [Fintype V] [DecidableEq V] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) {x y : Ones F.ind} {p q : V} (hpq : p ≠ q) (hy : ↑y = flipSet ↑x {p, q}) : F.ind (flipSet ↑x {p}) = true ∨ F.ind (flipSet ↑x {q}) = true

Of the two midpoints between x and y = x^{p,q}, at least one is positive: some certificate containing x or y leaves p or q free, because otherwise p and q would both be conflict coordinates of the two owners (Section 11.2).

theorem BSLambda.CertFamily.gram_le_one {V : Type u_1} [Fintype V] [DecidableEq V] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) {x y : Ones F.ind} (hxy : x ≠ y) : gram F.ind x y ≤ 1

Distinct positive inputs have at most one common negative neighbour: the two candidates are the midpoints x^p and x^q, and by ind_flipSet_singleton_eq_true_or at most one of them is negative (Section 11.2).

theorem BSLambda.CertFamily.dist_eq_one_or_dist_eq_one {V : Type u_1} [Fintype V] [DecidableEq V] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) {x y : Ones F.ind} (hxy : x ≠ y) (hne : gram F.ind x y ≠ 0) : (F.P (F.owner y)).dist ↑x = 1 ∨ (F.P (F.owner x)).dist ↑y = 1

Orientation of a nonzero off-diagonal entry: one of the two inputs lies at distance exactly one from the other's certificate (Section 11.2). In either case the conflict coordinate is the only violated literal, by PartialAssign.violSet_eq_singleton_of_conflict.

theorem BSLambda.CertFamily.exists_flip_pair_of_dist_eq_one {V : Type u_1} [Fintype V] [DecidableEq V] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) {x y : Ones F.ind} (hne : gram F.ind x y ≠ 0) (hd : (F.P (F.owner y)).dist ↑x = 1) : ∃ (p : V) (q : V), p ≠ q ∧ (F.P (F.owner x)).Conflict (F.P (F.owner y)) q ∧ ↑y = flipSet ↑x {p, q} ∧ p ∈ (F.P (F.owner x)).fixedSet ∧ p ∉ (F.P (F.owner y)).fixedSet

Oriented form of exists_flip_pair_of_gram_ne_zero: once it is known which of the two inputs is the near one, the alternative on p is resolved — C_i fixes p and C_j leaves it free, since otherwise x would violate both p and q of C_j (Section 11.3).

theorem BSLambda.CertFamily.dist_eq_two_of_dist_eq_one {V : Type u_1} [Fintype V] [DecidableEq V] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) {x y : Ones F.ind} (hne : gram F.ind x y ≠ 0) (hd : (F.P (F.owner y)).dist ↑x = 1) : (F.P (F.owner x)).dist ↑y = 2 ∧ ↑x = (F.P (F.owner x)).proj ↑y

The two alternatives of dist_eq_one_or_dist_eq_one are exclusive, and in the oriented case the reverse distance is exactly two and is realised by the nearest-point projection: y violates both p and q for C_i, and resetting them returns x (Section 11.3, column bound).

theorem BSLambda.CertFamily.exists_flip_proj {V : Type u_1} [Fintype V] [DecidableEq V] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) {x y : Ones F.ind} (hne : gram F.ind x y ≠ 0) (hd : (F.P (F.owner y)).dist ↑x = 1) : ∃ p ∈ (F.P (F.owner x)).fixedSet, ↑y = flipSet ((F.P (F.owner y)).proj ↑x) {p}

In the oriented case the projection of x onto C_j is x^q, and y is obtained from it by flipping the single coordinate p, which is fixed by C_i (Section 11.3, row bound).

theorem BSLambda.CertFamily.exists_flip_proj_self {V : Type u_1} [Fintype V] [DecidableEq V] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (F : CertFamily V ι) {i j : ι} (hij : i ≠ j) {x : Input V} (hx : (F.P i).Sat x) (hd : (F.P j).dist x = 1) : ∃ p₀ ∈ (F.P i).fixedSet, x = flipSet ((F.P j).proj x) {p₀}

The point x itself is a single flip of its own projection onto C_j, namely at the conflict coordinate, which is fixed by C_i. This removes one option from the row bound of Section 11.3.