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 obtains pairwise coprime rough composite rows in short bands, supplies safe composite supporting columns using a polynomial Jacobsthal bound, and forces a small integer interpolation polynomial to vanish at a point of every bad crossing. A summable simultaneous estimate for exceptional directions and planar crossing duality connect the resulting crossings across scales. Prior mechanism and attribution. This revision credits rafalwrona's mixed-modulus determinant observation of 23 August 2026 and Duncan's drift and finite-path observations of 21 July 2026. The former shares the local arithmetic mechanism used in the interpolation step. These observations do not supply the global infinite-path construction. The present proof additionally provides rough composite bands, safe supports, simultaneous exceptional-direction estimates and connections across scales. The mathematical statements and proofs are unchanged. Formalization. The original existence conclusion and the displayed main theorem have a public Lean 4 formalization. The recorded 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.