putnam_2013_a5: use EuclideanSpace so area3 measures Euclidean area

[logical-ivan]

Addresses #277 for putnam_2013_a5, following exactly the resolution Joseph Myers proposed there.

What

A type-only change to lean4/src/putnam_2013_a5.lean: the ambient types Fin 2 → ℝ / Fin 3 → ℝ become EuclideanSpace ℝ (Fin 2) / EuclideanSpace ℝ (Fin 3) (in the area2/area3 signatures and the two A : binders). harea2, harea3 and the conclusion are character-for-character unchanged — 4 lines touched, no new definitions.

The defect

The problem is about ordinary Euclidean areas of triangles, but Fin 3 → ℝ carries Mathlib's Pi instance, i.e. the supremum norm, and μH[2] is built from EMetric.diam, so harea3 computes the 2-dimensional Hausdorff measure of the ℓ∞ metric. That is not "area scaled by a constant": its ratio to Euclidean area varies with the plane's orientation (1 on coordinate planes vs 4/(3√3) ≈ 0.77 on the plane orthogonal to (1,1,1)). Meanwhile harea2's volume on Fin 2 → ℝ is genuine Lebesgue area, so the two sides of the implication measure different geometries. The mismatch is fatal to the intended projection-and-averaging solution: the ℓ∞ Busemann 2-area admits no positive Crofton measure (it violates Hlawka's inequality), so no analogue of the "integrate |n·n̂| over the sphere and factor out the constant" step exists, and the statement as written appears to be substantially harder than the Putnam problem.

Why the fix is correct (and why unnormalized μH[2] is fine)

μH[2] is unnormalized — Mathlib's Hausdorff measure carries no ω_d/2^d factor — so it doesn't literally equal Euclidean area: on any 2-dimensional affine subspace of EuclideanSpace ℝ (Fin 3) one gets μH[2] = (4/π) × Euclidean area. The key point is that this is a single constant, the same for every plane, because the Euclidean metric is rotation-invariant. Since area-definiteness is of the form ∑ aᵢⱼₖ · area(…) ≥ 0 quantified over configurations, it is invariant under multiplying the area functional by any positive constant — so the EuclideanSpace statement is equivalent to the original problem, exactly as predicted in #277 ("area scaled by some positive constant… scaling the area doesn't actually matter to the statement"). The same argument covers the constant mismatch with harea2 (true area, constant 1): each side's predicate is separately scale-invariant.

Notes

• This matches how putnam_2019_a4 — the other instance mentioned in Fix 2013 A5 #277 — already states μH[2] on EuclideanSpace ℝ (Fin 3) on current main.
• We have machine-checked verification for the claims above and are happy to share it privately (keeping proofs out of public view per the benchmark's policy).
• A similar sup-norm artifact affects putnam_1975_b2 (‖normals i‖ = 1 with normals : ℕ → (Fin 3 → ℝ) reads as the sup norm, weakening the intended statement); we can file that separately if useful.

🤖 Generated with Claude Code

[GeorgeTsoukalas]

This looks correct to me - thanks for the justification!