Internal obstructions

The bad events of the local lemma are not the global proximity events "some point of C_h is close to many other certificates": those depend on gate labels with an endpoint outside the support, and so have no local dependency graph (Section 7).

Instead we keep only the necessary conditions that mention arcs internal to the support. For a support S, an owner h ∈ S and a radius ell, a centered internal obstruction is a family of putative zero sets Z j ⊆ Fin r — the coordinates of block j at which a hypothetical point is 0 — such that Z h = ∅, every gate out of h lands in its target zero set, and every non-owner spends at most ell on its own zeros plus its internal misses. This is IntObstruction, and intObstruction_of_close is the implication of Section 7: a genuine proximity configuration produces one. The converse is neither claimed nor needed.

Section 8 analyses radius one. Every non-owner has already spent its whole budget on its unique conflict with the owner, so the set of non-owners beating the owner has at most one element, leaving exactly two patterns on a five-element support: Type A, where the owner dominates the other four, and Type B, where a single vertex a beats the owner and both beat the remaining three. In either case all six arcs among the non-owners are forced to reproduce the owner's gate label in their head block, an event of probability r ^ (-6).

Section 9 consolidates radius two on a nine-element support into the single event radiusTwoEvent of probability at most radiusTwoConst / r ^ 20.

The lemmas below take an IsTournament hypothesis rather than an IsDRTournamentWith instance: none of them needs double regularity.

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

@[reducible, inline]

abbrev BSLambda.LLL.GateCfg (ι : Type u_2) (r : ℕ) : Type u_2

The arc variables: an independent uniform gate label for each ordered pair.

Equations

• BSLambda.LLL.GateCfg ι r = (ι × ι → Fin r)

def BSLambda.LLL.toGamma {ι : Type u_1} {r : ℕ} : GateCfg ι r → ι → ι → Fin r

Read a configuration of the product space as a gate labelling.

Equations

• BSLambda.LLL.toGamma = Function.curry

theorem BSLambda.LLL.disjoint_offDiag_of_card_inter_le_one {ι : Type u_1} [DecidableEq ι] {S T : Finset ι} (h : (S ∩ T).card ≤ 1) : Disjoint S.offDiag T.offDiag

Supports meeting in at most one vertex share no arc variable (Section 7). This is what makes the dependency graph of Section 10 — adjacency iff the supports share at least two vertices — a valid one.

The variables of a support S are its off-diagonal pairs: no event ever reads a loop variable ω (v, v), since every arc is irreflexive and every conditioned owner gate (h, j) has j a non-owner, and leaving the diagonal out is exactly what makes this true.

def BSLambda.LLL.ownerGates {ι : Type u_1} (i : ι) (T : Finset ι) : Finset (ι × ι)

The owner gates of i into T: the arc variables (i, j) for j ∈ T. Both probability estimates condition on this family and pin the remaining internal arc labels to values read off it.

Equations

• BSLambda.LLL.ownerGates i T = {i} ×ˢ T

@[simp]

theorem BSLambda.LLL.mem_ownerGates {ι : Type u_1} {i : ι} {T : Finset ι} {p : ι × ι} : p ∈ ownerGates i T ↔ p.1 = i ∧ p.2 ∈ T

The arcs inside a vertex set

def BSLambda.LLL.arcSet {ι : Type u_1} (Arc : ι → ι → Bool) (T : Finset ι) : Finset (ι × ι)

The arcs internal to T: the ordered pairs of distinct vertices of T carrying a forward arc. These are exactly the variables constrained by the radius-one flag event of Section 8.1 (with T the non-owners of the flag) and by the radius-two branches of Section 9 (with T the non-owners of the support).

Equations

• BSLambda.LLL.arcSet Arc T = {p ∈ T.offDiag | Arc p.1 p.2 = true}

@[simp]

theorem BSLambda.LLL.mem_arcSet {ι : Type u_1} {Arc : ι → ι → Bool} {T : Finset ι} {p : ι × ι} : p ∈ arcSet Arc T ↔ (p.1 ∈ T ∧ p.2 ∈ T ∧ p.1 ≠ p.2) ∧ Arc p.1 p.2 = true

theorem BSLambda.LLL.card_arcSet_swap {ι : Type u_1} (Arc : ι → ι → Bool) (T : Finset ι) : (arcSet (fun (a b : ι) => Arc b a) T).card = (arcSet Arc T).card

Swapping the two entries is a bijection from the arcs of T to the reversed arcs.

theorem BSLambda.LLL.arcSet_union_arcSet_swap {ι : Type u_1} [DecidableEq ι] {Arc : ι → ι → Bool} (hT : IsTournament Arc) (T : Finset ι) : arcSet Arc T ∪ arcSet (fun (a b : ι) => Arc b a) T = T.offDiag

In a tournament the arcs of T and the reversed arcs of T together exhaust the off-diagonal pairs of T.

theorem BSLambda.LLL.disjoint_arcSet_arcSet_swap {ι : Type u_1} {Arc : ι → ι → Bool} (hT : IsTournament Arc) (T : Finset ι) : Disjoint (arcSet Arc T) (arcSet (fun (a b : ι) => Arc b a) T)

A pair cannot carry an arc in both directions.

theorem BSLambda.LLL.card_arcSet {ι : Type u_1} {Arc : ι → ι → Bool} (hT : IsTournament Arc) (T : Finset ι) : (arcSet Arc T).card = T.card.choose 2

A tournament on T has exactly C(|T|, 2) internal arcs: six for the four non-owners of a radius-one flag, and Q = 28 for the eight non-owners of Section 9.

Internal obstructions (Section 7)

def BSLambda.LLL.missSet {ι : Type u_1} {r : ℕ} (Arc : ι → ι → Bool) (γ : ι → ι → Fin r) (Z : ι → Finset (Fin r)) (T : Finset ι) (i : ι) : Finset ι

The misses of i inside T (Section 7): the out-neighbours j ∈ T of i whose gate label γ i j avoids the putative zero set Z j, so that the gate literal of the arc i → j is violated. A miss costs i one unit of its budget.

Equations

• BSLambda.LLL.missSet Arc γ Z T i = {j ∈ T | Arc i j = true ∧ γ i j ∉ Z j}

@[simp]

theorem BSLambda.LLL.mem_missSet {ι : Type u_1} {r : ℕ} {Arc : ι → ι → Bool} {γ : ι → ι → Fin r} {Z : ι → Finset (Fin r)} {T : Finset ι} {i j : ι} : j ∈ missSet Arc γ Z T i ↔ j ∈ T ∧ Arc i j = true ∧ γ i j ∉ Z j

theorem BSLambda.LLL.missSet_subset_missSet {ι : Type u_1} {r : ℕ} {Arc : ι → ι → Bool} {γ : ι → ι → Fin r} {Z : ι → Finset (Fin r)} {T T' : Finset ι} {i : ι} (hT : T ⊆ T') : missSet Arc γ Z T i ⊆ missSet Arc γ Z T' i

theorem BSLambda.LLL.missSet_congr {ι : Type u_1} {r : ℕ} {Arc : ι → ι → Bool} {γ γ' : ι → ι → Fin r} {S : Finset ι} {i : ι} (hT : IsTournament Arc) (hi : i ∈ S) (Z : ι → Finset (Fin r)) (hagree : ∀ a ∈ S, ∀ b ∈ S, a ≠ b → γ a b = γ' a b) : missSet Arc γ Z S i = missSet Arc γ' Z S i

The misses out of i only read gate labels of arcs with both endpoints in S, so they are unchanged by a relabelling that fixes those arcs.

def BSLambda.LLL.IntObstruction {ι : Type u_1} {r : ℕ} (Arc : ι → ι → Bool) (ell : ℕ) (S : Finset ι) (h : ι) (γ : ι → ι → Fin r) : Prop

A centered internal obstruction of radius ell (Section 7). The sets Z j are the putative zero coordinates of a hypothetical point in block j. Z h = ∅ because a point of C_h is 1 throughout its own block; each gate out of the owner is forced into its target zero set; and every other index of the support spends at most ell on its own zeros together with its internal misses.

Equations

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

theorem BSLambda.LLL.intObstruction_congr {ι : Type u_1} {r : ℕ} {Arc : ι → ι → Bool} (hT : IsTournament Arc) {ell : ℕ} {S : Finset ι} {h : ι} (hh : h ∈ S) {γ γ' : ι → ι → Fin r} (hagree : ∀ a ∈ S, ∀ b ∈ S, a ≠ b → γ a b = γ' a b) (hobs : IntObstruction Arc ell S h γ) : IntObstruction Arc ell S h γ'

A centered internal obstruction only reads gate labels of arcs with both endpoints in its support, so it transports along any relabelling that fixes those arcs.

def BSLambda.LLL.zeroSet {ι : Type u_1} {r : ℕ} (x : Input (Construction.Coord ι r)) (i : ι) : Finset (Fin r)

The zero set of an input inside a block.

Equations

• BSLambda.LLL.zeroSet x i = {k : Fin r | x (i, k) = false}

@[simp]

theorem BSLambda.LLL.mem_zeroSet {ι : Type u_1} {r : ℕ} {x : Input (Construction.Coord ι r)} {i : ι} {k : Fin r} : k ∈ zeroSet x i ↔ x (i, k) = false

theorem BSLambda.LLL.zeroSet_owner_eq_empty {ι : Type u_1} [DecidableEq ι] {r : ℕ} {Arc : ι → ι → Bool} {γ : ι → ι → Fin r} {h : ι} {x : Input (Construction.Coord ι r)} (hx : (Construction.cert Arc γ h).Sat x) : zeroSet x h = ∅

The zero set of a point of C_h in the owner's own block is empty.

theorem BSLambda.LLL.mem_violSet_cert {ι : Type u_1} [Fintype ι] [DecidableEq ι] {r : ℕ} {Arc : ι → ι → Bool} {γ : ι → ι → Fin r} {i : ι} {x : Input (Construction.Coord ι r)} {v : Construction.Coord ι r} : v ∈ (Construction.cert Arc γ i).violSet x ↔ v.1 = i ∧ x v = false ∨ v.1 ≠ i ∧ Arc i v.1 = true ∧ v.2 = γ i v.1 ∧ x v = true

The literals of P_i violated by x, spelled out: either a coordinate of the owner block B_i where x is 0, or the gate coordinate of an outgoing arc where x is 1.

theorem BSLambda.LLL.violSet_cert_eq {ι : Type u_1} [Fintype ι] [DecidableEq ι] {r : ℕ} (Arc : ι → ι → Bool) (hT : IsTournament Arc) (γ : ι → ι → Fin r) (i : ι) (x : Input (Construction.Coord ι r)) : (Construction.cert Arc γ i).violSet x = Finset.image (fun (k : Fin r) => (i, k)) (zeroSet x i) ∪ Finset.image (Construction.gateCoord γ i) (missSet Arc γ (zeroSet x) Finset.univ i)

The violated literals of P_i split into the zeros of x in the owner block and the outgoing gates whose target coordinate x fails to zero out.

theorem BSLambda.LLL.disjoint_zeros_image_gate_image {ι : Type u_1} [Fintype ι] [DecidableEq ι] {r : ℕ} (Arc : ι → ι → Bool) (hT : IsTournament Arc) (γ : ι → ι → Fin r) (i : ι) (x : Input (Construction.Coord ι r)) : Disjoint (Finset.image (fun (k : Fin r) => (i, k)) (zeroSet x i)) (Finset.image (Construction.gateCoord γ i) (missSet Arc γ (zeroSet x) Finset.univ i))

The two halves of the violation set are disjoint: both halves shrink to the two halves of Construction.disjoint_block_image_gateCoord, the owner block and the image of the full out-neighbourhood.

theorem BSLambda.LLL.dist_cert_eq {ι : Type u_1} [Fintype ι] [DecidableEq ι] {r : ℕ} (Arc : ι → ι → Bool) (hT : IsTournament Arc) (γ : ι → ι → Fin r) (i : ι) (x : Input (Construction.Coord ι r)) : (Construction.cert Arc γ i).dist x = (zeroSet x i).card + (missSet Arc γ (zeroSet x) Finset.univ i).card

The distance from x to C_i counts the zeros of x in block i together with the gates out of i that miss their target zero set.

theorem BSLambda.LLL.intObstruction_of_close {ι : Type u_1} [Fintype ι] [DecidableEq ι] {r : ℕ} {Arc : ι → ι → Bool} (hT : IsTournament Arc) {γ : ι → ι → Fin r} {S : Finset ι} {h : ι} {ell : ℕ} {x : Input (Construction.Coord ι r)} (hx : (Construction.cert Arc γ h).Sat x) (hclose : ∀ i ∈ S, i ≠ h → (Construction.cert Arc γ i).dist x ≤ ell) : IntObstruction Arc ell S h γ

Section 7: a genuine proximity configuration yields an internal obstruction. Only external misses have been discarded, so the implication is valid.

Radius-one flags (Section 8)

structure BSLambda.LLL.Flag1 (ι : Type u_2) [DecidableEq ι] : Type u_2

The data of a candidate radius-one flag on a five-element support: an owner (owner), an optional second top vertex (top) — absent for Type A, present for Type B — and the remaining bottom vertices (bot) (Section 8).

• owner : ι

  The proposed owner.

• top : Option ι

  The second top vertex, for Type B patterns.

• bot : Finset ι

  The bottom vertices.

theorem BSLambda.LLL.Flag1.ext_iff {ι : Type u_2} {inst✝ : DecidableEq ι} {x y : Flag1 ι} : x = y ↔ x.owner = y.owner ∧ x.top = y.top ∧ x.bot = y.bot

theorem BSLambda.LLL.Flag1.ext {ι : Type u_2} {inst✝ : DecidableEq ι} {x y : Flag1 ι} (owner : x.owner = y.owner) (top : x.top = y.top) (bot : x.bot = y.bot) : x = y

def BSLambda.LLL.Flag1.equivProd {ι : Type u_1} [DecidableEq ι] : Flag1 ι ≃ ι × Option ι × Finset ι

A flag is a triple (owner, top, bot); both the DecidableEq and the Fintype instance are transported along this equivalence. deriving DecidableEq does not work here: the derived instance builds its own decision procedure for the Finset field instead of using the ambient Finset.decidableEq, and Lean rejects it as not definitionally equal.

Equations

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

@[instance_reducible]

instance BSLambda.LLL.Flag1.instDecidableEq {ι : Type u_1} [DecidableEq ι] : DecidableEq (Flag1 ι)

Equations

• BSLambda.LLL.Flag1.instDecidableEq = ⋯.decidableEq

@[instance_reducible]

instance BSLambda.LLL.Flag1.instFintype {ι : Type u_1} [Fintype ι] [DecidableEq ι] : Fintype (Flag1 ι)

Equations

• BSLambda.LLL.Flag1.instFintype = Fintype.ofEquiv (ι × Option ι × Finset ι) BSLambda.LLL.Flag1.equivProd.symm

def BSLambda.LLL.Flag1.nonOwners {ι : Type u_1} [DecidableEq ι] (F : Flag1 ι) : Finset ι

The non-owners of a flag.

Equations

• F.nonOwners = match F.top with | none => F.bot | some v => insert v F.bot

def BSLambda.LLL.Flag1.supp {ι : Type u_1} [DecidableEq ι] (F : Flag1 ι) : Finset ι

The five-element support of a flag.

Equations

• F.supp = insert F.owner F.nonOwners

theorem BSLambda.LLL.Flag1.nonOwners_of_top_eq_none {ι : Type u_1} [DecidableEq ι] {F : Flag1 ι} (ha : F.top = none) : F.nonOwners = F.bot

theorem BSLambda.LLL.Flag1.nonOwners_of_top_eq_some {ι : Type u_1} [DecidableEq ι] {F : Flag1 ι} {a : ι} (ha : F.top = some a) : F.nonOwners = insert a F.bot

@[simp]

theorem BSLambda.LLL.Flag1.mem_nonOwners {ι : Type u_1} [DecidableEq ι] {F : Flag1 ι} {j : ι} : j ∈ F.nonOwners ↔ j ∈ F.top ∨ j ∈ F.bot

@[simp]

theorem BSLambda.LLL.Flag1.mem_supp {ι : Type u_1} [DecidableEq ι] {F : Flag1 ι} {j : ι} : j ∈ F.supp ↔ j = F.owner ∨ j ∈ F.nonOwners

Activeness

def BSLambda.LLL.Flag1.Active {ι : Type u_1} [DecidableEq ι] (F : Flag1 ι) (Arc : ι → ι → Bool) : Prop

Activeness of a flag (Section 8): the tournament must realise the pattern. For Type A the owner dominates four vertices; for Type B the second top vertex beats the owner and both top vertices beat the three bottom ones.

Consumers should use the two unfolding lemmas Flag1.active_iff_of_top_eq_none and Flag1.active_iff_of_top_eq_some, or the named accessors in the Flag1.Active namespace, rather than unfolding this definition.

Equations

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

theorem BSLambda.LLL.Flag1.active_iff_of_top_eq_none {ι : Type u_1} [DecidableEq ι] {F : Flag1 ι} {Arc : ι → ι → Bool} (ha : F.top = none) : F.Active Arc ↔ F.owner ∉ F.bot ∧ F.bot.card = 4 ∧ ∀ j ∈ F.bot, Arc F.owner j = true

Activeness of a Type A flag: the owner dominates its four bottom vertices.

theorem BSLambda.LLL.Flag1.active_iff_of_top_eq_some {ι : Type u_1} [DecidableEq ι] {F : Flag1 ι} {Arc : ι → ι → Bool} {a : ι} (ha : F.top = some a) : F.Active Arc ↔ F.owner ≠ a ∧ F.owner ∉ F.bot ∧ a ∉ F.bot ∧ F.bot.card = 3 ∧ Arc a F.owner = true ∧ ∀ j ∈ F.bot, Arc F.owner j = true ∧ Arc a j = true

Activeness of a Type B flag: the owner, the second top vertex a and the three bottom vertices are distinct, a beats the owner, and both top vertices dominate every bottom vertex.

theorem BSLambda.LLL.Flag1.Active.owner_notMem_nonOwners {ι : Type u_1} [DecidableEq ι] {F : Flag1 ι} {Arc : ι → ι → Bool} (hF : F.Active Arc) : F.owner ∉ F.nonOwners

The owner of an active flag is not one of its non-owners.

theorem BSLambda.LLL.Flag1.Active.owner_notMem_bot {ι : Type u_1} [DecidableEq ι] {F : Flag1 ι} {Arc : ι → ι → Bool} (hF : F.Active Arc) : F.owner ∉ F.bot

The owner of an active flag is not one of its bottom vertices.

theorem BSLambda.LLL.Flag1.Active.card_bot_of_top_eq_none {ι : Type u_1} [DecidableEq ι] {F : Flag1 ι} {Arc : ι → ι → Bool} (hF : F.Active Arc) (ha : F.top = none) : F.bot.card = 4

An active Type A flag has four bottom vertices.

theorem BSLambda.LLL.Flag1.Active.card_bot_of_top_eq_some {ι : Type u_1} [DecidableEq ι] {F : Flag1 ι} {Arc : ι → ι → Bool} {a : ι} (hF : F.Active Arc) (ha : F.top = some a) : F.bot.card = 3

An active Type B flag has three bottom vertices.

theorem BSLambda.LLL.Flag1.Active.owner_ne_top {ι : Type u_1} [DecidableEq ι] {F : Flag1 ι} {Arc : ι → ι → Bool} {a : ι} (hF : F.Active Arc) (ha : F.top = some a) : F.owner ≠ a

The owner of an active flag differs from its second top vertex.

theorem BSLambda.LLL.Flag1.Active.top_notMem_bot {ι : Type u_1} [DecidableEq ι] {F : Flag1 ι} {Arc : ι → ι → Bool} {a : ι} (hF : F.Active Arc) (ha : F.top = some a) : a ∉ F.bot

The second top vertex of an active flag is not a bottom vertex.

theorem BSLambda.LLL.Flag1.Active.arc_top_owner {ι : Type u_1} [DecidableEq ι] {F : Flag1 ι} {Arc : ι → ι → Bool} {a : ι} (hF : F.Active Arc) (ha : F.top = some a) : Arc a F.owner = true

The second top vertex of an active flag beats the owner.

theorem BSLambda.LLL.Flag1.Active.arc_owner_bot {ι : Type u_1} [DecidableEq ι] {F : Flag1 ι} {Arc : ι → ι → Bool} {j : ι} (hF : F.Active Arc) (hj : j ∈ F.bot) : Arc F.owner j = true

The owner of an active flag dominates every bottom vertex, in both patterns.

theorem BSLambda.LLL.Flag1.Active.arc_top_bot {ι : Type u_1} [DecidableEq ι] {F : Flag1 ι} {Arc : ι → ι → Bool} {a j : ι} (hF : F.Active Arc) (ha : F.top = some a) (hj : j ∈ F.bot) : Arc a j = true

The second top vertex of an active flag dominates every bottom vertex.

theorem BSLambda.LLL.Flag1.Active.card_nonOwners {ι : Type u_1} [DecidableEq ι] {F : Flag1 ι} {Arc : ι → ι → Bool} (hF : F.Active Arc) : F.nonOwners.card = 4

An active flag has exactly four non-owners.

theorem BSLambda.LLL.Flag1.Active.card_supp {ι : Type u_1} [DecidableEq ι] {F : Flag1 ι} {Arc : ι → ι → Bool} (hF : F.Active Arc) : F.supp.card = 5

An active flag has a five-element support.

The flag event (Section 8.1)

theorem BSLambda.LLL.Flag1.Active.card_arcs {ι : Type u_1} [DecidableEq ι] {F : Flag1 ι} {Arc : ι → ι → Bool} (hT : IsTournament Arc) (hF : F.Active Arc) : (arcSet Arc F.nonOwners).card = 6

An active flag has exactly six internal arcs among its four non-owners: C(4, 2) = 6.

theorem BSLambda.LLL.Flag1.snd_mem_bot {ι : Type u_1} [DecidableEq ι] (F : Flag1 ι) {Arc : ι → ι → Bool} (hT : IsTournament Arc) (hF : F.Active Arc) {p : ι × ι} (hp : p ∈ arcSet Arc F.nonOwners) : p.2 ∈ F.bot

Every non-owner arc of an active flag has its head in F.bot, so the owner's gate into that head block is defined; and its tail is not the owner, so its label is a variable distinct from the conditioned owner gates.

noncomputable def BSLambda.LLL.flagEvent {ι : Type u_1} [Fintype ι] [DecidableEq ι] {r : ℕ} (Arc : ι → ι → Bool) (F : Flag1 ι) : Finset (GateCfg ι r)

The active radius-one flag event (Section 8.1): every internal non-owner arc selects exactly the zero coordinate forced by the owner's gate in its head block.

Equations

• BSLambda.LLL.flagEvent Arc F = {ω : BSLambda.LLL.GateCfg ι r | ∀ p ∈ BSLambda.LLL.arcSet Arc F.nonOwners, ω p = ω (F.owner, p.2)}

theorem BSLambda.LLL.mem_flagEvent {ι : Type u_1} [Fintype ι] [DecidableEq ι] {r : ℕ} {Arc : ι → ι → Bool} {F : Flag1 ι} {ω : GateCfg ι r} : ω ∈ flagEvent Arc F ↔ ∀ p ∈ arcSet Arc F.nonOwners, ω p = ω (F.owner, p.2)

theorem BSLambda.LLL.Flag1.mem_offDiag_supp {ι : Type u_1} [DecidableEq ι] {Arc : ι → ι → Bool} (hT : IsTournament Arc) {F : Flag1 ι} (hF : F.Active Arc) {p : ι × ι} (hp : p ∈ arcSet Arc F.nonOwners) : p ∈ F.supp.offDiag ∧ (F.owner, p.2) ∈ F.supp.offDiag

Both variables read by the flag event at an internal arc are variables of its support.

theorem BSLambda.LLL.flagEvent_determined {ι : Type u_1} [Fintype ι] [DecidableEq ι] {r : ℕ} {Arc : ι → ι → Bool} (hT : IsTournament Arc) {F : Flag1 ι} (hF : F.Active Arc) : Determined F.supp.offDiag (flagEvent Arc F)

The flag event is determined by the arc variables inside its support.

theorem BSLambda.LLL.Flag1.disjoint_gates_arcs {ι : Type u_1} [DecidableEq ι] (F : Flag1 ι) {Arc : ι → ι → Bool} (hF : F.Active Arc) : Disjoint (ownerGates F.owner F.bot) (arcSet Arc F.nonOwners)

The owner gates conditioned on in Section 8.1 are disjoint from the internal arcs, so the two families of variables are independent.

theorem BSLambda.LLL.Flag1.gate_mem_gates {ι : Type u_1} [DecidableEq ι] (F : Flag1 ι) {Arc : ι → ι → Bool} (hT : IsTournament Arc) (hF : F.Active Arc) {p : ι × ι} (hp : p ∈ arcSet Arc F.nonOwners) : (F.owner, p.2) ∈ ownerGates F.owner F.bot

The owner gate into the head block of an internal arc is one of the conditioned gates.

theorem BSLambda.LLL.pr_flagEvent_le_pow {ι : Type u_1} [Fintype ι] [DecidableEq ι] {r : ℕ} [NeZero r] {Arc : ι → ι → Bool} (hT : IsTournament Arc) {F : Flag1 ι} (hF : F.Active Arc) : pr (flagEvent Arc F) ≤ (1 / ↑r) ^ (arcSet Arc F.nonOwners).card

Section 8.1: the flag event pins one uniform label per internal arc, each to a single value read off the owner gates.

theorem BSLambda.LLL.pr_flagEvent_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {r : ℕ} [NeZero r] {Arc : ι → ι → Bool} (hT : IsTournament Arc) {F : Flag1 ι} (hF : F.Active Arc) : pr (flagEvent Arc F) ≤ 1 / ↑r ^ 6

Section 8.1: an active radius-one flag has probability r ^ (-6). After conditioning on the owner gates, the six non-owner arc labels are independent and uniform, and each is pinned to a single value.

The two radius-one patterns

theorem BSLambda.LLL.intObstruction_one_of_owner_arc {ι : Type u_1} {r : ℕ} {Arc : ι → ι → Bool} {γ : ι → ι → Fin r} {S : Finset ι} {h : ι} {Z : ι → Finset (Fin r)} (hgate : ∀ j ∈ S, Arc h j = true → γ h j ∈ Z j) (hbud : ∀ i ∈ S, i ≠ h → (Z i).card + (missSet Arc γ Z S i).card ≤ 1) {j : ι} (hj : j ∈ S) (hjh : j ≠ h) (harc : Arc h j = true) : Z j = {γ h j} ∧ ∀ k ∈ S, Arc j k = true → γ j k ∈ Z k

Under a radius-one obstruction centred at h, a vertex j dominated by h has its zero set pinned to the single owner gate γ h j, and hence no internal miss of its own.

theorem BSLambda.LLL.intObstruction_one_of_arc_to_owner {ι : Type u_1} {r : ℕ} {Arc : ι → ι → Bool} {γ : ι → ι → Fin r} {S : Finset ι} {h : ι} (hh : h ∈ S) {Z : ι → Finset (Fin r)} (hZh : Z h = ∅) (hbud : ∀ i ∈ S, i ≠ h → (Z i).card + (missSet Arc γ Z S i).card ≤ 1) {j : ι} (hj : j ∈ S) (hjh : j ≠ h) (harc : Arc j h = true) : Z j = ∅ ∧ ∀ k ∈ S, k ≠ h → Arc j k = true → γ j k ∈ Z k

Under a radius-one obstruction centred at h, a vertex j that beats h already spends its whole budget on the miss j → h, so Z j = ∅ and it has no other miss.

theorem BSLambda.LLL.intObstruction_one_card_beats_le_one {ι : Type u_1} {r : ℕ} {Arc : ι → ι → Bool} (hT : IsTournament Arc) {γ : ι → ι → Fin r} {S : Finset ι} {h : ι} (hh : h ∈ S) (hobs : IntObstruction Arc 1 S h γ) : {j ∈ S | Arc j h = true}.card ≤ 1

Section 8: at most one vertex of the support beats the centre h; two of them would give one a second internal miss.

theorem BSLambda.LLL.intObstruction_one_pattern {ι : Type u_1} {r : ℕ} {Arc : ι → ι → Bool} (hT : IsTournament Arc) {γ : ι → ι → Fin r} {S : Finset ι} {h : ι} (hh : h ∈ S) (hobs : IntObstruction Arc 1 S h γ) : (∀ j ∈ S, j ≠ h → Arc h j = true) ∨ ∃ a ∈ S, a ≠ h ∧ Arc a h = true ∧ ∀ j ∈ S, j ≠ h → j ≠ a → Arc h j = true ∧ Arc a j = true

Section 8: a radius-one obstruction realises exactly one of the two patterns — either h dominates the whole support (Type A), or a single a beats h and the two of them jointly dominate the rest (Type B).

theorem BSLambda.LLL.intObstruction_one_gate_eq {ι : Type u_1} {r : ℕ} {Arc : ι → ι → Bool} (hT : IsTournament Arc) {γ : ι → ι → Fin r} {S : Finset ι} {h : ι} (hh : h ∈ S) (hobs : IntObstruction Arc 1 S h γ) {i j : ι} (hi : i ∈ S) (hj : j ∈ S) (hih : i ≠ h) (hjh : j ≠ h) (harc : Arc i j = true) (hhj : Arc h j = true) : γ i j = γ h j

Section 8: every non-owner arc into a dominated j carries the owner's label, since Z j is the singleton {γ h j}.

theorem BSLambda.LLL.active_flag_typeA {ι : Type u_1} [DecidableEq ι] {Arc : ι → ι → Bool} {S : Finset ι} (hS : S.card = 5) {h : ι} (hh : h ∈ S) (hdom : ∀ j ∈ S, j ≠ h → Arc h j = true) : { owner := h, top := none, bot := S.erase h }.Active Arc ∧ { owner := h, top := none, bot := S.erase h }.supp = S

The Type A flag built from a dominating centre is active with support S.

theorem BSLambda.LLL.active_flag_typeB {ι : Type u_1} [DecidableEq ι] {Arc : ι → ι → Bool} {S : Finset ι} (hS : S.card = 5) {h a : ι} (hh : h ∈ S) (ha : a ∈ S) (hah : a ≠ h) (harc : Arc a h = true) (hdom : ∀ j ∈ S, j ≠ h → j ≠ a → Arc h j = true ∧ Arc a j = true) : { owner := h, top := some a, bot := (S.erase h).erase a }.Active Arc ∧ { owner := h, top := some a, bot := (S.erase h).erase a }.supp = S

The Type B flag built from a centre h and the unique a beating it is active with support S.

theorem BSLambda.LLL.gate_eq_of_active_of_intObstruction {ι : Type u_1} [DecidableEq ι] {r : ℕ} {Arc : ι → ι → Bool} (hT : IsTournament Arc) {γ : ι → ι → Fin r} {S : Finset ι} {h : ι} (hh : h ∈ S) (hobs : IntObstruction Arc 1 S h γ) {F : Flag1 ι} (hF : F.Active Arc) (hsupp : F.supp = S) (hFh : F.owner = h) (p : ι × ι) : p ∈ arcSet Arc F.nonOwners → γ p.1 p.2 = γ h p.2

Section 8: all internal arcs of the flag produced from a radius-one obstruction carry the owner's gate label.

theorem BSLambda.LLL.exists_active_flag_of_intObstruction {ι : Type u_1} [DecidableEq ι] {r : ℕ} {Arc : ι → ι → Bool} (hT : IsTournament Arc) {γ : ι → ι → Fin r} {S : Finset ι} (hS : S.card = 5) {h : ι} (hh : h ∈ S) (hobs : IntObstruction Arc 1 S h γ) : ∃ (F : Flag1 ι), F.Active Arc ∧ F.supp = S ∧ F.owner = h ∧ ∀ p ∈ arcSet Arc F.nonOwners, γ p.1 p.2 = γ h p.2

Section 8: on a five-element support a radius-one internal obstruction forces one of the two patterns. If h → j then |Z j| = 1 and j can have no internal miss; if j → h then the arc j → h is automatically a miss, so Z j = ∅ and again j has no other miss. Hence any two vertices beating h would give one of them a second miss, so at most one vertex beats h.

theorem BSLambda.LLL.mem_flagEvent_of_intObstruction {ι : Type u_1} [Fintype ι] [DecidableEq ι] {r : ℕ} {Arc : ι → ι → Bool} (hT : IsTournament Arc) {ω : GateCfg ι r} {S : Finset ι} (hS : S.card = 5) {h : ι} (hh : h ∈ S) (hobs : IntObstruction Arc 1 S h (toGamma ω)) : ∃ (F : Flag1 ι), F.Active Arc ∧ F.supp = S ∧ ω ∈ flagEvent Arc F

Section 8: the flag produced from a radius-one obstruction satisfies its event.

Radius-two obstructions (Section 9)

noncomputable def BSLambda.LLL.radiusTwoEvent {ι : Type u_1} [Fintype ι] [DecidableEq ι] {r : ℕ} (Arc : ι → ι → Bool) (S : Finset ι) : Finset (GateCfg ι r)

The consolidated radius-two internal obstruction on a nine-element support (Section 9): some vertex of the support owns a radius-two internal obstruction.

Equations

• BSLambda.LLL.radiusTwoEvent Arc S = {ω : BSLambda.LLL.GateCfg ι r | ∃ h ∈ S, BSLambda.LLL.IntObstruction Arc 2 S h (BSLambda.LLL.toGamma ω)}

theorem BSLambda.LLL.mem_radiusTwoEvent {ι : Type u_1} [Fintype ι] [DecidableEq ι] {r : ℕ} {Arc : ι → ι → Bool} {S : Finset ι} {ω : GateCfg ι r} : ω ∈ radiusTwoEvent Arc S ↔ ∃ h ∈ S, IntObstruction Arc 2 S h (toGamma ω)

Membership in the radius-two event.

theorem BSLambda.LLL.radiusTwoEvent_determined {ι : Type u_1} [Fintype ι] [DecidableEq ι] {r : ℕ} {Arc : ι → ι → Bool} (hT : IsTournament Arc) (S : Finset ι) : Determined S.offDiag (radiusTwoEvent Arc S)

The radius-two event is determined by the arc variables inside its support.

def BSLambda.LLL.radiusTwoOwnerConst : ℕ

The Section 9 constant for a single owner: l of the eight non-owners spend their residual discrepancy on a discretionary zero (C(8,l) choices), at most C(28, 8-l) arcs are exceptional, and each of the remaining 20 + l arc labels has two admissible values.

Equations

• BSLambda.LLL.radiusTwoOwnerConst = 2 ^ 20 * ∑ l ∈ Finset.range 9, Nat.choose 8 l * Nat.choose 28 (8 - l) * 2 ^ l

def BSLambda.LLL.radiusTwoConst : ℕ

The constant radiusTwoConst = 9 · 2 ^ 20 · ∑_{l=0}^{8} C(8,l) C(28,8-l) 2 ^ l of Section 9.

Equations

• BSLambda.LLL.radiusTwoConst = 1300311466573824

theorem BSLambda.LLL.radiusTwoConst_eq_nine_mul : radiusTwoConst = 9 * radiusTwoOwnerConst

radiusTwoConst has one radiusTwoOwnerConst for each of the nine possible owners.

def BSLambda.LLL.missArcs {ι : Type u_1} {r : ℕ} (Arc : ι → ι → Bool) (γ : ι → ι → Fin r) (Z : ι → Finset (Fin r)) (T : Finset ι) : Finset (ι × ι)

The missing arcs of T: the internal arcs whose gate label avoids the target zero set. Section 9 covers these by an exceptional set X.

Equations

• BSLambda.LLL.missArcs Arc γ Z T = {p ∈ BSLambda.LLL.arcSet Arc T | γ p.1 p.2 ∉ Z p.2}

def BSLambda.LLL.discSet {ι : Type u_1} {r : ℕ} (γ : ι → ι → Fin r) (Z : ι → Finset (Fin r)) (T : Finset ι) (h : ι) : Finset ι

The discretionary vertices of T: those whose zero set is not just the owner gate, so that they have spent their residual discrepancy on a zero of their own.

Equations

• BSLambda.LLL.discSet γ Z T h = {j ∈ T | ¬Z j ⊆ {γ h j}}

@[simp]

theorem BSLambda.LLL.mem_missArcs {ι : Type u_1} {r : ℕ} {Arc : ι → ι → Bool} {γ : ι → ι → Fin r} {Z : ι → Finset (Fin r)} {T : Finset ι} {p : ι × ι} : p ∈ missArcs Arc γ Z T ↔ p ∈ arcSet Arc T ∧ γ p.1 p.2 ∉ Z p.2

@[simp]

theorem BSLambda.LLL.mem_discSet {ι : Type u_1} {r : ℕ} {γ : ι → ι → Fin r} {Z : ι → Finset (Fin r)} {T : Finset ι} {h j : ι} : j ∈ discSet γ Z T h ↔ j ∈ T ∧ ¬Z j ⊆ {γ h j}

theorem BSLambda.LLL.missArcs_subset {ι : Type u_1} {r : ℕ} {Arc : ι → ι → Bool} {γ : ι → ι → Fin r} {Z : ι → Finset (Fin r)} {T : Finset ι} : missArcs Arc γ Z T ⊆ arcSet Arc T

theorem BSLambda.LLL.discSet_subset {ι : Type u_1} {r : ℕ} {γ : ι → ι → Fin r} {Z : ι → Finset (Fin r)} {T : Finset ι} {h : ι} : discSet γ Z T h ⊆ T

theorem BSLambda.LLL.card_discSet_eq_sum {ι : Type u_1} {r : ℕ} {γ : ι → ι → Fin r} {Z : ι → Finset (Fin r)} (T : Finset ι) (h : ι) : (discSet γ Z T h).card = ∑ j ∈ T, if Z j ⊆ {γ h j} then 0 else 1

The discretionary vertices are counted by their indicator.

theorem BSLambda.LLL.card_missArcs_eq_sum {ι : Type u_1} {r : ℕ} {Arc : ι → ι → Bool} {γ : ι → ι → Fin r} {Z : ι → Finset (Fin r)} (hT : IsTournament Arc) (T : Finset ι) : (missArcs Arc γ Z T).card = ∑ j ∈ T, (missSet Arc γ Z T j).card

The missing arcs of T fibre over their tails, the fibre above j being the misses of j inside T.

noncomputable def BSLambda.LLL.branch2 {ι : Type u_1} [Fintype ι] [DecidableEq ι] {r : ℕ} (Arc : ι → ι → Bool) (S : Finset ι) (h : ι) (L : Finset ι) (w : (j : ι) → j ∈ L → Fin r) (X : Finset (ι × ι)) : Finset (GateCfg ι r)

One branch of the Section 9 enumeration: the owner is h, the non-owners in L spend their residual discrepancy on the discretionary zero w, the arcs of X are the exceptional (missing) ones, and every other internal non-owner arc hits the two-element target set of its head block.

Equations

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

theorem BSLambda.LLL.mem_branch2 {ι : Type u_1} [Fintype ι] [DecidableEq ι] {r : ℕ} {Arc : ι → ι → Bool} {S : Finset ι} {h : ι} {L : Finset ι} {w : (j : ι) → j ∈ L → Fin r} {X : Finset (ι × ι)} {ω : GateCfg ι r} : ω ∈ branch2 Arc S h L w X ↔ ∀ p ∈ arcSet Arc (S.erase h), p ∉ X → ω p = ω (h, p.2) ∨ ω p = if hp : p.2 ∈ L then w p.2 hp else ω (h, p.2)

theorem BSLambda.LLL.radiusTwoEvent_subset_biUnion_owner {ι : Type u_1} [Fintype ι] [DecidableEq ι] {r : ℕ} (Arc : ι → ι → Bool) (S : Finset ι) : radiusTwoEvent Arc S ⊆ S.biUnion fun (h : ι) => {ω : GateCfg ι r | IntObstruction Arc 2 S h (toGamma ω)}

Section 9: the consolidated event is the union over the nine possible owners.

theorem BSLambda.LLL.disjoint_ownerGates_arcSet {ι : Type u_1} [DecidableEq ι] (Arc : ι → ι → Bool) (S : Finset ι) (h : ι) : Disjoint (ownerGates h (S.erase h)) (arcSet Arc (S.erase h))

The eight conditioned owner gates are disjoint from the arcs among the non-owners.

theorem BSLambda.LLL.card_arcSet_erase {ι : Type u_1} [DecidableEq ι] {Arc : ι → ι → Bool} (hT : IsTournament Arc) {S : Finset ι} (hS : S.card = 9) {h : ι} (hh : h ∈ S) : (arcSet Arc (S.erase h)).card = 28

The eight non-owners of a nine-element support span Q = C(8, 2) = 28 internal arcs.

theorem BSLambda.LLL.intObstruction_two_nonowner {ι : Type u_1} [DecidableEq ι] {r : ℕ} [NeZero r] {Arc : ι → ι → Bool} (hT : IsTournament Arc) {S : Finset ι} {h : ι} (hh : h ∈ S) {γ : ι → ι → Fin r} {Z : ι → Finset (Fin r)} (hZh : Z h = ∅) (hgate : ∀ j ∈ S, Arc h j = true → γ h j ∈ Z j) {j : ι} (hj : j ∈ S.erase h) (hbud : (Z j).card + (missSet Arc γ Z S j).card ≤ 2) : (∃ (z : Fin r), Z j ⊆ {γ h j, z}) ∧ ((missSet Arc γ Z (S.erase h) j).card + if Z j ⊆ {γ h j} then 0 else 1) ≤ 1

Section 9, budget at one non-owner. If h → j then γ h j ∈ Z j; if j → h then the arc j → h is an automatic miss because Z h = ∅. Either way Z j is contained in a two-element set consisting of the owner gate and one discretionary zero, and j has at most one further internal discrepancy, which it loses if it uses the discretionary zero.

theorem BSLambda.LLL.card_miss_add_card_disc_le {ι : Type u_1} [DecidableEq ι] {r : ℕ} [NeZero r] {Arc : ι → ι → Bool} (hT : IsTournament Arc) {S : Finset ι} (hS : S.card = 9) {h : ι} (hh : h ∈ S) {γ : ι → ι → Fin r} {Z : ι → Finset (Fin r)} (hZh : Z h = ∅) (hgate : ∀ j ∈ S, Arc h j = true → γ h j ∈ Z j) (hbud : ∀ i ∈ S, i ≠ h → (Z i).card + (missSet Arc γ Z S i).card ≤ 2) : (missArcs Arc γ Z (S.erase h)).card + (discSet γ Z (S.erase h) h).card ≤ 8

Section 9: if l non-owners take a discretionary zero, the total number of misses among the twenty-eight internal non-owner arcs is at most 8 - l.

theorem BSLambda.LLL.intObstruction_two_data {ι : Type u_1} [Fintype ι] [DecidableEq ι] {r : ℕ} [NeZero r] {Arc : ι → ι → Bool} (hT : IsTournament Arc) {S : Finset ι} (hS : S.card = 9) {h : ι} (hh : h ∈ S) {ω : GateCfg ι r} (hobs : IntObstruction Arc 2 S h (toGamma ω)) : ∃ (L : Finset ι) (w : (j : ι) → j ∈ L → Fin r) (X : Finset (ι × ι)), L ⊆ S.erase h ∧ X ⊆ arcSet Arc (S.erase h) ∧ X.card + L.card = 8 ∧ ω ∈ branch2 Arc S h L w X

Section 9: every radius-two internal obstruction with owner h lies in one of the enumerated branches.

theorem BSLambda.LLL.obs2_subset_branches {ι : Type u_1} [Fintype ι] [DecidableEq ι] {r : ℕ} [NeZero r] {Arc : ι → ι → Bool} (hT : IsTournament Arc) {S : Finset ι} (hS : S.card = 9) {h : ι} (hh : h ∈ S) : {ω : GateCfg ι r | IntObstruction Arc 2 S h (toGamma ω)} ⊆ (S.erase h).powerset.biUnion fun (L : Finset ι) => (L.pi fun (x : ι) => Finset.univ).biUnion fun (w : (a : ι) → a ∈ L → Fin r) => (Finset.powersetCard (8 - L.card) (arcSet Arc (S.erase h))).biUnion fun (X : Finset (ι × ι)) => branch2 Arc S h L w X

Section 9: the radius-two event for a fixed owner is covered by the branches.

theorem BSLambda.LLL.pr_branch2_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {r : ℕ} [NeZero r] {Arc : ι → ι → Bool} {S : Finset ι} {h : ι} {L : Finset ι} (w : (j : ι) → j ∈ L → Fin r) {X : Finset (ι × ι)} (hX : X ⊆ arcSet Arc (S.erase h)) : pr (branch2 Arc S h L w X) ≤ (2 / ↑r) ^ ((arcSet Arc (S.erase h)).card - X.card)

Section 9: in a fixed branch the 28 - |X| remaining arc labels are independent and uniform after conditioning on the owner gates, and each must hit a target set of size at most two.

theorem BSLambda.LLL.sum_branch_pow_eq {ι : Type u_1} [DecidableEq ι] {r : ℕ} [NeZero r] {S : Finset ι} {h : ι} (hh : h ∈ S) (hS : S.card = 9) {AA : Finset (ι × ι)} (hAA : AA.card = 28) : ∑ L ∈ (S.erase h).powerset, ∑ _w ∈ L.pi fun (x : ι) => Finset.univ, ∑ _X ∈ Finset.powersetCard (8 - L.card) AA, (2 / ↑r) ^ (AA.card - (8 - L.card)) = ↑radiusTwoOwnerConst / ↑r ^ 20

Section 9: evaluating the triple sum of the branch bounds: collapse the two inner constant sums, then regroup the outer powerset sum by cardinality.

theorem BSLambda.LLL.pr_intObstruction_owner_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {r : ℕ} [NeZero r] {Arc : ι → ι → Bool} (hT : IsTournament Arc) {S : Finset ι} (hS : S.card = 9) {h : ι} (hh : h ∈ S) : pr {ω : Cfg fun (x : ι × ι) => Fin r | IntObstruction Arc 2 S h (toGamma ω)} ≤ ↑radiusTwoOwnerConst / ↑r ^ 20

Section 9: the radius-two obstruction for a fixed owner has probability at most radiusTwoConst / (9 * r ^ 20).

theorem BSLambda.LLL.pr_radiusTwoEvent_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {r : ℕ} [NeZero r] {Arc : ι → ι → Bool} (hT : IsTournament Arc) {S : Finset ι} (hS : S.card = 9) : pr (radiusTwoEvent Arc S) ≤ ↑radiusTwoConst / ↑r ^ 20

Section 9: the consolidated radius-two obstruction on a nine-element support has probability at most radiusTwoConst / r ^ 20. Each non-owner has one residual discrepancy; if l of them spend it on a discretionary zero there are at most C(8,l) r ^ l choices, at most C(28, 8-l) choices of an exceptional superset of the missing arcs, and each of the remaining 20 + l arc labels must hit a target set of size at most two.