A generic-state counterexample in the kicked Ising chain

Abstract

Pathak’s generic-state negativity identity fails on a four-site kicked Ising chain.

For arbitrary local index types, partialTranspose sends the entry at ((a,b),(c,d)) to the input entry at ((a,d),(c,b)). It is definitionally equal to Bipartite.partialTranspose on the same complex matrix domain.

Definition 1.1 (Ising Hamiltonian).

$$\forall L\in \mathbb{N},\forall h\in \mathrm{Fin}\left(L\right)\to \mathbb{R},\mathrm{hIsing}\left(h\right)=\mathrm{smul}\left(\mathrm{ofReal}\left(\frac{\pi }{4}\right),\sum _{i:\mathrm{Fin}\left(L\right)}((\mathrm{localOp}\left(i,qubitZ\right))\cdot (\mathrm{localOp}\left(\mathrm{finRotate}\left(L\right)\left(i\right),qubitZ\right)))\right)+\sum _{i:\mathrm{Fin}\left(L\right)}(\mathrm{smul}\left(\mathrm{ofReal}\left(h\left(i\right)\right),\mathrm{localOp}\left(i,qubitZ\right)\right))$$

Formalization. D5/S3/Quantum/Dynamics/KickedIsingNegativityRefutation.hIsing (✓ std3).

Citation. T. Pathak (2026). Mixed-State Entanglement in a Minimal Model of Quantum Chaos. DOI: 10.48550/arXiv.2603.14292. URL: https://arxiv.org/abs/2603.14292v1.

Commentary.

Equation (1), p. 1, defines H_I = J ∑ᵢ σᶻᵢσᶻᵢ₊₁ + ∑ᵢ hᵢσᶻᵢ. The source states: “We specifically consider J = π/4, b = −π/4 for our analysis.” Sites use Fin L, with finRotate L as the periodic successor; ↑ and ↓ are 0 and 1. The frozen localOp embeds a qubit matrix at its site, and qubitZ is the Pauli Z matrix. Real coefficients enter ℂ through ofReal; smul is scalar multiplication.

Definition 1.2 (Kick Hamiltonian).

$$\forall L\in \mathbb{N},\mathrm{hKick}\left(L\right)=\mathrm{smul}\left(\mathrm{ofReal}\left(\frac{0-(\pi )}{4}\right),\sum _{i:\mathrm{Fin}\left(L\right)}(\mathrm{localOp}\left(i,qubitX\right))\right)$$

Formalization. D5/S3/Quantum/Dynamics/KickedIsingNegativityRefutation.hKick (✓ std3).

Citation. T. Pathak (2026). Mixed-State Entanglement in a Minimal Model of Quantum Chaos. DOI: 10.48550/arXiv.2603.14292. URL: https://arxiv.org/abs/2603.14292v1.

Commentary.

Equation (1), p. 1, defines H_K = ∑ᵢ b σˣᵢ. Here b = −π/4; qubitX is the frozen Pauli X matrix.

Definition 1.3 (Literal Floquet operator).

$$\forall L\in \mathbb{N},\forall h\in \mathrm{Fin}\left(L\right)\to \mathbb{R},\mathrm{floquet}\left(h\right)=(NormedSpace.exp\left(\mathrm{smul}\left(0-(Complex.I),\mathrm{hKick}\left(L\right)\right)\right))\cdot (NormedSpace.exp\left(\mathrm{smul}\left(0-(Complex.I),\mathrm{hIsing}\left(h\right)\right)\right))$$

Formalization. D5/S3/Quantum/Dynamics/KickedIsingNegativityRefutation.floquet (✓ std3).

Citation. T. Pathak (2026). Mixed-State Entanglement in a Minimal Model of Quantum Chaos. DOI: 10.48550/arXiv.2603.14292. URL: https://arxiv.org/abs/2603.14292v1.

Commentary.

Equation (2), p. 1: U = U_K U_I. The source states “where U_I = e^{−i H_I} and U_K = e^{−i H_K}.” The matrix exponentials are NormedSpace.exp, and I in Complex.I denotes the imaginary unit.

Definition 1.4 (Initial product state).

$$\forall L\in \mathbb{N},\forall theta\in \mathrm{Fin}\left(L\right)\to \mathbb{R},\forall phi\in \mathrm{Fin}\left(L\right)\to \mathbb{R},\forall x\in \mathrm{Fin}\left(L\right)\to \mathrm{Fin}\left(2\right),\mathrm{initial}\left(theta,phi\right)\left(x\right)=\prod _{i:\mathrm{Fin}\left(L\right)}(\mathrm{ite}\left(x\left(i\right)=0,\mathrm{ofReal}\left(Real.cos\left(\frac{theta\left(i\right)}{2}\right)\right),(Complex.exp\left((Complex.I)\cdot (\mathrm{ofReal}\left(phi\left(i\right)\right))\right))\cdot (\mathrm{ofReal}\left(Real.sin\left(\frac{theta\left(i\right)}{2}\right)\right))\right))$$

Formalization. D5/S3/Quantum/Dynamics/KickedIsingNegativityRefutation.initial (✓ std3).

Citation. T. Pathak (2026). Mixed-State Entanglement in a Minimal Model of Quantum Chaos. DOI: 10.48550/arXiv.2603.14292. URL: https://arxiv.org/abs/2603.14292v1.

Commentary.

Equation (3), pp. 1–2: |ψ_{θ,φ}⟩ = ⊗ₖ (cos(θₖ/2)|↑⟩ + e^{iφₖ}sin(θₖ/2)|↓⟩). The formula displays the computational-basis amplitude at x. The letters theta and phi encode the Lean parameters θ and φ. All trigonometric arguments are real, and their values are embedded in ℂ by ofReal. The conditional ite(c,a,b) selects a when c holds and b otherwise.

Definition 1.5 (Generic states).

$$\forall L\in \mathbb{N},\forall theta\in \mathrm{Fin}\left(L\right)\to \mathbb{R},\mathrm{generic}\left(theta\right)\iff ((\neg (\forall i\in \mathrm{Fin}\left(L\right),theta\left(i\right)=\frac{\pi }{2}))\wedge (\neg (\forall i\in \mathrm{Fin}\left(L\right),(theta\left(i\right)=0)\vee (theta\left(i\right)=\pi ))))$$

Formalization. D5/S3/Quantum/Dynamics/KickedIsingNegativityRefutation.generic (✓ std3).

Citation. T. Pathak (2026). Mixed-State Entanglement in a Minimal Model of Quantum Chaos. DOI: 10.48550/arXiv.2603.14292. URL: https://arxiv.org/abs/2603.14292v1.

Commentary.

Page 2 states verbatim: “States which do not belong to these class will henceforth be called generic.” Equation (4) defines the transverse class by θₖ = π/2 for every site and the longitudinal class by θₖ ∈ {0,π} for every site. Thus generic excludes both classes, rather than imposing randomness or a measure-theoretic qualifier.

Definition 1.6 (Half-order Rényi entropy).

$$\forall n\in Type,[\mathrm{Fintype}\left(n\right)][\mathrm{DecidableEq}\left(n\right)]\forall rho\in \mathrm{Matrix}\left(n,n,\mathbb{C}\right),\mathrm{renyiHalf}\left(rho\right)=(2)\cdot (Real.log\left(Complex.re\left(Matrix.trace\left(\mathrm{cfc}\left(Real.sqrt,rho\right)\right)\right)\right))$$

Formalization. D5/S3/Quantum/Dynamics/KickedIsingNegativityRefutation.renyiHalf (✓ std3).

Citation. T. Pathak (2026). Mixed-State Entanglement in a Minimal Model of Quantum Chaos. DOI: 10.48550/arXiv.2603.14292. URL: https://arxiv.org/abs/2603.14292v1.

Commentary.

Equation (9), p. 2, defines S_A^(α) = (1/(1−α)) log(tr(ρ_A^α)). At α = 1/2 this is twice the logarithm of the trace of the matrix square root. For density matrices cfc Real.sqrt is precisely that square root, and the trace is real. The real part makes the ℝ-valued expression explicit. On non-Hermitian inputs the real continuous functional calculus is zero. Anonymous bracket entries record the Lean typeclass arguments.

Definition 1.7 (Contiguous cyclic tripartition).

$$\forall L\in \mathbb{N},\forall A\in \mathrm{Finset}\left(\mathrm{Fin}\left(L\right)\right),\forall B\in \mathrm{Finset}\left(\mathrm{Fin}\left(L\right)\right),\forall C\in \mathrm{Finset}\left(\mathrm{Fin}\left(L\right)\right),\mathrm{contiguous}\left(A,B,C\right)\iff (\exists o\in \mathbb{N},\exists a\in \mathbb{N},\exists b\in \mathbb{N},(0<a)\wedge ((a<b)\wedge ((b<L)\wedge ((A=Finset.filter\left((i:\mathrm{Fin}\left(L\right))\mapsto \mathrm{val}\left(\left((\mathrm{finRotate}\left(L\right){)}^o\right)\left(i\right)\right)<a,Finset.univ\right))\wedge ((B=Finset.filter\left((i:\mathrm{Fin}\left(L\right))\mapsto (a\le \mathrm{val}\left(\left((\mathrm{finRotate}\left(L\right){)}^o\right)\left(i\right)\right))\wedge (\mathrm{val}\left(\left((\mathrm{finRotate}\left(L\right){)}^o\right)\left(i\right)\right)<b),Finset.univ\right))\wedge (C=Finset.filter\left((i:\mathrm{Fin}\left(L\right))\mapsto b\le \mathrm{val}\left(\left((\mathrm{finRotate}\left(L\right){)}^o\right)\left(i\right)\right),Finset.univ\right)))))))$$

Formalization. D5/S3/Quantum/Dynamics/KickedIsingNegativityRefutation.contiguous (✓ std3).

Citation. T. Pathak (2026). Mixed-State Entanglement in a Minimal Model of Quantum Chaos. DOI: 10.48550/arXiv.2603.14292. URL: https://arxiv.org/abs/2603.14292v1.

Commentary.

Page 2 states: “In the following we now consider a tri-partition of state ABC with subsystem size L_A,L_B and L_C.” The periodic chain is cut at a and b after a rotation by o. The three blocks are nonempty and disjoint and exhaust the sites. The val function extracts the natural value of a Fin index; the exponent o is a natural permutation power.

Definition 1.8 (Join subsystem coordinates).

$$\forall L\in \mathbb{N},\forall A\in \mathrm{Finset}\left(\mathrm{Fin}\left(L\right)\right),\forall B\in \mathrm{Finset}\left(\mathrm{Fin}\left(L\right)\right),\forall x\in \mathrm{Subtype}\left((i:\mathrm{Fin}\left(L\right))\mapsto i\in A\right)\to \mathrm{Fin}\left(2\right),\forall y\in \mathrm{Subtype}\left((i:\mathrm{Fin}\left(L\right))\mapsto i\in B\right)\to \mathrm{Fin}\left(2\right),\forall z\in \mathrm{Outside}\left(A\cup B\right)\to \mathrm{Fin}\left(2\right),\forall i\in \mathrm{Fin}\left(L\right),\mathrm{joinParts}\left(A,B,x,y,z\right)\left(i\right)=\mathrm{dite}\left(i\in A,(hA:i\in A)\mapsto x\left(Subtype.mk\left(i,hA\right)\right),(hA:\neg i\in A)\mapsto \mathrm{dite}\left(i\in B,(hB:i\in B)\mapsto y\left(Subtype.mk\left(i,hB\right)\right),(hB:\neg i\in B)\mapsto z\left(Subtype.mk\left(i,Finset.notMe{m}_{union}.mpr\left(⟨hA,hB⟩\right)\right)\right)\right)\right)$$

Formalization. D5/S3/Quantum/Dynamics/KickedIsingNegativityRefutation.joinParts (✓ std3).

Citation. T. Pathak (2026). Mixed-State Entanglement in a Minimal Model of Quantum Chaos. DOI: 10.48550/arXiv.2603.14292. URL: https://arxiv.org/abs/2603.14292v1.

Commentary.

The coordinates x, y and z lie on A, B and the complement of A ∪ B. The dependent conditional dite supplies membership proofs hA and hB to Subtype.mk. In the final branch hA and hB are nonmembership hypotheses, and Finset.notMem_union.mpr ⟨hA, hB⟩ proves membership in the complement. Outside is the frozen complement subtype. On disjoint blocks these assignments combine to one chain configuration, as used in the partial-trace expression on p. 2.

Definition 1.9 (Joint reduced density matrix).

$$\forall L\in \mathbb{N},\forall A\in \mathrm{Finset}\left(\mathrm{Fin}\left(L\right)\right),\forall B\in \mathrm{Finset}\left(\mathrm{Fin}\left(L\right)\right),\forall psi\in \left(\mathrm{Fin}\left(L\right)\to \mathrm{Fin}\left(2\right)\right)\to \mathbb{C},\mathrm{reducedAB}\left(A,B,psi\right)=\mathrm{partialTraceRight}\left(Matrix.vecMulVec\left((p:((\mathrm{Subtype}\left((i:\mathrm{Fin}\left(L\right))\mapsto i\in A\right)\to \mathrm{Fin}\left(2\right))\times (\mathrm{Subtype}\left((i:\mathrm{Fin}\left(L\right))\mapsto i\in B\right)\to \mathrm{Fin}\left(2\right)))\times (\mathrm{Outside}\left(A\cup B\right)\to \mathrm{Fin}\left(2\right)))\mapsto psi\left(\mathrm{joinParts}\left(A,B,\mathrm{fst}\left(\mathrm{fst}\left(p\right)\right),\mathrm{snd}\left(\mathrm{fst}\left(p\right)\right),\mathrm{snd}\left(p\right)\right)\right),\mathrm{star}\left((p:((\mathrm{Subtype}\left((i:\mathrm{Fin}\left(L\right))\mapsto i\in A\right)\to \mathrm{Fin}\left(2\right))\times (\mathrm{Subtype}\left((i:\mathrm{Fin}\left(L\right))\mapsto i\in B\right)\to \mathrm{Fin}\left(2\right)))\times (\mathrm{Outside}\left(A\cup B\right)\to \mathrm{Fin}\left(2\right)))\mapsto psi\left(\mathrm{joinParts}\left(A,B,\mathrm{fst}\left(\mathrm{fst}\left(p\right)\right),\mathrm{snd}\left(\mathrm{fst}\left(p\right)\right),\mathrm{snd}\left(p\right)\right)\right)\right)\right)\right)$$

Formalization. D5/S3/Quantum/Dynamics/KickedIsingNegativityRefutation.reducedAB (✓ std3).

Citation. T. Pathak (2026). Mixed-State Entanglement in a Minimal Model of Quantum Chaos. DOI: 10.48550/arXiv.2603.14292. URL: https://arxiv.org/abs/2603.14292v1.

Commentary.

Page 2 defines ρ_AB(t) = tr_C(|ψ(t)⟩⟨ψ(t)|). The coordinate function inside vecMulVec is the same ψ expressed on the product of the retained blocks and the complement. Its star is complex conjugation, so vecMulVec forms the rank-one density matrix. The frozen partialTraceRight sums over the complement.

Definition 1.10 (Integer-time evolution).

$$\forall L\in \mathbb{N},\forall h\in \mathrm{Fin}\left(L\right)\to \mathbb{R},\forall theta\in \mathrm{Fin}\left(L\right)\to \mathbb{R},\forall phi\in \mathrm{Fin}\left(L\right)\to \mathbb{R},\forall t\in \mathbb{Z},\mathrm{evolved}\left(h,theta,phi,t\right)=Matrix.mulVec\left((\mathrm{floquet}\left(h\right){)}^t,\mathrm{initial}\left(theta,phi\right)\right)$$

Formalization. D5/S3/Quantum/Dynamics/KickedIsingNegativityRefutation.evolved (✓ std3).

Citation. T. Pathak (2026). Mixed-State Entanglement in a Minimal Model of Quantum Chaos. DOI: 10.48550/arXiv.2603.14292. URL: https://arxiv.org/abs/2603.14292v1.

Commentary.

The source evolves the initial state with U_KI[h]^t (supplement, p. 6). The exponent is an integer power of the literal Floquet matrix, and Matrix.mulVec is its action on the amplitude vector. The counterexample uses t = 1.

Definition 1.11 (Logarithmic negativity).

$$\forall A\in Type,\forall B\in Type,[\mathrm{Fintype}\left(A\right)][\mathrm{Fintype}\left(B\right)][\mathrm{DecidableEq}\left(A\right)][\mathrm{DecidableEq}\left(B\right)]\forall rho\in \mathrm{Matrix}\left((A)\times (B),(A)\times (B),\mathbb{C}\right),\mathrm{logNegativity}\left(rho\right)=Real.log\left(\mathrm{traceNorm}\left(\mathrm{partialTranspose}\left(rho\right)\right)\right)$$

Formalization. D5/S3/Quantum/Dynamics/KickedIsingNegativityRefutation.logNegativity (✓ std3).

Citation. T. Pathak (2026). Mixed-State Entanglement in a Minimal Model of Quantum Chaos. DOI: 10.48550/arXiv.2603.14292. URL: https://arxiv.org/abs/2603.14292v1.

Commentary.

Equation (5), p. 2: 𝓔(t) = ln tr(√((ρ_AB^{T_B}(t))†ρ_AB^{T_B}(t))). The frozen traceNorm is defined by precisely this trace-of-square-root expression, with conjTranspose as the adjoint. Real.log is the natural logarithm.

Definition 1.12 (Half-order Rényi mutual information).

$$\forall A\in Type,\forall B\in Type,[\mathrm{Fintype}\left(A\right)][\mathrm{Fintype}\left(B\right)][\mathrm{DecidableEq}\left(A\right)][\mathrm{DecidableEq}\left(B\right)]\forall rho\in \mathrm{Matrix}\left((A)\times (B),(A)\times (B),\mathbb{C}\right),\mathrm{mutualHalf}\left(rho\right)=\mathrm{renyiHalf}\left(\mathrm{partialTraceRight}\left(rho\right)\right)+\mathrm{renyiHalf}\left(\mathrm{partialTraceLeft}\left(rho\right)\right)-\mathrm{renyiHalf}\left(rho\right)$$

Formalization. D5/S3/Quantum/Dynamics/KickedIsingNegativityRefutation.mutualHalf (✓ std3).

Citation. T. Pathak (2026). Mixed-State Entanglement in a Minimal Model of Quantum Chaos. DOI: 10.48550/arXiv.2603.14292. URL: https://arxiv.org/abs/2603.14292v1.

Commentary.

Equation (9), p. 2: I_{A:B}^(α)(t) = S_A^(α)(t) + S_B^(α)(t) − S_AB^(α)(t). Here α = 1/2, partialTraceRight retains A and partialTraceLeft retains B.

Definition 1.13 (Pathak’s Conjecture 1 at half order).

$$claim\iff (\forall L\in \mathbb{N},\forall h\in \mathrm{Fin}\left(L\right)\to \mathbb{R},\forall theta\in \mathrm{Fin}\left(L\right)\to \mathbb{R},\forall phi\in \mathrm{Fin}\left(L\right)\to \mathbb{R},\forall A\in \mathrm{Finset}\left(\mathrm{Fin}\left(L\right)\right),\forall B\in \mathrm{Finset}\left(\mathrm{Fin}\left(L\right)\right),\forall C\in \mathrm{Finset}\left(\mathrm{Fin}\left(L\right)\right),\forall t\in \mathbb{Z},(\mathrm{contiguous}\left(A,B,C\right))\Rightarrow ((\mathrm{generic}\left(theta\right))\Rightarrow ((2)\cdot (\mathrm{logNegativity}\left(\mathrm{reducedAB}\left(A,B,\mathrm{evolved}\left(h,theta,phi,t\right)\right)\right))=\mathrm{mutualHalf}\left(\mathrm{reducedAB}\left(A,B,\mathrm{evolved}\left(h,theta,phi,t\right)\right)\right))))$$

Formalization. D5/S3/Quantum/Dynamics/KickedIsingNegativityRefutation.claim (✓ std3).

Citation. T. Pathak (2026). Mixed-State Entanglement in a Minimal Model of Quantum Chaos. DOI: 10.48550/arXiv.2603.14292. URL: https://arxiv.org/abs/2603.14292v1.

Commentary.

Conjecture 1, p. 3, states verbatim: “2𝓔(t) = I_{A:B}^{(α)}(t), hold for generic states at all times t.” This is its α = 1/2 specialization, quantified over the chain length, real fields, product-state angles, contiguous tripartition and integer time. Each allowed tripartition has nonempty blocks. The specific fields are hᵢ = 1, with phases φᵢ = 0, for the counterexample.

Theorem 1.14 (Partial trace under a right unitary).

$$\forall a\in Type,\forall b\in Type,[\mathrm{Fintype}\left(a\right)][\mathrm{Fintype}\left(b\right)][\mathrm{DecidableEq}\left(a\right)][\mathrm{DecidableEq}\left(b\right)]\forall rho\in \mathrm{Matrix}\left((a)\times (b),(a)\times (b),\mathbb{C}\right),\forall V\in \mathrm{Matrix}\left(b,b,\mathbb{C}\right),((Matrix.conjTranspose\left(V\right))\cdot (V)=1)\Rightarrow (D5.S3.Quantum.Information.PartialTraceMutualInformation.partialTraceRight\left(((Matrix.kronecker\left(1,V\right))\cdot (rho))\cdot (Matrix.conjTranspose\left(Matrix.kronecker\left(1,V\right)\right))\right)=D5.S3.Quantum.Information.PartialTraceMutualInformation.partialTraceRight\left(rho\right))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/KickedIsingNegativityRefutation.trace_conjugate_right (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. T. Pathak (2026). Mixed-State Entanglement in a Minimal Model of Quantum Chaos. DOI: 10.48550/arXiv.2603.14292. URL: https://arxiv.org/abs/2603.14292v1.

Commentary.

For arbitrary finite index types a and b with decidable equality, conjugating a complex bipartite operator by the identity on a and a matrix V on b with V adjoint times V equal to the identity leaves the partial trace over b unchanged.

Theorem 1.15 (Partial trace under left conjugation).

$$\forall a\in Type,\forall b\in Type,[\mathrm{Fintype}\left(a\right)][\mathrm{Fintype}\left(b\right)][\mathrm{DecidableEq}\left(a\right)][\mathrm{DecidableEq}\left(b\right)]\forall rho\in \mathrm{Matrix}\left((a)\times (b),(a)\times (b),\mathbb{C}\right),\forall U\in \mathrm{Matrix}\left(a,a,\mathbb{C}\right),D5.S3.Quantum.Information.PartialTraceMutualInformation.partialTraceRight\left(((Matrix.kronecker\left(U,1\right))\cdot (rho))\cdot (Matrix.conjTranspose\left(Matrix.kronecker\left(U,1\right)\right))\right)=((U)\cdot (D5.S3.Quantum.Information.PartialTraceMutualInformation.partialTraceRight\left(rho\right)))\cdot (Matrix.conjTranspose\left(U\right))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/KickedIsingNegativityRefutation.trace_conjugate_left (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. T. Pathak (2026). Mixed-State Entanglement in a Minimal Model of Quantum Chaos. DOI: 10.48550/arXiv.2603.14292. URL: https://arxiv.org/abs/2603.14292v1.

Commentary.

For arbitrary finite index types a and b with decidable equality, conjugating a complex bipartite operator by U on a and the identity on b conjugates its partial trace over b by U. The matrix U is arbitrary.

Theorem 1.16 (Partial trace under local conjugation).

$$\forall a\in Type,\forall b\in Type,[\mathrm{Fintype}\left(a\right)][\mathrm{Fintype}\left(b\right)][\mathrm{DecidableEq}\left(a\right)][\mathrm{DecidableEq}\left(b\right)]\forall rho\in \mathrm{Matrix}\left((a)\times (b),(a)\times (b),\mathbb{C}\right),\forall U\in \mathrm{Matrix}\left(a,a,\mathbb{C}\right),\forall V\in \mathrm{Matrix}\left(b,b,\mathbb{C}\right),((Matrix.conjTranspose\left(V\right))\cdot (V)=1)\Rightarrow (D5.S3.Quantum.Information.PartialTraceMutualInformation.partialTraceRight\left(((Matrix.kronecker\left(U,V\right))\cdot (rho))\cdot (Matrix.conjTranspose\left(Matrix.kronecker\left(U,V\right)\right))\right)=((U)\cdot (D5.S3.Quantum.Information.PartialTraceMutualInformation.partialTraceRight\left(rho\right)))\cdot (Matrix.conjTranspose\left(U\right)))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/KickedIsingNegativityRefutation.trace_local_right (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. T. Pathak (2026). Mixed-State Entanglement in a Minimal Model of Quantum Chaos. DOI: 10.48550/arXiv.2603.14292. URL: https://arxiv.org/abs/2603.14292v1.

Commentary.

For arbitrary finite index types a and b with decidable equality, conjugation by U tensor V acts on the partial trace over b as conjugation by U whenever V adjoint times V equals the identity. The operator rho and the matrix U are arbitrary complex matrices of the displayed sizes.

Theorem 1.17 (The left partial trace under local conjugation).

$$\forall a\in Type,\forall b\in Type,[\mathrm{Fintype}\left(a\right)][\mathrm{Fintype}\left(b\right)][\mathrm{DecidableEq}\left(a\right)][\mathrm{DecidableEq}\left(b\right)]\forall rho\in \mathrm{Matrix}\left((a)\times (b),(a)\times (b),\mathbb{C}\right),\forall U\in \mathrm{Matrix}\left(a,a,\mathbb{C}\right),\forall V\in \mathrm{Matrix}\left(b,b,\mathbb{C}\right),((Matrix.conjTranspose\left(U\right))\cdot (U)=1)\Rightarrow (D5.S3.Quantum.Information.PartialTraceMutualInformation.partialTraceLeft\left(((Matrix.kronecker\left(U,V\right))\cdot (rho))\cdot (Matrix.conjTranspose\left(Matrix.kronecker\left(U,V\right)\right))\right)=((V)\cdot (D5.S3.Quantum.Information.PartialTraceMutualInformation.partialTraceLeft\left(rho\right)))\cdot (Matrix.conjTranspose\left(V\right)))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/KickedIsingNegativityRefutation.trace_local_left (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. T. Pathak (2026). Mixed-State Entanglement in a Minimal Model of Quantum Chaos. DOI: 10.48550/arXiv.2603.14292. URL: https://arxiv.org/abs/2603.14292v1.

Commentary.

For arbitrary finite index types a and b with decidable equality, conjugation by U tensor V acts on the partial trace over a as conjugation by V whenever U adjoint times U equals the identity. The operator rho and the matrix V are arbitrary complex matrices of the displayed sizes.

Theorem 1.18 (Partial transpose under local conjugation).

$$\forall rho\in \mathrm{Matrix}\left((\mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right))\times (\mathrm{Fin}\left(2\right)),\mathbb{C}\right),\forall U\in \mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right),\forall V\in \mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right),D5.S3.Quantum.Entanglement.StructuredNegativityCoincidenceRefutation.partialTransposeB\left(((Matrix.kronecker\left(U,V\right))\cdot (rho))\cdot (Matrix.conjTranspose\left(Matrix.kronecker\left(U,V\right)\right))\right)=((Matrix.kronecker\left(U,Matrix.map\left(V,star\right)\right))\cdot (D5.S3.Quantum.Entanglement.StructuredNegativityCoincidenceRefutation.partialTransposeB\left(rho\right)))\cdot (Matrix.conjTranspose\left(Matrix.kronecker\left(U,Matrix.map\left(V,star\right)\right)\right))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/KickedIsingNegativityRefutation.partialTransposeB_kronecker_conj (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. T. Pathak (2026). Mixed-State Entanglement in a Minimal Model of Quantum Chaos. DOI: 10.48550/arXiv.2603.14292. URL: https://arxiv.org/abs/2603.14292v1.

Commentary.

For every complex two-qubit matrix rho and arbitrary complex two-by-two matrices U and V, partial transposition on the second factor carries conjugation by U tensor V to conjugation by U tensor the entrywise complex conjugate of V. No Hermitian or unitary hypothesis is required.

Theorem 1.19 (Refutation).

$$\neg claim$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/KickedIsingNegativityRefutation.result (✓ std3). ∎

Resolves. Problems/pathak-2026-kicked-ising-negativity-refutation (refuted) by D5/S3/Quantum/Dynamics/KickedIsingNegativityRefutation.result.

Source. Repository-derived.

Acknowledgement. T. Pathak (2026). Mixed-State Entanglement in a Minimal Model of Quantum Chaos. DOI: 10.48550/arXiv.2603.14292. URL: https://arxiv.org/abs/2603.14292v1.

Commentary.

Take L = 4, A = {0}, B = {1}, C = {2,3}, t = 1, hᵢ = 1 and φᵢ = 0. The initial state is |+⟩|+⟩|r⟩|r⟩, where |r⟩ = (2|0⟩+|1⟩)/√5, encoded by θ = (π/2,π/2,2 arctan(1/2),2 arctan(1/2)). It is generic. Factoring the commuting kick exponentials and the diagonal Ising exponential gives U = −W^{⊗4}G, with W a single-qubit unitary and G the periodic product of controlled-Z gates. The local unitaries preserve both measures. Before their action, the reduced density matrix has spectrum {16/25,4/25,4/25,1/25}; its partial transpose has spectrum {23/50,17/50,17/50,−7/50}, and both marginals are 1/2 times the identity. Hence 2𝓔(1) = log(1024/625) and I_{A:B}^(1/2)(1) = log(100/81). Strict injectivity of the logarithm on positive reals and the unequal rational arguments contradict the asserted equality. These finite-chain values do not settle a thermodynamic-limit identity at early times.

References

• Truth anchor: D5/S3/Quantum/Dynamics/KickedIsingNegativityRefutation.claim
• Truth anchor: D5/S3/Quantum/Dynamics/KickedIsingNegativityRefutation.contiguous
• Truth anchor: D5/S3/Quantum/Dynamics/KickedIsingNegativityRefutation.evolved
• Truth anchor: D5/S3/Quantum/Dynamics/KickedIsingNegativityRefutation.floquet
• Truth anchor: D5/S3/Quantum/Dynamics/KickedIsingNegativityRefutation.generic
• Truth anchor: D5/S3/Quantum/Dynamics/KickedIsingNegativityRefutation.hIsing
• Truth anchor: D5/S3/Quantum/Dynamics/KickedIsingNegativityRefutation.hKick
• Truth anchor: D5/S3/Quantum/Dynamics/KickedIsingNegativityRefutation.initial
• Truth anchor: D5/S3/Quantum/Dynamics/KickedIsingNegativityRefutation.joinParts
• Truth anchor: D5/S3/Quantum/Dynamics/KickedIsingNegativityRefutation.logNegativity
• Truth anchor: D5/S3/Quantum/Dynamics/KickedIsingNegativityRefutation.mutualHalf
• Truth anchor: D5/S3/Quantum/Dynamics/KickedIsingNegativityRefutation.partialTransposeB_kronecker_conj
• Truth anchor: D5/S3/Quantum/Dynamics/KickedIsingNegativityRefutation.reducedAB
• Truth anchor: D5/S3/Quantum/Dynamics/KickedIsingNegativityRefutation.renyiHalf
• Truth anchor: D5/S3/Quantum/Dynamics/KickedIsingNegativityRefutation.result
• Truth anchor: D5/S3/Quantum/Dynamics/KickedIsingNegativityRefutation.trace_conjugate_left
• Truth anchor: D5/S3/Quantum/Dynamics/KickedIsingNegativityRefutation.trace_conjugate_right
• Truth anchor: D5/S3/Quantum/Dynamics/KickedIsingNegativityRefutation.trace_local_left
• Truth anchor: D5/S3/Quantum/Dynamics/KickedIsingNegativityRefutation.trace_local_right
• Dependency: D5/S3/Quantum/Entanglement/AbsolutePPT/UniformSchmidtCorner
• Dependency: D5/S3/Quantum/Entanglement/FourQubitResidualSumMonotoneRefutation
• Dependency: D5/S3/Quantum/Entanglement/StructuredNegativityCoincidenceRefutation
• Dependency: D5/S3/Quantum/Foundation/FiniteTraceDistance