Proof of the flip-flop statement

flipFlop_contract β C₀ : FlipFlopContract β C₀, with ρ = δ. Assembly of FlipFlop.top_step (top level), FlipFlop.inner_step (levels 2 ≤ m < M, with the diffusivity-recursion bounds), and the alternating telescoping FlipFlop.flipflop_unroll.

theorem AVenhance.Infra.FullTheorem.Contracts.kappaSeq_pred_succ {β : ℝ} (I : Ingredients β) (κ : ℝ) {M n : ℕ} (hn : n + 1 ≤ M) : I.kappaSeq κ M n = I.KhomScalar (I.kappaSeq κ M (n + 1)) (n + 1)

theorem AVenhance.Infra.FullTheorem.Contracts.kappaSeq_top_pred {β : ℝ} (I : Ingredients β) (κ : ℝ) {M : ℕ} (hM : 1 ≤ M) : I.kappaSeq κ M (M - 1) = I.KhomScalar κ M

theorem AVenhance.Infra.FullTheorem.Contracts.a_mul_eps_pow {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) (j : ℕ) : a β Λ j * epsilon β Λ j ^ (2 + gamma β) = epsilon β Λ j ^ (β + gamma β)

theorem AVenhance.Infra.FullTheorem.Contracts.flipFlop_contract (β C₀ : ℝ) : FlipFlopContract β C₀

Flip-flop statement.