Jordan curves traced by paths #
A path whose two endpoints agree is a parametrised closed curve, but its range need not be a
Jordan curve: the path may pause, retrace an arc, or cross itself. This file supplies the exact
criterion needed to exclude those degeneracies. If a closed path has no repeated values except
for its two endpoint parameters, its range is a Jordan curve
(TauCeti.isJordanCurve_range_of_eq_or_eq_endpoints).
The proof uses the quotient model of the circle already in Mathlib. The extension of a path
γ : Path x x to ℝ has equal values at 0 and 1, so
AddCircle.liftIco 1 0 γ.extend factors it through the additive circle ℝ / ℤ. The hypothesis on
repetitions says precisely that this factor is injective, and its range is the range of γ. The
additive circle is itself a Jordan curve, AddCircle.homeomorphCircle identifying it with
Circle, so TauCeti.IsJordanCurve.image carries that along the factor: the compactness argument
upgrading a continuous injection to a homeomorphism onto its image is already packaged there and is
not repeated here.
The condition is stated directly rather than bundled as a new notion of simple closed path. This is the only operation needed here, and keeping it as a theorem hypothesis avoids introducing a second simplicity vocabulary alongside Mathlib's path API.
Gluing two arcs #
The criterion has one immediate use that is worth naming on its own: two arcs — ranges of
injective paths — that share their two endpoints and meet nowhere else glue to a Jordan curve
(TauCeti.isJordanCurve_range_union_range_of_inter_eq_pair). The closed path traversed is
γ.trans δ.symm, whose range is range γ ∪ range δ; the meeting hypothesis is what turns a
coincidence between a value of γ and a value of δ into a coincidence of endpoints, and
injectivity of each of the two paths handles the coincidences internal to one of them. The
endpoints are not asked to be distinct: injectivity of δ already forces that, since a path with
equal endpoints repeats the value at the two distinct parameters 0 and 1.
Main results #
TauCeti.isJordanCurve_range_of_eq_or_eq_endpoints— the range of a closed path whose only possible repetition is its pair of endpoints is a Jordan curve.TauCeti.isJordanCurve_range_union_range_of_inter_eq_pair— two arcs with the same two endpoints, meeting exactly there, glue to a Jordan curve.
Roadmap role #
This is the topological gluing step used by layer L5 of
TauCetiRoadmap/ConformalMapping/README.md, the Carathéodory boundary correspondence. A
finite-length image crosscut is already packaged as a path with exactly this simplicity property in
TauCeti/Analysis/Complex/Conformal/Crosscut/Path.lean; when its two boundary ends coincide, the
first result below identifies the closure of that crosscut as a Jordan curve, and when they are
distinct the second closes that crosscut up with an arc of the boundary of the image domain. The
coincident-end specialization is in TauCeti/Analysis/Complex/Conformal/Crosscut/Jordan.lean and
the distinct-end one in TauCeti/Analysis/Complex/Conformal/Crosscut/Arc.lean.
The range of a simple closed path is a Jordan curve. Let γ : Path x x be a closed path.
If equality γ s = γ t forces either s = t or the unordered pair of parameters to be {0, 1},
then range γ is homeomorphic to the circle.
The disjunction records both orientations of the exceptional endpoint pair explicitly. No local
injectivity or embedding hypothesis is needed, and no separation assumption on the ambient space
beyond the Hausdorffness that TauCeti.IsJordanCurve.image asks for.
Gluing two arcs along their endpoints #
Two arcs meeting exactly at their common endpoints glue to a Jordan curve. Let
γ δ : Path x y be injective and let their ranges meet in exactly the two endpoints,
range γ ∩ range δ = {x, y}. Then range γ ∪ range δ is a Jordan curve.
The curve traversed is γ.trans δ.symm, a closed path at x whose range is range γ ∪ range δ
by Path.trans_range and Path.symm_range. Its only repetitions are the ones
TauCeti.isJordanCurve_range_of_eq_or_eq_endpoints allows: a coincidence between two parameters on
the same half is excluded by injectivity of that half, and one between the two halves lands in
{x, y}, so it is either the pair {0, 1} of endpoint parameters or the single parameter 1 / 2
at which the two halves are joined.
Distinctness of x and y is a consequence rather than a hypothesis: δ 0 = δ 1 would contradict
injectivity of δ.