OAI/Analysis/CircleDomains/Topology/FiniteCircleChartIntersections.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Two branch cuts cover a smooth circle coordinate. Each branch has the intrinsic differential, so scalar coarea gives a finite expected intersection count without a global real lift.

  1. theorem OAI.CircleDomainRigidity.mean_circle_chart_count_finite line 23