formal-foundations

Files (1)

• SKILL.md

SKILL.md (first lines)

# Formal Mathematical Foundations

**Reference corpus — `/form`, `/spec`, `boundary`.** This skill survives as the mathematical-language authority; the mandate to apply it is ambient, rooted in the workflows that invoke it as a lens. It supplies the foundational vocabulary for [form](../form/SKILL.md)'s structural representations, the verification semantics for [spec](../spec/SKILL.md)'s formal tiers, and the theoretical grounding consulted by [boundary](../boundary/SKILL.md). The formalisms here anchor the symbolic path of the [Verification Dual](../../rules.md#2-prime-invariants): types-as-propositions (Curry-Howard), bisimulation as behavioral equivalence, and adjoint functors as the semantic spine of data migration.

**Disposition directive:** Recognize that the structures you encounter in software engineering — types, protocols, state machines, data schemas — are instances of deeper mathematical patterns. This skill equips you with the vocabulary to see those patterns. The `sdma` skill provides the domain-specific toolkit for _applying_ these foundations to concrete problems; this skill provides the _language_.

---

## 1. Categorical Foundations

Category theory is the algebra of composition. Its value to engineering is not abstraction for abstraction's sake — it provides a _universal language_ for describing how things combine, transform, and relate.

### 1.1. Symmetric Monoidal Categories (SMC)

A symmetric monoidal category is a quintuple (C, ⊗, I, α, λ, ρ, γ) defining a category C equipped with a bifunctor ⊗: C × C → C and a unit object I.

- **Associator (α):** A natural isomorphism α\_{X,Y,Z}: (X ⊗ Y) ⊗ Z ≅ X ⊗ (Y ⊗ Z). _Grouping doesn't matter — only the components and their order._
- **Left and Right Unitors (λ, ρ):** Natural isomorphisms λ*X: I ⊗ X ≅ X and ρ_X: X ⊗ I ≅ X. \_The unit is invisible — combining with "nothing" changes nothing.*
- **Braiding (γ):** A natural isomorphism γ\_{X,Y}: X ⊗ Y ≅ Y ⊗ X such that γ\_{Y,X} ∘ γ\_{X,Y} = id\_{X ⊗ Y}. _Order can be swapped — swapping twice returns to the original._

**Coherence Axioms:**

1. **Pentagon Identity:** For any objects W, X, Y, Z, the following diagram commutes:

   (id_W ⊗ α\_{X,Y,Z}) ∘ α\_{W, X⊗Y, Z} ∘ (α\_{W,X,Y} ⊗ id_Z) = α\_{W, X, Y⊗Z} ∘ α\_{W⊗X, Y, Z}

   _All possible re-bracketings of four objects yield the same result. There is exactly one way to re-associate._

2. **Hexagon Identity:** Connects the braiding γ to the associator α:

   α\_{Y,Z,X} ∘ γ\_{X, Y⊗Z} ∘ α\_{X,Y,Z} = (id_Y ⊗ γ\_{X,Z}) ∘ α\_{Y,X,Z} ∘ (γ\_{X,Y} ⊗ id_Z)

   _Braiding is compatible with association. Swapping "through" a group works the same as swapping then regrouping._

### 1.2. Closed Categories

A monoidal category is **closed** if the functor (− ⊗ Y) has a right adjoint, denoted as the internal hom [Y, −] or Y ⊸ −.

- **Currying Isomorphism:** The adjunction is defined by the natural isomorphism:

  Hom(X ⊗ Y, Z) ≅ Hom(X, Y ⊸ Z)

  _A function of two arguments is equivalent to a function that takes one argument and returns a function of the other. This is the mathematical foundation of currying in every programming language._

### 1.3. Compact Closed Categories

A compact closed category is a symmetric monoidal category where every object X has a dual X\*, a unit η_X: I → X\* ⊗ X, and a counit ε_X: X ⊗ X\* → I satisfying the **Zig-Zag (Yanking) Identities:**

(ε_X ⊗ id_X) ∘ α\_{X, X\*, X} ∘ (id_X ⊗ η_X) = id_X

(id\_{X\*} ⊗ ε_X) ∘ α\_{X\*, X, X\*}⁻¹ ∘ (η_X ⊗ id\_{X\*}) = id\_{X\*}

_Every type has a "dual" (its continuation, its adjoint space, its negation). Creating a pair and then collapsing it is the same as doing nothing. This is the mathematical spine of evaluation, measurement, and resource consumption._

---

## 2. The Rosetta Stone Isomorphisms

The Rosetta Stone (Baez-Stay) maps the structural primitives of four disparate fields onto the common core of compact closed categories. **This is the central insight:** these four fields are not merely analogous — they are _formally isomorphic_. A proof about one transfers to the others via functorial mapping.

### 2.1. Physics (Hilbert Spaces)

- **Objects:** Finite-dimensional Hilbert spaces H.
- **Morphisms:** Linear operators f: H → K.
- **Bell States:** Formulated via the unit η: ℂ → H\* ⊗ H, representing the preparation of an entangled state.
- **Inner Product:** Formulated via the counit ε: H ⊗ H\* → ℂ, representing measurement or annihilation.

### 2.2. Topology (Cobordisms)

- **Objects:** (n−1)-dimensional manifolds representing spatial slices.
- **Morphisms:** n-dimensional cobordisms M: X → Y representing spacetime evolution.
- **String Diagrams:** A graphical syntax where "Cups" represent the unit η and "Caps" represent the counit ε.

### 2.3. Logic (Multiplicative Linear Logic — MILL)

- **Objects:** Propositions (resources) A, B.
- **Morphisms:** Proofs π: A ⊢ B.
- **Tensor (⊗):** Simultaneous conjunctive resource usage.
- **Linear Implication (⊸):** Resource transformation; distinct from the "Par" (⅋) used in classical linear logic.
- **Negation (A^⊥):** The linear dual, satisfying A ⊸ B ≅ A^⊥ ⅋ B.

### 2.4. Computation (Linear Type Theory)

- **Objects:** Types A, B.
- **Morphisms:** Programs or terms f: A → B.
- **β-reduction:** Computation as the elimination of a detour (application of a lambda abstraction).
- **η-expansion:** The principle of extensionality: (λx. f x) ≡ f.

---

## 3. Curry-Howard and Compositional Reasoning

The Curry-Howard correspondence — **types are propositions, programs are proofs** — is the computational column of the Rosetta Stone, but its implications extend beyond type theory:

- **Type checking is proof checking.** A well-typed program is a constructive proof that a proposition holds. A type error is a failed proof attempt.
- **Composition is inference.** If you have a proof of A → B and a proof of B → C, function composition gives you a proof of A → C. This is _modus ponens_ expressed as pipeline composition.
- **Parametric polymorphism is universal quantification.** A function `∀a. a → a` must be the identity — there is _no other_ inhabitant of that type. The type constrains the implementation absolutely.
- **Linearity is resource discipline.** In linear type theory, every value must be used exactly once. This isn't just a programming restriction — it's the logical principle that resources cannot be duplicated or discarded. This is the foundation of session types, ownership systems (Rust's borrow checker), and protocol verification.

---

## 4. Algebra vs. Coalgebra

This is the fundamental duality in formal modeling. Recognizing which side of this duality a problem lives on determines the correct tools.

| Aspect      | Algebra                          | Coalgebra                                               |
| :---------- | :------------------------------- | :------------------------------------------------------ |
| Defined by  | Constructors (how to build)      | Observers (how to interact)                             |
| Identity    | Structural (isomorphism)         | Behavioral (bisimulation)                               |
| Reasoning   | Induction (from parts to whole)  | Co-induction (from observations)                        |
| Data model  | Finite, inductive (lists, trees) | Potentially infinite, co-inductive (streams, processes) |
| Typical use | Data structures, ADTs            | State machines, protocols, reactive systems             |

### Coalgebra (formal definition)

A coalgebra is a morphism c: X → F(X) where X is the state space and F is a behavior endofunctor.

### Bisimulation

From nrdxp/predicate, MIT.

More from nrdxp/predicate