Special Functions

Download original file

This is the original source text. Reading it does not run or verify the program.

Read the typeset paper

1 [
2   {
3     "manuscript": "Appendix F.1",
4     "component": "infinite coefficient recurrence; existence and uniqueness",
5     "status": "kernel_checked",
6     "targets": [
7       "coefficients_solution",
8       "coefficient_solution_exists_unique"
9     ],
10     "boundary": "No equivalence to an analytic differential equation is asserted."
11   },
12   {
13     "manuscript": "Appendix F.1",
14     "component": "strict positivity and geometric bound",
15     "status": "kernel_checked",
16     "targets": [
17       "coefficients_positive",
18       "coefficients_le_geometric"
19     ],
20     "boundary": "Scale bounds are explicit. The geometric bound allows scales equal to one."
21   },
22   {
23     "manuscript": "Appendix F.1 local step",
24     "component": "absolute convergence on norm(z)^2 < 2",
25     "status": "kernel_checked",
26     "targets": [
27       "coefficient_series_absolutely_convergent"
28     ],
29     "boundary": "Holomorphicity, differentiated equations and entire continuation remain unformalized."
30   },
31   {
32     "manuscript": "supporting derived bound",
33     "component": "infinite-series tail certificate on the same disk",
34     "status": "kernel_checked",
35     "targets": [
36       "odd_series_tail_bound"
37     ],
38     "boundary": "Not the full outer-radius whole-plane laboratory certificate."
39   },
40   {
41     "manuscript": "Appendix G.1 algebraic step",
42     "component": "exact factorization and zero locus of D",
43     "status": "kernel_checked",
44     "targets": [
45       "defect_factor",
46       "defect_eq_zero_iff"
47     ],
48     "boundary": "The equivalence with analytic component rescaling is still open as a Lean obligation."
49   },
50   {
51     "manuscript": "Appendix G.2 coefficient formulation",
52     "component": "generic injectivity of the labeled six-coordinate jet and formal recurrence",
53     "status": "kernel_checked",
54     "targets": [
55       "seven_jet_injective",
56       "parameters_of_jet_through_degree_seven",
57       "parameters_of_formal_pair_eq"
58     ],
59     "boundary": "Analytic-germ formulation awaits the analytic-solution-to-recurrence bridge."
60   },
61   {
62     "manuscript": "Appendix G worked pair and guard",
63     "component": "nondegenerate exact example and degenerate jet collision",
64     "status": "kernel_checked",
65     "targets": [
66       "workedScales_defect",
67       "workedScales_recoverable",
68       "boundary_collision"
69     ],
70     "boundary": "The collision is an example, not a classification of identifiability on the exceptional set."
71   }
72 ]

Back to source controls

Back to Special Functions