Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Radial coordinates for a cyclic triangle quotient

Abstract

Cyclic edge identifications of closed triangles give the closed unit disk with explicit radial coordinates.

Let n be a positive natural number. Take n copies of the closed triangle with coordinates a and b satisfying a >= 0, b >= 0 and a+b <= 1. The sector labels have the discrete topology, each triangle has its relative Euclidean topology, and the product has the product topology. Identify (i,t,0) with (i+1,0,t), where the sector addition is modulo n and 0 <= t <= 1. Only these identifications generate the equivalence relation.

In the formulas, N denotes the natural numbers, R the real numbers, C the complex numbers, and pi the usual positive circle constant. The function sector gives the label’s integer representative from zero to n-1. Carrier selects the triangle point, and first and second select its coordinates. Coordinates forget a triangle subtype proof. Some and None are the constructors of an option type. The symbol imaginary denotes the imaginary unit, exp is the complex exponential, and real scalars are included in C when multiplied by a complex expression. Class is the projection to the actual generated quotient. The closed disk has the relative topology from C. No separation property of the quotient is assumed.

Definition 1.1 (The closed coordinate triangle).

Formalization. D5/S3/Geometry/Gluing/CyclicTriangleDisk.Triangle (✓ std3).

Source. Repository-derived.

Commentary.

A triangle point carries exactly the three coordinate inequalities.

Definition 1.2 (Sector copies of the triangle).

Formalization. D5/S3/Geometry/Gluing/CyclicTriangleDisk.Point (✓ std3).

Source. Repository-derived.

Commentary.

A point consists of a sector label and a point of the closed triangle.

Definition 1.3 (Exchange the two triangle coordinates).

Formalization. D5/S3/Geometry/Gluing/CyclicTriangleDisk.swap (✓ std3).

Source. Repository-derived.

Commentary.

Exchanging the coordinates preserves nonnegativity and their sum.

Definition 1.4 (The radial coordinate).

Formalization. D5/S3/Geometry/Gluing/CyclicTriangleDisk.radius (✓ std3).

Source. Repository-derived.

Commentary.

The radial coordinate is the sum of the two nonnegative triangle coordinates.

Definition 1.5 (The origin in a sector).

Formalization. D5/S3/Geometry/Gluing/CyclicTriangleDisk.apex (✓ std3).

Source. Repository-derived.

Commentary.

Every sector has an origin with both triangle coordinates zero.

Definition 1.6 (The original edge identification).

Formalization. D5/S3/Geometry/Gluing/CyclicTriangleDisk.seam (✓ std3).

Source. Repository-derived.

Commentary.

A seam starts on the edge b=0 and ends at the swapped point in the next sector. The triangle inequalities give the full original range 0 <= a <= 1.

Definition 1.7 (Equivalence generated by the seams).

Formalization. D5/S3/Geometry/Gluing/CyclicTriangleDisk.Related (✓ std3).

Source. Repository-derived.

Commentary.

The relation is the equivalence closure of the actual seam relation.

Definition 1.8 (Canonical apex or positive representative).

Formalization. D5/S3/Geometry/Gluing/CyclicTriangleDisk.normal (✓ std3).

Source. Repository-derived.

Commentary.

The common apex is represented by None. A positive point on b=0 moves once to the next sector; every other positive point stays in its own sector. Every representative inside Some has strictly positive second coordinate.

Theorem 1.9 (Exact seam classes).

Proof. Machine-checked in Lean as D5/S3/Geometry/Gluing/CyclicTriangleDisk.related_iff_normal_eq (✓ std3). ∎

Source. Repository-derived.

Commentary.

Each generating seam preserves the displayed representative, so induction on the equivalence closure gives one implication. A positive point reaches its representative by zero or one seam. At radius zero both coordinates vanish, and successive zero seams connect all sector origins. Joining these actual paths gives the converse.

Definition 1.10 (The sector angle).

Formalization. D5/S3/Geometry/Gluing/CyclicTriangleDisk.angle (✓ std3).

Source. Repository-derived.

Commentary.

At positive radius the fraction a/(a+b) subdivides the angular interval of the chosen sector. For a positive canonical representative it lies in [0,1). The auxiliary angle extends to the origin of sector i with value (2*pi/n)*i. The radius is nonnegative, so the zero and positive cases exhaust all points. The radial map has its own zero-radius value zero, independently of this angle extension.

Definition 1.11 (The complex radial expression).

Formalization. D5/S3/Geometry/Gluing/CyclicTriangleDisk.radial (✓ std3).

Source. Repository-derived.

Commentary.

At radius zero the value is zero. At positive radius the complex exponential gives the prescribed angle and preserves the radius.

Theorem 1.12 (The original exact radial norm).

Proof. Machine-checked in Lean as D5/S3/Geometry/Gluing/CyclicTriangleDisk.radial_norm (✓ std3). ∎

Source. Repository-derived.

Commentary.

This is the existing radius identity, now public with its statement and proof unchanged. The actual affine-link strict chart consumes it to identify the preimage of the open unit disk with a+b<1. This API exposure is not a new mathematical theorem.

Theorem 1.13 (A polar angle in a half-open period).

Proof. Machine-checked in Lean as D5/S3/Geometry/Gluing/CyclicTriangleDisk.positive_circle_angle (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every complex number has a polar angle in [0, 2π), including zero.

Theorem 1.14 (Exact fibers of the radial map).

Proof. Machine-checked in Lean as D5/S3/Geometry/Gluing/CyclicTriangleDisk.radial_eq_iff_related (✓ std3). ∎

Source. Repository-derived.

Commentary.

The radial expression agrees across every actual seam, including the final sector wrapping to sector zero. Equality of images recovers the common radius from the complex norm. Positive canonical representatives have angles in [0,2*pi), where the circle parametrization is injective at nonzero radius. Disjoint half-open sector intervals recover the label, then the angular fraction and both triangle coordinates. The already constructed seam paths identify the original points.

Definition 1.15 (The closed unit disk).

Formalization. D5/S3/Geometry/Gluing/CyclicTriangleDisk.Disk (✓ std3).

Source. Repository-derived.

Commentary.

The disk is the complex norm sublevel set with radius one.

Definition 1.16 (The radial map with disk codomain).

Formalization. D5/S3/Geometry/Gluing/CyclicTriangleDisk.diskRadial (✓ std3).

Source. Repository-derived.

Commentary.

The image norm equals a+b and therefore is at most one.

Definition 1.17 (The equivalence structure of the seams).

Formalization. D5/S3/Geometry/Gluing/CyclicTriangleDisk.seamSetoid (✓ std3).

Source. Repository-derived.

Commentary.

The equivalence closure supplies the reflexivity, symmetry and transitivity laws.

Definition 1.18 (The topological seam quotient).

Formalization. D5/S3/Geometry/Gluing/CyclicTriangleDisk.Fan (✓ std3).

Source. Repository-derived.

Commentary.

The projection from the sector copies induces the quotient topology.

Definition 1.19 (The induced map on seam classes).

Formalization. D5/S3/Geometry/Gluing/CyclicTriangleDisk.quotientRadial (✓ std3).

Source. Repository-derived.

Commentary.

Constancy on the generated seam classes gives a well-defined disk-valued map.

Theorem 1.20 (The quotient is the closed disk).

Proof. Machine-checked in Lean as D5/S3/Geometry/Gluing/CyclicTriangleDisk.quotientRadial_isHomeomorph (✓ std3). ∎

Source. Repository-derived.

Commentary.

At the apex, the identity norm(radial(x))=radius(x) proves continuity without an angular limit. Away from the apex, division by the nonzero radius and the complex exponential are continuous. To obtain a preimage of a nonzero disk point, choose its angle theta in [0,2pi), set t=ntheta/(2pi), and use sector floor(t). With f=t-floor(t) and r equal to the point’s norm, the triangle coordinates are rf and r*(1-f). They have radius r and the prescribed angle. The exact fiber theorem gives injectivity on the quotient. The triangle, its finitely many sector copies and the quotient are compact, while the disk is Hausdorff. Thus the continuous bijection is a homeomorphism.

Definition 1.21 (Bundled radial homeomorphism).

Formalization. D5/S3/Geometry/Gluing/CyclicTriangleDisk.homeomorphism (✓ std3).

Source. Repository-derived.

Commentary.

The bundled homeomorphism has exactly the induced radial map as its forward function. Restricting it to the inverse image of the open unit disk gives a homeomorphism to that open disk. This inverse image is an open neighborhood of the common apex class. Its inverse image under the class projection is exactly a+b < 1, and a+b=1 maps to the unit circle. For a return orbit of length r >= 1 the parameter n=3r satisfies the source range n >= 3. Applying this fan model to an actual link still requires an ordered enumeration of all 3r corner occurrences, a biconditional between the original pairing closure and these seams, and the saturated openness and subspace quotient topology of the strict corner neighborhoods. The standalone fan homeomorphism establishes none of those correspondences or the orientability and genus of the full link. The fan-disk model and compact-to-Hausdorff criterion are classical.

References