PathSelectionProof.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Discharge the published completed-measure path-selection input by parametrizing the Borel relation with Baire space and selecting a branch.