12 Brouwer via Sperner (mathlib-bound)
12.1 Position
This chapter is different from the rest of the cycle: the target is mathlib, not a VR object. The deliverable is the Brouwer fixed-point theorem, formalised via the Sperner route, as two layers — a constructive Sperner core and a classical limit — with the boundary between them made precise. What VR contributes here is not the mathematics (the theorem is Brouwer; competent mathlib work reaches it) but the meta-discipline: an honest constructive/classical partition, an abstraction caught vacuous at its first concrete use, and a machine-checked differential witness.
Two layers, one boundary. The constructive layer is Sperner’s lemma in every dimension plus the approximate fixed point; it evaluates the map pointwise but uses no continuity and no choice-driven extraction. The classical layer is the exact theorem, where Classical.choice enters — and only there — through the compactness extraction. Isolating and certifying that single choice point is the chapter’s distinctive contribution (Section 12.5).
Why #print axioms is not enough here (Findings B-1, B-2). The cycle’s usual axiom-tier discipline fails against the analytic substrate: \(\mathbb {R}\) carries Classical.choice at the type level (B-1), and the canonical Fin.fintype enumeration carries it through List.nodup_finRange (B-2). So absolute #print axioms cannot discriminate constructivity over mathlib’s substrate — every declaration touching \(\mathbb {R}\) or a Fintype enumeration is Tier-3 regardless of its local argument. The honest replacement is a dependency claim, witnessed differentially, not an axiom-tier claim (Section 12.5).
12.2 The architecture (stage pipeline)
The formalisation is a linear pipeline of eight modules, each consuming the previous:
Handshake carries the encoding-independent parity kernel; Sperner the one-dimensional door count; Grid the realisation \(\texttt{gridToSimplex}\, k\, v = v/k\) with mesh \(\le 1/k\); KuhnGen the general Kuhn–Freudenthal cells and the whole dimension recursion. The three nodes that carry the difficulty — the dimension recursion, the vacuity finding, and the differential witness — are the subject of the next three sections.
12.3 Load-bearing node I: the dimension recursion
Sperner’s lemma is proved by induction on dimension. The combinatorial heart is the parity bridge — rainbow cells against boundary doors — via the handshake.
For a bipartite incidence between rooms and doors, the number of odd-degree rooms and the number of odd-degree doors have equal parity (each equals the incidence count mod \(2\)). The one genuinely hard combinatorial step, isolated from all geometry.
The recursion step itself is a bijection between the degree-one doors of a \((n{+}2)\)-cell and the rainbow valid \((n{+}1)\)-cells under an induced colouring.
\(\# \{ \text{degree-1 colored doors of } \mathrm{KCell}\, (n{+}2)\} = \# \{ \text{rainbow valid } \mathrm{KCell}\, (n{+}1) \text{ under } \mathrm{col}'\} \), via \(D \mapsto \texttt{facetSet}(\texttt{liftCell}\, D)\, 0\). Injectivity is the \(\varphi \)-functional argument (a cell is determined by its vertex set); surjectivity recovers the cell from a degree-one door (Finding K-3: such a door is exactly \(\texttt{facetSet}\, C_0\, 0\) with first move last). This was the project’s last conceptual risk; it is a theorem.
For every dimension \(m \ge 1\) and every admissible colouring of the resolution-\(k\) grid, there is a rainbow valid cell — one whose vertices realise all \(m{+}1\) colours. The parity step rainbow_parity_step (the drop bijection chained with the handshake) drives the induction; the base case is the one-dimensional door count Sperner.odd_doors. Axiom profile: [propext, Classical.choice, Quot.sound] — substrate-absolute (B-2, Fin enumeration), differentially clean (Section 12.5).
12.4 Load-bearing node II: a vacuous abstraction, caught
The admissibility predicate driving the whole recursion was first stated as \(\forall v\, i,\; v_i = 0 \to \operatorname {col} v \ne i\), quantified over all integer vectors. The zero vector makes it demand \(\operatorname {col} 0 \ne i\) for every \(i\) — impossible. Verified in Lean: (h : SpernerAdmissible col) \(\vdash \) False. Consequence: every Stage-2 theorem carrying this hypothesis was vacuously true — real, green, axiom-audited, and uninstantiable.
The flaw was invisible while Stage 2 only ever consumed the hypothesis. It surfaced at the Stage-3 boundary, where one must construct the colouring from the map and prove it admissible — the recognition-discipline gate (“no abstraction without a concrete user”) firing exactly on first contact with a concrete user. The fix guards the predicate with a positive-sum hypothesis (\(0 {\lt} \sum _j v_j\), automatically met by grid vertices, which sum to \(k{\gt}0\)) and is certified non-vacuous: exists_spernerAdmissible exhibits a witness colouring. The old vacuity proof is now rejected by the kernel. This is the methods contribution of the node: the discipline turned a silent soundness-adjacent defect into a documented, repaired, certified finding.
12.5 Load-bearing node III: the differential witness (machine-checked)
Since absolute axiom tiers are saturated (B-1, B-2), constructivity is witnessed differentially: the constructive layer introduces no dependency on the choice-driven extraction IsCompact.tendsto_subseq (nor on Continuous); the classical layer does. The approximate fixed point is the constructive endpoint.
For a self-map \(f\) of the standard simplex (Set.MapsTo, not Continuous) and resolution \(k{\gt}0\), there is a family \(y\) (the realised vertices of a rainbow cell, one per colour) with \(f(y_i)_i \le (y_i)_i\) for every coordinate \(i\), all points within \(2/k\). The Sperner labeling colours a grid vertex by a coordinate \(f\) does not increase (the coordinate-sum argument exists_coord_le); a rainbow cell realises one such witness per coordinate. Uses \(f\) only pointwise.
A continuous self-map of \(\texttt{stdSimplex}\, \mathbb {R}\, (\texttt{Fin}\, (n{+}1))\), \(n \ge 1\), has a fixed point. The approximate fixed points at resolutions \(k=m{+}1\) form a sequence in the compact simplex; IsCompact.tendsto_subseq extracts a convergent subsequence (the single classical step); continuity plus mesh \(\to 0\) force \(f(x^\ast )_i \le x^\ast _i\) for every \(i\), and equal coordinate sums upgrade this to \(f\, x^\ast = x^\ast \). Axiom profile: [propext, Classical.choice, Quot.sound] — the Classical.choice here is expected and correct: Brouwer is not constructive.
The witness is a build invariant, not a claim. A transitive-dependency checker (VR/Meta/DependsOn.lean, project-agnostic) walks the environment and gates the build on the partition below; the depends rows certify the boundary is genuine, not vacuous. A negative control (asserting a false dependency) is correctly rejected, so the checker is sound in both directions.
|
layer |
tendsto_subseq |
Continuous |
|
Stage 2 exists_rainbow_cell (Sperner) |
free |
free |
|
Stage 3 exists_approx_fixed (approximate) |
free |
free |
|
Stage 4 brouwer_stdSimplex (exact) |
depends |
depends |
This table is the differential witness, machine-checked at build time (#assert_not_depends_on / #assert_depends_on). It is the dependency-graph cut that absolute #print axioms could not see: the constructive nodes are blue (free of the extraction), the classical node is red, and the colouring is sourced from the checker, not asserted by the author.
12.6 The general theorem — compact convex sets
The simplex form extends to any nonempty compact convex set by a retraction argument that keeps the standard simplex as the Brouwer universe. (The gauge/ball homeomorphism route is blocked: the standard simplex has empty interior in its ambient \(\mathbb {R}^{n+1}\), living in the hyperplane \(\sum = 1\).) The reusable cornerstone is the metric projection, which mathlib packages only for subspaces.
For a nonempty complete convex set \(K\) in a real inner product space, the nearest-point projection \(\texttt{projConvex}\, K\) is a \(1\)-Lipschitz (hence continuous) retraction onto \(K\). Built from the Hilbert projection theorem (exists_norm_eq_iInf_of_complete_convex) and its variational inequality.
A continuous self-map of the full-dimensional corner simplex \(\{ x \in \mathbb {R}^n \mid x_i \ge 0,\ \sum x_i \le 1\} \) has a fixed point, by conjugating through the drop-/extend-last-coordinate maps to the standard simplex.
Every continuous self-map of a nonempty compact convex subset \(K\) of Euclidean \(\mathbb {R}^n\) has a fixed point. An affine map \(\psi (x) = a\, (x + M\mathbf{1})\) (with \(M\) a coordinate bound from compactness, \(a\) small) fits a copy \(K' = \psi (K)\) inside the corner simplex; the projection onto \(K'\) conjugated with \(f\) is a self-map of the corner simplex, and its fixed point — which lands in \(K'\), where the projection is the identity — pulls back to a fixed point of \(f\) in \(K\).
12.7 Honest scope
The mathematics is mathlib’s, the meta-layer is VR’s. Roughly ninety percent of the code is ordinary formalisation craft (the triangulation, the \(\varphi \)-functional, the drop bijection, the real-analysis limit); VR did not make Brouwer provable. Its value is precision of the constructivity claim and the finding-discipline that caught S-1.
The differential witness is meta-trusted. The checker certifies the dependency relation but is not itself kernel-verified — the same tier as #print axioms.
Coverage. The theorem holds for the standard simplex in every dimension (including the degenerate point \(n=0\), brouwer_stdSimplex_all) and for an arbitrary nonempty compact convex subset of Euclidean \(\mathbb {R}^n\) (Section 12.6). A further extension to infinite-dimensional convex sets (Schauder) is out of scope.
12.8 References
The Lean 4 formalisation lives under VRClassical/Brouwer/ (modules Skeleton, Sperner, Grid, Handshake, Kuhn, KuhnGen, Approx, Fixed), with the differential witness in Brouwer/DiffWitness.lean over the generic engine Meta/DependsOn.lean. The target is a mathlib pull request; this chapter is the canonical exposition of the architecture and the two methods contributions (Finding S-1, the machine-checked differential witness).