Range of the square-root rescaling

Proved

QAlgorithms.Papers.Independent.Intakethird100.P13.sqrtRescaling_range

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

prove2quantum

Let $\gamma,s\in[0,1]$ and assume $1-\gamma s>0$ , the domain of the displayed real quotient. Then

0\le\sqrt{\frac{1-\gamma}{1-\gamma s}}\le1.

This is the regular transverse rescaling factor of the positive-translation decomposition. No value is assigned at the singular pair $(1,1)$ .

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P13

Formal statement

noncomputable section

open scoped BigOperators Matrix ComplexConjugate ComplexOrder

namespace QAlgorithms.Papers.Independent.Intakethird100.P13

attribute [local instance] Classical.propDecidable Classical.decEq

/-- arXiv:1706.05384v2 PDF p.12, Corollary 21; the same regular domain correction. -/
theorem sqrtRescaling_range (gamma s30 : ℝ) (hg0 : 0 ≤ gamma) (hg1 : gamma ≤ 1)
    (hs0 : 0 ≤ s30) (hs1 : s30 ≤ 1) (hden : 0 < 1-gamma*s30) :
    Real.sqrt (rescaling gamma s30) ∈ Set.Icc (0 : ℝ) 1 := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P13

end

Source

Simulation of non-Pauli Channels, arXiv:1706.05384v2, PDF p. 12, Corollary 21

Read-back

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

For all real $\gamma,s_{30}$ satisfying $0\le\gamma\le1$ , $0\le s_{30}\le1$ , and $0<1-\gamma s_{30}$ , the real square root satisfies

0\le\sqrt{\frac{1-\gamma}{1-\gamma s_{30}}}\le1.

Both endpoints of this interval are permitted; the denominator must be strictly positive, so the pair $(\gamma,s_{30})=(1,1)$ is excluded.

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