Strict local insertion and the strict two-point bound

This module assembles all interior insertion edges with the terminal edge, then feeds the resulting local insertion principle into the permutation reduction for an arbitrary (not initially ordered) strict system.

theorem Feige.strictOrderedLocalInsertion : StrictOrderedLocalInsertion

The analytic insertion construction realizes the complete strict local insertion hypothesis used by the ordered induction.

theorem Feige.strictTwoPoint_rejectionMass_le_alpha {m : ℕ} (γ β : Fin m → ℝ) (hγpos : ∀ (i : Fin m), 0 < γ i) (hγle : ∀ (i : Fin m), γ i ≤ 1) (hβpos : ∀ (i : Fin m), 0 < β i) {α : ℝ} (hα : 0 ≤ α) : twoPointRejectionMass γ β α ≤ α

For every strict two-point system, without any prior ordering of its coordinates, the rejection mass at a nonnegative threshold is at most the threshold.