refactor(Core/Probability): mathlib-register Gumbel, rewrite GumbelLuce

[hawkrobe]

From the GumbelLuce audit, targeting "what would actually go in mathlib": mathlib has no Gumbel (or any extreme-value) distribution, so the universal half becomes a genuine upstream candidate and the RUM half becomes thin glue.

• New Core/Probability/Gumbel.lean in the Mathlib/Probability/Distributions register (density → withDensity measure → CDF as a theorem → max-stability → the max-probability integral), location-scale, replacing the old bare-ℝ gumbelCDF/gumbelPDF pair that was stipulated in the wrong order (CDF primitive, never connected to its density) and the 150-line private FTC block.
• GumbelLuce.lean rewritten: shared n-ary RUM carrier rumMaxProb lands in RandomUtility.lean (parallel to the probit side); mcfaddenIntegral — an unevaluated proof intermediate consumers were quantifying over — is gone, with Flemming2021/GaussianChoice/SignalDetection restated over rumMaxProb/softmax/sigmoid (Flemming's MaxEnt=RUM theorem now states the claim its docstring made); fromGumbelRUM is defined through fromSoftmax.
• Attribution fixes verified against the McFadden 1974 PDF: Lemma 1 credited to Marschak and Holman–Marley per McFadden's own p. 111 note; the uniqueness section now states Lemma 2's hypotheses and its terminal-step scope; Yellott 1977 binary non-uniqueness noted; verified bib entries yellott-1977/marschak-1960/luce-suppes-1965 added; stale Core.Agent.* doc paths swept.