Formalize closure, DSI, and contraction identities

[rickyjreyes]

Summary

Adds a paper-level Lean formalization batch drawn from the August 2026 WCT closure, compact-dynamics, and WCT-DSI revisions.

Added kernel targets

• exact DSI/WCT positive-log-coordinate scale-ratio definition
• DSI forward/inverse round-trip theorems under explicit nonzero/positivity hypotheses
• exact DSI/WCT log-frequency matching identity
• exact quartic square completion behind the coercivity absorption estimate
• nonnegativity of the coercivity remainder for positive eta
• strict averaged-update contraction factor 1 - L*delta
• perturbation factor 1 - L*delta + epsilon
• sufficient margin epsilon <= L*delta for norm nonexpansion

Scope

This deliberately does not claim the full Lions concentration-compactness theorem, free-space minimizer theorem, full complex quotient first variation, nonlinear PDE well-posedness, or empirical validation.

These are paper-level theorem additions and therefore do not automatically change the canonical 80/142 equation-specific coverage count without a separate exact registry mapping.

Validation

All current PR workflows pass:

• Pinned Lean 4.23 / Mathlib formal reproducibility build: PASS
• Formal source audit: PASS
• Pinned Lean container CI: PASS

The first CI attempt exposed only mechanical Lean issues (noncomputable, explicit division cancellation, and 1 * ||x|| simplification); those were patched before the green build.