Trace — 2607.19276v1
**Inspecting workspace documents**
I’ll first reconstruct the exact theorem and dependency chain from the local paper, then map each ingredient against the bundled mathlib before choosing the Lean representation. I’ll keep the development under `repro/`, compile every stage offline, and record semantic-equivalence checks and any hypotheses in `repro/README.md`.
**Planning file inspection**
$ /bin/bash -lc "pwd && rg --files -g 'paper.*' -g 'repro/**' | sed -n '1,120p' && wc -l paper.txt && sed -n '1,240p' paper.txt" pro/Mathlib/LinearAlgebra/DirectSum/Finsupp.lean repro/Mathlib/LinearAlgebra/AnnihilatingPolynomial.lean repro/Mathlib/LinearAlgebra/CrossProduct.lean repro/.github/actions/setup-build-env/action.yml repro/Mathlib/Condensed/EffectiveEpi.lean repro/Mathlib/LinearAlgebra/Charpoly/BaseChange.lean repro/Mathlib/LinearAlgebra/Charpoly/ToMatrix.lean repro/Mathlib/LinearAlgebra/Charpoly/Basic.lean repro/Mathlib/LinearAlgebra/BilinearMap.lean repro/.github/actions/get-cache/action.yml repro/Mathlib/Condensed/Discrete/Characterization.lean repro/Mathlib/Condensed/Discrete/Colimit.lean repro/Mathlib/Condensed/Discrete/LocallyConstant.lean repro/Mathlib/LinearAlgebra/SModEq/Pointwise.lean repro/Mathlib/LinearAlgebra/SModEq/Basic.lean repro/Mathlib/Condensed/Discrete/Basic.lean repro/Mathlib/LinearAlgebra/SModEq/Pow.lean repro/Mathlib/Condensed/Discrete/Module.lean repro/Mathlib/Condensed/Epi.lean repro/Mathlib/Condensed/CartesianClosed.lean repro/.github/actions/cache-trust-dispatch/action.yml repro/Mathlib/Condensed/TopCatAdjunction.lean repro/Mathlib/Condensed/AB.lean repro/Mathlib/Condensed/TopComparison.lean repro/Mathlib/LinearAlgebra/TensorPower/Pairing.lean repro/Mathlib/LinearAlgebra/TensorPower/Basic.lean repro/Mathlib/LinearAlgebra/TensorPower/Symmetric.lean repro/.github/actions/get-tools/action.yml repro/.github/actionlint.yml repro/.github/PULL_REQUEST_TEMPLATE.md repro/Mathlib/Condensed/Light/EffectiveEpi.lean repro/Mathlib/LinearAlgebra/Span/TensorProduct.lean repro/Mathlib/Condensed/Light/Instances.lean repro/Mathlib/Condensed/Light/Monoidal.lean repro/Mathlib/Condensed/Light/Epi.lean repro/Mathlib/Condensed/Light/CartesianClosed.lean repro/Mathlib/Condensed/Light/TopCatAdjunction.lean repro/Mathlib/Condensed/Light/InternallyProjective.lean repro/Mathlib/Condensed/Light/AB.lean repro/Mathlib/Condensed/Light/TopComparison.lean repro/Mathlib/Condensed/Light/Limits.lean repro/Mathlib/Condensed/Light/Basic.lean repro/Mathlib/Condensed/Light/Module.lean repro/Mathli
$ /bin/bash -lc "sed -n '240,760p' paper.txt" ker ∂iC = im ∂i+1 ker ϵC = im ∂1C , (1 ≤ i ≤ d), Di = 0 (i > d), ker(id + Ui ) = im(id + Ui ) (0 ≤ i ≤ d). Then there is no equivariant augmentation-preserving chain map C∗ → D∗ . Proof. Write νC = id + T, νD = id + U. These are degreewise maps. Since the coefficients lie in F2 , 2 νC2 = νD = 0, ∂ C νC = νC ∂ C , ∂ D νD = νD ∂ D , ϵC νC = ϵD νD = 0. 5 Choose x0 with ϵC (x0 ) = 1. The source assumptions give chains xi ∈ Ci , 1 ≤ i ≤ d + 1, satisfying ϵC (x0 ) = 1, ∂ C xi+1 = νC xi (0 ≤ i ≤ d). Indeed, ϵC (νC x0 ) = 0, so exactness in degree 0 gives x1 . Inductively, for i ≥ 1, ∂ C (νC xi ) = νC ∂ C xi = νC2 xi−1 = 0. Exactness in degree i therefore supplies xi+1 . Suppose that ϕ exists and put yi = ϕi (xi ). Then ∂ D yi+1 = νD yi , and yd+1 = 0 because Dd+1 = 0. Set zd+1 = 0. Descending from degree d, choose zi ∈ Di , 0 ≤ i ≤ d, such that yi = ∂ D zi+1 + νD zi (0 ≤ i ≤ d). For i = d, this follows from νD yd = ∂ D yd+1 = 0. If it holds in degree i + 1, then νD yi + ∂ D zi+1 = ∂ D yi+1 + νD zi+1 = (∂ D )2 zi+2 = 0, so the same kernel–image equality supplies zi . Finally, ϵD (y0 ) = ϵD (∂ D z1 ) + ϵD (νD z0 ) = 0, whereas augmentation preservation gives ϵD (y0 ) = ϵC (x0 ) = 1, a contradiction. □ If U permutes a chosen basis of D, then ker(id + U ) = im(id + U ) if and only if the induced involution has no fixed basis element. Therefore, Lemma 3.1 is a chain-level version of the Z/2Z-case of Dold’s theorem [3]. By the Equivariant Simplicial Approximation Theorem, it is a generalization of the Borsuk–Ulam obstruction to an antipodal map S d+1 → S d . We shall use it with the standard cellular chains of the cubical boundary ∂top I K as the source. Their augmentation sends every vertex to 1, and their augmented complex is exact below the top dimension by cellular homology [9, Section 2.2]. 4. The target sphere and polyhedral chains Fix K ≥ 2 and put ( WK = z ∈ RK : K X ) zi = 0 , d = K − 2. i=1 Since dim WK = K − 1, its unit sphere S(WK ) has
$ /bin/bash -lc "sed -n '760,1425p' paper.txt"
Then
νj W =
X
µz (Q) [Q] + [−Q]
Q∈Rj
=
X
µz (Q)[Q] = Z.
Q∈K
dim Q=j
This shows that Z ∈ im νj .
□
5. From a rook labeling to a polyhedral chain map
5.1. Rook galleries and rank. For (a, b) ∈ ΩK , define
root(a, b) = ea − eb ∈ WK .
Here e1 , . . . , eK are the standard basis vectors of RK . All ranks and linear-independence
statements concerning roots are over R. A sequence (ai , bi )m
i=1 with m ≥ 1 is a rook
gallery if every two consecutive terms have the same first coordinate or the same second
coordinate.
Lemma 5.1. Let (ai , bi )m
i=1 be a rook gallery. If
0 ∈ conv{eai − ebi : 1 ≤ i ≤ m},
then
rank{eai − ebi : 1 ≤ i ≤ m} ≤ m − 2.
Proof. Let G be the directed multigraph with edges ai → bi , and put v = |V (G)|. Split
each used coordinate symbol s into a tail vertex s+ and a head vertex s− , retaining only
−
the roles in which s occurs, and replace ai → bi by the bipartite edge a+
i bi . Consecutive
gallery edges meet at the copy of their common coordinate, so this split graph is connected.
In particular, the underlying graph of G is connected.
Let t be the number of coordinate symbols that occur both as tails and as heads. The
split graph has v + t vertices and m edges. Its connectedness gives
m ≥ v + t − 1.
(1)
There are coefficients satisfying
λi ≥ 0,
m
X
i=1
λi = 1,
m
X
λi (eai − ebi ) = 0.
i=1
The last equality is flow conservation at every vertex. Start with an edge of positive
weight. At its head, conservation supplies an outgoing edge of positive weight; iterating in
the finite graph eventually repeats a vertex and hence produces a directed cycle. Because
ai ̸= bi , this cycle is not a loop, so at least two coordinate symbols on it occur in both
roles. Hence t ≥ 2. Incidence vectors of a connected graph on v vertices have rank v − 1.
By (1),
rank{eai − ebi : 1 ≤ i ≤ m} = v − 1 ≤ m − t ≤ m − 2.
□
For the rest of the construction, suppose that
q : V (QK ) −→ ΩK
is a rook labeling.
12
5.2. Freudenthal subdivision. The cubical cellul**Planning formalization of central theorem**
The paper’s core reduction is clean: it is enough to rule out a “rook labeling” \(q:\{0,1\}^K\to\{(a,b):a\ne b\}\) with coordinate-swap antipodality. The long polyhedral-chain construction exists only to produce a forbidden equivariant map \(S^{K-1}\to S^{K-2}\), so I’m now checking whether mathlib already contains a Borsuk–Ulam/Tucker theorem that can replace that custom target while preserving the exact rook condition.$ /bin/bash -lc "rg -n -i \"borsuk|tucker|antipodal|dold.?s theorem|freudenthal|simplicial approximation\" Mathlib | sed -n '1,240p' rg -n \"Hypercube|hypercube|Hamming|Bool.*cube|cubeGraph|SimpleGraph.*cube\" Mathlib | sed -n '1,200p' rg -n \"Sphere.*antipod|antipod.*Sphere|antipodal\" Mathlib/Topology Mathlib/AlgebraicTopology | sed -n '1,240p'" ionTheory/Hamming.lean:394:instance [∀ i, Zero (β i)] : Norm (Hamming β) := Mathlib/InformationTheory/Hamming.lean:395: ⟨fun x => hammingNorm (ofHamming x)⟩ Mathlib/InformationTheory/Hamming.lean:398:theorem norm_eq_hammingNorm [∀ i, Zero (β i)] (x : Hamming β) : ‖x‖ = hammingNorm (ofHamming x) := Mathlib/InformationTheory/Hamming.lean:401:instance [∀ i, AddGroup (β i)] : NormedAddGroup (Hamming β) where Mathlib/InformationTheory/Hamming.lean:404:instance [∀ i, AddCommGroup (β i)] : NormedAddCommGroup (Hamming β) where Mathlib/InformationTheory/Hamming.lean:408:theorem nnnorm_eq_hammingNorm [∀ i, AddGroup (β i)] (x : Hamming β) : Mathlib/InformationTheory/Hamming.lean:409: ‖x‖₊ = hammingNorm (ofHamming x) := rfl Mathlib/InformationTheory/Hamming.lean:413:end Hamming Mathlib/Order/Interval/Set/UnorderedInterval.lean:31:In `Finset α` (seen as a hypercube of dimension `Fintype.card α`), `uIcc a b` is the smallest Mathlib/GroupTheory/Coxeter/Matrix.lean:40:* `CoxeterMatrix.Bₙ` : Coxeter matrix for the symmetry group of the regular n-hypercube
**Planning Tucker lemma formalization** **Exploring algebraic chain complex formulation** **Investigating radial map chain truncation**
**Analyzing convex hull conditions in simplicial chains** **Designing fan-based cellular chain model** **Exploring Coxeter complex for root cones**
**Exploring combinatorial invariant proof** **Formulating discrete Borsuk-Ulam variant**
$ /bin/bash -lc "rg -n -i \"sperner|KKM|poincar[eé].?miranda|hex theorem|combinatorial.*sphere|octahed\" Mathlib | sed -n '1,240p' rg -n \"SimplicialComplex.*homology|boundary.*Finset|Fintype.*Euler|Euler.*characteristic\" Mathlib/Combinatorics Mathlib/AlgebraicTopology | sed -n '1,240p' find . -maxdepth 2 -name 'AGENTS.md' -o -name 'README.md' | sed -n '1,100p' sed -n '1,160p' lakefile.toml 2>/dev/null || sed -n '1,160p' lakefile.lean lean --version"
**Searching for Lean 4 Borsuk-Ulam formalization**
**Evaluating formalization approach using external theorems** **Assessing Tucker lemma as external hypothesis** **Designing antipodal label mapping for Tucker lemma**
**Planning signed labeling for Freudenthal triangulation** **Evaluating Tucker lemma and barycentric subdivision alternatives** **Formulating perturbation to avoid zero convex hull**
**Assessing generic perturbation effects** **Analyzing perturbation effects on simplex interiors** **Investigating robust zero inclusion in perturbations**
**Assessing topological obstructions for rook labeling** **Planning abstract chain map construction** **Defining target via antipodal cellular chains**
**Defining equivalence classes for polytopes** **Formalizing chain maps via relative interiors** **Constructing quotient modules via generic membership**
**Planning chain complex construction** **Considering combinatorial chain obstruction proof** **Formulating equivariant chain assumption**
**Confirming borsuk-ulam verification**
**Testing network connectivity with curl**
$ /bin/bash -lc "curl -L --fail --max-time 30 -sS https://leangenius.org/proof/borsuk-ulam | sed -n '1,240p'"
<!doctype html>
<html lang="en">
<head>
<meta charset="UTF-8" />
<link rel="icon" href="data:image/svg+xml,<svg xmlns='http://www.w3.org/2000/svg' viewBox='0 0 100 100'><text y='.9em' font-size='90'>📐</text></svg>" />
<meta name="viewport" content="width=device-width, initial-scale=1.0" />
<meta name="description" content="Understand Lean proofs line-by-line with annotated explanations" />
<title>LeanGenius - Annotated Lean Proofs</title>
<link rel="preconnect" href="https://fonts.googleapis.com">
<link rel="preconnect" href="https://fonts.gstatic.com" crossorigin>
<link href="https://fonts.googleapis.com/css2?family=JetBrains+Mono:wght@400;500;600&display=swap" rel="stylesheet">
<script type="module" crossorigin src="/assets/index-B-a5o2SN.js"></script>
<link rel="modulepreload" crossorigin href="/assets/vendor-katex-D6N9Pdbk.js">
<link rel="stylesheet" crossorigin href="/assets/vendor-katex-DvXFAOB1.css">
<link rel="stylesheet" crossorigin href="/assets/index-DstGmaze.css">
</head>
<body>
<div id="root"></div>
</body>
</html>**Fetching API and asset URLs**
$ /bin/bash -lc "curl -L --fail --max-time 30 -sS https://leangenius.org/assets/index-B-a5o2SN.js -o /tmp/leangenius.js && rg -o 'https?["'^" ]+|/api/[''^" ]+|proofs[''^" ]+|borsuk[''^" ]+'"' /tmp/leangenius.js | sed -n '1,120p'" https://react.dev/errors/ https://react.dev/errors/ httpEquiv http-equiv http://www.w3.org/2000/svg http://www.w3.org/1998/Math/MathML http://www.w3.org/2000/svg http://www.w3.org/1998/Math/MathML http://www.w3.org/2000/svg http-equiv httpEquiv==null?null:l.httpEquiv)&&u.getAttribute( http://www.w3.org/1999/xlink http://www.w3.org/1999/xlink http://www.w3.org/1999/xlink http://www.w3.org/1999/xlink http://www.w3.org/1999/xlink http://www.w3.org/1999/xlink http://www.w3.org/1999/xlink http://www.w3.org/XML/1998/namespace http://www.w3.org/XML/1998/namespace http://www.w3.org/XML/1998/namespace http://www.w3.org/2000/svg http://www.w3.org/1998/Math/MathML http://www.w3.org/2000/svg http://localhost httpEquiv: https://reactrouter.com/en/main/routers/picking-a-router.`}function https://reactrouter.com/en/main/routers/picking-a-router.`}function https://github.com/ungap/url-search-params. /api/auth/me /api/auth/google/login /api/auth/login /api/auth/register /api/auth/logout /api/auth/me proofs, borsuk-ulam-oq-03-oq-03
**Inspecting borsuk directory**
$ /bin/bash -lc "rg -n -o '.{0,500}borsuk-ulam.{0,1000}' /tmp/leangenius.js | sed -n '1,80p'
rg -o '/api/[A-Za-z0-9_?&=/.-]+' /tmp/leangenius.js | sort -u | sed -n '1,160p'"
12:","slug":"erdos-346","title":"Erdős Problem #346: Complete Sequences and the Golden Ratio"},{"fact":"The essence of mathematics lies in its freedom.","slug":null,"title":"Georg Cantor"},{"fact":"K₄ is 3-regular but minimal: no proper 3-regular subgraph exists, showing the threshold is exactly 4.","slug":"erdos-715","title":"Erdős Problem #715: Regular Subgraphs in Regular Graphs"},{"fact":"The antipodal condition is NECESSARY: without it, constant labelings have no complementary edges.","slug":"borsuk-ulam-oq-03-oq-03","title":"Constructive 2D Borsuk-Ulam via Tucker's Lemma"},{"fact":"Vertices of odd degree must be endpoints of an Eulerian path (if one exists).","slug":"konigsberg","title":"Königsberg Bridges Problem"},{"fact":"Collinearity of the three division points is captured by a single 2×2 signed-area determinant.","slug":"menelaus-theorem-oq-01","title":"Menelaus's Theorem: Collinearity via Signed Side Ratios"},{"fact":"Optimal lower bound: Erdős showed infinitely many gaps achieve (π²/6)·log(sₙ)/log(log(sₙ)), so this would be tight.","slug":"erdos-208","title":"Erdős Problem #208: Gaps Between Squarefree Numbers"},{"fact":"The Dickman function ρ(u) governs the density of smooth numbers.","slug":"erdos-334","title":"Erdős Problem #334: Smooth Number Representation"},{"fact":"All 50 elements are even — the parity constraint (any admissible set containing 0 must be all-even) is satisfied.","slug":"bounded-prime-gaps-oq-01-oq-03","title":"Minimum Admissible 50-Tuple Diameter: The E
/api/auth/google/login
/api/auth/login
/api/auth/logout
/api/auth/me
/api/auth/register**Searching theorem source for slug**
$ /bin/bash -lc "python3 - <<'PY'
p='/tmp/leangenius.js'
s=open(p).read()
for needle in ['borsuk-ulam-oq-03-oq-03','SchauderFixedPoint','Tucker']:
i=s.find(needle)
print(needle,i)
print(s[max(0,i-2000):i+5000])
PY"
borsuk-ulam-oq-03-oq-03 270362
h roots of primes generate non-trivial field extensions is a foundational fact.","slug":"nth-root-irrational-oq-01","title":"Nth Root Irrationality via Irreducible Polynomials"},{"fact":"This is the honest boundary of what is formalizable for OQ-05: the decidable skeleton is provable; a polynomial algorithm and NP-hardness are not, and remain open.","slug":"erdos-1012-oq-05","title":"Erdős #1012 (OQ-05): Decidability and the Brute-Force Search Space for (n−k)-Cycle Detection"},{"fact":"Additive combinatorics meets Diophantine approximation: The problem bridges two major branches of number theory.","slug":"erdos-254","title":"Erdős Problem #254: Subset Sum Representation"},{"fact":"Smooth numbers give limit point 1: When n+1 has only small prime factors, all factors in the product are near 1, so the ratio → 1.","slug":"erdos-419","title":"Erdős Problem #419: Limit Points of τ((n+1)!)/τ(n!)"},{"fact":"The conjecture asks whether every interval of the natural scale captures Ω(1) contribution, with no anomalously empty intervals.","slug":"erdos-462","title":"Erdős Problem #462: Least Prime Factor Sums in Short Intervals"},{"fact":"The physical explanation: strong coupling confines dynamics within single plaquettes; inter-plaquette correlations are exponentially suppressed regardless of L.","slug":"yang-mills-transfer-matrix-oq-01","title":"Yang-Mills Transfer Matrix OQ-01: Infinite-Volume Mass Gap"},{"fact":"The conjecture applies only to lacunary sequences; irregular ones exist.","slug":"erdos-346","title":"Erdős Problem #346: Complete Sequences and the Golden Ratio"},{"fact":"The essence of mathematics lies in its freedom.","slug":null,"title":"Georg Cantor"},{"fact":"K₄ is 3-regular but minimal: no proper 3-regular subgraph exists, showing the threshold is exactly 4.","slug":"erdos-715","title":"Erdős Problem #715: Regular Subgraphs in Regular Graphs"},{"fact":"The antipodal condition is NECESSARY: without it, constant labelings have no**Planning dynamic ProofPage JS**
$ /bin/bash -lc "curl -L --fail --max-time 30 -sS https://leangenius.org/assets/ProofPage-OX5snYpy.js -o /tmp/proofpage.js && rg -o 'https?["'^" ]+|/[A-Za-z0-9_?&=/.-]*(proof|api)[A-Za-z0-9_?&=/.-]*'"' /tmp/proofpage.js | sed -n '1,200p'
python3 - <<'PY'
s=open('/tmp/proofpage.js').read()
for needle in ['fetch(','supabase','proofs','/api']:
print('\\n',needle)
start=0
for _ in range(10):
i=s.find(needle,start)
if i<0: break
print(s[max(0,i-400):i+800])
start=i+len(needle)
PY"
/proof-badge-Bg1eZVM5.js
/api/comments
http:
https:
https://www.erdosproblems.com/${t}`,s=xe(o);if(!s)return
/proof/
https://doi.org/${t.doi}`:void
https://arxiv.org/abs/${t.arxiv}`:void
/proof/
/proof/
https://github.com/rjwalters/lean-genius
https://github.com/rjwalters/lean-genius
fetch(
onst o=new Map,r=[];for(const s of t)o.set(s.id,{...s,children:[]});for(const s of t){const a=o.get(s.id);if(s.parentId){const n=o.get(s.parentId);n?(n.children=n.children||[],n.children.push(a)):r.push(a)}else r.push(a)}return r}async function Cs(t,o){const r=new URLSearchParams({proof_id:t});o!==void 0&&r.set("line",o.toString());const s=X(),a={};s&&(a.Authorization=`Bearer ${s}`);const n=await fetch(`${G}?${r}`,{headers:a});if(!n.ok)throw new Error("Failed to fetch comments");return(await n.json()).comments}async function Ce(t,o,r,s={}){const a=X();if(!a)throw new Error("Not authenticated");const n=await fetch(`${G}/create`,{method:"POST",headers:{"Content-Type":"application/json",Authorization:`Bearer ${a}`},body:JSON.stringify({proofId:t,annotationId:s.annotationId||void 0,lineNumber:o,content:r,parentId:s.parentId})});if(!n.ok){const i=await n.json();throw new Error(i.error||"Failed to create comment")}return(await n.json()).comment}async function ks(t,o){const r=X();if(!r)throw new Error("Not authenticated");const s=await fetch(`${G}/${t}`,{method:"PUT",headers:{"Content-Type":"application/json",Authorization:`Bearer ${r}`},body:JSON.stringify({content:o})});if(!s.ok){const
sh(a)}return r}async function Cs(t,o){const r=new URLSearchParams({proof_id:t});o!==void 0&&r.set("line",o.toString());const s=X(),a={};s&&(a.Authorization=`Bearer ${s}`);const n=await fetch(`${G}?${r}`,{headers:a});if(!n.ok)throw new Error("Failed to fetch comments");return(await n.json()).comments}async function Ce(t,o,r,s={}){const a=X();if(!a)throw new Error("Not authenticated");const n=await fetch(`${G}/create`,{method:"POST",headers:{"Content-Type":"application/json",Authorization:`Bearer ${a}`**Inspecting endpoint constants in data imports**
$ /bin/bash -lc "sed 's/;/;\\n/g' /tmp/proofpage.js | rg -n \"function.*Proof|fetch|useLazy|json|proofData|slug|assets/proofs|content\" | sed -n '1,240p'"
14:import{a as yt,b as St}from"./oq-slug-BhgfOjhS.js";
32:return e.jsx(es,{scope:r,type:s,dir:A,scrollHideDelay:n,scrollArea:i,viewport:c,onViewportChange:x,content:u,onContentChange:h,scrollbarX:f,onScrollbarXChange:w,scrollbarXEnabled:j,onScrollbarXEnabledChange:v,scrollbarY:S,onScrollbarYChange:g,scrollbarYEnabled:y,onScrollbarYEnabledChange:P,onCornerWidthChange:E,onCornerHeightChange:b,children:e.jsx(K.div,{dir:A,...l,ref:N,style:{position:"relative","--radix-scroll-area-corner-width":k+"px","--radix-scroll-area-corner-height":p+"px",...t.style}})})});
55:return H(r.viewport,d),H(r.content,d),e.jsx(se,{present:s||n,children:e.jsx(fe,{"data-state":n?"visible":"hidden",...a,ref:o})})}),fe=m.forwardRef((t,o)=>{const{orientation:r="vertical",...s}=t,a=L(D,t.__scopeScrollArea),n=m.useRef(null),l=m.useRef(0),[i,d]=m.useState({content:0,viewport:0,scrollbar:{size:0,paddingStart:0,paddingEnd:0}}),c=Xe(i.viewport,i.content),x={...s,sizes:i,onSizesChange:d,hasThumb:c>0&&c<1,onThumbChange:h=>n.current=h,onThumbPointerUp:()=>l.current=0,onThumbPointerDown:h=>l.current=h};
60:t.onWheelScroll(h),Ge(h,u)&&x.preventDefault()}},onResize:()=>{d.current&&n.viewport&&l&&s({content:n.viewport.scrollWidth,viewport:n.viewport.offsetWidth,scrollbar:{size:d.current.clientWidth,paddingStart:te(l.paddingLeft),paddingEnd:te(l.paddingRight)}})}})}),rs=m.forwardRef((t,o)=>{const{sizes:r,onSizesChange:s,...a}=t,n=L(D,t.__scopeScrollArea),[l,i]=m.useState(),d=m.useRef(null),c=W(o,d,n.onScrollbarYChange);
62:t.onWheelScroll(h),Ge(h,u)&&x.preventDefault()}},onResize:()=>{d.current&&n.viewport&&l&&s({content:n.viewport.scrollHeight,viewport:n.viewport.offsetHeight,scrollbar:{size:d.current.clientHeight,paddingStart:te(l.paddingTop),paddingEnd:te(l.paddingBottom)}})}})}),[os,He]=Oe(D),We=m.forwardRef((t,o)=>{const{__scopeScrollArea:r,sizes:s,hasThumb:a,onThumbChange:n,onThumbPointerUp:l,onThumbPointerDown:i,onThumbPositionChange:d,onDragScroll:c,onWheelScroll:x,onResize:u,...h}=t,f=L(D,r),[w,S]=m$ /bin/bash -lc "sed 's/;/;\\n/g' /tmp/proofpage.js | sed -n '250,272p'"
const a=Bs(t.year);
if(a&&s.push(a),s.length>0?o.push(s.join(", ")):a&&o.push(`(${a})`),o.length!==0)return o.join(". ")+"."}function Hs({reference:t,index:o}){const r=t.citation,s=Vs(t),a=r||s,n=a?void 0:t.text;
if(!a&&!n&&!t.note)return null;
const l=t.doi?`https://doi.org/${t.doi}`:void 0,i=t.arxiv?`https://arxiv.org/abs/${t.arxiv}`:void 0,d=t.url,c=l||i||d;
return e.jsxs("li",{className:"flex gap-3 text-sm",children:[e.jsx("span",{className:"shrink-0 h-5 w-5 rounded-full bg-blue-500/20 text-blue-400 text-xs flex items-center justify-center font-medium mt-0.5",children:o+1}),e.jsxs("div",{className:"min-w-0 space-y-1",children:[a&&e.jsx("p",{className:"text-foreground/90 leading-relaxed",children:c?e.jsx("a",{href:c,target:"_blank",rel:"noopener noreferrer",className:"hover:text-blue-400 transition-colors",children:a}):a}),n&&e.jsx("p",{className:"text-foreground/90 leading-relaxed",children:t.url?e.jsx("a",{href:t.url,target:"_blank",rel:"noopener noreferrer",className:"hover:text-blue-400 transition-colors",children:n}):n}),t.note&&e.jsx("p",{className:"text-xs text-muted-foreground leading-relaxed italic",children:t.note}),e.jsxs("div",{className:"flex flex-wrap gap-2",children:[l&&e.jsxs("a",{href:l,target:"_blank",rel:"noopener noreferrer",className:"inline-flex items-center gap-1 text-xs px-2 py-0.5 rounded bg-blue-500/10 text-blue-400 border border-blue-500/20 hover:bg-blue-500/20 transition-colors",children:[e.jsx(B,{className:"h-3 w-3"}),"DOI"]}),i&&e.jsxs("a",{href:i,target:"_blank",rel:"noopener noreferrer",className:"inline-flex items-center gap-1 text-xs px-2 py-0.5 rounded bg-orange-500/10 text-orange-400 border border-orange-500/20 hover:bg-orange-500/20 transition-colors",children:[e.jsx(B,{className:"h-3 w-3"}),"arXiv"]}),d&&!l&&!i&&e.jsxs("a",{href:d,target:"_blank",rel:"noopener noreferrer",className:"inline-flex items-center gap-1 text-xs px-2 py-0.5 rounded bg-muted/50 text-muted-foreground border border-border/50 hover:bg-muted/70 transition**Inspecting import of wt function**
$ /bin/bash -lc 'head -c 4000 /tmp/proofpage.js'
import{r as m,j as e,c as C,g as X,u as Le,L as O,d as nt,b as rt}from"./index-B-a5o2SN.js";import{c as ot,P as K,a as se,b as U,u as z,d as at,E as B}from"./tooltip-B_CIitWl.js";import{u as W,a as Z,C as de}from"./circle-check-big-BLCv2ICZ.js";import{B as _}from"./button-D4tJB0XT.js";import{M as R,L as _e,a as $}from"./markdown-math--ZISpQ9o.js";import{a as ve}from"./vendor-katex-D6N9Pdbk.js";import{C as J}from"./chevron-up-CMjiUArV.js";import{C as V,P as De,R as lt,E as it}from"./rotate-ccw-VZMMmR74.js";import{C as he}from"./chevron-right-QZ86Uq2Q.js";import{M as ne,a as ct,X as Ie,A as $e,D as dt,c as mt,d as ut,e as xt,f as ht,b as pt,R as ft,T as gt,C as bt,h as jt,P as vt,O as Nt,i as wt,U as Ne}from"./UserMenu-DSE3jFLJ.js";import{c as T}from"./createLucideIcon-CPlCr9k0.js";import{B as me}from"./book-open-CXSrDKw0.js";import{c as F,d as we,P as Me,C as ie}from"./proof-badge-Bg1eZVM5.js";import{a as yt,b as St}from"./oq-slug-BhgfOjhS.js";import{G as ye}from"./github-C-UsvIbD.js";const Ct=[["path",{d:"m15.477 12.89 1.515 8.526a.5.5 0 0 1-.81.47l-3.58-2.687a1 1 0 0 0-1.197 0l-3.586 2.686a.5.5 0 0 1-.81-.469l1.514-8.526",key:"1yiouv"}],["circle",{cx:"12",cy:"8",r:"6",key:"1vp47v"}]],kt=T("award",Ct);const Pt=[["circle",{cx:"12",cy:"12",r:"10",key:"1mglay"}],["circle",{cx:"12",cy:"12",r:"1",key:"41hilf"}]],At=T("circle-dot",Pt);const Et=[["circle",{cx:"12",cy:"12",r:"10",key:"1mglay"}]],Rt=T("circle",Et);const Tt=[["path",{d:"M3 12a9 9 0 1 0 9-9 9.75 9.75 0 0 0-6.74 2.74L3 8",key:"1357e3"}],["path",{d:"M3 3v5h5",key:"1xhq8a"}],["path",{d:"M12 7v5l4 2",key:"1fdv2h"}]],Lt=T("history",Tt);const _t=[["path",{d:"M11 6a13 13 0 0 0 8.4-2.8A1 1 0 0 1 21 4v12a1 1 0 0 1-1.6.8A13 13 0 0 0 11 14H5a2 2 0 0 1-2-2V8a2 2 0 0 1 2-2z",key:"q8bfy3"}],["path",{d:"M6 14a12 12 0 0 0 2.4 7.2 2 2 0 0 0 3.2-2.4A8 8 0 0 1 10 14",key:"1853fq"}],["path",{d:"M8 6v8",key:"15ugcq"}]],Dt=T("megaphone",_t);const It=[["path",{d:"M4 5h16",key:"1tepv9"}],["path",{d:"M4 12h16",key:"1lakjw"}],["path",{**Inspecting UserMenu component**
$ /bin/bash -lc "curl -L --fail --max-time 30 -sS https://leangenius.org/assets/UserMenu-DSE3jFLJ.js -o /tmp/usermenu.js
python3 - <<'PY'
s=open('/tmp/usermenu.js').read()
for needle in ['async function','proofs/','data/','fetch(']:
print('\\nNEEDLE',needle)
start=0
for _ in range(30):
i=s.find(needle,start)
if i<0: break
print(s[max(0,i-200):i+600])
start=i+len(needle)
PY"
NEEDLE async function
ange={startLine:c,endLine:c},!0):!1})}function Ua(e){return e&&e.map(a=>typeof a=="string"?{proofId:a,relationship:"related"}:a).filter(a=>{const c=a.proofId??a.targetId;return c!=null&&ne[c]!=null})}async function vn(e){if(e===Le)return;const a=ne[e];if(a)try{const[c,n]=await Promise.all([fetch(`/data/proofs/${e}/meta.json?v=${a.meta}`),fetch(`/data/proofs/${e}/annotations.json?v=${a.ann}`)]);if(!c.ok)return;const t=await c.json();let o=[];if(n.ok)try{o=await n.json()}catch{o=[]}const b={proof:{id:t.id,title:t.title,slug:t.slug,description:t.description,meta:t.meta,sections:t.sections??[],overview:t.overview,conclusion:t.conclusion,crossReferences:Ua(t.crossReferences),references:t.references,source:""},annotations:Wa(o)};try{const s=await fetch(`/data/proofs/${e}/source.lean?v=${a.src}`)
NEEDLE proofs/
a:"303b6a74",ann:"a645a61c",src:"b3970a04"},__listings__:Ia,__searchindex__:Oa},ne=Fa,Le="__listings__",La="__searchindex__";let G=null,Y=null;function $a(){if(!G){const e=ne[Le]?.meta;G=fetch(`/data/proofs/listings.json?v=${e}`).then(a=>{if(!a.ok)throw new Error(`Failed to load listings (HTTP ${a.status})`);return a.json()}).catch(a=>{throw G=null,a})}return G}function yn(){if(!Y){const e=ne[La]?.meta;Y=fetch(`/data/proofs/search-index.json?v=${e}`).then(a=>{if(!a.ok)throw new Error(`Failed to load search index (HTTP ${a.status})`);return a.json()}).catch(a=>{throw Y=null,a})}return Y}function Wa(e){return e.filter(a=>{if(a.range)return!0;const c=a.lineNumber??a.line;return c!=null?(a.range={startLine:c,endLine:c},!0):!1})}function Ua(e){return e&&e.map(a=>typeof a=="string"?{proofId:a,re
v=${e}`).then(a=>{if(!a.ok)throw new Error(`Failed to load listings (HTTP ${a.status})`);return a.json()}).catch(a=>{throw G=null,a})}return G}function yn(){if(!Y){const e=ne[La]?.meta;Y=fetch(`/data/proofs/search-index.json?v=${e}`).then(a=>{if(!a.ok)throw new Error(`Failed to load search index (HTTP ${a.status})`);return a.json()}).catch(a=>{throw Y=null,a**Reviewing curl source code**
$ /bin/bash -lc "curl -L --fail --max-time 30 -sS https://leangenius.org/data/proofs/borsuk-ulam-oq-03-oq-03/source.lean -o /tmp/borsuk.lean && wc -l /tmp/borsuk.lean && sed -n '1,260p' /tmp/borsuk.lean" 2640 /tmp/borsuk.lean import Mathlib /- # Constructive 2D Borsuk-Ulam via Tucker's Lemma (borsuk-ulam-oq-03-oq-03) ## The Open Question Can the 2D Borsuk-Ulam theorem (∀ f : S² → ℝ², ∃ antipodal pair with f(x)=f(-x)) be proved via Tucker's lemma instead of algebraic topology? ## Answer YES — the proof strategy is: 1. Given continuous f : S² → ℝ², define g(x) = f(x) - f(-x) (odd function on S²) 2. g is continuous and antipodal: g(-x) = -g(x) 3. Triangulate the upper hemisphere (≈ disk D²) with antipodally symmetric boundary 4. Label each vertex v by the "dominant component direction" of g(v) - g(v) is in ℝ², so label = sign of the larger coordinate (±1 or ±2) 5. The antipodal condition g(-x) = -g(x) ensures boundary labels are complementary 6. Tucker's 2D lemma gives a complementary edge (vertices labeled +k and -k) 7. Along this edge, g changes sign in coordinate k → by IVT, g ≈ 0 nearby 8. Refining the triangulation, the complementary edge midpoints converge to a point where g = 0, i.e., f(x) = f(-x) ## Infrastructure from Existing Files - Tucker's 2D lemma (axiom): grid-specific, properly constrained - 1D BU and Tucker: BorsukUlamOQ03.lean - Spheres, antipodal maps: BorsukUlamOQ01/02.lean ## What This File Proves 1. The "dominant component labeling" is antipodal (Part II) 2. Tucker complementary edge → approximate zero via IVT (Parts XVIII-XX) 3. Mesh refinement on compact sets gives arbitrarily small zeros (Part XXI) 4. Radial extension from D² to [-1,1]² preserving odd boundary (Part XXII) 5. Grid infrastructure: vertices, edges, boundary, antipodal map (Part XXIII) 5b. **Triangulated grid** `gridEdgesTriFin`: H/V + NE-SW diagonal edges (Part XXIII) 5c. **Grid antipodal properties**: involution, boundary preservation, edge preservation 6. **Main theorem**: tucker_disk_approx_zero_proved (from tucker_2d_grid axiom) 7. Approximate and exact 2D Borsuk-Ulam (Part XVI) ## Status: 1 axiom, 0 sorries The entire proof chain is complete modulo Tucker's
**Exploring generalized Borsuk-Ulam availability**
$ /bin/bash -lc "curl -L --fail --max-time 30 -sS https://leangenius.org/data/proofs/listings.json -o /tmp/listings.json && rg -i -n \"borsuk|tucker|sperner|brouwer\" /tmp/listings.json | sed -n '1,120p'"
1:[{"id":"a054656-distinct-prime-partition","title":"OEIS A054656: Primes Absent from Every Distinct-Prime Partition of n","slug":"a054656-distinct-prime-partition","description":"For n ≥ 23, the primes p ≤ n absent from every partition of n into distinct primes are exactly {n−1, n−4, n−6} ∩ P. This first iteration…","status":"formalized","badge":"wip","tags":["oeis","additive-number-theory","distinct-primes","partitions","bertrand","ramanujan-prime","research"],"dateAdded":"2026-07-22","updatedAt":"2026-07-22T17:02:02-07:00","sorries":4,"annotationCount":5},{"id":"abel-ruffini","title":"Abel-Ruffini Theorem","slug":"abel-ruffini","description":"A pedagogical walkthrough of the Abel-Ruffini theorem (Wiedijk #16) composed from Mathlib's Galois theory infrastructure: the…","status":"verified","badge":"mathlib","tags":["algebra","galois-theory","group-theory","field-theory","classic","intermediate","wiedijk-100"],"dateAdded":"2025-12-21","updatedAt":"2026-07-20T16:18:16-07:00","wiedijkNumber":16,"mathlibCount":4,"sorries":0,"annotationCount":16},{"id":"abel-ruffini-galois-extensions","title":"Abel-Ruffini Galois Theory Extensions","slug":"abel-ruffini-galois-extensions","description":"Extends the Abel-Ruffini formalization with the complete solvability classification of symmetric groups. Proves S₀–S₄ are solvable, S_n is…","status":"axiomatized","badge":"axiom","tags":["group-theory","galois-theory","symmetric-groups","solvability","abel-ruffini"],"dateAdded":"2026-04-02","updatedAt":"2026-07-20T16:18:16-07:00","mathlibCount":11,"sorries":0,"annotationCount":21},{"id":"abel-ruffini-galois-extensions-oq-01","title":"Explicit Quintic with Galois Group S₅ — X⁵ − 4X + 2","slug":"abel-ruffini-galois-extensions-oq-01","description":"Constructs the concrete witness `q = X⁵ − 4X + 2 ∈ ℚ[X]` and proves, with 0 sorries and 0 axioms, that its Galois group is the full…","status":"verified","badge":"mathlib","tags":["galois-theory","abel-ruffini","solvability","symmetric-group","qu$ /bin/bash -lc "jq -r '.[] | select(((.title // \"\") + \" \" + (.description // \"\") + \" \" + ((.tags // [])|join(\" \"))) | test(\"Borsuk|Tucker|Sperner|Brouwer\"; \"i\")) | [.slug,.status,.sorries,.title] | @tsv' /tmp/listings.json | sed -n '1,200p'" /bin/bash: line 1: jq: command not found
$ /bin/bash -lc "python3 - <<'PY'
import json,re
for x in json.load(open('/tmp/listings.json')):
s=' '.join([x.get('title',''),x.get('description',''),' '.join(x.get('tags',[]))])
if re.search(r'borsuk|tucker|sperner|brouwer',s,re.I): print(x.get('slug'), x.get('status'),x.get('sorries'),x.get('title'))
PY"
borsuk-ulam axiomatized 0 Borsuk-Ulam Theorem
borsuk-ulam-oq-02 axiomatized 0 Equivariant Borsuk-Ulam: Extensions to Other Group Actions (Open Question)
borsuk-ulam-oq-02-oq-01 axiomatized 0 Equivariant Borsuk-Ulam for Non-Prime Groups
borsuk-ulam-oq-02-oq-01-oq-01 axiomatized 0 Borsuk-Ulam Dimension Formula for Composite n
borsuk-ulam-oq-02-oq-01-oq-02 verified 0 No Exotic Free Representations for Cyclic Groups
borsuk-ulam-oq-02-oq-01-oq-03 axiomatized 0 Borsuk-Ulam for Non-Cyclic Groups: Dihedral and Symmetric Lower Bounds
borsuk-ulam-oq-02-oq-01-oq-04 axiomatized 0 Fadell-Husseini Index Theory for Equivariant Borsuk-Ulam
borsuk-ulam-oq-02-oq-02 axiomatized 0 Equivariant Borsuk-Ulam for Compact Lie Groups
borsuk-ulam-oq-02-oq-02-wip-01 axiomatized 0 Equivariant Borsuk-Ulam for Free Involutions
borsuk-ulam-oq-02-oq-03 axiomatized 0 Dold's Theorem: Cohomological Index for Free G-Spaces
borsuk-ulam-oq-02-oq-04 axiomatized 0 Non-Free Z/p Index: The Localization Collapse
borsuk-ulam-oq-03 axiomatized 0 Constructive Borsuk-Ulam Theorem and Equivalences
borsuk-ulam-oq-03-oq-01 axiomatized 0 Tucker's 1D Lemma via Discrete IVT, with Interval and Circle Bounds
borsuk-ulam-oq-03-oq-01-oq-01 verified 0 Tucker 2D Lemma via Graph-Theoretic Path-Following
borsuk-ulam-oq-03-oq-02 verified 0 Brouwer Degree via Mathlib Homology: the Functorial Core
borsuk-ulam-oq-03-oq-03 axiomatized 0 Constructive 2D Borsuk-Ulam via Tucker's Lemma
borsuk-ulam-oq-03-oq-04 verified 0 Quantitative 1D Borsuk-Ulam: Effective Bounds on Antipodal Pairs
borsuk-ulam-oq-04 axiomatized 0 Higher Categorical Analogues of the Covering Space Argument
borsuk-ulam-oq-04-oq-03 verified 0 The ∞-Topos Section Problem: the π₁ Shadow of the Covering Obstruction
borsuk-ulam-oq001 axiomatized 0 Exotic G-Representations and the Composite BU Dimension Gap
borsuk-ulam-oq002 axiomatized 0 Borsuk-Ulam Dimension for Semiprimes: Direct Proof via CRT Compatibility
borsuk-ulam-oq003 axiomatized 0 Borsuk-Ulam CRT for Squarefree Nu**Evaluating alternative Borsuk-Ulam proofs** **Analyzing rook labeling for antipodal contradiction** **Bounding bichromatic edges via antipodal-free classes**
**Establishing lower bound on edge boundary** **Analyzing minimal partitions with antipodal constraints**
**Formalizing exterior algebra approach** **Evaluating chain-level Borsuk-Ulam hypothesis** **Analyzing rank constraints for rook galleries**
**Applying Ky Fan and Tucker lemmas** **Exploring directed cycles from Ky Fan parity** **Defining antisymmetric labeling for pairs**
**Assessing complementary label constraints on cube edges** **Testing cubical Tucker lemma on antipodal labelings** **Planning brute force verification for K=3 and 4**
A promising simplification emerged from the rook labels themselves. Mapping \((a,b)\) to the signed label \(\operatorname{sgn}(b-a)\min(a,b)\) uses only \(K-1\) absolute labels, flips sign under \((a,b)\leftrightarrow(b,a)\), and—crucially—two rook-adjacent labels can never be complementary. I’m testing whether the needed cubical Tucker statement guarantees a complementary original cube edge (not merely a subdivision diagonal); if it does, the entire geometric chain apparatus collapses to a much smaller combinatorial proof.$ /bin/bash -lc "python3 - <<'PY'
# SAT by simple backtracking: antipodal labelings cube vertices -> ±[K-1], no complementary cube edge.
# Fix one from each antipodal pair, domains labels; antipodes determined.
from itertools import product
def solve(K):
verts=list(product(range(2), repeat=K))
idx={v:i for i,v in enumerate(verts)}
A=lambda v: tuple(1-x for x in v)
reps=[v for v in verts if idx[v]<idx[A(v)]]
rid={v:i for i,v in enumerate(reps)}
def varsign(v):
a=A(v)
return (rid[v],1) if v in rid else (rid[a],-1)
edges=[]
for v in verts:
for j in range(K):
w=list(v);w[j]"'^=1;w=tuple(w)
if idx[v]<idx[w]:
rv,sv=varsign(v); rw,sw=varsign(w)
edges.append((rv,sv,rw,sw))
vals=[None]*len(reps)
dom=[i for i in range(1,K)]+[-i for i in range(1,K)]
# constraint actual endpoint labels not negatives: sv*vals[rv] != -sw*vals[rw]
inc=[[] for _ in reps]
for e in edges:
inc[e[0]].append(e);inc[e[2]].append(e)
def ok(e):
a,sa,b,sb=e
return vals[a] is None or vals[b] is None or sa*vals[a] != -sb*vals[b]
def bt(done):
if done==len(reps): return vals.copy()
# choose unassigned max constrained
r=max((i for i,x in enumerate(vals) if x is None),key=lambda i:sum(vals[e[2] if e[0]==i else e[0]] is not None for e in inc[i]))
for z in dom:
vals[r]=z
if all(ok(e) for e in inc[r]):
ans=bt(done+1)
if ans:return ans
vals[r]=None
ans=bt(0)
print('"'K',K,'solution',bool(ans),ans)
for k in range(2,6):solve(k)
PY"
K 2 solution False None
K 3 solution True [1, 1, 2, 2]
K 4 solution True [1, 1, 1, 1, 2, 2, 2, 2]
K 5 solution True [1, 1, 1, 1, 1, 1, 1, 1, 2, 2, 2, 2, 2, 2, 2, 2]**Assessing lambda properties on face diagonals** **Exploring triangulation choices to avoid complementary pairs** **Confirming complementary pair length bounds**
**Exploring alternating orientation feasibility** **Generating rook galleries for K=3 and K=4**
$ /bin/bash -lc "python3 - <<'PY'
from itertools import product
for K in range(2,7):
roots=[(a,b) for a in range(K) for b in range(K) if a"'!=b]
def adj(x,y):return x[0]==y[0] or x[1]==y[1]
def alab(r):
a,b=r; return ((min(a,b),max(a,b)), 1 if a<b else -1)
cnt=0; witness=None
def bt(g):
global cnt,witness
if witness:return
if len(g)==K:
labs=[alab(x) for x in g]
if len({x[0] for x in labs})<K:return
signs=[s for _,s in sorted(labs)]
if all(signs[i]==-signs[i+1] for i in range(K-1)):
witness=(g.copy(),sorted(labs))
return
for r in roots:
if not g or adj(g[-1],r): bt(g+[r])
if witness:return
bt([])
print(K,witness)
PY'
2 None
3 None
4 ([(0, 2), (1, 2), (1, 0), (3, 0)], [((0, 1), -1), ((0, 2), 1), ((0, 3), -1), ((1, 2), 1)])
5 ([(0, 1), (0, 3), (2, 3), (2, 0), (2, 1)], [((0, 1), 1), ((0, 2), -1), ((0, 3), 1), ((1, 2), -1), ((2, 3), 1)])
6 ([(0, 1), (0, 3), (1, 3), (4, 3), (4, 0), (2, 0)], [((0, 1), 1), ((0, 2), -1), ((0, 3), 1), ((0, 4), -1), ((1, 3), 1), ((3, 4), -1)])**Planning adaptive edge ordering search**
$ /bin/bash -lc "python3 - <<'PY'
from itertools import permutations,product
for K in range(3,6):
pairs=[(a,b) for a in range(K) for b in range(a+1,K)]
roots=[(a,b) for a in range(K) for b in range(K) if a"'!=b]
def adj(x,y):return x[0]==y[0] or x[1]==y[1]
galleries=[]
def bt(g):
if len(g)==K:
if len({tuple(sorted(x)) for x in g})==K:galleries.append(g.copy())
else:
for r in roots:
if not g or adj(g[-1],r):bt(g+[r])
bt([])
print('"'K',K,'pairs',len(pairs),'galleries',len(galleries))
if len(pairs)>8:continue
found=None
for perm in permutations(pairs):
rank={p:i for i,p in enumerate(perm)}
good=True
for g in galleries:
gs=sorted(g,key=lambda r:rank[tuple(sorted(r))])
signs=[a<b for a,b in gs]
if all(signs[i]"'!=signs[i+1] for i in range(K-1)):
good=False;break
if good:found=perm;break
print('"'ordering',found)
PY"
K 3 pairs 3 galleries 12
ordering ((0, 1), (0, 2), (1, 2))
K 4 pairs 6 galleries 336
ordering ((0, 1), (0, 2), (1, 2), (1, 3), (2, 3), (0, 3))
K 5 pairs 10 galleries 10320**Analyzing edge orderings to avoid alternating bipartite paths** **Exploring root systems and Sperner formalization for edge ordering**
$ /bin/bash -lc 'for slug in sperner-ndim sperner-ndim-mathlib sperner-ndim-mathlib-oq-01 sperner-ndim-mathlib-oq-01-oq-04 sperner-mathlib4-oq-02-oq-05; do curl -L --fail --max-time 30 -sS "https://leangenius.org/data/proofs/$slug/source.lean" -o "/tmp/$slug.lean"; echo "$slug $(wc -l < /tmp/$slug.lean)"; rg -n "''^(axiom|theorem|def|structure).*([Ss]perner|[Tt]ucker|antipod|main|freudenthal)|sorry|axiom" "/tmp/$slug.lean" | tail -40; done' sperner-ndim-mathlib 523 12:adjacency axioms, using the door-counting parity argument. 476:theorem sperner_parity (c : V → Fin (d + 1)) (K : CellComplex V d) : 511:theorem sperner (c : V → Fin (d + 1)) (K : CellComplex V d) sperner-ndim-mathlib-oq-01 413 16:## Part I: SpernerTriangulation → CellComplex Bridge (0 axioms, fully proved) 19:`CellComplex (Vertex d N) d` with two boundary axioms (`adj_unique_facet`, `boundary_face`). 23:## Part II: Freudenthal CellComplex (0 axioms, fully proved) 31:Four facts (originally axiomatized, all eliminated as theorems): 45:axiom-3-now-theorem), `adj_ne` (uses axiom-4-now-theorem), `vertices_injective` 71:def toAbstractCellComplex (K : SpernerNDim.SpernerTriangulation d N) : 83:theorem isFC_bridge (c : SpernerNDim.Coloring d N) 87:theorem isDoorAt_bridge (c : SpernerNDim.Coloring d N) 93:theorem sperner_from_triangulation (c : SpernerNDim.Coloring d N) 102:theorem boundary_doors_agree (c : SpernerNDim.Coloring d N) 217:-- Eliminated axioms (now theorems) 404:theorem freudenthal_sperner (n : ℕ) (c : Finset (Fin n) → Fin (n + 1)) sperner-ndim-mathlib-oq-01-oq-04 207 sperner-mathlib4-oq-02-oq-05 175 26:## What this file proves (0 sorries, 0 axioms; `decide` only on the finite alphabet's 59:`ZMod 2` mod-reduction the n = 1 file uses). 0 sorries, 0 axioms 60:(`propext` / `Classical.choice` / `Quot.sound` only — no `sorryAx`, no `Lean.ofReduceBool`). 115:theorem antipodal_signDegree_odd 171:#print axioms antipodal_signDegree_odd 172:#print axioms loop_signDegree_even 173:#print axioms HexagonInstance.hexagon_arc_signDegree_odd
**Inspecting missing dependency paths**
$ /bin/bash -lc "sed -n '1,180p' /tmp/sperner-ndim-mathlib.lean sed -n '1,130p' /tmp/sperner-ndim-mathlib-oq-01.lean sed -n '390,430p' /tmp/sperner-ndim-mathlib-oq-01.lean" /- Copyright (c) 2026 RJ Walters. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: RJ Walters -/ import Mathlib /-! # Sperner's Lemma via Abstract Cell Complex This file proves Sperner's lemma for any abstract cell complex satisfying adjacency axioms, using the door-counting parity argument. ## Main definitions * `SpernerAbstract.CellComplex`: Abstract cell complex with adjacency. * `SpernerAbstract.IsFC`: Fully colored (panchromatic) cell. * `SpernerAbstract.isDoorAt`: Door predicate for a facet. ## Main statements * `SpernerAbstract.even_card_fpf_invol`: Fixed-point-free involution parity. * `SpernerAbstract.abstract_door_parity`: Per-cell door parity. * `SpernerAbstract.sperner_parity`: **Sperner Parity Theorem**. * `SpernerAbstract.sperner`: **Sperner's Lemma**. ## Tags Sperner, combinatorics, parity, triangulation, door-counting -/ set_option linter.unusedVariables false set_option maxHeartbeats 3200000 namespace SpernerAbstract open Finset BigOperators -- ============================================================ -- SECTION I: ZMod 2 Parity Helpers -- ============================================================ private lemma odd_of_zmod2_one (m : ℕ) (h : (m : ZMod 2) = 1) : Odd m := by rw [Nat.odd_iff] have hval := ZMod.val_natCast (n := 2) m rw [h] at hval rw [show (1 : ZMod 2).val = 1 from rfl] at hval omega -- ============================================================ -- SECTION II: Abstract Cell Complex -- ============================================================ /-- An abstract cell complex with adjacency. Each cell has `d + 1` vertices from type `V`. Interior facets pair up via `adj`; boundary facets have `adj = none`. -/ structure CellComplex (V : Type*) [DecidableEq V] (d : ℕ) where Simplex : Type simplex_decidableEq : DecidableEq Simplex simplex_fintype : Fintype Simplex vertices : Simplex → Fin (d + 1) → V vertices_injective : ∀ s, Function.Injective (vertices
**Planning Sperner lemma application for dimension proof** **Planning combinatorial chain complex formalization** **Evaluating chain map construction from free resolution**
**Planning chain map construction** **Exploring triangulation via hyperplane arrangements** **Defining target basis from fan cones**
**Planning abstracting fan properties** **Developing combinatorial induction framework** **Defining Orlik-Solomon chain complex**
**Proving radial cancellation via exterior algebra** **Formulating global chain complex via augmented exterior algebra** **Analyzing antipodal action eigenvalues in exterior algebra**
**Assessing linear dependence in root wedges** **Exploring affine simplex volume chain maps** **Planning top boundary volume cancellation**
**Defining chain map using affine volume wedge** **Analyzing chain involution effects on affine volume map** **Confirming antipodal equivariance of affine volume map**
**Formulating geometric cone basis with antipodal pairing** **Defining chain basis using oriented wedge rays**
$ /bin/bash -lc "rg -n \"homology.*[Ss]phere|[Ss]phere.*homology|reducedHomology.*sphere|homologySphere|homology.*S¹|homology.*circle\" Mathlib/AlgebraicTopology Mathlib/Topology | sed -n '1,240p' rg -n \"Simplex.*boundary|standardSimplex|singular.*simplex|alternating.*face\" Mathlib/AlgebraicTopology/Singular | sed -n '1,240p'" rg: Mathlib/AlgebraicTopology/Singular: IO error for operation on Mathlib/AlgebraicTopology/Singular: No such file or directory (os error 2)
**Evaluating Borsuk-Ulam assumption for chain obstruction** **Analyzing chain map realizability and cone lemmas** **Confirming subdivision relations and refinements**
**Verifying graph rank and lemma properties** **Confirming facet dimension bounds and chain identities** **Considering using Classical.choice in Lean**
**Assessing quotient inductive approaches** **Evaluating external theorem dependencies** **Defining quotient chain complex structure**
**Defining modules via antipodal orbits** **Assigning canonical orientations to cones** **Testing facet cone independence**
**Modeling cones with indicator functions** **Constructing function spaces on Grassmannians** **Defining symmetrized invariant representatives**
**Defining dimension filtration for supports** **Formulating boundary operator for cone indicators** **Planning geometric lemma for differential**
**Defining chain complex with nonzero differential** **Formalizing mod2 boundary operators with stratification** **Identifying classical rook gallery Tucker theorem**
**Analyzing acyclic carrier theorem application** **Planning graph-based cube coloring formalization** **Defining monochromatic path relation**
**Extending cube dimension for component labeling** **Generalizing rook theorem with component roots** **Establishing label equality via antipodal paths**
**Designing coordinate embedding and projection** **Formulating adjacency via coordinate flips**
$ /bin/bash -lc "git status --short && find .. -name AGENTS.md -print && rg -n \"theorem.*Nat.*le.*two_pow|le_two_pow|self_le_two_pow|card_fun|Fintype.card_fun\" Mathlib | sed -n '1,160p'"
Mathlib/Topology/Separation/NotNormal.lean:33:theorem two_pow_mk_le_two_pow_mk_dense [NormalSpace X] {s d : Set X} (hs : IsClosed s)
Mathlib/Topology/Separation/NotNormal.lean:56: (#s).cantor.trans_le <| hs.two_pow_mk_le_two_pow_mk_dense hd
Mathlib/Topology/Separation/NotNormal.lean:64: 2 ^ #s ≤ 2 ^ #d := hs.two_pow_mk_le_two_pow_mk_dense hd_dense
Mathlib/LinearAlgebra/Projectivization/Cardinality.lean:120: have hc : Nat.card V = Nat.card k ^ n := by simp [Nat.card_congr e.toEquiv, Nat.card_fun]
Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean:180: simp only [Fintype.card_fun, Fintype.card_coe, Fintype.card_fin, le_refl]
Mathlib/Combinatorics/SimpleGraph/Coloring/EdgeLabeling.lean:69: Fintype.card_fun.trans (by rw [← edgeFinset_card, card_edgeFinset_top_eq_card_choose_two])
Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean:118: grw [sum_const, smul_eq_mul, card_filter_atomise_le_two_pow (s := U) hX,
Mathlib/GroupTheory/IndexNSmul.lean:47: Nat.card_fun, Int.range_nsmulAddMonoidHom,
Mathlib/Analysis/PSeries.lean:85: grw [← le_sum_condensed' hf n, ← sum_range_add_sum_Ico _ n.one_le_two_pow, sum_range_succ,
Mathlib/GroupTheory/Commutator/Finite.lean:63: rw [← hS1, ← Fintype.card_coe, ← Nat.card_eq_fintype_card, ← Finset.coe_sort_coe, ← Nat.card_fun]
Mathlib/GroupTheory/RegularWreathProduct.lean:131: rw [Nat.card_congr (equivProd D Q), Nat.card_prod (Q → D) Q, Nat.card_fun]
Mathlib/GroupTheory/RegularWreathProduct.lean:248: (Finite.equivFinOfCardEq (by rw [Nat.card_fun, Nat.card_fin, hG])).symm
Mathlib/Computability/Ackermann.lean:230:private theorem sq_le_two_pow_add_one_minus_three (n : ℕ) : n ^ 2 ≤ 2 ^ (n + 1) - 3 := by
Mathlib/Computability/Ackermann.lean:236: | 0, n => by simpa using sq_le_two_pow_add_one_minus_three (n + 2)
Mathlib/FieldTheory/Finiteness.lean:99: rw [Nat.card_congr b.equivFun.toEquiv, Nat.card_fun, finrank_eq_nat_card_basis b]
Mathlib/RingTheory/WittVector/Truncated.lean:386: simp only [TruncatedWittVector, Fint**Planning graph theory implementation**
$ /bin/bash -lc "rg -n \"ConnectedComponent|connectedComponent|Reachable.*equiv|component.*eq\" Mathlib/Combinatorics/SimpleGraph | sed -n '1,240p' sed -n '1,220p' Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean" Mathlib/Combinatorics/SimpleGraph/Tutte.lean:79: (h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), Mathlib/Combinatorics/SimpleGraph/Tutte.lean:82: have hrep := ConnectedComponent.Represents.image_out G.deleteUniversalVerts.coe.oddComponents Mathlib/Combinatorics/SimpleGraph/Tutte.lean:89: have exists_complMatch (K : G.deleteUniversalVerts.coe.ConnectedComponent) : Mathlib/Combinatorics/SimpleGraph/Tutte.lean:103: SimpleGraph.pairwise_disjoint_supp_connectedComponent _ hij Mathlib/Combinatorics/SimpleGraph/Tutte.lean:117: use G.deleteUniversalVerts.coe.connectedComponentMk ⟨v, hv⟩ Mathlib/Combinatorics/SimpleGraph/Tutte.lean:125: (h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), Mathlib/Combinatorics/SimpleGraph/Tutte.lean:147: choose f hf g hgf hg using ConnectedComponent.odd_matches_node_outside hM (u := u) Mathlib/Combinatorics/SimpleGraph/Tutte.lean:150: exact Subtype.val_injective <| ConnectedComponent.eq_of_common_vertex (hg c) (hcd ▸ hg d) Mathlib/Combinatorics/SimpleGraph/Tutte.lean:193: have induce_le : ((cycles.connectedComponentMk c).toSimpleGraph).spanningCoe ≤ Mathlib/Combinatorics/SimpleGraph/Tutte.lean:195: refine le_trans (spanningCoe_induce_le cycles (cycles.connectedComponentMk c).supp) ?_ Mathlib/Combinatorics/SimpleGraph/Tutte.lean:199: by_cases! hxc : x ∉ (cycles.connectedComponentMk c).supp Mathlib/Combinatorics/SimpleGraph/Tutte.lean:200: · use (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe Mathlib/Combinatorics/SimpleGraph/Tutte.lean:201: refine ⟨hcalt.mono (spanningCoe_induce_le cycles (cycles.connectedComponentMk c).supp), ?_⟩ Mathlib/Combinatorics/SimpleGraph/Tutte.lean:202: simp only [ConnectedComponent.adj_spanningCoe_toSimpleGraph, hxc, hcac, false_and, Mathlib/Combinatorics/SimpleGraph/Tutte.lean:203: not_false_eq_true, ConnectedComponent.mem_supp_iff, ConnectedComponent.eq, and_true, Mathlib/Combinatorics/SimpleGraph/Tutte.lean:205: refine ⟨hcycles.toSimpleGrap
**Defining cube graph adjacency and component bounds** **Defining cube graph and rook labeling structures** **Formalizing dimension extension with Fin.castAdd embedding**
**Planning projection adjacency proof**
**Compiling codebase**
$ /bin/bash -lc 'lake env lean Norine.lean'
Norine.lean:34:2: error(lean.unknownIdentifier): Unknown identifier `involutive_iff_injective`
Norine.lean:41:36: warning: `Symmetric` has been deprecated: Use `Std.Symm` instead
Note: The updated constant has a different type:
{α : Sort u} → (α → α → Prop) → Prop
instead of
{α : Sort u_1} → (α → α → Prop) → Prop
Norine.lean:45:38: warning: `Irreflexive` has been deprecated: Use `Std.Irrefl` instead
Note: The updated constant has a different type:
{α : Sort u} → (α → α → Prop) → Prop
instead of
{α : Sort u_1} → (α → α → Prop) → Prop
Norine.lean:53:10: error: Type mismatch
cubeAdjacent_symm
has type
Symmetric CubeAdjacent
but is expected to have type
Std.Symm CubeAdjacent
Norine.lean:54:14: error: Type mismatch
cubeAdjacent_irrefl
has type
Irreflexive CubeAdjacent
but is expected to have type
Std.Irrefl CubeAdjacent
Norine.lean:75:9: warning: `Symmetric` has been deprecated: Use `Std.Symm` instead
Note: The updated constant has a different type:
{α : Sort u} → (α → α → Prop) → Prop
instead of
{α : Sort u_1} → (α → α → Prop) → Prop
Norine.lean:75:19: error: Application type mismatch: The argument
color
has type
Cube n → Cube n → Bool
but is expected to have type
?m.1 → ?m.1 → Prop
in the application
Symmetric color
Norine.lean:79:27: error: Function expected at
EdgeColoring
but this term has type
?m.1
Note: Expected a function because this term is being applied to the argument
n
Hint: The identifier `EdgeColoring` is unknown, and Lean's `autoImplicit` option causes an unknown identifier to be treated as an implicitly bound variable with an unknown type. However, the unknown type cannot be a function, and a function is what Lean expects here. This is often the result of a typo or a missing `import` or `open` statement.
Norine.lean:80:3: error(lean.invalidField): Invalid field notation: Field projection operates on types of the form `C ...` where C is a constant. The expression
EdgeColoring
has type `x✝` which does not have t**Fixing symmetry property in color structure**
$ /bin/bash -lc 'lake env lean Norine.lean' Norine.lean:43:9: error: Tactic `introN` failed: There are no additional binders or `let` bindings in the goal to introduce n : ℕ ⊢ Std.Symm CubeAdjacent Norine.lean:47:8: error: Tactic `introN` failed: There are no additional binders or `let` bindings in the goal to introduce n : ℕ ⊢ Std.Irrefl CubeAdjacent Norine.lean:89:24: error: Function expected at cubeAdjacent_irrefl but this term has type Std.Irrefl CubeAdjacent Note: Expected a function because this term is being applied to the argument x Norine.lean:87:11: error: Tactic `introN` failed: There are no additional binders or `let` bindings in the goal to introduce n : ℕ c : EdgeColoring n b : Bool ⊢ Std.Symm fun x y => CubeAdjacent x y ∧ c.color x y = b Norine.lean:93:63: error: Type mismatch Iff.rfl has type ?m.6 ↔ ?m.6 but is expected to have type (c.colorGraph b).Adj x y ↔ CubeAdjacent x y ∧ c.color x y = b
**Verifying Std.Symm structure**
$ /bin/bash -lc "cat >/tmp/Check.lean <<'EOF'
import Mathlib
#check Std.Symm
#print Std.Symm
#check Std.Irrefl
#print Std.Irrefl
#check SimpleGraph.mk
#print SimpleGraph
EOF
lake env lean /tmp/Check.lean"
Std.Symm.{u} {α : Sort u} (r : α → α → Prop) : Prop
class Std.Symm.{u} {α : Sort u} (r : α → α → Prop) : Prop
number of parameters: 2
fields:
Std.Symm.symm : ∀ (a b : α), r a b → r b a
constructor:
Std.Symm.mk.{u} {α : Sort u} {r : α → α → Prop} (symm : ∀ (a b : α), r a b → r b a) : Std.Symm r
Std.Irrefl.{u} {α : Sort u} (r : α → α → Prop) : Prop
class Std.Irrefl.{u} {α : Sort u} (r : α → α → Prop) : Prop
number of parameters: 2
fields:
Std.Irrefl.irrefl : ∀ (a : α), ¬r a a
constructor:
Std.Irrefl.mk.{u} {α : Sort u} {r : α → α → Prop} (irrefl : ∀ (a : α), ¬r a a) : Std.Irrefl r
SimpleGraph.mk.{u} {V : Type u} (Adj : V → V → Prop) (symm : Std.Symm Adj := by aesop_graph)
(loopless : Std.Irrefl Adj := by aesop_graph) : SimpleGraph V
structure SimpleGraph.{u} (V : Type u) : Type u
number of parameters: 1
fields:
SimpleGraph.Adj : V → V → Prop
SimpleGraph.symm : Std.Symm self.Adj := by
aesop_graph
SimpleGraph.loopless : Std.Irrefl self.Adj := by
aesop_graph
constructor:
SimpleGraph.mk.{u} {V : Type u} (Adj : V → V → Prop) (symm : Std.Symm Adj := by aesop_graph)
(loopless : Std.Irrefl Adj := by aesop_graph) : SimpleGraph V**Fixing theorem proofs with symmetric tactic**
**Verifying theorem instance usage**
$ /bin/bash -lc 'lake env lean Norine.lean' Norine.lean:91:11: error(lean.synthInstanceFailed): failed to synthesize instance of type class Std.Symm CubeAdjacent Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. Norine.lean:94:20: error(lean.synthInstanceFailed): failed to synthesize instance of type class Std.Irrefl CubeAdjacent Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
**Refining symmetry and projection naming**
$ /bin/bash -lc 'lake env lean Norine.lean'
**Defining redGraph and component equivalences** **Implementing projection and adjacency lemmas**
**Detailing rook labeling construction** **Verifying adjacency and antipodal conditions**
**Compiling codebase**
$ /bin/bash -lc 'lake env lean Norine.lean'
Norine.lean:164:15: warning: `Fin.coe_castAdd` has been deprecated: Use `Fin.val_castAdd` instead
Norine.lean:182:4: error(lean.dependsOnNoncomputable): failed to compile definition, consider marking it as 'noncomputable' because it depends on 'SetLike.instFintype', which is 'noncomputable'
Norine.lean:186:4: error(lean.dependsOnNoncomputable): failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Fintype.equivFin', which is 'noncomputable'
Norine.lean:207:8: error: Tactic `rewrite` failed: Did not find an occurrence of the pattern
(EdgeColoring.colorGraph ?c true).Reachable ?x ?y
in the target expression
c.MonoConnected true (restrictCube n (redComponentCount c) x) (antipode (restrictCube n (redComponentCount c) x))
n : ℕ
c : EdgeColoring n
hc : c.IsAntipodal
hcounter : ¬HasMonochromaticAntipodalPath c
x : Cube (n + redComponentCount c)
h :
Fin.natAdd n (redComponentIndex c (restrictCube n (redComponentCount c) x)) =
Fin.natAdd n (redComponentIndex c (antipode (restrictCube n (redComponentCount c) x)))
⊢ c.MonoConnected true (restrictCube n (redComponentCount c) x) (antipode (restrictCube n (redComponentCount c) x))
Norine.lean:220:6: error: `simp` made no progress
Norine.lean:225:40: error(lean.invalidField): Invalid field `mpr`: The environment does not contain `Function.mpr`, so it is not possible to project the field `mpr` from an expression
Fin.natAdd_injective n
of type
∀ (n_1 : ℕ), Injective (Fin.natAdd n_1)
Norine.lean:226:8: error: No goals to be solved
Norine.lean:229:40: error(lean.invalidField): Invalid field `mpr`: The environment does not contain `Function.mpr`, so it is not possible to project the field `mpr` from an expression
Fin.natAdd_injective n
of type
∀ (n_1 : ℕ), Injective (Fin.natAdd n_1)
Norine.lean:230:8: error: No goals to be solved
Norine.lean:197:4: error(lean.dependsOnNoncomputable): failed to compile definition, consider marking it as 'noncomputable' because it depends on 'redCo**Marking noncomputable sections globally**
$ /bin/bash -lc "nl -ba Norine.lean | sed -n '190,240p'"
190 theorem redComponentIndex_injective_on_components {n : ℕ} (c : EdgeColoring n)
191 {x y : Cube n} :
192 redComponentIndex c x = redComponentIndex c y ↔ redComponent c x = redComponent c y :=
193 (Fintype.equivFin _).injective.eq_iff
194
195 /-- The label `(p(x),p(Ax))` from Lemma 2.2, padded to a square label set and
196 to a cube of the same dimension. -/
197 def counterexampleRookLabeling {n : ℕ} (c : EdgeColoring n) (hc : c.IsAntipodal)
198 (hcounter : ¬HasMonochromaticAntipodalPath c) :
199 RookLabeling (n + redComponentCount c) (n + redComponentCount c) where
200 fst x := Fin.natAdd n (redComponentIndex c (restrictCube n (redComponentCount c) x))
201 snd x := Fin.natAdd n
202 (redComponentIndex c (antipode (restrictCube n (redComponentCount c) x)))
203 offDiagonal := by
204 intro x h
205 apply hcounter
206 refine ⟨restrictCube n (redComponentCount c) x, true, ?_⟩
207 rw [← redComponent_eq_iff]
208 apply (redComponentIndex_injective_on_components c).mp
209 exact Fin.natAdd_injective n h
210 antipodal_fst := by
211 intro x
212 simp only [restrictCube_antipode, antipode_antipode]
213 antipodal_snd := by
214 intro x
215 simp only [restrictCube_antipode, antipode_antipode]
216 rook := by
217 intro x y hxy
218 obtain hproj | hproj := restrictCube_eq_or_adjacent hxy
219 · left
220 simp only
221 rw [hproj]
222 · by_cases hred : c (restrictCube n (redComponentCount c) x)
223 (restrictCube n (redComponentCount c) y) = true
224 · left
225 apply Fin.natAdd_injective n |>.mpr
226 apply (redComponentIndex_injective_on_components c).mpr
227 exact redComponent_eq_of_red_edge c hproj hred
228 · right
229 apply Fin.natAdd_injective n |>.mpr
230 apply (redComponentIndex_injective_on_components c)**Refactoring Fin.natAdd and MonoConnected proofs**
$ /bin/bash -lc 'lake env lean Norine.lean'
Norine.lean:166:15: warning: `Fin.coe_castAdd` has been deprecated: Use `Fin.val_castAdd` instead
Norine.lean:212:33: error: Application type mismatch: The argument
h
has type
Fin.natAdd n (redComponentIndex c (restrictCube n (redComponentCount c) x)) =
Fin.natAdd n (redComponentIndex c (antipode (restrictCube n (redComponentCount c) x)))
of sort `Prop` but is expected to have type
ℕ
of sort `Type` in the application
Fin.natAdd_injective n h
Norine.lean:229:8: error: Tactic `apply` failed: could not unify the conclusion of `Fin.natAdd_injective n`
?a₁ = ?a₂
with the goal
Fin.natAdd n (redComponentIndex c (restrictCube n (redComponentCount c) x)) =
Fin.natAdd n (redComponentIndex c (restrictCube n (redComponentCount c) y))
Note: The full type of `Fin.natAdd_injective n` is
∀ (n_1 : ℕ), Injective (Fin.natAdd n_1)
case pos
n : ℕ
c : EdgeColoring n
hc : c.IsAntipodal
hcounter : ¬HasMonochromaticAntipodalPath c
x y : Cube (n + redComponentCount c)
hxy : CubeAdjacent x y
hproj : CubeAdjacent (restrictCube n (redComponentCount c) x) (restrictCube n (redComponentCount c) y)
hred : c.color (restrictCube n (redComponentCount c) x) (restrictCube n (redComponentCount c) y) = true
⊢ Fin.natAdd n (redComponentIndex c (restrictCube n (redComponentCount c) x)) =
Fin.natAdd n (redComponentIndex c (restrictCube n (redComponentCount c) y))
Norine.lean:233:8: error: Tactic `apply` failed: could not unify the conclusion of `Fin.natAdd_injective n`
?a₁ = ?a₂
with the goal
Fin.natAdd n (redComponentIndex c (antipode (restrictCube n (redComponentCount c) x))) =
Fin.natAdd n (redComponentIndex c (antipode (restrictCube n (redComponentCount c) y)))
Note: The full type of `Fin.natAdd_injective n` is
∀ (n_1 : ℕ), Injective (Fin.natAdd n_1)
case neg
n : ℕ
c : EdgeColoring n
hc : c.IsAntipodal
hcounter : ¬HasMonochromaticAntipodalPath c
x y : Cube (n + redComponentCount c)
hxy : CubeAdjacent x y
hproj : CubeAdjacent (restrictCube n (redComponentCount c) x)**Verifying argument order for Fin.natAdd_injective**
$ /bin/bash -lc "cat >/tmp/Check.lean <<'EOF'
import Mathlib
#check Fin.natAdd_injective
#check Fin.castAdd_injective
#check Fin.natAdd
EOF
lake env lean /tmp/Check.lean"
Fin.natAdd_injective (m n : ℕ) : Function.Injective (Fin.natAdd n)
Fin.castAdd_injective (m n : ℕ) : Function.Injective (Fin.castAdd n)
Fin.natAdd {m : ℕ} (n : ℕ) (i : Fin m) : Fin (n + m)**Adding missing end statements**
$ /bin/bash -lc 'lake env lean Norine.lean'
Norine.lean:166:15: warning: `Fin.coe_castAdd` has been deprecated: Use `Fin.val_castAdd` instead
Norine.lean:230:8: error: Tactic `apply` failed: could not unify the conclusion of `(redComponentIndex_injective_on_components c).mpr`
redComponentIndex c ?m.114 = redComponentIndex c ?m.115
with the goal
Fin.natAdd n (Fin.natAdd n (redComponentIndex c (restrictCube n (redComponentCount c) x))) =
Fin.natAdd n (Fin.natAdd n (redComponentIndex c (restrictCube n (redComponentCount c) y)))
Note: The full type of `(redComponentIndex_injective_on_components c).mpr` is
redComponent c ?m.114 = redComponent c ?m.115 → redComponentIndex c ?m.114 = redComponentIndex c ?m.115
case pos
n : ℕ
c : EdgeColoring n
hc : c.IsAntipodal
hcounter : ¬HasMonochromaticAntipodalPath c
x y : Cube (n + redComponentCount c)
hxy : CubeAdjacent x y
hproj : CubeAdjacent (restrictCube n (redComponentCount c) x) (restrictCube n (redComponentCount c) y)
hred : c.color (restrictCube n (redComponentCount c) x) (restrictCube n (redComponentCount c) y) = true
⊢ Fin.natAdd n (Fin.natAdd n (redComponentIndex c (restrictCube n (redComponentCount c) x))) =
Fin.natAdd n (Fin.natAdd n (redComponentIndex c (restrictCube n (redComponentCount c) y)))
Norine.lean:234:8: error: Tactic `apply` failed: could not unify the conclusion of `(redComponentIndex_injective_on_components c).mpr`
redComponentIndex c ?m.127 = redComponentIndex c ?m.128
with the goal
Fin.natAdd n (Fin.natAdd n (redComponentIndex c (antipode (restrictCube n (redComponentCount c) x)))) =
Fin.natAdd n (Fin.natAdd n (redComponentIndex c (antipode (restrictCube n (redComponentCount c) y))))
Note: The full type of `(redComponentIndex_injective_on_components c).mpr` is
redComponent c ?m.127 = redComponent c ?m.128 → redComponentIndex c ?m.127 = redComponentIndex c ?m.128
case neg
n : ℕ
c : EdgeColoring n
hc : c.IsAntipodal
hcounter : ¬HasMonochromaticAntipodalPath c
x y : Cube (n + redComponentCount c)
hxy : CubeAdjacent x y
hpr**Correcting proof tactic to use congrArg**
$ /bin/bash -lc 'lake env lean Norine.lean'
Norine.lean:166:15: warning: `Fin.coe_castAdd` has been deprecated: Use `Fin.val_castAdd` instead
Norine.lean:215:38: warning: This simp argument is unused:
antipode_antipode
Hint: Omit it from the simp argument list.
[apply] simp only [restrictCube_antipode]
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
Norine.lean:223:6: warning: 'change
Fin.natAdd n (redComponentIndex c (restrictCube n (redComponentCount c) x)) =
Fin.natAdd n (redComponentIndex c (restrictCube n (redComponentCount c) y))' tactic does nothing
Note: This linter can be disabled with `set_option linter.unusedTactic false`**Exploring topological lemmas for diagonal proof** **Designing chain obstruction structure in Lean** **Clarifying kernel and image relations in chains**
**Planning dependent recursion construction** **Considering abstracting chain obstruction theorem** **Declaring central theorem hypothesis**
**Refining algebraic Borsuk-Ulam hypothesis** **Formulating degenerate simplicial Borsuk-Ulam hypothesis** **Verifying rank degeneracy conditions**
**Formalizing rank lemma hypothesis** **Planning external tooling search for chain complexes**
$ /bin/bash -lc 'curl -L --fail --max-time 30 -sS https://leangenius.org/data/proofs/borsuk-ulam-oq-03-oq-02/source.lean -o /tmp/bu-homology.lean
wc -l /tmp/bu-homology.lean
rg -n "''^(axiom|theorem|def|structure)|sorry|#print axioms" /tmp/bu-homology.lean | sed -n '"'1,240p'
sed -n '1,180p' /tmp/bu-homology.lean"
238 /tmp/bu-homology.lean
34:theorems have the honest shape *"given the standard identification `Hₙ(X) ≃+ ℤ`, the degree is
70:def degreeOfEnd (e : G ≃+ ℤ) (f : G →+ G) : ℤ := e (f (e.symm 1))
74:theorem degreeOfEnd_conj (e : G ≃+ ℤ) (f : G →+ G) (n : ℤ) :
92:theorem degreeOfEnd_comp (e : G ≃+ ℤ) (g f : G →+ G) :
105:theorem degreeOfEnd_indep (e₁ e₂ : G ≃+ ℤ) (f : G →+ G) :
133:theorem degreeOfEnd_equiv_isUnit (e : G ≃+ ℤ) (σ : G ≃+ G) :
143:theorem degreeOfEnd_equiv_eq (e : G ≃+ ℤ) (σ : G ≃+ G) :
170:theorem functorDegree_comp (F : C ⥤ AddCommGrpCat) {X : C}
179:theorem functorDegree_iso_eq (F : C ⥤ AddCommGrpCat) {X : C}
214:theorem brouwerDegree_comp (n : ℕ) {X : TopCat} (e : ((Hn n).obj X : Type) ≃+ ℤ)
220:theorem brouwerDegree_iso_eq (n : ℕ) {X : TopCat} (e : ((Hn n).obj X : Type) ≃+ ℤ)
/-
Copyright (c) 2026 Lean Genius. All rights reserved.
Released under Apache 2.0 license.
Authors: Lean Genius Researcher
# Brouwer Degree via Mathlib Homology
This file develops the algebraic and functorial core of **Brouwer degree theory** and
instantiates it on Mathlib's genuine singular-homology functor
(`AlgebraicTopology.singularHomologyFunctor`, Andrew Yang, 2025).
## Mathematical background
For a continuous self-map `f : Sⁿ → Sⁿ` of the `n`-sphere, the *Brouwer degree* `deg f` is
the integer by which the induced endomorphism `f∗ : Hₙ(Sⁿ) → Hₙ(Sⁿ)` acts, after the canonical
identification `Hₙ(Sⁿ) ≅ ℤ`. Its defining properties are
* `deg id = 1`,
* `deg (g ∘ f) = (deg g) · (deg f)` (functoriality / multiplicativity),
* a homeomorphism has degree `±1`,
* the degree does **not** depend on the chosen identification `Hₙ(Sⁿ) ≅ ℤ`.
These four facts are *purely formal* consequences of homology being a functor into abelian
groups together with `Hₙ(Sⁿ) ≅ ℤ`. This file isolates that formal content and proves it in
full generality, with **0 sorries and 0 axioms** (only the standard `propext / Classical.choice
/ Quot.sound`).
## What is and is not assumed
Mathlib's singular**Assessing polyhedral package availability**
$ /bin/bash -lc "rg -n \"def Polytope|structure Polytope|polyhedral cone|PolyhedralCone|IsPolyhedral|Minkowski.Weyl|finitelyGenerated.*cone\" Mathlib | sed -n '1,240p'" Mathlib/Geometry/Convex/Cone/DualFinite.lean:21:In finite dimensional vector spaces, `FG` is equivalent to `DualFG` by the Minkowski-Weyl theorem. Mathlib/Geometry/Convex/Cone/DualFinite.lean:22:In this case, V- and H-cones are known as polyhedral cones.
**Formulating polyhedral chain hypothesis** **Planning abstract chain obstruction formalization** **Implementing abstract chain obstruction lemma**
**Detailing AugComplex structure and instances** **Designing recursive tower construction and induction**
**Planning recursive construction with reverse induction** **Formulating descending lemma with recursive induction**
**Planning finite cell complex abstraction** **Defining direct limit for complexes**
**Designing PolyhedralBorsukUlam theorem structure** **Proving equivalence between rook and naive structures**
The cubical-Tucker shortcut fails in dimensions \(K\ge3\): there are antipodal signed labelings of cube vertices with no complementary original cube edge, so the subdivision diagonals cannot be ignored. I also checked the available external Lean material; it provides Sperner infrastructure and only low-dimensional Tucker/Borsuk–Ulam results, while mathlib has no polytope face/subdivision library. I’m retaining the exact graph reduction and now adding formal equivalence checks for the paper’s definitions before deciding whether the missing general polyhedral-chain layer can be completed honestly.
**Compiling codebase**
$ /bin/bash -lc 'lake env lean Norine.lean'
Norine.lean:226:15: warning: `Fin.coe_castAdd` has been deprecated: Use `Fin.val_castAdd` instead
Norine.lean:275:38: warning: This simp argument is unused:
antipode_antipode
Hint: Omit it from the simp argument list.
[apply] simp only [restrictCube_antipode]
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
Norine.lean:283:6: warning: 'change
Fin.natAdd n (redComponentIndex c (restrictCube n (redComponentCount c) x)) =
Fin.natAdd n (redComponentIndex c (restrictCube n (redComponentCount c) y))' tactic does nothing
Note: This linter can be disabled with `set_option linter.unusedTactic false`**Formalizing chain obstruction using finite SmithTower** **Planning decomposition property proof via induction**
**Formulating recursive descend lemma** **Refining recursion using uniform grading** **Outlining lemma conditions for chain sequences**
**Formulating induction proof for augmentation** **Adjusting sequence for recursive dimension**
**Formalizing induction lemma proof** **Planning ChainObstruction lemma coding**
**Establishing add_self_eq_zero lemma for characteristic two** **Planning chain map construction and descent proof**
**Compiling project sources**
$ /bin/bash -lc 'lake env lean ChainObstruction.lean' ChainObstruction.lean:22:56: error: unsolved goals D : Type u_1 inst✝¹ : AddCommGroup D inst✝ : Module F₂ D x : D ⊢ 2 = 0 ∨ x = 0 ChainObstruction.lean:65:38: error: Tactic `rewrite` failed: Did not find an occurrence of the pattern boundary ∘ₗ norm in the target expression boundary (if True then 0 else y (d + 1)) = norm (y d) + (norm ∘ₗ boundary) z case pos D : Type u_1 inst✝¹ : AddCommGroup D inst✝ : Module F₂ D boundary norm : D →ₗ[F₂] D aug : D →ₗ[F₂] F₂ boundary_sq : boundary ∘ₗ boundary = 0 boundary_norm : boundary ∘ₗ norm = norm ∘ₗ boundary aug_boundary : aug ∘ₗ boundary = 0 aug_norm : aug ∘ₗ norm = 0 norm_exact : ∀ (y : D), norm y = 0 → ∃ z, norm z = y d : ℕ ih : ∀ (y : ℕ → D), (∀ i ≤ d, boundary (y (i + 1)) = norm (y i)) → y (d + 1) = 0 → aug (y 0) = 0 y : ℕ → D tower : ∀ i ≤ d + 1, boundary (y (i + 1)) = norm (y i) top : y (d + 1 + 1) = 0 hnorm_top : norm (y (d + 1)) = 0 z : D hz : norm z = y (d + 1) y' : ℕ → D := fun i => if i = d then y i + boundary z else if i = d + 1 then 0 else y i hy'_top : y' (d + 1) = 0 hi : d ≤ d ⊢ boundary (if True then 0 else y (d + 1)) = norm (y d) + (norm ∘ₗ boundary) z ChainObstruction.lean:74:24: error: Tactic `rewrite` failed: Did not find an occurrence of the pattern boundary (y (i + 1)) in the target expression boundary (y d) = norm (if False then y i + boundary z else if False then 0 else y i) case pos D : Type u_1 inst✝¹ : AddCommGroup D inst✝ : Module F₂ D boundary norm : D →ₗ[F₂] D aug : D →ₗ[F₂] F₂ boundary_sq : boundary ∘ₗ boundary = 0 boundary_norm : boundary ∘ₗ norm = norm ∘ₗ boundary aug_boundary : aug ∘ₗ boundary = 0 aug_norm : aug ∘ₗ norm = 0 norm_exact : ∀ (y : D), norm y = 0 → ∃ z, norm z = y d : ℕ ih : ∀ (y : ℕ → D), (∀ i ≤ d, boundary (y (i + 1)) = norm (y i)) → y (d + 1) = 0 → aug (y 0) = 0 y : ℕ → D tower : ∀ i ≤ d + 1, boundary (y (i + 1)) = norm (y i) top : y (d + 1 + 1) = 0 hnorm_top : norm (y (d + 1)) = 0 z : D hz : norm z = y (d + 1) y' : ℕ → D := fun i => if i = d then y i + boundary z els
**Fixing add_self lemma in F2 syntax** **Refining simp strategy for boundary norm proof**
**Applying linear map congruences**
**Reviewing unused HSQL error linting**
$ /bin/bash -lc 'lake env lean ChainObstruction.lean' ChainObstruction.lean:26:13: error: unsolved goals D : Type u_1 inst✝¹ : AddCommGroup D inst✝ : Module F₂ D x : D ⊢ 2 = 0 ∨ x = 0 ChainObstruction.lean:69:33: error: Tactic `rewrite` failed: Did not find an occurrence of the pattern (norm ∘ₗ boundary) z in the target expression 0 = norm (y d) + norm (boundary z) case pos D : Type u_1 inst✝¹ : AddCommGroup D inst✝ : Module F₂ D boundary norm : D →ₗ[F₂] D aug : D →ₗ[F₂] F₂ boundary_sq : boundary ∘ₗ boundary = 0 boundary_norm : boundary ∘ₗ norm = norm ∘ₗ boundary aug_boundary : aug ∘ₗ boundary = 0 aug_norm : aug ∘ₗ norm = 0 norm_exact : ∀ (y : D), norm y = 0 → ∃ z, norm z = y d : ℕ ih : ∀ (y : ℕ → D), (∀ i ≤ d, boundary (y (i + 1)) = norm (y i)) → y (d + 1) = 0 → aug (y 0) = 0 y : ℕ → D tower : ∀ i ≤ d + 1, boundary (y (i + 1)) = norm (y i) top : y (d + 1 + 1) = 0 hnorm_top : norm (y (d + 1)) = 0 z : D hz : norm z = y (d + 1) y' : ℕ → D := fun i => if i = d then y i + boundary z else if i = d + 1 then 0 else y i hy'_top : y' (d + 1) = 0 hi : d ≤ d hcomm : (boundary ∘ₗ norm) z = (norm ∘ₗ boundary) z ⊢ 0 = norm (y d) + norm (boundary z) ChainObstruction.lean:82:16: error: unsolved goals D : Type u_1 inst✝¹ : AddCommGroup D inst✝ : Module F₂ D boundary norm : D →ₗ[F₂] D aug : D →ₗ[F₂] F₂ boundary_sq : boundary ∘ₗ boundary = 0 boundary_norm : boundary ∘ₗ norm = norm ∘ₗ boundary aug_boundary : aug ∘ₗ boundary = 0 aug_norm : aug ∘ₗ norm = 0 norm_exact : ∀ (y : D), norm y = 0 → ∃ z, norm z = y d : ℕ ih : ∀ (y : ℕ → D), (∀ i ≤ d, boundary (y (i + 1)) = norm (y i)) → y (d + 1) = 0 → aug (y 0) = 0 y : ℕ → D tower : ∀ i ≤ d + 1, boundary (y (i + 1)) = norm (y i) top : y (d + 1 + 1) = 0 hnorm_top : norm (y (d + 1)) = 0 z : D hz : norm z = y (d + 1) y' : ℕ → D := fun i => if i = d then y i + boundary z else if i = d + 1 then 0 else y i hy'_top : y' (d + 1) = 0 i : ℕ hi : i ≤ d hid : ¬i = d hilt : i < d hi_ne_succ : i ≠ d + 1 his_ne_succ : i + 1 ≠ d + 1 hisd : ¬i + 1 = d ⊢ i = d → 0 = y (i + 1) ChainObstruction.lean:83:34: warn
**Exploring scalar multiplication rewriting in F₂**
$ /bin/bash -lc "rg -n \"add_self_eq_zero.*Module|add_self.*CharP|two_smul.*CharP|Module.*ZMod 2|ZMod.*add_self\" Mathlib | sed -n '1,160p'
cat >/tmp/Check.lean <<'EOF'
import Mathlib
#check two_smul
#check Nat.cast_smul_eq_nsmul
#check Nat.smul_one_eq_cast
#check CharP.cast_eq_zero
#check add_self_eq_zero
#check eq_neg_of_add_eq_zero_left
EOF
lake env lean /tmp/Check.lean"
two_smul.{u_1, u_3} (R : Type u_1) {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) : 2 • x = x + x
Nat.cast_smul_eq_nsmul.{u_1, u_3} (R : Type u_1) {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (n : ℕ)
(b : M) : ↑n • b = n • b
Nat.smul_one_eq_cast.{u_5} {R : Type u_5} [NonAssocSemiring R] (m : ℕ) : m • 1 = ↑m
CharP.cast_eq_zero.{u_1} (R : Type u_1) [AddMonoidWithOne R] (p : ℕ) [CharP R p] : ↑p = 0
add_self_eq_zero.{u_2} {R : Type u_2} [NonAssocSemiring R] [NoZeroDivisors R] [CharZero R] {a : R} : a + a = 0 ↔ a = 0
eq_neg_of_add_eq_zero_left.{u_1} {G : Type u_1} [SubtractionMonoid G] {a b : G} (h : a + b = 0) : a = -b**Patching simplification bug in hcomm and hisd proofs**
$ /bin/bash -lc 'lake env lean ChainObstruction.lean'
**Planning chain certificate structure** **Formulating certificate-based contradiction hypothesis** **Modularizing forbidden chain map definition**
**Refactoring chain obstruction structure**
$ /bin/bash -lc 'lake env lean ChainObstruction.lean'
**Planning formalization of rank lemma** **Formalizing norm kernel image lemma** **Defining linear pullback operator**
**Planning antipodal module proof**
**Compiling codebase**
$ /bin/bash -lc 'lake env lean AntipodalModule.lean' AntipodalModule.lean:1:0: error: unknown module prefix 'ChainObstruction' No directory 'ChainObstruction' or file 'ChainObstruction.olean' in the search path entries: /work/repro/.lake/packages/Cli/.lake/build/lib/lean /work/repro/.lake/packages/batteries/.lake/build/lib/lean /work/repro/.lake/packages/Qq/.lake/build/lib/lean /work/repro/.lake/packages/aesop/.lake/build/lib/lean /work/repro/.lake/packages/proofwidgets/.lake/build/lib/lean /work/repro/.lake/packages/importGraph/.lake/build/lib/lean /work/repro/.lake/packages/LeanSearchClient/.lake/build/lib/lean /work/repro/.lake/packages/plausible/.lake/build/lib/lean /work/repro/.lake/build/lib/lean /opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/lib/lean /opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/lib/lean
**Planning file restructuring and renaming** **Organizing Norine module imports and moves**
**Planning separate move and patch operations**
**Verifying Lean compilation produces olean**
$ /bin/bash -lc "lake env lean Norine/ChainObstruction.lean && ls -l Norine | sed -n '1,40p' && lake env lean Norine/AntipodalModule.lean" total 24 -rw-r--r-- 1 root root 2654 Jul 23 14:12 AntipodalModule.lean -rw-r--r-- 1 root root 11611 Jul 23 14:12 Basic.lean -rw-r--r-- 1 root root 8074 Jul 23 14:12 ChainObstruction.lean Norine/AntipodalModule.lean:1:0: error: unknown module prefix 'Norine' No directory 'Norine' or file 'Norine.olean' in the search path entries: /work/repro/.lake/packages/Cli/.lake/build/lib/lean /work/repro/.lake/packages/batteries/.lake/build/lib/lean /work/repro/.lake/packages/Qq/.lake/build/lib/lean /work/repro/.lake/packages/aesop/.lake/build/lib/lean /work/repro/.lake/packages/proofwidgets/.lake/build/lib/lean /work/repro/.lake/packages/importGraph/.lake/build/lib/lean /work/repro/.lake/packages/LeanSearchClient/.lake/build/lib/lean /work/repro/.lake/packages/plausible/.lake/build/lib/lean /work/repro/.lake/build/lib/lean /opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/lib/lean /opt/elan/toolchains/leanprover--lean4---v4.33.0-rc1/lib/lean
**Planning Norine library integration** **Preparing to build Norine library**
$ /bin/bash -lc 'lake build Norine.ChainObstruction' ✔ [8677/8677] Built Norine.ChainObstruction (5.7s) Build completed successfully (8677 jobs).
**Compiling Antipodal**
$ /bin/bash -lc 'lake env lean Norine/AntipodalModule.lean' Norine/AntipodalModule.lean:34:0: warning: automatically included section variable(s) unused in theorem `Norine.basisPull_apply`: [Fintype α] [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype α] [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` Norine/AntipodalModule.lean:38:0: warning: automatically included section variable(s) unused in theorem `Norine.basisNorm_apply`: [Fintype α] [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype α] [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` Norine/AntipodalModule.lean:49:28: error(lean.unknownIdentifier): Unknown constant `LinearOrder.ofFinite` Norine/AntipodalModule.lean:52:37: error: Application type mismatch: The argument hf has type f ∈ (basisNorm A).ker but is expected to have type ?m.64 = ?m.65 in the application LinearMap.congr_fun hf Norine/AntipodalModule.lean:52:17: error(lean.synthInstanceFailed): failed to synthesize instance of type class AddCommMonoid α Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. Norine/AntipodalModule.lean:61:4: error: unsolved goals case a.inl α : Type u_1 inst✝¹ : Fintype α inst✝ : DecidableEq α A : α → α hA : ∀ (a : α), A (A a) = a hfree : ∀ (a : α), A a ≠ a f : α → F₂ hf : f ∈ (basisNorm A).ker this : LinearOrder α := sorry hinv : ∀ (a : α), f (A a) = f a g : α → F₂ := fun a => if a < A a then f a else 0 a : α haa : a < A a hnot : ¬A a < A (A a) ⊢ A a < a → f (A a) = 0 Norine/AntipodalModule.lean:65:2: error: unsolved goals case a α : Type u_1 inst✝¹ : Fintype α inst✝ : DecidableEq α A : α → α hA : ∀ (a : α), A (A a) = a hfree : ∀ (a : α), A a ≠ a g : α → F₂ a : α ⊢ g a
**Investigating finite linear order existence**
$ /bin/bash -lc "rg -n \"def.*[Ll]inearOrder.*[Ff]inite|linearOrderOf|Fintype.*LinearOrder|Finite.*LinearOrder\" Mathlib/Data Mathlib/Order | sed -n '1,160p'
cat >/tmp/Check.lean <<'EOF'
import Mathlib
#check Fintype.truncEquivFin
#check Fintype.equivFin
#check LinearOrder.lift
#check LinearOrder.liftWithOrd
#check Fintype.ofFinite
#check LinearMap.mem_ker
#check LinearMap.mem_ker'
EOF
lake env lean /tmp/Check.lean"
Fintype.truncEquivFin.{u_4} (α : Type u_4) [DecidableEq α] [Fintype α] : Trunc (α ≃ Fin (Fintype.card α))
Fintype.equivFin.{u_4} (α : Type u_4) [Fintype α] : α ≃ Fin (Fintype.card α)
LinearOrder.lift.{u_2, u_3} {α : Type u_2} {β : Type u_3} [LinearOrder β] [Max α] [Min α] (f : α → β)
(inj : Function.Injective f) (hsup : ∀ (x y : α), f (x ⊔ y) = max (f x) (f y))
(hinf : ∀ (x y : α), f (x ⊓ y) = min (f x) (f y)) : LinearOrder α
LinearOrder.liftWithOrd.{u_2, u_3} {α : Type u_2} {β : Type u_3} [LinearOrder β] [Max α] [Min α] [Ord α] (f : α → β)
(inj : Function.Injective f) (hsup : ∀ (x y : α), f (x ⊔ y) = max (f x) (f y))
(hinf : ∀ (x y : α), f (x ⊓ y) = min (f x) (f y)) (compare_f : ∀ (a b : α), compare a b = compare (f a) (f b)) :
LinearOrder α
Fintype.ofFinite.{u_4} (α : Type u_4) [Finite α] : Fintype α
LinearMap.mem_ker.{u_1, u_2, u_5, u_7} {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [Semiring R]
[Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂}
{y : M} : y ∈ f.ker ↔ f y = 0
/tmp/Check.lean:8:7: error(lean.unknownIdentifier): Unknown constant `LinearMap.mem_ker'`**Refining kernel and norm proof approach** **Simplifying addition cases with finite indexing**
$ /bin/bash -lc 'lake env lean Norine/AntipodalModule.lean' Norine/AntipodalModule.lean:34:0: warning: automatically included section variable(s) unused in theorem `Norine.basisPull_apply`: [Fintype α] [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype α] [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` Norine/AntipodalModule.lean:38:0: warning: automatically included section variable(s) unused in theorem `Norine.basisNorm_apply`: [Fintype α] [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype α] [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` Norine/AntipodalModule.lean:61:61: error: Application type mismatch: The argument h has type e a = e (A a) but is expected to have type e (A a) = e a in the application Equiv.injective e h Norine/AntipodalModule.lean:63:4: error: unsolved goals case a.inl α : Type u_1 inst✝¹ : Fintype α inst✝ : DecidableEq α A : α → α hA : ∀ (a : α), A (A a) = a hfree : ∀ (a : α), A a ≠ a f : α → F₂ hf : f ∈ (basisNorm A).ker e : α ≃ Fin (Fintype.card α) := Fintype.equivFin α hinv : ∀ (a : α), f (A a) = f a g : α → F₂ := fun a => if e a < e (A a) then f a else 0 a : α hne : e a ≠ e (A a) haa : e a < e (A a) hnot : ¬e (A a) < e (A (A a)) ⊢ e (A a) < e a → f (A a) = 0 Norine/AntipodalModule.lean:66:17: warning: This simp argument is unused: hnot Hint: Omit it from the simp argument list. [apply] simp [haa, hA] Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
**Planning proof steps for condition simplification** **Applying conditional rewrites for proof branches**
**Inspecting code lines**
$ /bin/bash -lc "nl -ba Norine/AntipodalModule.lean | sed -n '50,76p'"
50 have hinv : ∀ a, f (A a) = f a := by
51 intro a
52 have hker : basisNorm A f = 0 := LinearMap.mem_ker.mp hf
53 have ha := congrFun hker a
54 simp only [basisNorm_apply, Pi.zero_apply] at ha
55 have hneg := eq_neg_of_add_eq_zero_left ha
56 simpa [ZModModule.neg_eq_self] using hneg.symm
57 let g : α → F₂ := fun a ↦ if e a < e (A a) then f a else 0
58 refine ⟨g, ?_⟩
59 funext a
60 simp only [basisNorm_apply, g]
61 have hne : e a ≠ e (A a) := fun h ↦ hfree a (e.injective h)
62 rcases lt_or_gt_of_ne hne with haa | haa
63 · have hnot : ¬e (A a) < e (A (A a)) := by
64 rw [hA]
65 exact not_lt_of_ge haa.le
66 simp [haa, hnot, hA]
67 · have hnot : ¬e a < e (A a) := not_lt_of_ge haa.le
68 simp [hnot, haa, hA, hinv]
69 · intro f
70 rintro ⟨g, rfl⟩
71 ext a
72 simp only [basisNorm_apply, hA]
73 calc
74 g a + g (A a) + (g (A a) + g a) =
75 (g a + g a) + (g (A a) + g (A a)) := by ac_rfl
76 _ = 0 := by simp [ZModModule.add_self]$ /bin/bash -lc 'lake env lean Norine/AntipodalModule.lean' Norine/AntipodalModule.lean:34:0: warning: automatically included section variable(s) unused in theorem `Norine.basisPull_apply`: [Fintype α] [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype α] [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` Norine/AntipodalModule.lean:38:0: warning: automatically included section variable(s) unused in theorem `Norine.basisNorm_apply`: [Fintype α] [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [Fintype α] [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false` Norine/AntipodalModule.lean:43:0: warning: automatically included section variable(s) unused in theorem `Norine.basisNorm_ker_eq_range`: [DecidableEq α] consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit [DecidableEq α] in theorem ... Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
**Planning cubical source tower implementation** **Constructing explicit Smith tower chains** **Defining chain groups and contraction maps**
**Drafting conditional theorem file** **Enumerating partial proof obstacles**
**Building Basic and Antipodal dependencies**
$ /bin/bash -lc 'lake build Norine.Basic Norine.AntipodalModule && lake env lean Norine/Reproduction.lean'
⚠ [8678/8679] Built Norine.AntipodalModule (5.1s)
warning: Norine/AntipodalModule.lean:34:0: automatically included section variable(s) unused in theorem `Norine.basisPull_apply`:
[Fintype α]
[DecidableEq α]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
omit [Fintype α] [DecidableEq α] in theorem ...
Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Norine/AntipodalModule.lean:38:0: automatically included section variable(s) unused in theorem `Norine.basisNorm_apply`:
[Fintype α]
[DecidableEq α]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
omit [Fintype α] [DecidableEq α] in theorem ...
Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: Norine/AntipodalModule.lean:43:0: automatically included section variable(s) unused in theorem `Norine.basisNorm_ker_eq_range`:
[DecidableEq α]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
omit [DecidableEq α] in theorem ...
Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
⚠ [8679/8679] Built Norine.Basic (5.7s)
warning: Norine/Basic.lean:226:15: `Fin.coe_castAdd` has been deprecated: Use `Fin.val_castAdd` instead
warning: Norine/Basic.lean:275:38: This simp argument is unused:
antipode_antipode
Hint: Omit it from the simp argument list.
[apply] simp only [restrictCube_antipode]
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Norine/Basic.lean:283:6: 'change
Fin.natAdd n (redComponentIndex c (restrictCube n (redComponentCount c) x)) =
Fin.natAdd n (redComponentIndex c (restrictCube n (redComponentCount c) y))' tactic does nothing
Note: This linter can be disabled with `set_option linter.unusedTactic false`
Build completed successfully (867**Cleaning warnings and removing unused variables**
**Planning polyhedral chain formalization** **Outlining comprehensive README contents** **Gathering build and axiom metadata**
The formal development now checks three substantial layers with zero `sorry`: the exact Norine-to-rook reduction, the algebraic chain-level Borsuk–Ulam obstruction (including its descending norm argument), and the fixed-point-free antipodal permutation-module identity \(\ker(1+A)=\operatorname{im}(1+A)\). The remaining gap is now isolated to one proposition-level interface: constructing the forbidden chain map from a rook labeling via subdivision-invariant radial polyhedral chains—the genuinely new Sections 4–5 machinery for which neither mathlib nor the tooling projects provide a usable general library.$ /bin/bash -lc "git rev-parse HEAD && cat lean-toolchain && rg -n \"\\bsorry\\b|"'^'"\\s*axiom\\b|"'^'"\\s*opaque\\b\" Norine || true lake build Norine && lake env lean Norine/Reproduction.lean" ✔ [8678/8681] Built Norine.AntipodalModule (4.9s) ✔ [8679/8681] Built Norine.Basic (4.9s) ℹ [8680/8681] Built Norine.Reproduction (4.3s) info: Norine/Reproduction.lean:46:0: 'Norine.monoConnected_iff_walk' does not depend on any axioms info: Norine/Reproduction.lean:47:0: 'Norine.rookLabelingEquivNaive' does not depend on any axioms info: Norine/Reproduction.lean:48:0: 'Norine.norine_of_diagonal_rook' depends on axioms: [propext, Classical.choice, Quot.sound] info: Norine/Reproduction.lean:49:0: 'Norine.norm_tower_aug_zero' depends on axioms: [propext, Classical.choice, Quot.sound] info: Norine/Reproduction.lean:50:0: 'Norine.chain_level_borsuk_ulam' depends on axioms: [propext, Classical.choice, Quot.sound] info: Norine/Reproduction.lean:51:0: 'Norine.forbiddenChainMap_isEmpty' depends on axioms: [propext, Classical.choice, Quot.sound] info: Norine/Reproduction.lean:52:0: 'Norine.basisNorm_ker_eq_range' depends on axioms: [propext, Classical.choice, Quot.sound] info: Norine/Reproduction.lean:53:0: 'Norine.norine_conjecture_of_polyhedralChainRealization' depends on axioms: [propext, Classical.choice, Quot.sound] Build completed successfully (8681 jobs). 'Norine.monoConnected_iff_walk' does not depend on any axioms 'Norine.rookLabelingEquivNaive' does not depend on any axioms 'Norine.norine_of_diagonal_rook' depends on axioms: [propext, Classical.choice, Quot.sound] 'Norine.norm_tower_aug_zero' depends on axioms: [propext, Classical.choice, Quot.sound] 'Norine.chain_level_borsuk_ulam' depends on axioms: [propext, Classical.choice, Quot.sound] 'Norine.forbiddenChainMap_isEmpty' depends on axioms: [propext, Classical.choice, Quot.sound] 'Norine.basisNorm_ker_eq_range' depends on axioms: [propext, Classical.choice, Quot.sound] 'Norine.norine_conjecture_of_polyhedralChainRealization' depends on axioms: [propext, Classical.choice, Quot.sound]
**Verifying comment search results**
**Updating plan statuses**
**Planning final README verification**
$ /bin/bash -lc "lake build Norine && lake env lean Norine/Reproduction.lean && rg -n '\\bsorry\\b|"'^'"\\s*axiom\\b|"'^'"\\s*opaque\\b' Norine || true git status --short -- Norine README.md lakefile.lean git diff --stat -- Norine README.md lakefile.lean" ℹ [8680/8681] Replayed Norine.Reproduction info: Norine/Reproduction.lean:46:0: 'Norine.monoConnected_iff_walk' does not depend on any axioms info: Norine/Reproduction.lean:47:0: 'Norine.rookLabelingEquivNaive' does not depend on any axioms info: Norine/Reproduction.lean:48:0: 'Norine.norine_of_diagonal_rook' depends on axioms: [propext, Classical.choice, Quot.sound] info: Norine/Reproduction.lean:49:0: 'Norine.norm_tower_aug_zero' depends on axioms: [propext, Classical.choice, Quot.sound] info: Norine/Reproduction.lean:50:0: 'Norine.chain_level_borsuk_ulam' depends on axioms: [propext, Classical.choice, Quot.sound] info: Norine/Reproduction.lean:51:0: 'Norine.forbiddenChainMap_isEmpty' depends on axioms: [propext, Classical.choice, Quot.sound] info: Norine/Reproduction.lean:52:0: 'Norine.basisNorm_ker_eq_range' depends on axioms: [propext, Classical.choice, Quot.sound] info: Norine/Reproduction.lean:53:0: 'Norine.norine_conjecture_of_polyhedralChainRealization' depends on axioms: [propext, Classical.choice, Quot.sound] Build completed successfully (8681 jobs). 'Norine.monoConnected_iff_walk' does not depend on any axioms 'Norine.rookLabelingEquivNaive' does not depend on any axioms 'Norine.norine_of_diagonal_rook' depends on axioms: [propext, Classical.choice, Quot.sound] 'Norine.norm_tower_aug_zero' depends on axioms: [propext, Classical.choice, Quot.sound] 'Norine.chain_level_borsuk_ulam' depends on axioms: [propext, Classical.choice, Quot.sound] 'Norine.forbiddenChainMap_isEmpty' depends on axioms: [propext, Classical.choice, Quot.sound] 'Norine.basisNorm_ker_eq_range' depends on axioms: [propext, Classical.choice, Quot.sound] 'Norine.norine_conjecture_of_polyhedralChainRealization' depends on axioms: [propext, Classical.choice, Quot.sound] M README.md M lakefile.lean ?? Norine/ README.md | 336 +++++++++++++++++++++++++++++++--------------------------- lakefile.lean | 4 + 2 files changed, 181 insertions(+), 159 deletions(-)
**Planning to preserve existing README changes** **Planning README merge with original content**
$ /bin/bash -lc "git show HEAD:README.md | sed -n '1,260p'" # mathlib4  [](https://mathlib-bors-ca18eefec4cb.herokuapp.com/repositories/16) [](https://leanprover.zulipchat.com) [](https://gitpod.io/#https://github.com/leanprover-community/mathlib4) [Mathlib](https://leanprover-community.github.io) is a user maintained library for the [Lean theorem prover](https://leanprover.github.io). It contains both programming infrastructure and mathematics, as well as tactics that use the former and allow to develop the latter. ## Installation You can find detailed instructions to install Lean, mathlib, and supporting tools on [our website](https://leanprover-community.github.io/get_started.html). Alternatively, click on one of the buttons below to open a GitHub Codespace or a Gitpod workspace containing the project. [](https://codespaces.new/leanprover-community/mathlib4) [](https://gitpod.io/#https://github.com/leanprover-community/mathlib4) ## Using `mathlib4` as a dependency Please refer to [https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency](https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency) ## Experimenting Got everything installed? Why not start with the [tutorial project](https://leanprover-community.github.io/install/project.html)? For more pointers, see [Learning Lean](https://leanprover-community.github.io/learn.html). ## Documentation Besides the installation guides above and [Lean's general documentation](https://docs.lea
**Planning README patch with original appendix**
**Reviewing summary accuracy and update plan**
**Composing single valid JSON object** **Refining JSON content and formatting**
{"status":"partial","claim":"Lean proves NorineConjecture from the explicit hypothesis PolyhedralChainRealization: every diagonal rook labeling yields the forbidden Smith tower constructed by the paper's radial polyhedral chains. The reduction to rook labelings, chain-level Borsuk–Ulam obstruction, and ker(1+A)=im(1+A) for free antipodal modules are proved with zero sorry and only mathlib's standard axioms.","note":"The missing hypothesis encapsulates Sections 4–5: polyhedral subdivisions, common refinements, radial cancellation, the rook-gallery rank bound, and the resulting chain map. Mathlib lacks the required polytope face/subdivision theory. Attempts via continuous perturbation, cubical Tucker, exterior/Orlik–Solomon chains, constructible functions, and external Lean projects did not close this gap; README.md documents each obstruction and the tooling trace. `lake build Norine` and `lake env lean Norine/Reproduction.lean` pass. No error in the paper was found.","significance":"The paper claims that every antipodal red–blue edge-coloring of $Q_n$, for $n\\ge2$, has a monochromatic path from some vertex to its antipode. This would settle Norine's conjecture uniformly in all dimensions; the formal run verifies its reduction and algebraic obstruction but not the novel geometric chain-map construction."}