phaseCharacter

formal source

 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
 148  apply Fin.ext
 149  simp [shiftedConfig, sub4]
 150
 151/-- Shifting after adding the same displacement returns the original configuration. -/
 152theorem shiftedConfig_addedConfig {N : ℕ} (a s : CoupledCoreIndex N) :
 153    shiftedConfig a (addedConfig a s) = s := by
 154  funext x
 155  exact sub4_add4_cancel_core (a x) (s x)
 156
 157/-- Adding after shifting the same displacement returns the original configuration. -/
 158theorem addedConfig_shiftedConfig {N : ℕ} (a s : CoupledCoreIndex N) :