Bolo Formalization

项目把《From Linearity to Borrowing》逐节翻译成 Lean 4 定义、定理与证明，`Paper/INDEX.md` 对应论文每个编号结果。已机械化 Fundamental Property，并从类型推导证明闭合程序能从空内存运行到 `unit`；仓库还明确标出哪些证明是对原论文补写或对语义定义的修订。