# Corpus and verified pairs — vector_behavior

Companion to the theorem/embedding/proof bundle already in this repo.

| file | contents |
|---|---|
| `corpus.jsonl.gz` | all 180,907 Mathlib declarations with source `code`, one JSON object per file: `{path, imports, premises:[{full_name, code, start, end, kind}]}` |
| `real_pairs_verified.json.gz` | 7,731 verified pairs over 1,666 substitutions, plus per-relation precision for the old name-matched pairs |
| `llm_judge.json` | blinded LLM verdicts on discovered groups, with decoy floors |
| `pca_view.json` | 2,761 arrows projected on the duality and strictness axes, and on PCA |
| `verified_relations.json` | every relation re-measured on verified pairs vs all pairs |
| `strictness_axis.json` | the strictness-axis test with bootstrap intervals |
| `ablation_relations*.json` | name-stripping ablation, e5-large and e5-mistral |
| `normalisation.json` | preprocessing study with a pre-registered decision rule |

## The pairs

```python
import gzip, json
vp = json.load(gzip.open("real_pairs_verified.json.gz", "rt"))

for a, b, from_tok, to_tok in vp["pairs"][:5]:
    print(f"{from_tok} -> {to_tok}:  {a}  |  {b}")

vp["top_substitutions"][:10]   # the substitutions Mathlib actually attests
vp["rule_precision"]           # how good the old name-matched pairs were
```

A pair is here if one token can be substituted throughout A's statement to give B's,
with nothing else changed and declaration names deleted before matching. No embedding
and no proof was consulted, so the set is usable as ground truth for either.

Precision is a **lower bound on relatedness**: a pair can be genuine without being a
one-substitution match, since statements also differ in binders and `add→mul` usually
travels with `zero→one`. Trust the ranking, not the level.

## The corpus

```python
import gzip, json
for line in gzip.open("corpus.jsonl.gz", "rt"):
    f = json.loads(line)
    for p in f["premises"]:
        if "@[to_additive" in p["code"]:
            print(p["full_name"])
```

180,907 declarations against the bundle's 99,552 theorem statements — the extra ~81,000
are definitions, instances and structures. Note that `@[to_additive]` twins are
generated by the compiler and are **not** separate declarations here: of 9,602 marked
declarations only 157 have a resolvable partner in the corpus and 12 have both halves
embedded. That route to ground-truth pairs is a dead end, which is why the
substitution matcher above exists.

## Please read this before using either file

Both are answer keys, and the study they come from depends on their being held back.

Proofs validate discovery *because* no encoder ever saw one. The verified pairs
validate the pairing step *because* they were not used to build it. Use either to find
structure and then confirm with the same thing, and you have proved nothing. Validate
with something else: human judgement, a held-out corpus, or the source organisation.