TheoremStatement: AI-adaptedProof: AI-generatedPipeline-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A verified contour count encloses every Floquet multiplier in a cluster

Statement

If Finite complex-contour validation of Floquet multiplier clusters returns certified-count(c) for a nonempty matrix family $M$ and a simple positively oriented convex polygon $Γ$ , then every $M \in M$ has exactly $c$ eigenvalues in $int P$ , counted with algebraic multiplicity, and no eigenvalue on $Γ$ . In particular, this holds for every exact monodromy matrix enclosed by a validated shooting jet whose interval block is contained in $M$ .

Facts & Assumptions

Given: A successful count record, its outward interval arithmetic, its resolvent-cover result, the matrix family, and the positive polygon.

[F1]

A successful resolvent-cover validation bounds $∥ (z I - M)^{- 1} ∥_{\infty, C}$ uniformly on each covered edge and for all $M \in M$ (The finite disk cover validator returns a uniform resolvent bound on success).

[F2]

For an invertible matrix $A$ , the determinant derivative in direction $H$ is $D \det (A) [H] = \det (A) tr (A^{- 1} H)$ (The determinant differential is $D \det (A) [H] = tr (adj (A) H)$ at every matrix, and Jacobi's formula holds on the invertible locus).

[F3]

The argument principle counts zeros of a holomorphic function by the logarithmic-derivative contour integral with winding-number weights (The argument principle for an admissible null-homologous cycle); for the positive convex polygon the index is one inside and zero outside (A positively oriented convex polygon has winding index one inside and zero outside).

[F4]

Eigenvalues are exactly the roots of the characteristic polynomial (For every finite-dimensional space, $σ_{F} (T)$ is exactly the set of roots in $F$ of $χ_{T}$ ). Algebraic multiplicity means the multiplicity of the corresponding polynomial root. The characteristic polynomial of an $n \times n$ matrix is monic of degree $n$ ( $χ_{A} (x)$ is monic of degree $n$ ; for $n \geq 1$ its $x^{n - 1}$ coefficient is $- tr (A)$ and its constant coefficient is $(- 1)^{n} \det (A)$ , while $χ_{0 \times 0} = 1$ ), so it has $n$ complex roots counted with multiplicity (A complex polynomial of degree $n$ has exactly $n$ roots counted with multiplicity).

[F5]

The identity $π = 4 \arctan (1)$ and the alternating-series remainder bound justify the rational interval for $π$ (Principal arctangent: derivative, integral, power series, and the Gregory–Leibniz series, 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}$ ); all later endpoint operations are exact rational arithmetic.

[F6]

The finite procedure verifies the resolvent cover, midpoint subdivisions, sample inverses, error terms and strict integer-neighborhood test before returning a count (Finite complex-contour validation of Floquet multiplier clusters).

[F7]

The complex infinity matrix norm is submultiplicative (The complex infinity matrix norm is compatible and submultiplicative).

[F8]

Under $C ≅ R^{2}$ , a continuously differentiable complex-valued curve whose modulus of the derivative is bounded by $L$ changes by at most $L$ times the interval length (The mean value inequality: if $f : [a, b] \to R^{m}$ is continuous and differentiable on $(a, b)$ with $∥ f^{'} ∥_{2} \leq M$ , then $∥ f (b) - f (a) ∥_{2} \leq M (b - a)$ ).

Proof

1.1F1F7F8givenalgebra

Fix $M \in M$ . Along an edge $z (t) = a + t e$ , put $R_{M} (t) = (z (t) I - M)^{- 1}$ . By [F1] this inverse exists and has norm at most $m$ . For $h$ with $t, t + h \in [0, 1]$ , the resolvent identity gives $R_{M} (t + h) - R_{M} (t) = - h e R_{M} (t + h) R_{M} (t)$ . Thus [F1] and [F7] imply $∥ R_{M} (t + h) - R_{M} (t) ∥_{\infty, C} \leq ∣ h ∣ ∣ e ∣ m^{2}$ , so $R_{M}$ is continuous; dividing the identity by $h$ and taking the limit gives $R_{M}' (t) = - e R_{M} (t)^{2}$ for interior $t$ . Therefore $g (t) = e tr R_{M} (t)$ has $g' (t) = - e^{2} tr (R_{M} (t)^{2})$ . Since each diagonal entry is bounded by its row sum, $∣ tr A ∣ \leq n ∥ A ∥_{\infty, C}$ , so [F1] and [F7] give $∣ g' (t) ∣ \leq n ∣ e ∣^{2} m^{2}$ . By [F8], on each subinterval of length $1 / N$ , $∣ g (t) - g (t_{m i d}) ∣ \leq n ∣ e ∣^{2} m^{2} / (2 N)$ ; hence the integral error on that cell is at most $n ∣ e ∣^{2} m^{2} / (2 N^{2})$ . Summing all $N$ cells and edges gives the first term of $E$ .

2.1F1F5F6F7step 1.1algebra

At a sample point, the resolvent identity gives $R_{M} - R^{0} = R_{M} (M - M_{0}) R^{0}$ . Therefore $∣ tr (R_{M} - R^{0}) ∣ \leq n m b_{j k} δ_{A}$ . Multiplying by the edge weight and using $s_{j} \geq ∣ e_{j} ∣$ yields the second term of $E$ after summing samples. Thus the exact contour integral $\int_{Γ} tr (z I - M)^{- 1} d z$ lies in the complex disk centered at $S_{0}$ with radius $E$ , simultaneously for every $M \in M$ . Exact rational interval endpoint arithmetic and the valid $π$ interval [F5] make $I$ contain the normalized integral.

3.1F1F2F3F4step 2.1

For each fixed $M$ , put $p_{M} (z) = \det (z I - M)$ . The boundary is in the resolvent by [F1], so $p_{M}$ is nonzero on $Γ$ . By [F2] with $A = z I - M$ and direction $I$ , $p_{M}^{'} (z) / p_{M} (z) = tr (z I - M)^{- 1}$ . Facts [F3]–[F4] therefore identify $(2 π i)^{- 1} \int_{Γ} tr (z I - M)^{- 1} d z$ with the number of eigenvalues inside $P$ , counted with algebraic multiplicity; it is an integer from $0$ to $n$ .

4.1F5F6step 3.1∎

The successful output places the real part of every such integer strictly inside the half-unit interval around $c$ . There is only one integer in that interval, namely $c$ . Its imaginary part is zero and is contained by the checked imaginary interval. Hence every $M$ has exactly $c$ interior eigenvalues and none on the resolvent-certified boundary. If a monodromy matrix lies in $M$ , the same universal statement applies to it.

Depends on

Used by

Cited to discharge well-definedness by Finite complex-contour validation of Floquet multiplier clusters.

Dependency tree · two levels

93 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

J. Lebl, Guide to Cultivating Complex Analysis (standard reference, not scraped)
S. M. Rump, Verification methods: Rigorous results using floating-point arithmetic, Acta Numerica 19 (2010) (standard reference, not scraped)