The counterexample

Fix the Paley tournament on k = 14011 vertices and a gate labelling γ : Idx → Idx → Fin 144 satisfying the local certificate-list conditions (L1) and (L2) of Section 6. The function ind Arc γ is the indicator of the union of the certificate subcubes of Section 3.

The two headline estimates are

• bs_ge — bs(f) ≥ 14011 (Section 5), and
• lam_sq_le — lambda(f)^2 ≤ 7149 + 2 √150108 (Sections 11–12),

with U := 7149 + 2 √150108 < 7924 < 14011. Setting

α := 2 log 14011 / log U > 2,

we obtain lambda(f)^α ≤ 14011 ≤ bs(f), and, for the m-fold self-composition F_m of Section 14 (using BSLambda.lam_iterFun_eq, the multiplicativity of lambda under composition, which is proved in BSLambda/Spectral/Multiplicative.lean),

• lam_iter_rpow_le_bs — lambda(F_m)^α ≤ bs(F_m), and
• bs_div_lam_sq_ge — bs(F_m) / lambda(F_m)^2 ≥ (14011/U)^m with 14011/U > 1.768,

which tends to infinity and so refutes bs(f) = O(lambda(f)^2).

Everything in this file is stated for an arbitrary gate labelling satisfying (L1) and (L2); BSLambda/LLL/GateExists.lean is where such a labelling is produced.

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

@[reducible, inline]

abbrev BSLambda.Final.Idx : Type

The vertex set of the Paley tournament: Z/14011.

Equations

• BSLambda.Final.Idx = ZMod 14011

def BSLambda.Final.Arc : Idx → Idx → Bool

The arc relation of the Paley tournament on 14011 vertices (Section 2).

Equations

• BSLambda.Final.Arc = BSLambda.paleyArc 14011

theorem BSLambda.Final.isDR_arc : IsDRTournamentWith Arc 7005 3502

The Paley orientation is a doubly regular tournament with d = 7005 and t = 3502 (Section 2).

theorem BSLambda.Final.isTournament_arc : IsTournament Arc

The Paley orientation is in particular a tournament (Section 2).

@[reducible, inline]

abbrev BSLambda.Final.r : ℕ

The number of coordinates in each block, r = 144 (Section 3).

Equations

• BSLambda.Final.r = 144

@[reducible, inline]

abbrev BSLambda.Final.certCodim : ℕ

The certificate codimension c = r + d = 144 + 7005 = 7149 (Section 3.2).

Equations

• BSLambda.Final.certCodim = 7149

noncomputable def BSLambda.Final.U : ℝ

The spectral bound U = 7149 + 2 √150108 of Section 12.

Equations

• BSLambda.Final.U = 7149 + 2 * √150108

noncomputable def BSLambda.Final.alpha : ℝ

The separation exponent α = 2 log 14011 / log U of Section 14.

Equations

• BSLambda.Final.alpha = 2 * Real.log 14011 / Real.log BSLambda.Final.U

theorem BSLambda.Final.card_idx : Fintype.card Idx = 14011

The tournament has 14011 vertices (Section 2).

theorem BSLambda.Final.codim_cert_eq (γ : Idx → Idx → Fin r) (i : Idx) : (Construction.cert Arc γ i).codim = certCodim

Every certificate has codimension c = 7149 (Section 3.2).

theorem BSLambda.Final.uniqueConflict_cert (γ : Idx → Idx → Fin r) (i j : Idx) (hij : i ≠ j) : ∃! v : Construction.Coord Idx r, (Construction.cert Arc γ i).Conflict (Construction.cert Arc γ j) v

Distinct certificates have exactly one conflicting fixed literal (Section 4).

def BSLambda.Final.ListOne (γ : Idx → Idx → Fin r) : Prop

Property (L1) of Section 6: every positive point has at most three other certificates at distance one.

Equations

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

def BSLambda.Final.ListTwo (γ : Idx → Idx → Fin r) : Prop

Property (L2) of Section 6: every positive point has at most seven other certificates at distance at most two.

Equations

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

def BSLambda.Final.family (γ : Idx → Idx → Fin r) (h₁ : ListOne γ) (h₂ : ListTwo γ) : CertFamily (Construction.Coord Idx r) Idx

The certificate family attached to a gate labelling satisfying (L1) and (L2) (Sections 3, 4 and 6).

Equations

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

@[simp]

theorem BSLambda.Final.family_A (γ : Idx → Idx → Fin r) (h₁ : ListOne γ) (h₂ : ListTwo γ) : (family γ h₁ h₂).A = 3

@[simp]

theorem BSLambda.Final.family_B (γ : Idx → Idx → Fin r) (h₁ : ListOne γ) (h₂ : ListTwo γ) : (family γ h₁ h₂).B = 7

@[simp]

theorem BSLambda.Final.family_c (γ : Idx → Idx → Fin r) (h₁ : ListOne γ) (h₂ : ListTwo γ) : (family γ h₁ h₂).c = certCodim

@[simp]

theorem BSLambda.Final.family_P (γ : Idx → Idx → Fin r) (h₁ : ListOne γ) (h₂ : ListTwo γ) (i : Idx) (a✝ : Construction.Coord Idx r) : (family γ h₁ h₂).P i a✝ = Construction.cert Arc γ i a✝

theorem BSLambda.Final.family_ind {γ : Idx → Idx → Fin r} (h₁ : ListOne γ) (h₂ : ListTwo γ) : (family γ h₁ h₂).ind = Construction.ind Arc γ

The indicator of the certificate family is definitionally the indicator Construction.ind of the union of the certificate subcubes (Section 3.3).

Block sensitivity

theorem BSLambda.Final.bs_ge {γ : Idx → Idx → Fin r} : 14011 ≤ bs (Construction.ind Arc γ)

Block sensitivity (Section 5): bs(f) ≥ 14011.

theorem BSLambda.Final.bs_ge_real {γ : Idx → Idx → Fin r} : 14011 ≤ ↑(bs (Construction.ind Arc γ))

bs_ge cast into ℝ, the form in which the numeric comparisons below use it.

The spectral bound

theorem BSLambda.Final.family_bound_eq_U {γ : Idx → Idx → Fin r} (h₁ : ListOne γ) (h₂ : ListTwo γ) : ↑(family γ h₁ h₂).c + 2 * (family γ h₁ h₂).offBound = U

Substituting c = 7149, A = 3, B = 7 into the Spectral Lemma's right-hand side c + 2 √(A (c-1) B) gives exactly U = 7149 + 2 √150108 (Section 12).

theorem BSLambda.Final.lam_sq_le {γ : Idx → Idx → Fin r} (h₁ : ListOne γ) (h₂ : ListTwo γ) : lam (Construction.ind Arc γ) ^ 2 ≤ U

The spectral bound (Sections 11–12): lambda(f)^2 ≤ 7149 + 2 √150108.

theorem BSLambda.Final.sqrt_150108_lt : √150108 < 387.5

√150108 < 387.5, the only numerical estimate needed in Section 12.

theorem BSLambda.Final.U_lt : U < 7924

U < 7924 (Section 12).

theorem BSLambda.Final.U_ge : 7149 ≤ U

7149 ≤ U; in particular 1 < U and 0 < log U (Section 12).

theorem BSLambda.Final.U_pos : 0 < U

U is positive, since 7149 ≤ U.

theorem BSLambda.Final.log_U_pos : 0 < Real.log U

log U is positive.

The exponent

theorem BSLambda.Final.two_lt_alpha : 2 < alpha

The exponent exceeds two (Section 14): α > 2, because U < 14011.

theorem BSLambda.Final.U_rpow_alpha : U ^ (alpha / 2) = 14011

U ^ (α/2) = 14011 (Section 14).

theorem BSLambda.Final.lam_rpow_le {γ : Idx → Idx → Fin r} (h₁ : ListOne γ) (h₂ : ListTwo γ) : lam (Construction.ind Arc γ) ^ alpha ≤ 14011

The separation for the seed (Sections 12 and 14): lambda(f)^α ≤ 14011 ≤ bs(f).

Self-composition

theorem BSLambda.Final.bs_iter_ge {γ : Idx → Idx → Fin r} (m : ℕ) : 14011 ^ m ≤ bs (iterFun (Construction.ind Arc γ) m)

Block sensitivity of the iterates (Section 14): bs(F_m) ≥ 14011 ^ m.

theorem BSLambda.Final.lam_iter_rpow_le_bs {γ : Idx → Idx → Fin r} (h₁ : ListOne γ) (h₂ : ListTwo γ) (m : ℕ) : lam (iterFun (Construction.ind Arc γ) m) ^ alpha ≤ ↑(bs (iterFun (Construction.ind Arc γ) m))

The separation for the iterates (Section 14): lambda(F_m)^α ≤ bs(F_m).

theorem BSLambda.Final.bs_div_lam_sq_ge {γ : Idx → Idx → Fin r} (h₁ : ListOne γ) (h₂ : ListTwo γ) (m : ℕ) : (14011 / U) ^ m * lam (iterFun (Construction.ind Arc γ) m) ^ 2 ≤ ↑(bs (iterFun (Construction.ind Arc γ) m))

The ratio blows up (Section 14): bs(F_m) / lambda(F_m)^2 ≥ (14011/U)^m, and 14011/U > 1.768. This refutes bs(f) = O(lambda(f)^2).

theorem BSLambda.Final.ratio_gt : 1.768 < 14011 / U

The growth ratio exceeds 1.768 (Section 12).

The separation with an explicit exponent

theorem BSLambda.Final.lam_sq_lt_bs {γ : Idx → Idx → Fin r} (h₁ : ListOne γ) (h₂ : ListTwo γ) : lam (Construction.ind Arc γ) ^ 2 < ↑(bs (Construction.ind Arc γ))

bs(f) > lambda(f)^2 (Sections 5 and 12): the seed has a gap by a factor 14011/7924 > 1.768. Self-composition amplifies this gap without bound, as proved in exists_ratio_blowup.

theorem BSLambda.Final.rpow_1_06_lt : 7924 ^ 1.06 < 14011

7924 ^ 1.06 < 14011 (Section 14). Raising to the fiftieth power turns this into the integer inequality 7924 ^ 53 < 14011 ^ 50, which avoids estimating any logarithm. It is the quantitative form of 2.12 < alpha (the true value being 2.1269738...).

theorem BSLambda.Final.lam_rpow_212_lt_bs {γ : Idx → Idx → Fin r} (h₁ : ListOne γ) (h₂ : ListTwo γ) : lam (Construction.ind Arc γ) ^ 2.12 < ↑(bs (Construction.ind Arc γ))

bs(f) > lambda(f)^2.12 (Sections 5, 12 and 14). This is lam_rpow_le with the irrational exponent alpha = 2.1269738... replaced by the explicit rational 2.12, and with a strict inequality.

Existence of the gate labelling

theorem BSLambda.Final.exists_listOne_listTwo : ∃ (γ : Idx → Idx → Fin r), ListOne γ ∧ ListTwo γ

Existence of a good gate labelling (Sections 6-10): the asymmetric Lovász Local Lemma produces a labelling γ : Idx → Idx → Fin 144 satisfying both (L1) and (L2).

The unconditional statements

theorem BSLambda.Final.exists_bs_gt_lam_rpow : ∃ (f : Input (Construction.Coord Idx r) → Bool), lam f ^ 2.12 < ↑(bs f)

The headline separation (Sections 5-12). There is a total Boolean function f with

bs(f) > lambda(f) ^ 2.12.

Self-composition amplifies the seed separation; exists_ratio_blowup below supplies the family of inequalities used to refute bs(f) = O(lambda(f)^2).

theorem BSLambda.Final.exists_counterexample : ∃ (γ : Idx → Idx → Fin r), 14011 ≤ bs (Construction.ind Arc γ) ∧ lam (Construction.ind Arc γ) ^ 2 ≤ U ∧ lam (Construction.ind Arc γ) ^ alpha ≤ ↑(bs (Construction.ind Arc γ))

The counterexample (Sections 5 and 12). There is a total Boolean function f with bs(f) ≥ 14011 and lambda(f)^2 ≤ U = 7149 + 2 √150108 < 7924; since α = 2 log 14011 / log U > 2, it also satisfies lambda(f)^α ≤ bs(f).

theorem BSLambda.Final.exists_ratio_blowup : ∃ (γ : Idx → Idx → Fin r), ∀ (m : ℕ), (14011 / U) ^ m * lam (iterFun (Construction.ind Arc γ) m) ^ 2 ≤ ↑(bs (iterFun (Construction.ind Arc γ) m))

bs is not O(lambda²) (Section 14). There is a function f whose m-fold self-compositions satisfy bs(F_m) / lambda(F_m)^2 ≥ (14011/U)^m with 14011/U > 1.768, so the ratio tends to infinity. Unlike in Section 14, the multiplicativity of lambda under composition is not imported but proved (BSLambda.lam_iterFun_eq).