On the Constructive Theory of Jordan Curves

TL;DR

This paper develops a constructive framework for Jordan curves, proving their properties and their relation to the winding number within Bishop's constructive analysis, providing new insights and detailed expository material.

Contribution

It introduces a new constructive definition of Jordan curves, proves their key properties, and relates their index to the classical winding number within Bishop's framework.

Findings

Equivalent definitions of Jordan curves established

Properties of Jordan curves and index functions proved

Index of a point equals the winding number in the complex plane

Abstract

Using a definition of Jordan curve similar to that of Dieudonn\'e, we prove that our notion is equivalent to that used by Berg et al. in their constructive proof of the Jordan Curve Theorem. We then establish a number of properties of Jordan curves and their corresponding index functions, including the important Proposition 32 and its corollaries about lines crossing a Jordan curve at a smooth point. The final section is dedicated to proving that the index of a point with respect to a piecewise smooth Jordan curve in the complex plane is identical to the familiar winding number of the curve around that point. The paper is written within the framework of Bishop's constructive analysis. Although the work in Sections 3--5 is almost entirely new, the paper contains a substantial amount of expository material for the benefit of the reader.