Finite complex-contour validation of Floquet multiplier clusters

Input a positive integer $n$, a nonempty complex matrix family $\mathcal{M}$ enclosed entrywise by finite dyadic real/imaginary rectangles, a dyadic center matrix $M_0$, a certified dyadic bound ${\delta }_A\ge {\sup }_{M\in \mathcal{M}}\mathrm{\parallel }M-M_0{\mathrm{\parallel }}_{\mathrm{\infty },\mathbb{C}}$, and a simple positively oriented strictly convex polygon $\mathrm{\Gamma }$ with dyadic vertices and filled interior $P$. Supply the dyadic disk cover and point preconditioners required by Finite complex contour resolvent validator with cover and inconclusive statuses, a positive integer $N$ for midpoint subdivisions of each edge, a positive integer $K_{\pi }$ for the arctangent series, and a finite arithmetic budget. The family may be the monodromy block of a validated shooting jet; no correlation between matrix entries is required. A complex rectangle here is the product of one closed dyadic real interval and one closed dyadic imaginary interval for each matrix entry.

1. Write the ordered dyadic vertices as $v_0,\dots ,v_{r-1}$, with indices modulo $r$. Require $r\ge 3$, pairwise distinct vertices, and, for every $i$ and every $k\mathrm{\notin }\{i,i+1\}$, the exact rational determinant $\mathrm{Im}(\overline{(v_{i+1}-v_i)}(v_k-v_i))>0$. Each directed edge is then an exposed edge of the convex hull; since there are $r$ such edges and $r$ distinct vertices, they form its simple counterclockwise boundary. If any test fails, output inconclusive. Then run the resolvent-cover validator on every edge for the entire family. If any segment is uncovered, an outward inequality is not strict, or no finite upper bound $M_R$ on $\mathrm{\parallel }(zI-M{)}^{-1}{\mathrm{\parallel }}_{\mathrm{\infty },\mathbb{C}}$ is returned, output inconclusive.
2. Subdivide each oriented edge $e_j=b_j-a_j$ into $N$ equal parts, with rational midpoints $z_{jk}=a_j+(k+1\mathrm{/}2)e_j\mathrm{/}N$. By exact rational complex elimination, compute $R_{jk}^0=(z_{jk}I-M_0{)}^{-1}$; a singular center matrix or an incomplete operation returns inconclusive. For each rational complex entry $a+ib$ of $R_{jk}^0$, use rational square-root bisection to find an upper bound for $\sqrt{a^2+b^2}$, then sum row bounds to obtain $b_{jk}\ge \mathrm{\parallel }{R}_{jk}^0{\mathrm{\parallel }}_{\mathrm{\infty },\mathbb{C}}$. Use the same bisection to obtain $s_j\ge \mathrm{\mid }{e}_j\mathrm{\mid }$. If the finite budget does not produce these rational bounds, return inconclusive.
3. Form the exact center midpoint sum $S_0={\sum }_j\frac{e_j}{N}{\sum }_{k=0}^{N-1}\mathrm{tr}{R}_{jk}^0,$ and the outward error allowance $E=\frac{n{M}_R^2}{2N}{\sum }_j\mathrm{\mid }{e}_j{\mathrm{\mid }}^2+\frac{n{M}_R{\delta }_A}{N}{\sum }_{j,k}{s}_j{b}_{jk}\mathrm{.}$ The first term uses the exact rational squared modulus of each rational edge; the second uses the rational upper edge length $s_j$. The first term bounds midpoint quadrature error; the second bounds replacing each family resolvent by the center resolvent. All sums and products are exact rationals; if a required rational square-root upper bound is unavailable, return inconclusive.
4. Enclose $\pi$ using $\pi =4\arctan (1)$ and the alternating partial sum $4{\sum }_{k=0}^{K_{\pi }-1}(-1{)}^k\mathrm{/}(2k+1)$ with tail radius $4\mathrm{/}(2K_{\pi }+1)$. Require a positive lower endpoint. Using exact rational endpoint arithmetic, enclose $S_0\mathrm{/}(2\pi i)$ and inflate its real and imaginary intervals by $E\mathrm{/}(2{\pi }_{\mathrm{l}\mathrm{o}\mathrm{w}})$; call the resulting rectangle $I$.
5. Choose an integer $c$ and return certified-count(c) only if $0\le c\le n$, $\mathrm{Re}I\subset (c-1\mathrm{/}2,c+1\mathrm{/}2)$, $\mathrm{Im}I\subset (-1\mathrm{/}2,1\mathrm{/}2)$, and $0\in \mathrm{Im}I$. Otherwise return inconclusive. This operation counts roots with algebraic multiplicity in $\mathrm{int}P$ for every matrix in the supplied family; it does not classify a cluster touching the unit circle as stable or unstable.

For a simple separated multiplier, an optional left/right-conditioned finite enclosure may also be reported using A separated simple Floquet multiplier has a left/right-conditioned finite enclosure. The contour count remains the required path for clusters or unresolved individual eigenvectors.

The matrix family may be taken from the monodromy block of Certified residual, Jacobian, trajectory, and monodromy enclosures for periodic shooting. Resolvent bounds use the complex infinity norm The complex induced infinity matrix norm and its product inequality The complex infinity matrix norm is compatible and submultiplicative; the boundary cover is interpreted by The finite disk cover validator returns a uniform resolvent bound on success. Root counting uses The argument principle for an admissible null-homologous cycle, the inside/outside polygon index A positively oriented convex polygon has winding index one inside and zero outside, and the determinant derivative The determinant differential is $D\det (A)[H]=\mathrm{tr}(\mathrm{adj}(A)H)$ at every matrix, and Jacobi's formula holds on the invertible locus. The root multiplicities are those of the characteristic polynomial by A complex polynomial of degree $n$ has exactly $n$ roots counted with multiplicity. The rational $\pi$ enclosure uses Principal arctangent: derivative, integral, power series, and the Gregory–Leibniz series and The alternating series test: if $(b_k)$ is nonincreasing with $b_k\to 0$ then ${\sum }_k(-1{)}^k{b}_k$ converges, the sum lies between any two consecutive partial sums, and the error after $n$ terms is at most $b_n$.