Special Functions: formal sources and recorded coverage

Recorded checkpoint: SF-LEAN-B17, 3 November 2026.

Inspect the Lean sources or run a selected file with dependencies. The inspector includes the coupled production modules, their axiom-audit files, and selected controls alongside the inherited finite core. The original Block01 status file remains available as a historical checkpoint.

Choose a production module

The existing declaration registers record 426 theorem names across the seventeen coupled modules below. The separate inherited finite core records 39 names, for 465 registered names at this checkpoint. These are registered names with individual scopes; they do not measure whole-book formalization.

Block	Production source	Registered theorem names	Declaration register
01	CoupledFormal.lean	29	Names and source lines
02	CoupledAnalytic.lean	21	Names and source lines
03	CoupledEntire.lean	19	Names and source lines
04	CoupledUniqueness.lean	16	Names and source lines
05	CoupledGermInverse.lean	13	Names and source lines
06	CoupledRescaling.lean	19	Names and source lines
07	CoupledCharacteristic.lean	23	Names and source lines
08	CoupledPositiveReal.lean	22	Names and source lines
09	CoupledLowerGrowth.lean	16	Names and source lines
10	CoupledUpperGrowth.lean	34	Names and source lines
11	CoupledGrowthTypes.lean	22	Names and source lines
12	CoupledTypeProportions.lean	26	Names and source lines
13	CoupledScalarReduction.lean	43	Names and source lines
14	CoupledOperator.lean	27	Names and source lines
15	CoupledEvaluation.lean	36	Names and source lines
16	CoupledNormalization.lean	30	Names and source lines
17	CoupledGuardedMajorant.lean	30	Names and source lines

Read the evidence with the source

The Block17 report, claim map, recorded execution receipt, and source inventory identify the checkpoint's statements, assumptions, inputs, and recorded checks. The formal I/O inventory and dependency pins provide the reproduction context.

Production modules contain the mathematical definitions and proofs. Files whose names end in Audit.lean inspect axiom use; files in control directories test acceptance or rejection boundaries. Their presence in the inspector does not make them additional production theorems. Local import links open an explicitly selected module in the same work.

The original import receipt is preserved. Later files are separately bound to the dated Block17 publication inventory and their committed source bytes. Adding these reading routes performs no new Lean execution or proof review. The native runner prepares the selected source's dependencies; browser import availability and successful compilation remain separate questions.

Remaining scope

The recorded Block17 development proves an exact guarded-majorant algorithm model. Full Python runtime and dictionary correspondence remains open. Other analytic regions and ordinary type convergence retain their recorded conditions. Consult the remaining-work inventory and current continuation guidance for subsequent work.

Current assessment · Reading volumes