TauLib.Holomorphy.GlobalHartogs

The Global Hartogs Extension Theorem — the CLIMAX of Book I.

Registry Cross-References

• [I.T31] Global Hartogs Extension — global_hartogs

Ground Truth Sources

• chunk_0072_M000759: Program monoid, normal form

• chunk_0310_M002679: CRT decomposition, primorial structure

Mathematical Content

THE BOOK I CLIMAX.

If f ∈ HolFun is defined on L \ K with K primordially thin, then f extends uniquely to all of L.

Proof strategy:

• Spectral coefficients are determined by restriction data (I.T29)

• CRT extension at each primorial stage (I.L08)

• Tower coherence ensures global consistency (I.D46)

• Uniqueness by Identity Theorem (I.T21)

This uses ALL machinery from Parts IX-XII.

Tau.Holomorphy.HartogsData

source structure Tau.Holomorphy.HartogsData :Type

A Hartogs extension pair: two tower-coherent functions that agree outside a thin set K at some reference depth.

• f₁ : StageFun
• f₂ : StageFun
• coh₁ : TowerCoherent self.f₁
• coh₂ : TowerCoherent self.f₂
• depth : Denotation.TauIdx

• agree_ref

  (n : Denotation.TauIdx)

  agree_at self.f₁ self.f₂ n self.depth Instances For

Tau.Holomorphy.global_hartogs

source **theorem Tau.Holomorphy.global_hartogs (hd : HartogsData)

(n k : Denotation.TauIdx) :k ≤ hd.depth → agree_at hd.f₁ hd.f₂ n k**

[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.

Tau.Holomorphy.hartogs_unique_b

source **theorem Tau.Holomorphy.hartogs_unique_b (hd : HartogsData)

(n k : Denotation.TauIdx) :k ≤ hd.depth → hd.f₁.b_fun n k = hd.f₂.b_fun n k**

Hartogs uniqueness for B-sector: extension is unique.

Tau.Holomorphy.hartogs_unique_c

source **theorem Tau.Holomorphy.hartogs_unique_c (hd : HartogsData)

(n k : Denotation.TauIdx) :k ≤ hd.depth → hd.f₁.c_fun n k = hd.f₂.c_fun n k**

Hartogs uniqueness for C-sector: extension is unique.

Tau.Holomorphy.hartogs_ingredient_spectral

source theorem Tau.Holomorphy.hartogs_ingredient_spectral (f₁ f₂ : StageFun) :(∀ (n k : Denotation.TauIdx), spectral_of f₁ n k = spectral_of f₂ n k) → f₁ = f₂

Ingredient 1: Spectral coefficients determine the function (I.T29).

Tau.Holomorphy.hartogs_ingredient_crt

source **theorem Tau.Holomorphy.hartogs_ingredient_crt (f : StageFun)

(hcoh : TowerCoherent f)

(n k : Denotation.TauIdx) :Polarity.reduce (f.b_fun n k) k = f.b_fun n k**

Ingredient 2: CRT extension constrains values via reduce (I.L08).

Tau.Holomorphy.hartogs_ingredient_coherence

source **theorem Tau.Holomorphy.hartogs_ingredient_coherence (f : StageFun)

(hcoh : TowerCoherent f)

(n k l : Denotation.TauIdx)

(hkl : k ≤ l) :Polarity.reduce (f.b_fun n l) k = f.b_fun n k**

Ingredient 3: Tower coherence gives downward propagation.

Tau.Holomorphy.hartogs_ingredient_identity

source theorem Tau.Holomorphy.hartogs_ingredient_identity (f₁ f₂ : StageFun) :TowerCoherent f₁ → TowerCoherent f₂ → ∀ (d₀ : Denotation.TauIdx), (∀ (n : Denotation.TauIdx), agree_at f₁ f₂ n d₀) → ∀ (n k : Denotation.TauIdx), k ≤ d₀ → agree_at f₁ f₂ n k

Ingredient 4: Identity Theorem provides uniqueness (I.T21).

Tau.Holomorphy.hartogs_id_example

source def Tau.Holomorphy.hartogs_id_example :HartogsData

Construct a Hartogs data from id_stage (agrees with itself trivially). Equations

• One or more equations did not get rendered due to their size. Instances For