Prove2Me

Corrected divergence is positive throughout the positive-wall region

Proved
BianchiIX.corrected_divergence_amplitude_pos

by trppppp · Nov 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

bianchi-ix-era-statisticsdynamical-systems

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

K=a2+b2+c2−2(ab+bc+ca),S=p2+s2,C=S+K.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−2a2+b2+c2+ab−2bc+ac,P=Kp-2a^2+b^2+c^2+ab-2bc+ac, Q=Ks+3(−b2+c2+ab−ac),Q=Ks+\sqrt{3}(-b^2+c^2+ab-ac), r1=−S+2p,r2=−S−p+3s,r3=−S−p−3s.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,r1a,r2b,r3c)(P,Q,r_1a,r_2b,r_3c).

Define H(a,b,c)=(abc)2/3H(a,b,c)=(abc)^{2/3} and

Δ(q,h)=2(q+4h)1+4h.\Delta(q,h)=\frac{2(q+4h)}{1+4h}.

Real powers and division have their total Lean meanings. If a,b,c>0a,b,c>0, then

Δ(K(a,b,c),H(a,b,c))>0.\Delta(K(a,b,c),H(a,b,c))>0.
Preamble
import Definitions.Def_BianchiIX_Algebra_Flow
import Definitions.Def_BianchiIX_Algebra_Flux
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.Pow.Deriv
import Mathlib.Tactic.FieldSimp

open BianchiIX
noncomputable section
Formal statement
theorem BianchiIX.corrected_divergence_amplitude_pos
    {a b c : ℝ} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
    0 < correctedDivergence (curvature a b c) (wallAmplitude a b c) := by sorry
Source
https://github.com/l46430640-del/ERA-STATISTICS-FORMAL/blob/d74c241819f896ab8d050b21ace80c8e90eabd9e/BianchiIX/Algebra/Flux.lean#L139-L145

View graph