1.7. Verification boundary🔗

All correctness statements are proved in Lean. The module-boundary tests exercise array construction, vector updates, tree-map operations, exact division, and deterministic randomness after importing the public umbrella, so accidental opacity is caught by the ordinary build. HexBasic uses no external oracle and introduces no native runtime dependency.