WINNEX — proof of what a search left out

indices: [0, 4] — the query was an exact copy of document 0, so document 0 comes first. Document 4 is [0.7, 0.7, 0, 0, …], whose cosine with the query is 0.7 — the closest of the remaining four.

bound violations: 0 — this is the number that matters. For documents 1, 2 and 3 the engine computed an upper bound on their possible similarity and found it below 0.7. It proved they could not be in the top-2. If this number were anything but zero, the proof would be broken and the library unsound.

latency: 0.016 ms — one query over five vectors. The point is not the speed; it is that the answer arrived with evidence attached.

proof: … — a human-readable summary of what was proven. The machine-readable version is the record produced when audit_exhaustive=True.

Of the five documents, two were returned and three were proven irrelevant — not guessed, not assumed, proven with arithmetic you can re-run.

1.0000 and 1.0000 mean exact reproduction. Every query returned precisely the top-10 a brute-force cosine scan would return. That is the claim being tested, and it held on all 50 queries — on synthetic data the script generated itself, not on a number we supplied.

Search time is higher than brute force here, and that is the honest reading. At 20,000 vectors the bound computation costs more than it saves: 108,0 ms against 33,6 ms. The engine is 3,2× slower per query at this size. What it buys is the bound violations: 0 line — the record that each of the 19,990 documents not returned was proven unable to belong.

The 11× gap between Colab and local is hardware, not code. 1186,6 ms against 108,0 ms for the same script and the same seed. Anyone reading a benchmark should ask which machine produced it; this page shows both.

Where the engine does win at this size is the build: 169,7 ms to index 20,000 vectors. That is the number that makes per-tenant indexes and rebuild-on-write practical.

The most important line is the one without an error. indexed garbage anyway, bound_violations=0 — the engine accepted the broken corpus, ran a search, and reported zero violations. Eight of the ten values it compared were NaN or zero, and the proof came back clean. Zero violations does not mean "the answer is right"; it means "the arithmetic was consistent with the inputs", and consistent garbage is still garbage.

250 of 500 dropped, exactly. The corpus was built with three defects: 100 rows with NaN in column 0, 100 all-zero rows, and 50 rows with inf. 100 + 100 + 50 = 250. The gate removed precisely the defective rows and nothing else — that is the number to check, not a round percentage.

WARN [dataset.recall_not_guaranteed] is the subtle one. Seed recall came back at 0.375 against a floor of 0.95, and all 8 seed queries were classified pool_only. That means the returned top-K is the best within the candidate pool — not proven to be the global top-K. If stage-2 truncation dropped the true neighbour before the bound was computed, the bound never had a chance to be violated. The engine will not claim a guarantee it cannot deliver.

WARN [dataset.foldable] is about PCA, not about the engine. With NaN present, enabling block_pca would build a covariance matrix of NaNs, whose eigenvectors are garbage — and recall collapses with no error raised anywhere. The gate is saying: fix the data before you turn on the compression, not after.

All thirteen flag codes are documented in the main documentation.

Both runs return bound_violations=0. The engine proved the exact top-3 in both cases. What changed is which question was answered.

With the demo encoder, "exact" means exact relative to a character-overlap ranking. The query asks about secrecy; the top result is about rent. The proof is perfectly valid and the answer is wrong.

With the real encoder the correct clause comes first — 0.548 against 0.441 for the same clause under the demo encoder. Nothing about the query mentions "sigilo"; the encoder connects "guardar segredo" to it. That is the entire difference.

Margin −0.0459 is not a win. One unrelated pair — a termination clause against a delivery deadline — scores 0.5262, above the weakest paraphrase at 0.4803. Only 3 of 6 paraphrases sit above the worst negative.

What the real encoder improves is the average: 0.5276 against 0.3316, a separation that lets a threshold work most of the time. The demo encoder averages 0.3720 against 0.3592 — a gap of 0.013, which is noise.

This is why the quality gate exists (example 05). No encoder separates all cases, so you check the corpus and the recall floor rather than trusting the model.

The first two hits answer the question directly — the original rent of $2,000.00 and the adjustment to $2,400.00. Read together they tell you the current rent is the second one; the first is history.

The third hit is the honest part. A confidentiality clause scored 0.7169 against a query about rent — it shares vocabulary ("prazo", "partes") and nothing else. Retrieval finds similar text, not correct text. The engine cannot know that a confidentiality clause is not an answer to a rent question; it only guarantees that nothing more similar was left out.

Three documents stayed behind, and the margin is visible. Their exact cosine scores are 0.6928 (medical report), 0.6893 (legal opinion) and 0.6442 (invoice). All three fall below the cut of 0.7169 — set by the confidentiality clause itself. Note how thin the first gap is: 0.6928 against 0.7169 is a difference of 0.024. That is precisely the situation where an approximate index drops a neighbour and nobody notices; here the bound is computed, not assumed.

The proof line reports recall of 99.6–100% against exact scan. This is where honesty matters: it is not stated as 100%. With k1_fraction=1.0 and postfilter the configuration is designed to guarantee recall, but the measured range across progressive configurations is 99.6% at the low end. The engine reports the range it actually measured rather than the best number it saw.

The ordering is right, and that is the whole test. The question asks for the current rent. The addendum ("$2,400.00 a partir de janeiro") comes first at 0.7521; the original clause ("$2,000.00, corrigido pelo IGP-M") comes second at 0.7467. A model that reads only the second passage answers $2,000.00 — wrong, and confidently so. Retrieval order is what prevents that.

The third hit is a false positive you should expect. "A multa por rescisão é de três aluguéis" scores 0.7391 for a question about rent — near-miss vocabulary ("aluguéis") and nothing else. The demo encoder hashes characters, so it cannot tell a penalty clause from a price clause. That is the encoder's limit, not the retrieval's.

The cut fell at 0.7391, excluding three documents at 0.7028, 0.6796 and 0.6517. The margin above the cut is comfortable here (0.036), unlike example 07 where it was 0.024 — a reminder that the guarantee is only as strong as the gap the query produces.

The retrieval block handed to the model carries an evidence section. That is what allows the prompt to say "the system can produce that proof" — because the proof exists in the payload, not because the prompt asserts it. A model told to claim completeness without evidence produces the same sentence with a hallucination underneath it.

What the prompt does not do is check the answer. Nothing here verifies that the model said $2,400.00 instead of $2,000.00 — the example shows retrieval wiring, not answer validation. Anyone deploying this still owns that last step.

Indexing only the response, not the instruction. The Kaggle dataset repeats the same system prompt in the instruction column of all 704 rows. Indexing instruction + output makes every document look alike — top score 0.45 and the top-4 is arbitrary. Indexing the response alone lifts the top score to 0.775 and the first result is the correct clinical case: persistent thirst with normal glucose.

The multilingual encoder. The corpus is in English, the question in Portuguese. all-MiniLM-L6-v2 returns 0.198 and an essentially random top-1. The multilingual variant returns 0.402 on the same data — and 0.775 once the repeated system prompt is out of the index.

Both fixes were found by running it, not by reading the docs. The first version of this example returned 0.199 and the LLM correctly answered "the passages do not contain this information". The pipeline was working; the retrieval was not.

Citations must point at passages that exist. The regex finds [N] and rejects any N outside 1..4.

Numbers must trace back to the context. Any figure in the answer that does not appear in the retrieved passages is flagged — that is where fabricated dosages and values surface.

Abstention is recorded, not penalised. When the LLM says it cannot answer, that is a valid outcome and it gets logged as such.

Why the recall returned "hospitalar, Portugal" for the question "when can I contact the client". The demo embedding hashes characters, so it matches on vocabulary rather than meaning. "Cliente" appears in both, and the Portugal memory shares the most characters with the query. That is a limitation of the demo encoder, not of the retrieval — swap embed() for a real model and the ranking reflects meaning.

The second hit is the one that matters in production. "Não ser contatado às sextas" is the memory an agent must never lose — a missed preference is a broken commitment. It came second with score 0.899, above the cut.

The two explanations are the point of the example. The contract memory scored 0.817 against a cut of 0.899 — it lost by 0.082, and the output says so. An agent that prints "memory not found" tells you nothing; an agent that prints "5th of 5, score 0.817, cut 0.899" lets you decide whether the embedding is good enough.

Notice that the preference about short answers also fell out — 4th place at 0.839. In a real deployment that is a signal: if your encoder cannot separate "answer briefly" from "when can I call", the threshold needs tuning before it costs you a client.

Every remember() rebuilds the index — which sounds expensive until you look at the numbers. A 1M-vector index builds in 1.69 s against 33.6 s for HNSW on the same corpus. Agent memory can grow in real time without the guarantee degrading or the write path blocking.

The norms before are ~90 to 107, after they are exactly 1. Cosine similarity is invariant to that scaling, so the rescaling changes nothing about ranking — what it changes is that the Cauchy–Schwarz bound becomes tight and cheap to compute. An unnormalized corpus still gives correct answers, just with a looser bound and more work per query.

The two rejections are the reason this package exists. A zero vector passes silently through almost every production pipeline: no error, no log line, and the proof stays "valid" over garbage. The NaN case is worse — the bound arithmetic produces NaN, comparisons with NaN are always false, and a document that should have been excluded silently survives every check.

Drift at cosine 0.045 against a 0.8 threshold means the space moved almost completely. Both fingerprints claim the same provider ("openai") and the same dimension (384) — so a schema check would pass. Only the centroid comparison catches it. That is the scenario where a provider silently upgrades a model behind a stable endpoint name, and every query afterwards returns plausible neighbours from an incompatible space.

The seed is fixed at 15 so these numbers are reproducible. Without it the norms and the drift cosine change on every run, and the output you see would never match the page.

The count that matters most. Seven documents exist. One was withheld before indexing — the privileged employment contract. That is the first duty in a production review: privileged material must never enter a searchable index, not even one that is later deleted. Only six documents were indexed.

Why these three and not the others. The query was "multa por atraso na entrega conforme cláusula contratual". The three returned documents are the ones that mention the delay penalty: the original contract clause, the accounting reconciliation of the paid fine, and the internal disagreement about the deadline.

The score column is the cosine similarity. It is shown here because the scores field of the result comes back as zeros in version 1.9.23 — the ordering is correct, the score column is not populated. The example recomputes it so the output is readable.

This is the part a court can check. Three documents go to the opposing party. Three stay back — and for each one the engine computed a Cauchy–Schwarz upper bound below 0.477, the score of the third responsive document. That means DOC-0003, DOC-0005 and DOC-0007 could not belong in the responsive set for this query.

Notice what is in the withheld set: the board minutes approving a $48,000 payment, the 2024 vacation policy, and an invoice. The board minutes are arguably relevant to the dispute — which is exactly the point. The engine says they are not similar to this query, and it says so with arithmetic rather than a similarity score. If counsel disagrees, they can query differently; what they cannot say is that the search silently lost something.

Start with the number four. This patient has four clinical notes in the record. Not four hundred — four. That is realistic for a single admission, and it is the size at which the bound costs almost nothing (0.02 ms). The question is not whether the search is fast; it is whether the appeal can cite every note that supports the bill.

Why these three, in this order. The surgical description scores highest because it names the procedure directly — "apendicectomia videolaparoscópica". It is the document that answers the insurer's question in one line.

The first-day progress note comes second: it records the clinical reasoning that justified operating — pain for 18 hours, fever, raised white count, Blumberg sign. That is the medical necessity argument.

The discharge summary comes third: the final diagnosis, written after the fact, confirming what was done.

Notice the scores cluster tightly (0.558 to 0.466). That is expected in short clinical notes with overlapping vocabulary — and it is exactly the situation where an approximate index drops a neighbour without anyone noticing.

The one note that stays behind — and why it is provable. The excluded note is the 2026-03-04 post-operative progress note. It describes recovery, not justification for surgery. The engine computed its upper bound and found it below 0.466 — it could not belong in the top-3 for a query about the indication.

This distinction matters in an appeal. The hospital is not saying "we chose not to send that note". It is saying the note is not responsive to this question, and the arithmetic proves it.

An approximate search returns the same three notes and cannot write the second half of that sentence. When the payer challenges the search — and auditors do — the hospital has evidence rather than assurance.

The four returned clauses are the whole argument, in order. POL-0187 comes first because the operation exceeds $100,000 with no real guarantee — the query says so explicitly. PRE-0088 next: it is the precedent, a client approved at exactly 33% commitment. POL-0203 third: the exception clause that allows up to 35%.

POL-0142 — the 30% cap — comes last, and that is the correct ranking. It is the rule that was applied, but it is the least specific to this applicant's situation. The three above it are the reasons the rule might not apply.

Only two policies were excluded, and both for good reason: POL-0115 covers active credit-bureau restrictions — this applicant has none. POL-0264 covers income documentation for self-employed applicants — not the case here. The engine bounded both out below 0.713 and can show the arithmetic.

0.03 ms for six policies. The cost is not the point at this size. What the bank is buying is the sentence in the supervisory record: two policies were examined and excluded with proof, not merely skipped.

POL-0203 allows up to 35% commitment for clients with more than five years of relationship and no active restriction. The applicant has seven years, no restriction, and 33% commitment.

The retrieval surfaces it — and proves no other policy in the repository is responsive. Whether the denial was correct is a credit judgement; whether it was made on a complete reading of policy is now on the record.

17 excluded out of 400 looks wrong at first. If the answer is meant to be complete, why only 17? The answer is in a field this example does not print. Running the same query in audited mode returns bound_pairs: 400 — all 400 documents were examined. The 17 are the ones the bound alone proved outside the top-2. The other 381 were not excluded by the bound; they were resolved by exact score comparison in the postfilter and simply ranked below the cut.

That is why exact_global holds with only 17. The guarantee comes from the postfilter comparing every candidate exactly — not from the bound firing on all of them. The bound is a pruning accelerator; the exact comparison is the proof. A corpus where the bound never fires still returns an exact top-K.

Verified against brute force: this example's top-2 ([1, 301], both at 0.3938) is byte-identical to what a full cosine scan returns. The engine is not approximating here.

exact_global means the returned top-K is proven to be the global top-K, not merely the best within a truncated candidate pool. The recall_not_guaranteed flag from example 05 fires when a configuration can only offer pool_only — that is the case where this claim would be false.

The threshold of 0.3938 is the exact score of the second result, not a user-chosen cutoff. It is derived, and it moves with the query.

Each sampled record carries the bound computed for that document — 0.3854, 0.3913, 0.3876, all below 0.3938. That is the arithmetic an auditor re-runs. The sample is boundary-biased on purpose: it shows the documents closest to slipping through, which are the ones worth spot-checking.

73 of the 600 processes are emergency dispensations. They were generated from a fixed list of eight procurement types, and one of those types appears 73 times. The query was written to find exactly them.

With k=5 the example returns 5 of those 73. The engine is not wrong — the top-5 really is the top-5, verified identical to a brute-force scan. But a court of accounts that reads five processes and declares the audit complete has examined 7% of the matches. exact_global does not mean "I found everything relevant"; it means "the five I returned are provably the five closest, and the other 595 are provably further away".

Set k=73 and the answer changes completely: all 73 emergency processes come back, ranked 1 through 73. The guarantee was already exact at k=5 — the parameter that decides coverage is k, and it is the analyst's responsibility, not the engine's.

54 of the 500 clauses are early-termination clauses. The query was written to find them. With k=4 the example returns 4 — so 50 of the 54 risk clauses are never shown to the analyst.

The engine is not wrong. The top-4 is provably the exact top-4; that part is verified. What exact_global certifies is narrower than it sounds: the four I returned are correct, and the other 496 are provably further away. It does not certify that four is all there is.

An earlier draft of this page ended with "prova de que nenhuma cláusula de risco foi omitida". That sentence was false — the run omitted 50 of them. The example now prints the real count and the gap before it says anything about completeness.

The query was "provisão sem baixa ou documento de suporte". That asks two separate questions: 95 entries have provisions without write-off, 106 lack supporting documentation. An internal auditor reading that query wants both sets.

The combined query returned zero provisions. Not one of the five results came from condition A. All five are condition B. The embedding added both sides of the "ou" into a single vector and the result is a weighted average — and the average sits closer to the larger, longer, more token-dense condition.

This is not a bug in the engine. The top-5 is provably the exact top-5 for that vector. The bug is in translating a boolean query into a single embedding. Vector search has no set semantics: "A or B" is not A ∪ B, and "A and not B" is not representable at all.

The fix is two searches. One per condition, then union the document IDs. The example now demonstrates both and prints the difference, because an auditor who trusts the combined query would sign off having reviewed only half the risk.

The record is 4,347 bytes — not the full certificate. It carries the count, the threshold, a boundary sample of excluded documents, an integrity hash and the Ed25519 signature. That is small enough to store one per query in a WORM for years.

Changing 516 to 0 breaks the signature. Not the hash check, not a validation rule — the signature itself. The engine cannot rewrite its own past even if the whole binary is compromised, because the private key never lived inside it.

The third block is a different failure. The record is untouched; the verifier is using another issuer's public key. An auditor needs to tell "this document was altered" apart from "this is not the issuer's key" — both come back INVALID, and the reason string is what distinguishes them.

Every record points at the one before it. Record 3 carries the hash of record 2, record 4 carries record 3, and so on. That is the chain — not a list with signatures attached, but a structure where each element commits to its predecessor.

Deleting AUD-0004 breaks the link, not the signature. Records 1, 2, 3, 5 and 6 are each still individually valid — their Ed25519 signatures verify. What fails is the chain: record 5 says its predecessor was 5072a19a… and the verifier finds 7f7decd5… in its place. That mismatch is the evidence of removal.

The report localises the break. It does not say "something is wrong" — it names the block, the hash it expected and the hash it found. An auditor can point at the exact position in the history where the record was removed.

Two measurements, two different data sets. The first block uses pure gaussian noise: rank 236 of 256, and the projection returns the full vector. Noise has no low-dimensional structure, so there is nothing to find.

The control block answers the question that matters: does the method work at all? Same code, same vocabulary size, but the data generated from 40 latent factors. Result: rank 36 of 256 — a 7.1× reduction, with 96% of variance preserved.

Without the control, this example would be a failure report. Reading only the noise result, you cannot tell whether X-Factor is broken or whether the input has no structure. The control separates the two.

The round-trip is exact across five scripts, including Portuguese diacritics and Japanese — with no vocabulary file and no training. That is the actual claim, and it holds.

The state counts are the number to look at. 576 states for 9 characters is 64 per character. That is not a coincidence: the tokenizer emits embed_dim states per UTF-8 byte, so embed_dim=64 means 64× expansion by construction. At 1,960 bytes the text produced 125,440 states.

Compare that to a trained BPE: roughly 0.3 token per byte. This is about 213× less compact — the "about 1000×" figure in earlier drafts was in the right order of magnitude but never measured. The example now prints the real ratio.

The weight blend is trivially correct by inspection: 0.7·1 + 0.3·10 = 3.7. The float32 values print as 3.700000047683716 because that is the nearest representable float32, and the example compares with rel_tol=1e-6 rather than equality — the right way to check a float computation.

The build is 5 to 6× faster on the local machine — 237,9 ms against 1369,0 ms at 200,000 vectors. Same code, same seed, different CPU. Any single benchmark number without a machine attached is close to meaningless, so the page shows both.

What holds on both machines is the shape of the curve: build cost per 1,000 documents falls as the corpus grows — 10,90 → 6,85 ms on Colab, 3,87 → 1,19 ms locally. Fixed overhead amortises; the build is linear in corpus size, not quadratic.

Query latency against brute force is a different story on each. On Colab, Madhava beats brute force at every size (48,22 ms against 66,07 ms at 200,000). Locally brute force wins above 10,000 vectors (8,91 ms against 21,80 ms) — the numpy BLAS path is simply faster on a wide desktop CPU than the bound scan.

That difference is worth stating plainly: the "Madhava is competitive with exact scan up to ~50,000 vectors" claim depends on the hardware. It holds on the Colab CPU and does not hold on a fast desktop. The guarantee is identical either way; the latency comparison is not.