Dropout analysis properties

TorchLean splits stochastic training-mode dropout into two pieces:

• a mask/seed producer, treated as non-differentiated data in autograd proofs, and
• a deterministic tensor map once the mask or inference probability is fixed.

This file records the spec-level identity for the deterministic inference map. The fixed-mask training-mode derivative infrastructure lives with the autograd tape-node proofs.

Reference: Srivastava et al., 2014, “Dropout: A Simple Way to Prevent Neural Networks from Overfitting”.

theorem Proofs.dropoutInferenceSpec_eq_id {s : Spec.Shape} (p : ℝ) (x : Spec.Tensor ℝ s) : Spec.dropoutInferenceSpec p x = x

Evaluation-mode dropout is the identity for every configured training probability.