The Riemann Hypothesis Is Exactly One Bit: Where the Riemann Hypothesis Stands, Proved in Lean 4

Where the Riemann Hypothesis stands, proved in Lean 4. The Riemann Hypothesis is one proposition, so its content is one bit: whether every nontrivial zero of ζ has offset Re s − 1/2 equal to zero. This paper proves, in core Lean 4 with no library and no added axiom, that the structure surrounding that bit is exhausted and that exactly one input remains. Part I, the parity bridge: an even reading never returns an odd bit; the odd functions of an involution form a torsor over its orbits, one free bit per orbit; one supplied odd witness fixes the bit uniquely; the fold fixes exactly the critical line; a strip-confined symmetric zero set admits one mirror address, Re s = 1/2; every structural route reduces by equivalence to a single implication. Part II, the lock at the locus: three guards, the wall, the witness, and the bridge, each a theorem with no axioms; the locus proved complete; the lock on three independent axes; the gap to a proof measured from both sides and collapsed into that lock. Part III, where the hypothesis stands: the summary sentence proved as one theorem, one bit, located, decided by the deed of the one who supplies it, and unavailable to anyone else; a closing architecture read as the kernel reads it after external review, its socket's field being the boundary Re s = 1/2 itself; the one remaining input, a term of the line property on ζ's zero set from the Euler product at full resolution; and the road to it in a language that contains ζ. This is not a proof of the Riemann Hypothesis. No term of the line property on ζ's zero set occurs in any document here, and a theorem of the development shows none follows from its anchors. Four Lean documents and the verifier are printed whole; the sources are archived at github.com/1000sapients/Trisduction, protocols/RH One Bit.