> ## Documentation Index
> Fetch the complete documentation index at: https://docs.theformalera.com/llms.txt
> Use this file to discover all available pages before exploring further.

# Op Specs

> The operator definitions every Model Spec is built from, in Lean 4.

Op Specs live in `TheFormalEra.Ops` (`specs/TheFormalEra/Ops/`). Each is a `noncomputable def` over Mathlib's `ℝ`. Model Specs instantiate them with constants; a node's `op` field names the Op Spec it uses.

## Scalar functions

```lean theme={"system"}
noncomputable def sigmoid (x : ℝ) : ℝ := 1 / (1 + Real.exp (-x))
noncomputable def silu (x : ℝ) : ℝ := x * sigmoid x
noncomputable def softplus (x : ℝ) : ℝ := Real.log (1 + Real.exp x)
/-- Tanh approximation of GELU (`gelu_pytorch_tanh`). -/
noncomputable def geluTanh (x : ℝ) : ℝ :=
  1 / 2 * x * (1 + Real.tanh (Real.sqrt (2 / Real.pi) * (x + 44715 / 1000000 * x ^ 3)))
/-- Soft-capping `c · tanh(x / c)`. -/
noncomputable def softcap (c x : ℝ) : ℝ := c * Real.tanh (x / c)
```

## Normalisation

| Op Spec | Formula | Used by |
| - | - | - |
| `rmsnorm` | `x / √(mean(x²) + ε) · w` | Qwen3, Granite, Gemma 4 |
| `rmsnormOffset` | `x / √(mean(x²) + ε) · (1 + w)` | Qwen3.8, Muse Glimmer |
| `rmsnormUnit` | `x / √(mean(x²) + ε)` (no weight) | Gemma 4 value norm, Muse Glimmer q/k and embedding norms |
| `rmsnormGated` | `w ⊙ x / √(mean(x²) + ε) ⊙ silu(z)` | Gated DeltaNet output |
| `l2norm` | `x / √(Σ x² + ε)` | Delta-rule queries and keys |

```lean theme={"system"}
noncomputable def rmsnormOffset (eps : ℝ) (x : ι → Fin H → ℝ) (w : Fin H → ℝ) : ι → Fin H → ℝ :=
  fun t h => x t h / Real.sqrt ((∑ j, x t j ^ 2) / (H : ℝ) + eps) * (1 + w h)
```

The row index type `ι` is arbitrary: tokens `Fin T` for a hidden-state norm, or (token, head) pairs for a per-head norm.

## Linear maps and feed-forward

| Op Spec | Formula |
| - | - |
| `linear` | `y[t, n] = Σₖ x[t, k] · W[n, k]`: a bias-free `nn.Linear(K, N)`, `W` stored `[N, K]` |
| `gateUp` | `[x W_gateᵀ ‖ x W_upᵀ]`, gate first |
| `siluMul` | `y[t, i] = silu(gu[t, i]) · gu[t, I + i]` (SwiGLU on a fused `[gate ‖ up]` row) |
| `geluMul` | `y[t, i] = geluTanh(gu[t, i]) · gu[t, I + i]` (GeGLU) |
| `residual` | `y = x + r · h` (`r = 1` except where a model uses a residual multiplier) |
| `embed` | `y[t] = c · E[tokens[t]]` |
| `lmHead` | `z = mul · x Wᵀ`, then optionally `softcap c z` |

## Attention

```lean theme={"system"}
noncomputable def softmax {L : ℕ} (s : Fin L → ℝ) (visible : Fin L → Prop)
    [DecidablePred visible] : Fin L → ℝ :=
  fun l => if visible l then
    Real.exp (s l) / ∑ m ∈ Finset.univ.filter visible, Real.exp (s m) else 0

noncomputable def causalGQA {S L Hkv G D : ℕ} (scale : ℝ) (pos : Fin S → ℕ)
    (q : Fin S → Fin Hkv → Fin G → Fin D → ℝ)
    (k v : Fin L → Fin Hkv → Fin D → ℝ) : Fin S → Fin Hkv → Fin G → Fin D → ℝ :=
  fun s c g d =>
    let logit : Fin L → ℝ := fun l => scale * ∑ e, q s c g e * k l c e
    ∑ l, softmax logit (fun l => l.val ≤ pos s) l * v l c d
```

| Op Spec | What it is |
| - | - |
| `causalGQA` | Causal grouped-query attention: KV head `c` serves `G` query heads |
| `slidingGQA` | The same, where the query at position `p` sees keys `l` with `p − w < l ≤ p` |
| `decodeGQA` | Decode attention: one query at the last position of `L` cached tokens. Query head `c·G + g` reads KV head `c`. |
| `sigmoidGate` | Output gate of gated attention: `o ⊙ σ(gate)` |

> [!NOTE]
>
> The sliding-window decode nodes of Gemma 4 and Muse Glimmer are labelled `slidingDecodeGQA` in the compute graph: decode attention over the last `w` cached positions. In spec 1.0 that label has no Lean definition of its own. The window semantics are defined by `slidingGQA`, and the conformance oracle evaluates them, but the engine has no Op Spec to prove a sliding-window decode kernel against. Those kernels are UNKNOWN.

## Rotary embeddings

```lean theme={"system"}
noncomputable def invFreq (theta : ℝ) (denom active i : ℕ) : ℝ :=
  if i < active then theta ^ (-(2 * (i : ℝ) / denom)) else 0
```

`rope θ rot denom active` rotates pairs `(i, i + rot/2)` for `i < rot/2` by `pos · invFreq i`, and leaves coordinates `≥ rot` unchanged. That one definition covers every variant in the supported models:

| Variant | Parameters | Example |
| - | - | - |
| Full RoPE | `rot = denom = D`, `active = D/2` | Qwen3-0.6B, Granite |
| Partial RoPE | `rot = denom < D` | Qwen3.8-27B: 64 of 256 dimensions |
| Proportional RoPE | `rot = denom = D`, `active < D/2` | Gemma 4 global layers: 64 active frequencies of 256 |
| NoPE | no `attn.rope` node | Muse Glimmer global layers |

## Gated DeltaNet

```lean theme={"system"}
/-- State of the gated delta rule (single head):
    S_t = α_t · S_{t-1} · (I − β_t k_t k_tᵀ) + β_t v_t k_tᵀ -/
noncomputable def gdnState {T Dk Dv : ℕ} (α β : Fin T → ℝ)
    (k : Fin T → Fin Dk → ℝ) (v : Fin T → Fin Dv → ℝ) :
    (t : ℕ) → t ≤ T → Matrix (Fin Dv) (Fin Dk) ℝ
  | 0, _ => 0
  | t + 1, h =>
    let i : Fin T := ⟨t, h⟩
    α i • (gdnState α β k v t (Nat.le_of_succ_le h) * (1 - β i • Matrix.vecMulVec (k i) (k i)))
      + β i • Matrix.vecMulVec (v i) (k i)

/-- Output at step t: o_t = S_t q_t -/
noncomputable def gatedDeltaRule {T Dk Dv : ℕ} (α β : Fin T → ℝ)
    (q k : Fin T → Fin Dk → ℝ) (v : Fin T → Fin Dv → ℝ) : Fin T → Fin Dv → ℝ :=
  fun i => (gdnState α β k v (i.val + 1) i.isLt).mulVec (q i)
```

| Op Spec | What it is |
| - | - |
| `gatedDeltaRule` | The recurrence above; the decode step is `gdnStep` (`gdnState_succ` proves they agree) |
| `causalConvSilu` | Depthwise causal convolution of width `K` followed by SiLU, with zero left padding |

High-performance kernels use the chunk-parallel (WY) form, which looks nothing like this recurrence. `chunkDeltaRule_eq` proves in Lean that the chunked form equals the recurrence, for every chunk size.


This documentation is built and hosted on [Mintlify](https://mintlify.com), a developer documentation platform.