Random assignment identifies the ATT (the second design, on the same skeleton as DiD)

[raphaelrrcoelho]

context

Identification/DiD.lean proves one design end to end: parallel trends identifies the
ATT (Model.att_eq_didContrast). It does that by rewriting each observed group mean
into the potential-outcome mean it equals almost everywhere
(Model.condMean_observed_post_treated / _control), then letting the identifying
restriction collapse the difference.

That is the shape every identification argument in this library will have, and right
now exactly one design uses it. Random assignment is the other benchmark design —
the one every applied paper compares itself to — and it is the natural second
instance of the same skeleton. It needs no new machinery: the realization lemmas, the
integrability transfer (MeasureTheory.Integrable.cond) and condMean_sub all already
exist and are all reused verbatim.

Stating it also makes the DiD theorem mean more by contrast: the two differ only in
which untestable restriction they assume, and having both on the page shows that on
the face of the statements rather than in prose.

task

State and prove that mean-independence of the untreated potential outcome from
assignment identifies the ATT: under that restriction, Model.att — which reads the
counterfactual Y false .post on treated units — equals the post-period difference in
observed group means, which reads only Observed fields.

Concretely, the conclusion is an equation between m.att μ and

condMean μ m.treated (m.observed.outcome .post)
  - condMean μ m.treatedᶜ (m.observed.outcome .post)

and the identifying hypothesis is

condMean μ m.treated (m.Y false .post) = condMean μ m.treatedᶜ (m.Y false .post)

Follow Model.ParallelTrends / Observed.didContrast and give both of these named
definitions rather than inlining them — the restriction is a statement about
counterfactuals and deserves to be named as one, and the estimator being a function of
Observed alone is the whole content of the claim. Inlining them into the theorem is
acceptable if naming turns out awkward, but the named form is the house shape.

Integrability hypotheses go on μ itself, not on the conditioned measures —
Integrable.cond transfers them, and "this outcome has a finite mean" is the weakest
form an econometrician would actually state. Follow Model.att_eq_didContrast
exactly here.

Note what is not needed and must not be assumed: IsProbabilityMeasure,
IsFiniteMeasure, or positivity of μ m.treated. ProbabilityTheory.cond degenerates
to the zero measure on a null event and the algebra survives it, exactly as it does in
the DiD proof. An unnecessary guard makes the theorem strictly weaker.

scope

Post-period only, and mean-independence only. Full statistical independence, the ATE
(as opposed to the ATT), and covariate-conditional versions are all separate statements
and are not in scope — the last of those needs the σ-algebra route through
MeasureTheory.condExp, which docs/phase0-verdict.md records as untested and as the
top residual risk.

acceptance criteria

• the identifying restriction and the observable estimator are named definitions,
  in the register of Model.ParallelTrends / Observed.didContrast.
• the identification theorem is proved, reusing the existing realization lemmas
  rather than re-deriving them.
• no IsProbabilityMeasure / IsFiniteMeasure / μ m.treated ≠ 0 hypothesis.
• axioms-clean ([propext, Classical.choice, Quot.sound]); lake build green;
  the entry declares its formalization_status and the ledger is re-verified.

pointers

• Econometrics/Identification/PotentialOutcomes.lean — Model, Observed,
  Model.observed, condMean, condMean_sub, Model.att.
• Econometrics/Identification/DiD.lean — Model.ParallelTrends,
  Observed.didContrast, Model.condMean_observed_post_treated,
  Model.condMean_observed_post_control, MeasureTheory.Integrable.cond, and
  Model.att_eq_didContrast as the proof to model this one on.