Documentation

LeanMlir.Proofs.Codegen.StableHLO.Basic

StableHLO — the emitted-graph AST and its ℝ semantics #

The verified renderers build the computation in each verified_mlir/ artifact from pretty of terms of one typed AST, SHlo, and add hand-written text around it: the function signature and constants, the report-only %loss block, the %bc1/%bc2 passthroughs of the AdamW steps, and the carve-outs each renderer's docstring names (for ConvNeXt: the GAP-backward block, the %dy divide, and in the SGD step the stem weight's update). This file holds that AST and its semantic reading; the syntactic one, pretty, is in StableHLO.Pretty.

Layout, in file order:

partwhere
BatchableOp — the per-example ops SHlo.batchOp lifts by batchMaptop
inductive SHlo (≈215 constructors; suffixes: F forward/optimizer op, B/Batched batched index, Grad/GradB raw gradient node, Sgd/SgdB fused θ − lr·g, Bf16/F8 reduced precision)§ StableHLO-subset AST
den, the denStep/denStepApp dsimprocs, the per-op *_faithful lemmasafter the AST
chapter graphs and their faithfulness (linear, MLP, CNN, CIFAR) and the optimizer/clip ops§ Chapter 1–3, § Param gradients, § Global-norm clipping

Trusted residue. den is over ℝ, so the ℝ→Float32 gap stays trusted. Everything here closes under [propext, Classical.choice, Quot.sound] (tests/AuditAxioms.lean).

source
inductive Proofs.StableHLO.BatchableOp :
ℕ → ℕ → Type

A batch-separable EfficientNet op, shape-indexed by per-example in/out length. The descriptor carried by SHlo.batchOp; its denOp is the proven per-example forward, lifted by batchMap.

On the pointwise ops. The descriptor-less swish/sigmoid/relu/addV tokens do denote block-diagonally at the batched index N·(c·h·w), but they do not EMIT correctly there. SHlo.swishF's token carries only the SHlo index n and emits tensor<B×n>, i.e. it reads the index as a PER-EXAMPLE width; a descriptor-less pointwise node at the batched index N·s therefore emits tensor<B×(N·s)>, which does not even typecheck against its own operand. Giving the pointwise ops descriptors separates the two numbers — N (batch, denotation) from n (per-example width, emit) — which is what lets a whole graph sit at N := B where the batch-coupled dens (bnBatchF, the *SgdB family) are honest. The per-example renderers keep the descriptor-less tokens unchanged.

Instances For
    source
    inductive Proofs.StableHLO.SHlo :
    ℕ → Type

    A StableHLO-subset expression, shape-indexed by result length. Leaves carry both a value (for den) and an SSA name (for pretty); the name is denotation-irrelevant. One constructor per emitted op.

    Instances For
      source
      noncomputable def Proofs.StableHLO.maxPoolBackFlat (c h w : ℕ) (xv : Vec (c * (2 * h) * (2 * w))) (dyv : Vec (c * h * w)) :
      Vec (c * (2 * h) * (2 * w))
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def Proofs.StableHLO.maxPool3s2BackFlat (c h w : ℕ) (xv : Vec (c * (2 * h) * (2 * w))) (dyv : Vec (c * h * w)) :
        Vec (c * (2 * h) * (2 * w))

        3×3/s2 max-pool backward (flattened) — the peer of maxPoolBackFlat at He et al.'s stem pool, matching maxPool3s2HasVJPAt3.backward lifted through HasVJPAt3.toHasVJPAt. Total in the saved input xv (the no-ties proof lives only in .correct).

        This is a SUM where the 2×2 peer is a lookup, and that is the whole difference between the two pools. maxPool2's windows tile, so each input is the argmax of at most one output and the backward can name it directly. 3×3/s2 windows OVERLAP, so an input can be the argmax of up to four outputs (win3Row_mem_le_two squared) and the cotangent must ACCUMULATE. Nothing in HasVJPAt3.correct had to change for that — it already states the backward as a sum over all outputs, and maxPool2's peer merely collapses it using disjointness.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def Proofs.StableHLO.rowSoftmaxFlat (m n : ℕ) (v : Vec (m * n)) :
          Vec (m * n)

          Row-softmax (flattened) — apply the 1-D softmax (MLP.lean) to each of the m rows of the row-major Vec (m*n). Definitionally equal to Mat.flatten ∘ rowSoftmax ∘ Mat.unflatten (Attention.lean's rowSoftmax; the tie is rowSoftmaxFlat_flat in ViTFwdGraph).

          Equations
          Instances For
            source
            noncomputable def Proofs.StableHLO.rowSoftmaxBackFlat (m n : ℕ) (preAct dy : Vec (m * n)) :
            Vec (m * n)

            Row-softmax backward (flattened) — per row, the proven closed form pᵢ⊙(dyᵢ − ⟨pᵢ,dyᵢ⟩) with pᵢ = softmax(preActᵢ). Definitionally equal to Mat.flatten ∘ rowSoftmaxHasVJPMat.backward (Mat.unflatten preAct) ∘ Mat.unflatten (since softmaxHasVJP.backward z dy i = let p := softmax z; p i·(dy i − ⟨p,dy⟩)).

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              noncomputable def Proofs.StableHLO.matMulFlat (m k n : ℕ) (a : Vec (m * k)) (b : Vec (k * n)) :
              Vec (m * n)

              Flattened matrix multiply C = A·B on row-major flat operands. Definitionally Mat.flatten ∘ Mat.mul ∘ Mat.unflatten².

              Equations
              Instances For
                source
                noncomputable def Proofs.StableHLO.transposeFlat (m n : ℕ) (v : Vec (m * n)) :
                Vec (n * m)

                Flattened transpose — Mat.transpose conjugated by row-major flattening.

                Equations
                Instances For
                  source
                  noncomputable def Proofs.StableHLO.rowLNFlat (m n : ℕ) (ε γ β : ℝ) (v : Vec (m * n)) :
                  Vec (m * n)

                  Row-wise LayerNorm (flattened) — each of the m token rows gets the 1-D bnForward over its n features (LayerNorm IS per-example BN: layerNormForward := bnForward definitionally, LayerNorm.lean).

                  Equations
                  Instances For
                    source
                    noncomputable def Proofs.StableHLO.rowLNBackFlat (m n : ℕ) (ε γ : ℝ) (x dy : Vec (m * n)) :
                    Vec (m * n)

                    Row-wise LayerNorm input-VJP (flattened) — per row the consolidated three-term bnGradInput, recomputing x̂/istd from the saved pre-LN input.

                    Equations
                    Instances For
                      source
                      noncomputable def Proofs.StableHLO.rowDenseFlat (N a c : ℕ) (W : Mat a c) (b : Vec c) (v : Vec (N * a)) :
                      Vec (N * c)

                      Per-token dense (flattened) — every row of the [N,a] flat through the same dense W b.

                      Equations
                      Instances For
                        source
                        noncomputable def Proofs.StableHLO.rowDenseBackFlat (N a c : ℕ) (W : Mat a c) (dy : Vec (N * c)) :
                        Vec (N * a)

                        Per-token dense input-VJP (flattened) — per row dX = W·dy (= (denseHasVJP W b).backward's Mat.mulVec W, MLP.lean).

                        Equations
                        Instances For
                          source
                          @[reducible, inline]
                          noncomputable abbrev Proofs.StableHLO.patchEmbedBackFlat (ic H W patchSize N D : ℕ) (W_conv : Kernel4 D ic patchSize patchSize) (dy : Vec ((N + 1) * D)) :
                          Vec (ic * H * W)

                          ViT patch-embedding input-VJP (flattened) — the proven patchEmbedInputGradFormula (Attention.lean), i.e. patchEmbedFlatHasVJP.backward: the strided patchify conv's input-VJP on the patch-token rows of the cotangent. The CLS row and the position-add (a +constant) contribute nothing.

                          Equations
                          Instances For
                            source
                            noncomputable def Proofs.StableHLO.patchEmbedWeightGradFlat (ic H W patchSize N D : ℕ) (img : Vec (ic * H * W)) (dy : Vec ((N + 1) * D)) :
                            Vec (D * ic * patchSize * patchSize)

                            ViT patch-embedding weight-grad (flattened) — TokenParamGrad's patchEmbedWeightGrad, flattened (that file is downstream of this one; the tie is patchEmbed_weight_sgd_certified). The non-overlapping 16×16/s16 patchify conv's weight-VJP: dW_(d,c,kh,kw) = Σ_patches (patch pixel read)·dy_(patch.succ, d) — token 0 is the CLS row (excluded); the pixel read mirrors patchEmbedFlat's, and dy (finProdFinEquiv (p.succ, d)) mirrors patchEmbedBackFlat.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              noncomputable def Proofs.StableHLO.patchEmbedFlatBf16 (rnd : ℝ → ℝ) (ic H W patchSize N D : ℕ) (W_conv : Kernel4 D ic patchSize patchSize) (b_conv cls_token : Vec D) (pos_embed : Mat (N + 1) D) :
                              Vec (ic * H * W) → Vec ((N + 1) * D)

                              ViT patch embedding at bf16 operands (flattened) — patchEmbedFlat's body with the three roundings the emit actually performs, and nothing else.

                              The placement of each rnd is the whole content of this definition, so read it against the emitted text rather than against the f32 peer:

                              • rnd (W_conv …) and rnd (img …) are the two operand casts — the stablehlo.converts that make the convolution's inputs bf16.
                              • the outer rnd on the patch sum is the bf16 STORE: the convolution is emitted with a bf16-TYPED result, so the hardware accumulates the MAC in f32 and rounds on the way out. Dropping it would claim more precision than the hardware delivers — the unsound direction.
                              • b_conv, cls_token and pos_embed are added outside every rounding, because the emit adds them after the convert-back, in f32. They are f32 parameters that never reach a tensor core.

                              The CLS row (n = 0) carries no convolution at all, so no rounding touches it — which is why the if is INSIDE the roundings' scope rather than outside it.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                source
                                noncomputable def Proofs.StableHLO.clsSliceFlat (N D : ℕ) (v : Vec ((N + 1) * D)) :
                                Vec D

                                CLS slice (flattened) — gather row 0 of the [N+1,D] flat (= the proven clsTokenFlat, Attention.lean; tie is rfl in ViTFwdGraph).

                                Equations
                                Instances For
                                  source
                                  noncomputable def Proofs.StableHLO.clsPadFlat (N D : ℕ) (dy : Vec D) :
                                  Vec ((N + 1) * D)

                                  CLS pad (flattened) — scatter dy to row 0, zeros elsewhere (= the proven clsTokenFlatHasVJP.backward; tie is rfl in ViTFwdGraph).

                                  Equations
                                  Instances For
                                    source
                                    noncomputable def Proofs.StableHLO.headSliceFlat (N heads d : ℕ) (h : Fin heads) (v : Vec (N * (heads * d))) :
                                    Vec (N * d)

                                    Per-head column slice (flattened) — head h's [N,d] block of the [N,heads·d] flat: the finProdFinEquiv (h, ·) column gather mhsaLayer uses to feed each head's SDPA.

                                    Equations
                                    Instances For
                                      source
                                      noncomputable def Proofs.StableHLO.headPadFlat (N heads d : ℕ) (h : Fin heads) (v : Vec (N * d)) :
                                      Vec (N * (heads * d))

                                      Per-head column pad (flattened) — scatter an [N,d] head block into head h's columns of a zero [N,heads·d]. mhsaLayer's concat is the sum of these over heads; it is also headSliceFlat's VJP.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        source
                                        noncomputable def Proofs.StableHLO.rowScaleFlat (m n : ℕ) (γ : Vec n) (v : Vec (m * n)) :
                                        Vec (m * n)

                                        Row-broadcast scale (flattened) — every token row elementwise-scaled by the shared γ : Vec n (= rowwise layerScale γ).

                                        Equations
                                        Instances For
                                          source
                                          noncomputable def Proofs.StableHLO.rowBiasFlat (m n : ℕ) (β : Vec n) (v : Vec (m * n)) :
                                          Vec (m * n)

                                          Row-broadcast bias (flattened) — + β on every token row.

                                          Equations
                                          Instances For
                                            source
                                            def Proofs.StableHLO.chanIdx (c h w : ℕ) (k : Fin (c * h * w)) :
                                            Fin c

                                            Channel index of a flat c·h·w position (the repo's left-assoc finProdFinEquiv convention: k ↔ ((chan, row), col)). Used to expand a per-channel parameter (Vec c) to the flat per-element map.

                                            Equations
                                            Instances For
                                              source
                                              noncomputable def Proofs.StableHLO.denOp {a b : ℕ} :
                                              BatchableOp a b → Vec a → Vec b

                                              The proven per-example forward of a BatchableOp — exactly the existing batch-1 op (flatConv/depthwiseFlat/dense/globalAvgPoolFlat/seBlockFull/…). SHlo.batchOp's den is batchMap N (denOp op).

                                              Equations
                                              Instances For
                                                source
                                                inductive Proofs.StableHLO.BnMode :
                                                Type

                                                Which BatchNorm a batched forward chain emits, for the renders whose one traversal produces both the training forward and its frozen-stats eval partner (EfficientNet, MobileNetV4).

                                                The distinction is not cosmetic: a .train chain reduces its statistics out of the activation (bnBatchF, which couples the batch), a .eval chain consumes frozen per-channel running stats as graph inputs (the bnEval descriptor, which does not). A net trained on one and scored with the other is evaluating a different function.

                                                • train : BnMode

                                                  Training: batch statistics reduced out of the activation (bnBatchF, reduce [0,2,3], n = B·H·W). What the train step differentiates.

                                                • eval : BnMode

                                                  Inference: frozen per-channel running stats arriving as graph inputs %{p}mu/%{p}var (the bnEval descriptor). Class-batch-independent.

                                                Instances For
                                                  source
                                                  @[instance_reducible]
                                                  instance Proofs.StableHLO.instDecidableEqBnMode :
                                                  DecidableEq BnMode
                                                  Equations
                                                  source
                                                  def Proofs.StableHLO.instReprBnMode.repr :
                                                  BnMode → ℕ → Std.Format
                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    source
                                                    @[instance_reducible]
                                                    instance Proofs.StableHLO.instReprBnMode :
                                                    Repr BnMode
                                                    Equations
                                                    source
                                                    noncomputable def Proofs.StableHLO.den {n : ℕ} :
                                                    SHlo n → Vec n

                                                    AST denotation ⟦·⟧ₐ — our reading of each StableHLO op's spec, over ℝ, in primitive terms — independent of dense/Mat.mulVec. The per-example constructors denote one example; batchOp and the *B/*GradB/bnBatchF constructors denote at the batched index N·n (the batch-statistic and gradient-sum arms couple the batch); allReduceMeanF denotes the mean over its R replica children. SSA names are ignored.

                                                    Instances For
                                                      source
                                                      def Proofs.StableHLO.denUnfold? (e : Lean.Expr) :
                                                      Lean.MetaM (Option Lean.Expr)

                                                      den e (and den e i) one constructor deep, by smart unfolding at default transparency: the match reduces the way the den_* lemmas' rfl does, and nothing asks for den.eq_def.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        source
                                                        def Proofs.StableHLO.denStep :
                                                        Lean.Meta.Simp.DSimproc

                                                        What simp only should name instead of den. Naming den itself makes Lean build den.eq_def — about four minutes for the 215-arm match, on the critical path of this module and anything that first asks for it. denStepApp is the same step where den e is applied to an index, which simp does not visit as den e.

                                                        Equations
                                                        Instances For
                                                          source
                                                          def Proofs.StableHLO.denStepApp :
                                                          Lean.Meta.Simp.DSimproc

                                                          denStep where den e is applied to an index.

                                                          Equations
                                                          Instances For
                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_operand {n : ℕ} (s : String) (v : Vec n) :
                                                            den (SHlo.operand s v) = v
                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_dotIn {m n : ℕ} (s : String) (W : Mat m n) (e : SHlo m) :
                                                            den (SHlo.dotIn s W e) = fun (j : Fin n) => ∑ i : Fin m, den e i * W i j
                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_dotInBf16 {m n : ℕ} (rnd : ℝ → ℝ) (s : String) (W : Mat m n) (e : SHlo m) :
                                                            den (SHlo.dotInBf16 rnd s W e) = fun (j : Fin n) => ∑ i : Fin m, rnd (den e i) * rnd (W i j)

                                                            The mixed-precision matmul denotes the EXACT sum over ROUNDED operands. The fp32 accumulate is why the ∑ carries no rounding of its own — the whole deviation from dotIn sits in the two rnds, which is the structural reason bf16 is the easy twin of fp8 (no block scale to factor through the sum).

                                                            source
                                                            theorem Proofs.StableHLO.dotInBf16_eq_dotIn_rounded {m n : ℕ} (rnd : ℝ → ℝ) (s : String) (W : Mat m n) (e : SHlo m) :
                                                            den (SHlo.dotInBf16 rnd s W e) = den (SHlo.dotIn s (fun (i : Fin m) (j : Fin n) => rnd (W i j)) (SHlo.convertF rnd e))

                                                            The bundling is inert. dotInBf16 on raw operands denotes exactly what dotIn denotes on PRE-rounded ones — so every tie already proven in the dotIn vocabulary (e.g. Bf16PoC.bf16_render_faithful) transfers to the emittable node by rewriting with this, rather than being reproved.

                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_dotOut {m n : ℕ} (s : String) (W : Mat m n) (e : SHlo n) :
                                                            den (SHlo.dotOut s W e) = fun (i : Fin m) => ∑ j : Fin n, W i j * den e j
                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_addBcast {n : ℕ} (s : String) (b : Vec n) (e : SHlo n) :
                                                            den (SHlo.addBcast s b e) = fun (j : Fin n) => den e j + b j
                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_expe {n : ℕ} (e : SHlo n) :
                                                            den e.expe = fun (j : Fin n) => Real.exp (den e j)
                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_softmaxDiv {n : ℕ} (e : SHlo n) :
                                                            den e.softmaxDiv = fun (j : Fin n) => den e j / ∑ k : Fin n, den e k
                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_addV {n : ℕ} (a b : SHlo n) :
                                                            den (a.addV b) = fun (j : Fin n) => den a j + den b j
                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_reluF {n : ℕ} (e : SHlo n) :
                                                            den e.reluF = fun (i : Fin n) => max (den e i) 0
                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_selectPos {n : ℕ} (s : String) (x : Vec n) (e : SHlo n) :
                                                            den (SHlo.selectPos s x e) = fun (i : Fin n) => if x i > 0 then den e i else 0
                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_convertF {n : ℕ} (rnd : ℝ → ℝ) (e : SHlo n) :
                                                            den (SHlo.convertF rnd e) = fun (i : Fin n) => rnd (den e i)

                                                            The round node is den-faithful for any rounding. This is the equation Proofs/Float/Bf16Fold.lean asks for by name to lift its depth-1 tie to depth > 1: rounding an intermediate activation is now an in-graph op whose denotation is exactly post-composition with rnd. No bf16 specifics appear here — bf16 round-to-nearest is one instance, and the accuracy half is supplied separately by dense_close_mixed at u_leaf = 2⁻⁸.

                                                            source
                                                            theorem Proofs.StableHLO.convertF_faithful {n : ℕ} (rnd : ℝ → ℝ) (e : SHlo n) :
                                                            den (SHlo.convertF rnd e) = rnd ∘ den e

                                                            The round node composed with den as a function, the form the tie proofs want.

                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_relu6F {n : ℕ} (e : SHlo n) :
                                                            den e.relu6F = fun (i : Fin n) => min (max (den e i) 0) 6
                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_selectMid {n : ℕ} (s : String) (x : Vec n) (e : SHlo n) :
                                                            den (SHlo.selectMid s x e) = fun (i : Fin n) => if 0 < x i ∧ x i < 6 then den e i else 0
                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_batchOp {N a b : ℕ} (op : BatchableOp a b) (e : SHlo (N * a)) :
                                                            den (SHlo.batchOp op e) = batchMap N (denOp op) (den e)

                                                            A batched token denotes its per-example op, lifted. den (.batchOp op e) is batchMap N of denOp op, the proven per-example map, by rfl; simp only [den_batchOp, denOp] reads a batched graph's denotation off denOp's arms. skel erases values, so a descriptor with the wrong denOp emits identical bytes: this equation is the half the emit ties cannot see. The true-batch-norm token is not a descriptor; it denotes bnBatchLA (den_bnBatchF).

                                                            source
                                                            theorem Proofs.StableHLO.den_batchOp_swish_eq_swishF {N n : ℕ} (e : SHlo (N * n)) :
                                                            den (SHlo.batchOp BatchableOp.swish e) = den e.swishF

                                                            The descriptor form of swish denotes exactly what the descriptor-less swishF denoted at the same index — the batched graph computes the same function, only the emit width now travels separately from the batch.

                                                            source
                                                            theorem Proofs.StableHLO.den_batchOp_softmaxDiv_per_example {N n : ℕ} (e : SHlo (N * n)) (k : Fin N) (j : Fin n) :
                                                            den (SHlo.batchOp BatchableOp.softmaxDiv e) (finProdFinEquiv (k, j)) = batchSlice N n (den e) k j / ∑ i : Fin n, batchSlice N n (den e) k i

                                                            The softmax denominator is PER EXAMPLE — the property this descriptor exists for. Example k's output divides by example k's own sum, not by the sum over the whole batch.

                                                            This is the half the emit tie structurally cannot see. .softmaxDiv's emitted MLIR was already per-example (it reduces over dimensions = [1] of tensor<B,n>), so the batched and per-example forms render byte-for-byte identically and always would — while the descriptor-less den at index N·n reads v j / ∑ k, v k over ALL N·n coordinates, i.e. it divides by the batch's total. Same bytes, different function, and only this statement separates them.

                                                            source
                                                            theorem Proofs.StableHLO.den_batchOp_clsSlice_per_example {N tk D : ℕ} (e : SHlo (N * ((tk + 1) * D))) (k : Fin N) (i : Fin D) :
                                                            den (SHlo.batchOp BatchableOp.clsSlice e) (finProdFinEquiv (k, i)) = clsSliceFlat tk D (batchSlice N ((tk + 1) * D) (den e) k) i

                                                            THE CLS SLICE IS THE ONE PLACE THE BATCH AND THE TOKEN AXIS COULD SWAP SILENTLY. clsSlice takes (tk+1)*D to D — it CONTRACTS — and batchMap N of it takes N*((tk+1)*D) to N*D. A render that read the batch as the token axis would take (N+1)*D to D, i.e. drop every example but one and still type-check at N = tk. Stated so the two indices are pinned apart by a theorem rather than by a naming convention.

                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_scaleB {N n : ℕ} (sS : String) (s : ℝ) (e : SHlo (N * n)) :
                                                            den (SHlo.scaleB sS s e) = fun (i : Fin (N * n)) => den e i * s
                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_shiftB {N n : ℕ} (sS : String) (s : ℝ) (e : SHlo (N * n)) :
                                                            den (SHlo.shiftB sS s e) = fun (i : Fin (N * n)) => den e i + s
                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_divConstB {N n : ℕ} (sS : String) (s : ℝ) (e : SHlo (N * n)) :
                                                            den (SHlo.divConstB sS s e) = fun (i : Fin (N * n)) => den e i / s
                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_allReduceMeanF {n : ℕ} (R : ℕ) (hR : 0 < R) (t : String) (ds : List ℕ) (g : Fin R → SHlo n) :
                                                            den (SHlo.allReduceMeanF R hR t ds g) = fun (i : Fin n) => 1 / ↑R * ∑ r : Fin R, den (g r) i

                                                            The all-reduce node denotes the replica mean of its operands. The DataParallel.dpMean spelling, stated here so a tie can read it without importing that file.

                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_bnBatchMeanB {N oc h w : ℕ} (e : SHlo (N * (oc * (h * w)))) :
                                                            den e.bnBatchMeanB = fun (c : Fin oc) => bnMean (N * (h * w)) (Mat.unflatten (bnchwFwd N oc h w (den e)) c)
                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_bnBatchVarB {N oc h w : ℕ} (e : SHlo (N * (oc * (h * w)))) :
                                                            den e.bnBatchVarB = fun (c : Fin oc) => bnVar (N * (h * w)) (Mat.unflatten (bnchwFwd N oc h w (den e)) c)
                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_bnBatchVarAtB {N oc h w : ℕ} (e : SHlo (N * (oc * (h * w)))) (mu : SHlo oc) :
                                                            den (e.bnBatchVarAtB mu) = fun (c : Fin oc) => bnVar (N * (h * w)) (Mat.unflatten (bnchwFwd N oc h w (den e)) c) + (bnMean (N * (h * w)) (Mat.unflatten (bnchwFwd N oc h w (den e)) c) - den mu c) * (bnMean (N * (h * w)) (Mat.unflatten (bnchwFwd N oc h w (den e)) c) - den mu c)
                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_bnPackB {oc : ℕ} (a b : SHlo oc) :
                                                            den (a.bnPackB b) = Fin.append (den a) (den b)
                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_bnSyncF {N oc h w : ℕ} (gName bName epsStr : String) (ε : ℝ) (γ β : Vec oc) (x : SHlo (N * (oc * (h * w)))) (st : SHlo (oc + oc)) :
                                                            den (SHlo.bnSyncF gName bName epsStr ε γ β x st) = bnSyncTensor4 N oc h w ε γ β (fun (c : Fin oc) => den st (Fin.castAdd oc c)) (fun (c : Fin oc) => den st (Fin.natAdd oc c) + den st (Fin.castAdd oc c) * den st (Fin.castAdd oc c)) (den x)
                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_bnSyncDyStatsB {N oc h w : ℕ} (gName xName epsStr : String) (ε : ℝ) (γ : Vec oc) (x : Vec (N * (oc * (h * w)))) (dy : SHlo (N * (oc * (h * w)))) (st : SHlo (oc + oc)) :
                                                            den (SHlo.bnSyncDyStatsB gName xName epsStr ε γ x dy st) = Fin.append (den st) (Fin.append (fun (c : Fin oc) => bnMean (N * (h * w)) fun (k : Fin (N * (h * w))) => γ c * Mat.unflatten (bnchwFwd N oc h w (den dy)) c k) fun (c : Fin oc) => bnMean (N * (h * w)) fun (k : Fin (N * (h * w))) => bnSyncXhat (N * (h * w)) ε (den st (Fin.castAdd oc c)) (den st (Fin.natAdd oc c) + den st (Fin.castAdd oc c) * den st (Fin.castAdd oc c)) (Mat.unflatten (bnchwFwd N oc h w x) c) k * (γ c * Mat.unflatten (bnchwFwd N oc h w (den dy)) c k))
                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_bnSyncBack {N oc h w : ℕ} (gName xName epsStr : String) (ε : ℝ) (γ : Vec oc) (x : Vec (N * (oc * (h * w)))) (dy : SHlo (N * (oc * (h * w)))) (ds : SHlo (oc + oc + (oc + oc))) :
                                                            den (SHlo.bnSyncBack gName xName epsStr ε γ x dy ds) = bnSyncTensor4GradInput N oc h w ε γ (fun (c : Fin oc) => den ds (Fin.castAdd (oc + oc) (Fin.castAdd oc c))) (fun (c : Fin oc) => den ds (Fin.castAdd (oc + oc) (Fin.natAdd oc c)) + den ds (Fin.castAdd (oc + oc) (Fin.castAdd oc c)) * den ds (Fin.castAdd (oc + oc) (Fin.castAdd oc c))) (fun (c : Fin oc) => den ds (Fin.natAdd (oc + oc) (Fin.castAdd oc c))) (fun (c : Fin oc) => den ds (Fin.natAdd (oc + oc) (Fin.natAdd oc c))) x (den dy)
                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_bnSyncGammaGradB {N oc h w : ℕ} (xName epsStr : String) (ε : ℝ) (x : Vec (N * (oc * (h * w)))) (dy : SHlo (N * (oc * (h * w)))) (st : SHlo (oc + oc)) :
                                                            den (SHlo.bnSyncGammaGradB xName epsStr ε x dy st) = bnSyncPerChannelGradGamma oc (N * (h * w)) ε (fun (c : Fin oc) => den st (Fin.castAdd oc c)) (fun (c : Fin oc) => den st (Fin.natAdd oc c) + den st (Fin.castAdd oc c) * den st (Fin.castAdd oc c)) (bnchwFwd N oc h w x) (bnchwFwd N oc h w (den dy))
                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_bnStatsMeanB {oc : ℕ} (e : SHlo (oc + oc)) :
                                                            den e.bnStatsMeanB = fun (c : Fin oc) => den e (Fin.castAdd oc c)
                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_bnStatsVarB {oc : ℕ} (e : SHlo (oc + oc)) :
                                                            den e.bnStatsVarB = fun (c : Fin oc) => den e (Fin.natAdd oc c)
                                                            source
                                                            theorem Proofs.StableHLO.den_allReduceMeanF_one {n : ℕ} (t : String) (ds : List ℕ) (g : SHlo n) (i : Fin n) :
                                                            den (SHlo.allReduceMeanF 1 Nat.one_pos t ds fun (x : Fin 1) => g) i = den g i

                                                            The one-replica collective threads its operand.

                                                            source
                                                            theorem Proofs.StableHLO.den_syncStats_R1 {N oc h w : ℕ} (t t' : String) (ds ds' : List ℕ) (x : SHlo (N * (oc * (h * w)))) (c : Fin oc) :
                                                            den ((SHlo.allReduceMeanF 1 Nat.one_pos t ds fun (x_1 : Fin 1) => x.bnBatchMeanB).bnPackB (SHlo.allReduceMeanF 1 Nat.one_pos t' ds' fun (x_1 : Fin 1) => x.bnBatchVarAtB (SHlo.allReduceMeanF 1 Nat.one_pos t ds fun (x_2 : Fin 1) => x.bnBatchMeanB))) (Fin.castAdd oc c) = bnMean (N * (h * w)) (Mat.unflatten (bnchwFwd N oc h w (den x)) c) ∧ den ((SHlo.allReduceMeanF 1 Nat.one_pos t ds fun (x_1 : Fin 1) => x.bnBatchMeanB).bnPackB (SHlo.allReduceMeanF 1 Nat.one_pos t' ds' fun (x_1 : Fin 1) => x.bnBatchVarAtB (SHlo.allReduceMeanF 1 Nat.one_pos t ds fun (x_2 : Fin 1) => x.bnBatchMeanB))) (Fin.natAdd oc c) = bnVar (N * (h * w)) (Mat.unflatten (bnchwFwd N oc h w (den x)) c)

                                                            At R = 1 the two-round statistics subgraph is [μ ‖ σ²] of the batch itself: the replica's own mean, and its own two-pass variance with a zero offset.

                                                            source
                                                            theorem Proofs.StableHLO.den_bnSyncF_allReduce_R1 {N oc h w : ℕ} (gN bN es t t' : String) (ds ds' : List ℕ) (ε : ℝ) (γ β : Vec oc) (hm : N * (h * w) ≠ 0) (x : SHlo (N * (oc * (h * w)))) :
                                                            den (SHlo.bnSyncF gN bN es ε γ β x ((SHlo.allReduceMeanF 1 Nat.one_pos t ds fun (x_1 : Fin 1) => x.bnBatchMeanB).bnPackB (SHlo.allReduceMeanF 1 Nat.one_pos t' ds' fun (x_1 : Fin 1) => x.bnBatchVarAtB (SHlo.allReduceMeanF 1 Nat.one_pos t ds fun (x_2 : Fin 1) => x.bnBatchMeanB)))) = bnBatchTensor4 N oc h w ε γ β (den x)

                                                            THE DROP-IN, on actual graph nodes: at R = 1 the sync-BN subgraph denotes bnBatchTensor4.

                                                            The Foundation anchors say the sync forward at its own statistics is the batch forward; this says the GRAPH a sync render emits — bnSyncF fed by bnPackB of the two one-replica collectives (μ, then σ² at μ) — is that, once R = 1 collapses every collective to its single operand.

                                                            So a single-device sync render computes exactly what today's bnBatchF render computes, and the R = 1 artifacts need not move. The R > 1 case is then purely a question about how shard statistics compose (bnMean_shard / bnVar_shard_chan), with BatchNorm itself already accounted for here.

                                                            source
                                                            theorem Proofs.StableHLO.den_bnSyncBack_allReduce_R1 {N oc h w : ℕ} (gN xN es t t' t'' : String) (ds ds' ds'' : List ℕ) (ε : ℝ) (γ : Vec oc) (hm : N * (h * w) ≠ 0) (xg : SHlo (N * (oc * (h * w)))) (x : Vec (N * (oc * (h * w)))) (hx : den xg = x) (dy : SHlo (N * (oc * (h * w)))) :
                                                            den (SHlo.bnSyncBack gN xN es ε γ x dy (SHlo.allReduceMeanF 1 Nat.one_pos t'' ds'' fun (x_1 : Fin 1) => SHlo.bnSyncDyStatsB gN xN es ε γ x dy ((SHlo.allReduceMeanF 1 Nat.one_pos t ds fun (x : Fin 1) => xg.bnBatchMeanB).bnPackB (SHlo.allReduceMeanF 1 Nat.one_pos t' ds' fun (x : Fin 1) => xg.bnBatchVarAtB (SHlo.allReduceMeanF 1 Nat.one_pos t ds fun (x : Fin 1) => xg.bnBatchMeanB))))) = bnBatchTensor4GradInput N oc h w ε γ x (den dy)

                                                            THE DROP-IN, backward half: at R = 1 the sync-BN backward subgraph denotes bnBatchTensor4GradInput.

                                                            The peer of den_bnSyncF_allReduce_R1. The graph is the one a sync render emits — an outer allReduceMeanF over bnSyncDyStatsB, itself fed by the packed forward statistics — and at R = 1 every collective collapses to its single operand, leaving the committed three-term backward. hx ties the saved host activation to the graph value it came from, which is the renderer's own invariant.

                                                            source
                                                            theorem Proofs.StableHLO.den_bnSyncGammaGradB_allReduce_R1 {N oc h w : ℕ} (xN es t t' : String) (ds ds' : List ℕ) (ε : ℝ) (hm : N * (h * w) ≠ 0) (xg : SHlo (N * (oc * (h * w)))) (x : Vec (N * (oc * (h * w)))) (hx : den xg = x) (dy : SHlo (N * (oc * (h * w)))) :
                                                            den (SHlo.bnSyncGammaGradB xN es ε x dy ((SHlo.allReduceMeanF 1 Nat.one_pos t ds fun (x : Fin 1) => xg.bnBatchMeanB).bnPackB (SHlo.allReduceMeanF 1 Nat.one_pos t' ds' fun (x : Fin 1) => xg.bnBatchVarAtB (SHlo.allReduceMeanF 1 Nat.one_pos t ds fun (x : Fin 1) => xg.bnBatchMeanB)))) = den (SHlo.bnGammaGradB xN es ε x dy)

                                                            THE DROP-IN, γ half: at R = 1 the sync γ-gradient node denotes bnGammaGradB. The third anchor beside den_bnSyncF_allReduce_R1 / den_bnSyncBack_allReduce_R1: fed the collapsed collectives, the sync γ node reads the batch's own statistics and is the committed γ gradient.

                                                            source
                                                            theorem Proofs.StableHLO.den_bnStatsMeanB_allReduce_R1 {N oc h w : ℕ} (t t' : String) (ds ds' : List ℕ) (x : SHlo (N * (oc * (h * w)))) :
                                                            den ((SHlo.allReduceMeanF 1 Nat.one_pos t ds fun (x_1 : Fin 1) => x.bnBatchMeanB).bnPackB (SHlo.allReduceMeanF 1 Nat.one_pos t' ds' fun (x_1 : Fin 1) => x.bnBatchVarAtB (SHlo.allReduceMeanF 1 Nat.one_pos t ds fun (x_2 : Fin 1) => x.bnBatchMeanB))).bnStatsMeanB = den x.bnBatchMeanB

                                                            R = 1: the handed-back sync mean IS bnBatchMeanB.

                                                            source
                                                            theorem Proofs.StableHLO.den_bnStatsVarB_allReduce_R1 {N oc h w : ℕ} (t t' : String) (ds ds' : List ℕ) (x : SHlo (N * (oc * (h * w)))) :
                                                            den ((SHlo.allReduceMeanF 1 Nat.one_pos t ds fun (x_1 : Fin 1) => x.bnBatchMeanB).bnPackB (SHlo.allReduceMeanF 1 Nat.one_pos t' ds' fun (x_1 : Fin 1) => x.bnBatchVarAtB (SHlo.allReduceMeanF 1 Nat.one_pos t ds fun (x_2 : Fin 1) => x.bnBatchMeanB))).bnStatsVarB = den x.bnBatchVarB

                                                            R = 1: the handed-back sync variance IS bnBatchVarB — the batch's own two-pass variance, offset zero.

                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_maxPoolBackB {N c h w : ℕ} (xN : String) (x : Vec (N * (c * (2 * h) * (2 * w)))) (e : SHlo (N * (c * h * w))) :
                                                            den (SHlo.maxPoolBackB xN x e) = batchMapAux N (maxPoolBackFlat c h w) x (den e)
                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_maxPool3s2BackB {N c h w : ℕ} (xN : String) (x : Vec (N * (c * (2 * h) * (2 * w)))) (e : SHlo (N * (c * h * w))) :
                                                            den (SHlo.maxPool3s2BackB xN x e) = batchMapAux N (maxPool3s2BackFlat c h w) x (den e)
                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_selectPosB {N n : ℕ} (xN : String) (x : Vec (N * n)) (e : SHlo (N * n)) :
                                                            den (SHlo.selectPosB xN x e) = fun (i : Fin (N * n)) => if x i > 0 then den e i else 0
                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_selectMidB {N n : ℕ} (xN : String) (x : Vec (N * n)) (e : SHlo (N * n)) :
                                                            den (SHlo.selectMidB xN x e) = fun (i : Fin (N * n)) => if 0 < x i ∧ x i < 6 then den e i else 0
                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_dropPathB {N n : ℕ} (mN : String) (s : Vec N) (e : SHlo (N * n)) :
                                                            den (SHlo.dropPathB mN s e) = dropPath N n s (den e)
                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_dropoutB {N n : ℕ} (mN : String) (mask : Vec (N * n)) (e : SHlo (N * n)) :
                                                            den (SHlo.dropoutB mN mask e) = dropout N n mask (den e)
                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_swishBackB {N n : ℕ} (xN : String) (x : Vec (N * n)) (e : SHlo (N * n)) :
                                                            den (SHlo.swishBackB xN x e) = (swishHasVJP (N * n)).backward x (den e)
                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_geluBackB {N n : ℕ} (xN : String) (x : Vec (N * n)) (e : SHlo (N * n)) :
                                                            den (SHlo.geluBackB xN x e) = (geluHasVJP (N * n)).backward x (den e)
                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_rowDenseBiasGradB {N R c : ℕ} (e : SHlo (N * (R * c))) :
                                                            den e.rowDenseBiasGradB = fun (j : Fin c) => ∑ n : Fin N, ∑ r : Fin R, batchSlice R c (batchSlice N (R * c) (den e) n) r j
                                                            source
                                                            theorem Proofs.StableHLO.den_rowDenseBiasGradB_at_one {R c : ℕ} (e : SHlo (1 * (R * c))) (j : Fin c) :
                                                            den e.rowDenseBiasGradB j = ∑ r : Fin R, batchSlice R c (batchSlice 1 (R * c) (den e) 0) r j

                                                            The two-level contraction is real, and this is what would have been silently lost. At N = 1 the batched bias gradient collapses to its per-example peer — so a render that dropped the batch sum type-checks, emits the same bytes and agrees on a one-example batch. The gate that catches it has to run at N > 1, which is why the emit tie alone is not enough here.

                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_lnRowBackB {N m n : ℕ} (gN xN es : String) (ε γ : ℝ) (x : Vec (N * (m * n))) (e : SHlo (N * (m * n))) :
                                                            den (SHlo.lnRowBackB gN xN es ε γ x e) = batchMapAux N (rowLNBackFlat m n ε γ) x (den e)
                                                            source
                                                            theorem Proofs.StableHLO.den_lnRowBackB_per_example {N m n : ℕ} (gN xN es : String) (ε γ : ℝ) (x : Vec (N * (m * n))) (e : SHlo (N * (m * n))) (k : Fin N) (i : Fin (m * n)) :
                                                            den (SHlo.lnRowBackB gN xN es ε γ x e) (finProdFinEquiv (k, i)) = rowLNBackFlat m n ε γ (batchSlice N (m * n) x k) (batchSlice N (m * n) (den e) k) i

                                                            lnRowBackB hands each example its OWN saved activation — the property that forced it to be a constructor rather than a descriptor, stated so it can be cited instead of re-argued. Example k's output block is the per-example backward applied to batchSlice k x, never to the whole x and never to example 0's. A descriptor would give the latter, silently: same types, same emitted bytes, different function.

                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_sigmoidBackB {N n : ℕ} (xN : String) (x : Vec (N * n)) (e : SHlo (N * n)) :
                                                            den (SHlo.sigmoidBackB xN x e) = (sigmoidHasVJP (N * n)).backward x (den e)
                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.sigmoidB_faithful {N n : ℕ} (e : SHlo (N * n)) :
                                                            den e.sigmoidB = sigmoid (N * n) (den e)

                                                            sigmoidB denotes Proofs.sigmoid at the batched index — rfl, the same function sigmoidF_faithful states one index down. This is BCE-with-logits' only new op.

                                                            ViT increment 2 — the six forms that cannot be descriptors #

                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_matmulFB {N m k n : ℕ} (a : SHlo (N * (m * k))) (b : SHlo (N * (k * n))) :
                                                            den (a.matmulFB b) = batchMapAux N (matMulFlat m k n) (den a) (den b)
                                                            source
                                                            theorem Proofs.StableHLO.den_matmulFB_per_example {N m k n : ℕ} (a : SHlo (N * (m * k))) (b : SHlo (N * (k * n))) (t : Fin N) (i : Fin (m * n)) :
                                                            den (a.matmulFB b) (finProdFinEquiv (t, i)) = matMulFlat m k n (batchSlice N (m * k) (den a) t) (batchSlice N (k * n) (den b) t) i

                                                            ATTENTION'S MATMUL IS PER-EXAMPLE IN BOTH OPERANDS, which is the property the whole matmulF scoping worry was about. Example k's output is Qₖ·Kₖᵀ — its own Q against its own K — never Q₀ against Kₖ, and never the whole batch flattened into one big matrix.

                                                            All three of those type-check. At the batched index N*(m*k), a den that read the index as one matrix would compute matMulFlat at the wrong m and still be a Vec; a descriptor would hand every example operand 0's left factor. What separates them is this statement, and the emit tie cannot make it — the emitted dot_general carries batching_dims = [0] x [0] in every one of those worlds.

                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_softmaxRowBackB {N m n : ℕ} (xN : String) (preAct : Vec (N * (m * n))) (e : SHlo (N * (m * n))) :
                                                            den (SHlo.softmaxRowBackB xN preAct e) = batchMapAux N (rowSoftmaxBackFlat m n) preAct (den e)
                                                            source
                                                            theorem Proofs.StableHLO.den_softmaxRowBackB_per_example {N m n : ℕ} (xN : String) (preAct : Vec (N * (m * n))) (e : SHlo (N * (m * n))) (k : Fin N) (i : Fin (m * n)) :
                                                            den (SHlo.softmaxRowBackB xN preAct e) (finProdFinEquiv (k, i)) = rowSoftmaxBackFlat m n (batchSlice N (m * n) preAct k) (batchSlice N (m * n) (den e) k) i

                                                            Each example's softmax backward recomputes from ITS OWN saved scores. The descriptor version would hand all N example 0's — same types, same bytes, different function. lnRowBackB's statement, on attention.

                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_posEmbedGradB {N tk D : ℕ} (e : SHlo (N * ((tk + 1) * D))) :
                                                            den e.posEmbedGradB = fun (i : Fin ((tk + 1) * D)) => ∑ b : Fin N, batchSlice N ((tk + 1) * D) (den e) b i
                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_patchEmbedBiasGradB {N tk c : ℕ} (e : SHlo (N * ((tk + 1) * c))) :
                                                            den e.patchEmbedBiasGradB = fun (i : Fin c) => ∑ b : Fin N, ∑ p : Fin tk, batchSlice (tk + 1) c (batchSlice N ((tk + 1) * c) (den e) b) p.succ i
                                                            source
                                                            theorem Proofs.StableHLO.den_posEmbedGradB_at_one {tk D : ℕ} (e : SHlo (1 * ((tk + 1) * D))) (i : Fin ((tk + 1) * D)) :
                                                            den e.posEmbedGradB i = batchSlice 1 ((tk + 1) * D) (den e) 0 i

                                                            THE BATCH SUM IS INVISIBLE AT N = 1. At one example the outer ∑ b has a single term, so a render that dropped it type-checks, emits the same bytes and agrees exactly — which is why any gate on these four must run at N > 1. den_rowDenseBiasGradB_at_one says the same thing for ConvNeXt's bias gradient; this is ViT's positional embedding, where the shared parameter is the whole (tk+1) × D table.

                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_addVB {N n : ℕ} (a b : SHlo (N * n)) :
                                                            den (a.addVB b) = fun (j : Fin (N * n)) => den a j + den b j
                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_subB {N n : ℕ} (a b : SHlo (N * n)) :
                                                            den (a.subB b) = fun (j : Fin (N * n)) => den a j - den b j
                                                            source
                                                            @[simp]
                                                            theorem Proofs.StableHLO.den_bnBatchF {N oc h w : ℕ} (gN bN es : String) (ε : ℝ) (γ β : Vec oc) (e : SHlo (N * (oc * h * w))) :
                                                            den (SHlo.bnBatchF gN bN es ε γ β e) = bnBatchLA N oc h w ε γ β (den e)
                                                            source
                                                            def Proofs.StableHLO.fwdGraph {m n : ℕ} (W : Mat m n) (b : Vec n) (x : Vec m) :
                                                            SHlo n

                                                            Forward logits graph @linear_fwd: broadcast(b) + dot_general(x, W).

                                                            Equations
                                                            Instances For
                                                              source
                                                              def Proofs.StableHLO.backGraph {m n : ℕ} (W : Mat m n) (dy : Vec n) :
                                                              SHlo m

                                                              Dense input-VJP graph (@linear_back): dot_general(dy, W).

                                                              Equations
                                                              Instances For
                                                                source
                                                                def Proofs.StableHLO.lossCotGraph {m n : ℕ} (W : Mat m n) (b : Vec n) (x : Vec m) (oh : Vec n) :
                                                                SHlo n

                                                                Softmax-CE loss-cotangent graph softmax(logits) − onehot. The one-hot is a parameter (a graph input %onehot); den reads it, pretty ignores it.

                                                                Equations
                                                                Instances For
                                                                  source
                                                                  theorem Proofs.StableHLO.fwdGraph_faithful {m n : ℕ} (W : Mat m n) (b : Vec n) (x : Vec m) :
                                                                  den (fwdGraph W b x) = mnistLinear W b x

                                                                  Forward faithfulness. The forward graph denotes mnistLinear W b.

                                                                  source
                                                                  theorem Proofs.StableHLO.backGraph_faithful {m n : ℕ} (W : Mat m n) (b : Vec n) (x : Vec m) (dy : Vec n) :
                                                                  den (backGraph W dy) = (denseHasVJP W b).backward x dy

                                                                  Dense input-VJP faithfulness. The backward graph denotes the proven dense VJP backward (denseHasVJP W b).backward x = Mat.mulVec W.

                                                                  source
                                                                  theorem Proofs.StableHLO.softmaxDiv_expe_faithful {n : ℕ} (z : Vec n) :
                                                                  den (SHlo.operand "%logits" z).expe.softmaxDiv = softmax n z

                                                                  The softmax sub-graph denotes the proven softmax.

                                                                  source
                                                                  theorem Proofs.StableHLO.lossCotGraph_faithful {m n : ℕ} (W : Mat m n) (b : Vec n) (x : Vec m) (label : Fin n) :
                                                                  den (lossCotGraph W b x (oneHot n label)) = IR.emitLossCot n (mnistLinear W b x) label

                                                                  Loss-cotangent faithfulness (spec level).

                                                                  source
                                                                  theorem Proofs.StableHLO.lossCotGraph_isCEgrad {m n : ℕ} (W : Mat m n) (b : Vec n) (x : Vec m) (label j : Fin n) :
                                                                  den (lossCotGraph W b x (oneHot n label)) j = pdiv (fun (z : Vec n) (x : Fin 1) => crossEntropy n z label) (mnistLinear W b x) j 0

                                                                  Loss-cotangent faithfulness (to the proven gradient). Via IR.lossCot_bridge: the cotangent graph denotes ∂(crossEntropy)/∂logits at the linear logits.

                                                                  source
                                                                  def Proofs.StableHLO.wGrad {m n : ℕ} (x : Vec m) (dy : Vec n) :
                                                                  Mat m n

                                                                  Weight-gradient (per-example): the batch-contracting dot_general, i.e. the outer product x ⊗ dy.

                                                                  Equations
                                                                  Instances For
                                                                    source
                                                                    def Proofs.StableHLO.bGrad {n : ℕ} (dy : Vec n) :
                                                                    Vec n

                                                                    Bias-gradient (per-example): the batch reduce-add is the cotangent.

                                                                    Equations
                                                                    Instances For
                                                                      source
                                                                      theorem Proofs.StableHLO.wGrad_faithful {m n : ℕ} (x : Vec m) (dy : Vec n) :
                                                                      wGrad x dy = IR.emitWeightGrad x IR.Back.cotangent dy
                                                                      source
                                                                      theorem Proofs.StableHLO.wGrad_isWeightJacobian {m n : ℕ} (W : Mat m n) (b : Vec n) (x : Vec m) (dy : Vec n) (i : Fin m) (j : Fin n) :
                                                                      wGrad x dy i j = ∑ k : Fin n, pdiv (fun (v : Vec (m * n)) => dense (Mat.unflatten v) b x) W.flatten (finProdFinEquiv (i, j)) k * dy k

                                                                      Weight-grad faithfulness to the certified ∂/∂W Jacobian.

                                                                      source
                                                                      theorem Proofs.StableHLO.bGrad_faithful {n : ℕ} (dy : Vec n) :
                                                                      bGrad dy = IR.emitBiasGrad IR.Back.cotangent dy
                                                                      source
                                                                      theorem Proofs.StableHLO.bGrad_isBiasJacobian {m n : ℕ} (W : Mat m n) (b : Vec n) (x : Vec m) (dy : Vec n) (i : Fin n) :
                                                                      bGrad dy i = ∑ j : Fin n, pdiv (fun (b' : Vec n) => dense W b' x) b i j * dy j

                                                                      Bias-grad faithfulness to the certified ∂/∂b Jacobian.

                                                                      source
                                                                      noncomputable def Proofs.StableHLO.sgdW {m n : ℕ} (W : Mat m n) (b : Vec n) (x : Vec m) (lr : ℝ) (label : Fin n) :
                                                                      Mat m n

                                                                      The emitted weight SGD update W − lr·(x⊗dy), with dy the proven softmax-CE cotangent.

                                                                      Equations
                                                                      Instances For
                                                                        source
                                                                        noncomputable def Proofs.StableHLO.sgdB {m n : ℕ} (W : Mat m n) (b : Vec n) (x : Vec m) (lr : ℝ) (label : Fin n) :
                                                                        Vec n

                                                                        The emitted bias SGD update b − lr·dy.

                                                                        Equations
                                                                        Instances For
                                                                          source
                                                                          theorem Proofs.StableHLO.sgdW_isCertifiedGradStep {m n : ℕ} (W : Mat m n) (b : Vec n) (x : Vec m) (lr : ℝ) (label : Fin n) (i : Fin m) (j : Fin n) :
                                                                          sgdW W b x lr label i j = W i j - lr * ∑ k : Fin n, pdiv (fun (v : Vec (m * n)) => dense (Mat.unflatten v) b x) W.flatten (finProdFinEquiv (i, j)) k * den (lossCotGraph W b x (oneHot n label)) k

                                                                          SGD weight-step faithfulness. The emitted update subtracts lr times the certified ∂/∂W Jacobian contracted with the proven loss cotangent — plain-SGD optimizer promoted from trusted to proven.

                                                                          source
                                                                          theorem Proofs.StableHLO.sgdB_isCertifiedGradStep {m n : ℕ} (W : Mat m n) (b : Vec n) (x : Vec m) (lr : ℝ) (label j : Fin n) :
                                                                          sgdB W b x lr label j = b j - lr * ∑ i : Fin n, pdiv (fun (b' : Vec n) => dense W b' x) b j i * den (lossCotGraph W b x (oneHot n label)) i

                                                                          SGD bias-step faithfulness. Likewise for b.

                                                                          source
                                                                          theorem Proofs.StableHLO.reluF_faithful {k : ℕ} (e : SHlo k) :
                                                                          den e.reluF = relu k (den e)

                                                                          ReLU forward faithfulness. maximum(·,0) denotes the proven relu.

                                                                          source
                                                                          theorem Proofs.StableHLO.selectPos_faithful {k : ℕ} (s : String) (x : Vec k) (hx : ∀ (i : Fin k), x i ≠ 0) (e : SHlo k) :
                                                                          den (SHlo.selectPos s x e) = (reluHasVJPAt k x hx).backward (den e)

                                                                          ReLU backward faithfulness (smooth point). select(x>0,·,0) denotes the proven reluHasVJPAt backward — the codegen's relu'(0)=0 convention.

                                                                          source
                                                                          theorem Proofs.StableHLO.den_batchOp_relu_eq_reluF {N n : ℕ} (e : SHlo (N * n)) :
                                                                          den (SHlo.batchOp BatchableOp.relu e) = den e.reluF

                                                                          The relu descriptor denotes exactly what the descriptor-less reluF denoted at the same index: the batched graph computes the same function, only the emit width now travels separately from the batch. The ResNet-34 peer of den_batchOp_swish_eq_swishF.

                                                                          source
                                                                          theorem Proofs.StableHLO.selectPosB_faithful {N n : ℕ} (s : String) (x : Vec (N * n)) (hx : ∀ (i : Fin (N * n)), x i ≠ 0) (e : SHlo (N * n)) :
                                                                          den (SHlo.selectPosB s x e) = (reluHasVJPAt (N * n) x hx).backward (den e)

                                                                          Batched ReLU backward faithfulness. selectPosB denotes the same proven reluHasVJPAt backward as selectPos, now over the whole batch — which is what the emitted xName holds. This is the statement that would be FALSE had selectPos been made a BatchableOp descriptor (that den would apply one example's mask to all N).

                                                                          source
                                                                          @[simp]
                                                                          theorem Proofs.StableHLO.relu6F_faithful {k : ℕ} (e : SHlo k) :
                                                                          den e.relu6F = relu6 k (den e)

                                                                          ReLU6 forward faithfulness. min(max(·,0),6) denotes the proven relu6 (MLP.lean). (rfl — relu6 is defined as exactly this clamp.)

                                                                          source
                                                                          theorem Proofs.StableHLO.selectMid_faithful {k : ℕ} (s : String) (x : Vec k) (h_smooth : ∀ (i : Fin k), x i ≠ 0 ∧ x i ≠ 6) (e : SHlo k) :
                                                                          den (SHlo.selectMid s x e) = (relu6HasVJPAt k x h_smooth).backward (den e)

                                                                          ReLU6 backward faithfulness (smooth point). select(0<x<6,·,0) denotes the proven relu6HasVJPAt backward — the two-sided kink's mask, smooth iff x≠0 ∧ x≠6 (both bounds, unlike ReLU's one-sided x≠0).

                                                                          source
                                                                          theorem Proofs.StableHLO.den_batchOp_relu6_eq_relu6F {N n : ℕ} (e : SHlo (N * n)) :
                                                                          den (SHlo.batchOp BatchableOp.relu6 e) = den e.relu6F

                                                                          Batched ReLU6 forward faithfulness. The relu6 descriptor at the batched index denotes exactly relu6F's per-example clamp applied across the batch — the MobileNetV2 peer of den_batchOp_relu_eq_reluF. This is the statement that keeps the emit width off the SHlo index: at N := B the descriptor emits tensor<B×n>, not tensor<B×(N·n)>.

                                                                          source
                                                                          theorem Proofs.StableHLO.selectMidB_faithful {N n : ℕ} (s : String) (x : Vec (N * n)) (h_smooth : ∀ (i : Fin (N * n)), x i ≠ 0 ∧ x i ≠ 6) (e : SHlo (N * n)) :
                                                                          den (SHlo.selectMidB s x e) = (relu6HasVJPAt (N * n) x h_smooth).backward (den e)

                                                                          Batched ReLU6 backward faithfulness. selectMidB denotes the same proven relu6HasVJPAt backward as selectMid, now over the whole batch — which is what the emitted xName holds. FALSE had selectMid been made a BatchableOp descriptor beside relu6 (that den would apply one example's two-sided mask to all N). Note the smoothness hypothesis is TWO-sided (x ≠ 0 ∧ x ≠ 6), unlike selectPosB_faithful's x ≠ 0.

                                                                          source
                                                                          theorem Proofs.StableHLO.dropPathB_faithful {N n : ℕ} (mN : String) (s : Vec N) (e : SHlo (N * n)) :
                                                                          den (SHlo.dropPathB mN s e) = dropPath N n s (den e)

                                                                          Stochastic-depth forward faithfulness. dropPathB denotes Proofs.dropPath, the per-sample residual-branch scale. rfl, because dropPath is layerScale at a per-example-broadcast scale and this op is that multiply.

                                                                          source
                                                                          theorem Proofs.StableHLO.dropPathB_back_faithful {N n : ℕ} (mN : String) (s : Vec N) (x : Vec (N * n)) (e : SHlo (N * n)) :
                                                                          den (SHlo.dropPathB mN s e) = (dropPathHasVJP N n s).backward x (den e)

                                                                          Stochastic-depth BACKWARD faithfulness — and it is the SAME constructor. A diagonal linear map is its own transpose, so the renderer emits dropPathB on the cotangent at the same scale, and that IS the certified VJP. No *Grad peer exists to drift out of step with this one, which is the whole reason this feature costs one op rather than two.

                                                                          source
                                                                          @[simp]
                                                                          theorem Proofs.StableHLO.den_dropPathB_ones {N n : ℕ} (mN : String) (e : SHlo (N * n)) :
                                                                          den (SHlo.dropPathB mN (fun (x : Fin N) => 1) e) = den e
                                                                          source
                                                                          theorem Proofs.StableHLO.dropoutB_faithful {N n : ℕ} (mN : String) (mask : Vec (N * n)) (e : SHlo (N * n)) :
                                                                          den (SHlo.dropoutB mN mask e) = dropout N n mask (den e)

                                                                          Classifier-dropout forward faithfulness. dropoutB denotes Proofs.dropout, the per-ELEMENT inverted mask. rfl, because dropout is layerScale at a mask of the value's own type — no lift, which is what makes it cheaper than dropPathB rather than dearer.

                                                                          source
                                                                          theorem Proofs.StableHLO.dropoutB_back_faithful {N n : ℕ} (mN : String) (mask x : Vec (N * n)) (e : SHlo (N * n)) :
                                                                          den (SHlo.dropoutB mN mask e) = (dropoutHasVJP N n mask).backward x (den e)

                                                                          Classifier-dropout BACKWARD faithfulness — the SAME constructor, dropPathB_back_faithful one mask rank up. This covers the cotangent flowing THROUGH the site and nothing else; see Proofs.dropout_vjp_is_self on the classifier weight gradient, which reads the dense's input and must therefore read the DROPPED activation.

                                                                          source
                                                                          @[simp]
                                                                          theorem Proofs.StableHLO.den_dropoutB_ones {N n : ℕ} (mN : String) (e : SHlo (N * n)) :
                                                                          den (SHlo.dropoutB mN (fun (x : Fin (N * n)) => 1) e) = den e

                                                                          The ones-mask identity on the AST, which is what licenses emitting the dropout site in the FORWARD artifact: @efficientnet_do_fwd and @efficientnet_adamdo_train_step are then one graph differing only in the mask the driver supplies, and the prefix audit survives.

                                                                          source
                                                                          theorem Proofs.StableHLO.den_dropoutB_of_dropScale {N n : ℕ} (mN dN : String) (s : Vec N) (e : SHlo (N * n)) :
                                                                          den (SHlo.dropoutB mN (dropScale N n s) e) = den (SHlo.dropPathB dN s e)

                                                                          THE TWO OPS AGREE EXACTLY WHEN THE MASK IS LIFTED, AND THE AST SAYS SO. Proofs.dropout_of_dropScale at the node level: a dropoutB carrying dropScale N n s denotes what the dropPathB at s denotes. This is the substitution that would be a silent regulariser swap if it were made in the other direction on an unlifted mask, and it is stated here so that the containment is checkable rather than argued.

                                                                          source
                                                                          def Proofs.StableHLO.denseF {a c : ℕ} (wN bN : String) (W : Mat a c) (bias : Vec c) (e : SHlo a) :
                                                                          SHlo c

                                                                          A dense forward layer graph: broadcast(bias) + dot_general(·, W).

                                                                          Equations
                                                                          Instances For
                                                                            source
                                                                            theorem Proofs.StableHLO.denseF_faithful {a c : ℕ} (wN bN : String) (W : Mat a c) (bias : Vec c) (e : SHlo a) :
                                                                            den (denseF wN bN W bias e) = dense W bias (den e)
                                                                            source
                                                                            theorem Proofs.StableHLO.flatConvF_faithful {ic oc h w kH kW : ℕ} (wN bN : String) (W : Kernel4 oc ic kH kW) (b : Vec oc) (e : SHlo (ic * h * w)) :
                                                                            den (SHlo.flatConvF wN bN W b e) = flatConv W b (den e)

                                                                            Conv forward faithfulness. The (flattened) stablehlo.convolution op denotes the proven flatConv.

                                                                            source
                                                                            theorem Proofs.StableHLO.flatConvFBf16_faithful {ic oc h w kH kW : ℕ} (rnd : ℝ → ℝ) (wN bN : String) (W : Kernel4 oc ic kH kW) (b : Vec oc) (e : SHlo (ic * h * w)) :
                                                                            den (SHlo.flatConvFBf16 rnd wN bN W b e) = fun (i : Fin (oc * h * w)) => rnd (flatConv (fun (o : Fin oc) (c : Fin ic) (kh : Fin kH) (kw : Fin kW) => rnd (W o c kh kw)) 0 (fun (j : Fin (ic * h * w)) => rnd (den e j)) i) + Tensor3.flatten (fun (o : Fin oc) (x : Fin h) (x_1 : Fin w) => b o) i

                                                                            bf16 conv forward faithfulness. The bf16 stablehlo.convolution op denotes the proven flatConv on ROUNDED operands, with the accumulated sum rounded and the bias added afterwards in f32 — i.e. exactly what the emitted graph computes.

                                                                            Contrast flatConvF_faithful, which has no rounding, and dotInBf16, which rounds the operands but NOT the result. The outer rnd here is not decoration: the emit gives the convolution a bf16-typed result, so the hardware stores the accumulator rounded.

                                                                            source
                                                                            theorem Proofs.StableHLO.flatConvFBf16_id {ic oc h w kH kW : ℕ} (wN bN : String) (W : Kernel4 oc ic kH kW) (b : Vec oc) (e : SHlo (ic * h * w)) :
                                                                            den (SHlo.flatConvFBf16 id wN bN W b e) = den (SHlo.flatConvF wN bN W b e)

                                                                            The bundling is inert at the identity rounding. At rnd = id the bf16 op denotes exactly what flatConvF does. The dotInBf16_eq_dotIn_rounded analogue: it says the op adds ROUNDING and nothing else — no reassociation, no dropped bias, no moved padding. Without it, "the emit is bf16" and "the emit is the same conv" are two separate hopes.

                                                                            source
                                                                            theorem Proofs.StableHLO.maxPoolF_faithful {c h w : ℕ} (e : SHlo (c * (2 * h) * (2 * w))) :
                                                                            den e.maxPoolF = maxPoolFlat c h w (den e)

                                                                            Max-pool forward faithfulness. The (flattened) reduce_window(max) op denotes the proven maxPoolFlat.

                                                                            source
                                                                            theorem Proofs.StableHLO.maxPool3s2F_faithful {c h w : ℕ} (e : SHlo (c * (2 * h) * (2 * w))) :
                                                                            den e.maxPool3s2F = maxPool3s2Flat c h w (den e)

                                                                            3×3/s2 max-pool forward faithfulness. The (flattened) reduce_window(max) op at window 3, stride 2, symmetric padding 1 denotes the proven maxPool3s2Flat — He et al.'s stem pool.

                                                                            source
                                                                            theorem Proofs.StableHLO.convBack_faithful {ic oc h w kH kW : ℕ} (wN : String) (W : Kernel4 oc ic kH kW) (b : Vec oc) (v : Vec (ic * h * w)) (e : SHlo (oc * h * w)) :
                                                                            den (SHlo.convBack wN W b v e) = (conv2dHasVJP3 W b).toHasVJP.backward v (den e)

                                                                            Conv backward faithfulness. The reversed-kernel stablehlo.convolution (transpose+reverse+conv) denotes the proven conv input-VJP — the flattened conv2dHasVJP3 backward (conv is linear, so this is a global VJP).

                                                                            source
                                                                            theorem Proofs.StableHLO.maxPoolBack_faithful {c h w : ℕ} (xN : String) (x : Vec (c * (2 * h) * (2 * w))) (h_smooth : MaxPool2Smooth (Tensor3.unflatten x)) (e : SHlo (c * h * w)) :
                                                                            den (SHlo.maxPoolBack xN x e) = (maxPoolFlatHasVJPAt (Tensor3.unflatten x) h_smooth).backward (den e)

                                                                            Max-pool backward faithfulness (smooth point). The emitted select_and_scatter graph denotes the proven maxPoolFlatHasVJPAt backward — routing the cotangent to each window's argmax (the codegen's no-ties convention), under the MaxPool smoothness hypothesis.

                                                                            source
                                                                            theorem Proofs.StableHLO.maxPool3s2Back_faithful {c h w : ℕ} (xN : String) (x : Vec (c * (2 * h) * (2 * w))) (h_smooth : MaxPool3s2Smooth (Tensor3.unflatten x)) (e : SHlo (c * h * w)) :
                                                                            den (SHlo.maxPool3s2Back xN x e) = (maxPool3s2FlatHasVJPAt (Tensor3.unflatten x) h_smooth).backward (den e)

                                                                            3×3/s2 max-pool backward faithfulness (smooth point). The emitted select_and_scatter graph at window 3 / stride 2 / symmetric padding 1 denotes the proven maxPool3s2FlatHasVJPAt backward, under MaxPool3s2Smooth.

                                                                            The hypothesis is stated over positions, not window offsets, and that is not a stylistic difference from maxPoolBack_faithful: with overlapping windows two offsets can name one input cell (the clamped duplicate at the first window), where the values are equal by construction and smoothness must say nothing. maxPool2 has no analogue because there distinct offsets always meant distinct positions. See MaxPool3s2.lean's header.

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.bnF_faithful {n : ℕ} (gN bN es : String) (ε γ β : ℝ) (e : SHlo n) :
                                                                            den (SHlo.bnF gN bN es ε γ β e) = bnForward n ε γ β (den e)

                                                                            BN forward faithfulness. The per-example reduce/normalize/affine graph (γ·(x−μ)·istd + β, μ/var over the feature axis) denotes the proven bnForward (BatchNorm.lean).

                                                                            source
                                                                            theorem Proofs.StableHLO.addV_faithful {n : ℕ} (a b : SHlo n) :
                                                                            den (a.addV b) = fun (j : Fin n) => den a j + den b j

                                                                            Residual-add faithfulness (= den_addV). The binary stablehlo.add denotes pointwise vector addition — the fan-in of a residual/skip connection. (rfl, so kept out of the axiom audit.)

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.gapF_faithful {c h w : ℕ} (e : SHlo (c * h * w)) :
                                                                            den e.gapF = globalAvgPoolFlat c h w (den e)

                                                                            Global-average-pool faithfulness. The reduce-over-spatial / ÷h·w graph denotes the proven globalAvgPoolFlat (CNN.lean).

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.flatConvStridedF_faithful {ic oc h w kH kW : ℕ} (wN bN : String) (W : Kernel4 oc ic kH kW) (b : Vec oc) (e : SHlo (ic * (2 * h) * (2 * w))) :
                                                                            den (SHlo.flatConvStridedF wN bN W b e) = flatConvStride2 W b (den e)

                                                                            Strided-conv forward faithfulness. The window_strides=[2,2] stablehlo.convolution denotes the proven flatConvStride2 (= decimate ∘ stride-1 conv, StridedConv.lean).

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.flatConvStridedXlaF_faithful {ic oc h w kH kW : ℕ} (wN bN : String) (W : Kernel4 oc ic kH kW) (b : Vec oc) (e : SHlo (ic * (2 * h) * (2 * w))) :
                                                                            den (SHlo.flatConvStridedXlaF wN bN W b e) = flatConvStride2Xla W b (den e)

                                                                            The XLA-SAME peer's faithfulness. flatConvStride2Xla, NOT flatConvStride2 — identical types, so this rfl is the only place the distinction is recorded.

                                                                            source
                                                                            theorem Proofs.StableHLO.convStridedBack_faithful {ic oc h w kH kW : ℕ} (wN : String) (W : Kernel4 oc ic kH kW) (b : Vec oc) (v : Vec (ic * (2 * h) * (2 * w))) (e : SHlo (oc * h * w)) :
                                                                            den (SHlo.convStridedBack wN W b v e) = (flatConvStride2HasVJP W b).backward v (den e)

                                                                            Strided-conv input-VJP faithfulness. The zero-upsample (lhs_dilation)

                                                                            • reversed-kernel conv denotes the proven flatConvStride2HasVJP backward.
                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.flatConvStride4F_faithful {ic oc h w kH kW : ℕ} (wN bN : String) (W : Kernel4 oc ic kH kW) (b : Vec oc) (e : SHlo (ic * (2 * (2 * h)) * (2 * (2 * w)))) :
                                                                            den (SHlo.flatConvStride4F wN bN W b e) = flatConvStride4 W b (den e)

                                                                            Stride-4 conv forward faithfulness. The window_strides=[4,4] stablehlo.convolution (the ConvNeXt 4×4/s4 patchify stem) denotes the proven flatConvStride4 (= decimate ∘ decimate ∘ stride-1 conv, StridedConv.lean).

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.den_bnBack {n : ℕ} (gN xN es : String) (ε γ : ℝ) (x : Vec n) (e : SHlo n) :
                                                                            den (SHlo.bnBack gN xN es ε γ x e) = bnGradInput n ε γ x (den e)

                                                                            The scalar-BN backward node denotes the grad-input helper at its cotangent.

                                                                            source
                                                                            theorem Proofs.StableHLO.bnBack_faithful {n : ℕ} (gN xN es : String) (ε γ β : ℝ) (hε : 0 < ε) (x : Vec n) (e : SHlo n) (i : Fin n) :
                                                                            den (SHlo.bnBack gN xN es ε γ x e) i = ∑ j : Fin n, pdiv (bnForward n ε γ β) x i j * den e j

                                                                            BN backward faithfulness. The consolidated three-term graph denotes the proven BN input-VJP — equal to the pdiv-contracted Jacobian of bnForward (bn_input_grad_correct), under 0 < ε. β-independent (a constant shift does not enter the Jacobian).

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.bnPerChannelF_faithful {oc h w : ℕ} (gN bN es : String) (ε : ℝ) (γ β : Vec oc) (e : SHlo (oc * h * w)) :
                                                                            den (SHlo.bnPerChannelF gN bN es ε γ β e) = bnPerChannelTensor3 oc h w ε γ β (den e)

                                                                            Per-channel BN forward faithfulness. The 4-D reshape + per-channel reduce/normalize (μ/var over the spatial axes [2,3], rank-1 γ/β dims=[1]) denotes the proven bnPerChannelTensor3 (PerChannelBN.lean). (rfl: den's arm is this function by definition.)

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.weightGrad_faithful {m n : ℕ} (xN : String) (x : Vec m) (e : SHlo n) :
                                                                            den (SHlo.weightGrad xN x e) = Mat.flatten fun (i : Fin m) (j : Fin n) => x i * den e j

                                                                            Dense weight-gradient faithfulness — the outer product xᵢ·dyⱼ.

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.convWeightGrad_faithful {ic oc h w kH kW : ℕ} (xN : String) (b : Vec oc) (x : Tensor3 ic h w) (W : Kernel4 oc ic kH kW) (e : SHlo (oc * h * w)) :
                                                                            den (SHlo.convWeightGrad xN b x W e) = (conv2dWeightGradHasVJP b x).backward W.flatten (den e)

                                                                            Conv weight-gradient faithfulness — the proven conv2dWeightGrad VJP.

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.convBiasGrad_faithful {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (x : Tensor3 ic h w) (b : Vec oc) (e : SHlo (oc * h * w)) :
                                                                            den (SHlo.convBiasGrad W x b e) = (conv2dBiasGradHasVJP W x).backward b (den e)

                                                                            Conv bias-gradient faithfulness — the proven conv2dBiasGrad VJP.

                                                                            The gradient ops agree with the SGD ops they were split out of. Each says den (θSgd …) = θ − lr · den (θGrad …) coordinatewise — so un-fusing the update did not quietly change the gradient, and anything already proven about a *Sgd output transfers to θ − lr·(*Grad). All rfl: the *Grad den is literally the subterm.

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.weightSgd_eq_grad {m n : ℕ} (xN wN lrS : String) (x : Vec m) (W : Mat m n) (lr : ℝ) (e : SHlo n) (idx : Fin (m * n)) :
                                                                            den (SHlo.weightSgd xN wN lrS x W lr e) idx = W.flatten idx - lr * den (SHlo.weightGrad xN x e) idx

                                                                            The TRANSFORMER peers of the same statement — the ViT family's un-fused gradients, which the certified vit_adam_train_step render uses. Same rfl discipline.

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.rowDenseWeightSgd_eq_grad {N a c : ℕ} (xN wN lrS : String) (x : Vec (N * a)) (W : Mat a c) (lr : ℝ) (e : SHlo (N * c)) (idx : Fin (a * c)) :
                                                                            den (SHlo.rowDenseWeightSgd xN wN lrS x W lr e) idx = W.flatten idx - lr * den (SHlo.rowDenseWeightGrad xN x e) idx
                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.rowDenseBiasSgd_eq_grad {N c : ℕ} (bN lrS : String) (b : Vec c) (lr : ℝ) (e : SHlo (N * c)) (j : Fin c) :
                                                                            den (SHlo.rowDenseBiasSgd bN lrS b lr e) j = b j - lr * den e.rowDenseBiasGrad j
                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.veclnGammaSgd_eq_grad {N D : ℕ} (gN xN esS lrS : String) (ε : ℝ) (x : Vec (N * D)) (γ : Vec D) (lr : ℝ) (e : SHlo (N * D)) (k : Fin D) :
                                                                            den (SHlo.veclnGammaSgd gN xN esS lrS ε x γ lr e) k = γ k - lr * den (SHlo.veclnGammaGrad xN esS ε x e) k
                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.patchEmbedWeightSgd_eq_grad {ic H W P N D : ℕ} (wN xN lrS : String) (x : Vec (ic * H * W)) (Wp : Kernel4 D ic P P) (lr : ℝ) (e : SHlo ((N + 1) * D)) (idx : Fin (D * ic * P * P)) :
                                                                            den (SHlo.patchEmbedWeightSgd wN xN lrS x Wp lr e) idx = Wp.flatten idx - lr * den (SHlo.patchEmbedWeightGrad xN x e) idx
                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.patchEmbedBiasSgd_eq_grad {N c : ℕ} (bN lrS : String) (b : Vec c) (lr : ℝ) (e : SHlo ((N + 1) * c)) (i : Fin c) :
                                                                            den (SHlo.patchEmbedBiasSgd bN lrS b lr e) i = b i - lr * den e.patchEmbedBiasGrad i
                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.depthwiseWeightSgdB_eq_grad {N c h w kH kW : ℕ} (xN wN lrS : String) (b : Vec c) (x : Vec (N * (c * h * w))) (W : DepthwiseKernel c kH kW) (lr : ℝ) (e : SHlo (N * (c * h * w))) (idx : Fin (c * kH * kW)) :
                                                                            den (SHlo.depthwiseWeightSgdB xN wN lrS b x W lr e) idx = Tensor3.flatten W idx - lr * den (SHlo.depthwiseWeightGradB xN b x W e) idx
                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.depthwiseStridedWeightSgdB_eq_grad {N c h w kH kW : ℕ} (xN wN lrS : String) (b : Vec c) (x : Vec (N * (c * (2 * h) * (2 * w)))) (W : DepthwiseKernel c kH kW) (lr : ℝ) (e : SHlo (N * (c * h * w))) (idx : Fin (c * kH * kW)) :
                                                                            den (SHlo.depthwiseStridedWeightSgdB xN wN lrS b x W lr e) idx = Tensor3.flatten W idx - lr * den (SHlo.depthwiseStridedWeightGradB xN b x W e) idx

                                                                            The depthwise BIAS gradients (MobileNetV2) #

                                                                            MobileNetV2RenderB is AdamW-only, like ResNet34RenderB — mnv2's SGD render stays at the per-example index, so there is deliberately no fused depthwise{,Strided}BiasSgdB peer and hence no *SgdB_eq_grad statement to make. What pins these two ops instead is that den IS the shared-parameter batch sum of the proven per-example depthwise bias VJP, which is what the emitted reduce … [0, 2, 3] computes. The emit side is covered separately by the byte-PREFIX case in tests/TestBatchedEmitTie.lean against the per-example fused depthwiseBiasSgd.

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.depthwiseBiasGradB_faithful {N c h w kH kW : ℕ} (W : DepthwiseKernel c kH kW) (x : Vec (N * (c * h * w))) (b : Vec c) (e : SHlo (N * (c * h * w))) (o : Fin c) :
                                                                            den (SHlo.depthwiseBiasGradB W x b e) o = ∑ n : Fin N, (depthwiseBiasGradHasVJP W (Tensor3.unflatten (batchSlice N (c * h * w) x n))).backward b (batchSlice N (c * h * w) (den e) n) o
                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.depthwiseStridedBiasGradB_faithful {N c h w kH kW : ℕ} (W : DepthwiseKernel c kH kW) (x : Vec (N * (c * (2 * h) * (2 * w)))) (b : Vec c) (e : SHlo (N * (c * h * w))) (o : Fin c) :
                                                                            den (SHlo.depthwiseStridedBiasGradB W x b e) o = ∑ n : Fin N, (depthwiseStride2BiasGradHasVJP W (batchSlice N (c * (2 * h) * (2 * w)) x n)).backward b (batchSlice N (c * h * w) (den e) n) o

                                                                            The ConvNeXt five — same statement, the last *Sgd/*Grad pairs the kit was missing #

                                                                            den (xSgd …) = θ − lr · den (xGrad …), all rfl. Together with the emit-side byte-PREFIX checks in tests/TestBatchedEmitTie.lean this is what lets convnext_adam_train_step hand its gradients to adamWParamF instead of to the SGD tail — the fusion was the blocker, never Adam.

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.depthwiseWeightSgd_eq_grad {c h w kH kW : ℕ} (xN wN lrS : String) (b : Vec c) (x : Tensor3 c h w) (W : DepthwiseKernel c kH kW) (lr : ℝ) (e : SHlo (c * h * w)) (idx : Fin (c * kH * kW)) :
                                                                            den (SHlo.depthwiseWeightSgd xN wN lrS b x W lr e) idx = Tensor3.flatten W idx - lr * den (SHlo.depthwiseWeightGrad xN b x W e) idx
                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.depthwiseBiasSgd_eq_grad {c h w kH kW : ℕ} (bN lrS : String) (W : DepthwiseKernel c kH kW) (x : Tensor3 c h w) (b : Vec c) (lr : ℝ) (e : SHlo (c * h * w)) (o : Fin c) :
                                                                            den (SHlo.depthwiseBiasSgd bN lrS W x b lr e) o = b o - lr * den (SHlo.depthwiseBiasGrad W x b e) o
                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.lnGammaSgd_eq_grad {n : ℕ} (gN xN es lrS : String) (ε : ℝ) (x : Vec n) (γ : Vec 1) (lr : ℝ) (e : SHlo n) (c : Fin 1) :
                                                                            den (SHlo.lnGammaSgd gN xN es lrS ε x γ lr e) c = γ 0 - lr * den (SHlo.lnGammaGrad xN es ε x e) c
                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.lnBetaSgd_eq_grad {n : ℕ} (bN lrS : String) (β : Vec 1) (lr : ℝ) (e : SHlo n) (c : Fin 1) :
                                                                            den (SHlo.lnBetaSgd bN lrS β lr e) c = β 0 - lr * den e.lnBetaGrad c
                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.layerScaleChGammaSgd_eq_grad {c h w : ℕ} (gN xN lrS : String) (x : Vec (c * h * w)) (γ : Vec c) (lr : ℝ) (e : SHlo (c * h * w)) (cc : Fin c) :
                                                                            den (SHlo.layerScaleChGammaSgd gN xN lrS x γ lr e) cc = γ cc - lr * den (SHlo.layerScaleChGammaGrad xN x e) cc
                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.posEmbedSgd_eq_grad {N D : ℕ} (pN lrS : String) (pos : Mat (N + 1) D) (lr : ℝ) (e : SHlo ((N + 1) * D)) (i : Fin ((N + 1) * D)) :
                                                                            den (SHlo.posEmbedSgd pN lrS pos lr e) i = pos.flatten i - lr * den e.posEmbedGrad i
                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.biasSgd_eq_grad {n : ℕ} (bN lrS : String) (b : Vec n) (lr : ℝ) (e : SHlo n) (j : Fin n) :
                                                                            den (SHlo.biasSgd bN lrS b lr e) j = b j - lr * den e.biasGrad j
                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.convWeightSgd_eq_grad {ic oc h w kH kW : ℕ} (xN wN lrS : String) (b : Vec oc) (x : Tensor3 ic h w) (W : Kernel4 oc ic kH kW) (lr : ℝ) (e : SHlo (oc * h * w)) (idx : Fin (oc * ic * kH * kW)) :
                                                                            den (SHlo.convWeightSgd xN wN lrS b x W lr e) idx = W.flatten idx - lr * den (SHlo.convWeightGrad xN b x W e) idx
                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.convBiasSgd_eq_grad {ic oc h w kH kW : ℕ} (bN lrS : String) (W : Kernel4 oc ic kH kW) (x : Tensor3 ic h w) (b : Vec oc) (lr : ℝ) (e : SHlo (oc * h * w)) (o : Fin oc) :
                                                                            den (SHlo.convBiasSgd bN lrS W x b lr e) o = b o - lr * den (SHlo.convBiasGrad W x b e) o

                                                                            The strided + BN peers, same shape: den (xSgd …) = θ − lr · den (xGrad …), all rfl.

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.convStridedWeightSgd_eq_grad {ic oc h w kH kW : ℕ} (xN wN lrS : String) (b : Vec oc) (x : Vec (ic * (2 * h) * (2 * w))) (W : Kernel4 oc ic kH kW) (lr : ℝ) (e : SHlo (oc * h * w)) (idx : Fin (oc * ic * kH * kW)) :
                                                                            den (SHlo.convStridedWeightSgd xN wN lrS b x W lr e) idx = W.flatten idx - lr * den (SHlo.convStridedWeightGrad xN b x W e) idx
                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.convStride4WeightGrad_faithful {ic oc h w kH kW : ℕ} (xN : String) (b : Vec oc) (x : Vec (ic * (2 * (2 * h)) * (2 * (2 * w)))) (W : Kernel4 oc ic kH kW) (e : SHlo (oc * h * w)) :
                                                                            den (SHlo.convStride4WeightGrad xN b x W e) = (flatConvStride4WeightGradHasVJP b x).backward W.flatten (den e)

                                                                            Stride-4 weight-gradient faithfulness (ConvNeXt's patchify stem). den IS the proven flatConvStride4WeightGradHasVJP backward. There is no fused convStride4WeightSgd peer — nothing but ConvNeXt's stem is stride-4, and its AdamW render consumes the un-fused gradient directly — so this, not a *Sgd_eq_grad statement, is what pins the op's den.

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.convStridedBiasSgd_eq_grad {ic oc h w kH kW : ℕ} (bN lrS : String) (W : Kernel4 oc ic kH kW) (x : Vec (ic * (2 * h) * (2 * w))) (b : Vec oc) (lr : ℝ) (e : SHlo (oc * h * w)) (o : Fin oc) :
                                                                            den (SHlo.convStridedBiasSgd bN lrS W x b lr e) o = b o - lr * den (SHlo.convStridedBiasGrad W x b e) o
                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.bnGammaSgd_eq_grad {oc h w : ℕ} (gN vN es lrS : String) (ε : ℝ) (γ : Vec oc) (v : Vec (oc * h * w)) (lr : ℝ) (e : SHlo (oc * h * w)) (c : Fin oc) :
                                                                            den (SHlo.bnGammaSgd gN vN es lrS ε γ v lr e) c = γ c - lr * den (SHlo.bnGammaGrad vN es ε v e) c
                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.bnBetaSgd_eq_grad {oc h w : ℕ} (bN lrS : String) (β : Vec oc) (lr : ℝ) (e : SHlo (oc * h * w)) (c : Fin oc) :
                                                                            den (SHlo.bnBetaSgd bN lrS β lr e) c = β c - lr * den e.bnBetaGrad c

                                                                            den (xSgdB …) = θ − lr · den (xGradB …) — the BATCHED peers of the *Sgd_eq_grad set #

                                                                            All rfl, and all carrying the same content as the per-example *Sgd_eq_grad set: the fused *SgdB op IS θ − lr· applied to the un-fused gradient, so handing the gradient to AdamW instead of to the SGD tail changes nothing about what is computed. The batched AdamW renders (resnet34_adam_train_step, …) rely on this.

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.convWeightSgdB_eq_grad {N ic oc h w kH kW : ℕ} (xN wN lrS : String) (b : Vec oc) (x : Vec (N * (ic * h * w))) (W : Kernel4 oc ic kH kW) (lr : ℝ) (e : SHlo (N * (oc * h * w))) (idx : Fin (oc * ic * kH * kW)) :
                                                                            den (SHlo.convWeightSgdB xN wN lrS b x W lr e) idx = W.flatten idx - lr * den (SHlo.convWeightGradB xN b x W e) idx
                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.convStridedWeightSgdB_eq_grad {N ic oc h w kH kW : ℕ} (xN wN lrS : String) (b : Vec oc) (x : Vec (N * (ic * (2 * h) * (2 * w)))) (W : Kernel4 oc ic kH kW) (lr : ℝ) (e : SHlo (N * (oc * h * w))) (idx : Fin (oc * ic * kH * kW)) :
                                                                            den (SHlo.convStridedWeightSgdB xN wN lrS b x W lr e) idx = W.flatten idx - lr * den (SHlo.convStridedWeightGradB xN b x W e) idx
                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.convBiasSgdB_eq_grad {N ic oc h w kH kW : ℕ} (bN lrS : String) (W : Kernel4 oc ic kH kW) (x : Vec (N * (ic * h * w))) (b : Vec oc) (lr : ℝ) (e : SHlo (N * (oc * h * w))) (o : Fin oc) :
                                                                            den (SHlo.convBiasSgdB bN lrS W x b lr e) o = b o - lr * den (SHlo.convBiasGradB W x b e) o
                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.convStridedBiasSgdB_eq_grad {N ic oc h w kH kW : ℕ} (bN lrS : String) (W : Kernel4 oc ic kH kW) (x : Vec (N * (ic * (2 * h) * (2 * w)))) (b : Vec oc) (lr : ℝ) (e : SHlo (N * (oc * h * w))) (o : Fin oc) :
                                                                            den (SHlo.convStridedBiasSgdB bN lrS W x b lr e) o = b o - lr * den (SHlo.convStridedBiasGradB W x b e) o
                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.bnGammaSgdB_eq_grad {N oc h w : ℕ} (gN vN es lrS : String) (ε : ℝ) (γ : Vec oc) (v : Vec (N * (oc * (h * w)))) (lr : ℝ) (e : SHlo (N * (oc * (h * w)))) (c : Fin oc) :
                                                                            den (SHlo.bnGammaSgdB gN vN es lrS ε γ v lr e) c = γ c - lr * den (SHlo.bnGammaGradB vN es ε v e) c
                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.bnBetaSgdB_eq_grad {N oc h w : ℕ} (bN lrS : String) (β : Vec oc) (lr : ℝ) (e : SHlo (N * (oc * (h * w)))) (c : Fin oc) :
                                                                            den (SHlo.bnBetaSgdB bN lrS β lr e) c = β c - lr * den e.bnBetaGradB c
                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.denseWeightSgdB_eq_grad {N a c : ℕ} (xN wN lrS : String) (x : Vec (N * a)) (W : Mat a c) (lr : ℝ) (e : SHlo (N * c)) (idx : Fin (a * c)) :
                                                                            den (SHlo.denseWeightSgdB xN wN lrS x W lr e) idx = W.flatten idx - lr * den (SHlo.denseWeightGradB xN x e) idx
                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.denseBiasSgdB_eq_grad {N c : ℕ} (bN lrS : String) (b : Vec c) (lr : ℝ) (e : SHlo (N * c)) (j : Fin c) :
                                                                            den (SHlo.denseBiasSgdB bN lrS b lr e) j = b j - lr * den e.denseBiasGradB j
                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.adamMNextF_faithful {n : ℕ} (mN b1N ob1N : String) (ds : List ℕ) (β₁ : ℝ) (m : Vec n) (e : SHlo n) :
                                                                            den (SHlo.adamMNextF mN b1N ob1N ds β₁ m e) = adamMNext β₁ m (den e)

                                                                            AdamW first-moment faithfulness — m' = β₁·m + (1−β₁)·g, the proven adamMNext.

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.adamVNextF_faithful {n : ℕ} (vN b2N ob2N : String) (ds : List ℕ) (β₂ : ℝ) (v : Vec n) (e : SHlo n) :
                                                                            den (SHlo.adamVNextF vN b2N ob2N ds β₂ v e) = adamVNext β₂ v (den e)

                                                                            AdamW second-moment faithfulness — v' = β₂·v + (1−β₂)·g², the proven adamVNext.

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.adamWParamF_faithful {n : ℕ} (θN mN vN b1N ob1N b2N ob2N bc1N bc2N lrN epsN wdN : String) (ds : List ℕ) (β₁ β₂ ε lr wd bc₁ bc₂ : ℝ) (θ m v : Vec n) (e : SHlo n) :
                                                                            den (SHlo.adamWParamF θN mN vN b1N ob1N b2N ob2N bc1N bc2N lrN epsN wdN ds β₁ β₂ ε lr wd bc₁ bc₂ θ m v e) = adamWParam β₁ β₂ ε lr wd bc₁ bc₂ θ m v (den e)

                                                                            AdamW parameter-step faithfulness. The node's denotation is Proofs.adamWParam of the child's gradient (by definition of den), so ties stated over den can use it; the 26-op text emitTok prints for it is trusted, like every op's. Well-definedness of the √v̂ + ε denominator is Proofs.adam_denom_pos; there is deliberately no descent claim, because Adam is not a monotone descent method (AMSGrad counterexample).

                                                                            source
                                                                            theorem Proofs.StableHLO.adamW_triple_faithful {n : ℕ} (θN mN vN b1N ob1N b2N ob2N bc1N bc2N lrN epsN wdN : String) (ds : List ℕ) (β₁ β₂ ε lr wd bc₁ bc₂ : ℝ) (θ m v : Vec n) (e : SHlo n) :
                                                                            (den (SHlo.adamWParamF θN mN vN b1N ob1N b2N ob2N bc1N bc2N lrN epsN wdN ds β₁ β₂ ε lr wd bc₁ bc₂ θ m v e), den (SHlo.adamMNextF mN b1N ob1N ds β₁ m e), den (SHlo.adamVNextF vN b2N ob2N ds β₂ v e)) = adamWStep β₁ β₂ ε lr wd bc₁ bc₂ θ m v (den e)

                                                                            The rendered AdamW triple is Proofs.adamWStep. Bundles the three ops into the (θ', m', v') a train step returns per parameter — the whole optimizer, denoted.

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.sgdParamF_faithful {n : ℕ} (θN lrN : String) (ds : List ℕ) (lr : ℝ) (θ : Vec n) (e : SHlo n) :
                                                                            den (SHlo.sgdParamF θN lrN ds lr θ e) = sgdParam lr θ (den e)

                                                                            Rendered plain SGD is Proofs.sgdParam — θ − lr·g with lr a runtime arg.

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.momVNextF_faithful {n : ℕ} (vN muN : String) (ds : List ℕ) (μ : ℝ) (v : Vec n) (e : SHlo n) :
                                                                            den (SHlo.momVNextF vN muN ds μ v e) = momVNext μ v (den e)

                                                                            Rendered Nesterov velocity is Proofs.momVNext — v' = μ·v + g.

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.momParamF_faithful {n : ℕ} (θN vN muN lrN : String) (ds : List ℕ) (μ lr : ℝ) (θ v : Vec n) (e : SHlo n) :
                                                                            den (SHlo.momParamF θN vN muN lrN ds μ lr θ v e) = momParam μ lr θ v (den e)

                                                                            Rendered Nesterov update is Proofs.momParam — θ' = θ − lr·(g + μ·v').

                                                                            source
                                                                            theorem Proofs.StableHLO.mom_pair_faithful {n : ℕ} (θN vN muN lrN : String) (ds : List ℕ) (μ lr : ℝ) (θ v : Vec n) (e : SHlo n) :
                                                                            (den (SHlo.momParamF θN vN muN lrN ds μ lr θ v e), den (SHlo.momVNextF vN muN ds μ v e)) = momStep μ lr θ v (den e)

                                                                            The rendered Nesterov pair is Proofs.momStep. The momentum analogue of adamW_triple_faithful: the (θ', v') a momentum train step returns per parameter, denoted. The m slot is a passthrough and so appears nowhere here — that is the packed-[θ|m|v] signature being shared verbatim with the AdamW render, not an omission.

                                                                            source
                                                                            theorem Proofs.StableHLO.momParamF_mu_zero {n : ℕ} (θN vN muN lrN : String) (ds : List ℕ) (lr : ℝ) (θ v : Vec n) (e : SHlo n) :
                                                                            den (SHlo.momParamF θN vN muN lrN ds 0 lr θ v e) = den (SHlo.sgdParamF θN lrN ds lr θ e)

                                                                            μ = 0 makes the rendered Nesterov update the rendered SGD update. Ties the two new op families to each other at the denotation level, so the mom and sgd renders provably agree in the limit rather than merely looking similar.

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.rmsBufNextF_faithful {n : ℕ} (sqN bufN rhoN orhoN muN epsN : String) (ds : List ℕ) (ρ μ ε : ℝ) (sq buf : Vec n) (e : SHlo n) :
                                                                            den (SHlo.rmsBufNextF sqN bufN rhoN orhoN muN epsN ds ρ μ ε sq buf e) = rmsBufNext ρ μ ε sq buf (den e)

                                                                            Rendered RMSProp buffer is Proofs.rmsBufNext — b' = μ·b + g/√(ρ·s + (1−ρ)·g² + ε), TensorFlow's ε placement.

                                                                            source
                                                                            theorem Proofs.StableHLO.rmsProp_triple_faithful {n : ℕ} (θN sqN bufN rhoN orhoN muN epsN lrN : String) (ds : List ℕ) (ρ μ ε lr : ℝ) (θ sq buf : Vec n) (e : SHlo n) (b' : Vec n) (hb : b' = rmsBufNext ρ μ ε sq buf (den e)) :
                                                                            (den (SHlo.sgdParamF θN lrN ds lr θ (SHlo.operand "%buf" b')), den (SHlo.rmsBufNextF sqN bufN rhoN orhoN muN epsN ds ρ μ ε sq buf e), den (SHlo.adamVNextF sqN rhoN orhoN ds ρ sq e)) = rmsPropStep ρ μ ε lr θ sq buf (den e)

                                                                            The rendered RMSProp triple is Proofs.rmsPropStep. The RMSProp analogue of adamW_triple_faithful / mom_pair_faithful: (θ', b', s') as the three ops the render actually emits, denoted together.

                                                                            Read the composition off this statement — it is the whole "one new op" claim, checked: the parameter slot is sgdParamF applied to this op's SSA output (.operand, so the buffer is emitted once and threaded, since pretty has no CSE), and the mean-square slot is the EXISTING adamVNextF at β₂ := ρ. Only rmsBufNextF is new.

                                                                            source
                                                                            theorem Proofs.StableHLO.adamVNextF_as_rmsSqNext {n : ℕ} (sqN rhoN orhoN : String) (ds : List ℕ) (ρ : ℝ) (sq : Vec n) (e : SHlo n) :
                                                                            den (SHlo.adamVNextF sqN rhoN orhoN ds ρ sq e) = rmsSqNext ρ sq (den e)

                                                                            The mean-square slot really is the Adam op. adamVNextF at β₂ := ρ denotes RMSProp's s', so reusing it is licensed rather than assumed — the emit-side twin of Proofs.rmsSqNext_eq_adamVNext, and the reason this optimizer cost ONE op and not three.

                                                                            source
                                                                            theorem Proofs.StableHLO.rmsBufNextF_mu_zero {n : ℕ} (sqN bufN rhoN orhoN muN epsN : String) (ds : List ℕ) (ρ ε : ℝ) (sq buf : Vec n) (e : SHlo n) :
                                                                            den (SHlo.rmsBufNextF sqN bufN rhoN orhoN muN epsN ds ρ 0 ε sq buf e) = fun (i : Fin n) => den e i / √(rmsSqNext ρ sq (den e) i + ε)

                                                                            μ = 0 makes the rendered RMSProp buffer the bare normalised gradient. The mu_zero bridge momParamF_mu_zero provides for Nesterov, at the denotation level.

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.gradSumSqAccF_faithful {n : ℕ} (ds : List ℕ) (acc : SHlo 1) (e : SHlo n) :
                                                                            den (SHlo.gradSumSqAccF ds acc e) = fun (x : Fin 1) => scalarOf (den acc) + gradSumSq (den e)

                                                                            The scalar fold is Proofs.gradSumSq accumulated — acc + ∑ᵢ gᵢ² for one parameter, reduced to a rank-0 scalar. SHlo 1 denoting a rank-0 tensor<f32> is lnBetaGrad's established reading, not a new convention.

                                                                            This op is what makes the global reduction an ordinary SHlo TREE. The norm reads like a shared DAG node — one scalar consumed by 200 sites — and SHlo is a tree; the resolution is that SHlo is single-OUTPUT, not single-INPUT, so folding 200 subtrees into one scalar is just a left-nested chain of this constructor, seeded at %zero. Nothing is recomputed, because every gradient it consumes is already an .operand leaf.

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.lambDirF_faithful {n : ℕ} (θN mN vN b1N ob1N b2N ob2N bc1N bc2N epsN wdN : String) (ds : List ℕ) (β₁ β₂ ε wd bc₁ bc₂ : ℝ) (θ m v : Vec n) (e : SHlo n) :
                                                                            den (SHlo.lambDirF θN mN vN b1N ob1N b2N ob2N bc1N bc2N epsN wdN ds β₁ β₂ ε wd bc₁ bc₂ θ m v e) = lambDir β₁ β₂ ε wd bc₁ bc₂ θ m v (den e)

                                                                            lambDirF denotes Proofs.lambDir — rfl, i.e. the rendered LAMB direction IS the ℝ definition, structurally. Same bar as adamWParamF_faithful.

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.lambScaleF_faithful {n : ℕ} (ds : List ℕ) (s : SHlo 1) (e : SHlo n) :
                                                                            den (SHlo.lambScaleF ds s e) = lambScale (scalarOf (den s)) (den e)

                                                                            lambScaleF denotes Proofs.lambScale. The trust ratio is computed from THIS tensor's own norm, which is what makes it layer-wise; clipScaleF's factor is shared across every parameter. The two ops look alike and differ in exactly that quantifier.

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.clipScaleF_faithful {n : ℕ} (clipS epsS : String) (c ε : ℝ) (ds : List ℕ) (s : SHlo 1) (e : SHlo n) :
                                                                            den (SHlo.clipScaleF clipS epsS c ε ds s e) = clipScale (clipFactor c ε (scalarOf (den s))) (den e)

                                                                            The rescale is Proofs.clipScale at Proofs.clipFactor of the summed total — the reference's g * jnp.minimum(1.0, CLIP / (gn + 1e-6)) with gn = sqrt(total).

                                                                            The factor is derived from the op's FIRST CHILD, the already-summed global total, so this constructor cannot express a per-parameter clip: it never receives enough to compute one. The c/ε ℝ fields pair with clipStr/epsStr exactly as bnF's ε/epsStr do. The factor is recomputed at every site rather than emitted once and threaded, for adamWParamF's reason — SHlo is single-result, so each output is its own node, and XLA's CSE folds the duplicates.

                                                                            source
                                                                            theorem Proofs.StableHLO.clipGrad_faithful {n m : ℕ} (dsN dsM : List ℕ) (clipS epsS : String) (c ε : ℝ) (gN : SHlo n) (gM : SHlo m) :
                                                                            den (SHlo.clipScaleF clipS epsS c ε dsN (SHlo.gradSumSqAccF dsM (SHlo.gradSumSqAccF dsN (SHlo.operand "%zero" fun (x : Fin 1) => 0) gN) gM) gN) = clipGrad c ε (0 + gradSumSq (den gN) + gradSumSq (den gM)) (den gN)

                                                                            THE WHOLE CLIP, END TO END, FOR TWO PARAMETERS — this is the transcription check.

                                                                            Read the reference's two lines off the right-hand side: gn = √(Σ_leaves Σ g²) folded from %zero, then g * min(1, CLIP/(gn + 1e-6)). Stated at TWO parameters because one cannot exhibit the property that matters — see clipShared_faithful. Holds by rfl.

                                                                            source
                                                                            theorem Proofs.StableHLO.clipShared_faithful {n m : ℕ} (dsN dsM : List ℕ) (clipS epsS : String) (c ε : ℝ) (s : SHlo 1) (gN : SHlo n) (gM : SHlo m) (i : Fin n) (j : Fin m) :
                                                                            den (SHlo.clipScaleF clipS epsS c ε dsN s gN) i * den gM j = den (SHlo.clipScaleF clipS epsS c ε dsM s gM) j * den gN i

                                                                            THE FACTOR IS SHARED ACROSS PARAMETERS — the statement the numeric gate drives.

                                                                            Two parameters clipped off the SAME total (and the same c/ε) satisfy g'₁ᵢ · g₂ⱼ = g'₂ⱼ · g₁ᵢ, i.e. the ratio g'/g is one constant across every coordinate of every parameter.

                                                                            This is the ONLY property that separates the reference from a per-parameter clip. A per-parameter clip scales, never amplifies, and is the identity below the threshold — it satisfies everything else in GradClip.lean. It differs here and nowhere else, which is why clip-tie measures the ratio's CONSTANCY across all 200/180 parameters instead of checking that any one parameter got smaller (wdx-tie's gate the partition, not the count).

                                                                            source
                                                                            theorem Proofs.StableHLO.clipScaleF_id_below {n : ℕ} (clipS epsS : String) (c ε : ℝ) (ds : List ℕ) (s : SHlo 1) (e : SHlo n) (hε : 0 < ε) (h : √(scalarOf (den s)) + ε ≤ c) :
                                                                            den (SHlo.clipScaleF clipS epsS c ε ds s e) = den e

                                                                            Below the threshold the rendered clip is the EXACT identity, so a clip-on render at a large c must agree with the clip-off render on every byte (x * 1.0 is exact in binary32). The emit-side reading of Proofs.clipGrad_id_below, and the licence for clip-tie's gate 3. It is also why gate 3 alone is not evidence: at factor 1 a per-parameter clip and a global one are the SAME FUNCTION, so an identity gate cannot see which was rendered.

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.bnPerChannelEvalF_faithful {oc h w : ℕ} (gN bN muN varN es : String) (ε : ℝ) (γ β μ var : Vec oc) (e : SHlo (oc * h * w)) :
                                                                            den (SHlo.bnPerChannelEvalF gN bN muN varN es ε γ β μ var e) = bnPerChannelEvalTensor3 oc h w ε γ β μ var (den e)

                                                                            Inference per-channel BN forward faithfulness. The 4-D reshape + affine γ·(x−μ)·rsqrt(var+ε)+β with rank-1 μ/var/γ/β (dims=[1]) denotes the proven bnPerChannelEvalTensor3 (PerChannelBN.lean). (rfl, so kept out of the axiom audit.)

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.den_bnPerChannelBack {oc h w : ℕ} (gN xN es : String) (ε : ℝ) (γ : Vec oc) (x : Vec (oc * h * w)) (e : SHlo (oc * h * w)) :
                                                                            den (SHlo.bnPerChannelBack gN xN es ε γ x e) = bnPerChannelTensor3GradInput oc h w ε γ x (den e)

                                                                            The per-channel BN backward node denotes the per-channel grad-input helper at its cotangent.

                                                                            source
                                                                            theorem Proofs.StableHLO.bnPerChannelBack_faithful {oc h w : ℕ} (gN xN es : String) (ε : ℝ) (hε : 0 < ε) (γ β : Vec oc) (x : Vec (oc * h * w)) (e : SHlo (oc * h * w)) (i : Fin (oc * h * w)) :
                                                                            den (SHlo.bnPerChannelBack gN xN es ε γ x e) i = ∑ j : Fin (oc * h * w), pdiv (bnPerChannelTensor3 oc h w ε γ β) x i j * den e j

                                                                            Per-channel BN backward faithfulness. The block-diagonal three-term graph (per-channel, reducing over the spatial axes) denotes the proven per-channel BN input-VJP — equal to the pdiv-contracted (block-diagonal) Jacobian of bnPerChannelTensor3 (bnPerChannelTensor3GradInput_correct), under 0 < ε.

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.depthwiseF_faithful {c h w kH kW : ℕ} (wN bN : String) (W : DepthwiseKernel c kH kW) (b : Vec c) (e : SHlo (c * h * w)) :
                                                                            den (SHlo.depthwiseF wN bN W b e) = depthwiseFlat W b (den e)

                                                                            Depthwise-conv forward faithfulness. The feature_group_count = c stablehlo.convolution (with a [c,1,kH,kW] kernel, one filter per channel) denotes the proven depthwiseFlat (= flatten ∘ depthwiseConv2d ∘ unflatten, Depthwise.lean). (rfl: den's arm is this function by definition.)

                                                                            source
                                                                            theorem Proofs.StableHLO.depthwiseBack_faithful {c h w kH kW : ℕ} (wN : String) (W : DepthwiseKernel c kH kW) (b : Vec c) (v : Vec (c * h * w)) (e : SHlo (c * h * w)) :
                                                                            den (SHlo.depthwiseBack wN W b v e) = (depthwiseFlatHasVJP W b).backward v (den e)

                                                                            Depthwise-conv input-VJP faithfulness. The reversed-kernel depthwise stablehlo.convolution (reverse the per-channel filters over the spatial axes [2,3]; the channel groups are 1×1 so no o↔i transpose, same feature_group_count = c) denotes the proven depthwiseFlatHasVJP backward (depthwise is linear, so this is a global VJP).

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.depthwiseStridedF_faithful {c h w kH kW : ℕ} (wN bN : String) (W : DepthwiseKernel c kH kW) (b : Vec c) (e : SHlo (c * (2 * h) * (2 * w))) :
                                                                            den (SHlo.depthwiseStridedF wN bN W b e) = depthwiseStride2Flat W b (den e)

                                                                            Strided-depthwise forward faithfulness. The window_strides=[2,2], feature_group_count = c stablehlo.convolution denotes the proven depthwiseStride2Flat (= decimate ∘ stride-1 depthwise, Depthwise.lean).

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.depthwiseStridedXlaF_faithful {c h w kH kW : ℕ} (wN bN : String) (W : DepthwiseKernel c kH kW) (b : Vec c) (e : SHlo (c * (2 * h) * (2 * w))) :
                                                                            den (SHlo.depthwiseStridedXlaF wN bN W b e) = depthwiseStride2FlatXla W b (den e)
                                                                            source
                                                                            theorem Proofs.StableHLO.depthwiseStridedBack_faithful {c h w kH kW : ℕ} (wN : String) (W : DepthwiseKernel c kH kW) (b : Vec c) (v : Vec (c * (2 * h) * (2 * w))) (e : SHlo (c * h * w)) :
                                                                            den (SHlo.depthwiseStridedBack wN W b v e) = (depthwiseStride2FlatHasVJP W b).backward v (den e)

                                                                            Strided-depthwise input-VJP faithfulness. The zero-upsample (stablehlo.pad interior=1) + reversed-kernel stride-1 depthwise denotes the proven depthwiseStride2FlatHasVJP backward.

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.swishF_faithful {n : ℕ} (e : SHlo n) :
                                                                            den e.swishF = swish n (den e)

                                                                            Swish forward faithfulness. The multiply(x, logistic(x)) graph denotes the proven swish (= x · σ(x), LayerNorm.lean). Smooth everywhere; no kink, no smoothness hypothesis. (rfl: den's arm is this function by definition.)

                                                                            source
                                                                            theorem Proofs.StableHLO.swishBack_faithful {n : ℕ} (xN : String) (x : Vec n) (e : SHlo n) :
                                                                            den (SHlo.swishBack xN x e) = (swishHasVJP n).backward x (den e)

                                                                            Swish input-VJP faithfulness. The closed-form dy ⊙ σ(x)·(1 + x·(1−σ(x))) graph (recomputing σ from the saved pre-activation x) denotes the proven GLOBAL swishHasVJP backward (dy ⊙ swishScalarDeriv x; swish is smooth everywhere, so this is a global VJP — no smoothness hypothesis).

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.sigmoidF_faithful {n : ℕ} (e : SHlo n) :
                                                                            den e.sigmoidF = sigmoid n (den e)

                                                                            Sigmoid forward faithfulness. The stablehlo.logistic(x) graph denotes the proven sigmoid (= σ(x), SE.lean) — the SE gate's output nonlinearity. Smooth everywhere. (rfl: den's arm is this function by definition.)

                                                                            source
                                                                            theorem Proofs.StableHLO.sigmoidBack_faithful {n : ℕ} (xN : String) (x : Vec n) (e : SHlo n) :
                                                                            den (SHlo.sigmoidBack xN x e) = (sigmoidHasVJP n).backward x (den e)

                                                                            Sigmoid input-VJP faithfulness. The closed-form dy ⊙ σ(x)·(1−σ(x)) graph (recomputing σ from the saved pre-activation x) denotes the proven GLOBAL sigmoidHasVJP backward (dy ⊙ sigmoidScalarDeriv x; sigmoid is smooth everywhere, so this is a global VJP — no smoothness hypothesis).

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.geluF_faithful {n : ℕ} (e : SHlo n) :
                                                                            den e.geluF = gelu n (den e)

                                                                            GELU forward faithfulness. The tanh-approximation graph 0.5·x·(1 + tanh(√(2/π)·(x + 0.044715·x³))) denotes the proven gelu (LayerNorm.lean). Smooth everywhere; no kink, no smoothness hypothesis. (rfl: den's arm is this function by definition.)

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.layerScaleF_faithful {n : ℕ} (γN : String) (γ : Vec n) (e : SHlo n) :
                                                                            den (SHlo.layerScaleF γN γ e) = layerScale γ (den e)

                                                                            Layer-scale faithfulness. The per-element multiply γ ⊙ x denotes the proven layerScale (LayerNorm.lean). (rfl.)

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.layerScaleChF_faithful {c h w : ℕ} (γN : String) (γ : Vec c) (e : SHlo (c * h * w)) :
                                                                            den (SHlo.layerScaleChF γN γ e) = layerScale (fun (k : Fin (c * h * w)) => γ (chanIdx c h w k)) (den e)

                                                                            Per-channel layer-scale faithfulness. The [c]-broadcast multiply denotes the proven layerScale at the channel-expanded vector. (rfl.)

                                                                            source
                                                                            theorem Proofs.StableHLO.geluBack_faithful {n : ℕ} (xN : String) (x : Vec n) (e : SHlo n) :
                                                                            den (SHlo.geluBack xN x e) = (geluHasVJP n).backward x (den e)

                                                                            GELU input-VJP faithfulness. The closed-form dy ⊙ gelu'(x) graph (recomputing tanh(u(x)) from the saved pre-activation x) denotes the proven GLOBAL geluHasVJP backward (dy ⊙ geluScalarDeriv x; GELU is smooth everywhere, so this is a global VJP — no smoothness hypothesis).

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.softmaxRowF_faithful {m n : ℕ} (e : SHlo (m * n)) :
                                                                            den e.softmaxRowF = rowSoftmaxFlat m n (den e)

                                                                            Row-softmax forward faithfulness. The per-row exp / reduce[last] / divide graph denotes rowSoftmaxFlat (= flattened rowSoftmax, Attention.lean). Plain exp/sum, no max-shift (matches the proven softmax). Smooth everywhere. (rfl: den's arm is this function by definition.)

                                                                            source
                                                                            theorem Proofs.StableHLO.softmaxRowBack_faithful {m n : ℕ} (xN : String) (preAct : Vec (m * n)) (e : SHlo (m * n)) :
                                                                            den (SHlo.softmaxRowBack xN preAct e) = rowSoftmaxBackFlat m n preAct (den e)

                                                                            Row-softmax input-VJP faithfulness. The per-row closed-form p ⊙ (dy − ⟨p,dy⟩) graph (recomputing p from the saved pre-softmax scores) denotes rowSoftmaxBackFlat (= flattened rowSoftmaxHasVJPMat.backward). Softmax is smooth, so this is a global VJP — no smoothness hypothesis.

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.matmulF_faithful {m k n : ℕ} (a : SHlo (m * k)) (b : SHlo (k * n)) :
                                                                            den (a.matmulF b) = matMulFlat m k n (den a) (den b)

                                                                            Matrix-multiply faithfulness. The reshape + batching-dim-0 dot_general (contracting [2] x [1]) + reshape graph denotes matMulFlat (= the flattened Mat.mul). Bilinear; the attention backwards reuse this token (dA = dC·Bᵀ, dB = Aᵀ·dC). (rfl: den's arm is this function by definition.)

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.transposeF_faithful {m n : ℕ} (e : SHlo (m * n)) :
                                                                            den e.transposeF = transposeFlat m n (den e)

                                                                            Transpose faithfulness. stablehlo.transpose dims=[0,2,1] (after reshape to rank 3) denotes transposeFlat (= the flattened Mat.transpose). (rfl.)

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.scaleF_faithful {n : ℕ} (sN : String) (s : ℝ) (e : SHlo n) :
                                                                            den (SHlo.scaleF sN s e) = fun (i : Fin n) => s * den e i

                                                                            Scalar-scale faithfulness. The splat-constant stablehlo.multiply denotes pointwise s · x — SDPA's 1/√d. (rfl; the sStr ↔ s literal agreement is the audited lexical boundary, like bnF's epsStr.)

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.lnRowF_faithful {m n : ℕ} (gN bN es : String) (ε γ β : ℝ) (e : SHlo (m * n)) :
                                                                            den (SHlo.lnRowF gN bN es ε γ β e) = rowLNFlat m n ε γ β (den e)

                                                                            Row-LayerNorm forward faithfulness. The rank-3 reduce[2]/normalize/affine graph (per token row, scalar γ/β) denotes rowLNFlat (rowwise bnForward = rowwise layerNormForward, definitionally). (rfl.)

                                                                            source
                                                                            theorem Proofs.StableHLO.lnRowBack_faithful {m n : ℕ} (gN xN es : String) (ε γ : ℝ) (x : Vec (m * n)) (e : SHlo (m * n)) :
                                                                            den (SHlo.lnRowBack gN xN es ε γ x e) = rowLNBackFlat m n ε γ x (den e)

                                                                            Row-LayerNorm input-VJP faithfulness. The per-row consolidated three-term graph (recomputing x̂/istd from the saved pre-LN input, reductions over the row axis) denotes rowLNBackFlat (rowwise bnGradInput — faithful to the pdiv-Jacobian per row under 0 < ε, bn_input_grad_correct).

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.denseRowF_faithful {N a c : ℕ} (wN bN : String) (W : Mat a c) (b : Vec c) (e : SHlo (N * a)) :
                                                                            den (SHlo.denseRowF wN bN W b e) = rowDenseFlat N a c W b (den e)

                                                                            Per-token dense forward faithfulness. The dot_general [2] x [0] + bias broadcast dims=[2] graph denotes rowDenseFlat (rowwise dense W b). (rfl.)

                                                                            source
                                                                            theorem Proofs.StableHLO.denseRowBack_faithful {N a c : ℕ} (wN : String) (W : Mat a c) (e : SHlo (N * c)) :
                                                                            den (SHlo.denseRowBack wN W e) = rowDenseBackFlat N a c W (den e)

                                                                            Per-token dense input-VJP faithfulness. The dot_general [2] x [1] graph (dy against W's output axis) denotes rowDenseBackFlat (rowwise Mat.mulVec W = the proven denseHasVJP backward; dense is affine — global VJP).

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.patchEmbedF_faithful {ic H W P N D : ℕ} (wN bN cN pN : String) (Wc : Kernel4 D ic P P) (bc cls : Vec D) (pos : Mat (N + 1) D) (e : SHlo (ic * H * W)) :
                                                                            den (SHlo.patchEmbedF wN bN cN pN Wc bc cls pos e) = patchEmbedFlat ic H W P N D Wc bc cls pos (den e)

                                                                            Patch-embedding faithfulness. The stride-P VALID conv + channels-last flatten + CLS concatenate + position-embed add graph denotes patchEmbedFlat (the local re-spelling of the proven patchEmbedFlat; the tie is rfl in ViTFwdGraph). (rfl, coarse-token like seBlock.)

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.clsSliceF_faithful {N D : ℕ} (e : SHlo ((N + 1) * D)) :
                                                                            den e.clsSliceF = clsSliceFlat N D (den e)

                                                                            CLS-slice faithfulness. The row-0 stablehlo.slice denotes clsSliceFlat (= the proven clsTokenFlat). (rfl.)

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.clsPadF_faithful {N D : ℕ} (e : SHlo D) :
                                                                            den e.clsPadF = clsPadFlat N D (den e)

                                                                            CLS-pad faithfulness. The zero-pad scatter-to-row-0 denotes clsPadFlat (= the proven clsTokenFlatHasVJP.backward; linear — global VJP). (rfl.)

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.headSliceF_faithful {N heads d : ℕ} (h : Fin heads) (e : SHlo (N * (heads * d))) :
                                                                            den (SHlo.headSliceF h e) = headSliceFlat N heads d h (den e)

                                                                            Per-head slice faithfulness. The feature-axis stablehlo.slice of head h's contiguous column block denotes headSliceFlat (= mhsaLayer's per-head column gather). Linear reindex. (rfl.)

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.headPadF_faithful {N heads d : ℕ} (h : Fin heads) (e : SHlo (N * d)) :
                                                                            den (SHlo.headPadF h e) = headPadFlat N heads d h (den e)

                                                                            Per-head pad faithfulness. The feature-axis zero-pad into head h's column block denotes headPadFlat (the slice's VJP; summed over heads it is mhsaLayer's concat). Linear. (rfl.)

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.rowScaleF_faithful {m n : ℕ} (gN : String) (γ : Vec n) (e : SHlo (m * n)) :
                                                                            den (SHlo.rowScaleF gN γ e) = rowScaleFlat m n γ (den e)

                                                                            Row-broadcast scale faithfulness. The reshape + broadcast-γ-over-rows + multiply graph denotes rowScaleFlat (rowwise layerScale γ). Diagonal-linear — its own input-VJP, so the backward reuses this token on the cotangent. (rfl.)

                                                                            source
                                                                            @[simp]
                                                                            theorem Proofs.StableHLO.rowBiasF_faithful {m n : ℕ} (bN : String) (β : Vec n) (e : SHlo (m * n)) :
                                                                            den (SHlo.rowBiasF bN β e) = rowBiasFlat m n β (den e)

                                                                            Row-broadcast bias faithfulness. The broadcast-β-over-rows + add graph denotes rowBiasFlat. Translation — identity input-VJP. (rfl.)

                                                                            source
                                                                            def Proofs.StableHLO.biasName (convBias : Bool) (nm : String) (c : ℕ) :
                                                                            String

                                                                            The conv-bias SSA name. Every conv in ResNet-34 is immediately followed by BatchNorm, and BN subtracts the batch mean, so in ℝ a conv bias cannot reach the BN output and its gradient is identically zero. He et al.'s .convBn therefore carries no conv bias, and this repo's render did — 8,512 parameters the reference does not have.

                                                                            With convBias := false the bias operand becomes a zero CONSTANT rather than a function argument: the op is the same proven flatConvF/flatConvStridedF at bias = 0, so den and every faithfulness theorem are untouched, and x + 0.0 is exact in IEEE, so the forward is bit-identical to the biased render fed zeros. What changes is the signature.

                                                                            In f32 the gradient is NOT exactly zero — the BN mean is a rounded sum, leaving a residue of the conv-weight gradient — and under AdamW's scale-free update that residue still moves θ. The biases are safe to drop because the FORWARD does not depend on them, not because they stay zero. See tests/TestConvBiasZero.lean.

                                                                            Equations
                                                                            Instances For