Optional drop sites — stochastic depth and classifier dropout as Option binders #

A verified render carries stochastic depth and classifier dropout as HOST-DRAWN mask inputs (Proofs.Training.DropPath: the keep probability is folded into the mask, the op is a diagonal scale, its VJP is itself). Whether a site is RENDERED is a renderer flag (sd, cd), so a graph or chain statement that covers both the drop-free artifact and the *drop* / *do* one takes the site as an Option: none emits no node and denotes the identity, some s emits the dropPathB / dropoutB node at the mask s. The forward graphs state their sites this way (LeanMlir.Proofs.Nets.EfficientNet.EfficientNetFullB0Drop's efficientnetFwdGraphBFullDrop); the step, sync and loss-gradient ties thread the same binder through their cotangent chains (Proofs.MobileNetV2TieB's classifier dropout first), so the drop-free tie is the none instance verbatim and the some instance is the artifact that trained.

• dropPathOpt / dropoutOpt — the real-valued site; _none is rfl, _ones the eval identity (dropPath_ones_id, dropout_ones_id).
• dropPathOptG / dropoutOptG — the graph node; den_* by cases on the site.
• dropoutOptHasVJP / dropPathOptHasVJP — the VJP, its backward THE OP ITSELF at the same mask at either value (dropout_vjp_is_self one Option up), stated as the backward field so a chain lemma that is rfl at the drop-free chain stays rfl with the site in; the differentiability each tie's HasGradAt.comp needs beside it.
• dropoutOpt_smul, dropoutOpt_shard — what a data-parallel tie needs: the site is linear in the cotangent and commutes with the batch cut when replica r holds shard r of the mask, as the DP renders' per-replica %do inputs are. dropPathOpt_smul, dropPathOpt_shard are the per-example-mask peers: a stochastic-depth mask is a Vec N of scalars, cut by exampleShard (batchShard's cut at width one), and dropPathOptFam is the replica family a DP chain feeds a drop site, with its _shard and _scaled (the invariant the sync ties carry block to block).