D-Differentiability

A function f: H_tau -> H_tau is D-differentiable if in sector coordinates (u,v) = (a+b, a-b), it decomposes as f(u,v) = (g(u), h(v)). Formalized as SectorFun: a pair (g, h) of sector component maps.

D-Differentiability

Summary

A function f: H_tau -> H_tau is D-differentiable if in sector coordinates (u,v) = (a+b, a-b), it decomposes as f(u,v) = (g(u), h(v)). Formalized as SectorFun: a pair (g, h) of sector component maps.

Statement

%
\label{def:d-differentiability}
A function $f : H_\tau \to H_\tau$
(at a given finite primorial stage)
is \textbf{D-differentiable} at $z \in H_\tau$
if the split-complex difference quotient
\[
    \boxed{%
    f'(z)
    \;:=\;
    \lim_{h \to 0}
    \bigl(f(z + h) - f(z)\bigr) \cdot h^{-1}}
\]
exists as an element of $H_\tau$,
where $h \to 0$ ranges over all $h \in H_\tau$
with $N(h) = h_{\mathrm{re}}^2 - h_{\mathrm{im}}^2 \neq 0$
(so that $h^{-1}$ exists),
and the limit is taken in the ultrametric topology
on $H_\tau$.

A function is \textbf{D-holomorphic} on an open subset $U$
if it is D-differentiable at every point of $U$.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

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

Lean / Formalization Notes

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

Dependencies

• Canonical: I.D20, I.D27

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.