UniformPerturbedParameters

Abstract

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

Theorem 1.1 (Anchor.largest_root_psd).

$$\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}.\mathrm{LargestRoot}abr)\to ((\mathrm{ConstructionReduction}.Dabr).\mathrm{PosSemidef}))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformPerturbedParameters.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.2 (Anchor.D_shift).

$$\forall (n:\mathbb{N}),\forall (a:Finn\to \mathbb{C}),\forall (b:Finn\to \mathbb{C}),\forall (r:\mathbb{R}),\forall (R:\mathbb{R}),\mathrm{ConstructionReduction}.DabR=\mathrm{ConstructionReduction}.Dabr+\mathrm{val}\left(R-r\right)\cdot 1$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformPerturbedParameters.D_shift (✓ 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.3 (Anchor.perturbed_kernel_stability).

$$\forall (m:\mathbb{N}),(15\le m)\to (\exists (r:\mathbb{R})(r^{\prime }:\mathbb{R})(q^{\prime }:\mathrm{EuclideanSpace}\mathbb{C}(Fin(m+2))),\mathrm{ConstructionReduction}.\mathrm{LargestRoot}(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{anchorAlpha}(m+2))(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{beta}(m+2))r\wedge \mathrm{ConstructionReduction}.\mathrm{LargestRoot}(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{alpha}(m+2))(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{beta}(m+2))r^{\prime }\wedge \mathrm{ConstructionReduction}.\mathrm{SimpleRoot}(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{alpha}(m+2))(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{beta}(m+2))r^{\prime }\wedge 5<r^{\prime }\wedge \Vert q^{\prime }\Vert =1\wedge (\mathrm{ConstructionReduction}.D(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{alpha}(m+2))(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{beta}(m+2))r^{\prime }).\mathrm{mulVec}{q}^{\prime }.\mathrm{ofLp}=0\wedge \Vert q^{\prime }-(\lambda (m:\mathbb{N})(r:\mathbb{R})\mapsto \mathrm{NormedSpace}.\mathrm{normalize}(\mathrm{WithLp}.\mathrm{toLp}2(\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.\mathrm{kernel}mr)))mr\Vert \le 4\cdot (\mathrm{norm}\circ \mathrm{val}\left(\mathrm{Matrix}.\mathrm{toEuclideanCLM}\right))(\mathrm{ConstructionReduction}.D(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{alpha}(m+2))(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{beta}(m+2))0-\mathrm{ConstructionReduction}.D(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{anchorAlpha}(m+2))(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{beta}(m+2))0)\mathrm{HDiv}.\mathrm{hDiv}(1\mathrm{HDiv}.\mathrm{hDiv}(9\cdot \mathrm{val}\left(m+2\right)))\wedge \Vert q^{\prime }-(\lambda (m:\mathbb{N})(r:\mathbb{R})\mapsto \mathrm{NormedSpace}.\mathrm{normalize}(\mathrm{WithLp}.\mathrm{toLp}2(\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.\mathrm{kernel}mr)))mr\Vert \le 4\cdot (2\cdot \mathrm{Real}.pi\mathrm{HDiv}.\mathrm{hDiv}(1000000000\cdot (\mathrm{val}\left(m+2\right){)}^4))\mathrm{HDiv}.\mathrm{hDiv}(1\mathrm{HDiv}.\mathrm{hDiv}(9\cdot \mathrm{val}\left(m+2\right))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformPerturbedParameters.perturbed_kernel_stability (✓ 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.4 (Anchor.n_ge_17).

$$\forall (n:\mathbb{N}),(17\le n)\to (\exists (r:\mathbb{R})(w:Finn\to \mathbb{C}),\mathrm{ConstructionReduction}.\mathrm{Admissible}(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{alpha}n)(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{beta}n)\wedge 5<r\wedge \mathrm{ConstructionReduction}.\mathrm{LargestRoot}(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{alpha}n)(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{beta}n)r\wedge \mathrm{ConstructionReduction}.\mathrm{SimpleRoot}(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{alpha}n)(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{beta}n)r\wedge w\ne 0\wedge (\mathrm{ConstructionReduction}.D(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{alpha}n)(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{beta}n)r).\mathrm{mulVec}w=0\wedge \mathrm{ConstructionReduction}.\mathrm{StarCondition}(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{alpha}n)(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{beta}n)w\wedge \mathrm{ConstructionReduction}.PPT(\mathrm{ConstructionReduction}.rho(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{alpha}n)(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{beta}n)r)\wedge \mathrm{ConstructionReduction}.\mathrm{Edge}(\mathrm{ConstructionReduction}.rho(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{alpha}n)(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{beta}n)r)\wedge (\mathrm{ConstructionReduction}.rho(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{alpha}n)(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{beta}n)r).\mathrm{rank}=n\cdot n-1\wedge (\mathrm{ConstructionReduction}.\mathrm{rhoGamma}(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{alpha}n)(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{beta}n)r).\mathrm{rank}=n\cdot n-2\cdot n+3)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformPerturbedParameters.n_ge_17 (✓ 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.

References

• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformPerturbedParameters.D_shift
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformPerturbedParameters.largest_root_psd
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformPerturbedParameters.n_ge_17
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformPerturbedParameters.perturbed_kernel_stability
• Dependency: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor