A Lean-Checked Finite Farey Mediator Theorem: Source Provenance, an Obstructed Endpoint Taxonomy, and a Direct Euclidean Constructor

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. It does not prove an infinite spectral theorem, the Riemann Hypothesis, full Super Information Theory, or a physical claim.