A single inflection and the unique supporting tangent

Open

QAlgorithms.Papers.Independent.Intakethird100.P21.profile_curvature_and_tangency

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

prove2quantum

Let $d\ge3$ and let $q_d(F)=2(1-\gamma_d(F)^4-(d-1)\delta_d(F)^4)$ on $[1/d,1]$ , with $\gamma_d(F)=\sqrt{F/d}+\sqrt{(d-1)(1-F)/d}$ and $\delta_d(F)=\sqrt{F/d}-\sqrt{(1-F)/(d(d-1))}$ . This profile is twice differentiable in the interior and has a unique inflection point $r\in(1/d,1)$ : $q_d''$ is positive below $r$ , zero at $r$ , and negative above $r$ . The function $c_d=\sqrt{q_d}$ is concave on the closed interval. The equation

q_d'(a)=\frac{2(d-1)/d-q_d(a)}{1-a},\qquad a\in(1/d,1),

has the unique solution $a_d=4(d-1)/d^2$ , with

q_d(a_d)=\frac{2(2d-3)}{d(d-1)},\qquad q_d'(a_d)=\frac{2d}{d-1}.

The line $q_d(a_d)+q_d'(a_d)(F-a_d)$ lies below $q_d(F)$ throughout $[1/d,1]$ .

These properties identify the straight segment needed in the isotropic tangle convex envelope. The endpoint $a=1$ and the exceptional dimension $d=2$ are excluded from the tangency and inflection claims.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P21

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P21

open scoped Matrix ComplexConjugate

open Filter

open QAlgorithms

open QAlgorithms.Papers.Independent.Information100.P03
  (PureEnsemble convexRoof pureConcurrence concurrence SchmidtData schmidtVector)

attribute [local instance] Classical.propDecidable Classical.decEq

/-- PDF pp.12--13, (3.40) and tangent calculation: one interior inflection,
unique supporting tangent before F=1, and closed-domain concavity of c_d.
The restriction d>=3 excludes q_2''=8. -/
theorem profile_curvature_and_tangency (d : ℕ) (hd : 3 ≤ d) :
    (∀ x ∈ Set.Ioo (1 / (d : ℝ)) 1,
      DifferentiableAt ℝ (explicitQ d) x ∧ DifferentiableAt ℝ (deriv (explicitQ d)) x) ∧
    (∃ b ∈ Set.Ioo (1 / (d : ℝ)) 1,
      deriv (deriv (explicitQ d)) b = 0 ∧
      (∀ x ∈ Set.Ioo (1 / (d : ℝ)) b, 0 < deriv (deriv (explicitQ d)) x) ∧
      (∀ x ∈ Set.Ioo b 1, deriv (deriv (explicitQ d)) x < 0)) ∧
    ConcaveOn ℝ (Set.Icc (1 / (d : ℝ)) 1) (rawC d) ∧
    explicitQ d (tangentPoint d) = 2 * (2*(d : ℝ)-3) / ((d : ℝ)*((d : ℝ)-1)) ∧
    deriv (explicitQ d) (tangentPoint d) = 2*d / ((d : ℝ)-1) ∧
    (∀ x ∈ Set.Ioo (1 / (d : ℝ)) 1,
      (deriv (explicitQ d) x =
        (2*((d : ℝ)-1)/d - explicitQ d x) / (1-x) ↔ x = tangentPoint d)) ∧
    (∀ F ∈ Set.Icc (1 / (d : ℝ)) 1,
      explicitQ d (tangentPoint d) + (2*d/((d : ℝ)-1))*(F-tangentPoint d) ≤
        explicitQ d F) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P21

end

Source

I-concurrence and tangle for isotropic states, arXiv:quant-ph/0208002v1, PDF p. 13, §3.4.3, (3.40) and tangent calculation: curvature and unique supporting tangent

Read-back

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

For every natural number $d\ge3$ , define

a_d(x)=\sqrt{\frac xd}+\sqrt{\frac{(d-1)(1-x)}d}, \quad b_d(x)=\sqrt{\frac xd}-\sqrt{\frac{1-x}{d(d-1)}}, \quad Q_d(x)=2\bigl(1-a_d(x)^4-(d-1)b_d(x)^4\bigr), \quad t_d=\frac{4(d-1)}{d^2}.

Also let $P_d(x)$ be the infimum of $2(1-\sum_i\mu_i^2)$ over $\mu_i\ge0$ , $\sum_i\mu_i=1$ , and $\sum_i\sqrt{\mu_i}=\sqrt{dx}$ , with $d$ coordinates, and set $r_d(x)=\sqrt{P_d(x)}$ . At every $x\in(1/d,1)$ , both $Q_d$ and its derivative function are differentiable. There exists $b\in(1/d,1)$ with $Q_d''(b)=0$ , $Q_d''(x)>0$ for every $x\in(1/d,b)$ , and $Q_d''(x)<0$ for every $x\in(b,1)$ . The function $r_d$ is concave on $[1/d,1]$ , and

Q_d(t_d)=\frac{2(2d-3)}{d(d-1)}, \qquad Q_d'(t_d)=\frac{2d}{d-1}.

For every $x\in(1/d,1)$ , the equality $Q_d'(x)=[2(d-1)/d-Q_d(x)]/(1-x)$ holds if and only if $x=t_d$ . Finally, for every $F\in[1/d,1]$ , including its endpoints,

Q_d(t_d)+\frac{2d}{d-1}(F-t_d)\le Q_d(F).

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