BGW formalization

Entry point of the library. It imports every area:

• Discrete trees and BGW laws (BGW.Tree, BGW.LocallyFinite.*, BGW.GeneratingFunction): finite plane trees with their list interface, Łukasiewicz coding and cycle lemmas, locally finite trees with the Bienaymé–Galton–Watson law of an arbitrary offspring law, its branching property and uniqueness, extinction, generations, size and degree conditioning, Kemperman identities, tilting, fringe laws and discrete contours.
• Probability tools (BGW.Probability): weak convergence, the continuous mapping theorem, Slutsky on varying spaces, Prokhorov and Skorokhod representation, convergence in measure.
• Skorokhod space (BGW.Skorokhod): càdlàg paths D T E with the J1 metric and Billingsley's complete metric, measurability, tightness criteria, scaling, the Vervaat map, jumps, and local paths DLoc.
• Metric-measure geometry (BGW.MetricMeasure): the Gromov–Hausdorff–Prokhorov metric on compact metric probability spaces, unrooted and rooted, with Polishness and sampled laws.
• Continuum trees (BGW.ContinuumTrees): real trees coded by continuous functions, the transfer of contour convergence to rooted GHP laws, the Brownian bridge and its Vervaat image, and the uniform leaf measure.
• Stable trees (BGW.StableTrees): the stable law and Lévy process, fluctuation and excursion theory, the height process, the Duquesne–Le Gall forest theorem and the limits of conditioned BGW trees, stable bridges, and the Marchal growth chain.

CLASSICAL_THEORY_COVERAGE.md maps each classical result C1–C39 to its declarations and module.