Planar connectivity for the standard configuration #
The fixed configuration used in the main assembly: inside the ball B(0, 8)
we remove the two closed unit disks centered at ±4. The remainder must be
path-connected (this feeds the clopen argument showing Y = X ∖ (K₀ ∪ K₁) is
connected, Anghel–Stan proof of Theorem 7, Step 0a of Rado/PLAN.md).
Also provided: the annuli 1 ≤ |z ∓ 4| ≤ 2 sit inside B(0, 8), and related
trivial inclusions used when instantiating the configuration in a chart.
Metric helpers #
Path-connectivity of products and annuli #
The pieces of the cover and their inclusion in the configuration set #
theorem
Rado.isPathConnected_ball_diff_two_disks :
IsPathConnected (Metric.ball 0 8 \ (Metric.closedBall (-4) 1 ∪ Metric.closedBall 4 1))
The standard punctured configuration: a large ball minus two small closed disks is path-connected.
Non-crossing: the two closed configuration disks are disjoint.
theorem
Rado.config_annuli_subset :
Metric.closedBall (-4) 2 ∪ Metric.closedBall 4 2 ⊆ Metric.ball 0 8
The closed annuli of outer radius 2 around ±4 lie in B(0, 8) and stay
disjoint from each other.