Would a proof that the traveling salesman algorithm can't be encoded on LAL also prove P!=NP?
Yes, in the same sense that if you prove that a specific NP-complete problem can't be reduced to a specific P-hard problem, then you also prove P!=NP. The only issue is that the reduction for which P-hardness hold must be "compatible" with the allowed encodings.

From the information you give in the question, I conclude that LAL is P-time hard. The article Light types for polynomial time computation in lambda calculus by R. Baillot and K. Terui confirms this, by showing that DLAL (dual light affine logic) is a P-complete subset of LAL.



My own experience is that many P-complete problems look attractive and natural. My favorites are linear programming and Horn-satisfiability, but I guess that DLAL (or LAL) look even more attractive to you. But even so they are attractive, using them for resolving N!=NP is probably futile. More than one reduction of specific NP-complete problems to linear programming has been published, but the reductions turned out to exponentially increase the size of the problem.