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.

Lck/Regex/RegexSpec.lean で regex_search_correct と既存の desugar_fullMatch_semantics ブリッジを読むことから始めます。.* のラップが Matches dr.toRegex と MatchesSubstring ast をどのように関連付けているかをたどり、続いて示されている regex_search_ast_correct の同値性を証明します。定理がコンパイルされ、検索モードの結果と元の AST セマンティクスが接続されれば完了です。