Enable --wfail axiom-guard gate once warnings are clean

The lean_extensions axiom-guard plugin is now wired into the build (see the feat/axiom-guard PR). It warns when a declaration depends on a non-standard axiom (anything beyond propext, Quot.sound, Classical.choice; sorry included).

CI currently runs a plain lake build (via leanprover/lean-action@v1), so these warnings are surfaced but do not fail the build. We cannot yet enforce the gate with lake build --wfail because the existing regex code uses sorry, which the guard reports as a dependency on the non-standard axiom sorryAx. Running lake build --wfail locally exits 1 on the following pre-existing declarations:

Lck/Regex/Parser.lean:77:0:  `Lck.Regex.parseCharClassContents` depends on non-standard axiom `sorryAx`
Lck/Regex/Parser.lean:107:0: `Lck.Regex.parseCharClass` depends on non-standard axiom `sorryAx`
Lck/Regex/Parser.lean:126:0: `Lck.Regex.parseAtom` depends on non-standard axiom `sorryAx`
Lck/Regex/Parser.lean:147:0: `Lck.Regex.parseRepetition` depends on non-standard axiom `sorryAx`
Lck/Regex/Parser.lean:160:0: `Lck.Regex.collectAtoms` depends on non-standard axiom `sorryAx`
Lck/Regex/Parser.lean:197:0: `Lck.Regex.parseConcat` depends on non-standard axiom `sorryAx`
Lck/Regex/Parser.lean:202:0: `Lck.Regex.collectAlternates` depends on non-standard axiom `sorryAx`
Lck/Regex/Parser.lean:232:0: `Lck.Regex.parseAlternation` depends on non-standard axiom `sorryAx`
Lck/Regex/Parser.lean:237:0: `Lck.Regex.parse` depends on non-standard axiom `sorryAx`
Lck/Regex/Matcher.lean:102:0: `Lck.Regex.epsilonClosure` depends on non-standard axiom `sorryAx`
Lck/Regex/Matcher.lean:138:0: `Lck.Regex.step` depends on non-standard axiom `sorryAx`
Lck/Regex/Matcher.lean:149:0: `Lck.Regex.matchesString` depends on non-standard axiom `sorryAx`
Lck/Regex/Matcher.lean:172:0: `Lck.Regex.matchesAt` depends on non-standard axiom `sorryAx`
Lck/Regex/Matcher.lean:195:0: `Lck.Regex.matchesLine` depends on non-standard axiom `sorryAx`
Lck/Regex/Regex.lean:18:0:   `Lck.Regex.compile` depends on non-standard axiom `sorryAx`
Lck/Regex/Regex.lean:24:0:   `Lck.Regex.matchFull` depends on non-standard axiom `sorryAx`
Lck/Regex/Regex.lean:29:0:   `Lck.Regex.matchCompiled` depends on non-standard axiom `sorryAx`
Lck/Regex/Regex.lean:33:0:   `Lck.Regex.search` depends on non-standard axiom `sorryAx`
Lck/Regex/Regex.lean:38:0:   `Lck.Regex.searchCompiled` depends on non-standard axiom `sorryAx`
test/Main.lean:6:0:          `main` depends on non-standard axiom `sorryAx` (transitive, via the regex lib under test)

These all stem from the sorry placeholders in Lck/Regex/Parser.lean and Lck/Regex/Matcher.lean; Regex.lean and test/Main.lean inherit them transitively.

Once these sorrys are discharged (or otherwise removed), switch CI from the plain lake build to lake build --wfail to turn the axiom guard into a hard gate. With leanprover/lean-action@v1 this is build-args: "--wfail".

Inizia eseguendo lake build --wfail e passa in rassegna le dichiarazioni elencate in Lck/Regex/Parser.lean e Lck/Regex/Matcher.lean, da cui provengono i segnaposto sorry. Controlla i report transitivi in Lck/Regex/Regex.lean e test/Main.lean; il lavoro è completato quando questi avvisi sono scomparsi e CI usa build-args: "--wfail" con leanprover/lean-action@v1.