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.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

@[implicit_reducible]

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

Equations

• HypergraphLowerBound.instDecidableIsValid spec = id (id inferInstance)

@[implicit_reducible]

instance HypergraphLowerBound.instDecidableEqChoiceKind : DecidableEq HypergraphLowerBound.ChoiceKind✝

Equations

• HypergraphLowerBound.instDecidableEqChoiceKind x✝ y✝ = if h : HypergraphLowerBound.ChoiceKind.ctorIdx✝ x✝ = HypergraphLowerBound.ChoiceKind.ctorIdx✝ y✝ then isTrue ⋯ else isFalse ⋯

def HypergraphLowerBound.instReprChoiceKind.repr : HypergraphLowerBound.ChoiceKind✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance HypergraphLowerBound.instReprChoiceKind : Repr HypergraphLowerBound.ChoiceKind✝

Equations

• HypergraphLowerBound.instReprChoiceKind = { reprPrec := HypergraphLowerBound.instReprChoiceKind.repr }

@[implicit_reducible]

instance HypergraphLowerBound.instInhabitedChoiceKind : Inhabited HypergraphLowerBound.ChoiceKind✝

Equations

• HypergraphLowerBound.instInhabitedChoiceKind = { default := HypergraphLowerBound.instInhabitedChoiceKind.default }

@[implicit_reducible]

instance HypergraphLowerBound.instInhabitedChoiceSpec : Inhabited HypergraphLowerBound.ChoiceSpec✝

Equations

• HypergraphLowerBound.instInhabitedChoiceSpec = { default := HypergraphLowerBound.instInhabitedChoiceSpec.default }

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.checkMasksDown (spec : FrameSpec) : ℕ → ℕ → ℕ → Bool

Recursively check all masks contributing to the raw frame inequalities.

Equations

• One or more equations did not get rendered due to their size.
• HypergraphLowerBound.checkMasksDown spec 0 x✝¹ x✝ = decide (List.countP (HypergraphLowerBound.rawWitness✝ x✝¹ x✝) spec.rawSupports ≤ HypergraphLowerBound.rawCapSum✝ spec x✝¹ x✝)

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

A Boolean validator for the raw frame inequalities of a frame specification.

Equations

• spec.rawCheckValid = HypergraphLowerBound.checkMasksDown spec spec.t 0 0

theorem HypergraphLowerBound.FrameSpec.rawCheckValid_sound (spec : FrameSpec) (h : spec.rawCheckValid = true) : spec.IsValid

theorem HypergraphLowerBound.checkMasksDown_step_true (spec : FrameSpec) (n Tmask Imask : ℕ) (h0 : checkMasksDown spec n Tmask Imask = true) (h1 : checkMasksDown spec n (Tmask ||| 1 <<< n) Imask = true) (h2 : checkMasksDown spec n (Tmask ||| 1 <<< n) (Imask ||| 1 <<< n) = true) : checkMasksDown spec (n + 1) Tmask Imask = true

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