An Explicit Infinite Model Refuting Ulrich's u4 as a Single Axiom for Positive Implication

Abstract

Corrected and strengthened v2. This release supplies a complete preprint and a Lean 4.33.0 formalization of an explicit substitution-closed infinite countermodel showing that Ulrich's u4 is not a single axiom for positive implicational logic under uniform substitution and modus ponens. Project-run checks include direct Lean compilation, leanchecker, nanoda, a compiled axiom-dependency audit, and a separate Python symbolic checker. Independent third-party specialist review and journal peer review have not yet occurred.