proof(S3): Rung-2 continuous entropy bound (Session 4) + sidecar refresh

hyperpolymath · claude · hyperpolymath · commit 37713fb18ad9 · 2026-04-27T19:34:54.000+01:00
- Add §8 to S3_h_theorem_ndim.v — 193 LOC of new Coquelicot 3.4.4
  Riemann-integration proof
- Proved: continuous_entropy_le_ln_bma — for any strictly-positive
  probability density f on [a,b] with ∫f = 1, the continuous
  Shannon entropy H_cont[f] = -∫f·ln(f) satisfies
  H_cont[f] &lt;= ln(b-a).
- Route: ln u ≤ u-1 pointwise → f(x)·(−ln(b-a)−ln f(x)) ≤ 1/(b-a)−f(x)
  → RInt_le → RInt_plus/scal/const linearity + normalisation → lra.
- Zero Admitted, zero sorry, zero banned constructs; all declarations
  inside ContinuousEntropySection (discharged at End).
- Suite: 35/35 passing after sidecar re-run.
- Rung-3 (Lebesgue, coq-mathcomp-analysis) and Rung-4 (Boltzmann
  collision operator) remain for future sessions.

Co-Authored-By: Claude Sonnet 4.6 &lt;noreply@anthropic.com&gt;
diff --git a/proofs/canonical-proof-suite/E1.sidecar.a2ml b/proofs/canonical-proof-suite/E1.sidecar.a2ml
@@ -11,6 +11,6 @@
   (expected-symbol "lyapunov_stability_ndim")
   (semantic-check "verified")
   (status "passing")
-  (elapsed-ms 2897)
+  (elapsed-ms 3863)
   (banned-constructs-found "")
-  (last-checked-utc "2026-04-27T17:37:57Z"))
+  (last-checked-utc "2026-04-27T18:34:18Z"))
diff --git a/proofs/canonical-proof-suite/E10.sidecar.a2ml b/proofs/canonical-proof-suite/E10.sidecar.a2ml
@@ -11,6 +11,6 @@
   (expected-symbol "weibull_bathtub_bound")
   (semantic-check "verified")
   (status "passing")
-  (elapsed-ms 148)
+  (elapsed-ms 144)
   (banned-constructs-found "")
-  (last-checked-utc "2026-04-27T17:38:14Z"))
+  (last-checked-utc "2026-04-27T18:34:38Z"))
diff --git a/proofs/canonical-proof-suite/E11.sidecar.a2ml b/proofs/canonical-proof-suite/E11.sidecar.a2ml
@@ -11,6 +11,6 @@
   (expected-symbol "kirchhoff_laws")
   (semantic-check "verified")
   (status "passing")
-  (elapsed-ms 163)
+  (elapsed-ms 165)
   (banned-constructs-found "")
-  (last-checked-utc "2026-04-27T17:38:14Z"))
+  (last-checked-utc "2026-04-27T18:34:38Z"))
diff --git a/proofs/canonical-proof-suite/E2.sidecar.a2ml b/proofs/canonical-proof-suite/E2.sidecar.a2ml
@@ -11,6 +11,6 @@
   (expected-symbol "adderEquivalence")
   (semantic-check "verified")
   (status "passing")
-  (elapsed-ms 2973)
+  (elapsed-ms 3465)
   (banned-constructs-found "")
-  (last-checked-utc "2026-04-27T17:38:02Z"))
+  (last-checked-utc "2026-04-27T18:34:24Z"))
diff --git a/proofs/canonical-proof-suite/E3.sidecar.a2ml b/proofs/canonical-proof-suite/E3.sidecar.a2ml
@@ -11,6 +11,6 @@
   (expected-symbol "cantilever_deflection_bound")
   (semantic-check "verified")
   (status "passing")
-  (elapsed-ms 161)
+  (elapsed-ms 180)
   (banned-constructs-found "")
-  (last-checked-utc "2026-04-27T17:38:03Z"))
+  (last-checked-utc "2026-04-27T18:34:25Z"))
diff --git a/proofs/canonical-proof-suite/E4.sidecar.a2ml b/proofs/canonical-proof-suite/E4.sidecar.a2ml
@@ -11,6 +11,6 @@
   (expected-symbol "mergeSortCorrect")
   (semantic-check "verified")
   (status "passing")
-  (elapsed-ms 2873)
+  (elapsed-ms 3528)
   (banned-constructs-found "")
-  (last-checked-utc "2026-04-27T17:38:08Z"))
+  (last-checked-utc "2026-04-27T18:34:31Z"))
diff --git a/proofs/canonical-proof-suite/E5.sidecar.a2ml b/proofs/canonical-proof-suite/E5.sidecar.a2ml
@@ -11,6 +11,6 @@
   (expected-symbol "needham_schroeder_fixed")
   (semantic-check "verified")
   (status "passing")
-  (elapsed-ms 125)
+  (elapsed-ms 170)
   (banned-constructs-found "")
-  (last-checked-utc "2026-04-27T17:38:08Z"))
+  (last-checked-utc "2026-04-27T18:34:31Z"))
diff --git a/proofs/canonical-proof-suite/E6.sidecar.a2ml b/proofs/canonical-proof-suite/E6.sidecar.a2ml
@@ -11,6 +11,6 @@
   (expected-symbol "cstr_steady_state_closure")
   (semantic-check "verified")
   (status "passing")
-  (elapsed-ms 145)
+  (elapsed-ms 253)
   (banned-constructs-found "")
-  (last-checked-utc "2026-04-27T17:38:09Z"))
+  (last-checked-utc "2026-04-27T18:34:32Z"))
diff --git a/proofs/canonical-proof-suite/E7.sidecar.a2ml b/proofs/canonical-proof-suite/E7.sidecar.a2ml
@@ -11,6 +11,6 @@
   (expected-symbol "carnot_efficiency_bound")
   (semantic-check "verified")
   (status "passing")
-  (elapsed-ms 160)
+  (elapsed-ms 145)
   (banned-constructs-found "")
-  (last-checked-utc "2026-04-27T17:38:11Z"))
+  (last-checked-utc "2026-04-27T18:34:35Z"))
diff --git a/proofs/canonical-proof-suite/E8.sidecar.a2ml b/proofs/canonical-proof-suite/E8.sidecar.a2ml
@@ -11,6 +11,6 @@
   (expected-symbol "nyquist_shannon_sufficient_rate")
   (semantic-check "verified")
   (status "passing")
-  (elapsed-ms 193)
+  (elapsed-ms 171)
   (banned-constructs-found "")
-  (last-checked-utc "2026-04-27T17:38:12Z"))
+  (last-checked-utc "2026-04-27T18:34:35Z"))
diff --git a/proofs/canonical-proof-suite/E9.sidecar.a2ml b/proofs/canonical-proof-suite/E9.sidecar.a2ml
@@ -11,6 +11,6 @@
   (expected-symbol "newton_quadratic_convergence")
   (semantic-check "verified")
   (status "passing")
-  (elapsed-ms 133)
+  (elapsed-ms 194)
   (banned-constructs-found "")
-  (last-checked-utc "2026-04-27T17:38:13Z"))
+  (last-checked-utc "2026-04-27T18:34:36Z"))
diff --git a/proofs/canonical-proof-suite/M1.sidecar.a2ml b/proofs/canonical-proof-suite/M1.sidecar.a2ml
@@ -11,6 +11,6 @@
   (expected-symbol "infinitudeOfPrimes")
   (semantic-check "verified")
   (status "passing")
-  (elapsed-ms 3188)
+  (elapsed-ms 8482)
   (banned-constructs-found "")
-  (last-checked-utc "2026-04-27T17:37:47Z"))
+  (last-checked-utc "2026-04-27T18:33:55Z"))
diff --git a/proofs/canonical-proof-suite/M10.sidecar.a2ml b/proofs/canonical-proof-suite/M10.sidecar.a2ml
@@ -11,6 +11,6 @@
   (expected-symbol "knot_composition_monoid")
   (semantic-check "verified")
   (status "passing")
-  (elapsed-ms 164)
+  (elapsed-ms 187)
   (banned-constructs-found "")
-  (last-checked-utc "2026-04-27T17:38:10Z"))
+  (last-checked-utc "2026-04-27T18:34:34Z"))
diff --git a/proofs/canonical-proof-suite/M11.sidecar.a2ml b/proofs/canonical-proof-suite/M11.sidecar.a2ml
@@ -11,6 +11,6 @@
   (expected-symbol "pigeonhole_principle")
   (semantic-check "verified")
   (status "passing")
-  (elapsed-ms 609)
+  (elapsed-ms 691)
   (banned-constructs-found "")
-  (last-checked-utc "2026-04-27T17:38:11Z"))
+  (last-checked-utc "2026-04-27T18:34:35Z"))
diff --git a/proofs/canonical-proof-suite/M12.sidecar.a2ml b/proofs/canonical-proof-suite/M12.sidecar.a2ml
@@ -11,6 +11,6 @@
   (expected-symbol "dominated_convergence")
   (semantic-check "verified")
   (status "passing")
-  (elapsed-ms 145)
+  (elapsed-ms 205)
   (banned-constructs-found "")
-  (last-checked-utc "2026-04-27T17:38:12Z"))
+  (last-checked-utc "2026-04-27T18:34:36Z"))
diff --git a/proofs/canonical-proof-suite/M13.sidecar.a2ml b/proofs/canonical-proof-suite/M13.sidecar.a2ml
@@ -11,6 +11,6 @@
   (expected-symbol "hahn_banach_extension")
   (semantic-check "verified")
   (status "passing")
-  (elapsed-ms 148)
+  (elapsed-ms 209)
   (banned-constructs-found "")
-  (last-checked-utc "2026-04-27T17:38:13Z"))
+  (last-checked-utc "2026-04-27T18:34:37Z"))
diff --git a/proofs/canonical-proof-suite/M14.sidecar.a2ml b/proofs/canonical-proof-suite/M14.sidecar.a2ml
@@ -11,6 +11,6 @@
   (expected-symbol "max_flow_min_cut")
   (semantic-check "verified")
   (status "passing")
-  (elapsed-ms 127)
+  (elapsed-ms 174)
   (banned-constructs-found "")
-  (last-checked-utc "2026-04-27T17:38:13Z"))
+  (last-checked-utc "2026-04-27T18:34:37Z"))
diff --git a/proofs/canonical-proof-suite/M2.sidecar.a2ml b/proofs/canonical-proof-suite/M2.sidecar.a2ml
@@ -11,6 +11,6 @@
   (expected-symbol "lagrangeTheorem")
   (semantic-check "verified")
   (status "passing")
-  (elapsed-ms 1355)
+  (elapsed-ms 6143)
   (banned-constructs-found "")
-  (last-checked-utc "2026-04-27T17:37:48Z"))
+  (last-checked-utc "2026-04-27T18:34:02Z"))
diff --git a/proofs/canonical-proof-suite/M3.sidecar.a2ml b/proofs/canonical-proof-suite/M3.sidecar.a2ml
@@ -11,6 +11,6 @@
   (expected-symbol "intermediate_value_theorem")
   (semantic-check "verified")
   (status "passing")
-  (elapsed-ms 911)
+  (elapsed-ms 2148)
   (banned-constructs-found "")
-  (last-checked-utc "2026-04-27T17:37:49Z"))
+  (last-checked-utc "2026-04-27T18:34:04Z"))
diff --git a/proofs/canonical-proof-suite/M4.sidecar.a2ml b/proofs/canonical-proof-suite/M4.sidecar.a2ml
@@ -11,6 +11,6 @@
   (expected-symbol "unit_interval_compact")
   (semantic-check "verified")
   (status "passing")
-  (elapsed-ms 999)
+  (elapsed-ms 2877)
   (banned-constructs-found "")
-  (last-checked-utc "2026-04-27T17:37:50Z"))
+  (last-checked-utc "2026-04-27T18:34:07Z"))
diff --git a/proofs/canonical-proof-suite/M5.sidecar.a2ml b/proofs/canonical-proof-suite/M5.sidecar.a2ml
@@ -11,6 +11,6 @@
   (expected-symbol "yoneda")
   (semantic-check "verified")
   (status "passing")
-  (elapsed-ms 366)
+  (elapsed-ms 1190)
   (banned-constructs-found "")
-  (last-checked-utc "2026-04-27T17:37:50Z"))
+  (last-checked-utc "2026-04-27T18:34:08Z"))
diff --git a/proofs/canonical-proof-suite/M6.sidecar.a2ml b/proofs/canonical-proof-suite/M6.sidecar.a2ml
@@ -11,6 +11,6 @@
   (expected-symbol "deduction_theorem")
   (semantic-check "verified")
   (status "passing")
-  (elapsed-ms 141)
+  (elapsed-ms 172)
   (banned-constructs-found "")
-  (last-checked-utc "2026-04-27T17:38:08Z"))
+  (last-checked-utc "2026-04-27T18:34:31Z"))
diff --git a/proofs/canonical-proof-suite/M7.sidecar.a2ml b/proofs/canonical-proof-suite/M7.sidecar.a2ml
@@ -11,6 +11,6 @@
   (expected-symbol "linearity_of_expectation")
   (semantic-check "verified")
   (status "passing")
-  (elapsed-ms 150)
+  (elapsed-ms 212)
   (banned-constructs-found "")
-  (last-checked-utc "2026-04-27T17:38:09Z"))
+  (last-checked-utc "2026-04-27T18:34:33Z"))
diff --git a/proofs/canonical-proof-suite/M8.sidecar.a2ml b/proofs/canonical-proof-suite/M8.sidecar.a2ml
@@ -11,6 +11,6 @@
   (expected-symbol "rank_nullity_theorem")
   (semantic-check "verified")
   (status "passing")
-  (elapsed-ms 723)
+  (elapsed-ms 698)
   (banned-constructs-found "")
-  (last-checked-utc "2026-04-27T17:38:10Z"))
+  (last-checked-utc "2026-04-27T18:34:33Z"))
diff --git a/proofs/canonical-proof-suite/M9.sidecar.a2ml b/proofs/canonical-proof-suite/M9.sidecar.a2ml
@@ -11,6 +11,6 @@
   (expected-symbol "unique_factorization")
   (semantic-check "verified")
   (status "passing")
-  (elapsed-ms 430)
+  (elapsed-ms 425)
   (banned-constructs-found "")
-  (last-checked-utc "2026-04-27T17:38:10Z"))
+  (last-checked-utc "2026-04-27T18:34:34Z"))
diff --git a/proofs/canonical-proof-suite/S1.sidecar.a2ml b/proofs/canonical-proof-suite/S1.sidecar.a2ml
@@ -11,6 +11,6 @@
   (expected-symbol "noether_energy_conservation")
   (semantic-check "verified")
   (status "passing")
-  (elapsed-ms 160)
+  (elapsed-ms 385)
   (banned-constructs-found "")
-  (last-checked-utc "2026-04-27T17:37:51Z"))
+  (last-checked-utc "2026-04-27T18:34:09Z"))
diff --git a/proofs/canonical-proof-suite/S10.sidecar.a2ml b/proofs/canonical-proof-suite/S10.sidecar.a2ml
@@ -11,6 +11,6 @@
   (expected-symbol "r_naught_threshold")
   (semantic-check "verified")
   (status "passing")
-  (elapsed-ms 140)
+  (elapsed-ms 172)
   (banned-constructs-found "")
-  (last-checked-utc "2026-04-27T17:38:13Z"))
+  (last-checked-utc "2026-04-27T18:34:37Z"))
diff --git a/proofs/canonical-proof-suite/S2.sidecar.a2ml b/proofs/canonical-proof-suite/S2.sidecar.a2ml
@@ -11,6 +11,6 @@
   (expected-symbol "gauss_law")
   (semantic-check "verified")
   (status "passing")
-  (elapsed-ms 165)
+  (elapsed-ms 414)
   (banned-constructs-found "")
-  (last-checked-utc "2026-04-27T17:37:51Z"))
+  (last-checked-utc "2026-04-27T18:34:09Z"))
diff --git a/proofs/canonical-proof-suite/S3.sidecar.a2ml b/proofs/canonical-proof-suite/S3.sidecar.a2ml
@@ -11,6 +11,6 @@
   (expected-symbol "boltzmann_h_theorem")
   (semantic-check "verified")
   (status "passing")
-  (elapsed-ms 901)
+  (elapsed-ms 1637)
   (banned-constructs-found "")
-  (last-checked-utc "2026-04-27T17:37:52Z"))
+  (last-checked-utc "2026-04-27T18:34:11Z"))
diff --git a/proofs/canonical-proof-suite/S3_h_theorem_ndim.v b/proofs/canonical-proof-suite/S3_h_theorem_ndim.v
diff --git a/proofs/canonical-proof-suite/S4.sidecar.a2ml b/proofs/canonical-proof-suite/S4.sidecar.a2ml
diff --git a/proofs/canonical-proof-suite/S5.sidecar.a2ml b/proofs/canonical-proof-suite/S5.sidecar.a2ml
diff --git a/proofs/canonical-proof-suite/S6.sidecar.a2ml b/proofs/canonical-proof-suite/S6.sidecar.a2ml
diff --git a/proofs/canonical-proof-suite/S7.sidecar.a2ml b/proofs/canonical-proof-suite/S7.sidecar.a2ml
diff --git a/proofs/canonical-proof-suite/S8.sidecar.a2ml b/proofs/canonical-proof-suite/S8.sidecar.a2ml
diff --git a/proofs/canonical-proof-suite/S9.sidecar.a2ml b/proofs/canonical-proof-suite/S9.sidecar.a2ml
