Infer Ma-Wang step certificates

[PerAlexandersson]

Summary:

• add zero-argument rr_ma_wang, rr_ma_wang_same, and rr_ma_wang_succ overloads
• discover only exact local or uniquely tagged splitting, degree, leading-coefficient, and root-sign certificates through rr_lookup
• delegate to the existing explicit frontends and proved prec_ma_wang declarations
• retain every explicit syntax form as a diagnostic fallback
• add checked general, same-degree, and successor-degree examples, including an unrelated decoy certificate packet

Verification:

• focused external-cache build of RealRooted.Tactic.Examples.MaWang
• full external-cache build of RealRooted (8951 jobs)
• python3 scripts/check_root_imports.py
• git diff --check and line-length/placeholder scans
• independent read-only implementation review

No theorem files or non-tactic modules are changed.