ch:first-class-universe-levels: finite-map levels

Problem and invariant. Decide the join-semilattice level equations by a canonical finite map. Store at most one greatest successor exponent for each generator, and remove every constant exponent absorbed by a variable exponent.

Representation and construction. Represent level expressions by zero, variable, successor, and join. Normalize zero to the empty map, join by pointwise maximum, and successor by incrementing all entries, inserting the first constant exponent when needed. Implement equality by map equality and below by normalizing one further join.

Observable result and mutation. Require equal, equal, not-below, and the summary line shown in Appendix E. Replacing maximum by minimum at join still checks but changes the final line to below; the test fails.

Acceptance and boundary. Match the accepted source record in Appendix E. Run the four Appendix-E commands. Restore and rerun after mutation. The program proves no normalization, conversion, or typing result for the first-class-level theory.