docs: paper §theory correctness proofs (combine, write-barrier, backfill)

[zzylol]

Summary

Rewrites docs/proofs.md to a per-proof structure (Statement / Setup-Lemmas / Proof / Caveats / Code anchors) for paper-blocker #5 — three formal correctness theorems the §theory chapter draws from:

• §2 combine_statistic correctness across schema-timeline segments — additive stats (Count / Sum) bounded by the sum of per-segment errors; idempotent stats (Min / Max) bounded by the max; non-combinable stats (Cardinality / Quantile / Topk / Rate / Increase) safely return Partial. Direct case-analysis proof relying on disjoint covering by SchemaRegistry::timeline_for_metric and the triangle inequality.
• §3 Write-barrier safety — no sample ingested at $t > t^\ast = $ time of force_expire(agg_id) reaches any query result. Direct path-chase: force_expire is monotonic on (retired_at_ms, expires_at_ms) $\to$ AggSchema::status returns Expired thereafter $\to$ is_writable rejects $\to$ route_decoded_samples drops $\to$ workers / store / queries never see it.
• §4 Backfill determinism — build_backfilled_accumulator produces bit-identical sketch bytes to a hypothetical live worker fed the same samples in the same order. Induction on sample-stream length, leveraging the §10.5 invariants enforced by BackfillRegistry::create_checked (known agg / time-disjoint / within retention) and the shared create_accumulator_updater factory.

Each proof cites runtime functions by symbol name (line-number-stable), lists caveats explicitly (clock skew, cross-language byte parity, HashMap-iteration order, etc.), and cross-links the corresponding sections of design-sketch-db-core.md. TODO.md item 5 marked done with a pointer.

Touches only:

• docs/proofs.md (full rewrite).
• TODO.md (one section header + bullet update).

No source *.rs files modified.

Test plan

• Render docs/proofs.md in mkdocs / GitHub markdown — confirm $...$ math renders, tables render, internal anchors (./design-sketch-db.md, ./design-sketch-db-core.md) resolve.
• Spot-check each cited symbol resolves: grep -n 'fn combine_statistic' in engines/timeline_dispatch.rs, grep -n 'fn force_expire\|fn is_writable\|fn status\|fn timeline_for_metric' in stores/sketch_db/schema.rs, grep -n 'fn create_checked\|fn build_backfilled_accumulator' in stores/sketch_db/{backfill,backfill_window_builder}.rs.
• Verify the cited test backfill_builds_bit_identical_sum_accumulator_to_live still passes: cargo test -p asap-query-engine backfill_builds_bit_identical_sum_accumulator_to_live.
• Confirm TODO.md item-5 link to docs/proofs.md resolves.

🤖 Generated with Claude Code