Emulation Theory

Emulation Theory is a subject of math developed by Stanford Professor Harvey Friedman. In this project, we seek to formalise and prove several results in Emulation Theory using the theorem prover Lean

This work was done by Atticus Kuhn and Zongshu

To see how far along we are, look at ./src/basic.lean. I welcome all contributions and pull requests.

Emulation Theory Basics

We say 2 vectors A and B are order equivalent iff

A_i < A_j \iff B_i < B_j

We say that a set of k-vectors E emulates a set of k-vectors S iff every concatenation of vectors in S is order-equivalent to some concatenation of vectors in E.