Topological groups containing the Sorgenfrey line The Sorgenfrey line $\mathbb S$ is the real line endowed with the topology generated by the base consisting of all half-intervals $[a,b)$ for real numbers $a<b$. 
The Sorgenfrey line is first-countable and non-metrizable and hence is not homeomorphic to a topological group. 
On the other hand, the Sorgenfrey line $\mathbb S$ is homeomorphic to a subset of a topological group. For example, the free topological group $F(\mathbb S)$ over $\mathbb S$ contains a closed topological copy of $\mathbb S$. But $F(\mathbb S)$ also contains a topological copy of the square $\mathbb S\times\mathbb S$ and hence $F(\mathbb S)$ contains an uncountable discrete subspace. Is this situation typical?

Problem. Let $G$ be a topological group containing a topological copy of the Sorgenfrey line. Does $G$ necessarily contain a uncountable discrete subspace?


Added in Edit. The answer to this problem is affirmative under OCA (the Open Coloring Axiom), which follows from PFA (the Proper Forcing Axiom).

Theorem (OCA). Under OCA, a topological group $G$ has uncountable spread if $G$ contains a subset, homeomorphic to an uncountable subspace of the Sorgenfrey line.

Combined with the result of Gruenhage, this allows to prove the following characterization of cosmic groups:

Theorem (OCA). A cometrizable topological group is cosmic if and only if it  has countable spread.

We recall that a topological space has a countable spread if it does not contain an uncountable discrete subspace. 
A topological space $X$ is cometrizable if it admits a weaker metrizable topology such that each point $x\in X$ has a (not necessarily open) neighborhood base consisting of metrically closed sets.
The following theorem shows that the above OCA-theorem is not true in ZFC.

Theorem (CH). Under CH there exists a cometrizable topological group which contains an uncountable subset of the Sorgenfrey line but is hereditarily Lindelof and hence has countable spread.

Proof. In this paper Michael constructs a CH-example of an uncountable subspace $X$ of the Sorgenfrey line whose countable power $X^\omega$ is hereditarily Lindelof. The space $X$ can be embedded into a cometrizable Boolean topological group $G$ so that $X$ generates $G$. Then $G$ is hereditarily Lindelof, being the countable union of continuous images of finite powers of $X$.
 A: Now I have a (relatively simple) ZFC-answer to the initial problem, see this preprint for more details.

Theorem 1. If a topological group $G$ contains a topological copy of the Sorgenfrey line, then it contains a discrete subspace of cardinality continuum.

Proof. Let $X$ be a subspace of $G$, homeomorphic to the Sorgenfrey line. Then $X$ contains a subset $Z\subset X$ of cardinality $|Z|=\mathfrak c$ and a function $f:Z\to X$ which is strictly decreasing with respect to a linear order $\le$ on $X$ such that for every $x\in X$ the set ${\uparrow}x:=\{y\in X:x\le y\}$ is a closed-and-open neighborhood of $x$ in $X$. Without loss of generality, the set $Z$ has no maximal element. 
For any point $x\in X$ choose a neighborhood $V_x\subset G$ of the unit $e$ of $G$ such that $X\cap (V_x^{-1}V_xx\cup xV_xV_x^{-1})\subset {\uparrow}x$.
The space $X$, being homeomorphic to the Sorgenfrey line is (hereditarily) separable and hence contains a countable dense subset $C$.
Then for every point $x\in X$ we can choose a point $u_x\in C\cap{\uparrow}x$ such that 
the order interval $[x,u_x):=\{y\in X:x\le y< u_x\}$ is a neighborhood of $x$ in $X$ such that $[x,u_x)\subset xV_{f(x)}$ if $x\in Z$ and $[x,u_x)\subset V_{f^{-1}(x)}x$ if $x\in f(Z)$. Since the continuum $\mathfrak c$ has uncountable cofinality, for some $c,d\in C$ the set $\{z\in Z:u_z=c,\; u_{f(z)}=d\}$ has cardinality $\mathfrak c$. Replacing $Z$ by this uncountable set, we can assume that $u_z=c$ and $u_{f(z)}=d$ for all $z\in Z$.
We claim that the subspace $D:=\{z\cdot f(z):z\in Z\}\subset G$ has cardinality $\mathfrak c$ and is discrete in $G$. For every $z\in Z$ consider the neighborhood $z(V_z\cap V_{f(z)})f(z)$ of the point $z\cdot f(z)$ in $G$. We claim that  $x\cdot f(x)\notin z(V_z\cap V_{f(z)})f(z)$ for any $x\in Z\setminus\{z\}$. To derive a contradiction, assume that $x\cdot f(x)\in z(V_z\cap V_{f(z)})f(z)$ for some $x\ne z$ in $Z$.
If $x>z$, then $x\in [z,u_z)\subset zV_{f(z)}$ and $$f(x)\in x^{-1}xf(x)\in x^{-1}zV_{f(z)}f(z)\subset V_{f(z)}^{-1}z^{-1}zV_{f(z)}f(z)=V_{f(z)}^{-1}V_{f(z)}f(z).$$Then $f(x)\in X\cap V_{f(z)}^{-1}V_{f(z)}f(z)\subset {\uparrow}f(z)$ and $f(x)\ge f(z)$, which is not possible as $x>z$ and $f$ is strictly decreasing.
If $z>x$, then $f(x)>f(z)$ and $f(x)\in [f(x),u_{f(x)})=[f(x),d)\subset [f(z),d)= [f(z),u_{f(z)})\subset V_{z}f(z)$ and then
$$x\in zV_zf(z)f(x)^{-1}\subset zV_zf(z)f(z)^{-1}V_z^{-1}=zV_zV_z^{-1}\subset{\uparrow}z,$$ which contradicts $z>x$. $\square$
By analogy we can prove the following more refined version of the above theorem.

Theorem 2. If a topological group $G$ contains a subspace $X$, homeomorphic to a subspace of the Sorgenfrey line, then $s(G)\ge s(X\times X)$.

Here $s(X)=\sup\{|D|:D$ is a discrete subspace in $X\}$ is the spread of a topological space $X$. 
To my big surprise I have discovered that for an uncountable subspace $X$ of the Sorgenfrey line the spread $s(X\times X)$ is not necessarily uncountable.

Theorem 3 (Michael). Under CH the Sorgenfrey line contains an uncountable subspace $X$ whose countable power $X^\omega$ is hereditarily Lindelof and hence has countable spread.

On the other hand, Theorem 4.8(c) of Todorcevic's book "Partition Problems in Topology" implies an opposite 

Theorem 4. Under OCA for any uncountable subspace $X$ of the Sorgenfrey line the square $X\times X$ has uncountable spread.

