ConstructionReduction

Abstract

Public declarations of ConstructionReduction, with complete parameters and the Lean operations.

Theorem 1.1 (Block diagonal matrix-vector action).

$$\forall (\iota :Type\ast ),[\mathrm{Fintype}\iota ][\mathrm{DecidableEq}\iota ]\forall (\kappa :\iota \to Type\ast ),[\forall i,\mathrm{Fintype}(\kappa i)][\forall i,\mathrm{DecidableEq}(\kappa i)]\forall (M:\forall i,\mathrm{Matrix}(\kappa i)(\kappa i)\mathbb{C}),\forall (v:(\Sigma i,\kappa i)\to \mathbb{C}),\forall (i:\iota ),\forall (j:(\kappa i)),(\mathrm{Matrix}.{\mathrm{blockDiagonal}}^{\prime }\left(M\right).\mathrm{mulVec})v⟨i,j⟩=((Mi).\mathrm{mulVec})(\mathrm{fun}k\mapsto v⟨i,k⟩)j$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.mulVec_block (✓ std3). ∎

Source. Repository-derived.

Commentary.

The matrix-vector action of Matrix.blockDiagonal’ on a dependent-sum coordinate is the action of the corresponding block on that coordinate.

Definition 1.2 (phaseAt).

$$\forall (n:\mathbb{N}),\forall (a:Finn\to \mathbb{C}),\forall (j:\mathbb{N}),\mathrm{phaseAt}aj=(ifh:j-1<n\mathrm{then}a⟨j-1,h⟩\mathrm{else}1)$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.phaseAt (✓ std3).

Citation. J. Choi, Y.-H. Kiem, and S.-H. Kye (2020). Entangled edge states of corank one with positive partial transposes. DOI: 10.1063/1.5122836. URL: https://arxiv.org/abs/1903.10745v2.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion.

Definition 1.3 (pEntry).

$$\forall (d:\mathbb{N}),\forall (z:\mathbb{N}\to \mathbb{C}),\forall (i:\mathbb{N}),\forall (j:\mathbb{N}),\mathrm{pEntry}dzij=(ifi=j\mathrm{then}ifd=2\mathrm{then}1\mathrm{else}2\mathrm{else}ifj=i+1\mathrm{then}zj\mathrm{HDiv}.\mathrm{hDiv}zi\mathrm{else}ifi=j+1\mathrm{then}zj\mathrm{HDiv}.\mathrm{hDiv}zi\mathrm{else}ifi=0\wedge j+1=d\mathrm{then}zj\mathrm{else}ifj=0\wedge i+1=d\mathrm{then}((zi){)}^{-1}\mathrm{else}0)$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.pEntry (✓ std3).

Citation. J. Choi, Y.-H. Kiem, and S.-H. Kye (2020). Entangled edge states of corank one with positive partial transposes. DOI: 10.1063/1.5122836. URL: https://arxiv.org/abs/1903.10745v2.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion.

Definition 1.4 (P).

$$\forall (d:\mathbb{N}),\forall (z:\mathbb{N}\to \mathbb{C}),Pdz=(\lambda (ij:Find)\mapsto \mathrm{ConstructionReduction}.\mathrm{pEntry}dz\mathrm{val}\left(i\right)\mathrm{val}\left(j\right))$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.P (✓ std3).

Citation. J. Choi, Y.-H. Kiem, and S.-H. Kye (2020). Entangled edge states of corank one with positive partial transposes. DOI: 10.1063/1.5122836. URL: https://arxiv.org/abs/1903.10745v2.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion.

Definition 1.5 (alphaUpper).

$$\forall (k:\mathbb{N}),\mathrm{alphaUpper}k=(\mathrm{List}.map(\lambda (j:\mathbb{N})\mapsto (j+1,k-j))(\mathrm{List}.\mathrm{range}(k\mathrm{HDiv}.\mathrm{hDiv}2)))$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.alphaUpper (✓ std3).

Citation. J. Choi, Y.-H. Kiem, and S.-H. Kye (2020). Entangled edge states of corank one with positive partial transposes. DOI: 10.1063/1.5122836. URL: https://arxiv.org/abs/1903.10745v2.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion.

Definition 1.6 (betaUpper).

$$\forall (n:\mathbb{N}),\forall (l:\mathbb{N}),\mathrm{betaUpper}nl=(\mathrm{List}.map(\lambda (j:\mathbb{N})\mapsto (l+j,n-j))(\mathrm{List}.\mathrm{range}((n-l+1)\mathrm{HDiv}.\mathrm{hDiv}2)))$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.betaUpper (✓ std3).

Citation. J. Choi, Y.-H. Kiem, and S.-H. Kye (2020). Entangled edge states of corank one with positive partial transposes. DOI: 10.1063/1.5122836. URL: https://arxiv.org/abs/1903.10745v2.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion.

Definition 1.7 (indexList).

$$\forall (\mathrm{upper}:\mathrm{List}(\mathbb{N}\times \mathbb{N})),\mathrm{indexList}\mathrm{upper}=(\mathrm{upper}++\mathrm{List}.map\mathrm{Prod}.\mathrm{swap}\mathrm{upper}.\mathrm{reverse})$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.indexList (✓ std3).

Citation. J. Choi, Y.-H. Kiem, and S.-H. Kye (2020). Entangled edge states of corank one with positive partial transposes. DOI: 10.1063/1.5122836. URL: https://arxiv.org/abs/1903.10745v2.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion.

Definition 1.8 (blockZ).

$$\forall (n:\mathbb{N}),\forall (a:Finn\to \mathbb{C}),\forall (\mathrm{upper}:\mathrm{List}(\mathbb{N}\times \mathbb{N})),\forall (j:\mathbb{N}),\mathrm{blockZ}a\mathrm{upper}j=(ifj<\mathrm{upper}.\mathrm{length}\mathrm{then}1\mathrm{else}ifj<(\mathrm{ConstructionReduction}.\mathrm{indexList}\mathrm{upper}).\mathrm{length}\mathrm{then}((\mathrm{ConstructionReduction}.\mathrm{phaseAt}a((\mathrm{ConstructionReduction}.\mathrm{indexList}\mathrm{upper})[j]).2){)}^{-1}\cdot \mathrm{ConstructionReduction}.\mathrm{phaseAt}a((\mathrm{ConstructionReduction}.\mathrm{indexList}\mathrm{upper})[j]).1\mathrm{else}1)$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.blockZ (✓ std3).

Citation. J. Choi, Y.-H. Kiem, and S.-H. Kye (2020). Entangled edge states of corank one with positive partial transposes. DOI: 10.1063/1.5122836. URL: https://arxiv.org/abs/1903.10745v2.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion. Optional list indexing is expanded into its defining in-bounds and out-of-bounds branches.

Definition 1.9 (blockEntry).

$$\forall (n:\mathbb{N}),\forall (a:Finn\to \mathbb{C}),\forall (\mathrm{upper}:\mathrm{List}(\mathbb{N}\times \mathbb{N})),\forall (\mathrm{scale}:\mathbb{C}),\forall (row:Finn\times Finn),\forall (col:Finn\times Finn),\mathrm{blockEntry}a\mathrm{upper}\mathrm{scale}rowcol=(\mathrm{have}\mathrm{indices}:=\mathrm{ConstructionReduction}.\mathrm{indexList}\mathrm{upper};\mathrm{have}rr:=(\mathrm{val}\left(row.1\right)+1,\mathrm{val}\left(row.2\right)+1);\mathrm{have}cc:=(\mathrm{val}\left(col.1\right)+1,\mathrm{val}\left(col.2\right)+1);ifrr\in \mathrm{indices}\wedge cc\in \mathrm{indices}\mathrm{then}\mathrm{scale}\cdot \mathrm{ConstructionReduction}.\mathrm{pEntry}\mathrm{indices}.\mathrm{length}(\mathrm{ConstructionReduction}.\mathrm{blockZ}a\mathrm{upper})(\mathrm{List}.\mathrm{idxOf}rr\mathrm{indices})(\mathrm{List}.\mathrm{idxOf}cc\mathrm{indices})\mathrm{else}0)$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.blockEntry (✓ std3).

Citation. J. Choi, Y.-H. Kiem, and S.-H. Kye (2020). Entangled edge states of corank one with positive partial transposes. DOI: 10.1063/1.5122836. URL: https://arxiv.org/abs/1903.10745v2.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion.

Definition 1.10 (rhoGamma).

$$\forall (n:\mathbb{N}),\forall (a:Finn\to \mathbb{C}),\forall (b:Finn\to \mathbb{C}),\forall (r:\mathbb{R}),\mathrm{rhoGamma}abr=(\lambda (rowcol:Finn\times Finn)\mapsto (ifrow.1=row.2\wedge row=col\mathrm{then}(r:\mathbb{C})\mathrm{else}0)+\mathrm{blockEntry}a[(1,2)]1rowcol+\mathrm{blockEntry}a[(1,3)]2rowcol+(\sum (k:\mathbb{N})\in \mathrm{Finset}.\mathrm{range}(n+1),if4\le k\mathrm{then}\mathrm{blockEntry}a(\mathrm{alphaUpper}k)1rowcol\mathrm{else}0)+(\sum (l:\mathbb{N})\in \mathrm{Finset}.\mathrm{range}(n+1),if2\le l\wedge l+3\le n\mathrm{then}\mathrm{blockEntry}b(\mathrm{betaUpper}nl)1rowcol\mathrm{else}0)+(if3<n\mathrm{then}\mathrm{blockEntry}b[(n-2,n)]2rowcol\mathrm{else}0)+\mathrm{blockEntry}b[(n-1,n)]1rowcol)$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.rhoGamma (✓ std3).

Citation. J. Choi, Y.-H. Kiem, and S.-H. Kye (2020). Entangled edge states of corank one with positive partial transposes. DOI: 10.1063/1.5122836. URL: https://arxiv.org/abs/1903.10745v2.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion.

Definition 1.11 (partialTranspose).

$$\forall (n:\mathbb{N}),\forall (A:\mathrm{Matrix}(Finn\times Finn)(Finn\times Finn)\mathbb{C}),\mathrm{partialTranspose}A=(D5.S3.\mathrm{Quantum}.\mathrm{Entanglement}.\mathrm{StructuredNegativityCoincidenceRefutation}.\mathrm{partialTransposeB}A.\mathrm{transpose})$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.partialTranspose (✓ std3).

Citation. J. Choi, Y.-H. Kiem, and S.-H. Kye (2020). Entangled edge states of corank one with positive partial transposes. DOI: 10.1063/1.5122836. URL: https://arxiv.org/abs/1903.10745v2.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion. Source, p. 1, verbatim: “The partial transpose (x ⊗ y)Γ of x ⊗ y ∈ Mₘ ⊗ Mₙ is given by xᵗ ⊗ y with the usual transpose xᵗ.” In the bound matrix carrier the entry at ((i,j),(k,l)) is A ((k,j),(i,l)); the frozen second-factor operation is applied to the ordinary transpose to obtain precisely this first-factor operation.

Definition 1.12 (rho).

$$\forall (n:\mathbb{N}),\forall (a:Finn\to \mathbb{C}),\forall (b:Finn\to \mathbb{C}),\forall (r:\mathbb{R}),rhoabr=(\mathrm{ConstructionReduction}.\mathrm{partialTranspose}(\mathrm{ConstructionReduction}.\mathrm{rhoGamma}abr))$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.rho (✓ std3).

Citation. J. Choi, Y.-H. Kiem, and S.-H. Kye (2020). Entangled edge states of corank one with positive partial transposes. DOI: 10.1063/1.5122836. URL: https://arxiv.org/abs/1903.10745v2.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion.

Definition 1.13 (D).

$$\forall (n:\mathbb{N}),\forall (a:Finn\to \mathbb{C}),\forall (b:Finn\to \mathbb{C}),\forall (r:\mathbb{R}),Dabr=(\lambda (ij:Finn)\mapsto ifi=j\mathrm{then}\mathrm{val}\left(r\right)\mathrm{else}if\mathrm{val}\left(i\right)=0\mathrm{then}(if\mathrm{val}\left(j\right)=2\mathrm{then}2\mathrm{else}1)\cdot (\mathrm{starRingEnd}\mathbb{C})(aj)\mathrm{else}if\mathrm{val}\left(j\right)=0\mathrm{then}(if\mathrm{val}\left(i\right)=2\mathrm{then}2\mathrm{else}1)\cdot ai\mathrm{else}if\mathrm{val}\left(j\right)+1=n\mathrm{then}(if\mathrm{val}\left(i\right)+3=n\mathrm{then}2\mathrm{else}1)\cdot bi\mathrm{else}if\mathrm{val}\left(i\right)+1=n\mathrm{then}(if\mathrm{val}\left(j\right)+3=n\mathrm{then}2\mathrm{else}1)\cdot (\mathrm{starRingEnd}\mathbb{C})(bj)\mathrm{else}if\mathrm{val}\left(i\right)+1=\mathrm{val}\left(j\right)\vee \mathrm{val}\left(j\right)+1=\mathrm{val}\left(i\right)\vee \mathrm{val}\left(i\right)+2=\mathrm{val}\left(j\right)\vee \mathrm{val}\left(j\right)+2=\mathrm{val}\left(i\right)\mathrm{then}if\mathrm{val}\left(i\right)+\mathrm{val}\left(j\right)+1\le n\mathrm{then}ai\cdot (\mathrm{starRingEnd}\mathbb{C})(aj)\mathrm{else}bi\cdot (\mathrm{starRingEnd}\mathbb{C})(bj)\mathrm{else}0)$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.D (✓ std3).

Citation. J. Choi, Y.-H. Kiem, and S.-H. Kye (2020). Entangled edge states of corank one with positive partial transposes. DOI: 10.1063/1.5122836. URL: https://arxiv.org/abs/1903.10745v2.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion.

Definition 1.14 (tensor).

$$\forall (n:\mathbb{N}),\forall (x:Finn\to \mathbb{C}),\forall (y:Finn\to \mathbb{C}),\forall (a:Finn\times Finn),\mathrm{tensor}xya=(\mathrm{Matrix}.\mathrm{vecMulVec}xya.1a.2)$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.tensor (✓ std3).

Citation. J. Choi, Y.-H. Kiem, and S.-H. Kye (2020). Entangled edge states of corank one with positive partial transposes. DOI: 10.1063/1.5122836. URL: https://arxiv.org/abs/1903.10745v2.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion.

Definition 1.15 (InRange).

$$\forall (n:\mathbb{N}),\forall (A:\mathrm{Matrix}(Finn\times Finn)(Finn\times Finn)\mathbb{C}),\forall (v:Finn\times Finn\to \mathbb{C}),\mathrm{InRange}Av=(v\in A.\mathrm{mulVecLin}.\mathrm{range})$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.InRange (✓ std3).

Citation. J. Choi, Y.-H. Kiem, and S.-H. Kye (2020). Entangled edge states of corank one with positive partial transposes. DOI: 10.1063/1.5122836. URL: https://arxiv.org/abs/1903.10745v2.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion.

Definition 1.16 (PPT).

$$\forall (n:\mathbb{N}),\forall (A:\mathrm{Matrix}(Finn\times Finn)(Finn\times Finn)\mathbb{C}),PPTA=(A.\mathrm{PosSemidef}\wedge (\mathrm{ConstructionReduction}.\mathrm{partialTranspose}A).\mathrm{PosSemidef})$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.PPT (✓ std3).

Citation. J. Choi, Y.-H. Kiem, and S.-H. Kye (2020). Entangled edge states of corank one with positive partial transposes. DOI: 10.1063/1.5122836. URL: https://arxiv.org/abs/1903.10745v2.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion.

Definition 1.17 (Edge).

$$\forall (n:\mathbb{N}),\forall (A:\mathrm{Matrix}(Finn\times Finn)(Finn\times Finn)\mathbb{C}),\mathrm{Edge}A=(\forall (xy:Finn\to \mathbb{C}),x\ne 0\to y\ne 0\to \neg (\mathrm{ConstructionReduction}.\mathrm{InRange}A(\mathrm{ConstructionReduction}.\mathrm{tensor}xy)\wedge \mathrm{ConstructionReduction}.\mathrm{InRange}(\mathrm{ConstructionReduction}.\mathrm{partialTranspose}A)(\mathrm{ConstructionReduction}.\mathrm{tensor}(\lambda (i:Finn)\mapsto (\mathrm{starRingEnd}\mathbb{C})(xi))y)))$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.Edge (✓ std3).

Citation. J. Choi, Y.-H. Kiem, and S.-H. Kye (2020). Entangled edge states of corank one with positive partial transposes. DOI: 10.1063/1.5122836. URL: https://arxiv.org/abs/1903.10745v2.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion. Source, p. 1, verbatim: “There exists no nonzero product vector |ξᵢ⟩ ⊗ |ηᵢ⟩ ∈ Im ϱ such that |ξ̄ᵢ⟩ ⊗ |ηᵢ⟩ ∈ Im ϱΓ. Such states are called PPT entangled edge states [19], in short, edge states in this paper.” The predicate encodes the range exclusion; PPT and nonzeroness are separate conjuncts of Full.claim.

Definition 1.18 (GenericPhases).

$$\forall (n:\mathbb{N}),\forall (a:Finn\to \mathbb{C}),\forall (b:Finn\to \mathbb{C}),\mathrm{GenericPhases}ab=((\forall (i:Finn),ai\ne 0\wedge bi\ne 0)\wedge (\forall (ij:Finn),i<j\to ((ai){)}^{-1}\cdot aj\ne ((bi){)}^{-1}\cdot bj))$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.GenericPhases (✓ std3).

Citation. J. Choi, Y.-H. Kiem, and S.-H. Kye (2020). Entangled edge states of corank one with positive partial transposes. DOI: 10.1063/1.5122836. URL: https://arxiv.org/abs/1903.10745v2.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion.

Definition 1.19 (Admissible).

$$\forall (n:\mathbb{N}),\forall (a:Finn\to \mathbb{C}),\forall (b:Finn\to \mathbb{C}),\mathrm{Admissible}ab=((\forall (i:Finn),\Vert ai\Vert =1\wedge \Vert bi\Vert =1)\wedge \mathrm{ConstructionReduction}.\mathrm{phaseAt}a1=1\wedge \mathrm{ConstructionReduction}.\mathrm{phaseAt}bn=1\wedge (\forall (ij:Finn),i<j\to ((ai){)}^{-1}\cdot aj\ne ((bi){)}^{-1}\cdot bj))$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.Admissible (✓ std3).

Citation. J. Choi, Y.-H. Kiem, and S.-H. Kye (2020). Entangled edge states of corank one with positive partial transposes. DOI: 10.1063/1.5122836. URL: https://arxiv.org/abs/1903.10745v2.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion.

Definition 1.20 (LargestRoot).

$$\forall (n:\mathbb{N}),\forall (a:Finn\to \mathbb{C}),\forall (b:Finn\to \mathbb{C}),\forall (r:\mathbb{R}),\mathrm{LargestRoot}abr=((\mathrm{ConstructionReduction}.Dabr).det=0\wedge (\forall (s:\mathbb{R}),(\mathrm{ConstructionReduction}.Dabs).det=0\to s\le r))$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.LargestRoot (✓ std3).

Citation. J. Choi, Y.-H. Kiem, and S.-H. Kye (2020). Entangled edge states of corank one with positive partial transposes. DOI: 10.1063/1.5122836. URL: https://arxiv.org/abs/1903.10745v2.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion.

Definition 1.21 (SimpleRoot).

$$\forall (n:\mathbb{N}),\forall (a:Finn\to \mathbb{C}),\forall (b:Finn\to \mathbb{C}),\forall (r:\mathbb{R}),\mathrm{SimpleRoot}abr=(\exists (d:\mathbb{R}),d\ne 0\wedge \mathrm{HasDerivAt}(\lambda (s:\mathbb{R})\mapsto (\mathrm{ConstructionReduction}.Dabs).det.re)dr)$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.SimpleRoot (✓ std3).

Citation. J. Choi, Y.-H. Kiem, and S.-H. Kye (2020). Entangled edge states of corank one with positive partial transposes. DOI: 10.1063/1.5122836. URL: https://arxiv.org/abs/1903.10745v2.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion.

Definition 1.22 (bracket).

$$\forall (n:\mathbb{N}),\forall (a:Finn\to \mathbb{C}),\forall (x:Finn\to \mathbb{C}),\forall (y:Finn\to \mathbb{C}),\forall (i:\mathbb{N}),\forall (j:\mathbb{N}),\mathrm{bracket}axyij=(\mathrm{ConstructionReduction}.\mathrm{phaseAt}xi\cdot \mathrm{ConstructionReduction}.\mathrm{phaseAt}yj-((\mathrm{ConstructionReduction}.\mathrm{phaseAt}ai){)}^{-1}\cdot \mathrm{ConstructionReduction}.\mathrm{phaseAt}aj\cdot \mathrm{ConstructionReduction}.\mathrm{phaseAt}xj\cdot \mathrm{ConstructionReduction}.\mathrm{phaseAt}yi)$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.bracket (✓ std3).

Citation. J. Choi, Y.-H. Kiem, and S.-H. Kye (2020). Entangled edge states of corank one with positive partial transposes. DOI: 10.1063/1.5122836. URL: https://arxiv.org/abs/1903.10745v2.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion.

Definition 1.23 (BilinearSystem).

$$\forall (n:\mathbb{N}),\forall (a:Finn\to \mathbb{C}),\forall (b:Finn\to \mathbb{C}),\forall (x:Finn\to \mathbb{C}),\forall (y:Finn\to \mathbb{C}),\mathrm{BilinearSystem}abxy=((\forall k\in \mathrm{Finset}.Icc2n,(\sum j\in \mathrm{Finset}.\mathrm{range}(k\mathrm{HDiv}.\mathrm{hDiv}2),((-1){)}^j\cdot \mathrm{ConstructionReduction}.\mathrm{bracket}axy(j+1)(k-j))=0)\wedge (\forall l\in \mathrm{Finset}.Icc1(n-2),(\sum j\in \mathrm{Finset}.\mathrm{range}((l+1)\mathrm{HDiv}.\mathrm{hDiv}2),((-1){)}^j\cdot \mathrm{ConstructionReduction}.\mathrm{bracket}bxy(n-l+j)(n-j))=0))$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.BilinearSystem (✓ std3).

Citation. J. Choi, Y.-H. Kiem, and S.-H. Kye (2020). Entangled edge states of corank one with positive partial transposes. DOI: 10.1063/1.5122836. URL: https://arxiv.org/abs/1903.10745v2.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion.

Definition 1.24 (AllowedSupport).

$$\forall (n:\mathbb{N}),\forall (\mathrm{isAlpha}:\mathrm{Bool}),\forall (s:\mathrm{Finset}(Finn)),\mathrm{AllowedSupport}n\mathrm{isAlpha}s=(if\mathrm{isAlpha}=\mathrm{true}\mathrm{then}((\forall i\in s,2\cdot (\mathrm{val}\left(i\right)+1)\le n+1)\vee \exists (p:Finn)(q:Finn),p\in s\wedge q\in s\wedge \mathrm{val}\left(p\right)+\mathrm{val}\left(q\right)+2\le n+1\wedge 2\cdot (\mathrm{val}\left(p\right)+1)<n+1\wedge n+1<2\cdot (\mathrm{val}\left(q\right)+1)\wedge (\forall i\in s,i=q\vee p\le i\wedge \mathrm{val}\left(i\right)+\mathrm{val}\left(q\right)+2\le n+1))\mathrm{else}((\forall i\in s,n+1\le 2\cdot (\mathrm{val}\left(i\right)+1))\vee \exists (p:Finn)(q:Finn),p\in s\wedge q\in s\wedge n+1<\mathrm{val}\left(p\right)+\mathrm{val}\left(q\right)+2\wedge 2\cdot (\mathrm{val}\left(p\right)+1)<n+1\wedge n+1<2\cdot (\mathrm{val}\left(q\right)+1)\wedge (\forall i\in s,i=p\vee n+1<\mathrm{val}\left(i\right)+\mathrm{val}\left(p\right)+2\wedge i\le q)))$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.AllowedSupport (✓ std3).

Citation. J. Choi, Y.-H. Kiem, and S.-H. Kye (2020). Entangled edge states of corank one with positive partial transposes. DOI: 10.1063/1.5122836. URL: https://arxiv.org/abs/1903.10745v2.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion.

Definition 1.25 (Classified).

$$\forall (n:\mathbb{N}),\forall (a:Finn\to \mathbb{C}),\forall (b:Finn\to \mathbb{C}),\forall (x:Finn\to \mathbb{C}),\forall (y:Finn\to \mathbb{C}),\mathrm{Classified}abxy=(x=0\vee y=0\vee \exists (\mathrm{isAlpha}:\mathrm{Bool})(s:\mathrm{Finset}(Finn))(c:Finn\to \mathbb{C})(t:\mathbb{C}),t\ne 0\wedge s.\mathrm{Nonempty}\wedge \mathrm{ConstructionReduction}.\mathrm{AllowedSupport}n\mathrm{isAlpha}s\wedge (\forall (i:Finn),ci\ne 0\iff i\in s)\wedge (\forall (i:Finn),xi=ci\cdot t\wedge yi=ci\cdot if\mathrm{isAlpha}=\mathrm{true}\mathrm{then}ai\mathrm{else}bi))$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.Classified (✓ std3).

Citation. J. Choi, Y.-H. Kiem, and S.-H. Kye (2020). Entangled edge states of corank one with positive partial transposes. DOI: 10.1063/1.5122836. URL: https://arxiv.org/abs/1903.10745v2.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion.

Definition 1.26 (StarCondition).

$$\forall (n:\mathbb{N}),\forall (a:Finn\to \mathbb{C}),\forall (b:Finn\to \mathbb{C}),\forall (w:Finn\to \mathbb{C}),\mathrm{StarCondition}abw=(\forall (\mathrm{isAlpha}:\mathrm{Bool})(s:\mathrm{Finset}(Finn)),s.\mathrm{Nonempty}\to \mathrm{ConstructionReduction}.\mathrm{AllowedSupport}n\mathrm{isAlpha}s\to \forall (u:Finn\to \mathbb{R}),(\forall (i:Finn),0\le ui)\to (\forall (i:Finn),ui\ne 0\iff i\in s)\to (\sum i:Finn,(\mathrm{val}\left(ui\right)\cdot if\mathrm{isAlpha}=\mathrm{true}\mathrm{then}ai\mathrm{else}bi)\cdot (\mathrm{starRingEnd}\mathbb{C})(wi))\ne 0)$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.StarCondition (✓ std3).

Citation. J. Choi, Y.-H. Kiem, and S.-H. Kye (2020). Entangled edge states of corank one with positive partial transposes. DOI: 10.1063/1.5122836. URL: https://arxiv.org/abs/1903.10745v2.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion.

Definition 1.27 (proposition61_statement).

$${proposition61}_{\mathrm{statement}}=(\forall (n:\mathbb{N}),3\le n\to \forall (ab:Finn\to \mathbb{C})(r:\mathbb{R})(w:Finn\to \mathbb{C}),\mathrm{ConstructionReduction}.\mathrm{Admissible}ab\to 1<r\to \mathrm{ConstructionReduction}.\mathrm{LargestRoot}abr\to \mathrm{ConstructionReduction}.\mathrm{SimpleRoot}abr\to w\ne 0\to (\mathrm{ConstructionReduction}.Dabr).\mathrm{mulVec}w=0\to \mathrm{ConstructionReduction}.\mathrm{StarCondition}abw\to \mathrm{ConstructionReduction}.PPT(\mathrm{ConstructionReduction}.rhoabr)\wedge \mathrm{ConstructionReduction}.\mathrm{Edge}(\mathrm{ConstructionReduction}.rhoabr)\wedge (\mathrm{ConstructionReduction}.rhoabr).\mathrm{rank}=n\cdot n-1\wedge (\mathrm{ConstructionReduction}.\mathrm{rhoGamma}abr).\mathrm{rank}=n\cdot n-2\cdot n+3)$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.proposition61_statement (✓ std3).

Citation. J. Choi, Y.-H. Kiem, and S.-H. Kye (2020). Entangled edge states of corank one with positive partial transposes. DOI: 10.1063/1.5122836. URL: https://arxiv.org/abs/1903.10745v2.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion.

Definition 1.28 (Partition.lo).

$$\forall (n:\mathbb{N}),\forall (t:\mathbb{N}),\mathrm{Partition}.lont=(ift+2\le n\mathrm{then}1\mathrm{else}t+3-n)$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.lo (✓ std3).

Source. Repository-derived.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion.

Definition 1.29 (Partition.hi).

$$\forall (n:\mathbb{N}),\forall (t:\mathbb{N}),\mathrm{Partition}.hint=(ift+2\le n\mathrm{then}t+2\mathrm{else}n)$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.hi (✓ std3).

Source. Repository-derived.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion.

Theorem 1.30 (Draft.triangular_pivot).

$$\forall (u:\mathbb{N}\to \mathbb{C}),\forall (v:\mathbb{N}\to \mathbb{C}),\forall (\mathrm{weight}:\mathbb{N}\to \mathbb{N}\to \mathbb{C}),\forall (N:\mathbb{N}),\forall (p:\mathbb{N}),(1\le p)\to ((up\ne 0\vee vp\ne 0)\to ((\forall (i:\mathbb{N}),1\le i\to i<p\to ui=0\wedge vi=0)\to ((\forall (ki:\mathbb{N}),2\le k\to k\le N\to i<k\mathrm{HDiv}.\mathrm{hDiv}2\to \mathrm{weight}ki\ne 0)\to ((\forall (k:\mathbb{N}),2\le k\to k\le N\to (\sum j\in \mathrm{Finset}.\mathrm{range}(k\mathrm{HDiv}.\mathrm{hDiv}2),\mathrm{weight}kj\cdot (u(j+1)\cdot v(k-j)-u(k-j)\cdot v(j+1)))=0)\to (\forall (q:\mathbb{N}),(p<q)\to ((p+q\le N+1)\to ((up\cdot vq-uq\cdot vp)=0)))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.triangular_pivot (✓ std3). ∎

Source. Repository-derived.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion. The private scalar wedge is displayed by its literal defining expression.

Definition 1.31 (Spectral.pencil).

$$\forall (\iota :\mathrm{Type}\ast ),\forall [\mathrm{DecidableEq}\iota ],\forall (A:\mathrm{Matrix}\iota \iota \mathbb{C}),\forall (s:\mathbb{R}),\mathrm{Spectral}.\mathrm{pencil}As=(\mathrm{val}\left(s\right)\cdot 1-A)$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.pencil (✓ std3).

Source. Repository-derived.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion.

Theorem 1.32 (Spectral.det_pencil).

$$\forall (\iota :\mathrm{Type}\ast ),\forall [\mathrm{Fintype}\iota ],\forall [\mathrm{DecidableEq}\iota ],\forall (A:\mathrm{Matrix}\iota \iota \mathbb{C}),\forall (hA:A.\mathrm{IsHermitian}),\forall (s:\mathbb{R}),(\mathrm{ConstructionReduction}.\mathrm{Spectral}.\mathrm{pencil}As).det=\prod i:\iota ,\mathrm{val}\left(s-hA.\mathrm{eigenvalues}i\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.det_pencil (✓ std3). ∎

Source. Repository-derived.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion.

Theorem 1.33 (Spectral.pencil_conjugate).

$$\forall (\iota :\mathrm{Type}\ast ),\forall [\mathrm{Fintype}\iota ],\forall [\mathrm{DecidableEq}\iota ],\forall (A:\mathrm{Matrix}\iota \iota \mathbb{C}),\forall (hA:A.\mathrm{IsHermitian}),\forall (s:\mathbb{R}),\mathrm{ConstructionReduction}.\mathrm{Spectral}.\mathrm{pencil}As=((\mathrm{Unitary}.\mathrm{conjStarAlgAut}\mathbb{C}(\mathrm{Matrix}\iota \iota \mathbb{C}))hA.\mathrm{eigenvectorUnitary})(\mathrm{Matrix}.\mathrm{diagonal}\lambda (i:\iota )\mapsto \mathrm{val}\left(s-hA.\mathrm{eigenvalues}i\right))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.pencil_conjugate (✓ std3). ∎

Source. Repository-derived.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion.

Theorem 1.34 (Spectral.largest_root_psd).

$$\forall (\iota :\mathrm{Type}\ast ),\forall [\mathrm{Fintype}\iota ],\forall [\mathrm{DecidableEq}\iota ],\forall (A:\mathrm{Matrix}\iota \iota \mathbb{C}),(A.\mathrm{IsHermitian})\to (\forall (r:\mathbb{R}),(\forall (s:\mathbb{R}),(\mathrm{ConstructionReduction}.\mathrm{Spectral}.\mathrm{pencil}As).det=0\to s\le r)\to ((\mathrm{ConstructionReduction}.\mathrm{Spectral}.\mathrm{pencil}Ar).\mathrm{PosSemidef}))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.largest_root_psd (✓ std3). ∎

Source. Repository-derived.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion.

Theorem 1.35 (Spectral.det_pencil_re).

$$\forall (\iota :\mathrm{Type}\ast ),\forall [\mathrm{Fintype}\iota ],\forall [\mathrm{DecidableEq}\iota ],\forall (A:\mathrm{Matrix}\iota \iota \mathbb{C}),\forall (hA:A.\mathrm{IsHermitian}),\forall (s:\mathbb{R}),(\mathrm{ConstructionReduction}.\mathrm{Spectral}.\mathrm{pencil}As).det.re=\prod i:\iota ,(s-hA.\mathrm{eigenvalues}i)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.det_pencil_re (✓ std3). ∎

Source. Repository-derived.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion.

Theorem 1.36 (D_hermitian).

$$\forall (n:\mathbb{N}),(3\le n)\to (\forall (a:Finn\to \mathbb{C}),\forall (b:Finn\to \mathbb{C}),\forall (r:\mathbb{R}),(\mathrm{ConstructionReduction}.Dabr).\mathrm{IsHermitian})$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.D_hermitian (✓ std3). ∎

Source. Repository-derived.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion.

Theorem 1.37 (D_pencil).

$$\forall (n:\mathbb{N}),\forall (a:Finn\to \mathbb{C}),\forall (b:Finn\to \mathbb{C}),\forall (r:\mathbb{R}),\mathrm{ConstructionReduction}.Dabr=\mathrm{ConstructionReduction}.\mathrm{Spectral}.\mathrm{pencil}(-\mathrm{ConstructionReduction}.Dab0)r$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.D_pencil (✓ std3). ∎

Source. Repository-derived.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion.

Theorem 1.38 (partialTranspose_involutive).

$$\forall (n:\mathbb{N}),\forall (A:\mathrm{Matrix}(Finn\times Finn)(Finn\times Finn)\mathbb{C}),\mathrm{ConstructionReduction}.\mathrm{partialTranspose}(\mathrm{ConstructionReduction}.\mathrm{partialTranspose}A)=A$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.partialTranspose_involutive (✓ std3). ∎

Source. Repository-derived.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion.

Theorem 1.39 (Path.scaled_dominance_posDef).

$$\forall (\iota :\mathrm{Type}\ast ),\forall [\mathrm{Fintype}\iota ],\forall [\mathrm{DecidableEq}\iota ],\forall (A:\mathrm{Matrix}\iota \iota \mathbb{C}),(A.\mathrm{IsHermitian})\to (\forall (g:\iota \to \mathbb{C}),(\forall (i:\iota ),gi\ne 0)\to ((\forall (i:\iota ),(\sum j\in \mathrm{Finset}.\mathrm{univ}.\mathrm{erase}i,\Vert ((gi){)}^{-1}\cdot Aij\cdot gj\Vert )<(Aii).re)\to (A.\mathrm{PosDef})))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.scaled_dominance_posDef (✓ std3). ∎

Source. Repository-derived.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion.

Theorem 1.40 (Path.sum_indicator_le).

$$\forall (\iota :\mathrm{Type}\ast ),\forall [\mathrm{Fintype}\iota ],\forall (P:\iota \to \mathrm{Prop}),\forall [\mathrm{DecidablePred}P],(\forall (ij:\iota ),Pi\to Pj\to i=j)\to (\forall (c:\mathbb{R}),(0\le c)\to (((\sum i:\iota ,ifPi\mathrm{then}c\mathrm{else}0))\le c))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.sum_indicator_le (✓ std3). ∎

Source. Repository-derived.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion.

Theorem 1.41 (proposition61).

$$\forall (n:\mathbb{N}),3\le n\to \forall (ab:Finn\to \mathbb{C})(r:\mathbb{R})(w:Finn\to \mathbb{C}),\mathrm{ConstructionReduction}.\mathrm{Admissible}ab\to 1<r\to \mathrm{ConstructionReduction}.\mathrm{LargestRoot}abr\to \mathrm{ConstructionReduction}.\mathrm{SimpleRoot}abr\to w\ne 0\to (\mathrm{ConstructionReduction}.Dabr).\mathrm{mulVec}w=0\to \mathrm{ConstructionReduction}.\mathrm{StarCondition}abw\to \mathrm{ConstructionReduction}.PPT(\mathrm{ConstructionReduction}.rhoabr)\wedge \mathrm{ConstructionReduction}.\mathrm{Edge}(\mathrm{ConstructionReduction}.rhoabr)\wedge (\mathrm{ConstructionReduction}.rhoabr).\mathrm{rank}=n\cdot n-1\wedge (\mathrm{ConstructionReduction}.\mathrm{rhoGamma}abr).\mathrm{rank}=n\cdot n-2\cdot n+3$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.proposition61 (✓ std3). ∎

Citation. J. Choi, Y.-H. Kiem, and S.-H. Kye (2020). Entangled edge states of corank one with positive partial transposes. DOI: 10.1063/1.5122836. URL: https://arxiv.org/abs/1903.10745v2.

Commentary.

The formula uses the actual Lean names and notation. HDiv.hDiv is displayed in infix position for Lean’s division operator: natural-number floor division, Euclidean integer division, or field division according to the carrier. Natural-number subtraction is truncated. val denotes the displayed Lean coercion.

References

• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.Admissible
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.AllowedSupport
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.BilinearSystem
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.Classified
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.D
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.D_hermitian
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.D_pencil
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.Edge
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.GenericPhases
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.InRange
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.LargestRoot
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.P
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.PPT
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.SimpleRoot
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.StarCondition
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.alphaUpper
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.betaUpper
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.blockEntry
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.blockZ
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.bracket
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.det_pencil
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.det_pencil_re
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.hi
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.indexList
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.largest_root_psd
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.lo
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.mulVec_block
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.pEntry
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.partialTranspose
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.partialTranspose_involutive
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.pencil
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.pencil_conjugate
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.phaseAt
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.proposition61
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.proposition61_statement
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.rho
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.rhoGamma
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.scaled_dominance_posDef
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.sum_indicator_le
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.tensor
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction.triangular_pivot
• Dependency: D5/S3/Quantum/Entanglement/StructuredNegativityCoincidenceRefutation
• Dependency: D5/S3/Quantum/Measurement/FiniteDetectionDarkSpace