Exact Enumeration and Fixed-Rank Asymptotics of Ballot-Admissible Fibonacci Ribbon Tableaux

Tenn asked for the enumeration of ballot-admissible Fibonacci ribbon tableaux beyond the three-letter case. We solve this problem for every alphabet size n >= 2 by encoding ribbon columns as an alternating dominant type-A walk and contracting the unique ballot-neutral forbidden adjacency. Endpoint-preserving inclusion-exclusion yields an exact finite formula and a highest-weight refinement in explicit Schur coefficients. Exact Weyl integral representations and Regev's strip asymptotics yield the fixed-rank leading asymptotic, including its explicit positive constant, for every fixed n >= 3. In the stable range n >= k, the count is the number of involutions with no adjacent transposition; a Poisson limit proves the 1/e limiting-proportion conjecture recorded in OEIS A170941. On each fixed-distance line n = k-r, the defect is eventually polynomial in k. The accompanying Lean 4 development provides premise-free publication endpoints for all 47 numbered mathematical labels. The complete publication root is checked with --trust=0, with axiom surface limited to propext, Classical.choice, and Quot.sound. Public source and release assets are available at https://github.com/crabsatellite/fibonacci-ribbon-ballot-enumeration.