`Level.normalize` incomplete for `imax-to-max` simplification

Disclaimer: this bug was found autonomously by Opus 4.6 using this setup and has not been reviewed by a Lean expert yet. Below is its (unedited) report.

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Level.normalize does not produce canonical forms when an imax simplifies
to max. This causes Level.isEquiv (and the C++ kernel's is_equivalent)
to return false for semantically equal universe levels.

Two manifestations:

1. Succ distribution (Lean + C++): normalize(succ(imax u (succ v)))
   yields (max u (v+1))+1 instead of max (u+1) (v+2). The imax is
   correctly converted to max, but outer succs are not distributed into the
   max arguments.

2. Sorting/flattening (C++ kernel only): normalize(imax v (imax u (succ w)))
   yields max(v, max(u, succ w)) instead of the canonically sorted
   max(u, max(v, succ w)). The Lean-side normalize handles this correctly
   because its isNeverZero branch passes the result through the Max
   normalization path.

Both stem from the IMax case of normalize: after mk_imax converts the
imax to a max, the result is returned without being re-normalized through
the Max path.

See test_univ_normalization_bugs.lean.

Context

Zulip thread

Steps to Reproduce

Bug 1 — Succ distribution:

import Lean

open Lean in
#eval do
  let u := Level.param `u
  let v := Level.param `v
  -- succ(imax u (succ v)) is semantically max(u+1, v+2)
  let e1 := Level.succ (Level.imax u (Level.succ v))
  let e2 := Level.max (Level.succ u) (Level.succ (Level.succ v))
  IO.println s!"normalize(e1) = {e1.normalize}"  -- (max u (v+1))+1
  IO.println s!"normalize(e2) = {e2.normalize}"  -- max (u+1) (v+2)
  IO.println s!"isEquiv = {Level.isEquiv e1 e2}"  -- false!

Bug 2 — Sorting (kernel):

import Lean

open Lean in
#eval show IO Unit from do
  let env ← importModules #[{module := `Init}] {} 0
  let u := Level.param `u
  let v := Level.param `v
  let w := Level.param `w
  -- imax v (imax u (succ w)) and imax u (imax v (succ w))
  -- are both semantically max(u, v, succ w)
  let axiomDecl : Declaration := .axiomDecl {
    name := `myConst
    levelParams := [`u, `v, `w]
    type := Expr.sort (Level.imax v (Level.imax u (Level.succ w)))
    isUnsafe := false
  }
  match env.addDeclCore 0 axiomDecl (cancelTk? := none) with
  | .error _ => IO.println "Could not add axiom"
  | .ok env1 => do
    let defDecl : Declaration := .defnDecl {
      name := `myUse
      levelParams := [`u, `v, `w]
      type := Expr.sort (Level.imax u (Level.imax v (Level.succ w)))
      value := Expr.const `myConst [u, v, w]
      hints := .regular 0
      safety := .safe
    }
    match env1.addDeclCore 0 defDecl (cancelTk? := none) with
    | .error e =>
      let msg ← (Kernel.Exception.toMessageData e {}).toString
      IO.println s!"Rejected: {msg}"
    | .ok _ => IO.println "Accepted"

Expected behavior: isEquiv returns true for semantically equal levels;
the kernel accepts the definition.

Actual behavior:

Bug 1:

normalize(e1) = (max u (v+1))+1
normalize(e2) = max (u+1) (v+2)
isEquiv = false

Bug 2:

Rejected: (kernel) declaration type mismatch, 'myUse' has type
    Sort (imax v u (w + 1))
but it is expected to have type
    Sort (imax u v (w + 1))

test_univ_normalization_bugs.lean.

Versions

Tested on:

• Lean 4.28.0 (7e01a1bf5c70)
• Lean 4.29.0-rc2 (83e54b65b65d)
• Linux x86-64

Additional Information

The root cause is in the IMax case of normalize.

C++ (src/kernel/level.cpp:448–451):

  case level_kind::IMax: {
      auto l1 = normalize(imax_lhs(r));
      auto l2 = normalize(imax_rhs(r));
      return mk_succ(mk_imax(l1, l2), p.second);
  }

Lean (src/Lean/Level.lean:392–397):

  | imax l₁ l₂ =>
      if l₂.isNeverZero then addOffset (normalize (mkLevelMax l₁ l₂)) k
      else
        let l₁ := normalize l₁
        let l₂ := normalize l₂
        addOffset (mkIMaxAux l₁ l₂) k

When mk_imax/mkIMaxAux converts an imax to a max (because the RHS is
never-zero), the resulting max is not passed through the Max normalization path.
This skips both succ distribution (bug 1) and sorting/flattening (bug 2, C++ only).

The Lean isNeverZero branch partially avoids this by calling
normalize (mkLevelMax l₁ l₂) which enters the Max path — but then
addOffset wraps succs on top without re-normalizing, causing bug 1.

I believe re-normalizing the result when mk_imax produces a max would
fix both issues, but I haven't tested a patch.

Impact

Low in practice. Normal Lean code goes through mkLevelIMax' which eagerly
simplifies imax u (succ v) to max u (succ v), preventing the raw imax
nodes that trigger this. The bug requires constructing raw Level.imax nodes
via metaprogramming, or possibly through universe instantiation in specific
patterns.

Start with src/kernel/level.cpp lines 448–451 and src/Lean/Level.lean lines 392–397, then run test_univ_normalization_bugs.lean against the reported Lean versions. Trace the IMax-to-Max normalization path in both implementations and verify that succ distribution, sorting, and flattening produce equivalent canonical levels and that the kernel accepts the definition.