The local lemma produces a good gate labelling #
This file proves the existence of a gate labelling satisfying the local certificate-list
conditions, and corresponds to Section 10 of bs_lambda.txt.
There are two families of bad events (Section 10):
- type 1 — one active radius-one flag on a five-element support, of probability
p₁ = 144⁻⁶; - type 2 — one consolidated radius-two internal obstruction on a nine-element
support, of probability at most
p₂ = radiusTwoConst · 144⁻²⁰.
Two events are declared adjacent when their vertex supports meet in at least two
vertices. This is a legitimate dependency graph: by disjoint_offDiag_of_card_inter_le_one,
supports meeting in at most one vertex use disjoint sets of gate variables.
The dependency counts of Section 10.1 are D11, D12, D21, D22 from
BSLambda/Numerics/LLLBounds.lean, where the two local-lemma inequalities
lll_cond_one and lll_cond_two have already been verified in exact rational
arithmetic. Feeding all of this into pr_avoid_pos_two_type gives a configuration
avoiding every bad event, and Section 10.3 turns that into the conditions (L1) and (L2).
Adapted for Lean Pool from Timeroot/BS_Lam at commit
7bd39a8d41ee7910d3296d0477ad18f8fff9d870; ported to Lean Pool with proof and dependency cleanup.
The index type of bad events #
The bad events (Section 10): an active radius-one flag, or a nine-element support carrying the consolidated radius-two obstruction. Inactive flags and supports of the wrong size are excluded, because the dependency counts of Section 10.1 count only the active patterns.
Equations
Instances For
Equations
The vertex support of a bad event: five vertices for type 1, nine for type 2.
Equations
Instances For
The variable support of a bad event: the arc variables internal to its vertices, that
is, the off-diagonal pairs of badVerts i.
Equations
Instances For
The type of a bad event: false for radius one, true for radius two.
Equations
Instances For
The bad event itself, as a set of gate configurations.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The probability bound for each type (Sections 8.1 and 9).
Equations
Instances For
The local-lemma weights of Section 10.2.
Equations
Instances For
The dependency counts of Section 10.1.
Equations
Instances For
The hypotheses of the local lemma #
Each bad event depends only on the arc variables internal to its own support (Section 10).
Two adjacent bad events have vertex supports meeting in at least two vertices: sharing a gate variable forces sharing two vertices (Section 10).
Counting helpers for the dependency bounds (Section 10.1) #
Two vertices shared between V and W yield a two-element subset of V contained in
W. This is what turns two_le_card_inter_of_mem_nbr into "the neighbour's support
contains one of the C(|V|,2) pairs of V" (Section 10.1).
The m-element subsets of ι meeting a fixed V in exactly s vertices are counted by
choosing the s shared vertices inside V and the other m - s outside V (Section 10.1);
this is the Finset-level refinement of Vandermonde's identity.
Summing card_filter_card_inter_eq over the possible intersection sizes bounds the number
of m-element subsets meeting V in at least two vertices (Section 10.1).
From dependency neighbourhoods to vertex supports (Section 10.1) #
The vertex support of a type-two neighbour of a bad event is a nine-element set meeting the event's own vertex set in at least two vertices (Section 10.1).
A type-two bad event is determined by its vertex support, so the type-two neighbours of a bad event are counted by their supports (Section 10.1).
The type-two neighbours of a bad event are counted by the nine-element supports meeting its vertex set in at least two vertices (Section 10.1).
Sharpened form of card_nbr_type_two_le for a type-two event: its own support is not one
of its neighbours, which is the - 1 in D22.
Every type-one neighbour of a bad event is an active flag whose support contains one of
the C(|V|,2) pairs of the event's vertex set V (Section 10.1).
Active radius-one flags through a fixed pair (Section 8.2) #
The common out-neighbourhood of a flag head (Section 8.2): the vertices dominated by
the owner q.1 and, when it is present, by the top vertex q.2. The bottom set of an active
flag is a subset of this (Flag1.Active.bot_subset_headOut), and its size is d = 7005 for a
Type-A head and t = 3502 for a Type-B head.
Equations
- BSLambda.LLL.headOut Arc q = q.2.elim (BSLambda.outNbrs Arc q.1) (BSLambda.commonOut Arc q.1)
Instances For
The counting scheme behind all six flag counts of Section 8.2. An active flag is
determined by its head (owner, top) together with its bottom set, and the bottom set is a
c-element subset of the common out-neighbourhood of the head containing the forced vertices
W. So if every flag satisfying P has its head in H and at most N unforced candidates
for the remaining c - |W| bottom vertices, there are at most |H| * C(N, c - |W|) of them.
Section 8.2, Type A, the fixed pair being owner and bottom vertex: at most
C(d-1,3) such flags, specializing to C(7004,3) in the construction.
Section 8.2, Type A with an owner outside the fixed pair: at most
t * C(d-2,2) such flags, with d = 7005, t = 3502 in the construction.
Section 8.2: at most N_A = C(d-1,3) + t C(d-2,2) = 143,100,492,510 Type-A flags pass
through the ordered pair u → v. The case owner = v is empty: it needs the reverse arc.
Section 8.2, Type B, the fixed pair being the ordered top pair (a, h) = (u, v): at
most C(t,3) such flags, with t = 3502 in the construction.
Section 8.2, Type B with u the upper top vertex and v a bottom vertex: at most
t * C(t-1,2) such flags, with t = 3502 in the construction.
Section 8.2, Type B with u the owner and v a bottom vertex: at most
t * C(t-1,2) such flags, with t = 3502 in the construction.
Section 8.2, Type B with both fixed vertices at the bottom: the top pair is one of the
C(t,2) arcs between the common in-neighbours of u and v, and the third bottom vertex is
one of t - 2, giving at most C(t,2) * (t-2) such flags.
Section 8.2: at most N_B = C(t,3) + 2 t C(t-1,2) + C(t,2)(t-2) = 71,519,595,000
Type-B flags pass through the ordered pair u → v. Of the nine possible pairs of roles for
u and v, two are impossible and three need the reverse arc v → u.
Section 8.2: at most N_1 = N_A + N_B = 214,620,087,510 active flags pass through the
ordered pair u → v.
Section 8.2: at most N_1 active flags pass through any two-element vertex set.
The four reduced dependency counts #
A type-one event has at most D11 type-one neighbours (Section 10.1).
A type-one event has at most D12 type-two neighbours (Section 10.1).
A type-two event has at most D21 type-one neighbours (Section 10.1).
A type-two event has at most D22 other type-two neighbours (Section 10.1).
The dependency counts, packaged as required by pr_avoid_pos_two_type. Double regularity
is what pins the number N_1 of active flags through a pair (Section 8.2).
The good configuration #
Section 10.2: some gate configuration avoids every bad event.
Consequences for certificate lists (Section 10.3) #
Section 10.3: a good configuration admits no radius-one internal obstruction on a
five-element support: mem_flagEvent_of_intObstruction would produce an active flag whose
event contains ω.
Section 10.3: a good configuration admits no radius-two internal obstruction on a
nine-element support, since such an obstruction puts ω into radiusTwoEvent.
Section 10.3: a positive point of C_h cannot have four further certificates of a
five-element support at distance at most one.
Section 10.3: a positive point of C_h cannot have eight further certificates of a
nine-element support at distance at most two.
The counting step behind both (L1) and (L2): if adjoining h to any m + 1 indices
satisfying P gives a support on which P is impossible, then at most m indices other
than h satisfy P.
(L1) (Section 10.3): a positive point has at most three other certificates at distance one.
(L2) (Section 10.3): a positive point has at most seven other certificates at distance at most two.
Section 10: a gate labelling satisfying the local certificate-list conditions (L1) and (L2) exists.