Block17 formal coverage and recorded replay
Special Functions
REPORT.md
1 # SF-LEAN-B17: guarded exact majorant specification
2
3 The bounded first-small ladder and guarded reverse-fold contract is proved
4 over exact rationals. A successful return B supplies a trace of length k no
5 larger than the step budget, terminal Q^k*R<1, and
6 B=rationalDiskMajorant Q k R. Under strict positive contractions and R>=0,
7 B bounds the actual canonical complex functions on |z|<=R. For S>x>=0,
8 the exact endpoints built from the Block16 array polynomial and
9 B*(x/S)^(2N+3) enclose the actual real component whenever the guarded
10 majorant at S succeeds. Last index N still retains N+1 coefficients.
11
12 The trace stops at the first radius strictly below one. A radius equal to
13 one requires a step, and a zero step budget then fails. Trace success is
14 equivalent to the trace relation plus length<=budget. Adequate mathematical
15 fuel gives a successful ladder; it does not guarantee a fixed step or bit
16 budget succeeds. Step errors and bit errors are explicit distinct results.
17
18 The reverse fold checks the size predicate after every computed update.
19 Its successful value is the ordinary foldr; success is characterized by
20 that value and the conjunction of all post-update checks. Bit failure is
21 equivalent to a failed check. The terminal seed is not checked. For Q=1/2,
22 R=2 the ladder is [2,1], terminal 1/2, seed 2/3 and bound 500/81. Forward
23 folding would give 757/81 and is rejected by an exact control. A small-radius
24 seed can exceed the bit limit and still be returned, as in the source.
25
26 The concrete rational size uses max of numerator-absolute-value and positive
27 denominator binary widths, with width(0)=0 and width(n)=log2(n)+1 otherwise.
28 An abstract checked-input wrapper preserves scale rejection before radius
29 rejection, zero-radius return before resource validation, step-input validation
30 before bit-input validation, and positive bit bounds. Some 0 is a valid step
31 budget. None represents an invalid nonnegative-integer resource input; it
32 does not implement a Python runtime type checker. Fraction conversion failures
33 and mappings of bool/int/negative/exception objects remain outside the model.
34
35 Authority: Appendix J, monograph/sections_v11/coupled_lab_full.tex lines
36 62-87, and research/coupled_lab.py:disk_majorant. Mathematical base `200a2798532028f863f923028cb0ead95563975a`;
37 editorial publication parent `0eae1fe6a4bf55db27af69ef40b405643aa2e5a9`. Python and manuscript sources are
38 assessed at pinned hashes, not used as trusted proof leaves and not edited.
39
40 There are **30 new theorem declarations**, for **465 registered names**.
41 All **66 fresh replay steps** pass: seventeen compilations, audits and
42 same-kernel replays, 426 fresh coupled theorem axiom audits, four expected
43 rejections and one positive fixture. The finite core's 39 names retain
44 inherited evidence; Mathlib imports are cached, not freshly rebuilt or replayed.
45 Allowed axioms are propext, Classical.choice and Quot.sound. Review is self-review.
46 Formal I/O records 59 inputs, 67 packaged outputs, seventeen generated objects
47 and 39 staging copies; assessment I/O has 37 inputs and two outputs. Development
48 source/log pairs and preflight diagnostics are separate from accepted evidence.
49
50 This completes the registered **Lean guarded-algorithm specification**.
51 Actual Python interpreter, Fraction, comb/factorial/bit_length implementation,
52 type/exception classification, list mutation and certified_evaluation dictionary
53 correspondence remain open. Next: compose the proved array and guarded-majorant
54 interfaces into a typed evaluation-result specification, then assess the source
55 call path and exact metadata/endpoints with explicit runtime assumptions.
56 Other J degree/denominator/symmetry, ancillary F/H, I and A-E remain.