OAI/InformationTheory/SecretKey/Main.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ZeroKey.class_uniformProtocolGap line 15
2. theorem OAI.ZeroKey.class_uniformCompletedGap line 21
3. theorem OAI.ZeroKey.Explicit.mainClaim_iff_original line 31

   Source documentation

   The explicit density witness removes a proof dependency from the challenge statement. This is equivalent to the original five-clause formulation.

   theorem mainClaim_iff_original : MainClaim.{u} ↔
       (Density rhoFin ∧ ¬ Separable rhoFin ∧
         distillableSecretKey.{u} rhoFin rhoFin_density = 0 ∧
         UniformProtocolGap.{u} rhoFin rhoFin_density ∧
         UniformCompletedGap.{u} rhoFin rhoFin_density) := by
   …

   Mentions: OAI.ZeroKey.Density, OAI.ZeroKey.Explicit.rhoFin, OAI.ZeroKey.Separable, OAI.ZeroKey.Explicit.rhoFin_density

4. theorem OAI.ZeroKey.Explicit.main line 42