We formalize the leading-order asymptotic analysis as an elementary example of abstract interpretation. The formalism omits complete partial orders and fixed-point iteration while retaining the Galois connection and assertion checking. This isolates the notion of semantic approximation from the heavier mathematical machinery to handle loops and recursion. We implement and partially mechanize the formalism in Lean. We also implement an interactive shell and fuzzer for experimentation with the key ideas of abstraction, soundness, and overapproximation, making abstract interpretation more approachable. This suggests a pathway toward lightweight pedagogical frameworks for teaching core ideas in program analysis.