OAI/Analysis/CircleDomains/Rigidity/MeanCircleLevelTrace.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite physical length gives the topology of a prior level union. The actual mean-index payment then makes its free component traces null.

  1. theorem OAI.CircleDomainRigidity.mean_circle_null_component_traces line 21