The second sentence is intended to be redundant, it gives further explanation as to the implications of the first sentence. (This doc was never intended to be a tight mathematical definition, only to give a quick introduction to the concepts, with links to the strict mathematical definitions.)
The reality is that the lattice or bounded poset formulation is only needed to understand that the specific language constraints described ensure that the dependency graph of any valid program can be statically determined to be a partial ordering. The compiler doesn't even need to build a DAG internally, it just needs to ensure the specific language constraints described are in place, and as a result, the language will be able to be parallelized in any manner consistent with the partial ordering of data dependencies.
Yes obviously, but nowhere is it clear that you actually have a lattice of any kind. Specifically, I see no reason why pruning DAGs of unused computations would yield a lattice, and this is a result you seem to rely on. Program lattice does indeed sound nicer than program bounded poset, but I would be more wary about misusing terminology than having a nice name! :)
Please understand that I'm not trying to be mean here. You mention you've been applying for grants to work on this, but if you don't explain the mathematics adequately or demonstrate how it differs from existing formalisms then I imagine people are just going to reject you instantly. I would suggest seriously trying to formalise some of this stuff in a proof assistant like Coq. That'll quickly tell you if your theory works or not.