theorem helperForProposition_4_7_14_gridBracket_by_floor (x₀ : ℝ) (m : ℕ) : have j := ⌊x₀ * 32 ^ m⌋; have a := ↑j / 32 ^ m; have b := ↑(j + 1) / 32 ^ m; a ≤ x₀ ∧ x₀ < b ∧ b - a = 1 / 32 ^ m

Helper for Proposition 4.7.14: floor-bracketing x₀ between consecutive 32^{-m}-mesh points.

theorem helperForProposition_4_7_14_powRatio_eight_div_thirtyTwo (m : ℕ) : 8 ^ m / 32 ^ m = 1 / 4 ^ m

Helper for Proposition 4.7.14: ratio identity (8^m)/(32^m) = 1/(4^m).

theorem helperForProposition_4_7_14_secantLower_from_numerator_and_distance (x₀ y : ℝ) (m : ℕ) (hnum : 1 / (2 * 4 ^ m) ≤ |scaledCosineSeriesFunction y - scaledCosineSeriesFunction x₀|) (hdist_pos : 0 < |y - x₀|) (hdist_le : |y - x₀| ≤ 1 / 32 ^ m) : 8 ^ m / 2 ≤ |(scaledCosineSeriesFunction y - scaledCosineSeriesFunction x₀) / (y - x₀)|

Helper for Proposition 4.7.14: a lower bound on numerator and an upper bound on distance imply a large secant quotient.

theorem helperForProposition_4_7_14_exists_large_local_secant (x₀ : ℝ) (m : ℕ) (hm : 1 ≤ m) : ∃ (y : ℝ), 0 < |y - x₀| ∧ |y - x₀| ≤ 1 / 32 ^ m ∧ 8 ^ m / 2 ≤ |(scaledCosineSeriesFunction y - scaledCosineSeriesFunction x₀) / (y - x₀)|

Helper for Proposition 4.7.14: for every mesh scale, one can find a nearby point with secant slope at least (8^m)/2.

theorem helperForProposition_4_7_14_eventual_secant_bound_of_differentiableAt (x₀ : ℝ) (hf : DifferentiableAt ℝ scaledCosineSeriesFunction x₀) : ∀ᶠ (y : ℝ) in nhdsWithin x₀ {x₀}ᶜ, |(scaledCosineSeriesFunction y - scaledCosineSeriesFunction x₀) / (y - x₀)| ≤ |deriv scaledCosineSeriesFunction x₀| + 1

Helper for Proposition 4.7.14: differentiability at x₀ forces eventual boundedness of punctured-neighborhood secant quotients.

theorem helperForProposition_4_7_14_choose_m_against_delta_and_C (δ : ℝ) (hδ : 0 < δ) (C : ℝ) : ∃ (m : ℕ), 1 ≤ m ∧ 1 / 32 ^ m < δ ∧ C < 8 ^ m / 2

Helper for Proposition 4.7.14: choose a scale m making 32^{-m} tiny and (8^m)/2 larger than a prescribed bound.

theorem scaledCosineSeries_nowhere_differentiable (x₀ : ℝ) : ¬DifferentiableAt ℝ scaledCosineSeriesFunction x₀

Proposition 4.7.14: for f(x) = ∑_{n=1}^∞ 4^{-n} cos(32^n π x) (encoded here as scaledCosineSeriesFunction from Definition 4.7.4), f is nowhere differentiable on ℝ; i.e., for every x₀ : ℝ, f is not differentiable at x₀.