Spatial Fubini for an arbitrary analytic R-322 block

The paper-order schedule need not begin with the cardinality-first block of the combinatorial extraction recursion. The physical integral can nevertheless put the coordinates of any certified analytic block on the inside. This file records that reindex directly for the original endpoint-fibre sum.

theorem Anderson4D.endpointFiberDetJSum_eq_blockSpatialFubini (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (B : Finset (Fin (2 * q))) (z : T4) (hint : ∀ (τ : ReductionEndpointFiberAt κ), MeasureTheory.Integrable (fun (v : Fin (2 * q - 2) → T4) => detJintegrand ρ ε q (↑τ) (primitiveAssemble q hq z 0 v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * q - 2)) => paperMeasure)) : endpointFiberDetJSum ρ lam ε q (reductionEndpointSignature κ) z = lamEps lam ε ^ (2 * q) * ∫ (vC : { i : Fin (2 * q - 2) // ¬r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq B) i } → T4), ∫ (vB : { i : Fin (2 * q - 2) // r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq B) i } → T4), ∑ τ : ReductionEndpointFiberAt κ, detJintegrand ρ ε q (↑τ) (primitiveAssemble q hq z 0 (r322MergeSelectedFinCoordinates (r322InternalCoordinatesOfBlock q hq B) vB vC)) ∂MeasureTheory.Measure.pi fun (x : { i : Fin (2 * q - 2) // r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq B) i }) => paperMeasure ∂MeasureTheory.Measure.pi fun (x : { i : Fin (2 * q - 2) // ¬r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq B) i }) => paperMeasure

Exact signed Fubini form of the actual grouped kernel for an arbitrary ambient block B. No pairing sum is split and no absolute value is taken.

theorem Anderson4D.endpointFiberDetJSum_eq_analyticStepSpatialFubini (ρ : SmoothCutoff) (lam ε : ℝ) {q : ℕ} (hq : 1 ≤ q) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (step : R322ExtractionStep (2 * q)) (_hstep : step ∈ r322AnalyticSchedule κ) (z : T4) (hint : ∀ (τ : ReductionEndpointFiberAt κ), MeasureTheory.Integrable (fun (v : Fin (2 * q - 2) → T4) => detJintegrand ρ ε q (↑τ) (primitiveAssemble q hq z 0 v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * q - 2)) => paperMeasure)) : endpointFiberDetJSum ρ lam ε q (reductionEndpointSignature κ) z = lamEps lam ε ^ (2 * q) * ∫ (vC : { i : Fin (2 * q - 2) // ¬r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq step.2) i } → T4), ∫ (vB : { i : Fin (2 * q - 2) // r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq step.2) i } → T4), ∑ τ : ReductionEndpointFiberAt κ, detJintegrand ρ ε q (↑τ) (primitiveAssemble q hq z 0 (r322MergeSelectedFinCoordinates (r322InternalCoordinatesOfBlock q hq step.2) vB vC)) ∂MeasureTheory.Measure.pi fun (x : { i : Fin (2 * q - 2) // r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq step.2) i }) => paperMeasure ∂MeasureTheory.Measure.pi fun (x : { i : Fin (2 * q - 2) // ¬r322SelectedFinPredicate (r322InternalCoordinatesOfBlock q hq step.2) i }) => paperMeasure

Schedule-step specialization of the arbitrary-block Fubini identity.