OAI.Kadison.MatrixCorners.normalizedStageAlphabet_centered: intermediate lemma from OpenAI, Kadison's similarity theorem through uniform derivation estimates (result family 288)

import Mathlib
import Definitions.Def_OAIQ039C013

section

set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

namespace OAI

noncomputable section

section

noncomputable section

open scoped BigOperators ComplexOrder InnerProductSpace

namespace Kadison.MatrixCorners

attribute [local instance] Classical.propDecidable

variable {A : Type*} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
  (τ : A →ₚ[ℂ] ℂ) (hτ : ∀ a b, τ (a*b)=τ (b*a)) (h1 : τ 1=1)
  {I : Type*} [Fintype I] [DecidableEq I] [Nonempty I]
  (φ : Matrix I I ℂ →⋆ₐ[ℂ] A) (p : Matrix I I ℂ) (hp : IsStarProjection p)
  {G : Type*} [Fintype G] [DecidableEq G] [AddCommGroup G]
  (e : G ≃ projectionIndices p hp)

variable (α : ℝ) (hα : 0<α) (hατ : τ (φ p)=(α:ℂ))

include hτ h1 in
omit [StarOrderedRing A] in
lemma normalizedStageAlphabet_centered (g : G) (hg : g≠0) :
    τ (normalizedStageAlphabet φ p hp e α g)=0 := by
  sorry

end Kadison.MatrixCorners

end

end
end

end OAI
end