Forgetting and completeness: the centre of the passage from Theorem 3.11 to Corollary 3.12 in inter-universal Teichmüller theory

The passage from Theorem 3.11 to Corollary 3.12 in inter-universal Teichmüller theory (IUT) is formulated as a problem of completeness in the sense of abstract interpretation: a forgetful map is complete for a query if the query factors through it. Sign abstraction (complete for products, incomplete for sums) and the interval dependency problem show that completeness is query-relative and that local completeness does not compose. In the cited theory fixing the log-volume content cited in the proof of Corollary 3.12, the conclusion follows once the scale defect Δ=(s-1)·vol(θ) is nonpositive, and on extremal data with no slack this is also necessary; preservation itself is Δ=0, i.e. s=1. Relative to the IUT route, a sufficient condition for the ABC-type conclusion thus reduces to whether the real scale is preserved through the whole transport; this is not an unconditional equivalence with the ABC conjecture. An interface-by-interface audit of IUT I–IV and the Frobenioid/étale-theta/absolute-anabelian sources finds every audited interface locally closed except one square: the lift of the Θ-link from bare to marked prime-strips. The abstract frame is checked in Lean (standalone Mathlib core included); the reduction to a scale defect itself is credited to Scholze–Stix and to Project LANA's xi_iff, of which this formulation is the reciprocal parameterization. Neither Corollary 3.12 nor the ABC conjecture is decided.