$$
% ============================================
% GENERAL / UNIVERSAL
% Used throughout the documentation
% ============================================
% --- Basic Number Systems ---
\newcommand{\IR}{\mathbb{R}} % Real numbers #listed
\newcommand{\IC}{\mathbb{C}} % Complex numbers #listed
\newcommand{\IN}{\mathbb{N}} % Natural numbers #listed
\newcommand{\IZ}{\mathbb{Z}} % Integers #listed
\newcommand{\IQ}{\mathbb{Q}} % Rational numbers #listed
\newcommand{\IA}{\mathbb{A}} % Affine space #listed
\newcommand{\IB}{\mathbb{B}} % Generic field #listed
\newcommand{\ik}{\Bbbk} % Ground field #listed
\newcommand{\ID}{\mathbb{D}} % Generic field #listed
\newcommand{\IF}{\mathbb{F}} % Generic field #listed
\newcommand{\IH}{\mathbb{H}} % Quaternions #listed
\newcommand{\II}{\mathbb{I}} % Generic field #listed
\newcommand{\IL}{\mathbb{L}} % Generic field #listed
\newcommand{\IP}{\mathbb{P}} % Projective space #listed
\newcommand{\IS}{\mathbb{S}} % Sphere #listed
\newcommand{\IT}{\mathbb{T}} % Tensor algebra #listed
\newcommand{\IV}{\mathbb{V}} % Generic vector space #listed
% --- Function Spaces ---
\newcommand{\CINF}{\mathcal{C}^\infty} % Smooth (infinitely differentiable) functions #listed
\newcommand{\CC}{\mathcal{C}} % C^k functions #listed
\newcommand{\Ck}{\mathcal{C}^k} % C^k functions #listed
\newcommand{\CK}{\mathcal{C}^K} % C^k functions #listed
% --- Fundamental Operators ---
\newcommand{\del}{\partial} % Partial derivative #listed
\newcommand{\uDelta}{\underline{\Delta}} % Discrete difference operator #listed
\newcommand{\Shift}{\mathrm{S}_\downarrow} % Shift operator #listed
% --- Logical & Set Operations ---
\newcommand{\IFF}{\Leftrightarrow} % If and only if #listed
\newcommand{\Ind}{\mathbb{1}} % Indicator/characteristic function #listed
\newcommand{\IndA}[1]{\mathbb{1}\lbrace #1 \rbrace} % Indicator with condition #listed
\newcommand{\1}{\mathbb{1}} % Indicator shorthand #listed
\newcommand{\set}[1]{\{#1\}} % Simple set braces #listed
\newcommand{\Set}[2]{\left\{\, #1 \;\vert\; #2 \,\right\}} % Set-builder notation #listed
\newcommand{\CSet}[2]{\#\{\, #1 \;\vert\; #2 \,\right\}} % Cardinality notation #listed
\newcommand{\C}{\,\#} % Cardinality operator #listed
% --- Limits & Categorical ---
\newcommand{\limproj}{\varprojlim} % Inverse limit #listed
\newcommand{\limind}{\varinjlim} % Direct limit #listed
\newcommand{\Hom}{\mathrm{Hom}} % Homomorphism #listed
\newcommand{\End}{\mathrm{End}} % Endomorphism #listed
\newcommand{\Ext}{\mathrm{Ext}} % Ext functor #listed
% --- Arrows & Relations ---
\newcommand{\ra}{\rightarrow} % Right arrow #listed
\newcommand{\lra}{\longrightarrow} % Long right arrow #listed
\newcommand{\xlra}[1]{\overset{#1}{\lra}} % Labeled long arrow #listed
\newcommand{\la}{\leftarrow} % Left arrow #listed
\newcommand{\lla}{\longleftarrow} % Long left arrow #listed
\newcommand{\mono}{\hookrightarrow} % Monomorphism #listed
\newcommand{\epi}{\twoheadrightarrow} % Epimorphism #listed
\newcommand{\isom}{\cong} % Isomorphism #listed
\newcommand{\downto}{\searrow} % Diagonal arrow #listed
% --- Tensor & Algebraic Structures ---
\newcommand{\tensor}{\otimes} % Tensor product #listed
\newcommand{\tensors}{\tensor\dots\tensor} % Multiple tensor products #listed
\newcommand{\Tensor}{\bigotimes} % Big tensor product #listed
\newcommand{\stensor}{\odot} % Symmetric tensor product #listed
\newcommand{\vsum}{\oplus} % Direct sum #listed
\newcommand{\Vsum}{\bigoplus} % Big direct sum #listed
% --- Calligraphic Letters (Generic) ---
\newcommand{\KA}{\mathcal{A}}
\newcommand{\KB}{\mathcal{B}}
\newcommand{\KC}{\mathcal{C}}
\newcommand{\KD}{\mathcal{D}}
\newcommand{\KF}{\mathcal{F}}
\newcommand{\KH}{\mathcal{H}}
\newcommand{\KI}{\mathcal{I}}
\newcommand{\KL}{\mathcal{L}}
\newcommand{\KN}{\mathcal{N}}
\newcommand{\KP}{\mathcal{P}}
\newcommand{\KQ}{\mathcal{Q}}
\newcommand{\KR}{\mathcal{R}}
\newcommand{\KS}{\mathcal{S}}
\newcommand{\KV}{\mathcal{V}}
\newcommand{\KZ}{\mathcal{Z}}
% --- Fraktur Letters (Generic) ---
\newcommand{\gc}{\mathfrak{C}}
\newcommand{\gd}{\mathfrak{D}}
\newcommand{\gM}{\mathfrak{M}}
\newcommand{\gm}{\mathfrak{m}}
\newcommand{\gf}{\mathfrak{f}}
\newcommand{\gu}{\mathfrak{U}}
\newcommand{\fa}{\mathfrak{a}}
\newcommand{\fg}{\mathfrak{g}}
\newcommand{\fn}{\mathfrak{n}}
\newcommand{\fk}{\mathfrak{k}}
\newcommand{\fm}{\mathfrak{m}}
\newcommand{\fp}{\mathfrak{p}}
\newcommand{\fP}{\mathfrak{P}}
% \fg already defined above (line 95) as \mathfrak{g}
% --- Text & Formatting ---
\newcommand{\qtext}[1]{\quad\text{#1}\quad} % Quad spaced text #listed
\newcommand{\stext}[1]{\;\text{#1}\;} % Small spaced text #listed
\newcommand{\ssum}[1]{\sum_{\substack{#1}}} % Sum with substacked condition #listed
\newcommand{\half}{\frac{1}{2}} % One-half #listed
\newcommand{\floor}[1]{\lfloor #1 \rfloor} % Floor function #listed
\newcommand{\ceil}[1]{\lceil #1 \rceil} % Ceiling function #listed
\newcommand{\nl}{\\} % Newline #listed
% --- Common Functions ---
\newcommand{\id}{\mathrm{id}} % Identity function #listed
\newcommand{\len}{\mathrm{len}} % Length of a word #listed
\newcommand{\rk}{\mathrm{rk}} % Rank #listed
\newcommand{\diag}{\operatorname{diag}} % Diagonal matrix #listed
\newcommand{\Res}{\operatorname{Res}} % Residue #listed
\newcommand{\Ker}{\mathrm{Ker}} % Kernel #listed
\newcommand{\Diff}{\mathrm{Diff}} % Diffeomorphism group #listed
\newcommand{\Pic}{\mathrm{Pic}} % Picard group #listed
\newcommand{\Spec}{\mathrm{Spec}} % Spectrum #listed
\newcommand{\D}{\mathrm{D}} % Differential operator #listed
\newcommand{\DP}{\mathrm{D_{\!+}}} % Positive differential #listed
\newcommand{\DDP}{\mathrm{D^{\!+}}} % Upper differential #listed
% --- Variants ---
\newcommand{\vphi}{\varphi} % Variant phi #listed
\newcommand{\sphi}{\phi} % Straight phi #listed
\newcommand{\eps}{\varepsilon} % Epsilon variant #listed
\newcommand{\pt}{*} % Point notation #listed
\newcommand{\point}{*} % Point notation alt #listed
% --- Set Operations ---
\newcommand{\union}{\cup} % Union #listed
\newcommand{\Union}{\bigcup} % Big union #listed
\newcommand{\dotcup}{\ensuremath{\mathaccent\cdot\cup}} % Disjoint union #listed
\newcommand{\dunion}{\dotcup} % Disjoint union alt #listed
% \< and \> removed - conflict with LaTeX tabbing commands and unused in docs
\newcommand{\inpart}[1]{\in\text{\part}(#1)} % In partition of #listed
\newcommand{\trl}{\triangleleft} % Left triangle #listed
\newcommand{\trr}{\triangleright} % Right triangle #listed
% --- Misc ---
\newcommand{\curly}[1]{\mathcal{#1}}
\newcommand{\op}[1]{\mathrm{#1}}
\newcommand{\Cat}[1]{\mathfrak{#1}}
\newcommand{\cat}[1]{\mathbf{#1}}
\newcommand{\CAT}[1]{\left\{\,\text{#1}\,\right\}}
\newcommand{\CATii}[2]{\left\{\,\begin{array}{c}\text{#1}\\\text{#2}\end{array}\,\right\}}
\newcommand{\Mon}{\mathrm{Mon}}
\newcommand{\Lin}{\mathrm{Lin}}
\newcommand{\ev}{\mathrm{ev}}
\newcommand{\tc}{\prec_{\mathrm{tc}}}
\newcommand{\tightlist}{\setlength{\itemsep}{0pt}\setlength{\parskip}{0pt}}
\newcommand{\QED}{\square} % End of proof #listed
\renewcommand{\part}{\vdash} % Turnstile #listed (overrides LaTeX \part sectioning)
\newcommand{\opart}{\models} % Semantic entailment #listed
\newcommand{\Def}{\mathrm{Def}} % Bialgebra defect #listed
% ============================================
% CHAPTER 1: DIFFERENTIAL DUALITY
% ============================================
\newcommand{\Jet}{\mathbf{Jet}} % Jet space of C infinity germs #listed
\newcommand{\jet}{\mathrm{jet}} % Jet functor #listed
\newcommand{\E}{\mathbf{E}} % Space of smooth functions #listed
\newcommand{\EE}{\mathbf{E}} % Space of smooth functions alt #listed
% ============================================
% CHAPTER 2: DISCRETE DUALITY
% ============================================
% --- Multisets and Iterated Structures ---
\newcommand{\KM}{\mathcal{M}} % Multiset / multi-index set #listed
\newcommand{\ualpha}{\underline{\alpha}} % Underline alpha (iterated multi-index) #listed
\newcommand{\ubeta}{\underline{\beta}} % Underline beta (iterated multi-index) #listed
\newcommand{\ugamma}{\underline{\gamma}} % Underline gamma (iterated multi-index) #listed
\newcommand{\uS}{\underline{S}} % Underline S (iterated subset) #listed
\newcommand{\uT}{\underline{T}} % Underline T (iterated subset) #listed
% --- From Affine Cubes ---
\newcommand{\BC}{\mathbf{B}} % Affine Cube space #listed
% --- From Cubes.md and affine cube space ---
\newcommand{\BB}{\mathbb{B}} % Boolean lattice #listed
\newcommand{\minelt}{\hat{0}} % Minimal element #listed
\newcommand{\maxelt}{\hat{1}} % Maximal element #listed
\newcommand{\sleq}{\subseteq} % Subset relation #listed
\newcommand{\drk}{\mathrm{rk_{\Delta}}} % Discrete rank #listed
\newcommand{\Fun}{\operatorname{F}} % Function space #listed
\newcommand{\Cube}{\operatorname{Cube}} % Geometric cubes #listed
\newcommand{\Cu}{\mathrm{Cube}} % Cube spaces (NC calculus); symbol choice revisable #listed
\newcommand{\Fl}{\operatorname{Fl}} % Flow (NC calculus) #listed
\newcommand{\Aff}{\operatorname{Aff}} % Affine cubes #listed
\newcommand{\Exp}{\operatorname{exp}} % Geometric realization (zeta transform) #listed
\newcommand{\Log}{\operatorname{log}} % Tangent logarithm (Möbius transform) #listed
\newcommand{\aprod}{\star} % Anchored product of cubes #listed
\newcommand{\acoprod}{\Delta} % Anchored coproduct of cubes #listed
\newcommand{\tcoprod}{\Delta^\tau} % Transport coproduct of cubes #listed
\newcommand{\tprod}{\star^\tau} % Transport product of cubes #listed
\newcommand{\Part}{\mathrm{Part}} % Partitions of a set #listed
\newcommand{\Cov}{\mathrm{Cov}} % Coverings #listed
\DeclareMathOperator{\lf}{\mathrm{leaf}} % Leaf support #listed
\newcommand{\CT}{\mathbf{CT}} % Covering trees #listed
\newcommand{\BH}{\mathbf{IH}} % Iterated hypergraphs #listed
\newcommand{\IHCov}{\mathbf{IHCov}} % Iterated hypergraph covers #listed
\newcommand{\vac}{{|0\rangle}} % Empty partition #listed
% --- From Filtered Vector Spaces.md ---
\newcommand{\gr}{\mathrm{gr}} % Graded/associated graded object #listed
% ============================================
% CHAPTER 3: ULTRA CALCULUS
% ============================================
\newcommand{\POS}{\mathbf{Pos}} % Growth domain spaces #listed
\newcommand{\U}{\mathbf{U}} % Ultra regulator quotient #listed
\newcommand{\IU}{\mathbb{U}} % Ultra regulator #listed
\newcommand{\IG}{\mathbb{G}} % Growth profile #listed
\newcommand{\Tame}{\mathbf{Tame}} % Tame growth functions #listed
\newcommand{\Scale}{\mathrm{Scale}} % Scaling operator #listed
\newcommand{\Bell}{\mathcal{B}} % Bell polynomials #listed
\newcommand{\uexp}{\exp_+} % Exponential generating series #listed
% --- Ultra Structures ---
\newcommand{\Sym}{\mathbf{S}} % Symmetric functions/algebra #listed
\newcommand{\SYM}{\mathrm{Sym}} % Symmetric algebra, roman #listed
\renewcommand{\SS}{\Sym} % Symmetric functions alt #listed (overrides LaTeX \SS)
\newcommand{\SP}{\Sym^+} % Positive symmetric functions #listed
\newcommand{\SH}{\hat{\Sym}} % Completed symmetric functions #listed
\newcommand{\SPH}{\hat{\Sym}^+} % Completed positive symmetric #listed
% --- Completed tangent/cotangent spaces (DDC paper) ---
\newcommand{\STH}{\hat{S}T} % Completed symmetric cotangent space #listed
\newcommand{\CTH}{\hat{C}T} % Completed co-cube space #listed
% --- Ultra Operators ---
\newcommand{\MIX}{\mathrm{Mix}} % Mixing operator #listed
\newcommand{\BMIX}{\mathrm{BMix}} % Boolean mixing #listed
\newcommand{\TMIX}{\mathrm{TMix}} % Transport mixing #listed
\newcommand{\TBMIX}{\mathrm{TMix}} % Transport boolean mixing #listed
\newcommand{\TRANS}{\mathrm{Trans}} % Transport operator #listed
% --- Gauge & Equivalence ---
\newcommand{\gaugeleq}{\preccurlyeq} % Gauge less-or-equal #listed
\newcommand{\gaugeeq}{\asymp} % Gauge equivalence #listed
\newcommand{\gaugegeq}{\preccurlygeq} % Gauge greater-or-equal #listed
\newcommand{\tstar}{\circledast} % Tight star product #listed
% --- Forward Differences ---
\newcommand{\FD}{\blacktriangle} % Forward difference #listed
\newcommand{\fd}{\FD} % Forward difference alt #listed
\newcommand{\AC}{\square} % Associated character #listed
% ============================================
% OPERATORS (DeclareMathOperator)
% ============================================
\DeclareMathOperator{\Supp}{\mathrm{Supp}} % Support #listed
\DeclareMathOperator{\supp}{\mathrm{Supp}} % Support #listed
\newcommand{\esssupp}{\operatorname*{ess-supp}} % Support #listed
\DeclareMathOperator{\Alt}{\Lambda} % Alternating/exterior #listed
\DeclareMathOperator{\ad}{ad} % Adjoint representation #listed
\DeclareMathOperator{\ch}{ch} % Chern character #listed
\DeclareMathOperator{\td}{td} % Todd class #listed
\DeclareMathOperator{\TD}{TD} % Todd operator #listed
\DeclareMathOperator{\pr}{pr} % Projection #listed
\DeclareMathOperator{\Map}{Map} % Mapping space #listed
\DeclareMathOperator{\Pol}{Pol} % Polarization
% ============================================
% ENVIRONMENT SIDEBARS
% Plain neutral-grey left rule on theorem-like environments,
% marking structure without web-style color coding.
% ============================================
\usepackage{xcolor}
\usepackage[framemethod=TikZ]{mdframed}
\usepackage{booktabs} % pandoc emits \toprule/\midrule/\bottomrule for pipe tables
\definecolor{envRule}{HTML}{666666}
\mdfdefinestyle{envstyle}{%
linewidth=0.8pt,
topline=false,
bottomline=false,
rightline=false,
leftline=true,
leftmargin=-8pt,
rightmargin=0pt,
innerleftmargin=7.2pt,
innerrightmargin=0pt,
innertopmargin=0pt,
innerbottommargin=0pt,
skipabove=1em,
skipbelow=1em,
linecolor=envRule,
}
\surroundwithmdframed[style=envstyle]{theorem}
\surroundwithmdframed[style=envstyle]{proposition}
\surroundwithmdframed[style=envstyle]{lemma}
\surroundwithmdframed[style=envstyle]{corollary}
\surroundwithmdframed[style=envstyle]{definition}
\surroundwithmdframed[style=envstyle]{example}
\surroundwithmdframed[style=envstyle]{remark}
\surroundwithmdframed[style=envstyle]{proof}
$$
Discrete product rule
The forward difference \(\Delta\) E0004 of a product expands over ordered coverings of the direction set, by the same Möbius mechanism as the composition formula E0006.
(1) Theorem. Let \(X\) be an abelian group, \(A\) an associative algebra, and \(f_1,\dots,f_r: X \to A\). For \(x \in X\) and \(u_1,\dots,u_n \in X\):
-
Boolean product rule:
\[ \Delta(f_1 \cdots f_r; x; u_1,\dots,u_n) = \sum_{\substack{J_1,\dots,J_r \subseteq [n] \\ J_1 \cup \cdots \cup J_r = [n]}} \Delta(f_1; x; u_{J_1}) \cdots \Delta(f_r; x; u_{J_r}). \] -
Boolean Taylor product rule:
\[ (f_1 \cdots f_r)(x + {\textstyle\sum_{i=1}^n} u_i) = \sum_{J_1, \dots, J_r \subseteq [n]} \Delta(f_1; x; u_{J_1}) \cdots \Delta(f_r; x; u_{J_r}). \]The sum in the first part runs over all ordered coverings \((J_1,\dots,J_r)\): the \(J_a\) may overlap and empty \(J_a\) are allowed. The second part is the product of Taylor expansions. Binomial versions follow by applying to \(S(\gamma)\).
Proof. By Taylor duality E0005, \(f_a(x + \sum_{i \in S} u_i) = \sum_{J_a \subseteq S} \Delta(f_a; x; u_{J_a})\). Multiplying \(r\) such expansions and substituting into the alternating sum for \(\Delta(f_1 \cdots f_r)\):
\[
\Delta(f_1 \cdots f_r; x; u_\bullet)
=
\sum_{\substack{J_1, \dots, J_r \subseteq [n] \\
S \supseteq J_1 \cup \cdots \cup J_r}}
(-1)^{n-|S|}\,
\Delta(f_1; x; u_{J_1}) \cdots \Delta(f_r; x; u_{J_r}).
\]
For a fixed tuple \((J_1, \dots, J_r)\), set \(M = [n] \setminus (J_1 \cup \cdots \cup J_r)\). The sign sum is \(\sum_{R \subseteq M} (-1)^{|M|-|R|} = (1-1)^{|M|}\): this is \(1\) if \(J_1 \cup \cdots \cup J_r = [n]\) and \(0\) otherwise.
(2) Validation (AI review, 2026-07-19, claude-fable-5, pass).
Both parts; sign collapse via \(S = U \cup R\), \(R \subseteq M\);
edge cases \(n = 0\) (holds, no nonempty hypothesis needed),
\(r = 1\), numeric check \(n = 1\), \(r = 2\); commutativity of \(A\)
correctly not assumed. Trimmed depends_on (E0002 was only a
thematic mention) and linked the existing Lean proofs. No
issues found.
Used by: