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 #!/usr/bin/env python3
2 """Finite exact regressions linking the new Lean formulas to the existing EGF laboratory.
3 These rational tests are not substitutes for the Lean universal proofs.
4 """
5 from __future__ import annotations
6 import argparse
7 from fractions import Fraction as Q
8 from itertools import product
9 import json
10 from math import factorial
11 from pathlib import Path
12 import sys
13 import time
14 sys.dont_write_bytecode = True
15 ROOT = Path(__file__).resolve().parents[1]
16 sys.path.insert(0, str(ROOT/'research'))
17 import coupled_lab  # preserved original EGF implementation
18 
19 def main() -> int:
20     parser = argparse.ArgumentParser(description=__doc__)
21     parser.add_argument('--output', type=Path, required=True)
22     args = parser.parse_args()
23     start = time.monotonic()
24     counts: dict[str, int] = {}
25     def check(label: str, condition: bool) -> None:
26         if not condition:
27             raise AssertionError(label)
28         counts[label] = counts.get(label, 0) + 1
29     def dense(scales: tuple[Q, ...], last: int) -> tuple[list[Q], list[Q]]:
30         q, r, a, b = scales
31         u, v = [Q(0)], [Q(0)]
32         for degree in range(2*last+1):
33             du = Q(degree == 0) + sum((q**i * r**(degree-i) * u[i] * v[degree-i]
34                                       for i in range(degree+1)), Q(0))
35             dv = Q(degree == 0) + sum((a**i * b**(degree-i) * u[i] * v[degree-i]
36                                       for i in range(degree+1)), Q(0))
37             u.append(du / (degree+1))
38             v.append(dv / (degree+1))
39         return u, v
40     grid = tuple(Q(i, 5) for i in range(1, 5))
41     seen: dict[tuple[Q, ...], tuple[Q, ...]] = {}
42     regular = 0
43     cases = list(product(grid, repeat=4))
44     for case, scales in enumerate(cases):
45         q, r, a, b = scales
46         p, k = q*r, a*b
47         u, v = dense(scales, 6)
48         A, B = coupled_lab.coupled_odd_derivatives(*scales, last=6)
49         for row, derivatives in ((u, A), (v, B)):
50             for n in range(7):
51                 check('ordinary_vs_EGF', row[2*n+1] == derivatives[n]/factorial(2*n+1))
52                 check('strict_positivity', row[2*n+1] > 0)
53                 check('geometric_majorant', row[2*n+1] <= Q(1,2)**n)
54                 check('even_coefficients_zero', row[2*n] == 0)
55         U1, V1 = p/3, k/3
56         U2, V2 = p*(p*q*q+k*r*r)/15, k*(p*a*a+k*b*b)/15
57         U3 = p*(q**4*U2+p*p*U1*V1+r**4*V2)/7
58         V3 = k*(a**4*U2+k*k*U1*V1+b**4*V2)/7
59         jets = (U1, V1, U2, V2, U3, V3)
60         check('six_jet_formula', jets == (u[3],v[3],u[5],v[5],u[7],v[7]))
61         defect = k*k*U2-p*p*V2
62         check('defect_factorization', defect == p*k*a*r*(q*q-b*b)*(q*b-a*r)/15)
63         check('zero_locus', (defect == 0) == (q == b or q*b == a*r))
64         if defect:
65             regular += 1
66             check('regular_jet_collision', jets not in seen or seen[jets] == scales)
67             seen[jets] = scales
68         if case < 8:
69             for z in (Q(1,2), Q(1), Q(4,3)):
70                 ratio = z*z/2
71                 for N in range(8):
72                     upper = z*ratio**N/(1-ratio)
73                     for row in (u, v):
74                         finite_tail = sum((row[2*n+1]*z**(2*n+1) for n in range(N,7)),Q(0))
75                         check('tail_bound_indexing', 0 <= finite_tail <= upper)
76     sl, sr = (Q(1,4),Q(1,2),Q(1,4),Q(1,2)), (Q(1,2),Q(1,4),Q(1,2),Q(1,4))
77     check('boundary_parameters_distinct', sl != sr)
78     check('boundary_jet_collision', dense(sl,3) == dense(sr,3))
79     worked = (Q(1,5),Q(2,5),Q(3,5),Q(7,10))
80     u, v = dense(worked,3)
81     p, k = worked[0]*worked[1], worked[2]*worked[3]
82     d = k*k*u[5]-p*p*v[5]
83     check('worked_defect', d == Q(189,7812500))
84     check('reject_draft_numeric_typo', d != Q(189,3125000))
85     report = {'passed':True, 'parameter_grid_cases':len(cases), 'regular_grid_cases':regular,
86               'last_odd_index':6, 'exact_assertions':sum(counts.values()), 'counts':counts,
87               'seconds':round(time.monotonic()-start,6),
88               'scope':'Finite rational regressions; distinct from kernel proof of the universal statements.'}
89     args.output.parent.mkdir(parents=True,exist_ok=True)
90     args.output.write_text(json.dumps(report,indent=2)+'\n')
91     print(json.dumps(report,indent=2))
92     return 0
93 
94 if __name__ == '__main__':
95     try:
96         raise SystemExit(main())
97     except (ValueError, OSError, AssertionError) as exc:
98         print('FAILED: '+str(exc),file=sys.stderr)
99         raise SystemExit(1)

Back to source controls

Back to Special Functions