ConditionalMain.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Conditional nonuniqueness for the periodic hard-sphere Boltzmann equation

All mathematical inputs from earlier publications are explicit arguments. NonuniquenessStatement includes bounded velocity support and two distinct global admissible renormalized solutions with strong initial continuity.

theorem OAI.BoltzmannNonuniqueness.nonuniqueness_conditional line 19