Special Functions: entire existence, 2 November 2026
SF-LEAN-B03 adds 19 checked declarations proving that the previously constructed coupled functions extend to the whole complex plane when all four positive real scales are strictly less than one.
The same coefficient sums now converge absolutely at every complex point, are holomorphic everywhere, and satisfy
The proof propagates convergence through the recurrence, using the absolutely
convergent Cauchy product and the denominator 2*n+3. A contraction-ladder
induction reaches every finite complex point. Uniform bounds on smaller balls
then justify holomorphy and termwise differentiation. No choice of glued
extensions is required: these are the same sums as in Block02.
The registered source scope is 108 named declarations: the inherited 39 in the finite core, 29 in Block01, 21 in Block02, and 19 here. Supporting lemmas are included in that count. This completes the entire-existence step, with the global equations, but does not prove the full analytic monograph.
- Exact result, proof mechanism and replay instructions
- New production Lean source
- Claim correspondence and remaining obligations
- All 19 new theorem names and source hash
- Source-bound verification receipt
- Focused mathematical self-review
- Continuation checkpoint
Compilation treats warnings as errors. The exact axiom audit and same-kernel replay cover all three coupled modules against the existing pinned Mathlib cache; the finite core's 39-declaration record is inherited. Four negative controls check a missing strictness guard, an incorrect denominator, an incorrect derivative sign, and a placeholder proof. A positive fixture checks the existing rational parameters beyond the old local disk. Review is self-review, not independent review.
The next step is the reverse Taylor coefficient bridge and uniqueness among arbitrary normalized analytic solutions. The same bridge supports the analytic-germ version of parameter recovery. Perron growth and full component rescaling remain later obligations.
The Block02 guide retains its earlier local scope. All earlier formal sources, manuscript sources and reading PDFs are preserved. Current catalogue entries link to this dated extension record.