Skip to content

Commit d1a4069

Browse files
author
florath-lean4-3
committed
Add Lean post-Keri comparison history
1 parent 19d1caa commit d1a4069

2 files changed

Lines changed: 52 additions & 0 deletions

File tree

‎reference-data/README.md‎

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -47,6 +47,35 @@ q,n,r,lower_bound,upper_bound,lower_bound_reference,upper_bound_reference
4747
The reference columns should contain BibTeX keys from
4848
`references.bib`. Multiple keys may be separated by semicolons.
4949

50+
`lean-post-keri-comparison-history.csv` is an append-only audit ledger for the
51+
aggregate summary printed by `reference-data/scripts/compare_lean_post_keri_bounds.py`.
52+
Each row compares the Lean generated table with the post-Keri reference table
53+
over overlapping `(q,n,r)` triples that have both reference bounds. The first
54+
column is the commit timestamp in UTC, followed by the total and tag counts,
55+
then a short commit hash and an optional `improvement` note. Percentages are
56+
derivable from `total` and are not stored.
57+
58+
The compact tag columns mean: `ref_tight` = `reference_tighter`, `exact` =
59+
`exact_agree`, `ref_lo` = `reference_better_lower`, `ref_hi` =
60+
`reference_better_upper`, `we_lo` = `we_better_lower`, `we_tight` =
61+
`we_tighter`, `we_hi` = `we_better_upper`, `agree_lo` = `agree_lower`,
62+
`agree_hi` = `agree_upper`, `missing` = `lean_missing`, and `contrad` =
63+
contradictions.
64+
65+
The `improvement` column is intentionally sparse. It records only bounds whose
66+
comparison tag changed relative to the previous history row, using compact forms
67+
such as `K_7(4,2)<=23 (was 25)` or `K_8(4,2)=23 (was [13,32])`; derived bound
68+
changes that do not move an aggregate tag are omitted.
69+
70+
To update the history ledger, run the comparison script from the repository root,
71+
copy the printed `COMPARISON SUMMARY` counts into a new row, record the current
72+
commit hash, and leave absent tags as `0`. If the row changes comparison tags,
73+
add the corresponding short bound changes in `improvement`. This file is not
74+
updated automatically; it is intended for occasional human or agent-driven
75+
snapshots.
76+
The detailed row-level report remains `reference-data/reference-db-comparison.csv`
77+
and is still generated/ignored.
78+
5079
## Lean Dump
5180

5281
`lean/non_mixed_covering_codes.csv` is a documentation dump of the generated

‎reference-data/lean-post-keri-comparison-history.csv‎

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
timestamp_utc,total,ref_tight,exact,ref_lo,ref_hi,we_lo,we_tight,we_hi,agree_lo,agree_hi,partial,missing,contrad,commit,improvement
2+
2026-06-07T08:40:45Z,1145,674,425,36,10,0,0,0,0,0,0,0,0,a467a01d8494,baseline
3+
2026-06-07T16:16:54Z,1145,674,425,36,10,0,0,0,0,0,0,0,0,c4c97f78af7e,
4+
2026-06-07T18:24:31Z,1145,674,425,36,10,0,0,0,0,0,0,0,0,460df105545c,
5+
2026-06-15T09:40:18Z,1145,673,425,36,10,1,0,0,0,0,0,0,0,59f23ea2c632,"K_8(4,2)=23 (was [13,32])"
6+
2026-06-15T11:02:36Z,1145,673,425,36,10,1,0,0,0,0,0,0,0,fae817df3d5b,
7+
2026-06-17T14:38:35Z,1145,672,425,37,10,1,0,0,0,0,0,0,0,3e50a1e38780,"K_3(6,2)<=17 (was 24)"
8+
2026-06-17T19:05:23Z,1145,672,425,37,10,1,0,0,0,0,0,0,0,5b2a770342eb,
9+
2026-06-18T10:28:53Z,1145,672,425,37,10,1,0,0,0,0,0,0,0,b7447bdacf5e,
10+
2026-06-21T16:34:25Z,1145,672,425,37,10,1,0,0,0,0,0,0,0,5b4f3bf2f661,
11+
2026-06-21T17:27:27Z,1145,672,425,37,10,1,0,0,0,0,0,0,0,66007d55c9af,
12+
2026-06-21T17:33:53Z,1145,672,425,37,10,1,0,0,0,0,0,0,0,0eea7a645b58,
13+
2026-06-21T17:44:38Z,1145,672,425,37,10,1,0,0,0,0,0,0,0,1d5217236d79,
14+
2026-06-21T19:51:47Z,1145,669,425,40,10,1,0,0,0,0,0,0,0,021e583013fd,"K_6(7,2)<=1296 (was 3888); K_6(8,2)<=5184 (was 23328); K_7(7,2)<=2401 (was 7889)"
15+
2026-06-22T04:51:01Z,1145,667,425,42,10,1,0,0,0,0,0,0,0,ab0ae885e732,"K_9(8,4)<=729 (was 3321); K_9(9,5)<=729 (was 3321)"
16+
2026-06-22T09:43:49Z,1145,667,425,42,10,1,0,0,0,0,0,0,0,2db30e1704d0,
17+
2026-06-22T11:03:31Z,1145,667,425,42,10,1,0,0,0,0,0,0,0,ad78b6641d65,
18+
2026-06-22T11:03:53Z,1145,666,425,43,10,1,0,0,0,0,0,0,0,13284f2572e1,"K_9(8,2)<=59049 (was 269001)"
19+
2026-06-22T11:58:59Z,1145,665,425,44,10,1,0,0,0,0,0,0,0,d2da727c20a9,"K_9(9,3)<=29889 (was 59049)"
20+
2026-06-22T12:26:36Z,1145,664,425,45,10,1,0,0,0,0,0,0,0,a53fc42fd958,"K_10(8,4)<=1156 (was 5000)"
21+
2026-06-22T12:58:41Z,1145,663,425,46,10,1,0,0,0,0,0,0,0,90abca12b7c2,"K_12(8,5)<=264 (was 864)"
22+
2026-06-22T13:41:05Z,1145,661,425,48,10,1,0,0,0,0,0,0,0,eeab6130eb91,"K_16(6,2)<=10752 (was 32768); K_16(7,2)<=172032 (was 524288)"
23+
2026-06-22T19:42:03Z,1145,661,425,48,10,1,0,0,0,0,0,0,0,19d1caad6302,

0 commit comments

Comments
 (0)