013 型 Benzel 铺砌的显式领圈递归

Propp's Problem 4 asks whether every benzel with nonpositive Conway--Lagarias invariant can be tiled using left stones and all three orientations of bones, with no right stones. We prove that the answer is yes by an explicit universal collar recursion. Iteration reduces every negative-invariant case to a bone-only Kim--Propp benzel or one of three small initial tilings. The construction also gives a closed straight-spine formula for all left-stone bases. The existence theorem and strengthened exact-spine endpoint are formalized in Lean 4 on the literal cell and prototile carriers and checked at trust level zero.