OAI/NumberTheory/CubicMoment/Theta/CubicThetaRamifiedPhaseEigen.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The explicit modulus-nine phase is an eigenvector of the actual middle-row operator, with eigenvalue two thirds.

  1. theorem OAI.CubicFirstMoment.cubicThetaRamifiedMiddle_phase_eigen line 12