formal-foundations

name

formal-foundations

description

Mathematical foundations, logical structures, and formal verification guidance. Trigger when: - Designing protocol contracts, formal specifications, verifying state spaces, or using proof assistants. - Tasks involve: TLA+, Alloy, Lean, Coq, model checkers, invariants, temporal logic. - Prompt contains keywords: formal verification, alloy, tla+, lean, coq, invariant, state machine, model checker, liveness, safety.

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's structural representations, the verification semantics for spec's formal tiers, and the theoretical grounding consulted by boundary. The formalisms here anchor the symbolic path of the Verification Dual: 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

A relation R ⊆ X × X is a bisimulation if for all (x₁, x₂) ∈ R, their transitions c(x₁) and c(x₂) map to equivalent behaviors in F(R). Bisimulation is the formal tool for checking behavioral equivalence in dynamical systems — two systems are "the same" if no external observer can distinguish them, regardless of internal structure.

When you ask "are these two state machines equivalent?" you are asking about bisimulation, not structural equality. This is the correct frame for protocol equivalence, API compatibility, and behavioral testing.

---

5. Foundational Vocabulary: Data and Structure

These definitions provide the formal vocabulary for the structures that the sdma skill applies in practice.

Database Schemas as Categories

• Database Schema: A small category S.
• Database Instance: A functor I: S → Set.
• Data Migration Adjoints: For a functor F: C → D between schemas, the migration of data is governed by the triple (Σ_F ⊣ Δ_F ⊣ Π_F):
  1. Pullback (Δ_F): Pre-composition I ∘ F. Restructure existing data into a new schema.
  2. Left Pushforward (Σ_F): The Left Kan Extension, used for data integration and colimits. Merge data from multiple sources.
  3. Right Pushforward (Π_F): The Right Kan Extension, used for defining data constraints and limits. Enforce invariants across schema boundaries.

Ologs (Ontology Logs) — Structural Constraints

1. Objects (Types): Must be labeled with a singular indefinite noun phrase (e.g., "An employee", "A department").
2. Morphisms (Aspects): Must represent functional relationships (mathematical functions), where each element of the domain maps to exactly one element of the codomain.
3. Facts: Represented as commutative diagrams demonstrating path equivalence.

Signal Flow and Control

Signal flow is analyzed via Linear Relations using four categorical generators:

1. Addition (+): ℝ × ℝ → ℝ.
2. Duplication (Δ): ℝ → ℝ × ℝ.
3. Integration (∫): The storage or delay operator.
4. Scalar Multiplication: Gain factor k ∈ ℝ.

Information Metrics

• Shannon Entropy (H): H(X) = −Σᵢ pᵢ log₂ pᵢ. In the SDMA, pᵢ is defined as the probability distribution of node interactions (degree/strength) per network science.
• Structural Entropy Index of a Community (SEIC): SEIC(C) = H_C / log₂ |C|, where H_C is calculated using the distribution pᵥ = deg(v) / Σ_{u∈C} deg(u), measuring the internal decentralization of a community C.
• Algorithmic Thermodynamics: Relates the information state to physical entropy S: dE = TdS − PdV. Entropy S acts as a measure of "surprise," where higher disorder corresponds to increased metric entropy and lower Kaplan-Yorke attractor dimensions.

---

6. Summary Reference Table

The Rosetta Stone in full — the correspondences that unify four fields under one algebraic structure:

Feature	Physics	Topology	Logic	Computation
Objects	Hilbert Space (H)	(n−1)-dim Manifold	Proposition (A)	Type (A)
Morphisms	Linear Operator (f)	n-dim Cobordism	Proof (π)	Program (P)
Tensor Product	Composite System (H ⊗ K)	Disjoint Union (X ⊔ Y)	Conjunction (A ⊗ B)	Pair Type (A × B)
Duals	Adjoint (H*)	Reversed Manifold (X*)	Negation (A^⊥)	Continuation (A → ⊥)
Internal Hom	Linear Maps (H ⊸ K)	(N/A)	Implication (A ⊸ B)	Function Type (A → B)
Unit (η)	Bell State / Preparation	Cup (Creation)	Identity (Axiom)	Variable / Unit Value
Counit (ε)	Inner Product / Measurement	Cap (Annihilation)	Cut (Elimination)	Application / Evaluation

---

7. Integration

Relationship to engineering.md

The engineering skill mandates strong typing, composition, and structural soundness. This skill provides the mathematical justification for why those mandates work: types are propositions (Curry-Howard), composition is inference (categorical composition), and structural soundness is a consequence of coherence (pentagon and hexagon identities). When engineering intuition says "this feels wrong," these foundations often reveal why — a violated commutativity condition, a broken adjunction, a misidentified duality.

Relationship to Cognitive Disposition (ambient.md)

The holonic lens in ambient.md's Cognitive Disposition — every component is both a whole and a part — is a natural language description of what category theory formalizes: objects that are simultaneously domains and codomains, algebras that are simultaneously initial and terminal, structures that compose fractally. The formal foundations give that ambient intuition teeth: instead of "think holistically," you can verify that the diagram commutes.

Relationship to SDMA

This skill tells you what these structures are. The sdma skill tells you how to wield them. If you need applied methodology — building an olog, verifying protocol equivalence via bisimulation, selecting between formalisms — load sdma alongside this skill.