IndisputableMonolith.Quantum.PureTwoQubit.EntropyConcurrence
Defines Wootters concurrence for a pure two-qubit amplitude matrix as twice the absolute determinant, and ties it to the reduced density matrix via det(ρ) = C²/4. Quantum skeleton and gravity master imports use the nonnegativity and vanishing criteria. Argument is elementary complex linear algebra over Mathlib: Frobenius norms, partial traces, and determinant identities.
claimFor a pure two-qubit amplitude matrix $A$, the Wootters concurrence is $C(A)=2\|\det A\|$. The one-qubit reduced density $\rho$ obtained by partial trace satisfies $\operatorname{tr}\rho=\|A\|_F^2$ (hence $\operatorname{tr}\rho=1$ when $A$ is normalized) and $\det\rho=C(A)^2/4$. Thus $C(A)=0$ iff $\det A=0$, and $C(A)>0$ iff $\det\rho\neq 0$.
background
Pure two-qubit states may be written as $2\times 2$ complex amplitude matrices $A$. For pure bipartite qubit states the general Wootters concurrence collapses to $C(A)=2|\det A|$: entanglement is measured by how far $A$ is from rank one.
The reduced density on one factor is the partial trace $\rho=A A^\dagger$ (up to the usual reshaping). Its purity and mixedness are controlled by $\det\rho$. The module also tracks the squared Frobenius norm $|A|_F^2$, which equals $\operatorname{tr}\rho$ and normalizes pure states.
Setting is standard finite-dimensional QM, imported only from Mathlib. Downstream skeleton text states the intended physics link: entanglement entropy is positive exactly when concurrence is.
proof idea
Definition module plus short algebraic lemmas, not a deep forcing argument. Concurrence is introduced as $2|\det A|$; nonnegativity is immediate from the absolute value. Vanishing and positivity are rewritten as $\det A=0$ or not.
Reduced density is defined from $A$; trace identities equate $\operatorname{tr}\rho$ to the Frobenius norm squared and to $1$ under normalization. Determinant lemmas relate $\det\rho$ to $|\det A|^2$ and thence to $C(A)^2/4$. The last lemmas push positivity of $C$ to nonvanishing of $\det\rho$. All steps are direct matrix algebra.
why it matters in Recognition Science
Feeds the quantum facade and the skeleton chapter that claims Born-rule forcing from J-cost and that entanglement entropy is positive exactly when concurrence is. That skeleton still flags the canonical commutator and the eight-tick Weyl relation as open; this module only supplies the pure two-qubit entanglement side.
Also imported by Gravity.MasterTheorem (Track 7.A structural master statement). Concurrence and reduced-state determinant give a clean algebraic witness for bipartite entanglement inside larger RS quantum and gravity assemblies, without touching T5–T8 forcing or the RCL directly.
scope and limits
- Does not treat mixed two-qubit states or the full Wootters spin-flip formula.
- Does not define or bound entanglement entropy; only concurrence and det(ρ).
- Does not prove Born rule, commutators, or eight-tick Weyl relations.
- Does not address multipartite entanglement or qudits beyond 2×2.
- Does not depend on RS constants (φ, ħ, α) or the forcing chain T0–T8.
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