ForMathlib: upstream candidates tracker

[cameronfreer]

Tracker for declarations kept under Graphon/ForMathlib/: statements that are signature-free, depend only on Mathlib, and are plausible upstream contributions. Nothing here is being upstreamed yet. This issue records candidacy and the promotion bar; the actual PR to Mathlib is a separate decision, taken per declaration and not before the bar below is met.

Promotion bar

A candidate is marked Hardened only once it has been consumed independently by at least two real call sites — for the current batch, I(1) and a later rank transition. Two independent consumers are what distinguish a tested orientation of the API from a speculative one; a single consumer tells us only that the statement was convenient for the theorem it was extracted from. Until then a candidate stays Provisional and its signature may change freely.

Current candidates

From #159 (Graphon/ForMathlib/RelativeFactorCoupling.lean):

• ProbabilityTheory.map_condDistrib_id — Provisional. Fibre concentration: (condDistrib id q μ).map q =ᵐ[μ.map q] Kernel.id. Belongs beside condDistrib_comp and condDistrib_self in Mathlib/Probability/Kernel/CondDistrib.lean; it is the missing "conditioning on q pins down q" statement, and both supporting lemmas (condDistrib_id_apply_fibre, ae_ae_eq_condDistrib_id) are immediate from it.
  • Consumers so far: the relative joining in the same file. Needs one genuinely independent consumer.
• ProbabilityTheory.relativeFactorCoupling and its API — Provisional. The relatively independent joining over a common factor, with both marginals, the common-factor identity, and condIndepFun_fst_snd_relativeFactorCoupling. Mathlib has the disintegration and conditional-independence machinery but not this canonical joining.
  • Consumers so far: exists_relativeFactorCoupling_uniform01 (feat: relatively independent joinings over a common factor (#107) #159), which is a specialization rather than an independent use.

Not candidates

Recorded to keep the boundary explicit — these either have one consumer or already compose cleanly from Mathlib primitives, and abstracting them now would cost more than it saves:

• the rank-one finite-family peel (iCondIndepFun_exactMap_singleton);
• a general "kernel concentrated on fibres" predicate — the two a.e. statements above suffice at every site so far;
• the short projection calculations using Kernel.fst_prod / Kernel.snd_prod;
• a general conditional-distribution transport theorem (Incubate and upstream reusable measure/probability infrastructure (Mathlib / Tau Ceti) #24).

Related: #107, #140, #159.

[cameronfreer]

Two additions to Graphon/ForMathlib/RelativeFactorCoupling.lean from #161, both Provisional:

• ProbabilityTheory.map_prodMap_relativeFactorCoupling — a measure-preserving T with q ∘ T = q gives Prod.map T id preserving the joining. Consumer so far: map_prodMap_relabel_rankOneCoupling (I(1)).
• ProbabilityTheory.condIndepFun_comp_fst_snd_relativeFactorCoupling — the transfer clause, conditional independence passed to any measurable reading of the first coordinate. One line from Mathlib's CondIndepFun.comp; named because it is what consumers cite. Consumer so far: condIndepFun_comp_fst_snd_rankOne (I(1)).

Both were driven by I(1) rather than added speculatively, so they meet the "driven by a real consumer" bar — but each has exactly one consumer, and I(1) is the first of the two the promotion bar requires. The later rank transition is the second. Neither is Hardened.

Note for that transition: I(1) leans on the rank-one factor being relabeling invariant on the nose (lowerFactorMap_one_relabel), which holds only because LowerIndex 1 is anchored at ∅. At higher rank the factor map is merely equivariant, so the second consumer will exercise map_prodMap_relativeFactorCoupling in a genuinely different shape — the factor space has to move by lowerFactorSpaceEquiv on the other side. That is the right kind of second consumer for hardening: it will show whether the current signature (a symmetry T of a single space fixing the factor) is the useful orientation, or whether it wants a two-space form with a factor-space equivalence.

[cameronfreer]

Correction to the candidate list, from review of #161 (now merged).

ProbabilityTheory.condIndepFun_comp_fst_snd_relativeFactorCoupling is not an upstream candidate. It is a discoverability wrapper around Mathlib's CondIndepFun.comp — the composition lemma already exists upstream, and this adds only the specialization to relativeFactorCoupling, which would have no meaning in Mathlib unless the joining itself went up first. It stays local and is removed from the tracked list; the promotion bar does not apply to it. It is still worth keeping as a named statement here, because it is what downstream consumers cite rather than re-deriving.

That leaves the candidate list as:

• ProbabilityTheory.map_condDistrib_id — Provisional. Fibre concentration.
• ProbabilityTheory.relativeFactorCoupling and its core API — Provisional. The joining, both marginals, the common-factor identity, condIndepFun_fst_snd_relativeFactorCoupling.
• ProbabilityTheory.map_prodMap_relativeFactorCoupling — Provisional, and the more substantive of the two additions from feat: I(1), the rank-one transfer step (#107) #161: a symmetry of the first space fixing the factor is a symmetry of the joining. It says something about the construction that is not a specialization of an existing Mathlib lemma.

Scope notes recorded while they are fresh:

• The relabeling statement in RelRankOneTransfer is finitary (FinSuppPerm) and that is the exact boundary, not a limitation to fix — the coherent basis is closed under FinSuppPerm and the invariance of empty-anchor events is proved from exactly that closure. Any measure-level or full-permutation formulation should be driven by higher-rank use, not added speculatively.
• No unresolvedStructure object. The theorem quantified over every measurable g is strictly stronger and avoids committing to a particular residual object. A name is warranted only if the recursion introduces a canonical residual state that recurs.