How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Complex Coordinate and Path Transport — Examples
1 · Prerequisites
- Arc Length and Rectifiable Curves
- Binary Operations, Monoids, Groups and Subgroups
- Bounded Variation and the Riemann–Stieltjes Integral
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- Complex Coordinate and Path Transport
- Connectedness
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Continuity, IVT, EVT, and Uniform Continuity
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Foundations of the Real Numbers for Analysis
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Metric Spaces
- Monotone Functions, Discontinuities, and Continuity Sets
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Normal Subgroups and Quotient Groups
- Order, Zorn's Lemma, and the Axiom of Choice
- Polynomial Rings, the Division Algorithm and Roots
- Properties of the Integral and the Working FTC
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Sequences and Limits
- Simple Field Extensions and the Construction of the Complex Numbers
- Suprema and Infima
- The Complex Exponential and Euler's Formula
- The Derivative and the Mean Value Theorems
- The Riemann Integral: Definition and Integrability
- The Total Derivative in ℝᵐ → ℝⁿ
- The ZFC Axioms and the Basic Set Constructions
- Topological Spaces and Continuity
- Topology of ℝ
- Vector Spaces, Linear Subspaces, Span and Direct Sums
2 · Summary
The worked example computes an explicit real-coordinate map and affine segment, checks a real total derivative, and follows a finite complex path through its coordinate length, a pause, a reversal, and the singleton-interval convention. It also verifies a continuous bounded complex path whose polygonal sums are unbounded, so bounded trace does not suffice for rectifiability.
3 · Logical flowchart
4 · Definitions, theorems and proofs
None yet.
5 · Examples, counterexamples and false statements
A finite coordinate path and a bounded nonrectifiable path
Example
Let , take , , , and . On , define the continuous path
It travels one unit horizontally, one unit vertically, then pauses. Compare its length with its coordinate path under both a decreasing reversal and a nondecreasing reparametrization with a pause. Also compare the coordinates of and , the distance between , the image of the ball , and the real total derivative of conjugation .
For the bounded-trace caveat, define a second real-valued complex path . For let , , , and . Put , and for set
For outside all , put . Each real value is read as its canonical image in .
Facts & Assumptions
Given: The displayed complex numbers, real parameters, functions, and intervals, including the path defined in the example.
The complex coordinate map preserves real scalar multiplication: and preserves real affine combinations.
The complex coordinate isometry transports topology and affine segments: preserves all distances and maps metric balls to the corresponding Euclidean balls.
Real total derivatives transport through the complex coordinate isometry: A real-linear first-order approximation in complex coordinates transports to the Euclidean total derivative by conjugating with .
Polygonal length and rectifiability of complex paths: A path is continuous from the usual real metric to ; singleton paths have length zero.
Complex path length equals coordinate length and piecewise speed integral: Complex path length equals coordinate length, rectifiability is equivalent to coordinate bounded variation, and piecewise- length is the sum of Euclidean speed integrals.
Complex path length is invariant under monotone surjective reparametrization: Continuous surjective monotone reparametrizations preserve complex length, including pauses, reversal, and singleton intervals.
Real and imaginary parts, complex conjugation, and modulus: If , then and .
The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement and Open ball, closed ball and sphere in a metric space: The whole metric space is open, and for .
Continuity of a map between metric spaces, at a point and globally, in the - form, The Euclidean metric, convergence, Cauchy sequences, and continuity on the complex plane, The absolute value makes a metric space: is a metric, its open balls are the intervals , and it is unbounded, and Intervals of : the nine order-convex forms, nondegeneracy, and length: Continuity is the metric - condition on the indicated interval subspaces; the real and complex distances are absolute difference and modulus difference.
The complex numbers as , with the real embedding and imaginary unit , Real and imaginary parts, complex conjugation, and modulus, Absolute value in an ordered field, Basic properties of the absolute value, and Square roots exist: a unique with ; the positives are : Real values embed as ; the complex modulus of a real difference is the square root of its square, which equals the real absolute value.
The natural numbers (von Neumann), Canonical naturals are positive and strictly increasing, Inverses of positives are positive, and reciprocation reverses order, and Every complete ordered field is Archimedean: Natural indices have positive real images, reciprocals of positive reals reverse order, and can be chosen so is arbitrarily small.
Finite sums and finite products, by recursion and Laws of finite sums and finite products: Prefix sums satisfy and ; they are additive, obey constant-sum scaling, and are monotone under termwise inequalities.
Addition of natural numbers, Order on the natural numbers, Order is compatible with addition, Left identity for addition, is a linear order on , The recursion theorem, and The principle of mathematical induction: Natural addition and order are compatible, , the natural order is transitive and total, recursion supplies the sequence below, and induction verifies properties of all its terms.
Verification
The coordinates are and . Since , by [F1]. Also , whose coordinates are by [F1] and [F2].
We have , so . The Euclidean distance between and is the same , and [F2] gives .
The domain is open by [F8]. For , conjugation has coordinates , the matrix map . If and , then and , so is real-linear. For any , [F1] and [F7] give , so its remainder is zero. The quotient is therefore zero for every , and [F3] gives .
The formulas agree at and . On the first and second pieces the distance between values at and equals , because their differences are respectively real and purely imaginary and the modulus formulas in [F7] and [F10] give this equality; on the constant third piece it is zero. Thus each restriction is continuous. At either breakpoint , take . Then every with lies in the adjacent pieces, where on a moving piece and is zero on the constant piece; hence the distance is less than . At 0 and 3 continuity follows from the corresponding endpoint of the continuous first and last restrictions. Thus is continuous by [F9]. Its coordinate functions are on and on , and on , on , and on .
Let send to . By [F4], and is rectifiable. The constant surjection also satisfies [F6], and both sides of its length equality are zero.
For every , , and by [F11]. Thus the intervals are disjoint, the two formulas for agree at , and their endpoint values are zero. Each interpolation factor lies in , so on ; outside them . Hence is well-defined and its trace is contained in .
Fix and choose with by [F11]. For , , so those intervals lie below ; only finitely many intervals meet . There is zero or one of finitely many affine pieces; the formulas agree at each midpoint and vanish at the interval endpoints, so their one-sided limits agree at every join. Thus is continuous at . At , given choose with . If lies in , then , so and ; outside the intervals . These real-distance bounds are also the bounds under the canonical embedding by [F10]. Hence is continuous as a complex path at and at every positive .
For , the increasing list is a partition of , since for . On each , the path values at are , so its two chord lengths sum to by [F10]; across each gap the chord length is zero. Define , also for . By the prefix recursion, and . Adding the spike contributions gives : this holds at , and inserting the next spike adds , proving it by induction.
By recursion [F13], define natural numbers and . For every natural , the definition of natural order with witness , together with [F13], gives ; compatibility of order with addition then gives . The base is . If , transitivity with gives , so induction [F13] yields for every .
Both coordinates are nondecreasing, with endpoint increments and . For any partition, each absolute coordinate increment equals the nonnegative increment, and the finite sum telescopes to the endpoint increment; the endpoint partition attains . Thus each coordinate has variation exactly . On the three pieces the coordinate velocities are , , and , so the speed integrals are , , and . Therefore the coordinate path has length , and [F5] gives and rectifiability.
For each , put and . For , the positive denominator satisfies in the canonical real images by [F11, F13]. Thus each summand is at least . Monotonicity and constant-sum scaling in [F12] give , since by step 1.9.
Step 2.1 gives . The map on is a continuous decreasing surjection, so [F6] gives . Define by on , on , and on . Its pieces agree at their endpoints; it is continuous and nondecreasing, and its range is . Thus it is a surjection with a pause, and [F6] gives .
Fix a natural . The prefix recursions in [F12] and step 1.8 give by induction on : at both sides equal , and the successor adds to both sides. Taking gives with no natural subtraction or lower-index sum. Since , step 2.2 and induction give for all . The Archimedean property [F11] makes these lower bounds unbounded, so the harmonic partial sums are unbounded.
The partition sums are unbounded by steps 1.8 and 3.2. Hence the partition sums of have no real upper bound, so is not rectifiable by [F4], although its trace is bounded by step 1.6.