The real Airy functions

The power series F = Σ aₙ xⁿ with a_{k+3} = a_k / ((k + 2)(k + 3)), a₀ = c0, a₁ = c1, a₂ = 0, as a real function airyFun c0 c1 : ℝ → ℝ. It is entire, solves F'' = x F as a functional identity, has zeros unbounded below, and does not decay at +∞ when positive with non-negative slope at some x₀ > 0. A decaying (recessive) solution is built by reduction of order, Ai_rec = f ∫ₓ^∞ f⁻², without the asymptotic expansions of DLMF §9.7, and is extended to an entire Airy function. Applied to the quantum bouncer ψ'' = α²(αx − β)ψ on [0, ∞) with ψ(0) = 0: there are infinitely many energy levels.

Main results

• Airy.airyFun_entire: airyFun c0 c1 is analytic on all of ℝ (radius of convergence ∞).
• Airy.airyFun_ode: deriv (deriv (airyFun c0 c1)) x = x * airyFun c0 c1 x.
• Airy.sturm_unbounded_zeros, Airy.airyFun_unbounded_zeros: every solution has zeros unbounded below (Sturm comparison with sin (√c (x − a)), from Rolle and the intermediate value theorem).
• Airy.airyFun_not_decaying: a solution positive with non-negative slope at x₀ > 0 does not tend to 0.
• Airy.exists_recessive_solution: a non-trivial solution on (0, ∞) tending to 0 at +∞.
• Airy.exists_entire_recessive: an entire airyFun c0 c1, not identically zero, tending to 0 at +∞ (through the basis Wronskian W(f, g) = 1).
• Airy.bouncer_ode, Airy.bouncer_bc, Airy.bouncer_levels_infinite: the quantum bouncer has infinitely many energy levels, the negatives of the zeros of an Airy function.

Implementation notes

Mathlib has no Sturm–Liouville or Sturm comparison theory; the oscillation argument is built here from Rolle's theorem, the mean value theorem and the intermediate value theorem.

References

• NIST Digital Library of Mathematical Functions, Chapter 9 (Airy and Related Functions), https://dlmf.nist.gov/9.
• O. Vallée, M. Soares, Airy Functions and Applications to Physics, Imperial College Press (2010).
• E. A. Coddington, N. Levinson, Theory of Ordinary Differential Equations, McGraw–Hill (1955), Ch. 8.
• R. L. Gibbs, The quantum bouncer, Am. J. Phys. 43 (1975) 25–28.
• V. V. Nesvizhevsky et al., Quantum states of neutrons in the Earth's gravitational field, Nature 415 (2002) 297–299.
• C. Marín, How a Falling Particle Counts Its Floors: the Airy function as a verified entire solution of y''=xy, its oscillation, and the quantum-bouncer spectrum, machine-checked in Lean 4 (2026), doi:10.5281/zenodo.20787671. Ported from AiryReal.lean of karlesmarin/airy-bouncer-lean (Lean v4.30.0-rc2).

noncomputable def Airy.coeffR (c0 c1 : ℝ) : ℕ → ℝ

Real Airy coefficients: solution of y''=xy with y(0)=c0, y'(0)=c1.

Equations

• Airy.coeffR c0 c1 0 = c0
• Airy.coeffR c0 c1 1 = c1
• Airy.coeffR c0 c1 2 = 0
• Airy.coeffR c0 c1 k.succ.succ.succ = Airy.coeffR c0 c1 k / ((↑k + 2) * (↑k + 3))

theorem Airy.coeffR_succ3 (c0 c1 : ℝ) (k : ℕ) : coeffR c0 c1 (k + 3) = coeffR c0 c1 k / ((↑k + 2) * (↑k + 3))

theorem Airy.coeffR_mul_succ3 (c0 c1 : ℝ) (k : ℕ) : (↑k + 2) * (↑k + 3) * coeffR c0 c1 (k + 3) = coeffR c0 c1 k

Recurrence cleared of its denominator: (k+2)(k+3)·a(k+3) = a(k). This is the identity (k+2)(k+1)c_{k+2}=c_{k-1} reindexed; it drives the F''=x·F coefficient match.

theorem Airy.coeffR_abs_le (c0 c1 : ℝ) (n : ℕ) : |coeffR c0 c1 n| ≤ max |c0| |c1| / ↑(n / 3).factorial

Coefficient bound. |aₙ| ≤ M / ⌊n/3⌋! with M = max |c0| |c1|. Each 3-step divides by (k+2)(k+3) ≥ ⌊k/3⌋+1, so the factorial grows one step per 3 indices.

theorem Airy.summable_coeffR_norm (c0 c1 : ℝ) (r : NNReal) : Summable fun (n : ℕ) => ‖coeffR c0 c1 n‖ * ↑r ^ n

Summability. For every radius r, ∑ |aₙ|·rⁿ converges. Comparison with the regrouped series ∑ rⁿ/⌊n/3⌋! = (1+r+r²)·∑(r³)ᵐ/m! = (1+r+r²)·e^{r³}.

theorem Airy.scalar_fms_ext (p q : FormalMultilinearSeries ℝ ℝ ℝ) (h : ∀ (n : ℕ), p.coeff n = q.coeff n) : p = q

A scalar formal multilinear series is determined by its coefficients.

theorem Airy.deriv_ofScalarsSum {a : ℕ → ℝ} {f : ℝ → ℝ} (hf : HasFPowerSeriesOnBall f (FormalMultilinearSeries.ofScalars ℝ a) 0 ⊤) : HasFPowerSeriesOnBall (deriv f) (FormalMultilinearSeries.ofScalars ℝ fun (n : ℕ) => (↑n + 1) * a (n + 1)) 0 ⊤

Term-by-term differentiation. If f is the sum of ∑ aₙ xⁿ on a ball, then deriv f is the sum of ∑ (n+1) a_{n+1} xⁿ. Built from HasFPowerSeriesOnBall.fderiv (the derivative's power series is derivSeries) + evaluation at 1 + derivSeries_coeff_one.

noncomputable def Airy.airySeries (c0 c1 : ℝ) : FormalMultilinearSeries ℝ ℝ ℝ

The Airy power series over ℝ as a FormalMultilinearSeries.

Equations

• Airy.airySeries c0 c1 = FormalMultilinearSeries.ofScalars ℝ (Airy.coeffR c0 c1)

noncomputable def Airy.airyFun (c0 c1 : ℝ) : ℝ → ℝ

The real Airy solution F : ℝ → ℝ with F(0)=c0, F'(0)=c1.

Equations

• Airy.airyFun c0 c1 = (Airy.airySeries c0 c1).sum

theorem Airy.airySeries_radius (c0 c1 : ℝ) : (airySeries c0 c1).radius = ⊤

Radius of convergence = ∞. The Airy series is entire.

theorem Airy.airyFun_hasFPowerSeries (c0 c1 : ℝ) : HasFPowerSeriesOnBall (airyFun c0 c1) (airySeries c0 c1) 0 ⊤

theorem Airy.airyFun_entire (c0 c1 : ℝ) : AnalyticOnNhd ℝ (airyFun c0 c1) Set.univ

F is a real entire function (analytic on all of ℝ).

noncomputable def Airy.coeffR2 (c0 c1 : ℝ) (n : ℕ) : ℝ

Coefficients of F'': (n+1)(n+2)·a(n+2) (= apply deriv_ofScalarsSum twice).

Equations

• Airy.coeffR2 c0 c1 n = (↑n + 1) * (↑n + 2) * Airy.coeffR c0 c1 (n + 2)

theorem Airy.coeffR2_zero (c0 c1 : ℝ) : coeffR2 c0 c1 0 = 0

theorem Airy.coeffR2_succ (c0 c1 : ℝ) (n : ℕ) : coeffR2 c0 c1 (n + 1) = coeffR c0 c1 n

The key shift: F'' coefficient at n+1 equals F coefficient at n — this IS the recurrence (n+2)(n+3)a(n+3)=a(n), i.e. the Airy ODE y''=xy read off coefficient-by-coefficient.

theorem Airy.airyFun_ode (c0 c1 x : ℝ) : deriv (deriv (airyFun c0 c1)) x = x * airyFun c0 c1 x

The Airy ODE y'' = x·y, as a real functional identity. Every entire solution F of the recurrence satisfies deriv (deriv F) x = x · F x at every real x. Proof: term-by-term differentiation gives F'' as the power series ∑ (n+1)(n+2)a(n+2) xⁿ; the recurrence coeffR2_succ reindexes it to ∑ aₙ xⁿ⁺¹ = x·F.

theorem Airy.sturm_pos_false (f f' : ℝ → ℝ) (a c : ℝ) (hc : 0 < c) (hf : ∀ (x : ℝ), HasDerivAt f (f' x) x) (hf' : ∀ (x : ℝ), HasDerivAt f' (x * f x) x) (hx : a + Real.pi / √c ≤ -c) (hpos : ∀ x ∈ Set.Icc a (a + Real.pi / √c), 0 < f x) : False

Sturm comparison core: a positive solution of y''=xy on an interval of length π/√c lying in (−∞,−c] is impossible. Wronskian W=f'z−fz' vs z=sin(√c(x−a)): W'=(x+c)·f·z ≤ 0 but the endpoints force W(a)<0<W(a+π/√c).

theorem Airy.const_sign_of_no_zero {g : ℝ → ℝ} {a d : ℝ} (hg : ContinuousOn g (Set.Icc a d)) (hnz : ∀ x ∈ Set.Icc a d, g x ≠ 0) (hax : a ≤ d) : (∀ x ∈ Set.Icc a d, 0 < g x) ∨ ∀ x ∈ Set.Icc a d, g x < 0

A continuous function with no zero on [a,d] has constant sign there (IVT).

theorem Airy.sturm_has_zero (f f' : ℝ → ℝ) (a c : ℝ) (hc : 0 < c) (hf : ∀ (x : ℝ), HasDerivAt f (f' x) x) (hf' : ∀ (x : ℝ), HasDerivAt f' (x * f x) x) (hx : a + Real.pi / √c ≤ -c) : ∃ x ∈ Set.Icc a (a + Real.pi / √c), f x = 0

Sturm zero existence: any solution of y''=xy has a zero in [a, a+π/√c] when that interval lies in (−∞,−c] (apply the positive-case contradiction to f or −f).

theorem Airy.sturm_unbounded_zeros (f f' : ℝ → ℝ) (hf : ∀ (x : ℝ), HasDerivAt f (f' x) x) (hf' : ∀ (x : ℝ), HasDerivAt f' (x * f x) x) (M : ℝ) : ∃ x < M, f x = 0

Oscillation (generic): any solution of y''=xy has zeros unbounded below — for every M there is a zero < M. Intervals of length π/√c pushed into (−∞,−c] as c→∞.

theorem Airy.airyFun_unbounded_zeros (c0 c1 M : ℝ) : ∃ x < M, airyFun c0 c1 x = 0

The Airy function oscillates: airyFun c0 c1 has zeros unbounded below (infinitely many zeros heading to −∞). For the quantum bouncer these are the gravitational energy levels.

theorem Airy.nondecr_of_deriv2_nonneg (f f' g : ℝ → ℝ) (a b : ℝ) (hab : a ≤ b) (hf : ∀ (x : ℝ), HasDerivAt f (f' x) x) (hf' : ∀ (x : ℝ), HasDerivAt f' (g x) x) (hg : ∀ x ∈ Set.Icc a b, 0 ≤ g x) (hfa' : 0 ≤ f' a) : MonotoneOn f (Set.Icc a b)

If f'' = g ≥ 0 on [a,b] and f'(a) ≥ 0, then f is non-decreasing on [a,b] (f' non-decreasing ⟹ f' ≥ f'(a) ≥ 0 ⟹ f non-decreasing).

theorem Airy.ode_pos_Ici (f f' : ℝ → ℝ) {x0 : ℝ} (hx0 : 0 ≤ x0) (hf : ∀ (x : ℝ), HasDerivAt f (f' x) x) (hf' : ∀ (x : ℝ), HasDerivAt f' (x * f x) x) (hfx0 : 0 < f x0) (hfx0' : 0 ≤ f' x0) (x : ℝ) : x ∈ Set.Ici x0 → 0 < f x

On (0,∞), a solution of y''=xy positive with non-negative slope stays positive. It is convex where positive, so once non-decreasing it cannot return to 0 (first-zero argument).

theorem Airy.ode_nondecreasing_Ici (f f' : ℝ → ℝ) {x0 : ℝ} (hx0 : 0 < x0) (hf : ∀ (x : ℝ), HasDerivAt f (f' x) x) (hf' : ∀ (x : ℝ), HasDerivAt f' (x * f x) x) (hfx0 : 0 < f x0) (hfx0' : 0 ≤ f' x0) : MonotoneOn f (Set.Ici x0)

Such a solution is non-decreasing on [x0,∞).

theorem Airy.ode_not_tendsto_zero (f f' : ℝ → ℝ) {x0 : ℝ} (hx0 : 0 < x0) (hf : ∀ (x : ℝ), HasDerivAt f (f' x) x) (hf' : ∀ (x : ℝ), HasDerivAt f' (x * f x) x) (hfx0 : 0 < f x0) (hfx0' : 0 ≤ f' x0) : ¬Filter.Tendsto f Filter.atTop (nhds 0)

A dominant solution does not decay: positive with non-negative slope at some x0>0 ⟹ it stays ≥ f x0 > 0, so it cannot tend to 0 at +∞.

theorem Airy.airyFun_hasDerivAt (c0 c1 x : ℝ) : HasDerivAt (airyFun c0 c1) (deriv (airyFun c0 c1) x) x

airyFun and its derivative as HasDerivAt facts (from entire + the ODE).

theorem Airy.airyFun_deriv_hasDerivAt (c0 c1 x : ℝ) : HasDerivAt (deriv (airyFun c0 c1)) (x * airyFun c0 c1 x) x

theorem Airy.airyFun_not_decaying (c0 c1 : ℝ) {x0 : ℝ} (hx0 : 0 < x0) (hpos : 0 < airyFun c0 c1 x0) (hslope : 0 ≤ deriv (airyFun c0 c1) x0) : (∀ x ∈ Set.Ici x0, 0 < airyFun c0 c1 x) ∧ MonotoneOn (airyFun c0 c1) (Set.Ici x0) ∧ ¬Filter.Tendsto (airyFun c0 c1) Filter.atTop (nhds 0)

Dominant Airy solutions. If F = airyFun c0 c1 is positive with non-negative slope at some x0>0, then on [x0,∞) it is positive and non-decreasing, and it does NOT decay to 0 at +∞. (The recessive solution, which does decay, is constructed below by reduction of order: exists_recessive_solution, exists_entire_recessive.)

theorem Airy.bouncer_ode (c0 c1 α β x : ℝ) : deriv (deriv fun (y : ℝ) => airyFun c0 c1 (α * y - β)) x = α ^ 2 * (α * x - β) * airyFun c0 c1 (α * x - β)

Bridge: ψ(x) = F(αx − β) (F any Airy solution) solves the rescaled Airy/bouncer equation ψ'' = α²(αx − β)·ψ. Pure chain rule on airyFun_ode.

theorem Airy.bouncer_bc (c0 c1 α β : ℝ) : (fun (y : ℝ) => airyFun c0 c1 (α * y - β)) 0 = airyFun c0 c1 (-β)

Boundary wall: the Dirichlet condition ψ(0)=0 is exactly Ai(−β)=0.

theorem Airy.bouncer_levels_infinite (c0 c1 B : ℝ) : ∃ (β : ℝ), B < β ∧ airyFun c0 c1 (-β) = 0

Infinitely many bound-state energies. For every bound B there is a (rescaled) energy β > B with Ai(−β)=0, i.e. the quantum bouncer has infinitely many gravitational levels, given by the (negatives of the) Airy zeros. This is a consequence of the oscillation theorem.

theorem Airy.airyFun_zero (c0 c1 : ℝ) : airyFun c0 c1 0 = c0

airyFun c0 c1 at 0 is c0 (the constant term of the series).

theorem Airy.deriv_airyFun_zero (c0 c1 : ℝ) : deriv (airyFun c0 c1) 0 = c1

(airyFun c0 c1)'(0) = c1 (the linear coefficient).

theorem Airy.airyFun10_pos (x : ℝ) : x ∈ Set.Ici 0 → 0 < airyFun 1 0 x

The dominant solution f = airyFun 1 0 is strictly positive on [0,∞) (it has f(0)=1>0, f'(0)=0, and f''=xf≥0, so the first-zero argument applies from x0=0).

theorem Airy.airyFun10_diff : Differentiable ℝ (airyFun 1 0)

theorem Airy.airyFun10_deriv_diff : Differentiable ℝ (deriv (airyFun 1 0))

theorem Airy.airyFun10_deriv_nonneg (x : ℝ) : x ∈ Set.Ici 0 → 0 ≤ deriv (airyFun 1 0) x

f' is non-negative on [0,∞) (it is non-decreasing, with f'(0)=0).

theorem Airy.airyFun10_ge_one (x : ℝ) : x ∈ Set.Ici 0 → 1 ≤ airyFun 1 0 x

f ≥ 1 on [0,∞) (non-decreasing, with f(0)=1).

theorem Airy.airyFun10_convex : ConvexOn ℝ (Set.Ici 0) (airyFun 1 0)

f is convex on [0,∞) (since f'' = x·f ≥ 0).

theorem Airy.airyFun10_deriv_ge_sq (x : ℝ) : x ∈ Set.Ici 0 → x ^ 2 / 2 ≤ deriv (airyFun 1 0) x

f'(x) ≥ x²/2 on [0,∞) (so f' → ∞). From h=f'−x²/2, h(0)=0, h'=x(f−1)≥0.

theorem Airy.inv_sq_eq_rpow {z : ℝ} (_hz : 0 < z) : z⁻¹ ^ 2 = z ^ (-2)

(z⁻¹)² as a real power, for z>0.

theorem Airy.integrableOn_affine_inv_sq (x c m : ℝ) (hc : 0 < c) (hm : 0 < m) : MeasureTheory.IntegrableOn (fun (t : ℝ) => (c + m * (t - x))⁻¹ ^ 2) (Set.Ioi x) MeasureTheory.volume

The affine tangent bound (c+m(t−x))⁻² is integrable on (x,∞) for c,m>0.

theorem Airy.integrableOn_airyFun10_inv_sq {x : ℝ} (hx : 0 < x) : MeasureTheory.IntegrableOn (fun (t : ℝ) => (airyFun 1 0 t)⁻¹ ^ 2) (Set.Ioi x) MeasureTheory.volume

1/f² is integrable on (x,∞) for x>0 (f = airyFun 1 0): dominated by the convexity tangent bound f(t) ≥ f(x)+f'(x)(t−x), which is integrable.

theorem Airy.hasDerivAt_integral_Ioi {h : ℝ → ℝ} {b a : ℝ} (hba : b < a) (hcont : ContinuousOn h (Set.Ici b)) (hint : MeasureTheory.IntegrableOn h (Set.Ioi b) MeasureTheory.volume) : HasDerivAt (fun (x : ℝ) => ∫ (t : ℝ) in Set.Ioi x, h t) (-h a) a

FTC on a half-line (reference b): d/dx ∫_x^∞ h = -h(a) for a > b, h continuous on [b,∞) and integrable on (b,∞).

noncomputable def Airy.airyRecInt (x : ℝ) : ℝ

The reduction-of-order integral ∫_x^∞ dt/f(t)².

Equations

• Airy.airyRecInt x = ∫ (t : ℝ) in Set.Ioi x, (Airy.airyFun 1 0 t)⁻¹ ^ 2

noncomputable def Airy.airyRec (x : ℝ) : ℝ

The recessive Airy solution on (0,∞): Ai_rec(x) = f(x)·∫_x^∞ dt/f(t)².

Equations

• Airy.airyRec x = Airy.airyFun 1 0 x * Airy.airyRecInt x

theorem Airy.continuousOn_airyFun10_inv_sq {b : ℝ} (hb : 0 < b) : ContinuousOn (fun (t : ℝ) => (airyFun 1 0 t)⁻¹ ^ 2) (Set.Ici b)

1/f² is continuous on [b,∞) for b>0.

theorem Airy.airyRecInt_hasDerivAt {a : ℝ} (ha : 0 < a) : HasDerivAt airyRecInt (-(airyFun 1 0 a)⁻¹ ^ 2) a

d/dx airyRecInt = -1/f(x)² for x>0.

theorem Airy.airyRec_hasDerivAt {x : ℝ} (hx : 0 < x) : HasDerivAt airyRec (deriv (airyFun 1 0) x * airyRecInt x - (airyFun 1 0 x)⁻¹) x

First derivative of Ai_rec: Ai_rec' = f'·g − 1/f (product rule; f·(1/f²) = 1/f).

theorem Airy.airyRec_deriv_hasDerivAt {x : ℝ} (hx : 0 < x) : HasDerivAt (fun (y : ℝ) => deriv (airyFun 1 0) y * airyRecInt y - (airyFun 1 0 y)⁻¹) (x * airyRec x) x

Reduction of order: Ai_rec'' = x·Ai_rec — the 1/f² terms cancel, leaving f''·g = xf·g. So Ai_rec solves y''=xy on (0,∞).

theorem Airy.airyRecInt_le {x : ℝ} (hx : 0 < x) : airyRecInt x ≤ (deriv (airyFun 1 0) x * airyFun 1 0 x)⁻¹

The convexity integral bound: ∫_x^∞ 1/f² ≤ 1/(f'(x)·f(x)) for x>0. The tangent bound dominates by the affine (c+m(t−x))⁻², whose exact tail integral is 1/(mc).

theorem Airy.airyRec_le_inv_deriv {x : ℝ} (hx : 0 < x) : airyRec x ≤ (deriv (airyFun 1 0) x)⁻¹

Ai_rec(x) ≤ 1/f'(x) for x>0 (from the integral bound: f·1/(f'f) = 1/f').

theorem Airy.airyRec_nonneg {x : ℝ} (hx : 0 < x) : 0 ≤ airyRec x

Ai_rec ≥ 0 on (0,∞).

theorem Airy.airyRec_tendsto_zero : Filter.Tendsto airyRec Filter.atTop (nhds 0)

The recessive solution decays: Ai_rec(x) → 0 as x → +∞ (0 ≤ Ai_rec ≤ 1/f' ≤ 2/x² → 0).

theorem Airy.airyRec_wronskian {x : ℝ} (hx : 0 < x) : airyFun 1 0 x * (deriv (airyFun 1 0) x * airyRecInt x - (airyFun 1 0 x)⁻¹) - deriv (airyFun 1 0) x * airyRec x = -1

The Wronskian W(f, Ai_rec) = f·Ai_rec' − f'·Ai_rec = −1 (constant; the synthesis identity). The f·g terms cancel, leaving −f·(1/f) = −1.

theorem Airy.exists_recessive_solution : ∃ (y : ℝ → ℝ) (y' : ℝ → ℝ), (y 1 ≠ 0 ∨ y' 1 ≠ 0) ∧ Filter.Tendsto y Filter.atTop (nhds 0) ∧ (∀ (x : ℝ), 0 < x → HasDerivAt y (y' x) x) ∧ ∀ (x : ℝ), 0 < x → HasDerivAt y' (x * y x) x

Existence of the recessive solution. There is a non-trivial real solution y of y''=xy on (0,∞) that decays to 0 at +∞. (y = Ai_rec; non-triviality from W(1)=−1≠0.) This is the decaying solution whose existence the DLMF §9.7 asymptotics classically guarantee — here built and verified by reduction of order, with no asymptotics.

Entire extension of the recessive solution (linearity + Wronskian + quotient identity)

theorem Airy.coeffR_linear (c0 c1 : ℝ) (n : ℕ) : coeffR c0 c1 n = c0 * coeffR 1 0 n + c1 * coeffR 0 1 n

Linearity of the Airy coefficient recurrence. coeffR is linear in the initial data, because the recurrence a_{k+3}=a_k/((k+2)(k+3)) is linear.

theorem Airy.summable_coeffR_term (c0 c1 x : ℝ) : Summable fun (n : ℕ) => coeffR c0 c1 n * x ^ n

The Airy power-series terms are summable at every point (entire).

theorem Airy.airyFun_linear (c0 c1 x : ℝ) : airyFun c0 c1 x = c0 * airyFun 1 0 x + c1 * airyFun 0 1 x

Linearity of airyFun in the initial data: airyFun c0 c1 = c0·f + c1·g with f = airyFun 1 0, g = airyFun 0 1.

theorem Airy.wronskian_fg (x : ℝ) : airyFun 1 0 x * deriv (airyFun 0 1) x - deriv (airyFun 1 0) x * airyFun 0 1 x = 1

The basis Wronskian W(f,g) = f·g' − f'·g ≡ 1 (Abel's identity): constant because both solve y''=x·y, and =1 at 0 from f(0)=1, f'(0)=0, g(0)=0, g'(0)=1.

theorem Airy.deriv_airyFun_linear (c0 c1 x : ℝ) : deriv (airyFun c0 c1) x = c0 * deriv (airyFun 1 0) x + c1 * deriv (airyFun 0 1) x

Derivative form of airyFun linearity.

theorem Airy.exists_entire_recessive : ∃ (c0 : ℝ) (c1 : ℝ), (c0 ≠ 0 ∨ c1 ≠ 0) ∧ Filter.Tendsto (airyFun c0 c1) Filter.atTop (nhds 0)

The entire recessive solution exists. There is a non-trivial entire airyFun c0 c1 (with c1 = −1, c0 = (Ai_rec(1)+g(1))/f(1) the synthesis constant) that decays to 0 at +∞ — the recessive Airy solution, now an honest entire power series rather than an imported asymptotic object. Proof: choosing c1=−1 forces W(f, airyFun c0 (−1)) = c1·W(f,g) = −1 = W(f, Ai_rec), so the difference has Wronskian 0 with f; hence (airyFun c0 (−1) − Ai_rec)/f has derivative 0 on (0,∞), is constant, and vanishes at 1 (by the choice of c0). Thus airyFun c0 (−1) = Ai_rec on (0,∞) and inherits its decay.