LBIT Proofs 1: Propositions 1-9 — LessWrong