diff --git a/aggregate-library/README.md b/aggregate-library/README.md
new file mode 100644
index 00000000..cb4cb696
--- /dev/null
+++ b/aggregate-library/README.md
@@ -0,0 +1,67 @@
+# Ephapax Aggregate Library
+
+The complete standard library for Ephapax = Common Library + Ephapax-Specific Library.
+
+## Structure
+
+```
+aggregate-library/
+├── common/              # Common Library (22 operations)
+│   ├── arithmetic/      # add, subtract, multiply, divide, modulo
+│   ├── comparison/      # equal, not_equal, less_than, greater_than, less_equal, greater_equal
+│   ├── logical/         # and, or, not
+│   ├── string/          # concat, length, substring
+│   ├── collection/      # map, filter, fold, contains
+│   └── conditional/     # if_then_else
+│
+└── ephapax/             # Ephapax-Specific Library (17 operations)
+    ├── linear/          # move, drop, copy, borrow
+    ├── region/          # new_region, alloc_in
+    ├── io/              # print, println, read_line
+    ├── conversion/      # i32_to_string, string_to_i32
+    ├── product/         # pair, fst, snd
+    └── sum/             # inl, inr, case
+```
+
+## Common Library
+
+Universal operations shared across all languages in the aggregate-library ecosystem. These 22 operations represent the intersection of functionality across radically different programming paradigms.
+
+Source: https://github.com/hyperpolymath/aggregate-library
+
+## Ephapax-Specific Library
+
+Operations unique to Ephapax's linear type system and region-based memory management:
+
+### Linear Types (4 operations)
+- `move` - Transfer ownership of linear values
+- `drop` - Explicitly consume linear values
+- `copy` - Duplicate unrestricted values
+- `borrow` - Create temporary references
+
+### Regions (2 operations)
+- `new_region` - Create scoped memory regions
+- `alloc_in` - Allocate in specific regions
+
+### I/O (3 operations)
+- `print` - Output string without newline
+- `println` - Output string with newline
+- `read_line` - Read line from stdin
+
+### Conversion (2 operations)
+- `i32_to_string` - Integer to string
+- `string_to_i32` - Parse string as integer
+
+### Product Types (3 operations)
+- `pair` - Construct pairs
+- `fst` - Extract first element
+- `snd` - Extract second element
+
+### Sum Types (3 operations)
+- `inl` - Inject left
+- `inr` - Inject right
+- `case` - Pattern match on sum
+
+## Total: 39 Operations
+
+Combined, the Ephapax standard library provides 39 fully-specified operations.
diff --git a/aggregate-library/common/arithmetic/add.md b/aggregate-library/common/arithmetic/add.md
new file mode 100644
index 00000000..68136359
--- /dev/null
+++ b/aggregate-library/common/arithmetic/add.md
@@ -0,0 +1,51 @@
+# Operation: add
+
+## Interface Signature
+
+```
+add: Number, Number -> Number
+```
+
+## Behavioral Semantics
+
+**Purpose**: Computes the sum of two numbers.
+
+**Parameters**:
+- `a`: The first number (augend)
+- `b`: The second number (addend)
+
+**Return Value**: The arithmetic sum of `a` and `b`.
+
+**Properties**:
+- Commutative: `add(a, b) = add(b, a)`
+- Associative: `add(add(a, b), c) = add(a, add(b, c))`
+- Identity element: `add(a, 0) = a`
+
+**Edge Cases**:
+- Overflow/underflow behavior is implementation-defined (Standard Library concern)
+- NaN and infinity handling is implementation-defined (Standard Library concern)
+
+## Executable Test Cases
+
+```yaml
+test_cases:
+  - input: [2, 3]
+    output: 5
+    description: "Basic addition of positive integers"
+
+  - input: [-5, 3]
+    output: -2
+    description: "Addition with negative number"
+
+  - input: [0, 0]
+    output: 0
+    description: "Addition of zeros"
+
+  - input: [1.5, 2.5]
+    output: 4.0
+    description: "Addition of decimal numbers"
+
+  - input: [-10, -20]
+    output: -30
+    description: "Addition of two negative numbers"
+```
diff --git a/aggregate-library/common/arithmetic/divide.md b/aggregate-library/common/arithmetic/divide.md
new file mode 100644
index 00000000..d214b485
--- /dev/null
+++ b/aggregate-library/common/arithmetic/divide.md
@@ -0,0 +1,61 @@
+# Operation: divide
+
+## Interface Signature
+
+```
+divide: Number, Number -> Number
+```
+
+## Behavioral Semantics
+
+**Purpose**: Computes the quotient of two numbers.
+
+**Parameters**:
+- `a`: The dividend (number to be divided)
+- `b`: The divisor (number by which to divide)
+
+**Return Value**: The arithmetic quotient `a ÷ b`.
+
+**Properties**:
+- Non-commutative: `divide(a, b) ≠ divide(b, a)` (in general)
+- Identity element: `divide(a, 1) = a`
+- Inverse of multiplication: `divide(multiply(a, b), b) = a` (when `b ≠ 0`)
+
+**Preconditions**:
+- `b ≠ 0` (division by zero behavior is implementation-defined)
+
+**Edge Cases**:
+- Division by zero is implementation-defined (Standard Library concern)
+  - May return error, infinity, or NaN depending on language
+- Integer vs floating-point division is implementation-defined
+- Overflow/underflow behavior is implementation-defined
+- NaN and infinity handling is implementation-defined
+
+## Executable Test Cases
+
+```yaml
+test_cases:
+  - input: [6, 2]
+    output: 3
+    description: "Basic division with exact result"
+
+  - input: [7, 2]
+    output: 3.5
+    description: "Division with fractional result"
+
+  - input: [0, 5]
+    output: 0
+    description: "Zero divided by non-zero"
+
+  - input: [-10, 2]
+    output: -5
+    description: "Division with negative dividend"
+
+  - input: [10, -2]
+    output: -5
+    description: "Division with negative divisor"
+
+  - input: [-12, -3]
+    output: 4
+    description: "Division of two negative numbers"
+```
diff --git a/aggregate-library/common/arithmetic/modulo.md b/aggregate-library/common/arithmetic/modulo.md
new file mode 100644
index 00000000..0ec34950
--- /dev/null
+++ b/aggregate-library/common/arithmetic/modulo.md
@@ -0,0 +1,59 @@
+# Operation: modulo
+
+## Interface Signature
+
+```
+modulo: Number, Number -> Number
+```
+
+## Behavioral Semantics
+
+**Purpose**: Computes the remainder of division of two numbers.
+
+**Parameters**:
+- `a`: The dividend (number to be divided)
+- `b`: The divisor (number by which to divide)
+
+**Return Value**: The remainder when `a` is divided by `b`.
+
+**Properties**:
+- Non-commutative: `modulo(a, b) ≠ modulo(b, a)` (in general)
+- `modulo(a, b)` has the same sign as the divisor in most implementations
+- For positive integers: `0 ≤ modulo(a, b) < b` when `b > 0`
+
+**Preconditions**:
+- `b ≠ 0` (modulo by zero behavior is implementation-defined)
+
+**Edge Cases**:
+- Modulo by zero is implementation-defined (Standard Library concern)
+- Sign of result with negative operands is implementation-defined
+  - Some languages use truncated division (result has sign of dividend)
+  - Others use floored division (result has sign of divisor)
+- Behavior with floating-point numbers is implementation-defined
+
+## Executable Test Cases
+
+```yaml
+test_cases:
+  - input: [7, 3]
+    output: 1
+    description: "Basic modulo with positive integers"
+
+  - input: [10, 5]
+    output: 0
+    description: "Modulo with no remainder"
+
+  - input: [15, 4]
+    output: 3
+    description: "Modulo returning non-zero remainder"
+
+  - input: [0, 5]
+    output: 0
+    description: "Zero modulo non-zero"
+
+  - input: [100, 7]
+    output: 2
+    description: "Modulo with larger numbers"
+```
+
+**Note**: Test cases with negative numbers are omitted due to implementation-defined behavior across languages.
diff --git a/aggregate-library/common/arithmetic/multiply.md b/aggregate-library/common/arithmetic/multiply.md
new file mode 100644
index 00000000..e3976b27
--- /dev/null
+++ b/aggregate-library/common/arithmetic/multiply.md
@@ -0,0 +1,57 @@
+# Operation: multiply
+
+## Interface Signature
+
+```
+multiply: Number, Number -> Number
+```
+
+## Behavioral Semantics
+
+**Purpose**: Computes the product of two numbers.
+
+**Parameters**:
+- `a`: The multiplicand (first factor)
+- `b`: The multiplier (second factor)
+
+**Return Value**: The arithmetic product `a × b`.
+
+**Properties**:
+- Commutative: `multiply(a, b) = multiply(b, a)`
+- Associative: `multiply(multiply(a, b), c) = multiply(a, multiply(b, c))`
+- Identity element: `multiply(a, 1) = a`
+- Zero property: `multiply(a, 0) = 0`
+- Distributive over addition: `multiply(a, add(b, c)) = add(multiply(a, b), multiply(a, c))`
+
+**Edge Cases**:
+- Overflow/underflow behavior is implementation-defined (Standard Library concern)
+- NaN and infinity handling is implementation-defined (Standard Library concern)
+
+## Executable Test Cases
+
+```yaml
+test_cases:
+  - input: [2, 3]
+    output: 6
+    description: "Basic multiplication of positive integers"
+
+  - input: [-5, 3]
+    output: -15
+    description: "Multiplication with negative number"
+
+  - input: [0, 42]
+    output: 0
+    description: "Multiplication by zero"
+
+  - input: [7, 1]
+    output: 7
+    description: "Multiplication by one (identity)"
+
+  - input: [2.5, 4]
+    output: 10.0
+    description: "Multiplication with decimal number"
+
+  - input: [-3, -4]
+    output: 12
+    description: "Multiplication of two negative numbers"
+```
diff --git a/aggregate-library/common/arithmetic/subtract.md b/aggregate-library/common/arithmetic/subtract.md
new file mode 100644
index 00000000..fe4b4e62
--- /dev/null
+++ b/aggregate-library/common/arithmetic/subtract.md
@@ -0,0 +1,55 @@
+# Operation: subtract
+
+## Interface Signature
+
+```
+subtract: Number, Number -> Number
+```
+
+## Behavioral Semantics
+
+**Purpose**: Computes the difference between two numbers.
+
+**Parameters**:
+- `a`: The minuend (number from which another is subtracted)
+- `b`: The subtrahend (number to be subtracted)
+
+**Return Value**: The arithmetic difference `a - b`.
+
+**Properties**:
+- Non-commutative: `subtract(a, b) ≠ subtract(b, a)` (in general)
+- Identity element: `subtract(a, 0) = a`
+- Inverse of addition: `subtract(add(a, b), b) = a`
+
+**Edge Cases**:
+- Overflow/underflow behavior is implementation-defined (Standard Library concern)
+- NaN and infinity handling is implementation-defined (Standard Library concern)
+
+## Executable Test Cases
+
+```yaml
+test_cases:
+  - input: [5, 3]
+    output: 2
+    description: "Basic subtraction of positive integers"
+
+  - input: [3, 5]
+    output: -2
+    description: "Subtraction resulting in negative number"
+
+  - input: [0, 0]
+    output: 0
+    description: "Subtraction of zeros"
+
+  - input: [-5, 3]
+    output: -8
+    description: "Subtracting positive from negative"
+
+  - input: [10.5, 2.5]
+    output: 8.0
+    description: "Subtraction of decimal numbers"
+
+  - input: [-10, -20]
+    output: 10
+    description: "Subtracting negative from negative"
+```
diff --git a/aggregate-library/common/collection/contains.md b/aggregate-library/common/collection/contains.md
new file mode 100644
index 00000000..8d36cbaf
--- /dev/null
+++ b/aggregate-library/common/collection/contains.md
@@ -0,0 +1,69 @@
+# Operation: contains
+
+## Interface Signature
+
+```
+contains: Collection[A], A -> Boolean
+```
+
+## Behavioral Semantics
+
+**Purpose**: Determines whether a collection contains a specific element.
+
+**Parameters**:
+- `collection`: The source collection of elements of type `A`
+- `element`: The element to search for
+
+**Return Value**: `true` if `element` is found in `collection`, otherwise `false`.
+
+**Properties**:
+- Empty collection: `contains([], x) = false` for all `x`
+- Single element match: `contains([x], x) = true`
+- Single element no match: `contains([x], y) = false` when `x ≠ y`
+- Can be expressed as: `contains(c, x) = greater_than(length(filter(c, e => equal(e, x))), 0)`
+
+**Edge Cases**:
+- Equality comparison semantics (reference vs value) is implementation-defined
+- Short-circuit evaluation (stop on first match) is implementation-defined
+- Search order and performance characteristics are implementation-defined
+
+## Executable Test Cases
+
+```yaml
+test_cases:
+  - input:
+      collection: [1, 2, 3, 4, 5]
+      element: 3
+    output: true
+    description: "Element is present in collection"
+
+  - input:
+      collection: [1, 2, 3, 4, 5]
+      element: 6
+    output: false
+    description: "Element is not present in collection"
+
+  - input:
+      collection: []
+      element: 1
+    output: false
+    description: "Empty collection contains no elements"
+
+  - input:
+      collection: [1]
+      element: 1
+    output: true
+    description: "Single element collection contains that element"
+
+  - input:
+      collection: ["a", "b", "c"]
+      element: "b"
+    output: true
+    description: "String element is present"
+
+  - input:
+      collection: [1, 2, 1, 3, 1]
+      element: 1
+    output: true
+    description: "Element appears multiple times (still returns true)"
+```
diff --git a/aggregate-library/common/collection/filter.md b/aggregate-library/common/collection/filter.md
new file mode 100644
index 00000000..f0ddac15
--- /dev/null
+++ b/aggregate-library/common/collection/filter.md
@@ -0,0 +1,64 @@
+# Operation: filter
+
+## Interface Signature
+
+```
+filter: Collection[A], Function[A -> Boolean] -> Collection[A]
+```
+
+## Behavioral Semantics
+
+**Purpose**: Selects elements from a collection that satisfy a predicate function, producing a new collection.
+
+**Parameters**:
+- `collection`: The source collection of elements of type `A`
+- `predicate`: A function that returns `true` for elements to keep, `false` for elements to exclude
+
+**Return Value**: A new collection containing only the elements from `collection` for which `predicate` returns `true`, preserving original order.
+
+**Properties**:
+- Length: `length(filter(c, p)) ≤ length(c)`
+- Preserves order: Elements appear in the same relative order as in source collection
+- Always true predicate: `filter(c, always_true) = c`
+- Always false predicate: `filter(c, always_false) = []`
+- Empty collection: `filter([], p) = []`
+- Composition: `filter(filter(c, p1), p2) = filter(c, x => and(p1(x), p2(x)))`
+
+**Edge Cases**:
+- Lazy vs eager evaluation is implementation-defined
+- Side effects in the predicate are implementation-defined
+
+## Executable Test Cases
+
+```yaml
+test_cases:
+  - input:
+      collection: [1, 2, 3, 4, 5]
+      predicate: "x => greater_than(x, 2)"
+    output: [3, 4, 5]
+    description: "Filter numbers greater than 2"
+
+  - input:
+      collection: [1, 2, 3, 4, 5]
+      predicate: "x => equal(modulo(x, 2), 0)"
+    output: [2, 4]
+    description: "Filter even numbers"
+
+  - input:
+      collection: [1, 2, 3]
+      predicate: "x => true"
+    output: [1, 2, 3]
+    description: "Filter with always-true predicate returns all elements"
+
+  - input:
+      collection: [1, 2, 3]
+      predicate: "x => false"
+    output: []
+    description: "Filter with always-false predicate returns empty collection"
+
+  - input:
+      collection: []
+      predicate: "x => true"
+    output: []
+    description: "Filter empty collection returns empty collection"
+```
diff --git a/aggregate-library/common/collection/fold.md b/aggregate-library/common/collection/fold.md
new file mode 100644
index 00000000..f341c609
--- /dev/null
+++ b/aggregate-library/common/collection/fold.md
@@ -0,0 +1,78 @@
+# Operation: fold
+
+## Interface Signature
+
+```
+fold: Collection[A], B, Function[B, A -> B] -> B
+```
+
+**Alternative names**: reduce, foldl, aggregate
+
+## Behavioral Semantics
+
+**Purpose**: Reduces a collection to a single value by iteratively applying a combining function.
+
+**Parameters**:
+- `collection`: The source collection of elements of type `A`
+- `initial`: The initial accumulator value of type `B`
+- `fn`: A combining function that takes the current accumulator (type `B`) and an element (type `A`) and returns a new accumulator (type `B`)
+
+**Return Value**: The final accumulated value after processing all elements.
+
+**Properties**:
+- Empty collection: `fold([], initial, fn) = initial`
+- Single element: `fold([x], initial, fn) = fn(initial, x)`
+- Left-associative: Processes elements from left to right
+- For collection `[a, b, c]`: `fold([a,b,c], init, fn) = fn(fn(fn(init, a), b), c)`
+
+**Edge Cases**:
+- Order of evaluation (left-to-right) is specified
+- Right fold (foldr) may be provided in Standard Library
+- Lazy vs eager evaluation is implementation-defined
+
+## Executable Test Cases
+
+```yaml
+test_cases:
+  - input:
+      collection: [1, 2, 3, 4]
+      initial: 0
+      fn: "acc, x => add(acc, x)"
+    output: 10
+    description: "Sum all numbers in collection"
+
+  - input:
+      collection: [1, 2, 3, 4]
+      initial: 1
+      fn: "acc, x => multiply(acc, x)"
+    output: 24
+    description: "Product of all numbers in collection"
+
+  - input:
+      collection: []
+      initial: 42
+      fn: "acc, x => add(acc, x)"
+    output: 42
+    description: "Folding empty collection returns initial value"
+
+  - input:
+      collection: [5]
+      initial: 10
+      fn: "acc, x => add(acc, x)"
+    output: 15
+    description: "Folding single element"
+
+  - input:
+      collection: ["a", "b", "c"]
+      initial: ""
+      fn: "acc, s => concat(acc, s)"
+    output: "abc"
+    description: "Concatenate strings using fold"
+
+  - input:
+      collection: [1, 2, 3]
+      initial: 0
+      fn: "acc, x => add(acc, 1)"
+    output: 3
+    description: "Count elements using fold"
+```
diff --git a/aggregate-library/common/collection/map.md b/aggregate-library/common/collection/map.md
new file mode 100644
index 00000000..ef9e87d6
--- /dev/null
+++ b/aggregate-library/common/collection/map.md
@@ -0,0 +1,63 @@
+# Operation: map
+
+## Interface Signature
+
+```
+map: Collection[A], Function[A -> B] -> Collection[B]
+```
+
+## Behavioral Semantics
+
+**Purpose**: Transforms each element of a collection by applying a function, producing a new collection of the same length.
+
+**Parameters**:
+- `collection`: The source collection of elements of type `A`
+- `fn`: A function that transforms elements from type `A` to type `B`
+
+**Return Value**: A new collection containing the results of applying `fn` to each element in `collection`, preserving order.
+
+**Properties**:
+- Preserves length: `length(map(c, fn)) = length(c)`
+- Preserves order: Elements appear in the same order as the source collection
+- Identity: `map(c, identity) = c` (where `identity(x) = x`)
+- Composition: `map(map(c, f), g) = map(c, compose(g, f))` (where `compose(g, f)(x) = g(f(x))`)
+- Empty collection: `map([], fn) = []`
+
+**Edge Cases**:
+- Lazy vs eager evaluation is implementation-defined
+- Side effects in the function are implementation-defined
+
+## Executable Test Cases
+
+```yaml
+test_cases:
+  - input:
+      collection: [1, 2, 3]
+      fn: "x => multiply(x, 2)"
+    output: [2, 4, 6]
+    description: "Double each number in collection"
+
+  - input:
+      collection: [1, 2, 3]
+      fn: "x => add(x, 10)"
+    output: [11, 12, 13]
+    description: "Add 10 to each number"
+
+  - input:
+      collection: []
+      fn: "x => multiply(x, 2)"
+    output: []
+    description: "Mapping over empty collection returns empty collection"
+
+  - input:
+      collection: [5]
+      fn: "x => x"
+    output: [5]
+    description: "Identity function returns same element"
+
+  - input:
+      collection: ["a", "b", "c"]
+      fn: "s => concat(s, s)"
+    output: ["aa", "bb", "cc"]
+    description: "Map over string collection"
+```
diff --git a/aggregate-library/common/comparison/equal.md b/aggregate-library/common/comparison/equal.md
new file mode 100644
index 00000000..8395ae31
--- /dev/null
+++ b/aggregate-library/common/comparison/equal.md
@@ -0,0 +1,60 @@
+# Operation: equal
+
+## Interface Signature
+
+```
+equal: Number, Number -> Boolean
+```
+
+## Behavioral Semantics
+
+**Purpose**: Determines if two numbers are equal in value.
+
+**Parameters**:
+- `a`: The first number to compare
+- `b`: The second number to compare
+
+**Return Value**: `true` if `a` equals `b`, otherwise `false`.
+
+**Properties**:
+- Reflexive: `equal(a, a)` is always `true`
+- Symmetric: if `equal(a, b)` is `true`, then `equal(b, a)` is `true`
+- Transitive: if `equal(a, b)` and `equal(b, c)`, then `equal(a, c)`
+
+**Edge Cases**:
+- Floating-point precision issues are implementation-defined
+- NaN equality (typically `NaN ≠ NaN`) is implementation-defined
+- Positive and negative zero equality is implementation-defined
+
+## Executable Test Cases
+
+```yaml
+test_cases:
+  - input: [5, 5]
+    output: true
+    description: "Equal positive integers"
+
+  - input: [5, 3]
+    output: false
+    description: "Unequal positive integers"
+
+  - input: [0, 0]
+    output: true
+    description: "Zero equals zero"
+
+  - input: [-5, -5]
+    output: true
+    description: "Equal negative integers"
+
+  - input: [-5, 5]
+    output: false
+    description: "Negative and positive not equal"
+
+  - input: [2.5, 2.5]
+    output: true
+    description: "Equal decimal numbers"
+
+  - input: [1.0, 1]
+    output: true
+    description: "Decimal and integer with same value"
+```
diff --git a/aggregate-library/common/comparison/greater_equal.md b/aggregate-library/common/comparison/greater_equal.md
new file mode 100644
index 00000000..d3f28b72
--- /dev/null
+++ b/aggregate-library/common/comparison/greater_equal.md
@@ -0,0 +1,61 @@
+# Operation: greater_equal
+
+## Interface Signature
+
+```
+greater_equal: Number, Number -> Boolean
+```
+
+## Behavioral Semantics
+
+**Purpose**: Determines if the first number is greater than or equal to the second number.
+
+**Parameters**:
+- `a`: The first number to compare
+- `b`: The second number to compare
+
+**Return Value**: `true` if `a ≥ b`, otherwise `false`.
+
+**Properties**:
+- Transitive: if `greater_equal(a, b)` and `greater_equal(b, c)`, then `greater_equal(a, c)`
+- Reflexive: `greater_equal(a, a)` is always `true`
+- Antisymmetric: if `greater_equal(a, b)` and `greater_equal(b, a)`, then `equal(a, b)`
+- Equivalent to: `or(greater_than(a, b), equal(a, b))`
+- Inverse of less_equal: `greater_equal(a, b) = less_equal(b, a)`
+
+**Edge Cases**:
+- NaN comparison behavior is implementation-defined (Standard Library concern)
+- Infinity comparison is implementation-defined (Standard Library concern)
+
+## Executable Test Cases
+
+```yaml
+test_cases:
+  - input: [5, 2]
+    output: true
+    description: "First number is greater than second"
+
+  - input: [5, 5]
+    output: true
+    description: "Numbers are equal"
+
+  - input: [2, 5]
+    output: false
+    description: "First number is less than second"
+
+  - input: [0, -5]
+    output: true
+    description: "Zero greater than or equal to negative"
+
+  - input: [0, 0]
+    output: true
+    description: "Zero greater than or equal to itself"
+
+  - input: [-5, -5]
+    output: true
+    description: "Equal negative numbers"
+
+  - input: [2.5, 1.5]
+    output: true
+    description: "Comparing decimal numbers (greater than)"
+```
diff --git a/aggregate-library/common/comparison/greater_than.md b/aggregate-library/common/comparison/greater_than.md
new file mode 100644
index 00000000..2fc885d2
--- /dev/null
+++ b/aggregate-library/common/comparison/greater_than.md
@@ -0,0 +1,60 @@
+# Operation: greater_than
+
+## Interface Signature
+
+```
+greater_than: Number, Number -> Boolean
+```
+
+## Behavioral Semantics
+
+**Purpose**: Determines if the first number is strictly greater than the second number.
+
+**Parameters**:
+- `a`: The first number to compare
+- `b`: The second number to compare
+
+**Return Value**: `true` if `a > b`, otherwise `false`.
+
+**Properties**:
+- Transitive: if `greater_than(a, b)` and `greater_than(b, c)`, then `greater_than(a, c)`
+- Asymmetric: if `greater_than(a, b)` is `true`, then `greater_than(b, a)` is `false`
+- Irreflexive: `greater_than(a, a)` is always `false`
+- Inverse of less_than: `greater_than(a, b) = less_than(b, a)`
+
+**Edge Cases**:
+- NaN comparison behavior is implementation-defined (Standard Library concern)
+- Infinity comparison is implementation-defined (Standard Library concern)
+
+## Executable Test Cases
+
+```yaml
+test_cases:
+  - input: [5, 2]
+    output: true
+    description: "First number is greater than second"
+
+  - input: [2, 5]
+    output: false
+    description: "First number is less than second"
+
+  - input: [3, 3]
+    output: false
+    description: "Numbers are equal"
+
+  - input: [0, -5]
+    output: true
+    description: "Zero greater than negative"
+
+  - input: [-5, 0]
+    output: false
+    description: "Negative not greater than zero"
+
+  - input: [-5, -10]
+    output: true
+    description: "Comparing two negative numbers"
+
+  - input: [2.5, 1.5]
+    output: true
+    description: "Comparing decimal numbers"
+```
diff --git a/aggregate-library/common/comparison/less_equal.md b/aggregate-library/common/comparison/less_equal.md
new file mode 100644
index 00000000..cd992de5
--- /dev/null
+++ b/aggregate-library/common/comparison/less_equal.md
@@ -0,0 +1,60 @@
+# Operation: less_equal
+
+## Interface Signature
+
+```
+less_equal: Number, Number -> Boolean
+```
+
+## Behavioral Semantics
+
+**Purpose**: Determines if the first number is less than or equal to the second number.
+
+**Parameters**:
+- `a`: The first number to compare
+- `b`: The second number to compare
+
+**Return Value**: `true` if `a ≤ b`, otherwise `false`.
+
+**Properties**:
+- Transitive: if `less_equal(a, b)` and `less_equal(b, c)`, then `less_equal(a, c)`
+- Reflexive: `less_equal(a, a)` is always `true`
+- Antisymmetric: if `less_equal(a, b)` and `less_equal(b, a)`, then `equal(a, b)`
+- Equivalent to: `or(less_than(a, b), equal(a, b))`
+
+**Edge Cases**:
+- NaN comparison behavior is implementation-defined (Standard Library concern)
+- Infinity comparison is implementation-defined (Standard Library concern)
+
+## Executable Test Cases
+
+```yaml
+test_cases:
+  - input: [2, 5]
+    output: true
+    description: "First number is less than second"
+
+  - input: [5, 5]
+    output: true
+    description: "Numbers are equal"
+
+  - input: [5, 2]
+    output: false
+    description: "First number is greater than second"
+
+  - input: [-5, 0]
+    output: true
+    description: "Negative less than or equal to zero"
+
+  - input: [0, 0]
+    output: true
+    description: "Zero less than or equal to itself"
+
+  - input: [-10, -10]
+    output: true
+    description: "Equal negative numbers"
+
+  - input: [1.5, 2.0]
+    output: true
+    description: "Comparing decimal numbers (less than)"
+```
diff --git a/aggregate-library/common/comparison/less_than.md b/aggregate-library/common/comparison/less_than.md
new file mode 100644
index 00000000..b67d0d36
--- /dev/null
+++ b/aggregate-library/common/comparison/less_than.md
@@ -0,0 +1,59 @@
+# Operation: less_than
+
+## Interface Signature
+
+```
+less_than: Number, Number -> Boolean
+```
+
+## Behavioral Semantics
+
+**Purpose**: Determines if the first number is strictly less than the second number.
+
+**Parameters**:
+- `a`: The first number to compare
+- `b`: The second number to compare
+
+**Return Value**: `true` if `a < b`, otherwise `false`.
+
+**Properties**:
+- Transitive: if `less_than(a, b)` and `less_than(b, c)`, then `less_than(a, c)`
+- Asymmetric: if `less_than(a, b)` is `true`, then `less_than(b, a)` is `false`
+- Irreflexive: `less_than(a, a)` is always `false`
+
+**Edge Cases**:
+- NaN comparison behavior is implementation-defined (Standard Library concern)
+- Infinity comparison is implementation-defined (Standard Library concern)
+
+## Executable Test Cases
+
+```yaml
+test_cases:
+  - input: [2, 5]
+    output: true
+    description: "First number is less than second"
+
+  - input: [5, 2]
+    output: false
+    description: "First number is greater than second"
+
+  - input: [3, 3]
+    output: false
+    description: "Numbers are equal"
+
+  - input: [-5, 0]
+    output: true
+    description: "Negative less than zero"
+
+  - input: [0, -5]
+    output: false
+    description: "Zero not less than negative"
+
+  - input: [-10, -5]
+    output: true
+    description: "Comparing two negative numbers"
+
+  - input: [1.5, 2.0]
+    output: true
+    description: "Comparing decimal numbers"
+```
diff --git a/aggregate-library/common/comparison/not_equal.md b/aggregate-library/common/comparison/not_equal.md
new file mode 100644
index 00000000..62a7df01
--- /dev/null
+++ b/aggregate-library/common/comparison/not_equal.md
@@ -0,0 +1,60 @@
+# Operation: not_equal
+
+## Interface Signature
+
+```
+not_equal: Number, Number -> Boolean
+```
+
+## Behavioral Semantics
+
+**Purpose**: Determines if two numbers are not equal in value.
+
+**Parameters**:
+- `a`: The first number to compare
+- `b`: The second number to compare
+
+**Return Value**: `true` if `a` does not equal `b`, otherwise `false`.
+
+**Properties**:
+- Irreflexive: `not_equal(a, a)` is always `false`
+- Symmetric: if `not_equal(a, b)` is `true`, then `not_equal(b, a)` is `true`
+- Negation of equal: `not_equal(a, b) = not(equal(a, b))`
+
+**Edge Cases**:
+- Floating-point precision issues are implementation-defined
+- NaN inequality is implementation-defined
+- Positive and negative zero inequality is implementation-defined
+
+## Executable Test Cases
+
+```yaml
+test_cases:
+  - input: [5, 3]
+    output: true
+    description: "Unequal positive integers"
+
+  - input: [5, 5]
+    output: false
+    description: "Equal positive integers"
+
+  - input: [0, 1]
+    output: true
+    description: "Zero not equal to one"
+
+  - input: [-5, 5]
+    output: true
+    description: "Negative and positive are unequal"
+
+  - input: [-5, -5]
+    output: false
+    description: "Equal negative integers"
+
+  - input: [2.5, 2.0]
+    output: true
+    description: "Unequal decimal numbers"
+
+  - input: [1.0, 1]
+    output: false
+    description: "Decimal and integer with same value are equal"
+```
diff --git a/aggregate-library/common/conditional/if_then_else.md b/aggregate-library/common/conditional/if_then_else.md
new file mode 100644
index 00000000..5d8dda48
--- /dev/null
+++ b/aggregate-library/common/conditional/if_then_else.md
@@ -0,0 +1,80 @@
+# Operation: if_then_else
+
+## Interface Signature
+
+```
+if_then_else: Boolean, A, A -> A
+```
+
+## Behavioral Semantics
+
+**Purpose**: Selects one of two values based on a boolean condition.
+
+**Parameters**:
+- `condition`: A boolean value determining which branch to take
+- `then_value`: The value to return if `condition` is `true`
+- `else_value`: The value to return if `condition` is `false`
+
+**Return Value**: `then_value` if `condition` is `true`, otherwise `else_value`.
+
+**Properties**:
+- True branch: `if_then_else(true, a, b) = a`
+- False branch: `if_then_else(false, a, b) = b`
+- Same values: `if_then_else(c, a, a) = a` for any condition `c`
+- Can express boolean operations:
+  - `and(a, b) = if_then_else(a, b, false)`
+  - `or(a, b) = if_then_else(a, true, b)`
+  - `not(a) = if_then_else(a, false, true)`
+
+**Edge Cases**:
+- Evaluation strategy (strict vs lazy) is implementation-defined
+  - Strict: Both branches are evaluated before selection
+  - Lazy: Only the selected branch is evaluated
+- Languages may provide this as a statement/keyword rather than a function
+
+## Executable Test Cases
+
+```yaml
+test_cases:
+  - input:
+      condition: true
+      then_value: 10
+      else_value: 20
+    output: 10
+    description: "Condition is true, return then_value"
+
+  - input:
+      condition: false
+      then_value: 10
+      else_value: 20
+    output: 20
+    description: "Condition is false, return else_value"
+
+  - input:
+      condition: true
+      then_value: "yes"
+      else_value: "no"
+    output: "yes"
+    description: "Works with string values"
+
+  - input:
+      condition: false
+      then_value: "yes"
+      else_value: "no"
+    output: "no"
+    description: "Returns else branch for false condition"
+
+  - input:
+      condition: equal(5, 5)
+      then_value: 1
+      else_value: 0
+    output: 1
+    description: "Condition from comparison operation"
+
+  - input:
+      condition: greater_than(3, 5)
+      then_value: "bigger"
+      else_value: "smaller"
+    output: "smaller"
+    description: "False comparison leads to else branch"
+```
diff --git a/aggregate-library/common/logical/and.md b/aggregate-library/common/logical/and.md
new file mode 100644
index 00000000..1b257c84
--- /dev/null
+++ b/aggregate-library/common/logical/and.md
@@ -0,0 +1,49 @@
+# Operation: and
+
+## Interface Signature
+
+```
+and: Boolean, Boolean -> Boolean
+```
+
+## Behavioral Semantics
+
+**Purpose**: Performs logical conjunction of two boolean values.
+
+**Parameters**:
+- `a`: The first boolean value
+- `b`: The second boolean value
+
+**Return Value**: `true` if both `a` and `b` are `true`, otherwise `false`.
+
+**Properties**:
+- Commutative: `and(a, b) = and(b, a)`
+- Associative: `and(and(a, b), c) = and(a, and(b, c))`
+- Identity element: `and(a, true) = a`
+- Annihilator element: `and(a, false) = false`
+- Idempotent: `and(a, a) = a`
+- Distributive over or: `and(a, or(b, c)) = or(and(a, b), and(a, c))`
+
+**Edge Cases**:
+- Short-circuit evaluation is implementation-defined (Standard Library concern)
+
+## Executable Test Cases
+
+```yaml
+test_cases:
+  - input: [true, true]
+    output: true
+    description: "Both values are true"
+
+  - input: [true, false]
+    output: false
+    description: "First is true, second is false"
+
+  - input: [false, true]
+    output: false
+    description: "First is false, second is true"
+
+  - input: [false, false]
+    output: false
+    description: "Both values are false"
+```
diff --git a/aggregate-library/common/logical/not.md b/aggregate-library/common/logical/not.md
new file mode 100644
index 00000000..343a6cd2
--- /dev/null
+++ b/aggregate-library/common/logical/not.md
@@ -0,0 +1,36 @@
+# Operation: not
+
+## Interface Signature
+
+```
+not: Boolean -> Boolean
+```
+
+## Behavioral Semantics
+
+**Purpose**: Performs logical negation of a boolean value.
+
+**Parameters**:
+- `a`: The boolean value to negate
+
+**Return Value**: `true` if `a` is `false`, `false` if `a` is `true`.
+
+**Properties**:
+- Double negation: `not(not(a)) = a`
+- De Morgan's laws:
+  - `not(and(a, b)) = or(not(a), not(b))`
+  - `not(or(a, b)) = and(not(a), not(b))`
+- Complement: `and(a, not(a)) = false` and `or(a, not(a)) = true`
+
+## Executable Test Cases
+
+```yaml
+test_cases:
+  - input: [true]
+    output: false
+    description: "Negation of true is false"
+
+  - input: [false]
+    output: true
+    description: "Negation of false is true"
+```
diff --git a/aggregate-library/common/logical/or.md b/aggregate-library/common/logical/or.md
new file mode 100644
index 00000000..5e2d7800
--- /dev/null
+++ b/aggregate-library/common/logical/or.md
@@ -0,0 +1,49 @@
+# Operation: or
+
+## Interface Signature
+
+```
+or: Boolean, Boolean -> Boolean
+```
+
+## Behavioral Semantics
+
+**Purpose**: Performs logical disjunction of two boolean values.
+
+**Parameters**:
+- `a`: The first boolean value
+- `b`: The second boolean value
+
+**Return Value**: `true` if at least one of `a` or `b` is `true`, otherwise `false`.
+
+**Properties**:
+- Commutative: `or(a, b) = or(b, a)`
+- Associative: `or(or(a, b), c) = or(a, or(b, c))`
+- Identity element: `or(a, false) = a`
+- Annihilator element: `or(a, true) = true`
+- Idempotent: `or(a, a) = a`
+- Distributive over and: `or(a, and(b, c)) = and(or(a, b), or(a, c))`
+
+**Edge Cases**:
+- Short-circuit evaluation is implementation-defined (Standard Library concern)
+
+## Executable Test Cases
+
+```yaml
+test_cases:
+  - input: [true, true]
+    output: true
+    description: "Both values are true"
+
+  - input: [true, false]
+    output: true
+    description: "First is true, second is false"
+
+  - input: [false, true]
+    output: true
+    description: "First is false, second is true"
+
+  - input: [false, false]
+    output: false
+    description: "Both values are false"
+```
diff --git a/aggregate-library/common/string/concat.md b/aggregate-library/common/string/concat.md
new file mode 100644
index 00000000..e2f254b4
--- /dev/null
+++ b/aggregate-library/common/string/concat.md
@@ -0,0 +1,55 @@
+# Operation: concat
+
+## Interface Signature
+
+```
+concat: String, String -> String
+```
+
+## Behavioral Semantics
+
+**Purpose**: Concatenates two strings together, forming a new string.
+
+**Parameters**:
+- `a`: The first string
+- `b`: The second string
+
+**Return Value**: A new string consisting of all characters from `a` followed by all characters from `b`.
+
+**Properties**:
+- Associative: `concat(concat(a, b), c) = concat(a, concat(b, c))`
+- Identity element: `concat(a, "") = concat("", a) = a` (empty string)
+- NOT commutative: `concat(a, b) ≠ concat(b, a)` (in general)
+
+**Edge Cases**:
+- Concatenating empty strings returns the other string
+- String encoding/character set handling is implementation-defined
+
+## Executable Test Cases
+
+```yaml
+test_cases:
+  - input: ["hello", "world"]
+    output: "helloworld"
+    description: "Basic string concatenation"
+
+  - input: ["hello", " world"]
+    output: "hello world"
+    description: "Concatenation with space"
+
+  - input: ["", "test"]
+    output: "test"
+    description: "Concatenation with empty string (left)"
+
+  - input: ["test", ""]
+    output: "test"
+    description: "Concatenation with empty string (right)"
+
+  - input: ["", ""]
+    output: ""
+    description: "Concatenation of two empty strings"
+
+  - input: ["123", "456"]
+    output: "123456"
+    description: "Concatenation of numeric strings"
+```
diff --git a/aggregate-library/common/string/length.md b/aggregate-library/common/string/length.md
new file mode 100644
index 00000000..59a4d816
--- /dev/null
+++ b/aggregate-library/common/string/length.md
@@ -0,0 +1,51 @@
+# Operation: length
+
+## Interface Signature
+
+```
+length: String -> Number
+```
+
+## Behavioral Semantics
+
+**Purpose**: Returns the number of characters in a string.
+
+**Parameters**:
+- `s`: The string to measure
+
+**Return Value**: A non-negative number representing the count of characters in `s`.
+
+**Properties**:
+- Empty string has length 0: `length("") = 0`
+- Non-negative: `length(s) ≥ 0` for all strings `s`
+- Concatenation: `length(concat(a, b)) = add(length(a), length(b))`
+
+**Edge Cases**:
+- What constitutes a "character" (code point, grapheme cluster, byte) is implementation-defined
+- Unicode handling (combining characters, etc.) is implementation-defined
+- Multi-byte character encoding is implementation-defined
+
+## Executable Test Cases
+
+```yaml
+test_cases:
+  - input: ["hello"]
+    output: 5
+    description: "Length of simple ASCII string"
+
+  - input: [""]
+    output: 0
+    description: "Length of empty string"
+
+  - input: ["a"]
+    output: 1
+    description: "Length of single character"
+
+  - input: ["hello world"]
+    output: 11
+    description: "Length including space"
+
+  - input: ["123"]
+    output: 3
+    description: "Length of numeric string"
+```
diff --git a/aggregate-library/common/string/substring.md b/aggregate-library/common/string/substring.md
new file mode 100644
index 00000000..3d0ebee4
--- /dev/null
+++ b/aggregate-library/common/string/substring.md
@@ -0,0 +1,62 @@
+# Operation: substring
+
+## Interface Signature
+
+```
+substring: String, Number, Number -> String
+```
+
+## Behavioral Semantics
+
+**Purpose**: Extracts a portion of a string between two indices.
+
+**Parameters**:
+- `s`: The source string
+- `start`: The starting index (inclusive)
+- `end`: The ending index (exclusive)
+
+**Return Value**: A new string containing characters from `s` starting at index `start` up to (but not including) index `end`.
+
+**Preconditions**:
+- `0 ≤ start ≤ length(s)`
+- `start ≤ end ≤ length(s)`
+
+**Properties**:
+- `substring(s, 0, length(s)) = s` (entire string)
+- `substring(s, i, i) = ""` (empty substring)
+- `length(substring(s, start, end)) = subtract(end, start)`
+
+**Edge Cases**:
+- Index out of bounds behavior is implementation-defined (may error or clamp)
+- Negative indices are implementation-defined
+- Zero-based vs one-based indexing is implementation-defined (specification assumes zero-based)
+- Character encoding and multi-byte characters is implementation-defined
+
+## Executable Test Cases
+
+```yaml
+test_cases:
+  - input: ["hello", 0, 5]
+    output: "hello"
+    description: "Extract entire string"
+
+  - input: ["hello", 1, 4]
+    output: "ell"
+    description: "Extract middle portion"
+
+  - input: ["hello", 0, 1]
+    output: "h"
+    description: "Extract first character"
+
+  - input: ["hello", 4, 5]
+    output: "o"
+    description: "Extract last character"
+
+  - input: ["hello", 2, 2]
+    output: ""
+    description: "Empty substring (start equals end)"
+
+  - input: ["hello world", 6, 11]
+    output: "world"
+    description: "Extract word from sentence"
+```
diff --git a/aggregate-library/ephapax/conversion/i32_to_string.md b/aggregate-library/ephapax/conversion/i32_to_string.md
new file mode 100644
index 00000000..496e709a
--- /dev/null
+++ b/aggregate-library/ephapax/conversion/i32_to_string.md
@@ -0,0 +1,41 @@
+# Operation: i32_to_string
+
+## Interface Signature
+
+```
+i32_to_string: I32 -> String
+```
+
+## Behavioral Semantics
+
+**Purpose**: Converts a 32-bit integer to its string representation.
+
+**Parameters**:
+- `n`: The integer to convert
+
+**Return Value**: A new linear String containing the decimal representation.
+
+**Properties**:
+- Negative numbers include minus sign
+- No leading zeros (except for 0 itself)
+- Returns linear String
+
+**Edge Cases**:
+- MIN_I32 (-2147483648) correctly represented
+
+## Executable Test Cases
+
+```yaml
+test_cases:
+  - input: [42]
+    output: "42"
+    description: "Positive integer"
+
+  - input: [-17]
+    output: "-17"
+    description: "Negative integer"
+
+  - input: [0]
+    output: "0"
+    description: "Zero"
+```
diff --git a/aggregate-library/ephapax/conversion/string_to_i32.md b/aggregate-library/ephapax/conversion/string_to_i32.md
new file mode 100644
index 00000000..05f8a568
--- /dev/null
+++ b/aggregate-library/ephapax/conversion/string_to_i32.md
@@ -0,0 +1,47 @@
+# Operation: string_to_i32
+
+## Interface Signature
+
+```
+string_to_i32: &String -> Option I32
+```
+
+## Behavioral Semantics
+
+**Purpose**: Parses a string as a 32-bit integer.
+
+**Parameters**:
+- `s`: A borrowed reference to the string to parse
+
+**Return Value**: Some(n) if valid integer, None if parse fails.
+
+**Properties**:
+- Accepts optional leading minus sign
+- Rejects leading/trailing whitespace
+- Takes borrow (non-consuming)
+
+**Edge Cases**:
+- Overflow returns None
+- Empty string returns None
+- Non-numeric characters return None
+
+## Executable Test Cases
+
+```yaml
+test_cases:
+  - input: ["42"]
+    output: Some(42)
+    description: "Parse positive"
+
+  - input: ["-17"]
+    output: Some(-17)
+    description: "Parse negative"
+
+  - input: ["hello"]
+    output: None
+    description: "Invalid input"
+
+  - input: [""]
+    output: None
+    description: "Empty string"
+```
diff --git a/aggregate-library/ephapax/io/print.md b/aggregate-library/ephapax/io/print.md
new file mode 100644
index 00000000..014fee6a
--- /dev/null
+++ b/aggregate-library/ephapax/io/print.md
@@ -0,0 +1,39 @@
+# Operation: print
+
+## Interface Signature
+
+```
+print: &String -> Unit
+```
+
+## Behavioral Semantics
+
+**Purpose**: Outputs a string to standard output without a trailing newline.
+
+**Parameters**:
+- `s`: A borrowed reference to the string to print
+
+**Return Value**: Unit
+
+**Properties**:
+- Takes a borrow (non-consuming)
+- No trailing newline added
+- Immediate output (not buffered)
+
+**Edge Cases**:
+- Empty string prints nothing
+
+## Executable Test Cases
+
+```yaml
+test_cases:
+  - input: ["hello"]
+    output: ()
+    side_effect: "hello printed to stdout"
+    description: "Print string"
+
+  - input: [""]
+    output: ()
+    side_effect: "nothing printed"
+    description: "Print empty string"
+```
diff --git a/aggregate-library/ephapax/io/println.md b/aggregate-library/ephapax/io/println.md
new file mode 100644
index 00000000..7b91d21a
--- /dev/null
+++ b/aggregate-library/ephapax/io/println.md
@@ -0,0 +1,39 @@
+# Operation: println
+
+## Interface Signature
+
+```
+println: &String -> Unit
+```
+
+## Behavioral Semantics
+
+**Purpose**: Outputs a string to standard output with a trailing newline.
+
+**Parameters**:
+- `s`: A borrowed reference to the string to print
+
+**Return Value**: Unit
+
+**Properties**:
+- Takes a borrow (non-consuming)
+- Appends newline after string
+- Flushes output buffer
+
+**Edge Cases**:
+- Empty string prints just a newline
+
+## Executable Test Cases
+
+```yaml
+test_cases:
+  - input: ["hello"]
+    output: ()
+    side_effect: "hello\\n printed to stdout"
+    description: "Print string with newline"
+
+  - input: [""]
+    output: ()
+    side_effect: "\\n printed"
+    description: "Print just newline"
+```
diff --git a/aggregate-library/ephapax/io/read_line.md b/aggregate-library/ephapax/io/read_line.md
new file mode 100644
index 00000000..b3ae3016
--- /dev/null
+++ b/aggregate-library/ephapax/io/read_line.md
@@ -0,0 +1,40 @@
+# Operation: read_line
+
+## Interface Signature
+
+```
+read_line: Unit -> String
+```
+
+## Behavioral Semantics
+
+**Purpose**: Reads a line of text from standard input.
+
+**Parameters**:
+- None (Unit input)
+
+**Return Value**: A new linear String containing the input (without trailing newline).
+
+**Properties**:
+- Blocks until newline received
+- Returns linear String (must be consumed)
+- Strips trailing newline
+
+**Edge Cases**:
+- EOF returns empty string
+- Very long lines may be truncated (implementation-defined)
+
+## Executable Test Cases
+
+```yaml
+test_cases:
+  - input: [()]
+    stdin: "hello\\n"
+    output: "hello"
+    description: "Read line strips newline"
+
+  - input: [()]
+    stdin: "\\n"
+    output: ""
+    description: "Empty line returns empty string"
+```
diff --git a/aggregate-library/ephapax/linear/borrow.md b/aggregate-library/ephapax/linear/borrow.md
new file mode 100644
index 00000000..939e22bc
--- /dev/null
+++ b/aggregate-library/ephapax/linear/borrow.md
@@ -0,0 +1,39 @@
+# Operation: borrow
+
+## Interface Signature
+
+```
+borrow: Linear a -> &a
+```
+
+## Behavioral Semantics
+
+**Purpose**: Creates a temporary immutable reference to a linear value without consuming it.
+
+**Parameters**:
+- `value`: A linear value to borrow
+
+**Return Value**: An immutable reference to the value.
+
+**Properties**:
+- Original value remains owned by caller
+- Borrow lifetime must not exceed value lifetime
+- Multiple concurrent borrows allowed (shared borrowing)
+- Cannot mutate through borrow
+
+**Edge Cases**:
+- Using the owned value while borrow is active is a compile-time error
+- Borrow cannot escape its scope
+
+## Executable Test Cases
+
+```yaml
+test_cases:
+  - input: [s]
+    output: "&s"
+    description: "Borrow creates reference"
+
+  - input: [string]
+    postcondition: "string still usable after borrow ends"
+    description: "Non-destructive access"
+```
diff --git a/aggregate-library/ephapax/linear/copy.md b/aggregate-library/ephapax/linear/copy.md
new file mode 100644
index 00000000..b1d0eb56
--- /dev/null
+++ b/aggregate-library/ephapax/linear/copy.md
@@ -0,0 +1,41 @@
+# Operation: copy
+
+## Interface Signature
+
+```
+copy: Unrestricted a -> (a, a)
+```
+
+## Behavioral Semantics
+
+**Purpose**: Duplicates an unrestricted (non-linear) value.
+
+**Parameters**:
+- `value`: An unrestricted value (I32, I64, F32, F64, Bool, Unit)
+
+**Return Value**: A pair containing two copies of the value.
+
+**Properties**:
+- Only valid for unrestricted types
+- Both copies are independent
+- Linear types cannot be copied (compile-time error)
+
+**Edge Cases**:
+- Attempting to copy a linear type fails at compile time
+
+## Executable Test Cases
+
+```yaml
+test_cases:
+  - input: [42]
+    output: (42, 42)
+    description: "Copy integer"
+
+  - input: [true]
+    output: (true, true)
+    description: "Copy boolean"
+
+  - input: ["hello"]
+    error: "Linear type cannot be copied"
+    description: "Strings are linear"
+```
diff --git a/aggregate-library/ephapax/linear/drop.md b/aggregate-library/ephapax/linear/drop.md
new file mode 100644
index 00000000..801b9261
--- /dev/null
+++ b/aggregate-library/ephapax/linear/drop.md
@@ -0,0 +1,35 @@
+# Operation: drop
+
+## Interface Signature
+
+```
+drop: Linear a -> Unit
+```
+
+## Behavioral Semantics
+
+**Purpose**: Explicitly consumes a linear value, releasing any associated resources.
+
+**Parameters**:
+- `value`: A linear value to consume
+
+**Return Value**: Unit
+
+**Properties**:
+- Value is consumed and cannot be used afterward
+- Required for linear values not otherwise consumed
+- Triggers destructor/cleanup logic
+
+**Edge Cases**:
+- Dropping an already-consumed value is a compile-time error
+- Cannot drop borrowed references
+
+## Executable Test Cases
+
+```yaml
+test_cases:
+  - input: [x]
+    output: ()
+    postcondition: "x resources released"
+    description: "Drop consumes linear value"
+```
diff --git a/aggregate-library/ephapax/linear/move.md b/aggregate-library/ephapax/linear/move.md
new file mode 100644
index 00000000..3cb19e8e
--- /dev/null
+++ b/aggregate-library/ephapax/linear/move.md
@@ -0,0 +1,39 @@
+# Operation: move
+
+## Interface Signature
+
+```
+move: Linear a -> Linear a
+```
+
+## Behavioral Semantics
+
+**Purpose**: Transfers ownership of a linear value, consuming the source binding.
+
+**Parameters**:
+- `value`: A linear value to transfer
+
+**Return Value**: The same value, now owned by the destination binding.
+
+**Properties**:
+- Source binding becomes unusable after move
+- Zero-cost at runtime (semantic operation only)
+- Preserves value identity: `move(x) ≡ x`
+
+**Edge Cases**:
+- Moving an already-moved value is a compile-time error
+- Moving through a borrow is not permitted
+
+## Executable Test Cases
+
+```yaml
+test_cases:
+  - input: [x]
+    output: x
+    postcondition: "x is no longer accessible"
+    description: "Move transfers ownership"
+
+  - input: [pair(a, b)]
+    output: pair(a, b)
+    description: "Move works on compound linear values"
+```
diff --git a/aggregate-library/ephapax/product/fst.md b/aggregate-library/ephapax/product/fst.md
new file mode 100644
index 00000000..d9c0d3c3
--- /dev/null
+++ b/aggregate-library/ephapax/product/fst.md
@@ -0,0 +1,38 @@
+# Operation: fst
+
+## Interface Signature
+
+```
+fst: (a, b) -> a
+```
+
+## Behavioral Semantics
+
+**Purpose**: Extracts the first element of a pair, consuming the pair.
+
+**Parameters**:
+- `p`: A pair to destructure
+
+**Return Value**: The first element of the pair.
+
+**Properties**:
+- Consumes the pair
+- Second element must be handled (dropped if linear)
+- For non-consuming access, use borrow
+
+**Edge Cases**:
+- If second element is linear, it is implicitly dropped
+
+## Executable Test Cases
+
+```yaml
+test_cases:
+  - input: [(1, 2)]
+    output: 1
+    description: "Extract first"
+
+  - input: [("hello", "world")]
+    output: "hello"
+    postcondition: "world is dropped"
+    description: "First of string pair"
+```
diff --git a/aggregate-library/ephapax/product/pair.md b/aggregate-library/ephapax/product/pair.md
new file mode 100644
index 00000000..b7ba21c1
--- /dev/null
+++ b/aggregate-library/ephapax/product/pair.md
@@ -0,0 +1,42 @@
+# Operation: pair
+
+## Interface Signature
+
+```
+pair: a, b -> (a, b)
+```
+
+## Behavioral Semantics
+
+**Purpose**: Constructs a product type (pair) from two values.
+
+**Parameters**:
+- `first`: The first element
+- `second`: The second element
+
+**Return Value**: A pair containing both values.
+
+**Properties**:
+- Consumes both arguments (if linear)
+- Pair is linear if either component is linear
+- Order preserved
+
+**Edge Cases**:
+- Nested pairs supported: `pair(pair(a, b), c)`
+
+## Executable Test Cases
+
+```yaml
+test_cases:
+  - input: [1, 2]
+    output: (1, 2)
+    description: "Pair of integers"
+
+  - input: ["hello", 42]
+    output: ("hello", 42)
+    description: "Mixed types"
+
+  - input: [(), ()]
+    output: ((), ())
+    description: "Pair of units"
+```
diff --git a/aggregate-library/ephapax/product/snd.md b/aggregate-library/ephapax/product/snd.md
new file mode 100644
index 00000000..c9bddfc2
--- /dev/null
+++ b/aggregate-library/ephapax/product/snd.md
@@ -0,0 +1,38 @@
+# Operation: snd
+
+## Interface Signature
+
+```
+snd: (a, b) -> b
+```
+
+## Behavioral Semantics
+
+**Purpose**: Extracts the second element of a pair, consuming the pair.
+
+**Parameters**:
+- `p`: A pair to destructure
+
+**Return Value**: The second element of the pair.
+
+**Properties**:
+- Consumes the pair
+- First element must be handled (dropped if linear)
+- For non-consuming access, use borrow
+
+**Edge Cases**:
+- If first element is linear, it is implicitly dropped
+
+## Executable Test Cases
+
+```yaml
+test_cases:
+  - input: [(1, 2)]
+    output: 2
+    description: "Extract second"
+
+  - input: [("hello", "world")]
+    output: "world"
+    postcondition: "hello is dropped"
+    description: "Second of string pair"
+```
diff --git a/aggregate-library/ephapax/region/alloc_in.md b/aggregate-library/ephapax/region/alloc_in.md
new file mode 100644
index 00000000..306b3584
--- /dev/null
+++ b/aggregate-library/ephapax/region/alloc_in.md
@@ -0,0 +1,38 @@
+# Operation: alloc_in
+
+## Interface Signature
+
+```
+alloc_in: Region r, a -> a @ r
+```
+
+## Behavioral Semantics
+
+**Purpose**: Allocates a value within a specific memory region.
+
+**Parameters**:
+- `region`: The region handle to allocate in
+- `value`: The value to allocate
+
+**Return Value**: A region-tagged reference to the allocated value.
+
+**Properties**:
+- Reference lifetime bounded by region lifetime
+- Allocation uses bump pointer (fast)
+- No individual deallocation; freed with region
+
+**Edge Cases**:
+- Using expired region handle is compile-time error
+
+## Executable Test Cases
+
+```yaml
+test_cases:
+  - input: [r, "hello"]
+    output: "hello @ r"
+    description: "Allocate string in region"
+
+  - input: [r, (1, 2)]
+    output: "(1, 2) @ r"
+    description: "Allocate pair in region"
+```
diff --git a/aggregate-library/ephapax/region/new_region.md b/aggregate-library/ephapax/region/new_region.md
new file mode 100644
index 00000000..38a89c21
--- /dev/null
+++ b/aggregate-library/ephapax/region/new_region.md
@@ -0,0 +1,43 @@
+# Operation: new_region
+
+## Interface Signature
+
+```
+new_region: (Region r -> a) -> a
+```
+
+## Behavioral Semantics
+
+**Purpose**: Creates a lexically-scoped memory region. All allocations within are freed when the region ends.
+
+**Parameters**:
+- `body`: A function receiving the region handle, returning a value
+
+**Return Value**: The result of `body`, which must not contain region-local references.
+
+**Properties**:
+- Tofte-Talpin style region-based memory management
+- All region allocations freed at once (bump pointer reset)
+- Region handles cannot escape their lexical scope
+- Nested regions supported
+
+**Edge Cases**:
+- Returning region-local reference is compile-time error
+- Region lifetime is strictly lexical
+
+## Executable Test Cases
+
+```yaml
+test_cases:
+  - input: ["|r| 42"]
+    output: 42
+    description: "Return non-allocated value"
+
+  - input: ["|r| length(alloc_in(r, 'hello'))"]
+    output: 5
+    description: "Use region-allocated value"
+
+  - input: ["|r| alloc_in(r, 'hello')"]
+    error: "Region-local reference escapes"
+    description: "Cannot return region reference"
+```
diff --git a/aggregate-library/ephapax/sum/case.md b/aggregate-library/ephapax/sum/case.md
new file mode 100644
index 00000000..00a92a51
--- /dev/null
+++ b/aggregate-library/ephapax/sum/case.md
@@ -0,0 +1,40 @@
+# Operation: case
+
+## Interface Signature
+
+```
+case: (a + b), (a -> c), (b -> c) -> c
+```
+
+## Behavioral Semantics
+
+**Purpose**: Pattern matches on a sum type, applying the appropriate function.
+
+**Parameters**:
+- `sum`: The sum value to match on
+- `left_fn`: Function to apply if left variant
+- `right_fn`: Function to apply if right variant
+
+**Return Value**: Result of applying the matching function.
+
+**Properties**:
+- Exactly one branch executes
+- Sum is consumed
+- Both branches must return same type
+- Linear values in non-taken branch are not evaluated
+
+**Edge Cases**:
+- Both branches must handle linearity correctly
+
+## Executable Test Cases
+
+```yaml
+test_cases:
+  - input: [inl(42), "x => add(x, 1)", "y => 0"]
+    output: 43
+    description: "Match left variant"
+
+  - input: [inr(true), "x => 0", "y => 1"]
+    output: 1
+    description: "Match right variant"
+```
diff --git a/aggregate-library/ephapax/sum/inl.md b/aggregate-library/ephapax/sum/inl.md
new file mode 100644
index 00000000..666620df
--- /dev/null
+++ b/aggregate-library/ephapax/sum/inl.md
@@ -0,0 +1,37 @@
+# Operation: inl
+
+## Interface Signature
+
+```
+inl: a -> (a + b)
+```
+
+## Behavioral Semantics
+
+**Purpose**: Injects a value into the left side of a sum type.
+
+**Parameters**:
+- `value`: The value to inject
+
+**Return Value**: A sum type with the value in the left position.
+
+**Properties**:
+- Consumes the value (if linear)
+- Right type is inferred from context
+- Sum is linear if component is linear
+
+**Edge Cases**:
+- Type annotation may be required for inference
+
+## Executable Test Cases
+
+```yaml
+test_cases:
+  - input: [42]
+    output: inl(42)
+    description: "Inject integer left"
+
+  - input: ["hello"]
+    output: inl("hello")
+    description: "Inject string left"
+```
diff --git a/aggregate-library/ephapax/sum/inr.md b/aggregate-library/ephapax/sum/inr.md
new file mode 100644
index 00000000..db52ab3d
--- /dev/null
+++ b/aggregate-library/ephapax/sum/inr.md
@@ -0,0 +1,37 @@
+# Operation: inr
+
+## Interface Signature
+
+```
+inr: b -> (a + b)
+```
+
+## Behavioral Semantics
+
+**Purpose**: Injects a value into the right side of a sum type.
+
+**Parameters**:
+- `value`: The value to inject
+
+**Return Value**: A sum type with the value in the right position.
+
+**Properties**:
+- Consumes the value (if linear)
+- Left type is inferred from context
+- Sum is linear if component is linear
+
+**Edge Cases**:
+- Type annotation may be required for inference
+
+## Executable Test Cases
+
+```yaml
+test_cases:
+  - input: [true]
+    output: inr(true)
+    description: "Inject boolean right"
+
+  - input: ["error"]
+    output: inr("error")
+    description: "Inject string right"
+```