proof(E1): CV_radius_exp_entry_coef_inf via bounded_of_lim_0 (Session 11, §24, Row-3 R1)

Land two lemmas discharging Row 3 Rung 1 of the E1 full-headline port
— the CV_radius sub-step that gates `is_derive_PSeries` applying to
every matrix entry of `exp_matrix t A` at every real `t`.

    Lemma bounded_of_lim_0 :
      forall u : nat -> R,
        is_lim_seq u 0 ->
        exists M : R, forall k : nat, Rabs (u k) <= M.

    Theorem CV_radius_exp_entry_coef_inf :
      forall (n : nat) (A : Mat n) (i j : Fin.t n),
        CV_radius (exp_entry_coef A i j) = p_infty.

bounded_of_lim_0.  Coquelicot 3.4.4 does not ship a name-matching
"convergent-implies-bounded" under Lim_seq / Series, so the ~25-line
textbook proof goes here.  Route through `is_lim_seq_spec` at
`mkposreal 1`, yielding a threshold `N` beyond which |u k| < 1; the
head is bounded by `sum_f_R0 (fun i => Rabs (u i)) N` (nonneg sum of
absolute values), yielding witness `M := 1 + Σ`.  Tail case closes
via Rminus_0_r + lra; head case closes by an inner induction showing
every term of a nonneg sequence is ≤ its partial sum.

CV_radius_exp_entry_coef_inf.  Uses the LUB characterisation from
`Coquelicot.PSeries.CV_radius_bounded`:

    is_lub_Rbar
      (fun r : R => exists M, forall k, Rabs (a k * r^k) <= M)
      (CV_radius a).

Strategy — show the underlying set is all of R, then a Finite LUB is
refuted at r := l + 1 (forces l + 1 <= l) and m_infty at r := 0
(Rbar_le (Finite 0) m_infty is False).  For every r we set

    c := INR n * Mbd * Rabs r   (Mbd from `matrix_bound_exists`)

and derive the per-term inequality

    Rabs (a k * r^k) <= / fact k * c^k

via `Apow_entry_abs_bound` (Session 4) + `Rpow_mult_distr`.  The
right-hand side is bounded uniformly in k because
`ex_series_exp_factorial c` (Session 5) gives the series is
ex_series, then `ex_series_lim_0` gives the terms tend to 0, then
`bounded_of_lim_0` gives a finite bound M'.  Rle_trans chains the
two.  Final Rbar case analysis on CV_radius closes the theorem.

Unlocks Row 3 Rung 2+ (vector trajectory ODE via entry-wise finSum
linearity of is_derive applied to is_derive_PSeries at each entry,
then inner-product chain rule for dV/dt).

Runner: 35/35 passing, exit 0, 0 regressed, 0 failing.
panic-attack assail E1_lyapunov_ndim.v: 0 weak points.
Banned-construct scan: clean (no believe_me / Admitted / sorry /
postulate / trustMe / unsafeCoerce / Obj.magic / assert_total).
MANIFEST unchanged (still points at E1_lyapunov_1d.v; §3.1 honest-
accounting — pointer only moves at Row-5 Qed).
LOC delta on E1_lyapunov_ndim.v: +196 (1988 → 2184).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

audits/canonical-proof-suite/REPORT.a2ml

@@ -6,7 +6,7 @@
   (metadata
     (project "007")
     (suite-spec-version "1.0")
-    (run-utc "2026-04-19T01:46:25Z")
+    (run-utc "2026-04-19T02:02:39Z")
     (host "fedora")
     (manifest "audits/canonical-proof-suite/MANIFEST.a2ml"))
   (summary
@@ -19,39 +19,39 @@
     (not-started 0)
     (prover-missing 0))
   (entries
-    (entry (id "M1") (status "passing") (elapsed-ms 2721) (prover "idris2") (kernel-version "Idris 2, version 0.8.0-712523a89") (proof-file "proofs/canonical-proof-suite/M1InfinitudeOfPrimes.idr") (semantic-check "verified"))
-    (entry (id "M2") (status "passing") (elapsed-ms 1281) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M2_lagrange.v") (semantic-check "verified"))
-    (entry (id "M3") (status "passing") (elapsed-ms 950) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M3_ivt.v") (semantic-check "verified"))
-    (entry (id "M4") (status "passing") (elapsed-ms 993) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M4_compactness_unit_interval.v") (semantic-check "verified"))
-    (entry (id "M5") (status "passing") (elapsed-ms 422) (prover "agda") (kernel-version "Agda version 2.8.0") (proof-file "proofs/canonical-proof-suite/M5-yoneda.agda") (semantic-check "verified"))
-    (entry (id "S1") (status "passing") (elapsed-ms 153) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S1_noether_energy.v") (semantic-check "verified"))
-    (entry (id "S2") (status "passing") (elapsed-ms 165) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S2_gauss_law.v") (semantic-check "verified"))
-    (entry (id "S3") (status "passing") (elapsed-ms 770) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S3_h_theorem_binary.v") (semantic-check "verified"))
-    (entry (id "S4") (status "passing") (elapsed-ms 886) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S4_heisenberg_discrete.v") (semantic-check "verified"))
-    (entry (id "S5") (status "passing") (elapsed-ms 944) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S5_shannon_source_coding.v") (semantic-check "verified"))
-    (entry (id "E1") (status "passing") (elapsed-ms 926) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E1_lyapunov_1d.v") (semantic-check "verified"))
-    (entry (id "E2") (status "passing") (elapsed-ms 2875) (prover "idris2") (kernel-version "Idris 2, version 0.8.0-712523a89") (proof-file "proofs/canonical-proof-suite/E2-adder-equivalence.idr") (semantic-check "verified"))
-    (entry (id "E3") (status "passing") (elapsed-ms 153) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E3_cantilever_deflection.v") (semantic-check "verified"))
-    (entry (id "E4") (status "passing") (elapsed-ms 3039) (prover "idris2") (kernel-version "Idris 2, version 0.8.0-712523a89") (proof-file "proofs/canonical-proof-suite/E4-mergesort.idr") (semantic-check "verified"))
-    (entry (id "E5") (status "passing") (elapsed-ms 138) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E5_auth_key_binding.v") (semantic-check "verified"))
-    (entry (id "M6") (status "passing") (elapsed-ms 132) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M6_deduction_theorem.v") (semantic-check "verified"))
-    (entry (id "S6") (status "passing") (elapsed-ms 158) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S6_mass_action.v") (semantic-check "verified"))
-    (entry (id "E6") (status "passing") (elapsed-ms 168) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E6_cstr_mass_balance.v") (semantic-check "verified"))
-    (entry (id "M7") (status "passing") (elapsed-ms 136) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M7_linearity_of_expectation.v") (semantic-check "verified"))
-    (entry (id "M8") (status "passing") (elapsed-ms 574) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M8_rank_nullity.v") (semantic-check "verified"))
-    (entry (id "M9") (status "passing") (elapsed-ms 301) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M9_unique_factorization.v") (semantic-check "verified"))
-    (entry (id "M10") (status "passing") (elapsed-ms 129) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M10_knot_composition_monoid.v") (semantic-check "verified"))
-    (entry (id "M11") (status "passing") (elapsed-ms 555) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M11_pigeonhole.v") (semantic-check "verified"))
-    (entry (id "E7") (status "passing") (elapsed-ms 125) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E7_carnot_efficiency.v") (semantic-check "verified"))
-    (entry (id "S7") (status "passing") (elapsed-ms 125) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S7_lorentz_velocity_addition.v") (semantic-check "verified"))
-    (entry (id "E8") (status "passing") (elapsed-ms 127) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E8_nyquist_shannon.v") (semantic-check "verified"))
-    (entry (id "M12") (status "passing") (elapsed-ms 142) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M12_dominated_convergence.v") (semantic-check "verified"))
-    (entry (id "S8") (status "passing") (elapsed-ms 176) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S8_hardy_weinberg.v") (semantic-check "verified"))
-    (entry (id "E9") (status "passing") (elapsed-ms 144) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E9_newton_convergence.v") (semantic-check "verified"))
-    (entry (id "M13") (status "passing") (elapsed-ms 158) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M13_hahn_banach.v") (semantic-check "verified"))
-    (entry (id "M14") (status "passing") (elapsed-ms 143) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M14_max_flow_min_cut.v") (semantic-check "verified"))
-    (entry (id "S9") (status "passing") (elapsed-ms 125) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S9_chandrasekhar.v") (semantic-check "verified"))
-    (entry (id "S10") (status "passing") (elapsed-ms 133) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S10_r_naught_threshold.v") (semantic-check "verified"))
-    (entry (id "E10") (status "passing") (elapsed-ms 139) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E10_bathtub_reliability.v") (semantic-check "verified"))
-    (entry (id "E11") (status "passing") (elapsed-ms 153) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E11_kirchhoff.v") (semantic-check "verified"))
+    (entry (id "M1") (status "passing") (elapsed-ms 2393) (prover "idris2") (kernel-version "Idris 2, version 0.8.0-712523a89") (proof-file "proofs/canonical-proof-suite/M1InfinitudeOfPrimes.idr") (semantic-check "verified"))
+    (entry (id "M2") (status "passing") (elapsed-ms 1075) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M2_lagrange.v") (semantic-check "verified"))
+    (entry (id "M3") (status "passing") (elapsed-ms 751) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M3_ivt.v") (semantic-check "verified"))
+    (entry (id "M4") (status "passing") (elapsed-ms 778) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M4_compactness_unit_interval.v") (semantic-check "verified"))
+    (entry (id "M5") (status "passing") (elapsed-ms 332) (prover "agda") (kernel-version "Agda version 2.8.0") (proof-file "proofs/canonical-proof-suite/M5-yoneda.agda") (semantic-check "verified"))
+    (entry (id "S1") (status "passing") (elapsed-ms 150) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S1_noether_energy.v") (semantic-check "verified"))
+    (entry (id "S2") (status "passing") (elapsed-ms 136) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S2_gauss_law.v") (semantic-check "verified"))
+    (entry (id "S3") (status "passing") (elapsed-ms 714) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S3_h_theorem_binary.v") (semantic-check "verified"))
+    (entry (id "S4") (status "passing") (elapsed-ms 674) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S4_heisenberg_discrete.v") (semantic-check "verified"))
+    (entry (id "S5") (status "passing") (elapsed-ms 715) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S5_shannon_source_coding.v") (semantic-check "verified"))
+    (entry (id "E1") (status "passing") (elapsed-ms 746) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E1_lyapunov_1d.v") (semantic-check "verified"))
+    (entry (id "E2") (status "passing") (elapsed-ms 2330) (prover "idris2") (kernel-version "Idris 2, version 0.8.0-712523a89") (proof-file "proofs/canonical-proof-suite/E2-adder-equivalence.idr") (semantic-check "verified"))
+    (entry (id "E3") (status "passing") (elapsed-ms 137) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E3_cantilever_deflection.v") (semantic-check "verified"))
+    (entry (id "E4") (status "passing") (elapsed-ms 2367) (prover "idris2") (kernel-version "Idris 2, version 0.8.0-712523a89") (proof-file "proofs/canonical-proof-suite/E4-mergesort.idr") (semantic-check "verified"))
+    (entry (id "E5") (status "passing") (elapsed-ms 108) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E5_auth_key_binding.v") (semantic-check "verified"))
+    (entry (id "M6") (status "passing") (elapsed-ms 117) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M6_deduction_theorem.v") (semantic-check "verified"))
+    (entry (id "S6") (status "passing") (elapsed-ms 117) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S6_mass_action.v") (semantic-check "verified"))
+    (entry (id "E6") (status "passing") (elapsed-ms 135) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E6_cstr_mass_balance.v") (semantic-check "verified"))
+    (entry (id "M7") (status "passing") (elapsed-ms 117) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M7_linearity_of_expectation.v") (semantic-check "verified"))
+    (entry (id "M8") (status "passing") (elapsed-ms 484) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M8_rank_nullity.v") (semantic-check "verified"))
+    (entry (id "M9") (status "passing") (elapsed-ms 297) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M9_unique_factorization.v") (semantic-check "verified"))
+    (entry (id "M10") (status "passing") (elapsed-ms 122) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M10_knot_composition_monoid.v") (semantic-check "verified"))
+    (entry (id "M11") (status "passing") (elapsed-ms 507) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M11_pigeonhole.v") (semantic-check "verified"))
+    (entry (id "E7") (status "passing") (elapsed-ms 108) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E7_carnot_efficiency.v") (semantic-check "verified"))
+    (entry (id "S7") (status "passing") (elapsed-ms 116) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S7_lorentz_velocity_addition.v") (semantic-check "verified"))
+    (entry (id "E8") (status "passing") (elapsed-ms 111) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E8_nyquist_shannon.v") (semantic-check "verified"))
+    (entry (id "M12") (status "passing") (elapsed-ms 110) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M12_dominated_convergence.v") (semantic-check "verified"))
+    (entry (id "S8") (status "passing") (elapsed-ms 126) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S8_hardy_weinberg.v") (semantic-check "verified"))
+    (entry (id "E9") (status "passing") (elapsed-ms 112) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E9_newton_convergence.v") (semantic-check "verified"))
+    (entry (id "M13") (status "passing") (elapsed-ms 118) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M13_hahn_banach.v") (semantic-check "verified"))
+    (entry (id "M14") (status "passing") (elapsed-ms 121) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M14_max_flow_min_cut.v") (semantic-check "verified"))
+    (entry (id "S9") (status "passing") (elapsed-ms 109) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S9_chandrasekhar.v") (semantic-check "verified"))
+    (entry (id "S10") (status "passing") (elapsed-ms 109) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S10_r_naught_threshold.v") (semantic-check "verified"))
+    (entry (id "E10") (status "passing") (elapsed-ms 110) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E10_bathtub_reliability.v") (semantic-check "verified"))
+    (entry (id "E11") (status "passing") (elapsed-ms 121) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E11_kirchhoff.v") (semantic-check "verified"))
   ))