Pith. sign in
module module high

IndisputableMonolith.Skeleton.Quantum

show as:
view Lean formalization →

Skeleton aggregator for the Recognition Science quantum layer: Born-rule uniqueness on 8-mode sectors, projector commutation structure, and pure two-qubit concurrence-to-entropy positivity. A physicist citing RS quantum predictions pulls this module as the single import surface. No local proofs; it only re-exports the three closed quantum tracks.

claimPackage of three quantum results: (i) Born rule $P=|\psi|^2$ as the unique normalised, phase-invariant, additive probability on 8-mode sectors consistent with two-branch $\exp(-C)$; (ii) idempotent projector algebra (structural commutation); (iii) Wootters concurrence of a pure two-qubit amplitude matrix implies strict positivity of von Neumann entanglement entropy.

background

Recognition Science forces quantum measurement statistics from the J-cost functional and the eight-tick (DFT-8) sector structure rather than postulating them. The Born-rule track (QF-002) states that $P=|\psi|^2$ is the unique probability measure on 8-mode sectors that is normalised, phase-invariant, additive over disjoint mode-sets, and consistent with the two-branch $\exp(-C)$ rule.

CommutationStructure supplies the elementary projector algebra: projectors are idempotent, giving the minimal non-commutative skeleton needed for measurement. PureTwoQubit.EntropyConcurrence closes Track 2.B: the chain from Wootters concurrence of a pure two-qubit amplitude matrix to strict positivity of the von Neumann entanglement entropy, with no proof holes and no extra RS assumptions.

This Skeleton.Quantum module sits above those three imports and presents them as the canonical quantum surface of the monolith.

proof idea

Definition and re-export module only; no local proofs. All argument lives in the three imports: BornRule (DFT-8 sector forcing of $P=|\psi|^2$), CommutationStructure (idempotent projector algebra), and EntropyConcurrence (concurrence $\Rightarrow$ positive entanglement entropy for pure two-qubit states). The skeleton simply aggregates those closed tracks under one namespace.

why it matters in Recognition Science

Gives a single entry point for the RS quantum layer inside the Skeleton domain. Downstream consumers that need Born-rule uniqueness, measurement projectors, or the Track 2.B entanglement-entropy theorem import this module rather than the three specialised paths. It records that Track 2.B is closed (structural theorem, no new RS assumptions) and that QF-002 derives the Born rule from J-cost plus eight-tick forcing, tying the quantum layer to the T7 octave and the Recognition Composition Law. No further parent theorems are listed yet; the module is a leaf aggregator in the current graph.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.