An optimized tag filter is claimed to return exactly the documents the brute-force one does — what does an argument by mutual inclusion give you that spot-checks do not?

## Subset, proper subset, equality Three relations, routinely blurred: - `X ⊆ Y` — **subset**: every member of `X` is a member of `Y`. It permits `X = Y`. - `X ⊂ Y` — **proper subset**: `X ⊆ Y` and `X ≠ Y`, so `Y` has at least one member `X` lacks. (Some authors use `⊂` for any subset, so in writing that matters, say which you mean or use `⊆` and `⊊`.) - `X = Y` — equality, which by definition means the two have exactly the same members. The bridge is the one that does the work here: **`X = Y` if and only if `X ⊆ Y` and `Y ⊆ X`.** Equality is not a separate thing to check; it is two containments. ## What each direction rules out For an optimized filter `O` and the brute-force filter `B` over the same corpus: | Direction | Plain reading | The bug it excludes | |---|---|---| | `O ⊆ B` | the fast one invents nothing | false positives: documents returned that do not match | | `B ⊆ O` | the fast one loses nothing | false negatives: matching documents silently missing | The second is the one that hurts in production, because a missing row looks like an empty state and nobody files a ticket. Naming the directions separately is therefore not pedantry: it tells you which risk you have actually retired. ## Why an arbitrary element beats a sample The argument shape is always the same: *let `d` be any document the first filter returns; here is why the second must return it too*. Because `d` was arbitrary — nothing about it was assumed except that it satisfied the condition — the conclusion holds for every document in every corpus, including corpora that do not exist yet. A spot-check does the opposite. It confirms the claim on the documents in the fixture and says nothing about the rest. The inputs that break a filter rewrite are rarely the ones a person types into a fixture: - a filter naming a label **no document carries** (an empty operand), - a document carrying **every** label in the taxonomy, - the **empty selection**, where a union is empty but an intersection is the whole universe, - a label created after the accelerating structure was built, - a document appearing in two operands where the fast path assumed disjointness. Each is a class of input, not a single row, which is exactly what the containment argument quantifies over and a sample does not. ## The failure is the useful part Attempt the direction `B ⊆ O` and follow it honestly: take a document the brute-force filter returns, and try to show the optimized path reaches it. When the argument stalls, the step where it stalls names the condition the fast path relies on — 'this only works if every label in the request has an index entry', say. That condition is now either a precondition to enforce or a bug to fix, and it came with a description of *all* the inputs that violate it. A failing test gives you one row and leaves the generalisation to you. ## Where a one-directional claim is what you actually want Equality is not always the goal, and asking for the wrong relation is its own defect. A permission-aware filter must never return more than the unrestricted one: the requirement is `permitted ⊆ unrestricted`, and demanding equality would defeat the point of the restriction. Similarly a cheap pre-filter used to narrow a candidate list must be a **superset** of the true answer — it may over-return, and a later exact pass removes the extras, but it must never drop a real match. Both are containments deliberately held in one direction only, and stating them that way is what makes them testable. ## Two traps worth naming First, the **vacuous direction**. The empty set is a subset of every set, so a rewrite that always returns nothing satisfies `O ⊆ B` perfectly. A one-directional argument that looks easy is often easy because it is vacuous; the other direction is where the content is. Second, **equality of results is not equality of behaviour**. Two filters can return the same set while differing in ordering, in paging, in cost, or in what they do when the taxonomy is mid-migration. Set equality is a statement about membership only, and claiming more from it than that is how a correct rewrite still breaks a screen. ## What an interviewer is listening for That you decompose equality into two containments and can say what each one buys; that you reach for an arbitrary element rather than examples; that you name the input classes at the edges; and that you recognise the cases where a single direction is the real requirement. Nobody wants a written proof at a whiteboard — they want the shape of the argument and the counterexample class it produces when it fails.