Provedattentionversion-9finite-lawconstructible-state

Built weighted member trees preserve every finite acceptance history statistic

For all $\htmlData{mx=2}{C : \htmlData{mx=1}{\htmlData{mx=0}{\operatorname{Type}} \cdot }}$ , $\htmlData{mx=1}{h \in \htmlData{mx=0}{\mathbb{N}}}$ , $\htmlData{mx=3}{\mathit{coeff} : \htmlData{mx=0}{C} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ , $\htmlData{mx=8}{\omega : \htmlData{mx=0}{C} \mathrel{\htmlData{mx=7}{\to}} \htmlData{mx=4}{\htmlData{mx=1}{\operatorname{Copies}}\,\htmlData{mx=2}{\operatorname{Bool}}\,\htmlData{mx=3}{h}} \mathrel{\htmlData{mx=6}{\to}} \htmlData{mx=5}{\mathbb{R}}}$ , $\htmlData{mx=6}{\mathit{accept} : \htmlData{mx=3}{\htmlData{mx=0}{\operatorname{Copies}}\,\htmlData{mx=1}{\operatorname{Bool}}\,\htmlData{mx=2}{h}} \mathrel{\htmlData{mx=5}{\to}} \htmlData{mx=4}{\mathbb{R}}}$ , $\htmlData{mx=1}{m \in \htmlData{mx=0}{\mathbb{N}}}$ and $\htmlData{mx=12}{f : (\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fin}}\,\htmlData{mx=1}{m}} \mathrel{\htmlData{mx=9}{\to}} \htmlData{mx=8}{\htmlData{mx=6}{\htmlData{mx=3}{\operatorname{Copies}}\,\htmlData{mx=4}{\operatorname{Bool}}\,\htmlData{mx=5}{h}} \times \htmlData{mx=7}{\operatorname{Bool}}}) \mathrel{\htmlData{mx=11}{\to}} \htmlData{mx=10}{\mathbb{R}}}$ , if $\htmlData{mx=5}{\forall \mathit{ch}, j,\ 0 \mathrel{\htmlData{mx=4}{\leq}} \htmlData{mx=3}{\htmlData{mx=0}{\omega}(\htmlData{mx=1}{\mathit{ch}}, \htmlData{mx=2}{j})}}$ (given $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fintype}}\,\htmlData{mx=1}{C}}$ ), then

\begin{aligned} & \left(\right. (\htmlData{mx=86}{\htmlData{mx=1}{\operatorname{sum}}(\htmlData{mx=2}{\operatorname{univ}}, \htmlData{mx=85}{z \mapsto \htmlData{mx=75}{\htmlData{mx=25}{\htmlData{mx=3}{\operatorname{rejectionWeight}}(\htmlData{mx=11}{x \mapsto \htmlData{mx=10}{\htmlData{mx=4}{\operatorname{treeJoint}}(\htmlData{mx=5}{h}, \htmlData{mx=6}{\mathit{coeff}}, \htmlData{mx=7}{\omega}, \htmlData{mx=8}{x_{1}}, \htmlData{mx=9}{x_{2}})}}, \htmlData{mx=22}{x \mapsto \htmlData{mx=21}{\htmlData{mx=12}{\mathit{accept}}(\htmlData{mx=20}{\htmlData{mx=13}{\operatorname{returned}}(\htmlData{mx=18}{\htmlData{mx=14}{\operatorname{memberTree}}(\htmlData{mx=15}{h}, \htmlData{mx=16}{\omega}, \htmlData{mx=17}{x_{1}})}, \htmlData{mx=19}{x_{2}})})}}, \htmlData{mx=23}{m}, \htmlData{mx=24}{z})} \cdot \htmlData{mx=74}{\htmlData{mx=26}{f}(\htmlData{mx=73}{i \mapsto \htmlData{mx=72}{\left( \htmlData{mx=67}{\operatorname{1.2}\left(\htmlData{mx=66}{\htmlData{mx=47}{\operatorname{returned}}(\htmlData{mx=62}{\operatorname{1.1}\left(\htmlData{mx=61}{\htmlData{mx=55}{\operatorname{memberTree}}(\htmlData{mx=56}{h}, \htmlData{mx=57}{\omega}, \htmlData{mx=60}{\htmlData{mx=58}{z}(\htmlData{mx=59}{i})})}\right)}, \htmlData{mx=65}{\htmlData{mx=63}{z}(\htmlData{mx=64}{i})})}\right)}, \htmlData{mx=71}{\htmlData{mx=70}{\htmlData{mx=68}{z}(\htmlData{mx=69}{i})}_{2}} \right)}})}}})}) \\ & \quad \htmlData{mx=0}{=} \htmlData{mx=124}{\htmlData{mx=87}{\operatorname{sum}}\left(\htmlData{mx=88}{\operatorname{univ}}, \htmlData{mx=123}{z \mapsto \htmlData{mx=115}{\htmlData{mx=111}{\htmlData{mx=89}{\operatorname{rejectionWeight}}\left(\htmlData{mx=107}{j \mapsto \htmlData{mx=106}{\frac{\htmlData{mx=101}{\htmlData{mx=90}{\operatorname{sum}}(\htmlData{mx=91}{\operatorname{univ}}, \htmlData{mx=100}{\mathit{ch} \mapsto \htmlData{mx=99}{\htmlData{mx=94}{\htmlData{mx=92}{\mathit{coeff}}(\htmlData{mx=93}{\mathit{ch}})} \cdot \htmlData{mx=98}{\htmlData{mx=95}{\omega}(\htmlData{mx=96}{\mathit{ch}}, \htmlData{mx=97}{j})}}})}}{\htmlData{mx=105}{\htmlData{mx=102}{\operatorname{mixtureTotal}}(\htmlData{mx=103}{\mathit{coeff}}, \htmlData{mx=104}{\omega})}}}}, \htmlData{mx=108}{\mathit{accept}}, \htmlData{mx=109}{m}, \htmlData{mx=110}{z}\right)} \cdot \htmlData{mx=114}{\htmlData{mx=112}{f}(\htmlData{mx=113}{z})}}}\right)} \left.\right) \end{aligned}

What the notation means · or point at any symbol

Type: Type: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Type)
·Multiplication: Type times . (Type*)
Fintype: Fintype: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Fintype)
f(x)Function application: Fintype applied to C. Lean writes f x; papers write f(x). (Fintype C)
NNatural numbers: The natural numbers 0, 1, 2, …. In Lean they start at 0. (ℕ)
⟹Implies: If C, then ℝ. (Between types, A → B is the type of functions from A to B.) (C → ℝ)
∀For all: The statement after the comma holds for every ch, j. (∀ ch j,0≤ω ch j)
Fin: Fin: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Fin)
RReal numbers: The real numbers: every point on the number line. (ℝ)
Copies: Copies: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Copies)
=Equality: sum(univ, z ↦ rejectionWeight(x ↦ treeJoint(h, coeff, ω, x… and sum(univ, z ↦ rejectionWeight(j ↦ sum(univ, ch ↦ coeff(ch)… are the same. ((Finset.sum Finset.univ (fun z : Path (…)
sum: Finset.sum: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Finset.sum)
≤At most: 0 is less than or equal to ω(ch, j). (0≤ω ch j)
×Product: Pairs of an element of Copies(Bool, h) and an element of Bool. (Copies Bool h × Bool)
Bool: Bool: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Bool)
univ: Finset.univ: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Finset.univ)
Path: Path: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Path)
rejectionWeight: rejectionWeight: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (rejectionWeight)
x ↦ f(x)Function (λ-abstraction): The function sending x to treeJoint(h, coeff, ω, x.1, x.2). Lean writes fun x => …; papers write x ↦ …. (fun x => treeJoint h coeff ω x.1 x.2)
treeJoint: treeJoint: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (treeJoint)
p₁Component: The first component of the pair x. (x.1)
returned: MassTree.returned: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (MassTree.returned)
memberTree: memberTree: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (memberTree)
(a, b)Tuple: The ordered pair (or tuple) of 1.2(returned(1.1(memberTree(h, ω, z(i))), z(i))), z(i).2. ((MassTree.returned (memberTree h ω (z i…)
e.f1.2: 1.2 of returned(1.1(memberTree(h, ω, z(i))), z(i)): Lean's dot notation e.1.2 means 1.2 applied to e. (MassTree.returned (memberTree h ω (z i)…)
e.f1.1: 1.1 of memberTree(h, ω, z(i)): Lean's dot notation e.1.1 means 1.1 applied to e. (memberTree h ω (z i).1.1)
a/bDivision: sum(univ, ch ↦ coeff(ch) · ω(ch, j)) divided by mixtureTotal(coeff, ω). In Lean, dividing by 0 gives 0. ((Finset.sum Finset.univ (fun ch => coef…)
mixtureTotal: mixtureTotal: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (mixtureTotal)

theorem attention-v9-tree-channel-history {C : Type*} [Fintype C] (h : ℕ) (coeff : C → ℝ) (ω : C → Copies Bool h → ℝ)
    (hω : ∀ ch j,0≤ω ch j) (accept : Copies Bool h → ℝ) (m : ℕ)
    (f : (Fin m → Copies Bool h × Bool) → ℝ) :
    (    (Finset.sum Finset.univ (fun z : Path (C × Copies Bool h) m =>
      rejectionWeight (fun x => treeJoint h coeff ω x.1 x.2)
        (fun x => accept (MassTree.returned (memberTree h ω x.1) x.2)) m z *
      f (fun i => (MassTree.returned (memberTree h ω (z i).1.1) (z i).1.2,(z i).2)))) =
      Finset.sum Finset.univ (fun z : Path (Copies Bool h) m =>
        rejectionWeight (fun j => (Finset.sum Finset.univ (fun ch => coeff ch*ω ch j))/mixtureTotal coeff ω) accept m z * f z))

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

Built weighted member trees preserve every finite acceptance history statistic

How it was proved

More proved statements