Access from a fresh anchor, for thm:finite-transfer(b)

Direction (b) of thm:finite-transfer transfers a target refinement back to the source. Every step of its induction is the same as direction (a)'s except one: when the target ear starts at a point of S, that point is by hypothesis a fresh image u(a) of an anchor a ∈ 𝒜, and the source endpoint a lies on the wild curve C, where no polygonal skeleton reaches it and lem:polygonal-side-accessibility says nothing. The blueprint's paragraph is:

The union K of all old closed nonboundary edges and the finitely many source ears already inserted is compact and does not contain a. By lem:tangent-cone, a tangent disk at a contains an open cone of access segments. By lem:compact-separation(c), shrink that cone until it misses K. Its punctured part is connected, lies in the complement of the current skeleton, and accumulates at a; therefore it lies in the unique current source 2-cell just identified. It supplies the required access arc.

That paragraph is proved here, end to end, as Schoenflies.polyAccessible_of_stronglyAccessible.

The three facts about the cone that the paragraph needs

Schoenflies.accessCone is on main (Schoenflies/Accessible.lean) with its openness, its truncation, and StronglyAccessible.exists_cone — a cone of any radius below the radius of the tangent disk lies in the domain, which is exactly the shrinking the paragraph performs. What was missing is the three properties that make it usable as the connected set of lem:cellulation-invariants(i):

• it is convex, hence preconnected (convex_accessCone, isPreconnected_accessCone) — the condition ‖x - p‖/2 < ⟪v, x - p⟫ is the superlevel set of a concave function and the truncation is a ball;
• the apex is in its closure (mem_closure_accessCone) — this is "accumulates at a", and it is what identifies the cell;
• it contains a straight access segment from the apex (polyAccessible_accessCone), which is Schoenflies.PolyAccessible in the shape lem:accessible-endpoints consumes.

Note that no puncturing is needed: Schoenflies.notMem_accessCone says the apex is not in the cone to begin with, so the blueprint's "its punctured part" is the cone itself.

Which 2-cell, and why that is a hypothesis

"Therefore it lies in the unique current source 2-cell just identified" has two halves. That the cone lies in some 2-cell is proved here, from Schoenflies.CellsAbsorb — the same single hypothesis Schoenflies/SkeletonAccess.lean carries, discharged by Schoenflies.cellsAbsorb_of_isComponent or .cellsAbsorb_of_isComponent_in — together with a covering clause. That the cell is the prescribed one is the separate combinatorial paragraph of the blueprint ("each of the resulting outer subedges is incident with exactly one source 2-cell … hence exactly one descendant 2-cell remains incident with a"), an induction over the ear sequence, and it enters here as the hypothesis hunique: the only cell whose closure contains a is F. That is a statement about the ear induction, not about the geometry of the cone, and the induction is what will discharge it.

Blueprint

• Schoenflies.convex_accessCone, Schoenflies.isPreconnected_accessCone, Schoenflies.mem_closure_accessCone, Schoenflies.polyAccessible_accessCone — the three properties of the cone of lem:tangent-cone that thm:finite-transfer(b) uses.
• Schoenflies.exists_accessCone_disjoint — "by lem:compact-separation(c), shrink that cone until it misses K", combining lem:tangent-cone with lem:compact-separation(c).
• Schoenflies.accessCone_subset_cell — "its punctured part is connected, lies in the complement of the current skeleton, and accumulates at a; therefore it lies in the unique current source 2-cell", from lem:cellulation-invariants(i) in the CellsAbsorb reading.
• Schoenflies.CellsAbsorbIn, Schoenflies.accessCone_subset_cell_in — the domain-restricted form actually used in direction (b): the access cone already lies in the Jordan domain, so absorption is needed only for connected subsets of that domain.
• Schoenflies.polyAccessible_of_stronglyAccessible — the whole paragraph: a strongly accessible point of the wild curve is polygonally accessible from the current source 2-cell incident with it. This is the one input direction (b) needs beyond direction (a).
• Schoenflies.polyAccessible_of_stronglyAccessible_in — the same conclusion from the domain-restricted absorption interface.

The cone is convex

accessCone p v s is cut out of the ball B(p, s) by ‖x - p‖/2 < ⟪v, x - p⟫. Both halves are convex — the second because y ↦ ⟪v, y⟫ - ‖y‖/2 is concave — so the cone is, and in particular it is connected, which is what lem:cellulation-invariants(i) asks of it.

theorem Schoenflies.convex_accessCone (p v : Plane) (s : ℝ) : Convex ℝ (accessCone p v s)

The truncated access cone is convex.

theorem Schoenflies.isPreconnected_accessCone (p v : Plane) (s : ℝ) : IsPreconnected (accessCone p v s)

The truncated access cone is preconnected: it is convex.

The cone accumulates at its apex

Schoenflies.notMem_accessCone says the apex is not a point of the cone; this says it is a limit of points of it. That is the blueprint's "accumulates at a", and it is what turns "the cone lies in some 2-cell" into "the cone lies in a 2-cell incident with a".

theorem Schoenflies.mem_closure_accessCone {p v : Plane} {s : ℝ} (hv : ‖v‖ = 1) (hs : 0 < s) : p ∈ closure (accessCone p v s)

The apex lies in the closure of its own access cone.

theorem Schoenflies.polyAccessible_accessCone {N : Set Plane} {p v : Plane} {s : ℝ} (hv : ‖v‖ = 1) (hs : 0 < s) (hsub : accessCone p v s ⊆ N) : PolyAccessible N p

The straight access segment. The cone contains an open segment leaving the apex, so the apex is polygonally accessible from anything containing the cone. This is PolyAccessible in the shape lem:accessible-endpoints consumes.

Shrinking the cone off the compact part already built

theorem Schoenflies.exists_accessCone_disjoint {D K : Set Plane} {a : Plane} (h : StronglyAccessible D a) (hK : IsCompact K) (ha : a ∉ K) : ∃ (v : Plane) (s : ℝ), ‖v‖ = 1 ∧ 0 < s ∧ accessCone a v s ⊆ D ∧ Disjoint (accessCone a v s) K

"Shrink that cone until it misses K." A strongly accessible point off a compact set has an access cone into the domain that is disjoint from that set. lem:tangent-cone supplies the cone and lem:compact-separation(c) the radius.

Which cell the cone lies in

def Schoenflies.CellsAbsorbIn (D K : Set Plane) (cells : Set (Set Plane)) : Prop

Absorption by cells for connected sets already known to lie in an ambient domain. This is the precise form needed for a tangent cone inside a Jordan domain when K contains only the closed nonboundary edges and not the wild boundary itself.

Equations

• Schoenflies.CellsAbsorbIn D K cells = ∀ N ⊆ D, IsPreconnected N → Disjoint N K → ∀ R ∈ cells, (N ∩ R).Nonempty → N ⊆ R

theorem Schoenflies.CellsAbsorb.cellsAbsorbIn {D K : Set Plane} {cells : Set (Set Plane)} (h : CellsAbsorb K cells) : CellsAbsorbIn D K cells

Global absorption implies its domain-restricted form.

theorem Schoenflies.accessCone_subset_cell {D K F : Set Plane} {cells : Set (Set Plane)} {v a : Plane} {s : ℝ} (habs : CellsAbsorb K cells) (hcover : ∀ x ∈ D, x ∉ K → ∃ R ∈ cells, x ∈ R) (hunique : ∀ R ∈ cells, a ∈ closure R → R = F) (hv : ‖v‖ = 1) (hs : 0 < s) (hD : accessCone a v s ⊆ D) (hdisj : Disjoint (accessCone a v s) K) : accessCone a v s ⊆ F

"Therefore it lies in the unique current source 2-cell just identified." A connected set disjoint from the current skeleton, contained in a region the cells cover, lies in a single cell; the closure clause then names it.

hcover is the covering half of lem:cellulation-invariants(i) — every point of the region off the skeleton is in an open cell — and habs is the absorption half, Schoenflies.CellsAbsorb. hunique is the combinatorial paragraph of thm:finite-transfer(b), not a geometric fact: it says that exactly one current 2-cell is incident with a.

theorem Schoenflies.accessCone_subset_cell_in {D K F : Set Plane} {cells : Set (Set Plane)} {v a : Plane} {s : ℝ} (habs : CellsAbsorbIn D K cells) (hcover : ∀ x ∈ D, x ∉ K → ∃ R ∈ cells, x ∈ R) (hunique : ∀ R ∈ cells, a ∈ closure R → R = F) (hv : ‖v‖ = 1) (hs : 0 < s) (hD : accessCone a v s ⊆ D) (hdisj : Disjoint (accessCone a v s) K) : accessCone a v s ⊆ F

The unique-cell argument with absorption required only inside the ambient domain.

The paragraph

theorem Schoenflies.polyAccessible_of_stronglyAccessible {D K F : Set Plane} {cells : Set (Set Plane)} {a : Plane} (h : StronglyAccessible D a) (hK : IsCompact K) (ha : a ∉ K) (habs : CellsAbsorb K cells) (hcover : ∀ x ∈ D, x ∉ K → ∃ R ∈ cells, x ∈ R) (hunique : ∀ R ∈ cells, a ∈ closure R → R = F) : PolyAccessible F a

The source access arc at a fresh anchor — the one input thm:finite-transfer(b) needs beyond direction (a).

A strongly accessible point a of the wild curve, off the compact set K of everything already drawn, is polygonally accessible from the current source 2-cell F incident with it. Compare lem:polygonal-side-accessibility, which does the same job at every point off C and is useless here precisely because a ∈ C.

lem:accessible-endpoints (Schoenflies.exists_crosscut_of_polyAccessible) turns this, together with the accessibility of the other endpoint, into the polygonal crosscut the ear needs.

theorem Schoenflies.polyAccessible_of_stronglyAccessible_in {D K F : Set Plane} {cells : Set (Set Plane)} {a : Plane} (h : StronglyAccessible D a) (hK : IsCompact K) (ha : a ∉ K) (habs : CellsAbsorbIn D K cells) (hcover : ∀ x ∈ D, x ∉ K → ∃ R ∈ cells, x ∈ R) (hunique : ∀ R ∈ cells, a ∈ closure R → R = F) : PolyAccessible F a

The fresh-anchor paragraph with the absorption invariant stated only inside the Jordan domain, where the tangent cone is already known to lie.