Has the notion of "non-cheating" quines been formalised?
Most formal semantics for programing languages tend to keep things simple, in particular, it's pretty rare to have the ability to express "grabbing your own source code" in a formal semantics.

This has the somewhat dubious advantage of disallowing some kinds of "cheating" by construction: the "cheat" is simply not part of the language semantics. In particular, a simple lambda calculus with simple string concatenation and printing primitives cannot implement many (any?) of the "cheats" you have in mind. In such a language, a quine might be a program which prints the exact string representation of it's own code. You can even avoid the print primitive if you allow returning the string rather than printing it. In that case, you only need string literals and concatenation.

It's a useful exercise to figure out various properties of quines in such a language. It's pretty easy to see that some variable will need to be repeated twice: there are no "linear" quines. However the statement 


  This structure is read twice, once to reformat it into the code part of the final output, and a second time where it's copied verbatim to reproduce the data part. 


is a bit vague, and I'm not sure it's true in general, depending on the precise meaning of "copied verbatim".