Add Lean-kernel formal verification for Theorem 4.2

Update logbook: Reproduction: Revisiting Padded Transformer Expressivity: Which Architectural Choices Matter and Which Don't