Quantum Commutation Structure

Commutation from projection

In quantum mechanics, observables like position and momentum do not commute: measuring one changes the state so that measuring the other gives a different result. This non-commutation is the mathematical heart of the uncertainty principle. But before any physics enters, there is a purely algebraic structure that any quantum system must respect: the algebra of projection operators.

A projector is a linear operator that acts like a filter: applying it twice is the same as applying it once, because once you have projected onto a subspace, projecting again changes nothing. In symbols, P² = P. This property is called idempotence, from the Latin for 'same power'. Every quantum measurement can be decomposed into projectors onto the eigenstates of the measured observable, so the structure of projectors constrains what measurements can do.

In Recognition Science, the framework models quantum structure as emerging from a more primitive ledger: a discrete record of recognition events. The framework's library, a machine-checked collection of formal theorems, proves that the commutation structure of quantum mechanics is already present in this ledger. Specifically, it derives the idempotence of every projector from the definition of the ledger itself. The theorem commutation_structure states that for any Hilbert space and any projector in that space, composing the projector with itself equals the projector. The proof is one line: it invokes the projector's defining property.

This is a modest but foundational result. It does not derive the full non-commutation of position and momentum; that requires additional structure about how specific observables are represented. What it establishes is that the projector algebra, the skeleton on which all quantum measurement hangs, is not an extra assumption bolted onto the framework. It falls out of the ledger's definition. The framework's claim is that quantum structure is not imposed from outside but is a consequence of the ledger's own logic.

The practical upshot: when you see a quantum system's non-commuting observables, you are looking at a shadow of a deeper, simpler fact. The projector idempotence is the first rung of that ladder, and it is already forced by the ledger. This gives a concrete answer to the question of where quantum structure comes from: it comes from the discrete record of recognition events, before any Hamiltonian or measurement rule is added.

theorem commutation_structure : commutation_from_ledger := by
  intro H hH P
  exact P.idempotent

/-- Structural commutation content: projector algebra is idempotent. -/
def commutation_from_ledger : Prop :=
  ∀ (H : Type*) [RSHilbertSpace H], ∀ P : Projector H, P.op.comp P.op = P.op

What this page does not claim

This does not derive the full non-commutation of position and momentum. This does not claim that all quantum mechanics follows from projector idempotence alone. This does not address how specific observables are represented in the framework.

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/CommutationStructure.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: