Finite-Defect Path Models for Peripheral Benzel Tilings: Propp's Problem 6 and the First Defect Diagonal

Propp asked for the number of tilings of the peripheral benzel B(n,2n-3) by right stones and all three orientations of bones. We prove his conjectured closed form for every n >= 5.

We then place the rigid case in a finite-defect hierarchy on the diagonals b=2a-d. In the nonoverlap range, an owner-label energy determines the exact defect number for d=3k and d=3k+1. Thus d=4 is the first one-defect diagonal. Deleting the unique defect gives three independent labelled ballot paths and five defect classes. Their exact cyclic ballot sum is evaluated by a specialized multivariate Lagrange-Good calculation, yielding an algebraic generating function for T_103(a,2a-4).

The accompanying Lean 4 development formalizes the literal exact-cover arguments, finite-defect theorem, one-defect bijection, ballot enumeration, and generating-function identities. The complete trust-zero audit maps all 20 Problem 6 labels and all 32 first-defect labels to exact endpoints and reports only propext, Classical.choice, and Quot.sound.