OAI/Analysis/CircleDomains/Transfer/AnchoredMeanSourceBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The retained inner mean circuit stays outside the fixed endpoint anchor. Its physical radius is therefore bounded before the final model radius is chosen.

  1. theorem OAI.CircleDomainRigidity.RecursiveMeanOutput.boundary_norm_lt_of_anchor line 19