# Bounded klt complements for Fano contractions

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Uniform Cartier sections for Fano type contractions](../../preprints/Uniform-Cartier-sections-for-Fano-type-contractions-September-25-2026/Uniform-Cartier-sections-for-Fano-type-contractions-September-25-2026.pdf)

## Scope

The paper develops uniform Cartier sections for Fano-type contractions as a step toward bounded klt complements. The linked formalization proves a local compactness result: for positive numbers $a_i$, the chart-field retractions indexed by nonnegative weights satisfying $\sum_i a_iw_i=1$ form a compact set in the pointwise topology on the fraction field.

The chart is built over an algebraically closed field from the localization of a polynomial ring at its origin. Its local domain is Noetherian, essentially of finite type and formally unramified over that localization, and formally étale over the polynomial ring. Uniform Cartier sections, bounded klt complements, and the paper's real-boundary and companion conclusions are outside this supporting statement.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Compactness of normalized chart-field retractions | [CartierChartCompactnessSupport.lean](../ComparatorChallenges/CartierChartCompactnessSupport.lean) |