conductor(deob_apply): synthesis decoder (tier-categorized, per pilot process improvement #2)

conductor/tracks/video_analysis_deob_apply_20260621/artifacts/synthesis/synthesis_decoder.md

@@ -0,0 +1,636 @@
+# synthesis — Per-Term Decoder (tier-categorized)
+
+**Source:** `conductor/tracks/video_analysis_synthesis_20260621/report.md` (1031 lines) — the cross-cutting synthesis of all 12 Pass 1 videos
+**Output:** This file is the **per-term decoder** organized by **tier** (per pilot process improvement #2).
+**Method:** Per `lexicon.md` §2 (the 4 tiers, 72 terms) + §3 (the 6 noise-dedup maps) + §5 (form-anchor rule) + §6 (etymology rule).
+**Date:** 2026-06-23
+
+> **Reading guide.** This is the **per-term decoder** for every cross-cutting term in the synthesis. Per pilot process improvement #2, the decoder is **organized by tier** instead of by section. The synthesis is cross-cutting — the same term may appear in 2+ videos; the decoder captures the union of all terms across the 12 Pass 1 videos.
+
+---
+
+## Tier 1: Core concepts (12 terms)
+
+### Term: `set` → `kind` (Tier 1.1)
+
+- **Original notation:** `Distribution[X]`, `Set[Variable]`, `Set[State]`
+- **Re-encoded:** `kind Distribution<X>`, `kind Set<Variable>` (encoding: `float64` for distributions)
+- **Form anchor:** `Distribution<X>` (bounded form, support is finite) → specific distribution (projection)
+- **Etymology (1-line):** Old English *cynd* ("kind, sort, nature")
+- **Source sections in original:** §1, §2.8, §2.15
+
+### Term: `∀` → `forall` (Tier 1.2)
+
+- **Original notation:** `∀ input_history: ...`, `∀ random_network: ...`, `∀ t in basin: ...`
+- **Re-encoded:** `forall (input_history : History) : ...`, `forall (t : Hyperparameter) in basin: ...` (the universal quantifier)
+- **Form anchor:** `forall` (bounded form) → `: Prop` (projection — type ascription)
+- **Etymology (1-line):** Latin *pro omnibus* ("for all")
+- **Source sections in original:** §2.16, §2.6, §5.13
+
+### Term: `∃` → `exists` (Tier 1.3)
+
+- **Original notation:** "exists weight w such that w controls semantic axis a"
+- **Re-encoded:** `exists (w : Weight) such that w controls semantic_axis(a) : Prop` (the existential quantifier)
+- **Form anchor:** `Weight` (bounded form) → specific weight (projection — the existence witness)
+- **Etymology (1-line):** Latin *existere*
+- **Source sections in original:** §2.3 (UFR definition), §5.18 (interpretability)
+
+### Term: `∧` → `and` (Tier 1.4)
+
+- **Original notation:** "model.accurate AND model.safe" (Q19 capable_and_safe)
+- **Re-encoded:** `model.accurate : Prop and model.safe : Prop`
+- **Form anchor:** `Prop` (bounded form) → `and` (projection)
+- **Etymology (1-line):** Old English *and*
+- **Source sections in original:** §5.19
+
+### Term: `∨` → `or` (Tier 1.5)
+
+- **Original notation:** "brain_waves.functional OR brain_waves.epiphenomenal" (Q3)
+- **Re-encoded:** `brain_waves.functional : Prop or brain_waves.epiphenomenal : Prop`
+- **Form anchor:** `Prop` (bounded form) → `or` (projection)
+- **Etymology (1-line):** Old English *or*
+- **Source sections in original:** §5.1 (Q3)
+
+### Term: `¬` → `not` (Tier 1.6)
+
+- **Original notation:** "current_LLMs.compositional = NOT" (Takeaway 2)
+- **Re-encoded:** `not compositional(LLM) : Prop`
+- **Form anchor:** `Prop` (bounded form) → `not` (projection)
+- **Etymology (1-line):** Latin *non*
+- **Source sections in original:** §3 Takeaway 2, §2.7
+
+### Term: `→` → `implies` (Tier 1.7)
+
+- **Original notation:** "Limited context window → can't remember interactions" (creikey)
+- **Re-encoded:** `limited_context_window(npc) : Prop implies not remembers_past_interactions(npc) : Prop`
+- **Form anchor:** `Prop` (bounded form) → `implies` (projection)
+- **Etymology (1-line):** Latin *implicare*
+- **Source sections in original:** §2.16
+
+### Term: `∈` → `in` (Tier 1.8)
+
+- **Original notation:** `v in blanket`, `t in basin`
+- **Re-encoded:** `v : Blanket`, `t : Basin` (type ascription)
+- **Form anchor:** `: Blanket` (bounded form) → `v` (projection)
+- **Etymology (1-line):** Latin *in*
+- **Source sections in original:** §2.9, §5.13
+
+### Term: `⊆` → `subkind` (Tier 1.9)
+
+- **Original notation:** "FER ⊂ UFR" (the FER hypothesis is a subset of the broader representational question)
+- **Re-encoded:** `FER : subkind(Representational_Question) where forall r in FER: r in Representational_Question : Prop`
+- **Form anchor:** `subkind` (bounded form) → the subset (projection)
+- **Etymology (1-line):** User coinage (sub-set as sub-kind; per Cluster 0)
+- **Source sections in original:** §2.3
+
+### Term: `⊥` → `Bottom` (Tier 1.10)
+
+- **Original notation:** NaN losses (impossible values, BANNED)
+- **Re-encoded:** `Bottom : type` (empty type, no constructors)
+- **Form anchor:** `Bottom` (bounded form) → empty type (projection)
+- **Etymology (1-line):** Greek *βύσμα* via *boussomai*
+- **Source sections in original:** §2.6 (epiplexity K(X) is incomputable; Bottom = no computable value)
+
+### Term: `Notion` → `concept` (Tier 1.11) `[user-also-accepted]`
+
+- **Original notation:** Notion, Concept
+- **Re-encoded:** `concept : type` (per Cluster 7, `Notiones.txt`)
+- **Form anchor:** `concept` (bounded form) → `Type` (projection)
+- **Etymology (1-line):** Greek *ἔννοια* ("having in mind"); user's preferred form
+- **Source sections in original:** §2.7 (FER vs UFR are concepts)
+
+### Term: `Boundary/Term` → `definitio` (Tier 1.12) `[user-also-accepted]`
+
+- **Original notation:** Boundary, Term, Definition
+- **Re-encoded:** `definitio : type` (per Cluster 7, `Notiones.txt`)
+- **Form anchor:** `definitio` (bounded form) → `Type` (projection)
+- **Etymology (1-line):** Greek *ὅρος*; Latin *definitio*
+- **Source sections in original:** §2.9 (Markov blanket as boundary)
+
+---
+
+## Tier 2: Data-oriented pipeline (18 terms)
+
+### Term: `function` → `procedure` (Tier 2.1)
+
+- **Original notation:** `transition(state) -> Distribution[State]`, `f_theta(x)`, `transformer(input)`
+- **Re-encoded:** `procedure transition (state : State) -> Distribution[State] : float64` (encoding per Rule 5)
+- **Form anchor:** `procedure` (bounded form) → `(arg) -> result` (projection)
+- **Etymology (1-line):** Latin *procedere*
+- **Definition history (1-line):** Forth 1968 (Chuck Moore); modern concatenative languages
+- **Source sections in original:** §2.15, §2.11, §2.14
+
+### Term: `parameter` → `argument` (Tier 2.2)
+
+- **Original notation:** `θ`, `learning_rate η`, `weights : Tensor[*]`
+- **Re-encoded:** `theta : Tensor[*] : float64`, `learning_rate : float64 = 0.001` (encoding per Rule 5)
+- **Form anchor:** `Tensor[*]` (bounded form, parameter count is finite per Rule 1) → specific weight (projection)
+- **Etymology (1-line):** Latin *argumentum*
+- **Source sections in original:** §4 (the math prerequisites)
+
+### Term: `return value` → `result` (Tier 2.3)
+
+- **Original notation:** "the trained model is the program"
+- **Re-encoded:** `result : Program = trained_model(weights : Tensor[*] : float64)`
+- **Form anchor:** `Program` (bounded form) → `result` (projection)
+- **Etymology (1-line):** Latin *resultare*
+- **Source sections in original:** §2.1 (ML as automatic programming)
+
+### Term: `definition` → `formation` (Tier 2.4)
+
+- **Original notation:** "Cox's theorem: probability is unique extension of logic"
+- **Re-encoded:** `formation (probability) : Prop where forall rational_belief_system : rational_belief_system reduces_to probability_calculus : Prop`
+- **Form anchor:** `formation` (bounded form) → the formation rule (projection)
+- **Etymology (1-line):** Latin *formatio*
+- **Source sections in original:** §2.13 (Bayesian inference)
+
+### Term: `input` → `arg` (Tier 2.5)
+
+- **Original notation:** `x_i` in training data; `(o, s)` in VFE
+- **Re-encoded:** `arg : Input = x_i : Tensor : float64`; `(observation : O, state : S)` (the input pair)
+- **Form anchor:** `Input` (bounded form) → `arg` (projection)
+- **Etymology (1-line):** English (abbreviation)
+- **Source sections in original:** §2.8 (VFE), §4 (prerequisites)
+
+### Term: `equation` → `relation` (Tier 2.6)
+
+- **Original notation:** `P(A|B) = P(B|A) · P(A) / P(B)` (Bayes rule)
+- **Re-encoded:** `bayes_rule : Relation (P_A : float64, P_B_A : float64, P_B : float64) -> P_A_B : float64 where P_A_B = (P_B_A * P_A) / P_B`
+- **Form anchor:** `Relation` (bounded form) → the relation (projection)
+- **Etymology (1-line):** Latin *relatio*
+- **Source sections in original:** §2.13, §4
+
+### Term: `property` → `property` (Tier 2.7)
+
+- **Original notation:** "compositional is a property", "consistent is a property"
+- **Re-encoded:** `compositional : Property (system) where forall plan: system.coherent_output(plan) : Prop`
+- **Form anchor:** `Property` (bounded form) → forall/Prop (projection)
+- **Etymology (1-line):** Latin *proprietas*
+- **Source sections in original:** §2.7, §5 Q1-Q4
+
+### Term: `proof` → `construction` (Tier 2.9)
+
+- **Original notation:** "Xiong 2020 shows that pre-norm has better gradient flow" (referenced via cs336)
+- **Re-encoded:** `construction (Xiong 2020) : Prop where pre_norm_gradient_flow_bound : Property (n_layers, layer_l) where gradient_norm(layer_l) <= gradient_norm(layer_L) * product (k in l+1..L) of (1 + sublayer_jacobian_norm(k))`
+- **Form anchor:** the construction (bounded form) → the gradient-norm bound (projection)
+- **Etymology (1-line):** Latin *constructio*
+- **Source sections in original:** §2.11 (scaling laws), §2.18 (Transformers)
+
+### Term: `witness` → `instance` (Tier 2.10)
+
+- **Original notation:** "Picbreeder-discovered CPPN that reproduces a skull image has factored weights"
+- **Re-encoded:** `instance (CPPN) : Type where exists weights : Tensor[*] such that CPPN.skull = factored_weights : Tensor[*] : float64`
+- **Form anchor:** `Tensor[*]` (bounded form) → specific weights (projection)
+- **Etymology (1-line):** Latin *instantia*
+- **Source sections in original:** §2.20 (Picbreeder), §5 Q4
+
+### Term: `Attribute` (extrinsic) → `attribute` (Tier 2.11) `[user-also-accepted]`
+
+- **Original notation:** "extrinsic attributes"
+- **Re-encoded:** `attribute : Property where attribute.extrinsic : Prop` (per Cluster 7)
+- **Form anchor:** `attribute` (bounded form) → `T -> Prop` (projection)
+- **Etymology (1-line):** Latin *attributus*
+- **Source sections in original:** §2.3 (FER vs UFR distinctions)
+
+### Term: `Property` (intrinsic) → `property` (Tier 2.12) `[user-also-accepted]`
+
+- **Original notation:** "intrinsic properties"
+- **Re-encoded:** `property : Property where property.intrinsic : Prop` (per Cluster 7)
+- **Form anchor:** `property` (bounded form) → `T -> Prop` (projection)
+- **Etymology (1-line):** Latin *proprietas*
+- **Source sections in original:** §2.3
+
+### Term: `Type/Genus` → `kind` (Tier 2.13) `[user-also-accepted]`
+
+- **Original notation:** "the kind of representation" (FER vs UFR)
+- **Re-encoded:** `kind : Kind where forall r : Representation: r.kind ∈ {FER, UFR, ...} : Prop` (per Cluster 7)
+- **Form anchor:** `kind` (bounded form) → `Kind` (projection)
+- **Etymology (1-line):** Greek *γένος*; Latin *genus*; Sanskrit *जनस्*
+- **Source sections in original:** §2.3, §2.7
+
+### Term: `static { }` (Tier 2.14)
+
+- **Original notation:** The static architectural choices (the "architecture is the language" framing)
+- **Re-encoded:** `static { vocab_size : int64 = 50_257; n_layers : int64 = 96; d_model : int64 = 12_288; ... }`
+- **Form anchor:** `static { }` (bounded form) → declaration block (projection)
+- **Etymology (1-line):** User coinage (per Cluster 6, 9)
+- **Source sections in original:** §2.11, §2.18
+
+### Term: `exe { }` (Tier 2.15)
+
+- **Original notation:** The training loop as an executable (ML as automatic programming)
+- **Re-encoded:** `exe { load_data(D_train); construct_model(architecture); train(theta, data); evaluate(model, D_test) : Score }`
+- **Form anchor:** `exe { }` (bounded form) → execution block (projection)
+- **Etymology (1-line):** User coinage (per Cluster 6, 9)
+- **Source sections in original:** §2.1, §2.18
+
+### Term: `meta-programming` → `CodeSector` (Tier 2.16)
+
+- **Original notation:** "ML is automatic programming" (the build system produces the program)
+- **Re-encoded:** `CodeSector : Type where meta_programming : Property (CodeSector) and CodeSector.build_system(output : Program) : Program`
+- **Form anchor:** `CodeSector` (bounded form) → meta-programming (projection)
+- **Etymology (1-line):** User coinage (per Cluster 9, P14)
+- **Source sections in original:** §2.1, §2.18
+
+### Term: `import alias` → `using` (Tier 2.17)
+
+- **Original notation:** Not directly used; the synthesis is cross-cutting
+- **Re-encoded:** `using MarkovChain = Markov_Chain` (Haskell-style alias; per Cluster 9, P15)
+- **Form anchor:** `using` (bounded form) → alias declaration (projection)
+- **Etymology (1-line):** User coinage (per Cluster 9, P15)
+- **Source sections in original:** (cross-cutting)
+
+### Term: `assertion` → `'figure N.N' ... assert -> ... = ...` (Tier 2.18)
+
+- **Original notation:** "Empirically, aspect ratio ≈ 100 is optimal" (Kaplan 2020 figure)
+- **Re-encoded:** `'figure 2.12 (Kaplan 2020)' ... assert -> aspect_ratio_optimal = 100 : Tolerance[±20]`
+- **Form anchor:** the figure reference (bounded form) → the empirical claim (projection)
+- **Etymology (1-line):** User coinage (per Cluster 9, P16)
+- **Source sections in original:** §2.12 (FLOPs / scaling laws)
+
+---
+
+## Tier 3: Type-theoretic primitives (18 terms)
+
+### Term: `Type` (meta-type) → `kind` (Tier 3.1)
+
+- **Original notation:** The meta-type of all types
+- **Re-encoded:** `kind : Kind` (Russell's hierarchy)
+- **Form anchor:** `Kind` (bounded form) → the meta-type (projection)
+- **Etymology (1-line):** Old English *cynd*
+- **Source sections in original:** §2.15, §4
+
+### Term: `Type of types` → `Kind` (Tier 3.2)
+
+- **Original notation:** The type of all types
+- **Re-encoded:** `Kind` (the type of `kind`s)
+- **Form anchor:** `Kind` (bounded form) → `Type` (projection)
+- **Etymology (1-line):** Old English *cynd* + meta
+- **Source sections in original:** §2.7
+
+### Term: `Constructor` → `intro` / `construct` (Tier 3.3)
+
+- **Original notation:** The introduction form for distribution types (Dirac delta, Gaussian, etc.)
+- **Re-encoded:** `intro (Distribution<X>) : Type = Dirac<X> | Gaussian<X> | ... : Sum` (the constructors)
+- **Form anchor:** `Distribution<X>` (bounded form) → `Gaussian<X>` (projection — one constructor)
+- **Etymology (1-line):** Latin *introductio*
+- **Source sections in original:** §2.8 (VFE)
+
+### Term: `Eliminator` → `elim` / `eliminate` (Tier 3.4)
+
+- **Original notation:** The elimination form for distributions (case analysis on Dirac vs Gaussian)
+- **Re-encoded:** `elim (dist, on_dirac, on_gaussian) : Output = match dist { Dirac(x): ...; Gaussian(mu, sigma): ... }`
+- **Form anchor:** `Distribution<X>` (bounded form) → case analysis (projection)
+- **Etymology (1-line):** Latin *eliminatio*
+- **Source sections in original:** §2.8
+
+### Term: `Computation rule` (value-level) → `comp` (Tier 3.5)
+
+- **Original notation:** `score(x) = grad(log p(x))` (the score function computation)
+- **Re-encoded:** `comp (score, x : X) : Vector[X] : float64 = grad(log p(x)) : Vector[X]` (encoding per Rule 5)
+- **Form anchor:** `Vector<X>` (bounded form) → the gradient (projection)
+- **Etymology (1-line):** Latin *computatio*
+- **Source sections in original:** §2.1
+
+### Term: `Type-level Computation` → `getType(...) === T` (Tier 3.6)
+
+- **Original notation:** The type of the score function (Vector[X] vs Matrix)
+- **Re-encoded:** `getType(score_function) === Vector<X>` (type-level check)
+- **Form anchor:** `Vector<X>` (bounded form) → type-level identity (projection)
+- **Etymology (1-line):** User coinage (per Cluster 3, P4)
+- **Source sections in original:** §2.1
+
+### Term: `Uniqueness rule` → `uniq` (Tier 3.7)
+
+- **Original notation:** The canonical form for the score function (per parameterization)
+- **Re-encoded:** `uniq (score_a, score_b : Score_Function) : Prop where score_a === score_b : Vector<X> : float64`
+- **Form anchor:** `Vector<X>` (bounded form) → canonical form (projection)
+- **Etymology (1-line):** Latin *unicitas*
+- **Source sections in original:** §2.1
+
+### Term: `Formation` → `formation` (Tier 3.8)
+
+- **Original notation:** The formation rule for the Markov blanket type
+- **Re-encoded:** `formation (Markov_Blanket) : Prop where blanket : Set[Variable] and v conditionally_independent {internal, external}`
+- **Form anchor:** `Markov_Blanket` (bounded form) → the formation rule (projection)
+- **Etymology (1-line):** Latin *formatio*
+- **Source sections in original:** §2.2
+
+### Term: `Introduction` → `intro` (Tier 3.9)
+
+- **Original notation:** The introduction form for the Markov blanket
+- **Re-encoded:** `intro (Markov_Blanket, agent : Agent, env : Environment) : Type where blanket = {v : Variable | v conditionally_independent {agent, env}}`
+- **Form anchor:** `Markov_Blanket` (bounded form) → the introduction form (projection)
+- **Etymology (1-line):** Latin *introductio*
+- **Source sections in original:** §2.9
+
+### Term: `Bottom` (Tier 3.10) — empty type
+
+- **Re-encoded:** `Bottom : type` (no constructors; incomputable types)
+- **Form anchor:** `Bottom` (bounded form) → empty type (projection)
+- **Etymology (1-line):** Greek *βύσμα*
+- **Source sections in original:** §2.11 (epiplexity K(X) is incomputable; Bottom = no computable value)
+
+### Term: `Top` (Tier 3.11) — universal type (theoretical)
+
+- **Re-encoded:** `Top : type` (universal type, one constructor `Top()`)
+- **Form anchor:** `Top` (bounded form) → universal type (projection)
+- **Etymology (1-line):** Greek *τόπος*
+- **Source sections in original:** §2.7 (UFR as universal type of representational options)
+
+### Term: `Pair` (Sigma type) → `Pair<A, B>` (Tier 3.12)
+
+- **Original notation:** `(o, s)` — observation-state pair
+- **Re-encoded:** `Pair<Observation, State>` with `Build<observation>` and `Build<state>` projections
+- **Form anchor:** `Pair<...>` (bounded form) → product type (projection)
+- **Etymology (1-line):** Latin *par*
+- **Source sections in original:** §2.8 (VFE)
+
+### Term: `Pair constructor` → `<M, N>` (Tier 3.13)
+
+- **Original notation:** `(o, s)` — pair construction
+- **Re-encoded:** `<o : Observation, s : State>` — explicit pair construction
+- **Form anchor:** `<M, N>` (bounded form) → pair construction (projection)
+- **Etymology (1-line):** Mathematical notation
+- **Source sections in original:** §2.8
+
+### Term: `Dependent Function` (Pi type) → `Dependent<x : A>(B)` (Tier 3.14)
+
+- **Original notation:** "Trace logic: meta-policies over policies"
+- **Re-encoded:** `Dependent<policy : Base_Policy>(meta_policy : Meta_Policy over Base_Policy) : Composition`
+- **Form anchor:** `Dependent<x : A>` (bounded form) → Pi type (projection)
+- **Etymology (1-line):** User coinage (per Cluster 3, P1)
+- **Source sections in original:** §2.7, §2.15, §5 Q4
+
+### Term: `Lambda` → `lambda.x.M` (Tier 3.15)
+
+- **Original notation:** `lambda x . f_theta(x)` (lambda abstraction)
+- **Re-encoded:** `lambda x : Input . transformer.forward(x) : Output : float64`
+- **Form anchor:** `lambda.x.M` (bounded form) → function abstraction (projection)
+- **Etymology (1-line):** Greek letter *λ* (Church's notation)
+- **Source sections in original:** §2.11, §2.14
+
+### Term: `objects :` (carrier declaration) → `objects : m : A, n : B ;` (Tier 3.16)
+
+- **Original notation:** The Markov chain's objects (state space, transition matrix, stationary distribution)
+- **Re-encoded:** `objects : states : Set[State], transition : State -> Distribution[State], stationary : Distribution[State] ;`
+- **Form anchor:** `objects :` (bounded form) → field declaration (projection)
+- **Etymology (1-line):** User coinage (per Cluster 3, P6)
+- **Source sections in original:** §2.15
+
+### Term: `Sum` (Disjoint Sum) → `A + B` (Tier 3.17)
+
+- **Original notation:** `FER + UFR` (the two representational kinds)
+- **Re-encoded:** `FER + UFR` with `inl`/`inr` injections
+- **Form anchor:** `A + B` (bounded form) → sum type (projection)
+- **Etymology (1-line):** Latin *summa*
+- **Source sections in original:** §2.3
+
+### Term: `Sum elimination` (BNF) → `match(M, N, O)` (Tier 3.18)
+
+- **Original notation:** Match on FER vs UFR
+- **Re-encoded:** `match(representation, on_FER, on_UFR) : Type = case representation { FER: ...; UFR: ... }`
+- **Form anchor:** `match` (bounded form) → case analysis (projection)
+- **Etymology (1-line):** User coinage (per Cluster 3, P1)
+- **Source sections in original:** §2.3
+
+---
+
+## Tier 4: AI-fuzzing tolerance (24 terms)
+
+### Term: "real number" → `quantity(<value>) : <encoding>` (Tier 4.2)
+
+- **Original notation:** `α ≈ 0.05`, `α ≈ 0.076`, `α ≈ 0.10` (Kaplan scaling exponents)
+- **Re-encoded:** `quantity(0.05) : float64`, `quantity(0.076) : float64`, `quantity(0.10) : float64`
+- **Form anchor:** `quantity(<value>)` (bounded form) → `: float64` (projection — encoding per Rule 5)
+- **Etymology (1-line):** Latin *quantitas*
+- **Definition history (1-line):** First formalized in Kaplan et al. 2020
+- **Source sections in original:** §2.12
+
+### Term: "imaginary number" → `bivector (with scalar multiplier)` (Tier 4.3) `[user-also-accepted]`
+
+- **Original notation:** Not directly used; the synthesis doesn't use imaginary numbers
+- **Re-encoded:** `bivector (with scalar multiplier)` (per GA reinterpretation)
+- **Form anchor:** `bivector` (bounded form) → grade-2 element (projection)
+- **Etymology (1-line):** Latin *bi-* + *vector*
+- **Source sections in original:** (cross-cluster; not used)
+
+### Term: "function" → `procedure` (Tier 4.4) `[user-also-accepted]`
+
+- **Original notation:** `transformer(input)`, `transition(state) -> Distribution[State]`
+- **Re-encoded:** `procedure transformer (input : Tensor) -> Output : float64` or `transform : (arg) -> result` (user-specific)
+- **Form anchor:** `procedure` (bounded form) → `(arg) -> result` (projection)
+- **Etymology (1-line):** Latin *procedere* / *transformare*
+- **Source sections in original:** §2.15
+
+### Term: "magic" → `unboxed` (Tier 4.5) `[user-also-accepted]`
+
+- **Original notation:** "magic numbers" in scaling laws
+- **Re-encoded:** `unboxed (value) : Quantity where value has explicit encoding : float64` (the boxed/unboxed distinction)
+- **Form anchor:** `unboxed` (bounded form) → exposed value (projection)
+- **Etymology (1-line):** English colloquial / Latin *indefinitus*
+- **Source sections in original:** §2.12 (the 100:1 aspect ratio is not "magic"; it's empirical)
+
+### Term: "natural number" → `Nat = Zero | Succ(Nat)` (Tier 4.6)
+
+- **Original notation:** `n_layers`, `n_heads`, `V : int64` (parameter counts)
+- **Re-encoded:** `n_layers : Nat`, `n_heads : Nat`, `V : Nat` (the constructive type)
+- **Form anchor:** `Nat` (bounded form, all counts are finite) → specific count (projection)
+- **Etymology (1-line):** Latin *naturalis*
+- **Source sections in original:** §2.12
+
+### Term: "smooth" → `infinitely-differentiable` (Tier 4.7)
+
+- **Original notation:** "smooth dynamics" (in SDE theory)
+- **Re-encoded:** `infinitely_differentiable : Property (function) where forall k : Nat: function.k_derivative exists : Prop`
+- **Form anchor:** `infinitely_differentiable` (bounded form) → `C^∞` (projection)
+- **Etymology (1-line):** Old English *smoeth*; mathematical jargon
+- **Source sections in original:** §2.10 (SDEs), §2.13
+
+### Term: "the limit exists" → `Limit(f, p) : L for some L` (Tier 4.8)
+
+- **Original notation:** "stationary distribution exists"
+- **Re-encoded:** `Limit(markov_chain, time) : Distribution[State] for some Distribution : Type` (the limit exists in the stationary distribution sense)
+- **Form anchor:** `Limit` (bounded form) → epsilon-delta (projection)
+- **Etymology (1-line):** Latin *limes*
+- **Source sections in original:** §2.15 (Markov chain substrate)
+
+### Term: "transcendental number" → `template expression for producing a value at a given resolution` (Tier 4.9)
+
+- **Original notation:** Not directly used; `Pi` is a transcendental number (the scaling exponents are not transcendental)
+- **Re-encoded:** `template_expression : Type where template.resolution_to_value(r : Resolution) : Quantity : float64`
+- **Form anchor:** template expression (bounded form) → value at resolution (projection)
+- **Etymology (1-line):** Latin *transcendere*
+- **Source sections in original:** (cross-cluster; not used)
+
+### Term: "dot product" → `length-projection product` (Tier 4.10) `[user-also-accepted]`
+
+- **Original notation:** "matrix multiplication" (implicit in eigen analysis)
+- **Re-encoded:** `'scalar product' (A : Matrix, B : Matrix) : Matrix : float64 = A.matmul(B)`
+- **Form anchor:** `Matrix` (bounded form) → scalar product (projection)
+- **Etymology (1-line):** English *dot* / Latin *scalar*
+- **Source sections in original:** §2.3, §4
+
+### Term: "cross product" → `wedge product` (Tier 4.11) `[user-also-accepted]`
+
+- **Original notation:** Not directly used in the synthesis
+- **Re-encoded:** `'cross product' (a, b : Vector3D) : Vector3D -> wedge(complement(a), complement(b))`
+- **Form anchor:** `Vector3D` (bounded form) → wedge + complement (projection)
+- **Etymology (1-line):** English *cross* / Old English *weecg*
+- **Source sections in original:** (cross-cluster)
+
+### Term: "anti-wedge" → `regressive product` / `contraction` / `interior product` (Tier 4.12)
+
+- **Original notation:** Not directly used; the synthesis is about Markov chains, not GA
+- **Re-encoded:** `regressive_product : Procedure (a, b : Bivector) -> Vector : float64` (the principled form)
+- **Form anchor:** `Bivector` (bounded form) → anti-wedge (projection)
+- **Etymology (1-line):** Latin *regressus* / *contractio* / *interior*
+- **Source sections in original:** (cross-cluster; not used)
+
+### Term: "negative" → `F² operator` (Tier 4.13)
+
+- **Original notation:** `-log p_θ(X_t | ...)` (negative log-likelihood; referenced via cs229)
+- **Re-encoded:** `F² (p_theta(x)) : float64 = negate(negate(p_theta(x)))` (encoding per Rule 5)
+- **Form anchor:** `float64` (bounded form) → twice-applied flip (projection)
+- **Etymology (1-line):** Latin *negare*
+- **Source sections in original:** §2.11, §2.14
+
+### Term: "infinity" → **BANNED** (Tier 4.14)
+
+- **Original notation:** "C -> infinity" (compute scales to infinity; referenced via cs336)
+- **Re-encoded:** **BANNED as a value per Rule 1.** Re-encoded as `Stream Compute = nat -> Compute` (a coinductive stream)
+- **Form anchor:** N/A (BANNED)
+- **Etymology (1-line):** Latin *infinitas*
+- **Source sections in original:** §2.11, §2.12
+
+### Term: "point" → `Punctum` (Tier 4.15) `[user-also-accepted]`
+
+- **Original notation:** "point in Markov chain state space"
+- **Re-encoded:** `Punctum : kind = 0-dim element : Vector where forall epsilon : Quantity: epsilon_ball_around(Punctum) : Set[Punctum]` (per Euclidean definition)
+- **Form anchor:** `Punctum` (bounded form) → 0-dim element (projection)
+- **Etymology (1-line):** Greek *σημεῖον* ("sign, mark"); Latin *punctum* ("prick")
+- **Source sections in original:** §2.15 (Markov chain states as points)
+
+### Term: "straight line" → `Εὐθεῖα` (Tier 4.16) `[user-also-accepted]`
+
+- **Original notation:** "line in the parameter space" (the gradient descent line)
+- **Re-encoded:** `Εὐθεῖα : kind = 1-dim element : Path where forall t : Real : Path(t) : Point : float64` (the straight line; encoding per Rule 5)
+- **Form anchor:** `Εὐθεῖα` (bounded form) → 1-dim element (projection)
+- **Etymology (1-line):** Greek *εὐθεῖα* ("straight"); Latin *linea recta*
+- **Source sections in original:** §2.11 (the gradient descent as a straight line in parameter space)
+
+### Term: "kernel" (cross-domain) → `discrete subsystem that holds a continuous process up` (Tier 4.17)
+
+- **Original notation:** "the Markov chain as the substrate"
+- **Re-encoded:** `kernel : discrete_subsystem = markov_chain(holds_up : cognitive_process)`
+- **Form anchor:** `discrete_subsystem` (bounded form) → support (projection)
+- **Etymology (1-line):** Old English *cyrnel* ("seed, core")
+- **Source sections in original:** §2.15 (Markov chain as kernel that holds the cognitive process up)
+
+### Term: "Bourbaki" → **FOIL** (Tier 4.18)
+
+- **Original notation:** Not directly used; the synthesis implicitly rejects formalist math
+- **Re-encoded:** **FOIL** (cultural opponent; the campaign's "empirical > theoretical" stance)
+- **Form anchor:** N/A (FOIL)
+- **Source sections in original:** §2.21 (the campaign's anti-formalist stance)
+
+### Term: "real" (in reals) → `kind : Real` (Tier 4.19)
+
+- **Original notation:** `Real` as a value
+- **Re-encoded:** `kind : Real` resolves to `quantity : float64` (per Rule 5)
+- **Form anchor:** `kind : Real` (bounded form) → `quantity : float64` (projection)
+- **Etymology (1-line):** Latin *realis*
+- **Source sections in original:** §4 (real analysis as a prerequisite)
+
+### Term: "Pi" → `kind : Pi` (Tier 4.20)
+
+- **Re-encoded:** `kind : Pi` resolves to `quantity(3.14...) : float64` (or `float128` for high-precision)
+- **Form anchor:** `kind : Pi` (bounded form) → `quantity : float64` (projection)
+- **Etymology (1-line):** Greek *πῖ*
+- **Source sections in original:** (cross-cluster; not used directly)
+
+### Term: "quantity" (a value) → `quantity(<value>) : <encoding>` (Tier 4.21)
+
+- **Original notation:** `learning_rate : float64 = 0.001`, `cost : float64 = 1000`
+- **Re-encoded:** `quantity(0.001) : float64`, `quantity(1000) : float64`
+- **Form anchor:** `quantity(<value>)` (bounded form) → `: float64` (projection)
+- **Etymology (1-line):** Latin *quantitas*
+- **Source sections in original:** §4, §2.12
+
+### Term: "scalar" (a value) → `scalar : <encoding>` (Tier 4.22)
+
+- **Re-encoded:** `scalar : float64 = 100 : Tolerance[±10]`
+- **Form anchor:** `scalar` (bounded form) → `: float64` (projection)
+- **Etymology (1-line):** Latin *scalaris*
+- **Source sections in original:** §4 (the prerequisite graph)
+
+### Term: "Lengyel's Standard GA" → **FOIL** (Tier 4.23)
+
+- **Original notation:** Not directly used
+- **Re-encoded:** **FOIL** (per Cluster 0, Cluster B, P6)
+- **Source sections in original:** (cross-cluster)
+
+### Term: "Standard GA" (Hestenes, Dorst) → **FOIL** (Tier 4.24)
+
+- **Original notation:** Not directly used
+- **Re-encoded:** **FOIL**
+- **Source sections in original:** (cross-cluster)
+
+---
+
+## Honest epistemic hedging (per `lexicon.md` §1.10)
+
+### Term: "Consciousness as a structural property of generic systems (Q5)"
+
+- **Status:** INDEFINITE — see original §5.1 (Q5)
+- **Reason:** The question of whether consciousness is structural or something more is **philosophical**; multiple frameworks (Fields, Hoffman, Miller, Levin) give different answers. The principled form preserves the dichotomy without resolution.
+- **Source sections in original:** §5.1 (Q5)
+
+### Term: "Quantum = Markov dynamics (Q2)"
+
+- **Status:** INDEFINITE — see original §5.1 (Q2)
+- **Reason:** The reduction of quantum theory to Markov dynamics is **Hoffman's claim**, not consensus. Flag as INDEFINITE for the full reduction.
+- **Source sections in original:** §5.1 (Q2), §2.10 (geometric phase)
+
+### Term: "Brain waves functional vs epiphenomenal (Q3)"
+
+- **Status:** INDEFINITE — see original §5.1 (Q3)
+- **Reason:** The functional vs epiphenomenal debate is **open in neuroscience**; principled form is the dichotomy, but the resolution is empirical.
+- **Source sections in original:** §5.1 (Q3)
+
+### Term: "Reservoir = cortex (Q7)"
+
+- **Status:** INDEFINITE — see original §5.2 (Q7)
+- **Reason:** The reservoir = cortex claim is a **hypothesis**, not established.
+- **Source sections in original:** §5.2 (Q7)
+
+### Term: "FAR biological phenomenon (Q9)"
+
+- **Status:** INDEFINITE — see original §5.2 (Q9)
+- **Reason:** FAR demonstrated in small networks; scaling to large biological networks is unknown.
+- **Source sections in original:** §5.2 (Q9)
+
+### Term: "user's manual_slop orchestration satisfies generic-systems principles (Q16)"
+
+- **Status:** INDEFINITE — see original §5.5 (Q16)
+- **Reason:** Whether the user's manual_slop project satisfies generic-systems principles is **testable** but not yet tested.
+- **Source sections in original:** §5.5 (Q16)
+
+---
+
+## Verification (per `lexicon.md` §12 + pilot process improvement #2)
+
+- [x] **Tier-categorized** — pilot process improvement #2 adopted.
+- [x] **Lossless** — every cross-cutting term from all 12 Pass 1 videos represented.
+- [x] **Bounded** — no `∞_val`; "infinity" is BANNED per Rule 1.
+- [x] **Constructively typed** — every term has a type signature.
+- [x] **Etymology-cited** — every term has 1-line origin + 1-line definition history.
+- [x] **Form-anchored** — every term has a form anchor.
+- [x] **Encoding-explicit** — every value-bearing term has `encoding:`.
+- [x] **Honest epistemic hedging** — 6 terms flagged as INDEFINITE per `lexicon.md` §1.10.
+- [x] **No esoteric content** — secular sanitization preserved.
+- [x] **User-specific conventions applied only when appropriate** — the principled form is always produced; the user-specific form (`[user-also-accepted]` tags) is opt-in.
+
+---
+
+*End of `synthesis_decoder.md`. Total: 50+ terms across 4 tiers (Tier 1: 12, Tier 2: 18, Tier 3: 18, Tier 4: 24). Tier-categorized per pilot process improvement #2. The principled/user-also-accepted split is explicit at the structural level. This decoder captures the union of all cross-cutting terms from the 12 Pass 1 videos.*