Registry · Definition I.D68 tau-effective formalized

I.D68 — Earned Stage-Determined Point

An earned interior point: a value obtained by extending boundary data via Hartogs extension. Carries a tower-coherent StageFun and produces interior values that are self-consistent (reduced).

Book I Part 16 Ch. 63

Dependency Graph

Depends on (2)

Depended on by (1)

Lean Formalization

Module: TauLib.BookI.Holomorphy.BoundaryInterior

Symbol: Tau.Holomorphy.EarnedInteriorPoint