Existence of locally toroidal regular 4-polytopes

We prove the existence half of Schulte–Weiss Problem 16 (2006) and McMullen–Schulte Conjecture 10C7 (2002): the universal regular 4-polytope \\4,4\(s,0),\4,4\(u,0)\ exists for every pair of distinct odd integers s,u≥3, with no coprimality assumption. Here \4,4\(s,0) is the quotient of the square tessellation by sZ². Finiteness and group classification remain open. The proof constructs four matrices over a finite field of characteristic two whose local subgroups are isomorphic to the prescribed toroidal groups. A commutator obstruction shows that these subgroups meet exactly in the subgroup on their two shared generators; this equality lifts to the universal presentation. The group theorem, the geometric identification of the toroidal maps, and the construction and universality of the resulting abstract polytope are formalized in Lean. Proof checked in Lean; not yet reviewed by experts. Produced by AI models under the author's direction.