IndisputableMonolith.Quantum.PureTwoQubit.EntropyConcurrence
Defines Wootters concurrence for a pure two-qubit amplitude matrix as twice the absolute determinant, plus the one-qubit reduced density and the elementary links among concurrence, det, and Frobenius norm. Quantum and gravity tracks cite these when they need entanglement positivity for pure bipartite states. Content is definition-and-lemma style over Mathlib matrix algebra.
claimFor a pure two-qubit amplitude matrix $A$, the Wootters concurrence is $C(A)=2\|\det A\|$. The reduced one-qubit density has $\det(\rho_A)=C(A)^2/4$, and $C(A)=0$ if and only if $\det A=0$.
background
Pure two-qubit states may be written as $2\times 2$ complex amplitude matrices $A$ (unnormalized until a trace or Frobenius condition is imposed). For pure bipartite states the general Wootters concurrence collapses to twice the absolute value of the determinant of that matrix: $C(A)=2|\det A|$.
The module also builds the reduced density on one factor by partial trace (equivalently, via the Gram/Frobenius data of $A$). Standard matrix identities then relate $\operatorname{Tr}(\rho_A)$, $\det(\rho_A)$, $|A|_F^2$, and $\det A$. Nonnegativity of concurrence is immediate from the absolute value; vanishing concurrence is equivalent to $\det A=0$ and hence to a product (separable) pure state.
The only import is Mathlib. No Recognition-native cost $J$ or $\phi$-ladder appears at this layer; the objects are ordinary finite-dimensional quantum algebra packaged for later RS use.
proof idea
Definition module with short algebraic lemmas, not a single deep theorem. concurrence is introduced as $2|\det A|$. Nonnegativity is immediate. Equivalences concurrence = 0 \Leftrightarrow \det A = 0 and the positive variants are determinant rewriting.
frobeniusNormSq and reducedDensity set up the partial-trace side. Trace identities equate $\operatorname{Tr}(\rho)$ to the Frobenius squared norm of $A$, and normalization of $A$ forces $\operatorname{Tr}(\rho)=1$. Determinant identities push $\det(\rho)$ through to $|\det A|^2$ and finally to $C(A)^2/4$, so positivity of concurrence is equivalent to nonvanishing reduced determinant. All steps are routine $2\times 2$ matrix algebra.
why it matters in Recognition Science
Skeleton.Quantum states that entanglement entropy is positive exactly when concurrence is; this module supplies the pure two-qubit concurrence side of that bridge and the det/reduced-density calculus behind it. The Quantum facade re-exports the layer as part of the recognition-derived quantum stack (Born rule, eight-tick Weyl, entanglement).
Gravity.MasterTheorem imports the module on the structural path of Track 7.A, so bipartite entanglement identities are available wherever the master gravity statement needs quantum-side positivity or separability control. Within RS, concurrence is the concrete pure-state entanglement monotone that matches the entropy story without postulating an extra axiom at the two-qubit level.
The module does not itself close the open D3 keystone (canonical commutator / eight-tick Weyl sorry); it only equips the entanglement half of the quantum skeleton.
scope and limits
- Does not treat mixed two-qubit states or the full Wootters spin-flip formula.
- Does not define entanglement entropy; only concurrence and reduced-density identities.
- Does not prove Born rule, eight-tick Weyl, or $[x,p]=i\hbar$.
- Does not introduce $J$-cost, $\phi$-ladder, or RS unit conventions.
- Does not handle $n>2$ qubits or continuous-variable entanglement.
used by (3)
declarations in this module (52)
-
def
concurrence -
theorem
concurrence_nonneg -
theorem
concurrence_eq_zero_iff_det_zero -
theorem
concurrence_pos_iff_det_ne_zero -
def
frobeniusNormSq -
def
reducedDensity -
theorem
reducedDensity_trace_eq_frobenius -
theorem
reducedDensity_trace_eq_one_of_normalized -
theorem
reducedDensity_det_eq_normSq_det -
theorem
reducedDensity_det_eq_norm_det_sq -
theorem
reducedDensity_det_eq_concurrence_sq_div_four -
theorem
reducedDensity_det_ne_zero_of_concurrence_pos -
theorem
reducedDensity_discriminant_eq_one_sub_concurrence_sq -
def
lambdaPlus -
def
lambdaMinus -
theorem
lambdaPlus_add_lambdaMinus -
theorem
lambdaPlus_mul_lambdaMinus -
theorem
lambdaPair_sum_product_of_concurrence_unit_interval -
def
binaryEntropy -
theorem
binaryEntropy_zero_left -
theorem
binaryEntropy_zero_right -
theorem
binaryEntropy_symm -
theorem
binaryEntropy_pos_of_open_unit_interval -
theorem
inner_radius_lt_one_of_pos_concurrence -
theorem
inner_radius_in_unit_interval_of_pos_concurrence -
theorem
binaryEntropy_inner_radius_pos_of_concurrence -
theorem
reducedDensity_eq_mul_conjTranspose -
theorem
reducedDensity_isHermitian -
theorem
reducedDensity_trace_eq_frobenius_complex -
theorem
reducedDensity_trace_eq_one_of_normalized_complex -
theorem
lambdaPlus_sub_lambdaMinus -
theorem
lambdaPlus_ge_lambdaMinus -
theorem
sum_product_implies_quadratic -
theorem
eq_lambdaPlus_or_lambdaMinus_of_quadratic -
theorem
eigenvalues_fin_two_sum_eq_of_complex_sum -
theorem
eigenvalues_fin_two_prod_eq_of_complex_prod -
theorem
reducedDensity_eigenvalues_sum_eq_one -
theorem
reducedDensity_eigenvalues_prod_eq_concurrence_sq_div_four -
theorem
concurrence_sq_le_one_of_normalized -
theorem
concurrence_le_one_of_normalized -
theorem
reducedDensity_eigenvalues_eq_lambda_or_swap -
def
reducedDensityVonNeumannEntropy -
theorem
binaryEntropy_eq_neg_sum_lambda -
def
PureTwoQubitReducedEntropyTarget -
theorem
pureTwoQubitReducedEntropyTarget_holds -
theorem
pure_two_qubit_entropy_eq_binaryEntropy_inner_radius -
abbrev
PureTwoQubitReducedEntropyTargetDef -
theorem
pure_two_qubit_entropy_positive_of_concurrence_positive -
theorem
pure_two_qubit_entropy_positive_unconditional -
structure
PureTwoQubitConcurrenceEntropyCert -
def
pureTwoQubitConcurrenceEntropyCert -
theorem
pureTwoQubitConcurrenceEntropyCert_inhabited