What remains after SF-LEAN-B17
Base 200a2798532028f863f923028cb0ead95563975a. Registered F.1-F.3, G.1, guarded G.2, named ancillary F,
main H.1, J mathematical evaluation, factorial normalization and finite arrays
remain complete. J's guarded exact-algorithm specification is now proved,
including first-small stopping, resource failures and abstract validation order.
Full Python refinement remains open; this inventory is not a whole-book audit.
Next: a typed evaluation-result specification combining arrayPolynomial, checkedMajorant, metadata, tail exponent and exact U/V endpoint fields. Then connect the actual certified_evaluation source call path to that specification with explicit Python interpreter/Fraction/stdlib/type/exception/mutation assumptions. Abstract invalid-input tags are not a Python type classifier. The seed is not bit-checked; zero radius bypasses resource validation; radius one requires a step; finite mathematical fuel does not promise fixed-limit success.
| Area | Remaining work |
|---|---|
| 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. |
| Appendix G: component reduction and inverse | Preserve the nonzero-defect guard and align any additional example wrappers before claiming complete chapter correspondence. |
| 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. |
| 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. |
| 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. |
| 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. |
| 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. |
| 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. |
| Appendix D: orbit spectral zeta | Complex analytic continuation, branch-safe absolute interchange, Mellin subtraction, pole/special-value proofs and regularized-product correspondence. |
| 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. |
There are 465 registered declarations, including 39 inherited finite-core names and supporting lemmas. They are not a fraction of manuscript claims. No full claim map or completion percentage exists. Ordinary type convergence remains conditional and G.2's nonzero-defect guard is retained. Reading proofreading is a separate record; earlier as-of reports and source editions remain intact.