Is HORN-SAT in LIN, if so why is that not an indication that P=LIN?
The deterministic time hierarchy theorem precludes all problems in P being decided in linear time.  If you try to reduce a problem to HORN-SAT that requires more than linear time to decide, you'll find that the reduction itself requires more than linear time.