A Lean-Checked Finite Farey Mediator Theorem

This revised preprint presents a Lean-checked theorem about finite Farey carriers. It proves that two listed reduced fractions in increasing order with determinant greater than one have a listed strict mediator. The proof package also preserves a counterexample showing that an earlier endpoint-shape classification was incomplete, while demonstrating that the target theorem survives through a direct Euclidean bounded-inverse construction. The promoted counterexample proof is kernel reducible, the complete constructor chain is included, and an independently implemented enumeration checks more than one million qualifying ordered pairs through order forty without a failure. The result is deliberately bounded. Its conclusions are limited to the assumptions, evidence, and testing conditions stated in the manuscript. It belongs to the arithmetic operator and Branch C research program. This is a corrected preprint edition released under the Creative Commons Attribution 4.0 license.