A Machine-Verified Algebraic Formalization of Gödel's 1949 Counterexample

We give a machine-verified algebraic formalization of Gödel's (1949) construction in the Platonic proof kernel. Fourteen theorems follow from nine structural hypotheses that encode the standard Gödel parameters — \(\rho = \omega^2/(8\pi G)\), \(\Lambda = -\omega^2/2\), \(a^2 = 1/(2\omega^2)\), \(R = 2\omega^2\) — and every theorem closes via automated nonlinear arithmetic. Seven items are established: (1) mutual consistency of the parameter system; (2) positivity of \(\rho\), \(R\), \(a^2\), and negativity of \(\Lambda\); (3) the field-equation constraint \(\omega^2 = 4\pi G\rho - \Lambda\) together with the linear relation \(4\pi G\rho = -\Lambda\); (4) the weak energy condition \(T_{\mu\nu} V^\mu V^\nu \geq 0\) for dust and arbitrary timelike \(V\); (5) monotonicity of the light-cone tilt \(e^r\); (6) the algebraic conditions at the CTC threshold \(e^{2 r_G} = 2\); (7) a closed-form algebraic bound on the squared norm of two-vectors in the \((t,\phi)\)-plane, together with its strict exponential growth in \(r\). The hypothesis set is mutually realisable (the parameter values are those of the classical Gödel solution), so the theorems are not vacuous. What is not formalized — the Lorentzian-manifold topology, the Cauchy-surface obstruction, Killing-vector homogeneity, and the quantum stress-energy divergence — is flagged in §5 and §4.6 and referenced to the classical literature.

Scope. Algebraic formalization of a 1949 classical result, not a new physical claim. Contribution. Machine verification of the parameter algebra and the CTC-threshold conditions, together with an explicit boundary between formalized and non-formalized content.