CPP Weakness Kernel

What is the algebraic structure of observational equivalence? The CPP weakness relation on process terms is more than a preorder — it carries meet-quantale structure: a complete lattice with an associative tensor operation distributing over joins. This project formalizes the weakness kernel, constructs the meet-quantale completion, proves frame distributivity (finite meets over arbitrary joins), and connects to Mathlib’s locale theory for pointless topology. The result is a reusable algebraic core for any system requiring compositional refinement.