Block01 recurrence companion report
Special Functions
REPORT.md
1 # Coupled special functions: formal verification block
2
3 ## Result
4
5 The new `lean/CoupledFormal.lean` contains **29 named theorem declarations**. They have passed Lean compilation with warnings treated as errors, an exact declaration-by-declaration axiom audit, and a separate kernel replay of the compiled module. The recovered 39-theorem projector core was compiled and audited again. The resulting 68 named declarations are not a count of independent discoveries. Several are supporting lemmas, and the earlier core is not counted a second time as new work.
6
7 The compiler and cached Mathlib were restored from the five stored compact runtime parts. Assembly matched SHA-256 `f7548038f94ea30789ce28fc2ff769c40e9c37d8879ea133e9bea821056342c7`. Lean remains pinned to 4.34.0-rc2 and Mathlib to `aeb72f1e9981b6d35b426b16dca7759be3e7ba06`. No network installation or online compiler service was used.
8
9 ## Mathematical object
10
11 Let the four labeled positive real scales be `(q,r,a,b)`. The paired recurrence begins with `u_0=v_0=1`. For n >= 0, its next terms are
12
13 \[
14 u_{n+1}=\frac{\sum_{i=0}^{n}q^{2i+1}r^{2(n-i)+1}u_i v_{n-i}}{2n+3},\qquad
15 v_{n+1}=\frac{\sum_{i=0}^{n}a^{2i+1}b^{2(n-i)+1}u_i v_{n-i}}{2n+3}.
16 \]
17
18 These are the odd coefficients of the normalized coupled family in Appendix F. The Lean definition constructs the sequence by well-founded recursion. Its existence is not supplied as an axiom or a premise. A separate recurrence contract proves uniqueness among all sequences satisfying the same initial values and equations.
19
20 The module proves that every odd coefficient is strictly positive when all scales are positive. If each scale is also at most one, it proves
21
22 \[
23 0<u_n\le 2^{-n},\qquad 0<v_n\le 2^{-n}.
24 \]
25
26 Both complex series are therefore absolutely convergent whenever `norm(z)^2 < 2`. This is the open disk of radius sqrt(2). The same majorant yields an explicit tail estimate. For either coefficient sequence `c_n`, put `rho=norm(z)^2/2`. For every N >= 0,
27
28 \[
29 \left|\sum_{n\ge N}c_nz^{2n+1}\right|
30 \le \frac{|z|\rho^N}{1-\rho},\qquad |z|^2<2.
31 \]
32
33 The compiled statement uses the reindexed tail `n+N`. It bounds the omitted infinite series. It is not the stronger, whole-plane outer-radius certificate in the research laboratory, and it does not yet identify the sum as a holomorphic solution of the differential equations.
34
35 ## Exact inverse from coefficients through degree seven
36
37 Set `p=qr` and `k=ab`. The formal recurrence is proved to produce the six explicit coefficients `u_1,v_1,u_2,v_2,u_3,v_3` used in Appendix G. In particular,
38
39 \[
40 D=k^2u_2-p^2v_2
41 =\frac{pkar}{15}(q^2-b^2)(qb-ar).
42 \]
43
44 Within the positive domain, Lean proves `D=0` exactly when `q=b` or `qb=ar`. Away from this union, equality of the six coefficients through degree seven forces equality of all four ordered scales. The conclusion is about the labeled pair, not an unlabeled pair up to permutation.
45
46 The proof does not assume the inverse as a black box. It reduces each parameter row to a positive-pair lemma. If `xy=XY` and `p*x+k*y=p*X+k*Y`, subtraction gives
47
48 \[
49 (x-X)(pX-ky)=0.
50 \]
51
52 If `x` and `X` differ, the alternative root relation and the seventh-order observation give
53
54 \[
55 (k^2u-p^2v)(x^2-X^2)=0.
56 \]
57
58 A nonzero defect and positivity then force `x=X`, a contradiction. The second row is treated by the same proved lemma. Positive squares recover the scales themselves, not just their magnitudes.
59
60 The theorem is first checked for the explicit jet map, then transported to the recursively constructed infinite sequence. There is no circular assumption that those coefficients already encode the parameters.
61
62 ## Examples and necessary boundaries
63
64 For `(q,r,a,b)=(1/5,2/5,3/5,7/10)`, the checked exact defect is `189/7812500`, which is nonzero. The corresponding recovery corollary is included.
65
66 A checked collision shows why the defect hypothesis cannot simply be deleted. The distinct positive tuples `(1/4,1/2,1/4,1/2)` and `(1/2,1/4,1/2,1/4)` have zero defect and equal six-coordinate jets. The theorem does not claim that every point on the exceptional surfaces is non-identifiable in every possible observation model. This example refutes unconditional injectivity of the specified jet map.
67
68 ## Verification evidence
69
70 The five verification stages passed: runtime and nine dependency pins, the inherited finite core, the new source compilation and all 29 axiom reports, kernel replay, and five deliberately failing controls. The only reported logical dependencies are `propext`, `Classical.choice`, and `Quot.sound`. There are no `sorryAx` dependencies or new custom axioms in the production module.
71
72 The kernel replay uses `leanchecker` on the newly compiled module. It rechecks the new declarations against the imported environment. It does not replay all of Mathlib from an empty environment, and it is not an external independent proof checker.
73
74 Five negative fixtures reject an incorrect worked defect, an incorrect fifth-order coefficient, equality of distinct boundary parameters, positivity without positive scales, and a placeholder proof. The placeholder exists only in the negative-control directory and is required to fail.
75
76 A separate standard-library Python regression compares dense ordinary-Taylor coefficient matching with the preserved EGF laboratory over 256 rational parameter tuples. It passes **15,658 exact assertions**. These cover coefficients, parity, positivity, geometric bounds, factorization, exceptional surfaces, tail-index conventions, and finite-grid collisions. They are implementation checks, not universal proofs or additional formal theorem counts.
77
78 ## What remains
79
80 This block does not formalize the entire analytic monograph. The next obligations are to identify the convergent sums with holomorphic germs satisfying the coupled differential equations, prove the termwise differentiation and product identities, and then formalize continuation along the strict contraction radius ladder. The global Perron growth law and the full rescaling equivalence of Appendix G.1 remain outside this block. None has been relabeled as complete.
81
82 Appendix G.2 is now checked in its exact coefficient and formal-recurrence form. Its analytic-germ wording still needs the explicit Lean bridge from analytic solutions to that recurrence. Appendix F.1 has checked recurrence, positivity, coefficient bounds, and local absolute convergence, but not its full entire-solution claim.
83
84 The three books and their manuscript sources are unchanged. Their evidence pages are historical snapshots. This companion records the newer formal coverage without pretending the books already contained it. The 99 missing prior-run records described by the previous repair report remain missing.
85
86 ## Reproduction
87
88 From the complete package root, with the stored Linux runtime available:
89
90 ```bash
91 python tools/verify_coupled_block.py --kit /path/to/Komorebi_Portable_Lean_4.34.0-rc2 --work /tmp/sf-coupled-check
92 python tools/check_coupled_exact.py --output /tmp/sf-coupled-exact.json
93 python tools/verify_package.py --strict
94 ```
95
96 Use a new external work directory for a clean replay. A command can be divided into `--stage runtime`, `baseline`, `compile`, `kernel`, and `controls` calls when the execution environment limits individual runs. Compile before kernel or controls. Every stage saves its own receipt even on failure. No network access is required. The runtime is Linux x86-64 and can be used in WSL; native Windows execution was not tested.