Small nonnegative coupling in the core

For real variables $p,s,a,b,c$, set

$$K=a^2+b^2+c^2-2(ab+bc+ca),\qquad S=p^2+s^2,\qquad C=S+K.$$

The shear components and wall rates are

$$P=Kp-2a^2+b^2+c^2+ab-2bc+ac,$$ $$Q=Ks+\sqrt{3}(-b^2+c^2+ab-ac),$$ $$r_1=-S+2p,\qquad r_2=-S-p+\sqrt{3}s,\qquad r_3=-S-p-\sqrt{3}s.$$

These functions define the normalized vacuum Bianchi IX vector field $(P,Q,r_1a,r_2b,r_3c)$. For $y=(m,u,v,w)\in\mathbb R^4$, define

$$K(u,v,w)=u^2+v^2+w^2-2(uv+vw+wu),\qquad \kappa=u(v+w-u),$$ $$F_m=-v^2+w^2+u(v-w)-m\kappa,\qquad F_u=\tfrac12(1-m^2-(v-w)^2+u^2)u,$$ $$F_v=(m-1-\kappa)v,\qquad F_w=(-m-1-\kappa)w,\qquad F=(F_m,F_u,F_v,F_w),$$

and $E(m,v)=(m-1)^2+v^2$.

For $x=(p,s,a,b,c)$, put

$$\psi(p,z)=\frac{\sqrt3\,z}{1+p},\qquad \Pi(x)=(\psi(p,s),\psi(p,a),\psi(p,b),\psi(p,c)).$$

For $y=(m,u,v,w)$, set $D(y)=3+m^2+K(u,v,w)$ and

$$\Xi_A(y)=\left(A-1,\frac{Am}{\sqrt3},\frac{Au}{\sqrt3}, \frac{Av}{\sqrt3},\frac{Aw}{\sqrt3}\right),\qquad \Xi(y)=\Xi_{6/D(y)}(y).$$

Write $N(x)=(P,Q,r_1a,r_2b,r_3c)$ for the normalized vector field and $\mathcal C(x)=C(p,s,a,b,c)$ for its constraint.

The normalized and projective state spaces are $\mathbb R^5$ and $\mathbb R^4$ with their finite-product norms. The maps $\Pi,\Xi,D,F$ act on these state spaces.

Define the core radius, angle, and clock factor by

$$r(m,v)=\sqrt{(m-1)^2+v^2},\qquad \theta(m,v)=\operatorname{arsinh}\frac{1-m}{v},\qquad d(r,u,w)=1-\frac{(u-w)^2}{r^2}.$$

For $y=(m,u,v,w)$, write $r_y=r(m,v)$, $\theta_y=\theta(m,v)$, and $d_y=d(r_y,u,w)$. All quotients use the total convention $x/0=0$. Assume $0\leq\varepsilon\leq1/100$, $r\varepsilon\leq1/1000$, $0\leq u,w\leq\varepsilon$, and $1\leq v\leq r$. Then

$$0\leq\kappa(u,v,w)\leq r\varepsilon+\varepsilon^2, \qquad \kappa(u,v,w)\leq\frac1{100}.$$

import Definitions.Def_BianchiIX_Algebra_Projective
import Mathlib.Analysis.Calculus.Deriv.Pow
import Mathlib.Analysis.Calculus.Deriv.Mul
import Mathlib.Analysis.Calculus.Deriv.Add
import Mathlib.Analysis.Real.Sqrt
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Ring
import Mathlib.Analysis.SpecialFunctions.Arsinh
import Mathlib.Analysis.SpecialFunctions.Sqrt
import Mathlib.Tactic.FieldSimp

noncomputable section
open BianchiIX

theorem BianchiIX.core_small_coupling {r m u v w : ℝ}
    (hm : 0 ≤ m ∧ m ≤ 1 / 100) (hrm : r * m ≤ 1 / 1000)
    (hu : 0 ≤ u ∧ u ≤ m) (hw : 0 ≤ w ∧ w ≤ m) (hv : 1 ≤ v ∧ v ≤ r) :
    0 ≤ coupling u v w ∧ coupling u v w ≤ r * m + m ^ 2 ∧ coupling u v w ≤ 1 / 100 := by sorry