REMAINING_WORK.md
Special Functions
REMAINING_WORK.md
1 # What remains after SF-LEAN-B17
2
3 Base `200a2798532028f863f923028cb0ead95563975a`. Registered F.1-F.3, G.1, guarded G.2, named ancillary F,
4 main H.1, J mathematical evaluation, factorial normalization and finite arrays
5 remain complete. J's guarded exact-algorithm specification is now proved,
6 including first-small stopping, resource failures and abstract validation order.
7 Full Python refinement remains open; this inventory is not a whole-book audit.
8
9 Next: a typed evaluation-result specification combining arrayPolynomial,
10 checkedMajorant, metadata, tail exponent and exact U/V endpoint fields. Then
11 connect the actual certified_evaluation source call path to that specification
12 with explicit Python interpreter/Fraction/stdlib/type/exception/mutation
13 assumptions. Abstract invalid-input tags are not a Python type classifier.
14 The seed is not bit-checked; zero radius bypasses resource validation; radius
15 one requires a step; finite mathematical fuel does not promise fixed-limit success.
16
17 | Area | Remaining work |
18 | --- | --- |
19 | Appendix F: reductions, examples and parameter structure | Exhaustive explanatory correspondence, including any scalar row-order maximum comparison and generic variation of actual functions/vectors along parameter surfaces. These are not part of the newly registered contracts. |
20 | Appendix G: component reduction and inverse | Preserve the nonzero-defect guard and align any additional example wrappers before claiming complete chapter correspondence. |
21 | Appendix H: autonomous projections and operator decoupling | Odd-input-only restriction remark and tensor/rank explanatory derivations are not separately registered. Main H.1 and S1-S3 operator contracts are complete. |
22 | Appendix I: finite-resolution atlas | Lean correspondence for the analytic tail/error bounds and exact numerical certificates for the three resolution mechanisms, including derivative channels and two-sided thresholds. |
23 | Appendix J: whole-plane certified evaluation | Compose the typed certified-evaluation result and metadata/endpoints, then establish actual Python source-to-model correspondence with explicit interpreter/Fraction/stdlib/type/exception/mutation assumptions. Other J degree/denominator-clearing/symmetry claims remain to map. |
24 | Appendix A: multi-tap growth and parameter continuity | Extend beyond the checked coupled/scalar foundations to the full positive active tap bank, exact growth/type law, holomorphic parameter dependence and quantitative tap continuity. |
25 | Appendix B: arithmetic inverse and character resolution | Infinite positive-atom measures and analytic inverse, conditioning/gap bounds, prime-window instability, Hilbert-feature interpretation and fixed-modulus character-sector decay. |
26 | Appendix C: finite-prime sieves and signed-atom detectors | Measure positivity chamber, explicit negative-atom detectors, conditional prime fibers, moment/margin geometry and their analytic/infinite-measure hypotheses. |
27 | Appendix D: orbit spectral zeta | Complex analytic continuation, branch-safe absolute interchange, Mellin subtraction, pole/special-value proofs and regularized-product correspondence. |
28 | Appendix E: sequences, trees and polyphase | Map the full sequence/tree/polyphase claims and bridge formal/finite identities to their actual analytic EGF/root-filter realizations. |
29
30 There are 465 registered declarations, including 39 inherited finite-core names
31 and supporting lemmas. They are not a fraction of manuscript claims. No full
32 claim map or completion percentage exists. Ordinary type convergence remains
33 conditional and G.2's nonzero-defect guard is retained. Reading proofreading
34 is a separate record; earlier as-of reports and source editions remain intact.