Sanity checks for the Lean-Eval representatives

The carrier and gluing relations are vendored verbatim in ChallengeDeps.lean. This file proves small project-owned consequences without changing those trusted definitions. In particular, radius is constant across every generating identification, so it descends to both quotient families and distinguishes the disk center from its boundary.

@[simp]

theorem Complex.ClosedUnitDisc.norm_bdyPtOfReal (r : ℝ) : ‖↑(bdyPtOfReal r)‖ = 1

Every point produced by bdyPtOfReal lies on the unit circle.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.orientableQuotRadius (p n : ℕ) : Quot (OrientableRel p n) → ℝ

Radius descends through every orientable boundary identification.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.orientableQuotRadius p n = Quot.lift (fun (z : Complex.ClosedUnitDisc) => ‖↑z‖) ⋯

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.nonOrientableQuotRadius (p n : ℕ) : Quot (NonOrientableRel p n) → ℝ

Radius descends through every non-orientable boundary identification.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.nonOrientableQuotRadius p n = Quot.lift (fun (z : Complex.ClosedUnitDisc) => ‖↑z‖) ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.not_subsingleton_orientableQuot (p n : ℕ) : ¬Subsingleton (Quot (OrientableRel p n))

No orientable representative collapses to a point: the disk center and boundary have different radii in the quotient.

theorem LeanEval.Topology.ClassificationOfSurfaces.not_subsingleton_nonOrientableQuot (p n : ℕ) : ¬Subsingleton (Quot (NonOrientableRel p n))

No non-orientable representative collapses to a point.