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     "id": "SF-B17-LADDER",
4     "manuscript": "Appendix J lines 62-87 and research/coupled_lab.py:disk_majorant",
5     "component": "Exact first-small trace, terminal power identity, budget equivalence, fold/fuel equality and adequate-budget existence.",
6     "status": "kernel_checked",
7     "targets": [
8       "ladder_terminal",
9       "ladder_terminal_small",
10       "ladder_adequate",
11       "ladder_fold_eq",
12       "build_ladder_ok",
13       "build_ladder_of_trace",
14       "build_ladder_ok_iff",
15       "build_ladder_not_bits",
16       "build_ladder_exists_of_adequate"
17     ],
18     "hypotheses": "Q,R rational; trace stops strictly below 1 and records radii >=1. No contraction needed for trace identities.",
19     "boundary": "Exact Lean algorithm specification; no Python interpreter/Fraction/stdlib/dictionary refinement is asserted."
20   },
21   {
22     "id": "SF-B17-FOLD",
23     "manuscript": "Appendix J lines 62-87 and research/coupled_lab.py:disk_majorant",
24     "component": "Reverse fold with a Boolean size predicate: exact successful value and bit-failure characterization.",
25     "status": "kernel_checked",
26     "targets": [
27       "guarded_fold_not_steps",
28       "guarded_fold_ok_iff",
29       "guarded_fold_bits_iff"
30     ],
31     "hypotheses": "Size check follows every update; seed and empty ladder are unchecked.",
32     "boundary": "Exact Lean algorithm specification; no Python interpreter/Fraction/stdlib/dictionary refinement is asserted."
33   },
34   {
35     "id": "SF-B17-CORE",
36     "manuscript": "Appendix J lines 62-87 and research/coupled_lab.py:disk_majorant",
37     "component": "Successful guarded majorants refine the fuel certificate, with explicit resource failures and actual complex/real bounds.",
38     "status": "kernel_checked",
39     "targets": [
40       "guarded_majorant_success",
41       "guarded_majorant_small",
42       "guarded_majorant_zero",
43       "guarded_majorant_no_steps",
44       "guarded_majorant_disk_bound",
45       "guarded_majorant_endpoint_enclosure",
46       "guarded_majorant_step_failure",
47       "guarded_majorant_bit_failure"
48     ],
49     "hypotheses": "Analytic consequences require strict positive contractions, R>=0 and S>x>=0. A success hypothesis is mandatory.",
50     "boundary": "Exact Lean algorithm specification; no Python interpreter/Fraction/stdlib/dictionary refinement is asserted."
51   },
52   {
53     "id": "SF-B17-SIZE",
54     "manuscript": "Appendix J lines 62-87 and research/coupled_lab.py:disk_majorant",
55     "component": "Exact rational binary-width guard.",
56     "status": "kernel_checked",
57     "targets": [
58       "size_fits_iff"
59     ],
60     "hypotheses": "Width is zero at integer zero and otherwise log2(n)+1. Numerator absolute value and positive denominator are measured.",
61     "boundary": "Exact Lean algorithm specification; no Python interpreter/Fraction/stdlib/dictionary refinement is asserted."
62   },
63   {
64     "id": "SF-B17-VALIDATION",
65     "manuscript": "Appendix J lines 62-87 and research/coupled_lab.py:disk_majorant",
66     "component": "Abstract input-validation order and checked endpoint interface.",
67     "status": "kernel_checked",
68     "targets": [
69       "checked_invalid_scales",
70       "checked_negative_radius",
71       "checked_zero_before_resources",
72       "checked_invalid_steps",
73       "checked_invalid_bits",
74       "checked_valid_inputs",
75       "checked_small_seed_unchecked",
76       "checked_success_core",
77       "checked_endpoint_enclosure"
78     ],
79     "hypotheses": "Rational inputs; None tags invalid nonnegative-integer resources. Zero radius bypasses resource validation after scales/radius checks. Runtime Python type classification remains open.",
80     "boundary": "Exact Lean algorithm specification; no Python interpreter/Fraction/stdlib/dictionary refinement is asserted."
81   }
82 ]

Back to source controls

Back to Special Functions