Special Functions: types and exact radial order, Block11
SF-LEAN-B11 completes the registered canonical F.2 growth contract. The actual spherical maximum has positive real lower type and finite real upper type between the explicit constants, and log(log(M_i(R)))/log(R) tends to the positive characteristic rho. Its limsup order is therefore exactly rho. The real filter boundedness/coboundedness premises and the attained-supremum identification are explicit. This does not assert ordinary type convergence.
The addition has 22 named theorem declarations, for 273 registered names. All 48 fresh replay steps pass across eleven coupled modules; 234 coupled declarations receive fresh axiom audits. The finite core's 39-name evidence is inherited; pinned Mathlib is cached rather than freshly rebuilt/replayed. Review is self-review. Four rejection controls and the positive fixture pass, including rho=1/2 and the distinction between radial exponent and type.
The report,
claim map,
review,
I/O inventory
and receipt
bind 41 formal inputs, 49 packaged outputs, eleven generated objects and 27
staged source copies. A resource-failed first replay is preserved separately.
The public verifier is tools/verify_coupled_growth_types.py
under the Special Functions directory; use a new external output directory.
The remaining-work inventory has separately hashed source inputs. Next is F.3's Perron type proportions. Ancillary Appendix F identities, H.1 operator classification, I-J resolution/ evaluation certificates and broad A-E analytic coverage remain. No valid whole-book completion percentage is available without a full claim map. The continuation gives the next proof obligations. Prior sources and reading PDFs remain unchanged.