test: cover allowedAxioms via lakefile leanOptions in consumer

[Oppen]

Summary

• Exercise the linter.axiomGuard.allowedAxioms option through the lakefile configuration path of the plugin-consumer package (previously only covered per-file via set_option ... in in the import-based fixtures).
• test/consumer/lakefile.lean allow-lists Consumer.benign and Consumer.alsoBenign project-wide:

  lean_lib Consumer where
    plugins := #[axiomGuardPlugin]
    leanOptions := #[⟨`linter.axiomGuard.allowedAxioms, "Consumer.benign, Consumer.alsoBenign"⟩]

• New fixtures: axiom alsoBenign plus uses_benign/uses_benign_also theorems in the consumer, value string exercises both separators (comma and space).
• test/run.sh gains two assertions: no guard warning may mention the allow-listed axioms (neither at the axiom declaration sites nor at use sites), and evil must still be flagged.

Verification

• test/run.sh: 10 passed, 0 failed.
• Negative control: with the leanOptions line removed, all six warnings fire (evil/benign/alsoBenign at declaration and use sites) — the option is load-bearing.
• The -D flag only validates because lake build passes --plugin (registering the option) alongside it; a bare lake env lean -Dlinter.axiomGuard.allowedAxioms=... is rejected with "unknown configuration option". Documented in the lakefile comment.