Second FTAP, the converse: unique martingale measure ⟹ complete

[raphaelrrcoelho]

context

MathFin/Foundations/MarketCompleteness.lean proves one direction of the second FTAP, and says so in
its "scope: one direction only" block. measure_eq_of_pricesGainsAtZero shows every gains-neutral
measure dominated by μ agrees with μ on 𝓕ᴮ_T, and emm_unique_of_complete is the corollary on
ContinuousMarket.IsEMM. the converse, unique martingale measure ⟹ complete, is absent.

task

prove the converse. the standard route is the extreme-point characterisation of the set of martingale
measures (jacod–yor): a martingale measure is an extreme point of that set exactly when the stable
subspace generated by the price process is dense in L¹, and a singleton set is trivially a set of
extreme points, so uniqueness gives density and hence replication.

concretely that means:

1. the set of martingale measures as a convex set, with the extreme-point predicate on it.
2. the stable subspace generated by a price process, and the jacod–yor equivalence.
3. the converse read off from a singleton set.

the honest note in MarketCompleteness.lean:60-67 is that this is additive: a new characterisation of
the EMM set, not a rewrite of what is there. worth re-reading before starting, since it also records why
the forward direction had to hypothesise PricesGainsAtZero: the missing ∫ φ dS is the same gap, and
the converse will meet it too.

acceptance criteria

• a full entry for the converse, or an honest re-scoping if the ∫ φ dS gap blocks it.
• the scope paragraph in MarketCompleteness.lean updated so it no longer says the converse is
  absent.
• axioms-clean; coverage row + audit + ledger updated.

pointers

• MathFin/Foundations/MarketCompleteness.lean, Foundations/ContinuousMarket.lean (IsEMM, and the
  deliberate absence of ∫ φ dS), Foundations/MartingaleRepresentation.lean.
• Foundations/FTAPDiscrete.lean and FTAPOnePeriodVector.lean for the finite-state shape of the
  statement.