Countermodels and semantic anchors

This file is the executable half of the Definition Faithfulness rules in docs/AUTOFORMALIZATION_GUIDE.md. It must stay in the default build target: if a definition is weakened until junk witnesses satisfy it, something in this file stops compiling (or a negation in this file becomes provable and its positive counterpart does too, which the trivial-closure review catches).

Contents:

• positive anchor: the standard 2-simplex carries a geometric triangulation with one face;
• must-imply anchors are proved at the definition site (GeometricTriangulation.compactSpace, GeometricTriangulation.t2Space, GeometricTriangulation.faces_nonempty);
• non-examples: ℝ and ℚ admit no geometric triangulation;
• vacuity probes: empty face families and one-point vertex types cannot triangulate a nonempty space;
• an executable witness showing why an arbitrary finite triangulation record is not itself a certified cell presentation;
• cell-complex non-examples: an unused dart orbit and disconnected face systems;
• a record of the vacuity failure of the retiring SurfaceTriangulable predicate, kept as documentation of why GeometricTriangulation replaces it.

Positive anchor

theorem LeanEval.Topology.ClassificationOfSurfaces.Countermodels.geometricRealization_single_face : GeometricRealization (Fin 3) {Finset.univ} = stdSimplex ℝ (Fin 3)

The one-face complex on three vertices realizes exactly the standard 2-simplex.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Countermodels.stdSimplexTriangulation : GeometricTriangulation ↑(stdSimplex ℝ (Fin 3))

The standard 2-simplex carries a geometric triangulation with a single face.

Equations

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

Vacuity probes for geometric triangulations

Non-examples

A faithful notion of finite triangulation must fail for non-compact spaces. The previous SurfaceTriangulable predicate passed both of these with the empty triangulation.

Legacy bridge countermodel

FiniteSurfaceTriangulation still has an arbitrary stored realization. This fixture satisfies its current validity record for every universe-0 topological space using Homeomorph.refl, while its two face words are empty. Consequently its cell presentation is neither incidence-valid nor face-edge connected. The faithful Radó theorem does not use this object as its conclusion; it enters only through the explicitly ledgered compatibility bridge.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Countermodels.arbitrarySpaceLegacyTriangulation (S : Type) [TopologicalSpace S] : FiniteSurfaceTriangulation S

Every universe-0 topological space inhabits the legacy triangulation structure.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Countermodels.arbitrarySpaceLegacyTriangulation_homeomorphSurface (S : Type) [TopologicalSpace S] : Nonempty ((arbitrarySpaceLegacyTriangulation S).realization ≃ₜ S)

The arbitrary stored realization makes the legacy topological field hold by reflexivity.

theorem LeanEval.Topology.ClassificationOfSurfaces.Countermodels.arbitrarySpaceLegacyTriangulation_not_isSurfaceValid (S : Type) [TopologicalSpace S] : ¬(arbitrarySpaceLegacyTriangulation S).toCellComplex.IsSurfaceValid

Empty boundary words leave the stored edge orbit unused, so the converted presentation is not incidence-valid.

theorem LeanEval.Topology.ClassificationOfSurfaces.Countermodels.arbitrarySpaceLegacyTriangulation_not_isConnected (S : Type) [TopologicalSpace S] : ¬(arbitrarySpaceLegacyTriangulation S).toCellComplex.IsConnected

The two empty face words have no adjacency path, so the converted presentation is not face-edge connected.

Cell-complex incidence countermodels

def LeanEval.Topology.ClassificationOfSurfaces.Countermodels.unusedDartOrbit : SurfaceCellComplex

A one-face presentation with an edge orbit omitted from every boundary word.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Countermodels.unusedDartOrbit = LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.oneFacePresentation PUnit.{1} []

theorem LeanEval.Topology.ClassificationOfSurfaces.Countermodels.unusedDartOrbit_not_isSurfaceValid : ¬unusedDartOrbit.IsSurfaceValid

Incidence validity rejects an edge orbit with zero boundary occurrences.

def LeanEval.Topology.ClassificationOfSurfaces.Countermodels.disconnectedBoundaryFaces : SurfaceCellComplex

Two otherwise plausible one-edge faces sharing only a stored vertex, but no edge orbit.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Countermodels.disconnectedBoundaryFaces_isSurfaceValid : disconnectedBoundaryFaces.IsSurfaceValid

The disconnected fixture is locally valid: each of its two edge orbits occurs exactly once.

theorem LeanEval.Topology.ClassificationOfSurfaces.Countermodels.disconnectedBoundaryFaces_not_isConnected : ¬disconnectedBoundaryFaces.IsConnected

Face-edge connectedness rejects two face systems even when the stored vertex type is a point.

Vacuity record

The legacy predicate SurfaceTriangulable was satisfied by every topological space via the empty triangulation, because its realization field was arbitrary and unlinked to the combinatorial data. The predicate and the machine-checked vacuity proof were deleted together (per the Definition Faithfulness rules); the proof is preserved in git history on the commit that introduced this file. If you find yourself able to write such a proof for GeometricTriangulation, the definition has been broken.