Reconstructed outer Fubini for one R-322 proper step

This file exposes the pre-collapse local factor in the same primitiveChainProduct × primitiveCovarianceProduct form obtained from the actual endpoint-fibre block coordinate. It then carries an arbitrary outer coordinate and outer factor through the signed block integral.

The one remaining global identification is pointwise: the processed endpoint-fibre skeleton on a reconstructed ambient tuple must equal rawLocalIntegrand * outer. No analytic estimate or new integrability claim is needed after that identity; integral_outer_rawLocalIntegrand_eq_nextState below performs the exact Fubini substitution.

def Anderson4D.R322AnalyticProperStepContext.blockIndex {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) : ExtractionBlockIndex ctx.pairing

The current concrete block as an actual extraction-block coordinate.

Equations

• ctx.blockIndex = ⟨ctx.step.2, ⋯⟩

def Anderson4D.R322AnalyticProperStepContext.standardBlockTuple {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (x : Fin (2 * q) → T4) : Fin (2 * residualBlockOrder ctx.step.2) → T4

An ambient tuple restricted to the current sparse block in increasing active order.

Equations

• ctx.standardBlockTuple x i = x ↑(ctx.blockOrderIso i)

theorem Anderson4D.R322AnalyticProperStepContext.extractionBlockPrimitiveSum_eq_standardBlock {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (ρ : SmoothCutoff) (ε : ℝ) (x : Fin (2 * q) → T4) : r322ExtractionBlockPrimitiveSum ρ ε ctx.pairing ctx.blockIndex x = ∑ κB : ↥(primitiveFullPairings (residualBlockOrder ctx.step.2)), primitiveCovarianceProduct ρ ε (residualBlockOrder ctx.step.2) (↑κB) (ctx.standardBlockTuple x)

The primitive covariance sum in the actual endpoint-fibre block product is literally the standard covariance sum on the sparse block tuple.

noncomputable def Anderson4D.R322AnalyticProperStepContext.rawLocalIntegrand {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (ρ : SmoothCutoff) (ε : ℝ) (u : T4) (t : Fin (2 * residualBlockOrder ctx.step.2) → T4) : ℝ

Local factor before recognizing the generalized closed J integrand. This is the exact chain-times-covariance form produced by the actual endpoint-fibre pointwise factorization.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.R322AnalyticProperStepContext.rawLocalIntegrand_eq_localIntegrand {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (ρ : SmoothCutoff) (ε : ℝ) (u : T4) (t : Fin (2 * residualBlockOrder ctx.step.2) → T4) : ctx.rawLocalIntegrand ρ ε u t = ctx.localIntegrand ρ ε u t

Exact pointwise recognition of the true primitive chain and covariance sum as the generalized closed-J local integrand.

theorem Anderson4D.R322AnalyticProperStepContext.rawLocalSpatialIntegral_mul_outer_eq_nextState {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (ρ : SmoothCutoff) (lam ε : ℝ) (u : T4) (outer : ℝ) (hstandard : MeasureTheory.Integrable (ctx.localIntegrand ρ ε u) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2)) => paperMeasure)) (hinternal : ∀ᵐ (p : T4 × T4) ∂paperMeasure.prod paperMeasure, ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder ctx.step.2))), MeasureTheory.Integrable (fun (v : Fin (2 * residualBlockOrder ctx.step.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder ctx.step.2) (↑κB) ctx.internalEdges (primitiveAssemble (residualBlockOrder ctx.step.2) ⋯ p.1 p.2 v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2 - 2)) => paperMeasure)) : (lamEps lam ε ^ (2 * residualBlockOrder ctx.step.2) * ∫ (t : Fin (2 * residualBlockOrder ctx.step.2) → T4), ctx.rawLocalIntegrand ρ ε u t * outer ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2)) => paperMeasure) = (ctx.nextState ρ lam ε).edges ctx.predecessorEdge u * outer

One reconstructed inner integral may carry any fixed outer factor.

theorem Anderson4D.R322AnalyticProperStepContext.integral_outer_rawLocalIntegrand_eq_nextState {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) {Ω : Type u_1} [MeasurableSpace Ω] (ν : MeasureTheory.Measure Ω) (ρ : SmoothCutoff) (lam ε : ℝ) (u : Ω → T4) (outer : Ω → ℝ) (hstandard : ∀ᵐ (ω : Ω) ∂ν, MeasureTheory.Integrable (ctx.localIntegrand ρ ε (u ω)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2)) => paperMeasure)) (hinternal : ∀ᵐ (p : T4 × T4) ∂paperMeasure.prod paperMeasure, ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder ctx.step.2))), MeasureTheory.Integrable (fun (v : Fin (2 * residualBlockOrder ctx.step.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder ctx.step.2) (↑κB) ctx.internalEdges (primitiveAssemble (residualBlockOrder ctx.step.2) ⋯ p.1 p.2 v)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2 - 2)) => paperMeasure)) : ∫ (ω : Ω), lamEps lam ε ^ (2 * residualBlockOrder ctx.step.2) * ∫ (t : Fin (2 * residualBlockOrder ctx.step.2) → T4), ctx.rawLocalIntegrand ρ ε (u ω) t * outer ω ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2)) => paperMeasure ∂ν = ∫ (ω : Ω), (ctx.nextState ρ lam ε).edges ctx.predecessorEdge (u ω) * outer ω ∂ν

Exact outer-Fubini substitution. The section-integrability premise is only almost everywhere in the genuine outer coordinate.