Split-CR Equations

The split-complex Cauchy-Riemann equations: dU/da = dV/db and dU/db = dV/da. In sector coordinates: dF+/dv = 0 and dF-/du = 0. Formalized as has_split_cr_form predicate.

Split-CR Equations

Summary

The split-complex Cauchy-Riemann equations: dU/da = dV/db and dU/db = dV/da. In sector coordinates: dF+/dv = 0 and dF-/du = 0. Formalized as has_split_cr_form predicate.

Statement

%
\label{def:split-cr-equations}
Let $f : H_\tau \to H_\tau$
be a function written in components as
\[
    f(a + bj) \;=\; U(a, b) + V(a, b) \cdot j,
\]
where $U, V : \hat{\mathbb{Z}}_\tau \times \hat{\mathbb{Z}}_\tau
\to \hat{\mathbb{Z}}_\tau$
are the real and imaginary parts of $f$
(relative to the basis $\{1, j\}$).
The \textbf{split Cauchy--Riemann equations}
(split-CR equations) are:
\[
    \boxed{%
    \frac{\partial U}{\partial a}
    = \frac{\partial V}{\partial b},
    \qquad
    \frac{\partial U}{\partial b}
    = \frac{\partial V}{\partial a}.}
\]

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-01.jsonl line 108
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part13/ch49-d-holomorphy.tex lines 271-293

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Holomorphy.DHolomorphic
• Name: Tau.Holomorphy.has_split_cr_form

Dependencies

• Canonical: I.D42

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.