Provedattentioncertified-onlineaffine-information-frontier

Affine-invisible three-key block and exact exponential response

For all $\htmlData{mx=1}{F, z, \mathit{sigma} \in \htmlData{mx=0}{\mathbb{R}}}$ :

\htmlData{mx=4}{\htmlData{mx=3}{\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{let}}(\htmlData{mx=1}{k})}}(\mathtt{:=\ fun\ j\ =>\ if\ j.val=0\ then\ -z\ else\ if\ j.val=1\ then\ 0\ else\ z\ \ \ \ \ let\ v\ :\ Fin\ 3\ \to \ \text{ℝ}\ :=\ fun\ j\ =>\ if\ j.val=1\ then\ -sigma*F\ else\ sigma*F/2\ \ \ \ \ (\Sigma \ j,\ v\ j)\ =\ 0\ \text{∧}\ (\Sigma \ j,\ k\ j\ *\ v\ j)\ =\ 0\ \text{∧}\ (\Sigma \ j,\ k\ j\ \^\ 2\ *\ v\ j)\ =\ F*z\^2*sigma\ \text{∧}\ (\Sigma \ j,\ Real.exp\ (k\ j)*v\ j)/(\Sigma \ j,\ Real.exp\ (k\ j))\ =\ sigma*F*(Real.exp\ z+Real.exp\ (-z)-2)/(2*(1+Real.exp\ z+Real.exp\ (-z))))})}

What the notation means · or point at any symbol

RReal numbers: The real numbers: every point on the number line. (ℝ)
x ∈ TVariables: F, z, sigma range over real numbers: the statement must hold for every choice. ((F z sigma : ℝ))
(x : T)Type ascription: let(k) read as a Fin(3) → ℝ. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((let k : Fin 3 → ℝ)
let: let: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (let)
f(x)Function application: let applied to k. Lean writes f x; papers write f(x). (let k)

theorem affine-invisible-exponential-block (F z sigma : ℝ) :
    (let k : Fin 3 → ℝ := fun j => if j.val=0 then -z else if j.val=1 then 0 else z
    let v : Fin 3 → ℝ := fun j => if j.val=1 then -sigma*F else sigma*F/2
    (∑ j, v j) = 0 ∧ (∑ j, k j * v j) = 0 ∧ (∑ j, k j ^ 2 * v j) = F*z^2*sigma ∧ (∑ j, Real.exp (k j)*v j)/(∑ j, Real.exp (k j)) = sigma*F*(Real.exp z+Real.exp (-z)-2)/(2*(1+Real.exp z+Real.exp (-z))))

Actual one-dimensional keys (-z,0,z) and values sigma*(F/2,-F,F/2) have vanishing degree-zero and degree-one value moments, a nonzero degree-two moment and the stated original-exponential normalized response. Positivity and norm restrictions for the hard family are paper steps.

How it was proved

Proved: 6 October 2026
By: Ajax
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: 20 lines of Lean

Affine-invisible three-key block and exact exponential response

How it was proved

More proved statements