module module high

`IndisputableMonolith.Foundation.CoupledRecognitionCores`

This module defines the ququart carrier to model local quarter-turn cores within the Recognition Science foundation. Researchers building operator cores or coupled recognition structures would cite it for the discrete state definitions. It supplies a set of type and function definitions for states, basis vectors, and modular operations on four elements, with no embedded proofs.

claimThe local quarter-turn core is modeled by a ququart carrier equipped with basis kets and modular addition and subtraction operations on a four-state space.

background

The module introduces QuquartState as the carrier type for a four-level discrete system. It defines basisKet for the standard basis elements, prev4 for the predecessor map, and add4 together with sub4 for addition and subtraction, plus core cancellation identities such as sub4_add4_cancel_core. These sit inside the Recognition Science foundation that derives physics from the J-cost functional equation and the phi-ladder.

The module imports only Mathlib and supplies the local modeling step for quarter-turn cores before they are lifted into operator-level constructions. No upstream Recognition lemmas are referenced inside the module itself.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module feeds the parent construction IndisputableMonolith.Foundation.OperatorCore.CoupledRecognitionCores by supplying the ququart carrier. It directly realizes the modeling statement that the local quarter-turn core is represented as a ququart carrier, closing one link in the foundation-to-operator chain.

scope and limits

Does not prove any theorems or contain sorry placeholders.
Does not import other Recognition Science modules.
Does not reference J-uniqueness, the phi-ladder, or the RCL.
Does not define mass formulas or coupling constants.

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