module module high

`IndisputableMonolith.Foundation.CoupledRecognitionCores`

This module models the local quarter-turn core as a ququart carrier, a four-state system for Recognition Science foundations. It supplies the state type, basis vectors, and cyclic operations add4 and sub4 that implement quarter-turn navigation. The module is cited by the coupled operator core extension when building recognition dynamics. It contains only definitions with no theorems or proofs.

claimA ququart carrier is a four-dimensional state space with basis kets and operations add$_4$, sub$_4$ realizing cyclic quarter-turn symmetry on the carrier.

background

Recognition Science models local recognition steps via quarter-turn cores. The module introduces the ququart carrier as the concrete type for these cores, together with a standard basis and the cyclic group operations prev4, add4, sub4 that shift states by one quarter turn. These definitions rest on the eight-tick octave structure from the forcing chain and prepare the carrier for coupling in later operator modules.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the ququart carrier that feeds directly into IndisputableMonolith.Foundation.OperatorCore.CoupledRecognitionCores, allowing the extension to coupled recognition systems. It fills the foundational carrier step required before any operator algebra or dynamics can be stated.

scope and limits

Does not define dynamics or time evolution on the carrier.
Does not derive constants such as alpha or G from the ququart structure.
Does not prove completeness or uniqueness of the chosen basis.
Does not address coupling between multiple carriers.

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