Verify YM C271 polar-conditioning firewall

[stevemoraco]

Public theorem-equivalent verifier for RH-Lean C271.

The source proves only a finite scalar shadow: the polar sign map has no uniform Lipschitz constant across arbitrarily near-singular opposite-sign inputs, and a fixed distance from the singular set gives a positive conditioning margin.

Failed-first run/job 32238731960 / 96024414078 is preserved as non-evidence: the initial Lean definition omitted noncomputable, causing failed declarations and sorryAx, and the strict wrapper also caught unused premises.

Clean repaired replay:

source head: e79e249120d5e67d1f1a98b1372f9c1f3de71de4
source SHA-256: b3edbf271a1d6cf9346bf48821934f6cd661c70c5dc8799c40347eb56875767c
run/job: 32238932147 / 96025024195
AXLE Lean: 4.30.0
okay: true
cached_response: false
failed declarations: []
Lean errors/warnings: [] / []
tool errors/warnings: [] / []
axiom union: {propext, Classical.choice, Quot.sound}
artifact: 9360005359
artifact ZIP SHA-256: 86561221f61cdf7b90a196a289d3826be0386a38676b3eac3b3f20d4c043c66e

This does not formalize SU(N), path holonomies, the matrix polar decomposition, the Yang–Mills block map, Gaussian chart factorization, RG, OS reconstruction, Yang–Mills, or a mass gap. FIVE-ALARM OFF.