diff --git a/conductor/tracks/video_analysis_deob_lexicon_20260621/dedup_map.md b/conductor/tracks/video_analysis_deob_lexicon_20260621/dedup_map.md new file mode 100644 index 00000000..6cb208ba --- /dev/null +++ b/conductor/tracks/video_analysis_deob_lexicon_20260621/dedup_map.md @@ -0,0 +1,223 @@ +# Dedup Map (the 6 noise-dedup maps refined, 2026-06-23) + +**Track:** `video_analysis_deob_lexicon_20260621` +**Source:** `lexicon.md` §3 (refined from warmup `report.md` §4) +**Format:** Per-map detail with principled/user-preferred split + +> **Reading guide.** The 6 noise-dedup maps are the user's preferred term collapses. They are split into **3 principled** (derived from the 5 rules) and **3 user-preferred** (the user's personal preferences, tagged `[user-preferred]`). +> +> **The 3 principled maps are scheme-canonical.** The scheme requires these collapses; they are derived from the Curry-Howard correspondence (Map 1), constructive type theory (Map 2), and concatenative programming (Map 3). +> +> **The 3 user-preferred maps are optional output conventions.** The user has specific preferences for the GA collapse (Map 4), the "invent → construct" rename (Map 5), and the "number = quantity = value" collapse (Map 6). The scheme produces the principled re-encoding; the LLM can additionally apply the user-preferred form if the reader would prefer it. + +--- + +## Map 1: Proofs = Programs = Computations (Curry-Howard) `[principled]` + +**Source cluster:** Cluster 3 (Type Theory — Function type formation/intro/elim rules); Cluster 4 (Lambda Calculus — the bilingual pattern); Cluster 7 (Pattern 2 — constructive proof structure). + +**Origin.** Howard, 1969 — "The formulae-as-types notion of construction." The Curry-Howard correspondence says a proof of proposition `P` corresponds to a program of type `P`. The user has adopted this as the principled foundation. + +**The map.** + +| Conventional | Principled re-encoding | Why it dedups | +|---|---|---| +| "we have a proof that x² ≥ 0" | `construction (x : Real) -> square(x) >= zero(Real) : Prop` | The "proof" is a program; the "proposition" is a type. | +| "the proof of the theorem" | `the program (lambda.x. proof_body) : Prop` | Same. | +| "a proof by induction" | `a recursive construction` | The induction principle is recursion. | +| "QED" | `(result : Prop)` | The "QED" is the value of the program. | + +**Edge cases:** + +1. **Classical logic (excluded middle, double negation):** the principled map preserves them as classical programs (via continuations or CPS transform). The user prefers constructive; the LLM should flag classical logic and offer the constructive alternative. +2. **Proofs in classical math textbooks:** the LLM should not blindly apply the map; the reader may want the classical proof preserved. The LLM should offer both forms. +3. **Coq/Lean/Agda proofs:** these are already in the principled form; the LLM should preserve them. + +**User-specific additions:** none. This map is fully principled. + +--- + +## Map 2: Sets = Kinds = Types (constructive) `[principled]` + +**Source cluster:** Cluster 3 (Type Theory — `kind`/`type` distinction); Cluster 4 (Lambda Calculus — `Data` type); Cluster 7 (`Notiones.txt` — `Type = "successful act of association"`). + +**Origin.** Per Martin-Löf, 1975 — "An intuitionistic theory of types." The constructive type theory identification of sets, kinds, and types. The user has adopted this as the principled foundation. + +**The map.** + +| Conventional | Principled re-encoding | Why it dedups | +|---|---|---| +| "the set of natural numbers" | `kind Nat = Zero | Succ(Nat)` | The "set" is a kind; the "kind" is a type. | +| "the set of pairs (A, B)" | `kind Pair = (A, B)` | Same. | +| "the set of functions A → B" | `kind Function = (A) -> B` | Same. | +| "x is in the set S" | `x : S` | The "in" relation is type ascription. | +| "for all x in S, P(x)" | `forall x : S, P(x) : Prop` | The "for all in" is dependent quantification. | + +**Edge cases:** + +1. **Naive set theory (comprehension axiom):** the principled map excludes comprehension (it leads to Russell's paradox). The user is constructive; the LLM should flag comprehension and offer the constructive alternative. +2. **ZFC set theory:** the user is not ZFC; the LLM should preserve ZFC if the reader is using it, but offer the constructive form. +3. **Class/set distinction (proper classes):** the principled map collapses this; the LLM should preserve the distinction if the reader needs it. + +**User-specific additions:** none. This map is fully principled. + +--- + +## Map 3: Functions = Procedures = Words (concatenative) `[principled]` + +**Source cluster:** Cluster 2 (University Notes — pseudo-code with explicit procedures); Cluster 4 (Lambda Calculus — `Application (algorithim, input)`); Cluster 9 (Chapter 1.sectr — `proc` keyword for procedures). + +**Origin.** Forth (1968), ColorForth (Chuck Moore), and the concatenative programming tradition. The identification of functions, procedures, and words (concatenative language terms). The user has adopted this as the principled foundation. + +**The map.** + +| Conventional | Principled re-encoding | Why it dedups | +|---|---|---| +| "the function f(x) = x + 1" | `procedure f (x : Real) -> Real : x + 1` | The "function" is a procedure; the procedure is a word. | +| "apply the function to the input" | `apply (procedure, input) -> result` | The "apply" is a word. | +| "compose the functions" | `compose (f, g) -> h where h(x) = f(g(x))` | The "compose" is a word. | +| "the function's body" | `the procedure's body` | Same. | +| "call the function" | `execute the procedure` | The "call" is "execute" in the concatenative tradition. | + +**Edge cases:** + +1. **Pure functions (no side effects):** the principled map preserves them. Concatenative languages can be pure (e.g., Kitten, Joy). +2. **First-class functions:** the principled map preserves them. Procedures are first-class values. +3. **Higher-order functions:** the principled map preserves them as procedures that return procedures. + +**User-specific additions:** none. This map is fully principled. + +--- + +## Map 4: "Real" = "Imaginary" = "Bivector" (geometric algebra) `[user-preferred]` + +**Source cluster:** Cluster 0 (Pattern 2 — Descartes-rejection / Clifford-affirmation); Cluster 8 (GeoAlg — `Point`, `Circle`, `Line`, `Plane` types). + +> **Reading guide.** This map is the **user's geometric-algebra reinterpretation**. It is the user's preference, NOT a scheme-canonical dedup. The scheme's principled form for "imaginary number" is `bivector` (or `Bivector` with explicit grade annotation); "real number" re-encodes to `quantity() : ` (per Rule 5). The collapse of "real" + "imaginary" into the GA framework is the user's contribution. + +**Origin.** William Kingdon Clifford, 1878 — "Applications of Grassmann's Extensive Algebra." The geometric algebra identification of reals (grade-0), imaginaries (grade-2), and the broader Clifford algebra. The user has adopted this as a user-preferred map. + +**The map (user-preferred form).** + +| Conventional | Principled re-encoding | User-preferred form | +|---|---|---| +| "the real number x" | `quantity(x) : float64` | `grade-0 element x (real)` (per GA) | +| "the imaginary number i" | `bivector (with scalar multiplier)` | `Bivector` (per Cluster 0, Pattern 2) | +| "x + iy" (a complex number) | `quantity(x) : float64 + bivector(y) : float64` | `Bivector y + Scalar x` (per GA) | +| "the complex plane" | `Multivector space (grade-0 + grade-2)` | `Multivector space (full GA)` | +| "i² = -1" | `bivector * bivector = -scalar (geometric product, 2D)` | `e₁ ∧ e₂ squared = -scalar` (per GA) | + +**Edge cases:** + +1. **Higher-dimensional complex numbers (quaternions, octonions):** the GA map generalizes naturally (biquaternions, etc.). The principled form: `multivector with explicit grade annotation`. +2. **Engineers vs mathematicians:** engineers often use the complex-number notation; mathematicians prefer the GA form. The LLM should offer both. +3. **The "i² = -1" identity:** in 2D GA, this is `e₁ ∧ e₂ * e₁ ∧ e₂ = -e₁e₁e₂e₂ = -1`. In higher dimensions, the identity generalizes. + +**When to apply:** +- (a) The user explicitly requests it. +- (b) The term appears in a context where the user's prior de-obfuscation work used GA. +- (c) The reader's preference is to use GA output. + +Otherwise, use the principled re-encoding from §2 (Tier 4 entries 4.2-4.3). + +--- + +## Map 5: "Invent" = "Create" = "Imagine" → "Construct" `[user-preferred]` + +**Source cluster:** Cluster 0 (Pattern 3 — "construct, not invent"); Cluster 7 (Pattern 2 — constructive proof structure); Cluster 9 (Pattern 14 — `CodeSector` meta-programming is the operational form). + +> **Reading guide.** This map is the **user's preferred translation** of "invent" / "create" / "imagine" to `construct`. The principled form preserves the original terms (e.g., "we invent the function f"); the user-preferred form rewrites them to "we construct the function f." The user explicitly states that "invent" is the wrong word for understanding math (per Cluster 0, Pattern 3). + +**Origin.** Constructive mathematics tradition (Brouwer, Martin-Löf). The user explicitly maps `invent → construct` because the verb "invent" implies a reified noun (an "invention"), while "construct" implies a process (a "construction"). + +**The map (user-preferred form).** + +| Conventional | Principled re-encoding | User-preferred form | +|---|---|---| +| "we invent a new function" | `we define a new function` | `we construct a new function` | +| "invent the construction" | `define the construction` | `construct the construction` | +| "the invention of calculus" | `the development of calculus` | `the construction of calculus` | +| "we imagine a new theorem" | `we conjecture a new theorem` | `we construct a new theorem` | +| "the inventor of this idea" | `the developer of this idea` | `the constructor of this idea` | + +**Edge cases:** + +1. **Historical references (e.g., "Newton invented calculus"):** the principled form preserves "invented" as the historical verb. The LLM should offer both. +2. **Engineering vs mathematics:** engineers often use "invent" / "design"; mathematicians use "construct" / "develop". The LLM should preserve the context. +3. **The "invention" of new objects (e.g., "we invent a new data type"):** the principled form is "we define a new data type" (per constructive type theory); the user-preferred form is "we construct a new data type." + +**When to apply:** +- (a) The user explicitly requests it. +- (b) The term appears in a context where the user has previously used "construct" instead of "invent." +- (c) The reader's preference is to use constructive language. + +Otherwise, use the principled form (which is "define" or "develop", not "invent"). + +--- + +## Map 6: "Number" = "Value" = "Quantity" → "Expression that resolves" `[user-preferred]` + +**Source cluster:** Cluster 0 (Pattern 2 — Descartes-rejection); Cluster 1 (LLM conversations — the user pushes back on `π` as a "constant"); Cluster 0 (Cluster A, P2 — "Pi is a type-class of expressions that resolve in discrete encoding to a fixed value"); Cluster 0 (Cluster C, P12 — "the user pushes back on the LLM whenever it conflates the model with the reality"). + +> **Reading guide.** This map is the **user's preferred translation** of "number" / "value" / "quantity" to "expression that resolves in a specific encoding." The principled form (per Rule 5) is `quantity() : ` (e.g., `quantity(3.14) : float64`); the user-preferred form makes the type-class / encoding-explicit aspect explicit (e.g., "this is an expression that resolves to a quantity in float64 encoding"). + +**Origin.** Constructive type theory + the user's encoding-explicit directive (per user 2026-06-23). The user explicitly maps "number" / "value" / "quantity" to "expression that resolves" because the conventional terms imply a reified noun (a "number" that "is" something), while "expression that resolves" implies a process (an expression that resolves to a value in a specific encoding). + +**The map (user-preferred form).** + +| Conventional | Principled re-encoding | User-preferred form | +|---|---|---| +| "the number 3.14" | `quantity(3.14) : float64` | `the expression that resolves to a quantity in float64 encoding` | +| "the value is 5" | `quantity(5) : int64` | `the expression that resolves to a quantity in int64 encoding` | +| "Pi" | `kind : Pi` (resolves to `quantity(3.14...) : float64`) | `the type-class of expressions that resolve in discrete encoding to a fixed value` | +| "the quantity is x" | `the expression is quantity(x) : ` | `the expression is a quantity in ` | +| "this is a number" | `this is a quantity() : ` | `this is an expression that resolves to a quantity in ` | + +**Edge cases:** + +1. **Constants (e.g., "Pi is a constant"):** the principled form is `kind : Pi` (a type-class). The user-preferred form is "the type-class of expressions that resolve in discrete encoding to a fixed value." The LLM should offer both. +2. **Variables (e.g., "let x be a real number"):** the principled form is `x : Real` (per Tier 1 #1.8). The user-preferred form is "let x be a quantity in float64 encoding." +3. **The "is" verb (e.g., "the value is 5"):** the principled form is `quantity(5) : int64`. The user-preferred form is "the expression resolves to a quantity(5) in int64 encoding." The LLM should preserve the type-class / encoding-explicit aspect. + +**When to apply:** +- (a) The user explicitly requests it. +- (b) The term appears in a context where the user has previously used the type-class / encoding-explicit form. +- (c) The reader's preference is to use encoding-explicit language. + +Otherwise, use the principled re-encoding from §2 (Tier 4 entries 4.2, 4.19-4.22). + +--- + +## Cross-map relationships + +The 6 maps are not independent. The 3 principled maps are the foundation; the 3 user-preferred maps are extensions. + +- **Map 1 (Curry-Howard)** + **Map 2 (Sets=Kinds)** + **Map 3 (Functions=Procedures)** = the constructive type theory + concatenative programming foundation. +- **Map 4 (GA collapse)** is the user's geometric algebra extension; it can be applied on top of the foundation. +- **Map 5 (invent → construct)** is a stylistic / linguistic map; it doesn't change the math, only the vocabulary. +- **Map 6 (number = expression that resolves)** is the encoding-explicit extension; it complements Rule 5 (per user 2026-06-23). + +**The 5 rules (per `lexicon.md` §1) constrain the maps:** +- Rule 1 (Boundedness) bans `∞_val` and `∞_card` — this constrains Map 1 (proofs can't be "infinite") and Map 2 (sets can't be "infinite" in cardinality). +- Rule 2 (Form-anchor) requires every re-encoding to have a form anchor — this constrains all 6 maps. +- Rule 3 (Etymology) requires 1-line origin + 1-line history — this applies to all 6 maps. +- Rule 4 (Lossless) requires every concept to be represented — this constrains the maps' coverage. +- Rule 5 (Encoding-explicit) requires every value-bearing term to have an encoding — this constrains Map 6 specifically. + +--- + +## Verification + +- [x] **3 principled maps** (Curry-Howard, Sets=Kinds, Functions=Procedures) clearly marked `[principled]` +- [x] **3 user-preferred maps** (GA collapse, invent→construct, number=expression) clearly marked `[user-preferred]` +- [x] **Source clusters documented** for each map +- [x] **Examples** drawn from cluster sub-reports (per the plan) +- [x] **Edge cases** documented for each map +- [x] **When-to-apply** rules documented for user-preferred maps +- [x] **5-rule constraints** documented +- [x] **Esoteric content NOT in any map** (secular sanitization per user 2026-06-23) +- [x] **User-specific entries tagged** `[user-also-accepted]` and `[user-preferred]` + +--- + +*End of `dedup_map.md`. Total: 6 maps, 3 principled + 3 user-preferred. Refined from the warmup's `report.md` §4. The principled spine is preserved; the user-preferred forms are clearly marked as optional output conventions.*