The lower bound by the real meagre-ideal uniformity

The proof constructs a nonmeagre set of real numbers of cardinality at most that of any rearranging family. All block, coding and category ingredients are instantiated by the constructions in the preceding modules.

theorem NonMRR.nonM_le_bounding_mul_blockSlalomNumber : nonM ≤ boundingNumber * blockSlalomNumber

The category lower bound for the concrete slalom relation.

theorem NonMRR.nonM_le_cardinal_of_isRearranging {P : Set (Equiv.Perm ℕ)} (hP : IsRearranging P) : nonM ≤ Cardinal.mk ↑P

Every rearranging family has cardinality at least nonM, with nonM defined using the actual meagre ideal on the real line.

theorem NonMRR.exists_preserved_series_of_cardinal_lt_nonM {P : Set (Equiv.Perm ℕ)} (hP : Cardinal.mk ↑P < nonM) : ∃ (a : ConditionalSeries), ∀ π ∈ P, HasSum (a.term ∘ ⇑π) a.sum (SummationFilter.conditional ℕ)

The simultaneous witnessing formulation of the lower bound.