Example 5.2

Proved

QAlgorithms.Papers.Independent.Intakethird100.P07.vectorSpace_loopContractible

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $V$ be a real topological vector space, with no norm, local convexity or completeness assumption. For $v\in V$ and $t\in[0,1]$ set $\Phi(v,t)=tv$ . This is a continuous homotopy through additive endomorphisms and

\Phi(v,0)=0,\qquad\Phi(v,1)=v,\qquad\Phi(v+w,t)=\Phi(v,t)+\Phi(w,t).

Reversing time gives a contraction to zero. Thus $V$ is loop contractible.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P07

Formal statement

noncomputable section

universe u v

namespace QAlgorithms.Papers.Independent.Intakethird100.P07

open CategoryTheory Topology TopologicalSpace

/-- Example 5.2, PDF p. 20: scalar multiplication is a loop contraction
of every real topological vector space, with no norm or completeness requirement. -/
theorem vectorSpace_loopContractible
    (V : Type u) [TopologicalSpace V] [AddCommGroup V] [Module ℝ V]
    [IsTopologicalAddGroup V] [ContinuousSMul ℝ V] :
    IsAddLoopContraction (scalarHomotopy (V := V)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P07

end

Source

Cohomology of Local Cochains, arXiv:1110.2661v2, PDF p. 20, Example 5.2

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

For every type $V$ equipped with a topology, an additive commutative group structure, and a real module structure, assume that addition $V\times V\to V$ and additive inversion $V\to V$ are continuous, and that scalar multiplication $\mathbb R\times V\to V$ is jointly continuous. Then the function $\phi:V\times[0,1]\to V$ defined by $\phi(x,t)=t\mathbin{\bullet}x$ is continuous for the product topology, satisfies $\phi(x,0)=0_V$ and $\phi(x,1)=x$ for every $x\in V$ , and satisfies $\phi(x+y,t)=\phi(x,t)+\phi(y,t)$ for every $t\in[0,1]$ and every $x,y\in V$ . The interval carries its usual subspace topology.

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph