Function gen_univ

crates/kernel/src/level.rs:1052–1073

Generate a bounded-depth `KUniv `. Parameter indices are drawn from `0..=max_param` so multiple universes in the same test can share parameters — important for geq transitivity tests.

(rng: &mut UPrng, depth: u32, max_param: u64)

    assert!(univ_eq(&lhs, &rhs));
    assert!(univ_eq(&rhs, &lhs));
    // Geq agrees in both directions (norm_level_le already skipped
    // empty entries — this is the antisymmetry pair univ_eq now matches).
    assert!(univ_geq(&lhs, &rhs));
    assert!(univ_geq(&rhs, &lhs));
    // Control: the comparator did not get weaker — a semantically
    // distinct near-miss stays distinct (at u=v=0: lhs=1, other=0).
    let smaller = AU::max(u.clone(), v.clone());
    assert!(!univ_eq(&lhs, &smaller));
    assert!(!univ_eq(&smaller, &lhs));
  }

  #[test]
  fn univ_geq_basic() {
    let z = AU::zero();
    let s1 = AU::succ(z.clone());
    let s2 = AU::succ(s1.clone());
    let p = AU::param(0, ());
    assert!(univ_geq(&z, &z));
    assert!(univ_geq(&s1, &z));
    assert!(univ_geq(&p, &z));
    assert!(univ_geq(&s2, &s1));
    assert!(!univ_geq(&s1, &s2));
  }

  #[test]