evidence_notes.tex

Special Functions

evidence_notes.tex

Download original file

This is the original TeX manuscript source. Use the paper’s PDF for typeset equations.

Read the typeset paper

Read this chapter with formatted equations

Skip source text

1 \hypertarget{computational-contract-and-limitations}{%
2 \section*{Dilation: computation and proof scope}\label{computational-contract-and-limitations}}
3 
4 \path{checks/dilation_type.py} uses exact \texttt{fractions.Fraction}
5 arithmetic for its finite assertions. It checks the algebraic
6 fixed-width and interval-propagation conditions for rational scales and
7 weights, the positive homogeneous weight-polynomial majorant, derivative
8 bounds on a normalized simplex, the improved total-variation coefficient
9 bound, and a distinct ordered-tree evaluation against the recurrence.
10 Scalar examples and the explicit real type constants are displayed at
11 high precision separately from exact assertions.
12 
13 The finite checks do not establish universal analytic conclusions.
14 The growth and convergence results depend on the proofs in Appendix~A.
15 Historical priority is a separate literature question. No numerical fit is
16 presented as evidence that a type limit exists.
17 
18 The earlier moving-width lower argument used a fixed \(\alpha<1\); it
19 proved orders below \(\rho\) and then recovered the order by
20 \(\alpha\uparrow1\), but did not establish positive lower type at
21 \(\rho\). This is a limitation of that argument, not a counterexample.
22 The fixed-width comparison closes precisely that missing implication.
23 The evidence archive retains execution failures, their causes and the
24 subsequent corrected runs.
25 
26 
27 \hypertarget{v11-coupled_growth_full-proof-provenance-and-remaining-questions}{%
28 \section*{Coupled growth: scope and open questions}\label{v11-coupled_growth_full-proof-provenance-and-remaining-questions}}
29 
30 The decisive extension is from a scalar positive comparison to a
31 comparison weighted by a positive eigenvector. The fixed-width integral
32 controls the lower type at the exact exponent. A fixed proportional
33 interval \([\alpha R,R]\), with \(\alpha<1\), would only give a smaller
34 exponent through \(\alpha^sP(s)\). Letting \(\alpha\) tend to one
35 recovers exact order but does not, by itself, yield positive lower type.
36 This is a limitation of that alternative route, not a failure of the
37 theorem.
38 
39 The complete proofs in Appendix~F close the target on the strictly positive
40 contraction domain. No computed example is used as a universal analytic
41 premise. The displayed rational Taylor coefficients were evaluated
42 directly from the exact recurrence with Python
43 \texttt{fractions.Fraction} as a transcription check. Their independent
44 algebraic residual checks belong to the archived exact computation record.
45 
46 Remaining questions include the existence and value of ordinary type
47 limits, possible oscillations, zeros, angular growth, connection
48 formulas, and regimes with zero, negative, complex, or noncontracting
49 scales. Positivity and strict contraction are hypotheses of the results
50 here. This route makes no historical priority claim and no claim of a
51 Lean formalization.
52 
53 The preserved self-review checked coefficient and eigenvector notation,
54 logarithm and power domains, seed and child interval endpoints, and both
55 vector orientations. Its recorded conclusion was that no unresolved gap had
56 been identified in that argument. This is a statement about the scope and
57 outcome of that review, not a substitute for independent verification.
58 
59 
60 \hypertarget{v11-coupled_inverse_full-verification-scope}{%
61 \section*{Coupled inverse: verification scope}\label{v11-coupled_inverse_full-verification-scope}}
62 
63 The identities above are algebraic and the proofs use exact positive
64 parameters. The companion check script compares the first coefficients
65 against the full independent recursion, verifies the factorization over
66 a rational grid, checks the candidate-selection formulas, and tests both
67 reduction surfaces by comparing many exact Taylor coefficients. Finite
68 checks test the implementation and the worked examples. The equivalence
69 and recovery theorems follow from the proofs.
70 
71 Historical priority of these specific statements remains a separate
72 literature question.

Back to source controls

Other PDFs for this work

Original file and source record

This copy matches the recorded source file. Its publication here does not change the work’s review status.

SHA-256: 25130f2a92de1ced440c928f1c7da26b1a3c77f8c975e774604c11b4d8d422a9

Original source on GitHub

Back to Special Functions