conductor(deob_warmup): Add §9 operator reference + decompress-names rule (2 user refinements)

Per user 2026-06-23 feedback on the pilot output:
1. **Decompress names AND expressions** (in prompt_template.md 'Your role'):
   - Name-bound terms should be DESCRIPTIVE, not single letters, unless the single letter is universally obvious (e.g., x for input, f for function)
   - Examples: p(X₁, ..., X_L) → language_model(sequence : Token^L) -> Probability : float64
                W · h + b → output_projection = weight_matrix.matmul(hidden_state) + bias_vector
                H(X) → entropy(distribution : Probability_Distribution) -> Entropy : float64
                K(X) → kolmogorov_complexity(object : Object) -> Complexity : int64
   - The LLM should NOT be afraid to translate expressions to multi-line definitions or build them up as constructions

2. **§9 Operator reference (indexed)** in report.md (new section):
   - 13 categories covering every operator the de-obfuscation uses in practice:
     arithmetic, comparison, logical, set-theoretic, type-theoretic, constructors, data-oriented, pipeline, sectors, type-class resolution, process, procedural/functional, why-this-exists
   - Each operator: symbol, name, behavior, type signature, example
   - Comprehensive expansion of the warmup's §3.3 14-primitive grammar
   - The LLM is expected to use this as a reference when applying the de-obfuscation

3. The 'while' operator is explicitly BANNED (per Rule 1) — use 'for', 'iterate', or 'Stream' instead.

These 2 refinements will be propagated forward:
- prompt_template.md 'Your role' updated (the LLM's direct operating stance)
- The §9 operator reference added to report.md (the warmup's design doc; the lexicon's source)
- Phase 3 (apply) TIER2_STARTER will reference both
This commit is contained in:
ed
2026-06-23 16:30:10 -04:00
parent 5b4448deaa
commit 59d048b51a
2 changed files with 177 additions and 0 deletions
@@ -11,6 +11,12 @@ You are a de-obfuscator. Your task: take a Pass 1 report (full of standard math
Your operational stance:
- **Library Specification > Philosophy** (per Cluster 0, Pattern 9): prefer executable, debuggable, deterministic specifications over intuition pumps.
- **Decompression > Compression** (per Cluster 0, P1): the first step for any math is to decompress it.
- **Decompress names AND expressions** (per user 2026-06-23): name-bound terms should be DESCRIPTIVE, not single letters, unless the single letter is universally obvious (e.g., `x` for input, `f` for function). Examples:
- `p(X₁, …, X_L)``language_model(sequence : Token^L) -> Probability : float64`
- `W · h + b``output_projection = weight_matrix.matmul(hidden_state) + bias_vector`
- `H(X)``entropy(distribution : Probability_Distribution) -> Entropy : float64`
- `K(X)``kolmogorov_complexity(object : Object) -> Complexity : int64`
The LLM should NOT be afraid to translate expressions to multi-line definitions or build them up as constructions when necessary. Compression is what the original math did; the de-obfuscation's job is to undo it.
- **Bounded form required** (per §1.1 of `report.md`): no `∞_val`; use `Stream A = nat -> A` for processes.
- **Form anchor required** (per §5): every re-encoding has a form anchor — "what bounded form does this project from the indefinite?"
- **Honest epistemic hedging** (per §1.10): if uncertain, flag it; do not guess.
@@ -625,6 +625,177 @@ The Phase 1 sub-agent dispatch was a success: the warmup now has 100% coverage o
---
## §9. Operator reference (indexed)
**Purpose.** This section is the **indexed reference** of every operator used in the de-obfuscation, with behavior + type signature + example per operator. The LLM and the reader can consult this when applying the lexicon to new material. The warmup's §3.3 has the 14-primitive grammar (the core forms); this section is the **comprehensive expansion** covering every operator the de-obfuscation uses in practice.
**Conventions:**
- **Symbol** is the LLM-facing form (ASCII preferred; math symbols used only when conventional)
- **Name** is the descriptive English label
- **Behavior** is 1-line ("what does it do")
- **Type** is the type signature (input → output)
- **Example** is a 1-2 line usage
### §9.1 Arithmetic
| Symbol | Name | Behavior | Type | Example |
|---|---|---|---|---|
| `+` | plus | sum of two values | `(A, A) -> A` (numeric) | `quantity(3) + quantity(5) = quantity(8) : int64` |
| `-` | minus | difference of two values | `(A, A) -> A` (numeric) | `quantity(10) - quantity(3) = quantity(7) : int64` |
| `*` | multiply | product of two values | `(A, A) -> A` (numeric) | `quantity(3) * quantity(4) = quantity(12) : int64` |
| `/` | divide | quotient of two values | `(A, A) -> A` (numeric) | `quantity(10) / quantity(2) = quantity(5) : float64` |
| `^` | power | a value raised to a power | `(A, A) -> A` (numeric) | `quantity(2) ^ quantity(3) = quantity(8) : int64` |
| `√` | square root | square root of a value | `(A) -> A` (numeric) | `sqrt(quantity(9)) = quantity(3) : float64` |
| `\|x\|` | absolute value | magnitude of a value | `(A) -> A` (numeric) | `abs(quantity(-5)) = quantity(5) : int64` |
| `mod` | modulo | remainder of division | `(A, A) -> A` (integer) | `quantity(10) mod quantity(3) = quantity(1) : int64` |
| `∏` | product (iterated) | product over a range | `(1..N -> A) -> A` | `product (i in 1..N) of p(i) = Π p(i)` |
| `∑` | sum (iterated) | sum over a range | `(1..N -> A) -> A` | `sum (i in 1..N) of p(i) = Σ p(i)` |
### §9.2 Comparison
| Symbol | Name | Behavior | Type | Example |
|---|---|---|---|---|
| `=` | equal | equality | `(A, A) -> Prop` | `quantity(3) = quantity(3) : Prop` |
| `≠` | not equal | inequality | `(A, A) -> Prop` | `quantity(3) ≠ quantity(4) : Prop` |
| `<` | less than | strict inequality | `(A, A) -> Prop` (ordered) | `quantity(3) < quantity(4) : Prop` |
| `>` | greater than | strict inequality | `(A, A) -> Prop` (ordered) | `quantity(4) > quantity(3) : Prop` |
| `≤` | less than or equal | non-strict inequality | `(A, A) -> Prop` (ordered) | `quantity(3) ≤ quantity(3) : Prop` |
| `≥` | greater than or equal | non-strict inequality | `(A, A) -> Prop` (ordered) | `quantity(3) ≥ quantity(3) : Prop` |
| `≡` | identical to / equivalent | definitional equality | `(A, A) -> Prop` (types) | `type_of(quantity(3)) ≡ int64` |
### §9.3 Logical
| Symbol | Name | Behavior | Type | Example |
|---|---|---|---|---|
| `and` | logical AND | both propositions hold | `(Prop, Prop) -> Prop` | `P and Q : Prop` |
| `or` | logical OR | either proposition holds | `(Prop, Prop) -> Prop` | `P or Q : Prop` |
| `not` | logical NOT | negation of a proposition | `(Prop) -> Prop` | `not P : Prop` |
| `implies` | implication | if-then | `(Prop, Prop) -> Prop` | `P implies Q : Prop` |
| `iff` | biconditional | if-and-only-if | `(Prop, Prop) -> Prop` | `P iff Q : Prop` |
| `forall` | universal quantification | for all x of type A, P holds | `(A -> Prop) -> Prop` | `forall (x : A), P(x) : Prop` |
| `exists` | existential quantification | there exists x of type A such that P | `(A -> Prop) -> Prop` | `exists (x : A), P(x) : Prop` |
### §9.4 Set-theoretic
| Symbol | Name | Behavior | Type | Example |
|---|---|---|---|---|
| `∈` | element of | x is in set S | `(A, kind A) -> Prop` | `x : Real in support(distribution) : Prop` |
| `⊆` | subset of | every element of S1 is in S2 | `(kind A, kind A) -> Prop` | `subkind(Nat, Int) : Prop` |
| `` | union | elements in either set | `(kind A, kind A) -> kind A` | `kind A = subkind A subkind B` |
| `∩` | intersection | elements in both sets | `(kind A, kind A) -> kind A` | `kind A = subkind A ∩ subkind B` |
| `∅` | empty set | no elements | `kind Bottom` | `empty_set : Bottom` |
### §9.5 Type-theoretic (per Cluster 3)
| Symbol | Name | Behavior | Type | Example |
|---|---|---|---|---|
| `: T` | type ascription | x has type T | `(value, type) -> typed value` | `x : Real` |
| `->` | function type | function from A to B | `(type, type) -> type` | `Real -> Probability : type` |
| `forall x : A, B` | dependent function (Pi) | function returning type depending on input | `(A -> type) -> type` | `forall (n : Nat), Vector(n) : type` |
| `exists x : A, B` | dependent pair (Sigma) | pair of (x : A) and (y : B(x)) | `(A -> type) -> type` | `exists (n : Nat), Vector(n)` |
| `lambda x . M` | lambda abstraction | anonymous function | `(A, term) -> term` | `lambda (x : Real). x * x` |
| `apply(f, x)` | function application | invoke f with argument | `(procedure, A) -> result` | `apply(square, quantity(3)) = quantity(9)` |
| `Bottom` | empty type | no values inhabit | `Type` | `empty_value : Bottom` (impossible) |
| `Top` | universal type | single inhabitant (unit) | `Type` | `unit_value : Top` |
| `Kind` | type of types | classifier of types | `Type` | `Real : Kind` |
### §9.6 Constructors (per Cluster 3's 4-rule pattern)
| Symbol | Name | Behavior | Type | Example |
|---|---|---|---|---|
| `formation` | formation rule | declares a type is well-formed | `(A, B, ...) -> rule` | `formation: A : type, B : type, -------, A -> B : type` |
| `intro` | introduction | constructs a value of a type | `(A) -> rule` | `intro: x : A, -------, lambda x . M : A -> B` |
| `elim` | elimination | consumes a value of a type | `(A) -> rule` | `elim: f : A -> B, x : A, -------, apply(f, x) : B` |
| `comp` | computation | β-reduction | `(A) -> rule` | `comp: apply(lambda x . M, N) = M[x := N]` |
| `uniq` | uniqueness | uniqueness of the elimination | `(A) -> rule` | `uniq: any two eliminations of same value yield same result` |
| `Build<A>` | Sigma projection (first) | extract first component of a pair | `(Sigma A B) -> A` | `Build<A>(pair) : A` |
| `Build<B>` | Sigma projection (second) | extract second component | `(Sigma A B) -> B` | `Build<B>(pair) : B` |
| `Zero` | natural number constructor | the natural number 0 | `Nat` | `zero : Zero` |
| `Succ(n)` | natural number constructor | the successor of n | `Nat -> Nat` | `succ(zero) : Succ(Zero)` |
### §9.7 Data-oriented (per Cluster 0 + 2)
| Symbol | Name | Behavior | Type | Example |
|---|---|---|---|---|
| `map` | transform each | apply f to each element | `(A -> B, list A) -> list B` | `map(square, [1, 2, 3]) = [1, 4, 9]` |
| `filter` | predicate | keep elements where p holds | `(A -> Prop, list A) -> list A` | `filter(even, [1, 2, 3, 4]) = [2, 4]` |
| `fold` | accumulate | reduce a list with f and base | `((B, A) -> B, B, list A) -> B` | `fold(+, 0, [1, 2, 3]) = 6` |
| `reduce` | (synonym for fold) | same as fold | same as fold | `reduce(max, 0, [3, 1, 4]) = 4` |
| `scan` | read source | enumerate elements of a source | `source -> stream A` | `scan(file_path) = stream(line)` |
| `select` | project columns | project specific columns | `(list column, table) -> table` | `select([name, age], table) = table'` |
| `sort` | order | sort elements by a key | `(A -> key, list A) -> list A` | `sort(age, people) = sorted_people` |
| `group` | partition | partition by a key | `(A -> key, list A) -> dict key (list A)` | `group(age, people) = dict` |
| `dedupe` | unique | remove duplicates | `(list A) -> list A` | `dedupe([1, 2, 2, 3]) = [1, 2, 3]` |
### §9.8 Pipeline (per Cluster 0 + 6 + 9)
| Symbol | Name | Behavior | Type | Example |
|---|---|---|---|---|
| `->` | data flow | output of left → input of right | `(A, A) -> A` (chain) | `scan -> filter -> map -> fold` |
| `<-` | input binding | the right side is the producer | `(A, producer A) -> A` | `for (i in 1..N) <- generate(i) = sequence` |
**Note on dual meaning of `->`:** In type context, `->` is the function type (`(A, B) -> C` = function from A, B to C). In pipeline context, `->` is data flow (`scan -> filter` = output of scan feeds filter). The LLM should disambiguate from context: in `(A) -> (B)` it's a function type; in `scan -> filter -> map` it's a pipeline.
### §9.9 Sectors (per Cluster 6 + 9, Sectored Language V1)
| Symbol | Name | Behavior | Type | Example |
|---|---|---|---|---|
| `static { ... }` | declaration block | declare types + constants, no execution | `(block) -> declaration` | `static { components : [n] Scalar }` |
| `exe { ... }` | execution block | execute statements, may have side effects | `(block) -> result` | `exe { sum := fold(+, zero, components) }` |
| `tape { ... }` | tape-drive region | arena-scoped block; contents pre-scattered to tape | `(block) -> result` | `tape { result := compute(weights, inputs) }` |
| `arena { ... }` | preemptive scatter region | Onat's term; pre-place arguments before consumption | `(block) -> result` | `arena { precompute(constants) }` |
### §9.10 Type-class resolution (per Rule 5)
| Symbol | Name | Behavior | Type | Example |
|---|---|---|---|---|
| `kind : Real` | type-class | resolves to `quantity : float64` (default encoding) | `(type) -> typed value` | `pi : kind : Real = quantity(3.14...) : float64` |
| `kind : Pi` | type-class | resolves to `quantity : float64` | `(type) -> typed value` | `pi : kind : Pi = quantity(3.14...) : float64` |
| `quantity(<value>) : <encoding>` | bounded form | a value with an explicit encoding | `(value, encoding) -> typed value` | `quantity(3.14) : float64` |
| `scalar : <encoding>` | bounded form (scalar) | a scalar with an explicit encoding | `(encoding) -> typed value` | `scalar : float64` |
| `vector : <encoding>` | bounded form (vector) | a vector with an explicit encoding | `(encoding) -> typed value` | `vector : float64` |
| `matrix : <encoding>` | bounded form (matrix) | a matrix with an explicit encoding | `(encoding) -> typed value` | `matrix : float64` |
### §9.11 Process (per Rule 1 + Cluster 0)
| Symbol | Name | Behavior | Type | Example |
|---|---|---|---|---|
| `Stream A` | potentially-infinite process | a function from nat to A | `type` | `Stream Compute = nat -> Compute` |
| `Limit(f, pivot)` | limit as a process | the limit of f at pivot | `(procedure, A) -> result` | `Limit(f, quantity(0)) = quantity(L)` |
| `coinductive A` | coinductive type | an infinite type defined by observation | `type` | `coinductive Stream = head : A, tail : Stream` |
| `F²` | explicit flip operator | the twice-applied "negative" (user's GA reframe) | `(A) -> A` | `F²(quantity(3)) = quantity(3)` (the user prefers F² over `negate`) |
### §9.12 Procedural / functional (per Cluster 2 + 4)
| Symbol | Name | Behavior | Type | Example |
|---|---|---|---|---|
| `procedure` | named function | a procedure (concatenative: a "word") | `(arg) -> result` | `procedure square (x : Real) -> Real : x * x` |
| `proc` | void-returning modifier | marks a procedure as side-effecting | `(modifier)` | `procedure log (msg : String) proc : print(msg)` |
| `let` | local bind | bind a name to a value in scope | `(name, value, scope) -> scope` | `let x = quantity(3) in x * x = quantity(9)` |
| `return` | function exit | exit the function with a value | `(value) -> result` | `procedure f (x : Real) -> Real : return x * x` |
| `if` | conditional | branch on a proposition | `(Prop, then, else) -> result` | `if (x > zero) then x else -x` |
| `for x in range` | bounded iteration | iterate over a bounded range | `(A, A, scope) -> result` | `for (i in 1..N), sum := sum + i` |
| `while` | (BANNED) | unbounded iteration | NOT ALLOWED (violates Rule 1) | use `for`, `iterate`, or `Stream` instead |
### §9.13 Why this section exists
The 2026-06-23 pilot produced de-obfuscation outputs that used **single-letter variables** (e.g., `p`, `W`, `H`, `K`) and **compressed expressions** (e.g., `p(X₁, …, X_L)`). This violated the user's "Decompression > Compression" directive. The pilot's refinements include adopting **descriptive names** + **multi-line constructions**. This operator reference is the LLM's reference for:
1. **Which operators exist** in the principled re-encoding (so the LLM uses them, not conventional math compressed forms).
2. **What each operator's behavior is** (so the LLM doesn't have to derive semantics each time).
3. **How operators compose** (type signatures show input → output).
**The LLM is expected to use this table as a reference.** When the LLM encounters a math expression, it should look up the relevant operators in this table, apply their principled re-encodings, and use descriptive names + multi-line constructions rather than single-letter compressions.
### §9.14 Cross-references
- **Per `lexicon.md` §2:** the 4 tiers (Tier 1: core concepts; Tier 2: data-oriented pipeline; Tier 3: type-theoretic primitives; Tier 4: AI-fuzzing tolerance). The operator reference above extends the lexicon's per-term entries with operator-level behavior.
- **Per `lexicon.md` §3.1:** Map 1 (Proofs = Programs = Computations) is operationalized through the Constructors + Procedural operators above.
- **Per `lexicon.md` §3.2:** Map 2 (Sets = Kinds = Types) is operationalized through the Type-theoretic operators + Type-class resolution above.
- **Per `lexicon.md` §3.3:** Map 3 (Functions = Procedures = Words) is operationalized through the `procedure` + `lambda` + `apply` operators above.
- **Per the warmup's §3.3:** the 14-primitive grammar is the SUBSET of these operators that the user explicitly named in their samples. This section is the full expansion.
---
*End of `report.md`. Total: 8 sections + Appendix A (provenance). Spec FR4 structure: complete. ~1,800 LOC main report + ~2,491 LOC cluster sub-reports = ~4,300 LOC total. Phase 1 (lexicon child) will refine and extend into the codified operational spec.*