docs(glossary): add concept map, citations, PIST classifier entries

New sections: Concept Map & Academic Citations, PIST Trace Classifier.
Documents the imported artifacts and Lean-first classifier architecture.
This commit is contained in:
allaun 2026-06-21 16:51:58 -05:00
parent 7d7c85f475
commit e16c967ba3

View file

@ -153,6 +153,26 @@ name and explains the delta.
| **QUBOLib** | Planned library layer for QUBO/QAOA optimization bridges. | `PORTING_MAP.md` |
| **PVGSLib** | Planned library layer for photon-varied Gaussian state bridges. | `PORTING_MAP.md` |
## Concept Map & Academic Citations
| Term | Definition | Source module |
|------|------------|---------------|
| **Concept Map** | JSONL artifact mapping files to extracted concepts with types, tags, dependencies, and summaries. 822 local + 752 Drive files. | `docs/concept_map/` |
| **Cornfield Concepts** | 48 formally grounded concepts with academic citations, novelty classification, and novelty_statements. | `extraction/cornfield_concepts.json` |
| **concept_citations** | Postgres table linking concepts to papers via paper_id, doi, title, authors, year, journal, relation_type. | neon-64gb `arxiv` DB |
| **paper_refs** | JSONB column storing structured citation array on math_objects. | neon-64gb `arxiv` DB |
| **is_novel_claim** | Boolean flag: true = original work, no prior paper covers exactly this. Requires novelty_statement. | neon-64gb `arxiv` DB |
| **relation_type** | Citation edge: `grounds` (foundational), `extends` (builds on), `applies` (application), `cites` (general). | neon-64gb `arxiv` DB |
| **Jaccard Matcher** | Script finding arxiv papers for concepts via keyword overlap against 700k papers. | `jaccard_matcher.py` |
## PIST Trace Classifier
| Term | Definition | Source module |
|------|------------|---------------|
| **PistClassifyTrace** | Lean executable reading trace JSON, computing spectral features with Q16_16, applying RRC shape thresholds, inferring tactic family. | `PistClassifyTrace.lean` |
| **Spectral Profile** | 10-feature Q16_16 vector from transition matrix: matrix_size, rank, spectral_gap, density, trace, frobenius, laplacian_zero_count, eigenvalue_max, etc. | `PistClassifyTrace.lean` |
| **Tactic Family** | Classification: rewrite, normalization, arithmetic, induction, algebraic, case_analysis, discharge, reflexivity, unknown. | `PistClassifyTrace.lean` |
## Infrastructure terms
| Term | Definition | Source module |