OAI/Analysis/CircleDomains/Rigidity/PhysicalMaskedBranches.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Nonsingular branches on the actual physical terminal boundaries

The disjointness of terminal and filling caps supplies the untouched boundary condition. The uniform staircase bounds from the physical terminal construction then give the actual filled branches and the square-sum excess estimate on each nonsingular subfamily.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.physical_masked_terminal_branches line 23