$$
% ============================================
% 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
% LaTeX-only styling (packages, layout, end marks) lives in preamble-pdf.tex
% and is loaded only by the PDF export pipeline.
$$
Weight bound
Among the higher coverings \(\Cov_r(S)\) E0007, the partitions \(\Part_r(S)\) are precisely those of minimal weight, with weight equal to \(|S|\).
(1) Lemma. For any covering \(H \in \Cov_r(S)\) with \(r \geq 1\),
\(\mathrm{wt}(H) \geq |S|\), with equality if and only if
\(H \in \Part_r(S)\).
Proof.
Ad \(r = 1\)) \(\Cov_1(S) = \Part_1(S) = \set{S}\) and
\(\mathrm{wt}(S) = |S|\).
Ad \(r = 2\)) \(\mathrm{wt}(H) = \sum_{T \in H} |T| \geq
|\bigcup H| = |S|\), with equality iff the blocks are pairwise
disjoint.
Ad \(r \geq 3\)) Each \(K \in H\) lies in \(\Cov_{r-1}(\lf(K))\),
since \(K \in \KP_+^{r-1}(\lf(K))\) by recursion on levels.
By induction,
\(\mathrm{wt}(H) = \sum_{K \in H} \mathrm{wt}(K) \geq
\sum_{K \in H} |\lf(K)| \geq |S|\), with equality iff each
\(K \in \Part_{r-1}(\lf(K))\) and the leaf supports partition \(S\).
In the equality case \(K \mapsto \lf(K)\) is injective (the
\(\lf(K)\) are nonempty and disjoint), so \(H\) matches the
recursion defining \(\Part_r\) E0007; conversely each
\(H_B \in \Part_{r-1}(B)\) has \(\lf(H_B) = B\).
Used by:
Lean formalization (source)
import Elements.E0001
/-!
# Weight bound (E0008)
Formalises `Lem:weight-bound` from
*Discrete Faà di Bruno via Möbius Inversion* (Hartmann, 2026).
The weight bound says `|S| ≤ wt(C) = ∑_{A∈C} |A|` for any cover C of S.
-/
open Finset
namespace Elements
variable {α : Type*} [DecidableEq α]
/-! ### Weight bound for coverings -/
/-- **Weight bound** (`Lem:weight-bound`).
For a cover C of S, `|S| ≤ ∑_{A ∈ C} |A|`.
This is the subadditivity of cardinality: `|⋃ C| ≤ ∑ |A|`. -/
lemma weight_bound {S : Finset α} {C : Finset (Finset α)}
(hC : C ∈ coverings S) : S.card ≤ ∑ A ∈ C, A.card := by
-- coverings S = (powPlus S).powerset.filter (fun C => C.biUnion id = S)
simp only [coverings, Finset.mem_filter] at hC
rw [← hC.2]
exact Finset.card_biUnion_le
/-- If a cover has at most `e` blocks each of size at most `d`,
then `|S| ≤ e * d`. -/
lemma cover_size_bound {S : Finset α} {C : Finset (Finset α)}
(hC : C ∈ coverings S) {e d : ℕ}
(he : C.card ≤ e) (hd : ∀ A ∈ C, A.card ≤ d) :
S.card ≤ e * d :=
calc S.card ≤ ∑ A ∈ C, A.card := weight_bound hC
_ ≤ C.card * d := Finset.sum_le_card_nsmul C _ d hd
_ ≤ e * d := Nat.mul_le_mul_right d he
end Elements