The Observation Theory EncyclopediaFrom TSKAboutBy kindBy chapterBy Lean fileLedgerProvenance

rank certificate instrument

DefinitionA bound, computed from a compressed representation, that certifies which neighbour rankings the compression preserved for a consumer and which it did not. In its strict setting the floor is a guarantee, in its percentile setting an estimate. A vacuous result supplies no guarantee about the corpus, and falling back to exact reranking is the program's policy for it rather than a consequence. Chapter 11. Also rank fidelity.
ExampleA ratio spread kappa of 1.0148 with mu of 0.0664 certifies Kendall tau at least 0.8671 across 19900 pairs.
BookData Mining as Observation, draft 0.2, commit f3914f0; entry id rank-certificate, kind instrument.
Statusno ledger row names this entry. Corrections: 1 item(s), see below.
Defining equationnone
Assumptions and scope
  • In the strict setting, the zeroth and hundredth percentiles of the distance ratio, the floor is a guarantee for the anchor sample, broken by a single collapsed pair.
  • In the percentile setting the implementation computes the distortion on the retained central pairs and the concentration over all pairs, and the floor is a robust estimate, not a guarantee on either set.
  • The floor is about the global ordering of the sampled pairwise distances. It does not directly certify a query’s top-k recall, one query’s neighbour order, or the trimmed tail.
  • A floor on a sample of anchors is a statement about that sample. Carrying it to the corpus needs a sampling argument the certificate records the inputs for and does not supply.
  • A vacuous certificate supplies no guarantee about the corpus. Reranking exactly is the policy the program adopts when the certificate is vacuous, and not something the certificate proves necessary.
Prior artnone recorded
Evidenceturboquant-pro/turboquant_pro/rank_certificate.py:25-36, lean/DataMiningAsObservation/RankCertificate.lean
Reviewedsemantic review 2026-09-06; generated 2026-09-10 from records at the commits on the provenance page.
00.51estimateresamples of the same rows
A bound on which neighbour rankings the compression preserved.

Equation

none

Conditions

Conditions are curated in entries.toml rather than read from a record.

Ledger

none

First stated

The compression program’s certificate specification, turboquant-pro/docs/CERTIFICATE_SPEC.md, DOI 10.5281/zenodo.20660087, and chapter 11 section 11.3 of Data Mining as Observation.

Measurements

none

Failures and corrections

Invariance envelope

none declared

Machine checked

lean/DataMiningAsObservation/RankCertificate.lean, theorems nn_preserved, nn_preserved_of_kappa_one, kappa_ge_one, at observation-data-mining f3914f0; what the check covers is stated in the book’s appendix C.

Used in

Data Mining as Observation chapters 11.

Related

certificate; vacuity threshold; the flip; hubness.

See also

Book equations stated beside the entry’s terms, not defining it: 11.2, 11.3.

Ledger rows that cite the entry’s records without naming it: GO-3.

Sources-table rows that share a record with the entry without naming it: chapter 4 section 4.5, chapter 8 section 8.9, chapter 9 section 9.3, chapter 11 section 11.2, chapter 11 section 11.3, chapter 11 section 11.5.

Status

Generated 2026-09-10 by encyclopedia/generate.py; book at observation-data-mining f3914f0; the commit of every record is listed in the encyclopedia’s provenance.

← rankrank-faithful →