OAI.FKCRT.finite_fk_maps_converge_to_brownian_crt

The theorem states that, for every real q>4, there is a constant c>0 such that the following holds for every probability space (Ω,P) carrying three independent real-valued standard Brownian motions B₀,B₁,B₂ (each satisfying Mathlib's IsBrownianReal, jointly independent as random functions on the nonnegative reals). Let the standard excursion be e(t)=√(Σᵢ(Bᵢ(t)−t·Bᵢ(1))²) on [0,1], the norm of three independent Brownian bridges, and let its tree be the quotient of [0,1] by the pseudometric e(s)+e(t)−2·inf of e over the interval between s and t, carrying the pushforward of Lebesgue measure. For n≥0, the finite model is the Fortuin–Kasteleyn law on rooted oriented genus-zero planar maps with n+1 edges, loops and multiple edges allowed, together with an arbitrary subset A of edges. Its weight is q^(k(A)+(|A|−V)/2), where k(A) counts connected components of the spanning graph on all vertices with edges A and V is the number of vertices, normalized by the total partition function. Each map is viewed as its vertex set with graph distance multiplied by c/√(n+1) and with the degree measure, namely each vertex weighted by its degree divided by 2(n+1). Then for every bounded test function F on measured metric spaces that is continuous in the Gromov–Hausdorff–Prokhorov distance at all compact metric probability spaces, the expectation of F under the finite law converges, as n→∞ through all integers, to the expectation of F at the Brownian excursion tree. This is an admitted theorem statement, not a verified proof.