Provedalphabaguettealgorithm-ideac7

In causal attention over T positions, key position j is read by exactly T − j queries

For all $\htmlData{mx=1}{T, j \in \htmlData{mx=0}{\mathbb{N}}}$ :

\htmlData{mx=20}{\lvert \htmlData{mx=19}{\htmlData{mx=14}{\operatorname{filter}\left(\htmlData{mx=13}{\{0, \dots, \htmlData{mx=12}{T} - 1\}}\right)}(\htmlData{mx=18}{i \mapsto \htmlData{mx=15}{j} \mathrel{\htmlData{mx=17}{\leq}} \htmlData{mx=16}{i}})} \rvert} \mathrel{\htmlData{mx=24}{=}} \htmlData{mx=23}{\htmlData{mx=21}{T} - \htmlData{mx=22}{j}}

What the notation means · or point at any symbol

NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
x ∈ TVariables: T, j range over natural numbers: the statement must hold for every choice. ((T j : ℕ))
|s|Cardinality: The number of elements of filter(range(T))(i ↦ j ≤ i). (((Finset.range T).filter (fun i => j ≤ …)
=Equality: card(filter(range(T))(i ↦ j ≤ i)) and T − j are the same. (((Finset.range T).filter (fun i => j ≤ …)
e.ffilter: filter of range(T): Lean's dot notation e.filter means filter applied to e. ((Finset.range T).filter)
f(x)Function application: filter(range(T)) applied to i ↦ j ≤ i. Lean writes f x; papers write f(x). ((Finset.range T).filter (fun i => j ≤ i))
{0,…,n−1}Range: The numbers 0, 1, …, T − 1 (T of them). (Finset.range T)
x ↦ f(x)Function (λ-abstraction): The function sending i to j ≤ i. Lean writes fun x => …; papers write x ↦ …. (fun i => j ≤ i)
≤At most: j is less than or equal to i. (j ≤ i)
-Subtraction: T minus j. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (T - j)

theorem causal-fan-in-position (T j : ℕ) :
    ((Finset.range T).filter (fun i => j ≤ i)).card = T - j

Idea C7 (sink-anchored windows). Position j is visible to queries j, …, T−1, so its key/value (and, through them, its token's embedding row) receives cotangents from T − j rows; the maximum, T, is at position 0. Baguette's recorded divergences surfaced in the embedding rows of position-0 tokens. Reserving position 0 for a dedicated sink token keeps that maximal fan-in off arbitrary vocabulary rows.

How it was proved

Proved: 3 October 2026
By: Ajax, with the agent “Baguette math & proofs (Claude Code, 2026-10-03)”
Checked by: Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
Axioms: Classical.choice, Quot.sound, propext
Proof: 18 lines of Lean

In causal attention over T positions, key position j is read by exactly T − j queries

How it was proved

More proved statements