CoupledCoreIndex

formal source

 114  exact ququartWeyl_relation_apply ψ
 115
 116/-- The finite-site configuration space of coupled ququart cores. -/
 117abbrev CoupledCoreIndex (N : ℕ) := Fin N → Fin 4
 118
 119/-- The concrete Hilbert carrier of `N` coupled recognition cores. -/
 120abbrev CoupledCoreSpace (N : ℕ) := CoupledCoreIndex N → ℂ
 121
 122/-- The dimension of the coupled-core index space is exactly `4^N`. -/
 123theorem coupledCoreIndex_card (N : ℕ) :
 124    Fintype.card (CoupledCoreIndex N) = 4 ^ N := by
 125  simp [CoupledCoreIndex]
 126
 127/-- The phase character appearing in the tensor-Weyl monomial. -/
 128def phaseCharacter {N : ℕ} (b s : CoupledCoreIndex N) : ℂ :=
 129  Finset.univ.prod fun x : Fin N => Complex.I ^ ((b x).val * (s x).val)
 130
 131/-- Shift a coupled-core configuration by a finite ququart displacement. -/
 132def shiftedConfig {N : ℕ} (a s : CoupledCoreIndex N) : CoupledCoreIndex N :=
 133  fun x => sub4 (s x) (a x)
 134
 135/-- Add a coupled-core displacement to a configuration. -/
 136def addedConfig {N : ℕ} (a s : CoupledCoreIndex N) : CoupledCoreIndex N :=
 137  fun x => add4 (a x) (s x)
 138
 139/-- Zero phase character. -/
 140lemma phaseCharacter_zero {N : ℕ} (s : CoupledCoreIndex N) :
 141    phaseCharacter 0 s = 1 := by
 142  simp [phaseCharacter]
 143
 144/-- Zero displacement leaves a coupled-core configuration unchanged. -/
 145lemma shiftedConfig_zero {N : ℕ} (s : CoupledCoreIndex N) :
 146    shiftedConfig 0 s = s := by
 147  funext x