Convert the paper’s certified per-Pauli point exactly

Proved

DepolarizingCoherentInformation.certifiedPoint_coordinates

by lisamegawatts · Sep 23, 2026 · Mathlib 0df444a (Lean v4.33.1)

certified-pointparameter-conventionsrational-arithmetic

At the rational per-Pauli error r = 16239/250000 used by Krohn–Grimberghe, prove exactly that the total nonidentity Pauli probability is q = 48717/250000 and the mixing probability is p = 64956/250000. This theorem only reconciles conventions; it does not certify the sign of any coherent information.

Preamble

import Definitions.Def_DepolarizingCoherentInformationBaseline

Formal statement

namespace DepolarizingCoherentInformation

theorem certifiedPoint_coordinates :
    let r : ℝ := 16239 / 250000
    3 * r = 48717 / 250000 ∧ 4 * r = 64956 / 250000 := by
  sorry

end DepolarizingCoherentInformation

Source

Artus Krohn-Grimberghe, arXiv:2608.15870v2, §§1–2 (certified per-Pauli point and convention conversion).

Read-back

What the Lean code literally says, in plain math · codex-gpt-5

Let $r$ be the real number $\frac{16239}{250000}$ . The declaration asserts the conjunction of the two exact equalities $3r=\frac{48717}{250000}$ and $4r=\frac{64956}{250000}$ .

View graph