Genesis Kernel (GK5)
In ProgressA Lean 4 project testing whether mathematical and physical structure can be derived from a minimal discrete starting point.
Genesis Kernel is a Lean 4 project that attempts to derive mathematical and physical structure from a single minimal starting point: a discrete existence event called Moment0.
The project is driven by a simple question: if you try to start lower than the usual foundations, how much familiar structure can you formally earn instead of assuming up front? Genesis Kernel is an attempt to make that question mechanically precise rather than philosophical.
What GK5 is trying to enforce
The current version, GK5, uses dependent types and opaque RetagToken security to enforce a strict derivation ladder. Later layers are allowed to depend on earlier ones, but not the other way around.
That is where the “Typed Arithmetic” system matters. The goal is to prevent metric smuggling: you should not be able to accidentally import real-number structure, geometric intuition, or measurement assumptions that have not actually been derived from the discrete substrate.
In other words, the project is not just trying to prove theorems inside Lean. It is trying to make illegitimate shortcuts hard to express in the first place.
Why the proof discipline matters
Genesis Kernel only makes sense if the build can certify what has genuinely been derived.
The verdict criterion is therefore a deterministic world_certificate.json with no sorryAx dependencies. Every step in the ladder has to close as a completed proof, not as a placeholder axiom or a hand-waved claim about what ought to be true later.
That requirement is part of the point. If the project is going to say anything ambitious about foundations, it has to do so in a form that is auditable by the checker rather than protected by rhetoric.
Current posture
This is still long-range formal research work, not a polished result package.
What exists today is the enforcement machinery: the derivation ladder, the typed arithmetic discipline, and the proof-security posture around opaque retagging. The hard part now is pushing more structure through that system without quietly relaxing the standard that makes the project interesting in the first place.