Fixed positive products and the complete actual Pauli family

Abstract

Fixed spin products, the actual real Pauli action and complete unaveraged residual with exact local data.

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)$$

Theorem 1.1 (The actual residual scales on all joint inputs).

$$\forall t\in \mathbb{R},\forall H\in V,\forall X\in V,\forall Y\in V,E\left(t,H,X,Y\right)=t\cdot E\left(1,H,X,Y\right)$$

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

Source. Repository-derived.

Commentary.

The actual action and residual are affine in the real parameter. The zero-parameter residual vanishes on the complete product basis, and multilinearity extends this equality through the basis span in every slot, including arbitrary sums of pure tensors.

Theorem 1.2 (All ordered labels and every output coordinate).

$$\forall t\in \mathbb{R},R\left(t\right)=288\cdot (t{)}^2$$

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

Source. Repository-derived.

Commentary.

The complete unaveraged report uses 4096 ordered triples of the sixteen-element joint basis. At parameter one, six complete first-label blocks contribute 48 each; the other ten blocks vanish. Each squared norm includes every output coordinate. All-input scaling gives the displayed identity for every real parameter.

Theorem 1.3 (The complete fixed realization and all four original identities).

$$\forall 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))))))))))))))$$

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

Source. Repository-derived.

Commentary.

These are the complete fifteen conjuncts of the realization contract. The fixed products and positive inner products serve every parameter. No alternation, Jacobi, vanishing unit generator or global joint derivation law is assumed.

Theorem 1.4 (Attained defects, all-input bounds and operator norm).

$$\forall t\in \mathbb{R},((\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|))))$$

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

Source. Repository-derived.

Commentary.

The diagonal maximum is attained at (e(0)+e(1))/sqrt(2); the unit-generator maximum is attained at e(1). The universal estimates follow from nonnegative square decompositions on arbitrary real coordinates, and the last conjunct is the norm of the actual continuous unit-generator operator.

Theorem 1.5 (Every original local constant is sharp).

$$\forall t\in \mathbb{R},(\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)))))$$

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

Source. Repository-derived.

Commentary.

The unit length is one. The spin bound is attained with both inputs (e(0)+e(1))/sqrt(2), and the action bound at (t e(0)+e(3))/sqrt(1+t squared) and e(1). For arbitrary local a,b,c, the spin commutator is minus C(C(a,b),c), by the general vector triple-product identity. Two applications of the all-input cross-channel bound, obtained from the existing action estimate at parameter zero, give commutator norm at most norm(a) norm(b) norm(c). Specialization to the original unit basis gives the curvature upper bound without enumerating its entries. The same identity and orthonormal normalization give kappa(1,2,2)=e(1), attaining one on the original finite domain. This calibration supplies no new report escape or numeric consumer.

Theorem 1.6 (The full action Gram, both kernels, support and eigenvalues).

$$\forall t\in \mathbb{R},(\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)))))))$$

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

Source. Repository-derived.

Commentary.

The coordinate identity holds on every vector. The label kernel and common fixed kernel are distinguished as actual operator statements. The exact coordinates retain eigenvalue multiplicities and their collision at zero parameter.

Theorem 1.7 (The label Gram and attained positive action minimum).

$$\forall t\in \mathbb{R},(\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})))$$

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

Source. Repository-derived.

Commentary.

H is the label Gram, distinct from the action Gram G. The displayed eigenvalue equivalence includes all real eigenvalues, including collisions. The positive action eigenvalue minimum is attained at e(3), and its square-root gap is uniform.

Theorem 1.8 (Complete support, uniform gap, activity and zero boundary).

$$\forall t\in \mathbb{R},(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))))))$$

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

Source. Repository-derived.

Commentary.

Every support and activity conjunct concerns the same actual maps. At parameter zero the diagonal and unit-generator defects vanish, while the spatial action remains nonzero and the positive support gap remains sqrt(2). These are algebraic conclusions for this realization; no physical acquisition or general reconstruction conclusion follows.

References

• Truth anchor: D5/S3/Quantum/Algebra/PauliFixedProductFamily.exact_action_data
• Truth anchor: D5/S3/Quantum/Algebra/PauliFixedProductFamily.exact_constants
• Truth anchor: D5/S3/Quantum/Algebra/PauliFixedProductFamily.exact_defects
• Truth anchor: D5/S3/Quantum/Algebra/PauliFixedProductFamily.exact_label_data
• Truth anchor: D5/S3/Quantum/Algebra/PauliFixedProductFamily.exact_support_gap
• Truth anchor: D5/S3/Quantum/Algebra/PauliFixedProductFamily.family_contract
• Truth anchor: D5/S3/Quantum/Algebra/PauliFixedProductFamily.full_report
• Truth anchor: D5/S3/Quantum/Algebra/PauliFixedProductFamily.residual_scaling