# Iitaka subadditivity, variation, and logarithmic additivity

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

- [The reverse logarithmic Kodaira inequality and additivity](../../preprints/The-reverse-logarithmic-Kodaira-inequality-and-additivity-September-26-2026/paper.pdf)

## Scope

The paper studies logarithmic Kodaira additivity for connected-fiber morphisms of smooth projective reduced simple-normal-crossing pairs that are smooth on all boundary strata away from the base boundary. The linked formalization proves the negative-fiber branch: for a very general base point, if the logarithmic Kodaira dimension of the fiber is $-\infty$, then the total logarithmic Kodaira dimension equals the sum of the base and fiber dimensions and is $-\infty$. Every positive-degree logarithmic pluriform section on the total space then vanishes.

The finite-dimension and negative-base branches of the paper's additivity theorem are outside this selected statement.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Logarithmic Kodaira additivity in the negative-fiber branch | [LogKodairaFiberNegative.lean](../ComparatorChallenges/LogKodairaFiberNegative.lean) |