The two-qubit kicked-Ising pilot model (quantum-chaos workstream, H3)

Category: Special (incubator — CSD-free; upstream-candidate(physlib)).

The concrete Floquet model of the §H3 pilot: one period of the kicked Ising chain on two qubits,

U(J, b) = exp(-iJ σᶻ⊗σᶻ) · (exp(-ib σˣ) ⊗ exp(-ib σˣ)),

built from EXPLICIT matrices (no matrix exponential needed: the Ising phase is diagonal, the kick is the standard x-rotation), indexed by Fin 2 × Fin 2 — the composite index the corpus's partial-trace machinery consumes directly.

• kickMat b — the one-qubit kick [[cos b, -i sin b], [-i sin b, cos b]], unitary (kickMat_mem_unitaryGroup, the sin² + cos² computation).
• phaseMat J — the Ising phase diag(e^{-iJ}, e^{iJ}, e^{iJ}, e^{-iJ}), unitary (unit-modulus diagonal).
• kronecker_mem_unitaryGroup — the Kronecker product of unitaries is unitary (generic; upstream-candidate(mathlib)).
• kickedIsingU J b — the Floquet unitary, assembled in the unitary GROUP (membership by group multiplication); kickedIsingFloquet J b — the model as a FloquetEvolution through the generic ofUnitaryMatrix seam.
• ★ kickedIsing_changes_marginal — the accessibility-change witness of the pilot statement: at kick angle b = π/2 the step sends |00⟩ to a phase times |11⟩, so the reduced (first-qubit) state flips |0⟩⟨0| ↦ |1⟩⟨1| — the restricted marginal genuinely changes — while the interface's inner_iterate_iterate says all global overlaps are exactly preserved. Together: global information intact, local accessibility moved.

The one-qubit kick

noncomputable def QuantumChaos.kickMat (b : ℝ) : Matrix (Fin 2) (Fin 2) ℂ

The kick matrix exp(-ib σˣ) = [[cos b, -i sin b], [-i sin b, cos b]].

Equations

• QuantumChaos.kickMat b = !![↑(Real.cos b), -(Complex.I * ↑(Real.sin b)); -(Complex.I * ↑(Real.sin b)), ↑(Real.cos b)]

theorem QuantumChaos.kickMat_mem_unitaryGroup (b : ℝ) : kickMat b ∈ Matrix.unitaryGroup (Fin 2) ℂ

The kick is unitary: sin² + cos² = 1.

The Ising phase

noncomputable def QuantumChaos.phaseEntry (J : ℝ) (p : Fin 2 × Fin 2) : ℂ

The Ising-phase diagonal entry: e^{-iJ} on aligned spins, e^{iJ} on anti-aligned.

Equations

• QuantumChaos.phaseEntry J p = Complex.exp (Complex.I * ↑J * if p.1 = p.2 then -1 else 1)

theorem QuantumChaos.phaseEntry_star_mul_self (J : ℝ) (p : Fin 2 × Fin 2) : star (phaseEntry J p) * phaseEntry J p = 1

Each phase entry has unit modulus times its conjugate: conj z * z = 1.

noncomputable def QuantumChaos.phaseMat (J : ℝ) : Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ

The Ising phase exp(-iJ σᶻ⊗σᶻ) as a diagonal matrix.

Equations

• QuantumChaos.phaseMat J = Matrix.diagonal (QuantumChaos.phaseEntry J)

theorem QuantumChaos.phaseMat_mem_unitaryGroup (J : ℝ) : phaseMat J ∈ Matrix.unitaryGroup (Fin 2 × Fin 2) ℂ

A unit-modulus diagonal is unitary.

Kronecker products of unitaries

theorem QuantumChaos.kronecker_mem_unitaryGroup {m : Type u_1} {n : Type u_2} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] {A : Matrix m m ℂ} {B : Matrix n n ℂ} (hA : A ∈ Matrix.unitaryGroup m ℂ) (hB : B ∈ Matrix.unitaryGroup n ℂ) : Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A B ∈ Matrix.unitaryGroup (m × n) ℂ

The Kronecker product of unitaries is unitary (upstream-candidate(mathlib)).

The assembled Floquet operator

noncomputable def QuantumChaos.kickedIsingU (J b : ℝ) : ↥(Matrix.unitaryGroup (Fin 2 × Fin 2) ℂ)

The kicked-Ising Floquet unitary, as a unitary-group element (membership by group multiplication).

Equations

• QuantumChaos.kickedIsingU J b = ⟨QuantumChaos.phaseMat J, ⋯⟩ * ⟨Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (QuantumChaos.kickMat b) (QuantumChaos.kickMat b), ⋯⟩

theorem QuantumChaos.kickedIsingU_val (J b : ℝ) : ↑(kickedIsingU J b) = phaseMat J * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (kickMat b) (kickMat b)

noncomputable def QuantumChaos.kickedIsingFloquet (J b : ℝ) : FloquetEvolution (EuclideanSpace ℂ (Fin 2 × Fin 2))

The pilot model: one kicked-Ising period as a FloquetEvolution, through the generic matrix-dynamics seam.

Equations

• QuantumChaos.kickedIsingFloquet J b = QuantumChaos.FloquetEvolution.ofUnitaryMatrix (QuantumChaos.kickedIsingU J b)

The accessibility-change witness at b = π/2

noncomputable def QuantumChaos.pilotOuter {n : Type u_1} [Fintype n] (v : EuclideanSpace ℂ n) : Matrix n n ℂ

The outer product |v⟩⟨v| on an arbitrary finite index (local pilot helper: the corpus outerProducts live in the CSD-side LF2 layer, which a CSD-free incubator module may not import).

Equations

• QuantumChaos.pilotOuter v = Matrix.vecMulVec v.ofLp (star v.ofLp)

theorem QuantumChaos.pilotOuter_apply {n : Type u_1} [Fintype n] (v : EuclideanSpace ℂ n) (p q : n) : pilotOuter v p q = v.ofLp p * (starRingEnd ℂ) (v.ofLp q)

theorem QuantumChaos.pilotOuter_smul_of_norm_one {n : Type u_1} [Fintype n] {c : ℂ} (hc : ‖c‖ = 1) (v : EuclideanSpace ℂ n) : pilotOuter (c • v) = pilotOuter v

Outer products are phase-invariant: ‖c‖ = 1 gives |cv⟩⟨cv| = |v⟩⟨v|.

theorem QuantumChaos.kickedIsing_step_e00 (J : ℝ) : (kickedIsingFloquet J (Real.pi / 2)).step (EuclideanSpace.single (0, 0) 1) = -phaseEntry J (1, 1) • EuclideanSpace.single (1, 1) 1

At b = π/2 the kicked-Ising step sends |00⟩ to a phase times |11⟩: the kick flips both spins (up to -i each), the Ising phase multiplies by e^{-iJ}.

theorem QuantumChaos.kickedIsing_phase_norm (J : ℝ) : ‖-phaseEntry J (1, 1)‖ = 1

The phase in kickedIsing_step_e00 has unit modulus.

theorem QuantumChaos.kickedIsing_changes_marginal (J : ℝ) : QuantumInfo.partialTraceRight (pilotOuter ((kickedIsingFloquet J (Real.pi / 2)).step (EuclideanSpace.single (0, 0) 1))) ≠ QuantumInfo.partialTraceRight (pilotOuter (EuclideanSpace.single (0, 0) 1))

★ The accessibility-change witness. At b = π/2 the reduced (first-qubit) state of the evolved |00⟩ differs from that of |00⟩ — the two partial traces compute by hand to |1⟩⟨1| and |0⟩⟨0|; the formal statement is the disequality itself. Restricted accessibility genuinely changes, while inner_iterate_iterate keeps every global overlap exactly invariant — the pilot's "global information intact, local accessibility moved" clause.

The Fin 4 reindex: reaching the Fin N machinery

theorem QuantumChaos.reindex_mem_unitaryGroup {m : Type u_1} {n : Type u_2} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] (e : m ≃ n) {M : Matrix m m ℂ} (hM : M ∈ Matrix.unitaryGroup m ℂ) : (Matrix.reindex e e) M ∈ Matrix.unitaryGroup n ℂ

Reindexing along an index equivalence preserves unitarity (upstream-candidate(mathlib)).

noncomputable def QuantumChaos.kickedIsingU₄ (J b : ℝ) : ↥(Matrix.unitaryGroup (Fin 4) ℂ)

The kicked-Ising Floquet unitary reindexed to Fin 4 along finProdFinEquiv, so the concrete model reaches the Fin N ontic machinery (KSigma 4, floquetOnticStep, the pilot closure) directly.

Equations

• QuantumChaos.kickedIsingU₄ J b = ⟨(Matrix.reindex finProdFinEquiv finProdFinEquiv) ↑(QuantumChaos.kickedIsingU J b), ⋯⟩