docs + test(sketchdb): proofs.md + accuracy empirical validation (#2.2 + #2.4) - #58
Merged
Merged
Conversation
…ckfill theorems (ASAPQuery-backend #2.4)
…rity + monotonicity sweeps Addresses TODO.md #2 sub-item #2. Paper-artifact regression guard on the `AccuracyProfile::derive` module: ## 1. Published-constant parity Each sketch family's theoretical ε at a canonical parameter matches the paper-published constant to ≥ 6 decimal places: * HLL(p=14) = 1.04/√(2^14) = 0.008125 — Flajolet 2007 * CMS(w=1000, d=3) = e/w ≈ 2.718e-3 — Cormode-Muthukrishnan 2005 * CountSketch(w=10_000) = 1/√w = 0.01 — Charikar-Chen-Farach-Colton * KLL(k=200) = 2.296/√k — Karnin-Lang-Liberty FOCS 2016 * DDSketch(α) passes through verbatim — Masson-Rim-Lee VLDB 2019 * CMS-with-heap combines CMS + retention — Metwally ICDT 2005 ## 2. Monotonicity sweeps Larger capacity monotonically tightens the bound — non-monotone sweeps indicate a broken formula. Covered: HLL over precision, CMS ε over width, CMS δ over depth, CountSketch ε over width, KLL ε over k, DDSketch ε over α, CMS-with-heap ε over heap_size. ## 3. Relative ordering Cross-family sanity: at w=10_000, CMS's ε (e/w ≈ 2.7e-4) beats CountSketch's (1/√w = 0.01), confirming the two formulas weren't accidentally swapped. ## Why no live sketch runs The backend's `asap_sketchlib` git-dep exposes a different API surface from sketchlib-bench's workspace path-dep (older commit, pre-ErtlMLE/DataInput refactor). Bridging the two inside a unit test couples to a specific dep pinning that churns. Live "measure sketch, compare to bound" sweeps live in sketchlib-bench's `sketchlib bench --metrics accuracy` output and are compared to `AccuracyProfile::derive` via an external script; this test pins the *theoretical* side of that comparison so it doesn't drift. ## Tests 788 → 801 (+13), all non-ignored, clippy + fmt clean.
zzylol
changed the title
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Two TODO.md #2 sub-items in one PR — both target paper §theory + §eval artifacts.
#2.4 —
docs/proofs.mdNew 245-line doc collecting:
combine_statisticcorrectness across schema-timeline segments — theorem + proof sketch.Cross-refs added from
accuracy.rsmodule doc-comment todocs/proofs.md.#2.2 — accuracy empirical validation (+13 tests)
Paper-artifact regression guard on
AccuracyProfile::derive:Live "measure sketch, compare to bound" sweeps live in sketchlib-bench's `sketchlib bench --metrics accuracy` output; this test pins the theoretical side.
Stats
788 → 801 tests green; clippy + fmt clean.
🤖 Generated with Claude Code