Range of the regular rescaling quotient

Proved

QAlgorithms.Papers.Independent.Intakethird100.P13.rescaling_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\frac{1-\gamma}{1-\gamma s}\le1.

In the decomposition proof $s=S_{30}\ge0$ . The singular pair $(1,1)$ is handled by the physical endpoint characterization and is not assigned a quotient value.

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, Lemma 20.
Domain correction: the printed proof uses a quotient at the singular pair (1,1);
strict positivity states its ordinary real-quotient domain. -/
theorem rescaling_range (gamma s30 : ℝ) (hg0 : 0 ≤ gamma) (hg1 : gamma ≤ 1)
    (hs0 : 0 ≤ s30) (hs1 : s30 ≤ 1) (hden : 0 < 1-gamma*s30) :
    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, Lemma 20

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 quotient satisfies

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

The interval bounds are non-strict; the strictly positive denominator hypothesis excludes the pair $(\gamma,s_{30})=(1,1)$ , while allowing $\gamma=1$ whenever $s_{30}<1$ .

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