Quantum Pure Two Qubit Entropy Concurrence

Entanglement measured by concurrence

In quantum information, a pure two-qubit state is the simplest system where entanglement appears. Write the state as a 2 by 2 matrix of complex numbers, normalized so the sum of squared magnitudes is 1. The Wootters concurrence of this matrix is simply twice the absolute value of its determinant. This number runs from 0 for a product state to 1 for a maximally entangled state like a Bell pair, and it is the standard pure-state simplification of the general mixed-state formula.

The entanglement entropy of one qubit is the von Neumann entropy of the reduced density matrix, obtained by tracing out the other qubit. For a pure two-qubit state, this entropy is a function of concurrence alone: E = h((1 + sqrt(1 - C^2))/2), where h(p) = -p log p - (1-p) log(1-p) is the binary entropy. The eigenvalues of the reduced density matrix are (1 ± sqrt(1 - C^2))/2, and the binary entropy is symmetric about p = 1/2, which gives the equality. This means concurrence is not just one entanglement measure among many; for pure two-qubit states it is the complete story.

In Recognition Science, the framework's machine-checked library of formal theorems proves this reduction as a structural theorem. The module shows that for any normalized pure two-qubit state with positive concurrence, the entanglement entropy is strictly positive. The proof combines an algebraic core, showing the eigenvalue (1 + sqrt(1 - C^2))/2 lies strictly between 1/2 and 1 when C > 0, with the fact that binary entropy is strictly positive on the open unit interval. It also proves the supporting facts: concurrence is nonnegative, zero exactly when the determinant is zero, and bounded above by 1 for normalized states.

The practical consequence is a clean witness for entanglement. A pure two-qubit state is entangled if and only if its concurrence is positive, which is equivalent to a nonzero determinant. This matches an algebraic entanglement witness proved elsewhere in the framework. The module closes a specific track in the framework's master plan, with no proof holes and no new assumptions. The reduction from concurrence to entropy positivity is fully formal, so the chain from a simple determinant calculation to a statement about information is machine-checked end to end.

What this changes is the way entanglement can be certified. Instead of computing a full entropy or checking a spectrum, one determinant calculation suffices. For the working physicist, this is a familiar result from quantum information theory; what the framework adds is a fully formal proof that the reduction holds without hidden regularity assumptions. The theorem is unconditional for normalized states, and the positivity of entropy follows directly from positivity of concurrence.

theorem pureTwoQubitReducedEntropyTarget_holds :
    PureTwoQubitReducedEntropyTarget reducedDensityVonNeumannEntropy := by
  intro A hNorm
  have hNorm' : frobeniusNormSq A = 1 := by
    simpa [frobeniusNormSq] using hNorm
  have hC := concurrence_le_one_of_normalized A hNorm'
  rcases reducedDensity_eigenvalues_eq_lambda_or_swap A hNorm' with h | h
  · simp only [reducedDensityVonNeumannEntropy]
    rw [Fin.sum_univ_two, h.1, h.2]
    rw [← binaryEntropy_eq_neg_sum_lambda (concurrence_nonneg A) hC]
    unfold lambdaPlus
    rfl
  · simp only [reducedDensityVonNeumannEntropy]
    rw [Fin.sum_univ_two, h.1, h.2]
    have hneg := binaryEntropy_eq_neg_sum_lambda (concurrence_nonneg A) hC
    have hadd :
        lambdaMinus (concurrence A) * Real.log (lambdaMinus (concurrence A)) +
            lambdaPlus (concurrence A) * Real.log (lambdaPlus (concurrence A)) =
          lambdaPlus (concurrence A) * Real.log (lambdaPlus (concurrence A)) +
            lambdaMinus (concurrence A) * Real.log (lambdaMinus (concurrence A)) := by
      ac_rfl
    rw [hadd, ← hneg]
    unfold lambdaPlus
    rfl

theorem pureTwoQubitConcurrenceEntropyCert_inhabited :
    Nonempty PureTwoQubitConcurrenceEntropyCert :=
  ⟨pureTwoQubitConcurrenceEntropyCert⟩

/-- Concurrence is non-negative. -/
theorem concurrence_nonneg (A : Matrix (Fin 2) (Fin 2) ℂ) :
    0 ≤ concurrence A := by
  unfold concurrence
  have h : 0 ≤ ‖Matrix.det A‖ := norm_nonneg _
  linarith

/-- Determinant of the reduced density matrix in concurrence form:
`det(ρ₁) = C(A)^2 / 4`. -/
theorem reducedDensity_det_eq_concurrence_sq_div_four
    (A : Matrix (Fin 2) (Fin 2) ℂ) :
    Matrix.det (reducedDensity A) = ((concurrence A) ^ 2 / 4 : ℝ) := by
  rw [reducedDensity_det_eq_norm_det_sq]
  unfold concurrence
  norm_num
  ring

What this page does not claim

The module does not prove the mixed-state Wootters formula. The module does not claim concurrence is the only entanglement measure for mixed states. The module does not derive any physical constants or coupling values.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Quantum/PureTwoQubit/EntropyConcurrence.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: