Gcd quotients: a quantitative lower bound and sharp fixed-dimensional orders

For a finite set A of positive integers, let Q(A) be the set of a/gcd(a,b) for a,b in A, and let h(n) be the minimum of |Q(A)| over n-element sets. We prove h(n) >= sqrt(n) exp(c sqrt(log(n)/log(log(n)))) for all sufficiently large n, with an explicit formalized constant c = 1/16000. For positive integers whose prime divisors lie in any prescribed set of d distinct primes, we determine h_d(n) = Theta_d(n^u_d), where u_1 = 1 and u_d is the minimum of (u_p+u_s)/(1+u_p+u_s) over positive splits p+s=d. Both headline results have Lean proofs. The paper compares these results with the classical planar bound, earlier fixed-dimensional lower bounds, the 2026 ProofCouncil upper-bound construction, and recent Lean developments. Our construction refines the earlier layering method; the fixed-dimensional theorem gives matching lower and upper bounds in every dimension. No priority claim is made over the unknown contents of the unpublished Bollobas-Leader work. The full unrestricted order remains open.