The goal was to derive classical results (like the uncountability of [0, 1]) from a single principle of distinction ("A = exists") rather than starting with ZFC axioms.
Key Technical Highlights:
135 theorems, 0 Admitted for the main uncountability proof.
Solves Digit Stability: Instead of digit extraction, it uses geometric interval trisection to prove uncountability constructively.
L5-Resolution: Implements a deterministic "leftmost" rule for argmax, ensuring that optimization processes are Cauchy even on flat plateaus.
No Axiom of Infinity: The infinite emerges as a property of the process levels (P4).
I'm currently looking for an ArXiv endorsement (cs.LO or math.LO) to publish the full 60-page preprint.
Repo: https://github.com/Horsocrates/theory-of-systems-coq
I'd love to hear your thoughts on the E/R/R (Elements/Roles/Rules) framework and the inclusion of the "Law of Order" as a 5th law of logic.