Positivity and geometric-sum estimates for the local complexity exponent.

theorem V7.Stage2.two_rpow_gt_one {a : ℝ} (ha : 0 < a) : 1 < 2 ^ a

theorem V7.Stage2.one_sub_two_neg_rpow_pos {a : ℝ} (ha : 0 < a) : 0 < 1 - 2 ^ (-a)

theorem V7.Stage2.localCostExponent_pos {p : ℝ} : 0 < localCostExponent p

theorem V7.Stage2.dyadic_geometric_sum_le_endpoint {a beta : ℝ} (ha : 0 < a) (hbeta : 0 ≤ beta) (J : ℕ) : ∑ j ∈ Finset.range (J + 1), (2 ^ j * beta) ^ a ≤ (2 ^ J * beta) ^ a / (1 - 2 ^ (-a))

A dependency-pure finite dyadic sum. The right hand side is the exact coefficient frozen into the V7 controller carriers.