Documentation

LeanMlir.Proofs.Nets.ConvNeXt.ConvNeXtChannelLN

ConvNeXt's channel LayerNorm — the render's γ/β outputs and the graph transport #

The op itself — chanLNTensor3, its VJP, chanLNRows and the γ/β gradient contractions — is Architectures/ChannelLN. This file holds what is ConvNeXt's: the two statements that the render's LN tail (veclnGammaSgd / rowDenseBiasSgd on the transposed views) denotes the certified γ/β step (cnx_render_chlngamma_certified, cnx_render_chlnbeta_certified), and the graph-side ▸ transport (den_reassocS / den_unassocS) that keeps ConvNeXtRender's reassoc and chanLNTensor3 describing one function.

source
theorem Proofs.cnx_render_chlngamma_certified {c h w : ℕ} (ε : ℝ) (β γ : Vec c) (x cot : Vec (c * h * w)) (lr : ℝ) (k : Fin c) :
γ k - lr * vecLNGradGamma (h * w) c ε (Mat.unflatten (chanLNRows c h w x)) (Mat.unflatten (chanLNRows c h w cot)) k = γ k - lr * ∑ j : Fin (c * h * w), pdiv (fun (γ' : Vec c) => chanLNTensor3 c h w ε γ' β x) γ k j * cot j

Channel-LN γ output, certified. The rendered per-channel reduce — ViT's vecLNGradGamma on the two transposed views the tail emits — equals the certified Jacobian of chanLNTensor3 in its Vec c γ, contracted with the activation-layout cotangent. The den target of the render's veclnGammaSgd LN tail.

source
theorem Proofs.cnx_render_chlnbeta_certified {c h w : ℕ} (ε : ℝ) (γ β : Vec c) (x cot : Vec (c * h * w)) (lr : ℝ) (k : Fin c) :
β k - lr * vecLNGradBeta (h * w) c (Mat.unflatten (chanLNRows c h w cot)) k = β k - lr * ∑ j : Fin (c * h * w), pdiv (fun (β' : Vec c) => chanLNTensor3 c h w ε γ β' x) β k j * cot j

Channel-LN β output, certified. The β grad is the plain reduce Σ_rows dy, so the same rowDenseBiasSgd op ViT's LN-β uses denotes it here too.

source
theorem Proofs.StableHLO.den_reassocS {c h w : ℕ} (e : SHlo (c * h * w)) :
den (reassoc e) = reassocFwd c h w (den e)

The graph's reassoc transport IS the math's Mat-split bridge — den_castIdx composed with reassocFwdIdx_val. This is the lemma that keeps ConvNeXtRender's channel-LN sites and chanLNTensor3 describing one function.

source
theorem Proofs.StableHLO.den_unassocS {c h w : ℕ} (e : SHlo (c * (h * w))) :
den (unassoc e) = reassocBack c h w (den e)