diaz-modulus-lean: a Palomar submission surface on its palomar branch

diaz-modulus-lean gained a Palomar submission surface on its palomar branch, parallel to the erdos-straus-offset-lean one: an axiom-free core, a Challenge.lean that imports full Mathlib so the statements match on the nose, and a companion note with attribution and search record. The repo also picked up an Apache-2.0 licence at the root.