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.

Beginne in Lck/Regex/RegexSpec.lean, indem du regex_search_correct und die bestehende desugar_fullMatch_semantics-Brücke liest. Verfolge, wie das .* Wrapping Matches dr.toRegex mit MatchesSubstring ast in Beziehung setzt, und beweise dann die angegebene Äquivalenz regex_search_ast_correct. Erledigt ist die Aufgabe, wenn der Theorem kompiliert und die Ergebnisse des Suchmodus mit der ursprünglichen AST-Semantik verbindet.