phaseCharacter_zero

formal source

 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) :
 159    addedConfig a (shiftedConfig a s) = s := by
 160  funext x
 161  exact add4_sub4_cancel_core (s x) (a x)
 162
 163/-- For fixed `s`, the displacement label is recoverable from `addedConfig a s`. -/
 164theorem addedConfig_eq_addedConfig_iff_left {N : ℕ}
 165    (a a' s : CoupledCoreIndex N) :
 166    addedConfig a s = addedConfig a' s ↔ a = a' := by
 167  constructor
 168  · intro h
 169    funext x
 170    exact (add4_eq_add4_iff_left_core (a x) (a' x) (s x)).mp (congrArg (fun f => f x) h)