global_hartogs (theorem)

/-- [I.T31] The Global Hartogs Extension Theorem: Any two tower-coherent functions that agree at some reference depth agree at ALL depths ≤ that reference depth. Interpretation: if f is defined on L \ K and we can extend it to agree at depth d₀, then the extension is unique everywhere below d₀. The thin set K is "removable" because tower coherence forces the values on K to be determined by the surrounding data. Proof: direct application of the Identity Theorem (I.T21) which gives downward propagation of agreement via tower coherence. -/