UniformParameterAnchor

Abstract

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

Definition 1.1 (Uniform.epsilon).

$$\forall (n:\mathbb{N}),\mathrm{Uniform}.\mathrm{epsilon}n=(1\mathrm{HDiv}.\mathrm{hDiv}(1000000000\cdot (\mathrm{val}\left(n\right){)}^6))$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.epsilon (✓ 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.2 (Uniform.angle).

$$\forall (n:\mathbb{N}),\forall (i:Finn),\mathrm{Uniform}.\mathrm{angle}ni=(if\mathrm{val}\left(i\right)=0\mathrm{then}0\mathrm{else}if\mathrm{val}\left(i\right)+1=n\mathrm{then}\mathrm{Real}.pi\mathrm{else}\mathrm{Real}.pi\cdot (1\mathrm{HDiv}.\mathrm{hDiv}4+\mathrm{val}\left(\mathrm{val}\left(i\right)\right)\cdot \mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{epsilon}n))$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.angle (✓ 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.3 (Uniform.alpha).

$$\forall (n:\mathbb{N}),\forall (i:Finn),\mathrm{Uniform}.\mathrm{alpha}ni=(\mathrm{Complex}.exp(\mathrm{Complex}.I\cdot \mathrm{val}\left(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{angle}ni\right)))$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.alpha (✓ 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.4 (Uniform.beta).

$$\forall (n:\mathbb{N}),\forall (a:Finn),\mathrm{Uniform}.\mathrm{beta}na=(1)$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.beta (✓ 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.5 (Uniform.anchorAlpha).

$$\forall (n:\mathbb{N}),\forall (i:Finn),\mathrm{Uniform}.\mathrm{anchorAlpha}ni=(if\mathrm{val}\left(i\right)=0\mathrm{then}1\mathrm{else}if\mathrm{val}\left(i\right)+1=n\mathrm{then}-1\mathrm{else}\mathrm{Complex}.exp(\mathrm{Complex}.I\cdot \mathrm{val}\left(\mathrm{Real}.pi\mathrm{HDiv}.\mathrm{hDiv}4\right)))$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.anchorAlpha (✓ 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.6 (Uniform.epsilon_pos).

$$\forall (n:\mathbb{N}),(0<n)\to (0<\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{epsilon}n)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.epsilon_pos (✓ 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.7 (Uniform.alpha_norm).

$$\forall (n:\mathbb{N}),\forall (i:Finn),\Vert \mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{alpha}ni\Vert =1$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.alpha_norm (✓ 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.8 (Uniform.admissible).

$$\forall (n:\mathbb{N}),(3\le n)\to (\mathrm{ConstructionReduction}.\mathrm{Admissible}(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{alpha}n)(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{beta}n))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.admissible (✓ 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.9 (Uniform.alpha_anchor_distance).

$$\forall (n:\mathbb{N}),(3\le n)\to (\forall (i:Finn),\Vert \mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{alpha}ni-\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{anchorAlpha}ni\Vert \le \mathrm{Real}.pi\cdot \mathrm{val}\left(n\right)\cdot \mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{epsilon}n)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.alpha_anchor_distance (✓ 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.10 (Uniform.operator_perturbation).

$$\forall (n:\mathbb{N}),(3\le n)\to (\forall (r:\mathbb{R}),(\mathrm{norm}\circ \mathrm{val}\left(\mathrm{Matrix}.\mathrm{toEuclideanCLM}\right))(\mathrm{ConstructionReduction}.D(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{alpha}n)(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{beta}n)r-\mathrm{ConstructionReduction}.D(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{anchorAlpha}n)(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{beta}n)r)\le 2\cdot \mathrm{Real}.pi\mathrm{HDiv}.\mathrm{hDiv}(1000000000\cdot (\mathrm{val}\left(n\right){)}^4))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.operator_perturbation (✓ 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.11 (Uniform.uniform_coordinate_lower).

$$\forall (n:\mathbb{N}),(17\le n)\to (\forall (r:\mathbb{R}),\forall (x:\mathbb{R}),(161\mathrm{HDiv}.\mathrm{hDiv}32<r)\to (((r{)}^2\le 9\cdot \mathrm{val}\left(n\right))\to (((r-5)\mathrm{HDiv}.\mathrm{hDiv}(r{)}^2\le x)\to (1\mathrm{HDiv}.\mathrm{hDiv}(288\cdot \mathrm{val}\left(n\right))<x))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.uniform_coordinate_lower (✓ 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.12 (Uniform.three_halfplanes_star).

$$\forall (n:\mathbb{N}),(3\le n)\to (\forall (a:Finn\to \mathbb{C}),\forall (b:Finn\to \mathbb{C}),\forall (w:Finn\to \mathbb{C}),\forall (\mathrm{zAlpha}:\mathbb{C}),\forall (\mathrm{zBeta}:\mathbb{C}),\forall (\mathrm{zEnds}:\mathbb{C}),(\forall (i:Finn),\mathrm{val}\left(i\right)+1\ne n\to 0<(\mathrm{zAlpha}\cdot (ai\cdot (\mathrm{starRingEnd}\mathbb{C})(wi))).re)\to ((\forall (i:Finn),\mathrm{val}\left(i\right)\ne 0\to 0<(\mathrm{zBeta}\cdot (bi\cdot (\mathrm{starRingEnd}\mathbb{C})(wi))).re)\to ((\forall (i:Finn),\mathrm{val}\left(i\right)=0\vee \mathrm{val}\left(i\right)+1=n\to 0<(\mathrm{zEnds}\cdot (ai\cdot (\mathrm{starRingEnd}\mathbb{C})(wi))).re)\to (\mathrm{ConstructionReduction}.\mathrm{StarCondition}abw))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.three_halfplanes_star (✓ 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.13 (Uniform.band).

$$\forall (m:\mathbb{N}),\mathrm{Uniform}.\mathrm{band}m=(\lambda (ij:Finm)\mapsto 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}1\mathrm{else}0)$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.band (✓ 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.14 (Uniform.band_hermitian).

$$\forall (m:\mathbb{N}),(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{band}m).\mathrm{IsHermitian}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.band_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.15 (Uniform.band_row_bound).

$$\forall (m:\mathbb{N}),\forall (i:Finm),(\sum j:Finm,\Vert \mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{band}mij\Vert )\le 4$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.band_row_bound (✓ 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.16 (Uniform.spike).

$$\forall (m:\mathbb{N}),\forall (a:Finm),\mathrm{Uniform}.\mathrm{spike}ma=(if\mathrm{val}\left(a\right)=1\mathrm{then}2\mathrm{else}1)$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.spike (✓ 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.17 (Uniform.spike_lower).

$$\forall (m:\mathbb{N}),\forall (i:Finm),1\le \mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{spike}mi$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.spike_lower (✓ 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.18 (Uniform.phase_aligned_stability).

$$\forall (H:\mathrm{Type}\ast ),\forall [\mathrm{NormedAddCommGroup}H],\forall [\mathrm{InnerProductSpace}\mathbb{C}H],\forall (A:H{\to }_L[\mathbb{C}]H),\forall (E:H{\to }_L[\mathbb{C}]H),\forall (q:H),\forall (q^{\prime }:H),\forall (lam:\mathbb{R}),\forall (la{m}^{\prime }:\mathbb{R}),\forall (g:\mathbb{R}),\forall (e:\mathbb{R}),(0<g)\to ((\Vert q\Vert =1)\to ((\Vert q^{\prime }\Vert =1)\to ((Aq=\mathrm{val}\left(lam\right)\cdot q)\to (((A+E)q^{\prime }=\mathrm{val}\left(la{m}^{\prime }\right)\cdot q^{\prime })\to ((\forall (v:H),\mathrm{inner}\mathbb{C}qv=0\to g\cdot \Vert v\Vert \le \Vert Av-\mathrm{val}\left(lam\right)\cdot v\Vert )\to ((\left|la{m}^{\prime }-lam\right|\le e)\to ((\Vert E\Vert \le e)\to (\exists (z:\mathbb{C}),\Vert z\Vert =1\wedge \Vert z\cdot q^{\prime }-q\Vert \le 4\cdot e\mathrm{HDiv}.\mathrm{hDiv}g))))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.phase_aligned_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.19 (Uniform.surviving_projection).

$$\forall (n:\mathbb{N}),(17\le n)\to (\forall (a:Finn\to \mathbb{C}),\forall (a^{\prime }:Finn\to \mathbb{C}),\forall (q:\mathrm{EuclideanSpace}\mathbb{C}(Finn)),\forall (q^{\prime }:\mathrm{EuclideanSpace}\mathbb{C}(Finn)),\forall (z:\mathbb{C}),\forall (i:Finn),(\Vert z\Vert =1)\to ((\Vert a^{\prime }i\Vert =1)\to ((\Vert q\Vert =1)\to ((1\mathrm{HDiv}.\mathrm{hDiv}(100000\cdot (\mathrm{val}\left(n\right){)}^3)\le (z\cdot (ai\cdot (\mathrm{starRingEnd}\mathbb{C})(q.\mathrm{ofLp}i))).re)\to ((\Vert q^{\prime }-q\Vert +\Vert a^{\prime }i-ai\Vert \le 73\cdot \mathrm{Real}.pi\mathrm{HDiv}.\mathrm{hDiv}(1000000000\cdot (\mathrm{val}\left(n\right){)}^3))\to (1\mathrm{HDiv}.\mathrm{hDiv}(200000\cdot (\mathrm{val}\left(n\right){)}^3)\le (z\cdot (a^{\prime }i\cdot (\mathrm{starRingEnd}\mathbb{C})(q^{\prime }.\mathrm{ofLp}i))).re))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.surviving_projection (✓ 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.20 (Uniform.perturbation_error_small).

$$\forall (n:\mathbb{N}),(17\le n)\to (2\cdot \mathrm{Real}.pi\mathrm{HDiv}.\mathrm{hDiv}(1000000000\cdot (\mathrm{val}\left(n\right){)}^4)<1\mathrm{HDiv}.\mathrm{hDiv}(36\cdot \mathrm{val}\left(n\right)))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.perturbation_error_small (✓ 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.21 (Uniform.shifted_gap).

$$\forall (n:\mathbb{N}),(17\le n)\to (\forall (x:\mathbb{R}),\forall (y:\mathbb{R}),\forall (x^{\prime }:\mathbb{R}),\forall (y^{\prime }:\mathbb{R}),(1\mathrm{HDiv}.\mathrm{hDiv}(9\cdot \mathrm{val}\left(n\right))\le x-y)\to ((\left|x^{\prime }-x\right|\le 2\cdot \mathrm{Real}.pi\mathrm{HDiv}.\mathrm{hDiv}(1000000000\cdot (\mathrm{val}\left(n\right){)}^4))\to ((\left|y^{\prime }-y\right|\le 2\cdot \mathrm{Real}.pi\mathrm{HDiv}.\mathrm{hDiv}(1000000000\cdot (\mathrm{val}\left(n\right){)}^4))\to (1\mathrm{HDiv}.\mathrm{hDiv}(18\cdot \mathrm{val}\left(n\right))\le x^{\prime }-y^{\prime }))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.shifted_gap (✓ 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.22 (Uniform.stability_error_budget).

$$\forall (n:\mathbb{N}),(17\le n)\to (\forall (g:\mathbb{R}),\forall (e:\mathbb{R}),(1\mathrm{HDiv}.\mathrm{hDiv}(9\cdot \mathrm{val}\left(n\right))\le g)\to ((0\le e)\to ((e\le 2\cdot \mathrm{Real}.pi\mathrm{HDiv}.\mathrm{hDiv}(1000000000\cdot (\mathrm{val}\left(n\right){)}^4))\to (4\cdot e\mathrm{HDiv}.\mathrm{hDiv}g+\mathrm{Real}.pi\cdot \mathrm{val}\left(n\right)\cdot \mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{epsilon}n\le 73\cdot \mathrm{Real}.pi\mathrm{HDiv}.\mathrm{hDiv}(1000000000\cdot (\mathrm{val}\left(n\right){)}^3)))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.stability_error_budget (✓ 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.23 (Uniform.resolvent).

$$\forall (m:\mathbb{N}),\forall (r:\mathbb{R}),\mathrm{Uniform}.\mathrm{resolvent}mr=(r\cdot 1+\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{band}m)$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.resolvent (✓ 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.24 (Uniform.resolvent_isUnit).

$$\forall (m:\mathbb{N}),\forall (r:\mathbb{R}),(5<r)\to (\mathrm{IsUnit}(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{resolvent}mr))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.resolvent_isUnit (✓ 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.25 (Uniform.anchorInterior).

$$\forall (m:\mathbb{N}),\forall (r:\mathbb{R}),\forall (a:Finm),\mathrm{Uniform}.\mathrm{anchorInterior}mra=(((\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{resolvent}mr){)}^{-1}.\mathrm{mulVec}(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{spike}m)a)$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.anchorInterior (✓ 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.26 (Uniform.anchorInterior_solve).

$$\forall (m:\mathbb{N}),\forall (r:\mathbb{R}),(5<r)\to ((\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{resolvent}mr).\mathrm{mulVec}(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{anchorInterior}mr)=\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{spike}m)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.anchorInterior_solve (✓ 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.27 (Uniform.anchorInterior_positive).

$$\forall (m:\mathbb{N}),\forall (r:\mathbb{R}),(5<r)\to (\forall (i:Finm),0<\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{anchorInterior}mri\wedge (r-5)\mathrm{HDiv}.\mathrm{hDiv}(r{)}^2\le \mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{anchorInterior}mri)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.anchorInterior_positive (✓ 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.28 (Uniform.band_reverse).

$$\forall (m:\mathbb{N}),\forall (i:Finm),\forall (j:Finm),\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{band}mi.revj.rev=\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{band}mij$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.band_reverse (✓ 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.29 (Uniform.anchorInterior_upper).

$$\forall (m:\mathbb{N}),\forall (r:\mathbb{R}),(5<r)\to (\forall (i:Finm),\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{anchorInterior}mri\le 2\mathrm{HDiv}.\mathrm{hDiv}(r-4))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.anchorInterior_upper (✓ 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 (Uniform.pencil_top_largest).

$$\forall (n:\mathbb{N}),\forall (hn:0<n),\forall (A:\mathrm{Matrix}(Finn)(Finn)\mathbb{C}),\forall (hA:A.\mathrm{IsHermitian}),\mathrm{have}{k}_0:=⟨0,hn⟩;\mathrm{have}r:=hA.{\mathrm{eigenvalues}}_0{k}_0;(\mathrm{ConstructionReduction}.\mathrm{Spectral}.\mathrm{pencil}Ar).det=0\wedge (\forall (s:\mathbb{R}),(\mathrm{ConstructionReduction}.\mathrm{Spectral}.\mathrm{pencil}As).det=0\to s\le r)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.pencil_top_largest (✓ 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.31 (Uniform.simple_root_of_rank).

$$\forall (n:\mathbb{N}),(0<n)\to (\forall (A:\mathrm{Matrix}(Finn)(Finn)\mathbb{C}),(A.\mathrm{IsHermitian})\to (\forall (r:\mathbb{R}),((\mathrm{ConstructionReduction}.\mathrm{Spectral}.\mathrm{pencil}Ar).det=0)\to (((\mathrm{ConstructionReduction}.\mathrm{Spectral}.\mathrm{pencil}Ar).\mathrm{rank}=n-1)\to (\exists (d:\mathbb{R}),d\ne 0\wedge \mathrm{HasDerivAt}(\lambda (s:\mathbb{R})\mapsto (\mathrm{ConstructionReduction}.\mathrm{Spectral}.\mathrm{pencil}As).det.re)dr))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.simple_root_of_rank (✓ 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 (Uniform.negative_eigenvalue_perturbation).

$$\forall (n:\mathbb{N}),\forall (hn:3\le n),\forall (k:Fin(\mathrm{Fintype}.\mathrm{card}(Finn))),\left|((\mathrm{ConstructionReduction}.D_{\mathrm{hermitian}}hn(\mathrm{Uniform}.\mathrm{alpha}n)(\mathrm{Uniform}.\mathrm{beta}n)0).neg).{\mathrm{eigenvalues}}_{0}k-((\mathrm{ConstructionReduction}.D_{\mathrm{hermitian}}hn(\mathrm{Uniform}.\mathrm{anchorAlpha}n)(\mathrm{Uniform}.\mathrm{beta}n)0).neg).{\mathrm{eigenvalues}}_{0}k\right|\le 2\cdot \mathrm{Real}.pi\mathrm{HDiv}.\mathrm{hDiv}(1000000000\cdot ((n:\mathbb{R}){)}^4)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.negative_eigenvalue_perturbation (✓ 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 (Uniform.top_root_simple).

$$\forall (n:\mathbb{N}),\forall (hn:0<n),\forall (A:\mathrm{Matrix}(Finn)(Finn)\mathbb{C}),\forall (hA:A.\mathrm{IsHermitian}),(\forall (k:Fin(\mathrm{Fintype}.\mathrm{card}(Finn))),\mathrm{val}\left(k\right)\ne 0\to hA.{\mathrm{eigenvalues}}_{0}k<hA.{\mathrm{eigenvalues}}_0⟨0,hn⟩)\to (\mathrm{have}r:=hA.{\mathrm{eigenvalues}}_0⟨0,hn⟩;\exists (d:\mathbb{R}),d\ne 0\wedge \mathrm{HasDerivAt}(\lambda (s:\mathbb{R})\mapsto (\mathrm{ConstructionReduction}.\mathrm{Spectral}.\mathrm{pencil}As).det.re)dr)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.top_root_simple (✓ 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.34 (Anchor17Probe.R).

$$Anchor17Probe.R=(161\mathrm{HDiv}.\mathrm{hDiv}32)$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.R (✓ 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.35 (Anchor17Probe.den).

$$Anchor17Probe.den=(467481426546007099229949447217505)$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.den (✓ 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.36 (Anchor17Probe.numerators).

$$\forall (a:Fin15),Anchor17Probe.\mathrm{numerators}a=(![54327066786808963613640806075424,162449231862550997644964313113664,31699139912323503403854828536864,31613948584422024541176559469600,59604881628347486929523162482720,54670494327411800278812578252832,49610783029226477391942069717024,51590888719220490214531871213600,52010909755231607428873297004576,51622580565559122738458025199648,52977284525991984008498705532960,51176235075093681300178634180640,46129738378725518219680378619936,59271390354165390221788584643616,71966270372793280156716617928736]a)$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.numerators (✓ 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.37 (Anchor17Probe.u).

$$\forall (a:Fin15),Anchor17Probe.ua=(\mathrm{val}\left(\mathrm{UniformParameterAnchor}.Anchor17Probe.\mathrm{numerators}a\right)\mathrm{HDiv}.\mathrm{hDiv}\mathrm{val}\left(\mathrm{UniformParameterAnchor}.Anchor17Probe.den\right))$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.u (✓ 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 (Anchor17Probe.rational_solve).

$$(\mathrm{UniformParameterAnchor}.Anchor17Probe.R\cdot 1+\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{band}15).\mathrm{mulVec}\mathrm{UniformParameterAnchor}.Anchor17Probe.u=\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{spike}15$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.rational_solve (✓ 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.39 (Anchor17Probe.knum).

$$Anchor17Probe.\mathrm{knum}=(1043170075740423325737604745085504)$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.knum (✓ 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.40 (Anchor17Probe.lnum).

$$Anchor17Probe.\mathrm{lnum}=(939992234232037718314429016615456)$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.lnum (✓ 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 (Anchor17Probe.k_value).

$$\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{spike}15\cdot \mathrm{UniformParameterAnchor}.Anchor17Probe.u=\mathrm{val}\left(\mathrm{UniformParameterAnchor}.Anchor17Probe.\mathrm{knum}\right)\mathrm{HDiv}.\mathrm{hDiv}\mathrm{val}\left(\mathrm{UniformParameterAnchor}.Anchor17Probe.den\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.k_value (✓ 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.42 (Anchor17Probe.ell_value).

$$(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{spike}15\cdot \lambda (i:Fin15)\mapsto \mathrm{UniformParameterAnchor}.Anchor17Probe.ui.rev)=\mathrm{val}\left(\mathrm{UniformParameterAnchor}.Anchor17Probe.\mathrm{lnum}\right)\mathrm{HDiv}.\mathrm{hDiv}\mathrm{val}\left(\mathrm{UniformParameterAnchor}.Anchor17Probe.den\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.ell_value (✓ 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.43 (Anchor17Probe.aa).

$$Anchor17Probe.aa=(\mathrm{val}\left(\mathrm{Real}.\mathrm{sqrt}2\mathrm{HDiv}.\mathrm{hDiv}2\right)+\mathrm{val}\left(\mathrm{Real}.\mathrm{sqrt}2\mathrm{HDiv}.\mathrm{hDiv}2\right)\cdot \mathrm{Complex}.I)$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.aa (✓ 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.44 (Anchor17Probe.aa_anchor).

$$\mathrm{UniformParameterAnchor}.Anchor17Probe.aa=\mathrm{Complex}.exp(\mathrm{Complex}.I\cdot \mathrm{val}\left(\mathrm{Real}.pi\mathrm{HDiv}.\mathrm{hDiv}4\right))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.aa_anchor (✓ 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.45 (Anchor17Probe.probeSchur).

$$Anchor17Probe.\mathrm{probeSchur}=(!![\mathrm{val}\left(\mathrm{UniformParameterAnchor}.Anchor17Probe.R-\mathrm{val}\left(\mathrm{UniformParameterAnchor}.Anchor17Probe.\mathrm{knum}\right)\mathrm{HDiv}.\mathrm{hDiv}\mathrm{val}\left(\mathrm{UniformParameterAnchor}.Anchor17Probe.den\right)\right),-1-(\mathrm{starRingEnd}\mathbb{C})\mathrm{UniformParameterAnchor}.Anchor17Probe.aa\cdot \mathrm{val}\left(\mathrm{val}\left(\mathrm{UniformParameterAnchor}.Anchor17Probe.\mathrm{lnum}\right)\mathrm{HDiv}.\mathrm{hDiv}\mathrm{val}\left(\mathrm{UniformParameterAnchor}.Anchor17Probe.den\right)\right);-1-\mathrm{UniformParameterAnchor}.Anchor17Probe.aa\cdot \mathrm{val}\left(\mathrm{val}\left(\mathrm{UniformParameterAnchor}.Anchor17Probe.\mathrm{lnum}\right)\mathrm{HDiv}.\mathrm{hDiv}\mathrm{val}\left(\mathrm{UniformParameterAnchor}.Anchor17Probe.den\right)\right),\mathrm{val}\left(\mathrm{UniformParameterAnchor}.Anchor17Probe.R-\mathrm{val}\left(\mathrm{UniformParameterAnchor}.Anchor17Probe.\mathrm{knum}\right)\mathrm{HDiv}.\mathrm{hDiv}\mathrm{val}\left(\mathrm{UniformParameterAnchor}.Anchor17Probe.den\right)\right)])$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.probeSchur (✓ 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.46 (Anchor17Probe.schur_det_negative).

$$\mathrm{UniformParameterAnchor}.Anchor17Probe.\mathrm{probeSchur}.det.re<0$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.schur_det_negative (✓ 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.47 (Anchor.a).

$$\mathrm{Anchor}.a=(\mathrm{Complex}.exp(\mathrm{Complex}.I\cdot \mathrm{val}\left(\mathrm{Real}.pi\right)\cdot (1\mathrm{HDiv}.\mathrm{hDiv}4)))$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.a (✓ 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.48 (Anchor.address).

$$\forall (m:\mathbb{N}),\mathrm{Anchor}.\mathrm{address}m=(\mathrm{Equiv}.\mathrm{sumCongr}(\mathrm{finSumFinEquiv}(m:=1)(n:=1)).\mathrm{symm}(\mathrm{Equiv}.\mathrm{refl}(\mathrm{Fin}m))).\mathrm{trans}((\mathrm{Equiv}.\mathrm{sumAssoc}(\mathrm{Fin}1)(\mathrm{Fin}1)(\mathrm{Fin}m)).\mathrm{trans}((\mathrm{Equiv}.\mathrm{sumCongr}(\mathrm{Equiv}.\mathrm{refl}(\mathrm{Fin}1))(\mathrm{Equiv}.\mathrm{sumComm}(\mathrm{Fin}1)(\mathrm{Fin}m))).\mathrm{trans}((\mathrm{Equiv}.\mathrm{sumCongr}(\mathrm{Equiv}.\mathrm{refl}(\mathrm{Fin}1))(\mathrm{finSumFinEquiv}(m:=m)(n:=1))).\mathrm{trans}((\mathrm{finSumFinEquiv}(m:=1)(n:=(m+1))).\mathrm{trans}((\mathrm{finCongr}(\mathrm{by}\mathrm{omega})))))))$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.address (✓ 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 defining forward map uses Mathlib’s Fin constructors; The equivalence sends Sum.inl 0 to 0, Sum.inl 1 to m+1, and Sum.inr i to i.val+1. Its inverse sends 0 to Sum.inl 0, m+1 to Sum.inl 1, and every other i to Sum.inr ⟨i.val−1, the induced bound⟩. The left and right inverse fields prove these literal formulas.

Definition 1.49 (Anchor.endpoints).

$$\forall (r:\mathbb{R}),\mathrm{Anchor}.\mathrm{endpoints}r=(!![\mathrm{val}\left(r\right),-1;-1,\mathrm{val}\left(r\right)])$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.endpoints (✓ 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.50 (Anchor.coupling).

$$\forall (m:\mathbb{N}),\mathrm{Anchor}.\mathrm{coupling}m=(\lambda (i:Finm)(j:Fin2)\mapsto if\mathrm{val}\left(j\right)=0\mathrm{then}\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.a\cdot \mathrm{val}\left(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{spike}mi\right)\mathrm{else}\mathrm{val}\left(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{spike}mi.rev\right))$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.coupling (✓ 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.51 (Anchor.interior).

$$\forall (m:\mathbb{N}),\forall (r:\mathbb{R}),\mathrm{Anchor}.\mathrm{interior}mr=((\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{resolvent}mr).map\mathrm{Complex}.\mathrm{ofReal})$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.interior (✓ 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.52 (Anchor.block).

$$\forall (m:\mathbb{N}),\forall (r:\mathbb{R}),\mathrm{Anchor}.\mathrm{block}mr=(\mathrm{Matrix}.\mathrm{fromBlocks}(\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.\mathrm{endpoints}r)(\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.\mathrm{coupling}m).\mathrm{conjTranspose}(\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.\mathrm{coupling}m)(\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.\mathrm{interior}mr))$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.block (✓ 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.53 (Anchor.phase_def).

$$\mathrm{Complex}.exp(\mathrm{Complex}.I\cdot \mathrm{val}\left(\mathrm{Real}.pi\mathrm{HDiv}.\mathrm{hDiv}4\right))=\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.a$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.phase_def (✓ 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.54 (Anchor.phase_unit).

$$\Vert \mathrm{UniformParameterAnchor}.\mathrm{Anchor}.a\Vert =1$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.phase_unit (✓ 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.55 (Anchor.phase_mul_conj).

$$\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.a\cdot (\mathrm{starRingEnd}\mathbb{C})\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.a=1$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.phase_mul_conj (✓ 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.56 (Anchor.anchor_reindex).

$$\forall (m:\mathbb{N}),(4\le m)\to (\forall (r:\mathbb{R}),(\mathrm{ConstructionReduction}.D(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{anchorAlpha}(m+2))(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{beta}(m+2))r).\mathrm{submatrix}\mathrm{val}\left(\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.\mathrm{address}m\right)\mathrm{val}\left(\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.\mathrm{address}m\right)=\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.\mathrm{block}mr)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.anchor_reindex (✓ 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.57 (Anchor.k).

$$\forall (m:\mathbb{N}),\forall (r:\mathbb{R}),\mathrm{Anchor}.kmr=(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{spike}m\cdot \mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{anchorInterior}mr)$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.k (✓ 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.58 (Anchor.ell).

$$\forall (m:\mathbb{N}),\forall (r:\mathbb{R}),\mathrm{Anchor}.ellmr=(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{spike}m\cdot (\lambda (m:\mathbb{N})(r:\mathbb{R})(i:Finm)\mapsto \mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{anchorInterior}mri.rev)mr)$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.ell (✓ 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.59 (Anchor.zeta).

$$\forall (m:\mathbb{N}),\forall (r:\mathbb{R}),\mathrm{Anchor}.\mathrm{zeta}mr=(1+\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.a\cdot \mathrm{val}\left(\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.ellmr\right))$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.zeta (✓ 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.60 (Anchor.b).

$$\forall (m:\mathbb{N})(r:\mathbb{R}),\mathrm{Anchor}.bmr=\mathrm{NormedSpace}.\mathrm{normalize}(\mathrm{Anchor}.\mathrm{zeta}mr)$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.b (✓ 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.61 (Anchor.kernelBlock).

$$\forall (m:\mathbb{N}),\forall (r:\mathbb{R}),\forall (a:Sum(Fin2)(Finm)),\mathrm{Anchor}.\mathrm{kernelBlock}mra=(Sum.\mathrm{elim}\mapsto -(\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.a\cdot (\mathrm{starRingEnd}\mathbb{C})(\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.bmr)\cdot \mathrm{val}\left(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{anchorInterior}mri\right)+\mathrm{val}\left((\lambda (m:\mathbb{N})(r:\mathbb{R})(i:Finm)\mapsto \mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{anchorInterior}mri.rev)mri\right)))a)$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.kernelBlock (✓ 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.62 (Anchor.kernel).

$$\forall (m:\mathbb{N}),\forall (r:\mathbb{R}),\forall (a:Fin(m+2)),\mathrm{Anchor}.\mathrm{kernel}mra=(\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.\mathrm{kernelBlock}mr((\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.\mathrm{address}m).\mathrm{symm}a))$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.kernel (✓ 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.63 (Anchor.a_cartesian).

$$\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.a=\mathrm{val}\left(D5.S3.\mathrm{Quantum}.\mathrm{Information}.\mathrm{BinaryStabilizerLocalInequivalence}.s2.re\right)+\mathrm{val}\left(D5.S3.\mathrm{Quantum}.\mathrm{Information}.\mathrm{BinaryStabilizerLocalInequivalence}.s2.re\right)\cdot \mathrm{Complex}.I$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.a_cartesian (✓ 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.64 (Anchor.h_positive).

$$0<D5.S3.\mathrm{Quantum}.\mathrm{Information}.\mathrm{BinaryStabilizerLocalInequivalence}.s2.re$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.h_positive (✓ 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.65 (Anchor.ell_positive).

$$\forall (m:\mathbb{N}),(0<m)\to (\forall (r:\mathbb{R}),(5<r)\to (0<\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.ellmr))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.ell_positive (✓ 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.66 (Anchor.zeta_re).

$$\forall (m:\mathbb{N}),\forall (r:\mathbb{R}),(\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.\mathrm{zeta}mr).re=1+D5.S3.\mathrm{Quantum}.\mathrm{Information}.\mathrm{BinaryStabilizerLocalInequivalence}.s2.re\cdot \mathrm{UniformParameterAnchor}.\mathrm{Anchor}.ellmr$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.zeta_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.67 (Anchor.zeta_im).

$$\forall (m:\mathbb{N}),\forall (r:\mathbb{R}),(\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.\mathrm{zeta}mr).im=D5.S3.\mathrm{Quantum}.\mathrm{Information}.\mathrm{BinaryStabilizerLocalInequivalence}.s2.re\cdot \mathrm{UniformParameterAnchor}.\mathrm{Anchor}.ellmr$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.zeta_im (✓ 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.68 (Anchor.zeta_norm_pos).

$$\forall (m:\mathbb{N}),(0<m)\to (\forall (r:\mathbb{R}),(5<r)\to (0<\Vert \mathrm{UniformParameterAnchor}.\mathrm{Anchor}.\mathrm{zeta}mr\Vert ))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.zeta_norm_pos (✓ 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.69 (Anchor.b_unit).

$$\forall (m:\mathbb{N}),(0<m)\to (\forall (r:\mathbb{R}),(5<r)\to (\Vert \mathrm{UniformParameterAnchor}.\mathrm{Anchor}.bmr\Vert =1))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.b_unit (✓ 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.70 (Anchor.d).

$$\forall (m:\mathbb{N}),\forall (r:\mathbb{R}),\mathrm{Anchor}.dmr=(\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.a\cdot (\mathrm{starRingEnd}\mathbb{C})(\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.bmr))$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.d (✓ 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.71 (Anchor.d_unit).

$$\forall (m:\mathbb{N}),(0<m)\to (\forall (r:\mathbb{R}),(5<r)\to (\Vert \mathrm{UniformParameterAnchor}.\mathrm{Anchor}.dmr\Vert =1))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.d_unit (✓ 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.72 (Anchor.d_im_pos).

$$\forall (m:\mathbb{N}),(0<m)\to (\forall (r:\mathbb{R}),(5<r)\to (0<(\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.dmr).im))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.d_im_pos (✓ 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.73 (Anchor.coupling_real).

$$\forall (m:\mathbb{N}),\forall (f:Finm\to \mathbb{R}),((\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.\mathrm{coupling}m).\mathrm{conjTranspose}.\mathrm{mulVec}\lambda (i:Finm)\mapsto \mathrm{val}\left(fi\right))=![(\mathrm{starRingEnd}\mathbb{C})\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.a\cdot \mathrm{val}\left(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{spike}m\cdot f\right),\mathrm{val}\left((\lambda (i:Finm)\mapsto \mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{spike}mi.rev)\cdot f\right)]$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.coupling_real (✓ 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.74 (Anchor.actual_kernel).

$$\forall (m:\mathbb{N}),(4\le m)\to (\forall (r:\mathbb{R}),(5<r)\to ((r-\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.kmr=\Vert \mathrm{UniformParameterAnchor}.\mathrm{Anchor}.\mathrm{zeta}mr\Vert )\to ((\mathrm{ConstructionReduction}.D(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{anchorAlpha}(m+2))(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{beta}(m+2))r).\mathrm{mulVec}(\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.\mathrm{kernel}mr)=0)))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.actual_kernel (✓ 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.75 (Anchor.interior_hermitian).

$$\forall (m:\mathbb{N}),\forall (r:\mathbb{R}),(\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.\mathrm{interior}mr).\mathrm{IsHermitian}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.interior_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.76 (Anchor.interior_posDef).

$$\forall (m:\mathbb{N}),\forall (r:\mathbb{R}),(5<r)\to ((\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.\mathrm{interior}mr).\mathrm{PosDef})$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.interior_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.

Definition 1.77 (Anchor.inverseCoupling).

$$\forall (m:\mathbb{N}),\forall (r:\mathbb{R}),\mathrm{Anchor}.\mathrm{inverseCoupling}mr=(\lambda (i:Finm)(j:Fin2)\mapsto if\mathrm{val}\left(j\right)=0\mathrm{then}\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.a\cdot \mathrm{val}\left(\mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{anchorInterior}mri\right)\mathrm{else}\mathrm{val}\left((\lambda (m:\mathbb{N})(r:\mathbb{R})(i:Finm)\mapsto \mathrm{UniformParameterAnchor}.\mathrm{Uniform}.\mathrm{anchorInterior}mri.rev)mri\right))$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.inverseCoupling (✓ 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.78 (Anchor.inverseCoupling_solve).

$$\forall (m:\mathbb{N}),\forall (r:\mathbb{R}),(5<r)\to (\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.\mathrm{interior}mr\cdot \mathrm{UniformParameterAnchor}.\mathrm{Anchor}.\mathrm{inverseCoupling}mr=\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.\mathrm{coupling}m)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.inverseCoupling_solve (✓ 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.79 (Anchor.inverseCoupling_eq).

$$\forall (m:\mathbb{N}),\forall (r:\mathbb{R}),(5<r)\to (((\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.\mathrm{interior}mr){)}^{-1}\cdot \mathrm{UniformParameterAnchor}.\mathrm{Anchor}.\mathrm{coupling}m=\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.\mathrm{inverseCoupling}mr)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.inverseCoupling_eq (✓ 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.80 (Anchor.schur).

$$\forall (m:\mathbb{N}),\forall (r:\mathbb{R}),\mathrm{Anchor}.\mathrm{schur}mr=(!![\mathrm{val}\left(r-\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.kmr\right),-1-(\mathrm{starRingEnd}\mathbb{C})\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.a\cdot \mathrm{val}\left(\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.ellmr\right);-1-\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.a\cdot \mathrm{val}\left(\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.ellmr\right),\mathrm{val}\left(r-\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.kmr\right)])$$

Formalization. D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.schur (✓ 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.81 (Anchor.schur_eq).

$$\forall (m:\mathbb{N}),\forall (r:\mathbb{R}),(5<r)\to (\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.\mathrm{endpoints}r-(\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.\mathrm{coupling}m).\mathrm{conjTranspose}\cdot ((\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.\mathrm{interior}mr){)}^{-1}\cdot \mathrm{UniformParameterAnchor}.\mathrm{Anchor}.\mathrm{coupling}m=\mathrm{UniformParameterAnchor}.\mathrm{Anchor}.\mathrm{schur}mr)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.schur_eq (✓ 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/UniformParameterAnchor.R
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.a
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.a_cartesian
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.aa
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.aa_anchor
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.actual_kernel
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.address
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.admissible
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.alpha
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.alpha_anchor_distance
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.alpha_norm
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.anchorAlpha
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.anchorInterior
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.anchorInterior_positive
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.anchorInterior_solve
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.anchorInterior_upper
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.anchor_reindex
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.angle
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.b
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.b_unit
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.band
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.band_hermitian
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.band_reverse
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.band_row_bound
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.beta
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.block
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.coupling
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.coupling_real
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.d
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.d_im_pos
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.d_unit
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.den
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.ell
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.ell_positive
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.ell_value
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.endpoints
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.epsilon
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.epsilon_pos
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.h_positive
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.interior
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.interior_hermitian
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.interior_posDef
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.inverseCoupling
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.inverseCoupling_eq
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.inverseCoupling_solve
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.k
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.k_value
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.kernel
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.kernelBlock
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.knum
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.lnum
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.negative_eigenvalue_perturbation
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.numerators
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.operator_perturbation
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.pencil_top_largest
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.perturbation_error_small
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.phase_aligned_stability
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.phase_def
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.phase_mul_conj
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.phase_unit
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.probeSchur
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.rational_solve
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.resolvent
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.resolvent_isUnit
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.schur
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.schur_det_negative
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.schur_eq
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.shifted_gap
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.simple_root_of_rank
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.spike
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.spike_lower
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.stability_error_budget
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.surviving_projection
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.three_halfplanes_star
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.top_root_simple
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.u
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.uniform_coordinate_lower
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.zeta
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.zeta_im
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.zeta_norm_pos
• Truth anchor: D5/S3/Quantum/Entanglement/ChoiKiemKye/UniformParameterAnchor.zeta_re
• Dependency: D5/S3/Quantum/Entanglement/ChoiKiemKye/ConstructionReduction
• Dependency: D5/S3/Quantum/Information/BinaryStabilizerLocalInequivalence
• Dependency: D5/S3/SpectralTopology/HermitianEigenvaluePerturbation