A mathematically rigorous, theorem-proven simulation of physical space on a discrete computational grid.
This project explores the fundamental question: How do we accurately simulate continuous physical reality on a discrete matrix of pixels?
-
Functional Purity — No object-oriented paradigms. Only pure functions with deterministic outputs for given inputs. No side effects in computational core.
-
Mathematical Rigor — Every function must be:
- Proven BEFORE implementation (proof-first development)
- Based on referenced, proven algorithms
- Mathematically verifiable
- Derived from first principles where possible
-
Discrete Foundation — The output device (monitor) is a matrix. All continuous concepts must be properly discretized using sound mathematical techniques (sampling theory, rasterization algorithms).
-
Determinism — Given identical inputs, all computations must produce identical outputs. 100% reproducibility.
-
Efficiency — Algorithms chosen for both correctness AND computational efficiency. No premature optimization, but no wasteful operations.
-
Incremental Construction — Each layer built carefully upon the previous, verified before proceeding.
Key Insight: Discretization is not "leaving mathematics" — it's moving from one algebraic structure to another. The pixel grid Fin w × Fin h is as mathematical as the real numbers ℝ.
LEAN 4 (All Proven)
┌──────────────────────────────────────────────────────────────┐
│ │
│ Continuous Mathematics │
│ (ℚ, ℝ-approximations, fields, vector spaces) │
│ │ │
│ │ Discretization │
│ │ (proven sampling, rasterization) │
│ ▼ │
│ Discrete Mathematics │
│ (Fin n, ZMod n, bounded integers, finite grids) │
│ │ │
│ ▼ │
│ Pixel Buffer: Fin w × Fin h × Color │
│ (type-safe, bounds-checked, proven correct) │
│ │
└──────────────────────────────────────────────────────────────┘
│
│ Raw bytes (no computation)
▼
┌──────────────────────────────────────────────────────────────┐
│ RUST (I/O Only) │
│ │
│ memcpy(buffer) → GPU → Display │
│ │
└──────────────────────────────────────────────────────────────┘
| Layer | Language | Purpose | Proven? |
|---|---|---|---|
| 0-6 | Lean 4 | Math, physics, geometry | ✓ |
| 7 | Lean 4 | Rasterization/discretization | ✓ |
| 8 | Lean 4 | Pixel buffer construction | ✓ |
| I/O | Rust | Buffer → Display | Trivial |
Everything mathematical happens in Lean 4. Rust only moves bytes.
matrix/
├── proofs/ # Mathematical documentation & references
├── src/ # Computation layers 0-8 (Lean 4, all proven)
│ ├── Layer0_Discrete/ # Fin, ZMod, bounded types
│ ├── Layer1_Continuous/ # ℚ, reals
│ ├── Layer2_Scalar/ # Field operations
│ ├── Layer3_Linear/ # Vectors, matrices
│ ├── Layer4_Coordinates/ # World/screen space
│ ├── Layer5_Geometry/ # Primitives
│ ├── Layer6_Physics/ # Simulation
│ ├── Layer7_Rasterize/ # Discretization algorithms
│ └── Layer8_Frame/ # Pixel buffer
├── viz/ # I/O layer (Rust, ~100 lines)
├── intel/ # Research, references, decisions
│ ├── prompts/
│ ├── research/
│ └── decisions/
└── tests/ # Runtime validation
Development flow: intel/research → proofs/ → src/Layer0 → ... → src/Layer8 → viz/
The fundamental challenge: physical space is (classically) continuous, but our representation is discrete.
Key mathematical concepts involved:
- Sampling Theory (Nyquist-Shannon)
- Rasterization algorithms (Bresenham, etc.)
- Fixed-point vs floating-point arithmetic
- Discrete differential geometry
- World Space — The simulated physical space (potentially 3D or higher)
- Screen Space — The 2D pixel matrix of the display
- Projection — The mathematical mapping between them
Time in simulation is necessarily discrete (simulation steps/ticks). The relationship between simulation time and physical time must be carefully defined.
Phase: Foundation — Establishing mathematical primitives and core abstractions.
"The map is not the territory, but with sufficient rigor, we can make the map arbitrarily faithful."