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 348 curated AI-written annotations and 373 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 12 manuscript-grounded curated result annotations were composed from pinned companion PDFs and named source records in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Twelve supporting declarations for the Hilbert-functions result were upgraded on 2026-10-14 from mechanically condensed doc comments to declaration-specific explanations bound to exact page-one terminology in the pinned human-written companion. The other Hilbert challenge statements were deliberately not described as companion-backed results because that manuscript proves P5 specifically. Fifteen previously unannotated declarations along the Hilbert P5 proof spine were annotated on 2026-10-14 from the pinned companion's seven-page argument, covering the two-generator decomposition, finite-difference bounds, critical-case reduction, and final log-concavity step. Each quotation is bound to its exact manuscript page and Lean declaration; no human review is claimed. Twenty-four further declarations along the Hilbert P5 box-count and finite-difference spine were annotated on 2026-10-14, covering the two-dimensional slice count, three-dimensional box formula, first- and second-difference identities, the seven-threshold curvature expression, boundary handling, pointwise transport, sum linearity, and lower-or-upper region classification. Every annotation is bound to an exact quotation on pages 2 or 3 of the pinned human-written companion; Lean-specific boundary and threshold helpers are identified as implementation lemmas rather than separate manuscript claims. No human review is claimed. Twenty-eight further declarations along the Hilbert P5 argument were annotated on 2026-10-14 from pages 2 through 6 of the pinned human-written companion. They expose the shifted residual sequence, exact lower- and upper-region formulas, symmetry by complementary divisors, the curvature-one and curvature-two splits, and the final algebraic reductions. Lean-only transport and integer-arithmetic helpers are labeled as proof infrastructure rather than new manuscript claims; each quotation is page-bound in the source ledger, and no human review is claimed. Twenty high-level declarations completing the Hilbert P5 curvature-one and curvature-two case spine were annotated on 2026-10-14 from pages 3 through 7 of the pinned human-written companion. The explanations separate cases A and B, lower and upper monomial regions, shifted residual evaluation, impossible mixed regions, and the surviving upper-upper estimate; wrapper lemmas are explicitly described as proof structure. Every quotation is page-bound, and no human review is claimed. Twenty-two graph-reconstruction declarations were upgraded or added on 2026-10-14 from the pinned four-page human-written companion, covering the incidence-deletion deck, edge and degree recovery, unique isolated vertices, vertex-type reconstruction, neighboring-type descent, adjacency recovery, and final bipartite isomorphism. The result annotation also records that `G_not_regular` is present in the Lean statement but unused by its proof term and absent from the companion theorem. Exact historical quotations from Paul J. Kelly (1957) and Bondy with Hemminger (1977) are linked separately; no human review is claimed. Eighteen declarations along the Erdős 741(i) strict-natural-density counterexample were added on 2026-10-14, covering the carry-free base-four digit split, full cross-sum coverage, sparse pure self-sums, fixed-factor fat intervals, the lower-scale density deficit, upper-scale sum growth, and the final convergence contradiction. The result annotation was corrected to distinguish the negative strict-natural-density Lean theorem from the compatible affirmative upper-density companion theorem; Ulam AI's written counterexample is explicitly identified as using a different interval length with the same mechanism. The quotations are page- and hash-bound where the PDFs expose text; Paul Erdős's scanned 1994 question was visually checked and is linked separately without a machine-audit claim. No human review is claimed. Twenty-eight additional declaration-level annotations were added on 2026-10-14 for the Erdős 12(i) proof, and its IsGood definition was upgraded from a source-comment condensation. They cover the prime and Chinese-remainder moduli, the actual Lean congruence-block witness, exclusion of cross-block and same-block triples, lower and upper counting bounds, and the positive liminf. The prior result annotation was corrected because the pinned human-written companion proves the same theorem with a different base-2-to-base-3 construction; it is no longer presented as the Lean proof. The original property-P definition from Erdős and Sárközy (1970) is separately linked and page-bound; no human review is claimed. The remaining fifty declarations in the Erdős 12(i) file were annotated on 2026-10-14, completing declaration-level coverage of all eighty definitions, lemmas, and theorems in that file. These additions expose the prime-recursion invariants, divisibility transport, Chinese-remainder witness bounds, numerical density envelopes, injective block coding, and liminf support lemmas instead of leaving the proof spine as raw Lean; no human review is claimed. Eighteen supporting declarations for Erdős 125 were added on 2026-10-14, completing all nineteen declarations in the file. The annotations follow the pinned companion through digit-block decomposition, irrational logarithmic approximation, the explicit Lean contraction factor 11/12, geometric iteration, and the lower-density conclusion. The original 1996 question of Burr, Erdős, Graham, and Li and the 2026 discussion contributions of GTSoukalas, Terence Tao, and Giuseppe Melfi are linked separately; no human review is claimed. Twenty-eight supporting declarations for Erdős 138 were upgraded or added on 2026-10-14, completing all twenty-nine declarations in the file. The annotations separate the greedy difference proof from the Lean-specific representation bridges and ultrafilter compactness proof of existence, and bind quotations from the pinned companion, the AlphaProof Nexus paper, Erdős's 1981 source, van der Waerden's recollection, and the 2026 Erdős Problems discussion. No human review is claimed. The curated Erdős 12(ii), 138, and 152 annotations were further linked on 2026-10-14 to exact quotations from Felix Behrend, Bartel van der Waerden, and Paul Erdős with Pál Turán; the historical quotation sources are labeled separately from the pinned AlphaProof proof companions. The curated Hilbert-functions result, its OrderIdeal and pureOSequence definitions, and the Erdős 846 annotation were further linked on 2026-10-14 to exact quotations from Richard P. Stanley and from Moe Putterman, Mehtaab Sawhney, and Gregory Valiant. The Stanley PDF is hash- and page-bound in the source ledger; these historical sources are labeled separately from the pinned AlphaProof proof companions. Three additional target-specific annotations for Ben Green's Problem 57, exact last-iterate anchored-GDA convergence, and Graffiti.pc Conjecture 2 were composed on 2026-10-14 from the exact pinned Lean statements, quotations from the AlphaProof Nexus paper, and quotations from Green, Ryu with Yuan and Yin, Surina et al., and Wang with Dai and Tong; no human review is claimed. Two additional target-specific quantum-optics annotations for the explicit AME(11,5) construction and the even N >= 4, D = N monochromatic-quantum-graph theorem were composed on 2026-10-14 from the exact pinned Lean statements, page-bound quotations from the AlphaProof Nexus paper, Helwig et al., and Krenn, Gu, and Zeilinger, and Mario Krenn's public priority correction. The AME annotation makes no first-discovery claim; the monochromatic annotation states that the local AlphaProof wrapper contains sorry and links the separate pinned proof-bearing Formal Conjectures artifact without silently treating it as local verification. Twelve declarations that the pinned source repeats verbatim in several files were annotated in only one of the copies, so the build rejected them as differing copies. On 2026-10-16 each curated annotation was copied unchanged to every identical copy: the eleven Hilbert-functions definitions from hilbert_functions_5 to hilbert_functions_1, _2, _3, _4, _7 and _8, and Erdos12.IsGood from erdos_12.parts.i to erdos_12.parts.ii (the better-sourced annotation was kept in each case). Each copy's quotations are bound in the source ledger like the original's; no new text was written and no human review is claimed. The remaining source-derived annotations were 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 source prose.

Credit: Google DeepMind published the AlphaProof Nexus proof artifacts. The pinned repository identifies the mathematical sources and collaborators, including OEIS, Erdős Problems, Gergely Bérczi, and Mario Krenn; those source records remain the authority for individual credit.

Project sources: Pinned AlphaProof Nexus results documentation, AlphaProof Nexus paper, Pinned human-written natural-language proof companions

194 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).

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)

FormalConjectures.Util.ProblemImports

abbrev OpenQuantumProblem35.Config A computational-basis configuration of $n$ parties with local dimension $d$ line 85 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 88 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 91 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 95) line 95 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 100 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 104 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 109 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 47 more
104 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 129 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 134 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 140 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 145 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 151 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, 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 160 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 171 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 175 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 180 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, dite, LT.lt, Fin.mk, Not, Eq.trans, eq_true, Fin.isLt, True, congrArg, dite_cond_eq_true, 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 187 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, dite, Fin.mk, Eq.trans, of_eq_false, eq_false, add_tsub_cancel_left, True, congrArg, dite_cond_eq_false, Fin.mk.congr_simp, 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 201 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
37 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 209 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
17 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 215 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 232 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 239 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 244 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, Eq, ENNReal, OpenQuantumProblem35.Config, Complex, Subsingleton.elim, IsEmpty.mk, Fin.elim0, Real, Eq.mpr, id, False.elim, Eq.mp, OpenQuantumProblem35.IsNormalized, Eq.trans, Norm.norm and 15 more
49 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 256 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, 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
15 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 261 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, HSMul.hSMul, Matrix, Eq.trans, HPow.hPow, True, congr, congrArg, Finset.prod, Finset.univ, Fintype.card_pi, Finset.card, Finset.prod_congr, Eq.refl, Finset, Membership.mem, Fintype.card_fin, Finset.prod_const, Nat.cast_pow and 11 more
51 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 272 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 276 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 279) line 279 source
def OpenQuantumProblem35.constantConfig The constant configuration with value $a$ line 285 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 290 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 297 source
Source documentation
A simple binary two-party configuration with different entries is not constant.

standard axioms: Classical.choice, 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 304 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 309 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 314 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 318 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 322 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 326 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 331 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 340 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 354 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, 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
58 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 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, 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, Complex.ofReal_inv, eq_self
59 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 375 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
80 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 422 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 433 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 446 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 457 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 472 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
16 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 487 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 509 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 530 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, congr, ite_cond_eq_false, eq_false, star_zero, MulZeroClass.mul_zero and 18 more
130 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 578 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
73 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 594 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, Decidable.byContradiction, Not, OpenQuantumProblem35.diagonalState
Proof uses: OpenQuantumProblem35.hasMaximallyMixedFirstReduction_of_completion, 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, congrArg, Eq.trans and 15 more
51 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 610 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 623 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 630 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 637 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 642 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 649 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, of_decide_eq_true, LE.le, id, Bool, Decidable.decide, Bool.true, Eq.refl, WithLp.ofLp, ENNReal, OpenQuantumProblem35.diagonalState
Proof uses: Not, OpenQuantumProblem35.IsConstantConfig, Eq.mp, OpenQuantumProblem35.leftIndex, congr, congrArg, OpenQuantumProblem35.combineFirst_leftIndex, of_eq_true, Eq.trans, True, ite, OpenQuantumProblem35.uniformCoeff, OpenQuantumProblem35.diagonalState_apply, ite_cond_eq_false, eq_false, eq_self
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 663 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
118 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 707 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 712 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 Source-backed benchmark statement: an $\mathrm{AME}(5,2)$ state exists sorry line 717 source
Source documentation
Source-backed benchmark statement: an $\mathrm{AME}(5,2)$ state exists. This is one of the four qubit cases $n=2,3,5,6$; see the OQP page and Scott (2004).

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_5_2_exists : ExistsAME 5 2 := by
…
```
Mentions: OpenQuantumProblem35.ExistsAME
theorem OpenQuantumProblem35.ame_6_2_exists Source-backed benchmark statement: an $\mathrm{AME}(6,2)$ state exists sorry line 722 source
Source documentation
Source-backed benchmark statement: an $\mathrm{AME}(6,2)$ state exists. This is one of the four qubit cases $n=2,3,5,6$; see the OQP page and Scott (2004).

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_6_2_exists : ExistsAME 6 2 := by
…
```
Mentions: OpenQuantumProblem35.ExistsAME
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 727 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 732 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_4_3_exists Source-backed benchmark statement: an $\mathrm{AME}(4,3)$ state exists; see Helwig et al sorry line 737 source
Source documentation
Source-backed benchmark statement: an $\mathrm{AME}(4,3)$ state exists; see Helwig et al. (2012) and Goyeneche et al. (2015).

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_3_exists : ExistsAME 4 3 := by
…
```
Mentions: OpenQuantumProblem35.ExistsAME
theorem OpenQuantumProblem35.ame_4_6_exists Source-backed benchmark statement: an $\mathrm{AME}(4,6)$ state exists; see Rather et al sorry line 742 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 Open benchmark statement: does an $\mathrm{AME}(7,6)$ state exist? sorry line 749 source
Source documentation
Open benchmark statement: does an $\mathrm{AME}(7,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_7_6_open :
    answer(sorry) ↔ ExistsAME 7 6 := by
…
```
Mentions: OpenQuantumProblem35.ExistsAME
theorem OpenQuantumProblem35.ame_7_10_open Open benchmark statement: does an $\mathrm{AME}(7,10)$ state exist? sorry line 755 source
Source documentation
Open benchmark statement: does an $\mathrm{AME}(7,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_7_10_open :
    answer(sorry) ↔ 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 761 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 767 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 773 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 Open benchmark statement: does an $\mathrm{AME}(9,6)$ state exist? sorry line 779 source
Source documentation
Open benchmark statement: does an $\mathrm{AME}(9,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_9_6_open :
    answer(sorry) ↔ ExistsAME 9 6 := by
…
```
Mentions: OpenQuantumProblem35.ExistsAME
theorem OpenQuantumProblem35.ame_9_10_open Open benchmark statement: does an $\mathrm{AME}(9,10)$ state exist? sorry line 785 source
Source documentation
Open benchmark statement: does an $\mathrm{AME}(9,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_9_10_open :
    answer(sorry) ↔ ExistsAME 9 10 := by
…
```
Mentions: OpenQuantumProblem35.ExistsAME
theorem OpenQuantumProblem35.ame_10_6_open Open benchmark statement: does an $\mathrm{AME}(10,6)$ state exist? sorry line 791 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 797 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 803 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 Open benchmark statement: does an $\mathrm{AME}(11,4)$ state exist? sorry line 809 source
Source documentation
Open benchmark statement: does an $\mathrm{AME}(11,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_11_4_open :
    answer(sorry) ↔ ExistsAME 11 4 := by
…
```
Mentions: OpenQuantumProblem35.ExistsAME
def OpenQuantumProblem35.omega5 line 818 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Complex
Proof uses: Complex.exp, HDiv.hDiv, HMul.hMul, OfNat.ofNat, Real.pi, Complex.I
10 instances, coercions and auxiliary constants left out.
lemma OpenQuantumProblem35.omega5_pow_sum line 820 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Ne, Eq, Complex, Finset.sum, Finset.univ, HPow.hPow, OpenQuantumProblem35.omega5, ZMod.val, HMul.hMul
Proof uses: by_contra, Not, absurd, Fact, Nat.Prime, False, Fact.mk, Nat.prime_five, Eq.trans, id, Complex.exp, HDiv.hDiv, Real.pi, Complex.I, HAdd.hAdd, Equiv, Equiv.mulLeft₀, Equiv.sum_comp, Finset.range, Fin.sum_univ_eq_sum_range and 11 more
96 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def OpenQuantumProblem35.explicit_A line 824 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Matrix, Fin, OfNat.ofNat, Nat, ZMod
Proof uses: Array, List.toArray, List.cons, List.nil, Array.getD, HMod.hMod, HSub.hSub, HAdd.hAdd
25 instances, coercions and auxiliary constants left out.
def OpenQuantumProblem35.S_mat line 828 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: List, Fin, OfNat.ofNat, Nat, ZMod
Proof uses: OpenQuantumProblem35.explicit_A, List.getD
5 instances, coercions and auxiliary constants left out.
def OpenQuantumProblem35.drop_col line 831 source
standard axioms: Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat
Proof uses: ite, LT.lt, Fin.mk, HAdd.hAdd
9 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def OpenQuantumProblem35.submatrix line 834 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, LE.le, Matrix, Fin, ZMod, OfNat.ofNat, Equiv.Perm, HSub.hSub
Proof uses: Equiv, Equiv.symm, OpenQuantumProblem35.leftIndex, OpenQuantumProblem35.rightIndex
11 instances, coercions and auxiliary constants left out.
def OpenQuantumProblem35.rankCondition line 838 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Matrix, Fin, ZMod, OfNat.ofNat
Proof uses: Equiv.Perm, OpenQuantumProblem35.Config, Ne, Exists, HSub.hSub, Finset.sum, Finset.univ, HMul.hMul, OpenQuantumProblem35.submatrix
28 instances, coercions and auxiliary constants left out.
def OpenQuantumProblem35.explicit_A_nat line 842 source
no axioms what this means
Statement uses: Nat
Proof uses: Array, List.toArray, List.cons, OfNat.ofNat, List.nil, Array.getD, HMod.hMod, HSub.hSub, HAdd.hAdd
7 instances, coercions and auxiliary constants left out.
def OpenQuantumProblem35.get_cols line 846 source
no axioms what this means
Statement uses: Nat, Prod
Proof uses: OpenQuantumProblem35.get_cols.loop, OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
def OpenQuantumProblem35.subset_rank_cond_fn line 867 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Matrix, Fin, OfNat.ofNat, Nat, ZMod
Proof uses: And, Ne, Or, Exists, HAdd.hAdd, HMul.hMul
15 instances, coercions and auxiliary constants left out.
def OpenQuantumProblem35.det2 line 876 source
no axioms what this means
Statement uses: Nat
Proof uses: HMod.hMod, HSub.hSub, HAdd.hAdd, HMul.hMul, OfNat.ofNat
9 instances, coercions and auxiliary constants left out.
def OpenQuantumProblem35.det3 line 879 source
no axioms what this means
Statement uses: Nat
Proof uses: HMod.hMod, HAdd.hAdd, HMul.hMul, OpenQuantumProblem35.det2, HSub.hSub, OfNat.ofNat
9 instances, coercions and auxiliary constants left out.
def OpenQuantumProblem35.det4 line 884 source
no axioms what this means
Statement uses: Nat
Proof uses: HMod.hMod, HAdd.hAdd, HMul.hMul, OpenQuantumProblem35.det3, HSub.hSub, OfNat.ofNat
9 instances, coercions and auxiliary constants left out.
def OpenQuantumProblem35.det5 line 893 source
no axioms what this means
Statement uses: Nat
Proof uses: HMod.hMod, HAdd.hAdd, HMul.hMul, OpenQuantumProblem35.det4, HSub.hSub, OfNat.ofNat
9 instances, coercions and auxiliary constants left out.
def OpenQuantumProblem35.is_full_rank_M line 904 source
no axioms what this means
Statement uses: Nat, Bool
Proof uses: bne, OpenQuantumProblem35.det5, OpenQuantumProblem35.explicit_A_nat, OfNat.ofNat, Bool.or
3 instances, coercions and auxiliary constants left out.
def OpenQuantumProblem35.subset_rank_cond_det_bool line 918 source
no axioms what this means
Statement uses: Fin, OfNat.ofNat, Nat, Bool
Proof uses: OpenQuantumProblem35.subset_rank_cond_det_bool.match_1, Prod, OpenQuantumProblem35.get_cols, OpenQuantumProblem35.is_full_rank_M
3 instances, coercions and auxiliary constants left out.
def OpenQuantumProblem35.get_cols_complement_bool line 924 source
no axioms what this means
Statement uses: Nat, Bool
Proof uses: Prod, OpenQuantumProblem35.get_cols, Prod.fst, Prod.snd, Bool.and, Decidable.decide, LT.lt, OfNat.ofNat, bne
5 instances, coercions and auxiliary constants left out.
def OpenQuantumProblem35.loop_comp_f4 line 940 source
no axioms what this means
Statement uses: Nat, Bool
Proof uses: OpenQuantumProblem35.get_cols.loop.match_2, Unit, OfNat.ofNat, Bool.true, Nat.succ, ite, Eq, Bool.and, Decidable.decide, GT.gt, OpenQuantumProblem35.get_cols_complement_bool, Bool.false
6 instances, coercions and auxiliary constants left out.
def OpenQuantumProblem35.loop_comp_f3 line 948 source
no axioms what this means
Statement uses: Nat, Bool
Proof uses: OpenQuantumProblem35.get_cols.loop.match_2, Unit, OfNat.ofNat, Bool.true, Nat.succ, Bool.and, OpenQuantumProblem35.loop_comp_f4
3 instances, coercions and auxiliary constants left out.
def OpenQuantumProblem35.loop_comp_f2 line 953 source
no axioms what this means
Statement uses: Nat, Bool
Proof uses: OpenQuantumProblem35.get_cols.loop.match_2, Unit, OfNat.ofNat, Bool.true, Nat.succ, Bool.and, OpenQuantumProblem35.loop_comp_f3
3 instances, coercions and auxiliary constants left out.
def OpenQuantumProblem35.loop_comp_f1 line 958 source
no axioms what this means
Statement uses: Nat, Bool
Proof uses: OpenQuantumProblem35.get_cols.loop.match_2, Unit, OfNat.ofNat, Bool.true, Nat.succ, Bool.and, OpenQuantumProblem35.loop_comp_f2
3 instances, coercions and auxiliary constants left out.
def OpenQuantumProblem35.loop_comp_f0 line 963 source
no axioms what this means
Statement uses: Nat, Bool
Proof uses: OpenQuantumProblem35.get_cols.loop.match_2, Unit, OfNat.ofNat, Bool.true, Nat.succ, Bool.and, OpenQuantumProblem35.loop_comp_f1
3 instances, coercions and auxiliary constants left out.
def OpenQuantumProblem35.check_all_subsets_complement line 968 source
no axioms what this means
Statement uses: Bool
Proof uses: OpenQuantumProblem35.loop_comp_f0, OfNat.ofNat, Nat
1 instances, coercions and auxiliary constants left out.
lemma OpenQuantumProblem35.check_all_subsets_complement_eq_true line 970 source
no axioms what this means
Statement uses: Eq, Bool, OpenQuantumProblem35.check_all_subsets_complement, Bool.true
Proof uses: of_decide_eq_true, id, Decidable.decide, Eq.refl
1 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.loop_comp_f4_implies line 972 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, Bool, OpenQuantumProblem35.loop_comp_f4, Bool.true, LT.lt, GT.gt, OpenQuantumProblem35.get_cols_complement_bool
Proof uses: Nat.recAux, OfNat.ofNat, Decidable.byContradiction, Not, Eq.mpr, HAdd.hAdd, ite, Bool.and, Decidable.decide, Bool.false, id, implies_congr, OpenQuantumProblem35.get_cols.loop.match_2, Unit, congrArg, OpenQuantumProblem35.loop_comp_f4.eq_def, Eq.refl, dite, if_pos, Or and 21 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.loop_comp_f3_implies line 998 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, Bool, OpenQuantumProblem35.loop_comp_f3, Bool.true, LT.lt, GT.gt, OpenQuantumProblem35.loop_comp_f4
Proof uses: Nat.recAux, OfNat.ofNat, Decidable.byContradiction, Not, Eq.mpr, HAdd.hAdd, Bool.and, id, implies_congr, OpenQuantumProblem35.get_cols.loop.match_2, Unit, congrArg, OpenQuantumProblem35.loop_comp_f3.eq_def, Eq.refl, And, of_eq_true, Eq.trans, True, Bool.and_eq_true, Or and 5 more
10 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.loop_comp_f2_implies line 1017 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, Bool, OpenQuantumProblem35.loop_comp_f2, Bool.true, LT.lt, GT.gt, OpenQuantumProblem35.loop_comp_f3
Proof uses: Nat.recAux, OfNat.ofNat, Decidable.byContradiction, Not, Eq.mpr, HAdd.hAdd, Bool.and, id, implies_congr, OpenQuantumProblem35.get_cols.loop.match_2, Unit, congrArg, OpenQuantumProblem35.loop_comp_f2.eq_def, Eq.refl, And, of_eq_true, Eq.trans, True, Bool.and_eq_true, Or and 5 more
10 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.loop_comp_f1_implies line 1036 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, Bool, OpenQuantumProblem35.loop_comp_f1, Bool.true, LT.lt, GT.gt, OpenQuantumProblem35.loop_comp_f2
Proof uses: Nat.recAux, OfNat.ofNat, Decidable.byContradiction, Not, Eq.mpr, HAdd.hAdd, Bool.and, id, implies_congr, OpenQuantumProblem35.get_cols.loop.match_2, Unit, congrArg, OpenQuantumProblem35.loop_comp_f1.eq_def, Eq.refl, And, of_eq_true, Eq.trans, True, Bool.and_eq_true, Or and 5 more
10 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.loop_comp_f0_implies line 1055 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, Bool, OpenQuantumProblem35.loop_comp_f0, Bool.true, LT.lt, OpenQuantumProblem35.loop_comp_f1
Proof uses: Nat.recAux, OfNat.ofNat, Decidable.byContradiction, Not, Eq.mpr, HAdd.hAdd, Bool.and, id, implies_congr, OpenQuantumProblem35.get_cols.loop.match_2, Unit, congrArg, OpenQuantumProblem35.loop_comp_f0.eq_def, Eq.refl, And, of_eq_true, Eq.trans, True, Bool.and_eq_true, Or and 5 more
10 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
def OpenQuantumProblem35.loop_det_f4 line 1076 source
no axioms what this means
Statement uses: Nat, Bool
Proof uses: OpenQuantumProblem35.get_cols.loop.match_2, Unit, OfNat.ofNat, Bool.true, Nat.succ, ite, Eq, Bool.and, Decidable.decide, GT.gt, dite, LT.lt, OpenQuantumProblem35.subset_rank_cond_det_bool, Fin.mk, Bool.false, Not
6 instances, coercions and auxiliary constants left out.
def OpenQuantumProblem35.loop_det_f3 line 1090 source
no axioms what this means
Statement uses: Nat, Bool
Proof uses: OpenQuantumProblem35.get_cols.loop.match_2, Unit, OfNat.ofNat, Bool.true, Nat.succ, Bool.and, OpenQuantumProblem35.loop_det_f4
3 instances, coercions and auxiliary constants left out.
def OpenQuantumProblem35.loop_det_f2 line 1095 source
no axioms what this means
Statement uses: Nat, Bool
Proof uses: OpenQuantumProblem35.get_cols.loop.match_2, Unit, OfNat.ofNat, Bool.true, Nat.succ, Bool.and, OpenQuantumProblem35.loop_det_f3
3 instances, coercions and auxiliary constants left out.
def OpenQuantumProblem35.loop_det_f1 line 1100 source
no axioms what this means
Statement uses: Nat, Bool
Proof uses: OpenQuantumProblem35.get_cols.loop.match_2, Unit, OfNat.ofNat, Bool.true, Nat.succ, Bool.and, OpenQuantumProblem35.loop_det_f2
3 instances, coercions and auxiliary constants left out.
def OpenQuantumProblem35.loop_det_f0 line 1105 source
no axioms what this means
Statement uses: Nat, Bool
Proof uses: OpenQuantumProblem35.get_cols.loop.match_2, Unit, OfNat.ofNat, Bool.true, Nat.succ, Bool.and, OpenQuantumProblem35.loop_det_f1
3 instances, coercions and auxiliary constants left out.
def OpenQuantumProblem35.check_all_subsets_det line 1110 source
no axioms what this means
Statement uses: Bool
Proof uses: OpenQuantumProblem35.loop_det_f0, OfNat.ofNat, Nat
1 instances, coercions and auxiliary constants left out.
lemma OpenQuantumProblem35.check_all_subsets_det_eq_true line 1112 source
no axioms what this means
Statement uses: Eq, Bool, OpenQuantumProblem35.check_all_subsets_det, Bool.true
Proof uses: of_decide_eq_true, id, Decidable.decide, Eq.refl
1 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.det_ne_zero_implies_v_zero line 1114 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Matrix, Fin, OfNat.ofNat, Nat, ZMod, Ne, Matrix.det, Eq, Finset.sum, Finset.univ, HMul.hMul
Proof uses: Fact, Nat.Prime, Fact.mk, Nat.prime_five, congr_fun, Matrix.eq_zero_of_vecMul_eq_zero, funext, Matrix.vecMul
32 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.loop_det_f4_implies line 1119 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, Bool, OpenQuantumProblem35.loop_det_f4, Bool.true, LT.lt, GT.gt, OfNat.ofNat, OpenQuantumProblem35.subset_rank_cond_det_bool, Fin.mk
Proof uses: Nat.recAux, Decidable.byContradiction, Not, Eq.mpr, HAdd.hAdd, ite, Bool.and, Decidable.decide, dite, Bool.false, id, implies_congr, OpenQuantumProblem35.get_cols.loop.match_2, Unit, congrArg, OpenQuantumProblem35.loop_det_f4.eq_def, Eq.refl, if_pos, dif_pos, Or and 22 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 66 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.loop_det_f3_implies line 1171 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, Bool, OpenQuantumProblem35.loop_det_f3, Bool.true, LT.lt, GT.gt, OpenQuantumProblem35.loop_det_f4
Proof uses: Nat.recAux, OfNat.ofNat, Decidable.byContradiction, Not, Eq.mpr, HAdd.hAdd, Bool.and, id, implies_congr, OpenQuantumProblem35.get_cols.loop.match_2, Unit, congrArg, OpenQuantumProblem35.loop_det_f3.eq_def, Eq.refl, And, of_eq_true, Eq.trans, True, Bool.and_eq_true, Or and 5 more
10 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.loop_det_f2_implies line 1190 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, Bool, OpenQuantumProblem35.loop_det_f2, Bool.true, LT.lt, GT.gt, OpenQuantumProblem35.loop_det_f3
Proof uses: Nat.recAux, OfNat.ofNat, Decidable.byContradiction, Not, Eq.mpr, HAdd.hAdd, Bool.and, id, implies_congr, OpenQuantumProblem35.get_cols.loop.match_2, Unit, congrArg, OpenQuantumProblem35.loop_det_f2.eq_def, Eq.refl, And, of_eq_true, Eq.trans, True, Bool.and_eq_true, Or and 5 more
10 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.loop_det_f1_implies line 1209 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, Bool, OpenQuantumProblem35.loop_det_f1, Bool.true, LT.lt, GT.gt, OpenQuantumProblem35.loop_det_f2
Proof uses: Nat.recAux, OfNat.ofNat, Decidable.byContradiction, Not, Eq.mpr, HAdd.hAdd, Bool.and, id, implies_congr, OpenQuantumProblem35.get_cols.loop.match_2, Unit, congrArg, OpenQuantumProblem35.loop_det_f1.eq_def, Eq.refl, And, of_eq_true, Eq.trans, True, Bool.and_eq_true, Or and 5 more
10 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.loop_det_f0_implies line 1228 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, Bool, OpenQuantumProblem35.loop_det_f0, Bool.true, LT.lt, OpenQuantumProblem35.loop_det_f1
Proof uses: Nat.recAux, OfNat.ofNat, Decidable.byContradiction, Not, Eq.mpr, HAdd.hAdd, Bool.and, id, implies_congr, OpenQuantumProblem35.get_cols.loop.match_2, Unit, congrArg, OpenQuantumProblem35.loop_det_f0.eq_def, Eq.refl, And, of_eq_true, Eq.trans, True, Bool.and_eq_true, Or and 5 more
10 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.check_all_subsets_det_implies line 1247 source
standard axioms: Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, GT.gt, Eq, Bool, OpenQuantumProblem35.subset_rank_cond_det_bool, Bool.true
Proof uses: OpenQuantumProblem35.loop_det_f1, OpenQuantumProblem35.loop_det_f0_implies, OpenQuantumProblem35.check_all_subsets_det_eq_true, Fin.isLt, OpenQuantumProblem35.loop_det_f2, OpenQuantumProblem35.loop_det_f1_implies, OpenQuantumProblem35.loop_det_f3, OpenQuantumProblem35.loop_det_f2_implies, OpenQuantumProblem35.loop_det_f4, OpenQuantumProblem35.loop_det_f3_implies, Fin.mk, OpenQuantumProblem35.loop_det_f4_implies
6 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.subset_rank_cond_swap01 line 1256 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Matrix, Fin, OfNat.ofNat, Nat, ZMod, OpenQuantumProblem35.subset_rank_cond_fn
Proof uses: id, Membership.mem, Bool, Set, setOf, And, Ne, Or, Exists, HAdd.hAdd, HMul.hMul, Bool.and, Function.comp, Not, Eq, Exists.imp, And.imp, Iff.mp, and_left_comm, mt and 24 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.subset_rank_cond_swap12 line 1261 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Matrix, Fin, OfNat.ofNat, Nat, ZMod, OpenQuantumProblem35.subset_rank_cond_fn
Proof uses: id, Membership.mem, Set, setOf, And, Ne, Or, Exists, HAdd.hAdd, HMul.hMul, Function.comp, Exists.imp, And.imp, And.imp_right, Iff.mp, and_left_comm, mt, Eq, Eq.trans, Mathlib.Tactic.Abel.termg and 24 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.subset_rank_cond_swap23 line 1266 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Matrix, Fin, OfNat.ofNat, Nat, ZMod, OpenQuantumProblem35.subset_rank_cond_fn
Proof uses: id, Eq.mpr, Membership.mem, Bool, Set, setOf, And, Ne, Or, Exists, HAdd.hAdd, HMul.hMul, Bool.and, Eq, implies_congr, Eq.trans, congrArg, funext, Eq.refl, forall_congr and 35 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.subset_rank_cond_swap34 line 1272 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Matrix, Fin, OfNat.ofNat, Nat, ZMod, OpenQuantumProblem35.subset_rank_cond_fn
Proof uses: id, IsEmpty, Nonempty, Or, Membership.mem, Bool, Set, setOf, And, Ne, Exists, HAdd.hAdd, HMul.hMul, Bool.and, isEmpty_or_nonempty, False.elim, Eq.mp, False, Eq.mpr, Eq and 37 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.det2_eq line 1287 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, ZMod, OfNat.ofNat, OpenQuantumProblem35.det2, HSub.hSub, HMul.hMul
Proof uses: id, Eq.trans, HMod.hMod, HAdd.hAdd, ZMod.natCast_mod, Nat.cast_sub, Decidable.byContradiction, LE.le, Not, of_eq_true, True, congrArg, congr, Nat.cast_add, Nat.cast_mul, of_decide_eq_true, Bool, Decidable.decide, Bool.true, Eq.refl and 2 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.det3_eq line 1292 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, ZMod, OfNat.ofNat, OpenQuantumProblem35.det3, HAdd.hAdd, HSub.hSub, HMul.hMul, OpenQuantumProblem35.det2
Proof uses: Decidable.byContradiction, Not, Star.star, Mod.mod, HMod.hMod, Eq.trans, ZMod.natCast_mod, Eq.mpr, id, congrArg, Nat.cast_add, Nat.cast_mul, Eq.refl, Fin, Neg.neg, congr, TrivialStar.star_trivial, sub_eq_add_neg, HAdd, Eq.rec and 3 more
74 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.det4_eq line 1305 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, ZMod, OfNat.ofNat, OpenQuantumProblem35.det4, HSub.hSub, HAdd.hAdd, HMul.hMul, OpenQuantumProblem35.det3
Proof uses: Eq.mpr, id, congrArg, sub_add, sub_sub, Int, Int.subNatNat, Eq.trans, congr, Nat.cast_mul, Eq.symm, Int.cast_mul, Int.cast_natCast, HMod.hMod, Iff.mpr, Nat.ModEq, ZMod.eq_iff_modEq_nat, Nat.mod_mod, of_eq_true, Neg.neg and 25 more
118 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.det5_eq line 1317 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, ZMod, OfNat.ofNat, OpenQuantumProblem35.det5, HAdd.hAdd, HSub.hSub, HMul.hMul, OpenQuantumProblem35.det4
Proof uses: Eq.mpr, id, congrArg, Eq.trans, sub_add, Int, Int.subNatNat, congr, Nat.cast_mul, Eq.symm, Int.cast_mul, Int.cast_natCast, Star.star, Mod.mod, HMod.hMod, Neg.neg, add_assoc, TrivialStar.star_trivial, sub_eq_add_neg, Int.cast_add and 28 more
122 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.matrix_det2_eq line 1330 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Matrix, Fin, OfNat.ofNat, Nat, ZMod, Eq, Matrix.det, HSub.hSub, HMul.hMul
Proof uses: Matrix.det_fin_two
21 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.matrix_det3_eq line 1334 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Matrix, Fin, OfNat.ofNat, Nat, ZMod, Eq, Matrix.det, HAdd.hAdd, HSub.hSub, HMul.hMul, Nat.succ, Matrix.vecCons, Matrix.vecEmpty
Proof uses: Eq.trans, Matrix.det_fin_three, symm, Eq.mpr, id, congrArg, Matrix.det_fin_two, Eq.refl, Eq.symm, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.sub_congr, Mathlib.Tactic.Ring.add_congr, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.add_mul and 25 more
59 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.matrix_det4_eq line 1340 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Matrix, Fin, OfNat.ofNat, Nat, ZMod, Eq, Matrix.det, HSub.hSub, HAdd.hAdd, HMul.hMul, Nat.succ, Matrix.vecCons, Matrix.vecEmpty
Proof uses: Eq.mpr, Neg.neg, Fin.succAbove, id, congr, Fin.succ, congrArg, Eq.trans, Finset.sum, Finset.univ, HPow.hPow, Matrix.submatrix, Matrix.det_succ_row_zero, Finset.sum_congr, Eq.refl, Finset, Membership.mem, CommRing, Matrix.det_fin_three, AddCommMonoid and 39 more
105 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.matrix_det5_eq line 1348 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Matrix, Fin, OfNat.ofNat, Nat, ZMod, Eq, Matrix.det, HAdd.hAdd, HSub.hSub, HMul.hMul, Nat.succ, Matrix.vecCons, Matrix.vecEmpty
Proof uses: Eq.mpr, Finset.sum, Finset.univ, HPow.hPow, Neg.neg, Matrix.submatrix, Fin.succ, Fin.succAbove, id, congrArg, Matrix.det_succ_row_zero, propext, eq_comm, congr, Eq.trans, sub_eq_add_neg, Finset.sum_congr, Eq.refl, Finset, Membership.mem and 35 more
92 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
def OpenQuantumProblem35.minor_matrix line 1363 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Matrix, ZMod
Proof uses: Matrix.vecCons, Nat.succ, Matrix.vecEmpty, OpenQuantumProblem35.explicit_A
2 instances, coercions and auxiliary constants left out.
lemma OpenQuantumProblem35.minor_matrix_apply line 1369 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Eq, ZMod, OpenQuantumProblem35.minor_matrix, OpenQuantumProblem35.explicit_A, Matrix.vecCons, Nat.succ, Matrix.vecEmpty
Proof uses: rfl
2 instances, coercions and auxiliary constants left out.
lemma OpenQuantumProblem35.det2_bridge line 1372 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Eq, ZMod, OpenQuantumProblem35.det2, OpenQuantumProblem35.explicit_A_nat, Matrix.det, Nat.succ, Matrix.vecCons, OpenQuantumProblem35.explicit_A, Matrix.vecEmpty
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, Eq.mpr, HSub.hSub, HMul.hMul, congrArg, OpenQuantumProblem35.det2_eq, OpenQuantumProblem35.matrix_det2_eq, of_eq_true, Eq.trans, True, congr, Matrix.cons_val', funext, Matrix.cons_val_fin_one, congrFun and 1 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.det3_bridge line 1381 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Eq, ZMod, OpenQuantumProblem35.det3, OpenQuantumProblem35.explicit_A_nat, Matrix.det, Nat.succ, Matrix.vecCons, OpenQuantumProblem35.explicit_A, Matrix.vecEmpty
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, Eq.mpr, HAdd.hAdd, HSub.hSub, HMul.hMul, OpenQuantumProblem35.det2, congrArg, OpenQuantumProblem35.det3_eq, OpenQuantumProblem35.matrix_det3_eq, congr, Eq.trans, Matrix.cons_val', funext, Matrix.cons_val_fin_one, Matrix.det.congr_simp and 5 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.det4_bridge line 1396 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Eq, ZMod, OpenQuantumProblem35.det4, OpenQuantumProblem35.explicit_A_nat, Matrix.det, Nat.succ, Matrix.vecCons, OpenQuantumProblem35.explicit_A, Matrix.vecEmpty
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, Eq.mpr, HSub.hSub, HAdd.hAdd, HMul.hMul, OpenQuantumProblem35.det3, congrArg, OpenQuantumProblem35.det4_eq, OpenQuantumProblem35.matrix_det4_eq, congr, Eq.trans, Matrix.cons_val', funext, Matrix.cons_val_fin_one, Matrix.det.congr_simp and 5 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.minor_det_bridge_eq line 1414 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Eq, ZMod, OpenQuantumProblem35.det5, OpenQuantumProblem35.explicit_A_nat, Matrix.det, OpenQuantumProblem35.minor_matrix
Proof uses: OpenQuantumProblem35.explicit_A, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, Eq.mpr, HAdd.hAdd, HSub.hSub, HMul.hMul, OpenQuantumProblem35.det4, congrArg, OpenQuantumProblem35.det5_eq, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, OpenQuantumProblem35.matrix_det5_eq, Eq.symm, OpenQuantumProblem35.det4_bridge and 5 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.minor_det_bridge line 1431 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Ne, OpenQuantumProblem35.det5, OpenQuantumProblem35.explicit_A_nat, ZMod, Matrix.det, OpenQuantumProblem35.minor_matrix
Proof uses: Eq.mpr, id, Eq, congrArg, Eq.symm, OpenQuantumProblem35.minor_det_bridge_eq, ZMod.val, HMod.hMod, ZMod.val_natCast, Eq.mp, Nat.mod_mod, HAdd.hAdd, HMul.hMul, OpenQuantumProblem35.det4, HSub.hSub
37 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.explicit_sum_eq line 1460 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Fin, Eq, HAdd.hAdd, HMul.hMul, OpenQuantumProblem35.explicit_A, Finset.sum, Finset.univ, Matrix.vecCons, Nat.succ, Matrix.vecEmpty
Proof uses: Eq.symm, Fin.sum_univ_five
26 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.subset_rank_cond_from_minor line 1465 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, And, Ne, ZMod, Matrix.det, OpenQuantumProblem35.minor_matrix, OpenQuantumProblem35.subset_rank_cond_fn, OpenQuantumProblem35.explicit_A
Proof uses: id, Or, Decidable.byContradiction, Exists, HAdd.hAdd, HMul.hMul, Eq, Not, Matrix.vecCons, Matrix.vecEmpty, List, List.Mem, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, List.cons, List.Mem.head and 24 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 43 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.is_full_rank_M_implies line 1508 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Eq, Bool, OpenQuantumProblem35.is_full_rank_M, Bool.true, bne, OpenQuantumProblem35.det5, OpenQuantumProblem35.explicit_A_nat, OfNat.ofNat, Or
Proof uses: id, Bool.or, Eq.mpr, Not, congr, Ne, congrArg, Eq.mp, Eq.trans, Bool.or_eq_true, of_eq_true, True, False, eq_false, not_false_eq_true, true_or, or_true
9 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.subset_rank_cond_from_full_rank line 1525 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, And, Ne, Eq, Bool, OpenQuantumProblem35.is_full_rank_M, Bool.true, OpenQuantumProblem35.subset_rank_cond_fn, OpenQuantumProblem35.explicit_A
Proof uses: bne, OpenQuantumProblem35.det5, OpenQuantumProblem35.explicit_A_nat, Or, OpenQuantumProblem35.is_full_rank_M_implies, Iff, of_eq_true, Not, Eq.trans, True, congrArg, iff_self, Iff.mp, ZMod, Matrix.det, OpenQuantumProblem35.minor_matrix, OpenQuantumProblem35.minor_det_bridge, OpenQuantumProblem35.subset_rank_cond_from_minor
19 instances, coercions and auxiliary constants left out.

Tactic trace: 44 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.subset_rank_cond_swap02 line 1573 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Matrix, Fin, OfNat.ofNat, Nat, ZMod, OpenQuantumProblem35.subset_rank_cond_fn
Proof uses: OpenQuantumProblem35.subset_rank_cond_swap01, OpenQuantumProblem35.subset_rank_cond_swap12
2 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.subset_rank_cond_swap03 line 1578 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Matrix, Fin, OfNat.ofNat, Nat, ZMod, OpenQuantumProblem35.subset_rank_cond_fn
Proof uses: OpenQuantumProblem35.subset_rank_cond_swap02, OpenQuantumProblem35.subset_rank_cond_swap23
2 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.subset_rank_cond_swap04 line 1583 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Matrix, Fin, OfNat.ofNat, Nat, ZMod, OpenQuantumProblem35.subset_rank_cond_fn
Proof uses: OpenQuantumProblem35.subset_rank_cond_swap03, OpenQuantumProblem35.subset_rank_cond_swap34
2 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.subset_rank_cond_swap13 line 1588 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Matrix, Fin, OfNat.ofNat, Nat, ZMod, OpenQuantumProblem35.subset_rank_cond_fn
Proof uses: OpenQuantumProblem35.subset_rank_cond_swap12, OpenQuantumProblem35.subset_rank_cond_swap23
2 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.subset_rank_cond_swap14 line 1593 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Matrix, Fin, OfNat.ofNat, Nat, ZMod, OpenQuantumProblem35.subset_rank_cond_fn
Proof uses: OpenQuantumProblem35.subset_rank_cond_swap13, OpenQuantumProblem35.subset_rank_cond_swap34
2 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.subset_rank_cond_reverse line 1598 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Matrix, Fin, OfNat.ofNat, Nat, ZMod, OpenQuantumProblem35.subset_rank_cond_fn
Proof uses: OpenQuantumProblem35.subset_rank_cond_swap04, OpenQuantumProblem35.subset_rank_cond_swap13
2 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.order_2 line 1605 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, LE.le, OpenQuantumProblem35.subset_rank_cond_fn, OpenQuantumProblem35.explicit_A
Proof uses: Or, le_total, OpenQuantumProblem35.subset_rank_cond_swap01
11 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.order_3 line 1613 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, LE.le, OpenQuantumProblem35.subset_rank_cond_fn, OpenQuantumProblem35.explicit_A
Proof uses: OpenQuantumProblem35.order_2, Or, le_total, OpenQuantumProblem35.subset_rank_cond_swap12, OpenQuantumProblem35.subset_rank_cond_swap01
11 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.order_4 line 1625 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, LE.le, OpenQuantumProblem35.subset_rank_cond_fn, OpenQuantumProblem35.explicit_A
Proof uses: OpenQuantumProblem35.order_3, Or, le_total, OpenQuantumProblem35.subset_rank_cond_swap23, OpenQuantumProblem35.subset_rank_cond_swap12, OpenQuantumProblem35.subset_rank_cond_swap01
11 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.order_5 line 1640 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, LE.le, OpenQuantumProblem35.subset_rank_cond_fn, OpenQuantumProblem35.explicit_A
Proof uses: OpenQuantumProblem35.order_4, Or, le_total, OpenQuantumProblem35.subset_rank_cond_swap34, OpenQuantumProblem35.subset_rank_cond_swap23, OpenQuantumProblem35.subset_rank_cond_swap12, OpenQuantumProblem35.subset_rank_cond_swap01
11 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.get_cols_complement line 1658 source
standard axioms: Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, GT.gt, And, LT.lt, Prod.fst, Prod, OpenQuantumProblem35.get_cols, Prod.snd, Ne
Proof uses: Eq, Bool, OpenQuantumProblem35.loop_comp_f1, Bool.true, OpenQuantumProblem35.loop_comp_f0_implies, OpenQuantumProblem35.check_all_subsets_complement_eq_true, Fin.isLt, OpenQuantumProblem35.loop_comp_f2, OpenQuantumProblem35.loop_comp_f1_implies, OpenQuantumProblem35.loop_comp_f3, OpenQuantumProblem35.loop_comp_f2_implies, OpenQuantumProblem35.loop_comp_f4, OpenQuantumProblem35.loop_comp_f3_implies, OpenQuantumProblem35.get_cols_complement_bool, OpenQuantumProblem35.loop_comp_f4_implies, id, Bool.and, Decidable.decide, bne, OpenQuantumProblem35.get_cols_complement.match_1 and 8 more
11 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.explicit_A_subset_rank_cond_sorted line 1685 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, LT.lt, OpenQuantumProblem35.subset_rank_cond_fn, OpenQuantumProblem35.explicit_A
Proof uses: OpenQuantumProblem35.subset_rank_cond_reverse, Eq, Bool, OpenQuantumProblem35.subset_rank_cond_det_bool, Bool.true, OpenQuantumProblem35.check_all_subsets_det_implies, And, Prod.fst, Prod, OpenQuantumProblem35.get_cols, Prod.snd, Ne, OpenQuantumProblem35.get_cols_complement, rfl, Prod.mk, Eq.mp, congr, congrArg, Fin.mk, Eq.mpr and 6 more
9 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.explicit_A_subset_rank_cond line 1721 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, OpenQuantumProblem35.subset_rank_cond_fn, OpenQuantumProblem35.explicit_A
Proof uses: OpenQuantumProblem35.order_5, LE.le, Eq, LT.lt, Or, eq_or_lt_of_le, And, Ne, ZMod, Exists, HAdd.hAdd, HMul.hMul, Fin.ext, False.elim, OpenQuantumProblem35.explicit_A_subset_rank_cond_sorted
22 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.inj_leftIndex line 1747 source
no axioms what this means
Statement uses: Fin, OfNat.ofNat, Nat, Eq, OpenQuantumProblem35.leftIndex, of_decide_eq_true, LE.le, id, Bool, Decidable.decide, Bool.true, Eq.refl
Proof uses: congrArg, Fin.ext
7 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.rightIndex_of_not_leftIndex line 1753 source
standard axioms: Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Ne, OpenQuantumProblem35.leftIndex, of_decide_eq_true, LE.le, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, Exists, OpenQuantumProblem35.rightIndex
Proof uses: Decidable.byContradiction, Not, Fin.mk, Eq.mp, LT.lt, Fin.ext, Exists.intro, HSub.hSub, HAdd.hAdd
22 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.perm_rightIndex_of_not_f line 1767 source
standard axioms: Quot.sound, propext what this means
Statement uses: Equiv.Perm, Fin, OfNat.ofNat, Nat, Ne, Equiv, Equiv.symm, OpenQuantumProblem35.leftIndex, of_decide_eq_true, LE.le, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, Exists, OpenQuantumProblem35.rightIndex
Proof uses: Eq.mpr, congrArg, Eq.symm, Equiv.symm_apply_apply, OpenQuantumProblem35.rightIndex_of_not_leftIndex, Exists.intro
13 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.v_neq_zero line 1783 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: OpenQuantumProblem35.Config, OfNat.ofNat, Nat, Ne, Exists, Fin, ZMod, HSub.hSub
Proof uses: Decidable.byContradiction, Eq, Not, funext, Fin.ext, Eq.mp, Eq.trans, binderNameHint, forall_congr, Iff.mp, sub_eq_zero, by_contra, Function.comp, False, absurd, LT.lt, Fin.mk, of_decide_eq_true, id, Bool and 4 more
53 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.explicit_A_rank line 1792 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: OpenQuantumProblem35.rankCondition, OfNat.ofNat, Nat, of_decide_eq_true, LE.le, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, OpenQuantumProblem35.explicit_A
Proof uses: Equiv.Perm, Fin, OpenQuantumProblem35.Config, Ne, Equiv, Equiv.symm, OpenQuantumProblem35.leftIndex, And, Equiv.injective, OpenQuantumProblem35.inj_leftIndex, And.intro, ZMod, HSub.hSub, Exists, OpenQuantumProblem35.v_neq_zero, Or, Not, HAdd.hAdd, Eq.mp, Eq.trans and 21 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 57 steps
Open to load the checked before-and-after goal states.
def OpenQuantumProblem35.graphStateAmp line 1835 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Matrix, Fin, ZMod, OfNat.ofNat, OpenQuantumProblem35.Config, Complex
Proof uses: Finset.sum, Finset.univ, HMul.hMul, HPow.hPow, OpenQuantumProblem35.omega5, ZMod.val
23 instances, coercions and auxiliary constants left out.
def OpenQuantumProblem35.graphState line 1840 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Matrix, Fin, ZMod, OfNat.ofNat, OpenQuantumProblem35.StateVector
Proof uses: Complex, Inv.inv, Real.sqrt, HPow.hPow, Real, OpenQuantumProblem35.mkStateVector, OpenQuantumProblem35.Config, HMul.hMul, OpenQuantumProblem35.graphStateAmp
12 instances, coercions and auxiliary constants left out.
lemma OpenQuantumProblem35.graph_state_is_normalized line 1844 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Matrix, Fin, ZMod, OfNat.ofNat, OpenQuantumProblem35.IsNormalized, OpenQuantumProblem35.graphState
Proof uses: id, OpenQuantumProblem35.StateVector, Complex, Inv.inv, Real.sqrt, HPow.hPow, Real, OpenQuantumProblem35.mkStateVector, OpenQuantumProblem35.Config, HMul.hMul, OpenQuantumProblem35.graphStateAmp, Eq, Norm.norm, ENNReal, Eq.mpr, WithLp.toLp, Finset.sum, Finset.univ, Eq.trans, EuclideanSpace and 82 more
151 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
def OpenQuantumProblem35.shiftEquiv line 1855 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Fin, Equiv, OfNat.ofNat
Proof uses: Equiv.mk, ite, Eq, HAdd.hAdd, HSub.hSub
11 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.sum_shift_eq line 1861 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, OfNat.ofNat, Complex, Eq, Finset.sum, Finset.univ, Equiv, OpenQuantumProblem35.shiftEquiv
Proof uses: Eq.symm, Equiv.sum_comp
36 instances, coercions and auxiliary constants left out.
lemma OpenQuantumProblem35.sum_omega5_shift_zero line 1865 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, ZMod, OfNat.ofNat, Ne, Complex, Eq, Equiv, OpenQuantumProblem35.shiftEquiv, HMul.hMul, HPow.hPow, OpenQuantumProblem35.omega5, ZMod.val, Finset.sum, Finset.univ
Proof uses: OpenQuantumProblem35.sum_shift_eq, Eq.mpr, id, congrArg, Finset.sum_mul, of_eq_true, Eq.trans, True, Finset.sum_congr, Eq.refl, Finset, Membership.mem, eq_self, HSub.hSub, Mathlib.Tactic.LinearCombination.eq_of_eq, HAdd.hAdd, Mathlib.Tactic.LinearCombination.add_eq_eq, Mathlib.Tactic.LinearCombination.eq_rearrange, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.sub_congr and 70 more
130 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.graphState_norm_sq_any line 1878 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Matrix, Fin, ZMod, OfNat.ofNat, OpenQuantumProblem35.Config, Eq, Complex, HMul.hMul, WithLp.ofLp, ENNReal, OpenQuantumProblem35.graphState, Star.star, HDiv.hDiv, HPow.hPow
Proof uses: id, Eq.mpr, Equiv, Real, Matrix.of, Complex.mk, HSub.hSub, Complex.re, Inv.inv, Real.sqrt, OpenQuantumProblem35.graphStateAmp, Complex.im, HAdd.hAdd, congr, congrArg, Eq.trans, MonoidWithZeroHom, Complex.normSq, Complex.inv_re, Complex.normSq_ofReal and 72 more
203 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.shiftEquiv_val line 1887 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, OfNat.ofNat, Eq, ZMod, Equiv, OpenQuantumProblem35.shiftEquiv, ite, HAdd.hAdd
Proof uses: id, Not, Or, em, Or.inl, of_eq_true, Eq.trans, True, congr, congrArg, Fin.last, ite_cond_eq_true, eq_self, Fin.val_add_one, ite_congr, Eq.refl, Nat.cast_ite, Nat.cast_zero, Nat.cast_add, Fin.NatCast.instNatCast and 8 more
56 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.permute_combine_shift line 1893 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Equiv.Perm, Fin, OpenQuantumProblem35.Config, OfNat.ofNat, HSub.hSub, Eq, ZMod, OpenQuantumProblem35.permuteConfig, OpenQuantumProblem35.combineFirst, Equiv, OpenQuantumProblem35.shiftEquiv, ite, Equiv.symm, OpenQuantumProblem35.rightIndex, HAdd.hAdd
Proof uses: Or, Ne, Classical.em, Or.inl, Eq.mpr, id, congrArg, Equiv.apply_symm_apply, Eq.refl, if_pos, OpenQuantumProblem35.combineFirst_rightIndex, OpenQuantumProblem35.shiftEquiv_val, Eq.mp, rfl, Or.inr, Equiv.injective, of_eq_true, Eq.trans, True, congr and 10 more
56 instances, coercions and auxiliary constants left out.

Tactic trace: 43 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.quad_form_shift line 1938 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Matrix, Fin, ZMod, OfNat.ofNat, Eq, Finset.sum, Finset.univ, HMul.hMul, ite, HAdd.hAdd
Proof uses: Eq.mpr, HSub.hSub, id, congr, congrArg, Eq.trans, Finset.sum_congr, Eq.refl, Finset, Membership.mem, Finset.filter, Not, mul_ite, ite_congr, mul_add, mul_one, mul_comm, Finset.sum_ite, Singleton.singleton, EmptyCollection.emptyCollection and 40 more
91 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.graphState_eval_eq line 1947 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Matrix, Fin, ZMod, OfNat.ofNat, OpenQuantumProblem35.Config, Eq, Complex, WithLp.ofLp, ENNReal, OpenQuantumProblem35.graphState, HMul.hMul, Inv.inv, Real.sqrt, HPow.hPow, Real, OpenQuantumProblem35.omega5, ZMod.val, Finset.sum, Finset.univ
Proof uses: rfl
39 instances, coercions and auxiliary constants left out.
lemma OpenQuantumProblem35.quad_form_shift_symm line 1950 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Matrix, Fin, ZMod, OfNat.ofNat, Eq, Matrix.transpose, Finset.sum, Finset.univ, HMul.hMul, ite, HAdd.hAdd
Proof uses: Eq.mpr, HSub.hSub, id, congr, congrArg, Eq.trans, Finset.sum_congr, Eq.refl, Finset, Membership.mem, Finset.filter, Not, mul_ite, ite_congr, mul_add, mul_one, mul_comm, Finset.sum_ite, Singleton.singleton, EmptyCollection.emptyCollection and 44 more
103 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.sum_A_v_diff_split line 1956 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Matrix, Fin, ZMod, OfNat.ofNat, LE.le, Equiv.Perm, OpenQuantumProblem35.Config, HSub.hSub, Eq, Finset.sum, Finset.univ, HMul.hMul, Equiv, Equiv.symm, OpenQuantumProblem35.rightIndex, OpenQuantumProblem35.permuteConfig, OpenQuantumProblem35.combineFirst, HAdd.hAdd, OpenQuantumProblem35.leftIndex
Proof uses: id, Eq.mpr, Fin.mk, Decidable.rec, LT.lt, Decidable, Not, Fin.isLt, congr, congrArg, Finset.sum_congr, Eq.refl, Finset, Membership.mem, Nat.succ, Eq.symm, Equiv.sum_comp, Finset.range, dite, Eq.mpr_prop and 34 more
99 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.sum_A_v_diff line 1967 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Matrix, Fin, ZMod, OfNat.ofNat, LE.le, Equiv.Perm, OpenQuantumProblem35.Config, HSub.hSub, Eq, Finset.sum, Finset.univ, HMul.hMul, Equiv, Equiv.symm, OpenQuantumProblem35.rightIndex, OpenQuantumProblem35.permuteConfig, OpenQuantumProblem35.combineFirst, OpenQuantumProblem35.submatrix
Proof uses: Eq.mpr, HAdd.hAdd, OpenQuantumProblem35.leftIndex, id, congrArg, OpenQuantumProblem35.sum_A_v_diff_split, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.sub_congr, Mathlib.Tactic.Ring.add_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.add_pf_add_lt, Mathlib.Tactic.Ring.add_pf_zero_add, Mathlib.Tactic.Ring.add_pf_add_gt, Mathlib.Tactic.Ring.add_pf_add_zero, Mathlib.Tactic.Ring.sub_pf and 27 more
81 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.omega5_add line 1992 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Eq, Complex, HPow.hPow, OpenQuantumProblem35.omega5, ZMod.val, HAdd.hAdd, HMul.hMul
Proof uses: id, Eq.trans, Complex.exp, HDiv.hDiv, Real.pi, Complex.I, HMod.hMod, Eq.symm, pow_eq_pow_mod, IsPrimitiveRoot.pow_eq_one, Complex.isPrimitiveRoot_exp, of_decide_eq_true, Ne, Bool, Decidable.decide, Bool.true, Eq.refl, pow_add
52 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.omega5_sub line 1996 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: ZMod, OfNat.ofNat, Nat, Eq, Complex, HPow.hPow, OpenQuantumProblem35.omega5, ZMod.val, HSub.hSub, HMul.hMul, Star.star
Proof uses: Eq.mpr, id, congrArg, star_pow, HAdd.hAdd, Neg.neg, sub_eq_add_neg, HMod.hMod, ZMod.val_add, Complex.exp, HDiv.hDiv, Real.pi, Complex.I, ite, ZMod.cast, congr, RingHom, starRingEnd, Eq.trans, ZMod.neg_val and 97 more
157 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.graphState_apply_eq line 2002 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Matrix, Fin, ZMod, OfNat.ofNat, OpenQuantumProblem35.Config, Eq, Complex, WithLp.ofLp, ENNReal, OpenQuantumProblem35.graphState, HMul.hMul, Inv.inv, Real.sqrt, HPow.hPow, Real, OpenQuantumProblem35.graphStateAmp
Proof uses: rfl
22 instances, coercions and auxiliary constants left out.
lemma OpenQuantumProblem35.graphStateAmp_shift line 2005 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Matrix, Fin, ZMod, OfNat.ofNat, Eq, Matrix.transpose, LE.le, Equiv.Perm, OpenQuantumProblem35.Config, HSub.hSub, Complex, OpenQuantumProblem35.graphStateAmp, OpenQuantumProblem35.permuteConfig, OpenQuantumProblem35.combineFirst, Equiv, OpenQuantumProblem35.shiftEquiv, HMul.hMul, HPow.hPow, OpenQuantumProblem35.omega5 and 5 more
Proof uses: ite, HAdd.hAdd, OpenQuantumProblem35.permute_combine_shift, OpenQuantumProblem35.quad_form_shift_symm, funext, AddCommMonoid, Finset, Eq.rec, Eq.refl, Eq.mpr, id, congrArg, congr_fun, OpenQuantumProblem35.omega5_add
75 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.graph_state_shift_prop line 2032 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Matrix, Fin, ZMod, OfNat.ofNat, Eq, Matrix.transpose, LE.le, Equiv.Perm, OpenQuantumProblem35.Config, HSub.hSub, Complex, OpenQuantumProblem35.combineFirst, Equiv, OpenQuantumProblem35.shiftEquiv, HMul.hMul, WithLp.ofLp, ENNReal, OpenQuantumProblem35.permuteState, OpenQuantumProblem35.graphState and 7 more
Proof uses: OpenQuantumProblem35.graphStateAmp, OpenQuantumProblem35.permuteConfig, Equiv.symm, OpenQuantumProblem35.rightIndex, OpenQuantumProblem35.graphStateAmp_shift, OpenQuantumProblem35.sum_A_v_diff, Eq.mpr, Inv.inv, Real.sqrt, Real, id, congr, congrArg, OpenQuantumProblem35.permuteState_apply, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.inv_congr and 47 more
129 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.graph_state_off_diag_zero line 2072 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Matrix, Fin, ZMod, OfNat.ofNat, Eq, Matrix.transpose, LE.le, Equiv.Perm, OpenQuantumProblem35.Config, Exists, HSub.hSub, Ne, Finset.sum, Finset.univ, HMul.hMul, OpenQuantumProblem35.submatrix, Complex, OpenQuantumProblem35.reducedDensityFirst, OpenQuantumProblem35.permuteState and 1 more
Proof uses: id, OpenQuantumProblem35.combineFirst, WithLp.ofLp, ENNReal, Star.star, Equiv, OpenQuantumProblem35.shiftEquiv, HPow.hPow, OpenQuantumProblem35.omega5, ZMod.val, OpenQuantumProblem35.graph_state_shift_prop, Function.comp, Not, Fact, Nat.Prime, False, absurd, Fact.mk, Nat.prime_five, mul_ne_zero and 6 more
99 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.graph_state_maximally_mixed line 2084 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Matrix, Fin, OfNat.ofNat, Nat, ZMod, Eq, Matrix.transpose, OpenQuantumProblem35.rankCondition, of_decide_eq_true, LE.le, id, Bool, Decidable.decide, Bool.true, Eq.refl, Equiv.Perm, OpenQuantumProblem35.HasMaximallyMixedFirstReduction, OpenQuantumProblem35.permuteState, OpenQuantumProblem35.graphState
Proof uses: Matrix.ext, OpenQuantumProblem35.Config, Complex, OpenQuantumProblem35.reducedDensityFirst, OpenQuantumProblem35.maximallyMixed, dite, HDiv.hDiv, HPow.hPow, HSMul.hSMul, Inv.inv, Fintype.card, Eq.mpr, HMul.hMul, Eq.trans, congr, congrArg, Finset.prod, Finset.univ, Fintype.card_pi, Finset.card and 68 more
121 instances, coercions and auxiliary constants left out.

Tactic trace: 50 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.explicit_A_symm line 2127 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Matrix, Fin, OfNat.ofNat, Nat, ZMod, Matrix.transpose, OpenQuantumProblem35.explicit_A
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
5 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.explicit_A_diag line 2128 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fin, OfNat.ofNat, Nat, Eq, ZMod, OpenQuantumProblem35.explicit_A
Proof uses: of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl
20 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.ame_matrix_implies_ame_state line 2130 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Matrix, Fin, OfNat.ofNat, Nat, ZMod, Eq, Matrix.transpose, OpenQuantumProblem35.rankCondition, of_decide_eq_true, LE.le, id, Bool, Decidable.decide, Bool.true, Eq.refl, OpenQuantumProblem35.IsAME, OpenQuantumProblem35.graphState
Proof uses: And.intro, OpenQuantumProblem35.IsNormalized, Equiv.Perm, OpenQuantumProblem35.HasMaximallyMixedFirstReduction, HDiv.hDiv, OpenQuantumProblem35.permuteState, OpenQuantumProblem35.graph_state_is_normalized, OpenQuantumProblem35.graph_state_maximally_mixed
25 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma OpenQuantumProblem35.yes_AME_11_5 line 2138 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: OpenQuantumProblem35.ExistsAME, OfNat.ofNat, Nat
Proof uses: Exists.intro, OpenQuantumProblem35.StateVector, OpenQuantumProblem35.IsAME, OpenQuantumProblem35.graphState, OpenQuantumProblem35.explicit_A, OpenQuantumProblem35.ame_matrix_implies_ame_state, OpenQuantumProblem35.explicit_A_symm, OpenQuantumProblem35.explicit_A_diag, OpenQuantumProblem35.explicit_A_rank
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 An explicit absolutely maximally entangled state for 11 five-level parties line 2147 source
Source documentation
Open benchmark statement: does an $\mathrm{AME}(11,5)$ state exist?
The DeepMind prover agent has shown that such a state exists.
L4DEL explanation
AME states are characterized by being maximally entangled for all bipartitions of the system
— Wolfram Helwig et al., Absolute Maximal Entanglement and Quantum Secret Sharing (2012)
AlphaProof Nexus indeed did find a new AME state AME(11,5). However, it turned out that the underlying Quantum Code was already discovered 2 years ago
— Mario Krenn's account of the Nexus quantum-optics results and priority correction
There exists a normalized pure state of 11 parties, each with local dimension 5, whose reduced density matrix on every choice of 5 parties is maximally mixed. The theorem is an existence result with a fully explicit graph-state witness; it does not claim that this is the first mathematical construction of the underlying quantum code.
1. explicit_A is an 11-by-11 symmetric, zero-diagonal circulant matrix over ZMod 5, built from the row [0,0,0,1,2,2,2,2,1,0,0].
2. The finite explicit_A_rank computation proves that, after every permutation of the parties, distinct configurations on the first five parties are separated by at least one of the remaining six columns.
3. That rank condition makes the off-diagonal entries of every five-party reduced density matrix vanish; normalization and the diagonal calculation identify the whole reduction with the maximally mixed matrix.
4. yes_AME_11_5 supplies graphState explicit_A as the witness, and ame_11_5_open packages the result as answer(True) ↔ ExistsAME 11 5 without using sorry in this declaration.
5. Priority boundary: Mario Krenn's public account says AlphaProof Nexus found this AME state but also records that the underlying quantum code had already been discovered two years earlier. This annotation therefore credits the checked construction without calling it a first discovery.
Sources and attribution: Pinned Lean source (0647711a7118), Wolfram Helwig et al., Absolute Maximal Entanglement and Quantum Secret Sharing (2012), Open Quantum Problems, Problem 35, Mario Krenn's account of the Nexus quantum-optics results and priority correction
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Iff, True, OpenQuantumProblem35.ExistsAME, OfNat.ofNat, Nat
Proof uses: Iff.intro, OpenQuantumProblem35.yes_AME_11_5, True.intro
2 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
theorem ame_11_5_open :
    answer(True) ↔ ExistsAME 11 5 := by
…
```
Mentions: OpenQuantumProblem35.ExistsAME
theorem OpenQuantumProblem35.ame_11_6_open Open benchmark statement: does an $\mathrm{AME}(11,6)$ state exist? sorry line 2159 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 Open benchmark statement: does an $\mathrm{AME}(11,10)$ state exist? sorry line 2165 source
Source documentation
Open benchmark statement: does an $\mathrm{AME}(11,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_11_10_open :
    answer(sorry) ↔ ExistsAME 11 10 := by
…
```
Mentions: OpenQuantumProblem35.ExistsAME
theorem OpenQuantumProblem35.ame_12_5_open Open benchmark statement: does an $\mathrm{AME}(12,5)$ state exist? sorry line 2171 source
Source documentation
Open benchmark statement: does an $\mathrm{AME}(12,5)$ 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_5_open :
    answer(sorry) ↔ 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 2177 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 2183 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 2191 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, setOf, 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