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

We construct an explicit infinite model showing that Ulrich's remaining 15-symbol candidate u4 is not a single axiom for positive implicational logic under substitution and modus ponens. The model satisfies every substitution instance of u4 and is closed under modus ponens, while falsifying reflexivity. Subject to the reduction of Fitelson and Peltier (2026), this implies that the minimum single-axiom length is 17 symbols. This deposit is a mathematical resolution submitted for external specialist verification and has not yet undergone peer review.