Foundational corpus mapping FC02 Munkres

Foundational corpus mapping FC02 Munkres

Foundational corpus mapping FC02 Munkres

Foundational corpus mapping FC02 Munkres

Foundational corpus mapping FC02 Munkres

Foundational corpus mapping FC02 Munkres

Foundational corpus mapping FC02 Munkres

FC02 — Munkres mapping

Status: Sweep II complete for FC02. All 844 canonical units C01–C14 are audited below.

Per-row provenance codes

• P: pinned Mathlib db584cd6d46c92f209a44c0f1c829460d327499d (v4.33.0), current upstream 4cbb42e75a050e830b7cf0f2ae748d7644f59cf7 rechecked 2026-09-05; Apache-2.0.
• N: project + pinned/current Mathlib + Loogle/LeanSearch + Reservoir/GitHub Lean + source-atlas negative search, 2026-09-05.
• J, I, R: project-existing, package-import, reference-port respectively; any such row retains its exact target/license details in the route/target/comparison fields.

Provenance contract for C01

• Project search: LeanCategories/** outside .lake was searched before external reuse; no project-owned replacement for Munkres §§1–11 was found. LeanCategories/Foundation/Sets.lean packages finite/countable categories but does not own the textbook C01 statements.
• Pinned Mathlib: repository pin db584cd6d46c92f209a44c0f1c829460d327499d (v4.33.0) was searched and declaration-level interfaces were checked for sets, relations, functions, finite/countable types, orders, ordinals, choice, recursion, and Zorn.
• Current Mathlib: current default branch rechecked 2026-09-05; the latest inspected commit was 251e86bd1fa42024826ccdb46c3d680edff03e1f. Open PR #41962 packages the ω₁ counterexample space but is not needed for the C01 order-theoretic mapping because the pinned library already contains the required ω₁/regularity declarations.
• External Lean search: GitHub/Lean ecosystem searches found mdnestor/basic_topology@10230d7997436e8be1644d0750ec6b03d845619b, but its Munkres sequence begins at §12 and therefore supplies no C01 owner; the repository also exposes no license file, so it would not be a reference-port source in any case. Exercise-solution repositories were not credited because the frozen corpus explicitly excludes exercises.
• Search-service cross-checks: Loogle and LeanSearch were queried for countability/union and adjacent foundational interfaces; LeanSearch returned Set.Countable.sUnion and Set.countable_iUnion.
• exact match means the assertion/interface is present up to harmless notation or a canonical reindexing; broad match means the mathematics exists in a more structural/native interface; partial match / wrong interface means a substantive packaging or semantic clause differs; unmatched after search is scoped to the searches above.
• Mathlib/Lean code is Apache-2.0. No external C01 package was credited.

C01 — Set Theory and Logic

FC02 ID	Verdict	Route	Lean target(s)	Provenance	Interface comparison
FC02-C01-U001	broad match	mathlib	Set α := α → Prop; membership notation x ∈ s	P	Membership is native to Lean’s set-as-predicate representation; this matches the source notation but not a ZF membership primitive.
FC02-C01-U002	exact match	mathlib	Set.ext; Set.ext_iff	P	Exact extensional equality criterion for sets.
FC02-C01-U003	exact match	mathlib	Set.Subset; set order ≤; strict subset <	P	Subset and proper-subset relations are native on Set α.
FC02-C01-U004	broad match	mathlib	Set.ofPred; Set.singleton; insert; finite-set notation	P	Set-builder and finite listing syntax are available; finite listings are notation over insert/singleton rather than a separate construction.
FC02-C01-U005	exact match	mathlib	set union s ∪ t; Set.union_def	P	Exact union-by-membership definition.
FC02-C01-U006	broad match	mathlib	proposition constructor Or	P	Lean’s logical disjunction is the inclusive mathematical ‘or’.
FC02-C01-U007	exact match	mathlib	set intersection s ∩ t; Set.inter_def	P	Exact intersection-by-membership definition.
FC02-C01-U008	exact match	mathlib	(∅ : Set α); Set.notMem_empty	P	Exact empty set.
FC02-C01-U009	exact match	mathlib	Disjoint; Set.disjoint_iff_inter_eq_empty	P	Exact equivalence between disjointness and empty intersection.
FC02-C01-U010	broad match	mathlib	function type on propositions P → Q	P	Implication is primitive logical syntax with the same truth condition.
FC02-C01-U011	broad match	mathlib	implication from False; False.elim	P	Vacuous implication is built into Lean’s implication semantics rather than named as a separate theorem.
FC02-C01-U012	exact match	mathlib	Set.empty_subset	P	Exact theorem that the empty set is a subset of every set.
FC02-C01-U013	exact match	mathlib	mt	P	mt is the contrapositive rule (P → Q) → (¬Q → ¬P).
FC02-C01-U014	broad match	mathlib	mt; classical propositional reasoning (Classical.em)	P	One direction is mt; equivalence with the converse contrapositive uses classical logic, available globally but not packaged as this textbook sentence.
FC02-C01-U015	broad match	mathlib	proposition implication with arguments swapped	P	The converse is simply Q → P; the source is terminology rather than a separate library object.
FC02-C01-U016	exact match	mathlib	Iff / notation P ↔︎ Q	P	Lean’s biconditional is exactly a pair of implications.
FC02-C01-U017	broad match	mathlib	Not; universal binder ∀; existential binder ∃	P	Negation and the two quantifiers are primitive logical syntax.
FC02-C01-U018	exact match	mathlib	not_exists; classical not_forall/Classical.not_forall	P	Exact quantifier-negation rules in classical logic.
FC02-C01-U019	exact match	mathlib	Set.sdiff_eq; Set.mem_sdiff	P	Exact relative complement/set-difference definition.
FC02-C01-U020	exact match	mathlib	set distributive lattice laws, e.g. inter_union_distrib_left, union_inter_distrib_left	P	Exact distributive identities.
FC02-C01-U021	exact match	mathlib	Boolean-algebra laws on Set α; Set.sdiff_eq	P	De Morgan laws are generic Boolean-algebra identities specialized to sets.
FC02-C01-U022	exact match	mathlib	Set.powerset; notation 𝒫 A	P	Exact power-set construction.
FC02-C01-U023	broad match	mathlib	Set (Set α)	P	A collection of sets is represented directly as a set whose elements are sets.
FC02-C01-U024	broad match	mathlib	Set.singleton; powerset membership	P	Lean’s types enforce the distinction between an element, its singleton, and the singleton as an element of a powerset.
FC02-C01-U025	exact match	mathlib	Set.sUnion; Set.mem_sUnion	P	Exact union of an arbitrary collection of sets.
FC02-C01-U026	exact match	mathlib	Set.sInter; Set.mem_sInter	P	For a nonempty collection, this is exactly the source intersection.
FC02-C01-U027	partial match / wrong interface	mathlib	Set.sUnion_empty; Set.sInter_empty	P	Mathlib agrees that the empty union is empty, but because Set α fixes an ambient universe it defines the empty intersection as univ; Munkres deliberately leaves that intersection undefined absent a fixed universe.
FC02-C01-U028	exact match	mathlib	Set.prod; notation s ×ˢ t; also ZFSet.prod	P	Exact Cartesian product, both for ordinary typed sets and in Mathlib’s internal ZFC model.
FC02-C01-U029	exact match	mathlib	ZFSet.pair; ZFSet.coe_pair; ZFSet.pair_inj	P	Mathlib’s ZFC model uses exactly the Kuratowski ordered pair {{x},{x,y}} and proves injectivity.
FC02-C01-U030	broad match	mathlib	ordinary pair notation (a,b); Prod; ZFSet.pair	P	Both typed and Kuratowski ordered pairs are available, but Munkres’s typography convention a × b is source-local.
FC02-C01-U031	exact match	mathlib	SetRel α β := Set (α × β); Relator.RightUnique	P	A rule of assignment is exactly a relation/set of pairs that is right-unique.
FC02-C01-U032	exact match	mathlib	SetRel.dom; SetRel.cod	P	Exact first-coordinate domain and second-coordinate image/range of a relation.
FC02-C01-U033	broad match	mathlib	typed functions A → B; Function.graph; Set.range	P	Lean packages totality and the chosen codomain into the function type, while the graph and actual image are derived.
FC02-C01-U034	broad match	mathlib	function application f a	P	Function value/image of a point is primitive syntax.
FC02-C01-U035	exact match	mathlib	Set.domRestrict / restriction along a subtype inclusion	P	Exact restriction of a function to a subset/subtype while retaining codomain.
FC02-C01-U036	unmatched after search	unmatched	—	N	No searched proved declaration packages Munkres’s four square-function variants and their injectivity/surjectivity behavior as this concrete example.
FC02-C01-U037	exact match	mathlib	Function.comp; notation g ∘ f	P	Exact function composition.
FC02-C01-U038	unmatched after search	unmatched	—	N	No searched Lean declaration records the concrete composite g(f(x)) = 5(3x²+2) as a reusable theorem; generic composition does not count as the example.
FC02-C01-U039	exact match	mathlib	Function.Injective; Function.Surjective; Function.Bijective	P	Exact predicates.
FC02-C01-U040	broad match	mathlib	Equiv.ofBijective; Equiv.symm; Function.invFun	P	A bijection is upgraded to an equivalence with an inverse; arbitrary-function inverse notation is not source-identical.
FC02-C01-U041	unmatched after search	unmatched	—	N	No searched proved declaration packages the concrete x ↦ x² domain/codomain variants and square-root inverse example.
FC02-C01-U042	exact match	mathlib	Function.bijective_iff_has_inverse; left/right-inverse uniqueness lemmas	P	Exact content: simultaneous left and right inverses force bijectivity and coincide with the inverse.
FC02-C01-U043	exact match	mathlib	Set.image; Set.preimage	P	Exact image of a subset and inverse image of a subset.
FC02-C01-U044	exact match	mathlib	Set.preimage / notation f ⁻¹' B₀	P	Exact preimage definition and notation.
FC02-C01-U045	unmatched after search	unmatched	—	N	No searched proved declaration records the interval image/preimage computation for x ↦ 3x²+2 as this concrete example.
FC02-C01-U046	exact match	mathlib	SetRel A A	P	SetRel is definitionally a set of ordered pairs, exactly the source relation model.
FC02-C01-U047	unmatched after search	unmatched	—	N	The human descendant relation example has no searched formal Lean owner.
FC02-C01-U048	exact match	mathlib	Equivalence; bundled Setoid A	P	Exact reflexive/symmetric/transitive equivalence relation.
FC02-C01-U049	unmatched after search	unmatched	—	N	The descendant/blood/sibling example over people has no searched formal Lean owner.
FC02-C01-U050	broad match	mathlib	Setoid.r; relation notation mechanisms	P	The generic equivalence relation is present; the glyph ~ is a source notation convention rather than one fixed Mathlib notation.
FC02-C01-U051	exact match	mathlib	Setoid.classes; class set {y \| r y x}	Mathlib db584cd6… (v4.33.0); current upstream rechecked 2026-09-05	Exact equivalence-class construction.
FC02-C01-U052	exact match	mathlib	Setoid.eqv_classes_disjoint and class equality lemmas	P	Exact theorem that two equivalence classes are equal or disjoint.
FC02-C01-U053	exact match	mathlib	Setoid.IsPartition	P	Exact partition into nonempty pairwise-disjoint blocks covering the type.
FC02-C01-U054	exact match	mathlib	Setoid.Partition.orderIso	P	Stronger exact correspondence: equivalence relations and partitions are order-isomorphic.
FC02-C01-U055	unmatched after search	unmatched	—	N	No searched proved declaration packages the equal-radius equivalence classes in the plane as the stated circle partition.
FC02-C01-U056	unmatched after search	unmatched	—	N	No searched proved declaration packages the same-y-coordinate equivalence classes as horizontal lines.
FC02-C01-U057	unmatched after search	unmatched	—	N	No searched proved declaration packages the x+y level-line partition example.
FC02-C01-U058	unmatched after search	unmatched	—	N	No searched proved declaration packages the collection of all plane lines as a non-partition example.
FC02-C01-U059	broad match	mathlib	strict-order relation classes / LinearOrder with <	P	Mathlib has the exact irreflexive/transitive/total strict-order structure, usually exposed through the < relation of a LinearOrder rather than Munkres’s raw relation package.
FC02-C01-U060	partial match / wrong interface	mathlib	usual LinearOrder ℝ; generic strict-order constructors	P	The usual real order is canonical, but no searched declaration packages the source’s second custom order x² first, then x as a named reusable example.
FC02-C01-U061	exact match	mathlib	irreflexive/transitive relation classes (IsIrrefl, IsTrans) / strict-order hierarchy	P	Exact strict partial-order axioms.
FC02-C01-U062	unmatched after search	unmatched	—	N	The people-relations comparison example has no searched formal Lean owner.
FC02-C01-U063	broad match	mathlib	LT, LE, <, ≤; chain inequalities	P	The strict/non-strict notation conventions are native to ordered types; chained inequalities are parsed as conjunction-like proposition structure.
FC02-C01-U064	exact match	mathlib	Set.Ioo; CovBy	P	Open intervals and the no-element-between/cover relation formalize immediate predecessor/successor.
FC02-C01-U065	exact match	mathlib	CovBy	P	a ⋖ b is precisely that a<b with no intermediate element, the source immediate-successor relation.
FC02-C01-U066	exact match	mathlib	OrderIso	P	Exact order-preserving bijection / same order type.
FC02-C01-U067	unmatched after search	unmatched	—	N	No searched proved declaration provides the specific order isomorphism (-1,1) ≃o ℝ via x/(1-x²).
FC02-C01-U068	unmatched after search	unmatched	—	N	No searched proved declaration provides the source’s concrete order isomorphism {0}∪(1,2) ≃o [0,1).
FC02-C01-U069	exact match	mathlib	Prod.Lex; notation α ×ₗ β	P	Exact dictionary/lexicographic order on a product.
FC02-C01-U070	broad match	mathlib	Prod.Lex.toLex_lt_toLex / lex-order characterization lemmas	P	The geometric description follows directly from the exact lexicographic-order characterization, though it is not named as a plane example.
FC02-C01-U071	unmatched after search	unmatched	—	N	No searched proved declaration packages the explicit order isomorphism ℕ₊ × [0,1) ≃o ℝ≥0 with formula n+t-1.
FC02-C01-U072	exact match	mathlib	IsGreatest; IsLeast; IsMax; IsMin	P	Exact largest/smallest-element notions.
FC02-C01-U073	exact match	mathlib	BddAbove; BddBelow; upperBounds; lowerBounds; IsLUB; IsGLB; sSup; sInf	P	Exact order-bound and supremum/infimum interfaces.
FC02-C01-U074	broad match	mathlib	ConditionallyCompleteLinearOrder; IsLUB; IsGLB	P	The source least-upper-/greatest-lower-bound properties are directly expressible and bundled in the stronger conditionally-complete linear-order interface.
FC02-C01-U075	broad match	mathlib	conditionally complete interval/subtype order instances; IsLUB interval lemmas	P	Mathlib proves the structural least-upper-bound property for appropriate real intervals; the source’s particular sequence example is not a separately named theorem.
FC02-C01-U076	broad match	mathlib	raw operation A → A → A; structures such as Mul/Add	P	Binary operations are primitive function data; algebraic structures only add notation/axioms.
FC02-C01-U077	exact match	mathlib	Real; ordered-field, conditional-completeness, and dense-order instances	P	The real numbers carry the field/order/completeness/density structure assumed by the source.
FC02-C01-U078	broad match	mathlib	negation, subtraction, inversion, division on fields	P	The derived operations are native field operations with the standard laws.
FC02-C01-U079	broad match	mathlib	order predicates; Set.Ioi 0; Set.Ici 0; ℝ≥0 / NNReal	P	Positive and nonnegative reals are represented by order predicates/subtypes rather than exactly the source notation.
FC02-C01-U080	broad match	mathlib	ConditionallyCompleteLinearOrder + DenselyOrdered	P	The two defining order properties of a linear continuum are formalized, but not bundled under Munkres’s terminology.
FC02-C01-U081	partial match / wrong interface	mathlib	primitive Nat; induction/recursion principles	P	Mathlib has the resulting positive-integer induction theory, but natural numbers are primitive inductive data, not defined as the intersection of inductive subsets of ℝ as in the source.
FC02-C01-U082	broad match	mathlib	Int; Rat	P	The standard integers and rationals are canonical types, with different internal constructions from the textbook presentation.
FC02-C01-U083	exact match	mathlib	Nat.lt_wfRel; Set.Nonempty.isLeast_natFind	P	Well-foundedness of < on naturals and least-witness extraction give the positive-integer well-ordering property.
FC02-C01-U084	exact match	mathlib	Nat.strong_induction_on; Nat.strongRecOn	P	Exact strong-induction principle.
FC02-C01-U085	broad match	mathlib	dependent family A : J → Type* or J → Set X	P	Lean represents an indexed family directly by a function; it does not require a separate surjective indexing map onto the image collection.
FC02-C01-U086	exact match	mathlib	Set.iUnion; Set.iInter; Set.mem_iUnion; Set.mem_iInter	P	Exact indexed unions and intersections.
FC02-C01-U087	broad match	mathlib	finite tuple type Fin m → X	P	A finite tuple is represented as a function on Fin m, canonically equivalent to the source’s 1,…,m indexing.
FC02-C01-U088	exact match	mathlib	Set.pi	P	Exact dependent Cartesian product of a finite indexed family; Mathlib’s definition works for arbitrary index types.
FC02-C01-U089	broad match	mathlib	Set.prod; Set.pi; finite-product/Pi equivalences	P	The binary product and two-coordinate function model are canonically equivalent; Mathlib does not make the source’s set-theoretic identification definitional.
FC02-C01-U090	exact match	mathlib	Equiv.prodAssoc	P	Exact canonical bijections among triples and the two parenthesized binary products.
FC02-C01-U091	broad match	mathlib	sequence type ℕ → X	P	Exact sequence data up to the source’s positive-integer versus Lean’s zero-based natural indexing.
FC02-C01-U092	broad match	mathlib	Set.pi over ℕ	P	Exact countable dependent product modulo the positive-integer/zero-based reindexing convention.
FC02-C01-U093	broad match	mathlib	Fin m → X; ℕ → X	P	Finite and countable powers are represented as function/Pi types rather than source-specific exponent notation.
FC02-C01-U094	broad match	mathlib	Fin m → ℝ; ℕ → ℝ	P	Euclidean finite tuples and countable real sequences are standard function types; the terminology is source-level.
FC02-C01-U095	broad match	mathlib	Fin n; Finset.range n; finite intervals	P	Mathlib’s standard finite section is zero-based (Fin n/range n), canonically equivalent to Munkres’s positive-integer section.
FC02-C01-U096	exact match	mathlib	Finite; Fintype; Fintype.equivFin	P	A type is finite exactly when it is equivalent to some Fin n, including the empty case.
FC02-C01-U097	exact match	mathlib	Fintype.card; Set.ncard	P	Exact finite cardinality as a natural number.
FC02-C01-U098	broad match	mathlib	Finset.card_erase_of_mem; Fintype.card_subtype_compl	P	Removing one chosen element decrements cardinality exactly; the source’s iff of explicit bijections is a repackaging of this finite-cardinality API.
FC02-C01-U099	exact match	mathlib	Set.ncard_lt_ncard; finite-cardinality equivalence lemmas	P	A proper subset of a finite set has strictly smaller cardinality, hence cannot be bijective with the whole set.
FC02-C01-U100	exact match	mathlib	finite cardinality + Fintype.card_congr / proper-subset cardinal inequality	P	This directly excludes a bijection between a finite type and a proper subtype.
FC02-C01-U101	exact match	mathlib	Infinite ℕ	P	The natural numbers (hence positive integers after reindexing) are infinite.
FC02-C01-U102	exact match	mathlib	Fin.equiv_iff_eq; Fintype.card_congr	P	Finite cardinality is uniquely determined.
FC02-C01-U103	exact match	mathlib	Set.Finite.subset; Set.ncard_lt_ncard	P	Subsets of finite sets are finite; proper subsets have smaller cardinality.
FC02-C01-U104	broad match	mathlib	Finite.of_surjective; Finite.of_injective; Fintype.equivFin	P	The source three-way characterization is directly obtained from Mathlib’s finite-type injection/surjection/equivalence API.
FC02-C01-U105	exact match	mathlib	Set.Finite.union; finite product instances / Set.Finite.prod	P	Finite unions and finite Cartesian products of finite sets are finite.
FC02-C01-U106	broad match	mathlib	Infinite; Denumerable	P	Denumerable is countably infinite via an equivalence with ℕ; this is the same notion up to positive-integer reindexing.
FC02-C01-U107	exact match	mathlib	Equiv; Cardinal.mk; Cardinal.mk_congr	P	Same cardinality is represented by existence of an equivalence / equality of cardinal numbers.
FC02-C01-U108	exact match	mathlib	denumerable instance for ℤ	P	The integers are countably infinite.
FC02-C01-U109	broad match	mathlib	denumerable/product-countable instances for ℕ × ℕ	P	The product is countably infinite, but the source’s displayed diagonal enumeration is not the canonical library map.
FC02-C01-U110	exact match	mathlib	Countable; Uncountable	P	Exact finite-or-countably-infinite/countability interface and its negation.
FC02-C01-U111	exact match	mathlib	countable_iff_exists_injective; countable_iff_exists_surjective	P	Exact injection-to-ℕ / surjection-from-ℕ characterization for nonempty types/sets.
FC02-C01-U112	exact match	mathlib	Set.countable_infinite_iff_nonempty_denumerable	P	Exact statement that an infinite countable subset is denumerable; applied to a subset of ℕ.
FC02-C01-U113	broad match	mathlib	Nat.rec; WellFounded.fix; Nat.strongRecOn	P	Recursive definitions are native recursion/well-founded-recursion mechanisms rather than a separate predicate.
FC02-C01-U114	exact match	mathlib	Set.Countable.mono	P	Exact closure of countability under subsets.
FC02-C01-U115	exact match	mathlib	denumerable instance on ℕ × ℕ	P	Exact countable infinitude of the product.
FC02-C01-U116	broad match	mathlib	Rat.instDenumerable; countable subtypes; positivity subtype	P	ℚ is denumerable and the positive rationals form an infinite countable subtype; the source’s explicit quotient enumeration is not a named theorem.
FC02-C01-U117	exact match	mathlib	Set.countable_iUnion; Set.Countable.sUnion	P	Exact theorem that a countable union of countable sets is countable.
FC02-C01-U118	exact match	mathlib	Set.countable_pi; Set.countable_univ_pi	P	Exact finite-product closure for countable sets.
FC02-C01-U119	broad match	mathlib	Cardinal.cantor; Pi/cardinal arithmetic; cantorSetEquivNatToBool	P	Mathlib has the Cantor-space type ℕ → Bool and the cardinal machinery proving it uncountable, but no searched single declaration states this textbook theorem verbatim.
FC02-C01-U120	exact match	mathlib	Cardinal.cantor; power-set/cardinality equivalences	P	Cantor’s theorem gives strictly larger cardinality for the power set, equivalently no injection 𝒫(A) → A and no surjection A → 𝒫(A).
FC02-C01-U121	broad match	mathlib	finite recursion on Fin n; Nat.rec / Nat.strongRecOn	P	The finite-stage existence lemma is subsumed by Lean’s recursion principles rather than exposed as this auxiliary theorem.
FC02-C01-U122	broad match	mathlib	uniqueness from recursion equations; Nat.rec/WellFounded.fix_eq	P	The overlap-uniqueness lemma is built into the uniqueness of recursively defined functions but is not a separately named source-shaped theorem.
FC02-C01-U123	broad match	mathlib	Nat.strongRecOn; WellFounded.fix	P	Existence and uniqueness of the recursively specified sequence follow from the standard recursion machinery; the positive-integer indexing differs.
FC02-C01-U124	exact match	mathlib	Nat.strongRecOn; WellFounded.fix; WellFounded.fix_eq	P	Strong/well-founded recursion allows each value to depend on the complete restriction to earlier values, matching the principle of recursive definition.
FC02-C01-U125	broad match	mathlib	recursion equations generated by Nat.rec / WellFounded.fix_eq	P	The source row is terminology for the equations that characterize a recursive definition.
FC02-C01-U126	broad match	mathlib	Nat.nth; Set.Infinite.natEmbedding; least-element APIs	P	Mathlib can enumerate an infinite subset of ℕ increasingly/without repetition using least-element machinery, but the exact source construction is not a dedicated named example.
FC02-C01-U127	exact match	mathlib	generic power recursion pow_succ, pow_one	P	Exact recursive equations for positive powers (up to the standard zero-based exponent convention).
FC02-C01-U128	broad match	mathlib	Infinite.natEmbedding; Infinite.of_injective_to_set; finite/infinite equivalence machinery	P	Mathlib directly provides the injection characterization and the proper-subset direction; the full Dedekind-infinite equivalence is recoverable classically but not found as one source-shaped declaration.
FC02-C01-U129	exact match	mathlib	Classical.axiomOfChoice	P	Mathlib’s choice theorem is stronger: it chooses from any family of nonempty fibers, so the disjoint-family form follows.
FC02-C01-U130	exact match	mathlib	Classical.axiomOfChoice; Classical.choose	P	Exact existence of a choice function for an arbitrary family of nonempty sets.
FC02-C01-U131	broad match	mathlib	dependent choice function (B : ι → Set α) → ∀ i, B i / Classical.choose	P	The choice-function data is represented directly as a dependent function with membership proofs.
FC02-C01-U132	broad match	mathlib	finite products/finite choice constructively; Classical.axiomOfChoice for arbitrary families	P	Mathlib distinguishes constructive finite choice from unrestricted classical choice, but not under this prose convention.
FC02-C01-U133	exact match	mathlib	IsWellOrder; WellFoundedLT	P	Exact well-order notion.
FC02-C01-U134	broad match	mathlib	Prod.Lex well-founded/well-order instances	P	The lexicographic product of the two-element finite order with ℕ is automatically well-ordered; the displayed two-block enumeration is not a named example.
FC02-C01-U135	exact match	mathlib	Prod.Lex.instIsWellFounded; well-order instance for lex products	P	Directly proves the lexicographic ℕ × ℕ example is well-ordered.
FC02-C01-U136	unmatched after search	unmatched	—	N	No searched reusable theorem packages both source counterexamples: usual-order ℤ and [0,1] are not well-ordered via the displayed subsets.
FC02-C01-U137	exact match	mathlib	Fintype.orderIsoFinOfCardEq; finite linear-order well-foundedness	P	Every finite linear order is order-isomorphic to a finite ordinal, hence well-ordered.
FC02-C01-U138	exact match	mathlib	WellOrderingRel; WellOrderingRel.isWellOrder; exists_wellFoundedLT	P	Exact well-ordering theorem for every type.
FC02-C01-U139	exact match	mathlib	Ordinal.omega / ω₁; Ordinal.omega0_lt_omega_one	P	ω₁ supplies an explicit uncountable well-ordered type/order, stronger than mere existence.
FC02-C01-U140	exact match	mathlib	Set.Iio α	P	The section below α in an ordered type is exactly the strict lower interval.
FC02-C01-U141	exact match	mathlib	Set.Iio α	P	Exact source notation/construction for a well-order section.
FC02-C01-U142	broad match	mathlib	Ordinal.ω₁; Set.Iio ω₁; Set.Iic ω₁; first-uncountable-ordinal/cardinal API	P	The source S_Ω and \bar S_Ω construction is represented by Iio ω₁ and Iic ω₁; countability of every proper initial section follows from ω₁ being the first uncountable ordinal, but is distributed across ordinal/cardinal declarations.
FC02-C01-U143	broad match	mathlib	Set.Iio ω₁; Set.Iic ω₁	P	These are the exact underlying orders of Munkres’s S_Ω and the same order with its largest point adjoined; source notation differs.
FC02-C01-U144	exact match	mathlib	Ordinal.iSup_lt_omega_one	P	A countable supremum of countable ordinals is below ω₁, which is exactly the boundedness theorem for a countable subset of S_Ω.
FC02-C01-U145	exact match	mathlib	irreflexive/transitive strict-order relations	P	Exact strict partial-order notion.
FC02-C01-U146	exact match	mathlib	IsChain; IsMaxChain	P	Exact simply ordered subset and maximal simply ordered subset.
FC02-C01-U147	exact match	mathlib	IsChain.exists_maxChain	P	Exact maximum principle: every chain is contained in a maximal chain, and in particular a maximal chain exists.
FC02-C01-U148	unmatched after search	unmatched	—	N	No searched proved declaration packages the two concrete maximal chains of circular regions in the plane.
FC02-C01-U149	unmatched after search	unmatched	—	N	No searched proved declaration packages the source’s concrete strict partial-order example on ℝ².
FC02-C01-U150	exact match	mathlib	upperBounds; IsMax	P	Exact upper-bound and maximal-element notions.
FC02-C01-U151	exact match	mathlib	upperBounds; IsMax	P	Exact full source definitions.
FC02-C01-U152	exact match	mathlib	exists_maximal_of_chains_bounded; zorn_le	P	Direct formulations of Zorn’s lemma.
FC02-C01-U153	broad match	mathlib	PartialOrder; strict/non-strict order conversion infrastructure	P	Mathlib’s standard interface takes ≤ as primary and derives <; the source starts from a strict partial order and adjoins equality, so the mathematics is present with the opposite packaging direction.

Provenance contract for C02

• Project search: LeanCategories/** outside .lake was searched first. Specialized topology uses exist (adic completions, quotient manifolds, adelic spaces), but no project-owned declaration replaces the Munkres §§12–22 foundational units, so none is credited merely for importing/using the same Mathlib interfaces.
• Pinned Mathlib: repository pin db584cd6d46c92f209a44c0f1c829460d327499d (v4.33.0) was declaration-checked across topology definitions, bases, order topology, products/Pi types, subspaces, separation, continuous maps, metric/metrizable spaces, uniform convergence, and quotient maps.
• Current Mathlib: default branch rechecked 2026-09-05 at 4cbb42e75a050e830b7cf0f2ae748d7644f59cf7; no current-only declaration was needed to upgrade a C02 verdict.
• External Lean search: GitHub/ecosystem/source-atlas searches rechecked mdnestor/basic_topology@10230d7997436e8be1644d0750ec6b03d845619b, whose Munkres files cover these sections, but the repository exposes no license file. It is therefore search corroboration only, not a package-import or reference-port route. Loogle/LeanSearch, Reservoir-style package discovery, broad GitHub Lean search, and the local formalization source atlas produced no separately licensed C02 owner that improved the routes below.
• The arbitrary Pi product topology is native in Mathlib (continuous_pi_iff, isTopologicalBasis_pi). The pinned and importable Counterexamples/SorgenfreyLine.lean supplies the lower-limit/Sorgenfrey topology itself and several of its standard separation/countability facts. No searched bundled box topology, K-topology, or Munkres uniform topology was found; concrete textbook examples are not counted as implemented merely because general definitions could be instantiated to prove them.
• exact match, broad match, partial match / wrong interface, and unmatched after search retain the C01 meanings. Mathlib/Lean code is Apache-2.0.

C02 — Topological Spaces and Continuous Functions

FC02 ID	Verdict	Route	Lean target(s)	Provenance	Interface comparison
FC02-C02-U001	exact match	mathlib	Mathlib/Topology/Defs/Basic.lean::TopologicalSpace; IsOpen	P	Exact topology axioms: univ/open intersections/arbitrary unions are the native structure.
FC02-C02-U002	broad match	mathlib	Mathlib/Topology/Defs/Basic.lean::TopologicalSpace; IsOpen	P	The source vocabulary “topological space/open set” is native; it is terminology rather than a separate theorem.
FC02-C02-U003	unmatched after search	unmatched	—	N	No searched proved declaration packages Munkres’s three-element concrete topology examples; abstract TopologicalSpace data alone does not count as the examples.
FC02-C02-U004	exact match	mathlib	Mathlib/Topology/Order.lean::DiscreteTopology; IndiscreteTopology	P	Exact discrete and indiscrete/trivial topology interfaces.
FC02-C02-U005	exact match	mathlib	Mathlib/Topology/Constructions.lean::TopologicalSpace.cofinite; CofiniteTopology.isOpen_iff'	P	Exact cofinite topology: nonempty opens have finite complement.
FC02-C02-U006	unmatched after search	unmatched	—	N	Mathlib has the cocountable/co-cardinal filter but no searched TopologicalSpace whose opens are empty or countable-complement, so the cocountable topology itself is not owned.
FC02-C02-U007	exact match	mathlib	Mathlib/Topology/Order.lean::TopologicalSpace.le_def	P	The topology lattice order is exactly reverse inclusion of open-set families, giving finer/coarser comparison.
FC02-C02-U008	exact match	mathlib	Mathlib/Topology/Bases.lean::IsTopologicalBasis; IsTopologicalBasis.eq_generateFrom	P	Exact basis/generation interface.
FC02-C02-U009	exact match	mathlib	Mathlib/Topology/Bases.lean::IsTopologicalBasis.exists_subset_of_mem_open	P	Exact point-in-open-set criterion for a basis.
FC02-C02-U010	broad match	mathlib	Mathlib/Topology/MetricSpace/Pseudo/Defs.lean::Metric.nhds_basis_ball	P	Metric balls form a neighborhood basis at every point, which structurally yields the circular-region basis on ℝ²; no source-specific plane theorem is needed.
FC02-C02-U011	broad match	mathlib	Mathlib/Topology/Order/Basic.lean::nhds_basis_Ioo; Mathlib/Topology/Bases.lean::IsTopologicalBasis.prod	P	Open intervals give the real local basis and products of bases give axis rectangles; this is the structural form of the plane rectangle basis.
FC02-C02-U012	exact match	mathlib	Mathlib/Topology/Bases.lean::isTopologicalBasis_singletons	P	Exact theorem that singletons are a basis in a discrete topology.
FC02-C02-U013	exact match	mathlib	Mathlib/Topology/Bases.lean::IsTopologicalBasis.open_eq_sUnion	P	Exact theorem that every open set is a union of basis elements.
FC02-C02-U014	exact match	mathlib	Mathlib/Topology/Bases.lean::IsTopologicalBasis.isTopologicalBasis_of_exists_subset	P	Exact refinement criterion constructing a basis from pointwise refinements inside opens.
FC02-C02-U015	exact match	mathlib	Mathlib/Topology/Bases.lean::IsTopologicalBasis.isTopologicalBasis_of_exists_subset	P	The same theorem gives the standard mutual-refinement criterion for equality/refinement of basis topologies.
FC02-C02-U016	broad match	mathlib	Metric.nhds_basis_ball; nhds_basis_Ioo; IsTopologicalBasis.prod	P	Mathlib supplies both circular and rectangular neighborhood bases for Euclidean ℝ²; the equality is structural through the canonical topology rather than a dedicated comparison theorem.
FC02-C02-U017	partial match / wrong interface	mathlib	Mathlib/Topology/MetricSpace/Pseudo/Lemmas.lean::OrderTopology ℝ; Topology/Order/Basic.lean::OrderTopology	P	The standard real topology is canonical, but lower-limit and K-topologies are not bundled as named Mathlib spaces.
FC02-C02-U018	exact match	mathlib	Mathlib/Topology/MetricSpace/Pseudo/Lemmas.lean::OrderTopology ℝ	P	The ordinary real topology is exactly its order topology.
FC02-C02-U019	exact match	mathlib	Counterexamples/SorgenfreyLine.lean::Counterexample.SorgenfreyLine; Counterexample.SorgenfreyLine.isOpen_Ico; Counterexample.SorgenfreyLine.nhds_basis_Ico	P	Exact lower-limit/Sorgenfrey topology: the type is the real line with topology generated by half-open intervals, and [a,b) is open with the expected neighborhood basis.
FC02-C02-U020	unmatched after search	unmatched	—	N	No searched declaration bundles Munkres’s K-topology on ℝ as the source example.
FC02-C02-U021	unmatched after search	unmatched	—	N	The strict-fineness and incomparability statements for the lower-limit/K topologies have no searched formal owner because those concrete topologies are not bundled.
FC02-C02-U022	exact match	mathlib	Mathlib/Topology/Bases.lean::isTopologicalBasis_of_subbasis; Mathlib/Topology/Order.lean::generateFrom	P	Exact subbasis-to-generated-topology construction.
FC02-C02-U023	broad match	mathlib	Mathlib/Order/Interval/Set/Defs.lean::Set.Ioo; Set.Iio; Set.Ioi	P	Exact interval/ray sets used by order topologies; source terminology is represented by standard interval notation.
FC02-C02-U024	exact match	mathlib	Mathlib/Topology/Order/Basic.lean::Preorder.topology; OrderTopology.topology_eq_generate_intervals	P	Exact order-topology generation by open rays/intervals.
FC02-C02-U025	exact match	mathlib	Mathlib/Topology/MetricSpace/Pseudo/Lemmas.lean::OrderTopology ℝ	P	Exact instance identifying the standard topology of ℝ with its order topology.
FC02-C02-U026	broad match	mathlib	Mathlib/Data/Prod/Lex.lean::Prod.Lex; Mathlib/Topology/Order/Basic.lean::OrderTopology	P	Lexicographic products and their order topology are native; the “dictionary order on the plane” is the corresponding specialization, not a separate named example.
FC02-C02-U027	broad match	mathlib	Mathlib/Topology/Instances/Discrete.lean (OrderTopology ℕ, DiscreteTopology ℕ)	P	The natural/positive-integer order topology is discrete; positive integers differ only by the standard reindexing/subtype presentation.
FC02-C02-U028	unmatched after search	unmatched	—	N	No searched declaration packages the displayed dictionary-order example on {1,2}×ℤ₊ with its source-specific neighborhoods.
FC02-C02-U029	exact match	mathlib	Mathlib/Topology/Order/Basic.lean::Preorder.topology; OrderTopology.topology_eq_generate_intervals	P	The four order rays are exactly the generating subbasis of the preorder/order topology.
FC02-C02-U030	broad match	mathlib	Set.Iio; Set.Ioi; Set.Iic; Set.Ici	P	Open/closed ray terminology is represented exactly by standard interval constructors, though not as a theorem.
FC02-C02-U031	exact match	mathlib	Mathlib/Topology/Constructions/SumProd.lean product TopologicalSpace; isOpen_prod_iff	P	Exact binary product topology characterized by products of open sets locally.
FC02-C02-U032	exact match	mathlib	Mathlib/Topology/Bases.lean::IsTopologicalBasis.prod	P	Exact theorem that products of basis elements form a basis for the product topology.
FC02-C02-U033	broad match	mathlib	nhds_basis_Ioo; IsTopologicalBasis.prod; standard product topology on ℝ×ℝ	P	Axis-aligned open rectangles form the structural product basis on ℝ²; Mathlib uses the generic product theorem rather than a plane-specific lemma.
FC02-C02-U034	exact match	mathlib	Mathlib/Topology/Constructions/SumProd.lean::continuous_fst; continuous_snd	P	Exact coordinate projection maps with their native continuity properties.
FC02-C02-U035	exact match	mathlib	Mathlib/Topology/Constructions/SumProd.lean::prod_eq_generateFrom	P	Exact generation of the product topology from inverse images under the two projections.
FC02-C02-U036	exact match	mathlib	Mathlib/Topology/Defs/Induced.lean::TopologicalSpace.induced; subtype topology	P	The subtype topology is exactly the topology induced by the inclusion.
FC02-C02-U037	exact match	mathlib	Mathlib/Topology/Bases.lean::isTopologicalBasis_subtype	P	Exact induced basis on a subspace by intersections/preimages.
FC02-C02-U038	exact match	mathlib	Mathlib/Topology/Constructions.lean::IsOpen.trans	P	An open subset of an open subspace is open in the ambient space, exactly the source theorem.
FC02-C02-U039	exact match	mathlib	Mathlib/Topology/Constructions/SumProd.lean::Topology.IsInducing.prodMap; IsInducing.subtypeVal	P	Product of subspace topologies agrees with the subspace topology on the product via the product inducing map.
FC02-C02-U040	broad match	mathlib	IsTopologicalBasis.subtype; nhds_basis_Ioo	P	The standard endpoint/interior basis forms on [0,1] follow from the generic subtype basis; no special interval basis theorem is required.
FC02-C02-U041	unmatched after search	unmatched	—	N	No searched declaration records the concrete Y=[0,1)∪{2} comparison between subspace and order topologies.
FC02-C02-U042	unmatched after search	unmatched	—	N	No searched declaration records the lexicographic ordered-square versus ambient lexicographic-plane subspace counterexample.
FC02-C02-U043	unmatched after search	unmatched	—	N	The named “ordered square” example is not a bundled searched Lean object/declaration.
FC02-C02-U044	exact match	mathlib	Mathlib/Topology/Order/Basic.lean::StrictMono.isEmbedding_of_ordConnected	P	Stronger generic statement: an order-connected (convex) subset embeds with induced topology equal to its order topology.
FC02-C02-U045	exact match	mathlib	Mathlib/Topology/Defs/Basic.lean::IsClosed	P	Exact definition: a set is closed iff its complement is open.
FC02-C02-U046	exact match	mathlib	Mathlib/Topology/Order/OrderClosed.lean::isClosed_Icc	P	Exact closedness of closed intervals in the real/order topology.
FC02-C02-U047	broad match	mathlib	Mathlib/Topology/Constructions/SumProd.lean::IsClosed.prod; isClosed_Ici	P	The first quadrant is a product of two closed rays, so its closedness is a direct specialization of generic declarations.
FC02-C02-U048	exact match	mathlib	Mathlib/Topology/Constructions.lean::CofiniteTopology.isClosed_iff	P	Exact characterization: closed sets are the whole space or finite sets.
FC02-C02-U049	exact match	mathlib	Mathlib/Topology/Order.lean::isClosed_discrete	P	Exact theorem that every set is closed in a discrete topology.
FC02-C02-U050	unmatched after search	unmatched	—	N	No searched declaration packages the concrete subspace Y=[0,1]∪(2,3) and its source list of closed/open subsets.
FC02-C02-U051	exact match	mathlib	Mathlib/Topology/Basic closed-set lattice theorems (isClosed_empty, isClosed_iInter, finite unions)	P	Exact closed-set axioms dual to the topology axioms.
FC02-C02-U052	exact match	mathlib	Mathlib/Topology/Constructions.lean::isClosed_induced_iff	P	Exact characterization of closed subspace sets as intersections/preimages of ambient closed sets.
FC02-C02-U053	exact match	mathlib	Mathlib/Topology/Constructions.lean::IsClosed.trans	P	Exact transitivity: closed in a closed subspace implies ambient closed.
FC02-C02-U054	exact match	mathlib	Mathlib/Topology/Defs/Basic.lean::interior; closure	P	Exact interior and closure constructions with maximal/minimal universal properties.
FC02-C02-U055	exact match	mathlib	Mathlib/Topology/Constructions.lean::closure_subtype	P	Exact comparison of closure in a subspace with ambient closure and intersection/restriction.
FC02-C02-U056	exact match	mathlib	Mathlib/Topology/ClusterPt.lean::mem_closure_iff_clusterPt; neighborhood/filter closure criteria	P	Exact neighborhood-intersection characterization of closure.
FC02-C02-U057	exact match	mathlib	Mathlib/Topology/Bases.lean::IsTopologicalBasis.mem_closure_iff	P	Exact basis version: closure membership iff every basis neighborhood meets the set.
FC02-C02-U058	broad match	mathlib	Mathlib/Topology/Defs/Filter.lean::nhds; IsOpen.mem_nhds	P	Neighborhoods are represented by the neighborhood filter; the source set-based terminology is equivalent but packaged more structurally.
FC02-C02-U059	unmatched after search	unmatched	—	N	No searched proved declaration simultaneously records the source’s six concrete closure calculations in ℝ; generic closure APIs do not count as the example.
FC02-C02-U060	unmatched after search	unmatched	—	N	No searched proved declaration records the stated closure computation of (0,1/2) inside Y=(0,1].
FC02-C02-U061	exact match	mathlib	Mathlib/Topology/ClusterPt.lean::accPt_principal_iff_clusterPt; accPt_iff_nhds	P	Exact accumulation-point/limit-point characterization using A\{x} and punctured neighborhoods.
FC02-C02-U062	unmatched after search	unmatched	—	N	No searched declaration packages the source’s concrete list of limit-point examples.
FC02-C02-U063	broad match	mathlib	Mathlib/Topology/DerivedSet.lean::derivedSet; closure_eq_self_union_derivedSet	P	The source notation A′ is Mathlib’s derivedSet A; the motivating relation is already formalized structurally.
FC02-C02-U064	exact match	mathlib	Mathlib/Topology/DerivedSet.lean::closure_eq_self_union_derivedSet	P	Exact theorem closure A = A ∪ derivedSet A.
FC02-C02-U065	exact match	mathlib	Mathlib/Topology/DerivedSet.lean::isClosed_iff_derivedSet_subset; ClusterPt.isClosed_iff_accPt	P	Exact theorem: closed iff all accumulation points lie in the set.
FC02-C02-U066	broad match	mathlib	Mathlib/Topology/Sequences.lean; Filter.Tendsto to 𝓝	P	Sequence convergence is represented by Tendsto u atTop (𝓝 x), exactly the standard topology but in filter form.
FC02-C02-U067	exact match	mathlib	Mathlib/Topology/Separation/Hausdorff.lean::T2Space	P	Exact Hausdorff separation axiom.
FC02-C02-U068	exact match	mathlib	Mathlib/Topology/Separation/Basic.lean::Set.Finite.isClosed	P	Stronger theorem under T1Space: every finite set is closed, hence in every Hausdorff space.
FC02-C02-U069	exact match	mathlib	Mathlib/Topology/Separation/Basic.lean::T1Space; isClosed_singleton	P	Exact T1/singletons-closed interface.
FC02-C02-U070	broad match	mathlib	Mathlib/Topology/ClusterPt.lean::accPt_iff_nhds; Topology/Separation/Basic.lean::nhdsNE_le_cofinite	P	In a T1 space punctured neighborhoods are cofinite in the required sense; combined with accPt_iff_nhds gives the source infinite-neighborhood characterization.
FC02-C02-U071	exact match	mathlib	Mathlib/Topology/Separation/Hausdorff.lean::tendsto_nhds_unique	P	Exact uniqueness of limits in Hausdorff spaces, stated for arbitrary filters and hence sequences.
FC02-C02-U072	broad match	mathlib	Filter.Tendsto; 𝓝	P	The source convergence notation is represented by Lean’s standard filter convergence notation/interface.
FC02-C02-U073	exact match	mathlib	Mathlib/Topology/Order/OrderClosed.lean::OrderClosedTopology.to_t2Space; Separation/Hausdorff.lean::Prod.t2Space; subtype T2 instance	P	Generic instances prove order-topological spaces, products, and subspaces Hausdorff under the source hypotheses.
FC02-C02-U074	exact match	mathlib	Mathlib/Topology/Defs/Basic.lean::Continuous	P	Exact inverse-image-of-open-sets definition of continuity.
FC02-C02-U075	unmatched after search	unmatched	—	N	No searched theorem packages Munkres’s generic calculus-analysis example as a specific formal object beyond the general continuity interface.
FC02-C02-U076	broad match	mathlib	Mathlib/Topology/Algebra/*; continuous_const, continuous_id, continuous algebraic operations	P	The common calculus map classes are broadly available through continuous algebraic operations, but the source row is an examples catalogue rather than one theorem.
FC02-C02-U077	unmatched after search	unmatched	—	N	No searched declaration packages the exact identity map between the usual and lower-limit real topologies; the lower-limit topology itself is not bundled.
FC02-C02-U078	exact match	mathlib	Mathlib/Topology/Continuous.lean::continuous_iff_image_closure_subset_closure_image; continuous_iff_isClosed; continuous_iff_continuousAt	P	Mathlib packages the source equivalent continuity criteria, with neighborhoods expressed by filters.
FC02-C02-U079	exact match	mathlib	Mathlib/Topology/Homeomorph/Defs.lean::Homeomorph	P	Exact homeomorphism data: equivalence with continuous forward and inverse maps.
FC02-C02-U080	broad match	mathlib	Homeomorph; invariant/property transport throughout topology	P	“Topological property” is source terminology; Mathlib realizes invariance by homeomorphism transport rather than one predicate.
FC02-C02-U081	exact match	mathlib	Mathlib/Topology/Defs/Induced.lean::Topology.IsEmbedding	P	Exact embedding notion: inducing topology plus injectivity.
FC02-C02-U082	unmatched after search	unmatched	—	N	No searched declaration packages the concrete affine homeomorphism x ↦ 3x+1 as this textbook example.
FC02-C02-U083	unmatched after search	unmatched	—	N	No searched declaration packages the specific homeomorphism (-1,1) → ℝ, x ↦ x/(1-x²).
FC02-C02-U084	unmatched after search	unmatched	—	N	No searched declaration packages the source’s concrete continuous-bijection/non-homeomorphism examples, including the lower-limit real line example.
FC02-C02-U085	unmatched after search	unmatched	—	N	No searched declaration packages the specific map g:[0,1)→ℝ² used as the source example.
FC02-C02-U086	exact match	mathlib	Mathlib/Topology/Continuous.lean::continuous_const; continuous_id; Continuous.comp; Topology/ContinuousOn.lean::continuous_of_cover_nhds	P	The standard continuity construction rules, including local gluing over open neighborhoods, are present generically.
FC02-C02-U087	exact match	mathlib	Mathlib/Topology/ContinuousOn.lean::ContinuousOn.union_of_isClosed; continuousOn_union_iff_of_isClosed	P	Exact closed-set pasting principle, in the general continuous-on form.
FC02-C02-U088	unmatched after search	unmatched	—	N	No searched declaration records the specific piecewise function used to illustrate the pasting lemma.
FC02-C02-U089	exact match	mathlib	Mathlib/Topology/Constructions/SumProd.lean::Continuous.prodMk; continuous_fst; continuous_snd	P	Exact criterion: a map into a binary product is continuous iff its coordinate maps are continuous.
FC02-C02-U090	broad match	mathlib	continuous_fst; continuous_snd; coordinate composition	P	Coordinate functions are native projections/compositions; the source row is terminology.
FC02-C02-U091	broad match	mathlib	Continuous; product-valued continuous maps	P	Parametrized curves/vector fields are represented directly as continuous maps into product/Euclidean types; no source-specific wrapper is needed.
FC02-C02-U092	partial match / wrong interface	mathlib	Mathlib/Topology/Constructions.lean Pi product topology; Mathlib/Topology/Bases.lean::isTopologicalBasis_pi	P	Mathlib has the arbitrary product topology but no searched general box-topology structure; the source row explicitly contrasts both.
FC02-C02-U093	broad match	mathlib	dependent function type ∀ i, X i	P	An indexed tuple is represented definitionally as a dependent function, matching the source up to packaging.
FC02-C02-U094	exact match	mathlib	Set.pi; dependent product type ∀ i, X i	P	Exact indexed Cartesian-product data, with set-level and type-level versions.
FC02-C02-U095	broad match	mathlib	Set.pi; Pi/function types	P	The source’s repeated identification of points with indexed tuples is the native Pi representation.
FC02-C02-U096	unmatched after search	unmatched	—	N	No searched Mathlib/project declaration defines the arbitrary box topology whose basis allows unrestricted open coordinates.
FC02-C02-U097	unmatched after search	unmatched	—	N	No searched bundled box-topology space/interface was found; the unlicensed mdnestor/basic_topology source is not creditable as a route.
FC02-C02-U098	exact match	mathlib	Mathlib/Topology/Constructions.lean::continuous_apply	P	Exact coordinate projection from a Pi product, continuous for the product topology.
FC02-C02-U099	exact match	mathlib	Mathlib/Topology/Constructions.lean Pi topology as infimum of induced evaluation topologies; Mathlib/Topology/Bases.lean::isTopologicalBasis_pi	P	Exact initial/product topology generated by coordinate projections, with finite-support basic opens.
FC02-C02-U100	exact match	mathlib	Mathlib/Topology/Constructions.lean Pi topological-space instance; continuous_pi_iff	P	Exact arbitrary product topology in Mathlib’s native Pi construction.
FC02-C02-U101	partial match / wrong interface	mathlib	Mathlib/Topology/Bases.lean::isTopologicalBasis_pi	P	The product-side finite-support basis is exact and finite products collapse as expected, but the comparison with a separately defined box topology is not bundled.
FC02-C02-U102	partial match / wrong interface	mathlib	IsTopologicalBasis.prod; isTopologicalBasis_pi	P	Factor bases induce the product basis exactly; the unrestricted box-basis half has no searched bundled box topology.
FC02-C02-U103	broad match	mathlib	nhds_basis_Ioo; isTopologicalBasis_pi for finite index	P	For finite n, rectangular boxes from interval bases give the standard topology on ℝⁿ; represented generically rather than as a named ℝⁿ theorem.
FC02-C02-U104	partial match / wrong interface	mathlib	Topology.IsInducing.prodMap; Pi subtype/inducing constructions	P	Subspace compatibility is formalized for ordinary products/Pi products; the source’s parallel box-topology assertion has no bundled box interface.
FC02-C02-U105	partial match / wrong interface	mathlib	Prod.t2Space; Pi T2 instance in separation API	P	Hausdorffness of product topologies is native; the box-topology half is unbundled.
FC02-C02-U106	partial match / wrong interface	mathlib	Mathlib/Topology/Constructions/SumProd.lean::closure_prod_eq; Pi closure infrastructure	P	Binary/product closure results are present; the source’s unrestricted-box statement is not separately formalized as a box theorem.
FC02-C02-U107	exact match	mathlib	Mathlib/Topology/Constructions.lean::continuous_pi_iff	P	Exact coordinatewise continuity criterion for maps into an arbitrary product topology.
FC02-C02-U108	broad match	mathlib	Pi type ℕ → ℝ; product topology; continuous_pi_iff	P	ℝ^ω is represented canonically as a countable Pi type with the product topology; source notation differs.
FC02-C02-U109	exact match	mathlib	Mathlib/Topology/MetricSpace/Defs.lean::MetricSpace; MetricSpace/Pseudo/Defs.lean::PseudoMetricSpace	P	Exact metric axioms (with a pseudometric superclass split in Mathlib).
FC02-C02-U110	exact match	mathlib	Mathlib/Topology/MetricSpace/Pseudo/Defs.lean::Metric.ball; dist	P	Exact distance and open-ball constructions.
FC02-C02-U111	exact match	mathlib	Mathlib/Topology/MetricSpace/Pseudo/Defs.lean::Metric.nhds_basis_ball	P	Balls are a neighborhood basis at each point, exactly the local basis content generating the metric topology.
FC02-C02-U112	broad match	mathlib	Mathlib/Topology/Instances/Discrete.lean; discrete metric/metricizable-space instances	P	Mathlib has the discrete topology and compatible discrete metric infrastructure; the source’s displayed 0/1 formula is not the canonical public theorem.
FC02-C02-U113	broad match	mathlib	Real.dist_eq; OrderTopology ℝ; standard real MetricSpace	P	The standard real metric/topology is canonical; Mathlib does not need a separate source-shaped declaration.
FC02-C02-U114	exact match	mathlib	Mathlib/Topology/Metrizable/Basic.lean::TopologicalSpace.MetrizableSpace	P	Exact notion: existence of a compatible metric (implemented via an equivalent countably generated uniformity interface).
FC02-C02-U115	partial match / wrong interface	mathlib	Metric.isBounded_iff; Metric.ediam; TopologicalSpace.MetrizableSpace	P	Metric boundedness/diameter are present and not topological invariants in general, but no searched theorem packages Munkres’s specific bounded-equivalent-metric construction in this row.
FC02-C02-U116	exact match	mathlib	Mathlib/Topology/MetricSpace/Bounded.lean::Metric.diam; Metric.dist_le_diam_of_mem	P	Exact real-valued diameter API on bounded metric sets, backed by extended diameter for unbounded cases.
FC02-C02-U117	unmatched after search	unmatched	—	N	No searched declaration states that d̄(x,y)=min(d(x,y),1) is a metric inducing exactly the same topology for arbitrary d.
FC02-C02-U118	unmatched after search	unmatched	—	N	No searched reusable declaration packages Munkres’s named “standard bounded metric” terminology/construction min(d,1).
FC02-C02-U119	broad match	mathlib	Mathlib/Analysis/InnerProductSpace/EuclideanDist.lean / finite Pi norm and metric infrastructure	P	Euclidean and sup/square metrics on finite real tuples are native analytic structures, though the source setup is not one named declaration.
FC02-C02-U120	broad match	mathlib	finite-dimensional Euclidean/Pi MetricSpace; standard norm-induced distance	P	The Euclidean metric on ℝⁿ is the canonical finite-dimensional metric structure, represented through normed-space infrastructure.
FC02-C02-U121	exact match	mathlib	Mathlib/Topology/MetricSpace/Pseudo/Pi.lean::pseudoMetricSpacePi; dist_pi_def	P	For finite index, Mathlib’s Pi metric is exactly the coordinate sup metric, matching the source square metric.
FC02-C02-U122	broad match	mathlib	Metric.nhds_basis_ball; topology equality/extensionality APIs	P	The standard local mutual-ball-inclusion criterion for equality/refinement of metric topologies is encoded by neighborhood ball bases, though not under the textbook theorem name.
FC02-C02-U123	broad match	mathlib	pseudoMetricSpacePi; dist_pi_def; finite Pi/product topology	P	For finite real powers the sup metric and Euclidean norm metrics induce the canonical product topology; Mathlib packages this through the compatible finite-product metric structures.
FC02-C02-U124	unmatched after search	unmatched	—	N	No searched declaration packages Munkres’s specific uniform metric on ℝ^ω defined as a supremum of bounded coordinate metrics.
FC02-C02-U125	unmatched after search	unmatched	—	N	No searched general ℝ^J uniform-topology object matching Munkres’s sup of bounded coordinate metrics was found.
FC02-C02-U126	unmatched after search	unmatched	—	N	The strict chain product < uniform < box for infinite J is not owned by a searched declaration; the latter two textbook topologies are not bundled in this form.
FC02-C02-U127	broad match	mathlib	Mathlib/Topology/MetricSpace/PiNat.lean countable-product metric (dist_eq_tsum)	P	Mathlib has an explicit metric inducing the countable product topology, but uses a summable weighted-min metric rather than Munkres’s exact sup (ar d_i/i) formula.
FC02-C02-U128	exact match	mathlib	Mathlib/Topology/MetricSpace/Pseudo/Defs.lean::Metric.nhds_basis_ball; Mathlib/Topology/Continuous.lean::continuous_iff_continuousAt	P	The neighborhood-ball Tendsto basis is exactly the epsilon-delta continuity criterion, with continuity packaged through ContinuousAt.
FC02-C02-U129	exact match	mathlib	Mathlib/Topology/Sequences.lean::mem_closure_iff_seq_limit (metrizable/first-countable setting)	P	Exact sequential characterization of closure in metrizable spaces, including the always-valid forward implication in the library’s sequence API.
FC02-C02-U130	exact match	mathlib	Mathlib/Topology/Sequences.lean::continuous_iff_seqContinuous (sequential spaces); MetrizableSpace.firstCountableTopology	P	Continuous maps preserve sequential limits, and in metrizable spaces sequential continuity conversely characterizes continuity.
FC02-C02-U131	exact match	mathlib	Mathlib/Topology/Algebra/Monoid/Defs.lean::ContinuousAdd.continuous_add; continuous_mul; Mathlib/Topology/Algebra/Group/Defs.lean::continuous_sub; continuous_div'	P	Exact continuity of the real field operations (division on the nonzero-denominator domain/appropriate structure).
FC02-C02-U132	exact match	mathlib	continuous-map algebra instances; Continuous.add/sub/mul/div	P	Exact closure rules for continuous real-valued functions under arithmetic operations with the usual denominator hypothesis.
FC02-C02-U133	exact match	mathlib	Mathlib/Topology/UniformSpace/UniformConvergence.lean::TendstoUniformly	P	Exact uniform-convergence concept, generalized from sequences/metrics to uniform spaces and filters.
FC02-C02-U134	exact match	mathlib	Mathlib/Topology/UniformSpace/UniformApproximation.lean::TendstoUniformly.continuous	P	Exact uniform limit theorem: a uniform limit of continuous functions is continuous.
FC02-C02-U135	unmatched after search	unmatched	—	N	No searched declaration formalizes Munkres’s specific proof that the box topology on ℝ^ω is nonmetrizable; the box topology is not bundled.
FC02-C02-U136	unmatched after search	unmatched	—	N	No searched declaration formalizes the stated uncountable-product nonmetrizability theorem in this Munkres form. Mathlib’s Pi metrizability instance is restricted by the surrounding [Finite ι] hypothesis.
FC02-C02-U137	exact match	mathlib	Mathlib/Topology/Defs/Induced.lean::Topology.IsQuotientMap	P	Exact quotient-map interface: surjective coinducing map, equivalent to the source final-topology characterization.
FC02-C02-U138	exact match	mathlib	Mathlib/Topology/Defs/Basic.lean::IsOpenMap; IsClosedMap; Topology/Maps/Basic.lean::IsOpenMap.isQuotientMap; closed analogue	P	Exact open/closed-map definitions and theorem that continuous surjective open/closed maps are quotient.
FC02-C02-U139	unmatched after search	unmatched	—	N	No searched declaration packages the source’s specific piecewise interval quotient map example.
FC02-C02-U140	partial match / wrong interface	mathlib	Mathlib/Topology/Constructions/SumProd.lean::isOpenMap_fst; isQuotientMap_fst	P	The projection is generically open and quotient, exactly the positive half; no searched declaration packages the hyperbola xy=1 counterexample proving this concrete projection is not closed.
FC02-C02-U141	exact match	mathlib	TopologicalSpace.coinduced; Topology.IsQuotientMap; IsQuotientMap.eq_coinduced	P	Exact unique quotient/final topology induced by a surjection.
FC02-C02-U142	unmatched after search	unmatched	—	N	No searched declaration packages the concrete quotient from ℝ to three points by sign partition.
FC02-C02-U143	broad match	mathlib	Quotient; Quotient.mk'; Mathlib/Topology/Constructions.lean::isQuotientMap_quotient_mk'	P	A partition/equivalence relation quotient carries exactly the quotient topology in the generic Quotient construction.
FC02-C02-U144	unmatched after search	unmatched	—	N	No searched declaration packages the source’s closed-unit-ball boundary-identification quotient example as stated.
FC02-C02-U145	broad match	mathlib	Set.preimage_image_eq; fiber/equivalence-class APIs	P	The equation p⁻¹(p(A))=A precisely expresses saturation and generic set APIs support it, but no searched named IsSaturated topological predicate matches Munkres’s terminology.
FC02-C02-U146	partial match / wrong interface	mathlib	Quotient/setoid topology infrastructure	P	Generic quotient-by-equivalence-relations handles edge identifications, but the specific square-edge partition example is not a searched named declaration.
FC02-C02-U147	partial match / wrong interface	mathlib	Mathlib/Topology/Constructions.lean::Topology.IsQuotientMap.restrictPreimage_isOpen; open/closed quotient-map APIs	P	Mathlib has restriction results to preimages of open target sets and strong open/closed quotient APIs, but no searched single theorem matches all of Munkres’s saturated-source restriction clauses.
FC02-C02-U148	exact match	mathlib	Mathlib/Topology/Maps/Basic.lean::Topology.IsQuotientMap.continuous_iff; Mathlib/Topology/Constructions.lean::continuous_quot_lift	P	Exact quotient universal property: a fiber-constant map descends, and the descended map is continuous iff its composite with the quotient map is continuous.
FC02-C02-U149	broad match	mathlib	Quotient induced equivalences; IsQuotientMap.continuous_iff; Homeomorph	P	The induced bijection and its continuity/homeomorphism criterion follow from the generic quotient universal property; Mathlib packages the ingredients rather than this source theorem verbatim.
FC02-C02-U150	unmatched after search	unmatched	—	N	No searched declaration packages Munkres’s concrete countable-line-segments quotient example.
FC02-C02-U151	unmatched after search	unmatched	—	N	No searched declaration packages the source counterexample in which a quotient map p has p×id_ℚ non-quotient; generic open-quotient product theorems deliberately require stronger hypotheses.

Provenance contract for C03

• Project search: LeanCategories/** outside .lake was searched first; no project-owned declaration supersedes the foundational connectedness/compactness/local-compactness interfaces below.
• Pinned Mathlib: repository pin db584cd6d46c92f209a44c0f1c829460d327499d (v4.33.0) was declaration-checked across connectedness, path components, order topology/intermediate value, compactness, metric compactness, sequential/countable compactness, local compactness, and one-point compactification.
• Current Mathlib: default branch rechecked 2026-09-05 at 251e86bd1fa42024826ccdb46c3d680edff03e1f; no current-only declaration was needed to upgrade a C03 verdict.
• External search: Loogle/LeanSearch, Reservoir/GitHub Lean, the local source atlas, and web search were checked for the concrete ordered-square, topologist’s-sine-curve, ordinal, and minimal-uncountable-well-order examples. mdnestor/basic_topology@10230d7997436e8be1644d0750ec6b03d845619b remains unlicensed and therefore corroboration only, not a creditable route. No separately licensed formal owner improved the unmatched concrete-example rows.
• Concrete examples remain unmatched unless an existing theorem/declaration actually realizes them; generic infrastructure that could be instantiated in a new proof is not counted as implementation.
• Mathlib/Lean code is Apache-2.0; verdict vocabulary is unchanged from C01–C02.

C03 — Connectedness and Compactness

FC02 ID	Verdict	Route	Lean target(s)	Provenance	Interface comparison
FC02-C03-U001	exact match	mathlib	Mathlib/Topology/Connected/Basic.lean::IsPreconnected; IsConnected	P	Exact no-nontrivial-open-separation definition, with nonemptiness split into IsConnected.
FC02-C03-U002	partial match / wrong interface	mathlib	Mathlib/Topology/Connected/Basic.lean::IsPreconnected.subset_of_closure_inter_subset; subset_left_of_subset_union	P	Mathlib has the exact separation-side lemmas used in the criterion, but not the source characterization phrased as neither side containing a limit point of the other as one declaration.
FC02-C03-U003	unmatched after search	unmatched	—	N	No searched declaration packages Munkres’s concrete two-point indiscrete connected-space example.
FC02-C03-U004	unmatched after search	unmatched	—	N	No searched declaration packages the concrete subspace [-1,0) ∪ (0,1] and its displayed separation.
FC02-C03-U005	exact match	mathlib	Mathlib/Topology/Order/IntermediateValue.lean::isConnected_Icc	P	Exact connectedness of real closed intervals, specializing to [-1,1].
FC02-C03-U006	exact match	mathlib	Mathlib/Topology/Instances/RatLemmas.lean::Rat.TotallyDisconnectedSpace; Topology/Connected/TotallyDisconnected.lean::connectedComponent_eq_singleton	P	Stronger native statement: ℚ is totally disconnected, hence every connected subset is a singleton.
FC02-C03-U007	unmatched after search	unmatched	—	N	No searched declaration packages the concrete plane subset consisting of the x-axis together with the specified hyperbola branch.
FC02-C03-U008	exact match	mathlib	Mathlib/Topology/Connected/Basic.lean::IsPreconnected.subset_left_of_subset_union; subset_right_of_subset_union	P	Exact theorem that a connected/preconnected subset contained in a separation lies entirely in one side once it meets that side.
FC02-C03-U009	exact match	mathlib	Mathlib/Topology/Connected/Basic.lean::isPreconnected_iUnion; IsPreconnected.union	P	Exact common-point union theorem, including arbitrary families.
FC02-C03-U010	exact match	mathlib	Mathlib/Topology/Connected/Basic.lean::IsPreconnected.subset_closure	P	Exact statement A ⊆ B ⊆ closure A preserves preconnectedness, with nonempty version for connectedness.
FC02-C03-U011	exact match	mathlib	Mathlib/Topology/Connected/Basic.lean::IsPreconnected.image; connected image lemmas	P	Exact continuous-image preservation of connectedness.
FC02-C03-U012	exact match	mathlib	Mathlib/Topology/Connected/Basic.lean::IsPreconnected.prod; product connected-space instances	P	Exact finite-product connectedness, in stronger generic product form.
FC02-C03-U013	unmatched after search	unmatched	—	N	No searched declaration formalizes the box-topology counterexample on ℝ^ω; Mathlib has no bundled box topology in this corpus audit.
FC02-C03-U014	exact match	mathlib	Mathlib/Topology/Connected/Basic.lean::isPreconnected_univ_pi	P	Stronger theorem: arbitrary Pi products of preconnected spaces are preconnected, directly covering countable products.
FC02-C03-U015	broad match	mathlib	ConditionallyCompleteLinearOrder; DenselyOrdered; OrderTopology	P	Mathlib represents the two clauses of a linear continuum by standard order typeclasses rather than a LinearContinuum wrapper.
FC02-C03-U016	exact match	mathlib	Mathlib/Topology/Order/IntermediateValue.lean::Set.OrdConnected.isPreconnected; isPreconnected_iff_ordConnected	P	Stronger order-topological theorem: order-convex intervals are exactly the preconnected subsets under the standard completeness hypotheses.
FC02-C03-U017	exact match	mathlib	Mathlib/Order/Interval/Set/Defs.lean::Set.OrdConnected	P	Exact order-convexity notion corresponding to the source definition of a convex subset of an ordered set.
FC02-C03-U018	exact match	mathlib	Mathlib/Topology/Order/IntermediateValue.lean::isPreconnected_iff_ordConnected; isConnected_Icc	P	Exact real-line connected interval theorem; the intermediate value theorem follows from the same API.
FC02-C03-U019	exact match	mathlib	Mathlib/Topology/Order/IntermediateValue.lean::IsPreconnected.intermediate_value	P	Exact generalized intermediate value theorem for a continuous map from a preconnected set into an ordered topological space.
FC02-C03-U020	unmatched after search	unmatched	—	N	No searched declaration packages the lexicographic ordered-square example as a concrete linear continuum.
FC02-C03-U021	unmatched after search	unmatched	—	N	No searched declaration packages the dictionary-ordered X × [0,1) linear-continuum construction from the source.
FC02-C03-U022	exact match	mathlib	Mathlib/Topology/Path.lean::Path; Mathlib/Topology/Connected/PathConnected.lean::IsPathConnected	P	Exact path and path-connectedness data.
FC02-C03-U023	broad match	mathlib	Mathlib/Topology/MetricSpace/Pseudo/Defs.lean::Metric.closedBall; Mathlib/Analysis/Convex/PathConnected.lean::Convex.isPathConnected; convex_closedBall	P	The Euclidean unit ball is a closed convex ball, and nonempty convex subsets are path connected; the source’s named Bⁿ is a specialization.
FC02-C03-U024	exact match	mathlib	Mathlib/Analysis/Convex/PathConnected.lean::Convex.isPathConnected	P	Stronger theorem subsuming the straight-line path construction in every convex real vector-space subset.
FC02-C03-U025	exact match	mathlib	Mathlib/Analysis/Normed/Module/Connected.lean::isPathConnected_compl_singleton_of_one_lt_rank	P	Exact punctured finite-dimensional real-space theorem under rank greater than one.
FC02-C03-U026	exact match	mathlib	Mathlib/Analysis/Normed/Module/Connected.lean::isPathConnected_sphere	P	Exact path-connectedness theorem for spheres in real normed spaces of rank greater than one.
FC02-C03-U027	unmatched after search	unmatched	—	N	No searched declaration packages the ordered square and proves connected-but-not-path-connected.
FC02-C03-U028	unmatched after search	unmatched	—	N	No searched declaration packages the source’s specified plane subset and its path-connectedness behavior.
FC02-C03-U029	unmatched after search	unmatched	—	N	No searched declaration packages the topologist’s sine curve and proves its closure connected but not path connected.
FC02-C03-U030	exact match	mathlib	Mathlib/Topology/Connected/Basic.lean::connectedComponent; connectedComponent_eq_iff_mem	P	Exact connected-component equivalence-class construction.
FC02-C03-U031	exact match	mathlib	Mathlib/Topology/Connected/Basic.lean::isConnected_connectedComponent; connectedComponent_disjoint; IsPreconnected.subset_connectedComponent; isClosed_connectedComponent	P	Exact component connectedness, disjointness/maximality, covering behavior and closedness.
FC02-C03-U032	exact match	mathlib	Mathlib/Topology/Connected/PathConnected.lean::pathComponent; mem_pathComponent_iff	P	Exact path-component equivalence-class construction.
FC02-C03-U033	partial match / wrong interface	mathlib	Mathlib/Topology/Connected/PathConnected.lean::pathComponent_subset_component; Mathlib/Topology/Connected/Basic.lean::isClosed_connectedComponent; Mathlib/Topology/Connected/LocallyPathConnected.lean::IsOpen.pathComponent	P	Mathlib has the structural component/path-component theorems, but the row also records source counterexamples showing path components need not be open or closed and the finite-components-open corollary; no one declaration packages all clauses.
FC02-C03-U034	partial match / wrong interface	mathlib	Rat.TotallyDisconnectedSpace; Topology/Connected/TotallyDisconnected.lean::connectedComponent_eq_singleton	P	Mathlib exactly proves that all connected components of ℚ are singletons. The row also asserts that none of those components is open; no searched public declaration packages that nondiscreteness clause for the components, so the complete source example is not an exact match.
FC02-C03-U035	unmatched after search	unmatched	—	N	No searched declaration packages the topologist’s sine curve component/path-component computation.
FC02-C03-U036	exact match	mathlib	Mathlib/Topology/Connected/LocallyConnected.lean::LocallyConnectedSpace; Mathlib/Topology/Connected/LocallyPathConnected.lean::LocallyPathConnectedSpace	P	Exact local connectedness and local path-connectedness notions.
FC02-C03-U037	partial match / wrong interface	mathlib	Mathlib/Topology/Order/IntermediateValue.lean::isPreconnected_iff_ordConnected; Mathlib/Topology/Instances/RatLemmas.lean::Rat.TotallyDisconnectedSpace	P	Several standard interval/rational examples are covered structurally, but the row also includes the punctured-interval and sine-curve examples without a complete bundled formal owner.
FC02-C03-U038	exact match	mathlib	Mathlib/Topology/Connected/LocallyConnected.lean::locallyConnectedSpace_iff_connectedComponentIn_open	P	Exact characterization by openness of components of every open subspace.
FC02-C03-U039	exact match	mathlib	Mathlib/Topology/Connected/LocallyPathConnected.lean::locallyPathConnectedSpace_iff_isOpen_pathComponentIn	P	Exact characterization by openness of path components of every open subspace.
FC02-C03-U040	exact match	mathlib	Mathlib/Topology/Connected/PathConnected.lean::pathComponent_subset_component; Mathlib/Topology/Connected/LocallyPathConnected.lean::pathComponent_eq_connectedComponent	P	Exact inclusion in general and equality in locally path-connected spaces.
FC02-C03-U041	broad match	mathlib	Set-indexed families; IsOpen	P	Open covers are represented directly as indexed families of open sets; the source row is terminology rather than a separate structure.
FC02-C03-U042	exact match	mathlib	Mathlib/Topology/Defs/Filter.lean::IsCompact; Mathlib/Topology/Compactness/Compact.lean::isCompact_iff_finite_subcover	P	Exact finite-subcover characterization of compactness.
FC02-C03-U043	unmatched after search	unmatched	—	N	No searched declaration packages the concrete open cover {(n,n+2)} witnessing noncompactness of ℝ.
FC02-C03-U044	unmatched after search	unmatched	—	N	No searched declaration packages the concrete compact subset {0} ∪ {1/n} as this source example.
FC02-C03-U045	exact match	mathlib	Mathlib/Topology/Compactness/Compact.lean::Set.Finite.isCompact; Finite.compactSpace	P	Stronger exact theorem: every finite subset is compact, and every finite topological space is compact.
FC02-C03-U046	unmatched after search	unmatched	—	N	No searched declaration packages the concrete cover (1/n,1] witnessing noncompactness of (0,1].
FC02-C03-U047	exact match	mathlib	Mathlib/Topology/Compactness/Compact.lean::isCompact_iff_compactSpace; subtype compactness interface	P	Exact equivalence between compactness of a subset and compactness of the corresponding subtype, which is the ambient-open-cover reformulation.
FC02-C03-U048	exact match	mathlib	Mathlib/Topology/Compactness/Compact.lean::IsClosed.isCompact	P	Exact theorem that a closed subset of a compact space is compact.
FC02-C03-U049	exact match	mathlib	Mathlib/Topology/Separation/Hausdorff.lean::IsCompact.isClosed	P	Exact theorem that compact subsets of Hausdorff spaces are closed.
FC02-C03-U050	exact match	mathlib	Mathlib/Topology/Separation/Hausdorff.lean::IsCompact.separation_of_notMem	P	Exact compact-set/point separation by disjoint open neighborhoods in a Hausdorff space.
FC02-C03-U051	broad match	mathlib	Mathlib/Topology/Order/Compact.lean::isCompact_Icc	P	Exact compactness of closed intervals subsumes the source interval examples; open/half-open failures are not separately packaged as this examples list.
FC02-C03-U052	unmatched after search	unmatched	—	N	The cofinite topology itself is bundled, but no searched declaration states the source’s concrete claim that every subset of an infinite cofinite space is compact; generic definitions alone are not credited as the example proof.
FC02-C03-U053	exact match	mathlib	Mathlib/Topology/Compactness/Compact.lean::IsCompact.image	P	Exact theorem that continuous images of compact sets are compact.
FC02-C03-U054	exact match	mathlib	Mathlib/Topology/Homeomorph/Lemmas.lean::Continuous.homeoOfEquivCompactToT2	P	Exact theorem: a continuous equivalence from a compact space to a Hausdorff space is a homeomorphism.
FC02-C03-U055	exact match	mathlib	Mathlib/Topology/Compactness/Compact.lean::IsCompact.prod	P	Exact finite-product compactness theorem.
FC02-C03-U056	exact match	mathlib	Mathlib/Topology/Compactness/Compact.lean::generalized_tube_lemma	P	Stronger generalized tube lemma for compact sets in both factors.
FC02-C03-U057	unmatched after search	unmatched	—	N	No searched declaration packages the source counterexample showing the tube lemma fails when the compactness hypothesis is removed.
FC02-C03-U058	exact match	mathlib	Mathlib/Topology/Compactness/Compact.lean::isCompact_univ_pi	P	Exact Tychonoff theorem for arbitrary products of compact sets/spaces.
FC02-C03-U059	broad match	mathlib	Mathlib/Topology/Compactness/Compact.lean::IsCompact.elim_finite_subfamily_closed; IsCompact.inter_iInter_nonempty	P	The finite-intersection property is represented directly by finite subfamily/intersection lemmas rather than a named FiniteIntersectionProperty predicate.
FC02-C03-U060	exact match	mathlib	Mathlib/Topology/Compactness/Compact.lean::IsCompact.elim_finite_subfamily_closed; isCompact_iff_finite_subcover	P	The dual closed-set finite-intersection characterization is exactly formalized by these equivalent compactness lemmas.
FC02-C03-U061	broad match	mathlib	Mathlib/Topology/Order/Compact.lean::ConditionallyCompleteLinearOrder.isCompact_Icc	P	Mathlib proves compactness of closed intervals for ConditionallyCompleteLinearOrders. Munkres assumes only the least-upper-bound property; in a linear order the corresponding greatest-lower-bound property is derivable, but the searched public theorem uses the stronger bundled conditionally-complete interface rather than the source-shaped hypothesis.
FC02-C03-U062	exact match	mathlib	Mathlib/Topology/Order/Compact.lean::isCompact_Icc	P	Exact compactness of real closed intervals.
FC02-C03-U063	exact match	mathlib	Mathlib/Topology/MetricSpace/Bounded.lean::isCompact_iff_isClosed_bounded; finite-dimensional ProperSpace instances	P	Exact Heine–Borel theorem in proper metric spaces, directly covering finite-dimensional Euclidean space.
FC02-C03-U064	partial match / wrong interface	mathlib	Mathlib/Topology/MetricSpace/ProperSpace.lean::isCompact_sphere; isCompact_closedBall	P	Sphere and closed-ball compactness are exact; the row’s additional source-specific compact graph example is not packaged by the searched declarations.
FC02-C03-U065	exact match	mathlib	Mathlib/Topology/Order/Compact.lean::IsCompact.exists_isMinOn; exists_isMaxOn	P	Exact extreme-value theorem for continuous functions on nonempty compact sets.
FC02-C03-U066	exact match	mathlib	Mathlib/Topology/MetricSpace/HausdorffDistance.lean::Metric.infDist; continuous_infDist_pt	P	Exact distance-to-a-set infimum and continuity interface.
FC02-C03-U067	exact match	mathlib	Mathlib/Topology/UniformSpace/Compact.lean::lebesgue_number_lemma	P	Stronger uniform-space Lebesgue-number lemma, specializing to compact metric spaces.
FC02-C03-U068	broad match	mathlib	Mathlib/Topology/UniformSpace/Compact.lean::lebesgue_number_lemma	P	The source term “Lebesgue number” is represented by the theorem’s entourage/radius witness rather than a separate named object.
FC02-C03-U069	exact match	mathlib	Mathlib/Topology/MetricSpace/Pseudo/Defs.lean::Metric.uniformContinuous_iff	P	Exact epsilon-delta characterization of uniform continuity in metric spaces.
FC02-C03-U070	exact match	mathlib	Mathlib/Topology/UniformSpace/HeineCantor.lean::IsCompact.uniformContinuousOn_of_continuous	P	Exact Heine–Cantor theorem on compact subsets, stronger uniform-space form.
FC02-C03-U071	exact match	mathlib	Mathlib/Topology/Neighborhoods.lean::isOpen_singleton_iff_nhds_eq_pure	P	Exact characterization of an isolated point by openness of its singleton/neighborhood filter being pure.
FC02-C03-U072	unmatched after search	unmatched	—	N	No searched declaration proves the full source theorem that every nonempty compact Hausdorff space with no isolated points is uncountable. Existing perfect-set cardinality theorems found in Mathlib impose second-countability/Polish hypotheses.
FC02-C03-U073	exact match	mathlib	Mathlib/Analysis/Real/Cardinality.lean::Real.Icc_countable_iff	P	Exact cardinality consequence: a nondegenerate closed real interval is not countable, hence uncountable.
FC02-C03-U074	partial match / wrong interface	mathlib	Mathlib/Topology/Compactness/CountablyCompact.lean::IsCountablyCompact.exists_accPt_of_infinite; isCountablyCompact_iff_infinite_subset_has_accPt	P	Mathlib has the Bolzano–Weierstrass predicate and proves the forward accumulation-point theorem generally, but its equivalence with IsCountablyCompact assumes T1Space. Munkres defines limit-point compactness for an arbitrary topological space, and no searched standalone library predicate has exactly that unconditional interface.
FC02-C03-U075	partial match / wrong interface	mathlib	Mathlib/Topology/Compactness/CountablyCompact.lean::IsCompact.isCountablyCompact	P	The implication compact ⇒ limit-point/countably compact is exact; the row’s converse-failure counterexample is not itself a searched declaration.
FC02-C03-U076	unmatched after search	unmatched	—	N	No searched declaration packages the source ℤ₊ × {0,1} indiscrete-factor counterexample.
FC02-C03-U077	unmatched after search	unmatched	—	N	No searched Lean declaration packages the minimal uncountable well-ordered set with its limit-point-compact but noncompact topology; external web search likewise found exposition rather than Lean formalization.
FC02-C03-U078	broad match	mathlib	Mathlib/Topology/Sequences.lean::IsSeqCompact; SeqCompactSpace	P	The source teaser/definition of sequential compactness is the library’s native sequence compactness predicate/interface.
FC02-C03-U079	exact match	mathlib	Mathlib/Topology/Sequences.lean::IsSeqCompact; subsequence convergence interface	P	Exact sequential compactness notion: every sequence in the set has a convergent subsequence with limit in the set.
FC02-C03-U080	exact match	mathlib	Mathlib/Topology/Sequences.lean::isCompact_iff_isSeqCompact; Mathlib/Topology/Compactness/CountablyCompact.lean::isCountablyCompact_iff_isSeqCompact	P	Exact metrizable equivalences among compactness, sequential compactness, and countable/limit-point compactness.
FC02-C03-U081	unmatched after search	unmatched	—	N	No searched declaration packages the source ordinal-space examples separating these compactness notions outside the metrizable setting.
FC02-C03-U082	exact match	mathlib	Mathlib/Topology/Defs/Filter.lean::LocallyCompactSpace	P	Exact local compactness interface: compact neighborhoods form a neighborhood basis in the source-equivalent filter formulation.
FC02-C03-U083	partial match / wrong interface	mathlib	Mathlib/Topology/MetricSpace/ProperSpace.lean::ProperSpace ℝ; local-compact instances from proper spaces	P	The real-line local compactness is native; no searched declaration packages the source assertion that ℚ with its usual topology is not locally compact.
FC02-C03-U084	partial match / wrong interface	mathlib	finite-dimensional Euclidean ProperSpace; Mathlib/Topology/Compactness/LocallyCompact.lean::Pi.locallyCompactSpace_of_finite	P	Finite-dimensional Euclidean local compactness is native; no searched theorem packages non-local-compactness of the countable product ℝ^ω.
FC02-C03-U085	partial match / wrong interface	mathlib	Mathlib/Topology/Order/Compact.lean::ConditionallyCompleteLinearOrder.isCompact_Icc	P	Compact order intervals provide the core theorem, but no searched declaration packages the full source implication “simply ordered with LUB property ⇒ locally compact” as a LocallyCompactSpace instance.
FC02-C03-U086	exact match	mathlib	Mathlib/Topology/Compactification/OnePoint/Basic.lean::OnePoint; OnePoint.isOpenEmbedding_coe; compact/normal instances; OnePoint.equivOfIsEmbeddingOfRangeEq; Mathlib/Topology/Compactness/LocallyCompact.lean::IsOpen.locallyCompactSpace	P	Together these declarations give both directions of the source characterization and the uniqueness clause: an LCH space has a compact Hausdorff one-point extension, while the embedded complement of the added point is an open locally compact subspace of any compact Hausdorff extension, and two such extensions are homeomorphic relative to X.
FC02-C03-U087	partial match / wrong interface	mathlib	Mathlib/Topology/Compactification/OnePoint/Basic.lean::OnePoint; OnePoint.isOpenEmbedding_coe; OnePoint.isDenseEmbedding_coe	P	Mathlib has the exact one-point compactification object and, for noncompact X, its dense open embedding. The row also defines the generic notion of an arbitrary compactification X ⊂ Y; no searched generic Compactification structure/predicate packages that first clause, so the complete definition row is only partially matched.
FC02-C03-U088	exact match	mathlib	Mathlib/Topology/Compactification/OnePoint/Sphere.lean::onePointEquivSphereOfFinrankEq	P	Stronger theorem: the one-point compactification of every finite-dimensional real vector space is homeomorphic to the appropriate unit sphere, covering ℝ and ℝ².
FC02-C03-U089	broad match	mathlib	Mathlib/Topology/Compactification/OnePoint/Sphere.lean::onePointEquivSphereOfFinrankEq; Mathlib/Topology/Compactification/OnePoint/ProjectiveLine.lean::OnePoint.equivProjectivization	P	The extended real/complex and sphere/projective-line examples are covered by stronger generic one-point compactification equivalences, though not all source notation is packaged verbatim.
FC02-C03-U090	exact match	mathlib	Mathlib/Topology/Separation/Regular.lean::IsCompact.exists_isOpen_closure_subset; Topology/Separation/Basic.lean::exists_isOpen_mem_isCompact_closure	P	Exact shrinking/compact-closure neighborhood machinery in locally compact Hausdorff (regular) spaces.
FC02-C03-U091	exact match	mathlib	Mathlib/Topology/Compactness/LocallyCompact.lean::IsOpen.locallyCompactSpace; IsClosed.locallyCompactSpace	P	Exact inheritance of local compactness by open and closed subspaces under the corresponding hypotheses.
FC02-C03-U092	broad match	mathlib	Mathlib/Topology/Compactification/OnePoint/Basic.lean::OnePoint.isOpenEmbedding_coe; compact-space instance; Mathlib/Topology/Compactness/LocallyCompact.lean::IsOpen.locallyCompactSpace; OnePoint.equivOfIsEmbeddingOfRangeEq	P	The two directions of the characterization are present as composable generic declarations: LCH spaces embed openly in compact Hausdorff one-point compactifications, while open subspaces of compact Hausdorff spaces are locally compact.

Provenance contract for C04

• Project-first search found no project-owned replacement for the foundational countability/separation/manifold units.
• Pinned Mathlib db584cd6d46c92f209a44c0f1c829460d327499d (v4.33.0) and current upstream 4cbb42e75a050e830b7cf0f2ae748d7644f59cf7 were declaration-checked for bases/countability, Lindelöf/separable spaces, separation axioms, Urysohn/Tietze, partitions of unity, manifolds, and Whitney embedding.
• Loogle/LeanSearch, Reservoir/GitHub Lean, the source atlas, and 2026-09-05 web/GitHub searches found the pinned/importable Counterexamples/SorgenfreyLine.lean owner for the Sorgenfrey line/plane topology, first-countability, separability, complete normality, failure of second countability, and failure of normality of the plane. No creditable owner was found for the missing Sorgenfrey Lindelöf claims or for the K-topology, ordered-square, ordinal-product, or uncountable-product counterexamples. mdnestor/basic_topology remains unlicensed corroboration only.
• P/N provenance codes are as defined above; concrete examples are not credited merely because generic infrastructure could prove them.

C04 — Countability and Separation Axioms

FC02 ID	Verdict	Route	Lean target(s)	Provenance	Interface comparison
FC02-C04-U001	exact match	mathlib	Mathlib/Topology/Bases.lean::FirstCountableTopology	P	Exact countable-neighborhood-basis condition, encoded as countable generation of each 𝓝 x.
FC02-C04-U002	exact match	mathlib	FirstCountableTopology; countable basis API for 𝓝 x	P	This is the native formulation: first countability is precisely countable generation of every neighborhood filter.
FC02-C04-U003	exact match	mathlib	Mathlib/Topology/Sequences.lean::mem_closure_iff_seq_limit; Continuous.seqContinuous; continuous_iff_seqContinuous; FirstCountableTopology.frechetUrysohnSpace	P	Exact sequence/closure and sequence/continuity characterizations; Mathlib states them through Fréchet–Urysohn/sequential spaces, with first countability supplying the instances.
FC02-C04-U004	exact match	mathlib	Mathlib/Topology/Bases.lean::SecondCountableTopology; TopologicalSpace.exists_countable_basis	P	Exact second-countability notion and an explicit countable topological basis theorem.
FC02-C04-U005	broad match	mathlib	SecondCountableTopology ℝ; countable-product instance for SecondCountableTopology (∀ i, X i)	P	The standard real and finite/countable products are second countable; Mathlib packages this through typeclass/product infrastructure rather than the source’s explicit rational-endpoint bases.
FC02-C04-U006	partial match / wrong interface	mathlib	Mathlib/Topology/Compactness/Lindelof.lean::countable_of_Lindelof_of_discrete; SecondCountableTopology.toHereditarilyLindelof	P	The lemma that discrete subspaces of second-countable spaces are countable follows exactly; Munkres’s separate uniform topology on ℝ^ω is not bundled, so the concrete first-but-not-second-countable example is not owned.
FC02-C04-U007	exact match	mathlib	Subtype.firstCountableTopology; Subtype.secondCountableTopology; countable Pi instances for both classes	P	Exact preservation by subspaces and countable products.
FC02-C04-U008	exact match	mathlib	Mathlib/Topology/Defs/Basic.lean::Dense; dense_iff_closure_eq	P	Exact dense-subset notion, equivalent to closure equal to the whole space.
FC02-C04-U009	exact match	mathlib	SecondCountableTopology.toHereditarilyLindelof; SecondCountableTopology.to_separableSpace	P	Stronger native result: second countability implies hereditary Lindelöfness and separability, hence the two source conclusions.
FC02-C04-U010	exact match	mathlib	Mathlib/Topology/Compactness/Lindelof.lean::LindelofSpace; Mathlib/Topology/Bases.lean::SeparableSpace	P	Exact Lindelöf and separable typeclasses.
FC02-C04-U011	partial match / wrong interface	mathlib	Counterexamples/SorgenfreyLine.lean::Counterexample.SorgenfreyLine.instFirstCountableTopology; instSeparableSpace; not_secondCountableTopology	P	The pinned module proves first countability, separability, and failure of second countability for the Sorgenfrey line. The source row also includes its Lindelöf property; no searched completed declaration proves that clause, so the bundled example remains partial.
FC02-C04-U012	partial match / wrong interface	mathlib	Counterexamples/SorgenfreyLine.lean::Counterexample.SorgenfreyLine; Counterexample.SorgenfreyLine.not_normalSpace_prod; antidiagonal declarations	P	The exact Sorgenfrey line/plane objects and the standard nonnormal plane obstruction are formalized. The source claim here is specifically Lindelöfness of the line and failure of Lindelöfness of the square; those two Lindelöf declarations were not found, so this is only a partial concrete owner.
FC02-C04-U013	unmatched after search	unmatched	—	N	No searched Lean declaration packages the ordered-square subspace counterexample to hereditary Lindelöfness.
FC02-C04-U014	exact match	mathlib	Mathlib/Topology/Separation/Hausdorff.lean::T2Space	P	Exact Hausdorff axiom.
FC02-C04-U015	exact match	mathlib	Mathlib/Topology/Separation/Regular.lean::RegularSpace; NormalSpace; T3Space; T4Space	P	Exact point/closed-set and disjoint-closed-set separation interfaces; the T3/T4 wrappers add the source T1 hypotheses.
FC02-C04-U016	broad match	mathlib	T1Space; T2Space; T3Space; T4Space	P	The source hierarchy terminology is exactly represented by Mathlib’s standard separation typeclasses.
FC02-C04-U017	exact match	mathlib	Mathlib/Topology/Separation/Regular.lean::regularSpace_TFAE; normal_exists_closure_subset	P	Exact closure-shrinking characterizations for regular and normal spaces.
FC02-C04-U018	exact match	mathlib	subtype/product T2 instances; Mathlib/Topology/Separation/Regular.lean::RegularSpace subtype/product/Pi instances	P	Exact preservation of Hausdorffness and regularity by subspaces and products.
FC02-C04-U019	unmatched after search	unmatched	—	N	No searched declaration bundles Munkres’s K-topology on ℝ; hence its Hausdorff-but-not-regular counterexample has no formal owner.
FC02-C04-U020	broad match	mathlib	Counterexamples/SorgenfreyLine.lean::Counterexample.SorgenfreyLine.instCompletelyNormalSpace	P	Stronger than the source conclusion: the Sorgenfrey line is formalized as completely normal, hence normal.
FC02-C04-U021	exact match	mathlib	Counterexamples/SorgenfreyLine.lean::Counterexample.SorgenfreyLine.instCompletelyNormalSpace; Counterexample.SorgenfreyLine.not_normalSpace_prod	P	The line is completely normal (hence regular and normal) while its square is proved not normal. This realizes both advertised uses: regular need not imply normal and products of normal spaces need not be normal.
FC02-C04-U022	exact match	mathlib	Mathlib/Topology/Separation/Regular.lean::NormalSpace.of_regularSpace_secondCountableTopology	P	Exact theorem: regular plus second countable implies normal.
FC02-C04-U023	exact match	mathlib	Mathlib/Topology/GDelta/MetrizableSpace.lean normal-space instance for PseudoMetrizableSpace; T4 instance for MetrizableSpace	P	Stronger native theorem: every (pseudo)metrizable space is normal; metrizable spaces are T4.
FC02-C04-U024	exact match	mathlib	Mathlib/Topology/Separation/Regular.lean::NormalSpace.of_compactSpace_r1Space	P	Stronger theorem: compact R1 spaces are normal; compact Hausdorff spaces satisfy the hypotheses.
FC02-C04-U025	exact match	mathlib	Mathlib/Topology/Order/T5.lean::OrderTopology.completelyNormalSpace; OrderTopology.t5Space	P	Stronger exact result: every linear order with its order topology is completely normal/T5, subsuming well-ordered spaces.
FC02-C04-U026	unmatched after search	unmatched	—	N	No searched declaration proves Munkres’s concrete nonnormality theorem for an uncountable product ℝ^J.
FC02-C04-U027	unmatched after search	unmatched	—	N	No searched declaration packages S_Ω × ar S_Ω and proves the source nonnormality counterexample.
FC02-C04-U028	exact match	mathlib	Mathlib/Topology/UrysohnsLemma.lean::exists_continuous_zero_one_of_isClosed	P	Exact Urysohn lemma for disjoint closed sets in a normal space, with [0,1] range; affine rescaling gives [a,b].
FC02-C04-U029	broad match	mathlib	exists_continuous_zero_one_of_isClosed	P	Mathlib represents “separated by a continuous function” by the corresponding existence theorem rather than a separate named predicate.
FC02-C04-U030	exact match	mathlib	Mathlib/Topology/Separation/CompletelyRegular.lean::T35Space; CompletelyRegularSpace	P	Munkres includes T1 in “completely regular”; Mathlib separates the function-separation property as CompletelyRegularSpace and packages the T0/T1-strengthened source notion as T35Space.
FC02-C04-U031	exact match	mathlib	Topology.IsEmbedding.t35Space; subtype T35 instance; Pi/product T35 instances in CompletelyRegular.lean	P	Exact inheritance by subspaces and arbitrary products.
FC02-C04-U032	partial match / wrong interface	mathlib	Counterexamples/SorgenfreyLine.lean::Counterexample.SorgenfreyLine.instCompletelyNormalSpace; Counterexample.SorgenfreyLine.not_normalSpace_prod	P	The Sorgenfrey-plane half is realized: complete normality of each line factor gives complete regularity/regularity of the product, while the plane is not normal. The separate ordinal-product example S_Ω × S̄_Ω remains unmatched.
FC02-C04-U033	exact match	mathlib	Mathlib/Topology/Metrizable/Urysohn.lean::metrizableSpace_of_t3_secondCountable; PseudoMetrizableSpace.of_regularSpace_secondCountableTopology	P	Exact Urysohn metrization theorem, in T3/regular second-countable forms.
FC02-C04-U034	partial match / wrong interface	mathlib	Mathlib/Topology/Metrizable/Urysohn.lean::exists_isInducing_l_infty; generic Pi IsEmbedding infrastructure	P	Mathlib realizes the countable-basis embedding construction used for metrization, but no searched declaration matches Munkres’s arbitrary real-valued family/support-separation embedding theorem in its stated generality.
FC02-C04-U035	partial match / wrong interface	mathlib	Mathlib/Topology/Separation/CompletelyRegular.lean::isEmbedding_stoneCechUnit; t35Space_iff_isEmbedding_stoneCechUnit	P	Exact T3.5 embedding characterization into the Stone–Čech compactification, but no searched theorem gives the source’s explicit embedding into a cube [0,1]^J.
FC02-C04-U036	exact match	mathlib	Mathlib/Topology/TietzeExtension.lean::ContinuousMap.exists_restrict_eq; exists_restrict_eq_forall_mem_of_closed; Real.instTietzeExtension	P	Exact Tietze extension theorem for real-valued maps on closed subsets of normal spaces; the interval-valued version is covered by the convex-range theorem/Tietze instances.
FC02-C04-U037	partial match / wrong interface	mathlib	Mathlib/Geometry/Manifold/ChartedSpace.lean::ChartedSpace; Geometry/Manifold/IsManifold/Basic.lean::IsManifold	P	Mathlib has local Euclidean chart/manifold structures, but deliberately does not bake Hausdorffness and second countability into ChartedSpace/IsManifold; those are separate hypotheses, so the interface is not declaration-identical to Munkres’s topological-manifold definition.
FC02-C04-U038	unmatched after search	unmatched	—	N	No searched declaration uses Munkres’s terminology “curve” for 1-manifold or “surface” for 2-manifold as a foundational type/predicate.
FC02-C04-U039	exact match	mathlib	Mathlib/Topology/Algebra/Support.lean::tsupport	P	Exact topological support: closure of the nonzero support.
FC02-C04-U040	exact match	mathlib	Mathlib/Topology/PartitionOfUnity.lean::PartitionOfUnity; PartitionOfUnity.IsSubordinate	P	Stronger native definition: locally finite continuous nonnegative functions summing to one, with subordination by topological support; the finite-cover notion is its finite-index specialization.
FC02-C04-U041	exact match	mathlib	Mathlib/Topology/PartitionOfUnity.lean::PartitionOfUnity.exists_isSubordinate_of_locallyFinite	P	Exact existence theorem for a partition subordinate to a locally finite open cover in a normal space; finite covers are automatically locally finite.
FC02-C04-U042	partial match / wrong interface	mathlib	Mathlib/Geometry/Manifold/WhitneyEmbedding.lean::exists_embedding_euclidean_of_compact	P	Mathlib proves a stronger smooth Euclidean embedding with closed embedding and injective differential, but assumes a smooth manifold structure; Munkres’s theorem needs only the topological m-manifold hypotheses.

Provenance contract for C05

• Project-first, pinned/current Mathlib, ecosystem/GitHub/source-atlas and 2026-09-05 web searches were rechecked. Mathlib owns Tychonoff, ultrafilter maximal-extension machinery, and Stone–Čech with its universal property; no creditable Lean owner was found for the four concrete compactification examples.
• Mathlib’s StoneCech construction is ultrafilter/T2-quotient based, not Munkres’s product-of-intervals construction; construction-sensitive rows are marked partial rather than silently conflated. P/N are the provenance codes defined above.

C05 — The Tychonoff Theorem

FC02 ID	Verdict	Route	Lean target(s)	Provenance	Interface comparison
FC02-C05-U001	broad match	mathlib	Mathlib/Order/Filter/Ultrafilter/Basic.lean::Ultrafilter.exists_ultrafilter_of_finite_inter_nonempty	P	Stronger equivalent maximal-extension principle: every finite-intersection family extends to the set-family of an ultrafilter, i.e. a maximal proper filter.
FC02-C05-U002	broad match	mathlib	Ultrafilter.inter_mem; Ultrafilter.mem_of_superset; Ultrafilter.le_of_inf_neBot	P	The maximal-FIP closure/intersection tests are native ultrafilter laws; Mathlib packages them as filter membership rather than Munkres’s raw family D.
FC02-C05-U003	exact match	mathlib	Mathlib/Topology/Compactness/Compact.lean::isCompact_univ_pi	P	Exact Tychonoff theorem for arbitrary products of compact spaces.
FC02-C05-U004	broad match	mathlib	Topology.IsDenseEmbedding; CompactSpace; T2Space	P	Mathlib has exactly the data comprising a compactification, but no searched bundled Compactification structure/equivalence notion.
FC02-C05-U005	unmatched after search	unmatched	—	N	No searched declaration packages the theorem constructing the compactification induced by an arbitrary embedding by taking the closure of its image, nor its equivalence uniqueness.
FC02-C05-U006	unmatched after search	unmatched	—	N	No searched declaration packages the specific (0,1) → S¹, t ↦ (cos 2πt,sin 2πt) compactification example.
FC02-C05-U007	unmatched after search	unmatched	—	N	No searched declaration packages [0,1] as the two-end compactification of (0,1) in this source form.
FC02-C05-U008	unmatched after search	unmatched	—	N	No searched declaration packages the sine-graph closure compactification example in [-1,1]².
FC02-C05-U009	unmatched after search	unmatched	—	N	No searched declaration proves the source iff criterion for extending bounded continuous (0,1) → ℝ functions to its one-point compactification via the two endpoint limits.
FC02-C05-U010	partial match / wrong interface	mathlib	Mathlib/Topology/Compactification/StoneCech.lean::StoneCech; stoneCechUnit	P	The resulting Stone–Čech object is native, but Mathlib constructs it from ultrafilters and a T2 quotient, not by the source embedding into a product of compact intervals followed by closure.
FC02-C05-U011	exact match	mathlib	StoneCech; isDenseEmbedding_stoneCechUnit; stoneCechExtend; continuous_stoneCechExtend	P	For Munkres-completely-regular (T3.5) spaces, stoneCechUnit is a dense embedding into compact Hausdorff StoneCech X; Mathlib proves the stronger extension property for every compact Hausdorff codomain, hence bounded real maps.
FC02-C05-U012	exact match	mathlib	Mathlib/Topology/DenseEmbedding.lean::Continuous.ext_on	P	Exact uniqueness principle: continuous maps into a Hausdorff space agreeing on a dense subset agree on its closure/domain; specialize to A dense in closure A.
FC02-C05-U013	exact match	mathlib	Mathlib/Topology/Compactification/StoneCech.lean::stoneCechExtend; stoneCechExtend_extends; continuous_stoneCechExtend; stoneCech_hom_ext	P	Exact stronger universal property: every continuous map to any compact Hausdorff target extends uniquely.
FC02-C05-U014	partial match / wrong interface	mathlib	stoneCech_hom_ext; universal property of StoneCech	P	Mathlib proves uniqueness of maps out of StoneCech, but has no searched bundled theorem comparing two arbitrary compactifications satisfying the extension property by a homeomorphism fixing X.
FC02-C05-U015	exact match	mathlib	Mathlib/Topology/Compactification/StoneCech.lean::StoneCech; stoneCechUnit; stoneCechExtend; stoneCech_hom_ext	P	Exact βX object and its compact-Hausdorff universal property; under T35Space X, stoneCechUnit is the required dense embedding.

Provenance contract for C06

• Project search: LeanCategories/** outside .lake was searched first; no project-owned general-topology declarations supersede the C06 local-finiteness/metrization/paracompactness interfaces.
• Pinned Mathlib: db584cd6d46c92f209a44c0f1c829460d327499d (v4.33.0, Apache-2.0) was declaration-checked for LocallyFinite, Gδ/perfect normality, paracompactness, shrinking lemmas, partitions of unity, metric-space paracompactness, and the relevant counterexample source. import Counterexamples.SorgenfreyLine compiles against this exact pin, so that module is credited as pinned mathlib, not as an external/reference-only source.
• Current/open Mathlib: default branch was rechecked at 4cbb42e75a050e830b7cf0f2ae748d7644f59cf7 on 2026-09-05. Open PR #41676 at cd6d319518617a42e975351cde7e6f20dac12512 proves Bing–Nagata–Smirnov and sigma-discrete refinements; PR #41719 at cede174dcee855873dc8d81a7b998a07407e903c proves the regular-space paracompact TFAE and regular-Lindelöf theorem; PR #41962 at bdf021dde563eb64202fee8732b82066c5b2593d supplies the ω₁ hereditary-paracompactness counterexample. These are Apache-2.0 reference implementations, not pinned/importable declarations.
• External packages: felixpernegger/pibase-lean@ff65933ec375d67a44013e4a26140893cab27acb (Apache-2.0) defines PiBase.LocallyMetrizableSpace exactly, but its toolchain is Lean v4.33.0-rc2 and its Mathlib manifest is 639923353ff2…, so compatibility with the repository pin is not exact and the definition is recorded as reference-port. Broad GitHub/Reservoir searches found no Lean proof of the Smirnov metrization theorem.
• mdnestor/basic_topology@10230d7997436e8be1644d0750ec6b03d845619b has no corresponding §§39–42 implementation and remains unlicensed. formal-conjectures searches returned no relevant Nagata/Smirnov/paracompactness statements.
• Loogle/LeanSearch were attempted for local finiteness, Gδ, paracompactness, and the two named metrization theorems; the remote probe timed out after 30 seconds, so no negative verdict relies on that failed service call. Negative rows are instead grounded in project, pinned/current/open-Mathlib, package, source-atlas, Reservoir/GitHub, and broad code searches.

C06 — Local Finiteness and Metrization

FC02 ID	Verdict	Route	Lean target(s)	Provenance	Interface comparison
FC02-C06-U001	exact match	mathlib	Mathlib/Topology/LocallyFinite.lean::LocallyFinite	P	Exact indexed-family definition: every point has a neighborhood meeting only finitely many family members.
FC02-C06-U002	broad match	mathlib	Mathlib/Topology/Order/AtTopBotIxx.lean::locallyFinite_Ioo_of_tendsto	P	The general theorem makes interval families with endpoints diverging at both ends locally finite; the concrete family (n,n+2), n : ℤ, is a direct specialization, but is not separately named.
FC02-C06-U003	exact match	mathlib	LocallyFinite.comp_injective / on_range; LocallyFinite.closure; LocallyFinite.closure_iUnion	P	These give the three clauses: subfamilies/reindexings remain locally finite, closures remain locally finite, and closure commutes with the union of a locally finite family.
FC02-C06-U004	exact match	mathlib	Mathlib/Topology/LocallyFinite.lean::LocallyFinite	P	The library definition is already indexed and counts indices, exactly matching the source formulation.
FC02-C06-U005	broad match	mathlib	LocallyFinite; sigma-family shape b : ℕ → Set (Set X) / ∀ n, LocallyFinite ((↑) : b n → Set X)	P	Mathlib has the local-finiteness predicate and the exact sigma-locally-finite data shape used by current metrization work, but no pinned named SigmaLocallyFinite predicate for this collection-level definition.
FC02-C06-U006	broad match	mathlib	set inclusion; ParacompactSpace.locallyFinite_refinement; precise_refinement	P	Refinement is represented directly by the containment condition ∀ b, ∃ a, t b ⊆ s a; openness/closedness are ordinary predicates rather than a separate refinement structure.
FC02-C06-U007	exact match	reference-port	mathlib4 PR #41676 cd6d319518617a42e975351cde7e6f20dac12512, Mathlib/Topology/DiscreteFamily.lean::exists_sigmaDiscrete_refinement	R	Apache-2.0 open Mathlib PR. It proves the stronger statement that every pseudometrizable-space open cover has an open sigma-discrete precise refinement; each discrete family is locally finite. Not in pinned Mathlib, so recorded as reference-port.
FC02-C06-U008	exact match	mathlib	Mathlib/Topology/GDelta/Basic.lean::IsGδ; isGδ_iff_eq_iInter_nat	P	Exact countable-intersection-of-open-sets definition and natural-number indexing characterization.
FC02-C06-U009	partial match / wrong interface	mathlib	IsOpen.isGδ; IsGδ.singleton	P	Open sets are Gδ and singletons are Gδ in first-countable T1 (hence Hausdorff) spaces. No searched proof of the source’s Ω singleton counterexample was found.
FC02-C06-U010	broad match	mathlib	Mathlib/Topology/GDelta/MetrizableSpace.lean PerfectlyNormalSpace instance for PseudoMetrizableSpace; IsClosed.isGδ; metric thickening API	P	Every closed subset of a metrizable space is Gδ exactly. Mathlib proves this via a countable uniform-ball basis rather than packaging the source’s literal ⋂ₙ U(A,1/n) formula as the theorem.
FC02-C06-U011	exact match	reference-port	mathlib4 PR #41676 cd6d319518617a42e975351cde7e6f20dac12512: NormalSpace.of_sigmaLocallyFiniteBasis; PseudoMetrizableSpace.of_sigmaLocallyFiniteBasis	R	The PR proves normality from a regular sigma-locally-finite basis and pseudometrizability from the same hypotheses; pinned Mathlib then gives that all closed sets are Gδ. This realizes both conclusions. Apache-2.0, open PR, not pinned.
FC02-C06-U012	unmatched after search	unmatched	—	N	Pinned/current Mathlib has Urysohn separation and Gδ machinery, but no searched declaration has exactly the normal-space + closed-Gδ hypotheses and produces an [0,1]-valued function vanishing exactly on the set. Existing locally-compact/compact Gδ lemmas have materially different hypotheses.
FC02-C06-U013	exact match	reference-port	mathlib4 PR #41676 cd6d319518617a42e975351cde7e6f20dac12512, Mathlib/Topology/Metrizable/BingNagataSmirnov.lean::metrizableSpace_iff_exists_sigmaLocallyFiniteBasis	R	Exact Bing–Nagata–Smirnov characterization, with Mathlib’s T3 separation class matching the source regular/T1 convention. Apache-2.0 open PR; not in the pinned revision.
FC02-C06-U014	broad match	mathlib	IsCompact; ParacompactSpace; finite-subcover and locally-finite-refinement APIs	P	The comparison is represented structurally: compactness asks for finite subcovers, while paracompactness asks for locally finite open refinements.
FC02-C06-U015	exact match	mathlib	Mathlib/Topology/Compactness/Paracompact.lean::ParacompactSpace	P	Exact open-cover/locally-finite-open-refinement definition.
FC02-C06-U016	broad match	mathlib	Euclidean metric-space instances; Mathlib/Topology/EMetricSpace/Paracompact.lean::Metric.instParacompactSpace	P	Every Euclidean ℝⁿ carries a metric/extended-metric structure and is therefore paracompact. The source’s explicit annular finite-cover construction is not separately packaged.
FC02-C06-U017	exact match	mathlib	Mathlib/Topology/Compactness/Paracompact.lean::NormalSpace.of_paracompactSpace_r1Space	P	A Hausdorff space is R1, so the pinned Dieudonné theorem gives exactly paracompact Hausdorff ⇒ normal.
FC02-C06-U018	exact match	mathlib	Mathlib/Topology/Compactness/Paracompact.lean::Topology.IsClosedEmbedding.paracompactSpace	P	Subtype inclusion of a closed set is a closed embedding, giving exact inheritance by closed subspaces.
FC02-C06-U019	broad match	mathlib	Metric.instParacompactSpace; Homeomorph.paracompactSpace_iff; isClosed_Ioo_iff	P	The usual open interval is metrizable and hence paracompact, and isClosed_Ioo_iff shows a nondegenerate open interval is not closed. The concrete source example is assembled from these generic declarations.
FC02-C06-U020	broad match	reference-port	mathlib4 PR #41962 bdf021dde563eb64202fee8732b82066c5b2593d, Counterexamples/Omega1Space.lean::not_normalSpace_Iio_prod_Iic_omega_one; subspace_of_paracompact_not_paracompact	R	Apache-2.0 open Mathlib PR formalizes the same ω₁-order-topology mechanism: Iic ω₁ is compact and an Iio ω₁ × Iic ω₁ subspace is not normal/paracompact. It is not yet in pinned Mathlib and is packaged via Shrink, so this is a broad reference match rather than declaration-identical source notation.
FC02-C06-U021	exact match	reference-port	mathlib4 PR #41719 cede174dcee855873dc8d81a7b998a07407e903c, Mathlib/Topology/Compactness/Paracompact.lean::paracompactSpace_TFAE_of_regular	R	The PR’s TFAE is precisely the source equivalence: open sigma-locally-finite refinement, arbitrary locally finite refinement, closed locally finite refinement, and paracompact/open locally finite refinement. Apache-2.0 open PR.
FC02-C06-U022	broad match	mathlib	TopologicalSpace.metrizableSpaceMetric; Mathlib/Topology/EMetricSpace/Paracompact.lean::Metric.instParacompactSpace	P	A MetrizableSpace can be upgraded canonically to a compatible metric, after which the metric-space paracompact instance applies. Pinned Mathlib has no direct MetrizableSpace → ParacompactSpace theorem/instance, so the interface is compositional.
FC02-C06-U023	exact match	reference-port	mathlib4 PR #41719 cede174dcee855873dc8d81a7b998a07407e903c, ParacompactSpace instance [RegularSpace X] [LindelofSpace X]	R	Exact regular-Lindelöf ⇒ paracompact theorem. Apache-2.0 open PR; absent from pinned Mathlib.
FC02-C06-U024	partial match / wrong interface	mathlib	Counterexamples/SorgenfreyLine.lean::Counterexample.SorgenfreyLine.instCompletelyNormalSpace; Counterexample.SorgenfreyLine.not_normalSpace_prod	P	The pinned/importable module proves the line completely normal and its square not normal, exactly supplying the product obstruction. It explicitly leaves paracompactness of the Sorgenfrey line as a TODO, so the source premise that both factors are paracompact is not yet formalized.
FC02-C06-U025	partial match / wrong interface	mathlib	Mathlib/Topology/MetricSpace/PiNat.lean::PiCountable.metricSpace; metric-space paracompact instance	P	The countable product topology on ℝ^ω is metrizable and hence paracompact. Munkres’s separate “uniform topology” is not a bundled Mathlib topology matching that construction, and the box-topology clause is also absent.
FC02-C06-U026	unmatched after search	unmatched	—	N	No searched Lean declaration proves non-paracompactness/non-normality of an uncountable product ℝ^J in the source topology. Generic Pi topology and paracompact infrastructure do not realize this counterexample.
FC02-C06-U027	exact match	mathlib	Mathlib/Topology/PartitionOfUnity.lean::PartitionOfUnity; PartitionOfUnity.IsSubordinate	P	Mathlib bundles continuous nonnegative locally-finite functions with sum one; subordination uses topological support contained in the indexed cover. Values are automatically in [0,1], matching the source.
FC02-C06-U028	broad match	mathlib	precise_refinement; Mathlib/Topology/ShrinkingLemma.lean::exists_iUnion_eq_closure_subset; NormalSpace.of_paracompactSpace_r1Space	P	Pinned Mathlib has the two exact generic steps: a locally finite precise open refinement and the normal-space shrinking lemma producing open sets with closures inside the cover. Their composition realizes the source shrinking statement, but no single declaration has exactly the source hypotheses/result.
FC02-C06-U029	exact match	mathlib	Mathlib/Topology/PartitionOfUnity.lean::PartitionOfUnity.exists_isSubordinate; NormalSpace.of_paracompactSpace_r1Space	P	A paracompact Hausdorff space is normal, and the pinned theorem gives a partition of unity subordinate to any indexed open cover exactly.
FC02-C06-U030	partial match / wrong interface	mathlib	Mathlib/Topology/MetricSpace/PartitionOfUnity.lean::Metric.exists_continuous_real_forall_closedBall_subset	P	Mathlib proves a closely related positive-continuous-function theorem for metric spaces and locally finite families of closed sets. The source theorem is for arbitrary paracompact Hausdorff spaces, arbitrary locally finite subsets, and pointwise prescribed bounds ε_C; no searched declaration matches that full interface.
FC02-C06-U031	exact match	reference-port	felixpernegger/pibase-lean@ff65933ec375d67a44013e4a26140893cab27acb, PiBaseLean/Properties/P82/Defs.lean::PiBase.LocallyMetrizableSpace, Apache-2.0	R	Exact local-metrizability definition. The package uses Lean v4.33.0-rc2 and Mathlib 639923353ff2…, not this project’s pinned db584cd6…, so it is preserved as a reference-port rather than credited as a compatible package import.
FC02-C06-U032	unmatched after search	unmatched	—	N	No searched Mathlib/current/open-PR/package/GitHub Lean theorem proves Smirnov’s characterization metrizable ↔︎ paracompact Hausdorff + locally metrizable. pibase-lean defines local metrizability but has no such theorem.

Provenance contract for C07

• Project search: LeanCategories/** outside .lake was searched first; no project-owned declarations supersede the metric-completion, function-space, compactly-generated, or Ascoli interfaces below.
• Pinned Mathlib: db584cd6d46c92f209a44c0f1c829460d327499d (v4.33.0, Apache-2.0) was declaration-checked across Cauchy/completion, total boundedness, uniform/compact convergence, bounded continuous functions, compactly generated/coherent spaces, compact-open topology, currying/evaluation, homotopy, and Arzelà–Ascoli. import Counterexamples.PeanoCurve compiles directly at the same revision and exists_peano_curve proves the exact source theorem, so it is credited as pinned mathlib.
• Current/open Mathlib: default branch was rechecked on 2026-09-05 at 4cbb42e75a050e830b7cf0f2ae748d7644f59cf7. Open-PR searches for Ascoli, compactly generated spaces, and completion found no current-only theorem closing the gaps below. Mathlib’s current Topology/UniformSpace/Ascoli.lean itself records the total-boundedness version and the converse “compact ⇒ equicontinuous” as TODOs.
• External search: broad GitHub Lean search found no complete formal owner for the usual-metric incompleteness of ℚ or (-1,1). The old ImperialCollegeLondon/real-number-game hit titled “rational numbers are not complete” concerns order completeness and contains explicit sorrys, so it is not credited. The direct unlicensed mdnestor/basic_topology repository has no §§43–47 implementation.
• Loogle/LeanSearch were attempted for Cauchy sequences, compactly generated spaces, Ascoli, and metric compactness; the remote probe timed out after 30 seconds, so no negative verdict relies on it.

C07 — Completeness, Function Spaces, and Ascoli

FC02 ID	Verdict	Route	Lean target(s)	Provenance	Interface comparison
FC02-C07-U001	partial match / wrong interface	mathlib	CauchySeq; CompleteSpace; Filter.Tendsto.cauchySeq; IsClosed.isComplete	P	Mathlib exactly has the Cauchy/completeness definitions, convergence implies Cauchy, and closed subsets of complete spaces are complete. The source row also asserts preservation under Munkres’s standard bounded metric min(d,1), for which no searched canonical metric replacement declaration exists.
FC02-C07-U002	exact match	mathlib	Mathlib/Topology/UniformSpace/Cauchy.lean::CompleteSpace; cauchySeq_tendsto_of_complete	P	Exact completeness interface specialized to metric spaces: every Cauchy sequence converges.
FC02-C07-U003	broad match	mathlib	Mathlib/Topology/UniformSpace/Cauchy.lean::tendsto_nhds_of_cauchySeq_of_subseq; UniformSpace.complete_of_cauchySeq_tendsto	P	The first theorem says a Cauchy sequence with a convergent subsequence converges; the second bundles that convergence property into CompleteSpace. Together they realize the source lemma, though not as one declaration.
FC02-C07-U004	broad match	mathlib	Real.instCompleteSpace; Pi.complete; finite Pi/sup metric and Euclidean-space structures	P	Real numbers and finite products are complete; finite Pi carries the sup metric while Euclidean space carries its usual norm metric. These generic instances cover both standard metrics on ℝ^k, but the source theorem is not one named declaration.
FC02-C07-U005	exact match	mathlib	Mathlib/Topology/Constructions.lean::tendsto_pi_nhds	P	Exact coordinatewise convergence criterion for product/Pi topologies.
FC02-C07-U006	exact match	mathlib	Mathlib/Topology/MetricSpace/PiNat.lean::PiCountable.metricSpace; Mathlib/Topology/UniformSpace/Pi.lean::Pi.complete	P	Mathlib constructs a metric inducing the countable product topology and the Pi space is complete when every factor is complete; specializing to real factors gives exactly the existence theorem.
FC02-C07-U007	unmatched after search	unmatched	—	N	No searched completed Lean declaration proves that ℚ with its usual metric is incomplete. The old Real Number Game hit concerns order completeness and contains explicit sorrys, so it is not a formal owner.
FC02-C07-U008	unmatched after search	unmatched	—	N	No searched completed Lean declaration packages the usual-metric incompleteness of the open interval (-1,1) or the displayed Cauchy sequence.
FC02-C07-U009	partial match / wrong interface	mathlib	Mathlib/Topology/MetricSpace/UniformConvergence.lean::UniformFun.dist_def; uniform-convergence uniformity	P	For a bounded metric target Mathlib gives exactly dist(f,g)=sup_x dist(f x,g x) and the uniform-convergence topology. Munkres first replaces an arbitrary metric by min(d,1); no searched canonical declaration performs that bounded-metric replacement, so the complete source definition is not declaration-identical.
FC02-C07-U010	broad match	mathlib	Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean complete-space instance for α →ᵤ β	P	Stronger uniform-space theorem: uniform convergence function spaces into a complete target are complete, for arbitrary index type. This subsumes Munkres’s complete uniform metric after the standard bounded-metric replacement, though the metric presentation differs.
FC02-C07-U011	partial match / wrong interface	mathlib	UniformOnFun.isClosed_setOfPred_continuous; BoundedContinuousFunction.instCompleteSpace; UniformFun complete-space instance	P	Uniform limits of continuous functions form a closed set under the appropriate coherent/uniform interface, and bounded continuous maps into a complete target form a complete space. The source also treats all bounded (not necessarily continuous) functions and relies on its explicit bounded target metric; no one searched declaration realizes every clause.
FC02-C07-U012	partial match / wrong interface	mathlib	BoundedContinuousFunction.dist_eq_iSup; UniformFun.dist_def	P	The exact sup-distance formula is present for bounded continuous functions and for all functions into an already bounded target. Munkres’s B(X,Y) is the space of all functions bounded in the original metric, for which no separately bundled Mathlib function-space type was found.
FC02-C07-U013	exact match	mathlib	Mathlib/Topology/MetricSpace/Completion.lean::UniformSpace.Completion; UniformSpace.Completion.coe_isometry; complete-space instance	P	The canonical metric completion is complete and the coercion from the original metric space is an isometry.
FC02-C07-U014	exact match	mathlib	Mathlib/Topology/UniformSpace/Completion.lean::UniformSpace.Completion.denseRange_coe; UniformSpace.Completion.isUniformEmbedding_coe; AbstractCompletion	P	Exact completion package: the original space embeds uniformly/isometrically with dense range into a complete space; AbstractCompletion records the universal completion data.
FC02-C07-U015	exact match	mathlib	Counterexamples/PeanoCurve.lean::exists_peano_curve	P	Exact pinned/importable theorem ∃ f : C(I, I × I), Function.Surjective f, i.e. a continuous surjection from the unit interval onto the square.
FC02-C07-U016	exact match	mathlib	Mathlib/Topology/UniformSpace/Defs.lean::TotallyBounded; metric uniformity basis	P	The uniform-space predicate specializes exactly to finite epsilon-ball covers in a metric space.
FC02-C07-U017	partial match / wrong interface	mathlib	Mathlib/Topology/MetricSpace/Bounded.lean::TotallyBounded.isBounded	P	The implication totally bounded ⇒ bounded is exact. No searched declaration packages the source converse-failure example on ℝ with truncated metric min(1,\|a-b\|).
FC02-C07-U018	partial match / wrong interface	mathlib	Real.instCompleteSpace; totallyBounded_Ioo; isCompact_Icc; IsCompact.totallyBounded; IsCompact.isComplete	P	Mathlib proves the positive structural pieces: ℝ is complete, open bounded intervals are totally bounded, and closed intervals are compact hence complete and totally bounded. It does not package the two required negative claims (ℝ not totally bounded in its usual metric and (-1,1) not complete) as searched declarations.
FC02-C07-U019	exact match	mathlib	Mathlib/Topology/UniformSpace/Cauchy.lean::isCompact_iff_totallyBounded_isComplete	P	Exact compact iff complete and totally bounded characterization, in stronger uniform-space form.
FC02-C07-U020	exact match	mathlib	Mathlib/Topology/UniformSpace/Equicontinuity.lean::EquicontinuousAt; Equicontinuous	P	Exact shared-neighborhood equicontinuity notions; metric epsilon formulations are provided in Metric.equicontinuousAt_iff.
FC02-C07-U021	unmatched after search	unmatched	—	N	No searched public theorem states that a totally bounded subset of the uniform function space is equicontinuous. Mathlib’s Ascoli file explicitly lists the total-boundedness version of Ascoli as TODO, and broad Lean search found no reusable owner.
FC02-C07-U022	broad match	mathlib	BoundedContinuousFunction.arzela_ascoli; IsCompact.totallyBounded	P	For compact source and compact metric target, Mathlib’s Arzelà–Ascoli theorem gives compact closure of an equicontinuous family; compact closure is totally bounded and hence so is the family. This realizes the source conclusion but compositionally rather than as the source lemma.
FC02-C07-U023	partial match / wrong interface	mathlib	pointwise boundedness via bounded evaluation images; BoundedContinuousFunction.arzela_ascoli; general ArzelaAscoli theorems	P	The pointwise-bounded condition is directly expressible and Mathlib proves strong forward Ascoli compactness theorems. The row also states the classical iff; Mathlib’s Ascoli.lean explicitly lists the converse compact ⇒ equicontinuous as a TODO, so the full row is not covered.
FC02-C07-U024	partial match / wrong interface	mathlib	BoundedContinuousFunction.arzela_ascoli; ArzelaAscoli.isCompact_closure_of_isClosedEmbedding	P	The forward direction (equicontinuity plus pointwise relative compactness/boundedness in finite-dimensional real space ⇒ compact closure) is formalized in stronger forms. The converse compact-closure ⇒ equicontinuous direction is explicitly TODO in Mathlib’s Ascoli file.
FC02-C07-U025	partial match / wrong interface	mathlib	BoundedContinuousFunction.arzela_ascoli₂; compactness/closedness APIs	P	Closed + equicontinuous + uniformly bounded finite-dimensional range gives compactness through Arzelà–Ascoli. The reverse implication includes compact ⇒ equicontinuous, which is explicitly not yet proved in the general Ascoli API, so the source iff is only partial.
FC02-C07-U026	broad match	mathlib	Pi/product TopologicalSpace (X → Y); continuous_apply; induced coordinate topologies	P	Mathlib’s Pi topology is exactly the topology of pointwise convergence, generated by coordinate evaluation maps; the source’s S(x,U) subbasis is the corresponding preimage subbasis, though no searched theorem names that family verbatim.
FC02-C07-U027	exact match	mathlib	Mathlib/Topology/Constructions.lean::tendsto_pi_nhds	P	Exact pointwise convergence criterion for sequences (indeed arbitrary filters) in a function/Pi topology.
FC02-C07-U028	unmatched after search	unmatched	—	N	No searched declaration packages the concrete sequence f_n(x)=x^n on [0,1] and its discontinuous pointwise limit.
FC02-C07-U029	exact match	mathlib	UniformOnFun with family {K \| IsCompact K}; UniformOnFun.hasBasis_uniformity_of_basis	P	Uniform convergence on the family of compact subsets is Mathlib’s native compact-convergence uniformity. In a metric target its entourage basis is exactly uniform epsilon control on a chosen compact set.
FC02-C07-U030	exact match	mathlib	UniformOnFun.tendsto_iff_tendstoUniformlyOn specialized to {K \| IsCompact K}	P	Exact characterization: convergence in compact convergence iff uniform convergence on every compact subset; the theorem is filter-general, stronger than the sequence statement.
FC02-C07-U031	partial match / wrong interface	mathlib	CompactlyGeneratedSpace; compactlyGeneratedSpace_of_isOpen_of_t2; CompactlyGeneratedSpace.isOpen	P	Mathlib defines compact generation via compact Hausdorff test maps. Its equivalence with Munkres’s “open on every compact subspace” formulation is provided under Hausdorff hypotheses; Munkres’s definition itself has no Hausdorff assumption, so the interfaces are not identical in full generality.
FC02-C07-U032	partial match / wrong interface	mathlib	FirstCountableTopology.frechetUrysohnSpace; sequential ⇒ compactly-generated instance; Hausdorff weakly-locally-compact ⇒ compactly-generated instance	P	The first-countable implication is covered via sequential spaces. The local-compact implication in Mathlib’s compactly-generated API is registered with a Hausdorff hypothesis, while the source statement says merely locally compact, so the full row is only partial.
FC02-C07-U033	broad match	mathlib	continuous_from_compactlyGeneratedSpace; compact-subspace restriction/embedding APIs	P	Mathlib’s universal test-map criterion yields the source restriction criterion by taking compact subspaces and composing their inclusions; the public theorem is phrased using arbitrary maps from compact Hausdorff spaces rather than exactly the source formulation.
FC02-C07-U034	partial match / wrong interface	mathlib	UniformOnFun.isClosed_setOfPred_continuous; ContinuousMap.range_toUniformOnFunIsCompact; to_compactlyCoherentSpace	P	Continuity is closed under compact convergence when the domain topology is coherent with compact sets. Mathlib derives compact coherence from compact generation under its Hausdorff-side interface; without that interface alignment the source theorem for arbitrary Munkres-compactly-generated X is not declaration-identical.
FC02-C07-U035	partial match / wrong interface	mathlib	ContinuousMap.tendsto_iff_forall_isCompact_tendstoUniformlyOn; closedness of continuous maps under compact convergence for compactly coherent domains	P	The sequential limit conclusion follows from the closed-range theorem under Mathlib’s compact-coherence hypotheses. The same compactly-generated/interface mismatch as U034 prevents an unconditional exact match to Munkres’s formulation.
FC02-C07-U036	partial match / wrong interface	mathlib	UniformFun; UniformOnFun; Pi topology; compact-domain uniform/compact-convergence equivalence; finite/discrete product infrastructure	P	The three topologies and the general comparison machinery are all present, and compact domains identify uniform with compact convergence. No searched single declaration packages the entire chain plus the discrete-domain equality for all functions exactly as stated, so the bundled theorem is only partially matched.
FC02-C07-U037	exact match	mathlib	Mathlib/Topology/CompactOpen.lean::ContinuousMap.compactOpen; isOpen_setOfPred_mapsTo	P	Exact compact-open topology generated by subbasic sets {f \| MapsTo f K U} for compact K and open U.
FC02-C07-U038	exact match	mathlib	ContinuousMap.compactConvergenceUniformSpace; ContinuousMap.tendsto_iff_forall_isCompact_tendstoUniformlyOn	P	Mathlib deliberately replaces the compact-convergence uniform-space topology by the compact-open topology and proves the exact convergence equivalence, so the two topologies coincide on continuous maps.
FC02-C07-U039	exact match	mathlib	ContinuousMap.compactOpen; tendsto_iff_forall_isCompact_tendstoUniformlyOn; compact-domain tendsto_iff_tendstoUniformly	P	Because compact convergence on continuous maps is identified with the metric-free compact-open topology, it is independent of the compatible metric on Y; on compact X it equals uniform convergence, yielding the source corollary.
FC02-C07-U040	exact match	mathlib	Mathlib/Topology/CompactOpen.lean ContinuousEval C(X,Y) X Y instance; continuous_eval	P	Exact joint continuity of evaluation for the compact-open topology under the locally compact Hausdorff hypotheses (via Mathlib’s locally compact pair machinery).
FC02-C07-U041	broad match	mathlib	ContinuousEval; continuous_eval	P	The evaluation map is a first-class generic interface; the source row is terminology rather than a distinct theorem.
FC02-C07-U042	exact match	mathlib	Mathlib/Topology/CompactOpen.lean::ContinuousMap.curry; uncurry; continuous_of_continuous_uncurry; continuous_uncurry_of_continuous	P	Exact currying correspondence and continuity theorem. The source’s X × Z ordering differs from Mathlib’s parameter order only by the standard product swap homeomorphism.
FC02-C07-U043	exact match	mathlib	ContinuousMap.continuous_of_continuous_uncurry; continuous_uncurry_of_continuous	P	Exact exponential-law continuity directions: continuity of an uncurried map implies continuity of its curry without local compactness; the converse holds when the function-space source variable is locally compact, matching the source after swapping product factors.
FC02-C07-U044	exact match	mathlib	Mathlib/Topology/Homotopy/Basic.lean::ContinuousMap.Homotopy	P	Exact structure: a continuous map I × X → Y with prescribed values at 0 and 1; product order is convention only.
FC02-C07-U045	partial match / wrong interface	mathlib	ArzelaAscoli.isCompact_of_equicontinuous; ArzelaAscoli.isCompact_closure_of_isClosedEmbedding; compact-convergence/pointwise inducing theorems	P	Mathlib proves strong forward Arzelà–Ascoli compactness statements from equicontinuity and pointwise relative compactness. Its Ascoli file explicitly lists the converse “compact subset ⇒ equicontinuous” as TODO, so part (b), and hence the full source theorem, is not yet represented.

Provenance contract for C08

• Project search: LeanCategories/** outside .lake was searched first; no project-owned Baire/category or Lebesgue-covering-dimension development supersedes the interfaces below.
• Pinned Mathlib: db584cd6d46c92f209a44c0f1c829460d327499d (v4.33.0, Apache-2.0) was declaration-checked for Baire spaces, Gδ/meagre/nowhere-dense sets, complete-metric and locally-compact Baire theorems, nested complete-set intersections, affine independence/affine spans, manifold embeddings, and the counterexample tree. import Counterexamples.NowhereDifferentiable compiles against this exact pin; therefore Counterexamples/NowhereDifferentiable.lean is credited as pinned mathlib, not as a reference-only source.
• Current/open Mathlib: default branch 4cbb42e75a050e830b7cf0f2ae748d7644f59cf7 and open PRs were searched on 2026-09-05. Mathlib has SmallInductiveDimension and a current zero-dimensional-space PR, but these are not Munkres’s Lebesgue covering dimension and are not used as substitutes. No open PR for the covering-dimension or Menger–Nöbeling statements was found.
• External search: google-deepmind/formal-conjectures@8323e878b83fcd7f4a448256069352a265460d75 (Apache-2.0) defines HasLebesgueCoveringDimensionLE/Eq in FormalConjecturesForMathlib/Topology/LebesgueCoveringDimension.lean using finite open covers; GitHub-wide Lean searches found no further proved development of these predicates. That revision uses Lean v4.33.1 and Mathlib 0df444a360eaa60ab8c11dca51a86af692955474, whereas this project pins Mathlib v4.33.0 at db584cd6d46c92f209a44c0f1c829460d327499d; no direct package compatibility test was performed, so these definitions remain reference-port, not package-import. The finite-cover interface is equivalent to Munkres’s all-open-cover definition on compact spaces but not definitionally identical for arbitrary spaces. An awesome_theorems search hit concerned metric covering numbers, a different notion, and the repository has no detected license, so it is not credited.
• Broad searches found no proved Lean owner for Munkres’s Baire-one dense-continuity theorem, the density of nowhere-differentiable functions in C([0,1],ℝ), the general-position perturbation lemma, or the covering-dimension embedding theorems.

C08 — Baire Spaces and Dimension Theory

FC02 ID	Verdict	Route	Lean target(s)	Provenance	Interface comparison
FC02-C08-U001	exact match	mathlib	interior; interior_eq_empty_iff_dense_compl	P	Exact interior operator and equivalence between empty interior and dense complement; the limit-point phrasing is equivalent through the standard closure/accumulation API.
FC02-C08-U002	broad match	mathlib	Set.Countable.dense_compl; interior_Icc; interior_prod_eq; interior_singleton	P	The standard examples follow from exact generic declarations: countable subsets of ℝ have dense complement, nondegenerate closed intervals have nonempty interior, and product interiors are computed coordinatewise. The four examples are not bundled as one theorem.
FC02-C08-U003	exact match	mathlib	BaireSpace; dense_iInter_of_isOpen_nat; closed-nowhere-dense/meagre duality	P	Mathlib takes the equivalent dense-open-intersection property as the class field; GDelta/Basic and Baire/Lemmas provide the dual countable-union-of-closed-empty-interior formulation used by Munkres.
FC02-C08-U004	partial match / wrong interface	mathlib	baire_of_finite; discrete/local-compact Baire infrastructure; rational topology infrastructure	P	The discrete-space Baire half is covered structurally (indeed discrete spaces are locally compact, and finite spaces have a direct Baire theorem). No searched public declaration states that ℚ with its usual topology is not a Baire space, so the complete comparison row is not exact.
FC02-C08-U005	exact match	mathlib	BaireSpace.baire_property; dense_iInter_of_isOpen_nat	P	This is Mathlib’s defining Baire property: countable intersections of dense open sets are dense.
FC02-C08-U006	exact match	mathlib	BaireSpace.of_completelyPseudoMetrizable; BaireSpace.of_t2Space_locallyCompactSpace	P	A complete metric space is completely pseudometrizable, and a compact Hausdorff space is locally compact Hausdorff; the two Mathlib Baire instances give exactly both source cases.
FC02-C08-U007	exact match	mathlib	IsComplete.nonempty_iInter_of_nonempty_biInter	P	The theorem gives nonempty total intersection for closed bounded sets in a complete set under the finite-intersection property and diameter tending to zero. Nested nonempty closed sets are the direct specialization.
FC02-C08-U008	exact match	mathlib	IsOpen.baireSpace	P	Exact theorem that an open subspace of a Baire space is Baire.
FC02-C08-U009	partial match / wrong interface	mathlib	IsGδ.setOfPred_continuousAt	P	Mathlib proves that the continuity set of an arbitrary map into a pseudometrizable space is Gδ, but no searched theorem gives density of the continuity set for a pointwise limit of continuous maps on a Baire domain. The source Baire-one theorem is therefore only partially represented.
FC02-C08-U010	partial match / wrong interface	mathlib	Counterexamples/NowhereDifferentiable.lean::NowhereDifferentiable.exists_uniformContinuous_and_not_differentiableAt	P	The pinned/importable theorem proves existence of a uniformly continuous nowhere-differentiable real function. Munkres proves the much stronger density/approximation theorem on C([0,1],ℝ); no searched declaration realizes arbitrary uniform approximation by nowhere-differentiable functions.
FC02-C08-U011	unmatched after search	unmatched	—	N	No searched declaration packages the source quadratic test function and the stated Δ_h lower bound / membership in U_4.
FC02-C08-U012	broad match	reference-port	google-deepmind/formal-conjectures@8323e878b83fcd7f4a448256069352a265460d75, Topology/LebesgueCoveringDimension.lean::HasLebesgueCoveringDimensionLE	R	The Apache-2.0 reference definition encodes the relevant multiplicity bound as encard {V \| x ∈ V} ≤ n+1. It does not separately name the exact order of a family, so this is a broad definition-level match.
FC02-C08-U013	broad match	reference-port	google-deepmind/formal-conjectures@8323e878b83fcd7f4a448256069352a265460d75, FormalConjecturesForMathlib/Topology/LebesgueCoveringDimension.lean::HasLebesgueCoveringDimensionLE	R	The definition contains exactly the source refinement relation as the conjunct ∀ V ∈ 𝓥, ∃ U ∈ 𝓤, V ⊆ U; it is embedded in the covering-dimension predicate rather than exposed as a standalone refinement declaration.
FC02-C08-U014	partial match / wrong interface	reference-port	google-deepmind/formal-conjectures@8323e878b83fcd7f4a448256069352a265460d75::HasLebesgueCoveringDimensionLE; HasLebesgueCoveringDimensionEq	R	This is the same Lebesgue covering-dimension invariant, but the reference definition quantifies over finite open covers, whereas Munkres defines dimension using every open cover. These agree for compact spaces after finite subcover reduction but are not declaration-identical for arbitrary spaces.
FC02-C08-U015	unmatched after search	unmatched	—	N	No searched proved Lean declaration realizes the source statement that compact subsets of ℝ have covering dimension at most 1. Mathlib’s SmallInductiveDimension and graph/simplicial infrastructure concern different interfaces and are not credited as covering-dimension proofs.
FC02-C08-U016	unmatched after search	unmatched	—	N	No searched proved Lean declaration realizes the source statement that the unit interval has covering dimension exactly 1. Mathlib’s SmallInductiveDimension and graph/simplicial infrastructure concern different interfaces and are not credited as covering-dimension proofs.
FC02-C08-U017	unmatched after search	unmatched	—	N	No searched proved Lean declaration realizes the source statement that compact subsets of ℝ² have covering dimension at most 2. Mathlib’s SmallInductiveDimension and graph/simplicial infrastructure concern different interfaces and are not credited as covering-dimension proofs.
FC02-C08-U018	unmatched after search	unmatched	—	N	No searched proved Lean declaration realizes the source statement that closed subspaces do not increase finite covering dimension. Mathlib’s SmallInductiveDimension and graph/simplicial infrastructure concern different interfaces and are not credited as covering-dimension proofs.
FC02-C08-U019	unmatched after search	unmatched	—	N	No searched proved Lean declaration realizes the source statement that dimension of a union of two closed finite-dimensional subspaces is the maximum. Mathlib’s SmallInductiveDimension and graph/simplicial infrastructure concern different interfaces and are not credited as covering-dimension proofs.
FC02-C08-U020	unmatched after search	unmatched	—	N	No searched proved Lean declaration realizes the source statement that finite closed-union version of the dimension maximum theorem. Mathlib’s SmallInductiveDimension and graph/simplicial infrastructure concern different interfaces and are not credited as covering-dimension proofs.
FC02-C08-U021	unmatched after search	unmatched	—	N	No searched proved Lean declaration realizes the source statement that compact 1-manifolds have covering dimension 1. Mathlib’s SmallInductiveDimension and graph/simplicial infrastructure concern different interfaces and are not credited as covering-dimension proofs.
FC02-C08-U022	unmatched after search	unmatched	—	N	No searched proved Lean declaration realizes the source statement that compact 2-manifolds have covering dimension at most 2. Mathlib’s SmallInductiveDimension and graph/simplicial infrastructure concern different interfaces and are not credited as covering-dimension proofs.
FC02-C08-U023	unmatched after search	unmatched	—	N	No searched proved Lean declaration realizes the source statement that finite linear graphs have covering dimension 1. Mathlib’s SmallInductiveDimension and graph/simplicial infrastructure concern different interfaces and are not credited as covering-dimension proofs.
FC02-C08-U024	unmatched after search	unmatched	—	N	No searched proved Lean declaration realizes the source statement that every finite linear graph embeds in ℝ³. Mathlib’s SmallInductiveDimension and graph/simplicial infrastructure concern different interfaces and are not credited as covering-dimension proofs.
FC02-C08-U025	exact match	mathlib	Mathlib/LinearAlgebra/AffineSpace/Independent.lean::AffineIndependent; affineIndependent_iff	P	Exact affine-independence condition: affine coefficients summing to zero and weighted vector sum zero are all zero.
FC02-C08-U026	exact match	mathlib	AffineSubspace; affineSpan; affineCombination_mem_affineSpan	P	Mathlib’s affine span is exactly the affine plane generated by the points, equivalently their affine combinations with coefficients summing to one.
FC02-C08-U027	exact match	mathlib	affine translations v +ᵥ p; AffineSubspace.mk'; pointwise translation of affine subspaces	P	Exact affine-space translation and affine subspace parallel to a linear direction; a k-plane is represented by an affine subspace whose direction has finrank k.
FC02-C08-U028	broad match	mathlib	AffineIndependent; finite-subfamily restriction APIs	P	The source general-position predicate is directly expressible as affine independence of every subfamily of cardinality at most N+1, but no searched named GeneralPosition predicate for arbitrary finite point sets is present.
FC02-C08-U029	unmatched after search	unmatched	—	N	No searched theorem proves the simultaneous arbitrarily-small perturbation of a finite Euclidean point set into general position.
FC02-C08-U030	unmatched after search	unmatched	—	N	No searched proved Lean theorem gives the Menger–Nöbeling-style embedding of every compact metrizable covering-dimension-m space into ℝ^(2m+1).
FC02-C08-U031	unmatched after search	unmatched	—	N	No searched proved Lean theorem identifies the Lebesgue covering dimension of compact subsets of Euclidean ℝ^N or proves the stated upper bound. Hausdorff/small-inductive dimension APIs are different invariants.
FC02-C08-U032	unmatched after search	unmatched	—	N	No searched covering-dimension theorem proves that compact topological m-manifolds have dimension at most m.
FC02-C08-U033	partial match / wrong interface	mathlib	Mathlib/Geometry/Manifold/WhitneyEmbedding.lean::exists_embedding_euclidean_of_compact	P	Mathlib proves a stronger Euclidean embedding for compact smooth finite-dimensional manifolds, but assumes a smooth manifold structure. Munkres’s corollary applies to every compact topological m-manifold using covering dimension, so the hypothesis/interface is strictly different.
FC02-C08-U034	unmatched after search	unmatched	—	N	No searched proved Lean theorem gives the equivalence “compact metrizable embeds in some Euclidean space iff finite Lebesgue covering dimension”. The only direct Lean covering-dimension source found supplies definitions, not this theorem.

Provenance contract for C09

• Project search: LeanCategories/** outside .lake was searched first for homotopy, fundamental-group, covering-space, retract, fixed-point, sphere/projective-space, and van-Kampen declarations; no project-owned implementation supersedes the routes below.
• Pinned Mathlib: db584cd6d46c92f209a44c0f1c829460d327499d (v4.33.0, Apache-2.0) was declaration-checked across Topology/Homotopy, AlgebraicTopology/FundamentalGroupoid, Topology/Covering, cyclic-group APIs, complex polynomial roots, radial sphere equivalences, and stereographic projection. A local compile probe used the explicit Lean v4.33.0 toolchain to check the covering/fundamental-group interfaces.
• Current/open Mathlib: GitHub default branch was rechecked on 2026-09-05 at 4cbb42e75a050e830b7cf0f2ae748d7644f59cf7; that exact object was fetched and searched. No current/open Mathlib owner was found for a circle π₁ ≃ ℤ theorem, Brouwer/Borsuk–Ulam, topological deformation retracts, Seifert–van Kampen for π₁, real-projective-space fundamental groups, or the surface computations below. Loogle’s live JSON search returned the existing fundamental-group declarations; the LeanSearch public endpoint requires POST and could not be exercised through the available connector policy, so no unmatched verdict relies on a LeanSearch-only negative.
• External/source-atlas search: mrdouglasny/jacobian-challenge@8ce1ec28aed1c78b3b39d0bae26e2858c82f5143 (Apache-2.0, Lean/Mathlib v4.30.0 at Mathlib c5ea00351c28e24afc9f0f84379aa41082b1188f) supplies native-Mathlib monodromy bijectivity, punctured-plane π₁ ≃ ℤ, and Rado Kirov’s two-open van-Kampen corollary; harfe/fixed-point-theorems-lean4@770940ddf9878cf61952ed53d910b92bca841838 (MIT, v4.32.0, Mathlib 81a5d257c8e410db227a6665ed08f64fea08e997) supplies Brouwer; mrdouglasny/spectral-positivity@9af3c3a7d9146c92a0ecae5ad269848bd4c25fca (Apache-2.0, v4.30.0) supplies Perron–Frobenius. Those three remain revision-mismatched reference-port sources. Arthur742Ramos/ComputationalPathsLean@f90943eecdde516817fbc33863486b681a0a9645 (MIT) now pins Lean v4.33.0 and this project’s exact Mathlib revision db584cd6d46c92f209a44c0f1c829460d327499d; its genuine AddCircle topological circle π₁ winding module was rechecked at that revision and lake build ComputationalPaths.Path.CompPath.CircleTopologicalRealization succeeds, so U041 is directly usable by package-import.
• Semantic rejection/negative evidence, dated 2026-09-05: broad GitHub/Reservoir/web searches found no completed Borsuk–Ulam or ham-sandwich owner, no genuine real-projective-space/topological figure-eight computation, and no full all-n≥2 sphere-simply-connected theorem. The similarly named ComputationalPaths RealProjective2 is literally a PUnit abbreviation, and its figure-eight free-group result is conditional on an unsupplied HasWedgeSVKDecodeBijective; those names are therefore not treated as implementations. Public Borsuk–Ulam benchmark hits are statements/axiomatized placeholders, not proofs.

C09 — The Fundamental Group

FC02 ID	Verdict	Route	Lean target(s)	Provenance	Interface comparison
FC02-C09-U001	exact match	mathlib	Mathlib/Topology/Homotopy/Basic.lean::ContinuousMap.Homotopy; ContinuousMap.Homotopic	P	Exact homotopy data for continuous maps with endpoint restrictions at 0 and 1; homotopy to a constant map expresses the source nullhomotopy clause.
FC02-C09-U002	exact match	mathlib	Mathlib/Topology/Homotopy/Path.lean::Path.Homotopy; Path.Homotopic	P	Path.Homotopy is homotopy relative to the two interval endpoints, exactly the source path-homotopy relation.
FC02-C09-U003	exact match	mathlib	Mathlib/Topology/Homotopy/Basic.lean::ContinuousMap.Homotopic.equivalence; Mathlib/Topology/Homotopy/Path.lean::Path.Homotopic.equivalence; Path.Homotopic.Quotient	P	Both homotopy relations are proved equivalence relations, and path-homotopy classes are the corresponding quotient.
FC02-C09-U004	broad match	mathlib	Mathlib/Topology/Homotopy/Path.lean::Path.Homotopic.Quotient.mk	P	The source notation [f] is represented by the quotient constructor/class; the difference is notation only.
FC02-C09-U005	broad match	mathlib	Mathlib/Topology/Homotopy/Affine.lean::ContinuousMap.Homotopy.affine; Mathlib/Analysis/Convex/Contractible.lean::Convex.contractibleSpace	P	The affine straight-line homotopy is formalized generically, and convex subsets are contractible. These specialize to the two Euclidean examples, though the examples are not bundled as one declaration.
FC02-C09-U006	exact match	mathlib	Mathlib/Topology/Homotopy/Affine.lean::ContinuousMap.Homotopy.affine	P	Exact straight-line/affine homotopy construction under the hypothesis that the affine segment remains in the target.
FC02-C09-U007	unmatched after search	unmatched	—	N	No searched project, pinned/current Mathlib, open-PR, package, or GitHub Lean declaration proves the concrete upper-semicircle/stretching homotopy together with non-homotopy to the lower semicircle in the punctured plane.
FC02-C09-U008	exact match	mathlib	Mathlib/Topology/Homotopy/Path.lean::Path.Homotopic.Quotient.trans; quotient compatibility of Path.trans	P	Path concatenation descends to path-homotopy classes exactly.
FC02-C09-U009	exact match	mathlib	Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean groupoid laws for Path.Homotopic.Quotient; refl; trans; symm	P	Associativity, identity classes, and reversal as inverse are precisely the groupoid laws of homotopy classes of paths.
FC02-C09-U010	broad match	mathlib	Mathlib/Topology/UnitInterval.lean interval affine/homeomorphism API; Mathlib/Topology/Subpath.lean::Path.subpath	P	Mathlib has the required positive affine reparameterizations and inverse/composition infrastructure, but not the source terminology as one named theorem.
FC02-C09-U011	exact match	mathlib	Mathlib/Topology/Subpath.lean::Path.Homotopic.concat_subpath; Path.Homotopy.concatSubpath	P	Exact finite subdivision theorem: concatenating consecutive reparameterized subpaths is homotopic to the full subpath, hence gives the source product of classes.
FC02-C09-U012	broad match	mathlib	group hierarchy; MonoidHom.ker; MonoidHom.range; Subgroup.Normal; quotient groups and coset APIs	P	All reviewed group notions and first-isomorphism/coset infrastructure are native Mathlib structures and theorems; this row is a textbook review bundle rather than one declaration.
FC02-C09-U013	exact match	mathlib	Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean::FundamentalGroup; FundamentalGroup.fromPath; FundamentalGroup.toPath	P	The fundamental group is exactly the automorphism group at the chosen basepoint in the fundamental groupoid, i.e. path-homotopy classes of loops with concatenation.
FC02-C09-U014	broad match	mathlib	Mathlib/Analysis/Convex/Contractible.lean::Convex.contractibleSpace; Mathlib/AlgebraicTopology/FundamentalGroupoid/SimplyConnected.lean::SimplyConnectedSpace.ofContractible	P	Every nonempty convex real subset is contractible and hence simply connected, so its fundamental group is subsingleton. This uniformly subsumes Euclidean space and balls.
FC02-C09-U015	exact match	mathlib	Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean::fundamentalGroupMulEquivOfPath	P	A path between basepoints induces the conjugation/basepoint-change group equivalence represented in the source by α̂.
FC02-C09-U016	exact match	mathlib	Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean::fundamentalGroupMulEquivOfPath	P	The construction is already a MulEquiv, exactly the theorem that basepoint change along a path is a group isomorphism.
FC02-C09-U017	exact match	mathlib	Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean::fundamentalGroupMulEquivOfPathConnected	P	A path-connected space supplies an isomorphism between fundamental groups at arbitrary basepoints.
FC02-C09-U018	exact match	mathlib	Mathlib/AlgebraicTopology/FundamentalGroupoid/SimplyConnected.lean::SimplyConnectedSpace; simply_connected_iff_unique_homotopic	P	Mathlib bundles the equivalent fundamental-groupoid characterization; the iff theorem recovers nonemptiness/path-connectedness and uniqueness of path classes, equivalent to path connected plus trivial π₁.
FC02-C09-U019	exact match	mathlib	Mathlib/AlgebraicTopology/FundamentalGroupoid/SimplyConnected.lean::SimplyConnectedSpace.paths_homotopic	P	Exact theorem that any two paths with common endpoints in a simply connected space are path homotopic.
FC02-C09-U020	exact match	mathlib	Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean::FundamentalGroup.map	P	The induced homomorphism sends a loop class to the class of its composition with the continuous map, exactly h_*.
FC02-C09-U021	exact match	mathlib	Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean::FundamentalGroupoid.map_id; FundamentalGroupoid.map_comp; FundamentalGroup.map	P	Identity and composition functoriality are formalized at the fundamental-groupoid level and restrict to the source induced-homomorphism identities.
FC02-C09-U022	broad match	mathlib	Mathlib/Topology/Homotopy/Equiv.lean::Homeomorph.toHomotopyEquiv; Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean::FundamentalGroupoidFunctor.equivOfHomotopyEquiv	P	A homeomorphism is a homotopy equivalence and induces an equivalence of fundamental groupoids, hence basepoint fundamental groups are isomorphic. The public target is groupoid-level rather than a single named MulEquiv theorem.
FC02-C09-U023	exact match	mathlib	Mathlib/Topology/Covering/Basic.lean::IsEvenlyCovered; IsEvenlyCovered.toTrivialization	P	The discrete-fiber trivialization over an open neighborhood is equivalent to the source decomposition into disjoint sheets, with each sheet mapped homeomorphically onto the neighborhood.
FC02-C09-U024	partial match / wrong interface	mathlib	Mathlib/Topology/Covering/Basic.lean::IsCoveringMap	P	Mathlib requires every point to be evenly covered but deliberately permits empty fibers, so IsCoveringMap p does not by itself imply the source convention that p is surjective. Adding Function.Surjective p aligns the definitions.
FC02-C09-U025	partial match / wrong interface	mathlib	Mathlib/Topology/Covering/Basic.lean::IsCoveringMap.mk; Mathlib/Topology/FiberBundle/Constructions.lean::Bundle.Trivial.trivialization	P	The generic constructors directly support identity/trivial finite-sheet coverings, but no searched pinned/current declaration packages the source two concrete covering examples themselves.
FC02-C09-U026	broad match	mathlib	Mathlib/Topology/Covering/AddCircle.lean::AddCircle.isCoveringMap_coe; AddCircle.isAddQuotientCoveringMap_coe	P	The quotient map ℝ → AddCircle 1 = ℝ/ℤ is the standard universal circle covering in Mathlib. Munkres presents the circle as the Euclidean unit circle via (cos 2πt,sin 2πt), so the carrier presentation differs.
FC02-C09-U027	unmatched after search	unmatched	—	N	No searched declaration packages the source local-homeomorphism-but-not-covering example from the positive reals onto the circle.
FC02-C09-U028	broad match	mathlib	Mathlib/Topology/Covering/AddCircle.lean::AddCircle.isAddQuotientCoveringMap_nsmul_of_ne_zero	P	Specializing to n=2 gives the degree-two self-cover of the additive circle; this is the source z ↦ z² covering after the standard identification with the Euclidean unit circle.
FC02-C09-U029	exact match	mathlib	Mathlib/Topology/Covering/Basic.lean::IsCoveringMapOn.restrictPreimage; IsCoveringMapOn.isCoveringMap_restrictPreimage	P	Exact restriction of a covering to the preimage of a subspace.
FC02-C09-U030	partial match / wrong interface	mathlib	Mathlib/Topology/FiberBundle/Constructions.lean::Bundle.Trivialization.prod; Mathlib/Topology/Covering/Basic.lean::IsCoveringMap.mk	P	Mathlib has product trivializations and the covering constructor, but no searched declaration states directly that the product of two covering maps is a covering map.
FC02-C09-U031	unmatched after search	unmatched	—	N	No searched existing theorem packages Munkres’s concrete torus covering p × p : ℝ² → S¹ × S¹; the generic covering and additive-circle infrastructure is not credited as this concrete example without an existing proof.
FC02-C09-U032	unmatched after search	unmatched	—	N	No searched Lean declaration realizes the figure-eight covering by the indicated infinite grid restriction.
FC02-C09-U033	partial match / wrong interface	reference-port	mrdouglasny/jacobian-challenge@8ce1ec28aed1c78b3b39d0bae26e2858c82f5143, Jacobians/Topology/PuncturedPlanePi1.lean::isAddQuotientCoveringMap_expAround; expAround	R	Apache-2.0, Lean/Mathlib v4.30.0 (c5ea00351c28e24afc9f0f84379aa41082b1188f). It proves a genuine native-Mathlib universal covering ℂ → ℂ ∖ {a} by shifted exponential, mathematically equivalent to the polar universal cover of the punctured plane, but not Munkres’s literal p × id presentation.
FC02-C09-U034	broad match	mathlib	Mathlib/Topology/Homotopy/Lifting.lean::IsCoveringMap.eq_liftPath_iff; existsUnique_continuousMap_lifts	P	The lift equation and chosen starting lift are exactly the relation used throughout Mathlib’s covering-lifting API, although there is no separate global IsLift definition with Munkres’s notation.
FC02-C09-U035	partial match / wrong interface	reference-port	mrdouglasny/jacobian-challenge@8ce1ec28aed1c78b3b39d0bae26e2858c82f5143, Jacobians/Topology/PuncturedPlanePi1.lean::circleLoop; pi1PuncturedPlaneIntOn_eq_fromPath	R	Apache-2.0, Lean/Mathlib v4.30.0. This gives explicit winding loops and their explicit lifts in the universal cover of the punctured plane, but not the source’s exact semicircle examples.
FC02-C09-U036	exact match	mathlib	Mathlib/Topology/Homotopy/Lifting.lean::IsCoveringMap.exists_path_lifts; liftPath; eq_liftPath_iff	P	Exact existence and uniqueness of a path lift after choosing a point over the initial point.
FC02-C09-U037	exact match	mathlib	Mathlib/Topology/Homotopy/Lifting.lean::IsCoveringMap.liftHomotopy; liftHomotopyRel; homotopicRel_liftPath	P	Exact homotopy-lifting theorem, including the relative-endpoint version needed for path homotopies.
FC02-C09-U038	exact match	mathlib	Mathlib/Topology/Homotopy/Lifting.lean::IsCoveringMap.homotopicRel_liftPath; liftPath_apply_one_eq_of_homotopicRel	P	Path-homotopic base paths lifted from the same starting point have homotopic lifts and equal endpoints.
FC02-C09-U039	exact match	mathlib	Mathlib/Topology/Homotopy/Lifting.lean::IsCoveringMap.monodromy; fundamentalGroupMulAction; monodromyPerm	P	Monodromy is exactly the source correspondence sending a loop/path-homotopy class and chosen starting fiber point to the endpoint of its lift.
FC02-C09-U040	exact match	reference-port	mrdouglasny/jacobian-challenge@8ce1ec28aed1c78b3b39d0bae26e2858c82f5143, Jacobians/Topology/CoveringPi1.lean::monodromy_surjective; monodromy_injective; pathClassEquivFiber	R	Apache-2.0, Lean/Mathlib v4.30.0. Against Mathlib’s native IsCoveringMap/Path.Homotopic.Quotient, path connectedness of the total space gives surjectivity onto the fiber and simple connectedness gives injectivity, hence a bijection exactly as in the source. Pinned Mathlib has the quotient-covering special case but not this generic packaged result.
FC02-C09-U041	broad match	package-import	Arthur742Ramos/ComputationalPathsLean@f90943eecdde516817fbc33863486b681a0a9645, ComputationalPaths/Path/CompPath/CircleTopologicalRealization.lean::topologicalPiOneEquivInt; topologicalPiOneEquivInt_mul; topologicalPiOneEquivInt_one; topologicalPiOneEquivInt_inv	I	MIT, Lean v4.33.0 / Mathlib db584cd6d46c92f209a44c0f1c829460d327499d, exactly this project’s pin; the targeted module builds successfully at this revision. It genuinely uses Mathlib’s FundamentalGroup (AddCircle 1) 0 and proves an integer winding equivalence preserving group operations. Packaging is a SimpleEquiv plus operation lemmas rather than one native MulEquiv, so this is a broad direct-import match.
FC02-C09-U042	exact match	mathlib	Mathlib/GroupTheory/SpecificGroups/Cyclic/Basic.lean::IsCyclic; isCyclic_iff_exists_zpowers_eq_top	P	Exact cyclic-group notion: one element generates the whole group.
FC02-C09-U043	exact match	mathlib	Mathlib/GroupTheory/SpecificGroups/Cyclic.lean::intCyclicMulEquiv; zmodCyclicMulEquiv; zmodMulEquivOfGenerator	P	Infinite cyclic groups are isomorphic to multiplicative integers, and finite cyclic groups are isomorphic to the corresponding ZMod; explicit-generator versions are also available.
FC02-C09-U044	exact match	mathlib	Mathlib/GroupTheory/SpecificGroups/Cyclic.lean::monoidHomOfForallMemZpowers; monoidHomOfForallMemZpowers_apply_gen; MonoidHom.eq_iff_eq_on_generator	P	The cyclic generator determines a homomorphism by its image, and two homomorphisms are equal exactly when they agree on a generator, which is the source universal property.
FC02-C09-U045	partial match / wrong interface	mathlib	Mathlib/Topology/Homotopy/Lifting.lean::IsCoveringMap.injective_path_homotopic_map; existsUnique_continuousMap_lifts_of_range_le; quotient-covering ker_monodromyPerm	P	Part (a) is exact for arbitrary covering maps: the induced map on fundamental-groupoid Hom-sets, hence π₁, is injective. Mathlib also has lifting/range criteria and a quotient-covering kernel formula, but no searched declaration packages the source’s full general right-coset-to-fiber bijection and loop-in-image iff lift-is-loop theorem.
FC02-C09-U046	broad match	mathlib	continuous maps plus Function.LeftInverse; subtype inclusion/restriction APIs	P	A retraction is directly expressible as a continuous map left-inverse to the subtype inclusion; Mathlib has the constituent native notions but no dedicated topological Retraction structure matching Munkres.
FC02-C09-U047	broad match	mathlib	FundamentalGroup.map; functoriality; Function.LeftInverse.injective	P	Applying π₁ functoriality to r ∘ i = id makes the inclusion-induced map left-invertible and therefore injective. The result is an immediate specialization of existing declarations, but no dedicated retract theorem was found.
FC02-C09-U048	unmatched after search	unmatched	—	N	No searched complete Lean proof establishes that the circle is not a retract of the disk. The older Brouwer-formalization hit explicitly leaves the no-retraction/fundamental-group route incomplete and is not credited.
FC02-C09-U049	partial match / wrong interface	mathlib	ContinuousMap.Homotopic; SimplyConnectedSpace.paths_homotopic; FundamentalGroup.map	P	Nullhomotopy and trivial induced maps are available, but no searched theorem proves the full equivalence with extension of a map S¹ → X over the disk.
FC02-C09-U050	partial match / wrong interface	reference-port	mrdouglasny/jacobian-challenge@8ce1ec28aed1c78b3b39d0bae26e2858c82f5143, Jacobians/Topology/PuncturedPlanePi1.lean::pi1PuncturedPlaneInt; pi1PuncturedPlaneInt_ofAdd_one; circleLoop	R	Apache-2.0, Lean/Mathlib v4.30.0. The explicit once-around circle loop in the punctured plane is identified with the integer generator of π₁, proving its nontrivial class; the source’s exact inclusion map and separate identity-map statement are not packaged verbatim.
FC02-C09-U051	unmatched after search	unmatched	—	N	No searched Lean declaration formalizes the inward/outward boundary-point conclusion for a nowhere-zero vector field on the disk.
FC02-C09-U052	exact match	reference-port	harfe/fixed-point-theorems-lean4@770940ddf9878cf61952ed53d910b92bca841838, FixedPointTheorems/brouwer.lean::brouwer_fixed_point	R	MIT, Lean/Mathlib v4.32.0 (81a5d257c8e410db227a6665ed08f64fea08e997). The theorem is stronger: every continuous self-map of a nonempty compact convex subset of a finite-dimensional real normed space has a fixed point; the closed disk is an immediate specialization. Toolchain differs from this project’s v4.33.0 pin, so this is reference-port.
FC02-C09-U053	exact match	reference-port	mrdouglasny/spectral-positivity@9af3c3a7d9146c92a0ecae5ad269848bd4c25fca, SpectralPositivity/Matrix/PerronFrobenius.lean::allpos_has_pos_eigenvec	R	Apache-2.0, Lean/Mathlib v4.30.0. This theorem exactly states that a finite nonempty real matrix with every entry strictly positive has a strictly positive eigenvalue with a strictly positive eigenvector; specializing the finite index type to Fin 3 gives the source theorem. The external toolchain differs from this project pin, so it remains reference-port.
FC02-C09-U054	unmatched after search	unmatched	—	N	No searched declaration proves the source fine-cover/triple-intersection theorem for the triangle. Existing covering-dimension and nerve infrastructure does not instantiate this concrete result.
FC02-C09-U055	broad match	mathlib	Mathlib/Analysis/Complex/Polynomial/Basic.lean::Complex.exists_root; Complex.isAlgClosed	P	The Fundamental Theorem of Algebra is exact for positive-degree complex polynomials. Real-coefficient equations are obtained by casting the polynomial to ℂ[X]; that specialization is not the same single declaration.
FC02-C09-U056	exact match	mathlib	Mathlib/Algebra/Group/EvenFunction.lean::Function.Odd specialized to sphere maps	P	Function.Odd h is exactly the equation h (-x) = -h x, i.e. the source antipode-preserving condition on sphere maps.
FC02-C09-U057	unmatched after search	unmatched	—	N	No searched proved Lean theorem states that an antipode-preserving map S¹ → S¹ is not nullhomotopic.
FC02-C09-U058	unmatched after search	unmatched	—	N	No searched proved Lean theorem excludes antipode-preserving maps S² → S¹.
FC02-C09-U059	unmatched after search	unmatched	—	N	No searched completed Lean formalization of the Borsuk–Ulam theorem S² → ℝ² was found. Public benchmark/search hits provide statements or axiomatized placeholders, not a proved owner.
FC02-C09-U060	unmatched after search	unmatched	—	N	No searched completed Lean declaration proves the two-region planar bisection/ham-sandwich corollary.
FC02-C09-U061	broad match	mathlib	Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean::Path.Homotopic.map_trans_evalAt; FundamentalGroupoidFunctor.homotopicMapsNatIso	P	Homotopic maps induce naturally isomorphic fundamental-groupoid functors; when the basepoint track is constant, the conjugation is trivial and the induced homomorphisms agree. The fixed-basepoint equality is a specialization, not a separately named theorem.
FC02-C09-U062	partial match / wrong interface	mathlib	Mathlib/Analysis/Normed/Module/Ball/RadialEquiv.lean::homeomorphSphereProd; homeomorphUnitSphereProd; FundamentalGroupoidFunctor.prodIso	P	The punctured normed space is homeomorphic to sphere × positive radii, and the latter radial factor is contractible, giving the expected π₁ equivalence structurally. No searched declaration identifies the source inclusion-induced homomorphism itself as the isomorphism.
FC02-C09-U063	partial match / wrong interface	mathlib	ContinuousMap.HomotopyRel; continuous subtype inclusion and retraction-as-left-inverse data	P	A deformation retract can be encoded with existing homotopy-relative-to-subset primitives, but Mathlib has no searched dedicated topological deformation-retract definition with the source interface.
FC02-C09-U064	partial match / wrong interface	mathlib	ContinuousMap.HomotopyEquiv; FundamentalGroupoidFunctor.equivOfHomotopyEquiv	P	A deformation retract gives a homotopy equivalence and hence equivalent fundamental groupoids, but no searched declaration converts the missing deformation-retract structure into the exact inclusion-induced MulEquiv claimed by the source.
FC02-C09-U065	partial match / wrong interface	reference-port	mrdouglasny/jacobian-challenge@8ce1ec28aed1c78b3b39d0bae26e2858c82f5143, Jacobians/Topology/PuncturedPlanePi1.lean::pi1PuncturedPlaneIntAt; pi1PuncturedPlaneInt	R	Apache-2.0, Lean/Mathlib v4.30.0. It proves natively that the once-punctured plane has fundamental group ℤ at every basepoint, matching the source cyclic-group conclusion. The source’s explicit deformation retraction from ℝ³ minus the z-axis is not formalized there.
FC02-C09-U066	unmatched after search	unmatched	—	N	No searched genuine topological declaration proves that the doubly punctured plane deformation retracts onto a figure eight. Synthetic computational-path figure-eight models do not realize this concrete topological space.
FC02-C09-U067	unmatched after search	unmatched	—	N	No searched genuine topological declaration proves the stated deformation retraction onto the theta space.
FC02-C09-U068	exact match	mathlib	Mathlib/Topology/Homotopy/Equiv.lean::ContinuousMap.HomotopyEquiv	P	Exact homotopy-equivalence data: continuous maps in both directions with composites homotopic to identities.
FC02-C09-U069	exact match	mathlib	Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean::Path.Homotopic.map_trans_evalAt; FundamentalGroupoidFunctor.homotopicMapsNatIso	P	The path traced by the basepoint during a homotopy gives exactly the conjugation/basepoint-change relation between the two induced maps.
FC02-C09-U070	broad match	mathlib	Path.Homotopic.map_trans_evalAt; fundamentalGroupMulEquivOfPath	P	The induced maps differ by conjugation with a group isomorphism, so injectivity, surjectivity, and triviality are invariant under homotopy. Mathlib provides the exact ingredients rather than this three-part corollary as one declaration.
FC02-C09-U071	broad match	mathlib	FundamentalGroupoidFunctor.homotopicMapsNatIso; FundamentalGroup.map for constant maps	P	A nullhomotopic map has induced map conjugate to the map of a constant map, hence trivial. The conclusion is compositionally realized but not exposed under the source theorem name.
FC02-C09-U072	broad match	mathlib	Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean::FundamentalGroupoidFunctor.equivOfHomotopyEquiv	P	Homotopy-equivalent spaces have equivalent fundamental groupoids, which yields isomorphic vertex/fundamental groups after the associated basepoint transport. The library theorem is groupoid-level rather than the source one-line π₁ statement.
FC02-C09-U073	unmatched after search	unmatched	—	N	No searched native-Mathlib Lean theorem proves the weak Seifert–van Kampen generation statement that the images from two path-connected open sets generate π₁(X). The located Kirov proof establishes only the simply-connected two-open corollary below.
FC02-C09-U074	exact match	reference-port	mrdouglasny/jacobian-challenge@8ce1ec28aed1c78b3b39d0bae26e2858c82f5143, vendor/kirov-dolbeault-port/KirovDolbeault/VanKampen.lean::Jacobians.RiemannSphere.VanKampen.twoOpenVanKampen_holds	R	Apache-2.0 source file by Rado Kirov, vendored in an Apache-2.0 project at Lean/Mathlib v4.30.0. It proves exactly: a path-connected space covered by two open simply connected sets with path-connected intersection is simply connected, using Mathlib’s native path-homotopy quotient.
FC02-C09-U075	partial match / wrong interface	reference-port	mrdouglasny/jacobian-challenge@8ce1ec28aed1c78b3b39d0bae26e2858c82f5143, vendor/kirov-dolbeault-port/KirovDolbeault/VanKampen.lean instance SimplyConnectedSpace (Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1)	R	Apache-2.0, Lean/Mathlib v4.30.0. The external proof establishes the S² case unconditionally. No searched declaration proves the source uniform theorem for every Sⁿ, n ≥ 2, so the row remains partial.
FC02-C09-U076	exact match	mathlib	Mathlib/Geometry/Manifold/Instances/Sphere.lean::stereographic'; stereographic'_source; stereographic'_target	P	Exact stereographic chart: the unit n-sphere minus a chosen pole is homeomorphic to all of EuclideanSpace ℝ (Fin n).
FC02-C09-U077	broad match	mathlib	Mathlib/AlgebraicTopology/FundamentalGroupoid/Product.lean::FundamentalGroupoidFunctor.prodIso	P	Mathlib proves the stronger groupoid equivalence π(X) × π(Y) ≌ π(X × Y); at a chosen pair of basepoints its automorphism group is the product of the two fundamental groups. The public theorem is groupoid-level.
FC02-C09-U078	unmatched after search	unmatched	—	N	No searched single existing Lean proof computes the torus fundamental group as ℤ × ℤ. The product-groupoid theorem and a separate external circle computation do not count as a realized concrete torus computation, especially across incompatible Mathlib revisions.
FC02-C09-U079	unmatched after search	unmatched	—	N	No searched genuine topological Lean definition realizes RP² as the antipodal quotient of S². The similarly named ComputationalPaths object is explicitly an abbreviation of a one-point type and is not credited.
FC02-C09-U080	unmatched after search	unmatched	—	N	No searched genuine topological Lean theorem proves compact-surface properties of real projective 2-space together with the antipodal quotient being a covering map.
FC02-C09-U081	unmatched after search	unmatched	—	N	No searched genuine topological Lean computation proves π₁(RP²) ≅ ℤ/2. The located synthetic rp2FundGroup is built on a one-point surrogate carrier, so it does not realize the source theorem.
FC02-C09-U082	unmatched after search	unmatched	—	N	No searched genuine topological Lean development constructs real projective n-space as the sphere antipodal quotient and proves the two-element fundamental group for n ≥ 2.
FC02-C09-U083	unmatched after search	unmatched	—	N	No searched proved topological Lean theorem establishes that the figure-eight fundamental group is nonabelian. The located ComputationalPaths equivalence is conditional on an unsupplied decode-bijectivity instance and its own comments flag the current circle carrier issue, so it is not credited.
FC02-C09-U084	unmatched after search	unmatched	—	N	No searched proved Lean theorem computes enough of the double-torus fundamental group to establish nonabelianness.
FC02-C09-U085	unmatched after search	unmatched	—	N	No searched Lean theorem packages the source comparison proving the four named surfaces pairwise topologically distinct via their fundamental groups.

Provenance contract for C10

• Project search: LeanCategories/** outside .lake was searched first for Jordan separation, invariance of domain, planar-graph embeddings, winding number, and Cauchy-formula owners; no project-owned C10 declaration was found.
• Pinned Mathlib: repository pin db584cd6d46c92f209a44c0f1c829460d327499d (v4.33.0, Apache-2.0) was checked declaration-by-declaration for stereographic projection, connected components, homotopy, finite graphs, and complex Cauchy integrals. It supplies infrastructure and the combinatorial K_n/K_{m,n} definitions, but no Jordan-curve, planar Kuratowski, or winding-number theorem. The open Mathlib issue #33018 still contains only a sorry statement for invariance of domain and is not credited as an implementation.
• Current Mathlib / search services: current default branch was rechecked 2026-09-05 at 4cbb42e75a050e830b7cf0f2ae748d7644f59cf7. Live Loogle name searches returned no Jordan-curve or winding-number declaration; its Kuratowski hits are the unrelated metric-space embedding. Mathlib’s current undergraduate coverage file still leaves winding number blank.
• Source-atlas / external Lean: mdnestor/basic_topology@10230d7997436e8be1644d0750ec6b03d845619b has no C10 Jordan/invariance implementation. alonamaloh/schoenflies-lean@05a43d29cde026618777db3d4e4316204ccca237 is Apache-2.0 and contains completed Jordan-curve/Jordan–Schönflies plus plane-graph/K3,3 results, but pins Lean 4.32.2 and Mathlib 905b95818eb32af7874a58b427f50c1711a5e96c; every credited row is therefore reference-port. mccorvie/classification-of-surfaces@e3c7230fe78d7b056a415d9ecae6f77887046b32 is Apache-2.0, pins Lean 4.32.0 and Mathlib 81a5d257c8e410db227a6665ed08f64fea08e997, and supplies a completed plane invariance-of-domain route and related Jordan-region infrastructure; these are likewise reference-port, not importable at the project pin.
• Negative verdicts below are dated 2026-09-05 and cover project source, pinned/current Mathlib, open Mathlib work, Loogle/LeanSearch where queryable, the known Munkres source atlas, Reservoir/GitHub Lean searches, and the two relevant external plane-topology developments above.

C10 — Separation Theorems in the Plane

FC02 ID	Verdict	Route	Lean target(s)	Provenance	Interface comparison
FC02-C10-U001	partial match / wrong interface	mathlib	Mathlib/Geometry/Manifold/Instances/Sphere.lean::stereographic'; stereographic'_source; stereographic'_target; Mathlib/Topology/Connected/Basic.lean::connectedComponentIn	P	The punctured-sphere homeomorphism and component API are native, and homeomorphisms transport components. No searched declaration packages the source bounded/unbounded dichotomy for the component containing the deleted pole.
FC02-C10-U002	unmatched after search	unmatched	—	N	No searched declaration proves Munkres Lemma 61.2: a compact-set map into the twice-punctured sphere is nullhomotopic when the two punctures lie in the same complementary component. Generic ContinuousMap.Nullhomotopic infrastructure does not realize this criterion.
FC02-C10-U003	broad match	mathlib	Mathlib/Topology/Connected/Basic.lean::IsConnected; connectedComponentIn; ConnectedComponents	P	The source notion “A separates connected X iff X minus A is disconnected, and into n components” is directly expressible with Mathlib connectedness/components, but there is no dedicated Separates predicate carrying Munkres’s packaging.
FC02-C10-U004	partial match / wrong interface	reference-port	alonamaloh/schoenflies-lean@05a43d29cde026618777db3d4e4316204ccca237, Schoenflies/Curve.lean::Schoenflies.IsArc; IsArcBetween	R	Apache-2.0, Lean 4.32.2 / Mathlib 905b95818eb32af7874a58b427f50c1711a5e96c. IsArc gives an injective continuous parametrization of a planar subset by [0,1]; Munkres defines an abstract Hausdorff arc as a space homeomorphic to [0,1], so the realization is plane-specific and parametrized rather than the literal abstract interface.
FC02-C10-U005	broad match	reference-port	alonamaloh/schoenflies-lean@05a43d29cde026618777db3d4e4316204ccca237, Schoenflies/JordanClosed.lean::Schoenflies.jordan_curve_theorem	R	Apache-2.0, Lean 4.32.2 / Mathlib 905b95818eb32af7874a58b427f50c1711a5e96c. The theorem proves a Jordan curve in ℝ² is IsSeparating (indeed exactly two complementary regions with the curve as frontier). This is the plane form equivalent to the source sphere separation theorem after deleting an off-curve point, but not the literal S² carrier.
FC02-C10-U006	unmatched after search	unmatched	—	N	No searched Lean theorem proves the general two-continuum separation result for closed connected A₁,A₂ ⊂ S² meeting exactly in two points. Jordan/crosscut implementations found impose substantially stronger arc/Jordan hypotheses.
FC02-C10-U007	unmatched after search	unmatched	—	N	No searched topological homotopy-extension theorem matches the stated normal-space/closed-subset extension into an open subset of ℝⁿ while preserving nullhomotopy. Model-category homotopy-extension APIs are a different interface and are not credited.
FC02-C10-U008	unmatched after search	unmatched	—	N	No searched declaration proves the Borsuk lemma that an injective compact-set map into S² minus {a,b} which is nullhomotopic forces a,b into one complementary component.
FC02-C10-U009	exact match	reference-port	mccorvie/classification-of-surfaces@e3c7230fe78d7b056a415d9ecae6f77887046b32, ClassificationOfSurfaces/Topology/InvarianceOfDomain.lean::LeanEval.Topology.ClassificationOfSurfaces.InvarianceOfDomain.invariance_of_domain_open_map; ClassificationOfSurfaces/Moise/Brouwer.lean plane BrouwerFixedPoint instance	R	Apache-2.0, Lean 4.32.0 / Mathlib 81a5d257c8e410db227a6665ed08f64fea08e997. The theorem states that a continuous map on an open subset of a finite-dimensional real inner-product space, injective there, has open image; the repository separately discharges its Brouwer assumption for Plane = EuclideanSpace ℝ (Fin 2). This specializes exactly to Munkres’s planar invariance-of-domain theorem; continuity plus injectivity then makes the inverse on the image continuous.
FC02-C10-U010	unmatched after search	unmatched	—	N	No searched declaration proves the specialized two-open-set fundamental-group theorem with the three conclusions about the loop α * β, its generated infinite cyclic subgroup, and trivial intersection with the comparison loop subgroup. Existing van Kampen material does not package this statement.
FC02-C10-U011	broad match	reference-port	alonamaloh/schoenflies-lean@05a43d29cde026618777db3d4e4316204ccca237, Schoenflies/JordanClosed.lean::Schoenflies.arc_complement	R	Apache-2.0, Lean 4.32.2 / Mathlib 905b95818eb32af7874a58b427f50c1711a5e96c. It proves exactly that the complement of a simple arc in ℝ² is connected. Munkres states the result for an arc in S²; these are equivalent by choosing a point off the compact arc and stereographically projecting, but the carrier differs.
FC02-C10-U012	unmatched after search	unmatched	—	N	No searched Lean declaration proves the stated Janiszewski-style nonseparation theorem for two closed subsets whose intersection has simply connected complement.
FC02-C10-U013	broad match	reference-port	alonamaloh/schoenflies-lean@05a43d29cde026618777db3d4e4316204ccca237, Schoenflies/JordanClosed.lean::Schoenflies.jordan_curve_theorem; Schoenflies/CrosscutCells.lean::Schoenflies.IsSeparating	R	Apache-2.0, Lean 4.32.2 / Mathlib 905b95818eb32af7874a58b427f50c1711a5e96c. IsSeparating records exactly two complementary regions, one bounded and one unbounded, each with the Jordan curve as frontier. This realizes the full plane Jordan-curve conclusion; Munkres phrases it on S², where bounded/unbounded becomes two components.
FC02-C10-U014	unmatched after search	unmatched	—	N	No searched theorem gives the source generalization for two closed connected subsets of S² meeting in two points, neither individually separating, whose union has exactly two complementary components.
FC02-C10-U015	broad match	reference-port	alonamaloh/schoenflies-lean@05a43d29cde026618777db3d4e4316204ccca237, Schoenflies/JordanSchoenflies.lean::Schoenflies.jordan_schoenflies_of_homeomorph	R	Apache-2.0, Lean 4.32.2 / Mathlib 905b95818eb32af7874a58b427f50c1711a5e96c. The formalized Jordan–Schönflies theorem is stronger in presentation: every homeomorphism between two planar Jordan curves extends to a homeomorphism of the plane. Taking the target to be the standard circle yields disk/exterior region homeomorphisms, hence the source closed-component-to-B² statement after the usual plane/sphere identification, but that corollary is not the literal theorem signature.
FC02-C10-U016	partial match / wrong interface	reference-port	alonamaloh/schoenflies-lean@05a43d29cde026618777db3d4e4316204ccca237, Schoenflies/Graph/Drawing.lean::Graph.IsDrawing; Graph.edgeArc; Graph.IsDrawing.edge_isArcBetween	R	Apache-2.0, Lean 4.32.2 / Mathlib 905b95818eb32af7874a58b427f50c1711a5e96c. IsDrawing packages an abstract graph drawn in the plane with every edge an injectively parametrized arc, edge interiors avoiding vertices, and distinct edges meeting only at common vertices; together with [G.Finite] it gives the finite case. This closely realizes a finite linear graph embedded in the plane, but Munkres’s definition is an already-realized Hausdorff union of arcs and is not restricted to the plane.
FC02-C10-U017	exact match	mathlib	Mathlib/Combinatorics/SimpleGraph/Basic.lean::SimpleGraph.completeGraph	P	completeGraph (Fin n) has every pair of distinct vertices adjacent, exactly the source complete graph K_n (written G_n there).
FC02-C10-U018	exact match	mathlib	Mathlib/Combinatorics/SimpleGraph/Basic.lean::completeBipartiteGraph	P	completeBipartiteGraph (Fin 3) (Fin 3) is exactly the utilities graph K_{3,3}.
FC02-C10-U019	unmatched after search	unmatched	—	N	No searched declaration packages Munkres’s theta-space definition as the union of three arcs with exactly the same two endpoints. External Jordan developments use such configurations internally but expose no equivalent general theta-space object.
FC02-C10-U020	partial match / wrong interface	reference-port	mccorvie/classification-of-surfaces@e3c7230fe78d7b056a415d9ecae6f77887046b32, Schoenflies/JordanThetaRegions.lean::Schoenflies.JordanThetaRegions.disjoint_inside; closure_inside_eq_union	R	Apache-2.0, Lean 4.32.0 / Mathlib 81a5d257c8e410db227a6665ed08f64fea08e997. These theorems formalize the region decomposition for a planar Jordan-theta configuration, but require Jordan-circle and local-polygonality hypotheses and state disjointness/union of the bounded regions rather than Munkres’s exact three-component enumeration and three boundary formulas.
FC02-C10-U021	exact match	reference-port	alonamaloh/schoenflies-lean@05a43d29cde026618777db3d4e4316204ccca237, Schoenflies/Graph/K33Land.lean::Graph.k33Graph_not_exists_isDrawing; Graph.IsArcK33.elim	R	Apache-2.0, Lean 4.32.2 / Mathlib 905b95818eb32af7874a58b427f50c1711a5e96c. The concrete theorem states there is no plane drawing of K_{3,3} with the repository’s arc-drawing interface; this is exactly nonplanarity of the utilities graph.
FC02-C10-U022	partial match / wrong interface	reference-port	alonamaloh/schoenflies-lean@05a43d29cde026618777db3d4e4316204ccca237, Schoenflies/FaceCyclesLand.lean::Graph.face_cycles'	R	Apache-2.0, Lean 4.32.2 / Mathlib 905b95818eb32af7874a58b427f50c1711a5e96c. The theorem proves that every face of a finite two-connected polygonal plane drawing is bounded by a graph cycle, supplying the face-boundary mechanism used by the source K4 claim. It does not package the K4-specific count of four components or identify the four opposite triangles, and it assumes polygonal edges.
FC02-C10-U023	unmatched after search	unmatched	—	N	No searched Lean declaration proves nonplanarity of K₅. The located plane-graph development proves K_{3,3} nonplanarity but exposes no K5 theorem.
FC02-C10-U024	unmatched after search	unmatched	—	N	No searched Lean implementation of Kuratowski’s planar-graph characterization was found. Loogle’s declarations named Kuratowski concern the metric-space Kuratowski embedding and are unrelated.
FC02-C10-U025	unmatched after search	unmatched	—	N	No searched theorem realizes the K4-diagonal configuration and proves both diagonal points lie in different complementary components of the 4-cycle and that the cycle inclusion induces a fundamental-group isomorphism.
FC02-C10-U026	unmatched after search	unmatched	—	N	No searched declaration proves that inclusion of an arbitrary Jordan curve into the sphere punctured at points from the two complementary components induces an isomorphism on fundamental groups. Existing Jordan and punctured-plane developments do not package this bridge.
FC02-C10-U027	unmatched after search	unmatched	—	N	No searched current Mathlib/external declaration defines Munkres’s integer winding number of a closed planar loop by lifting its normalized map to the universal cover of S¹. Mathlib’s current undergraduate coverage file explicitly leaves winding number unimplemented.
FC02-C10-U028	broad match	mathlib	Mathlib/Topology/Homotopy/Basic.lean::ContinuousMap.Homotopy; ContinuousMap.Homotopic; additive-circle/circle map infrastructure	P	A free homotopy of loops is exactly an ordinary homotopy after representing loops as maps from S¹ (or AddCircle 1) rather than interval maps with the seam equation F(0,t)=F(1,t). Mathlib has this equivalent map-space interface, not a dedicated interval-loop FreeHomotopy definition.
FC02-C10-U029	unmatched after search	unmatched	—	N	Without a winding-number object, no searched declaration proves the bundled reversal, free-homotopy invariance, and constancy-on-complement-components lemmas in the source. Path-lifting and homotopy-lifting infrastructure alone is not credited as those results.
FC02-C10-U030	exact match	reference-port	alonamaloh/schoenflies-lean@05a43d29cde026618777db3d4e4316204ccca237, Schoenflies/Curve.lean::Schoenflies.IsLoop	R	Apache-2.0, Lean 4.32.2 / Mathlib 905b95818eb32af7874a58b427f50c1711a5e96c. IsLoop requires continuity on [0,1], equality of the endpoint values, and injectivity on [0,1), exactly Munkres’s simple-loop condition for a planar parametrization.
FC02-C10-U031	unmatched after search	unmatched	—	N	No searched proved declaration establishes that a simple planar loop has winding number 0 on the unbounded complementary component and ±1 on the bounded component. Jordan separation exists externally, but the winding-number theorem does not.
FC02-C10-U032	unmatched after search	unmatched	—	N	No searched declaration packages clockwise/counterclockwise orientation by winding ±1 and proves the standard (cos 2πs, sin 2πs) loop has winding +1 about the origin.
FC02-C10-U033	unmatched after search	unmatched	—	N	No searched theorem identifies the topological winding number of a piecewise differentiable loop with (2πi)⁻¹∫ dz/(z-a). Mathlib has circle-integral identities but no general winding-number object to state this equality.
FC02-C10-U034	partial match / wrong interface	mathlib	Mathlib/Analysis/Complex/CauchyIntegral.lean::Complex.circleIntegral_sub_inv_smul_of_differentiable_on_off_countable; DiffContOnCl.two_pi_i_inv_smul_circleIntegral_sub_inv_smul; circleIntegral_div_sub_of_differentiable_on_off_countable	P	Pinned Mathlib proves the Cauchy integral formula for geometric circles/discs (with stronger allowance of countably many interior nondifferentiability points in one version). Munkres states the formula for an arbitrary simple closed piecewise-differentiable Jordan curve with sign determined by orientation; the general Jordan-contour statement is not present, so the match is substantive but not exact.

Provenance contract for C11

• Project search: LeanCategories/** outside .lake was searched for direct-sum/free-product/free-group presentations and for van Kampen, wedges, cell attachment, torus, and dunce-cap owners. No project-owned C11 theorem or example was found.
• Pinned Mathlib: project pin db584cd6d46c92f209a44c0f1c829460d327499d (v4.33.0, Apache-2.0) has substantial exact algebraic ownership: DirectSum, Monoid.CoprodI, FreeGroup, normal closure, commutators/abelianization, presentations, and the finitely generated abelian structure theorem. It has fundamental-group/path-class and product-groupoid infrastructure, but no topological van Kampen theorem, wedge-of-circles computation, 2-cell attachment theorem, torus fundamental-group computation, or dunce-cap formalization.
• Current Mathlib/open work: current default branch was rechecked 2026-09-05 at 4cbb42e75a050e830b7cf0f2ae748d7644f59cf7. Open PR #41603, head 9a19745bf2565abbbf56bb38c91bcd26c4c53b49, supplies a fundamental-groupoid/cosheaf van Kampen theorem but is unmerged and targets current upstream, so credited rows are reference-port, never pinned Mathlib. Open PR #41856, head 4a1f4b8bf1a32dd2734cd68d01db22f2af31bc62, supplies AddCircle.windingNumberIso : π₁(S¹) ≃ ℤ; it is likewise reference-port and is not credited as implementing wedge/torus examples that it only makes derivable.
• External/source-atlas search: mdnestor/basic_topology has no C11 implementation. mrdouglasny/jacobian-challenge@8ce1ec28aed1c78b3b39d0bae26e2858c82f5143 (Apache-2.0, Lean 4.30.0, Mathlib c5ea00351c28e24afc9f0f84379aa41082b1188f) contains the vendored Kirov two-open telescoping engine KirovDolbeault/VanKampen.lean, but its proved capstone is a simply-connectedness criterion rather than Munkres’s group pushout/kernel theorem; it is not used as a false exact owner. kadirhanpolat/pytop has an additive-group AmalgamDatum/Pushout formalization but no topological π₁ van Kampen theorem, so it is not credited to the source theorem. An exact Munkres-oriented Isabelle development exists at JUrban/isa_algtop1@37a45d805f4bb382f2ec4237ffe1b710c571f7e1 (including Theorem_68_7_quotient_free_product), but the repository exposes no LICENSE/README and uses Isabelle rather than the project’s Lean toolchain; it is therefore recorded only as negative provenance evidence, not reference-port.
• Negative verdicts below are dated 2026-09-05 and cover project source, pinned/current Mathlib, open Mathlib work, Loogle/LeanSearch where queryable, Reservoir/GitHub Lean searches, and the known topology source-atlas candidates above. Concrete examples are not marked implemented merely because their ingredients are available.

C11 — The Seifert–van Kampen Theorem

FC02 ID	Verdict	Route	Lean target(s)	Provenance	Interface comparison
FC02-C11-U001	broad match	mathlib	Mathlib/Algebra/Group/Subgroup/Lattice.lean::Subgroup.closure_iUnion; subgroup iSup lattice API	P	A family generates the ambient group exactly when the supremum of its subgroups is ⊤; closure_iUnion identifies this with the subgroup generated by their union. In an abelian group this is the source finite-sum notion, though no dedicated GeneratesFamily predicate is used.
FC02-C11-U002	exact match	mathlib	Mathlib/Algebra/DirectSum/Basic.lean::DirectSum.IsInternal; DirectSum.hasFiniteSupport; DirectSum.coeAddMonoidHom	P	IsInternal A is bijectivity of the canonical map from the external finite-support direct sum into the ambient additive group: surjectivity is existence and injectivity is uniqueness of the source finite-support decomposition.
FC02-C11-U003	unmatched after search	unmatched	—	N	Mathlib’s DirectSum/DFinsupp specializes to finitely supported real sequences, but no searched declaration names the source R^∞ subgroup of R^ω and proves it is the internal direct sum of the coordinate subgroups. Under the named-example rule, the generic construction is not an implementation of this example.
FC02-C11-U004	unmatched after search	unmatched	—	N	DirectSum.toAddMonoid gives the extension theorem for the canonical external direct sum, but no searched declaration proves Munkres Lemma 67.1 for an arbitrary family of subgroups of an ambient G, including the converse from generation plus the extension property to internal directness.
FC02-C11-U005	unmatched after search	unmatched	—	N	DirectSum.sigmaCurryEquiv flattens canonical external direct sums, but no searched declaration realizes Corollary 67.2 for nested internal decompositions by the subgroups H_α,H_β inside one ambient group. The external reindexing equivalence is not credited as the internal theorem.
FC02-C11-U006	broad match	mathlib	Mathlib/GroupTheory/QuotientGroup/Basic.lean::QuotientAddGroup.quotientKerEquivOfSurjective; DirectSum.IsInternal	P	Projection onto the first factor of an internal binary direct sum is surjective with kernel the second summand, and the additive first-isomorphism theorem gives the source quotient isomorphism. Mathlib has the exact ingredients but no one-line theorem specialized to an arbitrary internal G = G₁ ⊕ G₂.
FC02-C11-U007	exact match	mathlib	Mathlib/Algebra/DirectSum/Defs.lean::DirectSum; Mathlib/Algebra/DirectSum/Basic.lean::DirectSum.of; DirectSum.IsInternal	P	Mathlib’s external DirectSum together with the injective coordinate maps of is exactly the source external-direct-sum construction/interface.
FC02-C11-U008	exact match	mathlib	Mathlib/Algebra/DirectSum/Defs.lean::DirectSum; Mathlib/Algebra/DirectSum/Basic.lean::DirectSum.of	P	The type DirectSum ι G exists for every indexed family of additive commutative groups and carries the canonical summand maps, directly realizing the existence theorem.
FC02-C11-U009	unmatched after search	unmatched	—	N	Mathlib has the canonical DirectSum.toAddMonoid universal map, but no searched declaration states Lemma 67.5 for an arbitrary candidate group G and family i_α, especially the converse that generation plus the extension property forces injectivity of every i_α and internal directness of the images.
FC02-C11-U010	unmatched after search	unmatched	—	N	No searched declaration packages the source uniqueness theorem for two arbitrary external-direct-sum realizations and the unique isomorphism commuting with all factor monomorphisms. Canonical direct-sum UMP/extensionality makes it derivable but does not itself realize this theorem.
FC02-C11-U011	exact convention	mathlib	Mathlib/Algebra/DirectSum/Basic.lean::DirectSum.of; coercions from summand subtypes	P	The coordinate maps are canonical embeddings, so identifying a summand with its image is exactly the standard coercion/of convention used in the API.
FC02-C11-U012	exact match	mathlib	Mathlib/GroupTheory/FreeAbelianGroup.lean::FreeAbelianGroup; FreeAbelianGroup.of; Mathlib/GroupTheory/FreeGroup/GeneratorEquiv.lean::FreeAbelianGroup.basis	P	FreeAbelianGroup α is the free abelian group on basis α; of is the basis injection and basis realizes the direct-sum-of-copies-of-ℤ structure.
FC02-C11-U013	unmatched after search	unmatched	—	N	FreeAbelianGroup.lift proves the UMP for the canonical free abelian group, but no searched declaration proves the source iff for an arbitrary generated abelian group G: the extension property for the given elements implies that those same elements form a free basis.
FC02-C11-U014	exact match	mathlib	Mathlib/GroupTheory/FreeGroup/GeneratorEquiv.lean::Equiv.ofFreeAbelianGroupEquiv	P	An additive equivalence FreeAbelianGroup α ≃+ FreeAbelianGroup β produces an equivalence α ≃ β; for finite bases this proves equality of basis cardinalities, exactly the source theorem.
FC02-C11-U015	broad match	mathlib	FreeAbelianGroup.basis; Module.rank; basis indexEquiv API	P	The rank is represented by the cardinal-valued Module.rank ℤ / cardinality of the canonical ℤ-basis. Munkres’s terminology is a definition rather than a separate library constant.
FC02-C11-U016	unmatched after search	unmatched	—	N	Subgroup closure/lattice APIs express generated subgroups and CoprodI.Word later supplies reduced words in the canonical free product, but no searched declaration realizes this source definition for an arbitrary family of subgroups together with the finite-product word representation terminology.
FC02-C11-U017	exact match	mathlib	Mathlib/GroupTheory/CoprodI.lean::Monoid.CoprodI.Word	P	Word is a list of tagged factor elements with no identity letters and no adjacent letters from one summand; the empty list is the identity reduced word. This is exactly the source reduced-word convention.
FC02-C11-U018	exact match	mathlib	Mathlib/GroupTheory/CoprodI.lean::Monoid.CoprodI; Monoid.CoprodI.Word.equiv; Monoid.CoprodI.of_injective	P	Word.equiv : CoprodI M ≃ Word M gives existence and uniqueness of reduced-word normal forms, while of_injective identifies each factor as a subgroup. This realizes the source free product.
FC02-C11-U019	unmatched after search	unmatched	—	N	Pinned Mathlib has permutation/transposition identities such as Equiv.swap_mul_swap_mul_swap, but no searched declaration realizes the complete source counterexample: the two order-two subgroups generate S₃ and the displayed two distinct reduced words coincide. Generic permutation infrastructure is not credited as the concrete example.
FC02-C11-U020	exact match	mathlib	Mathlib/GroupTheory/CoprodI.lean::Monoid.CoprodI.lift; lift_comp_of; ext_hom	P	lift is precisely the unique homomorphism from the free product extending an arbitrary family of factor homomorphisms.
FC02-C11-U021	exact match	mathlib	Mathlib/GroupTheory/CoprodI.lean::Monoid.CoprodI; Monoid.CoprodI.of; of_injective	P	The indexed coproduct plus its injective factor maps is exactly an external free product.
FC02-C11-U022	exact match	mathlib	Mathlib/GroupTheory/CoprodI.lean::Monoid.CoprodI; Monoid.CoprodI.of_injective	P	CoprodI exists for every indexed family of groups and the canonical factor maps are injective, directly realizing the existence theorem.
FC02-C11-U023	exact match	mathlib	Mathlib/GroupTheory/CoprodI.lean::Monoid.CoprodI.lift; lift_comp_of; ext_hom	P	This is the native universal property of CoprodI, including uniqueness.
FC02-C11-U024	unmatched after search	unmatched	—	N	CoprodI.lift and extensionality establish the UMP for the canonical coproduct, but no searched declaration proves the source uniqueness theorem for two arbitrary generated groups satisfying the extension property, with the unique isomorphism commuting with every factor map.
FC02-C11-U025	unmatched after search	unmatched	—	N	No searched declaration proves Lemma 68.5 for an arbitrary group and family of homomorphisms: the extension property alone forces each map to be injective and the ambient group to have unique reduced-word free-product normal form. Canonical CoprodI facts do not realize this converse theorem.
FC02-C11-U026	unmatched after search	unmatched	—	N	MulEquiv.coprodAssoc and indexed coproduct reindexing flatten canonical external coproducts, but no searched declaration proves the source corollary for nested internal free-product decompositions by the specified subgroups inside one ambient G.
FC02-C11-U027	exact match	mathlib	group conjugation MulAut.conj; Subgroup.Normal	P	Mathlib’s conjugation action and Subgroup.Normal are exactly the source definitions of conjugate elements and normal subgroup.
FC02-C11-U028	exact match	mathlib	Mathlib/Algebra/Group/Subgroup/Basic.lean::Subgroup.normalClosure; normalClosure_eq_iInf	P	normalClosure S is the least normal subgroup containing S, and normalClosure_eq_iInf gives exactly the intersection-of-all-normal-overgroups construction.
FC02-C11-U029	unmatched after search	unmatched	—	N	Neither pinned nor current Mathlib exposes the arbitrary theorem (G₁ * G₂)/⟪N₁,N₂⟫ ≃ (G₁/N₁) * (G₂/N₂). PresentedGroup.coprodPresentations proves a related presentation-level statement, but its hypotheses/interface do not realize this arbitrary quotient theorem.
FC02-C11-U030	unmatched after search	unmatched	—	N	Monoid.Coprod.snd is a surjection killing the left factor and generic first-isomorphism machinery is available, but no searched declaration identifies its kernel with the normal closure of the left factor and packages the resulting quotient isomorphism. The concrete corollary is therefore not marked implemented.
FC02-C11-U031	exact match	mathlib	Mathlib/Algebra/Group/Subgroup/Basic.lean::Subgroup.normalClosure; Group.conjugatesOfSet; conjugatesOfSet_subset_normalClosure; normalClosure_le_normal	P	normalClosure S is defined through closure of the conjugates of S; the API proves it is precisely the subgroup generated by those conjugates, matching the source lemma.
FC02-C11-U032	broad match	mathlib	Mathlib/GroupTheory/FreeGroup/Basic.lean::FreeGroup.of; subgroup closure/generation API; Group.FG	P	Generation by powers is the ordinary subgroup-generation notion; Mathlib separately supplies free-group generators and the finite-generation typeclass. No source-specific notation is needed.
FC02-C11-U033	exact match	mathlib	Mathlib/GroupTheory/FreeGroup/Basic.lean::FreeGroup; Mathlib/GroupTheory/CoprodI.lean::freeGroupEquivCoprodI; IsFreeGroup	P	FreeGroup α is the free group on α; freeGroupEquivCoprodI identifies it with a free product of one-generator free groups, exactly Munkres’s structural definition up to the library’s canonical construction.
FC02-C11-U034	exact match	mathlib	Mathlib/GroupTheory/FreeGroup/Basic.lean::FreeGroup.lift; lift_of; lift_unique	P	FreeGroup.lift is exactly the extension property from arbitrary generator images to a unique homomorphism; the canonical free group supplies the converse realization.
FC02-C11-U035	exact match	mathlib	Mathlib/GroupTheory/CoprodI.lean::FreeGroupBasis.coprodI; instance IsFreeGroup (CoprodI G)	P	The theorem explicitly builds a basis for a free product of free groups from the sigma/disjoint union of the factor bases, exactly the source theorem.
FC02-C11-U036	exact match	mathlib	Mathlib/GroupTheory/FreeGroup/Basic.lean::FreeGroup; FreeGroup.of; Mathlib/GroupTheory/CoprodI.lean::freeGroupEquivCoprodI	P	The canonical FreeGroup α and its equivalence with a free product of copies of the one-generator free group realize the source symbol-and-integer-power construction.
FC02-C11-U037	exact match	mathlib	Mathlib/Algebra/Group/Commutator.lean::commutatorElement; Mathlib/GroupTheory/Commutator/Basic.lean::commutatorSet; commutator; commutator_eq_closure	P	The commutator element is xyx⁻¹y⁻¹, and commutator G is the subgroup generated by all such elements, exactly the source definition.
FC02-C11-U038	exact match	mathlib	Mathlib/GroupTheory/Commutator/Basic.lean::commutator_normal; Mathlib/GroupTheory/Abelianization/Defs.lean::Abelianization; commGroup; commutator_subset_ker; Abelianization.lift	P	The commutator subgroup is normal; the quotient is a commutative group; every map to a commutative group kills the commutator and factors uniquely through the quotient. This is exactly Lemma 69.3.
FC02-C11-U039	exact match / additive wrapper	mathlib	Mathlib/GroupTheory/FreeAbelianGroup.lean::FreeAbelianGroup; Mathlib/GroupTheory/FreeGroup/GeneratorEquiv.lean::FreeAbelianGroup.basis; Abelianization.abelianizationCongr	P	FreeAbelianGroup α is defined as the additive form of the abelianization of FreeGroup α, and its canonical basis is indexed by α. This is precisely the source statement after the multiplicative/additive wrapper.
FC02-C11-U040	exact match	mathlib	Mathlib/GroupTheory/FreeGroup/GeneratorEquiv.lean::Equiv.ofFreeGroupEquiv; Equiv.ofIsFreeGroupEquiv	P	Isomorphic free groups have equivalent generator types; finite generator systems therefore have the same cardinality, exactly the source corollary.
FC02-C11-U041	exact match / equivalent normal form	mathlib	Mathlib/GroupTheory/FiniteAbelian/Basic.lean::AddCommGroup.equiv_free_prod_directSum_zmod; equiv_directSum_zmod_of_finite	P	The structure theorem states every finitely generated abelian group is additively equivalent to ℤ^n times a finite direct sum of ZMod(p^e) with prime p; this is the source free part plus torsion prime-power cyclic decomposition, in a single canonical normal form.
FC02-C11-U042	exact match	mathlib	Mathlib/GroupTheory/PresentedGroup.lean::PresentedGroup; PresentedGroup.mk; mk_surjective; mk_eq_one_iff; Mathlib/GroupTheory/FreeGroup/Basic.lean::FreeGroup.lift	P	PresentedGroup rels is FreeGroup α modulo the normal closure of the relation set; the quotient map is surjective and its kernel is that normal closure. This exactly packages generators, relation subgroup, and a complete relation set.
FC02-C11-U043	exact match	mathlib	Mathlib/GroupTheory/PresentedGroup.lean::PresentedGroup; Mathlib/GroupTheory/FinitelyPresentedGroup.lean::Group.IsFinitelyPresented; exists_mulEquiv_presentedGroup	P	The library defines presentations as free-group quotients by normal closures and finite presentability via finitely many free generators and finitely normally generated kernel, equivalent to Munkres’s finite generators/relations definition.
FC02-C11-U044	broad match / stronger groupoid interface	reference-port	leanprover-community/mathlib4 PR #41603 head 9a19745bf2565abbbf56bb38c91bcd26c4c53b49, Mathlib/AlgebraicTopology/FundamentalGroupoid/VanKampen.lean::FundamentalGroupoid.isSheaf_op_opensToGrpd; VanKampenTransport.vanKampen_opensLeCover; .../VanKampen/IsColimit.lean::van_kampen_groupoid_main	R	Apache-2.0 upstream Mathlib, open/unmerged. The PR proves the stronger basepoint-free fundamental-groupoid cosheaf/colimit van Kampen theorem for open covers. Munkres’s two-open pointed-group universal property follows by taking automorphism groups at the basepoint, but that specialization is not the theorem’s literal interface.
FC02-C11-U045	exact match	mathlib	Mathlib/Topology/Homotopy/Path.lean::Path.Homotopic.Quotient; Path.Homotopic.Quotient.mk; Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean::FundamentalGroup; FundamentalGroup.fromPath	P	Mathlib represents [f] exactly as the quotient class of a path by endpoint-fixed path homotopy, with the ambient space encoded in the path type. The source’s subscripts U,V,U∩V correspond to changing that ambient type.
FC02-C11-U046	unmatched after search	unmatched	—	N	PR #41603 gives the groupoid colimit universal property but no searched declaration states the classical pointed-group map from π₁(U)*π₁(V) is surjective with kernel the normal closure of i₁(g)⁻¹i₂(g). Generic coproduct/normal-closure infrastructure is insufficient under the concrete-example/theorem rule.
FC02-C11-U047	unmatched after search	unmatched	—	N	No searched declaration specializes van Kampen to simply connected overlap and returns the free-product isomorphism on fundamental groups. It is derivable from the open groupoid theorem plus algebra, but not presently realized by a declaration.
FC02-C11-U048	unmatched after search	unmatched	—	N	No searched declaration gives the quotient formula π₁(U)/normalClosure(im π₁(U∩V)) ≃ π₁(X) when V is simply connected. The open van Kampen PR does not package this pointed-group corollary.
FC02-C11-U049	unmatched after search	unmatched	—	N	No searched Lean declaration computes the fundamental group of the theta space as the free group on two generators. Free-product algebra and van Kampen infrastructure do not realize this concrete topological example.
FC02-C11-U050	unmatched after search	unmatched	—	N	No searched pinned/current Mathlib or external source defines the finite topological wedge of circles in the source’s Hausdorff-union formulation. Generic quotient/sum topology constructors are only infrastructure.
FC02-C11-U051	unmatched after search	unmatched	—	N	No searched declaration proves the fundamental group of a finite wedge of circles is free on the circle loops. PR #41856 proves π₁(S¹) ≃ ℤ but does not realize the wedge theorem, and PR #41603 supplies only the general groupoid van Kampen engine.
FC02-C11-U052	exact match	mathlib	Mathlib/Topology/Defs/Induced.lean::Topology.IsCoherentWith; Mathlib/Topology/Coherent.lean::Topology.IsCoherentWith.isOpen_iff; isClosed_iff	P	Mathlib has the source notion under essentially the same name: IsCoherentWith S says relative openness on every member of S implies openness, and the companion theorem gives the equivalent relative-closed-set criterion. This exactly matches Munkres coherent topology for the family of subspaces.
FC02-C11-U053	unmatched after search	unmatched	—	N	No searched declaration packages an arbitrary-index wedge of circles with the final/coherent topology and common basepoint intersection hypotheses. The coinduced topology API alone is not the concrete construction.
FC02-C11-U054	unmatched after search	unmatched	—	N	No searched theorem proves that such an arbitrary wedge is normal and that every compact subset meets only finitely many circle summands. General compactness/normality infrastructure does not realize the source result.
FC02-C11-U055	unmatched after search	unmatched	—	N	No searched declaration computes the fundamental group of the arbitrary coherent wedge as a free group on all circle generators. Neither open Mathlib PR gives this infinite-wedge theorem.
FC02-C11-U056	unmatched after search	unmatched	—	N	No searched Lean declaration formalizes the Hawaiian/infinite earring ⋃ Cₙ ⊂ ℝ² and proves that its subspace topology is not the coherent wedge topology.
FC02-C11-U057	unmatched after search	unmatched	—	N	No searched declaration constructs, for every index type, a topological wedge of circles satisfying Munkres’s coherent-topology definition. Quotient/coinduced constructors make such a construction possible but do not themselves realize the theorem.
FC02-C11-U058	unmatched after search	unmatched	—	N	No searched declaration proves the 2-cell attachment theorem that inclusion on π₁ is surjective with kernel the normal closure of the attaching-circle image. The general van Kampen PR does not package this cell-attachment corollary.
FC02-C11-U059	exact construction / categorical interface	mathlib	Mathlib/Topology/Category/TopCat/Sphere.lean::TopCat.diskBoundaryInclusion; Mathlib/AlgebraicTopology/RelativeCellComplex/AttachCells.lean::AttachCells; nonempty_attachCells_iff; Mathlib/Topology/CWComplex/Abstract/Basic.lean::TopCat.RelativeCWComplex.basicCell	P	Mathlib’s cell-attachment API forms a pushout of the boundary inclusion ∂𝔻 2 ⟶ 𝔻 2 along an attaching map, exactly the construction of adjoining a 2-cell. It is categorical rather than Munkres’s explicit quotient-space presentation; it does not include the fundamental-group conclusion of U058.
FC02-C11-U060	unmatched after search	unmatched	—	N	No searched declaration proves the torus fundamental-group presentation with generators α,β and commutator relation. Product fundamental-groupoid infrastructure plus the circle-π₁ PR makes a computation possible but does not realize this presentation theorem.
FC02-C11-U061	unmatched after search	unmatched	—	N	No searched declaration states π₁(T²) ≃ ℤ² / free abelian rank two. Pinned FundamentalGroupoidFunctor.prodIso and open PR #41856’s AddCircle.windingNumberIso are ingredients only; under the concrete-example rule they are not counted as an implementation of the torus computation.
FC02-C11-U062	unmatched after search	unmatched	—	N	No searched Lean declaration constructs the n-fold dunce cap as the disk quotient identifying boundary points under the order-n rotation action.
FC02-C11-U063	unmatched after search	unmatched	—	N	No searched pinned/current Mathlib theorem states that a closed quotient map from a normal space has normal target. Mathlib has quotient-map and normal-space APIs, but the source preservation theorem is absent.
FC02-C11-U064	unmatched after search	unmatched	—	N	No searched declaration computes the fundamental group of the n-fold dunce cap as the cyclic group of order n; the space itself is also not formalized in the searched sources.

Provenance contract for C12

• Project search: LeanCategories/** outside .lake/.agents/.git was searched first for polygonal edge-pasting, surface-group, first-homology, polygon-word normalization, triangulation, and covering-space conventions; no project-owned C12 declaration was found.
• Pinned Mathlib: project pin db584cd6d46c92f209a44c0f1c829460d327499d (Lean v4.33.0, Apache-2.0) was checked for polygons, presented groups, abelianization/free abelian groups, fundamental-group basepoint transport, connectivity/covering maps, and induced fundamental-group images. It directly owns the abstract H₁ = π₁^ab ingredients/convention and the covering-subgroup convention, but has no surface-specific polygonal quotient theorem, surface π₁/H₁ computation, or surface-classification theorem.
• Current Mathlib / search services: current default branch was rechecked 2026-09-05 at 4cbb42e75a050e830b7cf0f2ae748d7644f59cf7; open-PR, Loogle/LeanSearch, Reservoir, and GitHub Lean searches found no native surface fundamental-group/homology/classification owner filling the negative rows below.
• External/source-atlas search: mccorvie/classification-of-surfaces@e3c7230fe78d7b056a415d9ecae6f77887046b32 is an Apache-2.0 formalization of compact-surface classification with polygonal quotients, signed cyclic presentations, P1/P2/cancellation moves, canonical orientable/nonorientable words, triangulation-to-polygonal realization, and complete normalization. It pins Lean v4.32.0 and Mathlib 81a5d257c8e410db227a6665ed08f64fea08e997, differing from this project pin, so every credited declaration from it is reference-port, never package-import.
• Negative verdicts below are dated 2026-09-05 and cover project source, pinned/current Mathlib, open Mathlib work, indexed search services, and the dedicated external surface-classification source. Generic algebraic or quotient-space ingredients are not credited for concrete surface examples or computations unless an actual declaration realizes the source unit.

C12 — Classification of Surfaces

FC02 ID	Verdict	Route	Lean target(s)	Provenance	Interface comparison
FC02-C12-U001	unmatched after search	unmatched	—	N	No searched declaration packages a filled Euclidean polygonal region together with Munkres’s Bd P/Int P convention. Pinned Mathlib/Geometry/Polygon/Basic.lean::Polygon, Polygon.edgePath, edgeSet, and boundary give cyclic polygon data but not this source object.
FC02-C12-U002	unmatched after search	unmatched	—	N	No searched declaration is the positive affine homeomorphism between two arbitrarily oriented straight segments. The external surface development has PolygonGluing.ParameterDirection.homeomorph on the unit interval, not this segment-to-segment construction.
FC02-C12-U003	broad match	reference-port	mccorvie/classification-of-surfaces@e3c7230fe78d7b056a415d9ecae6f77887046b32, ClassificationOfSurfaces/PolygonalQuotient.lean::PolygonCell; PolygonGluing.PreRealization; Side; ParameterDirection.homeomorph; Identification; Generator; setoid; Realization; mk	R	Apache-2.0, Lean v4.32.0 / Mathlib 81a5d257c8e410db227a6665ed08f64fea08e997. This is a genuine generated side-identification quotient with quotient topology. Its cells are closed disks with marked boundary arcs rather than literal planar polygons, so the topology is faithful but the geometric carrier differs.
FC02-C12-U004	unmatched after search	unmatched	—	N	The external TriangleCell.cellHomeomorph identifies its cell with the standard triangle, but no declaration realizes Munkres Example 1’s particular triangular edge-pasting and proves that quotient homeomorphic to B².
FC02-C12-U005	unmatched after search	unmatched	—	N	The external SphereQuotientHomeomorph.spherePolygonalRealizationHomeomorph proves a sphere quotient for a different two-monogon presentation, not Munkres’s square Example 2. The concrete square example is therefore not credited.
FC02-C12-U006	exact interface / alternate carrier	reference-port	mccorvie/classification-of-surfaces@e3c7230fe78d7b056a415d9ecae6f77887046b32, ClassificationOfSurfaces/CellComplex.lean::SurfaceCellComplex.SignedDart; SurfaceCellComplex.oneFacePresentation; ClassificationOfSurfaces/CanonicalWords.lean signed boundary words	R	The signed-dart one-face presentation is exactly a cyclic labelling scheme with orientation signs. It replaces printed edge labels/exponents by a typed signed-dart word.
FC02-C12-U007	unmatched after search	unmatched	—	N	External Examples.lean::torusCellComplex has boundary word aba⁻¹b⁻¹, but no declaration identifies its polygonal realization with the standard torus. Under the named-example rule the word alone is not the requested quotient-homeomorphism example.
FC02-C12-U008	unmatched after search	unmatched	—	N	External projectivePlaneCellComplex realizes the canonical aa word, not Munkres’s specified square word abab; no square-to-RP² homeomorphism matching the source example was found.
FC02-C12-U009	unmatched after search	unmatched	—	N	External mobiusStripCellComplex realizes aah, not Munkres’s one-square abac/two-square presentation, and no declaration proves the requested concrete quotient equivalence.
FC02-C12-U010	unmatched after search	unmatched	—	N	The external multi-face quotient machinery is generic, but no declaration realizes Munkres’s concrete disconnected two-square Example 6.
FC02-C12-U011	unmatched after search	unmatched	—	N	No searched theorem establishes compact Hausdorffness for every finite polygonal edge-pasting in the source interface. Quotient compactness/Hausdorff ingredients do not by themselves realize this theorem.
FC02-C12-U012	unmatched after search	unmatched	—	N	Pinned Mathlib/GroupTheory/PresentedGroup.lean::PresentedGroup, Subgroup.normalClosure, and FundamentalGroup provide the algebraic target, but no searched van-Kampen/polygon theorem identifies a polygonal quotient’s π₁ with the stated generator-relator presentation.
FC02-C12-U013	exact normal-form word	reference-port	mccorvie/classification-of-surfaces@e3c7230fe78d7b056a415d9ecae6f77887046b32, ClassificationOfSurfaces/CanonicalWords.lean::orientableHandleBlock; orientableBoundaryWord; orientableCellComplex	R	At boundary count zero these give exactly the 4p-letter product-of-commutators one-face word for the orientable genus-p surface. The implementation uses the canonical polygonal normal form rather than an independent connected-sum constructor.
FC02-C12-U014	unmatched after search	unmatched	—	N	No searched declaration computes the fundamental group of the orientable normal-form surface. PresentedGroup and commutator syntax are only algebraic ingredients without the topological π₁ identification.
FC02-C12-U015	exact normal-form word	reference-port	mccorvie/classification-of-surfaces@e3c7230fe78d7b056a415d9ecae6f77887046b32, ClassificationOfSurfaces/CanonicalWords.lean::nonOrientableCrosscapBlock; nonOrientableBoundaryWord; nonOrientableCellComplex	R	At boundary count zero these give exactly the one-face word a₁a₁⋯aₚaₚ for the nonorientable normal form. As above, this is the canonical word realization rather than a separate connected-sum construction.
FC02-C12-U016	unmatched after search	unmatched	—	N	No searched declaration computes the fundamental group of the nonorientable normal-form surface from this word. Generic presentations are not credited for the missing topological theorem.
FC02-C12-U017	broad match / definition-level API	mathlib	Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean::FundamentalGroup; fundamentalGroupMulEquivOfPathConnected; Mathlib/GroupTheory/Abelianization/Defs.lean::Abelianization; Abelianization.of; MulEquiv.abelianizationCongr	P	At a chosen basepoint, Munkres’s first homology group is exactly the abelianization of the fundamental group. Path-connected basepoint transport is available and abelianization transports across the resulting equivalence; Mathlib does not package the source’s basepoint-free H₁(X) notation as one named object.
FC02-C12-U018	unmatched after search	unmatched	—	N	Pinned Subgroup.map_commutator, map_commutator_eq, Abelianization.map, and QuotientGroup.quotientQuotientEquivQuotient are ingredients, but no declaration states the exact abelianization-of-F/N quotient formula; substantive quotient/join bookkeeping remains.
FC02-C12-U019	unmatched after search	unmatched	—	N	FreeAbelianGroup α := Additive (Abelianization (FreeGroup α)), FreeAbelianGroup.equivFinsupp, and presented-group APIs exist, but no searched declaration gives the source single-relator abelianization theorem.
FC02-C12-U020	unmatched after search	unmatched	—	N	No searched declaration computes H₁ of the orientable n-fold surface in the source form.
FC02-C12-U021	unmatched after search	unmatched	—	N	No searched declaration computes the rank-plus-ℤ/2 torsion form of H₁ for the nonorientable m-fold surface.
FC02-C12-U022	unmatched after search	unmatched	—	N	External EvalStatement.lean::classification_of_surfaces / topological_classification_of_surfaces proves existence of sphere/orientable/nonorientable normal-form representatives, but not uniqueness or pairwise nonhomeomorphism; no surface π₁/H₁ invariant calculation in that source closes Munkres Theorem 75.5.
FC02-C12-U023	exact move / alternate polygon model	reference-port	mccorvie/classification-of-surfaces@e3c7230fe78d7b056a415d9ecae6f77887046b32, ClassificationOfSurfaces/FiniteCyclicP2.lean::P2Cut; P2.split; P2.isNondegenerate_iff_lengths_pos; FiniteCyclicP2Realization.lean::P2.nondegeneratePolygonallyEquivalent	R	This is the face-splitting operation introducing a separator, together with the resulting polygonal-realization equivalence. Munkres’s length-at-least-two side condition is stronger than the repository’s nondegeneracy/positivity condition, but the move is the same.
FC02-C12-U024	broad match	reference-port	mccorvie/classification-of-surfaces@e3c7230fe78d7b056a415d9ecae6f77887046b32, FiniteCyclicPresentation.lean::EdgeRelabeling; SignedPresentationIso; cyclic boundary rotation; FiniteCyclicP2*.lean split/paste; FiniteCyclicUnorientedRealization.lean::UnorientedPresentationIso; FiniteCyclicCancellation.lean::Cancellation.normalizationEquivalent	R	These concrete operations realize relabelling/reorientation, cyclic/flip changes, cutting/pasting, and cancellation/uncancellation while preserving the polygonal realization. They use the repository’s typed P1/P2/signed-isomorphism vocabulary instead of Munkres’s list of elementary scheme moves.
FC02-C12-U025	exact closure semantics	reference-port	mccorvie/classification-of-surfaces@e3c7230fe78d7b056a415d9ecae6f77887046b32, ClassificationOfSurfaces/FiniteCyclicNormalization.lean::NormalizationStep; NormalizationEquivalent; NormalizationEquivalent.refl; symm; trans; polygonallyEquivalent	R	NormalizationEquivalent is the equivalence closure of the elementary normalization steps and carries a polygonal-realization equivalence, exactly the source notion of schemes related by finitely many allowed elementary operations.
FC02-C12-U026	unmatched after search	unmatched	—	N	No project/pinned/current/external declaration realizes the Klein-bottle labelling-scheme example in the exact source form. The dedicated surface repository contains torus/projective examples but no Klein-bottle declaration found by exact search.
FC02-C12-U027	unmatched after search	unmatched	—	N	No named proper-scheme predicate matches “every label occurs exactly twice.” External FiniteCyclicPresentation.IsSurfaceValid allows boundary labels of multiplicity one as well as paired labels, so its semantics are strictly broader.
FC02-C12-U028	unmatched after search	unmatched	—	N	No global torus-type/projective-type predicate matching Munkres was found. External FiniteCyclicWordReductionCore.lean::EdgePattern classifies each edge as boundary/crosscap/opposite, but does not itself state the source whole-word dichotomy.
FC02-C12-U029	exact match / cyclic spelling	reference-port	mccorvie/classification-of-surfaces@e3c7230fe78d7b056a415d9ecae6f77887046b32, ClassificationOfSurfaces/FiniteCyclicWordReduction.lean::CrosscapOccurrenceForm.groupedWord; CrosscapOccurrenceForm.exists_normalizationEquivalent_grouped	R	Exactly groups an equally oriented repeated label into an adjacent crosscap pair, with the intervening/remainder word transformed as required; the statement is modulo the repository’s cyclic-word spelling.
FC02-C12-U030	unmatched after search	unmatched	—	N	The external normalizer iteratively groups crosscaps and reaches a canonical form, but no declaration states the intermediate Corollary 77.2 form (a₁a₁)…(aₖaₖ)w₁ with w₁ torus type or empty. The stronger eventual algorithm is not credited as this absent intermediate statement.
FC02-C12-U031	exact match / cyclic context	reference-port	mccorvie/classification-of-surfaces@e3c7230fe78d7b056a415d9ecae6f77887046b32, ClassificationOfSurfaces/FiniteCyclicDerivedRewrites.lean::Handle.normalizationEquivalent; Handle.target_boundary_isRotated_handle	R	Exactly extracts an aba⁻¹b⁻¹ handle block from interleaved oppositely oriented pairs, modulo surrounding context and cyclic rotation.
FC02-C12-U032	exact match / cyclic context	reference-port	mccorvie/classification-of-surfaces@e3c7230fe78d7b056a415d9ecae6f77887046b32, ClassificationOfSurfaces/FiniteCyclicDerivedRewrites.lean::HandleToCrosscaps.normalizationEquivalent; HandleToCrosscaps.target_boundary_isRotated_crosscaps	R	This is the source crosscap-plus-handle rewrite into three crosscaps (cc·aba⁻¹b⁻¹ ~ aa·bb·cc) up to relabelling, context, and cyclic spelling.
FC02-C12-U033	broad match / stronger normalization theorem	reference-port	mccorvie/classification-of-surfaces@e3c7230fe78d7b056a415d9ecae6f77887046b32, ClassificationOfSurfaces/NormalForm.lean::FiniteCyclicPresentation.hasEvalRepresentative; EvalStatement.lean::classification_of_surfaces; topological_classification_of_surfaces; FiniteCyclicTerminalNormalization.lean::exists_admissible_normalForm_polygonallyEquivalent	R	This gives the complete sphere/orientable/nonorientable polygonal classification. The formal normal forms include a boundary-count parameter; Munkres’s closed pairwise-pasted case requires the adapter setting that parameter to zero and identifying the resulting representatives with T_p/P_p, so the external theorem is stronger but not literally the same signature.
FC02-C12-U034	broad match / alternate triangulation interface	reference-port	mccorvie/classification-of-surfaces@e3c7230fe78d7b056a415d9ecae6f77887046b32, ClassificationOfSurfaces/Moise/GeometricTriangulation.lean::GeometricTriangulation; nonempty_geometricTriangulation_iff_explicit	R	The external interface gives a finite family of geometric 2-simplices with a barycentric realization homeomorphism. It replaces Munkres’s curved-triangle charts and linear edge-transition axioms by a canonical simplicial realization.
FC02-C12-U035	broad match	reference-port	mccorvie/classification-of-surfaces@e3c7230fe78d7b056a415d9ecae6f77887046b32, ClassificationOfSurfaces/Triangulation.lean::GeometricTriangulation.toFiniteSurfaceTriangulation; surfaceIncidence; FiniteCyclicTriangulation.lean::GeometricTriangulation.toFiniteCyclicPresentation; toFiniteCyclicPresentation_isSurfaceValid; GeometricTriangulationRealization.lean::polygonalRealization_homeomorphic_of_surface	R	This is the exact bridge from a finite triangular surface realization to a finite polygonal quotient with paired/internal edge identifications and a homeomorphic realization. The hypotheses are encoded through the manifold/incidence interface rather than Munkres’s printed curved-triangle overlap axioms.
FC02-C12-U036	exact reduction / alternate presentation	reference-port	mccorvie/classification-of-surfaces@e3c7230fe78d7b056a415d9ecae6f77887046b32, ClassificationOfSurfaces/FiniteCyclicReduction.lean::OneFaceReduction; reduceToOneFace; FiniteCyclicNormalization.lean::NormalizationEquivalent.polygonallyEquivalent	R	Repeated face merges reduce a connected valid multi-face presentation to one face and preserve the polygonal realization, exactly the reduction required before applying the one-polygon classification.
FC02-C12-U037	exact convention	mathlib	Mathlib/Topology/Connected/PathConnected.lean::PathConnectedSpace; Mathlib/Topology/Connected/LocallyPathConnected.lean::LocallyPathConnectedSpace; Mathlib/Topology/Covering/Basic.lean::IsCoveringMap	P	Munkres’s standing convention is represented directly by typeclass assumptions [PathConnectedSpace B] [LocallyPathConnectedSpace B] [PathConnectedSpace E]; IsCoveringMap itself intentionally does not bundle these connectivity assumptions.
FC02-C12-U038	exact match / expression rather than alias	mathlib	Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean::FundamentalGroup.map; FundamentalGroup.mapOfEq; Mathlib/Topology/Homotopy/Lifting.lean::IsCoveringMap.existsUnique_continuousMap_lifts_of_range_le; ker_monodromyPerm	P	The associated subgroup is exactly (FundamentalGroup.mapOfEq ⟨p, hp.continuous⟩ e.2).range; Mathlib uses this expression directly in its lifting/monodromy theorems rather than introducing a separate alias H₀.

Provenance contract for C13

• Project search: LeanCategories/** outside .lake/.agents/.git was searched first for covering-space classification, universal covers, deck groups, quotient actions, and semilocal simple connectivity; no project-owned C13 theorem/example was found.
• Pinned Mathlib: project pin db584cd6d46c92f209a44c0f1c829460d327499d (Lean v4.33.0, Apache-2.0) owns the general covering-space lifting criterion, fundamental-group map/range infrastructure, subgroup conjugation/normalizers, orbit quotients, quotient-covering infrastructure, and the ambient definitions needed below. It does not yet contain the connected-cover classification/deck-group theorem suite.
• Current Mathlib: default branch rechecked 2026-09-05 at 4cbb42e75a050e830b7cf0f2ae748d7644f59cf7; its new Mathlib/Topology/Covering/Deck.lean supplies the deck-transformation subgroup but is post-pin and therefore recorded only as a reference-port.
• Current Mathlib freshness recheck (2026-09-06): upstream HEAD is 810b3888d0aa94294b18587c453466bc86c1f0fc; the 4cbb42e75a050e830b7cf0f2ae748d7644f59cf7..810b3888d0aa94294b18587c453466bc86c1f0fc file delta contains no Mathlib/Topology, Mathlib/AlgebraicTopology, covering, graph, or free-group path, so the C13 current-Mathlib positive owner and negative searches are unchanged.
• External/source-atlas search: Tau-Ceti/lean at 907e560a48c8b8a8a74ad9d9a6871c2431939fed (Apache-2.0, Lean 4.34.0-rc2, Mathlib 5fcc6656691ed31965746c369f41fa75e567ac9d) contains a substantial, source-shaped classification of connected covers, universal covers, monodromy, deck groups, regular covers, subgroup realizations, and semilocal simple connectivity. Its post-pin toolchain makes every credited TauCeti row reference-port, never package-import.
• TauCeti freshness recheck (2026-09-06): upstream HEAD is f67536627686de753796221ae5a6d503061369cd; the complete 907e560a48c8b8a8a74ad9d9a6871c2431939fed..f67536627686de753796221ae5a6d503061369cd path delta is confined to analysis/PDE/Sobolev, Hecke-ring, and Huber-ring files, with no topology/covering/graph change. Lean 4.34.0-rc2 and Mathlib 5fcc6656691ed31965746c369f41fa75e567ac9d are unchanged, so the dated C13 negative covering-space searches remain valid against current TauCeti HEAD.
• Arthur742Ramos/ComputationalPathsLean@f90943eecdde516817fbc33863486b681a0a9645 is MIT and exactly matches this project’s Lean/Mathlib pins, but its deeper covering-space APIs are bespoke computational-path data rather than Mathlib topological IsCoveringMap, so no C13 row is credited from it merely for compatibility.
• Negative verdicts below are dated 2026-09-05 and cover project source, pinned/current Mathlib, open/current work, TauCeti, ComputationalPaths, indexed search services, and the local source atlas. Concrete examples are not credited merely because their generic ingredients are formalized.

C13 — Classification of Covering Spaces

FC02 ID	Verdict	Route	Lean target(s)	Provenance	Interface comparison
FC02-C13-U001	exact match / categorical packaging	reference-port	TauCeti/Topology/Covering/Category.lean::CoveringSpace.isoMk; CoveringSpace.isIso_iff_isHomeomorph_hom_left; CoveringSpace.w	R	TauCeti 907e560a…, Apache-2.0, Lean 4.34.0-rc2 / Mathlib 5fcc665…. An isomorphism in CoveringSpace B is exactly a homeomorphism of total spaces commuting with the two projections, i.e. Munkres equivalence of covering spaces.
FC02-C13-U002	exact mathematical coverage / iff split across API	mathlib	Mathlib/Topology/Homotopy/Lifting.lean::IsCoveringMap.existsUnique_continuousMap_lifts_of_range_le; FundamentalGroup.map; FundamentalGroup.mapOfEq	P	The lifting theorem has the path-connected/local-path-connected source hypotheses, basepoint condition, induced-subgroup inclusion, existence, and uniqueness. The converse follows from functoriality of the induced fundamental-group maps when p ∘ F = f; TauCeti later packages the iff directly.
FC02-C13-U003	exact match	reference-port	TauCeti/AlgebraicTopology/UniversalCover/Classification/Pointed.lean::IsCoveringMap.exists_homeomorph_comp_eq_iff_range_eq; IsCoveringMap.eq_totalSpaceHomeomorphOfRangeEq	R	Exactly: pointed connected covers are equivalent over the base iff their recovered subgroups are equal, with uniqueness of the comparison map.
FC02-C13-U004	exact definition-level encoding	mathlib	Mathlib/GroupTheory/GroupAction/ConjAct.lean::ConjAct; Subgroup.pointwiseMulAction; MulAction.orbitRel	P	Conjugation acts on Subgroup G; two subgroups are conjugate exactly when they lie in one orbit, and the orbit quotient is the conjugacy-class object.
FC02-C13-U005	exact match / split declarations	reference-port	TauCeti/Topology/Homotopy/Monodromy/Basic.lean::IsCoveringMap.range_mapOfEq_monodromy; exists_monodromy_eq_of_joined; exists_range_eq_map_conj; exists_range_eq_map_conj_of_joined	R	Changing the lift in one connected cover conjugates the recovered subgroup, and every conjugate is realized by monodromy of a suitable loop/fiber point, exactly the two clauses of Lemma 79.3.
FC02-C13-U006	exact match	reference-port	TauCeti/AlgebraicTopology/UniversalCover/Classification/Unpointed.lean::IsCoveringMap.exists_homeomorph_comp_eq_iff_exists_range_eq_map_conj	R	Exact unpointed classification: connected covers are equivalent over the base iff the recovered subgroups are conjugate.
FC02-C13-U007	unmatched after search	unmatched	—	N	Pinned AddCircle.isCoveringMap_coe, isAddQuotientCoveringMap_nsmul_of_ne_zero, Int.subgroup_cyclic, and TauCeti’s AddCircle.fundamentalGroupMulEquivInt give the ingredients, but no searched declaration proves that the degree-n cover recovers nℤ and that every connected cover of S¹ is equivalent to one of these models.
FC02-C13-U008	exact definition-level API	mathlib	Mathlib/Topology/Covering/Basic.lean::IsCoveringMap; Mathlib/AlgebraicTopology/FundamentalGroupoid/SimplyConnected.lean::SimplyConnectedSpace	P	Munkres’s universal-cover definition is exactly a covering map whose total space is simply connected; Mathlib represents this by the conjunction rather than a redundant alias.
FC02-C13-U009	unmatched after search	unmatched	—	N	No searched declaration restricts an arbitrary cover to a path component of its total space and proves the restriction remains a cover. Pinned IsCoveringMap.restrictPreimage restricts the base, while TauCeti’s path-component cover is a different canonical construction.
FC02-C13-U010	partial match: (a) exact, generic (b) absent	reference-port	TauCeti/Topology/Covering/Factorization.lean::IsCoveringMap.of_comp_eq; special quotient case TauCeti/Topology/Covering/Quotient.lean::IsQuotientCoveringMap.isCoveringMap_of_comp	R	IsCoveringMap.of_comp_eq gives part (a), under TauCeti’s local-connectedness hypotheses. No generic declaration for part (b) was found; the cited quotient-cover theorem proves only a special case.
FC02-C13-U011	exact match	reference-port	TauCeti/AlgebraicTopology/UniversalCover/Classification/Intermediate.lean::IsCoveringMap.exists_isCoveringMap_comp_eq_iff_range_le; UniversalCover.exists_isCoveringMap_comp_eq_proj; FundamentalGroup.mapOfEq_range_eq_bot_of_subsingleton	R	A simply connected source has recovered subgroup ⊥, so the intermediate-cover criterion yields a covering comparison map through every other cover; the canonical universal-cover theorem states the factorization directly.
FC02-C13-U012	unmatched after search	unmatched	—	N	TauCeti defines and characterizes semilocal simple connectivity, but its universal-cover constructions assume it. No searched theorem derives the source neighborhood/π₁-triviality condition merely from existence of a simply connected covering space.
FC02-C13-U013	unmatched after search	unmatched	—	N	ComputationalPaths’ Hawaiian-earring file assumes an external loop-space obstruction and proves a quotient-topology transfer; it neither constructs the Munkres earring with the stated connectivity properties nor proves nonexistence of a universal cover. No requested theorem was found elsewhere.
FC02-C13-U014	exact match	reference-port	current Mathlib 4cbb42e75a050e830b7cf0f2ae748d7644f59cf7, Mathlib/Topology/Covering/Deck.lean::deck; deck.mem_iff; deck.comp_eq	R	Apache-2.0, post-pin Lean 4.34.0-rc2. deck p : Subgroup (E ≃ₜ E) is exactly the group of self-homeomorphisms satisfying p ∘ h = p, i.e. covering/deck transformations.
FC02-C13-U015	exact match	mathlib	Mathlib/Algebra/Group/Subgroup/Defs.lean::Subgroup.normalizer; mem_normalizer_iff; le_normalizer; Mathlib/Algebra/Group/Subgroup/Basic.lean::normal_subgroupOf_iff_le_normalizer; normal_in_normalizer; maximal_normal_subgroupOf_normalizer	P	Exact normalizer definition, subgroup property, containment H ≤ N(H), normality of H inside its normalizer, and the maximal/largest-subgroup characterization.
FC02-C13-U016	exact match / correspondence orientation reversed	reference-port	TauCeti/Topology/Homotopy/Monodromy/Basic.lean::IsCoveringMap.fiberEquivQuotientRange; fiberEquivQuotientRange_symm_apply_mk; TauCeti/AlgebraicTopology/UniversalCover/Deck/Connected/Basic.lean::Deck.orbitMap_injective	R	TauCeti identifies the fiber with the coset quotient and characterizes the inverse by monodromy; this is Munkres’s Φ with the displayed arrow reversed. Deck evaluation at a chosen fiber point is injective, exactly the Ψ claim.
FC02-C13-U017	exact match / assembled declarations	reference-port	TauCeti/AlgebraicTopology/UniversalCover/Deck/Quotient/Normalizer.lean::normalizerDeckHom_apply; ker_normalizerDeckHom; normalizerDeckHom_surjective; Classification/Bijection.lean::exists_homeomorph_subgroupQuotient_of_range_eq	R	The normalizer action and its quotient by H₀, transported from the subgroup-quotient model to an arbitrary connected cover, identify exactly the deck-evaluation image with Φ(N(H₀)/H₀).
FC02-C13-U018	exact match	reference-port	TauCeti/AlgebraicTopology/UniversalCover/Classification/DeckGroup.lean::UniversalCover.deckSubgroupQuotientProjEquiv; generic Deck.IsQuotientCoveringMap.normalizerQuotientDeckMulEquiv	R	Gives the group isomorphism N(H)/H ≃* Deck, the same theorem as Φ⁻¹ ∘ Ψ up to direction of the displayed equivalence and transport from the canonical subgroup cover.
FC02-C13-U019	exact match	reference-port	TauCeti/AlgebraicTopology/UniversalCover/Classification/Regular.lean::IsCoveringMap.isRegular_iff_normal_range; Classification/DeckGroup.lean::deckSubgroupQuotientProjEquivOfNormal; Deck/Regular/Basic.lean::isRegular_iff_exists_apply_eq	R	Exact normal-subgroup iff deck-transitivity criterion; in the normal case the deck group is the quotient π₁/H.
FC02-C13-U020	exact match / opposite-group convention	reference-port	TauCeti/AlgebraicTopology/UniversalCover/Deck/FundamentalGroup/UniversalCover.lean::UniversalCover.deckFundamentalGroupEquiv	R	Gives Deck(proj) ≃* (FundamentalGroup B b₀)ᵐᵒᵖ; the opposite group is the standard left-action/composition convention and is equivalent to Munkres’s displayed deck-group/π₁ isomorphism via inversion.
FC02-C13-U021	exact match / equivalent definition	reference-port	TauCeti/AlgebraicTopology/UniversalCover/Deck/Regular/Basic.lean::Deck.IsRegular; Classification/Regular.lean::IsCoveringMap.isRegular_iff_normal_range	R	TauCeti defines regularity by deck transitivity on fibers and proves it equivalent to normality of the recovered subgroup, exactly Munkres’s definition for connected covers.
FC02-C13-U022	broad match / concrete universal-cover computation	reference-port	TauCeti/AlgebraicTopology/UniversalCover/AddCircle.lean::Deck.addRightZMultiples; addRightZMultiples_apply; Deck.isRegular_addCircleCoe; Deck.addCircleMulEquivInt; addCircleMulEquivInt_apply	R	For ℝ → AddCircle 1, deck transformations are explicitly x ↦ x+n and the deck group is ℤ. No standalone declaration says every S¹ cover is regular, although it follows from the general normal-range criterion plus the cyclic fundamental group.
FC02-C13-U023	unmatched after search	unmatched	—	N	No searched project, pinned/current Mathlib, TauCeti, or ComputationalPaths declaration realizes the displayed figure-eight cover and proves its covering-transformation group is trivial.
FC02-C13-U024	exact match	mathlib	Mathlib/GroupTheory/GroupAction/Defs.lean::MulAction.orbitRel; MulAction.orbitRel.Quotient; orbitRel.Quotient.orbit; orbitRel.Quotient.orbit_mk	P	Exact quotient-by-same-orbit equivalence relation and identification of quotient classes with group orbits.
FC02-C13-U025	broad match / stronger standalone convention	mathlib	Mathlib/Topology/Algebra/ConstMulAction.lean::ProperlyDiscontinuousSMul; ProperlyDiscontinuousSMul.exists_nhds_disjoint_image; Mathlib/Topology/Covering/Quotient.lean::IsQuotientCoveringMap.disjoint	P	Mathlib’s named standalone class uses compact-set finiteness; under the standard Hausdorff/local-compactness/continuity/freeness hypotheses its neighborhood-disjointness theorem yields Munkres’s local condition. IsQuotientCoveringMap.disjoint records precisely the local distinct-translate disjointness condition in the quotient-cover structure.
FC02-C13-U026	broad match / assembled quotient-cover theorem	reference-port	pinned Mathlib/Topology/Covering/Quotient.lean::isQuotientCoveringMap_of_properlyDiscontinuousSMul; isQuotientCoveringMap_quotientMk_of_properlyDiscontinuousSMul; IsQuotientCoveringMap.isCoveringMap; isQuotientCoveringMap_iff_isCoveringMap_and; TauCeti Deck/Quotient/ActingGroup.lean::IsQuotientCoveringMap.deckMulEquiv; Deck/Quotient/Covering.lean::IsQuotientCoveringMap.isRegular	R	The quotient-cover construction, regularity, and identification of the acting group with the deck group are realized. The pinned properly-discontinuous direction uses stronger LC/T2 hypotheses and Mathlib’s distinct standalone convention, so the complete source-shaped package is recorded as a TauCeti reference-port assembly rather than a pinned exact theorem.
FC02-C13-U027	exact match	reference-port	TauCeti/AlgebraicTopology/UniversalCover/Deck/Quotient/Homeomorph.lean::Deck.IsRegular.orbitQuotientHomeomorphBase; orbitQuotientHomeomorphBase_mk	R	Exactly identifies X/Deck(p) ≃ₜ B, with representative formula k([x])=p(x), hence p=k∘π.
FC02-C13-U028	unmatched after search	unmatched	—	N	No searched declaration gives the two ℤ/2 actions on S¹×I whose orbit spaces are respectively a cylinder and a Möbius band. ComputationalPaths has Möbius-band abstractions but not these actions or orbit-space homeomorphisms.
FC02-C13-U029	exact match	reference-port	TauCeti/AlgebraicTopology/SemilocallySimplyConnected/On.lean::SemilocallySimplyConnectedAt; semilocallySimplyConnectedAt_iff; SemilocallySimplyConnected/Basic.lean::SemilocallySimplyConnectedSpace	R	Exact local definition by existence of a neighborhood whose inclusion-induced fundamental-group map has trivial range, with the equivalent loop-nullhomotopy formulation and global typeclass.
FC02-C13-U030	exact match	reference-port	TauCeti/AlgebraicTopology/UniversalCover/Classification/Existence.lean::UniversalCover.isCoveringMap_subgroupQuotientProj; subgroupCover; Classification/RecoveredSubgroup.lean::range_mapOfEq_subgroupQuotientProj	R	Under path-connected, locally path-connected, semilocally simply connected hypotheses, TauCeti constructs a connected cover for arbitrary H ≤ π₁ and proves its recovered subgroup is exactly H.
FC02-C13-U031	partial match: sufficiency formalized, necessity absent	unmatched	—	N	TauCeti UniversalCover/Covering.lean::UniversalCover.isCoveringMap and its simply-connected-space instance prove the sufficient direction from path connected + locally path connected + semilocally simply connected. No searched declaration proves the converse or the complete iff, so the full corollary remains unmatched.

Provenance contract for C14

• Project search: LeanCategories/** outside .lake/.agents/.git was searched first for linear/topological graph realizations, edge-path reduction, tree/fundamental-group results, Euler characteristic, and Schreier-index results; no project-owned C14 theorem or example was found.
• Pinned Mathlib: project pin db584cd6d46c92f209a44c0f1c829460d327499d (Lean v4.33.0, Apache-2.0) owns the combinatorial oriented-edge/walk API, trees and spanning-tree extension machinery, Nielsen–Schreier, and subgroup index/coset cardinality used below.
• Current Mathlib freshness recheck (2026-09-06): upstream HEAD is 810b3888d0aa94294b18587c453466bc86c1f0fc. The complete file delta from the previously audited 4cbb42e75a050e830b7cf0f2ae748d7644f59cf7 contains no relevant Topology, AlgebraicTopology, quiver/simple-graph, free-group, Schreier, or subgroup-index path, so no C14 verdict is upgraded to current Mathlib.
• Historical Mathlib PR #11604 (feat: Serre graphs, fundamental groups, covering spaces) is closed, unmerged at head 0a7c341ccbe6b354f277b0f48bad76e13e6ea866 (Apache-2.0, Lean 4.7.0-rc2). Its Mathlib/Combinatorics/Multigraph/ReducedPaths.lean supplies the path-reduction construction used only as a revision-specific reference-port for U015.
• Open draft Mathlib PR #41603 (WIP: ... Seifert–van Kampen) remains open at head 9a19745bf2565abbbf56bb38c91bcd26c4c53b49 (Apache-2.0, Lean 4.32.0-rc1). Its Mathlib/AlgebraicTopology/FundamentalGroupoid/VanKampen.lean::relative_vanKampen_subtype is therefore recorded only as a revision-specific reference-port for U022, never as pinned Mathlib.
• alonamaloh/schoenflies-lean was rechecked at current HEAD 05a43d29cde026618777db3d4e4316204ccca237 (Apache-2.0, Lean 4.32.2, Mathlib 905b95818eb32af7874a58b427f50c1711a5e96c). Its finite planar drawing formalization gives the geometric graph owners for U001 and U013, but the older toolchain and specialized plane/drawing hypotheses make them reference-port routes.
• Arthur742Ramos/finite-graph-fundamental-group was rechecked at current HEAD dd57e3ab8bc5a7042fcc5498e778b008d87ac032 (Apache-2.0, Lean 4.32.0, Mathlib 81a5d257c8e410db227a6665ed08f64fea08e997); lake build FiniteGraphFreeGroup succeeds at that revision. It supplies the topological graph-realization, edge-path, no-backtracking, tree-contraction, and graph fundamental-group interfaces below, but is a reference-port against this project’s newer 4.33 pin.
• Arthur742Ramos/GraphCoveringTheory was rechecked at current HEAD c918a72c5170503c98fd66a0f3116b7bfcd1250c (Apache-2.0, Lean 4.32.0, Mathlib 81a5d257c8e410db227a6665ed08f64fea08e997); lake build GraphCoveringTheory succeeds. It includes the finite-graph development and a sharp Schreier-index formalization, again as reference-port only.
• TauCeti was refreshed to upstream HEAD f67536627686de753796221ae5a6d503061369cd; the delta from audited 907e560a48c8b8a8a74ad9d9a6871c2431939fed contains no topology/covering/graph change. ComputationalPaths remains at current HEAD f90943eecdde516817fbc33863486b681a0a9645; its compatible computational bouquet/path developments do not implement the missing Munkres linear-graph assertions. The unlicensed Lean-3 repository dwarn/nielsen-schreier-lean@99fb30c0bf321c651edbb7524101604cf0242ea1 corroborates the sharp index formula but is not a creditable route because no license is present.
• Negative verdicts below are dated 2026-09-06 and cover project source, pinned/current Mathlib, current/open/historical PR work, TauCeti, ComputationalPaths, the two current Arthur742Ramos graph developments, Schoenflies, indexed search services, GitHub/Reservoir searches, and the local source atlas. Generic ingredients are not credited as realizing a concrete Munkres example or topology theorem unless a declaration actually supplies the relevant interface.

C14 — Applications to Group Theory

FC02 ID	Verdict	Route	Lean target(s)	Provenance	Interface comparison
FC02-C14-U001	broad match / specialized geometric realization	reference-port	Schoenflies/Graph/Drawing.lean::Graph.IsDrawing; edge_isArcBetween; arcs_meet_at_vertex; pointSet	R	schoenflies-lean@05a43d29cde026618777db3d4e4316204ccca237 realizes a finite graph as embedded planar arcs meeting only at common endpoints and packages the resulting point set. This is a stronger geometric realization but does not state Munkres’s general coherent-topology axiom for arbitrary linear graphs.
FC02-C14-U002	unmatched after search	unmatched	—	N	No searched declaration proves that an arbitrary Munkres linear graph is Hausdorff or normal. The current finite-graph realization has quotient, compactness, and path-connectedness infrastructure but no corresponding T2Space/normality theorem.
FC02-C14-U003	unmatched after search	unmatched	—	N	No searched declaration constructs an arbitrary wedge of circles as a Munkres linear graph after the stated three-edge subdivision. Bouquet/free-group ingredients do not realize this topological graph example.
FC02-C14-U004	unmatched after search	unmatched	—	N	No searched declaration realizes the quotient of [0,1] × J obtained by collapsing {0} × J for an arbitrary discrete index type and proves it is a linear graph.
FC02-C14-U005	unmatched after search	unmatched	—	N	No searched declaration proves that an arbitrary union of edges of a Munkres linear graph is closed and inherits the required linear-graph structure. Existing combinatorial subgraph APIs do not provide this topology theorem.
FC02-C14-U006	unmatched after search	unmatched	—	N	FiniteGraphFreeGroup.graphRealization_compact proves compactness of a whole finite graph realization, but no searched theorem proves that every compact subset of an arbitrary linear graph lies in a finite subgraph, nor the connected refinement.
FC02-C14-U007	unmatched after search	unmatched	—	N	No searched graph-realization declaration provides both local path connectedness and semilocal simple connectivity for arbitrary Munkres linear graphs. General semilocal-simple-connectivity APIs in TauCeti do not prove the graph instance.
FC02-C14-U008	unmatched after search	unmatched	—	N	The current finite-graph formalization’s graphVertexStar is deliberately a half-open local germ cut inside incident edge cells, not Munkres’s full star/closed-star construction, and no exact closed-star declaration was found.
FC02-C14-U009	unmatched after search	unmatched	—	N	FiniteGraphFreeGroup/TopologicalCover.lean::graphCoverRealizationProjection_isCovering proves that a specified combinatorial graph cover realizes to a topological covering map; no searched theorem proves the converse Munkres assertion that an arbitrary topological cover of a linear graph acquires lifted edge components mapping homeomorphically and an induced linear-graph structure.
FC02-C14-U010	unmatched after search	unmatched	—	N	No searched declaration or project convention identifies the unqualified term “graph” with Munkres’s topological linear-graph structure.
FC02-C14-U011	exact combinatorial encoding	mathlib	Mathlib/Combinatorics/SimpleGraph/Dart.lean::SimpleGraph.Dart; Dart.symm; Dart.edge; DartAdj; Mathlib/Combinatorics/SimpleGraph/Walk/Basic.lean::Walk; Walk.darts; isChain_dartAdj_darts; ofDarts	P	Pinned Mathlib directly represents oriented edges by darts with reversal, edge paths by walks/chains of adjacent darts, and closed edge paths by walks with equal endpoints.
FC02-C14-U012	exact match in a graph realization model	reference-port	FiniteGraphFreeGroup/Realization.lean::graphEdgePath; graphRealizationForwardPath; graphRealizationSymmetricEdgePath; graphRealizationQuiverPath	R	finite-graph-fundamental-group@dd57e3ab8bc5a7042fcc5498e778b008d87ac032 sends each oriented edge to its characteristic interval path, reverses negative orientations, and concatenates a symmetrified quiver path via Path.trans; endpoint typing makes a closed edge path a loop.
FC02-C14-U013	broad match / finite drawn-graph bridge	reference-port	Schoenflies/SourceOverlay.lean::Graph.IsDrawing.isConnected_pointSet; Schoenflies/CommonSubdivision.lean::Graph.connected_of_isPreconnected_pointSet	R	At schoenflies-lean@05a43d29cde026618777db3d4e4316204ccca237, combinatorial connectedness implies connectedness of the drawn point set, and the converse bridge is proved under the finite drawing/nonempty-vertex hypotheses. This realizes the Munkres edge-path/connectivity principle in a specialized geometric model.
FC02-C14-U014	exact no-backtracking predicate	reference-port	FiniteGraphFreeGroup/TopologicalComparison.lean::symPathNoBacktrack	R	At finite-graph-fundamental-group@dd57e3ab8bc5a7042fcc5498e778b008d87ac032, the inductive cons clause forbids the new oriented edge from being Quiver.reverse of the immediately preceding edge, exactly Munkres’s reduced-edge-path condition.
FC02-C14-U015	exact reduction construction	reference-port	Mathlib PR #11604 head 0a7c341ccbe6b354f277b0f48bad76e13e6ea866, Mathlib/Combinatorics/Multigraph/ReducedPaths.lean::reduction; reduction_reduced; reduction_eq_self_of_reduced; reduction_homotopic_self	R	The closed-unmerged PR recursively cancels adjacent inverse oriented edges and proves the output reduced, fixed on already-reduced paths, and homotopic to the original. Its old Lean 4.7.0-rc2 branch is revision-specific reference material only.
FC02-C14-U016	exact standard combinatorial formulation	mathlib	Mathlib/Combinatorics/SimpleGraph/Acyclic.lean::SimpleGraph.IsAcyclic; SimpleGraph.IsTree; Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean::Subgraph.Connected	P	On a subgraph’s vertex subtype, pinned Mathlib’s IsTree is connected plus acyclic, i.e. absence of graph cycles; this is the standard combinatorial equivalent of Munkres’s connected subgraph with no closed reduced edge path.
FC02-C14-U017	broad match / compositional tree API	mathlib	SimpleGraph.IsAcyclic.sup_edge_of_not_reachable; SimpleGraph.IsTree.exists_vert_degree_one_of_nontrivial; IsTree.exists_ne_and_degree_eq_one; SimpleGraph.Connected.induce_compl_singleton_of_degree_eq_one	P	Pinned Mathlib supplies the two structural ingredients of the lemma: attaching an edge across previously disconnected vertices preserves acyclicity, and every finite nontrivial tree has a leaf whose deletion leaves the remaining tree connected; acyclicity is inherited by subgraphs. The source’s ambient-subgraph union statement is assembled rather than named verbatim.
FC02-C14-U018	exact match for the realized tree model	reference-port	FiniteGraphFreeGroup/TreeContraction.lean::graphRealization_contractible; graphRealization_tree_simplyConnected	R	GraphCoveringTheory@c918a72c5170503c98fd66a0f3116b7bfcd1250c explicitly contracts the realization of a directed tree to a root and derives SimplyConnectedSpace, proving the source conclusion in its graph-realization model.
FC02-C14-U019	exact definition-level encoding	mathlib	Maximal; Mathlib/Combinatorics/SimpleGraph/Acyclic.lean::isTree_iff_maximal_isAcyclic; Connected.maximal_le_isAcyclic_iff_isTree	P	Maximality under inclusion is Mathlib’s Maximal; the specialized acyclic-subgraph theorems provide the standard maximal-tree encoding relative to an ambient graph.
FC02-C14-U020	exact fixed-vertex/spanning translation	mathlib	Mathlib/Combinatorics/SimpleGraph/Subgraph.lean::Subgraph.IsSpanning; isSpanning_iff; Mathlib/Combinatorics/SimpleGraph/Acyclic.lean::Connected.maximal_le_isAcyclic_iff_isTree	P	In a connected ambient graph, a maximal acyclic subgraph is a tree; Mathlib’s spanning predicate expresses that the subgraph contains every ambient vertex. This is Munkres’s maximal-tree iff all-vertices criterion under the fixed-vertex/subgraph representation.
FC02-C14-U021	exact extension theorem in the combinatorial model	mathlib	Mathlib/Combinatorics/SimpleGraph/Acyclic.lean::Connected.exists_isTree_le_of_le_of_isAcyclic; exists_isAcyclic_reachable_eq_le_of_le_of_isAcyclic	P	Every acyclic subgraph of a connected graph extends to a spanning tree. For a tree inside a possibly disconnected ambient graph, apply the result to its connected component; this is precisely extension to a maximal tree in the component containing the source tree.
FC02-C14-U022	partial match: van Kampen infrastructure, corollary absent	reference-port	Mathlib PR #41603 head 9a19745bf2565abbbf56bb38c91bcd26c4c53b49, Mathlib/AlgebraicTopology/FundamentalGroupoid/VanKampen.lean::relative_vanKampen_subtype; open-cover colimit/cosheaf API	R	The open draft proves a genuine Seifert–van Kampen theorem for the fundamental groupoid, enough infrastructure from which the source configuration can be derived. No declaration in the PR states the special two-component simply-connected corollary or that the single loop [α*β] generates π₁, so this is a partial revision-specific port.
FC02-C14-U023	broad match / explicit complement-of-tree basis	reference-port	FiniteGraphFreeGroup/Proof.lean::spanningTreeBasis; FiniteGraphFreeGroup/TopologicalComparison.lean::graphCombinatorialToTopologicalEquiv; FiniteGraphFreeGroup/Consequences.lean::graphFundamentalGroupBasis; graphFundamentalGroup_subsingleton_iff_cycleRank_zero	R	GraphCoveringTheory@c918a72c5170503c98fd66a0f3116b7bfcd1250c constructs a free basis indexed by arrows outside a spanning tree and identifies the combinatorial vertex group with the topological fundamental group of the realization. Its finite consequences make nontriviality explicit when a non-tree edge remains; translating Munkres’s undirected maximal tree to the symmetrified/arborescence model is the remaining interface step.
FC02-C14-U024	exact match	mathlib	Mathlib/GroupTheory/FreeGroup/NielsenSchreier.lean::subgroupIsFreeOfIsFree	P	Pinned Mathlib states Nielsen–Schreier directly: every subgroup of an IsFreeGroup group inherits an IsFreeGroup instance.
FC02-C14-U025	definition-level graph-count package	reference-port	FiniteGraphFreeGroup/Proof.lean::vertexCount; edgeCount; cycleRank	R	GraphCoveringTheory@c918a72c5170503c98fd66a0f3116b7bfcd1250c explicitly records finite vertex and edge counts and the equivalent cycle-rank expression E + 1 - V. It does not introduce a separate symbol χ := V-E, so the source definition is represented by these exact count components rather than a named Euler-number declaration.
FC02-C14-U026	exact numerical free-rank computation	reference-port	FiniteGraphFreeGroup/TopologicalComparison.lean::proved_topological_fundamental_group_free_rank; FiniteGraphFreeGroup/Consequences.lean::cycleRank_eq_edgeCount_sub_tree	R	At GraphCoveringTheory@c918a72c5170503c98fd66a0f3116b7bfcd1250c, a finite weakly connected graph realization has fundamental group free of rank E+1−V, exactly 1-χ for Munkres’s χ=V-E.
FC02-C14-U027	exact match	mathlib	Mathlib/GroupTheory/Index.lean::Subgroup.index; Subgroup.index_eq_card; Mathlib/GroupTheory/Coset/Defs.lean::QuotientGroup.quotientRightRelEquivQuotientLeftRel; Mathlib/GroupTheory/Coset/Card.lean::card_quotient_rightRel	P	Pinned Mathlib defines subgroup index as the natural cardinality of the coset quotient (zero in the infinite case), proves the cardinal formula, and supplies the left/right coset equivalence; under the source’s finite-index hypothesis this is exactly Munkres’s definition.
FC02-C14-U028	exact match	reference-port	GraphCoveringTheory/IndexFormula.lean::schreier_index_formula_fintype_proved; schreier_index_formula_proved; Solution.lean::schreier_index_formula	R	GraphCoveringTheory@c918a72c5170503c98fd66a0f3116b7bfcd1250c proves that a finite-index subgroup H ≤ FreeGroup (Fin m) is free of rank 1 + H.index*(m-1); setting m=n+1 gives exactly kn+1. Apache-2.0 provenance is usable, but the Lean/Mathlib 4.32 pin makes it a reference port rather than an importable package here.