module module moderate

`IndisputableMonolith.Foundation.CoupledRecognitionCores`

CoupledRecognitionCores models the local quarter-turn core as a ququart carrier. It supplies the type QuquartState together with basis kets, modular arithmetic on four levels, and the operators ququartX and ququartZ. Researchers building operator algebras on top of recognition cores cite these carriers. The module consists solely of definitions.

claimThe local quarter-turn core is realized by a ququart carrier whose states live in a four-dimensional space equipped with basis vectors, predecessor and successor maps, addition and subtraction modulo four, and the operators $X_4$, $Z_4$.

background

The module belongs to the Foundation layer and imports only Mathlib. Its single doc-comment states that the local quarter-turn core is modeled as a ququart carrier. Sibling definitions introduce QuquartState as the carrier type, basisKet for the standard basis, prev4/add4/sub4 for cyclic arithmetic on four elements, and ququartX/ququartZ as the corresponding Pauli-like operators on that space.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The carrier definitions are imported by IndisputableMonolith.Foundation.OperatorCore.CoupledRecognitionCores, which constructs the operator-level structures for coupled recognition cores. The module therefore supplies the concrete four-level object required to realize the quarter-turn model inside the Recognition Science foundation.

scope and limits

Does not contain theorems or proofs.
Does not define the full coupled recognition core.
Does not link to the forcing chain T0-T8 or the Recognition Composition Law.
Does not derive physical constants or mass formulas.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Foundation.OperatorCore.CoupledRecognitionCores module_import

declarations in this module (61)

abbrev QuquartState L12
def basisKet L15
def prev4 L20
def add4 L24
def sub4 L28
theorem sub4_add4_cancel_core L32
theorem add4_sub4_cancel_core L37
theorem add4_eq_add4_iff_left_core L42
def ququartX L47
def ququartZ L59
theorem ququartX_basisKet L73
theorem ququartZ_basisKet L79
lemma ququartWeyl_relation_apply L87
theorem ququartWeyl_relation L110
abbrev CoupledCoreIndex L117
abbrev CoupledCoreSpace L120
theorem coupledCoreIndex_card L123
def phaseCharacter L128
def shiftedConfig L132
def addedConfig L136
lemma phaseCharacter_zero L140
lemma shiftedConfig_zero L145
theorem shiftedConfig_addedConfig L152
theorem addedConfig_shiftedConfig L158
theorem addedConfig_eq_addedConfig_iff_left L164
def tensorWeylMonomial L176
theorem tensorWeylMonomial_zero_zero L191
def coupledBasisKet L197
theorem coupledBasisKet_orthonormal L201
theorem tensorWeylMonomial_basisKet L229
def localWeylMonomial L246
def localOperatorInner L261
theorem basisKet_orthonormal L265
theorem sub4_add4_cancel L270
theorem add4_sub4_cancel L275
theorem localWeylMonomial_basisKet L280
theorem add4_eq_add4_iff_left L296
lemma I_pow_star_mul_self L301
lemma neg_I_pow L312
lemma I_pow_five L316
lemma scaled_basisKet_inner L320
theorem localWeylMonomial_self_inner L336
theorem localWeylMonomial_shift_orthogonal L365
theorem localWeylMonomial_phase_orthogonal L383
theorem localWeylMonomial_orthogonal_of_ne L408
theorem localWeylFamily_card L420
lemma scaled_coupledBasisKet_inner L424
theorem tensorWeylMonomial_basis_image_orthogonal L444
def coupledOperatorInner L462
lemma phaseCharacter_star_mul_self L468
theorem tensorWeylMonomial_self_inner L482
theorem tensorWeylMonomial_shift_orthogonal L515
def coupledCoreEquivFin L524
def embedState L529
def projectState L547
theorem projectState_embedState L560
theorem embedState_injective L568
def liftOperator L576
theorem liftOperator_intertwines L583
theorem self_le_four_pow_self L590
theorem finite_dimensional_exact_embedding L610