A Registered-Provenance Audit of IUT III, Corollary 3.12, Step (xi)

Publication/preprint comprising a 50-page manuscript, a 5-page reader guide, and an 85-page registered-coverage technical audit report. Theorem A is a Lean theorem about frozen registered syntax: every registered derivation of the frozen target has provenance intersecting the generated target seed. Certificate B mechanically checks the internal consistency of the declared finite registration and its 147-row coverage; it does not prove source-faithfulness. Hypothesis F, the existence of a RegisteredFaithfulnessBridge that compiles the selected class of public derivations and preserves target-freeness as provenance seed-freeness, is unproved. The Conditional Corollary excludes a public target-free derivation only if Hypothesis F is supplied. This preprint does not unconditionally establish public-source or complete-IUT non-derivability, an IUT gap, falsity of Corollary 3.12, falsity of IUT, or falsity of the abc conjecture. External human specialist review is pending.