Documentation

LeanMlir.Proofs.Nets.MobileNet.MobileNetV2Fold

The stride-1 depthwise param updates, proof-tied to the certified SGD step #

The two stride-1 depthwise{Weight,Bias}Sgd ops (StableHLO.lean) each denote the certified loss-descent step θ − lr·(certified ∂/∂θ · c), generic in the cotangent c the backward chain delivers — the depthwise peers of CifarPoC.convW_den/convB_den, delegating to the mnv2_render_depthwise*_certified bridges (MobileNetV2Close.lean). Written for MobileNetV2's per-example fold; ConvNeXt-T's 7×7 depthwise ties (ConvNeXtStepTie) are what use them now.

depthwiseB_den delegates to mnv2_render_depthwiseb_certified. The weight is the one needing a bridge: the stride-1 depthwise weight VJP is 3-index (depthwise_weight_grad_has_vjp3), and the emitted op's den carries it flat (Tensor3.flatten (… .backward W (unflatten c))), so depthwiseW_den first routes through mnv2_render_depthwiseW_flat_certified — the flat pdiv-Jacobian form via hasVJP3_to_hasVJP.correct, modulo the unflatten ∘ flatten = id round-trip on W.

Honest residual #

source
theorem Proofs.Mnv2PoC.mnv2_render_depthwiseW_flat_certified {c h w kH kW : ℕ} (b : Vec c) (x : Tensor3 c h w) (W : DepthwiseKernel c kH kW) (cot : Vec (c * h * w)) (lr : ℝ) (idx : Fin (c * kH * kW)) :
Tensor3.flatten W idx - lr * ((depthwise_weight_grad_has_vjp3 b x).backward W (Tensor3.unflatten cot)).flatten idx = Tensor3.flatten W idx - lr * ∑ j : Fin (c * h * w), pdiv (fun (v' : Vec (c * kH * kW)) => (depthwiseConv2d (Tensor3.unflatten v') b x).flatten) (Tensor3.flatten W) idx j * cot j

Flat stride-1 depthwise weight render bridge. The emitted op's flat weight grad flatten W − lr·flatten((dwconv_weight_grad₃ b x).backward W (unflatten c)) equals the flat pdiv-Jacobian form. Via hasVJP3_to_hasVJP.correct (the triple→flat reindex), modulo unflatten (flatten W) = W. The stride-1 depthwise peer of cnn_render_convW_certified.

source
theorem Proofs.Mnv2PoC.depthwiseW_den {c h w kH kW : ℕ} (xN wN lrStr cotN : String) (b : Vec c) (x : Tensor3 c h w) (W : DepthwiseKernel c kH kW) (cot : Vec (c * h * w)) (lr : ℝ) (idx : Fin (c * kH * kW)) :
StableHLO.den (StableHLO.SHlo.depthwiseWeightSgd xN wN lrStr b x W lr (StableHLO.SHlo.operand cotN cot)) idx = Tensor3.flatten W idx - lr * ∑ j : Fin (c * h * w), pdiv (fun (v' : Vec (c * kH * kW)) => (depthwiseConv2d (Tensor3.unflatten v') b x).flatten) (Tensor3.flatten W) idx j * cot j

Stride-1 depthwise weight op = certified. The depthwiseWeightSgd op denotes flatten W − lr·(certified ∂(depthwiseConv2d)/∂W · c) (flat pdiv form). The stride-1 depthwise peer of CifarPoC.convW_den.

source
theorem Proofs.Mnv2PoC.depthwiseB_den {c h w kH kW : ℕ} (bN lrStr cotN : String) (W : DepthwiseKernel c kH kW) (x : Tensor3 c h w) (b : Vec c) (cot : Vec (c * h * w)) (lr : ℝ) (o : Fin c) :
StableHLO.den (StableHLO.SHlo.depthwiseBiasSgd bN lrStr W x b lr (StableHLO.SHlo.operand cotN cot)) o = b o - lr * ∑ j : Fin (c * h * w), pdiv (fun (b' : Vec c) => (depthwiseConv2d W b' x).flatten) b o j * cot j

Stride-1 depthwise bias op = certified. Delegates to mnv2_render_depthwiseb_certified.