Add unit-level contrasts and finite-population average effects

[bocowgill]

Closes #43.

Adds the next small layer on top of PotentialResponse: unit-level contrasts and their average over a finite population.

Changes

• Define PotentialResponse.contrast with only [Sub Value], its application simp lemma, and the named contrast_self and contrast_swap laws under [AddGroup Value].
• Define PotentialResponse.finitePopulationAverageContrast as the uniform Finset.expect over all of the finite type Unit. For empty Unit, zero is an algebraic convention, not a substantive causal claim.
• Prove that the average contrast equals the difference of the two average responses.
• Add the new module to Statlib.lean.

This PR adds estimands only. When interventions encode two unit-level treatments, the finite average is the conventional ATE; with complete allocation vectors, it compares regimes without assuming noninterference. It does not add assignment mechanisms, observed outcomes, causal assumptions, identification, estimators, or inference.

More general or weighted contrasts, explicit finite-subset averages, and superpopulation effects are follow-ups, not requirements of this PR.

Checks

• lake build Statlib.Causal.PotentialResponse.Contrast
• lake build
• lake lint
• lake exe mk_all --check
• git diff --check