Provedmoussesupportingeditorial-counterexamplesource-n3

The explicit anisotropic update is not any scalar multiple of the ordinary Muon direction

\htmlData{mx=19}{\lnot \left(\htmlData{mx=18}{\exists c \in \htmlData{mx=17}{\mathbb{R}},\ \htmlData{mx=11}{\htmlData{mx=0}{\operatorname{diagonal}}\left(\htmlData{mx=10}{i \mapsto \htmlData{mx=7}{\begin{cases} \htmlData{mx=3}{\htmlData{mx=2}{-\htmlData{mx=1}{\frac{1}{2}}}} & \text{if } \htmlData{mx=4}{i} \mathrel{\htmlData{mx=5}{=}} 0 \\ \htmlData{mx=6}{-1} & \text{otherwise} \end{cases}}}\right)} \mathrel{\htmlData{mx=16}{=}} \htmlData{mx=15}{\htmlData{mx=12}{c} \, \htmlData{mx=14}{-\htmlData{mx=13}{1}}}}\right)}

What the notation means · or point at any symbol

¬Not: It is not the case that ∃ c, diagonal(i ↦ −(1/2) if i = 0, else −1) = c • −1. (¬ (∃ c : ℝ, Matrix.diagonal (fun i : Fi…)
∃There exists: At least one c makes the statement after the comma true. (∃ c : ℝ, Matrix.diagonal (fun i : Fin 2…)
RReal numbers: The real numbers: every point on the number line. (ℝ)
diagonal: Matrix.diagonal: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Matrix.diagonal)
x ↦ f(x)Function (λ-abstraction): The function sending i to −(1/2) if i = 0, else −1. Lean writes fun x => …; papers write x ↦ …. (fun i : Fin 2 => if i = 0 then (-(1 / 2…)
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)
f(x)Function application: Fin applied to 2. Lean writes f x; papers write f(x). (Fin 2)
{ a if c; b otherwiseCases (if … then … else): −(1/2) when i = 0, and −1 otherwise. (if i = 0 then (-(1 / 2) : ℝ) else -1)
=Equality: i and 0 are the same. (i = 0)
(x : T)As real numbers: −(1/2) read as an element of real numbers. Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((-(1 / 2) : ℝ))
−xNegation: The negative of 1/2. (-(1 / 2))
a/bDivision: 1 divided by 2. In Lean, dividing by 0 gives 0. (1 / 2)
•Scalar multiplication: −1 scaled by the number c. (c • (-(1 : Matrix (Fin 2) (Fin 2) ℝ)))
(x : T)Type ascription: 1 read as a Matrix(Fin(2), Fin(2), ℝ). Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((1 : Matrix (Fin 2) (Fin 2) ℝ))

theorem mousse-two-dimensional-update-not-scaled-muon :
    ¬ (∃ c : ℝ, Matrix.diagonal (fun i : Fin 2 => if i = 0 then (-(1 / 2) : ℝ) else -1) = c • (-(1 : Matrix (Fin 2) (Fin 2) ℝ)))

S1 / N3. Exact original editorial counterexample: diag(-1/2,-1) cannot equal c*(-I₂) for any real c. This is the nonproportionality component only; weighted feasibility, global optimality, and the common-constraint objective gap are separate targets G2 and S2. No performance or history-realizability claim, and no disproof of the first idea's conditional Lean statements.

How it was proved

Proved: 29 September 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

The explicit anisotropic update is not any scalar multiple of the ordinary Muon direction

How it was proved

More proved statements