BasisState
plain-language theorem explainer
BasisState introduces the normalized amplitude vector over a finite set of size n as the mathematical object representing a basis state in Hilbert space. Quantum theorists studying decoherence and the emergence of classical pointer states would reference this when constructing models of environment-driven state selection. The definition consists of a direct structure with an amplitudes map and a summation constraint enforcing unit norm.
Claim. Let $n$ be a natural number. A basis state is a map $a$ from the finite set of $n$ elements to the complex numbers such that the sum over all elements $i$ of the squared modulus of $a(i)$ equals one.
background
The module develops the QF-003 claim that pointer states arise as neutral windows minimizing J-cost in the Recognition Science landscape. J-cost is the functional satisfying the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y), with the explicit form J(x) = (x + x^{-1})/2 - 1. Upstream foundations supply the integer one from IntegersFromLogic and the active edge count A from IntegrationGap, which supports the phi-power identities at three spatial dimensions.
proof idea
The declaration is a structure definition. It introduces the amplitudes field as a function from Fin n to complex numbers and the normalized field as the equality asserting that the sum of squared norms equals one. No tactics or lemmas are invoked.
why it matters
BasisState serves as the parent structure for PointerState, which extends it with stability and cost minimization properties. This supports the module's target of deriving classical pointer states from neutral windows in the J-cost landscape. It connects to the broader framework landmarks including the forcing chain to three dimensions and the phi-ladder for physical constants, providing the quantum substrate for decoherence timescales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.