pureTwoQubitConcurrenceEntropyCert_inhabited
plain-language theorem explainer
The pure two-qubit concurrence-entropy certificate is inhabited: a single package of algebraic facts relating Wootters concurrence of a 2×2 amplitude matrix to reduced-density trace and determinant identities exists. Anyone citing Track 2.B closure (concurrence to entanglement-entropy positivity) would point here. The proof is a one-line inhabitant from the concrete certificate assembly.
Claim. The type of pure two-qubit concurrence-entropy certificates is nonempty: there exists a record packing (i) $C(A)\ge 0$ for every $2\times 2$ complex amplitude matrix $A$, (ii) $C(A)=0$ iff $\det A=0$, (iii) the reduced-density trace equals the Frobenius norm of $A$, and (iv) the reduced-density determinant equals $C(A)^2/4$, with $C(A):=2|\det A|$.
background
Track 2.B in this module links Wootters concurrence of a pure two-qubit amplitude matrix to strict positivity of von Neumann entanglement entropy. For a normalized pure state with amplitude matrix $A:\mathrm{Fin},2\times\mathrm{Fin},2\to\mathbb{C}$, concurrence is the pure-state simplification $C(A):=2|\det A|$. The reduced density $\rho_1=\mathrm{tr}2|\psi\rangle\langle\psi|$ has eigenvalues $(1\pm\sqrt{1-C^2})/2$, so $E{\mathrm{VN}}(\rho_1)$ equals the binary entropy of that argument.
The certificate structure packages the algebraic core: nonnegativity of $C$, the iff with vanishing determinant, reduced-density trace equal to the Frobenius norm, and reduced-density determinant equal to $C^2/4$. Upstream, a concrete definition fills those fields by the already-proved lemmas on concurrence and reduced density. This theorem only asserts that the package type is inhabited.
proof idea
One-line term proof. The concrete definition already assembles the certificate by wiring concurrence_nonneg, the det-zero equivalence, the reduced-density/Frobenius trace identity, and the reduced-density det $=C^2/4$ identity into the structure fields. The proof is the standard inhabitant constructor: wrap that definition as a witness of Nonempty.
why it matters
Track 2.B is marked structurally closed in the module: no proof holes and no new Recognition Science assumptions. This inhabitedness statement is the formal seal that the algebraic core certificate exists as a single object, so downstream entropy-positivity arguments can cite one package rather than four separate lemmas.
The module composes that core with the reduced-entropy target to obtain $E_{\mathrm{VN}}(\rho_1)=h((1+\sqrt{1-C^2})/2)$ and strict positivity for $C>0$. No further used-by edges are recorded yet; the declaration is a terminal packaging step inside the pure two-qubit entropy-concurrence development. It does not touch the forcing chain (T0-T8), RCL, or the mass ladder; it is quantum-information infrastructure supporting the RS quantum track.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.