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.

Inizia in Lck/Regex/RegexSpec.lean leggendo regex_search_correct e il bridge esistente desugar_fullMatch_semantics. Traccia il modo in cui il wrapping .* mette in relazione Matches dr.toRegex con MatchesSubstring ast, quindi dimostra l’equivalenza regex_search_ast_correct indicata. Il lavoro è terminato quando il teorema compila e collega i risultati della modalità di ricerca alla semantica originale dell’AST.