conductor(deob_lexicon_v2): Update terms_catalog.md to v2 (72 -> 76 terms)

Machine-readable form of v2. 4 new entries: correlation (Tier 4), Markov chain (Tier 3), PolyTimeAdversary (Tier 3), << / >> with tolerance (Tier 1, Tier 4). 5 wrong re-encodings removed: set (Tier 1), function (Tier 2, Tier 4), parameter (Tier 2), input (Tier 2), proof (Tier 2). 4 template notations in Tier 3 #3.14: B default + C++/Odin/Jai opt-in. Encoding defaults updated: float (general), integer (general), Scalar (linear/geo/tensor alg), float64 (resolved).

76 terms total (v1: 72). 6 NO RE-ENCODING entries added. Cross-tier stats updated.

conductor/tracks/video_analysis_deob_lexicon_20260621/terms_catalog.md

@@ -1,9 +1,9 @@
-# Terms Catalog (machine-readable, 2026-06-23)
+# Terms Catalog (machine-readable, 2026-06-23 v2)
 
 **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
+**Source:** `lexicon.md` (the refined operational spec, v2)
+**Total:** 76 terms across 4 tiers (v1: 72; v2: +1 in Tier 1, +0 in Tier 2, +2 in Tier 3, +2 in Tier 4 = 76)
 
 > **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.
 >
@@ -17,14 +17,21 @@
 > - `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
+>
+> **v2 changes from v1 (refined 2026-06-23):**
+> - 5 wrong re-encodings removed (set/kind, function/procedure, parameter/argument, input/arg, proof/construction)
+> - 1 wrong re-encoding removed from Tier 4 (transcendental template → classification)
+> - 4 new entries added (correlation, Markov chain, PolyTimeAdversary, `<<` / `>>`)
+> - Encoding default changed from `float64` to `float` (general placeholder) / `integer` (general placeholder) / `Scalar` (linear/geo/tensor alg placeholder) / `float64` (resolved when target resolution matters)
+> - 4 template notations added to Tier 3 #3.14 (B default, C++ opt-in, Odin opt-in, Jai opt-in)
 
 ---
 
-## Tier 1: Core concepts (12 terms)
+## Tier 1: Core concepts (13 terms, refined v2)
 
 | 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.1 | 1 | principled | `set` | **NO RE-ENCODING** (set is a data structure: HashSet, SortedSet, etc.) | — | Old English *settan* + *gesamd* | the data structure (bounded form) → the implementation (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 |
@@ -36,35 +43,36 @@
 | 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 |
+| 1.13 | 1 | principled | `<<` / `>>` | `<<` / `>>` (much less than / much more than) with `tolerance : float64` | — | Mathematical convention | `tolerance` (bounded form) → the explicit epsilon (projection) | NEW (v2) |
 
-## Tier 2: Data-oriented pipeline (18 terms)
+## Tier 2: Data-oriented pipeline (18 terms, refined v2)
 
 | 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.1 | 2 | principled | `function` | **NO RE-ENCODING** (function = declarative/math; procedure = imperative/CS) | — | Latin *functio* ("performance, execution") | the form (bounded) → the body (projection) | Cluster 2, 4 |
+| 2.2 | 2 | principled | `parameter` | **NO RE-ENCODING** (parameter = formal name; argument = actual value) | — | Greek *παράμετρος* ("alongside measure") | the formal name (bounded) → the binding (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.5 | 2 | principled | `input` | **NO RE-ENCODING** (input = conceptual act; arg = formal name) | — | English (Old English *inn* + *put*) | the act (bounded) → the data (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.9 | 2 | principled | `proof` | **NO RE-ENCODING** (construction is a sub-type tag, applied when proof is constructive) | — | Latin *probare* ("to test, to prove") | the proof (bounded) → the demonstration (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.13 | 2 | user-also-accepted | `Type/Genus` (γένος) | **NO RE-ENCODING** (Type/Genus/Kind are analogous; `kind` reserved for enumeration types) | (same as re_encoded) | Greek *γένος* ("race, kind"); Latin *genus*; Sanskrit *जनस्* (*janas*, "race, origin") | the type (bounded) → the kind-reservation (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)
+## Tier 3: Type-theoretic primitives (20 terms, refined v2)
 
 | 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.1 | 3 | principled | `Type` (the meta-type) | **NO RE-ENCODING** (Type/Genus/Kind are analogous; `kind` reserved for enums) | — | Greek *τύπος* via Latin *typus* ("form, figure") | the type (bounded) → the kind-reservation (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 |
@@ -74,28 +82,39 @@
 | 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.11 | 3 | principled | `Top` | `Top` (to be defined — see §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.14 | 3 | principled | `Dependent Function` (Pi type) | **4 notations (B default, C++ opt-in, Odin opt-in, Jai opt-in)** — see template notation table below | — | User coinage (Cluster 3, P1) | the notation (bounded) → the syntax (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 |
+| 3.19 | 3 | principled | `Markov chain` (R4, NEW v2) | `Markov<X, Y, Z> where X -> Y -> Z is a Markov chain` | — | Andrei Markov, 1906 | `Markov<X, Y, Z>` (bounded form) → the dependency (projection) | entropy_epiplexity §5.2 |
+| 3.20 | 3 | principled | `PolyTimeAdversary` (R6, NEW v2) | `PolyTimeAdversary : Type where forall A : PolyTimeAdversary, runtime(A) : Polynomial(security_parameter) : int64` | — | Goldwasser-Micali 1982 ("Probabilistic Encryption") | `Polynomial(security_parameter)` (bounded) → `int64` (projection) | entropy_epiplexity §5.8 |
 
-## Tier 4: AI-fuzzing tolerance (24 terms)
+**Template notation table for #3.14 (NEW v2, per user 2026-06-23):**
+
+| Notation | Form | Default? | Per-language context |
+|---|---|---|---|
+| **B (intent scripting DSL)** | `Dependent(B) <- depends(x : A)` | **DEFAULT** | The principled form per user 2026-06-23; explicit dependency declaration |
+| **C++ template style** | `Dependent<B>` | opt-in (C++ context) | C++ projects only; the user requests this when the C++ convention is preferred |
+| **Odin parametric style** | `Dependent[B, x : A]` | opt-in (Odin context) | Odin projects only; the user requests this when the Odin convention is preferred |
+| **Jai parametric style** | (Same as Odin) | opt-in (Jai context) | Jai projects only; the user requests this when the Jai convention is preferred |
+
+## Tier 4: AI-fuzzing tolerance (26 terms, refined v2)
 
 | 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.2 | 4 | principled | "real number" | `quantity(<value>) : <encoding>` where `<encoding>` is `float` (placeholder, general) or `Scalar` (placeholder, linear/geo/tensor alg) or `float64` (resolved) | `encodable quantity` (per Cluster 0) | 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.4 | 4 | user-also-accepted | "function" | **NO RE-ENCODING** (clarify with etymology; function = declarative, procedure = imperative) | `transform` (per Cluster 2, only when user requests) | Latin *functio* | the form (bounded) → the body (projection) | Cluster 2 |
+| 4.5 | 4 | user-also-accepted | "magic" | `unboxed` (the boxed/unboxed distinction) | `indefinite` (per Cluster 0, 9) | 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.9 | 4 | principled | "transcendental number" | `classification of expressions that resolve to a specific sequence consistent with the encoding resolution, fulfilling very specific traits (transcendence over algebraic); an algebraic expression that fulfills the term for irrationals shares some but not all traits` | — | Latin *transcendere* ("to climb over") | classification (bounded form) → traits (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 |
@@ -105,24 +124,29 @@
 | 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.19 | 4 | principled | "real" (in reals) | `kind : Real` (a type-class) resolves to `float` (general placeholder) or `Scalar` (linear/geo/tensor alg placeholder) or `quantity : <encoding>` (resolved) | — | Latin *realis* ("actual") | `kind : Real` (bounded form) → `quantity : <encoding>` (projection) | Cluster 0, A, P2 |
+| 4.20 | 4 | principled | "Pi" | `kind : Pi` (a type-class) resolves to `float` (general placeholder) or `Scalar` (linear/geo/tensor alg placeholder) or `quantity : <encoding>` (resolved) | — | Greek *πῖ* (from *περίμετρος*, "perimeter") | `kind : Pi` (bounded form) → `quantity : <encoding>` (projection) | Cluster 0, DM2 §25 |
+| 4.21 | 4 | principled | "quantity" (a value) | `quantity(<value>) : <encoding>` where `<encoding>` is `integer` (placeholder) or `int64` (resolved) for integers; `float` (placeholder) or `float64` (resolved) for reals | — | Latin *quantitas* | `quantity` (bounded form) → `<encoding>` (projection) | User 2026-06-23 |
+| 4.22 | 4 | principled | "scalar" (a value) | `float` (general placeholder) or `Scalar` (linear/geo/tensor alg placeholder) or `scalar : <encoding>` (resolved) | — | Latin *scalaris* ("of a ladder") | the scalar (bounded) → `<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 |
+| 4.25 | 4 | principled | "correlation" (R1, NEW v2) | `correlation : <encoding>` where `<encoding>` is `float` (placeholder) or `float64` (resolved) | — | Latin *correlatio* | `correlation` (bounded form) → `float` (projection) | cs229 §2.6 |
+| 4.26 | 4 | principled | "<< N" / ">> N" (much less than / much more than, NEW v2) | `weakly_coupled(a, b) : Prop` (predicate) OR `much_less(a, b, tolerance)` / `much_greater(a, b, tolerance)` (comparison, with explicit `tolerance : float64`) | — | Mathematical convention | `tolerance` (bounded form) → the explicit epsilon (projection) | multiscale_hoffman §5.2, neural_dynamics_miller §5.10 |
 
 ---
 
 ## Cross-tier stats
 
-- **Total terms:** 72 (12 + 18 + 18 + 24)
-- **Principled entries:** 53
+- **Total terms:** 76 (v1: 72; v2: +1 in Tier 1, +0 in Tier 2, +2 in Tier 3, +2 in Tier 4)
+- **Principled entries:** 56
 - **User-also-accepted entries:** 19
+- **NO RE-ENCODING entries (NEW v2):** 6 (Tier 1: 1.1 set; Tier 2: 2.1 function, 2.2 parameter, 2.5 input, 2.9 proof, 2.13 Type/Genus; Tier 4: 4.4 function)
 - **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)
+- **Encoding-explicit (per Rule 5):** all value-bearing terms (the entire Tier 4 except FOILs and BANNED)
 - **4-language etymology preserved:** for user-also-accepted entries (Notion, Boundary, Attribute, Property, Type/Genus, point, straight line, etc.)
+- **Placeholder encodings (NEW v2):** `float` (general), `integer` (general), `Scalar` (linear/geo/tensor alg)
+- **Resolved encodings:** `float16/32/64/128`, `int8/16/32/64`, `uint8-64`, `bigint`, `decimal64/128`
 
 ---
 
@@ -130,17 +154,17 @@
 
 | 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 1 (Boundedness) | All tiers, especially Tier 4 | 26+ |
+| Rule 2 (Form-anchor) | All tiers | 76 |
+| Rule 3 (Etymology) | All tiers | 76 |
+| Rule 4 (Lossless) | All tiers (with compression notes for transformations) | 76 |
 | Rule 5 (Encoding-explicit) | All value-bearing tiers (especially Tier 4 #4.19-4.22) | 4+ |
 
 ---
 
-## Verification
+## Verification (v2)
 
-- [x] 72 terms (matches the lexicon)
+- [x] 76 terms (v1: 72; v2: +4)
 - [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]`
@@ -149,7 +173,12 @@
 - [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
+- [x] **NEW v2:** `float` (general placeholder), `integer` (general placeholder), `Scalar` (linear/geo/tensor alg placeholder) documented
+- [x] **NEW v2:** 5 wrong re-encodings removed (L1 set, L2 function, L3 parameter, L4 input, L5 proof)
+- [x] **NEW v2:** transcendental re-encoding replaced with classification form (L6)
+- [x] **NEW v2:** 4 new entries added (1.13 `<<` / `>>`, 3.19 Markov, 3.20 PolyTimeAdversary, 4.25 correlation, 4.26 `<<` / `>>` with tolerance)
+- [x] **NEW v2:** 4 template notations in Tier 3 #3.14 (B default, C++ opt-in, Odin opt-in, Jai opt-in)
 
 ---
 
-*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.*
+*End of `terms_catalog.md` v2. Total: 76 terms, 4 tiers. Refined from the warmup's `report.md` §3 + `lexicon.md` §2. Machine-readable for LLM input or transformation pipelines. v2 changes: 5 re-encodings removed, 1 re-encoding replaced, 4 new entries added, encoding defaults updated, template notations added.*