A strict certificate for the same fixed-product Pauli realization

Abstract

The complete actual Pauli report gives strict improvement on the literal nonempty real interval.

Notation is shared by every display below. J is EuclideanSpace over the reals on Fin 4, identified with a scalar and a spatial vector in real three-space; V is its real Hilbert tensor product. T(a,b) denotes a tensor b. Coordinates a_i have i in Fin 4. All inner products and norms are the fixed Euclidean and positive tensor-product ones. Scalar juxtaposition denotes real scalar multiplication. The cross and dot operations are the usual real three-dimensional cross and dot products. An ordered pair (scalar, spatial triple) denotes its four-vector in J. The vectors e(i) are EuclideanSpace.single i 1; e(0) is the unit, e(1), e(2), e(3) are x, y, z. b is localBasis and B is jointBasis, the complete orthonormal bases. Every displayed parameter and vector is explicitly quantified.

$$(J=\mathrm{EuclideanSpace}\left(\mathbb{R},\mathrm{Fin}\left(4\right)\right))\wedge ((V=\mathrm{TensorProduct}\left(\mathbb{R},J,J\right))\wedge (\forall i\in \mathrm{Fin}\left(4\right),e\left(i\right)=\mathrm{single}\left(i,1\right)))$$

$$\forall a\in J,\forall b\in J,(S\left(a,b\right)=(a_0\cdot b_0+\mathrm{dot}\left((a_1,a_2,a_3),(b_1,b_2,b_3)\right),a_0\cdot (b_1,b_2,b_3)+b_0\cdot (a_1,a_2,a_3)))\wedge (C\left(a,b\right)=(0,\mathrm{cross}\left((a_1,a_2,a_3),(b_1,b_2,b_3)\right)))$$

$$\forall t\in \mathbb{R},\forall a\in J,\forall b\in J,D\left(t,a,b\right)=(0,\mathrm{cross}\left((a_1,a_2,a_3+t\cdot a_0),(b_1,b_2,b_3)\right))$$

$$\forall a\in J,\forall b\in J,\forall c\in J,\forall d\in J,M\left(T\left(a,b\right),T\left(c,d\right)\right)=T\left(S\left(a,c\right),S\left(b,d\right)\right)-T\left(C\left(a,c\right),C\left(b,d\right)\right)$$

$$\forall t\in \mathbb{R},\forall a\in J,\forall b\in J,\forall c\in J,\forall d\in J,\mathrm{Gamma}\left(t,T\left(a,b\right),T\left(c,d\right)\right)=T\left(D\left(t,a,c\right),S\left(b,d\right)\right)+T\left(S\left(a,c\right),D\left(t,b,d\right)\right)$$

S, C and D(t) denote the existing bilinear maps S, C, D t; M and Gamma(t) are the existing fixed joint product and actual joint action, extended linearly from pure tensors. E(t,H,X,Y) is E t H X Y. R(t) is reportSquared t, with all six basis indices summed independently. Each output norm includes every coordinate; there is no averaging.

$$\forall t\in \mathbb{R},\forall H\in V,\forall X\in V,\forall Y\in V,E\left(t,H,X,Y\right)=\mathrm{Gamma}\left(t,H,M\left(X,Y\right)\right)-M\left(\mathrm{Gamma}\left(t,H,X\right),Y\right)-M\left(X,\mathrm{Gamma}\left(t,H,Y\right)\right)$$

$$\forall t\in \mathbb{R},R\left(t\right)=\sum _{i,j,k,l,m,n:\mathrm{Fin}\left(4\right)}(\Vert E\left(t,T\left(e\left(i\right),e\left(j\right)\right),T\left(e\left(k\right),e\left(l\right)\right),T\left(e\left(m\right),e\left(n\right)\right)\right)\Vert {)}^2$$

U(t) means unitOperator t, the continuous linear map b mapped to D(t,e(0),b); its norm with subscript op is the operator norm. G(t) means actionGram t, H(t) means labelGram t. Adjoint is taken for the same Euclidean inner product. W(t) means actionSupport t, the real span of all actual D(t,e(i),e(j)); Z(t) means commonFixed t, the intersection of the four action kernels. ker D(t) is the kernel of the label-linear map a mapped to D(t,a), whereas D(t,a)=0 is equality of linear operators. Orthogonal complement always uses the fixed Euclidean inner product.

$$\forall t\in \mathbb{R},(\forall b\in J,U\left(t,b\right)=D\left(t,e\left(0\right),b\right))\wedge ((G\left(t\right)=\sum _{i:\mathrm{Fin}\left(4\right)}\mathrm{compose}\left(\mathrm{adj}\left(D\left(t,e\left(i\right)\right)\right),D\left(t,e\left(i\right)\right)\right))\wedge ((H\left(t\right)=\sum _{i:\mathrm{Fin}\left(4\right)}\mathrm{compose}\left(\mathrm{adj}\left(\mathrm{flipD}\left(t,e\left(i\right)\right)\right),\mathrm{flipD}\left(t,e\left(i\right)\right)\right))\wedge ((\forall a\in J,\forall b\in J,\mathrm{flipD}\left(t,b,a\right)=D\left(t,a,b\right))\wedge ((W\left(t\right)=\mathrm{span}\left(\mathbb{R},\{v:J\mid \exists i\in \mathrm{Fin}\left(4\right),\exists j\in \mathrm{Fin}\left(4\right),v=D\left(t,e\left(i\right),e\left(j\right)\right)\}\right))\wedge (Z\left(t\right)=\{a:J\mid \forall i\in \mathrm{Fin}\left(4\right),D\left(t,e\left(i\right),a\right)=0\})))))$$

Lambda(t) is positiveActionSpectrum t; sigma(t) is actionGap t, the square root of the infimum of that set. Membership and universal inequalities are both displayed for every greatest or least value below, so attainment and the full domain are retained. kappa(i,j,k) is curvature i j k on precisely the original finite basis, not a redefined unit-ball maximum.

$$\forall t\in \mathbb{R},(\mathrm{Lambda}\left(t\right)=\{lambda:\mathbb{R}\mid (0<lambda)\wedge (\exists a\in J,(a\ne 0)\wedge (G\left(t,a\right)=lambda\cdot a))\})\wedge (\mathrm{sigma}\left(t\right)=\sqrt{\inf \left(\mathrm{Lambda}\left(t\right)\right)})$$

$$\forall i\in \mathrm{Fin}\left(4\right),\forall j\in \mathrm{Fin}\left(4\right),\forall k\in \mathrm{Fin}\left(4\right),\mathrm{kappa}\left(i,j,k\right)=S\left(e\left(i\right),S\left(e\left(j\right),e\left(k\right)\right)\right)-S\left(e\left(j\right),S\left(e\left(i\right),e\left(k\right)\right)\right)$$

All definitions above are the actual fixed-product family, reproduced here so that the existential realization statement is closed and complete. Cstar is PauliLinearCertificate.constant = 1+2sqrt(2). epsilon(t) is epsilon t, d(t) is localBound t, eta is smallEndpoint. L(t) means PauliLinearCertificate.linear (epsilon t) (localBound t); O(t) means PauliLinearCertificate.old at those same arguments. q(t) below is its original quadratic root; O retains the independent local cap. The computed report yields epsilon(t)=12sqrt(2)|t|, rather than a selected-block readout.

$$(\mathrm{Cstar}\left(\right)=1+2\cdot \sqrt{2})\wedge ((\mathrm{eta}\left(\right)=\frac{1}{192\cdot \sqrt{2}\cdot (1+2\cdot \sqrt{2})})\wedge (\forall t\in \mathbb{R},(\mathrm{epsilon}\left(t\right)=\sqrt{R\left(t\right)})\wedge ((d\left(t\right)=\sqrt{1+(t{)}^2})\wedge ((L\left(t\right)=\frac{2\cdot (1+2\cdot \sqrt{2})\cdot \sqrt{1+(t{)}^2}\cdot \mathrm{epsilon}\left(t\right)}{\sqrt{2}-2\cdot (1+2\cdot \sqrt{2})\cdot \mathrm{epsilon}\left(t\right)})\wedge ((q\left(t\right)=\frac{(1+2\cdot \sqrt{2})\cdot \mathrm{epsilon}\left(t\right)+\sqrt{(1+2\cdot \sqrt{2}{)}^2\cdot (\mathrm{epsilon}\left(t\right){)}^2+4\cdot (1+2\cdot \sqrt{2})\cdot \sqrt{1+(t{)}^2}\cdot \mathrm{epsilon}\left(t\right)}}{2})\wedge (O\left(t\right)=\min \left(\sqrt{1+(t{)}^2},q\left(t\right)\right)))))))$$

Theorem 1.1 (The literal interval contains a nonzero real parameter).

$$\exists t\in \mathbb{R},(0<|t|)\wedge (|t|<\frac{1}{192\cdot \sqrt{2}\cdot (1+2\cdot \sqrt{2})})$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Algebra/PauliFixedProductLinear.small_interval_nonempty (✓ std3). ∎

Source. Repository-derived.

Commentary.

The endpoint is positive, and half of it is an explicit positive member. The ambient family still includes the zero parameter.

Theorem 1.2 (The actual defect lies below both the original root and cap).

$$\forall t\in \mathbb{R},((0<|t|)\wedge (|t|<\frac{1}{192\cdot \sqrt{2}\cdot (1+2\cdot \sqrt{2})}))\Rightarrow ((0<\sqrt{2}-2\cdot (1+2\cdot \sqrt{2})\cdot \mathrm{epsilon}\left(t\right))\wedge ((\exists a\in J,D\left(t,a,a\right)\ne 0)\wedge ((D\left(t,e\left(0\right)\right)\ne 0)\wedge ((\forall a\in J,(\Vert a\Vert =1)\Rightarrow (\Vert D\left(t,a,a\right)\Vert \le L\left(t\right)))\wedge ((\frac{|t|}{2}\le L\left(t\right))\wedge (L\left(t\right)<O\left(t\right)))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Algebra/PauliFixedProductLinear.actual_strict_improvement (✓ std3). ∎

Source. Repository-derived.

Commentary.

The six conjuncts include denominator positivity, both activity statements and domination for every unit vector. Since O(t) is the displayed minimum, strict inequality means strict improvement below both d(t) and q(t). The complete report gives epsilon in (0,1/(16 Cstar)); the literal interval also gives |t|<1 and hence 1<=d(t)<=sqrt(2). With x=Cstar epsilon, the linear certificate is at most 4x, strictly below sqrt(x), at most the quadratic root, and strictly below one and thus the cap. The exact attained diagonal defect gives domination. This proves the family-specific comparison; the general stability theorem for arbitrary products and actions is not asserted.

Theorem 1.3 (One actual parameter realizes all data and strict improvement together).

$$\exists t\in \mathbb{R},((\dim \left(\mathbb{R},J\right)=4)\wedge ((\dim \left(\mathbb{R},V\right)=16)\wedge ((\forall i\in \mathrm{Fin}\left(4\right),b\left(i\right)=e\left(i\right))\wedge ((\forall i\in \mathrm{Fin}\left(4\right),\forall j\in \mathrm{Fin}\left(4\right),B\left(i,j\right)=T\left(e\left(i\right),e\left(j\right)\right))\wedge ((\forall a\in J,\forall b\in J,S\left(a,b\right)=S\left(b,a\right))\wedge ((\forall a\in J,S\left(e\left(0\right),a\right)=a)\wedge ((\forall a\in J,\forall b\in J,\forall c\in J,⟨S\left(a,b\right),c⟩=⟨a,S\left(b,c\right)⟩)\wedge ((\forall a\in J,\forall b\in J,\forall c\in J,D\left(t,a,S\left(b,c\right)\right)=S\left(D\left(t,a,b\right),c\right)+S\left(b,D\left(t,a,c\right)\right))\wedge ((D\left(t,e\left(1\right),e\left(2\right)\right)=e\left(3\right))\wedge ((\forall X\in V,\forall Y\in V,M\left(X,Y\right)=M\left(Y,X\right))\wedge ((\forall X\in V,M\left(T\left(e\left(0\right),e\left(0\right)\right),X\right)=X)\wedge ((\forall X\in V,\forall Y\in V,\forall Z\in V,⟨M\left(X,Y\right),Z⟩=⟨X,M\left(Y,Z\right)⟩)\wedge ((\forall X\in V,(0\le ⟨X,X⟩)\wedge ((⟨X,X⟩=0)\iff (X=0)))\wedge ((\forall a\in J,\forall b\in J,\forall c\in J,\forall d\in J,(M\left(T\left(a,e\left(0\right)\right),T\left(c,d\right)\right)=T\left(S\left(a,c\right),d\right))\wedge ((M\left(T\left(e\left(0\right),b\right),T\left(c,d\right)\right)=T\left(c,S\left(b,d\right)\right))\wedge ((\mathrm{Gamma}\left(t,T\left(a,b\right),T\left(c,e\left(0\right)\right)\right)=T\left(D\left(t,a,c\right),b\right))\wedge (\mathrm{Gamma}\left(t,T\left(a,b\right),T\left(e\left(0\right),d\right)\right)=T\left(a,D\left(t,b,d\right)\right)))))\wedge (R\left(t\right)=288\cdot (t{)}^2)))))))))))))))\wedge ((((\frac{|t|}{2}\in \{s:\mathbb{R}\mid \exists a\in J,(\Vert a\Vert =1)\wedge (s=\Vert D\left(t,a,a\right)\Vert )\})\wedge (\forall r\in \mathbb{R},(r\in \{s:\mathbb{R}\mid \exists a\in J,(\Vert a\Vert =1)\wedge (s=\Vert D\left(t,a,a\right)\Vert )\})\Rightarrow (r\le \frac{|t|}{2})))\wedge (((|t|\in \{s:\mathbb{R}\mid \exists b\in J,(\Vert b\Vert =1)\wedge (s=\Vert D\left(t,e\left(0\right),b\right)\Vert )\})\wedge (\forall r\in \mathbb{R},(r\in \{s:\mathbb{R}\mid \exists b\in J,(\Vert b\Vert =1)\wedge (s=\Vert D\left(t,e\left(0\right),b\right)\Vert )\})\Rightarrow (r\le |t|)))\wedge ((\forall a\in J,\forall b\in J,\Vert S\left(a,b\right)\Vert \le \sqrt{2}\cdot \Vert a\Vert \cdot \Vert b\Vert )\wedge ((\forall a\in J,\forall b\in J,\Vert D\left(t,a,b\right)\Vert \le \sqrt{1+(t{)}^2}\cdot \Vert a\Vert \cdot \Vert b\Vert )\wedge (\Vert U\left(t\right){\Vert }_{op}=|t|)))))\wedge (((\Vert e\left(0\right)\Vert =1)\wedge (((\sqrt{2}\in \{s:\mathbb{R}\mid \exists a\in J,\exists b\in J,(\Vert a\Vert =1)\wedge ((\Vert b\Vert =1)\wedge (s=\Vert S\left(a,b\right)\Vert ))\})\wedge (\forall r\in \mathbb{R},(r\in \{s:\mathbb{R}\mid \exists a\in J,\exists b\in J,(\Vert a\Vert =1)\wedge ((\Vert b\Vert =1)\wedge (s=\Vert S\left(a,b\right)\Vert ))\})\Rightarrow (r\le \sqrt{2})))\wedge (((\sqrt{1+(t{)}^2}\in \{s:\mathbb{R}\mid \exists a\in J,\exists b\in J,(\Vert a\Vert =1)\wedge ((\Vert b\Vert =1)\wedge (s=\Vert D\left(t,a,b\right)\Vert ))\})\wedge (\forall r\in \mathbb{R},(r\in \{s:\mathbb{R}\mid \exists a\in J,\exists b\in J,(\Vert a\Vert =1)\wedge ((\Vert b\Vert =1)\wedge (s=\Vert D\left(t,a,b\right)\Vert ))\})\Rightarrow (r\le \sqrt{1+(t{)}^2})))\wedge ((1\in \{s:\mathbb{R}\mid \exists i\in \mathrm{Fin}\left(4\right),\exists j\in \mathrm{Fin}\left(4\right),\exists k\in \mathrm{Fin}\left(4\right),s=\Vert \mathrm{kappa}\left(i,j,k\right)\Vert \})\wedge (\forall r\in \mathbb{R},(r\in \{s:\mathbb{R}\mid \exists i\in \mathrm{Fin}\left(4\right),\exists j\in \mathrm{Fin}\left(4\right),\exists k\in \mathrm{Fin}\left(4\right),s=\Vert \mathrm{kappa}\left(i,j,k\right)\Vert \})\Rightarrow (r\le 1))))))\wedge (((\forall a\in J,G\left(t,a\right)=(0,\left(2+(t{)}^2\right)\cdot a_1,\left(2+(t{)}^2\right)\cdot a_2,2\cdot a_3))\wedge ((\forall a\in J,(\forall i\in \mathrm{Fin}\left(4\right),D\left(t,e\left(i\right),a\right)=0)\iff (\exists r\in \mathbb{R},a=r\cdot e\left(0\right)))\wedge ((\forall a\in J,(a\in W\left(t\right))\iff (a_0=0))\wedge ((\forall a\in J,(D\left(t,a\right)=0)\iff (\exists r\in \mathbb{R},a=r\cdot (e\left(0\right)-t\cdot e\left(3\right))))\wedge (\forall lambda\in \mathbb{R},(\exists a\in J,(a\ne 0)\wedge (G\left(t,a\right)=lambda\cdot a))\iff ((lambda=0)\vee ((lambda=2+(t{)}^2)\vee (lambda=2))))))))\wedge (((\forall a\in J,H\left(t,a\right)=(2\cdot (t{)}^2\cdot a_0+2\cdot t\cdot a_3,2\cdot a_1,2\cdot a_2,2\cdot t\cdot a_0+2\cdot a_3))\wedge ((\forall lambda\in \mathbb{R},(\exists a\in J,(a\ne 0)\wedge (H\left(t,a\right)=lambda\cdot a))\iff ((lambda=0)\vee ((lambda=2)\vee (lambda=2\cdot (1+(t{)}^2)))))\wedge (((2\in \mathrm{Lambda}\left(t\right))\wedge (\forall r\in \mathbb{R},(r\in \mathrm{Lambda}\left(t\right))\Rightarrow (2\le r)))\wedge (\mathrm{sigma}\left(t\right)=\sqrt{2}))))\wedge (((W\left(t\right)=(Z\left(t\right){)}^{\perp })\wedge ((\forall a\in J,(a\in W\left(t\right))\Rightarrow (2\cdot (\Vert a\Vert {)}^2\le ⟨a,G\left(t,a\right)⟩))\wedge (((e\left(3\right)\in W\left(t\right))\wedge ((\Vert e\left(3\right)\Vert =1)\wedge (G\left(t,e\left(3\right)\right)=2\cdot e\left(3\right))))\wedge ((D\left(t\right)\ne 0)\wedge (((t\ne 0)\Rightarrow ((\exists a\in J,D\left(t,a,a\right)\ne 0)\wedge ((D\left(t,e\left(0\right)\right)\ne 0)\wedge (\ker \left(D\left(t\right)\right)\ne Z\left(t\right)))))\wedge ((\forall a\in J,D\left(0,a,a\right)=0)\wedge (D\left(0,e\left(0\right)\right)=0)))))))\wedge ((0<|t|)\wedge ((|t|<\frac{1}{192\cdot \sqrt{2}\cdot (1+2\cdot \sqrt{2})})\wedge ((\exists a\in J,D\left(t,a,a\right)\ne 0)\wedge ((D\left(t,e\left(0\right)\right)\ne 0)\wedge ((\frac{|t|}{2}\le L\left(t\right))\wedge (L\left(t\right)<O\left(t\right))))))))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Algebra/PauliFixedProductLinear.nonempty_improvement (✓ std3). ∎

Source. Repository-derived.

Commentary.

The full six Family proposition bodies are displayed in this same-t existential conjunction, followed by the six interval, activity and comparison clauses. This particular declaration does not output denominator positivity or all-unit domination as additional conjuncts; those are outputs of actual_strict_improvement. The source realization, exact constants, both Gram operators, both kernels, spectra, support, uniform gap and zero-boundary data all belong to the same fixed-product family. No physical acquisition or general noisy-reconstruction conclusion is supplied.

References

• Truth anchor: D5/S3/Quantum/Algebra/PauliFixedProductLinear.actual_strict_improvement
• Truth anchor: D5/S3/Quantum/Algebra/PauliFixedProductLinear.nonempty_improvement
• Truth anchor: D5/S3/Quantum/Algebra/PauliFixedProductLinear.small_interval_nonempty
• Dependency: D5/S3/Quantum/Algebra/PauliFixedProductFamily