OAI/Analysis/CircleDomains/Probability/SelectableMeanLaw.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The recursive positive-law alternative constructs a selectable mean coordinate with its concrete presentation. Finite compatibility is derived from the preceding law estimates, while preserving the coordinate’s Stokes budget and exclusion.

  1. theorem OAI.CircleDomainRigidity.RecursiveCodeLaw.selectable_mean_coordinate line 21