Infinite paths in the composite-restricted visible lattice

We consider the nearest-neighbour graph on pairs of integers greater than one that are coprime and have at least one composite coordinate. We prove that this graph contains an infinite simple path, answering Erdős Problem 1212 affirmatively. More precisely, for almost every slope in a fixed interval away from the diagonal, there is a ray with that limiting coordinate ratio. The proof first obtains many pairwise coprime composite rows free of small prime factors in a short band. A polynomial Jacobsthal bound supplies composite supporting columns, so a bad crossing through the band has a subcrossing of polylogarithmic width. Its large common prime divisors then force an integer interpolation polynomial of small height to vanish at one of its vertices. A summable estimate for the exceptional directions of all such polynomials permits one direction to be fixed at every sufficiently large scale. Planar crossing duality and explicit overlapping rectangles produce an unbounded connected subgraph along this direction, from which an infinite simple path is extracted. Formalization. The original existence conclusion and the displayed main theorem have a public Lean 4 formalization. The kernel audit reports only propext, Classical.choice and Quot.sound as axiom dependencies. The source, theorem entry points and verification instructions are available in the public formalization repository.