One-selected-block Fubini closure for R-322

This file isolates the signed Fubini step used when the deterministic smallest-leftmost selector removes one proper primitive block. The first checkpoint is the exact product-measure reindex: selected coordinates are integrated on the inside and all complement coordinates remain on the outside.

theorem Anderson4D.integral_pi_eq_integral_complement_integral_selected {ι : Type u_1} {X : Type u_2} [Fintype ι] [MeasurableSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.SigmaFinite μ] (selected : ι → Prop) [DecidablePred selected] (f : (ι → X) → ℝ) (hf : MeasureTheory.Integrable f (MeasureTheory.Measure.pi fun (x : ι) => μ)) : (∫ (x : ι → X), f x ∂MeasureTheory.Measure.pi fun (x : ι) => μ) = ∫ (xC : { i : ι // ¬selected i } → X), ∫ (xB : { i : ι // selected i } → X), f ((MeasurableEquiv.piEquivPiSubtypeProd (fun (x : ι) => X) selected).symm (xB, xC)) ∂MeasureTheory.Measure.pi fun (x : { i : ι // selected i }) => μ ∂MeasureTheory.Measure.pi fun (x : { i : ι // ¬selected i }) => μ

Exact signed Fubini reindex for one selected finite coordinate block.

The measurable equivalence remembers both pieces of the original tuple, so the integrand is not replaced by an absolute-value majorant. The selected coordinates occur in the inner integral, as required by the inside-to-outside collapse in paper Section 4.1.