Provedattentionversion-9finite-lawconstructible-state

Exact finite mean and variance of randomized dense correction

For all $\htmlData{mx=1}{c, o, \alpha \in \htmlData{mx=0}{\mathbb{R}}}$ , if $\htmlData{mx=0}{\alpha} \mathrel{\htmlData{mx=1}{\neq}} 0$ , then

\begin{aligned} & \left(\right. \htmlData{mx=10}{\htmlData{mx=1}{\operatorname{mean}}(\htmlData{mx=4}{\htmlData{mx=2}{\operatorname{coin}}(\htmlData{mx=3}{\alpha})}, \htmlData{mx=9}{\htmlData{mx=5}{\operatorname{denseGate}}(\htmlData{mx=6}{c}, \htmlData{mx=7}{o}, \htmlData{mx=8}{\alpha})})} \mathrel{\htmlData{mx=12}{=}} \htmlData{mx=11}{o} \\ & \htmlData{mx=0}{\land} \htmlData{mx=23}{\htmlData{mx=13}{\operatorname{mse}}(\htmlData{mx=16}{\htmlData{mx=14}{\operatorname{coin}}(\htmlData{mx=15}{\alpha})}, \htmlData{mx=21}{\htmlData{mx=17}{\operatorname{denseGate}}(\htmlData{mx=18}{c}, \htmlData{mx=19}{o}, \htmlData{mx=20}{\alpha})}, \htmlData{mx=22}{o})} \mathrel{\htmlData{mx=32}{=}} \htmlData{mx=31}{\left(\htmlData{mx=26}{\htmlData{mx=25}{\frac{1}{\htmlData{mx=24}{\alpha}}} - 1}\right) \cdot \htmlData{mx=30}{(\htmlData{mx=29}{\htmlData{mx=27}{o} - \htmlData{mx=28}{c}})^{2}}} \left.\right) \end{aligned}

What the notation means · or point at any symbol

RReal numbers: The real numbers: every point on the number line. (ℝ)
x ∈ TVariables: c, o, α range over real numbers: the statement must hold for every choice. ((c o α : ℝ))
≠Not equal: α and 0 are different. (α≠0)
mean: mean: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (mean)
=Equality: mean(coin(α), denseGate(c, o, α)) and o are the same. (mean (coin α) (denseGate c o α)=o)
∧And: Both hold: mean(coin(α), denseGate(c, o, α)) = o, and mse(coin(α), denseGate(c, o, α), o) = (1/α − 1) · (o − c)^2. (mean (coin α) (denseGate c o α)=o ∧ mse…)
coin: coin: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (coin)
f(x)Function application: coin applied to α. Lean writes f x; papers write f(x). (coin α)
denseGate: denseGate: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (denseGate)
mse: mse: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (mse)
·Multiplication: 1/α − 1 times (o − c)^2. ((1/α-1)*(o-c)^2)
a/bDivision: 1 divided by α. In Lean, dividing by 0 gives 0. (1/α)
-Subtraction: 1/α minus 1. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (1/α-1)
aᵇPower: o − c raised to the power 2. ((o-c)^2)

theorem attention-v9-dense-gate-attainment (c o α : ℝ) (hα : α≠0) :
    (    mean (coin α) (denseGate c o α)=o ∧
    mse (coin α) (denseGate c o α) o=(1/α-1)*(o-c)^2)

Version 9 exact frozen target. Proof references the validated additive definition library. This mathematical finite-law/invariant target does not certify compiled Rust RAM runtime or the general linear-summary LP bridge.

How it was proved

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

Exact finite mean and variance of randomized dense correction

How it was proved

More proved statements