Beyond Computation 2.0: Verified Meta-Trilemma - Mechanized Impossibility of Normatively Complete Computational Consciousness

# Beyond Computation 2.0: Verified Meta-Trilemma This paper presents the second iteration of the Charta Research Program on mechanized anti-computationalism. ## Relation to Version 1.0 Version 1.0 [Publication, December 2025] introduced a broad-spectrum axiomatic framework (A1-A4, modal depth limitations, emergent subject-functor S), establishing the philosophical foundations and demonstrating the performative irrefutability (T5) of the anti-computationalist position. ## Version 2.0 radically extends 1.0 through • **Minimal axiomatization:** A2_norm (normative existence) + A4_limit (computational limitation) • **T1_ComputationalLimit:** Direct proof of computational impossibility (constructive, Coq 8.19 verified) • **DavisSafe:** Closes the Martin Davis consistency loophole • **Meta-logical Identity Lock:** Formal preservation of absolute identity under realization • **Ur-Matrix framework:** Primordial source structure of normative identity → DOI: [10.5281/zenodo.18056466](https://doi.org/10.5281/zenodo.18056466) • **Exhaustive trilemma:** - **Accept A2_norm + A4_limit** → Computationalism impossible (⊥) - **Deny A2_norm** → Eliminativism (no normative subjects) - **Deny A4_limit** → Mechanism (universal provability) • **Verified Coq supplements:** Complete source code for all theorems included as supplementary files (Lucas_Penrose_Omniprover.v, T1_Weak_Omniprover.v, T1_Strong_Omniprover.v, Weak_Strong_Omniprover.v). Run `coqc` on any file to verify the proofs yourself. ## Key advancement 2.0 achieves a sharper, more destructive result with strictly weaker assumptions than 1.0 – reducing the anti-computationalist argument to its logical essence: two axioms, one Coq-verified theorem, three exhaustive paths. **Keywords:** computationalism, consciousness, Coq, formal verification, Gödel, meta-trilemma, philosophy of mind, verified proofs