35.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

86 declarations, 23 contain sorry, 0 declared as axioms

Open Quantum Problem 35: existence of absolutely maximally entangled pure states

Problem: For which numbers of parties $n$ and local dimensions $d$ does there exist a pure absolutely maximally entangled state $\psi$?

A pure state $\psi$ on $n$ parties of local dimension $d$ is called absolutely maximally entangled (AME) if, for every subset of at most half of the parties, the corresponding reduced density matrix is maximally mixed.

References:

Open Quantum Problems, Problem 35: https://oqp.iqoqi.oeaw.ac.at/existence-of-absolutely-maximally-entangled-pure-states
Formal Conjectures issue #3452: https://github.com/google-deepmind/formal-conjectures/issues/3452
W. Helwig, W. Cui, A. Riera, J. I. Latorre, and H.-K. Lo, Absolute Maximal Entanglement and Quantum Secret Sharing, Phys. Rev. A 86, 052335 (2012), arXiv:1204.2289.
D. Goyeneche, D. Alsina, J. I. Latorre, A. Riera, and K. Życzkowski, Absolutely Maximally Entangled states, combinatorial designs and multi-unitary matrices, Phys. Rev. A 92, 032316 (2015), arXiv:1506.08857.
A. Higuchi and A. Sudbery, How entangled can two couples get?, Phys. Lett. A 273, 213-217 (2000), arXiv:quant-ph/0005013.
A. J. Scott, Multipartite entanglement, quantum-error-correcting codes, and entangling power of quantum evolutions, Phys. Rev. A 69, 052330 (2004), arXiv:quant-ph/0310137.
F. Huber, O. Gühne, and J. Siewert, Absolutely maximally entangled states of seven qubits do not exist, Phys. Rev. Lett. 118, 200502 (2017), arXiv:1608.06228.
F. Huber and M. Grassl, Quantum Codes of Maximal Distance and Highly Entangled Subspaces, Quantum 4, 284 (2020), arXiv:1907.07733.
S. A. Rather, A. Burchardt, W. Bruzda, G. Rajchel-Mieldzioć, A. Lakshminarayan, and K. Życzkowski, Thirty-six entangled officers of Euler: Quantum solution to a classically impossible problem, Phys. Rev. Lett. 128, 080507 (2022), arXiv:2104.05122.
G. Rajchel-Mieldzioć, R. Bistroń, A. Rico, A. Lakshminarayan, and K. Życzkowski, Absolutely maximally entangled pure states of multipartite quantum systems, arXiv:2508.04777 (2025).
S. Bevins and Y. Bidav, Symmetry-guided constructions of absolutely maximally entangled states in five open cases, arXiv:2608.05781 (2026).
F. Shi, X. Zhang, Q. Zhao, and L. Li, Complete Existence Classification of Seven-Partite Absolutely Maximally Entangled States, arXiv:2608.01011 (2026).

This file formalizes the problem of determining for which pairs $(n,d)$ there exists an absolutely maximally entangled pure state $\mathrm{AME}(n,d)$.

We represent an $n$-partite state of local dimension $d$ by the finite-dimensional Hilbert space EuclideanSpace ℂ (Config n d), whose coordinates in the computational basis are amplitudes. The helper mkStateVector turns an amplitude function into such a state, and normalization is imposed explicitly via IsNormalized, i.e. via the ambient $L^2$ norm.

The main reusable lemma is reducedDensityFirst_of_completion: if a state is a uniform superposition over the graph of an injective completion function completion : Config m d → Config (n - m) d, then the reduced state on the first $m$ parties is maximally mixed.

As demonstration, we show that the Bell states with $n=2$ and GHZ states with $n=3$ are AME states, and the GHZ state with $n=4$ is not an AME state.

Imports (1)

FormalConjecturesUtil

Imported by 1 file

FormalConjectures/Subsets/FC100SolvedSet1.lean

abbrev OpenQuantumProblem35.Config A computational-basis configuration of $n$ parties with local dimension $d$ line 94 source
Source documentation
A computational-basis configuration of $n$ parties with local dimension $d$.

no axioms what this means
Statement uses: Nat
Proof uses: Fin
```
abbrev Config (n d : ℕ) := Fin n → Fin d
```
abbrev OpenQuantumProblem35.StateVector A state vector in the computational basis, viewed as a finite-dimensional Hilbert space line 97 source
Source documentation
A state vector in the computational basis, viewed as a finite-dimensional Hilbert space.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: EuclideanSpace, Complex, OpenQuantumProblem35.Config
```
abbrev StateVector (n d : ℕ) := EuclideanSpace ℂ (Config n d)
```
Mentions: OpenQuantumProblem35.Config
abbrev OpenQuantumProblem35.mkStateVector Build a state vector from its computational-basis amplitudes line 100 source
Source documentation
Build a state vector from its computational-basis amplitudes.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, OpenQuantumProblem35.Config, Complex, OpenQuantumProblem35.StateVector
Proof uses: WithLp.toLp, OfNat.ofNat, ENNReal
5 instances, coercions and auxiliary constants left out.
```
abbrev mkStateVector {n d : ℕ} (ψ : Config n d → ℂ) : StateVector n d :=
…
```
Mentions: OpenQuantumProblem35.Config, OpenQuantumProblem35.StateVector
instance OpenQuantumProblem35.(instance at line 104) line 104 source
Source documentation
A state vector can be evaluated on a computational-basis configuration to read its amplitude.
```
instance {n d : ℕ} : CoeFun (StateVector n d) (fun _ => Config n d → ℂ) where
…
```
Mentions: OpenQuantumProblem35.StateVector, OpenQuantumProblem35.Config
lemma OpenQuantumProblem35.mkStateVector_apply A state built from amplitudes has those amplitudes as its coordinates line 109 source
Source documentation
A state built from amplitudes has those amplitudes as its coordinates.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, OpenQuantumProblem35.Config, Complex, Eq, WithLp.ofLp, OfNat.ofNat, ENNReal, OpenQuantumProblem35.mkStateVector
Proof uses: rfl
10 instances, coercions and auxiliary constants left out.
```
lemma mkStateVector_apply {n d : ℕ} (ψ : Config n d → ℂ) (x : Config n d) :
    mkStateVector ψ x = ψ x := rfl
```
Mentions: OpenQuantumProblem35.Config, OpenQuantumProblem35.mkStateVector
def OpenQuantumProblem35.IsNormalized A state vector is normalized if it has $L^2$ norm $1$ line 113 source
Source documentation
A state vector is normalized if it has $L^2$ norm $1$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, OpenQuantumProblem35.StateVector
Proof uses: Eq, Real, Norm.norm, OfNat.ofNat, ENNReal, OpenQuantumProblem35.Config, Complex, Fin
12 instances, coercions and auxiliary constants left out.
```
def IsNormalized {n d : ℕ} (ψ : StateVector n d) : Prop :=
…
```
Mentions: OpenQuantumProblem35.StateVector
lemma OpenQuantumProblem35.isNormalized_iff_norm_sq_eq_one A state is normalized iff its squared $L^2$ norm is $1$ line 118 source
Source documentation
A state is normalized iff its squared $L^2$ norm is $1$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, OpenQuantumProblem35.StateVector, Iff, OpenQuantumProblem35.IsNormalized, Eq, Real, HPow.hPow, Norm.norm, OfNat.ofNat, ENNReal, OpenQuantumProblem35.Config, Complex, Fin
Proof uses: Iff.intro, Trans.trans, Eq.mpr, id, congrArg, Eq.mp, OpenQuantumProblem35.IsNormalized.eq_1, Eq.refl, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_pow, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Mathlib.Meta.NormNum.one_natPow, Or, Neg.neg, Eq.trans, one_pow, Iff.mp, sq_eq_sq_iff_eq_or_eq_neg, LE.le and 49 more
103 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
lemma isNormalized_iff_norm_sq_eq_one {n d : ℕ} (ψ : StateVector n d) :
    IsNormalized ψ ↔ ‖ψ‖ ^ 2 = 1 := by
…
```
Mentions: OpenQuantumProblem35.StateVector, OpenQuantumProblem35.IsNormalized
def OpenQuantumProblem35.permuteConfig Permute the parties of a configuration line 138 source
Source documentation
Permute the parties of a configuration.

standard axioms: Quot.sound what this means
Statement uses: Nat, Equiv.Perm, Fin, OpenQuantumProblem35.Config
3 instances, coercions and auxiliary constants left out.
```
def permuteConfig {n d : ℕ} (π : Equiv.Perm (Fin n)) (x : Config n d) : Config n d :=
…
```
Mentions: OpenQuantumProblem35.Config
theorem OpenQuantumProblem35.permuteConfig_refl The identity permutation leaves a configuration unchanged line 143 source
Source documentation
The identity permutation leaves a configuration unchanged.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, OpenQuantumProblem35.Config, Eq, OpenQuantumProblem35.permuteConfig, Equiv.refl, Fin
Proof uses: funext, Fin.ext, of_eq_true, eq_self
1 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem permuteConfig_refl {n d : ℕ} (x : Config n d) :
    permuteConfig (Equiv.refl (Fin n)) x = x := by
…
```
Mentions: OpenQuantumProblem35.Config, OpenQuantumProblem35.permuteConfig
def OpenQuantumProblem35.permuteState Permute the parties of a state vector line 149 source
Source documentation
Permute the parties of a state vector.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, OpenQuantumProblem35.StateVector
Proof uses: OpenQuantumProblem35.mkStateVector, OpenQuantumProblem35.Config, WithLp.ofLp, OfNat.ofNat, ENNReal, Complex, OpenQuantumProblem35.permuteConfig
5 instances, coercions and auxiliary constants left out.
```
def permuteState {n d : ℕ} (π : Equiv.Perm (Fin n)) (ψ : StateVector n d) : StateVector n d :=
…
```
Mentions: OpenQuantumProblem35.StateVector
lemma OpenQuantumProblem35.permuteState_apply Evaluating a permuted state vector reads the amplitude at the permuted configuration line 154 source
Source documentation
Evaluating a permuted state vector reads the amplitude at the permuted configuration.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, OpenQuantumProblem35.StateVector, OpenQuantumProblem35.Config, Eq, Complex, WithLp.ofLp, OfNat.ofNat, ENNReal, OpenQuantumProblem35.permuteState, OpenQuantumProblem35.permuteConfig
Proof uses: Eq.mpr, OpenQuantumProblem35.mkStateVector, id, congrArg, OpenQuantumProblem35.permuteState.eq_1, OpenQuantumProblem35.mkStateVector_apply, Eq.refl
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma permuteState_apply {n d : ℕ} (π : Equiv.Perm (Fin n)) (ψ : StateVector n d) (x : Config n d) :
    permuteState π ψ x = ψ (permuteConfig π x) := by
…
```
Mentions: OpenQuantumProblem35.StateVector, OpenQuantumProblem35.Config, OpenQuantumProblem35.permuteState, OpenQuantumProblem35.permuteConfig
theorem OpenQuantumProblem35.permuteState_refl The identity permutation leaves a state vector unchanged line 160 source
Source documentation
The identity permutation leaves a state vector unchanged.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, OpenQuantumProblem35.StateVector, Eq, OpenQuantumProblem35.permuteState, Equiv.refl, Fin
Proof uses: PiLp.ext, OfNat.ofNat, ENNReal, OpenQuantumProblem35.Config, Complex, of_eq_true, WithLp.ofLp, Eq.trans, True, congrFun', congrArg, OpenQuantumProblem35.permuteConfig, OpenQuantumProblem35.permuteState_apply, OpenQuantumProblem35.permuteConfig_refl, eq_self
5 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem permuteState_refl {n d : ℕ} (ψ : StateVector n d) :
    permuteState (Equiv.refl (Fin n)) ψ = ψ := by
…
```
Mentions: OpenQuantumProblem35.StateVector, OpenQuantumProblem35.permuteState
def OpenQuantumProblem35.combineFirst Merge a configuration on the first $m$ parties and a configuration on the remaining $n-m$ parties into a configuration on all $n$ parties line 169 source
Source documentation
Merge a configuration on the first $m$ parties and a configuration on the remaining $n-m$ parties into a configuration on all $n$ parties.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, LE.le, OpenQuantumProblem35.Config, HSub.hSub
Proof uses: Fin, dite, LT.lt, Fin.mk, Not
10 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def combineFirst {n d : ℕ} (m : ℕ) (hm : m ≤ n)
    (x : Config m d) (y : Config (n - m) d) : Config n d :=
…
```
Mentions: OpenQuantumProblem35.Config
def OpenQuantumProblem35.leftIndex The embedding of the first $m$ indices into $\mathrm{Fin}\, n$ line 180 source
Source documentation
The embedding of the first $m$ indices into $\mathrm{Fin}\, n$.

no axioms what this means
Statement uses: Nat, LE.le, Fin
Proof uses: Fin.mk
4 instances, coercions and auxiliary constants left out.
```
def leftIndex {m n : ℕ} (hm : m ≤ n) (i : Fin m) : Fin n :=
…
```
def OpenQuantumProblem35.rightIndex The embedding of the last $n-m$ indices into $\mathrm{Fin}\, n$ line 184 source
Source documentation
The embedding of the last $n-m$ indices into $\mathrm{Fin}\, n$.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, LE.le, Fin, HSub.hSub
Proof uses: Fin.mk, HAdd.hAdd
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
def rightIndex {m n : ℕ} (hm : m ≤ n) (i : Fin (n - m)) : Fin n :=
…
```
lemma OpenQuantumProblem35.combineFirst_leftIndex Combining and then restricting to the left block recovers the left input line 189 source
Source documentation
Combining and then restricting to the left block recovers the left input.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, LE.le, OpenQuantumProblem35.Config, HSub.hSub, Fin, Eq, OpenQuantumProblem35.combineFirst, OpenQuantumProblem35.leftIndex
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, dite_cond_eq_true, LT.lt, Fin.mk, Not, eq_true, Fin.isLt, eq_self
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma combineFirst_leftIndex {n d m : ℕ} (hm : m ≤ n)
    (x : Config m d) (y : Config (n - m) d) (i : Fin m) :
    combineFirst (n := n) (d := d) m hm x y (leftIndex hm i) = x i := by
…
```
Mentions: OpenQuantumProblem35.Config, OpenQuantumProblem35.combineFirst, OpenQuantumProblem35.leftIndex
lemma OpenQuantumProblem35.combineFirst_rightIndex Combining and then restricting to the right block recovers the right input line 196 source
Source documentation
Combining and then restricting to the right block recovers the right input.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OpenQuantumProblem35.Config, HSub.hSub, Fin, Eq, OpenQuantumProblem35.combineFirst, OpenQuantumProblem35.rightIndex
Proof uses: Not, LT.lt, HAdd.hAdd, of_eq_true, Eq.trans, True, congrFun', congrArg, dite, Fin.mk, of_eq_false, eq_false, dite_cond_eq_false, Fin.mk.congr_simp, add_tsub_cancel_left, eq_self
29 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma combineFirst_rightIndex {n d m : ℕ} (hm : m ≤ n)
    (x : Config m d) (y : Config (n - m) d) (i : Fin (n - m)) :
    combineFirst (n := n) (d := d) m hm x y (rightIndex hm i) = y i := by
…
```
Mentions: OpenQuantumProblem35.Config, OpenQuantumProblem35.combineFirst, OpenQuantumProblem35.rightIndex
def OpenQuantumProblem35.reducedDensityFirst The reduced density matrix obtained by tracing out the last $n-m$ parties line 210 source
Source documentation
The reduced density matrix obtained by tracing out the last $n-m$ parties.
The subsystem is always the first $m$ parties; different subsystems are handled by first permuting the parties.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OpenQuantumProblem35.StateVector, Matrix, OpenQuantumProblem35.Config, Complex
Proof uses: Finset.sum, HSub.hSub, Finset.univ, Fin, HMul.hMul, OpenQuantumProblem35.combineFirst, WithLp.ofLp, OfNat.ofNat, ENNReal, Star.star
25 instances, coercions and auxiliary constants left out.
```
noncomputable def reducedDensityFirst {n d : ℕ} (m : ℕ) (hm : m ≤ n) (ψ : StateVector n d) :
    Matrix (Config m d) (Config m d) ℂ :=
…
```
Mentions: OpenQuantumProblem35.StateVector, OpenQuantumProblem35.Config
def OpenQuantumProblem35.maximallyMixed The maximally mixed state on $m$ parties line 218 source
Source documentation
The maximally mixed state on $m$ parties.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Matrix, OpenQuantumProblem35.Config, Complex
Proof uses: HSMul.hSMul, Inv.inv, Fintype.card, Fin, OfNat.ofNat
15 instances, coercions and auxiliary constants left out.
```
noncomputable def maximallyMixed (m d : ℕ) :
    Matrix (Config m d) (Config m d) ℂ :=
…
```
Mentions: OpenQuantumProblem35.Config
def OpenQuantumProblem35.HasMaximallyMixedFirstReduction A state has maximally mixed reduction on the first $m$ parties line 224 source
Source documentation
A state has maximally mixed reduction on the first $m$ parties.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OpenQuantumProblem35.StateVector
Proof uses: Eq, Matrix, OpenQuantumProblem35.Config, Complex, OpenQuantumProblem35.reducedDensityFirst, OpenQuantumProblem35.maximallyMixed
2 instances, coercions and auxiliary constants left out.
```
def HasMaximallyMixedFirstReduction {n d : ℕ} (m : ℕ) (hm : m ≤ n)
    (ψ : StateVector n d) : Prop :=
…
```
Mentions: OpenQuantumProblem35.StateVector
def OpenQuantumProblem35.IsAME A state $\psi$ is absolutely maximally entangled line 241 source
Source documentation
A state $\psi$ is absolutely maximally entangled.
Standard AME definitions quantify over all subsets $A \subseteq \mathrm{Fin}\, n$ with $|A| \le \lfloor n/2 \rfloor$ and require that the reduction on $A$ be maximally mixed. For pure states it is enough to check subsets of size exactly $\lfloor n/2 \rfloor$; see the references of Helwig--Cui--Riera--Latorre--Lo (2012) and Goyeneche--Alsina--Latorre--Riera--Życzkowski (2015). In this file, a subsystem of that size is encoded by first permuting the chosen parties to the front and then tracing out the remaining parties.
We also require $\psi$ to be normalized explicitly.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, OpenQuantumProblem35.StateVector
Proof uses: And, OpenQuantumProblem35.IsNormalized, Equiv.Perm, Fin, OpenQuantumProblem35.HasMaximallyMixedFirstReduction, HDiv.hDiv, OfNat.ofNat, OpenQuantumProblem35.permuteState
4 instances, coercions and auxiliary constants left out.
```
def IsAME {n d : ℕ} (ψ : StateVector n d) : Prop :=
…
```
Mentions: OpenQuantumProblem35.StateVector
def OpenQuantumProblem35.ExistsAME Existence of an $\mathrm{AME}(n,d)$ state line 248 source
Source documentation
Existence of an $\mathrm{AME}(n,d)$ state.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Exists, OpenQuantumProblem35.StateVector, OpenQuantumProblem35.IsAME
```
def ExistsAME (n d : ℕ) : Prop :=
…
```
theorem OpenQuantumProblem35.not_existsAME_zero_dim No absolutely maximally entangled state exists in local dimension $0$ once $n \ge 1$ line 253 source
Source documentation
No absolutely maximally entangled state exists in local dimension $0$ once $n \ge 1$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Not, OpenQuantumProblem35.ExistsAME
Proof uses: OpenQuantumProblem35.StateVector, OpenQuantumProblem35.IsAME, False, Fin, Fin.mk, IsEmpty, OpenQuantumProblem35.Config, IsEmpty.mk, Fin.elim0, Eq, ENNReal, Complex, Subsingleton.elim, Real, Eq.mpr, id, False.elim, Eq.mp, OpenQuantumProblem35.IsNormalized, Eq.trans and 17 more
53 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
theorem not_existsAME_zero_dim {n : ℕ} (hn : 1 ≤ n) : ¬ ExistsAME n 0 := by
…
```
Mentions: OpenQuantumProblem35.ExistsAME
lemma OpenQuantumProblem35.card_config The number of computational-basis configurations on $m$ parties of local dimension $d$ is $d^m$ line 265 source
Source documentation
The number of computational-basis configurations on $m$ parties of local dimension $d$ is $d^m$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Fintype.card, OpenQuantumProblem35.Config, Fin, HPow.hPow
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Finset.prod, Finset.univ, Fintype.card_pi, Finset.card, Finset.prod_congr, Eq.refl, Finset, Membership.mem, Fintype.card_fin, Finset.prod_const, eq_self
18 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma card_config (m d : ℕ) : Fintype.card (Config m d) = d ^ m := by
…
```
Mentions: OpenQuantumProblem35.Config
lemma OpenQuantumProblem35.maximallyMixed_apply The matrix entries of the maximally mixed state are diagonal and equal to the inverse subsystem dimension line 270 source
Source documentation
The matrix entries of the maximally mixed state are diagonal and equal to the inverse subsystem dimension.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, OpenQuantumProblem35.Config, Eq, Complex, OpenQuantumProblem35.maximallyMixed, ite, Fin, Inv.inv, Fintype.card, OfNat.ofNat
Proof uses: dite, of_eq_true, Eq.trans, HPow.hPow, True, congr, congrArg, HSMul.hSMul, Matrix, congrFun', Finset.prod, Finset.univ, Fintype.card_pi, Finset.card, Finset.prod_congr, Eq.refl, Finset, Membership.mem, Fintype.card_fin, Finset.prod_const and 12 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma maximallyMixed_apply {m d : ℕ} (x y : Config m d) :
    maximallyMixed m d x y =
      if x = y then ((Fintype.card (Config m d) : ℂ)⁻¹) else 0 := by
…
```
Mentions: OpenQuantumProblem35.Config, OpenQuantumProblem35.maximallyMixed
def OpenQuantumProblem35.uniformCoeff The common amplitude of the Bell and GHZ witnesses line 281 source
Source documentation
The common amplitude of the Bell and GHZ witnesses.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Complex
Proof uses: Real.sqrt, Inv.inv, Real
4 instances, coercions and auxiliary constants left out.
```
noncomputable def uniformCoeff (d : ℕ) : ℂ :=
…
```
def OpenQuantumProblem35.IsConstantConfig A configuration is constant if all coordinates agree line 285 source
Source documentation
A configuration is constant if all coordinates agree.

no axioms what this means
Statement uses: Nat, OpenQuantumProblem35.Config
Proof uses: Fin, Eq

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
def IsConstantConfig {n d : ℕ} (x : Config n d) : Prop :=
…
```
Mentions: OpenQuantumProblem35.Config
instance OpenQuantumProblem35.(instance at line 288) line 288 source
def OpenQuantumProblem35.constantConfig The constant configuration with value $a$ line 294 source
Source documentation
The constant configuration with value $a$.

no axioms what this means
Statement uses: Nat, Fin, OpenQuantumProblem35.Config
```
def constantConfig {m d : ℕ} (a : Fin d) : Config m d :=
…
```
Mentions: OpenQuantumProblem35.Config
theorem OpenQuantumProblem35.isConstantConfig_constantConfig Every constant configuration is constant line 299 source
Source documentation
Every constant configuration is constant.

no axioms what this means
Statement uses: Nat, Fin, OpenQuantumProblem35.IsConstantConfig, OpenQuantumProblem35.constantConfig
Proof uses: Eq.refl

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem isConstantConfig_constantConfig {m d : ℕ} (a : Fin d) :
    IsConstantConfig (constantConfig (m := m) (d := d) a) := by
…
```
Mentions: OpenQuantumProblem35.IsConstantConfig, OpenQuantumProblem35.constantConfig
theorem OpenQuantumProblem35.not_isConstantConfig_example A simple binary two-party configuration with different entries is not constant line 306 source
Source documentation
A simple binary two-party configuration with different entries is not constant.

standard axioms: Quot.sound, propext what this means
Statement uses: Not, OpenQuantumProblem35.IsConstantConfig, OfNat.ofNat, Nat, Fin, ite, Eq
Proof uses: False.elim, False, Eq.mp, Eq.trans, congr, congrArg, ite_cond_eq_true, eq_self, ite_cond_eq_false
22 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem not_isConstantConfig_example :
    ¬ IsConstantConfig (fun i : Fin 2 => if i = 0 then (0 : Fin 2) else 1) := by
…
```
Mentions: OpenQuantumProblem35.IsConstantConfig
def OpenQuantumProblem35.diagonalState The diagonal $n$-party state: the uniform superposition over constant computational-basis strings line 313 source
Source documentation
The diagonal $n$-party state: the uniform superposition over constant computational-basis strings.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, OpenQuantumProblem35.StateVector
Proof uses: OpenQuantumProblem35.mkStateVector, OpenQuantumProblem35.Config, ite, Complex, OpenQuantumProblem35.IsConstantConfig, OpenQuantumProblem35.uniformCoeff, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.
```
noncomputable def diagonalState (n d : ℕ) : StateVector n d :=
…
```
Mentions: OpenQuantumProblem35.StateVector
lemma OpenQuantumProblem35.diagonalState_apply Evaluating the diagonal state returns the uniform coefficient on constant strings and 0 otherwise line 318 source
Source documentation
Evaluating the diagonal state returns the uniform coefficient on constant strings and 0 otherwise.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, OpenQuantumProblem35.Config, Eq, Complex, WithLp.ofLp, OfNat.ofNat, ENNReal, OpenQuantumProblem35.diagonalState, ite, OpenQuantumProblem35.IsConstantConfig, OpenQuantumProblem35.uniformCoeff
Proof uses: Eq.mpr, OpenQuantumProblem35.mkStateVector, id, congrArg, OpenQuantumProblem35.StateVector, OpenQuantumProblem35.diagonalState.eq_1, OpenQuantumProblem35.mkStateVector_apply, Eq.refl
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma diagonalState_apply {n d : ℕ} (x : Config n d) :
    diagonalState n d x = if IsConstantConfig x then uniformCoeff d else 0 := by
…
```
Mentions: OpenQuantumProblem35.Config, OpenQuantumProblem35.diagonalState, OpenQuantumProblem35.IsConstantConfig, OpenQuantumProblem35.uniformCoeff
abbrev OpenQuantumProblem35.bellState The standard $d$-dimensional Bell state line 323 source
Source documentation
The standard $d$-dimensional Bell state.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, OpenQuantumProblem35.StateVector, OfNat.ofNat
Proof uses: OpenQuantumProblem35.diagonalState
2 instances, coercions and auxiliary constants left out.
```
noncomputable abbrev bellState (d : ℕ) : StateVector 2 d :=
…
```
Mentions: OpenQuantumProblem35.StateVector
abbrev OpenQuantumProblem35.ghzState The standard $d$-dimensional GHZ state on $3$ parties line 327 source
Source documentation
The standard $d$-dimensional GHZ state on $3$ parties.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, OpenQuantumProblem35.StateVector, OfNat.ofNat
Proof uses: OpenQuantumProblem35.diagonalState
2 instances, coercions and auxiliary constants left out.
```
noncomputable abbrev ghzState (d : ℕ) : StateVector 3 d :=
…
```
Mentions: OpenQuantumProblem35.StateVector
abbrev OpenQuantumProblem35.ghzState4 The standard $d$-dimensional GHZ state on $4$ parties line 331 source
Source documentation
The standard $d$-dimensional GHZ state on $4$ parties.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, OpenQuantumProblem35.StateVector, OfNat.ofNat
Proof uses: OpenQuantumProblem35.diagonalState
2 instances, coercions and auxiliary constants left out.
```
noncomputable abbrev ghzState4 (d : ℕ) : StateVector 4 d :=
…
```
Mentions: OpenQuantumProblem35.StateVector
def OpenQuantumProblem35.constantCompletion The completion function for constant-support states reduced to one party line 335 source
Source documentation
The completion function for constant-support states reduced to one party.

standard axioms: propext what this means
Statement uses: Nat, OpenQuantumProblem35.Config, OfNat.ofNat, HSub.hSub
Proof uses: OpenQuantumProblem35.constantConfig, Fin
8 instances, coercions and auxiliary constants left out.
```
def constantCompletion {n d : ℕ} (x : Config 1 d) : Config (n - 1) d :=
…
```
Mentions: OpenQuantumProblem35.Config
lemma OpenQuantumProblem35.constantConfig_injective On a nonempty index type, different constants give different constant configurations line 340 source
Source documentation
On a nonempty index type, different constants give different constant configurations.

no axioms what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Function.Injective, Fin, OpenQuantumProblem35.Config, OpenQuantumProblem35.constantConfig
Proof uses: Fin.mk, Iff.mp, Nat.succ, LT.lt, Nat.succ_le_iff, Eq, congrArg
5 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma constantConfig_injective {n d : ℕ} (hn : 1 ≤ n) :
    Function.Injective (@constantConfig n d) := by
…
```
Mentions: OpenQuantumProblem35.constantConfig
lemma OpenQuantumProblem35.isConstantConfig_iff_exists_constantConfig A configuration on a nonempty index type is constant iff it is equal to some constant configuration line 349 source
Source documentation
A configuration on a nonempty index type is constant iff it is equal to some constant configuration.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, OpenQuantumProblem35.Config, Iff, OpenQuantumProblem35.IsConstantConfig, Exists, Fin, Eq, OpenQuantumProblem35.constantConfig
Proof uses: Fin.mk, Iff.mp, Nat.succ, LT.lt, Nat.succ_le_iff, Iff.intro, Exists.intro, funext, id, of_eq_true, eq_self, Eq.symm
7 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma isConstantConfig_iff_exists_constantConfig {n d : ℕ} (hn : 1 ≤ n)
    (x : Config n d) :
    IsConstantConfig x ↔ ∃ a : Fin d, x = constantConfig (m := n) (d := d) a := by
…
```
Mentions: OpenQuantumProblem35.Config, OpenQuantumProblem35.IsConstantConfig, OpenQuantumProblem35.constantConfig
lemma OpenQuantumProblem35.uniformCoeff_norm_sq The squared norm of the uniform coefficient is the inverse local dimension line 363 source
Source documentation
The squared norm of the uniform coefficient is the inverse local dimension.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Real, HPow.hPow, Norm.norm, Complex, OpenQuantumProblem35.uniformCoeff, OfNat.ofNat, Inv.inv
Proof uses: LE.le, inv_nonneg_of_nonneg, Nat.cast_nonneg', Eq.mpr, HMul.hMul, Real.sqrt, id, congrFun', congrArg, Eq.trans, Real.sqrt_inv, Complex.ofReal_inv, norm_inv, Complex.norm_real, abs_of_nonneg, Real.sqrt_nonneg, pow_two, Eq.mp, Real.sq_sqrt
55 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma uniformCoeff_norm_sq (d : ℕ) :
    ‖uniformCoeff d‖ ^ 2 = ((d : ℝ)⁻¹) := by
…
```
Mentions: OpenQuantumProblem35.uniformCoeff
lemma OpenQuantumProblem35.uniformCoeff_mul_star The squared norm of the uniform coefficient is the inverse local dimension line 372 source
Source documentation
The squared norm of the uniform coefficient is the inverse local dimension.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Complex, HMul.hMul, OpenQuantumProblem35.uniformCoeff, Star.star, Inv.inv
Proof uses: Trans.trans, Real, HPow.hPow, Norm.norm, OfNat.ofNat, Eq.mpr, RingHom, starRingEnd, id, congrArg, Complex.ofReal_pow, RCLike.mul_conj, OpenQuantumProblem35.uniformCoeff_norm_sq, Eq.refl, of_eq_true, Eq.trans, True, congrFun', Complex.ofReal_inv, eq_self
53 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma uniformCoeff_mul_star (d : ℕ) :
    uniformCoeff d * star (uniformCoeff d) = ((d : ℂ)⁻¹) := by
…
```
Mentions: OpenQuantumProblem35.uniformCoeff
lemma OpenQuantumProblem35.diagonalState_isNormalized For $n \ge 1$ and $d \ge 1$, the diagonal state is normalized line 384 source
Source documentation
For $n \ge 1$ and $d \ge 1$, the diagonal state is normalized.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, OpenQuantumProblem35.IsNormalized, OpenQuantumProblem35.diagonalState
Proof uses: Finset, OpenQuantumProblem35.Config, Finset.filter, OpenQuantumProblem35.IsConstantConfig, Finset.univ, Fin, Eq, Finset.image, OpenQuantumProblem35.constantConfig, Finset.ext, of_eq_true, Iff, Membership.mem, Eq.trans, Exists, True, congr, congrArg, And, propext and 54 more
87 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
```
lemma diagonalState_isNormalized {n d : ℕ} (hn : 1 ≤ n) (hd : 1 ≤ d) :
    IsNormalized (diagonalState n d) := by
…
```
Mentions: OpenQuantumProblem35.IsNormalized, OpenQuantumProblem35.diagonalState
lemma OpenQuantumProblem35.isConstantConfig_permute_iff Permuting the parties preserves the property of being a constant configuration line 431 source
Source documentation
Permuting the parties preserves the property of being a constant configuration.

standard axioms: Quot.sound what this means
Statement uses: Nat, Equiv.Perm, Fin, OpenQuantumProblem35.Config, Iff, OpenQuantumProblem35.IsConstantConfig, OpenQuantumProblem35.permuteConfig
Proof uses: Iff.intro, Eq, Equiv, Equiv.symm, Eq.mp, congr, congrArg, Equiv.apply_symm_apply, id
3 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma isConstantConfig_permute_iff {n d : ℕ} (π : Equiv.Perm (Fin n)) (x : Config n d) :
    IsConstantConfig (permuteConfig π x) ↔ IsConstantConfig x := by
…
```
Mentions: OpenQuantumProblem35.Config, OpenQuantumProblem35.IsConstantConfig, OpenQuantumProblem35.permuteConfig
lemma OpenQuantumProblem35.diagonalState_permute The diagonal state is invariant under permutations of the parties line 442 source
Source documentation
The diagonal state is invariant under permutations of the parties.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Equiv.Perm, Fin, Eq, OpenQuantumProblem35.StateVector, OpenQuantumProblem35.permuteState, OpenQuantumProblem35.diagonalState
Proof uses: PiLp.ext, OfNat.ofNat, ENNReal, OpenQuantumProblem35.Config, Complex, dite, WithLp.ofLp, OpenQuantumProblem35.IsConstantConfig, OpenQuantumProblem35.permuteConfig, Iff.mpr, OpenQuantumProblem35.isConstantConfig_permute_iff, of_eq_true, Eq.trans, OpenQuantumProblem35.uniformCoeff, True, congr, congrArg, OpenQuantumProblem35.permuteState_apply, ite, OpenQuantumProblem35.diagonalState_apply and 7 more
8 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma diagonalState_permute (n d : ℕ) (π : Equiv.Perm (Fin n)) :
    permuteState π (diagonalState n d) = diagonalState n d := by
…
```
Mentions: OpenQuantumProblem35.permuteState, OpenQuantumProblem35.diagonalState
lemma OpenQuantumProblem35.constantCompletion_eq_iff A tail configuration equals the constant completion of $x$ iff all of its entries agree with the unique entry of $x$ line 455 source
Source documentation
A tail configuration equals the constant completion of $x$ iff all of its entries agree with the unique entry of $x$.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, OpenQuantumProblem35.Config, OfNat.ofNat, HSub.hSub, Iff, Eq, OpenQuantumProblem35.constantCompletion, Fin
Proof uses: Iff.intro, congrArg, funext
10 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma constantCompletion_eq_iff {n d : ℕ} (x : Config 1 d) (z : Config (n - 1) d) :
    z = constantCompletion (n := n) (d := d) x ↔ ∀ i, z i = x 0 := by
…
```
Mentions: OpenQuantumProblem35.Config, OpenQuantumProblem35.constantCompletion
lemma OpenQuantumProblem35.eq_leftIndex_zero_or_eq_rightIndex Every index in $\mathrm{Fin}\, n$ is either the unique left index or a right index when the left block has size $1$ line 466 source
Source documentation
Every index in $\mathrm{Fin}\, n$ is either the unique left index or a right index when the left block has size $1$.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Fin, Or, Eq, OpenQuantumProblem35.leftIndex, Exists, HSub.hSub, OpenQuantumProblem35.rightIndex
Proof uses: dite, Or.inl, Fin.eq_of_val_eq, Eq.mpr, id, congrArg, Fin.mk, LT.lt, Fin.val_eq_zero, Fin.mk.congr_simp, Not, Or.inr, Exists.intro, Decidable.byContradiction, HAdd.hAdd
22 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma eq_leftIndex_zero_or_eq_rightIndex {n : ℕ} (hn : 1 ≤ n) (i : Fin n) :
    i = leftIndex (m := 1) (n := n) hn 0 ∨
…
```
Mentions: OpenQuantumProblem35.leftIndex
lemma OpenQuantumProblem35.constantCompletion_injective The completion map for constant configurations is injective once $n \ge 2$ line 481 source
Source documentation
The completion map for constant configurations is injective once $n \ge 2$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Function.Injective, OpenQuantumProblem35.Config, HSub.hSub, OpenQuantumProblem35.constantCompletion
Proof uses: Eq, funext, Fin, List, List.Mem, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, List.cons, List.Mem.head, Fin.mk, Nat.le_refl, List.nil, LT.lt, Decidable.byContradiction, Not, congrArg and 8 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma constantCompletion_injective {n d : ℕ} (hn : 2 ≤ n) :
    Function.Injective (@constantCompletion n d) := by
…
```
Mentions: OpenQuantumProblem35.constantCompletion
lemma OpenQuantumProblem35.isConstantConfig_combineFirst_one_iff A configuration obtained by combining one entry with a tail is constant iff the tail is the constant completion of that entry line 496 source
Source documentation
A configuration obtained by combining one entry with a tail is constant iff the tail is the constant completion of that entry.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, OpenQuantumProblem35.Config, HSub.hSub, Iff, OpenQuantumProblem35.IsConstantConfig, OpenQuantumProblem35.combineFirst, Eq, OpenQuantumProblem35.constantCompletion
Proof uses: Eq.mpr, Fin, id, congrArg, propext, OpenQuantumProblem35.constantCompletion_eq_iff, Iff.intro, OpenQuantumProblem35.rightIndex, OpenQuantumProblem35.leftIndex, Eq.mp, congr, OpenQuantumProblem35.combineFirst_rightIndex, OpenQuantumProblem35.combineFirst_leftIndex, Exists, Or, OpenQuantumProblem35.eq_leftIndex_zero_or_eq_rightIndex, of_eq_true, Eq.trans, True, eq_self and 1 more
13 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
lemma isConstantConfig_combineFirst_one_iff {n d : ℕ} (hn : 1 ≤ n)
    (x : Config 1 d) (z : Config (n - 1) d) :
    IsConstantConfig (combineFirst (n := n) (d := d) 1 hn x z) ↔
…
```
Mentions: OpenQuantumProblem35.Config, OpenQuantumProblem35.IsConstantConfig, OpenQuantumProblem35.combineFirst
lemma OpenQuantumProblem35.diagonalState_combineFirst_one The diagonal state on a split configuration is nonzero exactly on the graph of the constant completion map line 518 source
Source documentation
The diagonal state on a split configuration is nonzero exactly on the graph of the constant completion map.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, OpenQuantumProblem35.Config, HSub.hSub, Eq, Complex, OpenQuantumProblem35.combineFirst, WithLp.ofLp, ENNReal, OpenQuantumProblem35.diagonalState, ite, OpenQuantumProblem35.constantCompletion, Fin, OpenQuantumProblem35.uniformCoeff
Proof uses: dite, OpenQuantumProblem35.IsConstantConfig, Iff.mpr, OpenQuantumProblem35.isConstantConfig_combineFirst_one_iff, rfl, Eq.mpr, id, congrArg, OpenQuantumProblem35.diagonalState_apply, if_pos, Eq.refl, Eq.symm, Not, Iff.mp, if_neg
30 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma diagonalState_combineFirst_one {n d : ℕ} (hn : 1 ≤ n)
    (x : Config 1 d) (z : Config (n - 1) d) :
    diagonalState n d (combineFirst (n := n) (d := d) 1 hn x z) =
…
```
Mentions: OpenQuantumProblem35.Config, OpenQuantumProblem35.diagonalState, OpenQuantumProblem35.combineFirst
lemma OpenQuantumProblem35.reducedDensityFirst_of_completion A uniform superposition over the graph of an injective completion map has reduced density matrix $(c\overline c) I$ on the first subsystem line 539 source
Source documentation
A uniform superposition over the graph of an injective completion map has reduced density matrix $(c\overline c) I$ on the first subsystem.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OpenQuantumProblem35.StateVector, OpenQuantumProblem35.Config, HSub.hSub, Complex, Eq, OpenQuantumProblem35.combineFirst, WithLp.ofLp, OfNat.ofNat, ENNReal, ite, Fin, Function.Injective, Matrix, OpenQuantumProblem35.reducedDensityFirst, HSMul.hSMul, HMul.hMul, Star.star
Proof uses: Matrix.ext, dite, Eq.mpr, Finset.sum, Finset.univ, id, congrArg, OpenQuantumProblem35.reducedDensityFirst.eq_1, Finset.sum_eq_single, Membership.mem, Finset, Ne, of_eq_true, Eq.trans, True, congrFun', congr, ite_cond_eq_false, eq_false, star_zero and 19 more
111 instances, coercions and auxiliary constants left out.

Tactic trace: 36 steps
Open to load the checked before-and-after goal states.
```
lemma reducedDensityFirst_of_completion
    {n d m : ℕ} (hm : m ≤ n)
    (ψ : StateVector n d)
    (completion : Config m d → Config (n - m) d)
    (coeff : ℂ)
    (hψ : ∀ x z,
      ψ (combineFirst (n := n) (d := d) m hm x z) = if z = completion x then coeff else 0)
…
```
Mentions: OpenQuantumProblem35.StateVector, OpenQuantumProblem35.Config, OpenQuantumProblem35.combineFirst
lemma OpenQuantumProblem35.hasMaximallyMixedFirstReduction_of_completion The completion criterion gives a maximally mixed reduced state once the coefficient has the correct squared norm line 587 source
Source documentation
The completion criterion gives a maximally mixed reduced state once the coefficient has the correct squared norm.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OpenQuantumProblem35.StateVector, OpenQuantumProblem35.Config, HSub.hSub, Complex, Eq, OpenQuantumProblem35.combineFirst, WithLp.ofLp, OfNat.ofNat, ENNReal, ite, Fin, Function.Injective, HMul.hMul, Star.star, Inv.inv, Fintype.card, OpenQuantumProblem35.HasMaximallyMixedFirstReduction
Proof uses: Eq.mpr, Matrix, OpenQuantumProblem35.reducedDensityFirst, OpenQuantumProblem35.maximallyMixed, id, congrArg, OpenQuantumProblem35.HasMaximallyMixedFirstReduction.eq_1, HSMul.hSMul, OpenQuantumProblem35.reducedDensityFirst_of_completion, OpenQuantumProblem35.maximallyMixed.eq_1, Eq.refl
64 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma hasMaximallyMixedFirstReduction_of_completion
    {n d m : ℕ} (hm : m ≤ n)
    (ψ : StateVector n d)
    (completion : Config m d → Config (n - m) d)
    (coeff : ℂ)
    (hψ : ∀ x z,
      ψ (combineFirst (n := n) (d := d) m hm x z) = if z = completion x then coeff else 0)
…
```
Mentions: OpenQuantumProblem35.StateVector, OpenQuantumProblem35.Config, OpenQuantumProblem35.combineFirst
lemma OpenQuantumProblem35.diagonalState_hasMaximallyMixedFirstReduction_one The diagonal state has maximally mixed one-party reductions once $n \ge 2$ line 603 source
Source documentation
The diagonal state has maximally mixed one-party reductions once $n \ge 2$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, OpenQuantumProblem35.HasMaximallyMixedFirstReduction, OpenQuantumProblem35.diagonalState
Proof uses: OpenQuantumProblem35.hasMaximallyMixedFirstReduction_of_completion, Decidable.byContradiction, Not, OpenQuantumProblem35.constantCompletion, OpenQuantumProblem35.uniformCoeff, OpenQuantumProblem35.Config, HSub.hSub, OpenQuantumProblem35.diagonalState_combineFirst_one, OpenQuantumProblem35.constantCompletion_injective, Eq.mpr, Eq, Complex, HMul.hMul, Star.star, Inv.inv, Fintype.card, Fin, RingHom, starRingEnd, id and 17 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma diagonalState_hasMaximallyMixedFirstReduction_one {n d : ℕ} (hn : 2 ≤ n) :
    HasMaximallyMixedFirstReduction (n := n) (d := d) 1 (by omega) (diagonalState n d) := by
…
```
Mentions: OpenQuantumProblem35.HasMaximallyMixedFirstReduction, OpenQuantumProblem35.diagonalState
lemma OpenQuantumProblem35.diagonalState_isAME_of_div_two_eq_one If $\lfloor n/2 \rfloor = 1$, then the diagonal state is $\mathrm{AME}(n,d)$ for every $d \ge 2$ line 619 source
Source documentation
If $\lfloor n/2 \rfloor = 1$, then the diagonal state is $\mathrm{AME}(n,d)$ for every $d \ge 2$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Eq, HDiv.hDiv, OpenQuantumProblem35.IsAME, OpenQuantumProblem35.diagonalState
Proof uses: And.intro, OpenQuantumProblem35.IsNormalized, Equiv.Perm, Fin, OpenQuantumProblem35.HasMaximallyMixedFirstReduction, OpenQuantumProblem35.permuteState, Decidable.byContradiction, Not, OpenQuantumProblem35.diagonalState_isNormalized, Eq.mpr, id, congrArg, OpenQuantumProblem35.StateVector, OpenQuantumProblem35.diagonalState_permute, OpenQuantumProblem35.HasMaximallyMixedFirstReduction.congr_simp, Eq.refl, OpenQuantumProblem35.diagonalState_hasMaximallyMixedFirstReduction_one
13 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma diagonalState_isAME_of_div_two_eq_one {n d : ℕ}
    (hn : 2 ≤ n) (hhalf : n / 2 = 1) (hd : 2 ≤ d) :
    IsAME (n := n) (d := d) (diagonalState n d) := by
…
```
Mentions: OpenQuantumProblem35.IsAME, OpenQuantumProblem35.diagonalState
lemma OpenQuantumProblem35.bellState_isAME The standard Bell state is $\mathrm{AME}(2,d)$ for every physical local dimension $d \ge 2$ line 632 source
Source documentation
The standard Bell state is $\mathrm{AME}(2,d)$ for every physical local dimension $d \ge 2$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, OpenQuantumProblem35.IsAME, OpenQuantumProblem35.bellState
Proof uses: id, OpenQuantumProblem35.diagonalState_isAME_of_div_two_eq_one, of_decide_eq_true, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, Mathlib.Meta.NormNum.isNat_eq_true, HDiv.hDiv, Mathlib.Meta.NormNum.isNat_natDiv, Mathlib.Meta.NormNum.isNat_ofNat
8 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma bellState_isAME {d : ℕ} (hd : 2 ≤ d) :
    IsAME (n := 2) (d := d) (bellState d) := by
…
```
Mentions: OpenQuantumProblem35.IsAME, OpenQuantumProblem35.bellState
lemma OpenQuantumProblem35.ghzState_isAME The standard $3$-party GHZ state is $\mathrm{AME}(3,d)$ for every physical local dimension $d \ge 2$ line 639 source
Source documentation
The standard $3$-party GHZ state is $\mathrm{AME}(3,d)$ for every physical local dimension $d \ge 2$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, OpenQuantumProblem35.IsAME, OpenQuantumProblem35.ghzState
Proof uses: id, OpenQuantumProblem35.diagonalState_isAME_of_div_two_eq_one, of_decide_eq_true, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, Mathlib.Meta.NormNum.isNat_eq_true, HDiv.hDiv, Mathlib.Meta.NormNum.isNat_natDiv, Mathlib.Meta.NormNum.isNat_ofNat
8 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma ghzState_isAME {d : ℕ} (hd : 2 ≤ d) :
    IsAME (n := 3) (d := d) (ghzState d) := by
…
```
Mentions: OpenQuantumProblem35.IsAME, OpenQuantumProblem35.ghzState
theorem OpenQuantumProblem35.ame_2_exists The Bell state witnesses the existence of $\mathrm{AME}(2,d)$ for every local dimension $d \ge 2$ line 646 source
Source documentation
The Bell state witnesses the existence of $\mathrm{AME}(2,d)$ for every local dimension $d \ge 2$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, OpenQuantumProblem35.ExistsAME
Proof uses: Exists.intro, OpenQuantumProblem35.StateVector, OpenQuantumProblem35.IsAME, OpenQuantumProblem35.bellState, OpenQuantumProblem35.bellState_isAME
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem ame_2_exists {d : ℕ} (hd : 2 ≤ d) : ExistsAME 2 d := by
…
```
Mentions: OpenQuantumProblem35.ExistsAME
theorem OpenQuantumProblem35.ame_3_exists The $3$-party GHZ state witnesses the existence of $\mathrm{AME}(3,d)$ for every local dimension $d \ge 2$ line 651 source
Source documentation
The $3$-party GHZ state witnesses the existence of $\mathrm{AME}(3,d)$ for every local dimension $d \ge 2$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, OpenQuantumProblem35.ExistsAME
Proof uses: Exists.intro, OpenQuantumProblem35.StateVector, OpenQuantumProblem35.IsAME, OpenQuantumProblem35.ghzState, OpenQuantumProblem35.ghzState_isAME
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem ame_3_exists {d : ℕ} (hd : 2 ≤ d) : ExistsAME 3 d := by
…
```
Mentions: OpenQuantumProblem35.ExistsAME
lemma OpenQuantumProblem35.diagonalState_combineFirst_two_of_ne On $4$ parties, the diagonal state vanishes on any split configuration whose first two entries are different line 658 source
Source documentation
On $4$ parties, the diagonal state vanishes on any split configuration whose first two entries are different.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, OpenQuantumProblem35.Config, OfNat.ofNat, Ne, Fin, Eq, Complex, OpenQuantumProblem35.combineFirst, WithLp.ofLp, ENNReal, OpenQuantumProblem35.diagonalState
Proof uses: Not, OpenQuantumProblem35.IsConstantConfig, of_decide_eq_true, LE.le, id, Bool, Decidable.decide, Bool.true, Eq.refl, Eq.mp, OpenQuantumProblem35.leftIndex, congr, congrArg, OpenQuantumProblem35.combineFirst_leftIndex, of_eq_true, Eq.trans, True, congrFun', ite, OpenQuantumProblem35.uniformCoeff and 4 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma diagonalState_combineFirst_two_of_ne {d : ℕ} {x z : Config 2 d}
    (h : x 0 ≠ x 1) :
    diagonalState 4 d (combineFirst (n := 4) (d := d) 2 (by decide) x z) = 0 := by
…
```
Mentions: OpenQuantumProblem35.Config, OpenQuantumProblem35.diagonalState, OpenQuantumProblem35.combineFirst
lemma OpenQuantumProblem35.ghzState4_not_ame Sanity check: the standard GHZ family on $4$ parties is not absolutely maximally entangled for any local dimension $d \ge 2$ line 672 source
Source documentation
Sanity check: the standard GHZ family on $4$ parties is not absolutely maximally entangled for any local dimension $d \ge 2$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Not, OpenQuantumProblem35.IsAME, OpenQuantumProblem35.ghzState4
Proof uses: OpenQuantumProblem35.diagonalState, Fin, Fin.mk, Decidable.byContradiction, LT.lt, OpenQuantumProblem35.Config, ite, Eq, Ne, Eq.mpr, False, id, False.elim, Eq.mp, Eq.trans, congr, congrArg, congrFun', funext, ite_congr and 57 more
105 instances, coercions and auxiliary constants left out.

Tactic trace: 37 steps
Open to load the checked before-and-after goal states.
```
lemma ghzState4_not_ame {d : ℕ} (hd : 2 ≤ d) :
    ¬ IsAME (n := 4) (d := d) (ghzState4 d) := by
…
```
Mentions: OpenQuantumProblem35.IsAME, OpenQuantumProblem35.ghzState4
theorem OpenQuantumProblem35.ame_2_2_exists Source-backed benchmark statement: the Bell state witnesses the existence of an $\mathrm{AME}(2,2)$ state line 716 source
Source documentation
Source-backed benchmark statement: the Bell state witnesses the existence of an $\mathrm{AME}(2,2)$ state.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: OpenQuantumProblem35.ExistsAME, OfNat.ofNat, Nat
Proof uses: OpenQuantumProblem35.ame_2_exists, of_decide_eq_true, LE.le, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl
4 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem ame_2_2_exists : ExistsAME 2 2 := by
…
```
Mentions: OpenQuantumProblem35.ExistsAME
theorem OpenQuantumProblem35.ame_3_2_exists Source-backed benchmark statement: the three-qubit GHZ state witnesses the existence of an $\mathrm{AME}(3,2)$ state line 721 source
Source documentation
Source-backed benchmark statement: the three-qubit GHZ state witnesses the existence of an $\mathrm{AME}(3,2)$ state.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: OpenQuantumProblem35.ExistsAME, OfNat.ofNat, Nat
Proof uses: OpenQuantumProblem35.ame_3_exists, of_decide_eq_true, LE.le, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl
4 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem ame_3_2_exists : ExistsAME 3 2 := by
…
```
Mentions: OpenQuantumProblem35.ExistsAME
theorem OpenQuantumProblem35.ame_5_2_exists sorry line 727 source
depends on sorry what this means
Statement uses: OpenQuantumProblem35.ExistsAME, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem OpenQuantumProblem35.ame_6_2_exists sorry line 733 source
depends on sorry what this means
Statement uses: OpenQuantumProblem35.ExistsAME, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem OpenQuantumProblem35.ame_4_2_not_exists Source-backed benchmark statement: no $\mathrm{AME}(4,2)$ state exists; see Higuchi--Sudbery (2000) and the OQP page sorry line 738 source
Source documentation
Source-backed benchmark statement: no $\mathrm{AME}(4,2)$ state exists; see Higuchi--Sudbery (2000) and the OQP page.

depends on sorry what this means
Statement uses: Not, OpenQuantumProblem35.ExistsAME, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem ame_4_2_not_exists : ¬ ExistsAME 4 2 := by
…
```
Mentions: OpenQuantumProblem35.ExistsAME
theorem OpenQuantumProblem35.ame_7_2_not_exists Source-backed benchmark statement: no $\mathrm{AME}(7,2)$ state exists; see Huber--Gühne--Siewert (2017) and the OQP page sorry line 743 source
Source documentation
Source-backed benchmark statement: no $\mathrm{AME}(7,2)$ state exists; see Huber--Gühne--Siewert (2017) and the OQP page.

depends on sorry what this means
Statement uses: Not, OpenQuantumProblem35.ExistsAME, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem ame_7_2_not_exists : ¬ ExistsAME 7 2 := by
…
```
Mentions: OpenQuantumProblem35.ExistsAME
theorem OpenQuantumProblem35.ame_7_exists_iff For a physical local dimension $d \ge 2$, a seven-party AME state exists exactly when $d \ge 3$ sorry line 753 source
Source documentation
For a physical local dimension $d \ge 2$, a seven-party AME state exists exactly when $d \ge 3$. The hypothesis excludes the degenerate dimension $d = 1$, for which the unique computational-basis state is AME under the definitions of this file. Shi--Zhang--Zhao--Li (2026) construct cyclic quadratic-phase states in every odd dimension and a coupled binary--odd-dimensional state in every dimension congruent to 2 modulo 4; together with power-of-two constructions and the product property, this covers every d ≥ 3.

depends on sorry what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Iff, OpenQuantumProblem35.ExistsAME
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem ame_7_exists_iff (d : ℕ) (hd : 2 ≤ d) : ExistsAME 7 d ↔ 3 ≤ d := by
…
```
Mentions: OpenQuantumProblem35.ExistsAME
theorem OpenQuantumProblem35.ame_4_3_exists sorry line 759 source
depends on sorry what this means
Statement uses: OpenQuantumProblem35.ExistsAME, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem OpenQuantumProblem35.ame_4_6_exists Source-backed benchmark statement: an $\mathrm{AME}(4,6)$ state exists; see Rather et al sorry line 764 source
Source documentation
Source-backed benchmark statement: an $\mathrm{AME}(4,6)$ state exists; see Rather et al. (2022).

depends on sorry what this means
Statement uses: OpenQuantumProblem35.ExistsAME, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem ame_4_6_exists : ExistsAME 4 6 := by
…
```
Mentions: OpenQuantumProblem35.ExistsAME
theorem OpenQuantumProblem35.ame_7_6_open An $\mathrm{AME}(7,6)$ state exists, by the complete seven-party classification of Shi--Zhang--Zhao--Li (2026) line 772 source
Source documentation
An $\mathrm{AME}(7,6)$ state exists, by the complete seven-party classification of Shi--Zhang--Zhao--Li (2026).

depends on sorry what this means
Statement uses: Iff, True, OpenQuantumProblem35.ExistsAME, OfNat.ofNat, Nat
Proof uses: Iff.intro, Iff.mpr, LE.le, OpenQuantumProblem35.ame_7_exists_iff, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, of_eq_true, implies_true
10 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
theorem ame_7_6_open :
    answer(True) ↔ ExistsAME 7 6 := by
…
```
Mentions: OpenQuantumProblem35.ExistsAME
theorem OpenQuantumProblem35.ame_7_10_open An $\mathrm{AME}(7,10)$ state exists, by the complete seven-party classification of Shi--Zhang--Zhao--Li (2026) line 782 source
Source documentation
An $\mathrm{AME}(7,10)$ state exists, by the complete seven-party classification of Shi--Zhang--Zhao--Li (2026).

depends on sorry what this means
Statement uses: Iff, True, OpenQuantumProblem35.ExistsAME, OfNat.ofNat, Nat
Proof uses: Iff.intro, Iff.mpr, LE.le, OpenQuantumProblem35.ame_7_exists_iff, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, of_eq_true, implies_true
10 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
theorem ame_7_10_open :
    answer(True) ↔ ExistsAME 7 10 := by
…
```
Mentions: OpenQuantumProblem35.ExistsAME
theorem OpenQuantumProblem35.ame_8_4_open Open benchmark statement: does an $\mathrm{AME}(8,4)$ state exist? sorry line 791 source
Source documentation
Open benchmark statement: does an $\mathrm{AME}(8,4)$ state exist?

depends on sorry what this means
Statement uses: Iff, True, OpenQuantumProblem35.ExistsAME, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem ame_8_4_open :
    answer(sorry) ↔ ExistsAME 8 4 := by
…
```
Mentions: OpenQuantumProblem35.ExistsAME
theorem OpenQuantumProblem35.ame_8_6_open Open benchmark statement: does an $\mathrm{AME}(8,6)$ state exist? sorry line 797 source
Source documentation
Open benchmark statement: does an $\mathrm{AME}(8,6)$ state exist?

depends on sorry what this means
Statement uses: Iff, True, OpenQuantumProblem35.ExistsAME, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem ame_8_6_open :
    answer(sorry) ↔ ExistsAME 8 6 := by
…
```
Mentions: OpenQuantumProblem35.ExistsAME
theorem OpenQuantumProblem35.ame_8_10_open Open benchmark statement: does an $\mathrm{AME}(8,10)$ state exist? sorry line 803 source
Source documentation
Open benchmark statement: does an $\mathrm{AME}(8,10)$ state exist?

depends on sorry what this means
Statement uses: Iff, True, OpenQuantumProblem35.ExistsAME, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem ame_8_10_open :
    answer(sorry) ↔ ExistsAME 8 10 := by
…
```
Mentions: OpenQuantumProblem35.ExistsAME
theorem OpenQuantumProblem35.ame_9_6_open sorry line 815 source
depends on sorry what this means
Statement uses: Iff, True, OpenQuantumProblem35.ExistsAME, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem OpenQuantumProblem35.ame_9_10_open sorry line 829 source
depends on sorry what this means
Statement uses: Iff, True, OpenQuantumProblem35.ExistsAME, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem OpenQuantumProblem35.ame_10_6_open Open benchmark statement: does an $\mathrm{AME}(10,6)$ state exist? sorry line 835 source
Source documentation
Open benchmark statement: does an $\mathrm{AME}(10,6)$ state exist?

depends on sorry what this means
Statement uses: Iff, True, OpenQuantumProblem35.ExistsAME, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem ame_10_6_open :
    answer(sorry) ↔ ExistsAME 10 6 := by
…
```
Mentions: OpenQuantumProblem35.ExistsAME
theorem OpenQuantumProblem35.ame_10_10_open Open benchmark statement: does an $\mathrm{AME}(10,10)$ state exist? sorry line 841 source
Source documentation
Open benchmark statement: does an $\mathrm{AME}(10,10)$ state exist?

depends on sorry what this means
Statement uses: Iff, True, OpenQuantumProblem35.ExistsAME, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem ame_10_10_open :
    answer(sorry) ↔ ExistsAME 10 10 := by
…
```
Mentions: OpenQuantumProblem35.ExistsAME
theorem OpenQuantumProblem35.ame_11_3_open Open benchmark statement: does an $\mathrm{AME}(11,3)$ state exist? sorry line 847 source
Source documentation
Open benchmark statement: does an $\mathrm{AME}(11,3)$ state exist?

depends on sorry what this means
Statement uses: Iff, True, OpenQuantumProblem35.ExistsAME, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem ame_11_3_open :
    answer(sorry) ↔ ExistsAME 11 3 := by
…
```
Mentions: OpenQuantumProblem35.ExistsAME
theorem OpenQuantumProblem35.ame_11_4_open sorry line 864 source
depends on sorry what this means
Statement uses: Iff, True, OpenQuantumProblem35.ExistsAME, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem OpenQuantumProblem35.ame_11_5_open sorry line 874 source
depends on sorry what this means
Statement uses: Iff, True, OpenQuantumProblem35.ExistsAME, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem OpenQuantumProblem35.ame_11_6_open Open benchmark statement: does an $\mathrm{AME}(11,6)$ state exist? sorry line 880 source
Source documentation
Open benchmark statement: does an $\mathrm{AME}(11,6)$ state exist?

depends on sorry what this means
Statement uses: Iff, True, OpenQuantumProblem35.ExistsAME, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem ame_11_6_open :
    answer(sorry) ↔ ExistsAME 11 6 := by
…
```
Mentions: OpenQuantumProblem35.ExistsAME
theorem OpenQuantumProblem35.ame_11_10_open sorry line 893 source
depends on sorry what this means
Statement uses: Iff, True, OpenQuantumProblem35.ExistsAME, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem OpenQuantumProblem35.ame_12_5_open Does an $\mathrm{AME}(12,5)$ state exist? sorry line 903 source
Source documentation
Does an $\mathrm{AME}(12,5)$ state exist?
The answer is yes. Bevins and Bidav construct an explicit Hermitian self-dual MDS code with parameters $[12,6,7]_{25}$, whose associated nonbinary stabilizer state is an $\mathrm{AME}(12,5)$ state.

depends on sorry what this means
Statement uses: Iff, True, OpenQuantumProblem35.ExistsAME, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem ame_12_5_open :
    answer(True) ↔ ExistsAME 12 5 := by
…
```
Mentions: OpenQuantumProblem35.ExistsAME
theorem OpenQuantumProblem35.ame_12_6_open Open benchmark statement: does an $\mathrm{AME}(12,6)$ state exist? sorry line 909 source
Source documentation
Open benchmark statement: does an $\mathrm{AME}(12,6)$ state exist?

depends on sorry what this means
Statement uses: Iff, True, OpenQuantumProblem35.ExistsAME, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem ame_12_6_open :
    answer(sorry) ↔ ExistsAME 12 6 := by
…
```
Mentions: OpenQuantumProblem35.ExistsAME
theorem OpenQuantumProblem35.ame_12_10_open Open benchmark statement: does an $\mathrm{AME}(12,10)$ state exist? sorry line 915 source
Source documentation
Open benchmark statement: does an $\mathrm{AME}(12,10)$ state exist?

depends on sorry what this means
Statement uses: Iff, True, OpenQuantumProblem35.ExistsAME, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem ame_12_10_open :
    answer(sorry) ↔ ExistsAME 12 10 := by
…
```
Mentions: OpenQuantumProblem35.ExistsAME
theorem OpenQuantumProblem35.oqp_35 Open Quantum Problem 35: classify all pairs $(n,d)$ with $n \ge 2$ and $d \ge 2$ for which an $\mathrm{AME}(n,d)$ state exists sorry line 923 source
Source documentation
Open Quantum Problem 35: classify all pairs $(n,d)$ with $n \ge 2$ and $d \ge 2$ for which an $\mathrm{AME}(n,d)$ state exists.

depends on sorry what this means
Statement uses: Eq, Set, Prod, Nat, Set.ofPred, And, LE.le, OfNat.ofNat, Prod.fst, Prod.snd, OpenQuantumProblem35.ExistsAME, sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem oqp_35 :
    {nd : ℕ × ℕ | 2 ≤ nd.1 ∧ 2 ≤ nd.2 ∧ ExistsAME nd.1 nd.2} = answer(sorry) := by
…
```
Mentions: OpenQuantumProblem35.ExistsAME