Audit log — machine-certified proof corpus

Purpose: an independently checkable record of how every artifact in data/proofs/ came to exist. Two layers:

data/proofs/audit.jsonl (machine layer, append-only): from commit 1697dd7+, every prove_bound, recheck_certificate, certify_attainment, and write_report call appends one JSON line — UTC timestamp, the git commit of the code that ran, statement, outcome, box counts, achieved slack. Nothing that produces or checks a certificate can run without leaving a line here.
This file (human layer): chronological narrative with pointers. Events before the jsonl hook existed are reconstructed from git history and the run logs (data/proofs/*.log), all committed.

How to audit any theorem: open its <class>__<functional>.json certificate (statement, box count, achieved slack, leaf archives), its .md report, grep audit.jsonl for its prove/recheck/attainment lines, and re-run python3 -m gft.proofs recheck data/proofs/<name>.json — the recheck re-verifies sampled leaves in independent mpmath interval arithmetic. Full reproduction: the prove command in each report.

2026-06-11 session timeline (times IST, git SHAs verifiable)

time	commit	event
00:34	f56e405	Proof factory v1: certified branch-and-bound over the Schur box; exact sympy reduction; rotation lemma; negative controls pass (false bounds refused with witness).
00:49	1db028d	v2: factored-DAG interval evaluator (`gft/dag.py`) fixes the expanded-polynomial dependency blow-up on degenerate Schur faces (measured 1.6e-2 floor → 7.6e-14).
01:07	12b1e3c	Affine-arithmetic bound form; METHODS.md; v2 test suite.
01:20	2daf9d6	Public /proofs page (certificate gallery, reports, methods doc) deployed.
01:46–03:10	9cc17c9, 6185fd0, 2bc2029, c8ed9d8	LLM extraction program (Sonnet subagents propose; deterministic merge gate with sympy φ-series cross-check): corpus 487→548 papers, 204 at structured quality, 651 bounds, 1,004 claims. Agents never write the DB; the gate nulls refuted class guesses (12 mislabeled proof-candidates purged).
02:19	8ac8903	Parallel prover (`workers=N`, exact partition preserved); recheck subdivision; H₃(1) open-set geography probe — found the bulk-interior wall, not the extremal circle.
~03:20	—	m=4 (7-D) slate runs die honestly: lemniscate H₃ hits its memory cap at 156M boxes; certify-rate curve (3%/19%/81% at widths 1/8/16/32) shows ~10¹⁰ boxes needed → m=4 declared out of reach for the current bound family (HARDNESS.md §2).
~10:23	—	Incident: whole-WSL OOM kill. Root cause: an uncapped ad-hoc 240M-box run + in-RAM leaf accumulation (~10GB). Both causes fixed below; guardrail recorded in session memory.
10:40	b635cdf	OOM-proof prover: leaves spill to `.partN.npz` every 2M boxes (RAM-flat); runner capped 4 workers / `MemoryMax=4G`; trig-correlated affine form added (sound: 0/2000 violation samples).
10:50	044f7bc	Tier-1 slate runner (52 sharp Fekete–Szegő targets from exp2b plateaus; coarse-to-fine slack ladder 1e-3→1e-4→1e-6; failed tightenings can never overwrite a PROVED cert); HARDNESS.md published at /proofs/hardness.
11:06	43c7a9d	Trust-chain fix: certificates near sharp attainment certify only via affine forms, which the mpmath recheck lacked. Added iv-coefficient affine + trig-correlated forms to the recheck. Worst leaf (bell FS): RECHECK_OK at 2.5e-10 margin. Without this, some certificates were verifiable only by the arithmetic that produced them.
11:26	a7fbb9c	Corpus shipped: 38 sharp FS theorems (36 at slack 1e-6), 38/38 RECHECK_OK, 38/38 attainment-certified (= certified sharp). Deployed to /proofs. Logs: `tier1_fs.log`, `postpass.log`.
11:34	1697dd7	`sp.N` fix for algebraic constants (√2 classes); audit.jsonl hook added to all certificate-producing functions.
12:21	d9674b6	Corpus at 41: rational_kr FS(μ=1) ≤ −1/2+√2/2 and limaçon(1/√2) both μ at 1e-6. Two-family-tie analysis added to HARDNESS.md §3a: all 10 (now 11 incl. checks) Tier-1 failures are exactly the combos where the ω=z² family and the γ₀=1 face attain the same value (verified per-class; e.g. nephroid μ=1 both 1/2) — positive-dimensional attainment set, structurally beyond ε ≤ 1e-3 certification today.
~12:3x	ef7d364	Corpus #42: rational_kr FS(μ=½) ≤ −1/2+√2/2 + 1e-3 PROVED (57.6M boxes; 1e-4 rung refused — recorded). Audit layer pushed to GitHub after stripping 2.1GB of gate-probe leaf archives that an `add -A` had swept in (HTTP 500 root cause; scratch dirs now gitignored).
~13:3x	(this commit)	Tier-2 H₂(2) slate complete: 4/26 PROVED — lemniscate, sigmoid, strongly_0.25 (each ≤ 1/16 + 1e-2) and rational_kr (≤ 3/4 − √2/2 + 1e-2). Governing variable measured: relative slack ≳ 15% certifies, below refuses (exponential 4%, cardioid 2.3%, starlike 1%; starlike also refused + 1e-3 at ~240M boxes). Corpus: 46 theorems, all recheck + attainment certified. Logs: `h22_gate2.log`, `tier2_h22.log`, `postpass3.log`.

Standing verification invariants

A FAILED certificate is evidence, not error: it carries either a witness box or the exhausted budget; negative controls (e.g. H₃(1) ≤ 0.4 over S*, refused at 704K boxes with witness) are rerun in the test suite (tests/test_proofs.py, 23 checks).
No LLM output enters any proof artifact. LLM extraction touches only the paper registry, through app/merge_extraction.py's validation gate.
Heavy compute runs in systemd-run scopes with MemoryMax (see the 10:23 incident). Run logs under data/proofs/ are committed.