Exact three-setting correlation bounds at fixed steering centre

Q: What does this paper prove about CJWR steering at a fixed steering-ellipsoid centre?

It determines the exact least upper bound G(c) of F₃² = ‖T‖²_F over all two-qubit states with centre length c: G(c) = 1 + (2−3c)²/(2−2c−c²) for 0 ≤ c ≤ 2/3 and G(c) = 1 for 2/3 < c ≤ 1. The bound is attained for c < 2/3, approached but never attained for 2/3 ≤ c < 1, and attained by a pure product state at c = 1; the maximum fully entangled fraction at fixed centre length is shown to be 1 − c/2.

Q: Does the threshold c < 2/3 characterize steerable two-qubit states?

No. It concerns only violation of the specific optimized three-setting CJWR inequality, F₃ > 1; general steerability under all measurements is outside the result, and no published conjecture is claimed to be resolved. Canonical filtering and the maximally obese state family are credited to the steering-ellipsoid literature (Milne et al.).

Dev D. Goyal

Exact three-setting correlation bounds at fixed steering centre

Dev D. Goyal · 2026 · Research preprint, not externally peer reviewed

Problem and result

Problem: Maximum CJWR three-setting steering value at fixed steering-ellipsoid centre (two qubits)
Status: Determined exactly
Result: For two-qubit states with steering-ellipsoid centre length c, the exact supremum of F₃² = ‖T‖²_F is 1 + (2−3c)²/(2−2c−c²) for c ≤ 2/3 and 1 for c > 2/3, so F₃ > 1 is possible exactly when c < 2/3.

Abstract

The exact least upper bound of the optimized three-setting squared correlation value is determined for every two-qubit steering-centre length. The threshold for a value greater than one is c < 2/3. Attainment, nonattainment and the singular marginal boundary are included.

Details

Year: 2026
Discipline: Mathematical physics
Area: Quantum information
Subject: Quantum information
Result type: Standalone theorem and reproducible proof package
Formal proof: Standalone Lean package
Family: steering-bounds
Keywords: quantum steering, steering ellipsoids, two-qubit states, CJWR steering inequality, fully entangled fraction, Pauli correlations

Statement and scope

Formal scope. Actual two-qubit density matrices, canonical filters, Pauli correlations, the exact least upper bound, attainment and nonattainment, and fully entangled fraction are formalized. The steering-ellipsoid and optimized CJWR measurement interpretations use cited external correspondences; general steerability is outside the result.

A Lean check establishes only the formal statement that is checked. It does not establish novelty, historical priority or a faithful transcription of an external source. Known gaps are listed in UNFINISHED.md; the authorship disclosure describes how the results were produced.

Manuscript

PDF on this site: manuscript.pdf 330 KB
PDF on GitHub: papers/physics/steering-bounds/paper/steering_bounds.pdf
LaTeX source: papers/physics/steering-bounds/paper/steering_bounds.tex

Formal proof

This result has a standalone Lean 4 package, separate from the shared library. Build it with the toolchain and instructions given in its README.

Proof package

papers/physics/steering-bounds/ 19 Lean files

Lakefile

papers/physics/steering-bounds/lakefile.lean

Toolchain

leanprover/lean4:v4.19.0

Library roots

Reproduce

The commands below are quoted from papers/physics/steering-bounds/README.md, which gives their context and working directory.

Reproduction

python3 scripts/verify.py --fetch-cache --serial

README: papers/physics/steering-bounds/README.md
Proof map: papers/physics/steering-bounds/PROOF_MAP.md
Authorship: papers/physics/steering-bounds/AUTHORSHIP.md
Repository guide: verification/README.md
Unfinished proofs: UNFINISHED.md

Source and prior work

Prior work. The fully-entangled-fraction companion bound is Conjecture 2 of Milne et al.; the Omega Institute's public repository records a claimed Lean proof committed on 8 October 2026 (issue #14206), and a CHSH bound at fixed centre (issue #16558). No priority is claimed for the companion bound. Priority and novelty record.

Source. Prior results and source-comparison limits are stated in the manuscript. Historical priority is not certified. The fully-entangled-fraction companion bound is Conjecture 2 of Milne et al.; the Omega Institute's public repository records a claimed Lean proof of it committed on 8 October 2026 (issue #14206), and no priority is claimed for it.

Questions and answers

What does this paper prove about CJWR steering at a fixed steering-ellipsoid centre?

It determines the exact least upper bound G(c) of F₃² = ‖T‖²_F over all two-qubit states with centre length c: G(c) = 1 + (2−3c)²/(2−2c−c²) for 0 ≤ c ≤ 2/3 and G(c) = 1 for 2/3 < c ≤ 1. The bound is attained for c < 2/3, approached but never attained for 2/3 ≤ c < 1, and attained by a pure product state at c = 1; the maximum fully entangled fraction at fixed centre length is shown to be 1 − c/2.

Does the threshold c < 2/3 characterize steerable two-qubit states?

No. It concerns only violation of the specific optimized three-setting CJWR inequality, F₃ > 1; general steerability under all measurements is outside the result, and no published conjecture is claimed to be resolved. Canonical filtering and the maximally obese state family are credited to the steering-ellipsoid literature (Milne et al.).

Is the proof formally verified?

The matrix statements are proved in Lean 4 for actual 4×4 density matrices: canonical filters, Pauli correlations, the exact least upper bound, attainment and nonattainment, and the fully entangled fraction. The identification with the physical steering-ellipsoid centre and with the optimized CJWR measurement expression uses cited external correspondences that are not formalized.

Was the fully-entangled-fraction bound known before?

The companion bound f(ρ) ≤ 1 − c/2 is Conjecture 2 of Milne, Jennings, Jevtic and Rudolph, and the Omega Institute's public repository records a claimed Lean proof of it committed on 8 October 2026 (issue #14206), before this result was first committed here on 29 October 2026. No priority is claimed for it. The exact three-setting supremum is not in that record.

Cite

Citation file papers/physics/steering-bounds/CITATION.bib. For the whole collection, use CITATION.cff or CITATION.bib.

@unpublished{Goyal2026SteeringBounds,
  author = {Goyal, Dev D.},
  title = {The exact {CJWR} three-setting steering envelope at fixed steering-ellipsoid centre},
  year = {2026},
  url = {https://github.com/dvgyl/math-and-theory/tree/main/papers/physics/steering-bounds},
  note = {Unpublished preprint. Fully autonomous agentic research. Historical priority remains provisional}
}