A mass gap is a statement about the spectrum of an operator, but a latticegauge theory is given as a measure. The passage between the two - theOsterwalder-Seiler reconstruction - proceeds through reflection positivity, aGelfand-Naimark-Segal space, a transfer operator, and an identification theoremasserting that expectations in the measure are matrix elements of thatoperator. This paper reports a complete formal verification of that passage, inLean 4 with mathlib, for the Z_2 lattice gauge chain: from the Boltzmann weightexp(beta s) to exponential decay of a correlation function of the measure, withevery arrow a machine-checked theorem and no arrow assumed. The endpoint is theexact identity E_n[f(sigma_0) f(sigma_n)] = (tanh beta)^n for the signobservable, a statement in which no operator occurs and whose proof goes throughone, and whose rate is exactly the verified non-vacuum transfer eigenvaluetanh beta; equivalently, the normalised transfer operator has spectral gap1 - tanh beta > 0, and the corresponding mass is -log(tanh beta) > 0 forbeta > 0. All three are machine-checked.We state the limits with the same precision as the results. The system has oneZ_2 variable per time slice, so its spatial slice is a point and its transferoperator is a 2x2 matrix; a lattice with spatial extent is not treated. Thebound is at fixed finite size and is NOT volume-uniform. The pairing of thissystem is definite - proved, not assumed - so the Gelfand-Naimark-Segalquotient is the identity and therefore does no work; a system with a degeneratepairing still needs it. The underlying mathematics is textbook:Osterwalder-Seiler is from 1978 and the transfer matrix of the Ising chain isolder still. The contribution claimed here is not a new theorem but a verifiedcomposition: that the interfaces of the reconstruction fit together with nothinghidden between them, exhibited on the smallest system where all of them aresimultaneously present. Nothing in this paper is a claim about SU(N), thecontinuum limit, or the Yang-Mills mass gap.