OAI/NumberTheory/DukePrimeDegree/Dynamics/VelocityTransportRank.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Rank transport for actual stabilizer frames

Right translation conjugates the actual velocity space by a linear equivalence. Thus the cardinality of the constructed measurable frame is preserved under component-kernel covariance. This supplies the invariant rank events used by the finite-frame recurrence theorem.

  1. def OAI.DukePrimeDegree.slMatrixConjugationEquiv line 22
  2. theorem OAI.DukePrimeDegree.map_matrixVelocitySpace_rightAction line 31
  3. theorem OAI.DukePrimeDegree.velocityFrameCard_map_rightAction line 48