This repository contains the complete Lean 4 mechanization for the paper:
Gödel Mirror: A Formal System for Contradiction-Driven Recursion > Jhet Chan > (Forthcoming, link to be added upon publication)
The Gödel Mirror is a minimal, paraconsistent formal system that treats self-referential paradox not as an error, but as a deterministic control signal for structural transformation. This work provides a verifiable calculus where contradiction is metabolized into new syntactic structure without leading to logical explosion.
The formalization is organized into several modules to ensure clarity and separation of concerns.
| File Path | Description |
|---|---|
GodelMirror/Syntax.lean |
Defines the core inductive types for the calculus. |
GodelMirror/Semantics.lean |
Defines the operational semantics (rewrite rules). |
GodelMirror/MetaTheory.lean |
Contains the formal proofs of the system's properties. |
Examples.lean |
Provides a runnable case study of the paradox cycle. |
lakefile.lean |
The Lake build configuration file. |
This project is built using the Lean 4 proof assistant and its build manager, Lake.
You must have a working Lean 4 environment. We recommend installing it via elan. See the official Lean installation instructions.
- Clone the repository:
git clone [https://github.com/jhetchan/godel-mirror.git](https://github.com/jhetchan/godel-mirror.git) cd godel-mirror - Build the project:
Fetch the dependencies and compile the Lean files.
lake build
- Run the example:
To see the case study trace from the paper, run the
Examples.leanfile.lake env lean --run GodelMirror/Examples.lean
This work is licensed under the MIT License. See the LICENSE file for details.