OAI/Analysis/MutuallyUnbiased/Fourier/FourierEndpoint.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MUB6.FourierZero.permuted_charge line 10
2. theorem OAI.MUB6.fourier_vanishing_of_pair_certificates line 16

   Source documentation

   The structural deduction from the two exact pair identities. The final endpoint instantiates these identities with their checked integer certificates.

   theorem fourier_vanishing_of_pair_certificates {H : CMatrix} (hH : IsHadamard H)
       (hcross : PairCertificateIdentity H qCross) (hsame : PairCertificateIdentity H qSame)
       (hTao : ¬Equivalent H tao) (π : Equiv.Perm Coord) :
       g H (permuteCharge π alpha) = 0 := by
   …

   Mentions: OAI.MUB6.CMatrix, OAI.MUB6.IsHadamard, OAI.MUB6.PairCertificateIdentity, OAI.MUB6.qCross, OAI.MUB6.qSame, OAI.MUB6.Equivalent, OAI.MUB6.tao, OAI.MUB6.Coord, OAI.MUB6.g, OAI.MUB6.permuteCharge, OAI.MUB6.alpha