10 VR-Topology
10.1 Position
VR-Topology is the ninth and final work of the cycle. It formalises point-free topology in the style of Coquand (1992) and Vickers (2006), proving a binary Tychonoff theorem with axiom profile [propext, Quot.sound] — no Classical.choice.
Architectural principle. The formal topology structure \((\text{S},\, \text{le},\, \text{cov})\) is predicative: cov lives in Prop, avoiding the universe-inflation problem that blocked the original free-frame construction (Finding T0). The bridge to mathlib’s impredactive Order.Frame is built separately (Stage 7) and legitimately inherits Classical.choice; this does not affect the Tychonoff theorem.
Unique status. VR-Topology has no companion preprint by curatorial decision. This chapter is the canonical exposition of the result. It is also the chapter most directly relevant to Bas Spitters’ school (point-free topology, formal topology, constructive locales).
Apparatus application. OperationalFormalTopology and OperationalCompact use PredicateOperationality from Chapter 8. This is a fifth confirmation of Finding A3 (apparatus reuse without modification), extending the chain AddGroup \(\to \) Ring \(\to \) Group \(\to \) Module \(\to \) FormalTopology.
‘instProdOperationalCompact‘ is deferred. The abstract instance for the product of two operational compact topologies is not proved in v1.0.0 due to a structural limitation in listLowerOrder (Finding T20). Concrete instances on Unit × Bool work because IsOperational := True on finite carriers. Deferred to v1.1.0.
10.2 FormalTopology structure
\(\texttt{commonRefinement}\, \text{le}\, U\, V := \{ c \mid \exists \, u \in U,\; \exists \, v \in V,\; \text{le}\, c\, u \land \text{le}\, c\, v\} \). The set of elements that refine some element of \(U\) and some element of \(V\). Used in the cov_meet axiom. Axiom profile: [].
FormalTopology is a structure with fields: (i) S : Type* — the carrier of basic elements; (ii) le : S → S → Prop — a preorder (with le_refl, le_trans); (iii) cov : S → Set S → Prop — the coverage relation, satisfying five axioms:
cov_refl: \(a \in U \Rightarrow \texttt{cov}\, a\, U\) (membership implies coverage).
cov_trans: if \(\texttt{cov}\, a\, U\) and \(\forall b \in U,\; \texttt{cov}\, b\, V\), then \(\texttt{cov}\, a\, V\).
cov_ref_mono: if \(\text{le}\, a\, b\) and \(\texttt{cov}\, b\, U\), then \(\texttt{cov}\, a\, U\).
cov_local: if \(\text{le}\, a\, b\) and \(\texttt{cov}\, a\, U\), then \(\texttt{cov}\, a\, \{ c \in U \mid \text{le}\, c\, b\} \).
cov_meet (Sambin extension, Finding T7): if \(\texttt{cov}\, a\, U\) and \(\texttt{cov}\, a\, V\), then \(\texttt{cov}\, a\, (\texttt{commonRefinement}\, \text{le}\, U\, V)\).
The first four axioms are Coquand (1992); the fifth (cov_meet) is the Sambin extension required for the product universal property. cov lives in Prop: universe inflation is avoided. Axiom profile: [].
\(\texttt{CoverGen}\, \text{le}\, \text{basicCov}\) is an inductive Prop with six constructors mirroring the coverage axioms: basic (import), mem (membership), trans (transitivity), ref_mono (refinement-monotonicity), local_ (locality), meet (Sambin meet). Prop-valued: no universe issue. Structural induction on CoverGen derivations is the key proof technique for Tychonoff. Axiom profile: [].
\(\texttt{FormalTopology.ofPresentation}\) assembles a FormalTopology from a preorder and a relation of basic covers, using CoverGen as the coverage relation. This is the standard construction; concrete formal topologies (Unit, Bool, Product) are built via this function.
\(\texttt{cov\_ mono}\): \(U \subseteq V \Rightarrow \texttt{cov}\, a\, U \Rightarrow \texttt{cov}\, a\, V\) (monotonicity). \(\texttt{cov\_ singleton}\): \(\texttt{cov}\, a\, \{ a\} \) (every element covers its own singleton). \(\texttt{cov\_ trans\_ singleton}\): transitivity via singleton. All Axiom profile: [].
10.3 Operational layer
\(\texttt{IsDescribable}\) is a class (data class, not Prop) carrying an enumerator : ℕ → Option α for a set \(\alpha \). Finding T3: IsDescribable must be a data class (not Prop) because the enumerator carries computational content. \(\texttt{OpCoverGen}\) is a parallel inductive Prop tracking operationally-tagged cover derivations. \(\texttt{OpCoverGen.toCoverGen}\): every operational derivation gives a classical derivation.
\(\texttt{OperationalFormalTopology}\, (T : \texttt{FormalTopology})\) is a class with fields: IsOperational : T.S → Prop (predicate on basic elements), basicCov : T.S → Set T.S → Prop (basic cover presentation), op_preserved_by_le (operational status preserved under \(\le \), Finding T19). \(\texttt{opFormalTopologyPredicate}\): registers the apparatus instance PredicateOperationality T.S IsOperational. This is the fifth confirmation of Finding A3: apparatus reuse extends to formal topology.
10.4 Product of formal topologies
\(\texttt{prod}\, T_1\, T_2\) constructs a FormalTopology with: carrier \(T_1.S \times T_2.S\), product preorder, and inductively generated cover from rectangular basic covers. \(\texttt{opProdBasicCov}\): the product’s operational basic cover (Finding T14: a separate layer over prodBasicCov was needed to expose component basicCov). \(\texttt{instProd}\): the OperationalFormalTopology instance for the product.
\(\texttt{proj}_1\), \(\texttt{proj}_2\): continuous maps from the product topology to each component.
10.5 Compact witnesses and OperationalCompact
\(\texttt{listLowerOrder}\, \text{le}\, A\, B := \forall a \in A,\; \exists b \in B,\; \text{le}\, a\, b\) (Vickers’s \(vL\) relation on lists). Uses List (not Finset): avoids Classical.choice inherited from mathlib’s Finset (Finding T13). Axiom profile: [].
\(\texttt{CompactWitness}\, (T : \texttt{FormalTopology})\, (\text{basicCov})\): a structure with \(\texttt{F} : \texttt{Set}\, (\texttt{List}\, T.S)\) and four closure axioms (Vickers 2005/2007): inhabited (nonempty finite cover), upper_closed (monotone under \(vL\)), cover_closure (closed under covering), witness_operational (elements of \(F\) consist of operational points). \(\texttt{List}\) over \(\texttt{Finset}\) (Finding T13).
\(\texttt{OperationalCompact}\, (T : \texttt{FormalTopology})\) is a class with a single field: \(\texttt{witness} : \texttt{CompactWitness}\, T\, \text{basicCov}\). \(\texttt{markedAsModeBTarget}\): identifies OperationalCompact as a Mode B target (operational content extracted from classical compactness). \(\texttt{implies\_ classical\_ compact}\): every operational compact topology is classically compact.
Unit.formalTopology: formal topology on a one-point space. Bool.formalTopology: formal topology on Bool with the discrete preorder. Both with OperationalFormalTopology and OperationalCompact instances. Finding T11: Bool F-witness corrected from \(\{ S \mid S = \emptyset \lor \texttt{true} \in S \lor \texttt{false} \in S\} \) to \(\{ S \mid \texttt{true} \in S \land \texttt{false} \in S\} \).
10.6 Binary Tychonoff
\(\texttt{prodF}\, T_1\, T_2\, w_1\, w_2\): a list \(T\) is in prodF iff for every decomposition of \(T\) into parts \(T_{1,\text{part}}\) and \(T_{2,\text{part}}\), either the first-coordinate projection of \(T_{1,\text{part}}\) is in \(w_1.F\), or the second-coordinate projection of \(T_{2,\text{part}}\) is in \(w_2.F\). (Vickers 2006, Theorem 19 decomposition predicate.) \(\texttt{prodF\_ inhabited}\): non-empty; proved by finite case dispatch using DecidableEq (Finding T16: decidability hypotheses are required and explicit). \(\texttt{prodF\_ upper\_ closed}\): closed under listLowerOrder.
\(\texttt{prodF\_ cover\_ closure}\): the cover_closure field of the CompactWitness built from prodF. If \(a\) is covered by a basic product cover, then the singleton \(\{ a\} \) is in prodF. This is the core technical lemma: structural induction on CoverGen derivations, following Vickers (2006). The proof uses cov_meet at the product level to handle rectangular covers (the reason cov_meet is load-bearing). Axiom profile: [propext, Quot.sound].
\(\texttt{tychonoff\_ binary}\, (T_1\, T_2 : \texttt{FormalTopology})\, [w_1 : \texttt{CompactWitness}\, T_1]\, [w_2 : \texttt{CompactWitness}\, T_2] \, [\text{decidability instances}]\): a CompactWitness for the product topology \(\texttt{FormalTopology.prod}\, T_1\, T_2\).
The compact witness for the binary product is constructed from the Vickers F-witness prodF, prodWitness assembles the four fields using prodF_cover_closure as the closure axiom. This is a concrete def (construction), not merely an existence proof.
Proof sketch: structural induction on CoverGen derivations (hence: Inductive Prop, no Classical.choice). The ref_mono and meet cases use prodF_upper_closed and product cov_meet respectively. Decidability hypotheses (Finding T16) are required for constructive case splits in the basic case.
Axiom profile: [propext, Quot.sound]. Zero Classical.choice. This is the primary claim of VR-Topology: a constructive binary Tychonoff without the Axiom of Choice.
10.7 Bridge to Order.Frame
\(\texttt{IsSaturated}\, T\, U := \forall a,\; T.\texttt{cov}\, a\, U \Rightarrow a \in U\): a set is saturated iff it is downward-closed under coverage. \(\texttt{SatSet}\, T := \{ U : \texttt{Set}\, T.S \mid \texttt{IsSaturated}\, T\, U\} \). \(\texttt{saturate}\, T\, U\): smallest saturated set containing \(U\). These define the frame elements.
\(\texttt{instCompleteLattice}\): CompleteLattice (SatSet T); \(\sup = \texttt{saturate}\, (\bigcup )\), \(\inf = \bigcap \). \(\texttt{frameMinAx}\): Order.Frame.MinimalAxioms (SatSet T); frame distributivity \(a \sqcap \bigsqcup S = \bigsqcup (a \sqcap \cdot )\, ''S\) proved via iSup_pos bridging (Finding T21). \(\texttt{instFrame}\): Order.Frame (SatSet T) derived from frameMinAx.
Stages 1–6 (FormalTopology through tychonoff_binary) are strict-constructive: axiom profile [propext, Quot.sound]. Stage 7 crosses to mathlib’s impredicative Order.Frame, which legitimately acquires Classical.choice through the frame typeclass machinery. The bridge is expected and documented. instFrame has Axiom profile: [propext, Classical.choice, Quot.sound]. The Tychonoff theorem (tychonoff_binary) is unaffected: it is proved before the bridge and sits in its own constructive stratum.
10.8 Honest scope: deferred abstract instance
The abstract instance \(\texttt{OperationalCompact}\, (\texttt{prod}\, T_1\, T_2)\) from \([\texttt{OperationalCompact}\, T_1]\, [\texttt{OperationalCompact}\, T_2]\) is not provided in v1.0.0.
Root cause (Finding T20): listLowerOrder is one-directional (\(\forall a \in A,\; \exists b \in B,\; \text{le}\, a\, b\)), which suffices for F-membership transfer (prodF_upper_closed) but is insufficient to propagate per-element operationality from prodF witnesses back to the product. Specifically, elements of the product cover may have no prodLe-preimage with constrained operationality.
Concrete instances work: Unit × Bool satisfies OperationalCompact trivially because IsOperational := True on finite carriers. Abstract propagation is deferred to v1.1.0 (bidirectional listLowerOrder or restructured OperationalCompact). This is a scope discipline decision, not a methodological failure.
10.9 Architectural amendments (T_FINDINGS)
VR-Topology accumulated 18–19 architectural amendments (T0–T21) through nine implementation sessions. At no point did an architect direction error propagate into committed Lean code; all were caught at the word-first or paper-sketch phase. The five patterns below document the methodological significance.
Findings T5, T8, T9, T11, T15, T17, T20: seven distinct architect direction errors detected at the pre-implementation paper sketch stage before any Lean code was committed. This validates the word-first/paper-sketch workflow as a recognition-discipline gate.
Finding T6 (Nat.unpair_pair pulls Classical.choice via Nat.sqrt): resolved by custom bit-interleaving pairing. Finding T13 (Finset transitively imports Classical.choice via Quot.unquot): resolved by replacing Finset T.S with List T.S throughout CompactWitness (\({\sim }268\) lines discarded, \({\sim }245\) rewritten). The strict constructive baseline requires careful verification of all mathlib import chains.
Finding T7 (cov_meet required for product universal property), Finding T14 (opProdBasicCov layer needed), Finding T16 (decidability hypotheses in tychonoff_binary signature), Finding T19 (op_preserved_by_le field required). All were implicit in architect plans and surfaced as explicit requirements during implementation. Adding cov_meet to FormalTopology was the most architecturally significant (changed the structure definition globally).
Finding T21 (iSup_pos bridging): mathlib’s notation \(\bigsqcup _{b \in S} A \sqcap b\) elaborates to nested iSup with conditional; bridging required identifying the specific lemma iSup_pos. This is a notation/elaboration finding, not a mathematical one. The paper proof closes; Lean’s infrastructure requires a specific bridge tactic.
Finding T20 (R3 resolution): when the abstract instProdOperationalCompact could not be proved due to the listLowerOrder directionality issue, the correct response was to provide concrete-only instances and defer the abstract case to v1.1.0, rather than forcing an incorrect proof or adding a sorry. This preserved cycle stability and honesty.
10.10 Position relative to existing work
The proof of tychonoff_binary follows Vickers’s “Compactness in locales and in formal topology” (2006, Theorem 19). The key adaptation is the translation to Lean 4’s inductive type theory: the classical Kuratowski-finite sets are replaced by List-encoded covers (Finding T13); the classical case splits become explicit Decidable hypotheses (Finding T16).
The coverage axioms follow Coquand (1992)’s presentation. The fifth axiom (cov_meet) is the Sambin extension, required for the product universal property (Finding T7). Coquand’s minimal four-axiom system was insufficient; Sambin’s meet axiom is indispensable.
Tosun’s Agda formalisation of locale theory covers Stone and spectral spaces in point-free settings. VR-Topology uses formal topology (coverage relations) rather than frames directly; the bridge to Order.Frame (Stage 7) connects the two frameworks. The choice of formal topology (not frames) is what enables the constructive axiom profile of tychonoff_binary.
Spitters’s programme in pointless algebraic geometry (Grothendieck toposes in point-free formulation, topos of sheaves on a locale) is the downstream application context for formal topology. VR-Topology provides a verified binary Tychonoff in the style that formal topology researchers expect. The bridge to Order.Frame (Sections 10.7) prepares the infrastructure for sheaf-theoretic applications.
10.11 Axiom profile
Axiom profile: [] for core abstract objects: FormalTopology, CoverGen and its constructors, commonRefinement, listLowerOrder, CompactWitness, OperationalCompact, prodF, prodF_upper_closed, prodF_inhabited.
Axiom profile: [propext, Quot.sound] for the central results: tychonoff_binary, prodF_cover_closure, prodF_cover_closure_head, and all theorems derived through CoverGen induction.
Axiom profile: [propext, Classical.choice, Quot.sound] for the Order.Frame bridge: instCompleteLattice, frameMinAx, instFrame. The Classical.choice here is inherited from mathlib’s impredicative frame infrastructure and does not affect the Tychonoff theorem (proved in Stage 6, before Stage 7’s bridge).
Zero sorry. Zero admit. All deferred content is either concrete instances or explicitly marked as v1.1.0 scope.
10.12 References
No companion preprint by curatorial decision. This chapter is the canonical exposition of VR-Topology.
The Lean 4 formalisation is accessible at github.com/inventor1975/VRCycle, directory VR/Topology/, git tag v1.13-vr-topology-v1.0.0.