The uniform 26/25 factor and the finite bootstrap

The sequence A_n

structure HypergraphLowerBound.FrameSpec : Type

A support gadget together with its stated capacity vector.

• parts : List ℕ

  The capacity assigned to each part.

• rawSupports : List (List ℕ)

  Raw support patterns, represented as lists of part indices.

• rawSupports_ok (s : List ℕ) : s ∈ self.rawSupports → s.Nodup ∧ (∀ i ∈ s, i < self.parts.length) ∧ 2 ≤ s.length

  The raw support patterns are valid subsets of the part indices of size at least two.

def HypergraphLowerBound.FrameSpec.t (spec : FrameSpec) : ℕ

The arity of a frame specification.

Equations

• spec.t = spec.parts.length

def HypergraphLowerBound.FrameSpec.cap (spec : FrameSpec) : Fin spec.t → ℕ

The capacity vector of a frame specification.

Equations

• spec.cap i = spec.parts.get i

def HypergraphLowerBound.supportPatternOfList {t : ℕ} (s : List ℕ) (hIn : ∀ i ∈ s, i < t) (hNodup : s.Nodup) (hCard : 2 ≤ s.length) : SupportPattern t

Encode a list of support indices as a support pattern.

Equations

• HypergraphLowerBound.supportPatternOfList s hIn hNodup hCard = ⟨(List.pmap (fun (i : ℕ) (hi : i < t) => ⟨i, hi⟩) s hIn).toFinset, ⋯⟩

def HypergraphLowerBound.FrameSpec.supportList (spec : FrameSpec) : List (SupportPattern spec.t)

The support list of a frame specification, interpreted on Fin spec.t.

Equations

• spec.supportList = List.pmap (fun (s : List ℕ) (hs : s ∈ spec.rawSupports) => HypergraphLowerBound.supportPatternOfList s ⋯ ⋯ ⋯) spec.rawSupports ⋯

def HypergraphLowerBound.FrameSpec.supports (spec : FrameSpec) : Multiset (SupportPattern spec.t)

The support multiset of a frame specification, interpreted on Fin spec.t.

Equations

• spec.supports = ↑spec.supportList

def HypergraphLowerBound.FrameSpec.bonus (spec : FrameSpec) : ℕ

The total number of support occurrences in a frame specification.

Equations

• spec.bonus = spec.rawSupports.length

def HypergraphLowerBound.frameWitnesses {t : ℕ} (T I : Finset (Fin t)) (S : SupportPattern t) : Bool

Decide whether a support pattern contributes to the frame inequality for T and I.

Equations

• HypergraphLowerBound.frameWitnesses T I S = decide (↑S ⊆ T ∧ (↑S ∩ I).card = 1)

def HypergraphLowerBound.FrameSpec.countWitnesses (spec : FrameSpec) (T I : Finset (Fin spec.t)) : ℕ

The computable count of support occurrences contributing to the frame inequality.

Equations

• spec.countWitnesses T I = List.countP (HypergraphLowerBound.frameWitnesses T I) spec.supportList

def HypergraphLowerBound.FrameSpec.IsValid (spec : FrameSpec) : Prop

A frame specification is valid when its support multiset satisfies the corresponding frame inequalities.

Equations

• spec.IsValid = ∀ (T I : Finset (Fin spec.t)), I ⊆ T → spec.countWitnesses T I ≤ (T \ I).sum spec.cap

@[instance_reducible]

instance HypergraphLowerBound.instDecidableIsValid (spec : FrameSpec) : Decidable spec.IsValid

Equations

• HypergraphLowerBound.instDecidableIsValid spec = id (id inferInstance)

def HypergraphLowerBound.sup2 (a b : ℕ) : List ℕ

A support list with 2 specified indices.

Equations

• HypergraphLowerBound.sup2 a b = [a, b]

def HypergraphLowerBound.sup3 (a b c : ℕ) : List ℕ

A support list with 3 specified indices.

Equations

• HypergraphLowerBound.sup3 a b c = [a, b, c]

def HypergraphLowerBound.sup4 (a b c d : ℕ) : List ℕ

A support list with 4 specified indices.

Equations

• HypergraphLowerBound.sup4 a b c d = [a, b, c, d]

def HypergraphLowerBound.sup5 (a b c d e : ℕ) : List ℕ

A support list with 5 specified indices.

Equations

• HypergraphLowerBound.sup5 a b c d e = [a, b, c, d, e]

def HypergraphLowerBound.sup6 (a b c d e f : ℕ) : List ℕ

A support list with 6 specified indices.

Equations

• HypergraphLowerBound.sup6 a b c d e f = [a, b, c, d, e, f]

def HypergraphLowerBound.sup7 (a b c d e f g : ℕ) : List ℕ

A support list with 7 specified indices.

Equations

• HypergraphLowerBound.sup7 a b c d e f g = [a, b, c, d, e, f, g]

def HypergraphLowerBound.sup8 (a b c d e f g h : ℕ) : List ℕ

A support list with 8 specified indices.

Equations

• HypergraphLowerBound.sup8 a b c d e f g h = [a, b, c, d, e, f, g, h]

def HypergraphLowerBound.sup9 (a b c d e f g h i : ℕ) : List ℕ

A support list with 9 specified indices.

Equations

• HypergraphLowerBound.sup9 a b c d e f g h i = [a, b, c, d, e, f, g, h, i]

def HypergraphLowerBound.mkFrame (parts : List ℕ) (rawSupports : List (List ℕ)) (h : ∀ s ∈ rawSupports, s.Nodup ∧ (∀ i ∈ s, i < parts.length) ∧ 2 ≤ s.length) : FrameSpec

Build a frame specification from its parts and raw support lists.

Equations

• HypergraphLowerBound.mkFrame parts rawSupports h = { parts := parts, rawSupports := rawSupports, rawSupports_ok := h }

def HypergraphLowerBound.core4Supports : List (List ℕ)

The support lists of the four-core frame.

Equations

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

def HypergraphLowerBound.core4Spec : FrameSpec

The four-part core gadget used in the residue construction.

Equations

• HypergraphLowerBound.core4Spec = HypergraphLowerBound.mkFrame [3, 3, 3, 3] HypergraphLowerBound.core4Supports HypergraphLowerBound.core4Spec._proof_1

def HypergraphLowerBound.exactSmallFrames : List FrameSpec

The exact small frames listed in Appendix A.

Equations

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

def HypergraphLowerBound.boosters : List FrameSpec

The explicit boosters listed in Appendix B.

Equations

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

def HypergraphLowerBound.residueGadgets : List FrameSpec

The residue gadgets R_r used by the balanced four-way construction.

Equations

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

def HypergraphLowerBound.eBonus (r m : ℕ) : ℕ

The bonus terms e_r(m) for the balanced four-way construction.

Equations

• HypergraphLowerBound.eBonus r m = match r % 4 with | 0 => 13 * m / 3 | 1 => (13 * m + 1) / 3 | 2 => (13 * m + 5) / 3 | x => (13 * m + 6) / 3

def HypergraphLowerBound.bootstrapValues : List ℕ

The bootstrap table values for A_n, 0 ≤ n < 60.

Equations

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

@[irreducible]

def HypergraphLowerBound.A (n : ℕ) : ℕ

The sequence A(n) of vertex counts for the explicit hypergraph family.

Equations

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

theorem HypergraphLowerBound.card_filter_univ_get_eq_countP_prop {α : Type u_1} (l : List α) (p : α → Prop) [DecidablePred p] : {i : Fin l.length | p (l.get i)}.card = List.countP (fun (a : α) => decide (p a)) l

theorem HypergraphLowerBound.card_filter_univ_multiset_toList_eq_countP_prop {α : Type u_1} (m : Multiset α) (p : α → Prop) [DecidablePred p] : {i : Fin m.card | p (m.toList.get ⟨↑i, ⋯⟩)}.card = List.countP (fun (a : α) => decide (p a)) m.toList

theorem HypergraphLowerBound.omegaCount_coe_eq_countP {t : ℕ} (l : List (SupportPattern t)) (T I : Finset (Fin t)) : omegaCount (↑l) T I = List.countP (frameWitnesses T I) l

theorem HypergraphLowerBound.FrameSpec.isValid_iff_isFrame (spec : FrameSpec) : spec.IsValid ↔ IsFrame spec.supports spec.cap

The computable frame checker is equivalent to the abstract frame predicate.

def HypergraphLowerBound.maskFinset (spec : FrameSpec) (mask : ℕ) : Finset (Fin spec.t)

The frame coordinates selected by a natural-number bit mask.

Equations

• HypergraphLowerBound.maskFinset spec mask = {i : Fin spec.t | mask.testBit ↑i = true}

def HypergraphLowerBound.checkComplementMasksDown (spec : FrameSpec) : ℕ → ℕ → Bool

Recursively check the maximal witness set for each right-hand side support mask.

Equations

• One or more equations did not get rendered due to their size.
• HypergraphLowerBound.checkComplementMasksDown spec n.succ x✝ = (HypergraphLowerBound.checkComplementMasksDown spec n x✝ && HypergraphLowerBound.checkComplementMasksDown spec n (x✝ ||| 1 <<< n))

def HypergraphLowerBound.FrameSpec.checkComplementValid (spec : FrameSpec) : Bool

A Boolean validator using only maximal witness sets for each capacity support.

Equations

• spec.checkComplementValid = HypergraphLowerBound.checkComplementMasksDown spec spec.t 0

theorem HypergraphLowerBound.FrameSpec.checkComplementValid_sound (spec : FrameSpec) (h : spec.checkComplementValid = true) : spec.IsValid

The complement-based checker implies all frame inequalities.

theorem HypergraphLowerBound.checkComplementMasksDown_step_true (spec : FrameSpec) (n mask : ℕ) (h0 : checkComplementMasksDown spec n mask = true) (h1 : checkComplementMasksDown spec n (mask ||| 1 <<< n) = true) : checkComplementMasksDown spec (n + 1) mask = true

Combine the two child certificates for the next support-mask bit.

def HypergraphLowerBound.FrameSpec.checkValid (spec : FrameSpec) : Bool

A computable checker for the frame inequalities attached to a finite specification.

Equations

• spec.checkValid = decide spec.IsValid