We study maximum matching when the edges of a fixed graph arrive in a uniformly random order. For any fixed $\varepsilon>0$, we give a one-pass algorithm that achieves, with high probability over the arrival order, approximation ratios of $0.71295$ for unweighted graphs and $0.71295-\varepsilon$ for weighted graphs, using near-linear space with an explicit charge for weight precision. Both approximation ratios hold for bipartite and general graphs. The algorithm does not require the stream length or the weight range in advance. The main structural ingredient is a historical deletion inequality for weighted matchings. The deletion price of a vertex set is the decrease in maximum matching weight when that set is removed. We bound the sum of these prices for pairwise disjoint vertex sets, even when each price is evaluated at a different stage as edges are added to the graph. Applied to the usual unfolding of integer weights, it transfers a bipartite cardinality certificate to an original weighted matching, even when the original graph is not bipartite. This transfer preserves the approximation coefficient. We combine this transfer with a refined analysis of fractional matchings in the two auxiliary graphs arising in the transfer theorem. An exact rational linear-programming certificate proves the stated constant for every feasible graph profile. The approximation guarantees and the new structural results are formally verified in Lean.