proof(E1): exp_matrix_add Row-2 Qed (Session 9, §21-§22)

Land Row-2 of the E1 full-headline port: the matrix-exponential
semigroup identity

    exp_matrix (s + t) A = Mmul (exp_matrix s A) (exp_matrix t A)

is now Qed-closed.  Two new sections.

§21 Session 9a — three pure-algebra helpers (no new analytic content,
just Series_plus / ex_series_plus iterated over finSum indices, plus
a finite-finite swap):

  - ex_series_finSum       : finSum of term-wise ex_series families
                             is itself ex_series (induction on n via
                             ex_series_plus + ex_series_zero_fn base).
  - finSum_Series_commute  : finSum and Series commute when every
                             fibre converges (induction + Series_plus).
  - finSum_sum_f_R0_swap   : two finite sums commute freely (induction
                             on the sum_f_R0 index + finSum_add-reversed).

§22 Session 9b — the Row-2 Qed.  Proof chain, each step a rewrite
against a lemma already in the file:

  (i)   Unfold RHS entry-level Mmul into finSum n (fun l => ... l ...).
  (ii)  Rewrite each fibre via Session 8 exp_mult_per_l_cauchy
        (fibre product = Series of per-k Cauchy convolution).
  (iii) Commute finSum n with outer Series via Session 9a
        finSum_Series_commute, discharging ex_series at each l from
        exp_mult_per_l_is_series.
  (iv)  Reduce to pointwise term equality via Series_ext.
  (v)   Swap inner sum_f_R0 and outer-now-inner finSum n via
        Session 9a finSum_sum_f_R0_swap.
  (vi)  At fixed p ≤ k: pull scalar s^p/p! · t^(k-p)/(k-p)! out of
        the inner finSum (finSum_ext + finSum_scale); identify the
        residual finSum as (Mmul (Apow p A) (Apow (k-p) A)) i j by
        Mmul-defn; rewrite to Apow (p + (k-p)) A i j via Session 6
        Apow_add reversed; collapse p + (k-p) = k using lia on
        Hp : p <= k handed in by sum_eq.
  (vii) Pull Apow k A i j out of the outer sum via
        PartSum.scal_sum reversed.
  (viii)Collapse the remaining scalar sum via Session 7
        exp_term_convolution_eq:
          sum_f_R0 (fun p => s^p/p! · t^(k-p)/(k-p)!) k
          = (s + t)^k / k!.
  (ix)  Close with Rmult commutativity (lra).

Added `Lia` to the import list alongside `Lra` — lia is the discrete
counterpart needed for the p + (k-p) = k step on nat.

Row-2 status after this commit:
  ✅ Row 1 (absolute convergence of exp_entry) — Session 5.
  ✅ Row 2 (matrix-exp semigroup identity)      — this commit.
  ⬜ Row 3 (chain rule for V along trajectory via Coquelicot.Derive).
  ⬜ Row 4 (dV/dt identity: dV/dt = x^T (A^T P + P A) x).
  ⬜ Row 5 (final lyapunov_stability_ndim Qed via MVT_gen).
  ⬜ MANIFEST repoint from E1_lyapunov_1d.v to this file.

Runner: bash scripts/canonical-proof-suite-runner.sh → 35/35 passing,
0 regressed, exit 0.  MANIFEST still at re-scope per §3.1 honest-
accounting; pointer moves only at Row 5 Qed.

panic-attack assail proofs/canonical-proof-suite/E1_lyapunov_ndim.v
→ 0 weak points, 0 banned constructs, exit 0.

LOC delta: +222 (1717 → 1939).  No banned tokens anywhere in the
addition.

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:32:24Z")
+    (run-utc "2026-04-19T01:39:09Z")
     (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 2599) (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 1183) (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 811) (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 784) (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 310) (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 152) (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 177) (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 749) (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 724) (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 790) (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 785) (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 2391) (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 146) (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 2333) (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 116) (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 115) (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 132) (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 116) (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 526) (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 283) (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 125) (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 514) (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 121) (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 112) (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 110) (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 114) (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 136) (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 120) (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 122) (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 120) (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 118) (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 117) (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 112) (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 114) (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 2389) (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 1093) (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 744) (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 749) (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 283) (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 147) (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 154) (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 694) (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 706) (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 729) (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 749) (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 2300) (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 136) (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 2322) (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 119) (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 118) (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 128) (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 122) (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 508) (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 279) (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 120) (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 498) (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 118) (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 110) (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 114) (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 116) (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 131) (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 110) (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 119) (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 105) (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 104) (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 100) (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 109) (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 112) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E11_kirchhoff.v") (semantic-check "verified"))
   ))