bi-Lipschitz concept

Definition	Of a map between two spaces, neither stretching nor shrinking any distance by more than a fixed factor. Equation 0.21. Also Lipschitz.
Example	A map with factor 2 sends a distance of 1 to something between 0.5 and 2.
Book	Data Mining as Observation, draft 0.2, commit `f3914f0`; entry id `bi-lipschitz`, kind concept.
Status	refutes or corrects [refuted]. Corrections: 1 item(s), see below.
Defining equation	Book equation 0.21.
Assumptions and scope	A map is bi-Lipschitz with factor K when it neither stretches nor shrinks any distance by more than K. The factor is at least one, compositions multiply the factors, and the map preserves a nearest neighbour whenever the runner-up is more than K squared times as far, the rank certificate’s per-pair fact. It does not preserve every ordering, so it is not rank-faithful, and the program’s fixed-scale uniform bi-Lipschitz claim for the commute filter is refuted and carried in the ledger.
Prior art	none recorded
Evidence	`geometric-observation/claims/LEDGER.md:94`, `lean/DataMiningAsObservation/BiLipschitz.lean`
Reviewed	not yet reviewed; generated 2026-09-10 from records at the commits on the provenance page.

Every distance stretched or shrunk by at most a fixed factor.

Equation

Book equation 0.21.

\[\frac1K\,d(x,y)\ \le\ d'\big(f(x),f(y)\big)\ \le\ K\,d(x,y)\qquad\text{for all }x,y.\]

Conditions

A map is bi-Lipschitz with factor K when it neither stretches nor shrinks any distance by more than K. The factor is at least one, compositions multiply the factors, and the map preserves a nearest neighbour whenever the runner-up is more than K squared times as far, the rank certificate’s per-pair fact.
It does not preserve every ordering, so it is not rank-faithful, and the program’s fixed-scale uniform bi-Lipschitz claim for the commute filter is refuted and carried in the ledger.

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

Ledger

refutes or corrects. NEG-1 [refuted]. Fixed-scale, uniform-in-m bi-Lipschitz for the commute filter. geometric-observation/claims/LEDGER.md:94.

First stated

Chapter 0 section 0.10 of Data Mining as Observation, with the refuted uniform bi-Lipschitz claim for the commute filter in Volume 14’s honest negatives, ledger row NEG-1.

Measurements

none

Failures and corrections

NEG-1, [refuted]. Fixed-scale, uniform-in-m bi-Lipschitz for the commute filter. geometric-observation/claims/LEDGER.md:94.

Invariance envelope

none declared

Machine checked

lean/DataMiningAsObservation/BiLipschitz.lean, theorems one_le_factor, within_comp, nn_preserved, not_rank_faithful, at observation-data-mining f3914f0; what the check covers is stated in the book’s appendix C.

Used in

Data Mining as Observation chapters 0, 3.

rank-faithful; rank certificate; recognizer; quotient.

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.

← Bernoulli, binomialbit →