Eval representatives and normal-form indices

The Lean-Eval challenge owns Complex.ClosedUnitDisc, OrientableRel, and NonOrientableRel; they are imported verbatim from LeanEval/ChallengeDeps.lean. This file adds only the project-owned sphere abbreviation and the index type used by the normal-form reduction.

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.SphereRepresentative : Type

The sphere branch in the eval theorem.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.SphereRepresentative = ↑(Metric.sphere 0 1)

inductive LeanEval.Topology.ClassificationOfSurfaces.NormalForm : Type

The named normal forms that should eventually be realized by quotient spaces.

• sphere : NormalForm
• orientable (handles boundaryComponents : ℕ) : NormalForm
• nonOrientable (crosscaps boundaryComponents : ℕ) : NormalForm

def LeanEval.Topology.ClassificationOfSurfaces.instDecidableEqNormalForm.decEq (x✝ x✝¹ : NormalForm) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.instDecidableEqNormalForm : DecidableEq NormalForm

Equations

• LeanEval.Topology.ClassificationOfSurfaces.instDecidableEqNormalForm = LeanEval.Topology.ClassificationOfSurfaces.instDecidableEqNormalForm.decEq

def LeanEval.Topology.ClassificationOfSurfaces.instReprNormalForm.repr : NormalForm → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.instReprNormalForm : Repr NormalForm

Equations

• LeanEval.Topology.ClassificationOfSurfaces.instReprNormalForm = { reprPrec := LeanEval.Topology.ClassificationOfSurfaces.instReprNormalForm.repr }

def LeanEval.Topology.ClassificationOfSurfaces.NormalForm.IsEvalAdmissible : NormalForm → Prop

The normal forms that actually appear in the Lean Eval conclusion.

The orientable sphere is represented by the separate sphere branch, so an orientable polygonal normal form must have a handle or a boundary component; nonorientable forms must have at least one crosscap.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.NormalForm.sphere.IsEvalAdmissible = True
• (LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientable a a_1).IsEvalAdmissible = (1 ≤ a ∨ 1 ≤ a_1)
• (LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientable a a_1).IsEvalAdmissible = (1 ≤ a)