proof(E1): scalar binomial in divided form (Session 7, §19)

Add `exp_term_convolution_eq` at §19 of `E1_lyapunov_ndim.v`:

    Σ_{i=0}^{k} (s^i / i!) · (t^(k-i) / (k-i)!)  =  (s + t)^k / k!.

Pure scalar real-analysis — no matrix, no Coquelicot. Derived from
Stdlib.Reals.Binomial.binomial by dividing through by INR (fact k)
and per-term field algebra once C k i = fact k / (fact i * fact (k-i))
is unfolded. Dependencies are Stdlib-only:
  - Binomial.binomial   : (x + y)^n = Σ C n i · x^i · y^(n-i)
  - PartSum.scal_sum    : x · Σ f = Σ (f · x)
  - PartSum.sum_eq      : pointwise-equal terms give equal sums
  - Arith.INR_fact_neq_0: factorial is nonzero as a real
No new imports needed — `Reals` already re-exports SeqSeries ⇒
Binomial + PartSum.

This is the arithmetic kernel of the Row-2 semigroup identity
    exp_matrix (s + t) A = Mmul (exp_matrix s A) (exp_matrix t A).
Session 8 will lift it entry-wise via Coquelicot.Series.is_series_mult
(Cauchy product under absolute convergence established in Session 5)
and fold paired matrix powers (Apow p A) · (Apow q A) under p+q=k into
a single Apow index using Session 6's Apow_add, collapsing the entry-
level Cauchy convolution to a one-line rewrite.

Runner: bash scripts/canonical-proof-suite-runner.sh → 35/35 passing,
0 regressed, exit 0. Suite totals unchanged (MANIFEST continues to
point at E1_lyapunov_1d.v per §3.1 honest-accounting; pointer only
moves once `lyapunov_stability_ndim` is Qed-closed here).

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

LOC delta: +59 (1513 → 1572). No banned tokens anywhere in the
addition (no believe_me / Admitted / sorry / postulate / axiom /
unsafeCoerce / Obj.magic / trustMe / assert_total).

Row-2 remaining after this: (a) entry-level Cauchy-product bridge
using is_series_mult + Apow_add + exp_term_convolution_eq; (b) final
Row-2 Qed `exp_matrix_add`. Session 8 target.

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-19T00:41:49Z")
+    (run-utc "2026-04-19T01:22:50Z")
     (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 2500) (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 1106) (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 831) (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 731) (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 290) (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 143) (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 726) (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 698) (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 746) (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 758) (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 2443) (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 138) (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 2452) (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 126) (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 113) (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 125) (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 510) (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 284) (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 130) (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 126) (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 113) (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 109) (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 121) (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 "M1") (status "passing") (elapsed-ms 2659) (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 1243) (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 843) (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 820) (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 352) (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 162) (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 158) (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 857) (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 788) (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 837) (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 2490) (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 2623) (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 137) (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 141) (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 123) (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 144) (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 123) (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 535) (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 292) (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 126) (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 538) (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 120) (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 118) (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 116) (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 126) (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 140) (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 124) (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 129) (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 "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 133) (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 116) (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 121) (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 118) (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 114) (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 "S9") (status "passing") (elapsed-ms 122) (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 126) (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 108) (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 116) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E11_kirchhoff.v") (semantic-check "verified"))
   ))