pith. sign in
module module low

IndisputableMonolith.Foundation.OperatorCore.CoupledRecognitionCores

show as:
view Lean formalization →

The module supplies ququart-based definitions for coupled recognition cores, exposing 4-level states, Weyl monomials, and index spaces in the operator core layer. It imports the base CoupledRecognitionCores module and lists concrete constructions such as basis vectors, X/Z operators, and tensor monomials. The module contains only definitions with no theorems or proofs.

claimThe module defines the ququart state space $\mathbb{C}^4$, the coupled core index set, the tensor product space for two ququarts, and the Weyl monomial operators satisfying the commutation relation on that space.

background

The module sits in the Foundation domain and imports IndisputableMonolith.Foundation.CoupledRecognitionCores. It introduces QuquartState as the 4-dimensional complex vector space, basisKet for its standard basis vectors, add4 for the 4-level addition operation, ququartX and ququartZ as the generalized Pauli operators, CoupledCoreIndex as the indexing set, CoupledCoreSpace as the tensor product space, tensorWeylMonomial and localWeylMonomial as the monomial operators, and the relation ququartWeyl_relation together with its cardinality and zero cases.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the coupled-core operator primitives that later stages of the forcing chain (T5–T8) and the Recognition Composition Law rely on for constructing multi-particle structures. It feeds the definitions required for the eight-tick octave and spatial dimension emergence, although no downstream used_by edges are recorded yet.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (14)