Infer matrix preservation certificates

[PerAlexandersson]

Summary

• extend rr_lookup to consume complete forall certificates and parameterized certificate prefixes without leaking metavariable assignments
• add bare inferred matrix and row-threshold frontends backed by proved matrix preservation theorems
• cover decoy certificates, typeclass synthesis, inferred weak endpoints, and multi-matrix selection with checked examples

Verification

• lake ... build RealRooted.Tactic.Examples.Lookup RealRooted.Tactic.Examples.Matrix (external cache; 8626 jobs)
• lake ... build RealRooted (external cache; 8951 jobs)
• python3 scripts/check_root_imports.py
• python3 scripts/generate-oeis-tactic-coverage.py --check
• git diff --check
• touched-file line-length and placeholder scans

Only existing proved matrix preservation declarations are invoked; this adds no theorem assumptions or sequence-specific APIs.