# majorant/ -- certified tail envelope for Frobenius jet towers (main text Eq. (15); SM Section S4)

`envelope_certified.py` implements the lemma below in exact rational arithmetic; `selftest_envelope.py` is its
regression suite (norm bounds against exact operator norms, a planted violation that must be caught, resonant towers,
the DKMM order-6 towers read from `../restrict/` and `../cert_w0/`, and two exact counterexamples showing that an
empirical last-window tail estimate is not a bound). Run `python3 selftest_envelope.py`; it prints
`SELFTEST: ALL CHECKS PASS` and writes `envelope_comparison.md` (cost of rigor versus the empirical estimate).

## 1. Setting

L Fuchsian at z = 0, order r, theta-form  z^{-smin} L = sum_{s=0}^{S} z^s R_s(theta), R_s in Q[theta], deg R_s <= r,
R_0 the indicial polynomial with deg R_0 = r (regular singular point), leading coefficient lc, and factorization over C
R_0(theta) = lc prod_i (theta - lambda_i)^{mu_i}, sum_i mu_i = r.

Jet space V = C^J with the l1 norm ||v|| = sum_j |v_j|. Let D : V -> V be any nilpotent operator with D^J = 0 and
induced norm ||D|| <= 1. The two instances used here: (i) multiplication by rho on C[rho]/(rho^J) (rho-jets);
(ii) the divided-power shift (D gamma)_j = gamma_{j+1} (log-layer towers). Both have induced l1 norm exactly 1.

Definition (jet tower past horizon N0, exponent e in R). A sequence b_m in V (m >= 0) such that for every m > N0:

    R_0(e+m+D) b_m = - sum_{s=1}^{min(S,m)} R_s(e+m-s+D) b_{m-s}.                    (REC)

The Frobenius jets at a point of maximal unipotent monodromy satisfy (REC) with e = alpha, J = r, N0 = 0, D = (i);
Frobenius towers of a resonant operator satisfy it past the largest resonance; the DKMM order-6 towers satisfy it with
D = (ii), e = 0, N0 = 3.

## 2. Lemma (certified geometric tail envelope)

Let (b_m) be a jet tower past horizon N0 at exponent e. Put

    beta      = max(0, max_i Re lambda_i - e),
    rbar_{s,k} = |[theta^k] R_s|,   c_s = max(0, e - s + 1),
    G(m)      = prod_i sum_{j=0}^{J-1} C(mu_i+j-1, j) (m-beta)^{-j},
    Phi(m,t)  = G(m) / (|lc| (m-beta)^r) * sum_{s=1}^{S} t^{-s} sum_{k=0}^{r} rbar_{s,k} (m+c_s)^k.

Choose N and t > 0 with
    (H1) N >= N0,  N > beta,  N >= S + max(0, ceil(-e));
    (H2) Phi(N+1, t) <= 1.
Set K = max_{N-S < m' <= N} ||b_{m'}|| t^{-m'}. Then

    (C1) ||b_m|| <= K t^m for all m > N;
    (C2) for 0 < x < 1/t and each jet level j:  | sum_{m>N} (b_m)_j x^m | <= sum_{m>N} ||b_m|| x^m <= K (tx)^{N+1} / (1 - tx);
    (C3) for any d >= 0, if q := t x e^{d/(N+1)} < 1 then  sum_{m>N} ||b_m|| m^d x^m <= K (N+1)^d (tx)^{N+1} / (1 - q).

All quantities in (H2), K, (C2), (C3) are exactly computable in Q when the coefficients, e, t, x are rational and the
lambda_i are rational (otherwise replace Re lambda_i by any certified upper bound; the lemma holds a fortiori).

## 3. Proof

Throughout ||.|| is the l1 vector norm and its induced operator norm; m > N.

(P1) For u in R and P in R[theta]: ||P(u+D)|| <= sum_k |P_k| ||(u+D)^k|| <= sum_k |P_k| (|u| + ||D||)^k <= sum_k |P_k| (|u|+1)^k.

(P2) By (H1), e+m-s >= 0 for 1 <= s <= S (if e >= 0 this is m-s > N-S >= 0; if e < 0 it is m >= N+1 >= S+ceil(-e)+1 > s-e).
Hence |e+m-s| + 1 = m + (e-s+1) <= m + c_s, and by (P1)  ||R_s(e+m-s+D)|| <= sum_k rbar_{s,k} (m + c_s)^k.

(P3) For each root, a_i := e+m-lambda_i has Re a_i = m - (Re lambda_i - e) >= m - beta > 0, so a_i I + D is invertible with
(a_i I + D)^{-1} = sum_{j=0}^{J-1} (-1)^j D^j a_i^{-j-1} (multiply out; the sum telescopes and D^J = 0). Taking the mu_i-th
power and collecting D^j:  (a_i I + D)^{-mu_i} = sum_{j=0}^{J-1} C(mu_i+j-1, j) (-D)^j a_i^{-mu_i-j}, so
||(a_i I + D)^{-mu_i}|| <= sum_{j=0}^{J-1} C(mu_i+j-1, j) (m-beta)^{-mu_i-j}. Multiplying over i (sum mu_i = r):
||R_0(e+m+D)^{-1}|| <= G(m) / (|lc| (m-beta)^r).

(P4) Phi(., t) is nonincreasing on (beta, infinity): each factor (m-beta)^{-j} of G is nonincreasing, and each summand
carries (m+c_s)^k / (m-beta)^r with 0 <= k <= r, c_s >= 0 >= -beta; since m + c_s >= m - beta > 0,
d/dm log[(m+c_s)^k (m-beta)^{-r}] = k/(m+c_s) - r/(m-beta) <= (k-r)/(m-beta) <= 0. So Phi(m,t) <= Phi(N+1,t) <= 1 for
all m >= N+1 by (H2).

(P5) (C1) by strong induction on the claim ||b_m|| <= K t^m for m > N-S. Base: m in (N-S, N] is the definition of K.
Step m > N: (REC) applies since m > N >= N0 and m > S; the indices m-s in [m-S, m-1] lie in (N-S, m). R_0(e+m+D) is
invertible by (P3), so
||b_m|| <= ||R_0(e+m+D)^{-1}|| sum_{s=1}^{S} ||R_s(e+m-s+D)|| ||b_{m-s}||
        <= [G(m)/(|lc|(m-beta)^r)] sum_s (sum_k rbar_{s,k}(m+c_s)^k) K t^{m-s} = K t^m Phi(m,t) <= K t^m.

(P6) (C2): |(b_m)_j| <= ||b_m||, and sum_{m>N} K (tx)^m is a geometric series with ratio tx < 1.

(P7) (C3): the terms u_m = K m^d (tx)^m satisfy u_{m+1}/u_m = tx (1+1/m)^d <= tx e^{d/m} <= q < 1 for m >= N+1, so the
sum is at most the first term over (1-q).

Remark. If all S seeds in (N-S, N] vanish then K = 0 and (C1) gives b_m = 0 for m > N, as it must: (REC) determines
b_m from the previous S jets with an invertible leading operator.

## 4. Scope

The l1 route ignores sign cancellation among theta-form coefficients. The smallest admissible t (root of
Phi(N+1,t) = 1) tends, as N grows, to the root t*_inf of sum_s rbar_{s,r} t^{-s} = |lc|, and 1/t*_inf can be strictly
smaller than the true radius of convergence; no bound built from coefficientwise absolute values can certify the full
disk in general. The lemma therefore certifies the tail on |z| < 1/t_min(N), with 1/t_min(N) increasing to 1/t*_inf;
in every case used here half the radius of convergence is admissible. Where the evaluation point must lie closer to
the boundary, the transport inserts additional expansion points instead. `envelope_comparison.md` (written by the
self-test) tabulates, for the operators exercised, t_min against the true radius and the certified tail against the
measured one.