`NormLevel.subsumption_eval` is false for arbitrary NormLevel

[thomasahle]

Summary

NormLevel.subsumption_eval currently claims that subsumption preserves evaluation for every NormLevel:

theorem NormLevel.subsumption_eval {s : NormLevel} :
      s.subsumption.eval ls ρ = s.eval ls ρ := by sorry

But this is false for malformed internal maps. The subsumption algorithm relies on representation invariants established by normalizeAux, but these invariants are not reflected in the theorem statement or the NormLevel type.

This does not currently demonstrate incorrect normalization of an actual Lean.Level; it demonstrates that the general preservation theorem is too strong, or that subsumption needs hardening for arbitrary inputs.

Counterexample

The following example compiles against current master:

import Lean4Lean.Verify.Level

open Lean Lean.Level Lean.Level.Normalize

def malformed : NormLevel :=
  (({ inner := {} } : NormLevel).insert
      [] { var := [⟨`y, 0⟩] }).insert
    [`a] { const := 5, var := [⟨`x, 4⟩] }

#eval malformed.eval [`a, `x, `y] [1, 0, 0]
-- 5

#eval malformed.subsumption.eval [`a, `x, `y] [1, 0, 0]
-- 4

The node at path [`a] contains the constant 5 and the variable term x + 4. Since a = 1, that node evaluates to:

max 5 (x + 4) = max 5 4 = 5

During subsumption, the constant is cleared. The relevant test is:

n₁.const > n₁.var.foldl (·.max ·.offset) 0 + 1

Here that becomes 5 > 4 + 1, which is false. The implementation therefore assumes that the variable attaining offset 4 is positive whenever the path is active. That would be valid if the variable were a, or otherwise occurred in the path, but the malformed node contains x, whose assigned value is zero.

After clearing the constant, the map evaluates to 4.

Suggested improvement

The preferred fix is to make the representation invariant explicit:

theorem NormLevel.subsumption_eval
    (hs : s.WF) :
    s.subsumption.eval ls ρ = s.eval ls ρ := by
  ...

NormLevel.WF should capture the invariants required by subsumption, including at least:

• key paths are ordered and duplicate-free;
• variable lists are ordered and duplicate-free;
• variables whose positivity is used to subsume a constant occur in the corresponding path;
• the required parent/subpath nodes are present;
• domination facts established during the fold remain represented elsewhere in the map.

Then normalizeAux should be shown to produce or preserve this invariant, allowing normalize_eval to use the corrected theorem.

A narrower alternative is to state preservation only for maps reachable from normalizeAux, avoiding a public invariant until its exact formulation is settled:

theorem normalizeAux_subsumption_eval
    {s : NormLevel}
    (hs : s is produced by a valid normalizeAux run) :
    s.subsumption.eval ls ρ = s.eval ls ρ := by
  ...

Another possible fix is to harden subsumption by checking the required path-membership condition before using offset + 1 to discard a constant. That would make the operation safer on arbitrary maps, but an invariant is still useful for proving the other subsumption steps and documenting the internal representation.

With the invariants in place, I believe a proof can be build without too much work.

Reachability note

I also tested all generated level expressions through depth two over three parameters—3,280 expressions and 125 parameter assignments—and found no mismatch between normalization and direct VLevel evaluation. This is not a proof, but it supports the diagnosis that the counterexample violates an internal invariant rather than exposing a reachable normalization failure.