Provedsampleability-lawself-certifying-proposalimportance-samplingattention-compute-law

Sampleability loop 2: the log-cost penalty on a head with target-bucket size m is ≥ 2 log p + log m − log ρ

For all $\htmlData{mx=1}{p, \rho \in \htmlData{mx=0}{\mathbb{R}}}$ , $\htmlData{mx=1}{m \in \htmlData{mx=0}{\mathbb{N}}}$ and $\htmlData{mx=1}{C \in \htmlData{mx=0}{\mathbb{R}}}$ , if $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{p}$ , $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{\rho}$ , $0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{m}$ and $\htmlData{mx=5}{\frac{\htmlData{mx=3}{\htmlData{mx=1}{\htmlData{mx=0}{p}^{2}} \cdot \htmlData{mx=2}{m}}}{\htmlData{mx=4}{\rho}}} \mathrel{\htmlData{mx=7}{\leq}} \htmlData{mx=6}{C}$ , then

\htmlData{mx=8}{\htmlData{mx=5}{\htmlData{mx=2}{2\htmlData{mx=1}{\log \htmlData{mx=0}{p}}} + \htmlData{mx=4}{\log \htmlData{mx=3}{m}}} - \htmlData{mx=7}{\log \htmlData{mx=6}{\rho}}} \mathrel{\htmlData{mx=11}{\leq}} \htmlData{mx=10}{\log \htmlData{mx=9}{C}}

What the notation means · or point at any symbol

RReal numbers: The real numbers: every point on the number line. (ℝ)
x ∈ TVariables: p, ρ range over real numbers: the statement must hold for every choice. ((p ρ : ℝ))
NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
<Less than: 0 is strictly smaller than p. (0 < p)
aᵇPower: p raised to the power 2. (p ^ 2)
·Multiplication: p^2 times m. (p ^ 2 * m)
a/bDivision: p^2 · m divided by ρ. In Lean, dividing by 0 gives 0. (p ^ 2 * m / ρ)
≤At most: p^2 · m/ρ is less than or equal to C. (p ^ 2 * m / ρ ≤ C)
+Addition: 2 · log(p) plus log(m). (2 * Real.log p + Real.log m)
-Subtraction: 2 · log(p) + log(m) minus log(ρ). On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (2 * Real.log p + Real.log m - Real.log ρ)
logNatural logarithm: The logarithm of p to base e: the power e must be raised to to give p. (Real.log p)

theorem sl-penalty-lower-bound (p ρ : ℝ) (m : ℕ) (C : ℝ) (hp : 0 < p) (hρ : 0 < ρ) (hm : 0 < m) (hC : p ^ 2 * m / ρ ≤ C) :
    2 * Real.log p + Real.log m - Real.log ρ ≤ Real.log C

The certificate penalty grows like log m while the proposal has not localised the target; the bound is explicit so the penalty cannot be gamed by the model without reducing p (flattening the head). Part of 'The Sampleability Law: a transformer can be trained to make its own attention cheap to sample, and the samples certify the saving' (self-certifying learned proposals inside the Attention Compute Law).

How it was proved

Proved: 4 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: 14 lines of Lean

Sampleability loop 2: the log-cost penalty on a head with target-bucket size m is ≥ 2 log p + log m − log ρ

How it was proved

More proved statements