basisKet
basisKet defines the standard basis ket |m⟩ for m in Fin 4 as the vector that equals 1 at index m and 0 elsewhere in the ququart state space. Researchers constructing local Weyl monomials or proving orthonormality of the ququart basis cite this as the computational foundation. It appears in nine downstream results including operator inner products and phase orthogonality checks. The declaration is a direct one-line abbreviation of the explicit indicator-function definition from the CoupledRecognitionCores module.
claimThe standard basis ket $|m⟩$ for $m :$ Fin $4$ is the function QuquartState given by $|m⟩(n) = 1$ if $n = m$ and $0$ otherwise.
background
In the CoupledRecognitionCores module the ququart state space is the type of functions Fin 4 → ℂ. The basis ket supplies the standard computational basis vectors for this 4-dimensional space. The upstream definition reads: def basisKet (m : Fin 4) : QuquartState := fun n => if n = m then 1 else 0, with the accompanying note that it realizes the shift convention X|m⟩ = |m+1 mod 4⟩.
proof idea
This is a one-line abbreviation that directly aliases the basisKet definition from IndisputableMonolith.Foundation.CoupledRecognitionCores.
why it matters in Recognition Science
The definition feeds nine downstream declarations, among them basisKet_orthonormal (proved by fin_cases and simp), localOperatorInner (Hilbert-Schmidt pairing on single-core operators), and localWeylMonomial_basisKet (action of Weyl monomials on basis kets). It supplies the computational basis required for the ququart representation of coupled recognition cores and for the local operator algebra developed in the module.
scope and limits
- Does not prove orthonormality of the basis.
- Does not define the Weyl monomials or local operators.
- Does not address tensor products of multiple cores.
- Does not link to the phi-ladder or Recognition Science constants.
Lean usage
theorem basis_example (m : Fin 4) : (basisKet m) m = 1 := by simp [basisKet]formal statement (Lean)
10abbrev basisKet := IndisputableMonolith.Foundation.CoupledRecognitionCores.basisKet