Skip to content

Commit fb70aba

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
chore(audits): re-run canonical proof suite after S3 ndim Rung-2 fix
All 35 entries still passing; elapsed-ms and run-utc updated to reflect the post-fix verification run at 2026-04-27T18:34:38Z. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
1 parent f3690ef commit fb70aba

2 files changed

Lines changed: 72 additions & 72 deletions

File tree

‎audits/canonical-proof-suite/REPORT.a2ml‎

Lines changed: 36 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@
66
(metadata
77
(project "007")
88
(suite-spec-version "1.0")
9-
(run-utc "2026-04-27T17:38:14Z")
9+
(run-utc "2026-04-27T18:34:38Z")
1010
(host "fedora")
1111
(manifest "audits/canonical-proof-suite/MANIFEST.a2ml"))
1212
(summary
@@ -19,39 +19,39 @@
1919
(not-started 0)
2020
(prover-missing 0))
2121
(entries
22-
(entry (id "M1") (status "passing") (elapsed-ms 3188) (prover "idris2") (kernel-version "Idris 2, version 0.8.0-712523a89") (proof-file "proofs/canonical-proof-suite/M1InfinitudeOfPrimes.idr") (semantic-check "verified"))
23-
(entry (id "M2") (status "passing") (elapsed-ms 1355) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M2_lagrange.v") (semantic-check "verified"))
24-
(entry (id "M3") (status "passing") (elapsed-ms 911) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M3_ivt.v") (semantic-check "verified"))
25-
(entry (id "M4") (status "passing") (elapsed-ms 999) (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"))
26-
(entry (id "M5") (status "passing") (elapsed-ms 366) (prover "agda") (kernel-version "Agda version 2.8.0") (proof-file "proofs/canonical-proof-suite/M5-yoneda.agda") (semantic-check "verified"))
27-
(entry (id "S1") (status "passing") (elapsed-ms 160) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S1_noether_energy.v") (semantic-check "verified"))
28-
(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"))
29-
(entry (id "S3") (status "passing") (elapsed-ms 901) (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"))
30-
(entry (id "S4") (status "passing") (elapsed-ms 807) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S4_heisenberg_discrete.v") (semantic-check "verified"))
31-
(entry (id "S5") (status "passing") (elapsed-ms 880) (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"))
32-
(entry (id "E1") (status "passing") (elapsed-ms 2897) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E1_lyapunov_ndim.v") (semantic-check "verified"))
33-
(entry (id "E2") (status "passing") (elapsed-ms 2973) (prover "idris2") (kernel-version "Idris 2, version 0.8.0-712523a89") (proof-file "proofs/canonical-proof-suite/E2-adder-equivalence.idr") (semantic-check "verified"))
34-
(entry (id "E3") (status "passing") (elapsed-ms 161) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E3_cantilever_deflection.v") (semantic-check "verified"))
35-
(entry (id "E4") (status "passing") (elapsed-ms 2873) (prover "idris2") (kernel-version "Idris 2, version 0.8.0-712523a89") (proof-file "proofs/canonical-proof-suite/E4-mergesort.idr") (semantic-check "verified"))
36-
(entry (id "E5") (status "passing") (elapsed-ms 125) (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"))
37-
(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"))
38-
(entry (id "S6") (status "passing") (elapsed-ms 164) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S6_mass_action.v") (semantic-check "verified"))
39-
(entry (id "E6") (status "passing") (elapsed-ms 145) (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"))
40-
(entry (id "M7") (status "passing") (elapsed-ms 150) (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"))
41-
(entry (id "M8") (status "passing") (elapsed-ms 723) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M8_rank_nullity.v") (semantic-check "verified"))
42-
(entry (id "M9") (status "passing") (elapsed-ms 430) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M9_unique_factorization.v") (semantic-check "verified"))
43-
(entry (id "M10") (status "passing") (elapsed-ms 164) (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"))
44-
(entry (id "M11") (status "passing") (elapsed-ms 609) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M11_pigeonhole.v") (semantic-check "verified"))
45-
(entry (id "E7") (status "passing") (elapsed-ms 160) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E7_carnot_efficiency.v") (semantic-check "verified"))
46-
(entry (id "S7") (status "passing") (elapsed-ms 220) (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"))
47-
(entry (id "E8") (status "passing") (elapsed-ms 193) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E8_nyquist_shannon.v") (semantic-check "verified"))
48-
(entry (id "M12") (status "passing") (elapsed-ms 145) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M12_dominated_convergence.v") (semantic-check "verified"))
49-
(entry (id "S8") (status "passing") (elapsed-ms 166) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S8_hardy_weinberg.v") (semantic-check "verified"))
50-
(entry (id "E9") (status "passing") (elapsed-ms 133) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E9_newton_convergence.v") (semantic-check "verified"))
51-
(entry (id "M13") (status "passing") (elapsed-ms 148) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M13_hahn_banach.v") (semantic-check "verified"))
52-
(entry (id "M14") (status "passing") (elapsed-ms 127) (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"))
53-
(entry (id "S9") (status "passing") (elapsed-ms 131) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S9_chandrasekhar.v") (semantic-check "verified"))
54-
(entry (id "S10") (status "passing") (elapsed-ms 140) (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"))
55-
(entry (id "E10") (status "passing") (elapsed-ms 148) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E10_bathtub_reliability.v") (semantic-check "verified"))
56-
(entry (id "E11") (status "passing") (elapsed-ms 163) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E11_kirchhoff.v") (semantic-check "verified"))
22+
(entry (id "M1") (status "passing") (elapsed-ms 8482) (prover "idris2") (kernel-version "Idris 2, version 0.8.0-712523a89") (proof-file "proofs/canonical-proof-suite/M1InfinitudeOfPrimes.idr") (semantic-check "verified"))
23+
(entry (id "M2") (status "passing") (elapsed-ms 6143) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M2_lagrange.v") (semantic-check "verified"))
24+
(entry (id "M3") (status "passing") (elapsed-ms 2148) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M3_ivt.v") (semantic-check "verified"))
25+
(entry (id "M4") (status "passing") (elapsed-ms 2877) (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"))
26+
(entry (id "M5") (status "passing") (elapsed-ms 1190) (prover "agda") (kernel-version "Agda version 2.8.0") (proof-file "proofs/canonical-proof-suite/M5-yoneda.agda") (semantic-check "verified"))
27+
(entry (id "S1") (status "passing") (elapsed-ms 385) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S1_noether_energy.v") (semantic-check "verified"))
28+
(entry (id "S2") (status "passing") (elapsed-ms 414) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S2_gauss_law.v") (semantic-check "verified"))
29+
(entry (id "S3") (status "passing") (elapsed-ms 1637) (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"))
30+
(entry (id "S4") (status "passing") (elapsed-ms 1286) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S4_heisenberg_discrete.v") (semantic-check "verified"))
31+
(entry (id "S5") (status "passing") (elapsed-ms 1272) (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"))
32+
(entry (id "E1") (status "passing") (elapsed-ms 3863) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E1_lyapunov_ndim.v") (semantic-check "verified"))
33+
(entry (id "E2") (status "passing") (elapsed-ms 3465) (prover "idris2") (kernel-version "Idris 2, version 0.8.0-712523a89") (proof-file "proofs/canonical-proof-suite/E2-adder-equivalence.idr") (semantic-check "verified"))
34+
(entry (id "E3") (status "passing") (elapsed-ms 180) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E3_cantilever_deflection.v") (semantic-check "verified"))
35+
(entry (id "E4") (status "passing") (elapsed-ms 3528) (prover "idris2") (kernel-version "Idris 2, version 0.8.0-712523a89") (proof-file "proofs/canonical-proof-suite/E4-mergesort.idr") (semantic-check "verified"))
36+
(entry (id "E5") (status "passing") (elapsed-ms 170) (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"))
37+
(entry (id "M6") (status "passing") (elapsed-ms 172) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M6_deduction_theorem.v") (semantic-check "verified"))
38+
(entry (id "S6") (status "passing") (elapsed-ms 230) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S6_mass_action.v") (semantic-check "verified"))
39+
(entry (id "E6") (status "passing") (elapsed-ms 253) (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"))
40+
(entry (id "M7") (status "passing") (elapsed-ms 212) (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"))
41+
(entry (id "M8") (status "passing") (elapsed-ms 698) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M8_rank_nullity.v") (semantic-check "verified"))
42+
(entry (id "M9") (status "passing") (elapsed-ms 425) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M9_unique_factorization.v") (semantic-check "verified"))
43+
(entry (id "M10") (status "passing") (elapsed-ms 187) (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"))
44+
(entry (id "M11") (status "passing") (elapsed-ms 691) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M11_pigeonhole.v") (semantic-check "verified"))
45+
(entry (id "E7") (status "passing") (elapsed-ms 145) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E7_carnot_efficiency.v") (semantic-check "verified"))
46+
(entry (id "S7") (status "passing") (elapsed-ms 179) (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"))
47+
(entry (id "E8") (status "passing") (elapsed-ms 171) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E8_nyquist_shannon.v") (semantic-check "verified"))
48+
(entry (id "M12") (status "passing") (elapsed-ms 205) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M12_dominated_convergence.v") (semantic-check "verified"))
49+
(entry (id "S8") (status "passing") (elapsed-ms 171) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S8_hardy_weinberg.v") (semantic-check "verified"))
50+
(entry (id "E9") (status "passing") (elapsed-ms 194) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E9_newton_convergence.v") (semantic-check "verified"))
51+
(entry (id "M13") (status "passing") (elapsed-ms 209) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/M13_hahn_banach.v") (semantic-check "verified"))
52+
(entry (id "M14") (status "passing") (elapsed-ms 174) (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"))
53+
(entry (id "S9") (status "passing") (elapsed-ms 171) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/S9_chandrasekhar.v") (semantic-check "verified"))
54+
(entry (id "S10") (status "passing") (elapsed-ms 172) (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"))
55+
(entry (id "E10") (status "passing") (elapsed-ms 144) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E10_bathtub_reliability.v") (semantic-check "verified"))
56+
(entry (id "E11") (status "passing") (elapsed-ms 165) (prover "rocq") (kernel-version "The Rocq Prover, version 9.1.1") (proof-file "proofs/canonical-proof-suite/E11_kirchhoff.v") (semantic-check "verified"))
5757
))

0 commit comments

Comments
 (0)