Documentation

LeanMlir.Proofs.Codegen.StableHLO

R4 — printer faithfulness, Stage A (Chapter 1: the linear classifier) #

The seed of planning/archive/validated_codegen_book.md's Proofs/Hlo/{Syntax,Denote}.

IR.lean gives the backward/forward IR a denotation in ℝ and proves it equals the Mathlib-fderiv math. The remaining trusted link — R4 — is that the StableHLO text the printer emits means the same function. This file closes R4 for Chapter 1, both halves, over a single typed AST SHlo:

All together (the R4 chain for ch 1): render text = pretty (emit g) (syntactic, by construction); den (emit g) = Mathlib fderiv (semantic, the theorems below).

Scope / residue. Per-example semantics (Vec/Mat): the batch axis is an outer map, a printer concern (the doc's "D1 shortcut"). pretty's lexical conformance to the StableHLO spec is the audited/validated residue (the doc's "4b": cross-checked by iree-compile + execution — the verified-rendered train step trains MNIST to ~92%), not a verified parse round-trip ("4a"). Everything here closes under [propext, Classical.choice, Quot.sound] (tests/AuditAxioms.lean).

source
noncomputable def Proofs.StableHLO.batchMap (N : ℕ) {a b : ℕ} (f : Vec a → Vec b) :
Vec (N * a) → Vec (N * b)

Per-example block-apply. Lift a per-example map f : Vec a → Vec b to a batch of N examples laid out row-major [N, a] ↦ [N, b] (the network's [N,C,H,W]-style flattening): example n occupies the finProdFinEquiv block {(n, ·)}. Every spatial/channel op in EfficientNet is batch-separable and lifts this way; only true batch-norm (bnBatchTensor4) couples the batch.

Equations
Instances For
    source
    def Proofs.StableHLO.batchSlice (N a : ℕ) (v : Vec (N * a)) (n : Fin N) :
    Vec a

    The n-th example's slice of a batch laid out row-major [N, a]. A shared weight's batched gradient is the sum over n of the per-example gradient on batchSlice n — the form the batched param-SGD dens take (so the §1 fold closes via the per-example cert + sum-linearity).

    Equations
    Instances For
      source
      theorem Proofs.StableHLO.batchSlice_batchMap {N a b : ℕ} (f : Vec a → Vec b) (x : Vec (N * a)) (n : Fin N) :
      batchSlice N b (batchMap N f x) n = f (batchSlice N a x n)

      batchSlice of a batchMap is the lifted function at the slice — the lemma that peels a per-example lift back off at one example.

      source
      noncomputable def Proofs.StableHLO.batchMapAux (N : ℕ) {s a b : ℕ} (f : Vec s → Vec a → Vec b) (aux : Vec (N * s)) :
      Vec (N * a) → Vec (N * b)

      Per-example block-apply with per-example AUXILIARY data. batchMap lifts one fixed function across the batch; this lifts a family indexed by each example's own saved value — example n is handed batchSlice n aux, not the whole aux and not example 0's.

      Every batched backward that recomputes from a saved forward activation has this shape, and that is exactly why such ops cannot be BatchableOp descriptors: a descriptor's batchMap N (denOp op) would apply ONE example's saved value to all N. Cf. swishBackB, sigmoidBackB, selectPosB (pointwise, so they take the whole-batch x directly) and seBackBatched (which inlines this shape).

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        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. An earlier note here said swish/sigmoid/relu/addV "need no descriptor — the existing tokens already denote them block-diagonally at the batched index N·(c·h·w)". The denotation half of that is true and the emit half is false, and the difference is what pinned the batched renderers at N := 1. 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 maxPool3s2_has_vjp_at3.backward lifted through hasVJPAt3_to_hasVJPAt. 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); spelled with MLP's softmax so StableHLO needn't import Attention (the tie to rowSoftmax is an rfl faithfulness lemma in TestSoftmaxRow).

                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 ∘ rowSoftmax_has_vjp_mat.backward (Mat.unflatten preAct) ∘ Mat.unflatten (since softmax_has_vjp.backward z dy i = let p := softmax z; p i·(dy i − ⟨p,dy⟩)); spelled with MLP's softmax to keep Attention out of StableHLO's imports.

                  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 bn_grad_input, 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 (= (dense_has_vjp W b).backward's Mat.mulVec W, MLP.lean).

                              Equations
                              Instances For
                                source
                                noncomputable def Proofs.StableHLO.patchEmbedFlat (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 (flattened) — a LOCAL re-spelling of the proven patchEmbed_flat (Attention.lean), kept here so StableHLO needn't import Attention (the tie is an rfl lemma in ViTFwdGraph). Output row n: CLS token at n = 0, else conv-projection of patch n−1 + bias; plus the position embedding everywhere.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  source
                                  noncomputable def 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) — a LOCAL re-spelling of the proven patchEmbed_input_grad_formula (Attention.lean), kept here so StableHLO needn't import Attention (the tie is an rfl lemma in ViTBackB0). The closed-form image cotangent: a sum over patches p : Fin N with reconstructed kernel offsets (kh, kw) matching the decoded input position (c, hh, ww). The CLS row (n = 0) and the position-add (a +constant, input-VJP = id) contribute nothing — idx_in only flows through the conv-projection branch (n = p+1), so this is purely the strided 16×16 patchify conv's input-VJP on the patch-token part of the cotangent.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  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) — a LOCAL re-spelling of the proven patchEmbed_weight_grad (Attention.lean), kept here so StableHLO needn't import Attention (the tie is the §1-fold vit_render_patchW_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, and the trap planning/archive/bf16_renderer.md §9.2 exists to name.
                                      • 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 cls_slice_flat, 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 cls_slice_flat_has_vjp.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 mhsa_layer 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]. mhsa_layer'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
                                                        noncomputable def Proofs.StableHLO.bnBatchLA (N oc h w : ℕ) (ε : ℝ) (γ β : Vec oc) :
                                                        Vec (N * (oc * h * w)) → Vec (N * (oc * h * w))

                                                        True batch-norm at the network's left-assoc [N,C,H,W] flat index. The proven bnBatchTensor4 (typed at N·(oc·(h·w))) conjugated by the mul_assoc reindex so it slots into the N·(oc·h·w) batched composition (where conv/etc. produce oc·h·w = (oc·h)·w). Reindex only — the function IS bnBatchTensor4.

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

                                                          Which BatchNorm a forward chain emits — the batched-index peer of ResNet34Render.R34Bn, shared by the EfficientNet and MobileNetV2 renders so one traversal can produce both the training forward and its frozen-stats eval partner.

                                                          The distinction is not cosmetic and the §2a bug is what it exists to prevent: 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 — which is exactly what resnet34_fwd did until 2026-07-27, at rel 1.13 on real logits.

                                                          • 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
                                                            @[implicit_reducible]
                                                            instance Proofs.StableHLO.instDecidableEqBnMode :
                                                            DecidableEq BnMode
                                                            Equations
                                                            source
                                                            @[implicit_reducible]
                                                            instance Proofs.StableHLO.instReprBnMode :
                                                            Repr 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
                                                              noncomputable def Proofs.StableHLO.den {n : ℕ} :
                                                              SHlo n → Vec n

                                                              AST denotation ⟦·⟧ₐ — our reading of each StableHLO op's spec, over ℝ, per-example, in primitive terms — independent of dense/Mat.mulVec. SSA names are ignored.

                                                              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_sub {n : ℕ} (a b : SHlo n) :
                                                                den (a.sub b) = fun (j : Fin n) => den a j - den b j
                                                                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_conv {N ic oc h w kH kW : ℕ} (wN bN : String) (W : Kernel4 oc ic kH kW) (bias : Vec oc) (e : SHlo (N * (ic * h * w))) :
                                                                den (SHlo.batchOp (BatchableOp.conv wN bN W bias) e) = batchMap N (flatConv W bias) (den e)
                                                                source
                                                                @[simp]
                                                                theorem Proofs.StableHLO.den_batchOp_convStrided {N ic oc h w kH kW : ℕ} (wN bN : String) (W : Kernel4 oc ic kH kW) (bias : Vec oc) (e : SHlo (N * (ic * (2 * h) * (2 * w)))) :
                                                                den (SHlo.batchOp (BatchableOp.convStrided wN bN W bias) e) = batchMap N (flatConvStride2 W bias) (den e)
                                                                source
                                                                @[simp]
                                                                theorem Proofs.StableHLO.den_batchOp_convStridedXla {N ic oc h w kH kW : ℕ} (wN bN : String) (W : Kernel4 oc ic kH kW) (bias : Vec oc) (e : SHlo (N * (ic * (2 * h) * (2 * w)))) :
                                                                den (SHlo.batchOp (BatchableOp.convStridedXla wN bN W bias) e) = batchMap N (flatConvStride2Xla W bias) (den e)

                                                                The XLA-SAME peer. ⚠ Note it denotes flatConvStride2Xla, NOT flatConvStride2 — the two tokens have identical types and identical emitted shapes, so this rfl is the only place the distinction is recorded. Getting it wrong would make the render provably compute one net while emitting the other.

                                                                source
                                                                @[simp]
                                                                theorem Proofs.StableHLO.den_batchOp_depthwise {N c h w kH kW : ℕ} (wN bN : String) (W : DepthwiseKernel c kH kW) (bias : Vec c) (e : SHlo (N * (c * h * w))) :
                                                                den (SHlo.batchOp (BatchableOp.depthwise wN bN W bias) e) = batchMap N (depthwiseFlat W bias) (den e)
                                                                source
                                                                @[simp]
                                                                theorem Proofs.StableHLO.den_batchOp_depthwiseStrided {N c h w kH kW : ℕ} (wN bN : String) (W : DepthwiseKernel c kH kW) (bias : Vec c) (e : SHlo (N * (c * (2 * h) * (2 * w)))) :
                                                                den (SHlo.batchOp (BatchableOp.depthwiseStrided wN bN W bias) e) = batchMap N (depthwiseStride2Flat W bias) (den e)
                                                                source
                                                                @[simp]
                                                                theorem Proofs.StableHLO.den_batchOp_depthwiseStridedXla {N c h w kH kW : ℕ} (wN bN : String) (W : DepthwiseKernel c kH kW) (bias : Vec c) (e : SHlo (N * (c * (2 * h) * (2 * w)))) :
                                                                den (SHlo.batchOp (BatchableOp.depthwiseStridedXla wN bN W bias) e) = batchMap N (depthwiseStride2FlatXla W bias) (den e)

                                                                The XLA-SAME depthwise peer. ⚠ Denotes depthwiseStride2FlatXla, NOT depthwiseStride2Flat — same caveat as den_batchOp_convStridedXla: this rfl is the only place the two are distinguished.

                                                                source
                                                                @[simp]
                                                                theorem Proofs.StableHLO.den_batchOp_dense {N a c : ℕ} (wN bN : String) (W : Mat a c) (bias : Vec c) (e : SHlo (N * a)) :
                                                                den (SHlo.batchOp (BatchableOp.dense wN bN W bias) e) = batchMap N (dense W bias) (den e)
                                                                source
                                                                @[simp]
                                                                theorem Proofs.StableHLO.den_batchOp_bnEval {N oc h w : ℕ} (gN bN muN varN es : String) (ε : ℝ) (γ β μ var : Vec oc) (e : SHlo (N * (oc * h * w))) :
                                                                den (SHlo.batchOp (BatchableOp.bnEval gN bN muN varN es ε γ β μ var) e) = batchMap N (bnPerChannelEvalTensor3 oc h w ε γ β μ var) (den e)

                                                                Batched inference-BN faithfulness. The bnEval descriptor at the batched index denotes the proven bnPerChannelEvalTensor3 applied to each example independently, with the same frozen statistics. That is the formal statement of "eval is class-batch-independent" at N := B: no N appears on the right except as the number of independent applications, so an example's logits cannot depend on which others share its batch — unlike bnBatchF, whose den (bnBatchLA) genuinely couples the batch. Being affine in x, it needs no 0 < ε.

                                                                source
                                                                @[simp]
                                                                theorem Proofs.StableHLO.den_batchOp_gap {N c h w : ℕ} (e : SHlo (N * (c * h * w))) :
                                                                den (SHlo.batchOp BatchableOp.gap e) = batchMap N (globalAvgPoolFlat c h w) (den e)
                                                                source
                                                                @[simp]
                                                                theorem Proofs.StableHLO.den_batchOp_seBlock {N c h w r : ℕ} (w1 b1 w2 b2 : String) (W₁ : Mat c r) (β₁ : Vec r) (W₂ : Mat r c) (β₂ : Vec c) (e : SHlo (N * (c * h * w))) :
                                                                den (SHlo.batchOp (BatchableOp.seBlock w1 b1 w2 b2 W₁ β₁ W₂ β₂) e) = batchMap N (seBlockFull W₁ β₁ W₂ β₂) (den e)
                                                                source
                                                                @[simp]
                                                                theorem Proofs.StableHLO.den_batchOp_swish {N n : ℕ} (e : SHlo (N * n)) :
                                                                den (SHlo.batchOp BatchableOp.swish e) = batchMap N (swish n) (den e)
                                                                source
                                                                theorem Proofs.StableHLO.batchMap_pointwise {N n : ℕ} (g : ℝ → ℝ) (v : Vec (N * n)) :
                                                                batchMap N (fun (x : Vec n) (i : Fin n) => g (x i)) v = fun (idx : Fin (N * n)) => g (v idx)

                                                                Pointwise maps are batchMap-free. Lifting an elementwise map across N examples IS the elementwise map at the batched index N·n. This is why moving the pointwise nodes onto descriptors was denotation-preserving, and it is the half of that claim the artifact cannot witness: the render is value-independent, so a descriptor with the wrong den emits the same bytes. Cf. swishBackB/sigmoidBackB, which are NOT descriptors precisely because their backward is not of this shape — it reads a per-example saved activation.

                                                                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
                                                                @[simp]
                                                                theorem Proofs.StableHLO.den_batchOp_softmaxRow {N m n : ℕ} (e : SHlo (N * (m * n))) :
                                                                den (SHlo.batchOp BatchableOp.softmaxRow e) = batchMap N (rowSoftmaxFlat m n) (den e)
                                                                source
                                                                @[simp]
                                                                theorem Proofs.StableHLO.den_batchOp_denseRowBack {N rows a c : ℕ} (wN : String) (W : Mat a c) (e : SHlo (N * (rows * c))) :
                                                                den (SHlo.batchOp (BatchableOp.denseRowBack wN W) e) = batchMap N (rowDenseBackFlat rows a c W) (den e)
                                                                source
                                                                @[simp]
                                                                theorem Proofs.StableHLO.den_batchOp_relu {N n : ℕ} (e : SHlo (N * n)) :
                                                                den (SHlo.batchOp BatchableOp.relu e) = batchMap N (relu n) (den e)
                                                                source
                                                                @[simp]
                                                                theorem Proofs.StableHLO.den_batchOp_gelu {N n : ℕ} (e : SHlo (N * n)) :
                                                                den (SHlo.batchOp BatchableOp.gelu e) = batchMap N (gelu n) (den e)
                                                                source
                                                                @[simp]
                                                                theorem Proofs.StableHLO.den_batchOp_dotOut {N m n : ℕ} (wN : String) (W : Mat m n) (e : SHlo (N * n)) :
                                                                den (SHlo.batchOp (BatchableOp.dotOut wN W) e) = batchMap N (fun (v : Vec n) (i : Fin m) => ∑ j : Fin n, W i j * v j) (den e)
                                                                source
                                                                @[simp]
                                                                theorem Proofs.StableHLO.den_batchOp_expe {N n : ℕ} (e : SHlo (N * n)) :
                                                                den (SHlo.batchOp BatchableOp.expe e) = batchMap N (fun (v : Vec n) (j : Fin n) => Real.exp (v j)) (den e)
                                                                source
                                                                @[simp]
                                                                theorem Proofs.StableHLO.den_batchOp_softmaxDiv {N n : ℕ} (e : SHlo (N * n)) :
                                                                den (SHlo.batchOp BatchableOp.softmaxDiv e) = batchMap N (fun (v : Vec n) (j : Fin n) => v j / ∑ k : Fin n, v k) (den e)
                                                                source
                                                                @[simp]
                                                                theorem Proofs.StableHLO.den_batchOp_layerScaleCh {N c h w : ℕ} (gN : String) (γ : Vec c) (e : SHlo (N * (c * h * w))) :
                                                                den (SHlo.batchOp (BatchableOp.layerScaleCh gN γ) e) = batchMap N (fun (v : Vec (c * h * w)) => layerScale (fun (k : Fin (c * h * w)) => γ (chanIdx c h w k)) v) (den e)
                                                                source
                                                                @[simp]
                                                                theorem Proofs.StableHLO.den_batchOp_convStride4 {N ic oc h w kH kW : ℕ} (wN bN : String) (W : Kernel4 oc ic kH kW) (bias : Vec oc) (e : SHlo (N * (ic * (2 * (2 * h)) * (2 * (2 * w))))) :
                                                                den (SHlo.batchOp (BatchableOp.convStride4 wN bN W bias) e) = batchMap N (flatConvStride4 W bias) (den e)
                                                                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
                                                                @[simp]
                                                                theorem Proofs.StableHLO.den_batchOp_transpose {N m n : ℕ} (e : SHlo (N * (m * n))) :
                                                                den (SHlo.batchOp BatchableOp.transpose e) = batchMap N (transposeFlat m n) (den e)
                                                                source
                                                                @[simp]
                                                                theorem Proofs.StableHLO.den_batchOp_lnRow {N m n : ℕ} (gN bN es : String) (ε γ β : ℝ) (e : SHlo (N * (m * n))) :
                                                                den (SHlo.batchOp (BatchableOp.lnRow gN bN es ε γ β) e) = batchMap N (rowLNFlat m n ε γ β) (den e)
                                                                source
                                                                @[simp]
                                                                theorem Proofs.StableHLO.den_batchOp_rowScale {N m n : ℕ} (gN : String) (γ : Vec n) (e : SHlo (N * (m * n))) :
                                                                den (SHlo.batchOp (BatchableOp.rowScale gN γ) e) = batchMap N (rowScaleFlat m n γ) (den e)
                                                                source
                                                                @[simp]
                                                                theorem Proofs.StableHLO.den_batchOp_rowBias {N m n : ℕ} (bN : String) (β : Vec n) (e : SHlo (N * (m * n))) :
                                                                den (SHlo.batchOp (BatchableOp.rowBias bN β) e) = batchMap N (rowBiasFlat m n β) (den e)

                                                                ViT increment 1 — the six batch-invariant forms #

                                                                ⚠ Read the binders: N is the BATCH and tk is ViT's token count. The per-example renderer calls the token axis N, so these two statements are the place where that name is re-pointed, and getting them the wrong way round type-checks (both are Nat and both appear multiplied).

                                                                source
                                                                @[simp]
                                                                theorem Proofs.StableHLO.den_batchOp_denseRow {N tk a c : ℕ} (wN bN : String) (W : Mat a c) (b : Vec c) (e : SHlo (N * (tk * a))) :
                                                                den (SHlo.batchOp (BatchableOp.denseRow wN bN W b) e) = batchMap N (rowDenseFlat tk a c W b) (den e)
                                                                source
                                                                @[simp]
                                                                theorem Proofs.StableHLO.den_batchOp_patchEmbed {N ic H W P tk D : ℕ} (wN bN clsN posN : String) (Wc : Kernel4 D ic P P) (bc cls : Vec D) (pos : Mat (tk + 1) D) (e : SHlo (N * (ic * H * W))) :
                                                                den (SHlo.batchOp (BatchableOp.patchEmbed wN bN clsN posN Wc bc cls pos) e) = batchMap N (patchEmbedFlat ic H W P tk D Wc bc cls pos) (den e)
                                                                source
                                                                @[simp]
                                                                theorem Proofs.StableHLO.den_batchOp_clsSlice {N tk D : ℕ} (e : SHlo (N * ((tk + 1) * D))) :
                                                                den (SHlo.batchOp BatchableOp.clsSlice e) = batchMap N (clsSliceFlat tk D) (den e)
                                                                source
                                                                @[simp]
                                                                theorem Proofs.StableHLO.den_batchOp_clsPad {N tk D : ℕ} (e : SHlo (N * D)) :
                                                                den (SHlo.batchOp BatchableOp.clsPad e) = batchMap N (clsPadFlat tk D) (den e)
                                                                source
                                                                @[simp]
                                                                theorem Proofs.StableHLO.den_batchOp_headSlice {N tk heads d : ℕ} (h : Fin heads) (e : SHlo (N * (tk * (heads * d)))) :
                                                                den (SHlo.batchOp (BatchableOp.headSlice h) e) = batchMap N (headSliceFlat tk heads d h) (den e)
                                                                source
                                                                @[simp]
                                                                theorem Proofs.StableHLO.den_batchOp_headPad {N tk heads d : ℕ} (h : Fin heads) (e : SHlo (N * (tk * d))) :
                                                                den (SHlo.batchOp (BatchableOp.headPad h) e) = batchMap N (headPadFlat tk heads d h) (den e)
                                                                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
                                                                theorem Proofs.StableHLO.den_batchOp_lnRow_eq_lnRowF {N m n : ℕ} (gN bN es : String) (ε γ β : ℝ) (e : SHlo (N * (m * n))) :
                                                                den (SHlo.batchOp (BatchableOp.lnRow gN bN es ε γ β) e) = batchMap N (fun (v : Vec (m * n)) => den (SHlo.lnRowF gN bN es ε γ β (SHlo.operand "" v))) (den e)

                                                                The two halves agree, per form. The batched descriptor denotes the batch-lift of exactly what its per-example peer denotes — stated against den (.lnRowF …) rather than against rowLNFlat so the claim is "same function as the op the renderer is replacing", which is what a reader of the swapped render needs. rfl on both sides; kept as five separate statements because a simp set of five batchMap rewrites is what the whole-net faithfulness proof will consume.

                                                                source
                                                                theorem Proofs.StableHLO.den_batchOp_denseRow_eq_denseRowF {N tk a c : ℕ} (wN bN : String) (W : Mat a c) (b : Vec c) (e : SHlo (N * (tk * a))) :
                                                                den (SHlo.batchOp (BatchableOp.denseRow wN bN W b) e) = batchMap N (fun (v : Vec (tk * a)) => den (SHlo.denseRowF wN bN W b (SHlo.operand "" v))) (den e)

                                                                ViT increment 1's peer of the above, on the form that carries the most data. ⚠ Its per-example peer takes the TOKEN count as N; this one takes the BATCH as N and the token count as tk, and both Ns are Nat. Writing the equation out is what makes the two visible at once.

                                                                source
                                                                theorem Proofs.StableHLO.den_batchOp_gelu_eq_geluF {N n : ℕ} (e : SHlo (N * n)) :
                                                                den (SHlo.batchOp BatchableOp.gelu e) = batchMap N (fun (v : Vec n) => den (SHlo.operand "" v).geluF) (den e)
                                                                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_batchOp_maxPool {N c h w : ℕ} (e : SHlo (N * (c * (2 * h) * (2 * w)))) :
                                                                den (SHlo.batchOp BatchableOp.maxPool e) = batchMap N (maxPoolFlat c h w) (den e)
                                                                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_batchOp_maxPool3s2 {N c h w : ℕ} (e : SHlo (N * (c * (2 * h) * (2 * w)))) :
                                                                den (SHlo.batchOp BatchableOp.maxPool3s2 e) = batchMap N (maxPool3s2Flat c h w) (den e)

                                                                ⭐ The batched 3×3/s2 pool forward denotes He et al.'s pool lifted across the batch. ⚠ Read it beside den_batchOp_maxPool directly above: same type, different function. The two descriptors are indistinguishable to every structural check the repo has — arity, op counts, the prefix audit and the shape of the emitted text — which is exactly how the deviation survived undocumented on every ResNet here. maxPool3s2_ne_maxPool_descr pins them apart.

                                                                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) = (swish_has_vjp (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) = (gelu_has_vjp (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) = (sigmoid_has_vjp (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) = (dense_has_vjp W b).backward x dy

                                                                      Dense input-VJP faithfulness. The backward graph denotes the proven dense VJP backward (dense_has_vjp 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) = (relu_has_vjp_at k x hx).backward (den e)

                                                                              ReLU backward faithfulness (smooth point). select(x>0,·,0) denotes the proven relu_has_vjp_at 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) = (relu_has_vjp_at (N * n) x hx).backward (den e)

                                                                              Batched ReLU backward faithfulness. selectPosB denotes the same proven relu_has_vjp_at 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 (MobileNetV2.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) = (relu6_has_vjp_at k x h_smooth).backward (den e)

                                                                              ReLU6 backward faithfulness (smooth point). select(0<x<6,·,0) denotes the proven relu6_has_vjp_at 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 (§2f). 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) = (relu6_has_vjp_at (N * n) x h_smooth).backward (den e)

                                                                              Batched ReLU6 backward faithfulness. selectMidB denotes the same proven relu6_has_vjp_at 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) = (dropPath_has_vjp 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) = (dropout_has_vjp 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
                                                                                def Proofs.StableHLO.mlpFwdGraph {e₀ e₁ e₂ e₃ : ℕ} (W₀ : Mat e₀ e₁) (b₀ : Vec e₁) (W₁ : Mat e₁ e₂) (b₁ : Vec e₂) (W₂ : Mat e₂ e₃) (b₂ : Vec e₃) (x : Vec e₀) :
                                                                                SHlo e₃

                                                                                Whole-MLP forward graph dense W₂ ∘ relu ∘ dense W₁ ∘ relu ∘ dense W₀.

                                                                                Equations
                                                                                • One or more equations did not get rendered due to their size.
                                                                                Instances For
                                                                                  source
                                                                                  theorem Proofs.StableHLO.mlpFwdGraph_faithful {e₀ e₁ e₂ e₃ : ℕ} (W₀ : Mat e₀ e₁) (b₀ : Vec e₁) (W₁ : Mat e₁ e₂) (b₁ : Vec e₂) (W₂ : Mat e₂ e₃) (b₂ : Vec e₃) (x : Vec e₀) :
                                                                                  den (mlpFwdGraph W₀ b₀ W₁ b₁ W₂ b₂ x) = mlpForward W₀ b₀ W₁ b₁ W₂ b₂ x

                                                                                  MLP forward faithfulness. The forward graph denotes mlpForward.

                                                                                  source
                                                                                  def Proofs.StableHLO.mlpBackGraph {e₀ e₁ e₂ e₃ : ℕ} (W₀ : Mat e₀ e₁) (W₁ : Mat e₁ e₂) (W₂ : Mat e₂ e₃) (p₀ : Vec e₁) (p₁ : Vec e₂) (dy : Vec e₃) :
                                                                                  SHlo e₀

                                                                                  Whole-MLP backward (input-VJP) graph: dotOut W₀ ∘ select(p₀) ∘ dotOut W₁ ∘ select(p₁) ∘ dotOut W₂, pᵢ the ReLU pre-activations.

                                                                                  Equations
                                                                                  • One or more equations did not get rendered due to their size.
                                                                                  Instances For
                                                                                    source
                                                                                    theorem Proofs.StableHLO.mlpBackGraph_faithful {e₀ e₁ e₂ e₃ : ℕ} (W₀ : Mat e₀ e₁) (b₀ : Vec e₁) (W₁ : Mat e₁ e₂) (b₁ : Vec e₂) (W₂ : Mat e₂ e₃) (b₂ : Vec e₃) (x : Vec e₀) (h0 : ∀ (k : Fin e₁), dense W₀ b₀ x k ≠ 0) (h1 : ∀ (k : Fin e₂), dense W₁ b₁ (relu e₁ (dense W₀ b₀ x)) k ≠ 0) (dy : Vec e₃) :
                                                                                    den (mlpBackGraph W₀ W₁ W₂ (dense W₀ b₀ x) (dense W₁ b₁ (relu e₁ (dense W₀ b₀ x))) dy) = (mlp_has_vjp_at W₀ b₀ W₁ b₁ W₂ b₂ x h0 h1).backward dy

                                                                                    MLP backward faithfulness (smooth point). The backward graph denotes the proven mlp_has_vjp_at.backward — the per-op dot_general/select ops assembled into the proven whole-network VJP (cf. IR.mlp_whole_bridge).

                                                                                    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. planning/archive/rsb_a3_r50_verified.md §4b.

                                                                                    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) = (hasVJP3_to_hasVJP (conv2d_has_vjp3 W b)).backward v (den e)

                                                                                    Conv backward faithfulness. The reversed-kernel stablehlo.convolution (transpose+reverse+conv) denotes the proven conv input-VJP — the flattened conv2d_has_vjp3 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) = (maxPoolFlat_has_vjp_at (Tensor3.unflatten x) h_smooth).backward (den e)

                                                                                    Max-pool backward faithfulness (smooth point). The emitted select_and_scatter graph denotes the proven maxPoolFlat_has_vjp_at 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) = (maxPool3s2Flat_has_vjp_at (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 maxPool3s2Flat_has_vjp_at 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) = (flatConvStride2_has_vjp W b).backward v (den e)

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

                                                                                    • reversed-kernel conv denotes the proven flatConvStride2_has_vjp 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
                                                                                    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, so kept out of the axiom audit — roundtrip covers it structurally.)

                                                                                    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) = (conv2d_weight_grad_has_vjp b x).backward W.flatten (den e)

                                                                                    Conv weight-gradient faithfulness — the proven conv2d_weight_grad 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) = (conv2d_bias_grad_has_vjp W x).backward b (den e)

                                                                                    Conv bias-gradient faithfulness — the proven conv2d_bias_grad 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 §2a left fused, which is why vit_adam_train_step had no certified render until these existed. 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 (§2f, 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, (depthwise_bias_grad_has_vjp 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, (depthwiseStride2_bias_grad_has_vjp 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 (§2f) #

                                                                                    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 (§2a).

                                                                                    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) = (flatConvStride4_weight_grad_has_vjp b x).backward W.flatten (den e)

                                                                                    Stride-4 weight-gradient faithfulness (ConvNeXt's patchify stem). den IS the proven flatConvStride4_weight_grad_has_vjp 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.convStridedXlaWeightSgd_faithful {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.convStridedXlaWeightSgd xN wN lrS b x W lr e) idx = W.flatten idx - lr * (flatConvStride2Xla_weight_grad_has_vjp b x).backward W.flatten (den e) idx

                                                                                    XLA-SAME strided-conv weight-SGD faithfulness. The per-example op's den IS the proven flatConvStride2Xla_weight_grad_has_vjp descent step. There is no per-example convStridedXlaWeightGrad token to factor through (only the batched …B one exists), so this pins the den directly, as convStride4WeightGrad_faithful does.

                                                                                    source
                                                                                    @[simp]
                                                                                    theorem Proofs.StableHLO.convStridedXlaBiasSgd_faithful {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.convStridedXlaBiasSgd bN lrS W x b lr e) o = b o - lr * (flatConvStride2Xla_bias_grad_has_vjp W x).backward b (den e) o

                                                                                    XLA-SAME strided-conv bias-SGD faithfulness. Same reduce text as convBiasSgd; the den is the flatConvStride2Xla bias VJP.

                                                                                    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 §2a's per-example eight: 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. This is what unblocks a batched resnet34_adam_train_step rendered from Proofs/ — the blocker was the fusion, never Adam.

                                                                                    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 emitted 26-op block denotes exactly Proofs.adamWParam of the child's gradient — the theorem that moves the optimizer from a trusted hand-written emitter (ViTRender.emitAdamV, which only claimed to be op-for-op adamWParam) into the proven kit. 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, per §4's no-CSE rule), 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 (§2b-bis measured that on R34's 108 → 36 rsqrt at no run-time cost).

                                                                                    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
                                                                                    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 (bnPerChannelTensor3_grad_input_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, so kept out of the axiom audit — roundtrip covers it structurally.)

                                                                                    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) = (depthwiseFlat_has_vjp 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 depthwiseFlat_has_vjp 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) = (depthwiseStride2Flat_has_vjp 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 depthwiseStride2Flat_has_vjp backward.

                                                                                    source
                                                                                    theorem Proofs.StableHLO.depthwiseStridedXlaBack_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.depthwiseStridedXlaBack wN W b v e) = (depthwiseStride2FlatXla_has_vjp W b).backward v (den e)

                                                                                    XLA-SAME strided-depthwise input-VJP faithfulness. depthwiseStridedBack's text with the transposed-conv pad at [p+1, p-1]; denotes the proven depthwiseStride2FlatXla_has_vjp backward (= scatter onto the ODD positions, then the stride-1 depthwise input-VJP).

                                                                                    source
                                                                                    @[simp]
                                                                                    theorem Proofs.StableHLO.depthwiseStridedXlaWeightSgd_faithful {c h w kH kW : ℕ} (xN wN lrS : String) (b : Vec c) (x : Vec (c * (2 * h) * (2 * w))) (W : DepthwiseKernel c kH kW) (lr : ℝ) (e : SHlo (c * h * w)) (idx : Fin (c * kH * kW)) :
                                                                                    den (SHlo.depthwiseStridedXlaWeightSgd xN wN lrS b x W lr e) idx = Tensor3.flatten W idx - lr * (depthwiseStride2Xla_weight_grad_has_vjp b x).backward (Tensor3.flatten W) (den e) idx

                                                                                    XLA-SAME strided-depthwise weight-SGD faithfulness. den IS the depthwiseStride2Xla_weight_grad_has_vjp descent step (through the non-reducing depthwiseStridedXlaWeightSgdDen wrapper, Depthwise.lean).

                                                                                    source
                                                                                    @[simp]
                                                                                    theorem Proofs.StableHLO.depthwiseStridedXlaBiasSgd_faithful {c h w kH kW : ℕ} (bN lrS : String) (W : DepthwiseKernel c kH kW) (x : Vec (c * (2 * h) * (2 * w))) (b : Vec c) (lr : ℝ) (e : SHlo (c * h * w)) (o : Fin c) :
                                                                                    den (SHlo.depthwiseStridedXlaBiasSgd bN lrS W x b lr e) o = b o - lr * (depthwiseStride2Xla_bias_grad_has_vjp W x).backward b (den e) o

                                                                                    XLA-SAME strided-depthwise bias-SGD faithfulness.

                                                                                    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, so kept out of the axiom audit — roundtrip covers it structurally.)

                                                                                    source
                                                                                    theorem Proofs.StableHLO.swishBack_faithful {n : ℕ} (xN : String) (x : Vec n) (e : SHlo n) :
                                                                                    den (SHlo.swishBack xN x e) = (swish_has_vjp 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 swish_has_vjp 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), EfficientNet.lean) — the SE gate's output nonlinearity. Smooth everywhere. (rfl, so kept out of the axiom audit — roundtrip covers it.)

                                                                                    source
                                                                                    theorem Proofs.StableHLO.sigmoidBack_faithful {n : ℕ} (xN : String) (x : Vec n) (e : SHlo n) :
                                                                                    den (SHlo.sigmoidBack xN x e) = (sigmoid_has_vjp 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 sigmoid_has_vjp 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, so kept out of the axiom audit — roundtrip covers it structurally.)

                                                                                    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 (ConvNeXt.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) = (gelu_has_vjp 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 gelu_has_vjp 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, so kept out of the axiom audit — roundtrip covers it structurally.)

                                                                                    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 rowSoftmax_has_vjp_mat.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, so kept out of the axiom audit — roundtrip covers it structurally.)

                                                                                    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 bn_grad_input — 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 dense_has_vjp 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 patchEmbed_flat; the tie is rfl in ViTFwdGraph). (rfl, coarse-token like seBlock.)

                                                                                    source
                                                                                    @[simp]
                                                                                    theorem Proofs.StableHLO.patchEmbedBack_faithful {ic H W P N D : ℕ} (wN : String) (Wc : Kernel4 D ic P P) (e : SHlo ((N + 1) * D)) :
                                                                                    den (SHlo.patchEmbedBack wN Wc e) = patchEmbedBackFlat ic H W P N D Wc (den e)

                                                                                    Patch-embedding input-VJP faithfulness. The reversed-kernel strided conv_transpose (on the patch-token rows of the [N+1,D] cotangent) denotes patchEmbedBackFlat (= the proven patchEmbed_input_grad_formula; the tie to patchEmbed_flat_has_vjp.backward is rfl in ViTBackB0). (rfl.)

                                                                                    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 cls_slice_flat). (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 cls_slice_flat_has_vjp.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 (= mhsa_layer'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 mhsa_layer'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.cnnFwdGraph {ic c h w d1 nClasses kH kW : ℕ} (W₁ : Kernel4 c ic kH kW) (b₁ : Vec c) (W₂ : Kernel4 c c kH kW) (b₂ : Vec c) (W₃ : Mat (c * h * w) d1) (b₃ : Vec d1) (W₄ : Mat d1 d1) (b₄ : Vec d1) (W₅ : Mat d1 nClasses) (b₅ : Vec nClasses) (x : Vec (ic * (2 * h) * (2 * w))) :
                                                                                    SHlo nClasses

                                                                                    Whole MNIST-CNN forward graph: dense ∘ relu ∘ dense ∘ relu ∘ dense ∘ maxPool ∘ relu ∘ conv ∘ relu ∘ conv.

                                                                                    Equations
                                                                                    • One or more equations did not get rendered due to their size.
                                                                                    Instances For
                                                                                      source
                                                                                      theorem Proofs.StableHLO.cnnFwdGraph_faithful {ic c h w d1 nClasses kH kW : ℕ} (W₁ : Kernel4 c ic kH kW) (b₁ : Vec c) (W₂ : Kernel4 c c kH kW) (b₂ : Vec c) (W₃ : Mat (c * h * w) d1) (b₃ : Vec d1) (W₄ : Mat d1 d1) (b₄ : Vec d1) (W₅ : Mat d1 nClasses) (b₅ : Vec nClasses) (x : Vec (ic * (2 * h) * (2 * w))) :
                                                                                      den (cnnFwdGraph W₁ b₁ W₂ b₂ W₃ b₃ W₄ b₄ W₅ b₅ x) = mnistCnnNoBnForward W₁ b₁ W₂ b₂ W₃ b₃ W₄ b₄ W₅ b₅ x

                                                                                      CNN forward faithfulness. The forward graph denotes the proven mnistCnnNoBnForward.

                                                                                      source
                                                                                      def Proofs.StableHLO.cifarFwdGraph {ic c1 c2 h w d1 nClasses kH kW : ℕ} (W₁ : Kernel4 c1 ic kH kW) (b₁ : Vec c1) (W₂ : Kernel4 c1 c1 kH kW) (b₂ : Vec c1) (W₃ : Kernel4 c2 c1 kH kW) (b₃ : Vec c2) (W₄ : Kernel4 c2 c2 kH kW) (b₄ : Vec c2) (W₅ : Mat (c2 * h * w) d1) (b₅ : Vec d1) (W₆ : Mat d1 d1) (b₆ : Vec d1) (W₇ : Mat d1 nClasses) (b₇ : Vec nClasses) (x : Vec (ic * (2 * (2 * h)) * (2 * (2 * w)))) :
                                                                                      SHlo nClasses

                                                                                      Whole CIFAR-CNN forward graph (Chapter 4): two conv→relu→conv→relu→maxPool stages (channels ic→c1→c1, then c1→c2→c2) then dense→relu→dense→relu→dense. The Chapter-4 peer of cnnFwdGraph.

                                                                                      Equations
                                                                                      • One or more equations did not get rendered due to their size.
                                                                                      Instances For
                                                                                        source
                                                                                        theorem Proofs.StableHLO.cifarFwdGraph_faithful {ic c1 c2 h w d1 nClasses kH kW : ℕ} (W₁ : Kernel4 c1 ic kH kW) (b₁ : Vec c1) (W₂ : Kernel4 c1 c1 kH kW) (b₂ : Vec c1) (W₃ : Kernel4 c2 c1 kH kW) (b₃ : Vec c2) (W₄ : Kernel4 c2 c2 kH kW) (b₄ : Vec c2) (W₅ : Mat (c2 * h * w) d1) (b₅ : Vec d1) (W₆ : Mat d1 d1) (b₆ : Vec d1) (W₇ : Mat d1 nClasses) (b₇ : Vec nClasses) (x : Vec (ic * (2 * (2 * h)) * (2 * (2 * w)))) :
                                                                                        den (cifarFwdGraph W₁ b₁ W₂ b₂ W₃ b₃ W₄ b₄ W₅ b₅ W₆ b₆ W₇ b₇ x) = cifarCnnForward W₁ b₁ W₂ b₂ W₃ b₃ W₄ b₄ W₅ b₅ W₆ b₆ W₇ b₇ x

                                                                                        CIFAR-CNN forward faithfulness. The forward graph denotes the proven cifarCnnForward.

                                                                                        source
                                                                                        def Proofs.StableHLO.cifarBnFwdGraph {ic c1 c2 h w d1 nClasses kH kW : ℕ} (epsStr : String) (W₁ : Kernel4 c1 ic kH kW) (b₁ : Vec c1) (ε₁ : ℝ) (γ₁ β₁ : Vec c1) (W₂ : Kernel4 c1 c1 kH kW) (b₂ : Vec c1) (ε₂ : ℝ) (γ₂ β₂ : Vec c1) (W₃ : Kernel4 c2 c1 kH kW) (b₃ : Vec c2) (ε₃ : ℝ) (γ₃ β₃ : Vec c2) (W₄ : Kernel4 c2 c2 kH kW) (b₄ : Vec c2) (ε₄ : ℝ) (γ₄ β₄ : Vec c2) (W₅ : Mat (c2 * h * w) d1) (b₅ : Vec d1) (W₆ : Mat d1 d1) (b₆ : Vec d1) (W₇ : Mat d1 nClasses) (b₇ : Vec nClasses) (x : Vec (ic * (2 * (2 * h)) * (2 * (2 * w)))) :
                                                                                        SHlo nClasses

                                                                                        Whole BN-CIFAR forward graph (Chapter 4, BatchNorm variant): each conv is followed by a per-example bnF before its ReLU. epsStr is the shared ε literal; the four BN layers carry scalar γ/β inputs %g{i}/%bt{i}.

                                                                                        Equations
                                                                                        • One or more equations did not get rendered due to their size.
                                                                                        Instances For
                                                                                          source
                                                                                          theorem Proofs.StableHLO.cifarBnFwdGraph_faithful {ic c1 c2 h w d1 nClasses kH kW : ℕ} (epsStr : String) (W₁ : Kernel4 c1 ic kH kW) (b₁ : Vec c1) (ε₁ : ℝ) (γ₁ β₁ : Vec c1) (W₂ : Kernel4 c1 c1 kH kW) (b₂ : Vec c1) (ε₂ : ℝ) (γ₂ β₂ : Vec c1) (W₃ : Kernel4 c2 c1 kH kW) (b₃ : Vec c2) (ε₃ : ℝ) (γ₃ β₃ : Vec c2) (W₄ : Kernel4 c2 c2 kH kW) (b₄ : Vec c2) (ε₄ : ℝ) (γ₄ β₄ : Vec c2) (W₅ : Mat (c2 * h * w) d1) (b₅ : Vec d1) (W₆ : Mat d1 d1) (b₆ : Vec d1) (W₇ : Mat d1 nClasses) (b₇ : Vec nClasses) (x : Vec (ic * (2 * (2 * h)) * (2 * (2 * w)))) :
                                                                                          den (cifarBnFwdGraph epsStr W₁ b₁ ε₁ γ₁ β₁ W₂ b₂ ε₂ γ₂ β₂ W₃ b₃ ε₃ γ₃ β₃ W₄ b₄ ε₄ γ₄ β₄ W₅ b₅ W₆ b₆ W₇ b₇ x) = cifarCnnBnForward W₁ b₁ ε₁ γ₁ β₁ W₂ b₂ ε₂ γ₂ β₂ W₃ b₃ ε₃ γ₃ β₃ W₄ b₄ ε₄ γ₄ β₄ W₅ b₅ W₆ b₆ W₇ b₇ x

                                                                                          BN-CIFAR forward faithfulness. The forward graph denotes the proven cifarCnnBnForward.

                                                                                          source
                                                                                          def Proofs.StableHLO.cifar8FwdGraph {ic c1 c2 c3 c4 h w d1 nClasses kH kW : ℕ} (W₁ : Kernel4 c1 ic kH kW) (b₁ : Vec c1) (W₂ : Kernel4 c1 c1 kH kW) (b₂ : Vec c1) (W₃ : Kernel4 c2 c1 kH kW) (b₃ : Vec c2) (W₄ : Kernel4 c2 c2 kH kW) (b₄ : Vec c2) (W₅ : Kernel4 c3 c2 kH kW) (b₅ : Vec c3) (W₆ : Kernel4 c3 c3 kH kW) (b₆ : Vec c3) (W₇ : Kernel4 c4 c3 kH kW) (b₇ : Vec c4) (W₈ : Kernel4 c4 c4 kH kW) (b₈ : Vec c4) (W₉ : Mat (c4 * h * w) d1) (b₉ : Vec d1) (Wa : Mat d1 d1) (ba : Vec d1) (Wb : Mat d1 nClasses) (bb : Vec nClasses) (x : Vec (ic * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w)))))) :
                                                                                          SHlo nClasses

                                                                                          Whole deeper (8-conv) CIFAR-CNN forward graph: four conv→relu→conv→relu→maxPool stages (channels ic→c1→c1, c1→c2→c2, c2→c3→c3, c3→c4→c4) then dense→relu→dense→relu→dense. The 4-stage peer of cifarFwdGraph.

                                                                                          Equations
                                                                                          • One or more equations did not get rendered due to their size.
                                                                                          Instances For
                                                                                            source
                                                                                            theorem Proofs.StableHLO.cifar8FwdGraph_faithful {ic c1 c2 c3 c4 h w d1 nClasses kH kW : ℕ} (W₁ : Kernel4 c1 ic kH kW) (b₁ : Vec c1) (W₂ : Kernel4 c1 c1 kH kW) (b₂ : Vec c1) (W₃ : Kernel4 c2 c1 kH kW) (b₃ : Vec c2) (W₄ : Kernel4 c2 c2 kH kW) (b₄ : Vec c2) (W₅ : Kernel4 c3 c2 kH kW) (b₅ : Vec c3) (W₆ : Kernel4 c3 c3 kH kW) (b₆ : Vec c3) (W₇ : Kernel4 c4 c3 kH kW) (b₇ : Vec c4) (W₈ : Kernel4 c4 c4 kH kW) (b₈ : Vec c4) (W₉ : Mat (c4 * h * w) d1) (b₉ : Vec d1) (Wa : Mat d1 d1) (ba : Vec d1) (Wb : Mat d1 nClasses) (bb : Vec nClasses) (x : Vec (ic * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w)))))) :
                                                                                            den (cifar8FwdGraph W₁ b₁ W₂ b₂ W₃ b₃ W₄ b₄ W₅ b₅ W₆ b₆ W₇ b₇ W₈ b₈ W₉ b₉ Wa ba Wb bb x) = cifarCnn8Forward W₁ b₁ W₂ b₂ W₃ b₃ W₄ b₄ W₅ b₅ W₆ b₆ W₇ b₇ W₈ b₈ W₉ b₉ Wa ba Wb bb x

                                                                                            Deeper (8-conv) CIFAR-CNN forward faithfulness. The forward graph denotes the proven cifarCnn8Forward.

                                                                                            source
                                                                                            def Proofs.StableHLO.cifar8BnFwdGraph {ic c1 c2 c3 c4 h w d1 nClasses kH kW : ℕ} (epsStr : String) (W₁ : Kernel4 c1 ic kH kW) (b₁ : Vec c1) (ε₁ : ℝ) (γ₁ β₁ : Vec c1) (W₂ : Kernel4 c1 c1 kH kW) (b₂ : Vec c1) (ε₂ : ℝ) (γ₂ β₂ : Vec c1) (W₃ : Kernel4 c2 c1 kH kW) (b₃ : Vec c2) (ε₃ : ℝ) (γ₃ β₃ : Vec c2) (W₄ : Kernel4 c2 c2 kH kW) (b₄ : Vec c2) (ε₄ : ℝ) (γ₄ β₄ : Vec c2) (W₅ : Kernel4 c3 c2 kH kW) (b₅ : Vec c3) (ε₅ : ℝ) (γ₅ β₅ : Vec c3) (W₆ : Kernel4 c3 c3 kH kW) (b₆ : Vec c3) (ε₆ : ℝ) (γ₆ β₆ : Vec c3) (W₇ : Kernel4 c4 c3 kH kW) (b₇ : Vec c4) (ε₇ : ℝ) (γ₇ β₇ : Vec c4) (W₈ : Kernel4 c4 c4 kH kW) (b₈ : Vec c4) (ε₈ : ℝ) (γ₈ β₈ : Vec c4) (W₉ : Mat (c4 * h * w) d1) (b₉ : Vec d1) (Wa : Mat d1 d1) (ba : Vec d1) (Wb : Mat d1 nClasses) (bb : Vec nClasses) (x : Vec (ic * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w)))))) :
                                                                                            SHlo nClasses

                                                                                            Whole deeper (8-conv) BN-CIFAR forward graph: each of the eight convs is followed by a per-channel bnPerChannelF before its ReLU. epsStr is the shared ε literal; the eight BN layers carry per-channel γ/β inputs %g{i}/%bt{i}. The 4-stage peer of cifarBnFwdGraph.

                                                                                            Equations
                                                                                            • One or more equations did not get rendered due to their size.
                                                                                            Instances For
                                                                                              source
                                                                                              theorem Proofs.StableHLO.cifar8BnFwdGraph_faithful {ic c1 c2 c3 c4 h w d1 nClasses kH kW : ℕ} (epsStr : String) (W₁ : Kernel4 c1 ic kH kW) (b₁ : Vec c1) (ε₁ : ℝ) (γ₁ β₁ : Vec c1) (W₂ : Kernel4 c1 c1 kH kW) (b₂ : Vec c1) (ε₂ : ℝ) (γ₂ β₂ : Vec c1) (W₃ : Kernel4 c2 c1 kH kW) (b₃ : Vec c2) (ε₃ : ℝ) (γ₃ β₃ : Vec c2) (W₄ : Kernel4 c2 c2 kH kW) (b₄ : Vec c2) (ε₄ : ℝ) (γ₄ β₄ : Vec c2) (W₅ : Kernel4 c3 c2 kH kW) (b₅ : Vec c3) (ε₅ : ℝ) (γ₅ β₅ : Vec c3) (W₆ : Kernel4 c3 c3 kH kW) (b₆ : Vec c3) (ε₆ : ℝ) (γ₆ β₆ : Vec c3) (W₇ : Kernel4 c4 c3 kH kW) (b₇ : Vec c4) (ε₇ : ℝ) (γ₇ β₇ : Vec c4) (W₈ : Kernel4 c4 c4 kH kW) (b₈ : Vec c4) (ε₈ : ℝ) (γ₈ β₈ : Vec c4) (W₉ : Mat (c4 * h * w) d1) (b₉ : Vec d1) (Wa : Mat d1 d1) (ba : Vec d1) (Wb : Mat d1 nClasses) (bb : Vec nClasses) (x : Vec (ic * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w)))))) :
                                                                                              den (cifar8BnFwdGraph epsStr W₁ b₁ ε₁ γ₁ β₁ W₂ b₂ ε₂ γ₂ β₂ W₃ b₃ ε₃ γ₃ β₃ W₄ b₄ ε₄ γ₄ β₄ W₅ b₅ ε₅ γ₅ β₅ W₆ b₆ ε₆ γ₆ β₆ W₇ b₇ ε₇ γ₇ β₇ W₈ b₈ ε₈ γ₈ β₈ W₉ b₉ Wa ba Wb bb x) = cifarCnnBn8Forward W₁ b₁ ε₁ γ₁ β₁ W₂ b₂ ε₂ γ₂ β₂ W₃ b₃ ε₃ γ₃ β₃ W₄ b₄ ε₄ γ₄ β₄ W₅ b₅ ε₅ γ₅ β₅ W₆ b₆ ε₆ γ₆ β₆ W₇ b₇ ε₇ γ₇ β₇ W₈ b₈ ε₈ γ₈ β₈ W₉ b₉ Wa ba Wb bb x

                                                                                              Deeper (8-conv) BN-CIFAR forward faithfulness. The forward graph denotes the proven cifarCnnBn8Forward.

                                                                                              source
                                                                                              def Proofs.StableHLO.resnetFwdGraph {ic c oc h w kHs kWs kH₁ kW₁ kH₂ kW₂ kH₁' kW₁' kH₂' kW₂' kHp kWp nClasses : ℕ} (epsStr : String) (Ws : Kernel4 c ic kHs kWs) (bs : Vec c) (εs γs βs : ℝ) (W₁ : Kernel4 c c kH₁ kW₁) (b₁ : Vec c) (W₂ : Kernel4 c c kH₂ kW₂) (b₂ : Vec c) (e₁ g₁ bb₁ e₂ g₂ bb₂ : ℝ) (W₁' : Kernel4 oc c kH₁' kW₁') (b₁' : Vec oc) (W₂' : Kernel4 oc oc kH₂' kW₂') (b₂' : Vec oc) (Wp : Kernel4 oc c kHp kWp) (bp : Vec oc) (f₁ h₁ i₁ f₂ h₂ i₂ fp hp ip : ℝ) (Wd : Mat oc nClasses) (bd : Vec nClasses) (x : Vec (ic * (2 * h) * (2 * w))) :
                                                                                              SHlo nClasses

                                                                                              Whole ResNet-style forward graph (Chapter 5): the structure the proven whole-net VJP cnn_has_vjp_at already covers — dense ∘ GAP ∘ rblkP ∘ rblk ∘ maxPool ∘ cbr(stem). The stem is convBnRelu (SAME conv on the 2h×2w input), one maxpool to h×w, an identity basic block (rblk: relu(F(y)+y)), a projection basic block (rblkP: relu(proj(y)+F(y)), c→oc), global-average-pool, then dense. Each block's skip reuses the block-input subtree in BOTH addV operands, so the graph stays a tree (the §7 "tree-safe via operand leaves" trick, generalized to a computed input). epsStr is the shared ε literal; each BN carries scalar γ/β SSA inputs (%g*/%bt*). The Chapter-5 peer of cifarBnFwdGraph.

                                                                                              Equations
                                                                                              • One or more equations did not get rendered due to their size.
                                                                                              Instances For
                                                                                                source
                                                                                                theorem Proofs.StableHLO.resnetFwdGraph_faithful {ic c oc h w kHs kWs kH₁ kW₁ kH₂ kW₂ kH₁' kW₁' kH₂' kW₂' kHp kWp nClasses : ℕ} (epsStr : String) (Ws : Kernel4 c ic kHs kWs) (bs : Vec c) (εs γs βs : ℝ) (W₁ : Kernel4 c c kH₁ kW₁) (b₁ : Vec c) (W₂ : Kernel4 c c kH₂ kW₂) (b₂ : Vec c) (e₁ g₁ bb₁ e₂ g₂ bb₂ : ℝ) (W₁' : Kernel4 oc c kH₁' kW₁') (b₁' : Vec oc) (W₂' : Kernel4 oc oc kH₂' kW₂') (b₂' : Vec oc) (Wp : Kernel4 oc c kHp kWp) (bp : Vec oc) (f₁ h₁ i₁ f₂ h₂ i₂ fp hp ip : ℝ) (Wd : Mat oc nClasses) (bd : Vec nClasses) (x : Vec (ic * (2 * h) * (2 * w))) :
                                                                                                den (resnetFwdGraph epsStr Ws bs εs γs βs W₁ b₁ W₂ b₂ e₁ g₁ bb₁ e₂ g₂ bb₂ W₁' b₁' W₂' b₂' Wp bp f₁ h₁ i₁ f₂ h₂ i₂ fp hp ip Wd bd x) = cnnForward Ws bs εs γs βs W₁ b₁ W₂ b₂ e₁ g₁ bb₁ e₂ g₂ bb₂ W₁' b₁' W₂' b₂' Wp bp f₁ h₁ i₁ f₂ h₂ i₂ fp hp ip Wd bd x

                                                                                                ResNet-style forward faithfulness. The forward graph denotes the proven cnnForward — the net whose whole-network VJP is cnn_has_vjp_at (discharged unconditionally by CnnConcrete.cnnConcrete_has_vjp_correct). The residual addVs denote the + of residual/residualProj (biPath); each skip's duplicated subtree denotes the same block-input value, so den reads it twice and the fan-in is exact.

                                                                                                source
                                                                                                def Proofs.StableHLO.mobilenetv2FwdGraph {ic c mid₁ oc mid₂ h w kHs kWs kHe₁ kWe₁ kHd₁ kWd₁ kHp₁ kWp₁ kHe₂ kWe₂ kHd₂ kWd₂ kHp₂ kWp₂ nClasses : ℕ} (epsStr : String) (Ws : Kernel4 c ic kHs kWs) (bs : Vec c) (εs γs βs : ℝ) (We₁ : Kernel4 mid₁ c kHe₁ kWe₁) (be₁ : Vec mid₁) (e₁ ge₁ be1 : ℝ) (Wd₁ : DepthwiseKernel mid₁ kHd₁ kWd₁) (bd₁ : Vec mid₁) (d₁ gd₁ bd1 : ℝ) (Wp₁ : Kernel4 c mid₁ kHp₁ kWp₁) (bp₁ : Vec c) (p₁ gp₁ bp1 : ℝ) (We₂ : Kernel4 mid₂ c kHe₂ kWe₂) (be₂ : Vec mid₂) (e₂ ge₂ be2 : ℝ) (Wd₂ : DepthwiseKernel mid₂ kHd₂ kWd₂) (bd₂ : Vec mid₂) (d₂ gd₂ bd2 : ℝ) (Wp₂ : Kernel4 oc mid₂ kHp₂ kWp₂) (bp₂ : Vec oc) (p₂ gp₂ bp2 : ℝ) (Wh : Mat oc nClasses) (bh : Vec nClasses) (x : Vec (ic * h * w)) :
                                                                                                SHlo nClasses

                                                                                                Whole MobileNetV2 forward graph (representative, ch7 peer of resnetFwdGraph): stem (conv→bn→relu6) → skip inverted-residual addV(invresBody, stem) → no-skip inverted-residual → global-average-pool → dense. Each inverted-residual body is bn∘conv(project) ∘ relu6∘bn∘depthwise ∘ relu6∘bn∘conv(expand); the skip's addV reuses the block-input subtree (linear bottleneck — no relu6 after the add). Uses the MobileNetV2 ops relu6F/depthwiseF (SAME-spatial representative; the stride-2 depthwiseStridedF/flatConvStridedF of the full render are exercised at the op level, not assembled here — full strided graph deferred, see planning doc). epsStr = shared ε literal; each scalar BN carries γ/β SSA inputs %g*/%bt*.

                                                                                                Equations
                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                Instances For
                                                                                                  source
                                                                                                  theorem Proofs.StableHLO.mobilenetv2FwdGraph_faithful {ic c mid₁ oc mid₂ h w kHs kWs kHe₁ kWe₁ kHd₁ kWd₁ kHp₁ kWp₁ kHe₂ kWe₂ kHd₂ kWd₂ kHp₂ kWp₂ nClasses : ℕ} (epsStr : String) (Ws : Kernel4 c ic kHs kWs) (bs : Vec c) (εs γs βs : ℝ) (We₁ : Kernel4 mid₁ c kHe₁ kWe₁) (be₁ : Vec mid₁) (e₁ ge₁ be1 : ℝ) (Wd₁ : DepthwiseKernel mid₁ kHd₁ kWd₁) (bd₁ : Vec mid₁) (d₁ gd₁ bd1 : ℝ) (Wp₁ : Kernel4 c mid₁ kHp₁ kWp₁) (bp₁ : Vec c) (p₁ gp₁ bp1 : ℝ) (We₂ : Kernel4 mid₂ c kHe₂ kWe₂) (be₂ : Vec mid₂) (e₂ ge₂ be2 : ℝ) (Wd₂ : DepthwiseKernel mid₂ kHd₂ kWd₂) (bd₂ : Vec mid₂) (d₂ gd₂ bd2 : ℝ) (Wp₂ : Kernel4 oc mid₂ kHp₂ kWp₂) (bp₂ : Vec oc) (p₂ gp₂ bp2 : ℝ) (Wh : Mat oc nClasses) (bh : Vec nClasses) (x : Vec (ic * h * w)) :
                                                                                                  den (mobilenetv2FwdGraph epsStr Ws bs εs γs βs We₁ be₁ e₁ ge₁ be1 Wd₁ bd₁ d₁ gd₁ bd1 Wp₁ bp₁ p₁ gp₁ bp1 We₂ be₂ e₂ ge₂ be2 Wd₂ bd₂ d₂ gd₂ bd2 Wp₂ bp₂ p₂ gp₂ bp2 Wh bh x) = mobilenetv2Forward Ws bs εs γs βs We₁ be₁ e₁ ge₁ be1 Wd₁ bd₁ d₁ gd₁ bd1 Wp₁ bp₁ p₁ gp₁ bp1 We₂ be₂ e₂ ge₂ be2 Wd₂ bd₂ d₂ gd₂ bd2 Wp₂ bp₂ p₂ gp₂ bp2 Wh bh x

                                                                                                  MobileNetV2 forward faithfulness. The representative forward graph denotes the proven mobilenetv2Forward (whose end-to-end VJP at a smooth point is mobilenetv2_has_vjp_at). The skip addV denotes the + of residual/biPath; the inverted-residual body's bn/conv/depthwise/relu6 ops denote invresBody = ivProject ∘ ivDepthwise ∘ ivExpand. ch7 peer of resnetFwdGraph_faithful.

                                                                                                  source
                                                                                                  def Proofs.StableHLO.mobilenetv2FwdGraphFull (epsStr : String) (Ws : Kernel4 16 3 3 3) (bs : Vec 16) (εs γs βs : ℝ) (We1 : Kernel4 64 16 1 1) (be1 : Vec 64) (εe1 γe1 βe1 : ℝ) (Wd1 : DepthwiseKernel 64 3 3) (bd1 : Vec 64) (εd1 γd1 βd1 : ℝ) (Wp1 : Kernel4 24 64 1 1) (bp1 : Vec 24) (εp1 γp1 βp1 : ℝ) (We2 : Kernel4 96 24 1 1) (be2 : Vec 96) (εe2 γe2 βe2 : ℝ) (Wd2 : DepthwiseKernel 96 3 3) (bd2 : Vec 96) (εd2 γd2 βd2 : ℝ) (Wp2 : Kernel4 24 96 1 1) (bp2 : Vec 24) (εp2 γp2 βp2 : ℝ) (We3 : Kernel4 96 24 1 1) (be3 : Vec 96) (εe3 γe3 βe3 : ℝ) (Wd3 : DepthwiseKernel 96 3 3) (bd3 : Vec 96) (εd3 γd3 βd3 : ℝ) (Wp3 : Kernel4 32 96 1 1) (bp3 : Vec 32) (εp3 γp3 βp3 : ℝ) (We4 : Kernel4 128 32 1 1) (be4 : Vec 128) (εe4 γe4 βe4 : ℝ) (Wd4 : DepthwiseKernel 128 3 3) (bd4 : Vec 128) (εd4 γd4 βd4 : ℝ) (Wp4 : Kernel4 32 128 1 1) (bp4 : Vec 32) (εp4 γp4 βp4 : ℝ) (We5 : Kernel4 128 32 1 1) (be5 : Vec 128) (εe5 γe5 βe5 : ℝ) (Wd5 : DepthwiseKernel 128 3 3) (bd5 : Vec 128) (εd5 γd5 βd5 : ℝ) (Wp5 : Kernel4 64 128 1 1) (bp5 : Vec 64) (εp5 γp5 βp5 : ℝ) (We6 : Kernel4 256 64 1 1) (be6 : Vec 256) (εe6 γe6 βe6 : ℝ) (Wd6 : DepthwiseKernel 256 3 3) (bd6 : Vec 256) (εd6 γd6 βd6 : ℝ) (Wp6 : Kernel4 64 256 1 1) (bp6 : Vec 64) (εp6 γp6 βp6 : ℝ) (Wh : Kernel4 128 64 1 1) (bh : Vec 128) (εh γh βh : ℝ) (Wfc : Mat 128 10) (bfc : Vec 10) (x : Vec (3 * 224 * 224)) :
                                                                                                  SHlo 10

                                                                                                  Whole MobileNetV2 forward graph at the FULL ch7 render dims (3×224² → 7×7×64): strided stem (flatConvStridedXlaF, 224→112) → 6 inverted-residual blocks (b1/b3/b5/b6 stride-2 downsample via depthwiseStridedXlaF, b2/b4 stride-1 SAME with an addV skip) → 1×1 conv-bn-relu6 head → global-avg-pool → dense. Concrete (not symbolic) peer of mobilenetv2FwdGraph, tied to the full forward mobilenetv2Forward_full. Scalar BN. ⚠ The five stride-2 sites read the XLA-SAME (odd) phase, like every other MobileNetV2 graph since 2026-09-05; this one is the scalar-BN stepping stone mobilenetv2FwdGraphFullPC replaced, and writes no artifact.

                                                                                                  Equations
                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                  Instances For
                                                                                                    source
                                                                                                    theorem Proofs.StableHLO.mobilenetv2FwdGraphFull_faithful (epsStr : String) (Ws : Kernel4 16 3 3 3) (bs : Vec 16) (εs γs βs : ℝ) (We1 : Kernel4 64 16 1 1) (be1 : Vec 64) (εe1 γe1 βe1 : ℝ) (Wd1 : DepthwiseKernel 64 3 3) (bd1 : Vec 64) (εd1 γd1 βd1 : ℝ) (Wp1 : Kernel4 24 64 1 1) (bp1 : Vec 24) (εp1 γp1 βp1 : ℝ) (We2 : Kernel4 96 24 1 1) (be2 : Vec 96) (εe2 γe2 βe2 : ℝ) (Wd2 : DepthwiseKernel 96 3 3) (bd2 : Vec 96) (εd2 γd2 βd2 : ℝ) (Wp2 : Kernel4 24 96 1 1) (bp2 : Vec 24) (εp2 γp2 βp2 : ℝ) (We3 : Kernel4 96 24 1 1) (be3 : Vec 96) (εe3 γe3 βe3 : ℝ) (Wd3 : DepthwiseKernel 96 3 3) (bd3 : Vec 96) (εd3 γd3 βd3 : ℝ) (Wp3 : Kernel4 32 96 1 1) (bp3 : Vec 32) (εp3 γp3 βp3 : ℝ) (We4 : Kernel4 128 32 1 1) (be4 : Vec 128) (εe4 γe4 βe4 : ℝ) (Wd4 : DepthwiseKernel 128 3 3) (bd4 : Vec 128) (εd4 γd4 βd4 : ℝ) (Wp4 : Kernel4 32 128 1 1) (bp4 : Vec 32) (εp4 γp4 βp4 : ℝ) (We5 : Kernel4 128 32 1 1) (be5 : Vec 128) (εe5 γe5 βe5 : ℝ) (Wd5 : DepthwiseKernel 128 3 3) (bd5 : Vec 128) (εd5 γd5 βd5 : ℝ) (Wp5 : Kernel4 64 128 1 1) (bp5 : Vec 64) (εp5 γp5 βp5 : ℝ) (We6 : Kernel4 256 64 1 1) (be6 : Vec 256) (εe6 γe6 βe6 : ℝ) (Wd6 : DepthwiseKernel 256 3 3) (bd6 : Vec 256) (εd6 γd6 βd6 : ℝ) (Wp6 : Kernel4 64 256 1 1) (bp6 : Vec 64) (εp6 γp6 βp6 : ℝ) (Wh : Kernel4 128 64 1 1) (bh : Vec 128) (εh γh βh : ℝ) (Wfc : Mat 128 10) (bfc : Vec 10) (x : Vec (3 * 224 * 224)) :
                                                                                                    den (mobilenetv2FwdGraphFull epsStr Ws bs εs γs βs We1 be1 εe1 γe1 βe1 Wd1 bd1 εd1 γd1 βd1 Wp1 bp1 εp1 γp1 βp1 We2 be2 εe2 γe2 βe2 Wd2 bd2 εd2 γd2 βd2 Wp2 bp2 εp2 γp2 βp2 We3 be3 εe3 γe3 βe3 Wd3 bd3 εd3 γd3 βd3 Wp3 bp3 εp3 γp3 βp3 We4 be4 εe4 γe4 βe4 Wd4 bd4 εd4 γd4 βd4 Wp4 bp4 εp4 γp4 βp4 We5 be5 εe5 γe5 βe5 Wd5 bd5 εd5 γd5 βd5 Wp5 bp5 εp5 γp5 βp5 We6 be6 εe6 γe6 βe6 Wd6 bd6 εd6 γd6 βd6 Wp6 bp6 εp6 γp6 βp6 Wh bh εh γh βh Wfc bfc x) = mobilenetv2Forward_full Ws bs εs γs βs We1 be1 εe1 γe1 βe1 Wd1 bd1 εd1 γd1 βd1 Wp1 bp1 εp1 γp1 βp1 We2 be2 εe2 γe2 βe2 Wd2 bd2 εd2 γd2 βd2 Wp2 bp2 εp2 γp2 βp2 We3 be3 εe3 γe3 βe3 Wd3 bd3 εd3 γd3 βd3 Wp3 bp3 εp3 γp3 βp3 We4 be4 εe4 γe4 βe4 Wd4 bd4 εd4 γd4 βd4 Wp4 bp4 εp4 γp4 βp4 We5 be5 εe5 γe5 βe5 Wd5 bd5 εd5 γd5 βd5 Wp5 bp5 εp5 γp5 βp5 We6 be6 εe6 γe6 βe6 Wd6 bd6 εd6 γd6 βd6 Wp6 bp6 εp6 γp6 βp6 Wh bh εh γh βh Wfc bfc x

                                                                                                    Full MobileNetV2 forward faithfulness. The full strided render graph denotes the proven mobilenetv2Forward_full (the representative 6-block net, tied by mobilenetv2Rep_denote_eq in SpecVJP.lean — the committed 17-block spec's tie is mobilenetv2Verified_denote_eq there, against mobilenetv2ForwardPaper). simp-based — so unlike the VJP fold it does not hit the concrete-dim isDefEq wall.

                                                                                                    source
                                                                                                    def Proofs.StableHLO.convNextFwdGraph {ic c cExp h w kH kW nClasses : ℕ} (epsStr : String) (Wst : Kernel4 c ic 1 1) (bst : Vec c) (εst γst βst : ℝ) (Wdw₁ : DepthwiseKernel c kH kW) (bdw₁ : Vec c) (εn₁ γn₁ βn₁ : ℝ) (Wex₁ : Kernel4 cExp c 1 1) (bex₁ : Vec cExp) (Wpr₁ : Kernel4 c cExp 1 1) (bpr₁ : Vec c) (γls₁ : Vec (c * h * w)) (Wdw₂ : DepthwiseKernel c kH kW) (bdw₂ : Vec c) (εn₂ γn₂ βn₂ : ℝ) (Wex₂ : Kernel4 cExp c 1 1) (bex₂ : Vec cExp) (Wpr₂ : Kernel4 c cExp 1 1) (bpr₂ : Vec c) (γls₂ : Vec (c * h * w)) (εhd γhd βhd : ℝ) (Wd : Mat c nClasses) (bd : Vec nClasses) (x : Vec (ic * h * w)) :
                                                                                                    SHlo nClasses

                                                                                                    Whole ConvNeXt forward graph (representative, ch9 peer of resnetFwdGraph): 1×1 patchify conv → stem-LN → 2 residual ConvNeXt blocks (depthwise → LN → 1×1 expand → GELU → 1×1 project → layerScale, then addV skip) → GAP → head-LN → dense. Scalar LN (= bnForward, via bnF); uses geluF + the new layerScaleF. Denotes the proven convNextForward.

                                                                                                    Equations
                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                    Instances For
                                                                                                      source
                                                                                                      theorem Proofs.StableHLO.convNextFwdGraph_faithful {ic c cExp h w kH kW nClasses : ℕ} (epsStr : String) (Wst : Kernel4 c ic 1 1) (bst : Vec c) (εst γst βst : ℝ) (Wdw₁ : DepthwiseKernel c kH kW) (bdw₁ : Vec c) (εn₁ γn₁ βn₁ : ℝ) (Wex₁ : Kernel4 cExp c 1 1) (bex₁ : Vec cExp) (Wpr₁ : Kernel4 c cExp 1 1) (bpr₁ : Vec c) (γls₁ : Vec (c * h * w)) (Wdw₂ : DepthwiseKernel c kH kW) (bdw₂ : Vec c) (εn₂ γn₂ βn₂ : ℝ) (Wex₂ : Kernel4 cExp c 1 1) (bex₂ : Vec cExp) (Wpr₂ : Kernel4 c cExp 1 1) (bpr₂ : Vec c) (γls₂ : Vec (c * h * w)) (εhd γhd βhd : ℝ) (Wd : Mat c nClasses) (bd : Vec nClasses) (x : Vec (ic * h * w)) :
                                                                                                      den (convNextFwdGraph epsStr Wst bst εst γst βst Wdw₁ bdw₁ εn₁ γn₁ βn₁ Wex₁ bex₁ Wpr₁ bpr₁ γls₁ Wdw₂ bdw₂ εn₂ γn₂ βn₂ Wex₂ bex₂ Wpr₂ bpr₂ γls₂ εhd γhd βhd Wd bd x) = convNextForward Wst bst εst γst βst Wdw₁ bdw₁ εn₁ γn₁ βn₁ Wex₁ bex₁ Wpr₁ bpr₁ γls₁ Wdw₂ bdw₂ εn₂ γn₂ βn₂ Wex₂ bex₂ Wpr₂ bpr₂ γls₂ εhd γhd βhd Wd bd x

                                                                                                      ConvNeXt forward faithfulness. The representative forward graph denotes the proven convNextForward. Scalar LN (layerNormForward = bnForward); simp-based.

                                                                                                      source
                                                                                                      theorem Proofs.StableHLO.hasVJPAt_backward_det {m n : ℕ} {f : Vec m → Vec n} {x : Vec m} (v v' : HasVJPAt f x) (dy : Vec n) :
                                                                                                      v.backward dy = v'.backward dy

                                                                                                      Pointwise-VJP backwards are unique: .correct pins backward to the pdiv-contracted Jacobian, so any two HasVJPAt f x agree on backward. Lets us swap the maxpool's flatten∘unflatten transport (built into mnistCnnNoBn_has_vjp_at) for the cast-free witness below.

                                                                                                      source
                                                                                                      noncomputable def Proofs.StableHLO.maxPoolFlat_has_vjp_at' {c h w : ℕ} (v : Vec (c * (2 * h) * (2 * w))) (hs : MaxPool2Smooth (Tensor3.unflatten v)) :
                                                                                                      HasVJPAt (maxPoolFlat c h w) v

                                                                                                      Max-pool VJP at a raw flattened point (no flatten ∘ unflatten index), so it composes without a transport cast; backward is maxPoolBackFlat. The correct field reuses maxPoolFlat_has_vjp_at.correct, aligning the point via Tensor3.flatten_unflatten.

                                                                                                      Equations
                                                                                                      Instances For
                                                                                                        source
                                                                                                        @[simp]
                                                                                                        theorem Proofs.StableHLO.maxPoolFlat_has_vjp_at'_backward {c h w : ℕ} (v : Vec (c * (2 * h) * (2 * w))) (hs : MaxPool2Smooth (Tensor3.unflatten v)) :
                                                                                                        (maxPoolFlat_has_vjp_at' v hs).backward = maxPoolBackFlat c h w v
                                                                                                        source
                                                                                                        noncomputable def Proofs.StableHLO.cnnBackGraph {ic c h w d1 nClasses kH kW : ℕ} (W₁ : Kernel4 c ic kH kW) (b₁ : Vec c) (W₂ : Kernel4 c c kH kW) (b₂ : Vec c) (W₃ : Mat (c * h * w) d1) (b₃ : Vec d1) (W₄ : Mat d1 d1) (b₄ : Vec d1) (W₅ : Mat d1 nClasses) (x : Vec (ic * (2 * h) * (2 * w))) (dy : Vec nClasses) :
                                                                                                        SHlo (ic * (2 * h) * (2 * w))

                                                                                                        Whole MNIST-CNN backward (input-VJP) graph, reversing cnnFwdGraph: convBack W₁ ∘ select(a₁) ∘ convBack W₂ ∘ select(a₂) ∘ maxPoolBack ∘ dotOut W₃ ∘ select(a₃) ∘ dotOut W₄ ∘ select(a₄) ∘ dotOut W₅, with aᵢ the ReLU pre-activations and the conv/maxpool saved inputs threaded as in §4.

                                                                                                        Equations
                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                        Instances For
                                                                                                          source
                                                                                                          theorem Proofs.StableHLO.cnnBackGraph_faithful {ic c h w d1 nClasses kH kW : ℕ} (W₁ : Kernel4 c ic kH kW) (b₁ : Vec c) (W₂ : Kernel4 c c kH kW) (b₂ : Vec c) (W₃ : Mat (c * h * w) d1) (b₃ : Vec d1) (W₄ : Mat d1 d1) (b₄ : Vec d1) (W₅ : Mat d1 nClasses) (b₅ : Vec nClasses) (hc : 0 < c) (hh : 0 < h) (hw : 0 < w) (x : Vec (ic * (2 * h) * (2 * w))) (h1 : ∀ (k : Fin (c * (2 * h) * (2 * w))), flatConv W₁ b₁ x k ≠ 0) (h2 : ∀ (k : Fin (c * (2 * h) * (2 * w))), flatConv W₂ b₂ ((relu (c * (2 * h) * (2 * w)) ∘ flatConv W₁ b₁) x) k ≠ 0) (h_mp : MaxPool2Smooth (Tensor3.unflatten (((relu (c * (2 * h) * (2 * w)) ∘ flatConv W₂ b₂) ∘ relu (c * (2 * h) * (2 * w)) ∘ flatConv W₁ b₁) x))) (h3 : ∀ (k : Fin d1), dense W₃ b₃ (maxPoolFlat c h w (((relu (c * (2 * h) * (2 * w)) ∘ flatConv W₂ b₂) ∘ relu (c * (2 * h) * (2 * w)) ∘ flatConv W₁ b₁) x)) k ≠ 0) (h4 : ∀ (k : Fin d1), dense W₄ b₄ ((relu d1 ∘ dense W₃ b₃) (maxPoolFlat c h w (((relu (c * (2 * h) * (2 * w)) ∘ flatConv W₂ b₂) ∘ relu (c * (2 * h) * (2 * w)) ∘ flatConv W₁ b₁) x))) k ≠ 0) (dy : Vec nClasses) :
                                                                                                          den (cnnBackGraph W₁ b₁ W₂ b₂ W₃ b₃ W₄ b₄ W₅ x dy) = (mnistCnnNoBn_has_vjp_at W₁ b₁ W₂ b₂ W₃ b₃ W₄ b₄ W₅ b₅ hc hh hw x h1 h2 h_mp h3 h4).backward dy
                                                                                                          source
                                                                                                          def Proofs.StableHLO.ty (dims : List ℕ) :
                                                                                                          String

                                                                                                          Tensor-type string tensor<d₀x…xf32>.

                                                                                                          Equations
                                                                                                          Instances For
                                                                                                            source
                                                                                                            def Proofs.StableHLO.tyI1 (dims : List ℕ) :
                                                                                                            String

                                                                                                            Boolean (i1) tensor-type string, for compare/select masks.

                                                                                                            Equations
                                                                                                            Instances For
                                                                                                              source
                                                                                                              def Proofs.StableHLO.tyBf16 (dims : List ℕ) :
                                                                                                              String

                                                                                                              bf16 tensor-type string, for the convertF round node (planning/archive/bf16_renderer.md). Only the round trip uses it today; when a bf16-operand dot_general lands (rung 2+) this is the type its operands carry.

                                                                                                              Equations
                                                                                                              Instances For
                                                                                                                source
                                                                                                                def Proofs.StableHLO.tyF8 (dims : List ℕ) :
                                                                                                                String

                                                                                                                fp8 peer of tyBf16. E4M3 only — planning/archive/cifar_lowprec_stability.md §2.3 measured that f8E5M2 compiles, lowers to a plain __cublas$lt$matmul, and leaves ZERO f8e5m2 values in the optimized HLO: the type is silently widened away. Only E4M3 reaches the fp8 units on sm_89, so there is deliberately no E5M2 spelling here.

                                                                                                                Equations
                                                                                                                Instances For
                                                                                                                  source
                                                                                                                  @[reducible, inline]
                                                                                                                  abbrev Proofs.StableHLO.ShapeTbl :
                                                                                                                  Type

                                                                                                                  SSA name ↦ the [c,h,w] the value bound to that name really carries. See liftPointwise.

                                                                                                                  ⚠⚠ Keyed by NAME, not by flat width — and that is not a refinement, it is the whole correctness of the table. A width table collides whenever two layers have the same element count, and on the real nets they do: ConvNeXt-T's stage-2 MLP is 1536·14·14 = 301056 and its stage-0 block is 96·56·56 = 301056; stage 3's 3072·7·7 equals stage 1's 192·28·28. First writer won, so 24 of ConvNeXt's pointwise blocks unflattened to a shape with the right element count and the wrong layout — which is not a wrong program (the bracket is still an inverse reshape pair) but is exactly the relayout the bracket exists to remove. Measured: 2.434 GB of transposes and 84.45 ms/step keyed by width, 0.122 GB and 68.28 ms keyed by name.

                                                                                                                  Newest entry first, and no dedup: fresh never reuses a name, so a lookup for a value the previous token produced hits the head of the list.

                                                                                                                  ⚠⚠ The Bool is the value's LAYOUT: true means this is the map's row view [h·w, c] rather than the map [c, h, w]. It is not bookkeeping — it is what makes ConvNeXt's channel-LN transparent. That chain is transpose → lnRow → rowScale → rowBias → transpose, a layout ROUND TRIP whose two ends are the same [c,h,w] map; without the flag the closing transpose's result has no entry, the drop-path multiply that consumes it falls back to flat, and every pointwise op after it on the residual chain goes with it — 0.223 GB of relayout against 0.122 (measured, ConvNeXt-T bf16). And liftPointwise must NOT fire on a row view: [h·w, c] reshaped to [B,c,h,w] is a DIFFERENT permutation, not an inverse pair, so that one would be a wrong program rather than a slow one.

                                                                                                                  Equations
                                                                                                                  Instances For
                                                                                                                    source
                                                                                                                    @[reducible, inline]
                                                                                                                    abbrev Proofs.StableHLO.EmitS :
                                                                                                                    Type

                                                                                                                    Emitter state: the fresh-name counter, plus the name ↦ [c,h,w] table.

                                                                                                                    ⚠ The table lives in the STATE rather than in a pretty argument because a net renderer calls pretty once per graph FRAGMENT — a conv and the activation that consumes it land in different calls — and only the state is threaded across them.

                                                                                                                    Equations
                                                                                                                    Instances For
                                                                                                                      source
                                                                                                                      def Proofs.StableHLO.fresh :
                                                                                                                      StateM EmitS String

                                                                                                                      Fresh SSA name %v{k}.

                                                                                                                      Equations
                                                                                                                      Instances For
                                                                                                                        source
                                                                                                                        def Proofs.StableHLO.maxPool3s2FwdText (B c h w : ℕ) (r xn ninf p o : String) :
                                                                                                                        String

                                                                                                                        The 3×3/s2 pool's emitted forward text, given already-freshened names.

                                                                                                                        ⚠⚠ It is a shared helper rather than two copies for the reason sWGradGeom is (§2f-bis): the per-example .maxPool3s2F and the batched BatchableOp.maxPool3s2 are two emitTok arms emitting one program, and a window or padding that drifted between them would be a pair of renders that agree on every structural check and compute different functions — which is the exact failure this whole op exists to fix. With one writer they cannot drift, and TestBatchedEmitTie then measures rather than assumes it.

                                                                                                                        window_dimensions = 3, window_strides = 2, padding = [[1,1],[1,1]] on the spatial axes: He et al./torchvision MaxPool2d(3, stride=2, padding=1), window i = input [2i−1, 2i+1]. ⚠ NOT XLA 'SAME', which pads (0,1) and slides the grid one input position — the two are different functions everywhere.

                                                                                                                        Equations
                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                        Instances For
                                                                                                                          source
                                                                                                                          def Proofs.StableHLO.maxPool3s2BackText (B c h w : ℕ) (xN r xr dr z scn o : String) :
                                                                                                                          String

                                                                                                                          The 3×3/s2 pool's emitted backward text, given already-freshened names. Shared by the per-example and batched arms, for maxPool3s2FwdText's reason.

                                                                                                                          ⭐ Only the window attributes differ from maxPoolBack's emit — nothing else — because select_and_scatter's scatter region already reduces with add, which is exactly the accumulation overlapping windows need. The emitter was general enough before the op existed.

                                                                                                                          ⚠ %sa/%sb/%sc/%sd are hardcoded region block arguments and are therefore RESERVED SSA names (§4): a top-level value of the same name is a redefinition error that surfaces only at XLA compile time.

                                                                                                                          Equations
                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                          Instances For
                                                                                                                            source
                                                                                                                            def Proofs.StableHLO.dpName (i : ℕ) :
                                                                                                                            String

                                                                                                                            The stochastic-depth mask input name for ramp index i — the mName a dropPathB carries, and the tensor<Bxf32> the signature declares for it.

                                                                                                                            ⚠ It lives HERE, beside the emitter, rather than in one net's renderer, because the spelling is load-bearing in three places that must agree and only one of them is Lean: dropPathP's emit reads it as an operand, every SD render's signature declares it, and scripts/misplace_drop_sites.py matches %dp\d+ textually to build the placement control. A second definition would be the double-writer disease with a committed shell script as the third writer. (It started in EfficientNetRender.lean and moved when ConvNeXt needed it too; both renderers are in this namespace, so no call site changed and no artifact byte moved.)

                                                                                                                            Equations
                                                                                                                            Instances For
                                                                                                                              source
                                                                                                                              def Proofs.StableHLO.doName :
                                                                                                                              String

                                                                                                                              The classifier-dropout mask input name — the mName a dropoutB carries, and the tensor<B×n×f32> the signature declares for it.

                                                                                                                              ⚠⚠ IT IS DELIBERATELY NOT %dp{i}-SHAPED, and that is not cosmetic. scripts/misplace_drop_sites.py builds the stochastic-depth placement control by matching %dp\d+ textually; a dropout input spelled %dp9 would be swept into that rewrite, silently changing a control's meaning on a render it was never written for. Handoff §0.11 records the other half of this hazard on ViT — a control that quietly does nothing reads exactly like a control that ran — and the cheap defence is a name the SD tooling cannot match. grep -c '%do' verified_mlir/*.mlir is 0 across every committed artifact.

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

                                                                                                                                The renderable skeleton of an SHlo graph: opcodes + shapes + leaf SSA names, with ℝ operand values and the shape index erased — exactly what reaches the emitted text.

                                                                                                                                Instances For
                                                                                                                                  source
                                                                                                                                  @[implicit_reducible]
                                                                                                                                  instance Proofs.StableHLO.instDecidableEqRaw :
                                                                                                                                  DecidableEq Raw
                                                                                                                                  Equations
                                                                                                                                  source
                                                                                                                                  def Proofs.StableHLO.instDecidableEqRaw.decEq (x✝ x✝¹ : Raw) :
                                                                                                                                  Decidable (x✝ = x✝¹)
                                                                                                                                  Instances For
                                                                                                                                    source
                                                                                                                                    @[implicit_reducible]
                                                                                                                                    instance Proofs.StableHLO.instReprRaw :
                                                                                                                                    Repr Raw
                                                                                                                                    Equations
                                                                                                                                    source
                                                                                                                                    def Proofs.StableHLO.instReprRaw.repr :
                                                                                                                                    Raw → ℕ → Std.Format
                                                                                                                                    Instances For
                                                                                                                                      source
                                                                                                                                      @[implicit_reducible]
                                                                                                                                      instance Proofs.StableHLO.instInhabitedRaw :
                                                                                                                                      Inhabited Raw
                                                                                                                                      Equations
                                                                                                                                      source
                                                                                                                                      def Proofs.StableHLO.batchOpDescr {a b : ℕ} (N : ℕ) :
                                                                                                                                      BatchableOp a b → String × List String × List ℕ

                                                                                                                                      The (tag, names, info) skeleton descriptor of a batched per-example op — the discriminator + the SSA names the emit references + the shape dims. Keeps the batchOp skel one line and isolates the 7-variant match into a pure function.

                                                                                                                                      Equations
                                                                                                                                      Instances For
                                                                                                                                        source
                                                                                                                                        def Proofs.StableHLO.skel {k : ℕ} :
                                                                                                                                        SHlo k → Raw

                                                                                                                                        Erase an SHlo graph to its renderable skeleton (drops ℝ values + shape index; keeps op structure, shapes, leaf names).

                                                                                                                                        Instances For
                                                                                                                                          source
                                                                                                                                          inductive Proofs.StableHLO.Tok :
                                                                                                                                          Type

                                                                                                                                          One serialized token: an opcode with shapes/names; operands are positional.

                                                                                                                                          Instances For
                                                                                                                                            source
                                                                                                                                            @[implicit_reducible]
                                                                                                                                            instance Proofs.StableHLO.instDecidableEqTok :
                                                                                                                                            DecidableEq Tok
                                                                                                                                            Equations
                                                                                                                                            source
                                                                                                                                            def Proofs.StableHLO.instDecidableEqTok.decEq (x✝ x✝¹ : Tok) :
                                                                                                                                            Decidable (x✝ = x✝¹)
                                                                                                                                            Equations
                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                            Instances For
                                                                                                                                              source
                                                                                                                                              @[implicit_reducible]
                                                                                                                                              instance Proofs.StableHLO.instReprTok :
                                                                                                                                              Repr Tok
                                                                                                                                              Equations
                                                                                                                                              source
                                                                                                                                              def Proofs.StableHLO.instReprTok.repr :
                                                                                                                                              Tok → ℕ → Std.Format
                                                                                                                                              Equations
                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                              Instances For
                                                                                                                                                source
                                                                                                                                                def Proofs.StableHLO.toToks :
                                                                                                                                                Raw → List Tok

                                                                                                                                                Postorder serialization: children, then the node's opcode token.

                                                                                                                                                Equations
                                                                                                                                                Instances For
                                                                                                                                                  source
                                                                                                                                                  def Proofs.StableHLO.lookupEntry (tbl : ShapeTbl) (nm : String) :
                                                                                                                                                  Option (ℕ × ℕ × ℕ × Bool)

                                                                                                                                                  The full entry — [c,h,w] plus the row-view flag — recorded for SSA name nm.

                                                                                                                                                  Equations
                                                                                                                                                  Instances For
                                                                                                                                                    source
                                                                                                                                                    def Proofs.StableHLO.lookupShape (tbl : ShapeTbl) (nm : String) :
                                                                                                                                                    Option (ℕ × ℕ × ℕ)

                                                                                                                                                    The [c,h,w] nm carries as a map. A row view answers none: it holds the same elements in a different order, so unflattening it to [B,c,h,w] would not be an inverse pair.

                                                                                                                                                    Equations
                                                                                                                                                    Instances For
                                                                                                                                                      source
                                                                                                                                                      def Proofs.StableHLO.noteEntry (nm : String) :
                                                                                                                                                      Option (ℕ × ℕ × ℕ × Bool) → StateM EmitS Unit

                                                                                                                                                      Record nm ↦ [c,h,w] + layout, newest first. fresh never reuses a name, so an entry can never be contradicted by a later one; an .operand name re-pushed in a later fragment repeats.

                                                                                                                                                      Equations
                                                                                                                                                      Instances For
                                                                                                                                                        source
                                                                                                                                                        def Proofs.StableHLO.noteShapeOf (nm : String) :
                                                                                                                                                        Option (ℕ × ℕ × ℕ) → StateM EmitS Unit

                                                                                                                                                        Record nm as carrying the [c,h,w] MAP (not a row view).

                                                                                                                                                        Equations
                                                                                                                                                        Instances For
                                                                                                                                                          source
                                                                                                                                                          def Proofs.StableHLO.lookupShapeM (nm : String) :
                                                                                                                                                          StateM EmitS (Option (ℕ × ℕ × ℕ))

                                                                                                                                                          The [c,h,w] the running table has for the value bound to nm, as a map.

                                                                                                                                                          Equations
                                                                                                                                                          Instances For
                                                                                                                                                            source
                                                                                                                                                            def Proofs.StableHLO.lookupEntryM (nm : String) :
                                                                                                                                                            StateM EmitS (Option (ℕ × ℕ × ℕ × Bool))

                                                                                                                                                            The full entry the running table has for nm.

                                                                                                                                                            Equations
                                                                                                                                                            Instances For
                                                                                                                                                              source
                                                                                                                                                              def Proofs.StableHLO.noteTokShapes (t : Tok) (before after : List String) :
                                                                                                                                                              StateM EmitS Unit

                                                                                                                                                              Record what one token's operand and result carry, given the operand-name stack before and after it was emitted. Called from serializeToks, so no emitTok arm has to know about the table — which is what keeps the 94 arms free of it.

                                                                                                                                                              ⭐ Three cases, and the first two exist only for the channel-LN round trip: a transpose FLIPS the layout flag when its (m,n) match the operand's [c,h,w] (and records nothing when they do not, e.g. ViT's attention transposes, which are not maps at all), and the row ops carry it through unchanged. Everything else reads its shapes off the tag.

                                                                                                                                                              Equations
                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                              Instances For
                                                                                                                                                                source
                                                                                                                                                                def Proofs.StableHLO.liftPointwise (B n : ℕ) (r : String) (k : String → List ℕ → StateM EmitS (String × String)) :
                                                                                                                                                                StateM EmitS (String × String)

                                                                                                                                                                Render a pointwise block at its 4-D shape when the OPERAND's producer recorded one. k receives the (possibly unflattened) input name and the dims to type its ops with, and returns (text, result name).

                                                                                                                                                                ⚠ The c*h*w == n guard is what keeps a mismatched entry from emitting an ill-typed reshape rather than merely a suboptimal one. It cannot fire today — an entry is written by the token that produced the name — and it is the difference between a missed optimisation and a render that does not parse, so it stays.

                                                                                                                                                                ⭐ The block's own RESULT is recorded too, which is what lets a pointwise CHAIN stay 4-D: the value crossing the token boundary keeps its flat type, so without this the second op in a swish→multiply→add chain would find nothing for its operand and drop back to flat.

                                                                                                                                                                Equations
                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                Instances For
                                                                                                                                                                  source
                                                                                                                                                                  def Proofs.StableHLO.liftPointwise2 (B n : ℕ) (r s : String) (k : String → String → List ℕ → StateM EmitS (String × String)) :
                                                                                                                                                                  StateM EmitS (String × String)

                                                                                                                                                                  Two-tensor-operand peer of liftPointwise; both operands carry the same flat width. The shape comes from whichever operand has one — the cotangent first, since it is the stack operand and was produced nearby, then the saved activation.

                                                                                                                                                                  Equations
                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                  Instances For
                                                                                                                                                                    source
                                                                                                                                                                    def Proofs.StableHLO.allReduceMeanText (g : String) (ds : List ℕ) (t : String) (R : ℕ) :
                                                                                                                                                                    String × String

                                                                                                                                                                    The text of the cross-replica mean — ViTRender.emitGradAllReduce's body, verbatim, so that the allReduceMean token re-renders every committed *dp* artifact byte-identically. all_reduce(add) over replica_groups = [[0..R-1]], then a divide by R; the names are %arsum{t} … %armean{t} from the tag rather than fresh. At R ≤ 1 there is no text and the operand's name is the result, exactly as the text function did.

                                                                                                                                                                    Equations
                                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                                    Instances For
                                                                                                                                                                      source
                                                                                                                                                                      def Proofs.StableHLO.emitTok (B : ℕ) :
                                                                                                                                                                      Tok → List String → StateM EmitS (String × List String)

                                                                                                                                                                      Render one token: pop its operands' result-names off the stack, emit its StableHLO line(s), push its fresh result name. The per-op StableHLO syntax here is the audited lexical boundary (validated by iree-compile + GPU run); the structure it consumes is the proven-faithful token stream.

                                                                                                                                                                      Instances For
                                                                                                                                                                        source
                                                                                                                                                                        def Proofs.StableHLO.serializeToks (B : ℕ) :
                                                                                                                                                                        List Tok → String × List String → StateM EmitS (String × List String)

                                                                                                                                                                        Fold a token stream to accumulated (code, result-name-stack).

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

                                                                                                                                                                          The conv-bias SSA name — §2l step B. 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 (§2k).

                                                                                                                                                                          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.

                                                                                                                                                                          ⚠ MEASURED, and it corrects §2l's stated reason: in f32 the gradient is NOT exactly zero — the BN mean is a rounded sum, leaving a residue ~1e-6 of the conv-weight gradient — and under AdamW's scale-free update that residue still moves θ by ~lr per step. In the 80-epoch run all 8,512 biases drifted to |θ|max 0.041. They are safe to drop because the FORWARD does not depend on them (zeroing all of them moves the trained logits by rel 1e-6, against 0.79 for the same ablation on BN β), not because they stay zero. See tests/TestConvBiasZero.lean.

                                                                                                                                                                          Equations
                                                                                                                                                                          Instances For
                                                                                                                                                                            source
                                                                                                                                                                            def Proofs.StableHLO.biasSlot (convBias : Bool) (nm : String) :
                                                                                                                                                                            List String

                                                                                                                                                                            The bias's slot in a return-name list, gated the way biasName gates the operand: with convBias := false no bias SGD op is emitted, so the slot must LEAVE the list rather than carry the empty string the if convBias then … else pure ("", "") idiom hands back.

                                                                                                                                                                            ⚠ This exists because leaving it in is silent twice over. An empty name renders return %a, , %b — malformed text, but only the lowerer ever sees it; and the name list keeps its FULL length, so an arity #guard on the signature still passes. Measured on the first swap attempt: mobilenetv2_train_step at convBias := false returned 210 names (52 of them empty) against 160 types. Use this at every site where a names := [...] list is built from gated ops.

                                                                                                                                                                            Equations
                                                                                                                                                                            Instances For
                                                                                                                                                                              source
                                                                                                                                                                              def Proofs.StableHLO.zeroBiasPrelude (convBias : Bool) (widths : List ℕ) :
                                                                                                                                                                              String

                                                                                                                                                                              The zero-bias constants the convBias := false render consumes, one per channel width used as a conv bias. Emitted once at the top of the body; XLA folds the resulting add.

                                                                                                                                                                              Equations
                                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                                              Instances For
                                                                                                                                                                                source
                                                                                                                                                                                def Proofs.StableHLO.fmt6 (x : Float) :
                                                                                                                                                                                String

                                                                                                                                                                                Fixed-6-decimal float literal, so a computed smoothing constant emits in the SAME textual form the hand-written literals used and nClasses = 10 re-renders byte-identical.

                                                                                                                                                                                Equations
                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                Instances For
                                                                                                                                                                                  source
                                                                                                                                                                                  def Proofs.StableHLO.fmt12 (x : Float) :
                                                                                                                                                                                  String

                                                                                                                                                                                  Fixed-12-decimal float literal, for constants fmt6 would destroy.

                                                                                                                                                                                  ⚠ It exists because fmt6 is not a formatting preference, it is a PRECISION CEILING, and small derived constants fall straight through it. Gradient accumulation's second-moment coefficient is (1−β₂)/K²; at K = 4 that is 6.25e-5, which fmt6 emits as 0.000063 — 0.8% wrong, in a baked literal, in the optimizer, where nothing downstream would question it. Same class as §2k's hardcoded 0.010000 label-smoothing mass. fmt6 stays the default so every committed artifact re-renders byte-identically; this is for constants that need the room.

                                                                                                                                                                                  Equations
                                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                                  Instances For
                                                                                                                                                                                    source
                                                                                                                                                                                    def Proofs.StableHLO.alphaOverK (nClasses : ℕ) (alpha : Float := 0.1) :
                                                                                                                                                                                    String

                                                                                                                                                                                    The label-smoothing mass per class, α/K. α = 0.1 throughout; K is nClasses.

                                                                                                                                                                                    ⚠ This was hardcoded 0.010000 — correct at K = 10 and WRONG at every other K, and it sat in the COTANGENT, not just in the report-only %loss. At nClasses = 1000 it made the smoothing term 100× too large: it removes 10.0 of probability mass instead of 0.1, i.e. a different objective, silently. Caught 2026-07-30 by the first ImageNet smoke run reporting loss ≈ 87 where 1000-class CE at init must be ≈ ln(1000) = 6.9 — the number was implausible, and that is the only reason it surfaced. Nothing in the repo's proofs covers it: α is a literal in emitted text, which is exactly the carve-out class §5 says needs its own numeric check, and §2b's %loss bug is the standing precedent for it going wrong unnoticed.

                                                                                                                                                                                    Equations
                                                                                                                                                                                    Instances For
                                                                                                                                                                                      source
                                                                                                                                                                                      def Proofs.StableHLO.oneMinusAlpha (alpha : Float := 0.1) :
                                                                                                                                                                                      String

                                                                                                                                                                                      1 − α, the ON-class weight of label-smoothed CE. Emitted beside alphaOverK, because the two always move together and splitting them is how one of them gets updated alone.

                                                                                                                                                                                      Equations
                                                                                                                                                                                      Instances For
                                                                                                                                                                                        source
                                                                                                                                                                                        def Proofs.StableHLO.oneMinusRho (rho : Float) :
                                                                                                                                                                                        String

                                                                                                                                                                                        1 − ρ, the RMSProp mean-square mixing weight. Derived from ρ, never written as a second literal beside it — the oneMinusAlpha precedent, and the K-constant lesson (§2k): any emitted constant that depends on a hyperparameter must be DERIVED, because the copy is what gets left behind when the original moves. Five copies of one label-smoothing constant were found across four nets in a single session for exactly this reason.

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

                                                                                                                                                                                          Which optimizer tail a whole-net render emits. .adamw is every net's committed default and reproduces the existing artifacts byte-identically; .rmsprop is what the MobileNetV2 and EfficientNet ImageNet references actually use (planning/archive/recipe_gaps.md v1.2).

                                                                                                                                                                                          Lives here rather than in either renderer because both need it: a per-net copy of a two-constructor choice is the double-writer disease one level down, in code — the same argument vitBackAll/enetBackAll exist for (§2a-quater). Each renderer threads it through ONE traversal, so gate 1 applies for free: at .adamw every committed artifact must re-render byte-identical.

                                                                                                                                                                                          Instances For
                                                                                                                                                                                            source
                                                                                                                                                                                            @[implicit_reducible]
                                                                                                                                                                                            instance Proofs.StableHLO.instDecidableEqOptKind :
                                                                                                                                                                                            DecidableEq OptKind
                                                                                                                                                                                            Equations
                                                                                                                                                                                            source
                                                                                                                                                                                            def Proofs.StableHLO.instReprOptKind.repr :
                                                                                                                                                                                            OptKind → ℕ → Std.Format
                                                                                                                                                                                            Equations
                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                            Instances For
                                                                                                                                                                                              source
                                                                                                                                                                                              @[implicit_reducible]
                                                                                                                                                                                              instance Proofs.StableHLO.instReprOptKind :
                                                                                                                                                                                              Repr OptKind
                                                                                                                                                                                              Equations
                                                                                                                                                                                              source
                                                                                                                                                                                              structure Proofs.StableHLO.RmsHyper :
                                                                                                                                                                                              Type

                                                                                                                                                                                              The RMSProp hyperparameters, as the JAX reference configs state them. ρ/μ are 0.9 on both nets that use this optimizer; ε and wd are what differ, and ε differs in the way that matters most (see Proofs.rmsBufNext_eps_placement_at_zero).

                                                                                                                                                                                              • rho : Float

                                                                                                                                                                                                rmspropDecay — the running mean-square decay.

                                                                                                                                                                                              • mu : Float

                                                                                                                                                                                                momentum — μ for the buffer on the normalised gradient.

                                                                                                                                                                                              • eps : Float

                                                                                                                                                                                                rmspropEps — ⚠ emitted INSIDE the square root (TensorFlow), not added to the root.

                                                                                                                                                                                              • wd : Float

                                                                                                                                                                                                COUPLED L2 (folded into the gradient), not AdamW's decoupled decay.

                                                                                                                                                                                              Instances For
                                                                                                                                                                                                source
                                                                                                                                                                                                def Proofs.StableHLO.rmsConstsBlock (h : RmsHyper) :
                                                                                                                                                                                                String

                                                                                                                                                                                                ρ / (1−ρ) / μ / ε / wd as graph constants — the RMSProp peer of each renderer's adamConsts block. %lr stays a runtime tensor<f32> arg so one graph serves a whole LR schedule.

                                                                                                                                                                                                Equations
                                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                Instances For
                                                                                                                                                                                                  source
                                                                                                                                                                                                  def Proofs.StableHLO.mnv2RmsHyper :
                                                                                                                                                                                                  RmsHyper

                                                                                                                                                                                                  MobileNetV2's RMSProp knobs (jax/MainMobilenetV2Imagenet.lean): ε = 1.0.

                                                                                                                                                                                                  Equations
                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                    source
                                                                                                                                                                                                    def Proofs.StableHLO.enetRmsHyper :
                                                                                                                                                                                                    RmsHyper

                                                                                                                                                                                                    EfficientNet-B0's RMSProp knobs (jax/MainEfficientNetImagenet.lean): ε = 1e-3.

                                                                                                                                                                                                    Equations
                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                      source
                                                                                                                                                                                                      def Proofs.StableHLO.pretty (B : ℕ) {k : ℕ} (g : SHlo k) :
                                                                                                                                                                                                      StateM EmitS (String × String)

                                                                                                                                                                                                      pretty — render an SHlo graph to StableHLO, now defined as serialize ∘ toToks ∘ skel: tokenize the graph (postorder), then print the tokens. The emitter shares ONE structured form with the parser, so the round-trip parse (toToks (skel a)) = skel a (StableHLOParse.lean) is about the very tokens this prints — the printer can't structurally drift.

                                                                                                                                                                                                      Equations
                                                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                        source
                                                                                                                                                                                                        def Proofs.StableHLO.prettyAllReduceMean (grad : String) (ds : List ℕ) (t : String) (replicas : ℕ) :
                                                                                                                                                                                                        StateM EmitS (String × String)

                                                                                                                                                                                                        The cross-replica gradient mean as pretty of the allReduceMeanF node — the drop-in for ViTRender.emitGradAllReduce in every batched render (4d piece 2, 2026-09-07), measured byte-identical on every committed *dp* artifact. At replicas ≤ 1 it emits nothing and threads the gradient's name, exactly as the text function did. The R operand graphs are all .operand grad at a zero placeholder, because a render is value-independent — skel erases values — while the family is what den sums over in the tie.

                                                                                                                                                                                                        Equations
                                                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                          source
                                                                                                                                                                                                          def Proofs.StableHLO.renderModule (name argSig : String) (B retLen : ℕ) (g : SHlo retLen) :
                                                                                                                                                                                                          String

                                                                                                                                                                                                          Wrap a rendered single-result graph as a func.func module.

                                                                                                                                                                                                          Equations
                                                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                            source
                                                                                                                                                                                                            def Proofs.StableHLO.linearFwdModuleV (B d₀ d₁ : ℕ) (W : Mat d₀ d₁) (b : Vec d₁) (x : Vec d₀) :
                                                                                                                                                                                                            String

                                                                                                                                                                                                            @linear_fwd rendered from the verified AST.

                                                                                                                                                                                                            Equations
                                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                              source
                                                                                                                                                                                                              def Proofs.StableHLO.linearBackModuleV (B d₀ d₁ : ℕ) (W : Mat d₀ d₁) (dy : Vec d₁) :
                                                                                                                                                                                                              String

                                                                                                                                                                                                              @linear_back rendered from the verified AST.

                                                                                                                                                                                                              Equations
                                                                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                source
                                                                                                                                                                                                                def Proofs.StableHLO.linearTrainStepModuleV (B d₀ d₁ : ℕ) (lr : String) (W : Mat d₀ d₁) (b : Vec d₁) (x : Vec d₀) :
                                                                                                                                                                                                                String

                                                                                                                                                                                                                The full @linear_train_step rendered from the verified AST: forward + softmax-CE cotangent come from pretty (lossCotGraph …) (the %onehot operand value is pretty-irrelevant, so any placeholder renders the same text — at runtime %onehot is a graph input); the weight grad (dot_general over the batch axis), bias grad (reduce), and the SGD multiply/subtract updates are appended. Returns the two updated params. The verified-AST peer of IRPrint.linearTrainStepModule.

                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                  source
                                                                                                                                                                                                                  def Proofs.StableHLO.linTrainStepFaithfulV (B m n : ℕ) (lrStr : String) (W : Mat m n) (b : Vec n) (x : Vec m) :
                                                                                                                                                                                                                  String

                                                                                                                                                                                                                  The linear train step rendered ENTIRELY from the verified AST. Unlike linearTrainStepModuleV (forward via pretty, tail hand-written), here the whole module is pretty of denoted nodes: the cotangent (lossCotGraph, rendered once → shared %dy), then the two fused SGD ops weightSgd/biasSgd that consume %dy. So every emitted line is pretty(provenNode) and LinearFold proves the two outputs' den = the certified loss-descent SGD step. The lr ℝ / operand values are skel-erased (render is value-independent), so placeholders here render identically to the live graph the den theorems use.

                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                    source
                                                                                                                                                                                                                    def Proofs.StableHLO.mlpFwdModuleV (B d₀ d₁ d₂ d₃ : ℕ) (W₀ : Mat d₀ d₁) (b₀ : Vec d₁) (W₁ : Mat d₁ d₂) (b₁ : Vec d₂) (W₂ : Mat d₂ d₃) (b₂ : Vec d₃) (x : Vec d₀) :
                                                                                                                                                                                                                    String

                                                                                                                                                                                                                    @mlp_fwd rendered from the verified forward AST mlpFwdGraph.

                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                      source
                                                                                                                                                                                                                      def Proofs.StableHLO.cnnFwdModuleV (B ic c h w d1 nClasses kH kW : ℕ) (W₁ : Kernel4 c ic kH kW) (b₁ : Vec c) (W₂ : Kernel4 c c kH kW) (b₂ : Vec c) (W₃ : Mat (c * h * w) d1) (b₃ : Vec d1) (W₄ : Mat d1 d1) (b₄ : Vec d1) (W₅ : Mat d1 nClasses) (b₅ : Vec nClasses) (x : Vec (ic * (2 * h) * (2 * w))) :
                                                                                                                                                                                                                      String

                                                                                                                                                                                                                      @cnn_fwd rendered from the verified CNN forward AST cnnFwdGraph.

                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                        source
                                                                                                                                                                                                                        def Proofs.StableHLO.cifarFwdModuleV (B ic c1 c2 h w d1 nClasses kH kW : ℕ) (W₁ : Kernel4 c1 ic kH kW) (b₁ : Vec c1) (W₂ : Kernel4 c1 c1 kH kW) (b₂ : Vec c1) (W₃ : Kernel4 c2 c1 kH kW) (b₃ : Vec c2) (W₄ : Kernel4 c2 c2 kH kW) (b₄ : Vec c2) (W₅ : Mat (c2 * h * w) d1) (b₅ : Vec d1) (W₆ : Mat d1 d1) (b₆ : Vec d1) (W₇ : Mat d1 nClasses) (b₇ : Vec nClasses) (x : Vec (ic * (2 * (2 * h)) * (2 * (2 * w)))) :
                                                                                                                                                                                                                        String

                                                                                                                                                                                                                        @cifar_fwd rendered from the verified CIFAR forward AST cifarFwdGraph.

                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                          source
                                                                                                                                                                                                                          def Proofs.StableHLO.mlpTrainStepText (B d₀ d₁ d₂ d₃ : ℕ) (lr : String) :
                                                                                                                                                                                                                          String

                                                                                                                                                                                                                          Full MLP SGD train step. The forward layers emit exactly mlpFwdGraph's ops (dot_general+add, maximum), saving the pre-activations %h0,%h1; the backward emits mlpBackGraph's ops (dot_general, compare GT+select masks reading %h0,%h1); param grads + SGD as in the linear step. Each piece is proven faithful above (mlpFwdGraph_faithful, mlpBackGraph_faithful, reluF_faithful, selectPos_faithful, wGrad/bGrad_is*Jacobian, lossCotGraph_isCEgrad, sgd*_isCertifiedGradStep); the assembly/naming is the renderer (validated by iree-compile + the GPU run).

                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                            source
                                                                                                                                                                                                                            def Proofs.StableHLO.cnnTrainStepText (B ic c H W kH kW d1 nClasses : ℕ) (lr : String) :
                                                                                                                                                                                                                            String

                                                                                                                                                                                                                            Full CNN SGD train step (@cnn_train_step), the ch4 peer of mlpTrainStepText. Architecture (= mnistCnnNoBnForward): conv W₁ → relu → conv W₂ → relu → maxpool → flatten → dense W₃ → relu → dense W₄ → relu → dense W₅. Each mathematical op is a rendering of a proof-backed piece:

                                                                                                                                                                                                                            • forward conv/maxpool/dense/relu — flatConvF_faithful, maxPoolF_faithful, denseF_faithful, reluF_faithful (and cnnFwdGraph_faithful for the whole);
                                                                                                                                                                                                                            • loss cotangent %dy = softmax(logits) − onehot — lossCotGraph_isCEgrad;
                                                                                                                                                                                                                            • backward dense (dot_general, contract output axis) + relu masks (compare GT+select) — mlpBackGraph_faithful/selectPos_faithful;
                                                                                                                                                                                                                            • maxpool backward (select_and_scatter, GE/add, route dy to the window argmax) — maxPoolBack_faithful; conv input-VJP (transpose+reverse+conv) — convBack_faithful;
                                                                                                                                                                                                                            • dense W/b grads (dot_general over batch / reduce) — wGrad/bGrad;
                                                                                                                                                                                                                            • conv weight grad — the transpose trick (conv2d_weight_grad_has_vjp): the SAME stablehlo.convolution with the batch axis as the contraction feature; rendered here, validated by the GPU run (a convWGrad_faithful theorem is optional polish, see §B2 of the handoff);
                                                                                                                                                                                                                            • SGD θ' = θ − lr·∇ — sgd*_isCertifiedGradStep. The op text mirrors the GPU-validated emitter (emitTok) byte-for-byte for conv/maxpool/convBack/select_and_scatter; assembly + SSA naming is the renderer. lr = 0.1/B (grads sum over the batch).
                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                              source
                                                                                                                                                                                                                              def Proofs.StableHLO.cifarTrainStepText (B ic c1 c2 H W kH kW d1 nClasses : ℕ) (lr : String) :
                                                                                                                                                                                                                              String

                                                                                                                                                                                                                              Full CIFAR CNN SGD train step (@cifar_train_step), the Chapter-4 peer of cnnTrainStepText. Architecture (= cifarCnnForward): conv 3→32 → relu → conv 32→32 → relu → maxpool → conv 32→64 → relu → conv 64→64 → relu → maxpool → flatten → dense 4096→512 → relu → dense 512→512 → relu → dense 512→10 + softmax-CE. Two conv→conv→pool stages at two spatial sizes (H×W then H/2×W/2), with channel changes.

                                                                                                                                                                                                                              Every mathematical op is the SAME proof-backed render as cnnTrainStepText, just instantiated at more layers / two spatial scales — forward conv/maxpool/dense/relu (cifarFwdGraph_faithful); loss cotangent (lossCotGraph_isCEgrad); backward dense (dot_general) + relu masks (selectPos_faithful); maxpool backward (select_and_scatter, maxPoolBack_faithful); conv input-VJP (transpose+reverse+conv, convBack_faithful); dense W/b grads; conv weight grad (transpose trick); SGD θ' = θ − lr·∇. The per-op text mirrors the GPU-validated emitTok byte-for-byte; assembly + SSA naming is the renderer (validated by iree-compile + the GPU run). lr = 0.1/B.

                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                source
                                                                                                                                                                                                                                def Proofs.StableHLO.cifarBnFwdModuleV (B ic c1 c2 h w d1 nClasses kH kW : ℕ) (epsStr : String) (W₁ : Kernel4 c1 ic kH kW) (b₁ : Vec c1) (ε₁ : ℝ) (γ₁ β₁ : Vec c1) (W₂ : Kernel4 c1 c1 kH kW) (b₂ : Vec c1) (ε₂ : ℝ) (γ₂ β₂ : Vec c1) (W₃ : Kernel4 c2 c1 kH kW) (b₃ : Vec c2) (ε₃ : ℝ) (γ₃ β₃ : Vec c2) (W₄ : Kernel4 c2 c2 kH kW) (b₄ : Vec c2) (ε₄ : ℝ) (γ₄ β₄ : Vec c2) (W₅ : Mat (c2 * h * w) d1) (b₅ : Vec d1) (W₆ : Mat d1 d1) (b₆ : Vec d1) (W₇ : Mat d1 nClasses) (b₇ : Vec nClasses) (x : Vec (ic * (2 * (2 * h)) * (2 * (2 * w)))) :
                                                                                                                                                                                                                                String

                                                                                                                                                                                                                                @cifar_bn_fwd rendered from the verified BN-CIFAR forward AST. γ/β are scalar tensor<f32> inputs (%g{i}/%bt{i}); epsStr the ε literal.

                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                  source
                                                                                                                                                                                                                                  def Proofs.StableHLO.cifar8FwdModuleV (B ic c1 c2 c3 c4 h w d1 nClasses kH kW : ℕ) (W₁ : Kernel4 c1 ic kH kW) (b₁ : Vec c1) (W₂ : Kernel4 c1 c1 kH kW) (b₂ : Vec c1) (W₃ : Kernel4 c2 c1 kH kW) (b₃ : Vec c2) (W₄ : Kernel4 c2 c2 kH kW) (b₄ : Vec c2) (W₅ : Kernel4 c3 c2 kH kW) (b₅ : Vec c3) (W₆ : Kernel4 c3 c3 kH kW) (b₆ : Vec c3) (W₇ : Kernel4 c4 c3 kH kW) (b₇ : Vec c4) (W₈ : Kernel4 c4 c4 kH kW) (b₈ : Vec c4) (W₉ : Mat (c4 * h * w) d1) (b₉ : Vec d1) (Wa : Mat d1 d1) (ba : Vec d1) (Wb : Mat d1 nClasses) (bb : Vec nClasses) (x : Vec (ic * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w)))))) :
                                                                                                                                                                                                                                  String

                                                                                                                                                                                                                                  @cifar8_fwd rendered from the verified 8-conv CIFAR forward AST cifar8FwdGraph (cifar8FwdGraph_faithful proves it denotes cifarCnn8Forward). The 4-stage peer of cifarFwdModuleV — closes the cifar8 _fwd bytes (committed verified_mlir/cifar8_fwd.mlir is now renderModule(provenGraph), replacing the hand-written cifar8FwdText).

                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                    source
                                                                                                                                                                                                                                    def Proofs.StableHLO.cifar8BnFwdModuleV (B ic c1 c2 c3 c4 h w d1 nClasses kH kW : ℕ) (epsStr : String) (W₁ : Kernel4 c1 ic kH kW) (b₁ : Vec c1) (ε₁ : ℝ) (γ₁ β₁ : Vec c1) (W₂ : Kernel4 c1 c1 kH kW) (b₂ : Vec c1) (ε₂ : ℝ) (γ₂ β₂ : Vec c1) (W₃ : Kernel4 c2 c1 kH kW) (b₃ : Vec c2) (ε₃ : ℝ) (γ₃ β₃ : Vec c2) (W₄ : Kernel4 c2 c2 kH kW) (b₄ : Vec c2) (ε₄ : ℝ) (γ₄ β₄ : Vec c2) (W₅ : Kernel4 c3 c2 kH kW) (b₅ : Vec c3) (ε₅ : ℝ) (γ₅ β₅ : Vec c3) (W₆ : Kernel4 c3 c3 kH kW) (b₆ : Vec c3) (ε₆ : ℝ) (γ₆ β₆ : Vec c3) (W₇ : Kernel4 c4 c3 kH kW) (b₇ : Vec c4) (ε₇ : ℝ) (γ₇ β₇ : Vec c4) (W₈ : Kernel4 c4 c4 kH kW) (b₈ : Vec c4) (ε₈ : ℝ) (γ₈ β₈ : Vec c4) (W₉ : Mat (c4 * h * w) d1) (b₉ : Vec d1) (Wa : Mat d1 d1) (ba : Vec d1) (Wb : Mat d1 nClasses) (bb : Vec nClasses) (x : Vec (ic * (2 * (2 * (2 * (2 * h)))) * (2 * (2 * (2 * (2 * w)))))) :
                                                                                                                                                                                                                                    String

                                                                                                                                                                                                                                    @cifar8_bn_fwd rendered from the verified 8-conv per-channel-BN CIFAR forward AST cifar8BnFwdGraph (cifar8BnFwdGraph_faithful proves it denotes cifarCnnBn8Forward). The BN peer of cifar8FwdModuleV — closes the cifar8-bn _fwd bytes, replacing the hand-written cifar8BnFwdTextPC.

                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                      source
                                                                                                                                                                                                                                      def Proofs.StableHLO.cifarBnTrainStepText (B ic c1 c2 H W kH kW d1 nClasses : ℕ) (epsStr lr : String) :
                                                                                                                                                                                                                                      String

                                                                                                                                                                                                                                      Full BN-CIFAR SGD train step (@cifar_bn_train_step). The Chapter-4 BatchNorm peer of cifarTrainStepText: each conv→relu block becomes conv→BN→relu. The per-example BN forward (bnFwd = renderLN: reduce μ/var over the feature axis, normalize, scalar-affine — denotes bnForward), its consolidated three-term input-VJP (bnBack = renderLNBack — the proven bn_grad_input, bnBack_faithful), and the scalar param grads dγ = Σ dy·x̂, dβ = Σ dy are inserted. BN runs on the flattened [B, oc·H·W] per-example feature vec (reshape around the 4-D conv). 22 params (4×{W,b,γ,β} + 3×{W,b}). The whole-net backward is cifarCnnBn_has_vjp_at. lr = 0.1/B.

                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                        source
                                                                                                                                                                                                                                        def Proofs.StableHLO.cifarBnFwdTextPC (B ic c1 c2 H W kH kW d1 nClasses : ℕ) (epsStr : String) :
                                                                                                                                                                                                                                        String

                                                                                                                                                                                                                                        Per-channel BN-CIFAR eval forward (@cifar_bn_fwd): the forward half of cifarBnTrainStepText (conv→per-channel-BN→relu ×4, 2 pools, 3 dense), returning logits [B,nClasses]. Per-channel BN (m=H·W) is per-example ⇒ train=eval (no running stats). String-rendered (peer of the train-step) until the typed cifarBnFwdGraph is reconciled to per-channel in the proof pass.

                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                          Deeper 8-conv CIFAR CNN (FOUR conv→conv→pool stages) train-step + fwd text #

                                                                                                                                                                                                                                          The 4-stage peers of cifarTrainStepText / cifarBnTrainStepText and their forwards. Channels c1 c2 c3 c4; spatial H → H/2 → H/4 → H/8 → H/16 (CIFAR 32→16→8→4→2). The forward is (conv→[BN→]relu)×2 → pool four times → flatten c4·Hp·Wp → 3-dense head; the backward is the exact transpose/reverse mirror (the same op templates as the 2-stage text). The whole-net VJPs are Proofs.cifarCnn8_has_vjp_at / cifarCnnBn8_has_vjp_at. lr = 0.1/B.

                                                                                                                                                                                                                                          source
                                                                                                                                                                                                                                          def Proofs.StableHLO.cifar8TrainStepText (B ic c1 c2 c3 c4 H W kH kW d1 nClasses : ℕ) (lr : String) :
                                                                                                                                                                                                                                          String

                                                                                                                                                                                                                                          8-conv CIFAR train step (@cifar8_train_step, no BN). 4 conv→conv→pool stages (channels ic→c1→c1, c1→c2→c2, c2→c3→c3, c3→c4→c4) + 3-dense head.

                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                            source
                                                                                                                                                                                                                                            def Proofs.StableHLO.cifar8FwdText (B ic c1 c2 c3 c4 H W kH kW d1 nClasses : ℕ) :
                                                                                                                                                                                                                                            String

                                                                                                                                                                                                                                            8-conv CIFAR eval forward (@cifar8_fwd, no BN), returning logits [B,nClasses].

                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                              source
                                                                                                                                                                                                                                              def Proofs.StableHLO.cifar8BnTrainStepText (B ic c1 c2 c3 c4 H W kH kW d1 nClasses : ℕ) (epsStr lr : String) :
                                                                                                                                                                                                                                              String

                                                                                                                                                                                                                                              8-conv CIFAR per-channel BN train step (@cifar8_bn_train_step). Each of the 8 convs is followed by bnFwd (per-channel BN, reduce spatial axis [2]); the backward inserts the relu-mask → BN input-VJP (bnBack) → conv-back per block + BN param grads (dγ=Σ dy·x̂, dβ=Σ dy). 38 params (8×{W,b,γ,β} + 3×{W,b}). Whole-net VJP: Proofs.cifarCnnBn8_has_vjp_at. lr = 0.1/B.

                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                source
                                                                                                                                                                                                                                                def Proofs.StableHLO.cifar8BnFwdTextPC (B ic c1 c2 c3 c4 H W kH kW d1 nClasses : ℕ) (epsStr : String) :
                                                                                                                                                                                                                                                String

                                                                                                                                                                                                                                                8-conv CIFAR per-channel BN eval forward (@cifar8_bn_fwd), returning logits.

                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                Instances For