Beatty First-Passage Counts: Limit Laws, Fractal Geometry, and Arithmetic Rigidity

For a real slope α > 1 let c_(r) be the number of binary words of length ⌊αr⌋ + 1 whose running proportion of ones stays at least 1/α on every proper prefix and falls below it at the last letter. We show that for every real α > 1 the empirical distribution of the normalized counts $R_r=r\,c_r/\binom{\lfloor\alpha r\rfloor-1}{r-1}$ converges to an explicit law μ_(α), the image of Lebesgue measure on (0, 1] under a cumulative jump profile built from the counts themselves. For irrational α the ratios follow the profile at the Beatty phase {rα}, which proves a hypothesis of Bauer, Godrèche and Luck; the limit points form a null perfect set K_(α) and μ_(α) is singular continuous. For α = a/b the law is uniform on b atoms. The map α ↦ μ_(α) is right-continuous and continuous exactly at the irrationals. The set K_(α) has Minkowski dimension 2/3 with explicit content for every irrational slope, while its Hausdorff dimension is governed by Diophantine approximation: it equals 2/3 exactly when α has irrationality exponent 2, its two-thirds Hausdorff measure is positive exactly when α is badly approximable, it equals 2/(2 + ν) at regular slopes of Diophantine class ν, it vanishes at Liouville slopes, and its values over all irrational slopes fill [0, 2/3]. Slopes of the same Diophantine class ν > 1 can have dimension 2/(2 + ν), $s^*(\nu)=2(\sqrt{1+3\nu}-1)/(3\nu)$, or, when their good approximations recur at a fixed logarithmic rate, an explicit value strictly between the two, so the Hausdorff dimension of K_(α) is not a function of the class, while the lower Hausdorff dimension 2/(1 + ω) of the law μ_(α) is a function of the irrationality exponent ω. In the Gamma normalization of Bauer, Godrèche and Luck the same counts have an absolutely continuous limit law with an explicit density. Gap ratios recover the embedded slope field. At a transcendental slope the unordered normalized gap spectrum determines the slope, and every affine equality between cluster sets forces the identity map. The normalized gaps across all algebraic translates are jointly linearly independent over the real algebraic numbers. At the golden slopes φ, φ², shared gaps occur exactly at alternating Fibonacci index pairs, yet the cluster sets are affinely inequivalent. Complementary gap coordinates have rational rank equal to the algebraic degree once enough coordinates are included; all rational cancellations are controlled by the minimal polynomial. The square-root-two complementary spectra are disjoint, with an explicit separation bound. These results and the main limit and geometry theorems are formalized in Lean 4 for the actual counts. A general algebraic zero-or-separated bound uses a written Liouville argument. Appendix A records the precise formalization boundary.