1. The setup on a connected support
This page proves that every finite law p whose support is connected has a setup latent: a finite latent L that
attains \tau(p), with positive priors and pairwise distinct components, all of which are contacts of one common
feasible kernel, are positive on the whole support, and give positive posterior rows there. The proof has three steps:
an optimal latent and an affine minorant of the component functional \phi (Lemma S1.2), a normalization that turns
the minorant into one feasible kernel whose contacts are exactly the components with zero gap (Lemma S1.3), and the
propagation of positivity along the connected support (Lemma S1.4); Lemma S1.1 is the cost identity they rest on. The
assembly NaturalLatents.General.T_le_of_connected (NaturalLatents/General/Pricing.lean) starts by obtaining this
setup from exists_setup_of_connected. It applies the race to the setup latent and its positive posterior rows, forms
each pair of distinct components as two positive contacts of the common kernel for the contact moments
and the affinity bound, passes the whole setup to the mismatch payment, and uses M+B=\tau(p) in its
last step, as steps 1 to 8 of the route describe.
Each lemma below states its hypotheses, so that it can be read alone. Unless prefixed stoch_to_det, the Lean
declarations named below are in the namespace NaturalLatents.General; the stoch_to_det declarations are in
NaturalLatents/Upstream/, adapted from DLorell/stochtodet (see the
upstream inputs). The analytic content of Lemmas S1.2 to S1.4 is proved in Lean by that upstream code;
only the final assembly is in NaturalLatents/General/Setup.lean. The exceptions to the naming rule are the
declarations called private below (Valid, exists_approx_valid_certificate, exists_optimal_valid_certificate,
exists_tau_optimal_kernel, valid_iff_feasible, maximizer_rpow_two_thirds, Gdef_eq_certificate_gap and
Gdef_eq_zero_iff): they are Lean-private declarations in the namespace stoch_to_det, in the public file
NaturalLatents/Upstream/Duality.lean.