Ambient residual coordinates for the R-322 proper-step induction

After a proper prefix has been integrated, the variables which remain are the vertices of R322AnalyticEdgeState.active. The edge stored at an active left vertex connects it to the next active vertex, not necessarily to the next ambient index. This file supplies that successor, reconstructs one ambient block relative to its active successor, and proves the corresponding outer-Fubini update.

The relative block variable is translated back into the actual ambient tuple. Thus the theorem below does not identify an unintegrated original integrand with an already collapsed state.

The next vertex in a sparse active carrier

def Anderson4D.r322AnalyticSuccessorCandidates {q : ℕ} {hq : 1 ≤ q} (state : R322AnalyticEdgeState q hq) (i : Fin (2 * q)) : Finset (Fin (2 * q))

Active vertices strictly after i.

Equations

• Anderson4D.r322AnalyticSuccessorCandidates state i = {j ∈ state.active | i < j}

theorem Anderson4D.r322AnalyticSuccessorCandidates_nonempty {q : ℕ} {hq : 1 ≤ q} (state : R322AnalyticEdgeState q hq) (i : Fin (2 * q)) (hi : ↑i < 2 * q - 1) : (r322AnalyticSuccessorCandidates state i).Nonempty

There is a successor candidate whenever i lies before the global right endpoint.

def Anderson4D.r322AnalyticSuccessorVertex {q : ℕ} {hq : 1 ≤ q} (state : R322AnalyticEdgeState q hq) (i : Fin (2 * q)) (hi : ↑i < 2 * q - 1) : Fin (2 * q)

Least active vertex strictly after i.

Equations

• Anderson4D.r322AnalyticSuccessorVertex state i hi = (Anderson4D.r322AnalyticSuccessorCandidates state i).min' ⋯

theorem Anderson4D.r322AnalyticSuccessorVertex_mem_active {q : ℕ} {hq : 1 ≤ q} (state : R322AnalyticEdgeState q hq) (i : Fin (2 * q)) (hi : ↑i < 2 * q - 1) : r322AnalyticSuccessorVertex state i hi ∈ state.active

theorem Anderson4D.r322AnalyticSuccessorVertex_gt {q : ℕ} {hq : 1 ≤ q} (state : R322AnalyticEdgeState q hq) (i : Fin (2 * q)) (hi : ↑i < 2 * q - 1) : i < r322AnalyticSuccessorVertex state i hi

def Anderson4D.R322AnalyticProperStepContext.successorVertex {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) : Fin (2 * q)

The active successor immediately outside the right edge of this proper block.

Equations

• ctx.successorVertex = Anderson4D.r322AnalyticSuccessorVertex ctx.state ctx.step.1.2 ⋯

theorem Anderson4D.R322AnalyticProperStepContext.successorVertex_mem_active {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) : ctx.successorVertex ∈ ctx.state.active

theorem Anderson4D.R322AnalyticProperStepContext.stepRight_lt_successorVertex {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) : ctx.step.1.2 < ctx.successorVertex

theorem Anderson4D.R322AnalyticProperStepContext.predecessorVertex_not_mem_step {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) : r322AnalyticPredecessorVertex ctx.state ctx.step ⋯ ∉ ctx.step.2

The chosen predecessor is outside the block being integrated.

theorem Anderson4D.R322AnalyticProperStepContext.successorVertex_not_mem_step {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) : ctx.successorVertex ∉ ctx.step.2

The active successor is likewise outside the block.

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

Ambient value at the sparse predecessor.

Equations

• ctx.predecessorPoint x = x (Anderson4D.r322AnalyticPredecessorVertex ctx.state ctx.step ⋯)

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

Ambient value at the sparse successor.

Equations

• ctx.successorPoint x = x ctx.successorVertex

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

Translate the actual standard block tuple so that its active successor is at zero.

Equations

• ctx.translatedStandardBlockTuple x j = ctx.standardBlockTuple x j - ctx.successorPoint x

noncomputable def Anderson4D.R322AnalyticProperStepContext.reconstructRelativeBlockTuple {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (base : Fin (2 * q) → T4) (t : Fin (2 * residualBlockOrder ctx.step.2) → T4) : Fin (2 * q) → T4

Put a relative standard block tuple back into the ambient coordinates, using the actual active successor as translation anchor.

Equations

• ctx.reconstructRelativeBlockTuple base t = ctx.reconstructBlockTuple base fun (j : Fin (2 * Anderson4D.residualBlockOrder ctx.step.2)) => t j + ctx.successorPoint base

@[simp]

theorem Anderson4D.R322AnalyticProperStepContext.standardBlockTuple_reconstructRelativeBlockTuple {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (base : Fin (2 * q) → T4) (t : Fin (2 * residualBlockOrder ctx.step.2) → T4) : ctx.standardBlockTuple (ctx.reconstructRelativeBlockTuple base t) = fun (j : Fin (2 * residualBlockOrder ctx.step.2)) => t j + ctx.successorPoint base

@[simp]

theorem Anderson4D.R322AnalyticProperStepContext.predecessorPoint_reconstructRelativeBlockTuple {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (base : Fin (2 * q) → T4) (t : Fin (2 * residualBlockOrder ctx.step.2) → T4) : ctx.predecessorPoint (ctx.reconstructRelativeBlockTuple base t) = ctx.predecessorPoint base

@[simp]

theorem Anderson4D.R322AnalyticProperStepContext.successorPoint_reconstructRelativeBlockTuple {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (base : Fin (2 * q) → T4) (t : Fin (2 * residualBlockOrder ctx.step.2) → T4) : ctx.successorPoint (ctx.reconstructRelativeBlockTuple base t) = ctx.successorPoint base

@[simp]

theorem Anderson4D.R322AnalyticProperStepContext.translatedStandardBlockTuple_reconstructRelativeBlockTuple {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (base : Fin (2 * q) → T4) (t : Fin (2 * residualBlockOrder ctx.step.2) → T4) : ctx.translatedStandardBlockTuple (ctx.reconstructRelativeBlockTuple base t) = t

The actual local factor on an ambient residual tuple

noncomputable def Anderson4D.R322AnalyticProperStepContext.ambientLocalIntegrand {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (ρ : SmoothCutoff) (ε : ℝ) (x : Fin (2 * q) → T4) : ℝ

The local factor read from an actual ambient residual tuple.

The incoming edge reads the sparse predecessor, the internal chain reads the heterogeneous state edges, and the outgoing difference is anchored at the least active successor. Only the covariance sum of the current schedule block occurs here; all factors from the remaining suffix belong to the outer residual integrand.

Equations

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

theorem Anderson4D.R322AnalyticProperStepContext.ambientLocalIntegrand_eq_rawLocalIntegrand {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (ρ : SmoothCutoff) (ε : ℝ) (x : Fin (2 * q) → T4) : ctx.ambientLocalIntegrand ρ ε x = ctx.rawLocalIntegrand ρ ε (ctx.predecessorPoint x - ctx.successorPoint x) (ctx.translatedStandardBlockTuple x)

Translation by the actual active successor recognizes the ambient local factor as the exact raw local integrand consumed by the collapse theorem.

theorem Anderson4D.R322AnalyticProperStepContext.ambientLocalIntegrand_reconstructRelativeBlockTuple {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (ρ : SmoothCutoff) (ε : ℝ) (base : Fin (2 * q) → T4) (t : Fin (2 * residualBlockOrder ctx.step.2) → T4) : ctx.ambientLocalIntegrand ρ ε (ctx.reconstructRelativeBlockTuple base t) = ctx.rawLocalIntegrand ρ ε (ctx.predecessorPoint base - ctx.successorPoint base) t

On the translated ambient reconstruction, the actual local factor is literally the raw local factor at the predecessor-successor displacement.

Haar translation from actual to relative block coordinates

noncomputable def Anderson4D.R322AnalyticProperStepContext.residualBlockTranslation {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (a : T4) : (Fin (2 * residualBlockOrder ctx.step.2) → T4) ≃ᵐ (Fin (2 * residualBlockOrder ctx.step.2) → T4)

Simultaneous translation of every standard block coordinate.

Equations

• ctx.residualBlockTranslation a = MeasurableEquiv.piCongrRight fun (x : Fin (2 * Anderson4D.residualBlockOrder ctx.step.2)) => MeasurableEquiv.addRight a

@[simp]

theorem Anderson4D.R322AnalyticProperStepContext.residualBlockTranslation_apply {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (a : T4) (t : Fin (2 * residualBlockOrder ctx.step.2) → T4) : (ctx.residualBlockTranslation a) t = fun (j : Fin (2 * residualBlockOrder ctx.step.2)) => t j + a

theorem Anderson4D.R322AnalyticProperStepContext.measurePreserving_residualBlockTranslation {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (a : T4) : MeasureTheory.MeasurePreserving (⇑(ctx.residualBlockTranslation a)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2)) => paperMeasure) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2)) => paperMeasure)

Product Haar measure is invariant under the simultaneous block translation.

theorem Anderson4D.R322AnalyticProperStepContext.integral_actualBlock_eq_relativeBlock {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) (ρ : SmoothCutoff) (ε : ℝ) (base : Fin (2 * q) → T4) (outer : ℝ) : (∫ (actual : Fin (2 * residualBlockOrder ctx.step.2) → T4), ctx.ambientLocalIntegrand ρ ε (ctx.reconstructBlockTuple base actual) * outer ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2)) => paperMeasure) = ∫ (t : Fin (2 * residualBlockOrder ctx.step.2) → T4), ctx.ambientLocalIntegrand ρ ε (ctx.reconstructRelativeBlockTuple base t) * outer ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2)) => paperMeasure

The integral over actual block coordinates is exactly the integral over coordinates relative to the active successor.

One processed-prefix residual integral

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

The genuine pre-collapse integrand for one processed-prefix step, including an arbitrary factor depending only on the surviving outer coordinates.

Equations

• ctx.processedResidualIntegrand ρ ε base outer t = ctx.ambientLocalIntegrand ρ ε (ctx.reconstructRelativeBlockTuple base t) * outer

noncomputable def Anderson4D.R322AnalyticProperStepContext.processedResidualOuterIntegral {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) {Ω : Type u_1} [MeasurableSpace Ω] (ν : MeasureTheory.Measure Ω) (ρ : SmoothCutoff) (lam ε : ℝ) (base : Ω → Fin (2 * q) → T4) (outer : Ω → ℝ) : ℝ

The nested outer integral before one proper processed-prefix update.

Equations

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

noncomputable def Anderson4D.R322AnalyticProperStepContext.updatedResidualOuterIntegral {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) {Ω : Type u_1} [MeasurableSpace Ω] (ν : MeasureTheory.Measure Ω) (ρ : SmoothCutoff) (lam ε : ℝ) (base : Ω → Fin (2 * q) → T4) (outer : Ω → ℝ) : ℝ

The residual outer integral after the local block has been absorbed into the predecessor edge.

Equations

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

theorem Anderson4D.R322AnalyticProperStepContext.processedResidualOuterIntegral_eq_updated {q : ℕ} {hq : 1 ≤ q} (ctx : R322AnalyticProperStepContext q hq) {Ω : Type u_1} [MeasurableSpace Ω] (ν : MeasureTheory.Measure Ω) (ρ : SmoothCutoff) (lam ε : ℝ) (base : Ω → Fin (2 * q) → T4) (outer : Ω → ℝ) (hstandard : ∀ᵐ (ω : Ω) ∂ν, MeasureTheory.Integrable (ctx.localIntegrand ρ ε (ctx.predecessorPoint (base ω) - ctx.successorPoint (base ω))) (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)) : ctx.processedResidualOuterIntegral ν ρ lam ε base outer = ctx.updatedResidualOuterIntegral ν ρ lam ε base outer

Iterable processed-prefix Fubini headline.

One actual ambient block, reconstructed relative to its active successor, is integrated out and replaced by exactly the predecessor edge of nextState. The outer coordinate and its complete remaining factor are unchanged.

Connection to the actual endpoint fibre at the initial state

noncomputable def Anderson4D.r322InitialResidualIntegrand {q : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κ : PartialPairing (Fin (2 * q))) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (x : Fin (2 * q) → T4) : ℝ

The initial residual integrand is the exact analytic-head local factor times the complete suffix factor. At the initial state the active carrier is all vertices and every state edge is greenFn.

Equations

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

theorem Anderson4D.sum_endpointFiber_detJintegrand_eq_initialResidualIntegrand {q : ℕ} (ρ : SmoothCutoff) (ε : ℝ) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (x : Fin (2 * q) → T4) : ∑ τ : ReductionEndpointFiberAt κ, detJintegrand ρ ε q (↑τ) x = r322InitialResidualIntegrand ρ ε κ head tail hschedule x

The initial residual integrand is pointwise the actual endpoint-fibre sum, not a model integrand.

noncomputable def Anderson4D.r322InitialResidualOuterIntegral {q : ℕ} (hq : 1 ≤ q) (ρ : SmoothCutoff) (lam ε : ℝ) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (z : T4) : ℝ

Initial outer integral in standard coordinates for the first scheduled proper block. This is the residual object before any analytic absorption.

Equations

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

theorem Anderson4D.endpointFiberDetJSum_eq_initialResidualOuterIntegral {q : ℕ} (hq : 1 ≤ q) (ρ : SmoothCutoff) (lam ε : ℝ) (κ : PartialPairing (Fin (2 * q))) (hκ : κ ∈ nonSplitPairings q) (head : R322ExtractionStep (2 * q)) (tail : List (R322ExtractionStep (2 * q))) (hschedule : r322AnalyticSchedule κ = head :: tail) (hproper : head.1 ≠ r322WholeEndpoint q hq) (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 = r322InitialResidualOuterIntegral hq ρ lam ε κ hκ head tail hschedule hproper z

Actual-fibre initial headline. Spatial Fubini and the measure-preserving block reindex identify endpointFiberDetJSum with the initial processed residual outer integral.