Registry · Lemma VII.L20 tau-effective formalized

VII.L20 — Crossing Point Uniqueness

Lemniscate L = S¹ ∨ S¹ has exactly one crossing point p₀; π″ is the unique crossing mediator generator.

Book VII Part 1 Ch. 8

Dependency Graph

Depends on (1)

VII.L06

Lean Formalization

Module: TauLib.BookVII.Meta.Saturation

Symbol: Tau.BookVII.Meta.Saturation.crossing_point_uniqueness