Registry · Lemma II.L04 established formalized

II.L04 — Germ-Character Equivalence

Omega-germ data at a point is equivalent to boundary character data on L: the germ determines a unique character via bipolar projection, and the character recovers the germ via idempotent assembly.

Book II Part 6 Ch. 31

Dependency Graph

Depends on (6)

Depended on by (2)

Lean Formalization

Module: TauLib.BookII.Hartogs.MutualDetermination

Symbol: Tau.BookII.Hartogs.germ_character_check