Documentation

LeanPool.FrontierMathOpenHypergraphs.Uniform.Frames

Finite frame bank #

theorem HypergraphLowerBound.finite_bank_valid :
(∀ spec ∈ exactSmallFrames, spec.IsValid) ∧ (∀ spec ∈ boosters, spec.IsValid) ∧ ∀ spec ∈ residueGadgets, spec.IsValid

Every exact small frame, booster, and residue gadget listed in the appendices satisfies the stated frame inequalities.