Fix misc issues from issue #7: missing sidebar theorems, premature completion message, and proof simplification

- InnerProductWorld Level 8: Add TheoremDoc and NewTheorem for inner_product_expansion and cross_term_bound, mention add_sq in Introduction
- LinearMapsWorld Level 7: Replace premature "Congratulations on completing LinearMapsWorld!" with forward-looking message
- LinearMapsWorld Level 5: Use linear_map_preserves_zero in non-empty proof and add it to sidebar

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Author: ZRTMRH