OAI/NumberTheory/CubicMoment/Decomposition/StoppingLabelCollection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Exact primary-pair collection on an arbitrary finite stopping-label set. No end-crossing premise is needed for this fixed-label identity.

  1. theorem OAI.CubicFirstMoment.geometric_stopping_label_collection line 13