proof: add bridge theorem connecting search-mode Matches dr.toRegex to MatchesSubstring ast

Problem

regex_search_correct in Lck/Regex/RegexSpec.lean states correctness in terms of Matches dr.toRegex input (the desugared form) rather than MatchesSubstring ast input (the original AST).

The full-match variant has desugar_fullMatch_semantics for this bridge, but search mode does not.

Goal

Prove a theorem of the form:

theorem regex_search_ast_correct (pattern input : String) :
    Regex.search pattern input = .ok true ↔
    (∃ ast, parse pattern = .ok ast ∧ MatchesSubstring ast input)

This requires connecting the .*-wrapped desugared form back to MatchesSubstring.

References

Raised in AI code review.

Comienza en Lck/Regex/RegexSpec.lean leyendo regex_search_correct y el puente existente desugar_fullMatch_semantics. Traza cómo el envoltorio .* relaciona Matches dr.toRegex con MatchesSubstring ast y, a continuación, demuestra la equivalencia regex_search_ast_correct indicada. La tarea está terminada cuando el teorema compila y conecta los resultados del modo de búsqueda con la semántica original del AST.