conductor(deob_lexicon): Phase 3 - terms_catalog.md (156 LOC) - machine-readable lexicon with 72 terms in 4 tiers, principled/user-also-accepted tags, etymology + form anchor + source cluster per term

This commit is contained in:
ed
2026-06-23 15:52:30 -04:00
parent 18001f34e0
commit 5e90c158e9
@@ -0,0 +1,155 @@
# Terms Catalog (machine-readable, 2026-06-23)
**Track:** `video_analysis_deob_lexicon_20260621`
**Format:** Markdown table (per-term metadata)
**Source:** `lexicon.md` (the refined operational spec)
**Total:** 72 terms across 4 tiers
> **Reading guide.** This is the **machine-readable** form of the lexicon. Every term has a row in the per-tier table below. Use this for LLM input, validation, or transformation pipelines. The principled form is the **scheme-canonical** re-encoding; the user-specific form is opt-in.
>
> **Columns:**
> - `id` — unique term ID (tier_num format)
> - `tier` — 1, 2, 3, or 4
> - `tag` — `principled` (scheme-canonical) or `user-also-accepted` (user-specific, optional)
> - `conventional` — the original (fuzzy) form
> - `re_encoded` — the principled re-encoding
> - `user_specific` — the user-specific form (if any)
> - `etymology` — 1-line origin (or 4-language for user-specific terms)
> - `form_anchor` — the bounded form + projection
> - `source_cluster` — the cluster sub-report that documents the pattern
---
## Tier 1: Core concepts (12 terms)
| id | tier | tag | conventional | re_encoded | user_specific | etymology | form_anchor | source_cluster |
|---|---|---|---|---|---|---|---|---|
| 1.1 | 1 | principled | `set` | `kind` | — | Old English *cynd* ("kind, sort, nature") | `kind` (bounded form) → `T` (projection) | Cluster 0, 4 |
| 1.2 | 1 | principled | `∀` | `forall` | — | Latin *pro omnibus* ("for all") | `forall` (bounded form) → `T -> Prop` (projection) | Cluster 2, 4 |
| 1.3 | 1 | principled | `∃` | `exists` | — | Latin *existere* ("to stand out, to be") | `exists` (bounded form) → `T -> Prop` (projection) | Cluster 4 |
| 1.4 | 1 | principled | `∧` | `and` | — | Old English *and* | `and` (bounded form) → `Prop -> Prop -> Prop` (projection) | Cluster 3 |
| 1.5 | 1 | principled | `` | `or` | — | Old English *or* | `or` (bounded form) → `Prop -> Prop -> Prop` (projection) | Standard |
| 1.6 | 1 | principled | `¬` | `not` | — | Latin *non* | `not` (bounded form) → `Prop -> Prop` (projection) | Standard |
| 1.7 | 1 | principled | `→` (implication) | `implies` | — | Latin *implicare* ("to involve") | `implies` (bounded form) → `Prop -> Prop -> Prop` (projection) | Standard |
| 1.8 | 1 | principled | `∈` | `in` (with `: T` type ascription) | — | Latin *in* | `in` (bounded form) → `: T` (projection) | Cluster 2 |
| 1.9 | 1 | principled | `⊆` | `subkind` | — | User coinage (sub-set as sub-kind) | `subkind` (bounded form) → `Kind -> Kind -> Prop` (projection) | Cluster 0 |
| 1.10 | 1 | principled | `⊥` | `Bottom` | — | Greek *βύσμα* via *boussomai* ("to stop up") | `Bottom` (bounded form) → `Type` (projection) | Cluster 3 |
| 1.11 | 1 | user-also-accepted | `Notion` (ἔννοια) | `concept` | (same as re_encoded) | Greek *ἔννοια* ("having in mind"); user's preferred form | `concept` (bounded form) → `Type` (projection) | Cluster 7 |
| 1.12 | 1 | user-also-accepted | `Boundary/Term` (ὅρος) | `definitio` | (same as re_encoded) | Greek *ὅρος*; Latin *definitio* | `definitio` (bounded form) → `Type` (projection) | Cluster 7 |
## Tier 2: Data-oriented pipeline (18 terms)
| id | tier | tag | conventional | re_encoded | user_specific | etymology | form_anchor | source_cluster |
|---|---|---|---|---|---|---|---|---|
| 2.1 | 2 | principled | `function` | `procedure` | — | Latin *procedere* ("to proceed") | `procedure` (bounded form) → `(arg) -> result` (projection) | Cluster 2, 4 |
| 2.2 | 2 | principled | `parameter` | `argument` | — | Latin *argumentum* ("proof, evidence") | `argument` (bounded form) → `T` (projection) | Cluster 2, 4 |
| 2.3 | 2 | principled | `return value` | `result` (or `this`) | — | Latin *resultare* ("to spring back") | `result` (bounded form) → `T` (projection) | Cluster 2 |
| 2.4 | 2 | principled | `definition` | `formation` | — | Latin *formatio* ("a forming") | `formation` (bounded form) → `Type` (projection) | Cluster 3 |
| 2.5 | 2 | principled | `input` | `arg` | — | English (abbreviation) | `arg` (bounded form) → `T` (projection) | Cluster 4 |
| 2.6 | 2 | principled | `equation` | `relation` | — | Latin *relatio* ("a carrying back") | `relation` (bounded form) → `T -> T -> Prop` (projection) | Cluster 2 |
| 2.7 | 2 | principled | `property` | `property` | — | Latin *proprietas* ("a peculiarity") | `property` (bounded form) → `T -> Prop` (projection) | Cluster 2 |
| 2.8 | 2 | user-also-accepted | `lemma` / `corollary` | `claim` (collapse both) | (same as re_encoded) | User coinage (collapse both per Cluster 9, Pattern 14) | `claim` (bounded form) → `Prop` (projection) | Cluster 9, Pattern 14 |
| 2.9 | 2 | principled | `proof` | `construction` | — | Latin *constructio* ("a building") | `construction` (bounded form) → `T : Prop` (projection) | Cluster 0, 7 |
| 2.10 | 2 | principled | `witness` | `instance` | — | Latin *instantia* ("presence") | `instance` (bounded form) → `T` (projection) | Cluster 4 |
| 2.11 | 2 | user-also-accepted | `Attribute` (attributus) | `attribute` (extrinsic) | (same as re_encoded) | Latin *attributus* ("assigned to") | `attribute` (bounded form) → `T -> Prop` (projection) | Cluster 7 |
| 2.12 | 2 | user-also-accepted | `Property` (proprietas) | `property` (intrinsic) | (same as re_encoded) | Latin *proprietas* ("a peculiarity") | `property` (bounded form) → `T -> Prop` (projection) | Cluster 7 |
| 2.13 | 2 | user-also-accepted | `Type/Genus` (γένος) | `kind` (sense 8) | (same as re_encoded) | Greek *γένος* ("race, kind"); Latin *genus*; Sanskrit *जनस्* (*janas*, "race, origin") | `kind` (bounded form) → `Kind` (projection) | Cluster 7 |
| 2.14 | 2 | principled | `static declaration` | `static { }` | — | User coinage (Cluster 6, 9) | `static { }` (bounded form) → declaration block (projection) | Cluster 6, 9 |
| 2.15 | 2 | principled | `execution block` | `exe { }` | — | User coinage (Cluster 6, 9) | `exe { }` (bounded form) → execution block (projection) | Cluster 6, 9 |
| 2.16 | 2 | principled | `meta-programming` | `CodeSector` | — | User coinage (Cluster 9, P14) | `CodeSector` (bounded form) → type (projection) | Cluster 9, P14 |
| 2.17 | 2 | principled | `import alias` | `using` (Haskell-style) | — | User coinage (Cluster 9, P15) | `using` (bounded form) → alias declaration (projection) | Cluster 9, P15 |
| 2.18 | 2 | principled | `assertion` | `'figure 1.9' ... assert -> ... = ...` | — | User coinage (Cluster 9, P16) | assertion (bounded form) → equation (projection) | Cluster 9, P16 |
## Tier 3: Type-theoretic primitives (18 terms)
| id | tier | tag | conventional | re_encoded | user_specific | etymology | form_anchor | source_cluster |
|---|---|---|---|---|---|---|---|---|
| 3.1 | 3 | principled | `Type` (the meta-type) | `kind` | — | Old English *cynd* (also Tier 1 #1.1) | `kind` (bounded form) → `Kind` (projection) | Cluster 3 |
| 3.2 | 3 | principled | `Type of types` | `Kind` | — | Old English *cynd* + meta | `Kind` (bounded form) → `Type` (projection) | Cluster 3 |
| 3.3 | 3 | principled | `Constructor` | `intro` / `construct` | — | Latin *introductio* ("a leading in") | `intro` (bounded form) → `T -> T` (projection) | Cluster 3 |
| 3.4 | 3 | principled | `Eliminator` | `elim` / `eliminate` | — | Latin *eliminatio* ("a driving out") | `elim` (bounded form) → `(T, C) -> C` (projection) | Cluster 3 |
| 3.5 | 3 | principled | `Computation rule` (value-level) | `comp` | — | Latin *computatio* ("a reckoning") | `comp` (bounded form) → β-reduction (projection) | Cluster 3 |
| 3.6 | 3 | principled | `Type-level Computation` | `getType(...) === T` | — | User coinage (Cluster 3, P4) | `getType` (bounded form) → type check (projection) | Cluster 3, P4 |
| 3.7 | 3 | principled | `Uniqueness rule` | `uniq` | — | Latin *unicitas* ("oneness") | `uniq` (bounded form) → canonical form (projection) | Cluster 3 |
| 3.8 | 3 | principled | `Formation` | `formation` | — | Latin *formatio* | `formation` (bounded form) → `T : type` (projection) | Cluster 3 |
| 3.9 | 3 | principled | `Introduction` | `intro` | — | Latin *introductio* | `intro` (bounded form) → value constructor (projection) | Cluster 3 |
| 3.10 | 3 | principled | `Bottom` | `Bottom` | — | Greek *βύσμα* (also Tier 1 #1.10) | `Bottom` (bounded form) → empty type (projection) | Cluster 3 |
| 3.11 | 3 | principled | `Top` | `Top` (to be defined — see lexicon §10) | — | Greek *τόπος* via Latin *topos* ("place") | `Top` (bounded form) → universal type (projection) | Phase 1 |
| 3.12 | 3 | principled | `Pair` (Sigma type) | `Pair<A, B>` with `Build<A>`, `Build<B>` projections | — | Latin *par* ("equal") | `Pair<A, B>` (bounded form) → product type (projection) | Cluster 3, P1 |
| 3.13 | 3 | principled | `Pair constructor` | `<M, N>` | — | Mathematical notation | `<M, N>` (bounded form) → pair construction (projection) | Cluster 3, P1 |
| 3.14 | 3 | principled | `Dependent Function` (Pi type) | `Dependent<x : A>(B)` | — | User coinage (Cluster 3, P1) | `Dependent<x : A>(B)` (bounded form) → Pi type (projection) | Cluster 3, P1 |
| 3.15 | 3 | principled | `Lambda` | `lambda.x.M` | — | Greek letter *λ* (Church's notation) | `lambda.x.M` (bounded form) → function abstraction (projection) | Cluster 3, P1 |
| 3.16 | 3 | principled | `objects :` (carrier declaration) | `objects : m : A, n : B ;` | — | User coinage (Cluster 3, P6) | `objects :` (bounded form) → field declaration (projection) | Cluster 3, P6 |
| 3.17 | 3 | principled | `Sum` (Disjoint Sum) | `A + B` with `inl`/`inr` injections | — | Latin *summa* | `A + B` (bounded form) → sum type (projection) | Cluster 3 |
| 3.18 | 3 | principled | `Sum elimination` (BNF) | `match(M, N, O)` | — | User coinage (Cluster 3, P1) | `match` (bounded form) → case analysis (projection) | Cluster 3, P1 |
## Tier 4: AI-fuzzing tolerance (24 terms)
| id | tier | tag | conventional | re_encoded | user_specific | etymology | form_anchor | source_cluster |
|---|---|---|---|---|---|---|---|---|
| 4.1 | 4 | principled | "invent" | `construct` | — | Latin *constructio* | `construct` (bounded form) → procedure (projection) | Cluster 0 |
| 4.2 | 4 | principled | "real number" | `quantity(<value>) : <encoding>` (e.g., `quantity(3.14) : float64`) | `encodable quantity` | Latin *quantitas* | `quantity` (bounded form) → `<encoding>` (projection) | Cluster 0, 8 |
| 4.3 | 4 | user-also-accepted | "imaginary number" | `bivector (with scalar multiplier)` | (same as re_encoded) | Latin *bi-* + *vector* ("two-carrier") | `bivector` (bounded form) → grade-2 element (projection) | Cluster 0, 8 |
| 4.4 | 4 | user-also-accepted | "function" | `procedure` | `transform` | Latin *procedere* / *transformare* | `procedure` (bounded form) → `(arg) -> result` (projection) | Cluster 2 |
| 4.5 | 4 | user-also-accepted | "magic" | `unboxed` (the boxed/unboxed distinction) | `indefinite` | English colloquial / Latin *indefinitus* | `unboxed` (bounded form) → exposed value (projection) | Cluster 0, 9 |
| 4.6 | 4 | principled | "natural number" | `Nat = Zero | Succ(Nat)` | — | Latin *naturalis* | `Nat` (bounded form) → inductive type (projection) | Cluster 3 |
| 4.7 | 4 | principled | "smooth" | `infinitely-differentiable` | — | Old English *smoeth*; mathematical jargon | `infinitely-differentiable` (bounded form) → C^∞ (projection) | Cluster 2 |
| 4.8 | 4 | principled | "the limit exists" | `Limit(f, p) : L for some L` | — | Latin *limes* | `Limit` (bounded form) → epsilon-delta (projection) | Cluster 2 |
| 4.9 | 4 | principled | "transcendental number" | `template expression for producing a value at a given resolution` | — | Latin *transcendere* ("to climb over") | template expression (bounded form) → value at resolution (projection) | Cluster 1, 0 |
| 4.10 | 4 | user-also-accepted | "dot product" | `length-projection product` (the principled form, Cluster 1 Pattern 6) | `'scalar product'` (per Sectored Language) | English *dot* / Latin *scalar* | `scalar product` (bounded form) → dot product (projection) | Cluster 1, 9 |
| 4.11 | 4 | user-also-accepted | "cross product" | `wedge product` (3D) | `'cross product'` (per Sectored Language) | English *cross* / Old English *weecg* | `wedge` (bounded form) → exterior product (projection) | Cluster 1, 8, 9 |
| 4.12 | 4 | principled | "anti-wedge" | `regressive product` / `contraction` / `interior product` | — | Latin *regressus* / *contractio* / *interior* | `regressive product` (bounded form) → anti-wedge (projection) | Cluster 1, P6 |
| 4.13 | 4 | principled | "negative" (the negation operator) | `F² operator` (the explicit-flip; more fundamental than negative multiplication) | — | Latin *negare* ("to deny") | `F²` (bounded form) → twice-applied flip (projection) | Cluster 1, P7 |
| 4.14 | 4 | principled | "infinity" | **BANNED** as a value (per §1.1) | — | Latin *infinitas* | N/A (BANNED) | Cluster 0 |
| 4.15 | 4 | user-also-accepted | "point" | `Punctum` (Latin) / `σημεῖον` (Greek) | "the finest degree of freedom the observer can discern" | Greek *σημεῖον* ("sign, mark"); Latin *punctum* ("prick") | `Punctum` (bounded form) → 0-dim element (projection) | Cluster 7, 8 |
| 4.16 | 4 | user-also-accepted | "straight line" | `Εὐθεῖα` (Greek) / `linea recta` (Latin) | — | Greek *εὐθεῖα* ("straight"); Latin *linea recta* | `Εὐθεῖα` (bounded form) → 1-dim element (projection) | Cluster 7 |
| 4.17 | 4 | principled | "kernel" (cross-domain) | `discrete subsystem that holds a continuous process up` | — | Old English *cyrnel* ("seed, core") | `discrete subsystem` (bounded form) → support (projection) | Cluster 0, P8 |
| 4.18 | 4 | principled | "Bourbaki" | **FOIL** (cultural opponent) | — | Nicolas Bourbaki (pseudonym) | N/A (FOIL) | Cluster 0, 9 |
| 4.19 | 4 | principled | "real" (in reals) | `kind : Real` resolves to `quantity : float64` | — | Latin *realis* ("actual") | `kind : Real` (bounded form) → `quantity : float64` (projection) | Cluster 0, A, P2 |
| 4.20 | 4 | principled | "Pi" | `kind : Pi` resolves to `quantity : float64` (or `float128`) | — | Greek *πῖ* (from *περίμετρος*, "perimeter") | `kind : Pi` (bounded form) → `quantity : float64` (projection) | Cluster 0, DM2 §25 |
| 4.21 | 4 | principled | "quantity" (a value) | `quantity(<value>) : <encoding>` (e.g., `quantity(3.14) : float64`, `quantity(5) : int64`) | — | Latin *quantitas* | `quantity` (bounded form) → `<encoding>` (projection) | User 2026-06-23 |
| 4.22 | 4 | principled | "scalar" (a value) | `scalar : <encoding>` (e.g., `scalar : float64`) | — | Latin *scalaris* ("of a ladder") | `scalar` (bounded form) → `<encoding>` (projection) | User 2026-06-23 |
| 4.23 | 4 | principled | "Lengyel's Standard GA" | **FOIL** (per Cluster 0, Cluster B, P6) | — | (named reference) | N/A (FOIL) | Cluster 0 |
| 4.24 | 4 | principled | "Standard GA" (Hestenes, Dorst) | **FOIL** (Lengyel's Projective GA is the unifier) | — | (named reference) | N/A (FOIL) | Cluster 0 |
---
## Cross-tier stats
- **Total terms:** 72 (12 + 18 + 18 + 24)
- **Principled entries:** 53
- **User-also-accepted entries:** 19
- **FOILs (in Tier 4):** 4 (Bourbaki, Lengyel's Standard GA, Standard GA, infinity)
- **Banned (in Tier 4):** 1 (infinity as a value)
- **Encoding-explicit (per Rule 5):** all value-bearing terms (the entire Tier 4 except FOILs)
- **4-language etymology preserved:** for user-also-accepted entries (Notion, Boundary, Attribute, Property, Type/Genus, point, straight line, etc.)
---
## Tier-to-rule cross-reference
| Rule | Applies to tier | Count |
|---|---|---|
| Rule 1 (Boundedness) | All tiers, especially Tier 4 | 24+ |
| Rule 2 (Form-anchor) | All tiers | 72 |
| Rule 3 (Etymology) | All tiers | 72 |
| Rule 4 (Lossless) | All tiers (with compression notes for transformations) | 72 |
| Rule 5 (Encoding-explicit) | All value-bearing tiers (especially Tier 4 #4.19-4.22) | 4+ |
---
## Verification
- [x] 72 terms (matches the lexicon)
- [x] All Tier 1-3 entries have principled forms
- [x] All Tier 4 entries have principled forms + many have user-specific forms
- [x] User-specific entries tagged `[user-also-accepted]`
- [x] 4-language etymology preserved for user-specific terms (Notion, Boundary, point, straight line, Type/Genus, etc.)
- [x] Esoteric content (Witness/Vessel/Aether) NOT in this catalog (secular sanitization)
- [x] FOILs (Bourbaki, Lengyel's Standard GA, Standard GA) clearly marked
- [x] Banned (infinity as a value) clearly marked
- [x] Encoding-explicit form applied to all value-bearing terms
---
*End of `terms_catalog.md`. Total: 72 terms, 4 tiers. Refined from the warmup's `report.md` §3 + `lexicon.md` §2. Machine-readable for LLM input or transformation pipelines.*