Registry · Definition III.D40 tau-effective formalized

III.D40 — Hartogs Flow Operator

H_flow: acts on ω-germ assignments and produces their Hartogs extensions. Fluid flow = transport of ω-germs along τ³ fibration via Local Hartogs continuation (Book II Part VI).

Book III Part 5 Ch. 36

Dependency Graph

Depends on (2)

Depended on by (4)

Lean Formalization

Module: TauLib.BookIII.Physics.HartogsFlow

Symbol: flow_check