FormalConjectures/Kourovka/21_149.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

5 declarations, 2 contain sorry, 0 declared as axioms

Conjecture 21.149

by A. V. Zenkov

The problem is due to V. M. Kopytov and N. Ya. Medvedev. Its original form asked for an order automorphism of a Dlab group that is not inner (kourovka_21_149.variants.not_inner). After that form was solved, the problem was revised to the stronger question below [vDJMM, Appendix A]. [GYZ] answered the revised question for order-preserving embeddings and rank-one slope groups.

The Notebook does not define Dlab groups. We follow [Dl] and [GYZ]: the Dlab groups with slope group $H$ are four groups of order automorphisms of $I = [0, 1]$ and two groups of order automorphisms of the extended real line $\overline{\mathbb{R}}$. All six are viewed as subgroups of the order automorphisms of $\mathbb{R}$ (IsDlabGroup).

References:

Imports (1)
  1. def Kourovka.«21.149».IsLocallyRightLinear An order automorphism $f$ of $\mathbb{R}$ is locally right $H$-linear if every point has a right neighbourhood on which $f$ is affine with slope in $H \le \mathbb{R}_{>0}$ line 55 source

    Source documentation

    An order automorphism $f$ of $\mathbb{R}$ is locally right $H$-linear if every point has a right neighbourhood on which $f$ is affine with slope in $H \le \mathbb{R}_{>0}$.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Subgroup, Units, NNReal, OrderIso, Real

    Proof uses: Exists, And, GT.gt, OfNat.ofNat, Membership.mem, LT.lt, HAdd.hAdd, Eq, HMul.hMul, HSub.hSub

    23 instances, coercions and auxiliary constants left out.

    def IsLocallyRightLinear (H : Subgroup NNRealˣ) (f : ℝ ≃o ℝ) : Prop :=
…
  2. def Kourovka.«21.149».IsDlabGroup $A$ is one of the six Dlab groups with slope group $H$ line 71 source

    Source documentation

    $A$ is one of the six Dlab groups with slope group $H$. Each consists of the locally right $H$-linear order automorphisms $f$ with a condition at the ends.

    • Four act on $I = [0, 1]$. An order automorphism of $I$ is identified with its extension to $\mathbb{R}$ by the identity, so $f$ fixes every point outside $(0, 1)$. The four groups are $D_H(I)$ ($f$ is also the identity near $0$ and near $1$), $D_{H*}(I)$ (near $0$), $D_{*H}(I)$ (near $1$) and $\overline{D}_H(I)$ (no further condition).
    • Two act on the extended real line $\overline{\mathbb{R}}$, whose order automorphisms are those of $\mathbb{R}$. They are $D_H$ ($f$ is the identity near $-\infty$ and near $+\infty$) and $D_{H*}$ (near $-\infty$).

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Subgroup, Units, NNReal, OrderIso, Real, LE.le

    Proof uses: Or, Iff, Membership.mem, And, Kourovka.«21.149».IsLocallyRightLinear, Not, Set, Set.Ioo, OfNat.ofNat, Eq, Filter.Eventually, nhds, Filter.atBot, Filter.atTop

    23 instances, coercions and auxiliary constants left out.

    def IsDlabGroup (H : Subgroup NNRealˣ) (A : Subgroup (ℝ ≃o ℝ)) : Prop :=
…
  3. def Kourovka.«21.149».DlabLt Dlab's order on a group $G$ of order automorphisms of $\mathbb{R}$: $f < g$ if $f(x) < g(x)$ at some point $x$ and every point $y$ with $g(y) < f(y)$ lies to the right of $x$ line 88 source

    Source documentation

    Dlab's order on a group $G$ of order automorphisms of $\mathbb{R}$: $f < g$ if $f(x) < g(x)$ at some point $x$ and every point $y$ with $g(y) < f(y)$ lies to the right of $x$. For elements of a Dlab group, this says that $f$ is below $g$ just after the point where they start to differ.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Subgroup, OrderIso, Real, LE.le, Subtype, Membership.mem

    Proof uses: Exists, And, LT.lt

    12 instances, coercions and auxiliary constants left out.

    def DlabLt {G : Subgroup (ℝ ≃o ℝ)} (f g : G) : Prop :=
…
  4. theorem Kourovka.«21.149».kourovka_21_149 sorry line 104 source

    depends on sorry what this means

    Statement uses: Iff, True, Exists, Subgroup, Units, NNReal, OrderIso, Real, LE.le, And, Kourovka.«21.149».IsDlabGroup, MulEquiv, Subtype, Membership.mem, Kourovka.«21.149».DlabLt, Not, MonoidHom, Function.Injective, Eq, HMul.hMul and 1 more

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat

    39 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  5. theorem Kourovka.«21.149».kourovka_21_149.variants.not_inner sorry line 123 source

    depends on sorry what this means

    Statement uses: Iff, True, Exists, Subgroup, Units, NNReal, OrderIso, Real, LE.le, And, Kourovka.«21.149».IsDlabGroup, MulEquiv, Subtype, Membership.mem, Kourovka.«21.149».DlabLt, Not, Eq, HMul.hMul, Inv.inv

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat

    27 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.