feat(Geometry): add Gauss-Bonnet

[ocfnash]

No description provided.

[kim-em]

🤖 Claude says:

The docstring and the hypothesis disagree on the normalisation, and it is the docstring that is wrong.

hμ says μ = (NNReal.pi / 4) • μH[2], while the docstring says μ is "4 / π times the Hausdorff area measure". π/4 is the correct factor: Mathlib's μH is unnormalised, so on a Euclidean 2-space μH[2] = (4/π) • area, hence area = (π/4) • μH[2]. The prose has it inverted.

Worth fixing deliberately rather than as a typo, because the constant is load-bearing. If μ were c • area for any c ≠ 1, then μ (ball x r) = c(π r² - (π/12) K r⁴ + o(r⁴)), so the numerator of Q retains a (1 - c) π r² term, Q r → ∞ as r → 0⁺, and hK becomes unsatisfiable: the theorem would be vacuously true. The statement is right as it stands, but anyone "fixing" it to match the comment would silently trivialise the problem.

Since this is the declaration docstring rather than the module docstring, it also ships to solvers in the generated Challenge.lean.

[ocfnash]

-awaiting-author