Approximation property distinction library

Family 330: A uniformly discrete counterexample to bounded approximation in Lipschitz-free spaces. First review, 9 October 2026 Australia/Brisbane.

Problem and potential new use

Formalization teams can record why approximation by finite-rank operators differs from uniformly bounded approximation.

Applicability and commercial boundary

The infinite discrete metric example does not create a practical approximation algorithm or show that a finite software model cannot be approximated.

Initial business decision

Defer direct product. Commercial demand and profitability remain hypotheses.

Next verification action

Preserve the two property definitions and inspect how the counterexample is represented formally.

Evidence scope

The catalog statement was individually reviewed. Main-paper and selected formal-scope passages were additionally inspected for families 090, 093, 094, 097, 325, 328 and 332; this record does not claim a full proof audit or independent Lean verification. Source revision fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb. See source metadata.