OAI/Combinatorics/UniformKServer/EpochAlphaPieces.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Full-child formulas for the epoch primitives. They make genuinely changing active subtypes transparent and prove that a held coordinate has unchanged potential piece when A, mark and U are fixed.

  1. theorem OAI.UniformKServer.EpochAlphaPieces.regular_piece line 19
  2. theorem OAI.UniformKServer.EpochAlphaPieces.marked_piece line 29
  3. theorem OAI.UniformKServer.EpochAlphaPieces.regular_same line 49
  4. theorem OAI.UniformKServer.EpochAlphaPieces.marked_same line 65