An Explicit Collar Recursion for Type-013 Benzel Tilings

Benzels form a two-parameter family of threefold-symmetric regions in the hexagonal grid. They are tiled by three-cell shapes: triangular stones, called right and left, and straight bones in three orientations. In any such tiling, the number of right stones minus the number of left stones depends only on the region; this is the Conway–Lagarias invariant. We prove that a benzel can be tiled without right stones exactly when this invariant is nonpositive, answering Propp's Problem 4. The main construction is an explicit collar around a smaller benzel. It reduces both boundary parameters by three and consists of one left stone, two chains of diagonal bones, and vertical bones in the remaining columns. Iteration reduces the existence problem to the known bone-only family of Kim and Propp and three small initial tilings. We also give a closed formula for the left-stone positions: they lie on a straight line and their number is exactly the negative of the invariant. A Lean 4 formalization checks the construction and the existence theorem for the same cell regions and allowed tile shapes.